feat(formal): Clean/Lean model of BITWISE, LT, EQ and SHIFT with proo…

.github/workflows/formal.yml

@@ -0,0 +1,54 @@
+name: Formal model
+
+on:
+  push:
+    branches: ["main"]
+    paths: ["formal/**", ".github/workflows/formal.yml"]
+  pull_request:
+    paths: ["formal/**", ".github/workflows/formal.yml"]
+
+permissions:
+  contents: read
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }}
+  cancel-in-progress: true
+
+jobs:
+  lean:
+    name: Lean build and export check
+    runs-on: ubuntu-latest
+    timeout-minutes: 120
+    defaults:
+      run:
+        working-directory: formal
+    steps:
+      - name: Checkout sources
+        uses: actions/checkout@v4
+
+      - name: Install elan
+        run: |
+          curl https://elan.lean-lang.org/elan-init.sh -sSf | sh -s -- -y --default-toolchain none
+          echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
+
+      # Clean and CompPoly are compiled from source; Mathlib comes from its own cache below.
+      - name: Cache Lake builds
+        uses: actions/cache@v4
+        with:
+          path: |
+            formal/.lake
+            !formal/.lake/packages/mathlib
+          key: lake-${{ hashFiles('formal/lean-toolchain', 'formal/lake-manifest.json') }}-${{ github.sha }}
+          restore-keys: |
+            lake-${{ hashFiles('formal/lean-toolchain', 'formal/lake-manifest.json') }}-
+
+      - name: Fetch Mathlib binaries
+        run: lake exe cache get
+
+      - name: Build
+        run: lake build
+
+      - name: Export is up to date
+        run: |
+          lake env lean --run LambdaVM/Export.lean
+          git diff --exit-code -- export

crypto/stark/src/lookup.rs

@@ -1414,7 +1414,7 @@ impl Multiplicity {
     /// Evaluate the multiplicity expression to a field element. `get_col(i)`
     /// must return the value of main column `i` at the row being evaluated.
     #[inline]
-    fn evaluate_with<F, G>(&self, get_col: G) -> FieldElement<F>
+    pub fn evaluate_with<F, G>(&self, get_col: G) -> FieldElement<F>
     where
         F: IsField,
         G: Fn(usize) -> FieldElement<F>,

formal/.gitignore

@@ -0,0 +1 @@
+.lake/

formal/LambdaVM.lean

@@ -0,0 +1,14 @@
+module
+
+public import LambdaVM.Field
+public import LambdaVM.AluOp
+public import LambdaVM.Templates.IsBit
+public import LambdaVM.Templates.Add
+public import LambdaVM.Tables.Bitwise
+public import LambdaVM.Templates.IsByte
+public import LambdaVM.Buses.Alu
+public import LambdaVM.Tables.Lt
+public import LambdaVM.Tables.Eq
+public import LambdaVM.Tables.Shift
+public import LambdaVM.Ensembles.EqLookup
+public import LambdaVM.Channels.Counted

formal/LambdaVM/AluOp.lean

@@ -0,0 +1,23 @@
+module
+
+public import LambdaVM.Field
+
+@[expose] public section
+
+/-!
+# `alu_op` descriptors (`prover/src/tables/types.rs`)
+
+One enumeration serves two places: the `opsel` of the `BYTE_ALU` lookup (AND, OR, XOR) and the
+low bits of the flag byte on the `ALU` bus (EQ, LT, SHIFT).
+-/
+
+namespace LambdaVM
+
+def opselAND : ℕ := 0
+def opselOR : ℕ := 1
+def opselXOR : ℕ := 2
+def opselEQ : ℕ := 3
+def opselLT : ℕ := 4
+def opselSHIFT : ℕ := 5
+
+end LambdaVM

formal/LambdaVM/Buses/Alu.lean

@@ -0,0 +1,92 @@
+module
+
+public import LambdaVM.Field
+public import LambdaVM.AluOp
+
+@[expose] public section
+
+/-!
+# ALU bus (`BusId::Alu`)
+
+`ALU[out; in1, in2, flags]`: operands and result travel as `(lo32, hi32)` pairs, `flags`
+carries the `alu_op` descriptor plus per-chip flag bits. Every ALU chip pushes to this
+channel; the CPU pulls. Each chip adds the clause of `Guarantees` for its own `opsel`.
+-/
+
+namespace LambdaVM.Alu
+
+structure Msg (F : Type) where
+  in1Lo : F
+  in1Hi : F
+  in2Lo : F
+  in2Hi : F
+  flags : F
+  outLo : F
+  outHi : F
+deriving ProvableStruct
+
+/-- `lhs < rhs` on 64-bit values, signed (two's complement) or unsigned, as a bit. -/
+def ltRaw (signed L R : ℕ) : ℕ :=
+  if signed = 1 then (if (BitVec.ofNat 64 L).slt (BitVec.ofNat 64 R) then 1 else 0)
+  else (if (BitVec.ofNat 64 L).ult (BitVec.ofNat 64 R) then 1 else 0)
+
+/-- The two comparisons on values below `2⁶⁴`, read on naturals. -/
+lemma ult_ofNat_iff {L R : ℕ} (hL : L < 2^64) (hR : R < 2^64) :
+    (BitVec.ofNat 64 L).ult (BitVec.ofNat 64 R) = true ↔ L < R := by
+  simp only [BitVec.ult_eq_decide, decide_eq_true_eq, BitVec.toNat_ofNat, Nat.mod_eq_of_lt hL,
+    Nat.mod_eq_of_lt hR]
+
+lemma slt_ofNat_iff {L R : ℕ} (hL : L < 2^64) (hR : R < 2^64) :
+    (BitVec.ofNat 64 L).slt (BitVec.ofNat 64 R) = true ↔
+      (if L < 2^63 then (L : ℤ) else (L : ℤ) - 2^64) <
+        (if R < 2^63 then (R : ℤ) else (R : ℤ) - 2^64) := by
+  simp only [BitVec.slt_eq_decide, decide_eq_true_eq, BitVec.toInt_eq_toNat_cond, BitVec.toNat_ofNat,
+    Nat.mod_eq_of_lt hL, Nat.mod_eq_of_lt hR]
+  split_ifs <;> omega
+
+/-- LT result: `(lhs < rhs) xor invert`. -/
+def ltBit (signed invert L R : ℕ) : ℕ :=
+  if ltRaw signed L R = invert then 0 else 1
+
+/-- EQ result: `(a = b) xor invert`. -/
+def eqBit (invert A B : ℕ) : ℕ :=
+  if (if A = B then 1 else 0) = invert then 0 else 1
+
+/-- Arithmetic right shift of a 64-bit value: sign-extend to 128 bits, shift, truncate. -/
+def sra64 (x k : ℕ) : ℕ :=
+  if x < 2^63 then x >>> k else ((x + (2^128 - 2^64)) >>> k) % 2^64
+
+/-- `SHIFT` result (spec/shift.typ): the shift amount is reduced mod 32 for word instructions
+and mod 64 otherwise; `direction` picks left (0) or right (1); `signed` picks the arithmetic
+right shift. Word results are not sign-extended here (the CPU does that). -/
+def shiftResult (word signed direction x s : ℕ) : ℕ :=
+  let k := s % (if word = 1 then 32 else 64)
+  if direction = 0 then (x <<< k) % 2^64
+  else if signed = 0 then x >>> k
+  else sra64 x k
+
+/-- What a puller learns. The caller must have range-checked both words of both operands
+(the chips' `IS_WORD` assumptions). One clause per `opsel`, selected by the flag byte read
+as a natural. -/
+def Guarantees (m : Msg (F p)) : Prop :=
+  m.in1Lo.val < 2^32 → m.in1Hi.val < 2^32 → m.in2Lo.val < 2^32 → m.in2Hi.val < 2^32 →
+    -- LT (spec/lt.typ): flags = opsel(LT) + 32·signed + 64·invert, out = [res, 0]
+    (∀ s i : ℕ, s < 2 → i < 2 → m.flags.val = opselLT + 32 * s + 64 * i →
+      m.outHi = 0 ∧
+      m.outLo = ((ltBit s i (dword m.in1Lo m.in1Hi) (dword m.in2Lo m.in2Hi) : ℕ) : F p)) ∧
+    -- EQ (spec/eq.typ): flags = opsel(EQ) + 64·invert, out = [res, 0]
+    (∀ i : ℕ, i < 2 → m.flags.val = opselEQ + 64 * i →
+      m.outHi = 0 ∧
+      m.outLo = ((eqBit i (dword m.in1Lo m.in1Hi) (dword m.in2Lo m.in2Hi) : ℕ) : F p)) ∧
+    -- SHIFT (spec/shift.typ): flags = opsel(SHIFT) + word_instr + 32·signed + 64·direction,
+    -- only the low byte of the shift amount matters
+    (∀ w s d : ℕ, w < 2 → s < 2 → d < 2 →
+      m.flags.val = opselSHIFT + w + 32 * s + 64 * d →
+      m.outLo.val < 2^32 ∧ m.outHi.val < 2^32 ∧
+      dword m.outLo m.outHi = shiftResult w s d (dword m.in1Lo m.in1Hi) (m.in2Lo.val % 256))
+
+def channel : Channel (F p) Msg where
+  name := "ALU"
+  Guarantees m _ := Guarantees m
+
+end LambdaVM.Alu