spec: Add initial tooling to check data formats, prepare for more elaborate type checking

spec/chip.typ

@@ -113,7 +113,6 @@
     }
 
     if "poly" in def {
-      // assert(false, message: repr(index_all(var_name, gather_indices(def))))
       (
         [],
         table.cell(align: right, emph[definition]), 

spec/memory.typ

@@ -229,3 +229,4 @@ add the required balancing terms to the LogUp sum.
 = Future topics of interest
 
 - Optimize memory systems after determining factual bottlenecks (e.g. taking inspiration from Twist and Shout, or other recent research)
+- Double check whether IS_BYTE constraints are needed for fini

spec/src/bitwise.toml

@@ -4,67 +4,67 @@ name = "BITWISE"
 name = "X"
 type = "Byte"
 desc = ""
-precomputed = "true"
+precomputed = true
 
 [[variables.input]]
 name = "Y"
 type = "Byte"
 desc = ""
-precomputed = "true"
+precomputed = true
 
 [[variables.input]]
 name = "Z"
 type = "B4"
 desc = ""
-precomputed = "true"
+precomputed = true
 
 [[variables.output]]
 name = "AND"
 type = "Byte"
 desc = "the binary AND of `X` and `Y`"
-precomputed = "true"
+precomputed = true
 
 [[variables.output]]
 name = "OR"
 type = "Byte"
 desc = "the binary OR of `X` and `Y`"
-precomputed = "true"
+precomputed = true
 
 [[variables.output]]
 name = "XOR"
 type = "Byte"
 desc = "the binary XOR of `X` and `Y`"
-precomputed = "true"
+precomputed = true
 
 [[variables.output]]
 name = "MSB8"
 type = "Bit"
 desc = "the most significant bit of `X`"
-precomputed = "true"
+precomputed = true
 
 [[variables.output]]
 name = "MSB16"
 type = "Bit"
 desc = "the most significant bit of `Y`"
-precomputed = "true"
+precomputed = true
 
 [[variables.output]]
 name = "ZERO"
 type = "Bit"
 desc = "whether $#`X` = 0$, $#`Y` = 0$ and $#`Z` = 0$."
-precomputed = "true"
+precomputed = true
 
 [[variables.output]]
 name = "SLL"
 type = "Half"
 desc = "`X||Y` logically left-shifted by `Z`: $((#`X` + 256#`Y`) #`<<` #`Z`) mod 2^16$"
-precomputed = "true"
+precomputed = true
 
 [[variables.output]]
 name = "SLLC"
 type = "Half"
 desc = "`X||Y` logically right-shifted by `Z`: $(#`X` + 256#`Y`) #`>>` (16 - #`Z`)$"
-precomputed = "true"
+precomputed = true
 
 [[variables.multiplicity]]
 name = "μ_AND"
@@ -197,4 +197,4 @@ kind = "interaction"
 tag = "HWSLC"
 input = [["+", "X", ["*", 256, "Y"]], "Z"]
 output = "SLLC"
-multiplicity = ["-", "μ_HWSLC"]
+multiplicity = ["-", "μ_HWSLC"]

spec/src/branch.toml

@@ -11,7 +11,7 @@ pad = 0
 
 [[variables.input]]
 name = "offset"
-type = "Word"
+type = "DWordWL"
 desc = "The offset from the base address to jump to"
 pad = 0
 
@@ -59,7 +59,7 @@ name = "next_pc_unmasked"
 type = "DWordWL"
 desc = "The combination of `next_pc_high`, `next_pc_low[1]` and `unmasked_low_byte` to constrain the addition. This is the computed value for the next pc, before masking off the LSB as required by the ISA."
 def = {idx = "i", polys = [
-  {iter = 0, poly = ["+", ["*", ["^", 2, 16], ["idx", "next_pc_high", 0]], ["*", ["^", 2, 8], ["idx", "next_pc_low", 1]], ["idx", "unmasked_low_byte", 0]]},
+  {iter = 0, poly = ["+", ["*", ["^", 2, 16], ["idx", "next_pc_high", 0]], ["*", ["^", 2, 8], ["idx", "next_pc_low", 1]], "unmasked_low_byte"]},
   {iter = 1, poly = ["+", ["*", ["^", 2, 16], ["idx", "next_pc_high", 2]], ["idx", "next_pc_high", 1]]},
 ]}
 
@@ -124,7 +124,7 @@ multiplicity = "μ"
 [[constraints.all]]
 kind = "interaction"
 tag = "AND_BYTE"
-input = [["idx", "unmasked_low_byte", 0], 254]
+input = ["unmasked_low_byte", 254]
 output = ["idx", "next_pc_low", 0]
 multiplicity = "μ"
 
@@ -145,4 +145,4 @@ kind = "interaction"
 tag = "BRANCH"
 input = ["pc", "offset", "register", "JALR"]
 output = "next_pc"
-multiplicity = "-μ"
+multiplicity = ["-", "μ"]

spec/src/config.toml

@@ -4,63 +4,49 @@ version = 1
 [[variables.types]]
 label = "BaseField"
 subtypes = ["BaseField"]
+range = [0, "18446744069414584320"]
 desc = "Variable that can assume any value in the base field."
 
 [[variables.types]]
 label = "Bit"
 subtypes = ["BaseField"]
+range = [0, 1]
 desc = "Variable that can only assume values in the set ${0,1}$."
 
 [[variables.types]]
 label = "B4"
 subtypes = ["BaseField"]
+range = [0, 15]
 desc = "Variable that can only assume values in the range $[0, 2^4)$."
 
 [[variables.types]]
 label = "Byte"
 subtypes = ["BaseField"]
-count = 1
+range = [0, 255]
 desc = "Variable that can only assume values in the range $[0, 2^8)$."
 
 [[variables.types]]
 label = "Half"
 subtypes = ["BaseField"]
+range = [0, 65535]
 desc = "Variable that can only assume values in the range $[0, 2^16)$."
 
 [[variables.types]]
 label = "B20"
 subtypes = ["BaseField"]
+range = [0, 1048575]
 desc = "Variable that can only assume values in the range $[0, 2^20)$."
 
 [[variables.types]]
 label = "Word"
 subtypes = ["BaseField"]
+range = [0, 4294967295]
 desc = "Variable that can only assume values in the range $[0, 2^32)$."
 
-[[variables.types]]
-label = "WordHL"
-subtypes = ["Half", "Half"]
-desc = """\
-       Variable that can only assume values in the range $[0, 2^32)$. \\
-       Represented as an array of two `Half` variables.\
-       """
-
-[[variables.types]]
-label = "WordBL"
-subtypes = ["Byte", "Byte", "Byte", "Byte"]
-desc = """\
-       Variable that can only assume values in the range $[0, 2^32)$. \\
-       Represented as an array of four `Byte` variables.\
-       """
-
-[[variables.types]]
-label = "B35"
-subtypes = ["BaseField"]
-desc = "Variable that can only assume values in the range $[0, 2^35)$."
-
 [[variables.types]]
 label = "B51"
 subtypes = ["BaseField"]
+range = [0, 2251799813685247]
 desc = "Variable that can only assume values in the range $[0, 2^51)$."
 
 [[variables.types]]
@@ -96,6 +82,15 @@ desc = """\
        The `Word` is the *least* significant digit.
        """
 
+[[variables.types]]
+label = "DWordWHH"
+subtypes = ["Half", "Half", "Word"]
+desc = """\
+       Variable that can only assume values in the range $[0, 2^64)$. \\
+       Represented as a `Word` and two `Half` variables.\
+       The `Word` is the *most* significant digit.
+       """
+
 [[variables.types]]
 label = "QuadHL"
 subtypes = ["Half", "Half", "Half", "Half", "Half", "Half", "Half", "Half"]
@@ -112,15 +107,6 @@ desc = """\
        Represented as an array of four `Word` variables.\
        """
 
-[[variables.types]]
-label = "DWordWHH"
-subtypes = ["Half", "Half", "Word"]
-desc = """\
-       Variable that can only assume values in the range $[0, 2^64)$. \\
-       Represented as a `Word` and two `Half` variables.\
-       The `Word` is the *most* significant digit.
-       """
-
 [[variables.types]]
 label = "Timestamp"
 subtypes = ["DWordWL"]

spec/src/cpu.toml

@@ -343,6 +343,7 @@ name = "decode"
 kind = "interaction"
 tag = "DECODE"
 input = ["pc", "imm", "packed_decode"]
+multiplicity = 1
 
 
 [[constraint_groups]]
@@ -515,34 +516,40 @@ ref = "cpu:c:range_EBREAK"
 kind = "interaction"
 tag = "IS_BYTE"
 input = ["rs1"]
+multiplicity = 1
 
 [[constraints.range]]
 kind = "interaction"
 tag = "IS_BYTE"
 input = ["rs2"]
+multiplicity = 1
 
 [[constraints.range]]
 kind = "interaction"
 tag = "IS_BYTE"
 input = ["rd"]
+multiplicity = 1
 
 [[constraints.range]]
 kind = "interaction"
 tag = "IS_BYTE"
 input = [["idx", "arg1", "i"]]
 iter = ["i", 0, 7]
+multiplicity = 1
 
 [[constraints.range]]
 kind = "interaction"
 tag = "IS_BYTE"
 input = [["idx", "arg2", "i"]]
 iter = ["i", 0, 7]
+multiplicity = 1
 
 [[constraints.range]]
 kind = "interaction"
 tag = "IS_BYTE"
 input = [["idx", "res", "i"]]
 iter = ["i", 0, 7]
+multiplicity = 1
 
 
 [[constraint_groups]]
@@ -611,7 +618,7 @@ multiplicity = "SHIFT"
 [[constraints.alu]]
 kind = "template"
 tag = "ADD"
-input = ["pc", ["cast", ["+", ["*", 2, "c_type_instruction"], ["*", 4, ["not", "c_type_instruction"]]], "DWordWL"]]
+input = ["pc", ["*", ["+", ["*", 2, "c_type_instruction"], ["*", 4, ["not", "c_type_instruction"]]], ["cast", 1, "DWordWL"]]]
 output = ["cast", "res", "DWordWL"]
 cond = "JALR"
 
@@ -640,7 +647,7 @@ prefix = "M"
 [[constraints.mem]]
 kind = "interaction"
 tag = "MEMW"
-input = [1, ["*", 2, "rs1"], "rv1", ["+", "timestamp", 0], 1, 0, 0]
+input = [1, ["*", 2, "rs1"], "rv1", ["+", "timestamp", ["cast", 0, "DWordWL"]], 1, 0, 0]
 output = "rv1"
 multiplicity = "read_register1"
 
@@ -654,7 +661,7 @@ iter = ["i", 0, 2]
 [[constraints.mem]]
 kind = "interaction"
 tag = "MEMW"
-input = [1, ["*", 2, "rs2"], "rv2", ["+", "timestamp", 1], 1, 0, 0]
+input = [1, ["*", 2, "rs2"], "rv2", ["+", "timestamp", ["cast", 1, "DWordWL"]], 1, 0, 0]
 output = "rv2"
 multiplicity = "read_register2"
 
@@ -668,28 +675,28 @@ iter = ["i", 0, 2]
 [[constraints.mem]]
 kind = "interaction"
 tag = "MEMW"
-input = [1, ["*", 2, "rd"], "rvd", ["+", "timestamp", 2], 1, 0, 0]
+input = [1, ["*", 2, "rd"], "rvd", ["+", "timestamp", ["cast", 2, "DWordWL"]], 1, 0, 0]
 multiplicity = "write_register"
 
 [[constraints.mem]]
 kind = "interaction"
 tag = "LOAD"
-input = [0, "res", ["+", "timestamp", 0], "memory_2bytes", "memory_4bytes", "memory_8bytes", "signed"]
+input = [0, "res", ["+", "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", "rv2", ["+", "timestamp", 1], "memory_2bytes", "memory_4bytes", "memory_8bytes"]
+input = [0, "res", "rv2", ["+", "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", 1], 1, 0, 0]
+input = [1, ["*", 2, 255], "next_pc", ["+", "timestamp", ["cast", 1, "DWordWL"]], 1, 0, 0]
 output = "pc"
 multiplicity = ["not", "pad"]
 
@@ -795,7 +802,7 @@ poly = ["+",
         ["-", "branch_cond"],
         "JALR",
         ["*", ["idx", "res", 0], ["not", "mp_selector"], "BLT"],
-        ["*", ["not", ["idx", "res", 0]], "mp_selector", "BLT"],
+        ["*", ["-", 1, ["idx", "res", 0]], "mp_selector", "BLT"],
         ["*", "is_equal", ["not", "mp_selector"], "BEQ"],
         ["*", ["not", "is_equal"], "mp_selector", "BEQ"]
     ]
@@ -810,6 +817,6 @@ multiplicity = "branch_cond"
 [[constraints.misc]]
 kind = "template"
 tag = "ADD"
-input = ["pc", ["cast", ["+", ["*", 2, "c_type_instruction"], ["*", 4, ["not", "c_type_instruction"]]], "DWordWL"]]
+input = ["pc", ["*", ["+", ["*", 2, "c_type_instruction"], ["*", 4, ["not", "c_type_instruction"]]], ["cast", 1, "DWordWL"]]]
 output = "next_pc"
 desc = "Increment `pc` to `next_pc` if we're not branching"

spec/src/dvrm.toml

@@ -376,13 +376,13 @@ desc = "Each row contributes the following to the LogUp sum"
 [[constraints.output]]
 kind = "interaction"
 tag = "DVRM"
-input = ["n", "d", "signed", "0"]
+input = ["n", "d", "signed", 0]
 output = ["cast", "q", "DWordWL"]
-multiplicity = "-μ_q"
+multiplicity = ["-", "μ_q"]
 
 [[constraints.output]]
 kind = "interaction"
 tag = "DVRM"
-input = ["n", "d", "signed", "1"]
+input = ["n", "d", "signed", 1]
 output = ["cast", "r", "DWordWL"]
-multiplicity = "-μ_r"
+multiplicity = ["-", "μ_r"]

spec/src/is_bit.toml

@@ -16,5 +16,5 @@ name = "all"
 [[constraints.all]]
 kind = "arith"
 constraint = "$#`cond` => #`X` (1-#`X`) = 0$"
-poly = ["*", "cond", "X", ["not", "X"]]
+poly = ["*", "cond", "X", ["-", 1, "X"]]
 ref = "isbit:c:isbit"

spec/src/lt.toml

@@ -160,4 +160,4 @@ kind = "interaction"
 tag = "LT"
 input = [["cast", "lhs", "DWordWL"], ["cast", "rhs", "DWordWL"], "signed"]
 output = "lt"
-multiplicity = "-μ"
+multiplicity = ["-", "μ"]