feat: mprotect and koala bear constraint changes (#83)

Author: dtumad

SP1Chips.lean

@@ -6,12 +6,12 @@ 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.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/Add/Constraints.lean

@@ -7,15 +7,15 @@ namespace Add
 section constraints
 
 -- Generated Lean code for chip AddChip
-@[irreducible] def constraints (Main : Vector (Fin BB) 33) : SP1ConstraintList :=
-  let E0 : Fin BB := Main[32] - 1
-  let E1 : Fin BB := Main[32] * E0
-  let CS0 : SP1ConstraintList := AddOperation.constraints #v[Main[15], Main[16], Main[17], Main[18]] #v[Main[22], Main[23], Main[24], Main[25]] { value := #v[Main[28], Main[29], Main[30], Main[31]] } Main[32]
-  let E2 : Fin BB := Main[3] + 4
-  let CS1 : SP1ConstraintList := CPUState.constraints { clk_high := Main[0], clk_16_24 := Main[1], clk_0_16 := Main[2], pc := #v[Main[3], Main[4], Main[5]] } #v[E2, Main[4], Main[5]] 8 Main[32]
-  let E3 : Fin BB := Main[1] * 65536
-  let E4 : Fin BB := Main[2] + E3
-  let CS2 : SP1ConstraintList := RTypeReader.constraints Main[0] E4 #v[Main[3], Main[4], Main[5]] 0 #v[51, 0, 0] #v[Main[28], Main[29], Main[30], Main[31]] { op_a := Main[6], op_a_memory := { prev_value := #v[Main[7], Main[8], Main[9], Main[10]], access_timestamp := { prev_low := Main[11], diff_low_limb := Main[12] } }, op_a_0 := Main[13], op_b := Main[14], op_b_memory := { prev_value := #v[Main[15], Main[16], Main[17], Main[18]], access_timestamp := { prev_low := Main[19], diff_low_limb := Main[20] } }, op_c := Main[21], op_c_memory := { prev_value := #v[Main[22], Main[23], Main[24], Main[25]], access_timestamp := { prev_low := Main[26], diff_low_limb := Main[27] } } } Main[32]
+@[irreducible] def constraints (Main : Vector (Fin KB) 34) : SP1ConstraintList :=
+  let E0 : Fin KB := Main[33] - 1
+  let E1 : Fin KB := Main[33] * E0
+  let CS0 : SP1ConstraintList := AddOperation.constraints #v[Main[15], Main[16], Main[17], Main[18]] #v[Main[22], Main[23], Main[24], Main[25]] { value := #v[Main[29], Main[30], Main[31], Main[32]] } Main[33]
+  let E2 : Fin KB := Main[3] + 4
+  let CS1 : SP1ConstraintList := CPUState.constraints { clk_high := Main[0], clk_16_24 := Main[1], clk_0_16 := Main[2], pc := #v[Main[3], Main[4], Main[5]] } #v[E2, Main[4], Main[5]] 8 Main[33]
+  let E3 : Fin KB := Main[1] * 65536
+  let E4 : Fin KB := Main[2] + E3
+  let CS2 : SP1ConstraintList := RTypeReader.constraints Main[0] E4 #v[Main[3], Main[4], Main[5]] 0 #v[8, 51, 0, 0] #v[Main[29], Main[30], Main[31], Main[32]] { op_a := Main[6], op_a_memory := { prev_value := #v[Main[7], Main[8], Main[9], Main[10]], access_timestamp := { prev_low := Main[11], diff_low_limb := Main[12] } }, op_a_0 := Main[13], op_b := Main[14], op_b_memory := { prev_value := #v[Main[15], Main[16], Main[17], Main[18]], access_timestamp := { prev_low := Main[19], diff_low_limb := Main[20] } }, op_c := Main[21], op_c_memory := { prev_value := #v[Main[22], Main[23], Main[24], Main[25]], access_timestamp := { prev_low := Main[26], diff_low_limb := Main[27] } }, is_trusted := Main[28] } Main[33]
   CS0 ++ CS1 ++ CS2 ++ [
     (.assertZero E1),
   ]

SP1Chips/AddChip.lean

@@ -11,103 +11,69 @@ open LeanRV64D.Functions BitVec
 namespace Add
 
 variable
-  (Main : Vector (Fin BB) 33)
+  (Main : Vector (Fin KB) 34)
   (s : SailState)
   (cstrs : (constraints Main).allHold)
-  (h_is_real : Main[32] = 1)
+  (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 ()
 
-def sp1_op_a : BitVec 5 :=
-  by
-    refine BitVec.ofNatLT Main[6] ?_
-    simp
-    show Main[6] < 32
+def sp1_op_a : BitVec 5 := BitVec.ofNat 5 Main[6]
 
-    have reader_cstrs := by
-      simp [SP1ConstraintList.allHold, constraints, SP1Constraint.toProp] at cstrs
-      exact cstrs.2.2.1
+def sp1_op_b : BitVec 5 := BitVec.ofNat 5 Main[14]
 
-    clear cstrs
-    simp [RTypeReader.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 [RTypeReader.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 5 :=
-  by
-    refine BitVec.ofNatLT Main[21] ?_
-    simp
-    show Main[21] < 32
-
-    have reader_cstrs := by
-      simp [SP1ConstraintList.allHold, constraints, SP1Constraint.toProp] at cstrs
-      exact cstrs.2.2.1
-
-    clear cstrs
-    simp [RTypeReader.constraints, h_is_real, Opcode.ofNat, Nat.ble, Nat.beq, SP1Constraint.toProp] at reader_cstrs
-
-    exact reader_cstrs.1.1.2
+def sp1_op_c : BitVec 5 := BitVec.ofNat 5 Main[21]
 
 def sp1_add : SailM Unit := do
-  let op_a := sp1_op_a Main cstrs h_is_real
+  let op_a := sp1_op_a Main
   Sail.writeReg Register.nextPC (Word.toBitVec64 #v[Main[3] + 4, Main[4], Main[5], 0])
-  Sail.write_reg op_a (Word.toBitVec64 #v[Main[28], Main[29], Main[30], Main[31]])
+  Sail.write_reg op_a (Word.toBitVec64 #v[Main[29], Main[30], Main[31], Main[32]])
 
 open Sail
 
 set_option pp.parens true in
 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 cstrs h_is_real
-  let op_b := sp1_op_b Main cstrs h_is_real
-  let op_a := sp1_op_a Main cstrs h_is_real
-  (spec_add (.Regidx op_c) (.Regidx op_b) (.Regidx op_a)).run s = (sp1_add Main cstrs h_is_real).run 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, h_is_real] at state_cstrs
+    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
-    obtain ⟨ trusted_instr_prop, _, _, _, _, _, _, ⟨ ⟨ _, _, ⟨ _, is_U64_b, is_U64_c ⟩ ⟩, _ ⟩⟩ := 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
 
     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 at *
+    simp [BitVec.ofNatLT_eq_ofNat] at *
 
     -- 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 [BabyBear.add4_into_pc_ofNat (by omega)]
+    rw [KoalaBear.add4_into_pc_ofNat (by omega)]
 
     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])]
+    . rw [if_neg (by simp [← BitVec.toNat_inj]; omega)]
+      rw [if_neg (by simp [← BitVec.toNat_inj]; omega)]
       simp [Word.toBitVec64, Word.toNat]
       rfl
 

SP1Chips/Addi/Constraints.lean

@@ -7,15 +7,15 @@ namespace Addi
 section constraints
 
 -- Generated Lean code for chip AddiChip
-@[irreducible] def constraints (Main : Vector (Fin BB) 30) : SP1ConstraintList :=
-  let E0 : Fin BB := Main[29] - 1
-  let E1 : Fin BB := Main[29] * E0
-  let CS0 : SP1ConstraintList := AddOperation.constraints #v[Main[15], Main[16], Main[17], Main[18]] #v[Main[21], Main[22], Main[23], Main[24]] { value := #v[Main[25], Main[26], Main[27], Main[28]] } Main[29]
-  let E2 : Fin BB := Main[3] + 4
-  let CS1 : SP1ConstraintList := CPUState.constraints { clk_high := Main[0], clk_16_24 := Main[1], clk_0_16 := Main[2], pc := #v[Main[3], Main[4], Main[5]] } #v[E2, Main[4], Main[5]] 8 Main[29]
-  let E3 : Fin BB := Main[1] * 65536
-  let E4 : Fin BB := Main[2] + E3
-  let CS2 : SP1ConstraintList := ITypeReader.constraints Main[0] E4 #v[Main[3], Main[4], Main[5]] 1 #v[19, 0, 0] #v[Main[25], Main[26], Main[27], Main[28]] { op_a := Main[6], op_a_memory := { prev_value := #v[Main[7], Main[8], Main[9], Main[10]], access_timestamp := { prev_low := Main[11], diff_low_limb := Main[12] } }, op_a_0 := Main[13], op_b := Main[14], op_b_memory := { prev_value := #v[Main[15], Main[16], Main[17], Main[18]], access_timestamp := { prev_low := Main[19], diff_low_limb := Main[20] } }, op_c_imm := #v[Main[21], Main[22], Main[23], Main[24]] } Main[29]
+@[irreducible] def constraints (Main : Vector (Fin KB) 31) : SP1ConstraintList :=
+  let E0 : Fin KB := Main[30] - 1
+  let E1 : Fin KB := Main[30] * E0
+  let CS0 : SP1ConstraintList := AddOperation.constraints #v[Main[15], Main[16], Main[17], Main[18]] #v[Main[21], Main[22], Main[23], Main[24]] { value := #v[Main[26], Main[27], Main[28], Main[29]] } Main[30]
+  let E2 : Fin KB := Main[3] + 4
+  let CS1 : SP1ConstraintList := CPUState.constraints { clk_high := Main[0], clk_16_24 := Main[1], clk_0_16 := Main[2], pc := #v[Main[3], Main[4], Main[5]] } #v[E2, Main[4], Main[5]] 8 Main[30]
+  let E3 : Fin KB := Main[1] * 65536
+  let E4 : Fin KB := Main[2] + E3
+  let CS2 : SP1ConstraintList := ITypeReader.constraints Main[0] E4 #v[Main[3], Main[4], Main[5]] 1 #v[4, 19, 0, 0] #v[Main[26], Main[27], Main[28], Main[29]] { op_a := Main[6], op_a_memory := { prev_value := #v[Main[7], Main[8], Main[9], Main[10]], access_timestamp := { prev_low := Main[11], diff_low_limb := Main[12] } }, op_a_0 := Main[13], op_b := Main[14], op_b_memory := { prev_value := #v[Main[15], Main[16], Main[17], Main[18]], access_timestamp := { prev_low := Main[19], diff_low_limb := Main[20] } }, op_c_imm := #v[Main[21], Main[22], Main[23], Main[24]], is_trusted := Main[25] } Main[30]
   CS0 ++ CS1 ++ CS2 ++ [
     (.assertZero E1),
   ]

SP1Chips/AddiChip.lean

@@ -10,61 +10,35 @@ open LeanRV64D.Functions BitVec
 namespace Addi
 
 variable
-  (Main : Vector (Fin BB) 30)
+  (Main : Vector (Fin KB) 31)
   (s : SailState)
-  (cstrs : (constraints Main).allHold)
-  (h_is_real : Main[29] = 1)
 
 noncomputable 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
+def sp1_op_a : BitVec 5 := BitVec.ofNat 5 Main[6]
 
-    exact reader_cstrs.1.1.1
+def sp1_op_b : BitVec 5 := BitVec.ofNat 5 Main[14]
 
-def sp1_op_c : BitVec 12 := BitVec.ofNat 12 Main[21].val
+def sp1_op_c : BitVec 12 := BitVec.ofNat 12 Main[21]
 
 def sp1_addi : SailM Unit := do
-  let op_a := sp1_op_a Main cstrs h_is_real
+  let op_a := sp1_op_a Main
   Sail.writeReg Register.nextPC (Word.toBitVec64 #v[Main[3] + 4, Main[4], Main[5], 0])
-  Sail.write_reg op_a (Word.toBitVec64 #v[Main[25], Main[26], Main[27], Main[28]])
+  Sail.write_reg op_a (Word.toBitVec64 #v[Main[26], Main[27], Main[28], Main[29]])
 
 open Sail
 
 theorem correct_addi
+  (cstrs : (constraints Main).allHold)
+  (h_is_real : Main[30] = 1)
   (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
+  let op_b := sp1_op_b Main
+  let op_a := sp1_op_a Main
+  (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
@@ -73,7 +47,9 @@ theorem correct_addi
     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
-    obtain ⟨ trusted_instr_prop, _, _, c0, c1, c2, c3, _, _, _, _, _, _, _, _, _, _, ⟨ is_U64_a, is_U64_b, _ ⟩⟩ := 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
+
     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
@@ -82,20 +58,24 @@ theorem correct_addi
     apply AddOperation.spec is_U64_b is_U64_c at add_op_cstrs
     obtain ⟨ is_U64_val, is_add ⟩ := add_op_cstrs
     simp at *
-
+    simp [BitVec.ofNatLT_eq_ofNat] at *
     -- 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]
-    rw [BabyBear.add4_into_pc_ofNat (by omega)]
-
-    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])]
+    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]
+      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]
       simp [Word.toBitVec64, Word.toNat]
       rfl
 

SP1Chips/Addw/Constraints.lean

@@ -7,26 +7,23 @@ namespace Addw
 section constraints
 
 -- Generated Lean code for chip AddwChip
-@[irreducible] def constraints (Main : Vector (Fin BB) 37) : SP1ConstraintList :=
-  let E0 : Fin BB := Main[35] - 1
-  let E1 : Fin BB := Main[35] * E0
-  let E2 : Fin BB := Main[31] * 27
-  let E3 : Fin BB := 1 - Main[31]
-  let E4 : Fin BB := E3 * 59
-  let E5 : Fin BB := E2 + E4
-  let E6 : Fin BB := Main[36] - E5
-  let E7 : Fin BB := Main[35] * E6
-  let CS0 : SP1ConstraintList := AddwOperation.constraints #v[Main[15], Main[16], Main[17], Main[18]] #v[Main[25], Main[26], Main[27], Main[28]] { value := #v[Main[32], Main[33]], msb := { msb := Main[34] } } Main[35]
-  let E8 : Fin BB := Main[3] + 4
-  let CS1 : SP1ConstraintList := CPUState.constraints { clk_high := Main[0], clk_16_24 := Main[1], clk_0_16 := Main[2], pc := #v[Main[3], Main[4], Main[5]] } #v[E8, Main[4], Main[5]] 8 Main[35]
-  let E9 : Fin BB := Main[34] * 65535
-  let E10 : Fin BB := Main[34] * 65535
-  let E11 : Fin BB := Main[1] * 65536
-  let E12 : Fin BB := Main[2] + E11
-  let CS2 : SP1ConstraintList := ALUTypeReader.constraints Main[0] E12 #v[Main[3], Main[4], Main[5]] 39 #v[Main[36], 0, 0] #v[Main[32], Main[33], E9, E10] { op_a := Main[6], op_a_memory := { prev_value := #v[Main[7], Main[8], Main[9], Main[10]], access_timestamp := { prev_low := Main[11], diff_low_limb := Main[12] } }, op_a_0 := Main[13], op_b := Main[14], op_b_memory := { prev_value := #v[Main[15], Main[16], Main[17], Main[18]], access_timestamp := { prev_low := Main[19], diff_low_limb := Main[20] } }, op_c := #v[Main[21], Main[22], Main[23], Main[24]], op_c_memory := { prev_value := #v[Main[25], Main[26], Main[27], Main[28]], access_timestamp := { prev_low := Main[29], diff_low_limb := Main[30] } }, imm_c := Main[31] } Main[35]
+@[irreducible] def constraints (Main : Vector (Fin KB) 37) : SP1ConstraintList :=
+  let E0 : Fin KB := Main[36] - 1
+  let E1 : Fin KB := Main[36] * E0
+  let E2 : Fin KB := 4 * Main[31]
+  let E3 : Fin KB := 8 - E2
+  let E4 : Fin KB := 32 * Main[31]
+  let E5 : Fin KB := 59 - E4
+  let CS0 : SP1ConstraintList := AddwOperation.constraints #v[Main[15], Main[16], Main[17], Main[18]] #v[Main[25], Main[26], Main[27], Main[28]] { value := #v[Main[33], Main[34]], msb := { msb := Main[35] } } Main[36]
+  let E6 : Fin KB := Main[3] + 4
+  let CS1 : SP1ConstraintList := CPUState.constraints { clk_high := Main[0], clk_16_24 := Main[1], clk_0_16 := Main[2], pc := #v[Main[3], Main[4], Main[5]] } #v[E6, Main[4], Main[5]] 8 Main[36]
+  let E7 : Fin KB := Main[35] * 65535
+  let E8 : Fin KB := Main[35] * 65535
+  let E9 : Fin KB := Main[1] * 65536
+  let E10 : Fin KB := Main[2] + E9
+  let CS2 : SP1ConstraintList := ALUTypeReader.constraints Main[0] E10 #v[Main[3], Main[4], Main[5]] 39 #v[E3, E5, 0, 0] #v[Main[33], Main[34], E7, E8] { op_a := Main[6], op_a_memory := { prev_value := #v[Main[7], Main[8], Main[9], Main[10]], access_timestamp := { prev_low := Main[11], diff_low_limb := Main[12] } }, op_a_0 := Main[13], op_b := Main[14], op_b_memory := { prev_value := #v[Main[15], Main[16], Main[17], Main[18]], access_timestamp := { prev_low := Main[19], diff_low_limb := Main[20] } }, op_c := #v[Main[21], Main[22], Main[23], Main[24]], op_c_memory := { prev_value := #v[Main[25], Main[26], Main[27], Main[28]], access_timestamp := { prev_low := Main[29], diff_low_limb := Main[30] } }, imm_c := Main[31], is_trusted := Main[32] } Main[36]
   CS0 ++ CS1 ++ CS2 ++ [
     (.assertZero E1),
-    (.assertZero E7),
   ]
 
 end constraints