feat(fields): fast binary tower fields (up to 128 bits) by graikos · Pull Request #286 · Verified-zkEVM/CompPoly

graikos · 2026-08-06T08:11:19Z

Fast arithmetic for the binary tower GF(2^(2^k)), k <= 7, in pure Lean, no externs, no native_decide.

one UInt64 per element up to GF(2^64), two limbs for GF(2^128); unrolled Karatsuba ladder
ladder stops at GF(2^8), then uses byte tables, generated from the proven ladder via Array.ofFn, so correctness is structural and the kernel never evaluates a table
proven against ConcreteBTField
runtime defs are zero-import for precompileModules
#guard tests + fields-tower-bt128-{mul,inv} bench groups in CI
GF(2^128): mul ~47ns, inv ~93ns (vs ConcreteBTField: ~3ms / ~5ms)

Earlier drafts had a C extern tier, but pure Lean matched it on mul and beats it on inv so it was dropped.

…tem) Module headers on Fast.lean and its tests, de-private helpers the module system requires in exposed bodies, regenerated import lists. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

github-actions · 2026-08-06T08:13:23Z

🤖 PR Summary

Mathematical Formalization

Core definitions: FastBT k (one UInt64 for k ≤ 6) and FastBT128 (two UInt64 limbs) encode tower elements as packed machine words, with proofs that the toNat is within the field bound.
Recursive twin operations: mulByZRec, mulRec, sqRec, invRec mirror the unrolled runtime ladder; range-bound lemmas (mulByZRec_lt, …) and correctness theorems (mulByZRec_correct, …) are proven by induction for k ≤ 6.
Bridge theorems: mul8_eq_rec, mul16_eq_rec, …, sq2_eq_rec, …, inv2_eq_rec, … connect each width‑specific runtime operation to its recursive twin; table‑lookup bridges (mul8T_eq_mul8, …) relate byte‑table versions to the recursive ladder.
Field structure: For k = 3..6, FastBT k obtains AddCommGroup, Mul, Inv, and Field instances via an injective transport toConcrete and fieldOfHoms; ring isomorphisms ringEquivBT8, ringEquivBT16, ringEquivBT32, ringEquivBT64 are provided. For FastBT128, AddCommGroup, Mul, Inv and a toConcrete correctness proof are given.
Auxiliary lemmas: Word‑level bounds (and_mask_lt, xor_lt, shiftRight_lt, join_lt, half_lt, rec_step_bounds) and per‑width correctness for multiplication‑by‑generator and squaring (toConcrete_mulByZ, toConcrete_square).
No sorry or admit appear in any of the new formalization files.

Infrastructure & CI

CI benchmark addition: .github/workflows/lean_action_ci.yml adds fields-tower-bt128-mul and fields-tower-bt128-inv to the KECCAK_BENCHES environment variable, making these two benchmarks part of the automatic CI run.
New benchmark file (bench/CompPolyBench/Fields/Binary/Tower.lean): defines checksumFastBT128 and checksumConcreteBt128, a towerSampler that reuses a random 64‑element pool, and runTowerGroup that times multiplication and inversion for both ConcreteBTField 7 and Fast.FastBT128. It returns a BenchGroup with separate records; runners runTowerMul and runTowerInv set operation‑specific iteration budgets. The task list towerTasks is registered via bench/CompPolyBench/Setup.lean.
Bench display refinement (bench/CompPolyBench/Common.lean): formatNanosInUnitOrAuto is added to render very small times with a per‑value unit; groupResultColumns uses it for “Total” and “Avg” columns to avoid sub‑threshold display.

Refactoring / API exposure

Public imports: CompPoly.lean now publicly imports CompPoly.Fields.Binary.Tower.Fast and CompPoly.Fields.Binary.Tower.FastDefs; tests/CompPolyTests.lean publicly imports the new test module. These changes expose the fast tower definitions and tests in the public API.
Zero‑import runtime module (CompPoly/Fields/Binary/Tower/FastDefs.lean): contains the unrolled ladder primitives (mul2–mul64, sq2–sq64, inv2–inv64), table‑based variants, and the FastBT128 structure with limb‑level arithmetic — all with no imports, enabling inclusion in precompileModules without pulling mathlib.

Testing

New test file (tests/CompPolyTests/Fields/Binary/Tower/Fast.lean): uses #guard statements to cross‑validate addition, multiplication, squaring, inversion, powers, and field operations for BT8, BT16, BT32, BT64, and FastBT128 against concrete tower values and table‑based rung functions. Ring equivalence round‑trips via ringEquivBT* and FastBT128.ringEquiv are also checked. No sorry or admit appear.

Performance summary (from PR body)

GF(2^128): multiplication ~47 ns, inversion ~93 ns (vs ConcreteBTField ~3 ms / ~5 ms). The implementation is pure Lean with no external calls or native_decide.

Statistics

Metric	Count
📝 Files Changed	12
✅ Lines Added	2056
❌ Lines Removed	5

Lean Declarations

✏️ Added: 235 declaration(s)

CompPoly/Fields/Binary/Tower/Fast.lean (172)

@[inline] def BT16.mul (a b : BT16) : BT16
@[inline] def BT32.mul (a b : BT32) : BT32
@[inline] def BT64.mul (a b : BT64) : BT64
@[inline] def BT8.mul (a b : BT8) : BT8
@[inline] def FastBT.mulByZ {k : ℕ} (a : FastBT k) (_hk : k ≤ 6
@[inline] def FastBT.square {k : ℕ} (a : FastBT k) (_hk : k ≤ 6
@[inline] def add (a b : FastBT k) : FastBT k
@[inline] def ofNat (k n : ℕ) : FastBT k
@[reducible] def fieldOfHoms {k : ℕ} [Mul (FastBT k)] [Inv (FastBT k)]
@[reducible] def ringEquivOfHom {k : ℕ} [Mul (FastBT k)] (hk : k ≤ 6)
@[simp] theorem neg_def (a : FastBT128) : -a = a
@[simp] theorem ofConcrete_toConcrete (a : FastBT128) : ofConcrete (toConcrete a) = a
@[simp] theorem sub_def (a b : FastBT128) : a - b = a + b
@[simp] theorem toConcrete_add (a b : FastBT128) :
@[simp] theorem toConcrete_inv (v : FastBT128) : toConcrete v⁻¹ = (toConcrete v)⁻¹
@[simp] theorem toConcrete_inv_bt16 (a : BT16) : toConcrete a⁻¹ = (toConcrete a)⁻¹
@[simp] theorem toConcrete_inv_bt32 (a : BT32) : toConcrete a⁻¹ = (toConcrete a)⁻¹
@[simp] theorem toConcrete_inv_bt64 (a : BT64) : toConcrete a⁻¹ = (toConcrete a)⁻¹
@[simp] theorem toConcrete_inv_bt8 (a : BT8) : toConcrete a⁻¹ = (toConcrete a)⁻¹
@[simp] theorem toConcrete_mul (a b : FastBT128) :
@[simp] theorem toConcrete_mul_bt16 (a b : BT16) :
@[simp] theorem toConcrete_mul_bt32 (a b : BT32) :
@[simp] theorem toConcrete_mul_bt64 (a b : BT64) :
@[simp] theorem toConcrete_mul_bt8 (a b : BT8) :
@[simp] theorem toConcrete_neg (a : FastBT128) : toConcrete (-a) = -(toConcrete a)
@[simp] theorem toConcrete_ofConcrete (x : ConcreteBTField 7) :
@[simp] theorem toConcrete_one : toConcrete (1 : FastBT128) = 1
@[simp] theorem toConcrete_sub (a b : FastBT128) :
@[simp] theorem toConcrete_toNat (x : FastBT k) :
@[simp] theorem toConcrete_zero : toConcrete (0 : FastBT128) = 0
@[simp] theorem val_add (a b : FastBT k) : (a + b).val = a.val ^^^ b.val
@[simp] theorem val_inv_bt16 (a : BT16) : (a⁻¹).val = inv16 a.val
@[simp] theorem val_inv_bt32 (a : BT32) : (a⁻¹).val = inv32 a.val
@[simp] theorem val_inv_bt64 (a : BT64) : (a⁻¹).val = inv64 a.val
@[simp] theorem val_inv_bt8 (a : BT8) : (a⁻¹).val = inv8 a.val
@[simp] theorem val_mul_bt16 (a b : BT16) : (a * b).val = mul16 a.val b.val
@[simp] theorem val_mul_bt32 (a b : BT32) : (a * b).val = mul32 a.val b.val
@[simp] theorem val_mul_bt64 (a b : BT64) : (a * b).val = mul64 a.val b.val
@[simp] theorem val_mul_bt8 (a b : BT8) : (a * b).val = mul8 a.val b.val
@[simp] theorem val_one : (1 : FastBT k).val = 1
@[simp] theorem val_zero : (0 : FastBT k).val = 0
abbrev BT16
abbrev BT32
abbrev BT64
abbrev BT8
def FastBT.toNat {k : ℕ} (x : FastBT k) : ℕ
def invRec : ℕ → UInt64 → UInt64
def mulByZRec : ℕ → UInt64 → UInt64
def mulRec : ℕ → UInt64 → UInt64 → UInt64
def ofConcrete (x : ConcreteBTField 7) : FastBT128
def one : FastBT k
def ringEquiv : FastBT128 ≃+* ConcreteBTField 7 where
def ringEquivBT16 : BT16 ≃+* ConcreteBTField 4
def ringEquivBT32 : BT32 ≃+* ConcreteBTField 5
def ringEquivBT64 : BT64 ≃+* ConcreteBTField 6
def ringEquivBT8 : BT8 ≃+* ConcreteBTField 3
def sqRec : ℕ → UInt64 → UInt64
def toConcrete (v : FastBT128) : ConcreteBTField 7
def zero : FastBT k
theorem FastBT.mulByZ_val : ∀ {k : ℕ} (a : FastBT k) (hk : k ≤ 6),
theorem FastBT.square_val : ∀ {k : ℕ} (a : FastBT k) (hk : k ≤ 6),
theorem and_mask_lt (s : ℕ) {a m : UInt64} (hm : m.toNat = 2 ^ s - 1) :
theorem and_mask_toNat {k : ℕ} (hk : k ≤ 5) (a : UInt64) :
theorem byteTable_get_eq {f : UInt64 → UInt64}
theorem concrete_inv_step {k : ℕ} (a : ConcreteBTField (k + 1))
theorem concrete_mul_eq_mul {k : ℕ} (x y : ConcreteBTField k) :
theorem concrete_mul_step {k : ℕ} (a b : ConcreteBTField (k + 1))
theorem eq_zero_or_one {v : UInt64} (hv : v.toNat < 2 ^ 2 ^ 0) : v = 0 ∨ v = 1
theorem fromNat_inv64 (v : UInt64) :
theorem fromNat_join {k : ℕ} (hk : k + 1 ≤ 6) {hi lo : UInt64}
theorem fromNat_mul64 (a b : UInt64) :
theorem fromNat_mulByZ6 (v : UInt64) :
theorem fromNat_one {k : ℕ} :
theorem fromNat_sq64 (v : UInt64) :
theorem fromNat_toNat {k : ℕ} (x : ConcreteBTField k) : fromNat x.toNat = x
theorem fromNat_xor {k : ℕ} (x y : UInt64) :
theorem fromNat_zero {k : ℕ} :
theorem half16_lt {v : UInt64} (hv : v.toNat < 2 ^ 16) :
theorem half32_lt {v : UInt64} (hv : v.toNat < 2 ^ 32) :
theorem half64_lt (v : UInt64) :
theorem half_lit_lt (s : ℕ) (m sh : UInt64) {v : UInt64} (hm : m.toNat = 2 ^ s - 1)
theorem half_lt {k : ℕ} (hk : k + 1 ≤ 6) {v : UInt64}
theorem inv16T_eq_inv16 {v : UInt64} (hv : v.toNat < 2 ^ 16) :
theorem inv16_eq_rec (v : UInt64) : inv16 v = invRec 4 v
theorem inv16_lt {v : UInt64} (hv : v.toNat < 2 ^ 16) : (inv16 v).toNat < 2 ^ 16
theorem inv2_eq_rec (v : UInt64) : inv2 v = invRec 1 v
theorem inv32T_eq_inv32 {v : UInt64} (hv : v.toNat < 2 ^ 32) :
theorem inv32_eq_rec (v : UInt64) : inv32 v = invRec 5 v
theorem inv32_lt {v : UInt64} (hv : v.toNat < 2 ^ 32) : (inv32 v).toNat < 2 ^ 32
theorem inv4_eq_rec (v : UInt64) : inv4 v = invRec 2 v
theorem inv64T_eq_inv64 (v : UInt64) :
theorem inv64_eq_rec (v : UInt64) : inv64 v = invRec 6 v
theorem inv8T_eq_inv8 {v : UInt64} (hv : v.toNat < 2 ^ 8) : inv8T v = inv8 v
theorem inv8_eq_rec (v : UInt64) : inv8 v = invRec 3 v
theorem inv8_lt {v : UInt64} (hv : v.toNat < 2 ^ 8) : (inv8 v).toNat < 2 ^ 8
theorem invRec_correct : ∀ (k : ℕ), k ≤ 6 → ∀ (v : UInt64), v.toNat < 2 ^ 2 ^ k →
theorem invRec_lt : ∀ (k : ℕ), k ≤ 6 → ∀ (v : UInt64),
theorem invRec_succ (k : ℕ) (v : UInt64) :
theorem join_add_join {k : ℕ} (a b c d : ConcreteBTField k) :
theorem join_lt (s : ℕ) {hi lo sh : UInt64} (hsh : sh.toNat = s) (hs : 2 * s ≤ 64)
theorem join_word_toNat {k : ℕ} (hk : k + 1 ≤ 6) {hi : UInt64}
theorem mul16T_eq_mul16 {a b : UInt64} (ha : a.toNat < 2 ^ 16) (hb : b.toNat < 2 ^ 16) :
theorem mul16_eq_rec (a b : UInt64) : mul16 a b = mulRec 4 a b
theorem mul16_lt {a b : UInt64} (ha : a.toNat < 2 ^ 16) (hb : b.toNat < 2 ^ 16) :
theorem mul2_eq_rec (a b : UInt64) : mul2 a b = mulRec 1 a b
theorem mul32T_eq_mul32 {a b : UInt64} (ha : a.toNat < 2 ^ 32) (hb : b.toNat < 2 ^ 32) :
theorem mul32_eq_rec (a b : UInt64) : mul32 a b = mulRec 5 a b
theorem mul32_lt {a b : UInt64} (ha : a.toNat < 2 ^ 32) (hb : b.toNat < 2 ^ 32) :
theorem mul4_eq_rec (a b : UInt64) : mul4 a b = mulRec 2 a b
theorem mul64T_eq_mul64 (a b : UInt64) :
theorem mul64_eq_rec (a b : UInt64) : mul64 a b = mulRec 6 a b
theorem mul8T_eq_mul8 {a b : UInt64} (ha : a.toNat < 2 ^ 8) (hb : b.toNat < 2 ^ 8) :
theorem mul8_eq_rec (a b : UInt64) : mul8 a b = mulRec 3 a b
theorem mul8_lt {a b : UInt64} (ha : a.toNat < 2 ^ 8) (hb : b.toNat < 2 ^ 8) :
theorem mulByZ1_eq_rec (v : UInt64) : mulByZ1 v = mulByZRec 1 v
theorem mulByZ2_eq_rec (v : UInt64) : mulByZ2 v = mulByZRec 2 v
theorem mulByZ3T_eq_mulByZ3 {v : UInt64} (hv : v.toNat < 2 ^ 8) :
theorem mulByZ3_eq_rec (v : UInt64) : mulByZ3 v = mulByZRec 3 v
theorem mulByZ3_lt {v : UInt64} (hv : v.toNat < 2 ^ 8) : (mulByZ3 v).toNat < 2 ^ 8
theorem mulByZ4T_eq_mulByZ4 {v : UInt64} (hv : v.toNat < 2 ^ 16) :
theorem mulByZ4_eq_rec (v : UInt64) : mulByZ4 v = mulByZRec 4 v
theorem mulByZ4_lt {v : UInt64} (hv : v.toNat < 2 ^ 16) : (mulByZ4 v).toNat < 2 ^ 16
theorem mulByZ5T_eq_mulByZ5 {v : UInt64} (hv : v.toNat < 2 ^ 32) :
theorem mulByZ5_eq_rec (v : UInt64) : mulByZ5 v = mulByZRec 5 v
theorem mulByZ5_lt {v : UInt64} (hv : v.toNat < 2 ^ 32) : (mulByZ5 v).toNat < 2 ^ 32
theorem mulByZ6T_eq_mulByZ6 (v : UInt64) :
theorem mulByZ6_eq_rec (v : UInt64) : mulByZ6 v = mulByZRec 6 v
theorem mulByZRec_correct : ∀ (k : ℕ), k ≤ 6 → ∀ (v : UInt64), v.toNat < 2 ^ 2 ^ k →
theorem mulByZRec_lt : ∀ (k : ℕ), k ≤ 6 → ∀ (v : UInt64),
theorem mulByZRec_succ (k : ℕ) (v : UInt64) :
theorem mulRec_correct : ∀ (k : ℕ), k ≤ 6 → ∀ (a b : UInt64),
theorem mulRec_lt : ∀ (k : ℕ), k ≤ 6 → ∀ (a b : UInt64),
theorem mulRec_succ (k : ℕ) (a b : UInt64) :
theorem nat_join_and {H L s : ℕ} (hL : L < 2 ^ s) :
theorem nat_join_shiftRight {H L s : ℕ} (hL : L < 2 ^ s) :
theorem ofConcrete_val_toNat {k : ℕ} (hk : k ≤ 6) (x : ConcreteBTField k) :
theorem rec_step_bounds {k : ℕ} (hk : k + 1 ≤ 6) :
theorem shiftRight_lt (s : ℕ) {a sh : UInt64} {t : ℕ} (hsh : sh.toNat = s)
theorem shiftRight_toNat {k : ℕ} (hk : k ≤ 5) (a : UInt64) :
theorem split_fromNat {k : ℕ} (hk : k + 1 ≤ 6) {a : UInt64}
theorem split_one' {k : ℕ} : split (Nat.succ_pos k) (1 : ConcreteBTField (k + 1))
theorem split_zero' {k : ℕ} : split (Nat.succ_pos k) (0 : ConcreteBTField (k + 1))
theorem sq16T_eq_sq16 {v : UInt64} (hv : v.toNat < 2 ^ 16) :
theorem sq16_eq_rec (v : UInt64) : sq16 v = sqRec 4 v
theorem sq16_lt {v : UInt64} (hv : v.toNat < 2 ^ 16) : (sq16 v).toNat < 2 ^ 16
theorem sq2_eq_rec (v : UInt64) : sq2 v = sqRec 1 v
theorem sq32T_eq_sq32 {v : UInt64} (hv : v.toNat < 2 ^ 32) :
theorem sq32_eq_rec (v : UInt64) : sq32 v = sqRec 5 v
theorem sq32_lt {v : UInt64} (hv : v.toNat < 2 ^ 32) : (sq32 v).toNat < 2 ^ 32
theorem sq4_eq_rec (v : UInt64) : sq4 v = sqRec 2 v

…and 85 more not listed.

sorry Tracking

No sorrys were added, removed, or affected.

Coverage Notes

AI file summarization partially analyzed 1 file(s) because their individual diffs exceeded the per-file size budget. Statistics and Lean signal tracking still cover the full PR.

Partially Analyzed Files

CompPoly/Fields/Binary/Tower/Fast.lean (+1422/-0)

📋 **Additional Analysis**

The pull request introduces new arithmetic definitions and correctness proofs for packed-word binary tower fields (Fast.lean, FastDefs.lean), along with benchmarks, tests, and documentation updates. Several style guideline violations were identified, primarily missing docstrings, inconsistent spacing around infix operators, and possible misuse of terminal simp only.

📄 **Per-File Summaries**

.github/workflows/lean_action_ci.yml: The .github/workflows/lean_action_ci.yml file was modified to add two new benchmarks (fields-tower-bt128-mul and fields-tower-bt128-inv) to the comma-separated KECCAK_BENCHES environment variable. These are now part of the benchmarks executed during CI, meaning that this change expands the set of performance tests run automatically.
CompPoly.lean: Added public import statements for CompPoly.Fields.Binary.Tower.Fast and CompPoly.Fields.Binary.Tower.FastDefs, making the definitions and theorems from these modules part of the public API of CompPoly.
CompPoly/Fields/Binary/Tower/Fast.lean: This new file (CompPoly/Fields/Binary/Tower/Fast.lean) implements a fast, packed machine‑word arithmetic library for the binary tower fields from ConcreteBTField. It defines recursive twin functions (mulByZRec, mulRec, sqRec, invRec) that mirror the unrolled runtime ladder, then proves range‑bound lemmas (mulByZRec_lt, …) and correctness theorems (mulByZRec_correct, …) by induction for levels k ≤ 6. Bridge theorems (mul8_eq_rec, mul16_eq_rec, …, sq2_eq_rec, …, inv2_eq_rec, …) connect each per‑width runtime operation to its recursive twin, and table‑lookup bridges (mul8T_eq_mul8, mul16T_eq_mul16, …, mulByZ3T_eq_mulByZ3, …) relate the byte‑table versions to the recursive ladder. A structure FastBT k holds a UInt64 value with a proof that its toNat is below 2 ^ 2 ^ k. For levels 3–6 it provides AddCommGroup, Mul, Inv, and Field instances (via an injective transport toConcrete and the helper fieldOfHoms), plus ring isomorphisms ringEquivBT8, ringEquivBT16, ringEquivBT32, ringEquivBT64. For level‑7 (GF(2^128)) it defines FastBT128 (two UInt64 limbs) with AddCommGroup, Mul, Inv and a toConcrete correctness proof. Auxiliary lemmas include and_mask_lt, xor_lt, shiftRight_lt, join_lt, half_lt, and rec_step_bounds as well as toConcrete_mulByZ, toConcrete_square for the per‑width multiplication‑by‑generator and squaring helpers. No sorry or admit are present.
CompPoly/Fields/Binary/Tower/FastDefs.lean: This file adds the runtime arithmetic primitives for the packed binary tower representation of GF(2^128) (FastBT128), extracted from the main correctness module to enable zero-import native compilation. It defines recursive ladder-based operations (mul2, sq2, inv2 through mul64, sq64, inv64) using UInt64 word tricks, along with table-based variants at level 3 (mul8Table, sq8Table, inv8Table, and the *T derived operations for higher levels). On top of these, it provides the FastBT128 structure with limb-level addition, multiplication (mul via Karatsuba with mulByZ6T), squaring (square), inversion (inv), and natural-number conversions (ofNat, toNat). The module carries no imports, so downstream consumers can include it in precompileModules without pulling mathlib.
bench/CompPolyBench/Common.lean: Added formatNanosInUnitOrAuto (lines 258–263), which renders a nanosecond value in a given unit but falls back to an auto‑chosen unit (formatNanosAuto) if the shared‑unit display would be <0.01. In groupResultColumns (lines 835–838), the two column formatters for “Total” and “Avg” now call formatNanosInUnitOrAuto instead of formatNanosInUnit, so that very small times are shown with a per‑value unit rather than collapsing to a below‑threshold string.
bench/CompPolyBench/Fields/Binary/Tower.lean: This new file bench/CompPolyBench/Fields/Binary/Tower.lean adds benchmark infrastructure for GF(2¹²⁸) operations (multiplication and inversion) comparing a ConcreteBTField 7 semantic representation against a Fast.FastBT128 packed-word implementation. It defines two checksum functions (checksumFastBT128 and checksumConcreteBt128) that reduce tower elements to a Nat via a limb xor, a generic pairwise towerSampler that reuses a random 64-element pool, and the central runTowerGroup which times both implementations under configurable iteration budgets, runs consistent checksums, and returns a BenchGroup with both records. Separate runners runTowerMul and runTowerInv set operation-specific budgets (multiplication defaults to 1000/150/30 for concrete and 2 000 000/300 000/600 00 for fast; inversion uses 500/75/15 and 500 000/75 000/15 000), and towerTasks registers both as BenchTask entries. No sorry or admit appear in the file.
bench/CompPolyBench/Setup.lean: Added a public import for CompPolyBench.Fields.Binary.Tower and appended towerTasks to the allTasks list in def allTasks. This registers the new tower benchmark group as a runnable task, making it selectable via the command-line selector provided by allGroupInfos.
tests/CompPolyTests.lean: Added a public import for CompPolyTests.Fields.Binary.Tower.Fast, integrating the tests for the tower-field implementation (likely a fast arithmetic tower over the binary field) into the top-level test module. This ensures the test suite now covers the newly added Tower submodule alongside the existing binary-field test modules.
tests/CompPolyTests/Fields/Binary/Tower/Fast.lean: This new test file adds regression tests for the packed-word binary tower (FastBT) at widths 3–6 (BT8, BT16, BT32, BT64) and at level 7 (FastBT128). It uses #guard statements to cross-validate addition, multiplication, squaring, inversion, powers, and field operations against concrete tower values and table-based rung functions, and checks ring equivalence round‑trips via ringEquivBT* and FastBT128.ringEquiv. The addition ensures that the fast packed‑word implementation matches the reference concrete tower across all supported widths and that the Field instance behaves as expected (e.g., inverse of zero is zero, characteristic‑two reduction of numerals). No sorry or admit are present.
3 file(s) filtered as noise (lockfiles, generated, or trivial): CompPoly/Fields/README.md, bench/README.md, docs/wiki/binary-fields-and-ntt.md

Last updated: 2026-08-07 09:52 UTC.

dhsorens · 2026-08-07T09:59:49Z

@mitschabaude am I waiting on a review from you on this or is this ready for review?

dhsorens · 2026-08-07T11:16:24Z

I am broadly happy with it (nice improvement on performance here 😃 )

graikos and others added 14 commits August 6, 2026 07:14

feat(fields): initial fast binary towers (k <= 6)

a65c198

test(fields): fast binary tower regression guards

d503d52

docs(fields): fast binary tower rows in README and wiki

cb2d49c

feat(fields): fast binary towers multiplication + proofs

27e6048

feat(fields): fast binary towers mult, sqr and inv

8ca14a2

feat(fields): field instance for fast binary towers

3015edd

feat(fields): small optimizations for towers

7bd3c1b

feat(fields): port fast binary tower onto main (Lean 4.32, module sys…

f4dff45

…tem) Module headers on Fast.lean and its tests, de-private helpers the module system requires in exposed bodies, regenerated import lists. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

feat(fields): removed external C from fast BT; using tables for GF(2^8)

09d6e18

bench(fields): added benchmarks for fast BT implementation

fa4289a

feat(fields): minro proof changes in fast BT

5f21f27

chore(fields): added minor test case in fast BT

47d28f1

docs(fields): adding/modifying comments

1e5c454

refactor(fields): split defs in fast BT for zero-import

d69c605

graikos and others added 3 commits August 6, 2026 08:57

bench(fields): fixed result naming in fast BT benchmarks

d30e7ca

bench(fields): fast BT smaller units in benchmarks

2353013

Merge branch 'main' into tower_hybrid_table

c90a6aa

Navigation Menu

Uh oh!

feat(fields): fast binary tower fields (up to 128 bits) - #286

feat(fields): fast binary tower fields (up to 128 bits)#286
graikos wants to merge 17 commits into
Verified-zkEVM:mainfrom
graikos:tower_hybrid_table

graikos commented Aug 6, 2026

Uh oh!

github-actions Bot commented Aug 6, 2026 •

edited

Loading

Uh oh!

dhsorens commented Aug 7, 2026

Uh oh!

dhsorens commented Aug 7, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

graikos commented Aug 6, 2026

Uh oh!

github-actions Bot commented Aug 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

🤖 PR Summary

Uh oh!

dhsorens commented Aug 7, 2026

Uh oh!

dhsorens commented Aug 7, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

github-actions Bot commented Aug 6, 2026 •

edited

Loading