diff --git a/spec/book.typ b/spec/book.typ index fe1aef8a1..e8eb1855c 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -24,6 +24,7 @@ ("sign.typ", [`SIGN` template], ), ("add.typ", [`ADD`/`SUB` template], ), ("neg.typ", [`NEG` template], ), + ("reg.typ", [`REG`/`REGW` template], ), )), ("CPU", ( ("decode.typ", [`DECODE` table], ), diff --git a/spec/reg.typ b/spec/reg.typ new file mode 100644 index 000000000..6b294dc49 --- /dev/null +++ b/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) diff --git a/spec/src/commit.toml b/spec/src/commit.toml index a300ed095..f6e77ffd8 100644 --- a/spec/src/commit.toml +++ b/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" diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml index a434580f5..0dec36b03 100644 --- a/spec/src/cpu.toml +++ b/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" diff --git a/spec/src/cpu32.toml b/spec/src/cpu32.toml index fde581b42..4b3932f32 100644 --- a/spec/src/cpu32.toml +++ b/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" diff --git a/spec/src/ecsm.toml b/spec/src/ecsm.toml index f2ec79692..226c61816 100644 --- a/spec/src/ecsm.toml +++ b/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]] diff --git a/spec/src/halt.toml b/spec/src/halt.toml index db3420253..c72fac7dc 100644 --- a/spec/src/halt.toml +++ b/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]] diff --git a/spec/src/keccak.toml b/spec/src/keccak.toml index f4a3b2877..d2cc8bb5c 100644 --- a/spec/src/keccak.toml +++ b/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]] diff --git a/spec/src/reg_read.toml b/spec/src/reg_read.toml new file mode 100644 index 000000000..709f123a4 --- /dev/null +++ b/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" diff --git a/spec/src/reg_write.toml b/spec/src/reg_write.toml new file mode 100644 index 000000000..411adf24c --- /dev/null +++ b/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" diff --git a/spec/src/sha256.toml b/spec/src/sha256.toml index 22686d944..ba7ad43d5 100644 --- a/spec/src/sha256.toml +++ b/spec/src/sha256.toml @@ -54,11 +54,11 @@ pad = 0 name = "memory" [[constraints.memory]] -kind = "interaction" -tag = "MEMW" -input = [1, ["cast", ["*", 2, 11], "DWordWL"], ["arr", ["idx", ["cast", ["idx", "m_addr", 0], "DWordWL"], 0], ["idx", ["cast", ["idx", "m_addr", 0], "DWordWL"], 1], 0, 0, 0, 0, 0, 0], "timestamp", 1, 0, 0] -output = ["arr", ["idx", ["cast", ["idx", "m_addr", 0], "DWordWL"], 0], ["idx", ["cast", ["idx", "m_addr", 0], "DWordWL"], 1], 0, 0, 0, 0, 0, 0] -multiplicity = "μ" +kind = "template" +tag = "REG" +input = [11, ["cast", ["idx", "m_addr", 0], "DWordWL"], "timestamp"] +output = ["cast", ["idx", "m_addr", 0], "DWordWL"] +cond = "μ" [[constraints.memory]] kind = "interaction" @@ -101,11 +101,11 @@ iter = ["i", 0, 7] ref = "sha256:c:read_chunk" [[constraints.memory]] -kind = "interaction" -tag = "MEMW" -input = [1, ["cast", ["*", 2, 10], "DWordWL"], ["arr", ["idx", ["cast", ["idx", "h_addr", 0], "DWordWL"], 0], ["idx", ["cast", ["idx", "h_addr", 0], "DWordWL"], 1], 0, 0, 0, 0, 0, 0], "timestamp", 1, 0, 0] -output = ["arr", ["idx", ["cast", ["idx", "h_addr", 0], "DWordWL"], 0], ["idx", ["cast", ["idx", "h_addr", 0], "DWordWL"], 1], 0, 0, 0, 0, 0, 0] -multiplicity = "μ" +kind = "template" +tag = "REG" +input = [10, ["cast", ["idx", "h_addr", 0], "DWordWL"], "timestamp"] +output = ["cast", ["idx", "h_addr", 0], "DWordWL"] +cond = "μ" [[constraints.memory]] kind = "interaction" diff --git a/spec/src/signatures.toml b/spec/src/signatures.toml index 1492dcdde..f02ecd163 100644 --- a/spec/src/signatures.toml +++ b/spec/src/signatures.toml @@ -84,12 +84,27 @@ kind = "interaction" input = ["Bit", "DWordWL", ["BaseField", 8], "Word", "Bit", "Bit", "Bit"] output = ["BaseField", 8] +# REG[old; base_address, value, timestamp] +[[signatures]] +tag = "REG" +kind = "template" +input = ["Byte", "DWordWL", "Word"] +output = "DWordWL" +cond = "BaseField" + # MEMW[is_register, base_address, value, timestamp, write2, write4, write8] [[signatures]] tag = "MEMW" kind = "interaction" input = ["Bit", "DWordWL", ["BaseField", 8], "Word", "Bit", "Bit", "Bit"] +# REG[base_address, value, timestamp] +[[signatures]] +tag = "REGW" +kind = "template" +input = ["Byte", "DWordWL", "Word"] +cond = "BaseField" + # LOAD[res; base_address, timestamp, flags] [[signatures]] tag = "LOAD"