diff --git a/HexGF2/SPEC/hex-gf2.md b/HexGF2/SPEC/hex-gf2.md index f437ae4e6..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-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,11 +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: 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 - 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) @@ -107,6 +107,133 @@ compilations rather than one: individually; `HEX_CLMUL_NO_LEAN` drops the export wrapper so the self-test needs no Lean runtime. +## Multiplication ladder + +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. `mulWords` below the first crossover; +2. Karatsuba split at word boundaries between the two crossovers; +3. packed Schönhage multiplication above the second crossover. + +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 correctness proof converts packed polynomials to dense polynomials over +`ZMod64 2`. The new Mathlib-free API is: + +```lean +def GF2Poly.toDense : GF2Poly → DensePoly (ZMod64 2) +def GF2Poly.ofDense : DensePoly (ZMod64 2) → GF2Poly +``` + +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 planned packed kernel follows the generic algorithm in +[hex-poly-fast §Schönhage's radix-3 algorithm](../../HexPolyFast/SPEC/hex-poly-fast.md) +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. +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) 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 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 provides the optimized representations and operations; the convenience @@ -233,11 +360,13 @@ 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 +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 3fcf88972..37ab8b119 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; +- 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; @@ -104,8 +106,15 @@ 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; +- 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; - a limb-level arbitrary-precision integer middle product; - multivariate multiplication, sparse interpolation, or polynomial-matrix approximant bases; @@ -241,6 +250,173 @@ 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 + +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 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`. 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) +``` + +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.** 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 + M : Nat + L : Nat + k_pos : 0 < k + blocks : N = 3 ^ k * M + block_fits : M ≤ L + aligned : 3 ^ k ∣ L + decreasing : L < N +``` + +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.** + +```lean +def schoenhagePlan (base : MulPlan R) (cutoff : Nat) + (inv3 : R) (inv3_spec : 3 * inv3 = 1) : MulPlan R +``` + +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 proof-facing Karatsuba and Schönhage definitions use workers that are +parametric in 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 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 For a polynomial `f` and precision `n`, reversal reads the coefficient below @@ -658,6 +834,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 | +| 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)` | @@ -671,6 +851,14 @@ 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 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 The logical closure consists of schoolbook polynomial operations, the @@ -695,7 +883,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 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; @@ -714,6 +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`, 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 @@ -739,6 +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; +- 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; @@ -837,10 +1033,14 @@ 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. +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 @@ -865,11 +1065,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 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, 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 recurses through balanced +schedules until the Karatsuba cutoff. ## File organisation @@ -879,6 +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 -- positive-length triadic fold + TriadicRemainder.lean -- canonical remainder theorem + Schoenhage/ + 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 @@ -947,3 +1165,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. 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. 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 285854df6..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, 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), `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,6 +100,15 @@ 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** (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 proof-facing + Karatsuba and Schönhage workers, including specialization and + cost-obliviousness theorems. The bounds exclude raw `@[csimp]` runtimes. + ## Implementation dependencies Each library with its immediate dependencies: @@ -153,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-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 @@ -203,6 +212,11 @@ Mathlib companion libraries (each also depends on Mathlib): - **hex-summation-mathlib**: hex-summation - **hex-graph-iso-mathlib**: hex-graph-iso +cslib companion libraries (planned, each also depends on cslib and therefore +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 +517,34 @@ 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). +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 ───────────┐ +hex-poly-fast ──────┤ +hex-mod-arith ──────┼── hex-gf2 +hex-finite-field ───┤ +hex-basic ──────────┘ +``` + +`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 +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 +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, 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, 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`, `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 new file mode 100644 index 000000000..570e49363 --- /dev/null +++ b/SPEC/Libraries/hex-poly-fast-cslib.md @@ -0,0 +1,324 @@ +# 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 + +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 + +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, 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 (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 +``` + +`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 free interpretation of `CoeffOps` is: + +```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) +``` + +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 + +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) : + (karatsubaWorker freeOps cutoff fuel a b).eval ArithQuery.honest = + karatsubaWorker idOps cutoff fuel a b +``` + +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 + +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 (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) +``` + +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 with unit weight. This library also needs +a weighted form: + +```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 +``` + +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) +``` + +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 + +Write `K = 3^k`. For any valid `SchoenhageSchedule N`, the triadic worker +satisfies a recurrence of the form + +```text +T(N) ≤ 2 * K * T(L) + A * K * L * k + B * K * L + D * N +``` + +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`. + +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: + +```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. 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. **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 + +```text +HexPolyFastCslib/ + Query.lean -- freeOps, CostOblivious, WeightedBound + Karatsuba.lean -- specialization, obliviousness, dispatcher bound + Schoenhage.lean -- specialization, recurrence, chooser facts, global bound +HexPolyFastCslib.lean +``` + +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 +``` + +## References + +- cslib PR [#401, query complexity framework](https://github.com/leanprover/cslib/pull/401): + `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, + [*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/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 34882b14b..7d48a5add 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. + 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 arithmetic. New GMP `@[extern]` primitives where Lean's runtime diff --git a/SPEC/future-work.md b/SPEC/future-work.md index 62ab364fb..ddd006941 100644 --- a/SPEC/future-work.md +++ b/SPEC/future-work.md @@ -228,6 +228,33 @@ 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 + +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 Amend `hex-mv-gcd` with squarefree decomposition over perfect fields of 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