64-bit ALU Verification, Part I

SP1Chips/AddChip.lean

@@ -18,7 +18,7 @@ variable
 
 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
+  _ ← execute (.RTYPE (rs2, rs1, rd, rop.ADD))
   pure ()
 
 def sp1_op_a : BitVec 5 :=
@@ -73,7 +73,7 @@ def sp1_add : SailM Unit := do
 
 open Sail
 
-theorem correct
+theorem correct_add
   (state_cstrs : (constraints Main).initialState s) :
   let op_c := sp1_op_c Main cstrs h_is_real
   let op_b := sp1_op_b Main cstrs h_is_real
@@ -95,7 +95,7 @@ theorem correct
     simp at *
 
     -- Now the monadic manipulation
-    simp [spec_add, sp1_add, execute_RTYPE]
+    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)]

SP1Chips/AddiChip.lean

@@ -2,3 +2,99 @@ import SP1Operations.Operation.AddOperation
 import SP1Operations.Reader.CPUState
 import SP1Operations.Reader.ITypeReader
 import SP1Chips.Addi.Constraints
+
+import SP1Chips.Add.Constraints
+
+open LeanRV64IM.Functions BitVec
+
+namespace Addi
+
+variable
+  (Main : Vector (Fin BB) 30)
+  (s : SailState)
+  (cstrs : (constraints Main).allHold)
+  (h_is_real : Main[29] = 1)
+
+def spec_addi (imm : BitVec 12) (rs1 rd : regidx) : SailM Unit := do
+  Sail.writeReg Register.nextPC ((← Sail.readReg Register.PC) + 4#64)
+  _ ← execute (.ITYPE (imm, rs1, rd, iop.ADDI))
+  pure ()
+
+def sp1_op_a : BitVec 5 :=
+  by
+    refine BitVec.ofNatLT Main[6] ?_
+    simp
+    show Main[6] < 32
+
+    have reader_cstrs := by
+      simp [SP1ConstraintList.allHold, constraints, SP1Constraint.toProp] at cstrs
+      exact cstrs.2.2.1
+
+    clear cstrs
+    simp [ITypeReader.constraints, h_is_real, Opcode.ofNat, Nat.ble, Nat.beq, SP1Constraint.toProp] at reader_cstrs
+
+    exact reader_cstrs.1.2.1
+
+def sp1_op_b : BitVec 5 :=
+  by
+    refine BitVec.ofNatLT Main[14] ?_
+    simp
+    show Main[14] < 32
+
+    have reader_cstrs := by
+      simp [SP1ConstraintList.allHold, constraints, SP1Constraint.toProp] at cstrs
+      exact cstrs.2.2.1
+
+    clear cstrs
+    simp [ITypeReader.constraints, h_is_real, Opcode.ofNat, Nat.ble, Nat.beq, SP1Constraint.toProp] at reader_cstrs
+
+    exact reader_cstrs.1.1.1
+
+def sp1_op_c : BitVec 12 := BitVec.ofNat 12 Main[21].val
+
+def sp1_addi : SailM Unit := do
+  let op_a := sp1_op_a Main cstrs h_is_real
+  Sail.writeReg Register.nextPC (Word.toBitVec64 #v[Main[3], Main[4], Main[5], 0] + 4)
+  Sail.write_reg op_a (Word.toBitVec64 #v[Main[25], Main[26], Main[27], Main[28]])
+
+open Sail
+
+theorem correct_addi
+  (state_cstrs : (constraints Main).initialState s) :
+  let op_c := sp1_op_c Main
+  let op_b := sp1_op_b Main cstrs h_is_real
+  let op_a := sp1_op_a Main cstrs h_is_real
+  (spec_addi op_c (.Regidx op_b) (.Regidx op_a)).run s = (sp1_addi Main cstrs h_is_real).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
+    apply AddOperation.correct (h_is_real := h_is_real) at add_op_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
+    obtain ⟨ trusted_instr_prop, _, _, c0, c1, c2, c3, _, _, _, _, _, _, _, _, _, _, ⟨ is_U64_a, is_U64_b, _ ⟩⟩ := reader_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
+    specialize add_op_cstrs is_U64_b is_U64_c
+    obtain ⟨ is_U64_val, is_add ⟩ := add_op_cstrs
+    simp_all
+
+    -- Now the monadic manipulation
+    simp [spec_addi, sp1_addi, execute, execute_ITYPE]
+    rw [run_readReg, read_pc]
+    simp [sp1_op_b, read_op_b]
+    simp [sp1_op_c, read_op_c]
+    simp [sp1_op_a]
+
+    by_cases h_is_op_a_0 : Main[6] = 0 <;> simp_all
+    . rw [← is_add]
+      simp [Word.toBitVec64, Word.toNat]
+    . rw [if_neg (by simpa [← BitVec.toNat_inj])]
+      rw [if_neg (by simpa [← BitVec.toNat_inj])]
+      simp [Word.toBitVec64, Word.toNat]
+      rfl
+
+end Addi

SP1Chips/AddwChip.lean

@@ -2,3 +2,224 @@ import SP1Operations.Operation.AddwOperation
 import SP1Operations.Reader.CPUState
 import SP1Operations.Reader.ALUTypeReader
 import SP1Chips.Addw.Constraints
+
+open LeanRV64IM.Functions
+open BitVec
+
+namespace Addw
+
+variable
+  (Main : Vector (Fin BB) 37)
+  (s : SailState)
+  (cstrs : (constraints Main).allHold)
+  (h_is_real : Main[35] = 1)
+  (h_is_addw : Main[31] = 0)
+
+def spec_addw (rs2 rs1 rd : regidx) : SailM Unit := do
+  Sail.writeReg Register.nextPC ((← Sail.readReg Register.PC) + 4#64)
+  _ ← execute_RTYPEW rs2 rs1 rd ropw.ADDW
+  pure ()
+
+def sp1_op_a : BitVec 5 :=
+  by
+    refine BitVec.ofNatLT Main[6] ?_
+    simp
+    show Main[6] < 32
+
+    have alu_cstrs := by
+      simp [SP1ConstraintList.allHold, constraints, SP1Constraint.toProp] at cstrs
+      exact cstrs.2.2.1
+
+    clear cstrs
+    simp [ALUTypeReader.constraints, h_is_real, Opcode.ofNat, Nat.ble, Nat.beq, SP1Constraint.toProp] at alu_cstrs
+
+    exact alu_cstrs.1.2.1
+
+def sp1_op_b : BitVec 5 :=
+  by
+    refine BitVec.ofNatLT Main[14] ?_
+    simp
+    show Main[14] < 32
+
+    have alu_cstrs := by
+      simp [SP1ConstraintList.allHold, constraints, SP1Constraint.toProp] at cstrs
+      exact cstrs.2.2.1
+
+    clear cstrs
+    have : (Main[31] = 0 ∨ Main[31] = 1) := by
+      simp [ALUTypeReader.allHold_constraints_iff_is_real (h := h_is_real), Opcode.ofNat, Nat.ble] at alu_cstrs
+      aesop
+
+    simp [ALUTypeReader.allHold_constraints_iff_is_real (h := h_is_real), Opcode.ofNat, Nat.ble] at alu_cstrs
+    rcases this <;> simp_all
+
+def sp1_op_c : BitVec 5 :=
+  by
+    refine BitVec.ofNatLT Main[21] ?_
+    simp
+    show Main[21] < 32
+
+    have alu_cstrs := by
+      simp [SP1ConstraintList.allHold, constraints, SP1Constraint.toProp] at cstrs
+      exact cstrs.2.2.1
+
+    clear cstrs
+    simp [ALUTypeReader.allHold_constraints_iff_is_real (h := h_is_real), Opcode.ofNat, Nat.ble, h_is_addw] at alu_cstrs
+
+    exact alu_cstrs.1.2.1
+
+def sp1_addw : SailM Unit := do
+  let op_a := sp1_op_a Main cstrs h_is_real
+  -- TODO(gzgz): we can obtain this from the constraint compiler
+  -- This comes from the Interaction.state in CPUState
+  Sail.writeReg Register.nextPC (Word.toBitVec64 #v[Main[3], Main[4], Main[5], 0] + 4)
+  Sail.write_reg op_a (Word.toBitVec64 #v[Main[32], Main[33], Main[34] * 65535, Main[34] * 65535])
+
+theorem correct_addw
+  (state_cstrs : (constraints Main).initialState s)
+  (h_is_addw : Main[31] = 0) :
+  let op_c := sp1_op_c Main cstrs h_is_real h_is_addw
+  let op_b := sp1_op_b Main cstrs h_is_real h_is_addw
+  let op_a := sp1_op_a Main cstrs h_is_real
+  (spec_addw (.Regidx op_c) (.Regidx op_b) (.Regidx op_a)).run s = (sp1_addw Main cstrs h_is_real).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
+    apply AddwOperation.correct (h_is_real := h_is_real) at addw_op_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 [Opcode.ofNat, Nat.ble] at *
+    simp_all
+    obtain ⟨ _, _, is_U64_c ⟩ := is_U64_c
+    specialize addw_op_cstrs is_U64_b is_U64_c
+    obtain ⟨ is_U32_val, is_addw, is_msb ⟩ := addw_op_cstrs
+    simp_all
+
+    -- Now the monadic manipulation
+    simp [spec_addw, sp1_addw, execute, execute_RTYPEW']
+    rw [Sail.run_readReg, read_pc]
+    simp [sp1_op_a, sp1_op_b, sp1_op_c, read_op_b, read_op_c]
+    rw [exec_RTYPEW_pure_bv_to_w _ _ _ (by omega) (by omega)]
+    simp [execute_RTYPEW_pure_w]
+    rw [← is_addw] at is_msb
+
+    by_cases h_is_op_a_0 : Main[6] = 0 <;> simp_all
+    . simp [Word.toBitVec64, Word.toNat]
+    . rw [if_neg (by simpa [← BitVec.toNat_inj])]
+      rw [if_neg (by simpa [← BitVec.toNat_inj])]
+      simp [Word.toBitVec64, Word.toNat]
+      rw [← is_addw]; congr
+      rw [HalfWord.sign_extend_32_to_64_msb _ _ is_U32_val]
+      simp [Word.toBitVec64, Word.toNat]
+
+end Addw
+
+namespace Addiw
+
+open Addw
+
+variable
+  (Main : Vector (Fin BB) 37)
+  (s : SailState)
+  (cstrs : (constraints Main).allHold)
+  (h_is_real : Main[35] = 1)
+  (h_is_addiw : Main[31] = 1)
+
+def spec_addiw (imm : BitVec 12) (rs1 rd : regidx) : SailM Unit := do
+  Sail.writeReg Register.nextPC ((← Sail.readReg Register.PC) + 4#64)
+  _ ← execute_ADDIW imm rs1 rd
+  pure ()
+
+def sp1_op_a : BitVec 5 :=
+  by
+    refine BitVec.ofNatLT Main[6] ?_
+    simp
+    show Main[6] < 32
+
+    have alu_cstrs := by
+      simp [SP1ConstraintList.allHold, constraints, SP1Constraint.toProp] at cstrs
+      exact cstrs.2.2.1
+
+    clear cstrs
+    simp [ALUTypeReader.constraints, h_is_real, Opcode.ofNat, Nat.ble, Nat.beq, SP1Constraint.toProp] at alu_cstrs
+
+    exact alu_cstrs.1.2.1
+
+def sp1_op_b : BitVec 5 :=
+  by
+    refine BitVec.ofNatLT Main[14] ?_
+    simp
+    show Main[14] < 32
+
+    have alu_cstrs := by
+      simp [SP1ConstraintList.allHold, constraints, SP1Constraint.toProp] at cstrs
+      exact cstrs.2.2.1
+
+    clear cstrs
+    have : (Main[31] = 0 ∨ Main[31] = 1) := by
+      simp [ALUTypeReader.allHold_constraints_iff_is_real (h := h_is_real), Opcode.ofNat, Nat.ble] at alu_cstrs
+      aesop
+
+    simp [ALUTypeReader.allHold_constraints_iff_is_real (h := h_is_real), Opcode.ofNat, Nat.ble] at alu_cstrs
+    rcases this <;> simp_all
+
+def sp1_op_c : BitVec 12 := BitVec.ofNat 12 Main[21].val
+
+def sp1_addiw : SailM Unit := do
+  let op_a := sp1_op_a Main cstrs h_is_real
+  -- TODO(gzgz): we can obtain this from the constraint compiler
+  -- This comes from the Interaction.state in CPUState
+  Sail.writeReg Register.nextPC (Word.toBitVec64 #v[Main[3], Main[4], Main[5], 0] + 4)
+  Sail.write_reg op_a (Word.toBitVec64 #v[Main[32], Main[33], Main[34] * 65535, Main[34] * 65535])
+
+set_option maxHeartbeats 1000000 in
+theorem correct_addw
+  (state_cstrs : (constraints Main).initialState s) :
+  let op_c := sp1_op_c Main
+  let op_b := sp1_op_b Main cstrs h_is_real h_is_addiw
+  let op_a := sp1_op_a Main cstrs h_is_real
+  (spec_addiw op_c (.Regidx op_b) (.Regidx op_a)).run s = (sp1_addiw Main cstrs h_is_real).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
+    apply AddwOperation.correct (h_is_real := h_is_real) at addw_op_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 [Opcode.ofNat, Nat.ble] at *
+    simp_all
+    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
+    specialize addw_op_cstrs is_U64_b is_U64_c
+    obtain ⟨ is_U32_val, is_addw, is_msb ⟩ := addw_op_cstrs
+    simp_all
+    obtain ⟨ h_f, h_imm_c ⟩ := trusted_instr_prop
+    simp [h_is_addiw] at h_f h_imm_c
+    obtain ⟨ h_c, h_is_imm_c ⟩ := h_imm_c
+
+    -- Now the monadic manipulation
+    simp [spec_addiw, sp1_addiw, execute, execute_ADDIW']
+    rw [Sail.run_readReg, read_pc]
+    simp [sp1_op_a, sp1_op_b, sp1_op_c, read_op_b]
+    rw [← h_is_imm_c]
+    rw [exec_RTYPEW_pure_bv_to_w _ _ _ (by omega) (by omega)]
+    simp [execute_RTYPEW_pure_w]
+    rw [← is_addw] at is_msb
+
+    by_cases h_is_op_a_0 : Main[6] = 0 <;> simp_all
+    . simp [Word.toBitVec64, Word.toNat]
+    . rw [if_neg (by simpa [← BitVec.toNat_inj])]
+      rw [if_neg (by simpa [← BitVec.toNat_inj])]
+      simp [Word.toBitVec64, Word.toNat]
+      rw [← is_addw]; congr
+      rw [HalfWord.sign_extend_32_to_64_msb _ _ is_U32_val]
+      simp [Word.toBitVec64, Word.toNat]
+
+end Addiw