Verifier: Scaled multiplies, so eq_kernel holds up to 31 coordinates

VERIFICATION.md

@@ -12,7 +12,7 @@ Stage 1 is in place for every crate in `crates/`. [`formal/extraction/README.md`
 - Rust the toolchain cannot translate is rewritten by small patches applied only while extracting. The committed source is never patched, and CI runs each patched crate's tests, including checks against real proofs, on the patched source.
 - CI fails when a committed extraction no longer matches the Rust, when one no longer typechecks, or when the patched source fails its tests. Every run reports what each extraction trusts: opaque items, untranslated bodies, patches, and the shared standard-library models.
 
-Stage 2 has begun with the native verifier, whose proofs live in `crates/verifier/proofs/verifier/lean/Verifier/Verification/` and are built with every extraction. They show that the extracted field arithmetic is CompPoly's `BF64` and its cubic extension `Ext3`, that `eq_kernel` computes ArkLib's `multilinearWeight`, and that the verifier's WHIR fold of a queried row is ArkLib's `multilinearCombine` of the row's lanes, at level 0 (`level0_fold`) and at every deeper level (`deeper_fold`), resting on no opaque item's assumption.
+Stage 2 has begun with the native verifier, whose proofs live in `crates/verifier/proofs/verifier/lean/Verifier/Verification/` and are built with every extraction. They show that the extracted field arithmetic is CompPoly's `BF64` and its cubic extension `Ext3`, that `Scaled`, the table the verifier multiplies a fixed factor through, computes the product (`scaled_mul`), that `eq_kernel` computes ArkLib's `multilinearWeight` at points of up to 31 coordinates, and that the verifier's WHIR fold of a queried row is ArkLib's `multilinearCombine` of the row's lanes, at level 0 (`level0_fold`) and at every deeper level (`deeper_fold`), resting on no opaque item's assumption.
 
 ## Introduction
 

crates/verifier/proofs/verifier/lean/Verifier/Extraction/Funs.lean

@@ -2312,7 +2312,7 @@ def field.Scaled.new (r : field.E) : RustM field.Scaled := do
   ok tables1
 
 /-- [verifier::field::{verifier::field::Scaled}::mul]: loop body 1:
-    Source: 'crates/verifier/src/field.rs', lines 261:12-264:13
+    Source: 'crates/verifier/src/field.rs', lines 263:12-266:13
     Visibility: public -/
 @[rust_loop_body]
 def field.Scaled.mul_loop0_loop0.body
@@ -2342,7 +2342,7 @@ def field.Scaled.mul_loop0_loop0.body
     ok (cont (iter1, self, product1, table1))
 
 /-- [verifier::field::{verifier::field::Scaled}::mul]: loop 1:
-    Source: 'crates/verifier/src/field.rs', lines 261:12-264:13
+    Source: 'crates/verifier/src/field.rs', lines 263:12-266:13
     Visibility: public -/
 @[rust_loop]
 def field.Scaled.mul_loop0_loop0
@@ -2356,52 +2356,52 @@ def field.Scaled.mul_loop0_loop0
     (iter, self, product, table)
 
 /-- [verifier::field::{verifier::field::Scaled}::mul]: loop body 0:
-    Source: 'crates/verifier/src/field.rs', lines 260:8-265:9
+    Source: 'crates/verifier/src/field.rs', lines 261:8-267:9
     Visibility: public -/
 @[rust_loop_body]
 def field.Scaled.mul_loop0.body
-  (iter : core.array.iter.IntoIter Std.U64 3#usize) (self : field.Scaled)
-  (product : field.E) (table : Std.Usize) :
-  RustM (ControlFlow ((core.array.iter.IntoIter Std.U64 3#usize) ×
-    field.Scaled × field.E × Std.Usize) field.E)
+  (limbs : Array Std.U64 3#usize) (iter : core.ops.range.Range Std.Usize)
+  (self : field.Scaled) (product : field.E) (table : Std.Usize) :
+  RustM (ControlFlow ((core.ops.range.Range Std.Usize) × field.Scaled ×
+    field.E × Std.Usize) field.E)
   := do
   let (o, iter1) ←
-    core.array.iter.IntoIter.Insts.CoreIterTraitsIteratorIterator.next iter
+    core.ops.range.Range.Insts.CoreIterTraitsIteratorIterator.next
+      core.Usize.Insts.CoreIterRangeStep iter
   match o with
   | core.option.Option.None => ok (done product)
-  | core.option.Option.Some limb =>
+  | core.option.Option.Some t =>
+    let limb ← Array.index_usize limbs t
     let i ← field.WINDOWS_PER_LIMB
     let (self1, product1, table1) ←
       field.Scaled.mul_loop0_loop0 { start := 0#usize, «end» := i } self
         product table limb
     ok (cont (iter1, self1, product1, table1))
 
 /-- [verifier::field::{verifier::field::Scaled}::mul]: loop 0:
-    Source: 'crates/verifier/src/field.rs', lines 260:8-265:9
+    Source: 'crates/verifier/src/field.rs', lines 261:8-267:9
     Visibility: public -/
 @[rust_loop]
 def field.Scaled.mul_loop0
-  (iter : core.array.iter.IntoIter Std.U64 3#usize) (self : field.Scaled)
-  (product : field.E) (table : Std.Usize) :
+  (iter : core.ops.range.Range Std.Usize) (self : field.Scaled)
+  (product : field.E) (table : Std.Usize) (limbs : Array Std.U64 3#usize) :
   RustM field.E
   := do
   loop
-    (fun (iter1, self1, product1, table1) => field.Scaled.mul_loop0.body iter1
-      self1 product1 table1)
+    (fun (iter1, self1, product1, table1) => field.Scaled.mul_loop0.body limbs
+      iter1 self1 product1 table1)
     (iter, self, product, table)
 
 /-- [verifier::field::{verifier::field::Scaled}::mul]:
-    Source: 'crates/verifier/src/field.rs', lines 257:4-267:5
+    Source: 'crates/verifier/src/field.rs', lines 257:4-269:5
     Visibility: public -/
 def field.Scaled.mul (self : field.Scaled) (a : field.E) : RustM field.E := do
   let product ← field.ZERO
-  let iter ←
-    core.Array.Insts.CoreIterTraitsCollectIntoIteratorTIntoIter.into_iter
-      (Array.make 3#usize [ a.c0, a.c1, a.c2 ])
-  field.Scaled.mul_loop0 iter self product 0#usize
+  field.Scaled.mul_loop0 { start := 0#usize, «end» := 3#usize } self product
+    0#usize (Array.make 3#usize [ a.c0, a.c1, a.c2 ])
 
 /-- [verifier::field::powers]: loop body 0:
-    Source: 'crates/verifier/src/field.rs', lines 274:4-277:5
+    Source: 'crates/verifier/src/field.rs', lines 276:4-279:5
     Visibility: public -/
 @[rust_loop_body]
 def field.powers_loop.body
@@ -2421,7 +2421,7 @@ def field.powers_loop.body
     ok (cont (iter1, out1, power1))
 
 /-- [verifier::field::powers]: loop 0:
-    Source: 'crates/verifier/src/field.rs', lines 274:4-277:5
+    Source: 'crates/verifier/src/field.rs', lines 276:4-279:5
     Visibility: public -/
 @[rust_loop]
 def field.powers_loop
@@ -2435,7 +2435,7 @@ def field.powers_loop
     (iter, out, power)
 
 /-- [verifier::field::powers]:
-    Source: 'crates/verifier/src/field.rs', lines 271:0-279:1
+    Source: 'crates/verifier/src/field.rs', lines 273:0-281:1
     Visibility: public -/
 def field.powers
   (base : field.E) (count : Std.Usize) : RustM (alloc.vec.Vec field.E) := do

crates/verifier/proofs/verifier/lean/Verifier/Verification/Dot.lean

@@ -108,7 +108,7 @@ element of the row's words `3i, 3i + 1, 3i + 2`. -/
 def extLanes (words : List verifier.field.K) (ϑ : ℕ) : Fin (2 ^ ϑ) → Unit → BF64.Ext3 :=
   fun i _ => toExt3 (wordsE words i)
 
-theorem deeper_fold (point : Slice verifier.field.E) (hn : point.length ≤ 8)
+theorem deeper_fold (point : Slice verifier.field.E) (hn : point.length ≤ 31)
     (lw : alloc.vec.Vec verifier.field.E) (hlw : verifier.multilinear.eq_kernel point = ok lw)
     (words : Slice verifier.field.K) (hwords : words.length = 3 * 2 ^ point.length)
     (row : alloc.vec.Vec verifier.field.E) (hrow : verifier.whir.ext_row words = ok row)

crates/verifier/proofs/verifier/lean/Verifier/Verification/EqKernel.lean

@@ -1,9 +1,9 @@
-import Verifier.Verification.Std
+import Verifier.Verification.Scaled
 import ArkLib.Data.CodingTheory.Prelims
 
 /-! `eq_kernel(point)` is the table of ArkLib's `multilinearWeight point i` over every index `i`
-(`eq_kernel_spec`, `eqw_eq_multilinearWeight`), for the points of at most 8 coordinates on which it
-multiplies without `Scaled`'s table, which covers every fold. -/
+(`eq_kernel_spec`, `eqw_eq_multilinearWeight`), for points of at most 31 coordinates, whose `1 << len` fits
+a 32-bit `usize`, through `Scaled`'s table or not. -/
 
 open CoreModels Aeneas
 open Aeneas.Std hiding namespace core alloc
@@ -17,6 +17,19 @@ theorem scaler_plain_mul (r v : verifier.field.E) :
     verifier.multilinear.Scaler.mul (.Plain r) v = ok (ofExt3 (toExt3 v * toExt3 r)) := by
   simp [verifier.multilinear.Scaler.mul, E_mul_ok]
 
+/-- A `Scaler` multiplies by its factor, through `Scaled`'s table or not. -/
+@[spec]
+theorem scaler_new_spec (r : verifier.field.E) (uses : Std.Usize) :
+    ⦃ ⌜ True ⌝ ⦄
+    verifier.multilinear.Scaler.new r uses
+    ⦃ ⇓ sc => ⌜ ∀ v, verifier.multilinear.Scaler.mul sc v = ok (ofExt3 (toExt3 v * toExt3 r)) ⌝ ⦄ := by
+  unfold verifier.multilinear.Scaler.new
+  split
+  · obtain ⟨s, hs⟩ := Hax.triple_noThrow_exists_ok (new_spec r)
+    rw [hs, Aeneas.Std.bind_ok]
+    exact Hax.triple_of_ok rfl fun v => scaled_mul r s hs v
+  · exact Hax.triple_of_ok rfl fun v => scaler_plain_mul r v
+
 /-- What the inner loop of `eq_kernel` leaves at entry `j`, after `i` of its `half` steps. -/
 def innerAt (out0 : List verifier.field.E) (r : BF64.Ext3) (half i j : ℕ) : BF64.Ext3 :=
   if j < i then toExt3 out0[j]! * (1 + r)
@@ -138,7 +151,7 @@ def outerInv (point : Slice verifier.field.E) (n : ℕ) (k : Std.Usize) (out : a
     toExt3 out.val[j]! = if j < 2 ^ k.val then eqw (fun t => toExt3 point.val[t]!) k.val j else 0)
 
 @[spec]
-theorem outer_spec (point : Slice verifier.field.E) (hn : point.length ≤ 8) (out0 : alloc.vec.Vec verifier.field.E)
+theorem outer_spec (point : Slice verifier.field.E) (hn : point.length ≤ 31) (out0 : alloc.vec.Vec verifier.field.E)
     (h0 : (outerInv point point.length 0#usize out0).holds) (e : Std.Usize) (he : e = point.len) :
     ⦃ ⌜ True ⌝ ⦄
     verifier.multilinear.eq_kernel_loop0 { start := 0#usize, «end» := e } point out0
@@ -152,26 +165,17 @@ theorem outer_spec (point : Slice verifier.field.E) (hn : point.length ≤ 8) (o
     simp only [outerInv, holds_ok] at hinv
     obtain ⟨hlen, hval⟩ := hinv
     clear h0
-    hax_mvcgen [verifier.multilinear.eq_kernel_loop0.body, verifier.multilinear.Scaler.new, inner_spec, innerInv, outerInv]
-    case vc1.h_ok.isTrue =>
-      rename_i hlt s hs h hh1 _ _ _ _ hge
-      have hk7 : k.val ≤ 7 := by scalar_tac
-      have : 2 ^ k.val ≤ 2 ^ 7 := Nat.pow_le_pow_right (by omega) hk7
-      have hh : h.val = 2 ^ k.val := hh1.trans (one_shl k (by omega))
-      exfalso; scalar_tac
-    case vc3.hmul => exact scaler_plain_mul _ _
-    case vc4.hh =>
-      rename_i hlt s hs h hh1 _ _ _ _ _
-      have hk7 : k.val ≤ 7 := by scalar_tac
-      have : 2 ^ k.val ≤ 2 ^ 7 := Nat.pow_le_pow_right (by omega) hk7
+    hax_mvcgen [verifier.multilinear.eq_kernel_loop0.body, scaler_new_spec, inner_spec, innerInv, outerInv]
+    case vc3.hh =>
+      rename_i hlt s hs h hh1 _ _ _ _ _ _
+      have hk30 : k.val ≤ 30 := by scalar_tac
       have hh : h.val = 2 ^ k.val := hh1.trans (one_shl k (by omega))
       have : 2 ^ (k.val + 1) ≤ 2 ^ point.length := Nat.pow_le_pow_right (by omega) (by scalar_tac)
       rw [hh, hlen, ← pow_succ']
       exact this
-    case vc5 =>
-      rename_i hlt s hs h hh1 _ _ x hx _ out hol hov
-      have hk7 : k.val ≤ 7 := by scalar_tac
-      have : 2 ^ k.val ≤ 2 ^ 7 := Nat.pow_le_pow_right (by omega) hk7
+    case vc4 =>
+      rename_i hlt s hs h hh1 _ _ x hx _ _ out hol hov
+      have hk30 : k.val ≤ 30 := by scalar_tac
       have hh : h.val = 2 ^ k.val := hh1.trans (one_shl k (by omega))
       obtain ⟨hxk, rfl⟩ := hx
       refine ⟨hlt, trivial, hs, ?_⟩
@@ -180,17 +184,17 @@ theorem outer_spec (point : Slice verifier.field.E) (hn : point.length ≤ 8) (o
       refine outer_step _ point.length k.val (by scalar_tac) acc.val out.val hval (fun j hj => ?_)
       rw [hov j (by rw [hlen]; exact hj), hh]
       simp [getElem!_pos, hxk]
-    case vc6.h_fail => scalar_tac
-    case vc7.h_fail =>
-      have : k.val ≤ 7 := by scalar_tac
+    case vc5.h_fail => scalar_tac
+    case vc6.h_fail =>
+      have : k.val ≤ 30 := by scalar_tac
       exfalso; cases System.Platform.numBits_eq <;> omega
     case vc1.hQ =>
       rename_i hge
       have hkl : k.val = point.length := by scalar_tac
       refine ⟨hlen, fun j hj => ?_⟩
       rw [hval j hj, Slice.len_val, ← hkl]
 
-theorem eq_kernel_spec (point : Slice verifier.field.E) (hn : point.length ≤ 8) :
+theorem eq_kernel_spec (point : Slice verifier.field.E) (hn : point.length ≤ 31) :
     ⦃ ⌜ True ⌝ ⦄
     verifier.multilinear.eq_kernel point
     ⦃ ⇓ out => ⌜ out.length = 2 ^ point.length ∧

crates/verifier/proofs/verifier/lean/Verifier/Verification/Field.lean

@@ -1,5 +1,6 @@
 import Verifier.Verification.Field.Base
 import Verifier.Verification.Field.Ext
+import Verifier.Verification.Field.Window
 
 /-! The verifier's fields are CompPoly's: the extracted `K` and `E` products are `BF64` and `Ext3`
 multiplication (`Field.mul_ok`, `Field.E_mul_ok`), so ArkLib's statements over those fields

crates/verifier/proofs/verifier/lean/Verifier/Verification/Field/Window.lean

@@ -0,0 +1,74 @@
+import Verifier.Verification.Field.Bits
+
+/-! The base field by bits, as `Scaled` (`verifier::field`) reads it: `times_x` multiplies by `x`
+(`ofBitVec_timesX`), and a word is the sum over its six-bit windows of each window's bits weighed by
+the powers of `x` they stand for (`sum_win`). -/
+
+namespace Verifier.Field
+
+open BinaryField
+
+/-- `x` in `BF64`. -/
+def X : BF64 := BF64.ofBitVec 2#64
+
+/-- `Scaled::new`'s `times_x`: a word shifted up by one, its overflow past `x^63` reduced. -/
+def timesX (v : BitVec 64) : BitVec 64 := v <<< 1 ^^^ ((0#64 - (v >>> 63)) &&& 0x1B#64)
+
+set_option maxRecDepth 100000 in
+set_option maxHeartbeats 0 in
+theorem timesX_eq (v : BitVec 64) : timesX v = BF64.reduce (carryLessMul (w := 128) 2#64 v) := by
+  simp only [timesX, BF64.reduce, BF64.foldStep, BF64.highHalf, BF64.lowHalf, BF64.reductionConstant,
+    carryLessMul_eq_range, zeroExtendTo, List.range, List.range.loop, List.foldl]
+  bv_decide (config := { timeout := 3600 })
+
+theorem ofBitVec_timesX (v : BitVec 64) : BF64.ofBitVec (timesX v) = X * BF64.ofBitVec v := by
+  rw [timesX_eq]; rfl
+
+/-- A word is the sum of the powers of `x` its set bits stand for. -/
+theorem ofBitVec_eq_sum (c : BitVec 64) :
+    BF64.ofBitVec c = ∑ i ∈ Finset.range 64, if c.getLsbD i then X ^ i else 0 := by
+  apply BF64.toQuot_injective
+  have hX : BF64.toQuot X = AdjoinRoot.mk BF64.basePoly Polynomial.X := by
+    rw [BF64.toQuot, BF64.toPolyBF64, X, BF64.toBitVec_ofBitVec,
+      show (2#64 : BitVec 64) = 1 <<< 1 from rfl, toPoly_one_shiftLeft 1 (by omega), pow_one]
+  let q : BF64 →+ BF64.BF64Quot := AddMonoidHom.mk' BF64.toQuot BF64.toQuot_add
+  rw [show BF64.toQuot (∑ i ∈ Finset.range 64, if c.getLsbD i then X ^ i else 0) =
+    q (∑ i ∈ Finset.range 64, if c.getLsbD i then X ^ i else 0) from rfl, map_sum]
+  simp only [q, AddMonoidHom.mk'_apply, apply_ite BF64.toQuot, BF64.toQuot_npow, hX, BF64.toQuot_zero]
+  rw [BF64.toQuot, BF64.toPolyBF64, BF64.toBitVec_ofBitVec, toPoly, map_sum, Finset.sum_range
+    (fun i => if c.getLsbD i then AdjoinRoot.mk BF64.basePoly Polynomial.X ^ i else 0)]
+  refine Finset.sum_congr rfl fun i _ => ?_
+  simp [apply_ite (AdjoinRoot.mk BF64.basePoly), BitVec.getLsb, BitVec.getElem_eq_testBit_toNat]
+
+/-- Window `j`'s value `n`, its bits weighed by the powers of `x` they stand for. -/
+def win (j n : ℕ) : BF64 := ∑ b ∈ Finset.range 6, if n.testBit b then X ^ (6 * j + b) else 0
+
+theorem sum_range_six_mul {M : Type} [AddCommMonoid M] (f : ℕ → M) (m : ℕ) :
+    ∑ k ∈ Finset.range (6 * m), f k = ∑ j ∈ Finset.range m, ∑ b ∈ Finset.range 6, f (6 * j + b) := by
+  induction m with
+  | zero => simp
+  | succ m ih =>
+    rw [Nat.mul_succ, Finset.sum_range_add, ih, Finset.sum_range_succ (fun j => ∑ b ∈ Finset.range 6, f (6 * j + b))]
+
+/-- A word is the sum of its eleven six-bit windows, the last holding its top four bits. -/
+theorem sum_win (c : BitVec 64) :
+    ∑ j ∈ Finset.range 11, win j (c.toNat >>> (6 * j) % 64) = BF64.ofBitVec c := by
+  rw [ofBitVec_eq_sum]
+  have h66 : ∑ i ∈ Finset.range 64, (if c.getLsbD i then X ^ i else 0) =
+      ∑ k ∈ Finset.range (6 * 11), if c.toNat.testBit k then X ^ k else 0 := by
+    rw [show 6 * 11 = 64 + 2 by rfl, Finset.sum_range_add]
+    have : ∀ x ∈ Finset.range 2, (if c.toNat.testBit (64 + x) then X ^ (64 + x) else 0) = 0 := by
+      intro x _
+      rw [Nat.testBit_lt_two_pow (lt_of_lt_of_le c.isLt (Nat.pow_le_pow_right (by omega) (by omega)))]
+      rfl
+    rw [Finset.sum_eq_zero this, add_zero]
+    rfl
+  rw [h66, sum_range_six_mul]
+  refine Finset.sum_congr rfl fun j _ => Finset.sum_congr rfl fun b hb => ?_
+  have hb : b < 6 := Finset.mem_range.mp hb
+  have key : ((c.toNat >>> (6 * j)) % 2 ^ 6).testBit b = c.toNat.testBit (6 * j + b) := by
+    rw [Nat.testBit_mod_two_pow, Nat.testBit_shiftRight]
+    simp [hb]
+  rw [show c.toNat >>> (6 * j) % 64 = c.toNat >>> (6 * j) % 2 ^ 6 from rfl, key]
+
+end Verifier.Field

crates/verifier/proofs/verifier/lean/Verifier/Verification/Fold.lean

@@ -61,7 +61,7 @@ theorem base_fold_spec (row : Slice verifier.field.K) (w : Slice verifier.field.
 def lanes (row : List verifier.field.K) (ϑ : ℕ) : Fin (2 ^ ϑ) → Unit → BF64.Ext3 :=
   fun i _ => toBF64 row[2 ^ ϑ - 1 - (i : ℕ)]! • 1
 
-theorem level0_fold (point : Slice verifier.field.E) (hn : point.length ≤ 8)
+theorem level0_fold (point : Slice verifier.field.E) (hn : point.length ≤ 31)
     (lw : alloc.vec.Vec verifier.field.E) (hlw : verifier.multilinear.eq_kernel point = ok lw)
     (row : Slice verifier.field.K) (hrow : row.length = 2 ^ point.length)
     (w : Slice verifier.field.E) (hw : w.val = lw.val) :