chore: Cleanup and linting after the initial Clean changes

.github/workflows/lean_action_ci.yml

@@ -16,6 +16,8 @@ jobs:
       - uses: actions/checkout@v4
       - name: No skipKernelTC in source
         run: scripts/check_no_skipkerneltc.sh
+      - name: No native_decide in the main SP1Clean library
+        run: scripts/check_no_native_decide.sh
 
   build:
     runs-on:
@@ -31,10 +33,74 @@ jobs:
       - uses: actions/checkout@v4
       # Test that the project builds without failure
       # Note: defaults to ignore warnings and deprecations, maybe change eventually
+      # lean-action's `use-github-cache` caches the WHOLE `.lake` (project build + deps) under a
+      # commit-keyed key (`lake-<os>-<arch>-<toolchain>-<manifest>-<sha>`) with a manifest-prefix
+      # `restore-keys` fallback. So this build is incremental from the most recent prior commit, and the
+      # exact-`<sha>` cache it saves is what the `lint`/`test` jobs restore (an exact hit → `lake build`
+      # there just replays, no recompilation). No separate per-commit project cache is needed.
       - uses: leanprover/lean-action@v1
         with:
           build: "true"
           test: "false"
           lint: "false"
           use-github-cache: "true"
 
+  lint:
+    # Environment linters (`lake lint` → the `sp1Lint` lintDriver; a curated subset of the Batteries
+    # `#lint` linters over the hand-written `SP1Clean.*` declarations; see AGENTS.md § Linters). Split
+    # into its own job so it is clearly independent in the checks list. `needs: build` so it runs after
+    # the build job has saved its exact-`<sha>` `.lake` cache; lean-action below restores that on an exact
+    # hit, so `lake build` just replays the already-built project (no recompilation) before `lake lint`.
+    # If that cache were ever absent, lean-action's manifest-prefix `restore-keys` fallback does a correct
+    # incremental build instead, so the job stays correct either way.
+    needs: build
+    runs-on:
+      [
+        runs-on,
+        runner=64cpu-linux-x64,
+        spot=false,
+        disk=large,
+        "run-id=${{ github.run_id }}",
+      ]
+
+    steps:
+      - uses: actions/checkout@v4
+      - uses: leanprover/lean-action@v1
+        with:
+          build: "true"
+          test: "false"
+          lint: "false"
+          use-github-cache: "true"
+      - name: Environment linters (lake lint)
+        run: lake lint
+
+  test:
+    # Conformance tests (`lake test` → the `SP1CleanTest` testDriver: the witness-generation and
+    # whole-trace `native_decide` anchors checked against batteries dumped from SP1's real Rust prover).
+    # These live in their own library — the ONLY place `native_decide` is allowed — so they are gated
+    # here, separately from the `native_decide`-free main build. Split into its own job (in parallel with
+    # `lint`) so the trusted-compiler checks are clearly independent in the checks list. `needs: build`
+    # so it runs after the build job has saved its exact-`<sha>` `.lake` cache; lean-action below restores
+    # that on an exact hit, so `lake build` replays the already-built main library (no recompilation) and
+    # `lake test` only elaborates the test modules. If that cache were ever absent, lean-action's
+    # manifest-prefix `restore-keys` fallback does a correct incremental build instead.
+    needs: build
+    runs-on:
+      [
+        runs-on,
+        runner=64cpu-linux-x64,
+        spot=false,
+        disk=large,
+        "run-id=${{ github.run_id }}",
+      ]
+
+    steps:
+      - uses: actions/checkout@v4
+      - uses: leanprover/lean-action@v1
+        with:
+          build: "true"
+          test: "false"
+          lint: "false"
+          use-github-cache: "true"
+      - name: Conformance tests (lake test)
+        run: lake test

README.md

@@ -116,10 +116,14 @@ Trace-level consistency properties and the whole-machine capstone.
 - `GatedVm/` + `SP1GatedVm.lean` — the execution capstone (`sp1_machine_soundness`), the final
   Clean `FormalEnsemble`.
 
-### `Proofs/WitnessTests/` (+ `Extracted/WitnessVectors/`)
-Tests the witness generators for most operations against explicit vectors generated by SP1. The hand-written
-`native_decide` anchors (`<Op>Witness.lean`) live in `Proofs/WitnessTests/`; the auto-generated vectors live in
-`Extracted/WitnessVectors/`. Shows conformance on test cases; doesn't directly prove witness generation faithful.
+### `SP1CleanTest/` — the test library (`lake test`)
+A separate top-level library (it imports `SP1Clean`, but is **not** part of the main `lake build`) holding
+the conformance tests — the project's only `native_decide` (which trusts the whole compiler, so it is kept
+out of the main library by `scripts/check_no_native_decide.sh`). Two layers: `WitnessTests/` checks each
+operation's witness generator against explicit vectors dumped from SP1 (`<Op>Witness.lean` anchors +
+auto-generated `WitnessTests/Vectors/`), and `TraceGenTests/` checks whole chip traces re-derived from each
+chip's own circuit against SP1's real `generate_trace`. Shows conformance on test cases; doesn't directly
+prove witness generation faithful. Run with `lake test`.
 
 ## How a proof connects to SP1
 

SP1Clean.lean

@@ -32,6 +32,7 @@ import SP1Clean.Proofs.Chips.DivRemChip.Soundness.Remu
 import SP1Clean.Proofs.Chips.DivRemChip.Soundness.Remuw
 import SP1Clean.Proofs.Chips.DivRemChip.Soundness.Remw
 import SP1Clean.Proofs.Chips.DivRemChip.Soundness.Reader
+import SP1Clean.Proofs.Chips.DivRemChip.Soundness.Tail
 import SP1Clean.Proofs.Chips.DivRemChip.Populate
 import SP1Clean.Proofs.Chips.DivRemChip.Populate.Abs
 import SP1Clean.Proofs.Chips.DivRemChip.Populate.Bounds
@@ -217,6 +218,8 @@ import SP1Clean.Faithful.U16toU8OperationSafe
 import SP1Clean.Faithful.U16toU8OperationUnsafe
 import SP1Clean.Faithful.UTypeChip
 import SP1Clean.Math.Bitwise
+import SP1Clean.Math.EvalVec
+import SP1Clean.Math.Gate
 import SP1Clean.Model.ByteTable
 import SP1Clean.Model.Channels
 import SP1Clean.Model.ChipAir
@@ -334,53 +337,3 @@ import SP1Clean.FormalModel.Trace.Witness
 import SP1Clean.FormalModel.Contracts.Operations
 import SP1Clean.FormalModel.Contracts.Readers
 import SP1Clean.Soundness.RowView
-import SP1Clean.Proofs.WitnessTests.AddOperationWitness
-import SP1Clean.Extracted.WitnessVectors.AddOperation
-import SP1Clean.Proofs.WitnessTests.AddrAddOperationWitness
-import SP1Clean.Extracted.WitnessVectors.AddrAddOperation
-import SP1Clean.Proofs.WitnessTests.AddwOperationWitness
-import SP1Clean.Extracted.WitnessVectors.AddwOperation
-import SP1Clean.Proofs.WitnessTests.BitwiseOperationWitness
-import SP1Clean.Extracted.WitnessVectors.BitwiseOperation
-import SP1Clean.Proofs.WitnessTests.IsEqualWordOperationWitness
-import SP1Clean.Extracted.WitnessVectors.IsEqualWordOperation
-import SP1Clean.Proofs.WitnessTests.IsZeroOperationWitness
-import SP1Clean.Extracted.WitnessVectors.IsZeroOperation
-import SP1Clean.Proofs.WitnessTests.IsZeroWordOperationWitness
-import SP1Clean.Extracted.WitnessVectors.IsZeroWordOperation
-import SP1Clean.Proofs.WitnessTests.LtOperationUnsignedWitness
-import SP1Clean.Extracted.WitnessVectors.LtOperationUnsigned
-import SP1Clean.Proofs.WitnessTests.MulOperationWitness
-import SP1Clean.Extracted.WitnessVectors.MulOperation
-import SP1Clean.Proofs.WitnessTests.SubOperationWitness
-import SP1Clean.Extracted.WitnessVectors.SubOperation
-import SP1Clean.Proofs.WitnessTests.SubwOperationWitness
-import SP1Clean.Extracted.WitnessVectors.SubwOperation
-import SP1Clean.Proofs.WitnessTests.U16CompareOperationWitness
-import SP1Clean.Extracted.WitnessVectors.U16CompareOperation
-import SP1Clean.Proofs.WitnessTests.U16MSBOperationWitness
-import SP1Clean.Extracted.WitnessVectors.U16MSBOperation
-import SP1Clean.Proofs.WitnessTests.WitnessConformance
-import SP1Clean.Proofs.TraceGenTests.Conformance
-import SP1Clean.Proofs.TraceGenTests.EventPopulate
-import SP1Clean.Proofs.TraceGenTests.TraceGenerator
-import SP1Clean.Proofs.TraceGenTests.AddChipTraceVectors
-import SP1Clean.Proofs.TraceGenTests.AddChipTraceWitness
-import SP1Clean.Proofs.TraceGenTests.AddwChipTraceVectors
-import SP1Clean.Proofs.TraceGenTests.AddwChipTraceWitness
-import SP1Clean.Proofs.TraceGenTests.BitwiseChipTraceVectors
-import SP1Clean.Proofs.TraceGenTests.BitwiseChipTraceWitness
-import SP1Clean.Proofs.TraceGenTests.DivRemChipTraceVectors
-import SP1Clean.Proofs.TraceGenTests.DivRemChipTraceWitness
-import SP1Clean.Proofs.TraceGenTests.LtChipTraceVectors
-import SP1Clean.Proofs.TraceGenTests.LtChipTraceWitness
-import SP1Clean.Proofs.TraceGenTests.MulChipTraceVectors
-import SP1Clean.Proofs.TraceGenTests.MulChipTraceWitness
-import SP1Clean.Proofs.TraceGenTests.ShiftLeftChipTraceVectors
-import SP1Clean.Proofs.TraceGenTests.ShiftLeftChipTraceWitness
-import SP1Clean.Proofs.TraceGenTests.ShiftRightChipTraceVectors
-import SP1Clean.Proofs.TraceGenTests.ShiftRightChipTraceWitness
-import SP1Clean.Proofs.TraceGenTests.SubChipTraceVectors
-import SP1Clean.Proofs.TraceGenTests.SubChipTraceWitness
-import SP1Clean.Proofs.TraceGenTests.SubwChipTraceVectors
-import SP1Clean.Proofs.TraceGenTests.SubwChipTraceWitness

SP1Clean/Faithful/ALUTypeReader.lean

@@ -32,11 +32,6 @@ open scoped SP1Clean.ConstraintCoe
 
 variable {p : ℕ} [Fact p.Prime] [Fact (2 ^ 17 < p)]
 
-/-- `(16 : ZMod p).val = 16` under `Fact (2^17 < p)`. -/
-private lemma val_16' [NeZero p] : (16 : ZMod p).val = 16 := by
-  have : (131072 : ℕ) < p := by have := Fact.out (p := 2 ^ 17 < p); omega
-  exact ZMod.val_natCast_of_lt (show (16 : ℕ) < p by omega)
-
 set_option maxHeartbeats 4000000 in
 /-- **Faithfulness anchor (ALUTypeReader fragment).** Under `is_real = is_trusted = 1`, SP1's generated
 `ALUTypeReader` constraint list holds iff the combined spec holds. -/
@@ -69,9 +64,9 @@ theorem alutypereader_constraints_faithful
     Interaction.toProp_send_byte, Interaction.toProp_receive,
     Interaction.toProp_send_memory, Interaction.toProp_send_program,
     ByteOpcode.ofNat_six, ByteOpcode.ofNat_three, ByteOpcode.constrain_Range,
-    ByteOpcode.constrain_U8Range, val_16', ZMod.val_zero, one_ne_zero, ne_eq, not_false_eq_true,
+    ByteOpcode.constrain_U8Range, val_16_zmod_p, ZMod.val_zero, one_ne_zero, ne_eq, not_false_eq_true,
     true_implies, sub_self, mul_zero, sub_zero, zero_mul, Nat.ofNat_pos, true_and, and_true,
-    show (2 : ℕ) ^ 8 = 256 from by norm_num, show (2 : ℕ) ^ 16 = 65536 from by norm_num]
+    show (2 : ℕ) ^ 8 = 256 by norm_num, show (2 : ℕ) ^ 16 = 65536 by norm_num]
   tauto
 
 open SP1Clean.Channels (byteChannel memoryChannel MemoryMsg programChannel ProgramMsg)

SP1Clean/Faithful/AddrAddOperation.lean

@@ -7,6 +7,7 @@ import SP1Clean.Model.InteractionProjection
 import SP1Clean.Model.InteractionRecovery
 import SP1Clean.Faithful.ExtractedInteractionModel
 import SP1Clean.Extracted.AddrAddOperation
+import SP1Clean.Faithful.ChipTactics
 
 /-! # Faithfulness anchor to the SP1 (Rust-extraction) constraints (AddrAdd)
 
@@ -23,18 +24,6 @@ open scoped SP1Clean.ConstraintCoe
 
 variable {p : ℕ} [Fact p.Prime] [Fact (2 ^ 17 < p)]
 
-/-- `(16 : ZMod p).val = 16` under `Fact (2^17 < p)`. -/
-private lemma val_16 [NeZero p] : (16 : ZMod p).val = 16 := by
-  have : (131072 : ℕ) < p := by have := Fact.out (p := 2 ^ 17 < p); omega
-  exact ZMod.val_natCast_of_lt (show (16 : ℕ) < p by omega)
-
-omit [Fact (2 ^ 17 < p)] in
-/-- Carry-bool bridge: `x*(x-1)=0 ↔ x∈{0,1}` (field; `→` via `bool_of_mul_pred`). -/
-private lemma bool_iff {x : ZMod p} : x * (x - 1) = 0 ↔ (x = 0 ∨ x = 1) := by
-  rw [sub_eq_add_neg]
-  exact ⟨SP1Clean.bool_of_mul_pred,
-    fun h => by rcases h with h | h <;> rw [h] <;> ring⟩
-
 /-- **Faithfulness anchor.** SP1's `AddrAddOperation` constraint list holds iff the native gadget's
 `RawSpec` holds. -/
 theorem addrAdd_constraints_faithful (a b : Word (ZMod p))

SP1Clean/Faithful/AddressOperation.lean

@@ -3,6 +3,7 @@ import Mathlib.Data.ZMod.Basic
 import SP1Clean.Native.Operations.AddressOperation
 import SP1Clean.Model.SP1Constraint
 import SP1Clean.Extracted.AddressOperation
+import SP1Clean.Faithful.ChipTactics
 
 /-! # Faithfulness anchor to the SP1 (Rust-extraction) constraints (Address)
 
@@ -19,23 +20,6 @@ open scoped SP1Clean.ConstraintCoe
 
 variable {p : ℕ} [Fact p.Prime] [Fact (2 ^ 17 < p)]
 
-/-- `(16 : ZMod p).val = 16` under `Fact (2^17 < p)`. -/
-private lemma val_16 [NeZero p] : (16 : ZMod p).val = 16 := by
-  have : (131072 : ℕ) < p := by have := Fact.out (p := 2 ^ 17 < p); omega
-  exact ZMod.val_natCast_of_lt (show (16 : ℕ) < p by omega)
-
-/-- `(13 : ZMod p).val = 13` under `Fact (2^17 < p)`. -/
-private lemma val_13 [NeZero p] : (13 : ZMod p).val = 13 := by
-  have : (131072 : ℕ) < p := by have := Fact.out (p := 2 ^ 17 < p); omega
-  exact ZMod.val_natCast_of_lt (show (13 : ℕ) < p by omega)
-
-omit [Fact (2 ^ 17 < p)] in
-/-- Carry-bool bridge: `x*(x-1)=0 ↔ x∈{0,1}` (field; `→` via `bool_of_mul_pred`). -/
-private lemma bool_iff {x : ZMod p} : x * (x - 1) = 0 ↔ (x = 0 ∨ x = 1) := by
-  rw [sub_eq_add_neg]
-  exact ⟨SP1Clean.bool_of_mul_pred,
-    fun h => by rcases h with h | h <;> rw [h] <;> ring⟩
-
 set_option maxHeartbeats 4000000 in
 /-- **Faithfulness anchor.** SP1's `AddressOperation` constraint lists (`asserts` + `interactions`)
 hold iff the native gadget's `RawSpec` holds. -/
@@ -52,7 +36,7 @@ theorem address_constraints_faithful (b cc : Word (ZMod p))
     List.Forall, List.cons_append, List.nil_append,
     Vector.getElem_mk, List.getElem_toArray, List.getElem_cons_zero, List.getElem_cons_succ,
     Interaction.toProp_send_byte, ByteOpcode.ofNat_six,
-    ByteOpcode.constrain_Range, val_16, val_13, one_ne_zero, ne_eq, not_false_eq_true, true_implies,
+    ByteOpcode.constrain_Range, val_16, val_13_zmod_p, one_ne_zero, ne_eq, not_false_eq_true, true_implies,
     SP1Clean.AddressOperation.RawSpec, SP1Clean.AddrAddOperation.RawSpec,
     one_mul, add_zero, sub_zero, sub_self, mul_zero, true_and, and_assoc, bool_iff,
     show (2 : ℕ) ^ 16 = 65536 from by norm_num]

SP1Clean/Faithful/Addw.lean

@@ -8,6 +8,7 @@ import SP1Clean.Model.InteractionRecovery
 import SP1Clean.Faithful.ExtractedInteractionModel
 import SP1Clean.Extracted.AddwOperation
 import SP1Clean.Faithful.U16MSBOperation
+import SP1Clean.Faithful.ChipTactics
 
 /-! # Faithfulness anchor — `AddwOperation` constraints ↔ native raw spec
 
@@ -25,18 +26,6 @@ open scoped SP1Clean.ConstraintCoe
 
 variable {p : ℕ} [Fact p.Prime] [Fact (2 ^ 17 < p)]
 
-/-- `(16 : ZMod p).val = 16` under `Fact (2^17 < p)`. -/
-private lemma val_16 [NeZero p] : (16 : ZMod p).val = 16 := by
-  have : (131072 : ℕ) < p := by have := Fact.out (p := 2 ^ 17 < p); omega
-  exact ZMod.val_natCast_of_lt (show (16 : ℕ) < p by omega)
-
-omit [Fact (2 ^ 17 < p)] in
-/-- Carry-bool bridge: `x*(x-1)=0 ↔ x∈{0,1}` (field; `→` via `bool_of_mul_pred`). -/
-private lemma bool_iff {x : ZMod p} : x * (x - 1) = 0 ↔ (x = 0 ∨ x = 1) := by
-  rw [sub_eq_add_neg]
-  exact ⟨SP1Clean.bool_of_mul_pred,
-    fun h => by rcases h with h | h <;> rw [h] <;> ring⟩
-
 set_option linter.unusedSimpArgs false in
 /-- **Faithfulness anchor.** SP1's composed `AddwOperation` constraint list holds iff the native
 gadget's combined raw spec (`U16MSBOperation.RawSpec` on the sign bit ∧ `AddwOperation.RawSpec` on

SP1Clean/Faithful/AddwChip.lean

@@ -236,7 +236,6 @@ theorem addwcols_memory_interactions_faithful_syntactic
     h_pl_b, h_pv_b0, h_pv_b1, h_pv_b2, h_pv_b3,
     h_pl_c, h_pv_c0, h_pv_c1, h_pv_c2, h_pv_c3, sub_eq_add_neg]
 
-
 set_option maxHeartbeats 4000000 in
 set_option linter.unusedSimpArgs false in
 /-- **Chip-level faithfulness anchor — Byte-bus interactions, SYNTACTIC (multi-fragment `Perm` + WITNESSED).**
@@ -307,7 +306,6 @@ theorem addwcols_byte_interactions_faithful_syntactic
   -- swap the first two blocks (the `ALUTypeReader 6` tail is shared).
   exact (List.perm_append_comm (l₁ := [_, _]) (l₂ := [_, _, _])).append_right [_, _, _, _, _, _]
 
-
 set_option maxHeartbeats 4000000 in
 /-- **Chip-level faithfulness anchor — COMBINED, SYNTACTIC.** The full faithfulness statement for `AddwChip`:
 the interactions the row emits on its four buses — `State`, `Byte`, `Memory`, `Program` — taken together

SP1Clean/Faithful/AluX0.lean

@@ -22,10 +22,6 @@ open scoped SP1Clean.ConstraintCoe
 
 variable {p : ℕ} [Fact p.Prime] [Fact (2 ^ 17 < p)]
 
-private lemma val_16'' [NeZero p] : (16 : ZMod p).val = 16 := by
-  have : (131072 : ℕ) < p := by have := Fact.out (p := 2 ^ 17 < p); omega
-  exact ZMod.val_natCast_of_lt (show (16 : ℕ) < p by omega)
-
 private lemma val_29'' [NeZero p] : (29 : ZMod p).val = 29 := by
   have : (131072 : ℕ) < p := by have := Fact.out (p := 2 ^ 17 < p); omega
   exact ZMod.val_natCast_of_lt (show (29 : ℕ) < p by omega)
@@ -76,7 +72,7 @@ theorem alux0cols_constraints_faithful (cols : Extracted.AluX0Cols (ZMod p))
     Interaction.toProp_send_memory, Interaction.toProp_send_program,
     ByteOpcode.ofNat_six, ByteOpcode.ofNat_three, ByteOpcode.ofNat_four,
     ByteOpcode.constrain_Range, ByteOpcode.constrain_U8Range, ByteOpcode.constrain_LTU,
-    val_16'', val_29'', ZMod.val_zero, ZMod.val_one, one_ne_zero, ne_eq, not_false_eq_true,
+    val_16_zmod_p, val_29'', ZMod.val_zero, ZMod.val_one, one_ne_zero, ne_eq, not_false_eq_true,
     true_implies, sub_self, mul_zero, sub_zero, zero_mul, one_mul, Nat.ofNat_pos, true_and, and_true,
     false_or, true_iff, show (1 : ℕ) < 256 from by norm_num, show (29 : ℕ) < 256 from by norm_num,
     show (2 : ℕ) ^ 8 = 256 from by norm_num, show (2 : ℕ) ^ 16 = 65536 from by norm_num]

SP1Clean/Faithful/BranchChip.lean

@@ -3,6 +3,7 @@ import Mathlib.Data.ZMod.Basic
 import SP1Clean.Proofs.Chips.BranchChip.Formal
 import SP1Clean.Model.SP1Constraint
 import SP1Clean.Extracted.BranchChip
+import SP1Clean.Faithful.ChipTactics
 
 /-! # Chip-level faithfulness anchor for BRANCH
 
@@ -25,16 +26,6 @@ open scoped SP1Clean.ConstraintCoe
 
 variable {p : ℕ} [Fact p.Prime] [Fact (2 ^ 17 < p)]
 
-/-- `(14 : ZMod p).val = 14` under `Fact (2^17 < p)` (for the `Range(next_pc[0]/4, 14)` send). -/
-private lemma val_14 [NeZero p] : (14 : ZMod p).val = 14 := by
-  have : (131072 : ℕ) < p := by have := Fact.out (p := 2 ^ 17 < p); omega
-  exact ZMod.val_natCast_of_lt (show (14 : ℕ) < p by omega)
-
-/-- `(16 : ZMod p).val = 16` under `Fact (2^17 < p)` (for the `next_pc[1]`/`next_pc[2]` u16 sends). -/
-private lemma val_16 [NeZero p] : (16 : ZMod p).val = 16 := by
-  have : (131072 : ℕ) < p := by have := Fact.out (p := 2 ^ 17 < p); omega
-  exact ZMod.val_natCast_of_lt (show (16 : ℕ) < p by omega)
-
 /-- The chip-local structural meaning of BRANCH's `asserts` inline tail (everything past the composed
 `CPUState`/`ITypeReaderImmutable`/`LtOperationSigned` sub-lists): the six opcode-flag booleans, the flag
 sum bound (`E16 = Σ is_b*` boolean), the `is_branching` boolean, the `is_real`-gated decision constraint
@@ -97,7 +88,7 @@ theorem branch_interactions_faithful (cols : BranchColumns (ZMod p)) :
   -- `Range(next_pc[0]/4, 14)`, u16 `next_pc[1]`, u16 `next_pc[2]`, each gated by the flag sum `E16`.
   simp only [Extracted.BranchColumns.interactions, List.forall_append, List.Forall,
     Interaction.toProp_send_byte, ByteOpcode.ofNat_six, ByteOpcode.constrain_Range,
-    val_14, val_16] at h
+    val_14_zmod_p, val_16] at h
   obtain ⟨-, h0, h1, h2⟩ := h
   simp only [branchInteractSpec]
   refine ⟨?_, ?_, ?_⟩