modinv62 - #37
Draft
dannywillems wants to merge 8 commits into
Draft
modinv62#37dannywillems wants to merge 8 commits into
dannywillems wants to merge 8 commits into
Conversation
The mathematical core of safegcd, in the eta form that libsecp256k1's modinv64 uses: a divstep sends (f, g) to M (f, g) / 2 for one of three integer matrices of determinant 2, selected by the parity of g and the sign of eta. Composing n of them gives a single transition of determinant 2^n that turns n halvings into one exact division by 2^n, which is what licenses a batched implementation: read the branch decisions off the bottom limbs, accumulate the matrix, then apply it once at full width. run_spec proves the facts such an implementation rests on, by induction on n: the determinant is exactly 2^n, both divisions are exact, and f stays odd. Invariance of the gcd then comes out of the adjugate identity adj T . T = (det T) I rather than out of a per-step induction, which is what run_inv_f and run_inv_g record: the original pair is an integer combination of the final one. So once g reaches 0 the terminal f divides both inputs, and with coprime inputs it is +/-1, the sign the inversion driver reads. Co-authored-by: Claude <noreply@anthropic.com>
The driver of libsecp256k1's secp256k1_modinv64_var, specified and proved at the level of integers: f and g run the divstep recurrence while a pair of coefficients d and e tracks, modulo m, how the current f and g were built from the input. The scaled invariants carried across batches are X d = seed f and X e = seed g (mod m). They hold at the start for trivial reasons, and step_good shows that a batch preserves them; at termination g = 0 and, by run_eq_one_or_neg_one, f = +/-1, so the sign-corrected d satisfies X d = seed (mod m). That is invert_spec. The seed is a genuine parameter of the algorithm, and that is the point. Seeding with 1 gives the classical inverse; seeding with R^2 mod m gives R^2 / X, which for a Montgomery representative X = aR is exactly a^-1 R, the Montgomery representative of the inverse. The "no Montgomery conversion" trick of zcash/pasta_curves#119 is therefore proved in the generality in which it actually holds, for any modulus, batch width and seed. This is partial correctness. Totality, that g reaches 0 within the batch budget, is the Bernstein-Yang iteration bound and is not proved here; the driver returns none instead of looping, so the theorem is unconditional on it. Co-authored-by: Claude <noreply@anthropic.com>
divsteps_62_var of zcash/pasta_curves#119, transcribed into Lean with UInt64 standing for u64 (both wrap modulo 2^64) and Int for i64 where the Rust value is exact. Every declaration carries a line-anchored link into the Rust it came from, pinned at the pull request's head commit rather than at the branch, so the line numbers stay valid once the branch moves. The kernel is not proved equal to the recurrence; it is checked against it, on 512 pseudo-random single-word samples and on boundary eta values, comparing the matrix and the updated eta. Three things make that check sharp: the kernel compresses a variable number of divsteps into each inner iteration, it reads only the bottom words, so agreement on the full integers is exactly the claim that no more than that is needed, and it returns eta, so a drift in the branch schedule cannot hide. The two magic modular inverses the compression rests on are finite claims about a word modulo a small power of two, so they are proved outright rather than checked: f + (((f + 1) & 4) << 1) inverts f modulo 16, and f (f f - 2) inverts -f modulo 64. negative_eta_multiplier is deliberately not ported. It is an inline(never) helper that exists only to stop the AArch64 backend speculatively evaluating both cancellation formulas, and it computes exactly the expression it replaces; there is no Lean counterpart to a codegen barrier, and nothing to check. Co-authored-by: Claude <noreply@anthropic.com>
The rest of zcash/pasta_curves#119: pack62, unpack62, update_fg_62_var, update_de_62, normalize_62, is_zero, shrink_len and the driver, together with the first-batch, sparse-modulus and terminal specializations. Where the proved driver applies a batch's transition to (f, g) and (d, e) as single integers, these apply it limb by limb over five limbs. How the Rust types are modelled is set out in the module header. Every value the Rust holds in an i64 or an i128 is in range, so plain Int arithmetic is faithful; the places that genuinely rely on wrapping go through UInt64. The mask (x as u64 & MASK62) as i64 and the arithmetic shift x >>= 62 become low62 and shr62, which for the positive divisor 2^62 are exactly Lean's Euclidean % and /, and low62_add_shr62 records the decomposition they satisfy. Also ported is ref_update_de, the generic-modulus reference from the Rust test module, which multiplies by every modulus limb including the zero one. It exists so that the sparse kernels can be checked limb-exact against something other than themselves, and specializationsAgree walks a real inversion doing exactly that at every batch. Nothing here is proved. The limb layer is a representation of the integers the proof is about, so the honest claim for it is agreement with the proved layer, which the Pasta instantiation establishes by computation. Co-authored-by: Claude <noreply@anthropic.com>
pallasInv and vestaInv take their modulus from Fields.Pasta, their seed as 2^512 mod m, and their inverse of 2^62 as ((m + 1) / 2)^62, which is right because (m + 1) / 2 is 2^-1 for odd m. None of that is a magic constant, so the port's own hardcoded radix-2^62 MODULUS, MU and R2 can be checked against the derivations rather than restated, which is what fp_modulus_limbs_eq and its siblings do by kernel computation. The checks then replay the port's pinned regression vectors. For each, the proved driver must return the Fermat inverse, an oracle sharing no code with divsteps, and consume exactly the number of 62-divstep batches the port pins. All twelve reproduce. The batch counts are the sharpest of these: a count is a function of the whole divstep trajectory, so reproducing one from an independent implementation of the recurrence pins the eta convention, the branch selection, the batch width and the termination test at once. The limb layer is then checked against the proved integer driver on those vectors, on pseudo-random field elements and on boundary representations, value and batch count both. The Rust test module's own differential obligations are reproduced alongside: the specializations against the generic-modulus reference, normalize_62 against a value-level specification of what normalization means, and the pack62 round trip. Co-authored-by: Claude <noreply@anthropic.com>
The SafeGCD modules are already built by the CompElliptic.* glob, so this only puts them on the umbrella module's surface, alongside the other field material. Co-authored-by: Claude <noreply@anthropic.com>
The general theory, the divstep recurrence and its invertibility over the integers together with the correctness of the inversion driver, is quantified over every parameter set and every input, so it must not reach beyond the standard axioms. The concrete Pasta facts beneath it are closed numeric claims the kernel evaluates directly, so they add nothing either. Both tiers therefore take a plain assert_axioms with no flags: nothing in this development reaches native_decide, and the checks that are not proofs are #guard evaluations, which contribute no axioms at all. Co-authored-by: Claude <noreply@anthropic.com>
Co-authored-by: Claude <noreply@anthropic.com>
dannywillems
marked this pull request as draft
September 25, 2026 10:44
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.