spec: Typecheck signatures and make all chips pass

spec/memw.typ

@@ -56,4 +56,4 @@ This chip contributes the following to the lookup argument.
 - MEMB chip that deals does a one-byte write to remove old_timestamp from here (uncertain tradeoffs)
 - Compute `base_address[1] + 1` once and have high words of `address_add` as Words
 - Improve overflow trapping somehow so we don't need `LT` (could tie into previous one by checking carry bit of the +1)
-- Adding `μ_sum`/`w2`/`w4`/`write8` multiplicities to the `IS_HALFWORD` lookups may make some GKR things faster if there are known zeroes.
+- Adding `μ_sum`/`w2`/`w4`/`write8` multiplicities to the `IS_HALF` lookups may make some GKR things faster if there are known zeroes.

spec/src/branch.toml

@@ -130,7 +130,7 @@ multiplicity = "μ"
 
 [[constraints.all]]
 kind = "interaction"
-tag = "IS_HALFWORD"
+tag = "IS_HALF"
 input = [["idx", "next_pc_high", "i"]]
 iter = ["i", 0, 2]
 multiplicity = "μ"

spec/src/cpu.toml

@@ -77,8 +77,6 @@ type = "Bit"
 desc = "Whether the instruction is of C type, i.e., whether it is 2 bytes long instead of 4"
 pad = 0
 
-# TODO: Should this just be a word? (CHECK: effect on computation/extension of arg2)
-# TODO: make sure decode correctly extends this (may be zero for unsigned and word_instr?)
 [[variables.input]]
 name = "imm"
 type = "DWordWL"
@@ -619,7 +617,7 @@ iter = ["i", 0, 7]
 kind = "interaction"
 tag = "SHIFT"
 input = [["cast", "arg1", "DWordHL"], ["idx", "arg2", 0], "mp_selector", "signed", "word_instr"]
-output = ["cast", "res", "DWordHL"]
+output = ["cast", "res", "DWordWL"]
 multiplicity = "SHIFT"
 
 [[constraints.alu]]
@@ -629,33 +627,30 @@ input = ["pc", ["*", ["+", ["*", 2, "c_type_instruction"], ["*", 4, ["not", "c_t
 output = ["cast", "res", "DWordWL"]
 cond = "JALR"
 
-# TODO: no types available, so no casting yet
 [[constraints.alu]]
 kind = "interaction"
 tag = "MUL"
-input = ["arg1", "signed", "arg2", "mp_selector", "muldiv_selector"]
-output = "res"
+input = [["cast", "arg1", "DWordHL"], "signed", ["cast", "arg2", "DWordHL"], "mp_selector", "muldiv_selector"]
+output = ["cast", "res", "DWordWL"]
 multiplicity = "MUL"
 
-# TODO: no types available, so no casting yet
 [[constraints.alu]]
 kind = "interaction"
 tag = "DVRM"
-input = ["arg1", "arg2", "signed", "muldiv_selector"]
-output = "res"
+input = [["cast", "arg1", "DWordHL"], ["cast", "arg2", "DWordHL"], "signed", "muldiv_selector"]
+output = ["cast", "res", "DWordWL"]
 multiplicity = "DIVREM"
 
 
 [[constraint_groups]]
 name = "mem"
 prefix = "M"
 
-# TODO: no types available, so no casting yet
 [[constraints.mem]]
 kind = "interaction"
 tag = "MEMW"
-input = [1, ["*", 2, "rs1"], "rv1", ["+", "timestamp", ["cast", 0, "DWordWL"]], 1, 0, 0]
-output = "rv1"
+input = [1, ["*", ["cast", 2, "DWordWL"], "rs1"], ["arr", ["idx", ["cast", "rv1", "DWordWL"], 0], ["idx", ["cast", "rv1", "DWordWL"], 1], 0, 0, 0, 0, 0, 0], ["+", "timestamp", ["cast", 0, "DWordWL"]], 1, 0, 0]
+output = ["arr", ["idx", ["cast", "rv1", "DWordWL"], 0], ["idx", ["cast", "rv1", "DWordWL"], 1], 0, 0, 0, 0, 0, 0]
 multiplicity = "read_register1"
 
 [[constraints.mem]]
@@ -664,12 +659,11 @@ constraint = "$#`!read_register1` => #`rv1[i]` = 0$"
 poly = ["*", ["not", "read_register1"], ["idx", "rv1", "i"]]
 iter = ["i", 0, 2]
 
-# TODO: no types available, so no casting yet
 [[constraints.mem]]
 kind = "interaction"
 tag = "MEMW"
-input = [1, ["*", 2, "rs2"], "rv2", ["+", "timestamp", ["cast", 1, "DWordWL"]], 1, 0, 0]
-output = "rv2"
+input = [1, ["*", ["cast", 2, "DWordWL"], "rs2"], ["arr", ["idx", ["cast", "rv2", "DWordWL"], 0], ["idx", ["cast", "rv2", "DWordWL"], 1], 0, 0, 0, 0, 0, 0], ["+", "timestamp", ["cast", 1, "DWordWL"]], 1, 0, 0]
+output = ["arr", ["idx", ["cast", "rv2", "DWordWL"], 0], ["idx", ["cast", "rv2", "DWordWL"], 1], 0, 0, 0, 0, 0, 0]
 multiplicity = "read_register2"
 
 [[constraints.mem]]
@@ -678,33 +672,30 @@ constraint = "$#`!read_register2` => #`rv2[i]` = 0$"
 poly = ["*", ["not", "read_register2"], ["idx", "rv2", "i"]]
 iter = ["i", 0, 2]
 
-# TODO: no types available, so no casting yet
 [[constraints.mem]]
 kind = "interaction"
 tag = "MEMW"
-input = [1, ["*", 2, "rd"], "rvd", ["+", "timestamp", ["cast", 2, "DWordWL"]], 1, 0, 0]
+input = [1, ["*", ["cast", 2, "DWordWL"], "rd"], ["arr", ["idx", "rvd", 0], ["idx", "rvd", 1], 0, 0, 0, 0, 0, 0], ["+", "timestamp", ["cast", 2, "DWordWL"]], 1, 0, 0]
 multiplicity = "write_register"
 
 [[constraints.mem]]
 kind = "interaction"
 tag = "LOAD"
-input = [0, "res", ["+", "timestamp", ["cast", 0, "DWordWL"]], "memory_2bytes", "memory_4bytes", "memory_8bytes", "signed"]
+input = [["cast", "res", "DWordWL"], ["+", "timestamp", ["cast", 0, "DWordWL"]], "memory_2bytes", "memory_4bytes", "memory_8bytes", "signed"]
 output = "rvd"
 multiplicity = "LOAD"
 
-# TODO: no types available, so no casting yet
 [[constraints.mem]]
 kind = "interaction"
 tag = "MEMW"
-input = [0, "res", ["cast", "arg2", ["Byte", 8]], ["+", "timestamp", ["cast", 1, "DWordWL"]], "memory_2bytes", "memory_4bytes", "memory_8bytes"]
+input = [0, ["cast", "res", "DWordWL"], ["cast", "arg2", ["Byte", 8]], ["+", "timestamp", ["cast", 1, "DWordWL"]], "memory_2bytes", "memory_4bytes", "memory_8bytes"]
 multiplicity = "STORE"
 
-# TODO: no types available, so no casting yet
 [[constraints.mem]]
 kind = "interaction"
 tag = "MEMW"
-input = [1, ["*", 2, 255], "next_pc", ["+", "timestamp", ["cast", 1, "DWordWL"]], 1, 0, 0]
-output = "pc"
+input = [1, ["cast", ["*", 2, 255], "DWordWL"], ["arr", ["idx", "next_pc", 0], ["idx", "next_pc", 1], 0, 0, 0, 0, 0, 0], ["+", "timestamp", ["cast", 1, "DWordWL"]], 1, 0, 0]
+output = ["arr", ["idx", "pc", 0], ["idx", "pc", 1], 0, 0, 0, 0, 0, 0]
 multiplicity = ["not", "pad"]
 
 
@@ -817,7 +808,7 @@ poly = ["+",
 [[constraints.misc]]
 kind = "interaction"
 tag = "BRANCH"
-input = ["pc", ["idx", "imm", 0], ["cast", "arg1", "DWordWL"], "JALR"]
+input = ["pc", "imm", ["cast", "arg1", "DWordWL"], "JALR"]
 output = "next_pc"
 multiplicity = "branch_cond"
 

spec/src/halt.toml

@@ -17,31 +17,31 @@ name = "all"
 [[constraints.all]]
 kind = "interaction"
 tag = "MEMW"
-input = [1, ["*", 2, "i"], 0, ["-", ["^", 2, 64], 1], 1, 0, 0]
+input = [1, ["cast", ["*", 2, "i"], "DWordWL"], ["cast", 0, ["BaseField", 8]], ["cast", ["-", ["^", 2, 64], 1], "DWordWL"], 1, 0, 0]
 iter = ["i", 1, 9]
 multiplicity = 1
 ref = "halt:c:zeroize_registers_lo"
 
 [[constraints.all]]
 kind = "interaction"
 tag = "MEMW"
-input = [1, ["*", 2, 10], 0, ["-", ["^", 2, 64], 1], 1, 0, 0]
-output = 0
+input = [1, ["cast", ["*", 2, 10], "DWordWL"], ["cast", 0, ["BaseField", 8]], ["cast", ["-", ["^", 2, 64], 1], "DWordWL"], 1, 0, 0]
+output = ["cast", 0, ["BaseField", 8]]
 multiplicity = 1
 ref = "halt:c:read_zero_exit_code"
 
 [[constraints.all]]
 kind = "interaction"
 tag = "MEMW"
-input = [1, ["*", 2, "i"], 0, ["-", ["^", 2, 64], 1], 1, 0, 0]
+input = [1, ["cast", ["*", 2, "i"], "DWordWL"], ["cast", 0, ["BaseField", 8]], ["cast", ["-", ["^", 2, 64], 1], "DWordWL"], 1, 0, 0]
 iter = ["i", 11, 31]
 multiplicity = 1
 ref = "halt:c:zeroize_registers_hi"
 
 [[constraints.all]]
 kind = "interaction"
 tag = "MEMW"
-input = [1, ["*", 2, 255], 1, ["-", ["^", 2, 64], 1], 1, 0, 0]
+input = [1, ["cast", ["*", 2, 255], "DWordWL"], ["arr", 1, 0, 0, 0, 0, 0, 0, 0], ["cast", ["-", ["^", 2, 64], 1], "DWordWL"], 1, 0, 0]
 multiplicity = 1
 ref = "halt:c:pc"
 
@@ -51,6 +51,6 @@ name = "lookup"
 [[constraints.lookup]]
 kind = "interaction"
 tag = "ECALL"
-input = ["timestamp", 93]
+input = ["timestamp", ["cast", 93, "DWordWL"]]
 multiplicity = ["-", 1]
-ref = "halt:c:lookup"
+ref = "halt:c:lookup"

spec/src/lt.toml

@@ -130,21 +130,21 @@ iter = ["i", 0, 1]
 
 [[constraints.defs]]
 kind = "interaction"
-tag = "IS_HALFWORD"
+tag = "IS_HALF"
 input = [["idx", "lhs", 1]]
 multiplicity = "μ"
 ref = "lt:c:range_lhs"
 
 [[constraints.defs]]
 kind = "interaction"
-tag = "IS_HALFWORD"
+tag = "IS_HALF"
 input = [["idx", "rhs", 1]]
 multiplicity = "μ"
 ref = "lt:c:range_rhs"
 
 [[constraints.sub]]
 kind = "interaction"
-tag = "IS_HALFWORD"
+tag = "IS_HALF"
 input = [["idx", "lhs_sub_rhs", "i"]]
 iter = ["i", 0, 3]
 multiplicity = "μ"

spec/src/memw.toml

@@ -127,29 +127,29 @@ poly = ["*", "w2", ["not", "μ_sum"]]
 [[constraints.consistency]]
 kind = "template"
 tag = "ADD"
-input = ["base_address", 1]
+input = ["base_address", ["cast", 1, "DWordWL"]]
 output = ["cast", ["idx", "address_add", 0], "DWordWL"]
 cond = "w2"
 
 [[constraints.consistency]]
 kind = "template"
 tag = "ADD"
-input = ["base_address", ["+", "i", 1]]
+input = ["base_address", ["cast", ["+", "i", 1], "DWordWL"]]
 output = ["cast", ["idx", "address_add", "i"], "DWordWL"]
 iter = ["i", 1, 2]
 cond = "w4"
 
 [[constraints.consistency]]
 kind = "template"
 tag = "ADD"
-input = ["base_address", ["+", "i", 1]]
+input = ["base_address", ["cast", ["+", "i", 1], "DWordWL"]]
 output = ["cast", ["idx", "address_add", "i"], "DWordWL"]
 iter = ["i", 3, 6]
 cond = "write8"
 
 [[constraints.consistency]]
 kind = "interaction"
-tag = "IS_HALFWORD"
+tag = "IS_HALF"
 input = [["idx", ["idx", "address_add", "i"], "j"]]
 iters = [
   ["i", 0, 0],
@@ -159,7 +159,7 @@ multiplicity = "w2"
 
 [[constraints.consistency]]
 kind = "interaction"
-tag = "IS_HALFWORD"
+tag = "IS_HALF"
 input = [["idx", ["idx", "address_add", "i"], "j"]]
 iters = [
   ["i", 1, 2],
@@ -169,7 +169,7 @@ multiplicity = "w4"
 
 [[constraints.consistency]]
 kind = "interaction"
-tag = "IS_HALFWORD"
+tag = "IS_HALF"
 input = [["idx", ["idx", "address_add", "i"], "j"]]
 iters = [
   ["i", 3, 6],
@@ -253,40 +253,40 @@ multiplicity = ["-", "μ_sum"]
 [[constraints.memory]]
 kind = "interaction"
 tag = "memory"
-input = ["is_register", ["idx", "address_add", 0], ["idx", "old_timestamp", 1], ["idx", "old", 1]]
+input = ["is_register", ["cast", ["idx", "address_add", 0], "DWordWL"], ["idx", "old_timestamp", 1], ["idx", "old", 1]]
 multiplicity = "w2"
 
 [[constraints.memory]]
 kind = "interaction"
 tag = "memory"
-input = ["is_register", ["idx", "address_add", 0], "timestamp", ["idx", "value", 1]]
+input = ["is_register", ["cast", ["idx", "address_add", 0], "DWordWL"], "timestamp", ["idx", "value", 1]]
 multiplicity = ["-", "w2"]
 
 [[constraints.memory]]
 kind = "interaction"
 tag = "memory"
-input = ["is_register", ["idx", "address_add", ["-", "i", 1]], ["idx", "old_timestamp", "i"], ["idx", "old", "i"]]
+input = ["is_register", ["cast", ["idx", "address_add", ["-", "i", 1]], "DWordWL"], ["idx", "old_timestamp", "i"], ["idx", "old", "i"]]
 multiplicity = "w4"
 iter = ["i", 2, 3]
 
 [[constraints.memory]]
 kind = "interaction"
 tag = "memory"
-input = ["is_register", ["idx", "address_add", ["-", "i", 1]], "timestamp", ["idx", "value", "i"]]
+input = ["is_register", ["cast", ["idx", "address_add", ["-", "i", 1]], "DWordWL"], "timestamp", ["idx", "value", "i"]]
 multiplicity = ["-", "w4"]
 iter = ["i", 2, 3]
 
 [[constraints.memory]]
 kind = "interaction"
 tag = "memory"
-input = ["is_register", ["idx", "address_add", ["-", "i", 1]], ["idx", "old_timestamp", "i"], ["idx", "old", "i"]]
+input = ["is_register", ["cast", ["idx", "address_add", ["-", "i", 1]], "DWordWL"], ["idx", "old_timestamp", "i"], ["idx", "old", "i"]]
 multiplicity = "write8"
 iter = ["i", 4, 7]
 
 [[constraints.memory]]
 kind = "interaction"
 tag = "memory"
-input = ["is_register", ["idx", "address_add", ["-", "i", 1]], "timestamp", ["idx", "value", "i"]]
+input = ["is_register", ["cast", ["idx", "address_add", ["-", "i", 1]], "DWordWL"], "timestamp", ["idx", "value", "i"]]
 multiplicity = ["-", "write8"]
 iter = ["i", 4, 7]
 

spec/src/page.toml

@@ -55,7 +55,7 @@ multiplicity = 1
 [[constraints.all]]
 kind = "interaction"
 tag = "memory"
-input = [0, "address", 0, "init"]
+input = [0, "address", ["cast", 0, "DWordWL"], "init"]
 multiplicity = -1
 
 [[constraints.all]]

spec/src/shift.toml

@@ -133,7 +133,7 @@ pad = 0
 # Assumptions
 
 [[assumptions]]
-desc = "`IS_HALFWORD[in[i]]`"
+desc = "`IS_HALF[in[i]]`"
 iter = ["i", 0, 3]
 ref = "shift:a:range_in"
 

spec/src/signatures.toml

@@ -53,7 +53,7 @@ output = "DWordWL"
 [[signatures]]
 tag = "BRANCH"
 kind = "interaction"
-input = ["DWordWL", "Word", "DWordWL", "Bit"]
+input = ["DWordWL", "DWordWL", "DWordWL", "Bit"]
 output = "DWordWL"
 
 # MEMW[old; is_register, base_address, value, timestamp, write2, write4, write8]
@@ -175,4 +175,10 @@ output = "Half"
 tag = "HWSLC"
 kind = "interaction"
 input = ["Half", "B4"]
-output = "Half"
+output = "Half"
+
+# The actual memory tokens, see MEMW and PAGE
+[[signatures]]
+tag = "memory"
+kind = "interaction"
+input = ["Bit", "DWordWL", "DWordWL", "BaseField"]