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

[dtumad]

Overview

This branch rebuilds SP1's RISC-V chip verification from the ground up. The previous version restated each chip's constraints structurally and proved facts about them under a toProp mapping. This version is Clean-native and semantically specified: every chip is a real circuit in the public Clean DSL, its arithmetic is re-derived in-project and proven faithful to SP1, and each chip is connected directly to the official RISC-V Sail specification.

The old SP1Foundations / SP1Operations / SP1Chips libraries are removed and replaced by a new SP1Clean/ tree.

Main changes

• Built on the Clean DSL. Chips are composed from true Clean sub-circuits (gadgets + register readers) rather than inlined constraint lists. Each operation exposes one circuit and one semantic spec (what the row means, e.g. a 64-bit add identity), not a restatement of the constraint syntax.

• Anchored to the RISC-V Sail spec. Each chip carries a small "Sail bridge" proving that a real chip row reaches the official RISC-V ISA semantics (correct_<op>_native). These now depend only on the chip's own native arithmetic — no borrowed proofs.

• Models interactions much more SP1 faithfully. Beyond the arithmetic, the work anchors SP1's actual emitted constraints (extracted from the Rust source) to the Lean circuits, and adds a whole-trace layer: the four interaction buses (state, byte, program, memory) with per-bus consistency/balance theorems, so interactions no longer add anything to the trust base (aside from explicit assumptions about multiplicity balance).

• New ALUX0 chip. Adds AluX0Chip, covering ALU-family instructions whose destination is x0 (result discarded). It validates the program/register accesses without computing the ALU result, using an immediate-capable reader.

• Field-generic + honest witness generation. All circuits are generic over a prime field. A new witness-conformance layer pairs auto-generated vectors (dumped from SP1's real populate) with native_decide anchors, so the Lean model is checked against SP1's actual witness generation. This ensures conformance but is not actually a proof that witness generation is implemented faithfully.

• Toolchain / dependencies. Moves to Lean 4.28 with mathlib v4.28, adds the public Clean DSL, and pulls the RISC-V Sail model (LeanRV64D) and ISA functions (RISCV). Constraint extraction moves from update_constraints.py to update_extracted.py.

SP1Clean/ layout

• Extracted/ — constraint data generated from the SP1 Rust source
• Foundations/ — re-created core primitives: 64-bit Word (four 16-bit limbs), bitwise/byte helpers, registers, bus Channel definitions, and the Sail wrappers.
• Specs/ — consolidated input structs and semantic specs, with chip specs stated via the RV64 ISA functions.
• Chips/ — the per-row circuits (one directory per chip): ALU (Add/Sub/Addw/Subw/Bitwise/Lt), shifts, Addi, Mul, DivRem, AluX0, U-type, control flow (Jal/Jalr/Branch), and the full load/store family — each composing readers + gadgets and (where present) its Sail bridge. Each has a Defs.lean with basic setup, a Formal.lean with the final circuit proof (as a GeneralFormalCircuit), and Bridge.lean then connects this further to monadic sail.
• Operations/ — the witnessed operation gadgets (Add, Sub, Addw, Subw, Bitwise, Lt, Mul, compare/zero ops, address ops) with native arithmetic and semantic specs. Proven correct relative to their specs as FormalAssertions with populate functions that are called by the actual chips.
• Readers/ — register/PC adapters that emit row interactions to the buses (CPUState, R/I/J-type readers, memory-access columns, timestamps).
• Faithful/ — anchors proving SP1's extracted Rust constraint lists match the Lean gadget specs (asserts + bus interactions).
• WitnessTests/ — the witness-generation conformance layer (generated vectors + native_decide anchor unit tests). Note this has no coverage for chips.
• Soundness/ — the whole-machine layer: per-bus consistency, the chip registry, the gated execution capstone, and the instruction-coverage/routing table.

Scope

Soundness is the primary target and is axiom-clean (only propext, Classical.choice, Quot.sound). Completeness some chips still contain sorry, but this was not verified even partially in the old formulation. Some of the assumptions for completeness are also overly strong, and should eventually be relaxed to prove honest completeness.
The trace level multiplicity argument also still contains a sorry, but again this was never verified even partially before.

Docs

New docs/ (architecture, bus model, proof patterns, porting recipe, release audit, roadmap) describe the four-artifact chain and what's deferred.

Basic Example

Each chip is structured something similar to below, across a Specs/Chip.lean+Chips/<Chip>/Defs.lean+Chips/<Chip>/Formal.lean:

structure Extracted.MulCols (F : Type) where
  state : (CPUState F)
  adapter : (RTypeReader F)
  a : (Word F)
  mul_operation : (MulOperation F)
  is_mul : F
  is_mulh : F
  is_mulhu : F
  is_mulhsu : F
  is_mulw : F
deriving ProvableStruct

structure MulChip.Inputs (F : Type) where
  is_real : F
  state : Extracted.CPUState F
  adapter : Extracted.RTypeReader F
deriving ProvableStruct

@[reducible] def Inputs.op_b_val {F} (i : Inputs F) : Word F := i.adapter.op_b_memory.prev_value
@[reducible] def Inputs.op_c_val {F} (i : Inputs F) : Word F := i.adapter.op_c_memory.prev_value

def Spec (input : Inputs (ZMod p)) (cols : MulCols (ZMod p)) (_ : ProverData (ZMod p)) : Prop :=
  input.is_real = 1 →
    (cols.is_mul = 1 → Word.toBitVec64 cols.a = RV64.mul (Word.toBitVec64 input.op_c_val) (Word.toBitVec64 input.op_b_val)) ∧
    (cols.is_mulh = 1 → Word.toBitVec64 cols.a = RV64.mulh (Word.toBitVec64 input.op_c_val) (Word.toBitVec64 input.op_b_val)) ∧
    (cols.is_mulhu = 1 → Word.toBitVec64 cols.a = RV64.mulhu (Word.toBitVec64 input.op_c_val) (Word.toBitVec64 input.op_b_val)) ∧
    (cols.is_mulhsu = 1 → Word.toBitVec64 cols.a = RV64.mulhsu (Word.toBitVec64 input.op_c_val) (Word.toBitVec64 input.op_b_val)) ∧
    (cols.is_mulw = 1 → Word.toBitVec64 cols.a = RV64.mulw (Word.toBitVec64 input.op_c_val) (Word.toBitVec64 input.op_b_val))
∧... -- readers/cpu/is_binary etc. for chips w/ completeness proofs

def MulChip.main (input : Var Inputs (ZMod p)) : Circuit (ZMod p) (Var MulCols (ZMod p)) := do
  let cols ← ProvableType.witness (fun env =>
    MulOperation.populate
      #v[env input.op_b_val[0], env input.op_b_val[1], env input.op_b_val[2], env input.op_b_val[3]]
      #v[env input.op_c_val[0], env input.op_c_val[1], env input.op_c_val[2], env input.op_c_val[3]]
      (env is_mulh) (env is_mulhsu) (env is_mulw))
  assertion MulOperation.circuit
    ⟨input.op_b_val, input.op_c_val, cols, is_mul + is_mulh + is_mulhu + is_mulhsu + is_mulw,
      is_mul, is_mulh, is_mulhu, is_mulhsu, is_mulw⟩
  is_mul * (is_mul - 1) === 0
  is_mulh * (is_mulh - 1) === 0
  is_mulhu * (is_mulhu - 1) === 0
  is_mulhsu * (is_mulhsu - 1) === 0
  is_mulw * (is_mulw - 1) === 0
  (is_mul + is_mulh + is_mulhu + is_mulhsu + is_mulw)
    * ((is_mul + is_mulh + is_mulhu + is_mulhsu + is_mulw) - 1) === 0
  -- Ommitted --
  return ⟨input.state, input.adapter, a, cols, is_mul, is_mulh, is_mulhu, is_mulhsu, is_mulw⟩

instance MulChip.elaborated : ElaboratedCircuit (ZMod p) Inputs MulCols main where
  localLength _ := 54
  localLength_eq := by simp +arith [circuit_norm, main, MulOperation.circuit, Readers.CPUState.circuit, Readers.RTypeReader.circuit]
  subcircuitsConsistent := by simp only [circuit_norm, main, MulOperation.circuit, Readers.CPUState.circuit, Readers.RTypeReader.circuit]; try omega
  channelsWithGuarantees := [byteChannel.toRawGated]
  channelsWithRequirements :=
    [byteChannel.toRawGated, stateChannel.toRawGated, memoryChannel.toRaw, programChannel.toRaw]
  channelsLawful := by simp [circuit_norm, main, MulOperation.circuit, Readers.CPUState.circuit, Readers.RTypeReader.circuit]

-- Lots of lemmas and files in between these two

def MulChip.circuit : GeneralFormalCircuit (ZMod p) Inputs MulCols :=
  { MulChip.main, MulChip.elaborated,
    Assumptions := MulChip.Assumptions, Spec := MulChip.Spec,
    ProverAssumptions := MulChip.ProverAssumptions, ProverSpec := fun _ _ _ => True,
    soundness := MulChip.soundness, completeness := MulChip.completeness }