From 5234e2d9e0a5fa96dcc192f2b12bd62d20fa8849 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 1 Sep 2026 08:43:35 +0000 Subject: [PATCH 1/2] =?UTF-8?q?docs:=20specify=20Sch=C3=B6nhage=20radix-3?= =?UTF-8?q?=20multiplication=20and=20its=20cslib=20complexity=20companion?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This commit specifies Schönhage's 1977 radix-3 multiplication algorithm across three SPECs: triadic reference semantics, the fixed-length carrier, the proof-carrying schedule, and the generic plan as hex-poly-fast amendments; the packed F_2[x] kernel, the schoolbook/Karatsuba/Schönhage dispatch ladder, and the dense-correspondence refinement ladder as hex-gf2 amendments; and hex-poly-fast-cslib, the first -cslib companion library, holding operation-count bounds in cslib's query-complexity framework with operation-parametric workers, specialization theorems, and proved cost obliviousness. Index, future-work, and design-principles entries updated. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_018S4hrFX6e8B8s56182nAp4 --- HexGF2/SPEC/hex-gf2.md | 118 +++++++++- HexPolyFast/SPEC/hex-poly-fast.md | 219 ++++++++++++++++++- SPEC/Libraries/README.md | 48 +++- SPEC/Libraries/hex-poly-fast-cslib.md | 302 ++++++++++++++++++++++++++ SPEC/design-principles.md | 7 + SPEC/future-work.md | 28 +++ 6 files changed, 699 insertions(+), 23 deletions(-) create mode 100644 SPEC/Libraries/hex-poly-fast-cslib.md diff --git a/HexGF2/SPEC/hex-gf2.md b/HexGF2/SPEC/hex-gf2.md index f437ae4e6..811a9aef6 100644 --- a/HexGF2/SPEC/hex-gf2.md +++ b/HexGF2/SPEC/hex-gf2.md @@ -1,4 +1,4 @@ -# hex-gf2 (GF(2) packed arithmetic, depends on hex-basic) +# hex-gf2 (GF(2) packed arithmetic, depends on hex-basic, hex-poly, hex-poly-fast, hex-mod-arith) Packed bitwise representation of polynomials over F_2. Addition is XOR, multiplication uses carry-less multiply. Substantially faster @@ -34,9 +34,10 @@ it costs one scan of the top word and makes equality of elements equality of word arrays (`GF2Poly.ext_words`). - Addition: word-by-word XOR -- Multiplication: schoolbook or Karatsuba on 64-bit blocks, where - each block multiply uses carry-less multiply via `@[extern]` - calling a C wrapper that uses CLMUL on x86 (with compile-time +- Multiplication: a three-rung dispatch (see §Multiplication ladder): + schoolbook on 64-bit blocks, Karatsuba on 64-bit blocks, and the packed + Schönhage kernel, where each block multiply uses carry-less multiply via + `@[extern]` calling a C wrapper that uses CLMUL on x86 (with compile-time feature detection) and a portable shift-and-XOR fallback on other architectures. - Division with remainder (for polynomial GCD, modular reduction) @@ -107,6 +108,104 @@ compilations rather than one: individually; `HEX_CLMUL_NO_LEAN` drops the export wrapper so the self-test needs no Lean runtime. +## Multiplication ladder + +`GF2Poly.mul` is defined as the word-schoolbook convolution (`mulWords` with +clmul block products), and every existing theorem is stated against that +definition. The runtime is a proof-backed `@[csimp]` replacement that +dispatches by operand word count: + +1. word schoolbook (`mulWords`), below the first crossover; +2. Karatsuba on 64-bit blocks, splitting at word boundaries so the block + products are again `mulWords` calls; +3. the packed Schönhage kernel, above the second crossover. + +Both crossovers are benchmark-committed under the adoption law of +[hex-poly-fast §Benchmarking and production dispatch](../../HexPolyFast/SPEC/hex-poly-fast.md): +a rung enters the committed table only when its cells win on this library's +own ladder, and the logical definition, the coefficient theorems, and every +caller-visible statement are unchanged by dispatch. + +### Dense correspondence + +The fast rungs are proved through the dense representation. `FpPoly 2` is +`DensePoly (ZMod64 2)`, so the pair of Mathlib-free conversions + +```lean +def GF2Poly.toFpPoly : GF2Poly → FpPoly 2 +def GF2Poly.ofFpPoly : FpPoly 2 → GF2Poly +``` + +with round-trip laws and coefficient agreement (`(toFpPoly p).coeff i` is +bit `i % 64` of word `i / 64`) lets each packed operation land on the +corresponding `DensePoly` operation. The `≃+*` packaging of this pair stays +in hex-gf2-mathlib; the conversions and their operation-preservation lemmas +are Mathlib-free and live here. This is what the new hex-poly and +hex-poly-fast dependencies are for. The existing ring-law theorems +(`mul_assoc`, `mul_comm`, `left_distrib`, and companions) are bundled into a +`Lean.Grind.CommRing GF2Poly` instance so `DensePoly GF2Poly` and generic +plan machinery apply to the packed type. + +### Packed Schönhage kernel + +The kernel mirrors the generic algorithm of +[hex-poly-fast §Schönhage's radix-3 algorithm](../../HexPolyFast/SPEC/hex-poly-fast.md) +rung for rung: same `SchoenhageSchedule`, same transform shape, same +recursion. In characteristic two the inverse-of-three witness is `1` and +subtraction is XOR, so every carrier operation is a shift-and-XOR loop. + +The packed carrier holds a residue modulo `y^(2L) + y^L + 1` in +`ceil(2L / 64)` words with the unused top bits of the last word zero. +`L` is generally not a multiple of 64 +(Brent-Gaudry-Thomé-Zimmermann §3.2), and the kernel must not round it up: +the primitives are arbitrary-bit operations, not word-aligned ones. +Required packed primitives, each with an unpacking lemma identifying it +with the corresponding `Triadic (ZMod64 2) L` operation: + +- addition as overlap-safe XOR accumulation; +- multiplication by `y^j`: an arbitrary-bit left shift crossing word + boundaries, followed by the wrap of bits at exponent `2L` and above into + XOR contributions at exponents reduced by the relation + `y^(2L) = y^L + 1`, followed by the final-word mask; +- conversion between packed blocks of a `GF2Poly` and carrier values; +- the pointwise product, which recurses through the dispatcher. + +Correctness is a refinement ladder, not one whole-algorithm equality: + +1. each packed primitive equals its `Triadic (ZMod64 2) L` counterpart + under unpacking; +2. the packed transform equals the symbolic radix-3 transform under + elementwise unpacking; +3. the packed kernel equals `schoenhagePlan`'s product under `toFpPoly`; +4. the final theorem restates 3 against this library's own convolution + coefficient semantics: the kernel's output coefficients are the + carry-less convolution of the inputs. + +Step 4 is the statement the dispatcher's `@[csimp]` proof consumes, so +dispatch never depends on the dense detour at runtime. + +No operation-count theorem is claimed for the packed kernel. The +coefficient-operation bound in +[hex-poly-fast-cslib](../../SPEC/Libraries/hex-poly-fast-cslib.md) is about +the generic algorithm; one packed XOR performs 64 coefficient additions at +once, so a word-level cost model is a different theorem, reserved for a +possible later hex-gf2-cslib companion. + +### Conformance and benchmarks for the ladder + +The conformance stream gains multiplication fixtures whose operand sizes +bracket both committed crossovers, forced-rung cases for each of the three +rungs on shared inputs, and carrier cases at an `L` not divisible by 64. +The oracles are the existing NTL `GF2X` driver and python-flint at `p = 2`, +registered in the existing single CI job. + +The bench ladder extends the multiplication family until the +Karatsuba/Schönhage crossover is bracketed on the reference host. NTL/gf2x +remains the informational external comparator; once the Schönhage rung is +committed, its multiplication cells compare like against like +(gf2x's large-degree multiplication is this same algorithm family), and the +ratios feed the crossover table rather than Phase 4. + **GF(2^n) elements.** Elements of `GF(2^n)` are polynomials of degree < n over F_2, reduced modulo an irreducible of degree n. This library provides the optimized representations and operations; the convenience @@ -233,11 +332,12 @@ NTL is the speed reference for hand-tuned `GF(2)[x]` arithmetic. The measured NTL 11.6.0 build links gf2x 1.3.0 for large multiplication; NTL's `GF2X` source uses tuned base cases and Karatsuba/gf2x multiplication, crossover-based division and remainder, and switches its GCD to `HalfGCD` above the configured -crossover. Hex uses packed schoolbook -multiplication, long division and remainder, and Euclidean GCD. -Those operations therefore have different complexity classes at -the upper end of the ladder; their ratios orient future optimization -but do not gate Phase 4. Addition has the same linear packed-word +crossover. Hex currently implements packed schoolbook multiplication, long +division and remainder, and Euclidean GCD. §Multiplication ladder specifies +the Karatsuba and Schönhage rungs that put multiplication in the same +complexity class as gf2x; until they land, and for division and GCD +throughout, the ratios compare different complexity classes at the upper end +of the ladder. They orient future optimization but do not decide Phase 4. Addition has the same linear packed-word kernel shape, but the hex-framed driver measures serialization rather than raw NTL addition, so its paired registrations are correctness and protocol anchors rather than performance evidence. The comparator is diff --git a/HexPolyFast/SPEC/hex-poly-fast.md b/HexPolyFast/SPEC/hex-poly-fast.md index 3fcf88972..fca6f4f21 100644 --- a/HexPolyFast/SPEC/hex-poly-fast.md +++ b/HexPolyFast/SPEC/hex-poly-fast.md @@ -81,7 +81,9 @@ In scope: - explicit lawful multiplication plans; - schoolbook and Karatsuba full products, squaring, unbalanced products, and arbitrary clipped products; -- cyclic and negacyclic products with positive length; +- cyclic, negacyclic, and triadic products with positive length; +- the fixed-length triadic carrier, the symbolic radix-3 transform, the + proof-carrying Schönhage schedule, and the Schönhage multiplication plan; - reversal and fixed-precision `TSeries` bridges; - Newton reciprocal precomputation and fast monic/field division; - half-gcd, gcd, full extended gcd, and one-sided extended gcd; @@ -105,7 +107,16 @@ Out of scope: requirements; - a `PolyOps` abstraction over dense and sparse representations; - Toom-Cook before a measured gap remains between Karatsuba and the - coefficient-specific kernels; + coefficient-specific kernels. The Schönhage plan below is not subject to + this deferral: over coefficient rings with no suitable roots of unity + (`F_2` and its extensions), the word-prime radix-2 NTT path cannot be + instantiated, so no coefficient-specific kernel covers the regime the + radix-3 algorithm addresses, and the complexity-class gap against + NTL/gf2x is already recorded in + [hex-gf2 §External comparators](../../HexGF2/SPEC/hex-gf2.md); +- additive FFTs (Cantor, Gao-Mateer) and the wrapped-product splitting + reconstruction of Brent-Gaudry-Thomé-Zimmermann §3.3; +- integer Schönhage-Strassen multiplication; - a limb-level arbitrary-precision integer middle product; - multivariate multiplication, sparse interpolation, or polynomial-matrix approximant bases; @@ -241,6 +252,146 @@ hex-poly-fp may compute these operations directly with an NTT plan. The generic fold remains the reference and fallback, so the direct path needs no new algebraic semantics. +### Triadic products + +The triadic product is the ordinary product modulo `x^(2m) + x^m + 1`. It is +the third reference family beside the cyclic and negacyclic folds, and it is +the algebraic object of Schönhage's radix-3 multiplication algorithm: in the +quotient by `x^(2m) + x^m + 1` the residue of `x` has multiplicative order +`3m`, which supplies synthetic roots of unity over coefficient rings that +have none of their own. + +The reference fold maps input exponent `i` to `r = i % (3 * m)`. When +`r < 2 * m` the coefficient is added at slot `r`. Otherwise +`x^r = -x^(r - m) - x^(r - 2*m)`, so the coefficient is subtracted at slots +`r - m` and `r - 2*m`. As with the other two families, a proof-taking API +requires `0 < m`, checked forms return `none` at `m = 0`, and the theorems +identify the fold with the canonical remainder modulo the monic +`x^(2m) + x^m + 1` and bound its size by `2 * m`. + +### Schönhage's radix-3 algorithm + +The Schönhage plan computes full products through triadic products. It works +over any commutative ring with an explicit inverse of three; over `F_2` and +its extensions that witness is `1`, because three is odd. Subtraction is +already required by Karatsuba, so the plan signature adds only the +invertibility witness. + +**The fixed-length carrier.** Transform values are residues modulo +`y^(2L) + y^L + 1` held at fixed shape: + +```lean +structure Triadic (R : Type u) [DecidableEq R] [Lean.Grind.CommRing R] + (L : Nat) where + coeffs : Vector R (2 * L) +``` + +`Triadic` values are never normalized: trimming would make control flow +depend on coefficient values and would break the fixed-shape invariants the +transform relies on. The carrier has explicit addition, subtraction, +multiplication by `y^j` for `0 <= j < 3 * L` (a fold of index shifts and +sign flips with no ring multiplications), a full multiply-and-reduce that +consumes a supplied plan, and conversions to and from `DensePoly`. Its +agreement theorems identify each operation with the triadic reference fold +of the corresponding polynomial operation. A bundled ring instance on +`Triadic R L` is not required; the explicit operations carry the laws. + +**The schedule.** Parameter selection is a proof-carrying structure, not +arithmetic scattered through the recursion. For a target triadic product +modulo `x^(2N) + x^N + 1`: + +```lean +structure SchoenhageSchedule (N : Nat) where + k : Nat -- transform radix exponent; K = 3^k + M : Nat -- block length + L : Nat -- inner carrier half-length + k_pos : 0 < k + blocks : N = 3 ^ k * M + block_fits : M ≤ L + aligned : 3 ^ k ∣ L + decreasing : L < N +``` + +`blocks` splits the `2N`-coefficient representative into `2 * 3^k` blocks of +length `M`. `aligned` makes the root exponent `L / 3^k` an integer, so the +residue `ω = y^(L / 3^k)` of the inner carrier satisfies `ω^(3K) = y^(3L) = 1` +with `ω^K = y^L ≠ 1`, and the identity `1 + ω^K + ω^(2K) = 0` needed by the +transform's cancellations is exactly the defining relation of the carrier. +The `2K` evaluation points are the powers `ω^j` with `j` not divisible by +three; the transform reaches them as two radix-3 length-`K` transforms of +`ω`-twisted block sequences, and every twiddle multiplication is a +`mulByYPow` fold. `block_fits` makes the inner carrier hold each wrapped +block sum exactly. `decreasing` is the strict-decrease fact that drives the +well-founded recursion. `schedule? : Nat → Option (SchoenhageSchedule N)` +chooses `k` so that `L` is near `sqrt N` (the balanced choice behind the +`log log` recursion depth); correctness must not depend on which valid +schedule is chosen, only on the fields above. `L` is in general not a +multiple of the word size, and the packed kernel in hex-gf2 must not round +it up to one (Brent-Gaudry-Thomé-Zimmermann §3.2). + +**The recursion.** One triadic product modulo `x^(2N) + x^N + 1` with a +valid schedule reduces to `2 * 3^k` pointwise triadic products modulo +`y^(2L) + y^L + 1`, glued by forward and inverse symbolic transforms whose +twiddle multiplications are `mulByYPow` folds, plus the inverse scaling, +which multiplies by powers of the inverse-of-three witness. Recursive calls +multiply the pointwise operands through the same plan at half-length `L`; +when `schedule?` returns `none` or the size is below the committed cutoff, +the recursion delegates to a supplied base plan. Termination is by +`decreasing`. + +**The public plan.** + +```lean +def schoenhagePlan (base : MulPlan R) (cutoff : Nat) + (inv3 : R) (inv3_spec : 3 * inv3 = 1) : MulPlan R +``` + +The full product pads to the least scheduled `2N` with +`a.size + b.size - 1 ≤ 2 * N`, computes the triadic product, and reads the +ordinary product off the residue, which is exact because the true product +has degree below the modulus degree. `square` is `mul a a` and `slice` is +`coeffSlice` of the full product. Both choices are deliberate and accepted +under the no-placeholder rule: a transform-based product computes every +output coefficient at once, so a specialized square or slice saves at most a +constant factor, and the Karatsuba plan's pruned slice remains the tool for +clipped products in its own range. `mul_eq`, `square_eq`, and `coeff_slice` +are the plan laws, stated as always against schoolbook semantics. + +### Operation-parametric workers + +The counted models of this library's algorithms, their cost-obliviousness +properties, and their operation bounds are specified in +[hex-poly-fast-cslib](../../SPEC/Libraries/hex-poly-fast-cslib.md). A bound +proved about a program that merely returns the same polynomial would be +vacuous, because every lawful plan returns the same polynomial. The +faithfulness mechanism is that each counted algorithm body is written +exactly once, parametric over a monad and its coefficient operations: + +```lean +structure CoeffOps (m : Type → Type) (R : Type) where + add : R → R → m R + sub : R → R → m R + mul : R → R → m R + +def idOps : CoeffOps Id R + +def karatsubaWorker [Monad m] (ops : CoeffOps m R) (cutoff : Nat) : + Nat → Array R → Array R → m (Array R) + +def schoenhageWorker [Monad m] (ops : CoeffOps m R) ... : m (Array R) +``` + +The `idOps` instantiations are the executable definitions: the Karatsuba +recursion and the Schönhage recursion of this SPEC are *defined as* their +workers at `idOps`, so a theorem about a worker is a theorem about the +algorithm this library performs, not about a parallel reformulation. The +companion instantiates the same workers at a free-monad operations record +and counts queries. Workers cover the public dispatch structure (cutoffs, +the balanced and blocked Karatsuba paths, schedule selection), not only the +balanced textbook recursion. The raw array runtimes remain connected by the +existing output-equality `@[csimp]` theorems; operation counts are claims +about the workers, and the SPEC does not claim them for the raw runtimes. + ## Reversal and truncated series For a polynomial `f` and precision `n`, reversal reads the coefficient below @@ -658,6 +809,10 @@ Let `M(n)` be the measured balanced multiplication cost of the selected plan. | schoolbook full product | `O(n^2)` coefficient operations | | Karatsuba full/square | `O(n^(log₂ 3))` | | unbalanced `m x n`, `m >= n` | `O(ceil(m/n) * M(n))` | +| triadic reference fold | `O(n)` coefficient operations | +| `Triadic.mulByYPow` | `O(L)` coefficient additions, no ring multiplications | +| symbolic radix-3 transform | `O(K log K)` carrier additions and `mulByYPow` folds | +| Schönhage full product | `O(n log n log log n)` coefficient operations | | radix-2 NTT convolution | `O(n log n)` word operations | | reciprocal and division | `O(M(n))` | | half-gcd / extended gcd | `O(M(n) log n)` | @@ -671,6 +826,13 @@ remainder-tree node, pads an unbalanced product to the longer size, or rebuilds an NTT root table inside each transform violates the SPEC even if it returns the correct polynomial. +The Schönhage recursion adds its own body-shape constraints. The schedule is +computed once per level, never inside the transform loops. Twiddle +multiplications are `mulByYPow` folds; a twiddle implemented as a carrier +product violates the SPEC. `Triadic` values are never trimmed or normalized +between transform stages, and transform scratch is reused across butterflies +at one level rather than allocated per butterfly. + ## Kernel exposure and trust The logical closure consists of schoolbook polynomial operations, the @@ -695,7 +857,8 @@ hexpolyfast_emit_fixtures` emits the committed - `mul`, `square`, and `slice`; the `z_dispatch` result additionally reports the kernel selected by its public dispatcher; - `divmod`, `gcd`, `xgcd`, and `xgcd_left`; -- `cyclic` and `negacyclic`; +- `cyclic`, `negacyclic`, and `triadic`; +- forced-Schönhage `mul` cases across schedule boundaries; - `eval_many` and `interpolate`; - `pade` with the homogeneous relation and normalized success/failure; - NTT plan, round-trip, direct convolution, and CRT convolution cases; @@ -714,6 +877,10 @@ Mandatory edge families: - operand ratios from balanced through at least 64:1; - empty, one-coefficient, last-coefficient, and wholly out-of-range slices; - positive and negative coefficients at every Kronecker digit bound; +- triadic length `m = 1`, exponents in every residue class modulo `3 * m`, + and inputs whose reduction cancels a leading slot; +- Schönhage sizes at the smallest schedulable `N`, at `M = L`, at an `L` not + divisible by the word size, and immediately below the base-plan cutoff; - NTT lengths `1`, `2`, the largest catalogue length, and one beyond it. The largest case is an allocation-free theorem check in the coefficient owner's conformance module; the executable stream calls `NttPrime.plan?` on the @@ -739,6 +906,9 @@ Required families: - schoolbook, Karatsuba, square, and clipped products over `Int`, `Rat`, and small `ZMod64` fields, with degrees from 4 through at least 16384; +- Schönhage against Karatsuba over `ZMod64 2`, with degrees extended until + the crossover is bracketed (the packed `GF2Poly` ladder is a hex-gf2 + family); - balanced and unbalanced shapes, with ratios 1, 2, 4, 16, and 64; - KS1/KS2/KS3/KS4 over the current degree/coefficient-width grid, extended into the GMP Karatsuba, Toom, and FFT regimes; @@ -837,10 +1007,15 @@ Likewise, evaluation and interpolation soundness are stated directly with `DensePoly.eval`; a later Mathlib-facing consumer can rewrite through the existing equivalence. -If a future theorem needs Mathlib's asymptotic framework, it belongs in that -consumer or in a documentation proof, not in the computational dependency -graph. The executable complexity contracts here are enforced by body shape -and benchmarks. +Proved operation-count theorems live in +[hex-poly-fast-cslib](../../SPEC/Libraries/hex-poly-fast-cslib.md), a +proof-only companion in the style of the `-mathlib` libraries: this +computational library stays free of both Mathlib and cslib, and the +companion models its algorithms in cslib's query-complexity framework and +proves explicit coefficient-operation bounds about them. The executable +complexity contracts here remain enforced by body shape and benchmarks; the +companion's theorems are about the parametric workers this library exposes, +not about the raw array runtimes. ## Milestones @@ -865,11 +1040,22 @@ and benchmarks. conformance/benchmark families. 9. **Adoption.** Audit the named consumers, switch only winning cells, update their owning SPECs and benchmarks, and keep the single-job CI topology. +10. **Triadic references.** The triadic fold, its canonical-remainder law, + the fixed-length `Triadic` carrier, and the carrier agreement theorems. + Also `CoeffOps` and the refactor of the Karatsuba recursion and + dispatcher through `karatsubaWorker` at `idOps`, preserving every + existing theorem statement. +11. **Schönhage plan.** The schedule structure and chooser, the symbolic + radix-3 transforms and their round-trip and convolution theorems, the + operation-parametric recursion worker, `schoenhagePlan`, and its plan + laws. The packed `F_2` kernel and its dispatch are hex-gf2 milestones; + the counted model and its bound are hex-poly-fast-cslib milestones. No later milestone may be used to excuse a quadratic placeholder in an earlier one. In particular, milestone 3 implements Newton division with clipped -products, and milestone 4 implements an actual half-gcd recursion rather than -renaming the Euclidean loop. +products, milestone 4 implements an actual half-gcd recursion rather than +renaming the Euclidean loop, and milestone 11 implements the square-rooting +recursion rather than a single transform level over a quadratic base case. ## File organisation @@ -879,6 +1065,13 @@ HexPolyFast/ Karatsuba.lean -- full, square, unbalanced, and clipped recursion Cyclic.lean -- cyclic and negacyclic reference operations CyclicRemainder.lean -- cyclic and negacyclic canonical remainder laws + Triadic.lean -- triadic reference fold + TriadicRemainder.lean -- triadic canonical remainder law + Schoenhage/ + Carrier.lean -- fixed-length Triadic carrier and its operations + Schedule.lean -- SchoenhageSchedule and schedule? + Transform.lean -- symbolic radix-3 transforms + Plan.lean -- parametric worker and schoenhagePlan Reverse.lean -- DensePoly/TSeries bridges Reciprocal.lean -- plan-driven Newton inverse Division.lean -- DivPlan and one-shot division @@ -947,3 +1140,11 @@ implementation changes actually land, never by this SPEC-only change. Computation 47 (2012), 954-967. This SPEC uses the polynomial middle-product construction that the integer algorithm adapts; it does not add a limb-level integer primitive. +- Arnold Schönhage, *Schnelle Multiplikation von Polynomen über Körpern der + Charakteristik 2*, Acta Informatica 7 (1977), 395-398. The radix-3 + algorithm behind `schoenhagePlan`. +- Richard P. Brent, Pierrick Gaudry, Emmanuel Thomé, and Paul Zimmermann, + [*Faster Multiplication in GF(2)[x]*](https://doi.org/10.1007/978-3-540-79456-1_10), + ANTS-VIII (2008), LNCS 5011, 153-166. §3.2 is the implementation reference + for the schedule constraints and for the warning that `L` is generally not + word-aligned. diff --git a/SPEC/Libraries/README.md b/SPEC/Libraries/README.md index 285854df6..040956bfe 100644 --- a/SPEC/Libraries/README.md +++ b/SPEC/Libraries/README.md @@ -11,7 +11,7 @@ - **hex-mv-hensel**: multivariate Hensel lifting against an evaluation ideal, with the coprimality witness, leading-coefficient contract, and reconstruction that Wang's EEZ factorization needs - **hex-mv-factor**: factorization of `Z[x_1, ..., x_n]` by Wang's EEZ algorithm, with a checked product decomposition and a separate irreducibility certificate - **hex-truncated-series**: power series truncated at a precision fixed in the type, with Newton inversion, square root, `exp`, `log`, composition, and reversion -- **hex-poly-fast**: explicit lawful multiplication plans, Karatsuba and clipped products, Newton division, half-gcd, multipoint evaluation/interpolation, and Padé approximation +- **hex-poly-fast**: explicit lawful multiplication plans, Karatsuba and clipped products, Schönhage's radix-3 multiplication with triadic reference semantics, Newton division, half-gcd, multipoint evaluation/interpolation, and Padé approximation - **hex-matrix**: dense matrices, matrix/vector arithmetic, elementary row and column operations, submatrix slicing, the Gram matrix - **hex-row-reduce**: row reduction (RREF), rank, span, nullspace - **hex-determinant**: the Leibniz determinant and its cofactor/Cauchy-Binet/Plücker theory @@ -31,7 +31,7 @@ - **hex-modular-matrix**: multi-modular determinant, certified rank, and Dixon p-adic linear solving over `Q` - **hex-finite-field**: the Mathlib-free `F_q` interface (characteristic, degree, Frobenius, indexing), the generic `q`-power Frobenius and Frobenius matrix - **hex-poly-fp**: polynomials over `F_p`, Frobenius map, square-free decomposition, packed/NTT/CRT-NTT multiplication, lazy reduction for small p -- **hex-gf2**: packed bitwise polynomials over `F_2` (XOR + CLMUL), `GF(2^n)` elements +- **hex-gf2**: packed bitwise polynomials over `F_2` (XOR + CLMUL) with the schoolbook/Karatsuba/Schönhage multiplication ladder, `GF(2^n)` elements - **hex-poly-z**: polynomials over `Z`, content/primitive part, Mignotte bound, multipoint Kronecker and CRT-NTT multiplication - **hex-poly-z-gcd**: modular gcd for `Z[x]` with cofactors, a coprimality witness, and exact division - **hex-cyclotomic**: dense integer cyclotomic polynomials from a checked factorization of the index, the divisor family, and the factorization of `x^n - 1` @@ -100,6 +100,16 @@ Mathlib, and supplies correspondence proofs or Mathlib-facing APIs): - **hex-summation-mathlib**: `Finset.sum` semantics over characteristic-zero fields, the `Nat.choose` / `Nat.factorial` / `ascPochhammer` ratio kit, the summand recognizer, and the `gosper`, `zeilberger`, and `hyper` tactics - **hex-graph-iso-mathlib**: correspondence with finite `SimpleGraph`, ordered-colour isomorphisms, and the `SimpleGraph` extension of `graph_iso` +**cslib companion libraries** (each depends on a computational library and +on [cslib](https://github.com/leanprover/cslib), which itself depends on +Mathlib; they prove operation-count bounds in cslib's query-complexity +framework about the algorithms their computational owners execute): + +- **hex-poly-fast-cslib**: coefficient-operation bounds for the Karatsuba + dispatcher and Schönhage's radix-3 multiplication, with the + specialization and cost-obliviousness theorems that tie the counted + programs to the executable workers + ## Implementation dependencies Each library with its immediate dependencies: @@ -153,7 +163,7 @@ Each library with its immediate dependencies: - **hex-gfq-ring**: hex-poly-fp - **hex-gfq-field**: hex-gfq-ring, hex-berlekamp, hex-finite-field - **hex-gfq**: hex-gfq-field, hex-conway, hex-gf2 -- **hex-gf2**: hex-basic, hex-finite-field +- **hex-gf2**: hex-basic, hex-poly, hex-poly-fast, hex-mod-arith, hex-finite-field - **hex-berlekamp-zassenhaus**: hex-berlekamp, hex-hensel, hex-lll - **hex-summation**: hex-poly, hex-mv-poly, hex-resultant, hex-matrix, hex-row-reduce, hex-berlekamp-zassenhaus, hex-basic @@ -203,6 +213,11 @@ Mathlib companion libraries (each also depends on Mathlib): - **hex-summation-mathlib**: hex-summation - **hex-graph-iso-mathlib**: hex-graph-iso +cslib companion libraries (each also depends on cslib, and through it on +Mathlib): + +- **hex-poly-fast-cslib**: hex-poly-fast + LLL is the recombination primitive used by Berlekamp-Zassenhaus: BZ encodes its lifted local factors as a lattice basis and calls `hex-lll`'s reduced-basis and short-vector functions. The two @@ -503,6 +518,28 @@ hex-poly-z owns multipoint Kronecker and integer CRT-NTT dispatch. The complete boundary and staged dependency change are specified in [hex-poly-fast](../../HexPolyFast/SPEC/hex-poly-fast.md). +hex-gf2 joins this corner the same way hex-poly-fp did: it moves above +hex-poly-fast (and hex-mod-arith, for the `ZMod64 2` coefficient type) so it +can own the packed Schönhage kernel for `F_2[x]`, whose correctness goes +through the generic triadic algorithm: + +```text +hex-poly-fast ──┐ +hex-mod-arith ──┼── hex-gf2 +hex-basic ──────┘ +``` + +Beside the Mathlib companions there is one cslib companion so far. +`hex-poly-fast-cslib` depends on hex-poly-fast and cslib, and proves +coefficient-operation bounds for the Karatsuba and Schönhage workers; like +the `-mathlib` layers it is proof-only and sits outside the Mathlib-free +build surface: + +```text +hex-poly-fast ── hex-poly-fast-cslib +cslib ──────────────┘ +``` + `hex-primality` sits directly on `hex-arith`, which owns the `Hex.Nat.Prime` predicate, Fermat's little theorem, and the modular exponentiation its checkers replay. The predicate stays there rather @@ -625,9 +662,10 @@ for developments whose source-local move has not happened yet. - [hex-mv-factor.md](../../HexMvFactor/SPEC/hex-mv-factor.md): factorization of `Z[x_1, ..., x_n]` by Wang's EEZ algorithm, the evaluation-point and leading-coefficient search, the checked product decomposition, and the separate irreducibility certificate (the Mathlib companion is specified in the same file) - [hex-truncated-series](../../HexTruncatedSeries/SPEC/hex-truncated-series.md): power series truncated at a precision fixed in the type, Newton inversion, square root, `exp`, `log`, composition, and reversion - [hex-truncated-series-mathlib](../../HexTruncatedSeriesMathlib/SPEC/hex-truncated-series-mathlib.md): quotient-by-`X ^ n` equivalence and operation correspondence -- [hex-poly-fast.md](../../HexPolyFast/SPEC/hex-poly-fast.md): explicit lawful multiplication plans, Karatsuba and clipped products, Newton division, half-gcd, multipoint evaluation/interpolation, and Padé approximation +- [hex-poly-fast.md](../../HexPolyFast/SPEC/hex-poly-fast.md): explicit lawful multiplication plans, Karatsuba and clipped products, Schönhage's radix-3 multiplication with triadic reference semantics, Newton division, half-gcd, multipoint evaluation/interpolation, and Padé approximation +- [hex-poly-fast-cslib.md](hex-poly-fast-cslib.md) (planned): coefficient-operation bounds for the Karatsuba dispatcher and Schönhage's radix-3 multiplication, in cslib's query-complexity framework - [hex-poly-fp](../../HexPolyFp/SPEC/hex-poly-fp.md): polynomials over `F_p`, Frobenius, square-free decomposition, and packed/direct-NTT/CRT-NTT multiplication -- [hex-gf2](../../HexGF2/SPEC/hex-gf2.md): packed bitwise polynomials over `F_2`, `GF(2^n)` elements +- [hex-gf2](../../HexGF2/SPEC/hex-gf2.md): packed bitwise polynomials over `F_2` with the schoolbook/Karatsuba/Schönhage multiplication ladder, `GF(2^n)` elements - [hex-gf2-mathlib](../../HexGF2Mathlib/SPEC/hex-gf2-mathlib.md): `GF2Poly ≃+* FpPoly 2`, `GF2n`/`GF2nPoly ≃+* FiniteField 2 f hf hirr`, packed-field finiteness/cardinality - [hex-poly-fp-mathlib](../../HexPolyFpMathlib/SPEC/hex-poly-fp-mathlib.md): `FpPoly p ≃+* Polynomial (ZMod p)`, the crossing point to Mathlib's polynomial type - [hex-poly-z](../../HexPolyZ/SPEC/hex-poly-z.md): polynomials over `Z`, content/primitive part, Mignotte bound, multipoint Kronecker, and CRT-NTT multiplication diff --git a/SPEC/Libraries/hex-poly-fast-cslib.md b/SPEC/Libraries/hex-poly-fast-cslib.md new file mode 100644 index 000000000..18f59aa94 --- /dev/null +++ b/SPEC/Libraries/hex-poly-fast-cslib.md @@ -0,0 +1,302 @@ +# hex-poly-fast-cslib (operation-count bounds, depends on hex-poly-fast and cslib) + +Proved coefficient-operation bounds for the generic multiplication +algorithms of +[hex-poly-fast](../../HexPolyFast/SPEC/hex-poly-fast.md), built on the +query-complexity framework of the Lean computer-science library +[cslib](https://github.com/leanprover/cslib). This is the first `-cslib` +companion library. It plays the same architectural role for complexity +that the `-mathlib` companions play for Mathlib correspondence: the +computational library stays free of the external dependency, and the +companion proves theorems about it. + +## Complexity-layer classification + +This library is a `complexity-layer`. + +Computational conformance owner: `HexPolyFast` +Computational performance owner: `HexPolyFast` + +A complexity-layer library contains no algorithms of its own, no +conformance fixtures, no oracles, and no benchmarks. Its theorems bound +the number of coefficient operations performed by programs that are, by +the specialization theorems below, the algorithms its computational owner +executes. It claims nothing about wall-clock time; benchmarks in the +owning library remain the only evidence of speed. + +## Why this library exists + +**hex-poly-fast enforces complexity by body shape and benchmarks, and that +enforcement has no theorem.** Its complexity-contract table is a review +obligation: a quadratic body violates the SPEC, but nothing in the build +proves the bound. For most of the library that is the right trade, because +the contracts are simple enough to check by reading. The Schönhage +recursion is not: its bound depends on a schedule invariant +(`L` near `sqrt N` at every level), and an implementation that satisfies +every local body-shape rule can still lose the global bound by choosing +schedules badly. A proved operation count is the review tool that scales. + +**The bound must be a theorem about the shipped algorithm.** Every lawful +`MulPlan` returns the same polynomial, so a bound proved about a program +that merely agrees with the plan's output is vacuous. hex-poly-fast +therefore defines its counted algorithms once, as operation-parametric +workers, and executes them at the identity monad. This library +instantiates the same workers at a free monad and counts. The two +instantiations are connected by a specialization theorem, not by output +equality. + +**The dependency must stay out of the computational graph.** cslib +requires Mathlib. Placing operation counts in the computational libraries +would pull both into every consumer, which is the exact failure the +`-mathlib` split exists to prevent. The companion pattern already solves +this, and this library extends it to a second external proof dependency. + +hex-poly-fast's SPEC previously assigned any future asymptotic theorem to +"that consumer or a documentation proof". This library is the considered +replacement of that position, and hex-poly-fast's §The Mathlib layer now +points here. + +## Dependency and pin policy + +This library requires cslib, and cslib requires Mathlib. It is therefore +marked and treated like a `-mathlib` library: proof-only, no +`precompileModules`, no benches, and outside the Mathlib-free build +surface. + +Until cslib PR +[#401](https://github.com/leanprover/cslib/pull/401) merges, the lakefile +pins cslib to a recorded commit of that PR's branch (at SPEC time, +`36e098cfc04fbb8e9b44086d64ce433514ee18d4`). The pin is updated by ordinary +dependency bumps. The verified compatibility state at SPEC time: + +- cslib's and hex-dev's Lean toolchains agree (`v4.34.0-rc2`). +- cslib pins a newer Mathlib than hex-dev. Lake resolves dependencies from + the root manifest, so cslib builds against hex-dev's Mathlib revision. + The `Cslib.Algorithms.Lean.Query.*` modules this library imports build + cleanly against that revision. A handful of unrelated cslib modules + (the omega-sequence topology corner) import a Mathlib file that does not + exist at hex-dev's revision; they are not imported here and are never + built as dependencies. +- This library imports only `Cslib.Algorithms.Lean.Query.*` and the + `FreeM` foundations they re-export, never the `Cslib` umbrella module. + +Releasing or publishing this library requires a merged cslib revision (or +a maintained fork with a stable branch); a floating PR commit is +acceptable only inside the monorepo. + +## The query model + +Programs are `Cslib.FreeM Q α` values over cslib's arithmetic query type: + +```lean +inductive ArithQuery (α : Type) : Type → Type where + | add (a b : α) : ArithQuery α α + | sub (a b : α) : ArithQuery α α + | mul (a b : α) : ArithQuery α α +``` + +with cslib's `honest` oracle interpreting queries by the actual ring +operations, `FreeM.eval` for results, and `FreeM.cost` with +`ArithQuery.weight c_add c_mul` for weighted counts (subtraction weighs as +addition; multiplication weighs separately, because multiplications drive +the recursions). If the upstream `Arith` files change shape before the pin +is next moved, an equivalent local query type replaces them with no change +to the theorem statements; the pin makes this a scheduled decision rather +than a build break. + +The instantiation record is one definition: + +```lean +def freeOps : CoeffOps (FreeM (ArithQuery R)) R where + add a b := FreeM.lift (.add a b) + sub a b := FreeM.lift (.sub a b) + mul a b := FreeM.lift (.mul a b) +``` + +`CoeffOps` and the workers are hex-poly-fast's; this library adds no +algorithm text. Every quotient-ring operation of the Schönhage recursion +is scalar-expanded: `Triadic` elements are fixed-shape data, their +additions and twiddle folds issue base-ring queries coefficient by +coefficient, and pointwise products recurse through the same worker. The +bounds therefore count base-ring operations, which is the standard +algebraic complexity measure and what the headline inequality means. + +## Specialization + +For each worker, the specialization theorem identifies running the free +program under the honest oracle with the executable algorithm: + +```lean +theorem karatsubaWorker_eval (cutoff fuel : Nat) (a b : Array R) : + (karatsubaWorker freeOps cutoff fuel a b).eval ArithQuery.honest = + karatsubaWorker idOps cutoff fuel a b +``` + +and likewise for the Schönhage worker. The proof is induction over the +worker body (or one generic lemma about interpreting `freeOps` through +`FreeM.liftM`). Because hex-poly-fast *defines* its recursions as the +`idOps` instantiations, this theorem makes every count below a statement +about the algorithm hex-poly-fast executes. The raw array runtimes are +connected to those definitions by output-equality `@[csimp]` theorems +only, and no operation count is claimed for them. + +## Cost obliviousness + +Query traces are not oracle-independent: queries embed operands, and a +dishonest oracle changes the operands of later queries. What holds for +these workers is the weaker, sufficient property that the *cost* does not +depend on the oracle: + +```lean +def CostOblivious {T : Type} [AddMonoid T] + (weight : {ι : Type} → Q ι → T) (p : FreeM Q α) : Prop := + ∀ o₁ o₂, p.cost o₁ weight = p.cost o₂ weight +``` + +Each worker's program is proved `CostOblivious` for every weight: its +control flow (splits, schedule choice, recursion depth, base-case entry) +depends only on sizes and the schedule, never on coefficient values. This +is a real design constraint on hex-poly-fast's workers, and it is the +reason its `Triadic` carrier is never normalized mid-transform. With +`CostOblivious` proved, bounds quantified over all oracles follow from the +honest-oracle count; without it, a bound would be honest-oracle only. + +## Bounds + +cslib's `UpperBound` counts queries. Weighted bounds need the analogue +over `cost`, defined here and a candidate for upstreaming: + +```lean +def WeightedBound {T : Type} [AddMonoid T] [LE T] + (prog : α → FreeM Q β) (size : α → Nat) + (weight : {ι : Type} → Q ι → T) (bound : Nat → T) : Prop := + ∀ (oracle : {ι : Type} → Q ι → ι) (n : Nat) (x : α), + size x ≤ n → (prog x).cost oracle weight ≤ bound n +``` + +**Karatsuba (milestone 1).** The bound covers the public dispatcher, both +operand sizes, and the cutoff, in integer form with no real exponents: +for sizes `m ≥ n` and cutoff `c`, the query count of the dispatcher +worker is at most + +```text +ceil(m/n) * (A(c) * 3 ^ Nat.clog 2 n + B(c) * n) +``` + +with `A` and `B` explicit polynomials in `c` fixed by the proof. The +balanced case is the `ceil(m/n) = 1` row. A bound for the textbook +balanced recursion alone does not discharge this milestone: the point of +the warm-up is to validate the worker architecture against the dispatch +structure hex-poly-fast actually has. + +**Schönhage (milestone 2).** The recurrence is stated over the schedule: +for a valid `SchoenhageSchedule N`, the count for the triadic product +worker at half-length `N` is at most `2 * 3^k` times the count at +half-length `L` plus an explicit `O(N * k)` transform term. The chooser's +balance property (`L` within a constant factor of `sqrt N` whenever a +schedule exists) then closes the recurrence to the headline bound: an +explicit constant `C` with query count at most + +```text +C * n * Nat.clog 3 n * (Nat.clog 3 (Nat.clog 3 n) + 1) +``` + +for the full-product worker at input size `n`, all stated in `Nat`. The +`log log` factor is the recursion depth; the proof tracks it as the +number of schedule steps until `schedule?` returns `none`. + +## What is not claimed + +- Nothing about wall-clock time or memory; benchmarks in hex-poly-fast + and hex-gf2 remain the speed evidence. +- Nothing about the raw array runtimes or the packed `GF2Poly` kernel. + One packed XOR performs 64 coefficient additions at once, so a + word-level cost model is a different theorem, reserved for a possible + later hex-gf2-cslib. +- No lower bounds. cslib's decision-tree lemma requires finite query + response types; `ArithQuery R` over an infinite ring is outside it. + +## External comparators + +No external comparator is required. Justification: `complexity-layer`, +analogous to `correspondence-only-layer` per +[SPEC/benchmarking.md §Comparator naming](../benchmarking.md); the +computational owner carries the comparators. + +## Infrastructure amendments + +Implemented with the library, not by this SPEC-only change: + +- `lakefile.lean` gains the cslib `require` at the pinned revision. + `scripts/release/sync_released.py` reads external pins generically from + `lake-manifest.json`, so released-repo pin rewriting needs no change. +- `libraries.yml` gains a `cslib: true` field on this library. The schema + is enforced, so this touches the parser and validation in + `scripts/libgraph.py` and `scripts/check_dag.py` (`LIBRARY_FIELDS`, + `LibraryInfo`, and the field validators), not only the DAG check. +- `Cslib` joins `EXTERNAL_IMPORT_ROOTS` in `scripts/libgraph.py`, and + `check_dag.py` restricts `Cslib.*` imports to libraries marked + `cslib: true`, exactly as `Mathlib.*` imports are restricted to + `mathlib: true` libraries. A library marked `cslib: true` is implicitly + Mathlib-adjacent for every build rule (`precompileModules` ban, no + benches, proof-only runtime exemptions). +- `SPEC/design-principles.md` extends "No Mathlib in the computational + core" to cslib in one paragraph. +- CI: cslib modules build inside the existing single job. cslib has no + olean cache service, but the imported Query modules and their Mathlib + dependencies are covered by the Mathlib cache plus a small residual + build, measured before the library is activated. + +## Milestones + +1. **Framework and Karatsuba.** The cslib pin, `freeOps`, + `CostOblivious`, `WeightedBound`, the Karatsuba specialization and + cost-obliviousness theorems, and the dispatcher-covering Karatsuba + bound. This milestone validates the worker architecture end to end on + an algorithm whose mathematics is finished, before any of it is on the + Schönhage critical path. +2. **Schönhage.** Specialization and cost obliviousness for the Schönhage + worker, the schedule recurrence, the chooser balance property, and the + headline bound. +3. **Upstreaming review.** Offer `CostOblivious` and `WeightedBound` to + cslib; adopt the upstream forms if accepted; re-pin to merged cslib. + +No milestone may weaken a bound statement to an honest-oracle-only form +as a shortcut: cost obliviousness is part of milestones 1 and 2, not a +follow-up. + +## File organisation + +```text +HexPolyFastCslib/ + Query.lean -- freeOps, CostOblivious, WeightedBound + Karatsuba.lean -- specialization, obliviousness, dispatcher bound + Schoenhage.lean -- specialization, obliviousness, recurrence, bound +HexPolyFastCslib.lean +``` + +`libraries.yml` eventually gains, after cslib is pinned and the +hex-poly-fast workers exist: + +```yaml + HexPolyFastCslib: + deps: [HexPolyFast] + mathlib: true + cslib: true + done_through: 0 + status: planned +``` + +The release manifest is updated only when a release shape for `-cslib` +companions is decided, never by this SPEC-only change. + +## References + +- cslib PR [#401, query complexity framework](https://github.com/leanprover/cslib/pull/401): + `FreeM` programs, oracles, `cost`, `countQueries`, `UpperBound`, and the + `ArithQuery` example this library builds on. +- Arnold Schönhage, *Schnelle Multiplikation von Polynomen über Körpern + der Charakteristik 2*, Acta Informatica 7 (1977), 395-398. +- Richard P. Brent, Pierrick Gaudry, Emmanuel Thomé, and Paul Zimmermann, + [*Faster Multiplication in GF(2)[x]*](https://doi.org/10.1007/978-3-540-79456-1_10), + ANTS-VIII (2008), LNCS 5011, 153-166. diff --git a/SPEC/design-principles.md b/SPEC/design-principles.md index 34882b14b..ed4db0a2b 100644 --- a/SPEC/design-principles.md +++ b/SPEC/design-principles.md @@ -34,6 +34,13 @@ bridge, transported along the equivalence so the operations stay the executable ones. + The same boundary applies to cslib, which itself depends on Mathlib. + Computational libraries are cslib-free; proved operation-count bounds + live in `-cslib` companion libraries (the first is + [hex-poly-fast-cslib](Libraries/hex-poly-fast-cslib.md)), which are + proof-only and follow every build rule that applies to `-mathlib` + libraries. + 3. **Performant by default.** Dense array-backed representations, `UInt64` coefficients for `F_p`, Barrett/Montgomery reduction for modular arithmetic. New GMP `@[extern]` primitives where Lean's runtime diff --git a/SPEC/future-work.md b/SPEC/future-work.md index 62ab364fb..b5448321e 100644 --- a/SPEC/future-work.md +++ b/SPEC/future-work.md @@ -228,6 +228,34 @@ and normalization behaviour differ, and gcd or division of sparse inputs usually becomes dense. Keep explicit conversions until several real consumers show which operations a common interface must support. +### Fast multiplication in characteristic two, follow-ups + +Schönhage's radix-3 multiplication and its proved coefficient-operation +bound are specified: the generic algorithm and triadic reference semantics +as amendments to [hex-poly-fast](../HexPolyFast/SPEC/hex-poly-fast.md), +the packed `F_2[x]` kernel and dispatch ladder as amendments to +[hex-gf2](../HexGF2/SPEC/hex-gf2.md), and the operation counts in +[hex-poly-fast-cslib](Libraries/hex-poly-fast-cslib.md), the first `-cslib` +companion. What remains future work: + +- Additive FFTs (Cantor's algorithm, Gao-Mateer) as an alternative + large-degree family for `F_2[x]` and `F_(2^k)[x]`, and the + wrapped-product splitting reconstruction of + Brent-Gaudry-Thomé-Zimmermann §3.3 that smooths the schedule staircase. +- Instantiating the generic radix-3 plan for `F_(2^k)[x]` in the hex-gfq + family, where the word-prime NTT path is equally unavailable. +- Integer Schönhage-Strassen multiplication. Hex integer arithmetic + currently delegates large products to GMP through Lean core, so this is + a verification project, not a performance one, and it needs its own + motivation before a SPEC. +- A hex-gf2-cslib companion counting word operations of the packed kernel. + The existing bound counts coefficient operations of the generic + algorithm; one packed XOR performs 64 coefficient additions, so the + word-level statement is a separate theorem with its own cost model. +- Extending the `-cslib` pattern to other libraries once a second + worthwhile bound is identified. Turing-machine-model complexity is out + of scope for the foreseeable future. + ### Positive-characteristic multivariate squarefree decomposition Amend `hex-mv-gcd` with squarefree decomposition over perfect fields of From f78814441e911233f1ac9d1158b40cfdeaba4e76 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 1 Sep 2026 09:22:06 +0000 Subject: [PATCH 2/2] =?UTF-8?q?docs:=20tighten=20Sch=C3=B6nhage=20SPEC=20c?= =?UTF-8?q?ontracts=20and=20add=20the=20complexity-layer=20classification?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This commit revises the Schönhage SPECs: the operation bounds are stated for the operation-parametric workers only, with the raw @[csimp] runtimes related by output equality and explicitly outside the claims; the schedule gains chooser obligations (bounded padding, two-sided sqrt-N balance for K and L, recursive completeness) and the per-schedule recurrence carries the K*L*k transform term; cost obliviousness is stated for constructor- determined weights; the Schönhage bound fixes its base to the counted Karatsuba worker; the Triadic carrier carries 0 < L and exact-order claims take Nontrivial R; hex-gf2 states the ladder as a planned amendment with milestones, targets DensePoly (ZMod64 2) directly, gives the exact packed twiddle rule, and corrects the oracle attribution (python-flint conforms, NTL remains an informational comparator). SPEC/benchmarking.md and SPEC/testing.md gain the normative complexity_layer classification the companion cites. Co-Authored-By: Claude Fable 5 Claude-Session: https://claude.ai/code/session_018S4hrFX6e8B8s56182nAp4 --- HexGF2/SPEC/hex-gf2.md | 197 +++++++----- HexPolyFast/SPEC/hex-poly-fast.md | 317 ++++++++++--------- SPEC/Libraries/README.md | 61 ++-- SPEC/Libraries/hex-poly-fast-cslib.md | 436 ++++++++++++++------------ SPEC/benchmarking.md | 6 + SPEC/design-principles.md | 12 +- SPEC/future-work.md | 49 ++- SPEC/testing.md | 19 +- 8 files changed, 598 insertions(+), 499 deletions(-) diff --git a/HexGF2/SPEC/hex-gf2.md b/HexGF2/SPEC/hex-gf2.md index 811a9aef6..dd8a3abaa 100644 --- a/HexGF2/SPEC/hex-gf2.md +++ b/HexGF2/SPEC/hex-gf2.md @@ -1,4 +1,4 @@ -# hex-gf2 (GF(2) packed arithmetic, depends on hex-basic, hex-poly, hex-poly-fast, hex-mod-arith) +# hex-gf2 (GF(2) packed arithmetic, currently depends on hex-basic) Packed bitwise representation of polynomials over F_2. Addition is XOR, multiplication uses carry-less multiply. Substantially faster @@ -34,12 +34,11 @@ it costs one scan of the top word and makes equality of elements equality of word arrays (`GF2Poly.ext_words`). - Addition: word-by-word XOR -- Multiplication: a three-rung dispatch (see §Multiplication ladder): - schoolbook on 64-bit blocks, Karatsuba on 64-bit blocks, and the packed - Schönhage kernel, where each block multiply uses carry-less multiply via - `@[extern]` calling a C wrapper that uses CLMUL on x86 (with compile-time - feature detection) and a portable shift-and-XOR fallback on other - architectures. +- Multiplication: currently schoolbook on 64-bit blocks. The planned + multiplication ladder adds word Karatsuba and packed Schönhage dispatch. + Each base block product uses carry-less multiplication through `@[extern]`. + The C implementation uses CLMUL when it is enabled at compile time and a + portable shift-and-XOR implementation otherwise. - Division with remainder (for polynomial GCD, modular reduction) - GCD and extended GCD over `GF2Poly` - Shift operations (multiply/divide by x^k) @@ -110,101 +109,130 @@ self-test needs no Lean runtime. ## Multiplication ladder -`GF2Poly.mul` is defined as the word-schoolbook convolution (`mulWords` with -clmul block products), and every existing theorem is stated against that -definition. The runtime is a proof-backed `@[csimp]` replacement that -dispatches by operand word count: +This section specifies a planned extension. The current `GF2Poly.mul` is the +word-schoolbook convolution `mulWords`, and its existing theorems use that +definition. The extension retains `GF2Poly.mul` as the logical definition and +adds a proof-backed `@[csimp]` replacement selected by operand word count: -1. word schoolbook (`mulWords`), below the first crossover; -2. Karatsuba on 64-bit blocks, splitting at word boundaries so the block - products are again `mulWords` calls; -3. the packed Schönhage kernel, above the second crossover. +1. `mulWords` below the first crossover; +2. Karatsuba split at word boundaries between the two crossovers; +3. packed Schönhage multiplication above the second crossover. -Both crossovers are benchmark-committed under the adoption law of -[hex-poly-fast §Benchmarking and production dispatch](../../HexPolyFast/SPEC/hex-poly-fast.md): -a rung enters the committed table only when its cells win on this library's -own ladder, and the logical definition, the coefficient theorems, and every -caller-visible statement are unchanged by dispatch. +The base products in both recursive rungs use the existing carry-less word +product. The committed crossover table is determined only by within-Hex +comparisons between adjacent rungs, following +[hex-poly-fast §Benchmarking and production dispatch](../../HexPolyFast/SPEC/hex-poly-fast.md). +A new rung is selected only for cells in which it wins outside the recorded +uncertainty band. Dispatch does not change the logical definition or any +coefficient theorem. ### Dense correspondence -The fast rungs are proved through the dense representation. `FpPoly 2` is -`DensePoly (ZMod64 2)`, so the pair of Mathlib-free conversions +The correctness proof converts packed polynomials to dense polynomials over +`ZMod64 2`. The new Mathlib-free API is: ```lean -def GF2Poly.toFpPoly : GF2Poly → FpPoly 2 -def GF2Poly.ofFpPoly : FpPoly 2 → GF2Poly +def GF2Poly.toDense : GF2Poly → DensePoly (ZMod64 2) +def GF2Poly.ofDense : DensePoly (ZMod64 2) → GF2Poly ``` -with round-trip laws and coefficient agreement (`(toFpPoly p).coeff i` is -bit `i % 64` of word `i / 64`) lets each packed operation land on the -corresponding `DensePoly` operation. The `≃+*` packaging of this pair stays -in hex-gf2-mathlib; the conversions and their operation-preservation lemmas -are Mathlib-free and live here. This is what the new hex-poly and -hex-poly-fast dependencies are for. The existing ring-law theorems -(`mul_assoc`, `mul_comm`, `left_distrib`, and companions) are bundled into a -`Lean.Grind.CommRing GF2Poly` instance so `DensePoly GF2Poly` and generic -plan machinery apply to the packed type. +The coefficient theorem says that coefficient `i` of `toDense p` is the +element of `ZMod64 2` represented by bit `i % 64` in word `i / 64`. +Round-trip theorems account for normalization of the dense and packed +representations. Addition, multiplication, and the triadic carrier operations +commute with these conversions. + +The names `FpPoly 2` and the equivalence `GF2Poly ≃+* FpPoly 2` remain in +hex-gf2-mathlib, which already depends on hex-poly-fp. `HexGF2` does not +import `FpPoly`. The generic Schönhage plan is instantiated at coefficient +ring `ZMod64 2`, not at coefficient ring `GF2Poly`. ### Packed Schönhage kernel -The kernel mirrors the generic algorithm of +The planned packed kernel follows the generic algorithm in [hex-poly-fast §Schönhage's radix-3 algorithm](../../HexPolyFast/SPEC/hex-poly-fast.md) -rung for rung: same `SchoenhageSchedule`, same transform shape, same -recursion. In characteristic two the inverse-of-three witness is `1` and -subtraction is XOR, so every carrier operation is a shift-and-XOR loop. +with the same `SchoenhageSchedule`, transform indices, and recursive +half-lengths. In characteristic two, subtraction is XOR and the inverse of +three is `1`. Transform addition, subtraction, and twiddle operations are +therefore packed linear operations. Pointwise multiplication is not a linear +operation. Its base cases use carry-less word multiplication. The packed carrier holds a residue modulo `y^(2L) + y^L + 1` in `ceil(2L / 64)` words with the unused top bits of the last word zero. -`L` is generally not a multiple of 64 -(Brent-Gaudry-Thomé-Zimmermann §3.2), and the kernel must not round it up: -the primitives are arbitrary-bit operations, not word-aligned ones. -Required packed primitives, each with an unpacking lemma identifying it -with the corresponding `Triadic (ZMod64 2) L` operation: - -- addition as overlap-safe XOR accumulation; -- multiplication by `y^j`: an arbitrary-bit left shift crossing word - boundaries, followed by the wrap of bits at exponent `2L` and above into - XOR contributions at exponents reduced by the relation - `y^(2L) = y^L + 1`, followed by the final-word mask; -- conversion between packed blocks of a `GF2Poly` and carrier values; -- the pointwise product, which recurses through the dispatcher. - -Correctness is a refinement ladder, not one whole-algorithm equality: - -1. each packed primitive equals its `Triadic (ZMod64 2) L` counterpart - under unpacking; -2. the packed transform equals the symbolic radix-3 transform under - elementwise unpacking; -3. the packed kernel equals `schoenhagePlan`'s product under `toFpPoly`; -4. the final theorem restates 3 against this library's own convolution - coefficient semantics: the kernel's output coefficients are the - carry-less convolution of the inputs. - -Step 4 is the statement the dispatcher's `@[csimp]` proof consumes, so -dispatch never depends on the dense detour at runtime. +The selected `L` is not rounded to a word boundary. Brent, Gaudry, Thomé, and +Zimmermann §3.2 permits non-word-aligned `L`, and the schedule must be used +without changing its arithmetic constraints. + +Packed multiplication by `y^j` implements the exact triadic reduction. For a +set bit at exponent `i`, it sets `r = (i + j) % (3 * L)`. If `r < 2 * L`, it +XORs the bit into exponent `r`. Otherwise it XORs the bit into exponents +`r - L` and `r - 2 * L`. This rule is applied directly. A single rewrite at +exponent `2L` is insufficient because `i + j` can exceed `3L`. + +The required packed operations are: + +- overlap-safe XOR addition and subtraction; +- multiplication by `y^j` using the rule above, including shifts across word + boundaries and masking of the final word; +- conversion between `GF2Poly` blocks and packed triadic values; +- pointwise multiplication through the recursive packed dispatcher. + +Each operation has an unpacking theorem identifying it with the corresponding +operation on `Triadic (ZMod64 2) L`. Correctness is proved in four stages: + +1. packed carrier operations agree with generic triadic operations; +2. the packed forward and inverse transforms agree elementwise with the + generic radix-3 transforms; +3. the packed recursive product agrees under `toDense` with + `schoenhagePlan` instantiated over `ZMod64 2`; +4. the packed result has the carry-less convolution coefficients specified by + `GF2Poly.mul`. + +The fourth theorem supplies the `@[csimp]` correctness proof. None of the +dense values occur in the packed computation. No operation-count theorem is claimed for the packed kernel. The coefficient-operation bound in -[hex-poly-fast-cslib](../../SPEC/Libraries/hex-poly-fast-cslib.md) is about -the generic algorithm; one packed XOR performs 64 coefficient additions at -once, so a word-level cost model is a different theorem, reserved for a -possible later hex-gf2-cslib companion. +[hex-poly-fast-cslib](../../SPEC/Libraries/hex-poly-fast-cslib.md) applies to +the generic worker. One packed XOR represents 64 coefficient additions, and +the packed base product uses CLMUL. A possible hex-gf2-cslib library would +need a separate word-operation model. ### Conformance and benchmarks for the ladder -The conformance stream gains multiplication fixtures whose operand sizes -bracket both committed crossovers, forced-rung cases for each of the three -rungs on shared inputs, and carrier cases at an `L` not divisible by 64. -The oracles are the existing NTL `GF2X` driver and python-flint at `p = 2`, -registered in the existing single CI job. - -The bench ladder extends the multiplication family until the -Karatsuba/Schönhage crossover is bracketed on the reference host. NTL/gf2x -remains the informational external comparator; once the Schönhage rung is -committed, its multiplication cells compare like against like -(gf2x's large-degree multiplication is this same algorithm family), and the -ratios feed the crossover table rather than Phase 4. +The conformance stream will add shared-input cases that force each rung, +cases immediately below and above both crossovers, and packed carrier cases +with `L % 64 ≠ 0`. The registered conformance oracle remains python-flint at +`scripts/oracle/gf2_flint.py`. It recomputes the full product over `F_2` from +the serialized inputs. The NTL `GF2X` program is a checksum-based benchmark +comparator and is not a conformance oracle. + +The benchmark family will extend far enough to bracket both within-Hex +crossovers on the reference host. Schoolbook versus Karatsuba measurements +determine the first table entry. Karatsuba versus packed Schönhage +measurements determine the second. NTL/gf2x remains informational and gives +context for the resulting large-degree performance. Its ratios do not select +either Hex crossover. + +## Milestones + +1. **Dense correspondence and dependencies.** Add the specified + `HexFiniteField`, `HexPoly`, `HexPolyFast`, and `HexModArith` monorepo + dependencies. Define `toDense` and `ofDense`, then prove coefficient, + round-trip, and operation theorems. +2. **Word Karatsuba.** Implement the word-boundary recursion, prove its result + equal to `mulWords`, and add forced-rung conformance and benchmark cases. +3. **Packed Schönhage.** Implement the non-word-aligned carrier operations, + transforms, recursive product, and the four stages of correctness above. +4. **Dispatch.** Measure adjacent rungs, commit the crossover table, and add + the proof-backed `@[csimp]` dispatcher. Extend the python-flint fixtures and + retain NTL/gf2x as an informational comparator. + +`hex-poly-fast` depends on `hex-truncated-series`. Neither library is yet +listed in `scripts/release/released.yml`. The released hex-gf2 mirror can add +the planned dependencies only after hex-truncated-series and hex-poly-fast +have been published in dependency order. Development and the combined build +inside this monorepo do not depend on that publication step. **GF(2^n) elements.** Elements of `GF(2^n)` are polynomials of degree < n over F_2, reduced modulo an irreducible of degree n. This library @@ -334,10 +362,11 @@ source uses tuned base cases and Karatsuba/gf2x multiplication, crossover-based division and remainder, and switches its GCD to `HalfGCD` above the configured crossover. Hex currently implements packed schoolbook multiplication, long division and remainder, and Euclidean GCD. §Multiplication ladder specifies -the Karatsuba and Schönhage rungs that put multiplication in the same -complexity class as gf2x; until they land, and for division and GCD -throughout, the ratios compare different complexity classes at the upper end -of the ladder. They orient future optimization but do not decide Phase 4. Addition has the same linear packed-word +planned Karatsuba and Schönhage rungs with the same multiplication complexity +class as gf2x. Until those rungs are implemented, the upper multiplication +cells compare different complexity classes. The division and GCD cells +continue to do so. These ratios provide context and do not determine the Hex +dispatch table or Phase 4. Addition has the same linear packed-word kernel shape, but the hex-framed driver measures serialization rather than raw NTL addition, so its paired registrations are correctness and protocol anchors rather than performance evidence. The comparator is diff --git a/HexPolyFast/SPEC/hex-poly-fast.md b/HexPolyFast/SPEC/hex-poly-fast.md index fca6f4f21..37ab8b119 100644 --- a/HexPolyFast/SPEC/hex-poly-fast.md +++ b/HexPolyFast/SPEC/hex-poly-fast.md @@ -81,9 +81,9 @@ In scope: - explicit lawful multiplication plans; - schoolbook and Karatsuba full products, squaring, unbalanced products, and arbitrary clipped products; -- cyclic, negacyclic, and triadic products with positive length; -- the fixed-length triadic carrier, the symbolic radix-3 transform, the - proof-carrying Schönhage schedule, and the Schönhage multiplication plan; +- positive-length cyclic, negacyclic, and triadic products; +- fixed-length triadic arithmetic, radix-3 transforms, checked parameter + schedules, and the Schönhage multiplication plan; - reversal and fixed-precision `TSeries` bridges; - Newton reciprocal precomputation and fast monic/field division; - half-gcd, gcd, full extended gcd, and one-sided extended gcd; @@ -106,14 +106,12 @@ Out of scope: - changing `DensePoly.mul`, its `Mul` instance, or its minimal typeclass requirements; - a `PolyOps` abstraction over dense and sparse representations; -- Toom-Cook before a measured gap remains between Karatsuba and the - coefficient-specific kernels. The Schönhage plan below is not subject to - this deferral: over coefficient rings with no suitable roots of unity - (`F_2` and its extensions), the word-prime radix-2 NTT path cannot be - instantiated, so no coefficient-specific kernel covers the regime the - radix-3 algorithm addresses, and the complexity-class gap against - NTL/gf2x is already recorded in - [hex-gf2 §External comparators](../../HexGF2/SPEC/hex-gf2.md); +- Toom-Cook before measurements show a remaining gap between Karatsuba and + the coefficient-specific kernels. This deferral does not include the + Schönhage plan. The existing word-prime radix-2 NTT cannot be instantiated + directly over `F_2` or its extensions, and + [hex-gf2 §External comparators](../../HexGF2/SPEC/hex-gf2.md) records the + resulting complexity difference from NTL/gf2x; - additive FFTs (Cantor, Gao-Mateer) and the wrapped-product splitting reconstruction of Brent-Gaudry-Thomé-Zimmermann §3.3; - integer Schönhage-Strassen multiplication; @@ -254,57 +252,61 @@ new algebraic semantics. ### Triadic products -The triadic product is the ordinary product modulo `x^(2m) + x^m + 1`. It is -the third reference family beside the cyclic and negacyclic folds, and it is -the algebraic object of Schönhage's radix-3 multiplication algorithm: in the -quotient by `x^(2m) + x^m + 1` the residue of `x` has multiplicative order -`3m`, which supplies synthetic roots of unity over coefficient rings that -have none of their own. - -The reference fold maps input exponent `i` to `r = i % (3 * m)`. When -`r < 2 * m` the coefficient is added at slot `r`. Otherwise -`x^r = -x^(r - m) - x^(r - 2*m)`, so the coefficient is subtracted at slots -`r - m` and `r - 2*m`. As with the other two families, a proof-taking API -requires `0 < m`, checked forms return `none` at `m = 0`, and the theorems -identify the fold with the canonical remainder modulo the monic -`x^(2m) + x^m + 1` and bound its size by `2 * m`. +For `0 < m`, the triadic product is ordinary multiplication reduced modulo +`x^(2m) + x^m + 1`. It is the reference operation used by Schönhage's +radix-3 algorithm. + +The fold reduces an exponent `i` by setting `r = i % (3 * m)`. If +`r < 2 * m`, it adds the coefficient to position `r`. Otherwise it uses + +```text +x^r = -x^(r - m) - x^(r - 2 * m) +``` + +and subtracts the coefficient from positions `r - m` and `r - 2 * m`. +The proof-taking operation accepts a proof of `0 < m`. The checked operation +returns `none` when `m = 0`. Its agreement theorem identifies the result with +the canonical remainder modulo the monic polynomial +`x^(2m) + x^m + 1`, and its size theorem gives an upper bound of `2 * m`. + +In every commutative ring the residue of `x` satisfies `x^(3m) = 1` and +`1 + x^m + x^(2m) = 0`. Exact order `3m`, the inequality `x^m ≠ 1`, and +distinctness of the transform points are stated only with `[Nontrivial R]`. ### Schönhage's radix-3 algorithm -The Schönhage plan computes full products through triadic products. It works -over any commutative ring with an explicit inverse of three; over `F_2` and -its extensions that witness is `1`, because three is odd. Subtraction is -already required by Karatsuba, so the plan signature adds only the -invertibility witness. +The planned Schönhage multiplication reduces a full product to smaller +triadic products. It applies to a commutative ring equipped with `inv3 : R` +and a proof of `3 * inv3 = 1`. In characteristic two, `inv3` is `1`. **The fixed-length carrier.** Transform values are residues modulo -`y^(2L) + y^L + 1` held at fixed shape: +`y^(2L) + y^L + 1`. The carrier includes the positive-length condition: ```lean structure Triadic (R : Type u) [DecidableEq R] [Lean.Grind.CommRing R] (L : Nat) where + length_pos : 0 < L coeffs : Vector R (2 * L) ``` -`Triadic` values are never normalized: trimming would make control flow -depend on coefficient values and would break the fixed-shape invariants the -transform relies on. The carrier has explicit addition, subtraction, -multiplication by `y^j` for `0 <= j < 3 * L` (a fold of index shifts and -sign flips with no ring multiplications), a full multiply-and-reduce that -consumes a supplied plan, and conversions to and from `DensePoly`. Its -agreement theorems identify each operation with the triadic reference fold -of the corresponding polynomial operation. A bundled ring instance on -`Triadic R L` is not required; the explicit operations carry the laws. +Every operation preserves all `2 * L` positions. No transform operation trims +trailing zero coefficients. The API provides addition, subtraction, +multiplication by `y^j` for `j < 3 * L`, multiplication followed by triadic +reduction using a supplied `MulPlan R`, and conversions to and from +`DensePoly`. Multiplication by `y^j` uses index movement and additions or +subtractions. It performs no coefficient multiplications. Each semantic +theorem identifies an explicit carrier operation with the corresponding +polynomial operation followed by the triadic fold. A ring instance for +`Triadic R L` is optional because the algorithm uses the explicit operations. -**The schedule.** Parameter selection is a proof-carrying structure, not -arithmetic scattered through the recursion. For a target triadic product -modulo `x^(2N) + x^N + 1`: +**The schedule.** A schedule records the parameters for multiplication modulo +`x^(2N) + x^N + 1`. Write `K = 3^k`. ```lean structure SchoenhageSchedule (N : Nat) where - k : Nat -- transform radix exponent; K = 3^k - M : Nat -- block length - L : Nat -- inner carrier half-length + k : Nat + M : Nat + L : Nat k_pos : 0 < k blocks : N = 3 ^ k * M block_fits : M ≤ L @@ -312,32 +314,51 @@ structure SchoenhageSchedule (N : Nat) where decreasing : L < N ``` -`blocks` splits the `2N`-coefficient representative into `2 * 3^k` blocks of -length `M`. `aligned` makes the root exponent `L / 3^k` an integer, so the -residue `ω = y^(L / 3^k)` of the inner carrier satisfies `ω^(3K) = y^(3L) = 1` -with `ω^K = y^L ≠ 1`, and the identity `1 + ω^K + ω^(2K) = 0` needed by the -transform's cancellations is exactly the defining relation of the carrier. -The `2K` evaluation points are the powers `ω^j` with `j` not divisible by -three; the transform reaches them as two radix-3 length-`K` transforms of -`ω`-twisted block sequences, and every twiddle multiplication is a -`mulByYPow` fold. `block_fits` makes the inner carrier hold each wrapped -block sum exactly. `decreasing` is the strict-decrease fact that drives the -well-founded recursion. `schedule? : Nat → Option (SchoenhageSchedule N)` -chooses `k` so that `L` is near `sqrt N` (the balanced choice behind the -`log log` recursion depth); correctness must not depend on which valid -schedule is chosen, only on the fields above. `L` is in general not a -multiple of the word size, and the packed kernel in hex-gf2 must not round -it up to one (Brent-Gaudry-Thomé-Zimmermann §3.2). - -**The recursion.** One triadic product modulo `x^(2N) + x^N + 1` with a -valid schedule reduces to `2 * 3^k` pointwise triadic products modulo -`y^(2L) + y^L + 1`, glued by forward and inverse symbolic transforms whose -twiddle multiplications are `mulByYPow` folds, plus the inverse scaling, -which multiplies by powers of the inverse-of-three witness. Recursive calls -multiply the pointwise operands through the same plan at half-length `L`; -when `schedule?` returns `none` or the size is below the committed cutoff, -the recursion delegates to a supplied base plan. Termination is by -`decreasing`. +The equations `N = K * M`, `M ≤ L`, and `K ∣ L` are the parameter constraints +used in Figure 3 of Brent, Gaudry, Thomé, and Zimmermann. They split a +representative of length `2N` into `2K` blocks of length `M`, ensure that one +block fits in the inner carrier, and make `L / K` integral. The strict +inequality `L < N` proves termination. + +Set `ω = y^(L / K)` in the inner triadic carrier. The general identities give +`ω^(3K) = 1` and `1 + ω^K + ω^(2K) = 0`. With `[Nontrivial R]`, the exact-order +and distinct-point theorems also give `ω^K ≠ 1`. The algorithm evaluates at +the `2K` powers `ω^j` for which three does not divide `j`. It obtains these +values from two twisted radix-3 transforms of length `K`. Every twiddle is a +call to `mulByYPow`. + +Correctness uses only the fields of `SchoenhageSchedule`. Complexity also +uses chooser theorems. There are constants and a threshold such that every +sufficiently large requested product length `s` has `N` and `σ` with + +```text +s ≤ 2 * N ≤ C0 * s +schedule? N = some σ +N ≤ cK0 * σ.K * σ.K +σ.K * σ.K ≤ cK1 * N +N ≤ cL0 * σ.L * σ.L +σ.L * σ.L ≤ cL1 * N +``` + +where `σ.K = 3 ^ σ.k`. These inequalities place `K` and `L` within constant +factors of `sqrt N`. The chooser also proves recursive completeness: if the +`L` generated by a chosen schedule is above the committed base cutoff, then +`schedule? L` returns a schedule satisfying the same balance inequalities. +The packed implementation must retain the selected `L`. In general it is not +a multiple of the machine-word width, as noted in §3.2 of the same paper. + +**The recursion.** For each operand, one triadic product modulo +`x^(2N) + x^N + 1` computes the two twisted forward transforms described +above. It then computes `2K` recursive pointwise products modulo +`y^(2L) + y^L + 1` and applies the corresponding inverse transforms. Inverse +scaling uses powers of `inv3`. A recursive call has half-length `L`. +`decreasing` supplies the well-founded decrease. At or below the cutoff, the +worker calls the supplied base multiplication. + +For an arbitrary valid schedule, one transform performs +`O(K * L * k)` coefficient operations. The simplification to `O(N * k)` is +valid only after applying the chooser's two-sided balance bounds. Schedule +selection occurs once at each recursion level. **The public plan.** @@ -346,26 +367,28 @@ def schoenhagePlan (base : MulPlan R) (cutoff : Nat) (inv3 : R) (inv3_spec : 3 * inv3 = 1) : MulPlan R ``` -The full product pads to the least scheduled `2N` with -`a.size + b.size - 1 ≤ 2 * N`, computes the triadic product, and reads the -ordinary product off the residue, which is exact because the true product -has degree below the modulus degree. `square` is `mul a a` and `slice` is -`coeffSlice` of the full product. Both choices are deliberate and accepted -under the no-placeholder rule: a transform-based product computes every -output coefficient at once, so a specialized square or slice saves at most a -constant factor, and the Karatsuba plan's pruned slice remains the tool for -clipped products in its own range. `mul_eq`, `square_eq`, and `coeff_slice` -are the plan laws, stated as always against schoolbook semantics. +For nonempty inputs, let `s = a.size + b.size - 1`. The padding chooser +returns `N` and `σ` with `s ≤ 2N`. The plan embeds both inputs into the +triadic problem, computes the residue, and returns its first `s` +coefficients. Since the ordinary product has degree below `2N`, reduction by +the degree-`2N` modulus does not change it. + +The plan defines `square a` as `mul a a` and defines `slice` by slicing the +full product. A transform computes all output coefficients, so specialized +versions can improve these operations only by a constant factor. The +Karatsuba plan retains its pruned slice for sizes at which that plan is +selected. The laws `mul_eq`, `square_eq`, and `coeff_slice` identify all three +operations with the existing schoolbook semantics. + +Correctness holds for every lawful `base`. The operation-count theorem in +hex-poly-fast-cslib fixes `base` to the counted Karatsuba worker and allows +its constant to depend on the Karatsuba cutoff. Supplying another base plan +preserves correctness but provides no operation bound. ### Operation-parametric workers -The counted models of this library's algorithms, their cost-obliviousness -properties, and their operation bounds are specified in -[hex-poly-fast-cslib](../../SPEC/Libraries/hex-poly-fast-cslib.md). A bound -proved about a program that merely returns the same polynomial would be -vacuous, because every lawful plan returns the same polynomial. The -faithfulness mechanism is that each counted algorithm body is written -exactly once, parametric over a monad and its coefficient operations: +The proof-facing Karatsuba and Schönhage definitions use workers that are +parametric in coefficient operations: ```lean structure CoeffOps (m : Type → Type) (R : Type) where @@ -381,16 +404,18 @@ def karatsubaWorker [Monad m] (ops : CoeffOps m R) (cutoff : Nat) : def schoenhageWorker [Monad m] (ops : CoeffOps m R) ... : m (Array R) ``` -The `idOps` instantiations are the executable definitions: the Karatsuba -recursion and the Schönhage recursion of this SPEC are *defined as* their -workers at `idOps`, so a theorem about a worker is a theorem about the -algorithm this library performs, not about a parallel reformulation. The -companion instantiates the same workers at a free-monad operations record -and counts queries. Workers cover the public dispatch structure (cutoffs, -the balanced and blocked Karatsuba paths, schedule selection), not only the -balanced textbook recursion. The raw array runtimes remain connected by the -existing output-equality `@[csimp]` theorems; operation counts are claims -about the workers, and the SPEC does not claim them for the raw runtimes. +The logical definitions are the `idOps` instantiations. The planned +[hex-poly-fast-cslib](../../SPEC/Libraries/hex-poly-fast-cslib.md) companion +instantiates the same workers with `FreeM (ArithQuery R)` and counts the +resulting base-ring queries. The Karatsuba worker includes cutoff selection, +balanced recursion, blocking, and unbalanced dispatch. The Schönhage worker +includes padding, schedule selection, transforms, recursion, and its counted +Karatsuba base. + +The raw array definitions used by the `@[csimp]` replacements remain related +to the logical definitions by output equality only. The companion proves no +trace or cost relation for those raw definitions. Its operation bounds apply +to the operation-parametric workers, which are the proof-facing definitions. ## Reversal and truncated series @@ -811,8 +836,8 @@ Let `M(n)` be the measured balanced multiplication cost of the selected plan. | unbalanced `m x n`, `m >= n` | `O(ceil(m/n) * M(n))` | | triadic reference fold | `O(n)` coefficient operations | | `Triadic.mulByYPow` | `O(L)` coefficient additions, no ring multiplications | -| symbolic radix-3 transform | `O(K log K)` carrier additions and `mulByYPow` folds | -| Schönhage full product | `O(n log n log log n)` coefficient operations | +| one radix-3 transform | `O(K * L * log K)` coefficient operations | +| Schönhage worker with counted Karatsuba base | `O(n log n log log n)` coefficient operations | | radix-2 NTT convolution | `O(n log n)` word operations | | reciprocal and division | `O(M(n))` | | half-gcd / extended gcd | `O(M(n) log n)` | @@ -826,12 +851,13 @@ remainder-tree node, pads an unbalanced product to the longer size, or rebuilds an NTT root table inside each transform violates the SPEC even if it returns the correct polynomial. -The Schönhage recursion adds its own body-shape constraints. The schedule is -computed once per level, never inside the transform loops. Twiddle -multiplications are `mulByYPow` folds; a twiddle implemented as a carrier -product violates the SPEC. `Triadic` values are never trimmed or normalized -between transform stages, and transform scratch is reused across butterflies -at one level rather than allocated per butterfly. +The Schönhage worker selects one schedule per recursion level. A transform +uses `mulByYPow` for every twiddle and never substitutes a general carrier +product. It retains the fixed `2L` coefficient positions between transform +stages and reuses scratch storage within a level. The schedule chooser must +prove bounded padding, balanced `K` and `L`, and recursive completeness. The +operation bound is for the worker with its counted Karatsuba base. A lawful +but uncounted base plan receives only the correctness theorem. ## Kernel exposure and trust @@ -858,7 +884,7 @@ hexpolyfast_emit_fixtures` emits the committed the kernel selected by its public dispatcher; - `divmod`, `gcd`, `xgcd`, and `xgcd_left`; - `cyclic`, `negacyclic`, and `triadic`; -- forced-Schönhage `mul` cases across schedule boundaries; +- forced Schönhage multiplication on both sides of every schedule change; - `eval_many` and `interpolate`; - `pade` with the homogeneous relation and normalized success/failure; - NTT plan, round-trip, direct convolution, and CRT convolution cases; @@ -877,10 +903,10 @@ Mandatory edge families: - operand ratios from balanced through at least 64:1; - empty, one-coefficient, last-coefficient, and wholly out-of-range slices; - positive and negative coefficients at every Kronecker digit bound; -- triadic length `m = 1`, exponents in every residue class modulo `3 * m`, - and inputs whose reduction cancels a leading slot; -- Schönhage sizes at the smallest schedulable `N`, at `M = L`, at an `L` not - divisible by the word size, and immediately below the base-plan cutoff; +- triadic length `m = 1`, every residue class modulo `3 * m`, and cancellation + at the highest stored position; +- Schönhage inputs at the smallest scheduled `N`, at `M = L`, at an `L` not + divisible by the word width, and immediately below the base cutoff; - NTT lengths `1`, `2`, the largest catalogue length, and one beyond it. The largest case is an allocation-free theorem check in the coefficient owner's conformance module; the executable stream calls `NttPrime.plan?` on the @@ -906,9 +932,9 @@ Required families: - schoolbook, Karatsuba, square, and clipped products over `Int`, `Rat`, and small `ZMod64` fields, with degrees from 4 through at least 16384; -- Schönhage against Karatsuba over `ZMod64 2`, with degrees extended until - the crossover is bracketed (the packed `GF2Poly` ladder is a hex-gf2 - family); +- the generic Schönhage worker against Karatsuba over `ZMod64 2`, with degrees + extended through their crossover. Packed `GF2Poly` comparisons belong to + hex-gf2; - balanced and unbalanced shapes, with ratios 1, 2, 4, 16, and 64; - KS1/KS2/KS3/KS4 over the current degree/coefficient-width grid, extended into the GMP Karatsuba, Toom, and FFT regimes; @@ -1007,15 +1033,14 @@ Likewise, evaluation and interpolation soundness are stated directly with `DensePoly.eval`; a later Mathlib-facing consumer can rewrite through the existing equivalence. -Proved operation-count theorems live in -[hex-poly-fast-cslib](../../SPEC/Libraries/hex-poly-fast-cslib.md), a -proof-only companion in the style of the `-mathlib` libraries: this -computational library stays free of both Mathlib and cslib, and the -companion models its algorithms in cslib's query-complexity framework and -proves explicit coefficient-operation bounds about them. The executable -complexity contracts here remain enforced by body shape and benchmarks; the -companion's theorems are about the parametric workers this library exposes, -not about the raw array runtimes. +The planned +[hex-poly-fast-cslib](../../SPEC/Libraries/hex-poly-fast-cslib.md) library +proves coefficient-operation bounds for the operation-parametric Karatsuba +and Schönhage workers. It imports cslib and Mathlib, while this library +imports neither. The raw array definitions selected by `@[csimp]` have only +output-equality theorems relating them to the workers, so the proved bounds do +not apply to those raw definitions. Benchmarks and the structural constraints +in this SPEC remain the evidence for their performance. ## Milestones @@ -1040,22 +1065,22 @@ not about the raw array runtimes. conformance/benchmark families. 9. **Adoption.** Audit the named consumers, switch only winning cells, update their owning SPECs and benchmarks, and keep the single-job CI topology. -10. **Triadic references.** The triadic fold, its canonical-remainder law, - the fixed-length `Triadic` carrier, and the carrier agreement theorems. - Also `CoeffOps` and the refactor of the Karatsuba recursion and - dispatcher through `karatsubaWorker` at `idOps`, preserving every - existing theorem statement. -11. **Schönhage plan.** The schedule structure and chooser, the symbolic - radix-3 transforms and their round-trip and convolution theorems, the - operation-parametric recursion worker, `schoenhagePlan`, and its plan - laws. The packed `F_2` kernel and its dispatch are hex-gf2 milestones; - the counted model and its bound are hex-poly-fast-cslib milestones. +10. **Triadic arithmetic and workers.** Add the triadic fold, its remainder + theorem, the positive-length fixed carrier, and the carrier operation + theorems. Define `CoeffOps`. Express the proof-facing Karatsuba recursion + and dispatcher as `karatsubaWorker idOps` without changing their public + correctness statements. +11. **Schönhage multiplication.** Add `SchoenhageSchedule`, the chooser with + bounded-padding and balance theorems, the radix-3 transforms, and their + round-trip and convolution theorems. Define `schoenhageWorker` and + `schoenhagePlan`, then prove the plan laws. HexGF2 owns the packed + implementation. HexPolyFastCslib owns the operation-count proof. No later milestone may be used to excuse a quadratic placeholder in an earlier one. In particular, milestone 3 implements Newton division with clipped products, milestone 4 implements an actual half-gcd recursion rather than -renaming the Euclidean loop, and milestone 11 implements the square-rooting -recursion rather than a single transform level over a quadratic base case. +renaming the Euclidean loop, and milestone 11 recurses through balanced +schedules until the Karatsuba cutoff. ## File organisation @@ -1065,13 +1090,13 @@ HexPolyFast/ Karatsuba.lean -- full, square, unbalanced, and clipped recursion Cyclic.lean -- cyclic and negacyclic reference operations CyclicRemainder.lean -- cyclic and negacyclic canonical remainder laws - Triadic.lean -- triadic reference fold - TriadicRemainder.lean -- triadic canonical remainder law + Triadic.lean -- positive-length triadic fold + TriadicRemainder.lean -- canonical remainder theorem Schoenhage/ - Carrier.lean -- fixed-length Triadic carrier and its operations - Schedule.lean -- SchoenhageSchedule and schedule? - Transform.lean -- symbolic radix-3 transforms - Plan.lean -- parametric worker and schoenhagePlan + Carrier.lean -- fixed-length carrier operations + Schedule.lean -- schedules, chooser, padding, balance + Transform.lean -- radix-3 transforms + Plan.lean -- worker and lawful plan Reverse.lean -- DensePoly/TSeries bridges Reciprocal.lean -- plan-driven Newton inverse Division.lean -- DivPlan and one-shot division @@ -1141,10 +1166,10 @@ implementation changes actually land, never by this SPEC-only change. middle-product construction that the integer algorithm adapts; it does not add a limb-level integer primitive. - Arnold Schönhage, *Schnelle Multiplikation von Polynomen über Körpern der - Charakteristik 2*, Acta Informatica 7 (1977), 395-398. The radix-3 - algorithm behind `schoenhagePlan`. + Charakteristik 2*, Acta Informatica 7 (1977), 395-398. This paper gives + the radix-3 multiplication used by `schoenhagePlan`. - Richard P. Brent, Pierrick Gaudry, Emmanuel Thomé, and Paul Zimmermann, [*Faster Multiplication in GF(2)[x]*](https://doi.org/10.1007/978-3-540-79456-1_10), - ANTS-VIII (2008), LNCS 5011, 153-166. §3.2 is the implementation reference - for the schedule constraints and for the warning that `L` is generally not + ANTS-VIII (2008), LNCS 5011, 153-166. Figure 3 supplies the constraints + `N = K * M`, `M ≤ L`, and `K ∣ L`. Section 3.2 notes that `L` need not be word-aligned. diff --git a/SPEC/Libraries/README.md b/SPEC/Libraries/README.md index 040956bfe..c76087578 100644 --- a/SPEC/Libraries/README.md +++ b/SPEC/Libraries/README.md @@ -11,7 +11,7 @@ - **hex-mv-hensel**: multivariate Hensel lifting against an evaluation ideal, with the coprimality witness, leading-coefficient contract, and reconstruction that Wang's EEZ factorization needs - **hex-mv-factor**: factorization of `Z[x_1, ..., x_n]` by Wang's EEZ algorithm, with a checked product decomposition and a separate irreducibility certificate - **hex-truncated-series**: power series truncated at a precision fixed in the type, with Newton inversion, square root, `exp`, `log`, composition, and reversion -- **hex-poly-fast**: explicit lawful multiplication plans, Karatsuba and clipped products, Schönhage's radix-3 multiplication with triadic reference semantics, Newton division, half-gcd, multipoint evaluation/interpolation, and Padé approximation +- **hex-poly-fast**: explicit lawful multiplication plans, Karatsuba and clipped products, planned Schönhage radix-3 multiplication with triadic reference semantics, Newton division, half-gcd, multipoint evaluation/interpolation, and Padé approximation - **hex-matrix**: dense matrices, matrix/vector arithmetic, elementary row and column operations, submatrix slicing, the Gram matrix - **hex-row-reduce**: row reduction (RREF), rank, span, nullspace - **hex-determinant**: the Leibniz determinant and its cofactor/Cauchy-Binet/Plücker theory @@ -31,7 +31,7 @@ - **hex-modular-matrix**: multi-modular determinant, certified rank, and Dixon p-adic linear solving over `Q` - **hex-finite-field**: the Mathlib-free `F_q` interface (characteristic, degree, Frobenius, indexing), the generic `q`-power Frobenius and Frobenius matrix - **hex-poly-fp**: polynomials over `F_p`, Frobenius map, square-free decomposition, packed/NTT/CRT-NTT multiplication, lazy reduction for small p -- **hex-gf2**: packed bitwise polynomials over `F_2` (XOR + CLMUL) with the schoolbook/Karatsuba/Schönhage multiplication ladder, `GF(2^n)` elements +- **hex-gf2**: packed bitwise polynomials over `F_2` (XOR + CLMUL), a planned schoolbook/Karatsuba/Schönhage multiplication ladder, `GF(2^n)` elements - **hex-poly-z**: polynomials over `Z`, content/primitive part, Mignotte bound, multipoint Kronecker and CRT-NTT multiplication - **hex-poly-z-gcd**: modular gcd for `Z[x]` with cofactors, a coprimality witness, and exact division - **hex-cyclotomic**: dense integer cyclotomic polynomials from a checked factorization of the index, the divisor family, and the factorization of `x^n - 1` @@ -100,15 +100,14 @@ Mathlib, and supplies correspondence proofs or Mathlib-facing APIs): - **hex-summation-mathlib**: `Finset.sum` semantics over characteristic-zero fields, the `Nat.choose` / `Nat.factorial` / `ascPochhammer` ratio kit, the summand recognizer, and the `gosper`, `zeilberger`, and `hyper` tactics - **hex-graph-iso-mathlib**: correspondence with finite `SimpleGraph`, ordered-colour isomorphisms, and the `SimpleGraph` extension of `graph_iso` -**cslib companion libraries** (each depends on a computational library and -on [cslib](https://github.com/leanprover/cslib), which itself depends on -Mathlib; they prove operation-count bounds in cslib's query-complexity -framework about the algorithms their computational owners execute): +**cslib companion libraries** (planned proof-only libraries that depend on a +computational library and on +[cslib](https://github.com/leanprover/cslib), which itself depends on +Mathlib): -- **hex-poly-fast-cslib**: coefficient-operation bounds for the Karatsuba - dispatcher and Schönhage's radix-3 multiplication, with the - specialization and cost-obliviousness theorems that tie the counted - programs to the executable workers +- **hex-poly-fast-cslib**: coefficient-operation bounds for the proof-facing + Karatsuba and Schönhage workers, including specialization and + cost-obliviousness theorems. The bounds exclude raw `@[csimp]` runtimes. ## Implementation dependencies @@ -163,7 +162,7 @@ Each library with its immediate dependencies: - **hex-gfq-ring**: hex-poly-fp - **hex-gfq-field**: hex-gfq-ring, hex-berlekamp, hex-finite-field - **hex-gfq**: hex-gfq-field, hex-conway, hex-gf2 -- **hex-gf2**: hex-basic, hex-poly, hex-poly-fast, hex-mod-arith, hex-finite-field +- **hex-gf2**: hex-basic (specified additions: hex-finite-field, hex-poly, hex-poly-fast, hex-mod-arith) - **hex-berlekamp-zassenhaus**: hex-berlekamp, hex-hensel, hex-lll - **hex-summation**: hex-poly, hex-mv-poly, hex-resultant, hex-matrix, hex-row-reduce, hex-berlekamp-zassenhaus, hex-basic @@ -213,8 +212,8 @@ Mathlib companion libraries (each also depends on Mathlib): - **hex-summation-mathlib**: hex-summation - **hex-graph-iso-mathlib**: hex-graph-iso -cslib companion libraries (each also depends on cslib, and through it on -Mathlib): +cslib companion libraries (planned, each also depends on cslib and therefore +on Mathlib): - **hex-poly-fast-cslib**: hex-poly-fast @@ -518,22 +517,28 @@ hex-poly-z owns multipoint Kronecker and integer CRT-NTT dispatch. The complete boundary and staged dependency change are specified in [hex-poly-fast](../../HexPolyFast/SPEC/hex-poly-fast.md). -hex-gf2 joins this corner the same way hex-poly-fp did: it moves above -hex-poly-fast (and hex-mod-arith, for the `ZMod64 2` coefficient type) so it -can own the packed Schönhage kernel for `F_2[x]`, whose correctness goes -through the generic triadic algorithm: +The planned hex-gf2 multiplication ladder adds dependencies on hex-poly, +hex-poly-fast, and hex-mod-arith. HexGF2 will use `DensePoly (ZMod64 2)` to +prove the packed Schönhage kernel correct against the generic triadic +algorithm: ```text -hex-poly-fast ──┐ -hex-mod-arith ──┼── hex-gf2 -hex-basic ──────┘ +hex-poly ───────────┐ +hex-poly-fast ──────┤ +hex-mod-arith ──────┼── hex-gf2 +hex-finite-field ───┤ +hex-basic ──────────┘ ``` -Beside the Mathlib companions there is one cslib companion so far. -`hex-poly-fast-cslib` depends on hex-poly-fast and cslib, and proves -coefficient-operation bounds for the Karatsuba and Schönhage workers; like -the `-mathlib` layers it is proof-only and sits outside the Mathlib-free -build surface: +`hex-poly-fast` depends on `hex-truncated-series`. Neither library is yet in +[`scripts/release/released.yml`](../../scripts/release/released.yml). The +released hex-gf2 mirror can add these dependencies only after +hex-truncated-series and hex-poly-fast are published in dependency order. +The monorepo build is not blocked by this release ordering. + +The planned `hex-poly-fast-cslib` library depends on hex-poly-fast and cslib. +It proves coefficient-operation bounds for the proof-facing Karatsuba and +Schönhage workers. It has no computational or benchmark target: ```text hex-poly-fast ── hex-poly-fast-cslib @@ -662,10 +667,10 @@ for developments whose source-local move has not happened yet. - [hex-mv-factor.md](../../HexMvFactor/SPEC/hex-mv-factor.md): factorization of `Z[x_1, ..., x_n]` by Wang's EEZ algorithm, the evaluation-point and leading-coefficient search, the checked product decomposition, and the separate irreducibility certificate (the Mathlib companion is specified in the same file) - [hex-truncated-series](../../HexTruncatedSeries/SPEC/hex-truncated-series.md): power series truncated at a precision fixed in the type, Newton inversion, square root, `exp`, `log`, composition, and reversion - [hex-truncated-series-mathlib](../../HexTruncatedSeriesMathlib/SPEC/hex-truncated-series-mathlib.md): quotient-by-`X ^ n` equivalence and operation correspondence -- [hex-poly-fast.md](../../HexPolyFast/SPEC/hex-poly-fast.md): explicit lawful multiplication plans, Karatsuba and clipped products, Schönhage's radix-3 multiplication with triadic reference semantics, Newton division, half-gcd, multipoint evaluation/interpolation, and Padé approximation -- [hex-poly-fast-cslib.md](hex-poly-fast-cslib.md) (planned): coefficient-operation bounds for the Karatsuba dispatcher and Schönhage's radix-3 multiplication, in cslib's query-complexity framework +- [hex-poly-fast.md](../../HexPolyFast/SPEC/hex-poly-fast.md): explicit lawful multiplication plans, Karatsuba and clipped products, planned Schönhage radix-3 multiplication with triadic reference semantics, Newton division, half-gcd, multipoint evaluation/interpolation, and Padé approximation +- [hex-poly-fast-cslib.md](hex-poly-fast-cslib.md) (planned): coefficient-operation bounds for the proof-facing Karatsuba and Schönhage workers in cslib's query-complexity framework - [hex-poly-fp](../../HexPolyFp/SPEC/hex-poly-fp.md): polynomials over `F_p`, Frobenius, square-free decomposition, and packed/direct-NTT/CRT-NTT multiplication -- [hex-gf2](../../HexGF2/SPEC/hex-gf2.md): packed bitwise polynomials over `F_2` with the schoolbook/Karatsuba/Schönhage multiplication ladder, `GF(2^n)` elements +- [hex-gf2](../../HexGF2/SPEC/hex-gf2.md): packed bitwise polynomials over `F_2`, a planned schoolbook/Karatsuba/Schönhage multiplication ladder, `GF(2^n)` elements - [hex-gf2-mathlib](../../HexGF2Mathlib/SPEC/hex-gf2-mathlib.md): `GF2Poly ≃+* FpPoly 2`, `GF2n`/`GF2nPoly ≃+* FiniteField 2 f hf hirr`, packed-field finiteness/cardinality - [hex-poly-fp-mathlib](../../HexPolyFpMathlib/SPEC/hex-poly-fp-mathlib.md): `FpPoly p ≃+* Polynomial (ZMod p)`, the crossing point to Mathlib's polynomial type - [hex-poly-z](../../HexPolyZ/SPEC/hex-poly-z.md): polynomials over `Z`, content/primitive part, Mignotte bound, multipoint Kronecker, and CRT-NTT multiplication diff --git a/SPEC/Libraries/hex-poly-fast-cslib.md b/SPEC/Libraries/hex-poly-fast-cslib.md index 18f59aa94..570e49363 100644 --- a/SPEC/Libraries/hex-poly-fast-cslib.md +++ b/SPEC/Libraries/hex-poly-fast-cslib.md @@ -1,110 +1,95 @@ -# hex-poly-fast-cslib (operation-count bounds, depends on hex-poly-fast and cslib) - -Proved coefficient-operation bounds for the generic multiplication -algorithms of -[hex-poly-fast](../../HexPolyFast/SPEC/hex-poly-fast.md), built on the -query-complexity framework of the Lean computer-science library -[cslib](https://github.com/leanprover/cslib). This is the first `-cslib` -companion library. It plays the same architectural role for complexity -that the `-mathlib` companions play for Mathlib correspondence: the -computational library stays free of the external dependency, and the -companion proves theorems about it. +# hex-poly-fast-cslib (operation counts, depends on hex-poly-fast and cslib) + +This planned library proves coefficient-operation bounds for the +operation-parametric multiplication workers specified by +[hex-poly-fast](../../HexPolyFast/SPEC/hex-poly-fast.md). It uses the query +complexity definitions from +[cslib](https://github.com/leanprover/cslib). `HexPolyFast` remains free of +Mathlib and cslib. ## Complexity-layer classification -This library is a `complexity-layer`. - -Computational conformance owner: `HexPolyFast` -Computational performance owner: `HexPolyFast` - -A complexity-layer library contains no algorithms of its own, no -conformance fixtures, no oracles, and no benchmarks. Its theorems bound -the number of coefficient operations performed by programs that are, by -the specialization theorems below, the algorithms its computational owner -executes. It claims nothing about wall-clock time; benchmarks in the -owning library remain the only evidence of speed. - -## Why this library exists - -**hex-poly-fast enforces complexity by body shape and benchmarks, and that -enforcement has no theorem.** Its complexity-contract table is a review -obligation: a quadratic body violates the SPEC, but nothing in the build -proves the bound. For most of the library that is the right trade, because -the contracts are simple enough to check by reading. The Schönhage -recursion is not: its bound depends on a schedule invariant -(`L` near `sqrt N` at every level), and an implementation that satisfies -every local body-shape rule can still lose the global bound by choosing -schedules badly. A proved operation count is the review tool that scales. - -**The bound must be a theorem about the shipped algorithm.** Every lawful -`MulPlan` returns the same polynomial, so a bound proved about a program -that merely agrees with the plan's output is vacuous. hex-poly-fast -therefore defines its counted algorithms once, as operation-parametric -workers, and executes them at the identity monad. This library -instantiates the same workers at a free monad and counts. The two -instantiations are connected by a specialization theorem, not by output -equality. - -**The dependency must stay out of the computational graph.** cslib -requires Mathlib. Placing operation counts in the computational libraries -would pull both into every consumer, which is the exact failure the -`-mathlib` split exists to prevent. The companion pattern already solves -this, and this library extends it to a second external proof dependency. - -hex-poly-fast's SPEC previously assigned any future asymptotic theorem to -"that consumer or a documentation proof". This library is the considered -replacement of that position, and hex-poly-fast's §The Mathlib layer now -points here. +The library will have classification `complexity_layer: true`. + +- Computational conformance owner: `HexPolyFast`. +- Computational performance owner: `HexPolyFast`. + +A complexity layer contains proofs and definitions used by those proofs. It +does not own executable polynomial operations, conformance targets, external +oracles, benchmark targets, or a performance report. Its library entry names +the computational owners whose tests and measurements cover the operations +under study. This classification is defined in +[benchmarking](../benchmarking.md#comparator-naming) and +[testing](../testing.md#where-cross-check-content-lives). + +The specified results concern base-ring additions, subtractions, and +multiplications issued by the proof-facing workers. They do not estimate +elapsed time, allocation, machine instructions, or packed-word operations. + +## Motivation + +The complexity table in `HexPolyFast` constrains implementation structure and +benchmark behaviour. It does not itself prove an operation count. A proof is +useful for the Schönhage recursion because the bound depends on parameter +selection at every recursive level, including the amount of padding and the +balance between the transform length and the inner modulus length. + +Output equality alone cannot support such a result. Every lawful `MulPlan` +returns schoolbook multiplication, regardless of its implementation. The +counted definitions must therefore expose the operations performed by the +specific worker being analysed. `HexPolyFast` supplies one worker body +parametric in its coefficient operations. The identity interpretation gives +the proof-facing definition. The free interpretation gives the program whose +queries this library counts. + +The raw array definitions selected by `@[csimp]` are separate definitions. +Their current theorems prove output equality with the proof-facing +definitions. They do not prove equality of operation traces or costs. No bound +in this SPEC applies to those raw definitions. A later change could define +each raw runtime as an erasure of its worker and prove cost preservation, but +that is not required here. ## Dependency and pin policy -This library requires cslib, and cslib requires Mathlib. It is therefore -marked and treated like a `-mathlib` library: proof-only, no -`precompileModules`, no benches, and outside the Mathlib-free build -surface. +cslib depends on Mathlib, so this library will follow the build restrictions +for proof-only libraries that import Mathlib. It will have no +`precompileModules` setting and no benchmark or conformance target. +Computational libraries may not import it. Until cslib PR -[#401](https://github.com/leanprover/cslib/pull/401) merges, the lakefile -pins cslib to a recorded commit of that PR's branch (at SPEC time, -`36e098cfc04fbb8e9b44086d64ce433514ee18d4`). The pin is updated by ordinary -dependency bumps. The verified compatibility state at SPEC time: - -- cslib's and hex-dev's Lean toolchains agree (`v4.34.0-rc2`). -- cslib pins a newer Mathlib than hex-dev. Lake resolves dependencies from - the root manifest, so cslib builds against hex-dev's Mathlib revision. - The `Cslib.Algorithms.Lean.Query.*` modules this library imports build - cleanly against that revision. A handful of unrelated cslib modules - (the omega-sequence topology corner) import a Mathlib file that does not - exist at hex-dev's revision; they are not imported here and are never - built as dependencies. -- This library imports only `Cslib.Algorithms.Lean.Query.*` and the - `FreeM` foundations they re-export, never the `Cslib` umbrella module. - -Releasing or publishing this library requires a merged cslib revision (or -a maintained fork with a stable branch); a floating PR commit is -acceptable only inside the monorepo. - -## The query model - -Programs are `Cslib.FreeM Q α` values over cslib's arithmetic query type: +[#401](https://github.com/leanprover/cslib/pull/401) merges, development uses +commit `36e098cfc04fbb8e9b44086d64ce433514ee18d4`. The integration check replaced +cslib's Mathlib pin with hex-dev revision +`85e3a25e006c35636f0e53b0e9296caca2685bc0`. The +`Cslib.Algorithms.Lean.Query.*` modules required here built at that revision. +A build of the complete `Cslib` target did not succeed: unrelated +modules under `Cslib.Foundations.Data.OmegaSequence` and +`Cslib.Foundations.Combinatorics.InfiniteGraphRamsey` require +`Mathlib.Data.Set.Lattice.Bounded`, which is absent at the hex-dev revision. +This library therefore imports the query modules directly and never imports +the `Cslib` umbrella module. + +Publication requires a merged cslib revision or a maintained revision with a +stable source. A commit from an unmerged pull-request branch is permitted for +monorepo development only. + +## Query model + +The counted program type is `Cslib.FreeM (ArithQuery R) α`. The query type is: ```lean -inductive ArithQuery (α : Type) : Type → Type where - | add (a b : α) : ArithQuery α α - | sub (a b : α) : ArithQuery α α - | mul (a b : α) : ArithQuery α α +inductive ArithQuery (R : Type) : Type → Type where + | add (a b : R) : ArithQuery R R + | sub (a b : R) : ArithQuery R R + | mul (a b : R) : ArithQuery R R ``` -with cslib's `honest` oracle interpreting queries by the actual ring -operations, `FreeM.eval` for results, and `FreeM.cost` with -`ArithQuery.weight c_add c_mul` for weighted counts (subtraction weighs as -addition; multiplication weighs separately, because multiplications drive -the recursions). If the upstream `Arith` files change shape before the pin -is next moved, an equivalent local query type replaces them with no change -to the theorem statements; the pin makes this a scheduled decision rather -than a build break. +`ArithQuery.honest` returns the corresponding ring operation. The cost +function `ArithQuery.weight c_add c_mul` assigns `c_add` to addition and +subtraction and assigns `c_mul` to multiplication. This is the only weight +family used by the obliviousness and upper-bound theorems. -The instantiation record is one definition: +The free interpretation of `CoeffOps` is: ```lean def freeOps : CoeffOps (FreeM (ArithQuery R)) R where @@ -113,18 +98,21 @@ def freeOps : CoeffOps (FreeM (ArithQuery R)) R where mul a b := FreeM.lift (.mul a b) ``` -`CoeffOps` and the workers are hex-poly-fast's; this library adds no -algorithm text. Every quotient-ring operation of the Schönhage recursion -is scalar-expanded: `Triadic` elements are fixed-shape data, their -additions and twiddle folds issue base-ring queries coefficient by -coefficient, and pointwise products recurse through the same worker. The -bounds therefore count base-ring operations, which is the standard -algebraic complexity measure and what the headline inequality means. +The fixed-length triadic operations expand into queries over `R`. Carrier +addition and subtraction issue one query for each affected coefficient. +Multiplication by a power of `y` issues additions or subtractions according +to the triadic fold. A pointwise carrier product calls the same recursive +worker. Quotient-ring operations are not counted as primitive queries. + +If the upstream arithmetic example changes before the dependency is updated, +this library may define an equivalent local query type. The public cost +statements retain separate addition and multiplication weights. ## Specialization -For each worker, the specialization theorem identifies running the free -program under the honest oracle with the executable algorithm: +Each worker will have an interpretation theorem. The Karatsuba theorem has +the following required form, with the actual worker arguments retained in the +implemented statement: ```lean theorem karatsubaWorker_eval (cutoff fuel : Nat) (a b : Array R) : @@ -132,39 +120,41 @@ theorem karatsubaWorker_eval (cutoff fuel : Nat) (a b : Array R) : karatsubaWorker idOps cutoff fuel a b ``` -and likewise for the Schönhage worker. The proof is induction over the -worker body (or one generic lemma about interpreting `freeOps` through -`FreeM.liftM`). Because hex-poly-fast *defines* its recursions as the -`idOps` instantiations, this theorem makes every count below a statement -about the algorithm hex-poly-fast executes. The raw array runtimes are -connected to those definitions by output-equality `@[csimp]` theorems -only, and no operation count is claimed for them. +There is an analogous theorem for `schoenhageWorker` with the counted +Karatsuba base. The proof interprets each `FreeM.lift` by the corresponding +identity operation and follows the worker recursion. These theorems identify +the result of the free program under the honest oracle with the proof-facing +worker. They make no statement about a raw `@[csimp]` replacement. ## Cost obliviousness -Query traces are not oracle-independent: queries embed operands, and a -dishonest oracle changes the operands of later queries. What holds for -these workers is the weaker, sufficient property that the *cost* does not -depend on the oracle: +Queries contain their operands. An arbitrary oracle can change an operand +used by a later query, so query values and complete query traces need not be +oracle-independent. The required property concerns only the +constructor-determined weight: ```lean -def CostOblivious {T : Type} [AddMonoid T] - (weight : {ι : Type} → Q ι → T) (p : FreeM Q α) : Prop := - ∀ o₁ o₂, p.cost o₁ weight = p.cost o₂ weight +def CostOblivious (p : FreeM (ArithQuery R) α) + (c_add c_mul : Nat) : Prop := + ∀ o₁ o₂, + p.cost o₁ (ArithQuery.weight c_add c_mul) = + p.cost o₂ (ArithQuery.weight c_add c_mul) ``` -Each worker's program is proved `CostOblivious` for every weight: its -control flow (splits, schedule choice, recursion depth, base-case entry) -depends only on sizes and the schedule, never on coefficient values. This -is a real design constraint on hex-poly-fast's workers, and it is the -reason its `Triadic` carrier is never normalized mid-transform. With -`CostOblivious` proved, bounds quantified over all oracles follow from the -honest-oracle count; without it, a bound would be honest-oracle only. +The Karatsuba program and the Schönhage program with that counted Karatsuba +base must satisfy `CostOblivious` for every pair of natural weights. Their +branches may depend on array lengths, cutoffs, and schedule data. They must not +depend on coefficient values or oracle answers. Fixed-length triadic values +are necessary for this statement because trimming an intermediate value would +introduce coefficient-dependent branches. + +No theorem claims obliviousness for an arbitrary function on `ArithQuery`. +Such a function could inspect the operands stored in a query. ## Bounds -cslib's `UpperBound` counts queries. Weighted bounds need the analogue -over `cost`, defined here and a candidate for upstreaming: +cslib's `UpperBound` counts queries with unit weight. This library also needs +a weighted form: ```lean def WeightedBound {T : Type} [AddMonoid T] [LE T] @@ -174,96 +164,131 @@ def WeightedBound {T : Type} [AddMonoid T] [LE T] size x ≤ n → (prog x).cost oracle weight ≤ bound n ``` -**Karatsuba (milestone 1).** The bound covers the public dispatcher, both -operand sizes, and the cutoff, in integer form with no real exponents: -for sizes `m ≥ n` and cutoff `c`, the query count of the dispatcher -worker is at most +The implemented statements may use a pair of natural numbers to record +addition and multiplication counts before applying +`ArithQuery.weight c_add c_mul`. Either formulation must imply the weighted +inequalities below for all natural `c_add` and `c_mul`. + +### Karatsuba + +The first result covers the proof-facing dispatcher, including its balanced, +blocked, and unbalanced paths. If `m ≥ n > 0` and the cutoff is `c`, its cost +is bounded by ```text -ceil(m/n) * (A(c) * 3 ^ Nat.clog 2 n + B(c) * n) +ceil(m / n) * (A(c) * 3 ^ Nat.clog 2 n + B(c) * n) ``` -with `A` and `B` explicit polynomials in `c` fixed by the proof. The -balanced case is the `ceil(m/n) = 1` row. A bound for the textbook -balanced recursion alone does not discharge this milestone: the point of -the warm-up is to validate the worker architecture against the dispatch -structure hex-poly-fast actually has. +after multiplication and addition weights are incorporated into the explicit +functions `A` and `B`. The proof states their definitions. A theorem for only +the balanced textbook recurrence does not satisfy this contract. + +### Schönhage -**Schönhage (milestone 2).** The recurrence is stated over the schedule: -for a valid `SchoenhageSchedule N`, the count for the triadic product -worker at half-length `N` is at most `2 * 3^k` times the count at -half-length `L` plus an explicit `O(N * k)` transform term. The chooser's -balance property (`L` within a constant factor of `sqrt N` whenever a -schedule exists) then closes the recurrence to the headline bound: an -explicit constant `C` with query count at most +Write `K = 3^k`. For any valid `SchoenhageSchedule N`, the triadic worker +satisfies a recurrence of the form ```text -C * n * Nat.clog 3 n * (Nat.clog 3 (Nat.clog 3 n) + 1) +T(N) ≤ 2 * K * T(L) + A * K * L * k + B * K * L + D * N ``` -for the full-product worker at input size `n`, all stated in `Nat`. The -`log log` factor is the recursion depth; the proof tracks it as the -number of schedule steps until `schedule?` returns `none`. +where `A`, `B`, and `D` are explicit functions of `c_add` and `c_mul`. The +term `K * L * k` counts the coefficient operations in the two radix-3 +transforms and their inverse transforms. This term cannot be replaced by +`N * k` for an arbitrary value of `SchoenhageSchedule N`. -## What is not claimed +The chooser supplies the facts needed to solve the recurrence. There are +positive constants `C0`, `cK0`, `cK1`, `cL0`, and `cL1`, and a threshold +`s0`, such that every requested product length `s ≥ s0` has a padded +half-length `N` and schedule `σ` satisfying: -- Nothing about wall-clock time or memory; benchmarks in hex-poly-fast - and hex-gf2 remain the speed evidence. -- Nothing about the raw array runtimes or the packed `GF2Poly` kernel. - One packed XOR performs 64 coefficient additions at once, so a - word-level cost model is a different theorem, reserved for a possible - later hex-gf2-cslib. -- No lower bounds. cslib's decision-tree lemma requires finite query - response types; `ArithQuery R` over an infinite ring is outside it. +```text +s ≤ 2 * N ≤ C0 * s +schedule? N = some σ +N ≤ cK0 * σ.K * σ.K +σ.K * σ.K ≤ cK1 * N +N ≤ cL0 * σ.L * σ.L +σ.L * σ.L ≤ cL1 * N +``` + +Thus `K` and `L` are within constant factors of `sqrt N`, and the transform +term is bounded by a constant multiple of `N * k`. The chooser also proves +recursive completeness: whenever a generated `L` remains above the +Karatsuba cutoff, `schedule? L` returns a schedule satisfying the same +balance inequalities. These facts bound the number of schedule steps by an +explicit constant multiple of +`Nat.clog 3 (Nat.clog 3 N + 1) + 1`. + +The global theorem will fix the base case to the counted Karatsuba worker with +cutoff `c`. For inputs whose two lengths are at most `n`, it supplies an +explicit constant `C` depending on `c`, `c_add`, `c_mul`, and the chooser +constants such that the cost is at most + +```text +C * n * (Nat.clog 3 n + 1) * + (Nat.clog 3 (Nat.clog 3 n + 1) + 1) +``` + +for every `n`. The added ones cover zero, constant, and other small inputs. +The public `schoenhagePlan` may accept any lawful base plan, and its +correctness theorem applies to that general form. No operation bound follows +for a caller-supplied base plan unless it has its own parametric worker, +specialization theorem, obliviousness theorem, and weighted bound. + +## Non-claims + +- The theorems do not bound the raw array definitions selected by `@[csimp]`. +- The theorems do not bound `GF2Poly` word operations. One word XOR represents + 64 coefficient additions, and the packed base cases use carry-less + multiplication. +- The theorems do not bound time or memory. +- No lower bound is claimed. cslib's general lower-bound lemma requires finite + query response types, which excludes `ArithQuery R` for an arbitrary + infinite ring. ## External comparators -No external comparator is required. Justification: `complexity-layer`, -analogous to `correspondence-only-layer` per -[SPEC/benchmarking.md §Comparator naming](../benchmarking.md); the -computational owner carries the comparators. - -## Infrastructure amendments - -Implemented with the library, not by this SPEC-only change: - -- `lakefile.lean` gains the cslib `require` at the pinned revision. - `scripts/release/sync_released.py` reads external pins generically from - `lake-manifest.json`, so released-repo pin rewriting needs no change. -- `libraries.yml` gains a `cslib: true` field on this library. The schema - is enforced, so this touches the parser and validation in - `scripts/libgraph.py` and `scripts/check_dag.py` (`LIBRARY_FIELDS`, - `LibraryInfo`, and the field validators), not only the DAG check. -- `Cslib` joins `EXTERNAL_IMPORT_ROOTS` in `scripts/libgraph.py`, and - `check_dag.py` restricts `Cslib.*` imports to libraries marked - `cslib: true`, exactly as `Mathlib.*` imports are restricted to - `mathlib: true` libraries. A library marked `cslib: true` is implicitly - Mathlib-adjacent for every build rule (`precompileModules` ban, no - benches, proof-only runtime exemptions). -- `SPEC/design-principles.md` extends "No Mathlib in the computational - core" to cslib in one paragraph. -- CI: cslib modules build inside the existing single job. cslib has no - olean cache service, but the imported Query modules and their Mathlib - dependencies are covered by the Mathlib cache plus a small residual - build, measured before the library is activated. +No external comparator is required. The permitted reason is +`complexity-layer`: this library has no benchmark target, and `HexPolyFast` +owns the relevant performance measurements. + +## Infrastructure + +Implementation of this planned library requires the following changes: + +- `lakefile.lean` requires cslib at the selected revision. +- `libraries.yml` records `cslib: true`, `complexity_layer: true`, and the + computational owners. The schema parser and validators must accept these + fields and require zero benchmark and conformance targets for a complexity + layer. +- `scripts/libgraph.py` recognizes `Cslib` as an external import root. + `scripts/check_dag.py` permits `Cslib.*` imports only in libraries marked + `cslib: true` and applies the Mathlib-importing build restrictions to them. +- The library builds in the existing CI job. No workflow or additional job is + added. + +The release code already obtains external revisions from +`lake-manifest.json`. The release manifest is amended only after the project +chooses a release convention for cslib companions. ## Milestones -1. **Framework and Karatsuba.** The cslib pin, `freeOps`, - `CostOblivious`, `WeightedBound`, the Karatsuba specialization and - cost-obliviousness theorems, and the dispatcher-covering Karatsuba - bound. This milestone validates the worker architecture end to end on - an algorithm whose mathematics is finished, before any of it is on the - Schönhage critical path. -2. **Schönhage.** Specialization and cost obliviousness for the Schönhage - worker, the schedule recurrence, the chooser balance property, and the - headline bound. -3. **Upstreaming review.** Offer `CostOblivious` and `WeightedBound` to - cslib; adopt the upstream forms if accepted; re-pin to merged cslib. - -No milestone may weaken a bound statement to an honest-oracle-only form -as a shortcut: cost obliviousness is part of milestones 1 and 2, not a -follow-up. +1. **Query definitions and Karatsuba.** Add the cslib dependency and + complexity-layer metadata. Define `freeOps`, `CostOblivious`, and + `WeightedBound`. Refactor the proof-facing Karatsuba definition through + `karatsubaWorker`, then prove specialization, obliviousness, and the + dispatcher bound. +2. **Schönhage.** Prove specialization and obliviousness for + `schoenhageWorker`. Prove the per-schedule recurrence, bounded padding, + chooser balance, recursive completeness, and the global bound with the + counted Karatsuba base. +3. **cslib update.** Propose `CostOblivious` and `WeightedBound` upstream if + they are useful outside Hex. Replace local definitions with accepted cslib + definitions when their statements agree, then update to a merged revision. + +The obliviousness and chooser theorems are part of the corresponding bound +milestone. An honest-oracle-only inequality does not complete either +milestone. ## File organisation @@ -271,30 +296,27 @@ follow-up. HexPolyFastCslib/ Query.lean -- freeOps, CostOblivious, WeightedBound Karatsuba.lean -- specialization, obliviousness, dispatcher bound - Schoenhage.lean -- specialization, obliviousness, recurrence, bound + Schoenhage.lean -- specialization, recurrence, chooser facts, global bound HexPolyFastCslib.lean ``` -`libraries.yml` eventually gains, after cslib is pinned and the -hex-poly-fast workers exist: +The eventual library entry has this shape: ```yaml HexPolyFastCslib: deps: [HexPolyFast] mathlib: true cslib: true + complexity_layer: true + computational_owners: [HexPolyFast] done_through: 0 status: planned ``` -The release manifest is updated only when a release shape for `-cslib` -companions is decided, never by this SPEC-only change. - ## References - cslib PR [#401, query complexity framework](https://github.com/leanprover/cslib/pull/401): - `FreeM` programs, oracles, `cost`, `countQueries`, `UpperBound`, and the - `ArithQuery` example this library builds on. + `FreeM`, `eval`, `cost`, `countQueries`, `UpperBound`, and `ArithQuery`. - Arnold Schönhage, *Schnelle Multiplikation von Polynomen über Körpern der Charakteristik 2*, Acta Informatica 7 (1977), 395-398. - Richard P. Brent, Pierrick Gaudry, Emmanuel Thomé, and Paul Zimmermann, diff --git a/SPEC/benchmarking.md b/SPEC/benchmarking.md index 74b449717..a88b3266a 100644 --- a/SPEC/benchmarking.md +++ b/SPEC/benchmarking.md @@ -750,6 +750,12 @@ with a library-specific reason identifying exactly one of: the evidence for the operations it transports; more than one owner is normal, since a layer may transport operations from several Mathlib-free libraries. +- **complexity-layer**: the library is explicitly classified by + `complexity_layer: true` in `libraries.yml`. It contains only definitions + and proofs used to establish operation bounds, so it has zero bench targets + and requires no headline performance report. The declaration names every + computational performance owner whose bench targets measure the analysed + operations. Generic "not applicable" is not a valid declaration. Unwired-but- required comparators are declared with the `blocked` state per diff --git a/SPEC/design-principles.md b/SPEC/design-principles.md index ed4db0a2b..7d48a5add 100644 --- a/SPEC/design-principles.md +++ b/SPEC/design-principles.md @@ -34,12 +34,12 @@ bridge, transported along the equivalence so the operations stay the executable ones. - The same boundary applies to cslib, which itself depends on Mathlib. - Computational libraries are cslib-free; proved operation-count bounds - live in `-cslib` companion libraries (the first is - [hex-poly-fast-cslib](Libraries/hex-poly-fast-cslib.md)), which are - proof-only and follow every build rule that applies to `-mathlib` - libraries. + cslib also depends on Mathlib. A computational library therefore does not + import cslib. A planned `-cslib` proof library may import a computational + library and prove operation-count theorems for definitions in it. Such a + library has no executable API, conformance target, or benchmark target. + [hex-poly-fast-cslib](Libraries/hex-poly-fast-cslib.md) specifies the first + instance of this pattern. 3. **Performant by default.** Dense array-backed representations, `UInt64` coefficients for `F_p`, Barrett/Montgomery reduction for modular diff --git a/SPEC/future-work.md b/SPEC/future-work.md index b5448321e..ddd006941 100644 --- a/SPEC/future-work.md +++ b/SPEC/future-work.md @@ -230,31 +230,30 @@ show which operations a common interface must support. ### Fast multiplication in characteristic two, follow-ups -Schönhage's radix-3 multiplication and its proved coefficient-operation -bound are specified: the generic algorithm and triadic reference semantics -as amendments to [hex-poly-fast](../HexPolyFast/SPEC/hex-poly-fast.md), -the packed `F_2[x]` kernel and dispatch ladder as amendments to -[hex-gf2](../HexGF2/SPEC/hex-gf2.md), and the operation counts in -[hex-poly-fast-cslib](Libraries/hex-poly-fast-cslib.md), the first `-cslib` -companion. What remains future work: - -- Additive FFTs (Cantor's algorithm, Gao-Mateer) as an alternative - large-degree family for `F_2[x]` and `F_(2^k)[x]`, and the - wrapped-product splitting reconstruction of - Brent-Gaudry-Thomé-Zimmermann §3.3 that smooths the schedule staircase. -- Instantiating the generic radix-3 plan for `F_(2^k)[x]` in the hex-gfq - family, where the word-prime NTT path is equally unavailable. -- Integer Schönhage-Strassen multiplication. Hex integer arithmetic - currently delegates large products to GMP through Lean core, so this is - a verification project, not a performance one, and it needs its own - motivation before a SPEC. -- A hex-gf2-cslib companion counting word operations of the packed kernel. - The existing bound counts coefficient operations of the generic - algorithm; one packed XOR performs 64 coefficient additions, so the - word-level statement is a separate theorem with its own cost model. -- Extending the `-cslib` pattern to other libraries once a second - worthwhile bound is identified. Turing-machine-model complexity is out - of scope for the foreseeable future. +The generic radix-3 algorithm and its triadic semantics are specified in +[hex-poly-fast](../HexPolyFast/SPEC/hex-poly-fast.md). The packed +characteristic-two implementation is specified in +[hex-gf2](../HexGF2/SPEC/hex-gf2.md). Its generic coefficient-operation bound +is specified in +[hex-poly-fast-cslib](Libraries/hex-poly-fast-cslib.md). Those SPECs leave the +following separate projects: + +- Specify and compare additive FFT multiplication, including Cantor and + Gao-Mateer variants, for `F_2[x]` and `F_(2^k)[x]`. +- Specify the wrapped-product splitting reconstruction from §3.3 of Brent, + Gaudry, Thomé, and Zimmermann. It may reduce the performance discontinuities + caused by padding to an admissible schedule. +- Instantiate the generic radix-3 plan for `F_(2^k)[x]` in the hex-gfq + libraries. The existing word-prime radix-2 NTT does not apply directly to + those coefficient fields. +- Give integer Schönhage-Strassen multiplication its own motivation and SPEC. + Current large integer products use GMP through Lean's runtime. +- Specify a possible hex-gf2-cslib library for packed word-operation bounds. + The generic coefficient count cannot express that one word XOR processes + 64 coefficients or that a base product uses CLMUL. +- Apply the `-cslib` pattern to another library only after identifying a + concrete theorem that justifies the dependency. Turing-machine complexity + is not planned. ### Positive-characteristic multivariate squarefree decomposition diff --git a/SPEC/testing.md b/SPEC/testing.md index cbd82248d..de30a36b2 100644 --- a/SPEC/testing.md +++ b/SPEC/testing.md @@ -143,9 +143,11 @@ Each library has up to three conformance-tree modules: - `conformance/HexFoo/Conformance.lean` (module `HexFoo.Conformance`) — the `core` profile, specified above. Every Mathlib-free library at `done_through ≥ 2` has one. A Mathlib-importing library has one when it owns - an executable runtime contract; a layer explicitly classified by - `correspondence_only: true` must not (see §Banned anti-patterns and - [PLAN/Phase3.md §Correspondence-only mathlib layers](../PLAN/Phase3.md)). + an executable runtime contract. A layer with `correspondence_only: true` + must not have one (see + [PLAN/Phase3.md §Correspondence-only mathlib layers](../PLAN/Phase3.md)). A + layer with `complexity_layer: true` also must not have one (see §Banned + anti-patterns). - `conformance/HexFoo/CrossCheck.lean` (module `HexFoo.CrossCheck`) — the heavier cross-check sweeps: representation-correspondence campaigns, fast-vs-fast agreement over deterministic input streams, @@ -336,6 +338,12 @@ MUST NOT appear in any `Conformance.lean`: correspondence-only bridge and may have a dedicated conformance target when its library SPEC defines that runtime contract and CI reachability. +- **Conformance files in complexity layers.** A library with + `complexity_layer: true` contains operation-count definitions and proofs but + owns no executable operation. It has no conformance source, fixture stream, + or oracle. Its metadata names the computational conformance owners whose + tests cover the analysed operations. + ## `#eval` vs `#eval!` `#eval e` errors when `e` transitively depends on any `sorry`, @@ -443,6 +451,11 @@ executable reifier, certificate checker, or tactic, does have a `core` profile, exercising that runtime against the contract its library SPEC states rather than restating bridge theorems. +A library with `complexity_layer: true` likewise has no conformance profile +or external oracle. Its proofs concern workers owned by the computational +libraries named in its metadata, and those owners retain the conformance +fixtures. + ## Profile sizes Size policies per profile. Generators must be parameterised by size