feat: Clean DSL + Simplified per-chip RISCV spec + Generic field + Trace Theorms + Partial Honest Witness Gen

.gitignore

@@ -1,6 +1,7 @@
-/.lake
-/.claude
-.env
-.env.fish
+build/*
+build.log
+scratch/
 
-.DS_Store
+.lake/*
+.claude/*
+__pycache__/

.mcp.json

@@ -1,19 +1,5 @@
 {
   "mcpServers": {
-    "LeanExplore": {
-      "type": "stdio",
-      "command": "uvx",
-      "args": [
-        "--from",
-        "lean-explore",
-        "leanexplore",
-        "mcp",
-        "serve",
-        "--backend",
-        "local"
-      ],
-      "env": {}
-    },
     "lean-lsp": {
       "type": "stdio",
       "command": "uvx",
@@ -23,4 +9,4 @@
       "env": {}
     }
   }
-}
+}

CLAUDE.md

@@ -0,0 +1 @@
+See @AGENTS.md

LICENSE-MIT

@@ -1,6 +1,6 @@
 The MIT License (MIT)
 
-Copyright (c) 2025 Succinct Labs
+Copyright (c) 2023 Succinct Labs
 
 Permission is hereby granted, free of charge, to any person obtaining a copy
 of this software and associated documentation files (the "Software"), to deal

README.md

@@ -8,93 +8,157 @@ Formal verification of SP1 Hypercube zkVM arithmetization
 
 ## Overview
 
-This repository provides formal specifications and proofs for the arithmetization of the SP1 Hypercube zkVM using the Lean 4 theorem prover, we formally verify that the constraint systems used in SP1's AIR (Algebraic Intermediate Representation) in addition to constraints implied by the lookup argument, correctly implement the RISC-V ISA semantics.
-
-## Repository Structure
-
-The codebase is organized into three main libraries:
-
-### SP1Foundations
-Foundational definitions and utilities used throughout the verification:
-- **Field arithmetic**: Finite field operations over the KoalaBear field
-- **BitVec operations**: Bit vector manipulation and properties
-- **Constraints**: Framework for defining and reasoning about AIR constraints
-- **Register model**: RISC-V register state and operations
-- **SailM monad**: Integration with RISC-V formal semantics from Sail
-- **Memory model**: Memory consistency and checking infrastructure
-
-### SP1Operations
-Definitions of RISC-V instruction operations and their constraint encodings:
-- **Readers**: Instruction decoding for different RISC-V types (R-type, I-type, J-type, etc.)
-- **Operations**: Constraint definitions for individual operations (add, mul, shift, etc.)
-- **CPU state management**: Program counter and state transitions
-
-### SP1Chips
-Formal correctness proofs for individual instruction chips:
-- **Arithmetic**: Add, Sub, Mul, DivRem, Addw, Subw
-- **Logical**: Bitwise operations (AND, OR, XOR)
-- **Comparison**: Lt (less than) operations
-- **Shifts**: ShiftLeft, ShiftRight
-- **Memory**: Load/Store operations (byte, half, word, double)
-- **Control flow**: Jal, Jalr, Branch instructions
-- **Immediate**: Addi, UType instructions
-
-Each chip contains:
-- Constraint definitions that encode the operation
-- A `spec_*` function defining the RISC-V semantics
-- An `sp1_*` function defining the SP1 operation
-- A `correct_*` theorem proving equivalence
-
-## How It Works
-
-For each RISC-V instruction, we prove that:
-
-1. **The constraints are satisfiable**: When the instruction executes correctly, there exists an assignment to the constraint variables
-2. **The constraints are sound**: Any satisfying assignment corresponds to a valid RISC-V execution.
-
-The proofs connect two representations:
-- **RISC-V Semantics**: Formal specification from the Sail RISC-V model
-- **SP1 Constraints**: Polynomial constraints used in the SP1 zkVM
-
-Example from `AddChip.lean`:
-```lean
-theorem correct_add
-  (Main : Vector (Fin KB) 34)
-  (s : SailState)
-  (cstrs : (constraints Main).allHold)
-  (h_is_real : Main[33] = 1)
-  (state_cstrs : (constraints Main).initialState s) :
-  let op_c := sp1_op_c Main
-  let op_b := sp1_op_b Main
-  let op_a := sp1_op_a Main
-  (spec_add (.Regidx op_c) (.Regidx op_b) (.Regidx op_a)).run s = (sp1_add Main).run s
-```
-
-This theorem states that when all constraints hold, the SP1 add operation produces the same result as the RISC-V specification.
-
-## Constraints
-Constraints come from two sources:
-- Constraints implied by the lookup argument.
-- Constraints implied by the equations.
+A formal verification, in **Lean 4**, of the RISC-V chips in
+[SP1](https://github.com/succinctlabs/sp1) — Succinct's zkVM.
+
+SP1 proves the correct execution of a RISC-V program by encoding each instruction as rows of arithmetic
+constraints across a family of *chips* (one per operation: add, sub, bitwise, comparison, …). Those
+constraints are written in Rust. This project takes the constraints SP1's chips actually enforce and
+proves, in Lean, that satisfying them forces the row to compute the right RISC-V result.
+
+The circuits themselves are expressed in the [Clean](https://github.com/Verified-zkEVM/clean) zk-circuit
+DSL, and the reference for what each instruction *should* do is the official
+[Sail](https://github.com/riscv/sail-riscv) model of the RISC-V ISA. So a finished proof connects three
+things: SP1's Rust constraints, the Clean circuit, and the RISC-V ISA.
+
+### What is proven
+
+- **Soundness** — if a chip's row satisfies its constraints, the row computes the result the RISC-V ISA
+  specifies for that instruction (proved against the Sail model). Every soundness theorem is
+  *axiom-clean* — `#print axioms` shows only Lean's standard axioms, no `sorry`.
+- **Completeness** — because the circuits carry explicit witnesses, we also prove that every correct
+  input is accepted (no spurious constraint rejects a valid row).
+- **Faithfulness** — the constraints the Lean proof reasons about are *exactly* the constraints SP1's Rust
+  code emits, so the proof can't be vacuously about a different circuit.
+
+### What is assumed / out of scope
+
+- The Sail model is taken as the ground-truth definition of RISC-V.
+- The Clean DSL and the Lean toolchain are trusted.
+- **Soundness is `sorry`-free.** A handful of *completeness* proofs are still deferred skeletons
+  (currently five: Mul, ShiftLeft, ShiftRight and DivRem chips, plus one prerequisite premise in the
+  gated-VM capstone). These are liveness gaps — they say "this valid row is accepted", not "this row is
+  correct" — so they never weaken a soundness claim. See [`docs/release-audit.md`](docs/release-audit.md)
+  for the exact inventory and [`docs/roadmap.md`](docs/roadmap.md) for the plan to close them.
+- This is a per-chip, per-row result plus a trace-level composition layer; it is not yet an end-to-end
+  proof of the whole zkVM.
+
+## Code Structure
+
+All Lean sources live under `SP1Clean/`, with a mirror-of-SP1 layout. The root index
+`SP1Clean.lean` wires up every module's import.
+
+### `FormalModel/Contracts/`
+The input structs and specifications, stated against the RV64 ISA functions — what each reader, operation,
+and chip is expected to compute.
+- `Contracts/Readers.lean` — reader-circuit specs (CPU state, R-type reader, register-access columns/timestamps).
+- `Contracts/Operations.lean` — operation-level specs.
+- `Contracts/Chips.lean` — chip-row `Inputs` + semantic `Spec`s; `Contracts/ChipAssumptions.lean` adds the ALU chips' `Assumptions`/`ProverAssumptions`.
+- `Trace/GuestProgram.lean` — the guest-program execution model (`GuestProgram`, `IsInitialState`, `SailChain`, `SP1Halted`).
+
+### `Math/`
+General math with no SP1/Sail dependencies (the upstreaming candidate). Everything works over a prime field.
+- `Word.lean` — a `Word` as four little-endian 16-bit limbs, plus reassembly into a 64-bit value.
+- `Bitwise.lean` — byte-level AND/OR/XOR.
+- `MulCarryChain.lean` — multiplication carry-chain utilities.
+- `HWord.lean`, `GetElemFastPath.lean`, `Misc.lean` — half-word lemmas, a vector-access shim, misc lemmas.
+
+### `Model/`
+The SP1 substrate — Sail wrappers and the lookup-bus model.
+- `Register.lean`, `SailWrap.lean`, `SailMemory.lean` — register state, Sail monad wrappers, and the Sail memory model.
+- `Channels.lean`, `ChipAir.lean`, `InteractionBus.lean`, `InteractionProjection.lean`,
+  `InteractionRecovery.lean` — the model of the lookup buses chips use to talk to each other.
+- `ByteTable.lean` — the static byte-lookup table (SP1's preprocessed `ByteChip`).
+- `SP1Constraint.lean` — shared SP1 opcode datatypes (`ByteOpcode`, `Opcode`).
+
+### `Native/Operations/` + `Proofs/Operations/`
+The Clean circuit gadgets, one per operation (Add, Addw, Sub, Subw, Mul, Bitwise, BitwiseU16, Lt, U16Compare,
+U16MSB, U16toU8, IsZero(Word), IsEqualWord, Address, AddrAdd), each proved to compute the right 64-bit result.
+A structured op `<Op>/` is split across pillars: the witness + native arithmetic core
+(`Native/Operations/<Op>/{Populate,RawSpec}.lean`), the `FormalAssertion` proof
+(`Proofs/Operations/<Op>/Formal.lean`), and the auto-generated `eval` circuit (`Extracted/Circuit/<Op>.lean`).
+Single-file (flat) ops live in `Native/Operations/`.
+
+### `Native/Readers/`
+Register-adapter reader circuits that validate register reads/writes and instruction fetches per row:
+`CPUState.lean`, `RTypeReader.lean`, `ALUTypeReader.lean`, `RegisterAccessCols.lean`,
+`RegisterAccessTimestamp.lean`.
+
+### `Native/Chips/` + `Proofs/Chips/`
+The chips: each composes the reader circuits, an operation gadget, and an `is_real` selector. A chip
+`<Op>Chip/` is split across pillars — the `main` circuit (`Native/Chips/<Op>Chip/Defs.lean`) and the
+soundness/completeness proofs + Sail bridge (`Proofs/Chips/<Op>Chip/{Formal,Bridge}.lean`); the `Spec` lives
+in `FormalModel/Contracts/Chips.lean`. The ALU, control-flow, and memory chips are all here —
+Add/Addi/Addw/Sub/Subw, Bitwise, Lt, Mul, DivRem, ShiftLeft/ShiftRight, AluX0, Branch, Jal/Jalr, UType, and
+the Load*/Store*/LoadX0 memory chips — alongside the flat receiver-infra files `Proofs/Chips/ByteChip.lean`,
+`ProgramChip.lean`, and `MemoryProvider.lean`. (The 3 entangled complex chips DivRem/ShiftLeft/ShiftRight
+keep their `Defs` in `Proofs/Chips/` too.) Soundness is proved and `sorry`-free throughout; a few
+completeness proofs are still deferred skeletons.
+
+### `Faithful/`
+The faithfulness layer: proofs that the constraints used in the chip proofs are exactly those SP1 emits,
+plus witness-conformance checks (`*Witness.lean`) that the Lean witness matches SP1's `populate`. Shared
+scaffolding in `ChipTactics.lean` and `WitnessConformance.lean`.
+
+### `Extracted/`
+A copy of SP1's constraints, mechanically extracted from the Rust via `sp1-constraint-compiler`. The
+hand-written `ExtractionDSL.lean` defines the vocabulary these read in (a list of assertions plus lookup
+interactions); the rest are the per-chip/op constraint lists, reader columns, and witness vectors.
+
+### `Soundness/`
+Trace-level consistency properties and the whole-machine capstone.
+- `ChipRow.lean` — the `ChipKind` structure-of-functions each chip registers.
+- `StateConsistency.lean` (PC chain), `MemoryConsistency.lean`, `ByteConsistency.lean`,
+  `ProgramConsistency.lean` — per-bus consistency.
+- `Opcode.lean` + `Coverage.lean` — the auditable `Opcode → chip → Sail` routing table (mirroring SP1's
+  `RiscvAir`); `InstructionTrace.lean` maps an instruction sequence to a `ChipRow` sequence;
+  `Completeness.lean` is the partial whole-VM-completeness layer.
+- `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.
+
+## How a proof connects to SP1
+
+Each operation is verified through a short chain of artifacts that together link SP1's Rust, the Clean
+circuit, and the RISC-V ISA:
+
+1. **Gadget** (`Native/Operations/<Op>/` + `Proofs/Operations/<Op>/Formal.lean`) — the Clean circuit for the
+   operation, with a spec describing the result it computes on 64-bit words.
+2. **Chip** (`Native/Chips/<Op>Chip/Defs.lean` + `Proofs/Chips/<Op>Chip/Formal.lean`) — composes the gadget
+   with the register/instruction *readers* and an `is_real` selector, matching the shape of one of SP1's chips.
+3. **Sail bridge** (`Proofs/Chips/<Op>Chip/Bridge.lean`) — proves the chip's result matches the RISC-V ISA, as
+   defined by the Sail model.
+4. **Faithfulness anchor** (`Faithful/<Op>.lean`) — proves the constraints used above are exactly those SP1
+   emits, drawn from a Rust-extracted copy of SP1's constraints under `Extracted/`.
+
+Beyond a single row, chips talk to each other through lookup buses (registers, memory, the program ROM, a
+byte table). These are modeled as a multiplicity-weighted interaction bus, with per-bus consistency lemmas
+composed into a whole-trace result. See [`docs/bus-model.md`](docs/bus-model.md) for that layer.
 
 ## Building
 
-### Prerequisites
-- [Lean 4](https://github.com/leanprover/lean4) (v4.23.0-rc2)
-- [Lake](https://github.com/leanprover/lake) (Lean's build tool)
-
-### Build Instructions
-
 ```bash
-# Clone the repository
-git clone https://github.com/succinctlabs/sp1-lean
-cd sp1-lean
-
-# Build the project
-lake build
+# Build everything (the default target)
+lake build SP1Clean
 ```
 
-## Dependencies
+## Toolchain & Dependencies
+
+All dependencies are fetched from public Git repositories by `lake build` — there is nothing to check out
+by hand. They are pinned, and you should **not bump them**:
+
+| Dependency | Version / source |
+|------------|------------------|
+| Lean       | `leanprover/lean4:v4.28.0` (`lean-toolchain`) |
+| mathlib    | `github.com/leanprover-community/mathlib4 @ v4.28.0` |
+| Clean      | `github.com/Verified-zkEVM/clean @ main` |
+| `LeanRV64D` (Sail RV64 model) | `github.com/succinctlabs/sail-riscv-lean @ dtumad/clean-native` |
+| `RISCV` (lightweight RV64 ISA fns) | `github.com/succinctlabs/riscv-lean @ dtumad/clean-native` |
+| `Sail` (runtime) | `github.com/rems-project/lean-sail @ v4` (pulled in transitively) |
 
-- **[Mathlib](https://github.com/leanprover-community/mathlib4)**: Lean's mathematics library (v4.23.0-rc2)
-- **[Lean_RV64D](https://github.com/succinctlabs/sail-riscv-lean)**: Formal RISC-V semantics extracted from Sail
+The two `succinctlabs/*` Sail dependencies are pinned to the `dtumad/clean-native` branch and each carries a
+4.28 `lean-toolchain`; this is what keeps the project from being bumped to 4.29.