feat: sync constraints for UType (AUIPC/LUI)

Author: GZGavinZhao

SP1Chips.lean

@@ -15,6 +15,8 @@ import SP1Chips.Lt.Constraints
 import SP1Chips.LtChip
 import SP1Chips.Mul.Constraints
 import SP1Chips.MulChip
+import SP1Chips.UType.Constraints
+import SP1Chips.UTypeChip
 import SP1Chips.ShiftLeft.Constraints
 import SP1Chips.ShiftLeftChip
 import SP1Chips.ShiftRight.Constraints

SP1Chips/UType/Constraints.lean

@@ -0,0 +1,70 @@
+import SP1Operations.Reader.CPUState
+import SP1Operations.Reader.JTypeReader
+import SP1Operations.Operation.AddOperation
+
+namespace UType
+
+section constraints
+
+-- Generated Lean code for chip UTypeChip
+def constraints (Main : Vector (Fin BB) 31) : SP1ConstraintList :=
+  let E0 : Fin BB := Main[30] - 1
+  let E1 : Fin BB := Main[30] * E0
+  let E2 : Fin BB := Main[29] - 1
+  let E3 : Fin BB := Main[29] * E2
+  let E4 : Fin BB := Main[29] * 35
+  let E5 : Fin BB := 1 - Main[29]
+  let E6 : Fin BB := E5 * 36
+  let E7 : Fin BB := E4 + E6
+  let E8 : Fin BB := 1 - Main[29]
+  let E9 : Fin BB := Main[29] * 0
+  let E10 : Fin BB := E8 * 0
+  let E11 : Fin BB := E9 + E10
+  let E12 : Fin BB := Main[29] * 0
+  let E13 : Fin BB := E8 * 0
+  let E14 : Fin BB := E12 + E13
+  let E15 : Fin BB := Main[29] * 23
+  let E16 : Fin BB := E8 * 55
+  let E17 : Fin BB := E15 + E16
+  let E18 : Fin BB := Main[3] + 4
+  let CS0 : 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[E18, Main[4], Main[5]] 8 Main[30]
+  let E19 : Fin BB := Main[29] * Main[3]
+  let E20 : Fin BB := 1 - Main[29]
+  let E21 : Fin BB := E20 * 0
+  let E22 : Fin BB := E19 + E21
+  let E23 : Fin BB := Main[29] * Main[4]
+  let E24 : Fin BB := 1 - Main[29]
+  let E25 : Fin BB := E24 * 0
+  let E26 : Fin BB := E23 + E25
+  let E27 : Fin BB := Main[29] * Main[5]
+  let E28 : Fin BB := 1 - Main[29]
+  let E29 : Fin BB := E28 * 0
+  let E30 : Fin BB := E27 + E29
+  let E31 : Fin BB := Main[29] * 0
+  let E32 : Fin BB := 1 - Main[29]
+  let E33 : Fin BB := E32 * 0
+  let E34 : Fin BB := E31 + E33
+  let E35 : Fin BB := Main[22] - E22
+  let E36 : Fin BB := Main[23] - E26
+  let E37 : Fin BB := Main[24] - E30
+  let E38 : Fin BB := 0 - E34
+  let E39 : Fin BB := Main[30] - 1
+  let E40 : Fin BB := E39 * Main[13]
+  let E41 : Fin BB := Main[30] - Main[13]
+  let CS1 : SP1ConstraintList := AddOperation.constraints #v[Main[22], Main[23], Main[24], 0] #v[Main[14], Main[15], Main[16], Main[17]] { value := #v[Main[25], Main[26], Main[27], Main[28]] } E41
+  let E42 : Fin BB := Main[1] * 65536
+  let E43 : Fin BB := Main[2] + E42
+  let CS2 : SP1ConstraintList := JTypeReader.constraints Main[0] E43 #v[Main[3], Main[4], Main[5]] E7 #v[E17, E11, E14] #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_imm := #v[Main[14], Main[15], Main[16], Main[17]], op_c_imm := #v[Main[18], Main[19], Main[20], Main[21]] } Main[30]
+  CS0 ++ CS1 ++ CS2 ++ [
+    (.assertZero E1),
+    (.assertZero E3),
+    (.assertZero E35),
+    (.assertZero E36),
+    (.assertZero E37),
+    (.assertZero E38),
+    (.assertZero E40),
+  ]
+
+end constraints
+
+end UType

SP1Chips/UTypeChip.lean

@@ -0,0 +1 @@
+import SP1Chips.UType.Constraints

SP1Operations.lean

@@ -56,6 +56,8 @@ import SP1Operations.Reader.ITypeReader
 import SP1Operations.Reader.ITypeReader.Constraints
 import SP1Operations.Reader.ITypeReader.Operation
 import SP1Operations.Reader.JTypeReader
+import SP1Operations.Reader.JTypeReader.Constraints
+import SP1Operations.Reader.JTypeReader.Operation
 import SP1Operations.Reader.RTypeReader
 import SP1Operations.Reader.RTypeReader.Constraints
 import SP1Operations.Reader.RTypeReader.Operation

SP1Operations/Reader/JTypeReader.lean

@@ -1,14 +1,2 @@
--- import SP1Foundations
--- import SP1Operations.MemoryConsistency
--- import LeanRV32IM.RiscvRegs
-
--- open Sail
--- open LeanRV32IM.Functions
-
--- --- A Reader that only accesses values of type `T`.
--- structure JTypeReader (T : Type) where
---   op_a : T
---   op_a_memory : MemoryAccessInSharedCols
---   op_a_0 : T
---   op_b_imm : Word T
---   op_c_imm : Word T
+import SP1Operations.Reader.JTypeReader.Operation
+import SP1Operations.Reader.JTypeReader.Constraints

SP1Operations/Reader/JTypeReader/Constraints.lean

@@ -0,0 +1,52 @@
+import SP1Operations.Reader.JTypeReader.Operation
+
+namespace JTypeReader
+
+set_option linter.unusedVariables false
+-- Generated Lean code for operation JTypeReader (from chip Add)
+section constraints
+
+def constraints
+  (clk_high : (Fin BB))
+  (clk_low : (Fin BB))
+  (pc : (Vector (Fin BB) 3))
+  (opcode : (Fin BB))
+  (instr_field_consts : (Vector (Fin BB) 3))
+  (op_a_write_value : (Word (Fin BB)))
+  (cols : JTypeReader)
+  (is_real : (Fin BB))
+  : SP1ConstraintList :=
+  let E0 : Fin BB := is_real - 1
+  let E1 : Fin BB := is_real * E0
+  let E2 : Fin BB := op_a_write_value[0] - 0
+  let E3 : Fin BB := cols.op_a_0 * E2
+  let E4 : Fin BB := op_a_write_value[1] - 0
+  let E5 : Fin BB := cols.op_a_0 * E4
+  let E6 : Fin BB := op_a_write_value[2] - 0
+  let E7 : Fin BB := cols.op_a_0 * E6
+  let E8 : Fin BB := op_a_write_value[3] - 0
+  let E9 : Fin BB := cols.op_a_0 * E8
+  let E10 : Fin BB := clk_low + 3
+  let E11 : Fin BB := is_real - 1
+  let E12 : Fin BB := is_real * E11
+  let E13 : Fin BB := E10 - cols.op_a_memory.access_timestamp.prev_low
+  let E14 : Fin BB := E13 - 1
+  let E15 : Fin BB := E14 - cols.op_a_memory.access_timestamp.diff_low_limb
+  let E16 : Fin BB := E15 * 2013235201
+  [
+    (.assertZero E1),
+    (.send (.program pc[0] pc[1] pc[2] (Opcode.ofNat opcode) cols.op_a cols.op_b_imm[0] cols.op_b_imm[1] cols.op_b_imm[2] cols.op_b_imm[3] cols.op_c_imm[0] cols.op_c_imm[1] cols.op_c_imm[2] cols.op_c_imm[3] cols.op_a_0 1 1 instr_field_consts[0] instr_field_consts[1] instr_field_consts[2]) is_real),
+    (.assertZero E3),
+    (.assertZero E5),
+    (.assertZero E7),
+    (.assertZero E9),
+    (.assertZero E12),
+    (.send (.byte (ByteOpcode.ofNat 6) cols.op_a_memory.access_timestamp.diff_low_limb 16 0) is_real),
+    (.send (.byte (ByteOpcode.ofNat 3) 0 E16 0) is_real),
+    (.send (.memory clk_high cols.op_a_memory.access_timestamp.prev_low cols.op_a 0 0 cols.op_a_memory.prev_value[0] cols.op_a_memory.prev_value[1] cols.op_a_memory.prev_value[2] cols.op_a_memory.prev_value[3]) is_real),
+    (.receive (.memory clk_high E10 cols.op_a 0 0 op_a_write_value[0] op_a_write_value[1] op_a_write_value[2] op_a_write_value[3]) is_real),
+  ]
+
+end constraints
+
+end JTypeReader

SP1Operations/Reader/JTypeReader/Operation.lean

@@ -0,0 +1,9 @@
+import SP1Foundations
+
+--- A Reader that only accesses values of type `T`.
+structure JTypeReader where
+  op_a : Fin BB
+  op_a_memory : MemoryAccessInSharedCols
+  op_a_0 : Fin BB
+  op_b_imm : Word (Fin BB)
+  op_c_imm : Word (Fin BB)

update_constraints.py

@@ -23,6 +23,7 @@
     ("Mul", None, ""),
     ("Sub", None, ""),
     ("Subw", None, ""),
+    ("UType", None, ""),
 
     # Operations
     ("Add", "AddOperation", "Operation"),
@@ -49,6 +50,7 @@
     ("Add", "CPUState", "Reader"),
     ("Addi", "ITypeReader", "Reader"),
     ("Bitwise", "ALUTypeReader", "Reader"),
+    ("UType", "JTypeReader", "Reader"),
 ]
 
 def run_constraint_compiler(sp1_dir: str, chip: str, operation: Optional[str] = None) -> str: