spec: REG(W) templates

spec/book.typ

@@ -24,6 +24,7 @@
       ("sign.typ", [`SIGN` template], <sign>),
       ("add.typ", [`ADD`/`SUB` template], <add>),
       ("neg.typ", [`NEG` template], <neg>),
+      ("reg.typ", [`REG`/`REGW` template], <reg>),
     )),
     ("CPU", (
       ("decode.typ", [`DECODE` table], <decode>),

spec/reg.typ

@@ -0,0 +1,46 @@
+#import "/book.typ": book-page
+#import "/src.typ": load_config, load_chip
+#import "/chip.typ": render_chip_variable_table, render_constraint_table, set_nr_interactions,
+
+#let config = load_config()
+#let reg_read = load_chip("src/reg_read.toml", config)
+#let reg_write = load_chip("src/reg_write.toml", config)
+#let read = raw(reg_read.name)
+#let write = raw(reg_write.name)
+
+#show: book-page("REG")
+
+We provide the #read and #write templates.
+These templates act as short hand notation for `MEMW` interactions pertaining to operations in the `register` domain ($= 1$, see @memory).
+
+The necessity for two templates follows from the existence of two subtly different `MEMW` signatures (see @signatures): there is both a read-write and an write-only interaction.
+Here, the former is wrapped by #read, while the #write template encapsulates the latter.
+
+It is recommended to utilize these two templates in favor of direct `MEMW` interactions to specify register updates, as these
++ take care of the crucial register-number to register-address conversion, and
++ provide significantly more concise notation,
+improving both readability and correctness of the specification.
+
+= #read
+The #read template encapsulates register read-write interactions.
+Note: when `cond` is omitted, it defaults to 1.
+
+== Variables
+#set_nr_interactions(reg_read)
+#render_chip_variable_table(reg_read, config)
+
+== Constraints
+#render_constraint_table(reg_read, config)
+
+#pagebreak(weak: true)
+
+= #write
+The #write template encapsulates register write-only interactions.
+Note: when `cond` is omitted, it defaults to 1.
+
+== Variables
+#set_nr_interactions(reg_write)
+#render_chip_variable_table(reg_write, config)
+
+== Constraints
+#render_constraint_table(reg_write, config)

spec/src/commit.toml

@@ -82,35 +82,35 @@ ref = "commit:c:receive_ecall"
 name = "read_input"
 
 [[constraints.read_input]]
-kind = "interaction"
-tag = "MEMW"
-input = [1, ["cast", ["*", 2, 11], "DWordWL"], ["arr", ["idx", "address", 0], ["idx", "address", 1], 0, 0, 0, 0, 0, 0], "timestamp", 1, 0, 0]
-output = ["arr", ["idx", "address", 0], ["idx", "address", 1], 0, 0, 0, 0, 0, 0]
-multiplicity = "first"
+kind = "template"
+tag = "REG"
+input = [11, "address", "timestamp"]
+output = "address"
+cond = "first"
 ref = "commit:c:read_address"
 
 [[constraints.read_input]]
-kind = "interaction"
-tag = "MEMW"
-input = [1, ["cast", ["*", 2, 12], "DWordWL"], ["arr", ["idx", "count", 0], ["idx", "count", 1], 0, 0, 0, 0, 0, 0], "timestamp", 1, 0, 0]
-output = ["arr", ["idx", "count", 0], ["idx", "count", 1], 0, 0, 0, 0, 0, 0]
-multiplicity = "first"
+kind = "template"
+tag = "REG"
+input = [12, "count", "timestamp"]
+output = "count"
+cond = "first"
 ref = "commit:c:read_count"
 
 [[constraints.read_input]]
-kind = "interaction"
-tag = "MEMW"
-input = [1, ["cast", ["*", 2, 10], "DWordWL"], ["arr", ["idx", "count", 0], ["idx", "count", 1], 0, 0, 0, 0, 0, 0], "timestamp", 1, 0, 0]
-output = ["arr", 1, 0, 0, 0, 0, 0, 0, 0]
-multiplicity = "first"
+kind = "template"
+tag = "REG"
+input = [10, "count", "timestamp"]
+output = ["cast", 1, "DWordWL"]
+cond = "first"
 ref = "commit:c:read_fd_write_count"
 
 [[constraints.read_input]]
-kind = "interaction"
-tag = "MEMW"
-input = [1, ["cast", ["*", 2, 254], "DWordWL"], ["arr", ["+", "index", ["cast", "count", "BaseField"]], 0, 0, 0, 0, 0, 0, 0], "timestamp", 0, 0, 0]
-output = ["arr", "index", 0, 0, 0, 0, 0, 0, 0]
-multiplicity = "first"
+kind = "template"
+tag = "REG"
+input = [254, ["arr", ["+", "index", ["cast", "count", "BaseField"]], 0], "timestamp"]
+output = ["arr", "index", 0]
+cond = "first"
 ref = "commit:c:read_index"
 
 

spec/src/cpu.toml

@@ -421,11 +421,11 @@ multiplicity = "ALU"
 name = "mem"
 
 [[constraints.mem]]
-kind = "interaction"
-tag = "MEMW"
-input = [1, ["*", ["cast", 2, "DWordWL"], "rs1"], ["arr", ["idx", "rv1", 0], ["idx", "rv1", 1], 0, 0, 0, 0, 0, 0], ["+", "timestamp", 0], 1, 0, 0]
-output = ["arr", ["idx", "rv1", 0], ["idx", "rv1", 1], 0, 0, 0, 0, 0, 0]
-multiplicity = "read_register1"
+kind = "template"
+tag = "REG"
+input = ["rs1", "rv1", ["+", "timestamp", 0]]
+output = "rv1"
+cond = "read_register1"
 ref = "cpu:c:read_rv1"
 
 [[constraints.mem]]
@@ -435,11 +435,11 @@ poly = ["*", ["not", "read_register1"], ["idx", "rv1", "i"]]
 iter = ["i", 0, 1]
 
 [[constraints.mem]]
-kind = "interaction"
-tag = "MEMW"
-input = [1, ["*", ["cast", 2, "DWordWL"], "rs2"], ["arr", ["idx", "rv2", 0], ["idx", "rv2", 1], 0, 0, 0, 0, 0, 0], ["+", "timestamp", 1], 1, 0, 0]
-output = ["arr", ["idx", "rv2", 0], ["idx", "rv2", 1], 0, 0, 0, 0, 0, 0]
-multiplicity = "read_register2"
+kind = "template"
+tag = "REG"
+input = ["rs2", "rv2", ["+", "timestamp", 1]]
+output = "rv2"
+cond = "read_register2"
 
 [[constraints.mem]]
 kind = "arith"
@@ -448,10 +448,10 @@ poly = ["*", ["not", "read_register2"], ["idx", "rv2", "i"]]
 iter = ["i", 0, 1]
 
 [[constraints.mem]]
-kind = "interaction"
-tag = "MEMW"
-input = [1, ["*", ["cast", 2, "DWordWL"], "rd"], ["arr", ["idx", "rvd", 0], ["idx", "rvd", 1], 0, 0, 0, 0, 0, 0], ["+", "timestamp", 2], 1, 0, 0]
-multiplicity = "write_register"
+kind = "template"
+tag = "REGW"
+input = ["rd", "rvd", ["+", "timestamp", 2]]
+cond = "write_register"
 
 [[constraints.mem]]
 kind = "interaction"

spec/src/cpu32.toml

@@ -312,11 +312,11 @@ name = "mem"
 
 
 [[constraints.mem]]
-kind = "interaction"
-tag = "MEMW"
-input = [1, ["*", ["cast", 2, "DWordWL"], "rs1"], ["arr", ["idx", ["cast", "rv1", "DWordWL"], 0], ["idx", "rv1", 2], 0, 0, 0, 0, 0, 0], ["+", "timestamp", 0], 1, 0, 0]
-output = ["arr", ["idx", ["cast", "rv1", "DWordWL"], 0], ["idx", "rv1", 2], 0, 0, 0, 0, 0, 0]
-multiplicity = "read_register1"
+kind = "template"
+tag = "REG"
+input = ["rs1", ["cast", "rv1", "DWordWL"], ["+", "timestamp", 0]]
+output = ["cast", "rv1", "DWordWL"]
+cond = "read_register1"
 
 [[constraints.mem]]
 kind = "arith"
@@ -325,11 +325,11 @@ poly = ["*", ["not", "read_register1"], ["idx", "rv1", "i"]]
 iter = ["i", 0, 2]
 
 [[constraints.mem]]
-kind = "interaction"
-tag = "MEMW"
-input = [1, ["*", ["cast", 2, "DWordWL"], "rs2"], ["arr", ["idx", ["cast", "rv2", "DWordWL"], 0], ["idx", "rv2", 2], 0, 0, 0, 0, 0, 0], ["+", "timestamp", 1], 1, 0, 0]
-output = ["arr", ["idx", ["cast", "rv2", "DWordWL"], 0], ["idx", "rv2", 2], 0, 0, 0, 0, 0, 0]
-multiplicity = "read_register2"
+kind = "template"
+tag = "REG"
+input = ["rs2", ["cast", "rv2", "DWordWL"], ["+", "timestamp", 1]]
+output = ["cast", "rv2", "DWordWL"]
+cond = "read_register2"
 
 [[constraints.mem]]
 kind = "arith"
@@ -338,10 +338,10 @@ poly = ["*", ["not", "read_register2"], ["idx", "rv2", "i"]]
 iter = ["i", 0, 2]
 
 [[constraints.mem]]
-kind = "interaction"
-tag = "MEMW"
-input = [1, ["*", ["cast", 2, "DWordWL"], "rd"], ["arr", ["idx", "rvd", 0], ["idx", "rvd", 1], 0, 0, 0, 0, 0, 0], ["+", "timestamp", 2], 1, 0, 0]
-multiplicity = "write_register"
+kind = "template"
+tag = "REGW"
+input = ["rd", "rvd", ["+", "timestamp", 2]]
+cond = "write_register"
 
 [[constraint_groups]]
 name = "logup"

spec/src/ecsm.toml

@@ -257,16 +257,11 @@ pad = 0
 name = "read_xG"
 
 [[constraints.read_xG]]
-kind = "interaction"
-tag = "MEMW"
-input = [
-    1, 
-    ["cast", ["*", 2, 11], "DWordWL"],
-    ["arr", ["idx", ["cast", ["idx", "addr_xG", 0], "DWordWL"], 0], ["idx", ["cast", ["idx", "addr_xG", 0], "DWordWL"], 1], 0, 0, 0, 0, 0, 0],
-    "timestamp", 
-    1, 0, 0]
-output = ["arr", ["idx", ["cast", ["idx", "addr_xG", 0], "DWordWL"], 0], ["idx", ["cast", ["idx", "addr_xG", 0], "DWordWL"], 1], 0, 0, 0, 0, 0, 0]
-multiplicity = "μ"
+kind = "template"
+tag = "REG"
+input = [11, ["cast", ["idx", "addr_xG", 0], "DWordWL"], "timestamp"]
+output = ["cast", ["idx", "addr_xG", 0], "DWordWL"]
+cond = "μ"
 ref = "ec:c:read_addr_xG"
 
 [[constraints.read_xG]]
@@ -483,16 +478,11 @@ ref = "ec:c:range_c1"
 name = "verify_k"
 
 [[constraints.verify_k]]
-kind = "interaction"
-tag = "MEMW"
-input = [
-    1, 
-    ["cast", ["*", 2, 12], "DWordWL"],
-    ["arr", ["idx", ["cast", ["idx", "addr_k", 0], "DWordWL"], 0], ["idx", ["cast", ["idx", "addr_k", 0], "DWordWL"], 1], 0, 0, 0, 0, 0, 0],
-    ["+", "timestamp", 1],
-    1, 0, 0]
-output = ["arr", ["idx", ["cast", ["idx", "addr_k", 0], "DWordWL"], 0], ["idx", ["cast", ["idx", "addr_k", 0], "DWordWL"], 1], 0, 0, 0, 0, 0, 0]
-multiplicity = "μ"
+kind = "template"
+tag = "REG"
+input = [12, ["cast", ["idx", "addr_k", 0], "DWordWL"], ["+", "timestamp", 1]]
+output = ["cast", ["idx", "addr_k", 0], "DWordWL"]
+cond = "μ"
 ref = "ec:c:read_addr_k"
 
 [[constraints.verify_k]]
@@ -649,16 +639,11 @@ ref = "ec:c:xR_addition_overflows"
 name = "write_xR"
 
 [[constraints.write_xR]]
-kind = "interaction"
-tag = "MEMW"
-input = [
-    1, 
-    ["cast", ["*", 2, 10], "DWordWL"],
-    ["arr", ["idx", ["cast", ["idx", "addr_xR", 0], "DWordWL"], 0], ["idx", ["cast", ["idx", "addr_xR", 0], "DWordWL"], 1], 0, 0, 0, 0, 0, 0],
-    ["+", "timestamp", 2],
-    1, 0, 0]
-output = ["arr", ["idx", ["cast", ["idx", "addr_xR", 0], "DWordWL"], 0], ["idx", ["cast", ["idx", "addr_xR", 0], "DWordWL"], 1], 0, 0, 0, 0, 0, 0]
-multiplicity = "μ"
+kind = "template"
+tag = "REG"
+input = [10, ["cast", ["idx", "addr_xR", 0], "DWordWL"], ["+", "timestamp", 2]]
+output = ["cast", ["idx", "addr_xR", 0], "DWordWL"]
+cond = "μ"
 ref = "ec:c:load_addr_xR"
 
 [[constraints.write_xR]]

spec/src/halt.toml

@@ -18,27 +18,24 @@ desc = "`IS_WORD[timestamp]`"
 name = "all"
 
 [[constraints.all]]
-kind = "interaction"
-tag = "MEMW"
-input = [1, ["cast", ["*", 2, "i"], "DWordWL"], ["cast", 0, ["BaseField", 8]], ["-", ["^", 2, 32], 1], 1, 0, 0]
+kind = "template"
+tag = "REGW"
+input = ["i", ["cast", 0, "DWordWL"], ["-", ["^", 2, 32], 1]]
 iter = ["i", 1, 9]
-multiplicity = 1
 ref = "halt:c:zeroize_registers_lo"
 
 [[constraints.all]]
-kind = "interaction"
-tag = "MEMW"
-input = [1, ["cast", ["*", 2, 10], "DWordWL"], ["cast", 0, ["BaseField", 8]], ["-", ["^", 2, 32], 1], 1, 0, 0]
-output = ["cast", 0, ["BaseField", 8]]
-multiplicity = 1
+kind = "template"
+tag = "REG"
+input = [10, ["cast", 0, "DWordWL"], ["-", ["^", 2, 32], 1]]
+output = ["cast", 0, "DWordWL"]
 ref = "halt:c:read_zero_exit_code"
 
 [[constraints.all]]
-kind = "interaction"
-tag = "MEMW"
-input = [1, ["cast", ["*", 2, "i"], "DWordWL"], ["cast", 0, ["BaseField", 8]], ["-", ["^", 2, 32], 1], 1, 0, 0]
+kind = "template"
+tag = "REGW"
+input = ["i", ["cast", 0, "DWordWL"], ["-", ["^", 2, 32], 1]]
 iter = ["i", 11, 31]
-multiplicity = 1
 ref = "halt:c:zeroize_registers_hi"
 
 [[constraints.all]]

spec/src/keccak.toml

@@ -51,11 +51,11 @@ name = "mem"
 
 
 [[constraints.mem]]
-kind = "interaction"
-tag = "MEMW"
-input = [1, ["cast", ["*", 2, 10], "DWordWL"], ["arr", ["idx", ["cast", ["idx", ["idx", "state_ptr", 0], 0], "DWordWL"], 0], ["idx", ["cast", ["idx", ["idx", "state_ptr", 0], 0], "DWordWL"], 1], 0, 0, 0, 0, 0, 0], "timestamp", 1, 0, 0]
-output = ["arr", ["idx", ["cast", ["idx", ["idx", "state_ptr", 0], 0], "DWordWL"], 0], ["idx", ["cast", ["idx", ["idx", "state_ptr", 0], 0], "DWordWL"], 1], 0, 0, 0, 0, 0, 0]
-multiplicity = "μ"
+kind = "template"
+tag = "REG"
+input = [10, ["cast", ["idx", ["idx", "state_ptr", 0], 0], "DWordWL"], "timestamp"]
+output = ["cast", ["idx", ["idx", "state_ptr", 0], 0], "DWordWL"]
+cond = "μ"
 ref = "keccak:c:read_state_ptr"
 
 [[constraints.mem]]

spec/src/reg_read.toml

@@ -0,0 +1,37 @@
+name = "REG"
+
+[[variables.condition]]
+name = "cond"
+type = "BaseField"
+desc = "the multiplicity with which to apply the interaction"
+
+[[variables.input]]
+name = "register"
+type = "Byte"
+desc = "the index of the register being addressed"
+
+[[variables.input]]
+name = "value"
+type = "DWordWL"
+desc = "the value being written to the register"
+
+[[variables.input]]
+name = "timestamp"
+type = "Word"
+desc = "the timestamp of the access"
+
+[[variables.output]]
+name = "old"
+type = "DWordWL"
+desc = "the value being read from the register"
+
+
+[[constraint_groups]]
+name = "all"
+
+[[constraints.all]]
+kind = "interaction"
+tag = "MEMW"
+input = [1, ["arr", ["*", 2, "register"], 0], ["arr", ["idx", "value", 0], ["idx", "value", 1], 0, 0, 0, 0, 0, 0], "timestamp", 1, 0, 0]
+output = ["arr", ["idx", "old", 0], ["idx", "old", 1], 0, 0, 0, 0, 0, 0]
+multiplicity = "cond"

spec/src/reg_write.toml

@@ -0,0 +1,31 @@
+name = "REGW"
+
+[[variables.condition]]
+name = "cond"
+type = "BaseField"
+desc = "the multiplicity with which to apply the interaction"
+
+[[variables.input]]
+name = "register"
+type = "Byte"
+desc = "the index of the register being addressed"
+
+[[variables.input]]
+name = "value"
+type = "DWordWL"
+desc = "the value being written to the register"
+
+[[variables.input]]
+name = "timestamp"
+type = "Word"
+desc = "the timestamp of the access"
+
+
+[[constraint_groups]]
+name = "all"
+
+[[constraints.all]]
+kind = "interaction"
+tag = "MEMW"
+input = [1, ["arr", ["*", 2, "register"], 0], ["arr", ["idx", "value", 0], ["idx", "value", 1], 0, 0, 0, 0, 0, 0], "timestamp", 1, 0, 0]
+multiplicity = "cond"