spec: LOAD chip

spec/book.typ

@@ -13,6 +13,7 @@
     #chapter("branch.typ")[BRANCH]
     #chapter("lt.typ")[LT]
     #chapter("mul.typ")[MUL chip]
+    #chapter("load.typ")[LOAD chip]
     #chapter("bitwise.typ")[BITWISE]
   ]
 )

spec/load.typ

@@ -0,0 +1,42 @@
+#import "/book.typ": book-page, rj
+#import "/src.typ": load_config, load_chip
+#import "/chip.typ": (
+  render_chip_assumptions,
+  render_chip_column_table,
+  render_chip_padding_table,
+  render_constraint_table,
+  total_nr_instantiated_columns,
+  total_nr_variables,
+)
+
+#let config = load_config()
+#let chip = load_chip("src/load.toml", config)
+
+#show: book-page.with(title: "LOAD chip")
+
+== Columns
+#let nr_variables = total_nr_variables(chip)
+#let nr_columns = total_nr_instantiated_columns(chip, config)
+
+The `LOAD` chip is comprised of #nr_variables variables that are expressed using #nr_columns columns:
+#render_chip_column_table(chip, config)
+
+== Assumptions
+#render_chip_assumptions(chip, config)
+
+== Constraints
+The chip delegates the actual memory interaction to the `MEMW` chip,
+and ensures correctness of the requested sign/zero extension.
+The output `res` is correctly range-checked as long as the memory contents are.
+
+#render_constraint_table(chip, config, groups: "all")
+
+The chip contributes the following to the lookup argument.
+
+#render_constraint_table(chip, config, groups: "output")
+
+== Padding
+
+The table can be padded to the next power of two with the following value assignments:
+
+#render_chip_padding_table(chip, config)

spec/src/cpu.toml

@@ -582,7 +582,6 @@ kind = "interaction"
 tag = "MEMW"
 input = [1, ["*", 2, "rd"], "rvd", ["+", "timestamp", 2], 1, 0, 0]
 
-# TODO: no types available, so no casting yet
 [[constraints.mem]]
 kind = "interaction"
 tag = "LOAD"

spec/src/load.toml

@@ -0,0 +1,160 @@
+name = "LOAD"
+
+# Input
+
+[[variables.input]]
+name = "base_address"
+type = "DWordWL"
+desc = "The base address to read/write from/to, gets offset by $[0, 7]$, depending on how big the access is"
+pad = 0
+
+[[variables.input]]
+name = "timestamp"
+type = "DWordWL"
+desc = "The timestamp at which this memory access is said to occur"
+pad = 0
+
+[[variables.input]]
+name = "read2"
+type = "Bit"
+desc = "Whether to read exactly 2 bytes"
+pad = 0
+
+[[variables.input]]
+name = "read4"
+type = "Bit"
+desc = "Whether to read exactly 4 bytes"
+pad = 0
+
+[[variables.input]]
+name = "read8"
+type = "Bit"
+desc = "Whether to read exactly 8 bytes"
+pad = 0
+
+[[variables.input]]
+name = "signed"
+type = "Bit"
+desc = "Whether to sign-extend (1) or zero-extend (0)"
+pad = 0
+
+# Output
+
+[[variables.output]]
+name = "res"
+type = "DWordBL"
+desc = "The result of reading (up to) 8 bytes from `base_address`, extended corresponding to `signed`."
+pad = 0
+
+# Auxiliary
+
+[[variables.auxiliary]]
+name = "sign_bit"
+type = "Bit"
+desc = "The sign bit extracted from the bytes retrieved from memory"
+pad = 0
+
+# Virtual
+
+[[variables.virtual]]
+name = "read1"
+type = "Bit"
+desc = "Whether to read exactly 1 byte"
+def = ["-", "μ", "read2", "read4", "read8"]
+
+# Multiplicity
+
+[[variables.multiplicity]]
+name = "μ"
+type = "Bit"
+desc = ""
+pad = 0
+
+
+[[assumptions]]
+desc = "`IS_WORD[base_address[i]]`"
+iter = ["i", 0, 1]
+
+[[assumptions]]
+desc = "`IS_BIT<signed>`"
+
+[[assumptions]]
+desc = "`IS_BIT<read2>`"
+
+[[assumptions]]
+desc = "`IS_BIT<read4>`"
+
+[[assumptions]]
+desc = "`IS_BIT<read8>`"
+
+[[assumptions]]
+desc = "`IS_BIT<read2 + read4 + read8>`"
+
+[[assumptions]]
+desc = "`IS_WORD[timestamp[i]]`"
+iter = ["i", 0, 1]
+
+
+[[constraint_groups]]
+name = "all"
+
+[[constraints.all]]
+kind = "arith"
+constraint = "$#`read2` + #`read4` + #`read8` => #`μ`$"
+poly = ["*", ["+", "read2", "read4", "read8"], ["not", "μ"]]
+
+[[constraints.all]]
+kind = "interaction"
+tag = "MEMW"
+input = [0, "base_address", ["cast", "res", ["BaseField", 8]], "timestamp", "read2", "read4", "read8"]
+output = "res"
+multiplicity = "μ"
+
+[[constraints.all]]
+kind = "interaction"
+tag = "MSB8"
+input = [["idx", "res", 0]]
+output = "sign_bit"
+multiplicity = "read1"
+
+[[constraints.all]]
+kind = "interaction"
+tag = "MSB8"
+input = [["idx", "res", 1]]
+output = "sign_bit"
+multiplicity = "read2"
+
+[[constraints.all]]
+kind = "interaction"
+tag = "MSB8"
+input = [["idx", "res", 3]]
+output = "sign_bit"
+multiplicity = "read4"
+
+[[constraints.all]]
+kind = "arith"
+constraint = "$!#`read8` => #`res`_i = #`signed` dot #`sign_bit` dot 255$"
+poly = ["*", ["not", "read8"], ["-", ["idx", "res", "i"], ["*", "signed", "sign_bit", 255]]]
+iter = ["i", 4, 7]
+
+[[constraints.all]]
+kind = "arith"
+constraint = "$!(#`read4` + #`read8`) => #`res`_i = #`signed` dot #`sign_bit` dot 255$"
+poly = ["*", ["-", 1, "read4", "read8"], ["-", ["idx", "res", "i"], ["*", "signed", "sign_bit", 255]]]
+iter = ["i", 2, 3]
+
+[[constraints.all]]
+kind = "arith"
+constraint = "$!(#`read2` + #`read4` + #`read8`) => #`res`_1 = #`signed` dot #`sign_bit` dot 255$"
+poly = ["*", ["-", 1, "read2", "read4", "read8"], ["-", ["idx", "res", 1], ["*", "signed", "sign_bit", 255]]]
+
+
+[[constraint_groups]]
+name = "output"
+
+[[constraints.output]]
+kind = "interaction"
+tag = "LOAD"
+input = ["base_address", "timestamp", "read2", "read4", "read8"]
+output = ["cast", "res", "DWordWL"]
+multiplicity = ["-", "μ"]