feat(bz): word-sized Montgomery residue ring and CLD kernel#8697
Open
kim-em wants to merge 13 commits into
Open
feat(bz): word-sized Montgomery residue ring and CLD kernel#8697kim-em wants to merge 13 commits into
kim-em wants to merge 13 commits into
Conversation
Measured the SD4 recovery modulus (11^13, ~45 bits, not near 2^64) and a 1.8x byte-identical native-Montgomery cldQuotientMod prototype; posted findings + re-scope recommendation on the issue rather than landing a proof-only WordPolyMod layer as dead code. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…< 2^64 Add `Hex.WordMod ctx`, residues modulo an odd `m < 2^64` stored in Montgomery form on top of `HexArith.MontCtx`. Multiplication is a single `mulMont` reduction; addition and subtraction are full-range modular operations built from `UInt64.addCarry`/`subBorrow`, so the whole odd `m < 2^64` range is supported (unlike `ZMod64`, capped at 2^31). Every operation has a proven `toNat` characterisation modulo m; the additive specs use `MontCtx.cancel_word_mod_of_lt`, now exposed from the Montgomery context. This is the scalar layer (Phase 1) for the word-sized poly-mod-p^a arithmetic of the Berlekamp-Zassenhaus lattice tier (#8691), measured byte-identical and 1.8x faster than the Int/bignum path at the SD4 recovery modulus. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ientMod Add `Hex.cldQuotientModWord?`, the CLD quotient `(f · g') / g mod p^a` for a monic `g`, computed over `WordMod` (single-reduction Montgomery poly arithmetic) whenever the guard `Odd (p^a) ∧ p^a < 2^64` holds and declining otherwise. `powLtWord?` checks `p^a < 2^64` with early exit so a huge exponent never materialises a bignum. Give `WordMod` the `NatCast` and (monic-only) `Div` instances the dense-poly `derivative`/`divMod` need. Conformance `#guard`s in HexBerlekampZassenhaus.Conformance pin the kernel byte-identical to the bignum `cldQuotientMod` (SD3/√2+√3 cores, moduli 7^5, 11^13, 5^9) and confirm the guard declines on 11^400. The correspondence proof and `@[csimp]` wiring are the next phases (#8691). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
kim-em
changed the title
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Add `HexModArithMathlib.WordMod.toZMod : Hex.WordMod ctx → ZMod m.toNat` with its injectivity and the homomorphism laws (`toZMod_zero/one/add/mul/neg/sub`), mirroring the existing `ZMod64` bridge. This is the Phase-2 foundation for the byte-identical CLD correspondence (#8691): the next steps bundle a Mathlib `CommRing (WordMod ctx)` and `≃+* ZMod` through this map, then transport the word-sized and bignum CLD quotients into `Polynomial (ZMod (p^a))` to prove them equal under the guard. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Give the executable `WordMod ctx` a Mathlib `CommRing` structure, pulled back along the injective `toZMod` via `Function.Injective.commRing` (adding the `SMul ℕ/ℤ`, `Pow ℕ`, `IntCast` data with immediate transport proofs), and package `toZMod` as `toZModRingHom : WordMod ctx →+* ZMod m.toNat`. This is the algebraic backbone for the Phase-2 CLD correspondence (#8691): the remaining step transports both quotients through `DensePoly.toPolynomial` + `Polynomial.map` into `Polynomial (ZMod (p^a))` and proves them equal via monic-division uniqueness. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…roof Add the coefficient casts `cZ`/`cW` from executable integer / `WordMod` polynomials into `ZMod (p^a)[X]` with their homomorphism laws, the canonical-representative uniqueness lemma `eq_of_cZ_eq`, and the central `map_divMod_monic`: monic dense-polynomial division commutes with any coefficient ring hom (via `Polynomial.div_modByMonic_unique`). These are the reusable pieces the byte-identical `cldQuotientMod = cldQuotientModWord?` equality (#8691, Phase 2) assembles from. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Add the intCast-of-intModNat cast lemma, the cW-of-toW-mapped = cZ bridge, the reduceModPow-vanishing lemma, and derivative-commute for both casts. With the transport lemma these reduce the byte-identical CLD equality (#8691) to numerator/divisor agreement in ZMod (p^a)[X] plus monic-division uniqueness. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Refactor powLtWord?'s inner loop into a named @[expose] powLtWordAux, prove it computes p^a and stays below 2^64 (powLtWord?_eq), and add toPoly_degree_lt transporting the dense remainder-degree bound into Polynomial.degree. These are the last supporting lemmas before assembling the cldQuotientMod equality (#8691). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…embly Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
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.
This PR adds the word-sized Montgomery arithmetic layer for the Berlekamp-Zassenhaus lattice tier, issue #8691 "perf(bz): word-sized modulus arithmetic for the lattice tier's lift and CLD stages", in two proven-and-tested steps.
Hex.WordMod ctxis a residue ring modulo an oddm < 2^64stored in Montgomery form on top ofHexArith.MontCtx. Multiplication is a singlemulMontreduction; addition and subtraction are full-range modular operations built fromUInt64.addCarry/subBorrow, so the whole odd-m < 2^64range is supported (unlikeZMod64, which caps at2^31). Every operation carries a proventoNatcharacterisation modulom(toNat_mulfromMontCtx.mulMont_repr;toNat_add/toNat_sub/toNat_negvia a word-cancellation lemma,MontCtx.cancel_word_mod_of_lt, which this PR exposes from the Montgomery context). Nosorry, noaxiom.Hex.cldQuotientModWord?then computes the CLD quotient(f · g') / g mod p^afor a monicgoverWordModwhenever the guardOdd (p^a) ∧ p^a < 2^64holds, declining (returningnone) otherwise;powLtWord?checksp^a < 2^64with early exit so a huge exponent never materialises a bignum. Conformance#guards pin it byte-identical to the bignumcldQuotientModon the SD3 and √2+√3 cores at moduli7^5,11^13,5^9, and confirm the guard declines on11^400.Before building this I measured the premise: at the actual SD4 recovery point the modulus is
11^13(about 45 bits, not near2^64as the issue framed it, because #8395 early-termination stops the doubling schedule short), and a native-Montgomery prototype ofcldQuotientModthere is byte-identical to the currentInt/DensePolypath and 1.8x faster (the~90-bit intermediate products in theIntpath heap-allocate as GMP; Montgomery keeps them in words). Full measurement and the@[csimp]routing plan are on the issue.Follow-up (its own PR): prove
cldQuotientMod = cldQuotientModWord?-under-guard in the*Mathliblayer (via theDensePoly.toPolynomialring-equiv, aWordMod →+* ZMod (p^a)hom, and monic-division uniqueness), then wire the fast path with@[csimp]and re-measure. The runtime win lands there; this PR is the proven, conformance-checked foundation. The kernel is deliberately in its own module so the eventual@[csimp]inLattice.leanimports it without a cycle.🤖 Prepared with Claude Code