feat: merge release branch (#88)

* feat: release branch

* new files

* extra comments

* add comment

---------

Co-authored-by: Tamir Hemo <[email protected]>

Author: dtumad

README.md

@@ -50,7 +50,7 @@ Each chip contains:
 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
+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
@@ -72,6 +72,11 @@ theorem correct_add
 
 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.
+
 ## Building
 
 ### Prerequisites

SP1Chips.lean

@@ -6,12 +6,6 @@ import SP1Chips.Addw.Constraints
 import SP1Chips.AddwChip
 import SP1Chips.Bitwise.Constraints
 import SP1Chips.BitwiseChip
--- import SP1Chips.Branch.BEQ
--- import SP1Chips.Branch.BGE
--- import SP1Chips.Branch.BGEU
--- import SP1Chips.Branch.BLT
--- import SP1Chips.Branch.BLTU
--- import SP1Chips.Branch.BNE
 import SP1Chips.Branch.Constraints
 import SP1Chips.BranchChip
 import SP1Chips.DivRem.Constraints

SP1Chips/AddChip.lean

@@ -1,80 +1,76 @@
-import SP1Foundations
-import SP1Operations.Operation.AddOperation
-import SP1Operations.Reader.CPUState
-import SP1Operations.Reader.RTypeReader
-import LeanRV64D.RiscvInstsEnd
-
 import SP1Chips.Add.Constraints
 
-open LeanRV64D.Functions BitVec
+open LeanRV64D.Functions
 
 namespace Add
 
-variable
-  (Main : Vector (Fin KB) 34)
-  (s : SailState)
-  (cstrs : (constraints Main).allHold)
-  (h_is_real : Main[33] = 1)
-
-noncomputable def spec_add (rs2 rs1 rd : regidx) : SailM Unit := do
-  Sail.writeReg Register.nextPC ((← Sail.readReg Register.PC) + 4#64)
-  _ ← execute_RTYPE rs2 rs1 rd rop.ADD
-  pure ()
+variable (Main : Vector (Fin KB) 34)
 
+-- The input and output values in the SP1 implementation
 def sp1_op_a : BitVec 5 := BitVec.ofNat 5 Main[6]
-
 def sp1_op_b : BitVec 5 := BitVec.ofNat 5 Main[14]
-
 def sp1_op_c : BitVec 5 := BitVec.ofNat 5 Main[21]
 
-def sp1_add : SailM Unit := do
-  let op_a := sp1_op_a Main
+/-- Specification of the ADD operation in sail, while setting the next program counter-/
+def spec_add (rs2 rs1 rd : regidx) : SailM ExecutionResult := do
+  Sail.writeReg Register.nextPC ((← Sail.readReg Register.PC) + 4#64)
+  execute_RTYPE rs2 rs1 rd rop.ADD
+
+/-- Behavior of the ADD operation in SP1, writing the given values to registers-/
+def sp1_add : SailM ExecutionResult := do
   Sail.writeReg Register.nextPC (Word.toBitVec64 #v[Main[3] + 4, Main[4], Main[5], 0])
-  Sail.write_reg op_a (Word.toBitVec64 #v[Main[29], Main[30], Main[31], Main[32]])
+  Sail.write_reg (sp1_op_a Main) (Word.toBitVec64 #v[Main[29], Main[30], Main[31], Main[32]])
+  return RETIRE_SUCCESS
 
 open Sail
 
-set_option pp.parens true in
+/-- Given that all the constraints hold for the input `Main`, `s` is a machine state with
+registers initialized to appropriate values, and the column is a real column,
+the Sail spec and SP1 implementation behave the same. -/
 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
-  := by
-    simp [SP1ConstraintList.initialState, constraints, SP1Constraint.toStateProp, List.Forall, AddOperation.constraints, CPUState.constraints, RTypeReader.constraints] at state_cstrs
-    obtain ⟨read_pc, trusted_instr_state, _, read_op_b, read_op_c⟩ := state_cstrs
-    simp [constraints] at cstrs
-    obtain ⟨add_op_cstrs, cpu_cstrs, reader_cstrs, rest⟩ := cstrs
-    rw [CPUState.allHold_constraints_iff_is_real h_is_real] at cpu_cstrs
-    rw [RTypeReader.allHold_constraints_iff_is_real h_is_real] at reader_cstrs
-    simp [Opcode.ofNat, Nat.ble] at reader_cstrs
-    obtain ⟨ trusted_instr_prop, _, _, _, _, _, _, _, ⟨ ⟨ _, _, ⟨ _, is_U64_b, is_U64_c ⟩ ⟩, _ ⟩⟩ := reader_cstrs
-    simp [Opcode.ofNat, Nat.ble] at trusted_instr_state trusted_instr_prop
+    (Main : Vector (Fin KB) 34)
+    (s : SailState)
+    (h_cstrs : (constraints Main).allHold)
+    (h_is_real : Main[33] = 1)
+    (state_cstrs : (constraints Main).initialState s) :
+    let op_c := .Regidx (sp1_op_c Main)
+    let op_b := .Regidx (sp1_op_b Main)
+    let op_a := .Regidx (sp1_op_a Main)
+    (spec_add op_c op_b op_a).run s = (sp1_add Main).run s := by
+  -- Simplify the main constraints and split them into parts
+  simp [constraints] at h_cstrs
+  obtain ⟨add_op_cstrs, cpu_cstrs, reader_cstrs, rest⟩ := h_cstrs
+  rw [CPUState.allHold_constraints_iff_is_real h_is_real] at cpu_cstrs
+  rw [RTypeReader.allHold_constraints_iff_is_real h_is_real] at reader_cstrs
+  simp [Opcode.ofNat, Nat.ble] at reader_cstrs
 
-    rw [h_is_real] at *
-    apply AddOperation.spec is_U64_b is_U64_c at add_op_cstrs
-    obtain ⟨ is_U64_val, is_add ⟩ := add_op_cstrs
-    simp [BitVec.ofNatLT_eq_ofNat] at *
+  -- Show the write values are all register values (i.e. are 5-bit)
+  have h6 : Main[6] < 32 := by aesop
+  have h14 : Main[14] < 32 := by aesop
+  have h21 : Main[21] < 32 := by aesop
 
-    -- Now the monadic manipulation
-    simp [spec_add, sp1_add, execute, execute_RTYPE']
-    rw [run_readReg, read_pc]
-    simp [sp1_op_b, read_op_b (by omega)]
-    simp [sp1_op_c, read_op_c (by omega)]
-    simp [sp1_op_a]
-    rw [KoalaBear.add4_into_pc_ofNat (by omega)]
+  -- Extract constraints about the initial register states
+  simp [SP1ConstraintList.initialState, constraints, SP1Constraint.toStateProp,
+    List.Forall, AddOperation.constraints, CPUState.constraints, BitVec.ofNatLT_eq_ofNat,
+    RTypeReader.constraints, h6, h14, h21, h_is_real] at state_cstrs
+  obtain ⟨read_pc, read_op_a, read_op_b, read_op_c⟩ := state_cstrs
+
+  rw [h_is_real] at *
+  apply AddOperation.spec (by aesop) (by aesop) at add_op_cstrs
 
-    by_cases h_is_op_a_0 : Main[6] = 0 <;> simp_all
-    . rw [← is_add]
-      simp [Word.toBitVec64, Word.toNat]
-    . rw [if_neg (by simp [← BitVec.toNat_inj]; omega)]
-      rw [if_neg (by simp [← BitVec.toNat_inj]; omega)]
-      simp [Word.toBitVec64, Word.toNat]
-      rfl
+  -- Simplify the monadic operations
+  simp [spec_add, sp1_add, execute, execute_RTYPE']
+  rw [run_readReg, read_pc]
+  simp [sp1_op_b, read_op_b, sp1_op_c, read_op_c, sp1_op_a]
+
+  -- Simplify the expressions using the arithmetic constraints
+  by_cases h_is_op_a_0 : Main[6] = 0 <;> simp_all
+  . rw [← add_op_cstrs.2]
+    simp [Word.toBitVec64, Word.toNat]
+    rw [KoalaBear.add4_into_pc_ofNat (by omega)]
+  . rw [if_neg (by simp [← BitVec.toNat_inj]; omega), if_neg (by simp [← BitVec.toNat_inj]; omega)]
+    simp [execute_RTYPE_pure, bitVecToRegidxVal, Word.toBitVec64, Word.toNat]
+    rw [KoalaBear.add4_into_pc_ofNat (by omega)]
+    simp
 
 end Add

SP1Chips/AddiChip.lean

@@ -41,15 +41,23 @@ theorem correct_addi
   (spec_addi op_c (.Regidx op_b) (.Regidx op_a)).run s = (sp1_addi Main).run s
   := by
     -- Obtain and simplify state and pure constraints
-    simp [SP1ConstraintList.initialState, constraints, SP1Constraint.toStateProp, List.Forall, AddOperation.constraints, CPUState.constraints, ITypeReader.constraints, h_is_real] at state_cstrs
-    obtain ⟨read_pc, trusted_instr_state, read_op_b, read_op_c⟩ := state_cstrs
     simp [constraints] at cstrs
     obtain ⟨add_op_cstrs, cpu_cstrs, reader_cstrs, rest⟩ := cstrs
     rw [CPUState.allHold_constraints_iff_is_real h_is_real] at cpu_cstrs
     rw [ITypeReader.allHold_constraints_iff_is_real h_is_real] at reader_cstrs
+    simp [Opcode.ofNat, Nat.ble] at reader_cstrs
 
     obtain ⟨ _, trusted_instr_prop, hcm1, hcm2, c0, c1, c2, c3, h11, h12, h13, h14, h15, h16, h17, h18, h19, h20, ⟨ is_U64_a, is_U64_b, hu64 ⟩⟩ := reader_cstrs
 
+    have h6 : Main[6] < 32 := by aesop
+    have h14 : Main[14] < 32 := by aesop
+
+    simp [SP1ConstraintList.initialState, constraints, SP1Constraint.toStateProp,
+      List.Forall, AddOperation.constraints, CPUState.constraints, ITypeReader.constraints,
+      h6, h14, h_is_real] at state_cstrs
+
+    obtain ⟨read_pc, read_op_b, read_op_c⟩ := state_cstrs
+
     simp_all [Opcode.ofNat, Nat.ble]
     have is_U64_c : Word.isU64 #v[Main[21], Main[22], Main[23], Main[24]]
       := by apply Word.isU64_of_cases c0 c1 c2 c3
@@ -65,18 +73,21 @@ theorem correct_addi
     simp [sp1_op_b, read_op_b]
     simp [sp1_op_c, read_op_c]
     simp [sp1_op_a]
-    rw [KoalaBear.add4_into_pc_ofNat (by omega)]
+
 
     by_cases h_is_op_a_0 : Main[6] = 0
     . have : Main[13] = 1 := by clear *- h12 h_is_op_a_0; aesop
       rw [← is_add] at *
       simp [Word.toBitVec64, Word.toNat, h_is_op_a_0]
+      rw [KoalaBear.add4_into_pc_ofNat (by omega)]
       clear *- this hu64
       aesop
     . rw [if_neg (by simp [← BitVec.toNat_inj]; omega)]
       rw [if_neg (by simp [← BitVec.toNat_inj]; omega)]
-      rw [is_add, trusted_instr_prop.2]
+      rw [is_add, trusted_instr_prop]
       simp [Word.toBitVec64, Word.toNat]
+      rw [KoalaBear.add4_into_pc_ofNat (by omega)]
+      simp
       rfl
 
 end Addi

SP1Chips/AddwChip.lean

@@ -43,16 +43,18 @@ theorem correct_addw
   let op_a := sp1_op_a Main
   (spec_addw (.Regidx op_c) (.Regidx op_b) (.Regidx op_a)).run s = (sp1_addw Main).run s
   := by
-    simp [SP1ConstraintList.initialState, constraints, SP1Constraint.toStateProp, List.Forall,
-      AddwOperation.constraints, CPUState.constraints, ALUTypeReader.constraints, U16MSBOperation.constraints,
-      h_is_real, h_is_trusted] at state_cstrs
-    obtain ⟨read_pc, trusted_instr_state, read_op_a, read_op_b, read_op_c⟩ := state_cstrs
     simp [constraints] at cstrs
 
     obtain ⟨addw_op_cstrs, cpu_cstrs, alu_cstrs, _⟩ := cstrs
     rw [CPUState.allHold_constraints_iff_is_real h_is_real] at cpu_cstrs
     rw [ALUTypeReader.allHold_constraints_iff_is_real h_is_real] at alu_cstrs
     obtain ⟨ _, trusted_instr_prop, _, _, _, _, _, _, _, _, _, _, _, _, _, _, is_U64_a, is_U64_b, is_U64_c , _, _ ⟩ := alu_cstrs
+
+    simp [SP1ConstraintList.initialState, constraints, SP1Constraint.toStateProp, List.Forall,
+      AddwOperation.constraints, CPUState.constraints, ALUTypeReader.constraints, U16MSBOperation.constraints,
+      h_is_real, h_is_trusted] at state_cstrs
+    obtain ⟨read_pc, read_op_a, read_op_b, read_op_c⟩ := state_cstrs
+
     simp [Opcode.ofNat, Nat.ble] at *
     simp_all
 
@@ -73,16 +75,18 @@ theorem correct_addw
     rw [exec_RTYPEW_pure_bv_to_w _ _ _ (by omega) (by omega)]
     simp [execute_RTYPEW_pure_w]
     rw [← is_addw] at is_msb
-    rw [KoalaBear.add4_into_pc_ofNat (by omega)]
 
     by_cases h_is_op_a_0 : Main[6] = 0 <;> simp_all
     . simp [Word.toBitVec64, Word.toNat]
+      rw [KoalaBear.add4_into_pc_ofNat (by omega)]
     . have : BitVec.ofNat 5 Main[6] ≠ 0#5 := by
         simp [← BitVec.toNat_inj]; omega
       simp [this, Word.toBitVec64, Word.toNat]
-      rw [← is_addw]; congr
+      rw [← is_addw]
       rw [HWord.sign_extend_32_to_64_msb is_U32_val]
       simp [Word.toBitVec64, Word.toNat]
+      rw [KoalaBear.add4_into_pc_ofNat (by omega)]
+      simp [bitVecToRegidxVal]
 
 end Addw
 
@@ -124,14 +128,15 @@ theorem correct_addw
   let op_a := sp1_op_a Main
   (spec_addiw op_c (.Regidx op_b) (.Regidx op_a)).run s = (sp1_addiw Main).run s
   := by
-    -- Obtain and simplify state and pure constraints
-    simp [SP1ConstraintList.initialState, constraints, SP1Constraint.toStateProp, List.Forall, AddwOperation.constraints, CPUState.constraints, ALUTypeReader.constraints, U16MSBOperation.constraints, h_is_real] at state_cstrs
-    obtain ⟨read_pc, trusted_instr_state, read_op_a, read_op_b, read_op_c⟩ := state_cstrs
     simp [constraints] at cstrs
     obtain ⟨addw_op_cstrs, cpu_cstrs, alu_cstrs, _ ⟩ := cstrs
     rw [CPUState.allHold_constraints_iff_is_real h_is_real] at cpu_cstrs
     rw [ALUTypeReader.allHold_constraints_iff_is_real h_is_real] at alu_cstrs
     obtain ⟨ _, trusted_instr_prop, _, _, ⟨ c0, c1, c2, c3 ⟩, _, _, _, _, _, _, _, _, _, _, _, is_U64_a, is_U64_b, _, _, _ ⟩ := alu_cstrs
+
+    simp [SP1ConstraintList.initialState, constraints, SP1Constraint.toStateProp, List.Forall, AddwOperation.constraints, CPUState.constraints, ALUTypeReader.constraints, U16MSBOperation.constraints, h_is_real] at state_cstrs
+    obtain ⟨read_pc, read_op_a, read_op_b, read_op_c⟩ := state_cstrs
+
     simp [Opcode.ofNat, Nat.ble] at *
     simp_all
     have is_U64_c : Word.isU64 #v[Main[21], Main[22], Main[23], Main[24]]
@@ -155,15 +160,17 @@ theorem correct_addw
     rw [exec_RTYPEW_pure_bv_to_w _ _ _ (by omega) (by omega)]
     simp [execute_RTYPEW_pure_w]
     rw [← is_addw] at is_msb
-    rw [KoalaBear.add4_into_pc_ofNat (by omega)]
 
     by_cases h_is_op_a_0 : Main[6] = 0 <;> simp_all
     . simp [Word.toBitVec64, Word.toNat]
+      rw [KoalaBear.add4_into_pc_ofNat (by omega)]
     . have : BitVec.ofNat 5 Main[6] ≠ 0#5 := by
         simp [← BitVec.toNat_inj]; omega
       simp [this, Word.toBitVec64, Word.toNat]
-      rw [← is_addw]; congr
+      rw [← is_addw]
       rw [HWord.sign_extend_32_to_64_msb is_U32_val]
       simp [Word.toBitVec64, Word.toNat]
+      rw [KoalaBear.add4_into_pc_ofNat (by omega)]
+      simp [bitVecToRegidxVal]
 
 end Addiw