fv: machine-check all 104 chip determinism theorems in Lean

.github/workflows/ci.yml

@@ -28,7 +28,7 @@ jobs:
       - uses: actions/checkout@v5
       - uses: dtolnay/rust-toolchain@nightly
         with:
-          toolchain: nightly-2025-08-17
+          toolchain: nightly-2026-09-17
           components: rustfmt
       - run: cargo fmt --all -- --check
   clippy:
@@ -38,7 +38,7 @@ jobs:
       - uses: actions/checkout@v5
       - uses: dtolnay/rust-toolchain@nightly
         with:
-          toolchain: nightly-2025-08-17
+          toolchain: nightly-2026-09-17
       - run: curl --proto '=https' --tlsv1.2 -sSf https://raw.githubusercontent.com/ProjectZKM/toolchain/refs/heads/main/setup.sh | sh
       - run: source ~/.zkm-toolchain/env && cd crates/test-artifacts && cargo build && cd ../..
       - name: Install Dependencies

.gitignore

@@ -59,3 +59,11 @@ docs/paper/sections/old/
 
 # Soundness working notes stay local; they are not release material.
 docs/soundness/
+
+# Lean chip determinism files are generated (crates/fv/lean4/check/regen_all.sh), not committed
+crates/fv/lean4/ZirenDet/Chips/
+crates/fv/lean4/ZirenDet/Chips.lean
+__pycache__/
+picus_out/
+crates/fv/lean4/snippets/tools/
+crates/fv/lean4/check/

crates/core/machine/src/lib.rs

@@ -1,3 +1,4 @@
+#![recursion_limit = "256"]
 #![allow(
     clippy::new_without_default,
     clippy::field_reassign_with_default,

crates/core/machine/src/operations/global_accumulation.rs

@@ -199,6 +199,21 @@ impl<F: Field, const N: usize> GlobalAccumulationOperation<F, N> {
                 sum_checker_y,
                 SepticExtension::<AB::Expr>::from_base_fn(|_| AB::Expr::ZERO),
             );
+            builder.mark_gadget("septic_add", || {
+                let current =
+                    if i == 0 { initial_digest.clone() } else { ith_cumulative_sum(i - 1) };
+                let coords = |p: SepticCurve<AB::Expr>| -> Vec<AB::Expr> {
+                    p.x.0.into_iter().chain(p.y.0).collect()
+                };
+                (
+                    local_is_real[i].into(),
+                    vec![
+                        coords(ith_cumulative_sum(i)),
+                        coords(current),
+                        coords(ith_point_to_add(i)),
+                    ],
+                )
+            });
 
             let denominator = ith_point_to_add(i).x - current_sum.x.clone();
             let denominator_inv = SepticExtension::<AB::Expr>::from_base_fn(|j| {

crates/core/machine/src/operations/global_lookup.rs

@@ -189,6 +189,17 @@ impl<F: Field> GlobalLookupOperation<F> {
             + cols.y6_mid8 * AB::F::from_u32(1 << 16)
             + cols.y6_top * AB::F::from_u32(1 << 24);
 
+        builder.mark_gadget("septic_lift", || {
+            (
+                is_real.into(),
+                vec![
+                    (0..7).map(|i| cols.y_coordinate[i].into()).collect(),
+                    (0..7).map(|i| cols.x_coordinate[i].into()).collect(),
+                    vec![is_receive.clone(), is_send.clone()],
+                ],
+            )
+        });
+
         builder.when(is_receive).assert_eq(y.0[6].clone(), AB::Expr::ONE + y6_value.clone());
         builder.when(is_send).assert_eq(y.0[6].clone(), AB::Expr::from_u32(SEND_Y6_MIN) + y6_value);
     }

crates/core/machine/src/syscall/precompiles/sys_linux/air.rs

@@ -424,6 +424,16 @@ impl SysLinuxChip {
         builder.when(is_write).assert_word_zero(*local.output.value());
     }
 
+    /// A Linux syscall none of the decoders recognizes is a no-op: `eval` sets
+    /// `is_nop = is_real − (is_mmap + is_clone + is_exit_group + is_brk + is_fnctl + is_read +
+    /// is_write)`, so every other syscall number, and not only the no-op handlers the executor
+    /// registers, is accepted here with a zero result and a zero output word.
+    ///
+    /// This is wider than the executor, which returns `ExecutionError::UnsupportedSyscall` for a
+    /// number it has no handler for, so an honest trace never contains such a row.  A proof with
+    /// one proves only that the syscall returned 0 and wrote nothing, which is the no-op
+    /// semantics, so the statement stays sound; pinning the accepted numbers to the executor's
+    /// set would make the chip reject what the executor rejects.
     fn eval_nop<AB: ZKMAirBuilder>(
         &self,
         builder: &mut AB,

crates/curves/src/lib.rs

@@ -1,3 +1,5 @@
+#![recursion_limit = "256"]
+
 pub mod edwards;
 pub mod params;
 // pub mod polynomial;

crates/fv/lean4/README.md

@@ -38,11 +38,12 @@ program fetch and a previous memory value are *sends* on the bus but *inputs* to
 | `ZirenDet/Lib.lean` | hand-written | The field `F = ZMod (2^31 - 2^24 + 1)`, the lifting lemmas from `F` to bounded integers, and the `picus_det` tactic. |
 | `ZirenDet/Safe.lean` | hand-written | `picus_safe`, a wrapper that catches any runtime failure of the automation and admits the goal, so a generated file always elaborates. |
 | `ZirenDet/Basic.lean` | generated | The prelude every generated chip file imports. |
-| `ZirenDet/Chips/*.lean` | generated (64 files) | One file per chip; inside, one *module* per opcode selector, each with its determinism theorem. |
+| `ZirenDet/Chips/*.lean` | generated, not committed (62 files, `check/regen_all.sh`) | One file per chip; inside, one *module* per opcode selector, each with its determinism theorem. |
+| `ZirenDet/Chips.lean` | generated, not committed | Imports every generated chip file and the bridges built on them. |
 | `ZirenDet/Isa.lean` | hand-written | Executable MIPS32r2 semantics: `decode`, `step`, `run`. Little-endian, delay slots, `$zero` sink, separate `HI`/`LO`. |
 | `ZirenDet/IsaVectors.lean` | generated | 770 specification vectors replayed through `Isa.run`, each `by native_decide`. |
 | `ZirenDet/IsaDecode.lean` | generated | 2275 decodings of real instruction words checked against the emulator's decoder output. |
-| `ZirenDet/Bridge/*.lean` | hand-written | The *functional* direction: this chip computes *that* ISA function. One worked example (`AddSub`), still open. |
+| `ZirenDet/Bridge/*.lean` | hand-written | The *functional* direction: this chip computes *that* ISA function. One worked example (`AddSub`), still open; it builds against the generated chip files. |
 
 ## What a generated theorem looks like
 
@@ -87,33 +88,34 @@ every theorem into a `sorry`, so check the count after changing it.
 
 ## Building
 
-**Builds run on the GPU box, never on the dev host.** Mathlib plus 64 generated files is tens
-of gigabytes of elaboration; individual chip files have peaked above 200 GB of resident
-memory, so run them where there is room and watch the machine.
+**Build on a machine with plenty of memory, not a laptop.** Mathlib plus the generated chip files
+is tens of gigabytes of elaboration, and a large chip file built as one module has peaked above
+200 GB of resident memory. Build the library with `lake`, and check chip files with
+`check/check.sh`, which splits each into modules built in parallel under a memory gate
+(`check/README.md`).
 
 ```bash
-# from the repo root
-rsync -a --exclude .lake crates/fv/lean4/ ant-5090-2:/mnt_zkm/stephen/lean4/
-
-ssh ant-5090-2 'export ELAN_HOME=/mnt_zkm/stephen/.elan \
-                       PATH=/mnt_zkm/stephen/.elan/bin:$PATH \
-                       XDG_CACHE_HOME=/mnt_zkm/stephen/.cache
-                cd /mnt_zkm/stephen/lean4 && lake build 2>&1 | tee build.log'
+cd crates/fv/lean4
+lake build                      # ZirenDet: the library and the gadget proofs
 ```
 
-`ELAN_HOME` and `XDG_CACHE_HOME` matter: a non-interactive shell has no toolchain on its
-`PATH`, and without them `lake` re-downloads the toolchain onto the box's nearly full root
-filesystem.
+Point `ELAN_HOME` and `XDG_CACHE_HOME` at a disk with room when the home filesystem is small, and
+put `$ELAN_HOME/bin` on `PATH` in non-interactive shells, or `lake` cannot find or re-downloads
+the toolchain.
 
-To work on one chip, build its module alone — the files are independent:
+The `check/` scripts are not yet in the repository; until they are, take them from the archived
+snapshot of the checked files (`src/crates/fv/lean4/check`). The chip files are generated, not committed. `check/regen_all.sh OUT` writes all of them, with
+their gadget snippets, under `OUT`; `zkm-picus --chip NAME --format lean --derive --lean-out-dir
+crates/fv/lean4` writes one into this project. To work on one chip, build its module alone (the
+files are independent), or check a large one in parallel with `check/check.sh`:
 
 ```bash
 lake build ZirenDet.Chips.AddSub
 ```
 
 Kill a runaway file by explicit PID (`ps -o pid,rss,args -C lean --sort=-rss`). Never
-`pkill -f lean` on the box: the pattern matches the ssh session running it, and it will take
-down the other files with it.
+`pkill -f lean`: the pattern can match the shell that launched the build and take down the
+other files with it.
 
 ## Reading the result
 

crates/fv/lean4/ZirenDet.lean

@@ -1,67 +1,18 @@
 import ZirenDet.Basic
-import ZirenDet.Chips.AddSub
-import ZirenDet.Chips.AddSubImm
-import ZirenDet.Chips.Bitwise
-import ZirenDet.Chips.BitwiseImm
-import ZirenDet.Chips.Bls12381AddAssign
-import ZirenDet.Chips.Bls12381Decompress
-import ZirenDet.Chips.Bls12381DoubleAssign
-import ZirenDet.Chips.Bls12381FpOpAssign
-import ZirenDet.Chips.Bls12831Fp2AddSubAssign
-import ZirenDet.Chips.Bls12831Fp2MulAssign
-import ZirenDet.Chips.Bn254AddAssign
-import ZirenDet.Chips.Bn254DoubleAssign
-import ZirenDet.Chips.Bn254Fp2AddSubAssign
-import ZirenDet.Chips.Bn254Fp2MulAssign
-import ZirenDet.Chips.Bn254FpOpAssign
-import ZirenDet.Chips.Branch
-import ZirenDet.Chips.Byte
-import ZirenDet.Chips.CloClz
-import ZirenDet.Chips.DivRem
-import ZirenDet.Chips.EdAddAssign
-import ZirenDet.Chips.EdDecompress
-import ZirenDet.Chips.Global
-import ZirenDet.Chips.Jump
-import ZirenDet.Chips.KeccakSponge
-import ZirenDet.Chips.KeccakSpongeControl
-import ZirenDet.Chips.LoadNarrow
-import ZirenDet.Chips.LoadWord
-import ZirenDet.Chips.Lt
-import ZirenDet.Chips.LtImm
-import ZirenDet.Chips.MemoryBump
-import ZirenDet.Chips.MemoryGlobalFinalize
-import ZirenDet.Chips.MemoryGlobalInit
-import ZirenDet.Chips.MemoryLocal
-import ZirenDet.Chips.MemoryUnaligned
-import ZirenDet.Chips.MiscInstrs
-import ZirenDet.Chips.MovCond
-import ZirenDet.Chips.Mul
-import ZirenDet.Chips.Poseidon2Permute
-import ZirenDet.Chips.Program
-import ZirenDet.Chips.Range
-import ZirenDet.Chips.Secp256k1AddAssign
-import ZirenDet.Chips.Secp256k1Decompress
-import ZirenDet.Chips.Secp256k1DoubleAssign
-import ZirenDet.Chips.Secp256r1AddAssign
-import ZirenDet.Chips.Secp256r1Decompress
-import ZirenDet.Chips.Secp256r1DoubleAssign
-import ZirenDet.Chips.ShaCompress
-import ZirenDet.Chips.ShaCompressControl
-import ZirenDet.Chips.ShaExtend
-import ZirenDet.Chips.ShaExtendControl
-import ZirenDet.Chips.ShiftLeft
-import ZirenDet.Chips.ShiftLeftImm
-import ZirenDet.Chips.ShiftRight
-import ZirenDet.Chips.ShiftRightImm
-import ZirenDet.Chips.StoreNarrow
-import ZirenDet.Chips.StoreWord
-import ZirenDet.Chips.SysLinux
-import ZirenDet.Chips.SyscallCore
-import ZirenDet.Chips.SyscallInstrs
-import ZirenDet.Chips.SyscallPrecompile
-import ZirenDet.Chips.U256XU2048Mul
-import ZirenDet.Chips.Uint256MulMod
 import ZirenDet.Isa
 import ZirenDet.IsaVectors
 import ZirenDet.IsaDecode
-import ZirenDet.Bridge.AddSub
+import ZirenDet.Gadgets
+import ZirenDet.Replay
+import ZirenDet.LeadingOne
+import ZirenDet.DivRem
+import ZirenDet.CanonicalWord
+import ZirenDet.FieldOp
+import ZirenDet.Pratt
+import ZirenDet.Primes
+import ZirenDet.Edwards
+import ZirenDet.Keccak
+import ZirenDet.OneHot
+import ZirenDet.GtBytes
+import ZirenDet.Septic
+import ZirenDet.GadgetProofs