Skip to content

Additional general-size modulus operations for secp256k1#358

Open
jargh wants to merge 9 commits into
awslabs:mainfrom
jargh:secp
Open

Additional general-size modulus operations for secp256k1#358
jargh wants to merge 9 commits into
awslabs:mainfrom
jargh:secp

Conversation

@jargh
Copy link
Copy Markdown
Contributor

@jargh jargh commented Feb 25, 2026

This is a direct response to issue #356, addressing one of several items raised there.

The "co-authored by" in the commit messages is false modesty - code and proofs were 100% written by Claude.

jrh13 and others added 4 commits February 25, 2026 00:15
Add bignum_mod_p256k1 (field characteristic reduction) and
bignum_mod_n256k1 (group order reduction) for secp256k1,
supporting arbitrary input sizes via iterative long division.
Includes ARM assembly, HOL Light formal proofs, tests, and
benchmark hooks.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
HOL Light formal verification proofs for the x86-64 implementations of
reduction modulo the secp256k1 field characteristic (p_256k1) and group
order (n_256k1). Both proofs cover standard and Windows ABI variants
with IBT/non-IBT subroutine wrappers.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants