From 4d3f9e1e11108ead9e5fa3b30bd19c3ed5aead0b Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 6 Jan 2026 11:34:13 +0100 Subject: [PATCH 1/9] spec: Initial inefficient MEMW chip --- spec/book.typ | 1 + spec/memw.typ | 39 ++++++++ spec/src/memw.toml | 233 +++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 273 insertions(+) create mode 100644 spec/memw.typ create mode 100644 spec/src/memw.toml diff --git a/spec/book.typ b/spec/book.typ index af747c88c..203a92663 100644 --- a/spec/book.typ +++ b/spec/book.typ @@ -9,6 +9,7 @@ #chapter("is_bit.typ")[IS_BIT template] #chapter("cpu.typ")[CPU chip] #chapter("branch.typ")[BRANCH] + #chapter("memw.typ")[MEMW] ] ) diff --git a/spec/memw.typ b/spec/memw.typ new file mode 100644 index 000000000..68ab2c73e --- /dev/null +++ b/spec/memw.typ @@ -0,0 +1,39 @@ +#import "/book.typ": book-page, rj +#import "/src.typ": load_config, load_chip +#import "/chip.typ": ( + render_chip_assumptions, + render_chip_column_table, + total_nr_variables, + total_nr_instantiated_columns, + render_constraint_table, +) + +#let config = load_config() +#let chip = load_chip("src/memw.toml", config) + +#show: book-page.with(title: "MEMW chip") + +== Columns +#let nr_variables = total_nr_variables(chip) +#let nr_columns = total_nr_instantiated_columns(chip, config) + +The `MEMW` 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 + +#render_constraint_table(chip, config, groups: "consistency") + +The chip adds the following tuples to the lookup argument, +to effectuate that part of the memory argument. +#render_constraint_table(chip, config, groups: "memory") + +This chip contributes the following to the lookup argument. +#render_constraint_table(chip, config, groups: "output") + + + diff --git a/spec/src/memw.toml b/spec/src/memw.toml new file mode 100644 index 000000000..d9a3287af --- /dev/null +++ b/spec/src/memw.toml @@ -0,0 +1,233 @@ +name = "MEMW" + +# Input + +[[variables.input]] +name = "is_register" +type = "Bit" +desc = "Whether the address represents a register index" + +[[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" + +[[variables.input]] +name = "value" +type = ["BaseField", 8] +desc = "The values to store in memory. For regular memory, these should be (up to) 8 range-checked `Byte`s; registers are stored as two range-checked `Word`s" + +[[variables.input]] +name = "timestamp" +type = "DWordWL" +desc = "The timestamp at which this memory access is said to occur" + +[[variables.input]] +name = "write2" +type = "Bit" +desc = "Whether to write at least 2 values" + +[[variables.input]] +name = "write4" +type = "Bit" +desc = "Whether to write at least 4 values" + +[[variables.input]] +name = "write8" +type = "Bit" +desc = "Whether to write 8 values" + +# Output + +[[variables.output]] +name = "old" +type = ["BaseField", 8] +desc = """The old value written at `base_address`. See `value` for information about representation. +Only the elements corresponding to the `writeN` bits are guaranteed""" + +# Auxiliary + +[[variables.auxiliary]] +name = "address_add" +type = ["DWordHL", 7] +desc = "`base_address + i + 1`" + +[[variables.auxiliary]] +name = "old_timestamp" +type = ["DWordWL", 8] +desc = "The timestamp at which the address was last accessed" + +# Virtual + +[[variables.virtual]] +name = "μ_sum" +type = "Bit" +desc = "" +def = ["+", "μ_read", "μ_write"] + +# Multiplicity + +[[variables.multiplicity]] +name = "μ_read" +type = "Bit" +desc = "Whether we are performing a read (and hence return `out`)" + +[[variables.multiplicity]] +name = "μ_write" +type = "Bit" +desc = "Whether we are performing a write (and hence not return `out`)" + + +[[assumptions]] +desc = "`IS_WORD[base_address[i]]`" +range = ["i", 0, 7] + +[[assumptions]] +desc = "`IS_BIT`" + +[[assumptions]] +desc = "`IS_BIT`" + +[[assumptions]] +desc = "`IS_BIT`" + +[[assumptions]] +desc = "`write4 => write2`" + +[[assumptions]] +desc = "`write8 => write4`" + + +[[constraint_groups]] +name = "consistency" + +[[constraints.consistency]] +kind = "template" +tag = "IS_BIT" +input = ["μ_sum"] + +[[constraints.consistency]] +kind = "arith" +constraint = "$#`write2` => #`μ_sum`$" +poly = ["*", "write2", ["not", "μ_sum"]] + +# TODO: does it make sense to add writeX multiplicities? +[[constraints.consistency]] +kind = "template" +tag = "ADD" +input = ["base_address", ["+", "i", 1]] +output = ["idx", "address_add", "i"] +range = ["i", 0, 6] + +# TODO: whoops, double loop +# TODO: does it make sense to add writeX multiplicities? +[[constraints.consistency]] +kind = "interaction" +tag = "IS_HALFWORD" +input = [["idx", ["idx", "address_add", "i"], "j"]] +range = ["TODO", 0, 28] + +[[constraints.consistency]] +kind = "interaction" +tag = "LT" +input = [["idx", "old_timestamp", 0], "timestamp"] +output = 1 +multiplicity = "μ_sum" + +[[constraints.consistency]] +kind = "interaction" +tag = "LT" +input = [["idx", "old_timestamp", 1], "timestamp"] +output = 1 +multiplicity = "write2" + +[[constraints.consistency]] +kind = "interaction" +tag = "LT" +input = [["idx", "old_timestamp", "i"], "timestamp"] +output = 1 +range = ["i", 2, 3] +multiplicity = "write4" + +[[constraints.consistency]] +kind = "interaction" +tag = "LT" +input = [["idx", "old_timestamp", "i"], "timestamp"] +output = 1 +range = ["i", 4, 7] +multiplicity = "write8" + + +[[constraint_groups]] +name = "memory" +prefix = "M" + +[[constraints.memory]] +kind = "interaction" +tag = "memory" +input = ["is_register", "base_address", ["idx", "old_timestamp", 0], ["idx", "old", 0]] +multiplicity = "μ_sum" + +[[constraints.memory]] +kind = "interaction" +tag = "memory" +input = ["is_register", "base_address", "timestamp", ["idx", "value", 0]] +multiplicity = ["-", "μ_sum"] + +[[constraints.memory]] +kind = "interaction" +tag = "memory" +input = ["is_register", ["idx", "address_add", 0], ["idx", "old_timestamp", 1], ["idx", "old", 1]] +multiplicity = "write2" + +[[constraints.memory]] +kind = "interaction" +tag = "memory" +input = ["is_register", ["idx", "address_add", 0], "timestamp", ["idx", "value", 1]] +multiplicity = ["-", "write2"] + +[[constraints.memory]] +kind = "interaction" +tag = "memory" +input = ["is_register", ["idx", "address_add", ["-", "i", 1]], ["idx", "old_timestamp", "i"], ["idx", "old", "i"]] +multiplicity = "write4" +range = ["i", 2, 3] + +[[constraints.memory]] +kind = "interaction" +tag = "memory" +input = ["is_register", ["idx", "address_add", ["-", "i", 1]], "timestamp", ["idx", "value", "i"]] +multiplicity = ["-", "write4"] +range = ["i", 2, 3] + +[[constraints.memory]] +kind = "interaction" +tag = "memory" +input = ["is_register", ["idx", "address_add", ["-", "i", 1]], ["idx", "old_timestamp", "i"], ["idx", "old", "i"]] +multiplicity = "write8" +range = ["i", 4, 7] + +[[constraints.memory]] +kind = "interaction" +tag = "memory" +input = ["is_register", ["idx", "address_add", ["-", "i", 1]], "timestamp", ["idx", "value", "i"]] +multiplicity = ["-", "write8"] +range = ["i", 4, 7] + + +[[constraint_groups]] +name = "output" +prefix = "O" + +[[constraints.output]] +kind = "interaction" +tag = "MEMW" +input = ["is_register", "base_address", "value", "timestamp", "write2", "write4", "write8"] +output = "old" +multiplicity = "μ_read" + +[[constraints.output]] +kind = "interaction" +tag = "MEMW" +input = ["is_register", "base_address", "value", "timestamp", "write2", "write4", "write8"] +multiplicity = "μ_write" From b36ad0d297931d0e8ff39fd3ed49bb350450c947 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Mon, 12 Jan 2026 13:12:09 +0100 Subject: [PATCH 2/9] Apply suggestions from code review Co-authored-by: Erik <159244975+erik-3milabs@users.noreply.github.com> --- spec/src/memw.toml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spec/src/memw.toml b/spec/src/memw.toml index d9a3287af..471503762 100644 --- a/spec/src/memw.toml +++ b/spec/src/memw.toml @@ -50,7 +50,7 @@ Only the elements corresponding to the `writeN` bits are guaranteed""" [[variables.auxiliary]] name = "address_add" type = ["DWordHL", 7] -desc = "`base_address + i + 1`" +desc = "`address_add[i] = base_address + i + 1`" [[variables.auxiliary]] name = "old_timestamp" @@ -80,7 +80,7 @@ desc = "Whether we are performing a write (and hence not return `out`)" [[assumptions]] desc = "`IS_WORD[base_address[i]]`" -range = ["i", 0, 7] +range = ["i", 0, 1] [[assumptions]] desc = "`IS_BIT`" From 59536d915f2a9bd516512f05e4f244982e55d6ee Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Mon, 12 Jan 2026 15:54:03 +0100 Subject: [PATCH 3/9] spec: update range specifications to iters concept --- spec/chip.typ | 89 ++++++++++++++++++++++++++++++-------------- spec/expr.typ | 14 ++++++- spec/src/add.toml | 14 +++---- spec/src/branch.toml | 14 +++---- spec/src/cpu.toml | 14 +++---- spec/src/lt.toml | 12 +++--- spec/src/shift.toml | 22 +++++------ 7 files changed, 112 insertions(+), 67 deletions(-) diff --git a/spec/chip.typ b/spec/chip.typ index 84a575c92..92681e01c 100644 --- a/spec/chip.typ +++ b/spec/chip.typ @@ -24,22 +24,45 @@ .sum() } +// Return a list of iterators needed by `obj`. Taken from `iters` or `iter`. +// Prepend `name` to every iterator, if given. +#let iters_of(obj, name: none) = { + let clean_iter(it) = { + let arr = if type(it) == array { + it + } else { + (it,) + } + if name != none { + (name,) + arr + } else { + arr + } + } + + (if "iters" in obj { + obj.iters + } else if "iter" in obj { + (obj.iter,) + } else { + () + }).map(clean_iter) +} + /// Generates a table listing `chip`'s columns. #let render_chip_column_table(chip, config) = { - // Render a definition's range - let render_def_range(idx, range) = { - if type(range) == array { - if range.len() == 1 { - [#raw(idx) `=` #range.at(0)] - } else if range.len() == 2 { - [#raw(idx) #sym.in `[`#range.at(0)`,`#range.at(1)`]`] + // Render a definition's iterators + let render_def_iters(iters) = { + (..for (name, ..args) in iters { + if args.len() == 1 { + ([#raw(name) = #expr_to_code(args.at(0))],) + } else if args.len() == 2 { + ([#raw(name) #sym.in `[`#expr_to_code(args.at(0)), #expr_to_code(args.at(1))`]`],) } else { - assert(false, message: "invalid range: " + repr(range) + repr(range.len())) + assert(false, message: "Invalid def range: " + repr(name, ..args)) } - } else { - [#raw(idx) `=` #range] - } + }).join("\n") } // Render definition `def` @@ -54,25 +77,39 @@ assert(type(def) == dictionary, message: "invalid definition: " + repr(def)) + let idx = def.at("idx", default: none) + let gather_indices(obj) = iters_of(obj, name: idx).map(it => it.first()) + let index_all(expr, indices) = { + if indices.len() == 0 { + expr + } else { + index_all(("idx", expr, indices.first()), indices.slice(1)) + } + } if "poly" in def { + // assert(false, message: repr(index_all(var_name, gather_indices(def)))) ( [], table.cell(align: right, emph[definition]), - expr_to_math((":=", ("idx", var_name, def.idx), def.poly)), - render_def_range(def.idx, def.range) + expr_to_math((":=", index_all(var_name, gather_indices(def)), def.poly)), + render_def_iters(iters_of(def, name: idx)) ) } else if "polys" in def { + assert( + def.polys.all(poly => + gather_indices(poly) == gather_indices(def.polys.first()) + ), message: "Can only do multiple polys if they're indexed identically") ( [], table.cell(align: right, emph[definition]), - table.cell(colspan: 2, expr_to_math(("idx", var_name, def.idx))) + table.cell(colspan: 2, expr_to_math(index_all(var_name, gather_indices(def.polys.first())))) ) for (i, poly) in def.polys.enumerate() { ( [], [], table.cell(inset: (left: 1.5em), expr_to_math((":=", "", poly.poly))), - render_def_range(def.idx, poly.range), + render_def_iters(iters_of(poly, name: idx)), ) } } else { @@ -114,11 +151,9 @@ } } -// Render a range if `obj` contains one. -#let interval(obj) = { - if "range" in obj { - [#raw(obj.range.at(0)) #sym.in` [`#obj.range.at(1)`,`#obj.range.at(2)`]`] - } else { return [] } +// Render the iterators of `obj`. +#let iters(obj) = { + iters_of(obj).map(iter => [#raw(iter.at(0)) #sym.in `[`#expr_to_code(iter.at(1)), #expr_to_code(iter.at(2))`]`]).join("\n") } #let args_interaction_like(input, output) = { @@ -131,9 +166,9 @@ #let render_chip_assumptions(chip, config) = { let tag(assumption) = { - let index = if "range" in assumption { "." + assumption.range.at(0) } else { "" } + let with_index(x) = ((x,) + iters_of(assumption).map(it => it.at(0))).join(".") let lbl = [#chip.name\-A] - show figure: (it) => align(left, block[#lbl#context it.counter.display()#index]) + show figure: (it) => align(left, block[#lbl#context with_index(it.counter.display())]) cref(assumption)[#figure(kind: chip.name + "assumption", numbering: (i) => [#lbl#i], supplement: [], [])] } @@ -145,7 +180,7 @@ table.header([*Tag*], [*Range*], [*Description*]), table.hline(stroke: stroke(thickness: 2pt)), ..for assumption in chip.assumptions { - ([#tag(assumption)], [#interval(assumption)], [#eval(assumption.desc, mode: "markup")]) + ([#tag(assumption)], [#iters(assumption)], [#eval(assumption.desc, mode: "markup")]) }, ), caption: [Assumption overview of #chip.name chip.]) } @@ -167,10 +202,10 @@ /// Render the contraint's tag. let tag(constraint, group) = { - let index = if "range" in constraint { "." + constraint.range.at(0) } else { "" } + let with_index(x) = ((x,) + iters_of(constraint).map(it => it.at(0))).join(".") let prefix = if "prefix" in group { group.prefix } let lbl = [#chip.name\-C#prefix] - show figure: (it) => align(left, block[#lbl#context it.counter.display()#index]) + show figure: (it) => align(left, block[#lbl#context with_index(it.counter.display())]) cref(constraint)[#figure(kind: chip.name + "constraint", numbering: (i) => [#lbl#i], supplement: [], [])] } @@ -223,7 +258,7 @@ // Whether there is at least one constraint with a range // This can be used to see whether the "Range" label should be displayed - let do_display_range = selected_constraints.values().flatten().any(x => "range" in x) + let do_display_range = selected_constraints.values().flatten().any(x => iters_of(x).len() > 0) // Whether there is at least one constraint with a multiplicity // This can be used to see whether the "Multiplicity" label should be displayed @@ -246,7 +281,7 @@ for constraint in group_constraints { ( [#tag(constraint, lookup_group(group))], - [#interval(constraint)], + [#iters(constraint)], [#repr_constraint(constraint)], [#expr_to_math(constraint.at("multiplicity", default: ""))], ) diff --git a/spec/expr.typ b/spec/expr.typ index 745d95d23..d44523a71 100644 --- a/spec/expr.typ +++ b/spec/expr.typ @@ -129,10 +129,22 @@ } } +#let flat_idxs(expr) = { + if expr.at(0) != "idx" { + (expr, ()) + } else { + let (sub, gathered) = flat_idxs(expr.at(1)) + (sub, gathered + (expr.at(2),)) + } +} + // Typeset an expression as math #let expr_to_math = make_expr_formatter( ( - "idx": (pp, rec, e) => $#rec(PREC.idx, e.at(1))_(#rec(PREC.idx, e.at(2)))$, + "idx": (pp, rec, e) => { + let (val, idxs) = flat_idxs(e) + $#rec(PREC.idx, val)_(#idxs.map(idx => rec(PREC.idx, idx)).join($, $))$ + }, "not": (pp, rec, e) => mwrap($1 - #rec(PREC.not, e.at(1))$, pp < PREC.not), "+": (pp, rec, e) => mwrap($#e.slice(1).map(rec.with(PREC.add)).join($+$)$, pp < PREC.add), "sum": (pp, rec, e) => { diff --git a/spec/src/add.toml b/spec/src/add.toml index a0ccf6942..c928a8b32 100644 --- a/spec/src/add.toml +++ b/spec/src/add.toml @@ -27,26 +27,25 @@ name = "carry" desc = "Carry values used to constrain the addition" type = ["Bit", 2] def = {idx="i", polys=[ - {range=0, poly=["*", ["^", 2, -32], ["-", ["+", ["idx", "lhs", 0], ["idx", "rhs", 0]], ["idx", "sum", 0]]]}, - {range=1, poly=["*", ["^", 2, -32], ["-", ["+", ["idx", "lhs", 1], ["idx", "rhs", 1], ["idx", "carry", 0]], ["idx", "sum", 1]]]}, + {iter=0, poly=["*", ["^", 2, -32], ["-", ["+", ["idx", "lhs", 0], ["idx", "rhs", 0]], ["idx", "sum", 0]]]}, + {iter=1, poly=["*", ["^", 2, -32], ["-", ["+", ["idx", "lhs", 1], ["idx", "rhs", 1], ["idx", "carry", 0]], ["idx", "sum", 1]]]}, ]} - # Assumptions [[assumptions]] desc = "`IS_WORD[lhs[i]]`" -range = ["i", 0, 1] +iter = ["i", 0, 1] ref = "add:a:lhs" [[assumptions]] desc = "`IS_WORD[rhs[i]]`" -range = ["i", 0, 1] +iter = ["i", 0, 1] ref = "add:a:rhs" [[assumptions]] desc = "`IS_WORD[sum[i]]`" -range = ["i", 0, 1] +iter = ["i", 0, 1] ref = "add:a:sum" # Constraints @@ -58,7 +57,6 @@ name = "all" kind = "template" tag = "IS_BIT" input = [["idx", "carry", "i"]] -range = ["i", 0, 1] +iter = ["i", 0, 1] cond = "cond" ref = "add:c:carry" - diff --git a/spec/src/branch.toml b/spec/src/branch.toml index b93639602..b6cb93128 100644 --- a/spec/src/branch.toml +++ b/spec/src/branch.toml @@ -52,8 +52,8 @@ 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 = [ - {range = [0], poly = ["+", ["*", ["^", 2, 16], ["idx", "next_pc_high", 0]], ["*", ["^", 2, 8], ["idx", "next_pc_low", 1]], ["idx", "unmasked_low_byte", 0]]}, - {range = [1], poly = ["+", ["*", ["^", 2, 16], ["idx", "next_pc_high", 2]], ["idx", "next_pc_high", 1]]}, + {iter = 0, poly = ["+", ["*", ["^", 2, 16], ["idx", "next_pc_high", 0]], ["*", ["^", 2, 8], ["idx", "next_pc_low", 1]], ["idx", "unmasked_low_byte", 0]]}, + {iter = 1, poly = ["+", ["*", ["^", 2, 16], ["idx", "next_pc_high", 2]], ["idx", "next_pc_high", 1]]}, ]} [[variables.virtual]] @@ -61,8 +61,8 @@ name = "next_pc" type = "DWordWL" desc = "The computed next pc, after masking off the LSB as required by the ISA." def = {idx = "i", polys = [ - {range = [0], poly = ["+", ["*", ["^", 2, 16], ["idx", "next_pc_high", 0]], ["*", ["^", 2, 8], ["idx", "next_pc_low", 1]], ["idx", "next_pc_low", 0]]}, - {range = [1], poly = ["+", ["*", ["^", 2, 16], ["idx", "next_pc_high", 2]], ["idx", "next_pc_high", 1]]}, + {iter = 0, poly = ["+", ["*", ["^", 2, 16], ["idx", "next_pc_high", 0]], ["*", ["^", 2, 8], ["idx", "next_pc_low", 1]], ["idx", "next_pc_low", 0]]}, + {iter = 1, poly = ["+", ["*", ["^", 2, 16], ["idx", "next_pc_high", 2]], ["idx", "next_pc_high", 1]]}, ]} @@ -76,14 +76,14 @@ desc = "" [[assumptions]] desc = "`pc` is range checked, `IS_WORD[pc[i]]`" -range = ["i", 0, 1] +iter = ["i", 0, 1] [[assumptions]] desc = "`offset` is range checked, `IS_WORD[offset]`" [[assumptions]] desc = "`register` is range checked, `IS_WORD[register[i]]`" -range = ["i", 0, 1] +iter = ["i", 0, 1] [[assumptions]] desc = "`IS_BIT`" @@ -124,7 +124,7 @@ multiplicity = "μ" kind = "interaction" tag = "IS_HALFWORD" input = [["idx", "next_pc_high", "i"]] -range = ["i", 0, 2] +iter = ["i", 0, 2] multiplicity = "μ" diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml index 562a657d0..747497d44 100644 --- a/spec/src/cpu.toml +++ b/spec/src/cpu.toml @@ -456,19 +456,19 @@ input = ["rd"] kind = "interaction" tag = "IS_BYTE" input = [["idx", "arg1", "i"]] -range = ["i", 0, 7] +iter = ["i", 0, 7] [[constraints.range]] kind = "interaction" tag = "IS_BYTE" input = [["idx", "arg2", "i"]] -range = ["i", 0, 7] +iter = ["i", 0, 7] [[constraints.range]] kind = "interaction" tag = "IS_BYTE" input = [["idx", "res", "i"]] -range = ["i", 0, 7] +iter = ["i", 0, 7] [[constraint_groups]] @@ -501,7 +501,7 @@ multiplicity = ["+", "SLT", "BLT"] kind = "arith" constraint = "$#`SLT` + #`BLT` => #`res[i]` = 0$" poly = ["*", ["+", "SLT", "BLT"], ["idx", "res", "i"]] -range = ["i", 1, 7] +iter = ["i", 1, 7] [[constraints.alu]] kind = "interaction" @@ -509,7 +509,7 @@ tag = "AND_BYTE" input = [["idx", "arg1", "i"], ["idx", "arg2", "i"]] output = ["idx", "res", "i"] multiplicity = "AND" -range = ["i", 0, 7] +iter = ["i", 0, 7] [[constraints.alu]] kind = "interaction" @@ -517,7 +517,7 @@ tag = "OR_BYTE" input = [["idx", "arg1", "i"], ["idx", "arg2", "i"]] output = ["idx", "res", "i"] multiplicity = "OR" -range = ["i", 0, 7] +iter = ["i", 0, 7] [[constraints.alu]] kind = "interaction" @@ -525,7 +525,7 @@ tag = "XOR_BYTE" input = [["idx", "arg1", "i"], ["idx", "arg2", "i"]] output = ["idx", "res", "i"] multiplicity = "XOR" -range = ["i", 0, 7] +iter = ["i", 0, 7] [[constraints.alu]] kind = "interaction" diff --git a/spec/src/lt.toml b/spec/src/lt.toml index 1a441c2b3..3a2b7c6f5 100644 --- a/spec/src/lt.toml +++ b/spec/src/lt.toml @@ -50,8 +50,8 @@ name = "carry" type = ["Bit", 2] desc = "The carry for adding `lhs_sub_rhs` back to `rhs`" def = {idx = "i", polys = [ - {range = [0], poly = ["*", ["^", 2, -32], ["-", ["+", ["idx", "rhs", 0], ["idx", ["cast", "lhs_sub_rhs", "DWordWL"], 0]], ["idx", "lhs", 0]]]}, - {range = [1], poly = ["*", ["^", 2, -32], ["-", ["+", ["idx", ["cast", "rhs", "DWordWL"], 1], ["idx", ["cast", "lhs_sub_rhs", "DWordWL"], 1], ["idx", "carry", 0]], ["idx", ["cast", "lhs", "DWordWL"], 1]]]}, + {iter = 0, poly = ["*", ["^", 2, -32], ["-", ["+", ["idx", "rhs", 0], ["idx", ["cast", "lhs_sub_rhs", "DWordWL"], 0]], ["idx", "lhs", 0]]]}, + {iter = 1, poly = ["*", ["^", 2, -32], ["-", ["+", ["idx", ["cast", "rhs", "DWordWL"], 1], ["idx", ["cast", "lhs_sub_rhs", "DWordWL"], 1], ["idx", "carry", 0]], ["idx", ["cast", "lhs", "DWordWL"], 1]]]}, ]} [[variables.virtual]] @@ -71,12 +71,12 @@ desc = "" [[assumptions]] desc = "`IS_HALFWORD[lhs[i]]` and `IS_WORD[lhs[0]]`" -range = ["i", 1, 2] +iter = ["i", 1, 2] ref = "lt:a:range_lhs" [[assumptions]] desc = "`IS_HALFWORD[rhs[i]]` and `IS_WORD[rhs[0]]`" -range = ["i", 1, 2] +iter = ["i", 1, 2] ref = "lt:a:range_rhs" [[assumptions]] @@ -120,13 +120,13 @@ desc = "Constrain the subtraction" kind = "template" tag = "IS_BIT" input = [["idx", "carry", "i"]] -range = ["i", 0, 1] +iter = ["i", 0, 1] [[constraints.sub]] kind = "interaction" tag = "IS_HALFWORD" input = [["idx", "lhs_sub_rhs", "i"]] -range = ["i", 0, 3] +iter = ["i", 0, 3] multiplicity = "μ" ref = "lt:c:lhs_sub_rhs_range" diff --git a/spec/src/shift.toml b/spec/src/shift.toml index e2ddfa12b..3dca9ec6f 100644 --- a/spec/src/shift.toml +++ b/spec/src/shift.toml @@ -92,21 +92,21 @@ name = "intra_limb_left" type = "DWordHL" desc = "`in << (shift % 16)` if `left`" def = {idx="i", polys=[ - {range=0, poly=["idx", "X", 0]}, - {range=[1, 3], poly=["+", ["idx", "X", "i"], ["idx", "Y", ["-", "i", 1]]]}, + {iter=0, poly=["idx", "X", 0]}, + {iter=[1, 3], poly=["+", ["idx", "X", "i"], ["idx", "Y", ["-", "i", 1]]]}, ]} [[variables.virtual]] name = "intra_limb_right" type = "DWordHL" desc = "`in >>> (shift % 16)` if `right` and `signed`;\\ `in >> (shift % 16)` if `right` and `!signed`" -def = {idx="i", range=[0, 3], poly=["+", ["idx", "Y", "i"], ["idx", "X", ["+", "i", 1]]]} +def = {idx="i", iter=[0, 3], poly=["+", ["idx", "Y", "i"], ["idx", "X", ["+", "i", 1]]]} [[variables.virtual]] name = "shifted" type = "DWordHL" desc = "$#`in <>/>>>` (#`shift` mod 32 dot (2 - #`word_instr`))$" -def = {idx="i", range=[0, 3], poly=["+", ["*", "left", ["sum", ["=", "j", 0], "i", ["*", ["idx", "limb_shift", "j"], ["idx", "intra_limb_left", ["-", "i", "j"]]]]], ["*", "right", ["+", ["sum", ["=", "j", 0], ["-", 3, "i"], ["*", ["idx", "limb_shift", "j"], ["idx", "intra_limb_right", ["+", "i", "j"]]]], ["*", "extension", ["sum", ["=", "j", ["-", 3, "i"]], 3, ["idx", "limb_shift", "j"]]]]]]} +def = {idx="i", iter=[0, 3], poly=["+", ["*", "left", ["sum", ["=", "j", 0], "i", ["*", ["idx", "limb_shift", "j"], ["idx", "intra_limb_left", ["-", "i", "j"]]]]], ["*", "right", ["+", ["sum", ["=", "j", 0], ["-", 3, "i"], ["*", ["idx", "limb_shift", "j"], ["idx", "intra_limb_right", ["+", "i", "j"]]]], ["*", "extension", ["sum", ["=", "j", ["-", 3, "i"]], 3, ["idx", "limb_shift", "j"]]]]]]} # Multiplicities @@ -121,7 +121,7 @@ desc = "" [[assumptions]] desc = "`IS_HALFWORD[in[i]]`" -range = ["i", 0, 3] +iter = ["i", 0, 3] ref = "shift:a:range_in" [[assumptions]] @@ -201,7 +201,7 @@ kind = "interaction" tag = "HWSL" input = [["idx", "in", "i"], "bit_shift"] output = ["idx", "X", "i"] -range = ["i", 0, 3] +iter = ["i", 0, 3] ref = "shift:c:hwsl_if_not_zero" multiplicity = ["not", "zbs"] @@ -209,7 +209,7 @@ multiplicity = ["not", "zbs"] kind = "arith" constraint = "$#`zbs` => #`X[i]` = #`in[i]` dot #`left`$" poly = ["*", "zbs", ["-", ["idx", "X", "i"], ["*", ["idx", "in", "i"], "left"]]] -range = ["i", 0, 3] +iter = ["i", 0, 3] ref = "shift:c:zbs_implies_X" [[constraints.intra_limb_shift]] @@ -231,7 +231,7 @@ kind = "interaction" tag = "HWSLC" input = [["idx", "in", "i"], "bit_shift"] output = ["idx", "Y", "i"] -range = ["i", 0, 3] +iter = ["i", 0, 3] ref = "shift:c:hwslc_if_not_zero" multiplicity = ["not", "zbs"] @@ -239,7 +239,7 @@ multiplicity = ["not", "zbs"] kind = "arith" constraint = "$#`zbs` => #`Y[i]` = #`in[i]` dot #`right`$" poly = ["*", "zbs", ["-", ["idx", "Y", "i"], ["*", ["idx", "in", "i"], "right"]]] -range = ["i", 0, 3] +iter = ["i", 0, 3] ref = "shift:c:zbs_implies_Y" @@ -250,7 +250,7 @@ name = "limb_shifting" kind = "template" tag = "IS_BIT" input = [["idx", "limb_shift", "i"]] -range = ["i", 0, 3] +iter = ["i", 0, 3] ref = "shift:c:limb_shift_is_bit" [[constraints.limb_shifting]] @@ -265,7 +265,7 @@ multiplicity = "μ" kind = "arith" constraint = "$#`out[:2]` = #`shifted[:4]`$" poly = ["-", ["idx", "out", "i"], ["idx", ["cast", "shifted", "DWordWL"], "i"]] -range = ["i", 0, 1] +iter = ["i", 0, 1] ref = "shift:c:out_eq_shifted" From c0c0160257aaa74d8fa3135bdfb42fa9609b23b6 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 13 Jan 2026 14:47:26 +0100 Subject: [PATCH 4/9] Trap on overflow in MEMW --- spec/memw.typ | 9 +++++ spec/src/cpu.toml | 6 ++-- spec/src/memw.toml | 87 ++++++++++++++++++++++++++++++++++++---------- 3 files changed, 80 insertions(+), 22 deletions(-) diff --git a/spec/memw.typ b/spec/memw.typ index 68ab2c73e..f4e75cd92 100644 --- a/spec/memw.typ +++ b/spec/memw.typ @@ -28,6 +28,10 @@ The `MEMW` chip is comprised of #nr_variables variables that are expressed using #render_constraint_table(chip, config, groups: "consistency") +We additionally also check that the address does not overflow +for more significant bytes of the access. +#render_constraint_table(chip, config, groups: "overflow") + The chip adds the following tuples to the lookup argument, to effectuate that part of the memory argument. #render_constraint_table(chip, config, groups: "memory") @@ -36,4 +40,9 @@ This chip contributes the following to the lookup argument. #render_constraint_table(chip, config, groups: "output") +== Future optimization ideas +- Fast path for aligned memory access where all bytes have the same old timestamp +- 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) diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml index 562a657d0..4b5ec2c83 100644 --- a/spec/src/cpu.toml +++ b/spec/src/cpu.toml @@ -38,17 +38,17 @@ desc = "Whether to write back to the destination register" [[variables.input]] name = "memory_2bytes" type = "Bit" -desc = "Whether the memory access (read or write) touches at least 2 bytes" +desc = "Whether the memory access (read or write) touches exactly 2 bytes" [[variables.input]] name = "memory_4bytes" type = "Bit" -desc = "Whether the memory access (read or write) touches at least 4 bytes" +desc = "Whether the memory access (read or write) touches exactly 4 bytes" [[variables.input]] name = "memory_8bytes" type = "Bit" -desc = "Whether the memory access (read or write) touches at least 8 bytes" +desc = "Whether the memory access (read or write) touches exactly 8 bytes" # TODO: Are there usecases where it's nicer to just have this as a length constant? [[variables.input]] diff --git a/spec/src/memw.toml b/spec/src/memw.toml index 471503762..c4c8b7430 100644 --- a/spec/src/memw.toml +++ b/spec/src/memw.toml @@ -25,17 +25,17 @@ desc = "The timestamp at which this memory access is said to occur" [[variables.input]] name = "write2" type = "Bit" -desc = "Whether to write at least 2 values" +desc = "Whether to write exactly 2 values" [[variables.input]] name = "write4" type = "Bit" -desc = "Whether to write at least 4 values" +desc = "Whether to write exactly 4 values" [[variables.input]] name = "write8" type = "Bit" -desc = "Whether to write 8 values" +desc = "Whether to write exactly 8 values" # Output @@ -59,6 +59,18 @@ desc = "The timestamp at which the address was last accessed" # Virtual +[[variables.virtual]] +name = "w2" +type = "Bit" +desc = "writing at least 2 bytes" +def = ["+", "write2", "write4", "write8"] + +[[variables.virtual]] +name = "w4" +type = "Bit" +desc = "writing at least 4 bytes" +def = ["+", "write4", "write8"] + [[variables.virtual]] name = "μ_sum" type = "Bit" @@ -92,10 +104,7 @@ desc = "`IS_BIT`" desc = "`IS_BIT`" [[assumptions]] -desc = "`write4 => write2`" - -[[assumptions]] -desc = "`write8 => write4`" +desc = "`IS_BIT`" [[constraint_groups]] @@ -108,19 +117,33 @@ input = ["μ_sum"] [[constraints.consistency]] kind = "arith" -constraint = "$#`write2` => #`μ_sum`$" -poly = ["*", "write2", ["not", "μ_sum"]] +constraint = "$#`w2` => #`μ_sum`$" +poly = ["*", "w2", ["not", "μ_sum"]] + +[[constraints.consistency]] +kind = "template" +tag = "ADD" +input = ["base_address", 1] +output = ["cast", ["idx", "address_add", 0], "DWordWL"] +multiplicity = "w2" + +[[constraints.consistency]] +kind = "template" +tag = "ADD" +input = ["base_address", ["+", "i", 1]] +output = ["cast", ["idx", "address_add", "i"], "DWordWL"] +range = ["i", 1, 2] +multiplicity = "w4" -# TODO: does it make sense to add writeX multiplicities? [[constraints.consistency]] kind = "template" tag = "ADD" input = ["base_address", ["+", "i", 1]] -output = ["idx", "address_add", "i"] -range = ["i", 0, 6] +output = ["cast", ["idx", "address_add", "i"], "DWordWL"] +range = ["i", 3, 6] +multiplicity = "write8" # TODO: whoops, double loop -# TODO: does it make sense to add writeX multiplicities? [[constraints.consistency]] kind = "interaction" tag = "IS_HALFWORD" @@ -139,7 +162,7 @@ kind = "interaction" tag = "LT" input = [["idx", "old_timestamp", 1], "timestamp"] output = 1 -multiplicity = "write2" +multiplicity = "w2" [[constraints.consistency]] kind = "interaction" @@ -147,7 +170,7 @@ tag = "LT" input = [["idx", "old_timestamp", "i"], "timestamp"] output = 1 range = ["i", 2, 3] -multiplicity = "write4" +multiplicity = "w4" [[constraints.consistency]] kind = "interaction" @@ -158,6 +181,32 @@ range = ["i", 4, 7] multiplicity = "write8" +[[constraint_groups]] +name = "overflow" +prefix = "O" + +[[constraints.overflow]] +kind = "interaction" +tag = "LT" +input = ["base_address", ["cast", ["idx", "address_add", 0], "DWordWL"]] +output = 1 +multiplicity = "write2" + +[[constraints.overflow]] +kind = "interaction" +tag = "LT" +input = ["base_address", ["cast", ["idx", "address_add", 2], "DWordWL"]] +output = 1 +multiplicity = "write4" + +[[constraints.overflow]] +kind = "interaction" +tag = "LT" +input = ["base_address", ["cast", ["idx", "address_add", 6], "DWordWL"]] +output = 1 +multiplicity = "write8" + + [[constraint_groups]] name = "memory" prefix = "M" @@ -178,26 +227,26 @@ multiplicity = ["-", "μ_sum"] kind = "interaction" tag = "memory" input = ["is_register", ["idx", "address_add", 0], ["idx", "old_timestamp", 1], ["idx", "old", 1]] -multiplicity = "write2" +multiplicity = "w2" [[constraints.memory]] kind = "interaction" tag = "memory" input = ["is_register", ["idx", "address_add", 0], "timestamp", ["idx", "value", 1]] -multiplicity = ["-", "write2"] +multiplicity = ["-", "w2"] [[constraints.memory]] kind = "interaction" tag = "memory" input = ["is_register", ["idx", "address_add", ["-", "i", 1]], ["idx", "old_timestamp", "i"], ["idx", "old", "i"]] -multiplicity = "write4" +multiplicity = "w4" range = ["i", 2, 3] [[constraints.memory]] kind = "interaction" tag = "memory" input = ["is_register", ["idx", "address_add", ["-", "i", 1]], "timestamp", ["idx", "value", "i"]] -multiplicity = ["-", "write4"] +multiplicity = ["-", "w4"] range = ["i", 2, 3] [[constraints.memory]] From 0d7fdc2d49a9fa92118250114f1a733e58a2ccd8 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 13 Jan 2026 14:49:59 +0100 Subject: [PATCH 5/9] Update MEMW chip to iters --- spec/src/memw.toml | 24 +++++++++++++----------- 1 file changed, 13 insertions(+), 11 deletions(-) diff --git a/spec/src/memw.toml b/spec/src/memw.toml index c4c8b7430..bca8c44c7 100644 --- a/spec/src/memw.toml +++ b/spec/src/memw.toml @@ -92,7 +92,7 @@ desc = "Whether we are performing a write (and hence not return `out`)" [[assumptions]] desc = "`IS_WORD[base_address[i]]`" -range = ["i", 0, 1] +iter = ["i", 0, 1] [[assumptions]] desc = "`IS_BIT`" @@ -132,7 +132,7 @@ kind = "template" tag = "ADD" input = ["base_address", ["+", "i", 1]] output = ["cast", ["idx", "address_add", "i"], "DWordWL"] -range = ["i", 1, 2] +iter = ["i", 1, 2] multiplicity = "w4" [[constraints.consistency]] @@ -140,15 +140,17 @@ kind = "template" tag = "ADD" input = ["base_address", ["+", "i", 1]] output = ["cast", ["idx", "address_add", "i"], "DWordWL"] -range = ["i", 3, 6] +iter = ["i", 3, 6] multiplicity = "write8" -# TODO: whoops, double loop [[constraints.consistency]] kind = "interaction" tag = "IS_HALFWORD" input = [["idx", ["idx", "address_add", "i"], "j"]] -range = ["TODO", 0, 28] +iters = [ + ["i", 0, 6], + ["j", 0, 3], +] [[constraints.consistency]] kind = "interaction" @@ -169,7 +171,7 @@ kind = "interaction" tag = "LT" input = [["idx", "old_timestamp", "i"], "timestamp"] output = 1 -range = ["i", 2, 3] +iter = ["i", 2, 3] multiplicity = "w4" [[constraints.consistency]] @@ -177,7 +179,7 @@ kind = "interaction" tag = "LT" input = [["idx", "old_timestamp", "i"], "timestamp"] output = 1 -range = ["i", 4, 7] +iter = ["i", 4, 7] multiplicity = "write8" @@ -240,28 +242,28 @@ kind = "interaction" tag = "memory" input = ["is_register", ["idx", "address_add", ["-", "i", 1]], ["idx", "old_timestamp", "i"], ["idx", "old", "i"]] multiplicity = "w4" -range = ["i", 2, 3] +iter = ["i", 2, 3] [[constraints.memory]] kind = "interaction" tag = "memory" input = ["is_register", ["idx", "address_add", ["-", "i", 1]], "timestamp", ["idx", "value", "i"]] multiplicity = ["-", "w4"] -range = ["i", 2, 3] +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"]] multiplicity = "write8" -range = ["i", 4, 7] +iter = ["i", 4, 7] [[constraints.memory]] kind = "interaction" tag = "memory" input = ["is_register", ["idx", "address_add", ["-", "i", 1]], "timestamp", ["idx", "value", "i"]] multiplicity = ["-", "write8"] -range = ["i", 4, 7] +iter = ["i", 4, 7] [[constraint_groups]] From e29f371da724676b2643f215708dfd093cb41c52 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 13 Jan 2026 14:54:43 +0100 Subject: [PATCH 6/9] range check timestamps --- spec/src/memw.toml | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/spec/src/memw.toml b/spec/src/memw.toml index bca8c44c7..48d25fe89 100644 --- a/spec/src/memw.toml +++ b/spec/src/memw.toml @@ -106,6 +106,10 @@ desc = "`IS_BIT`" [[assumptions]] desc = "`IS_BIT`" +[[assumptions]] +desc = "`IS_HALFWORD[timestamp[i]]`" +iter = ["i", 0, 3] + [[constraint_groups]] name = "consistency" @@ -152,6 +156,15 @@ iters = [ ["j", 0, 3], ] +[[constraints.consistency]] +kind = "interaction" +tag = "IS_HALFWORD" +input = [["idx", ["idx", "old_timestamp", "i"], "j"]] +iters = [ + ["i", 0, 7], + ["j", 0, 3], +] + [[constraints.consistency]] kind = "interaction" tag = "LT" From b9faafa423c992a3a20c4880693faec589be1e34 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 13 Jan 2026 15:16:14 +0100 Subject: [PATCH 7/9] one more optimization idea for later --- spec/memw.typ | 1 + 1 file changed, 1 insertion(+) diff --git a/spec/memw.typ b/spec/memw.typ index f4e75cd92..8c1ddb8fc 100644 --- a/spec/memw.typ +++ b/spec/memw.typ @@ -46,3 +46,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) +- Check if `old_timestamp` is already range_checked by inclusion in the memory argument From add5c85f2181b0f8c30e76f6823d224545394ed6 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Tue, 13 Jan 2026 15:45:01 +0100 Subject: [PATCH 8/9] Address review comments --- spec/memw.typ | 7 ++++++- spec/src/memw.toml | 15 +++------------ 2 files changed, 9 insertions(+), 13 deletions(-) diff --git a/spec/memw.typ b/spec/memw.typ index 8c1ddb8fc..1dea04670 100644 --- a/spec/memw.typ +++ b/spec/memw.typ @@ -28,6 +28,11 @@ The `MEMW` chip is comprised of #nr_variables variables that are expressed using #render_constraint_table(chip, config, groups: "consistency") +As long as `timestamp` is properly range-checked, the presence of `old_timestamp` +in the memory argument automatically ensures appropriate range checking +(as long as no external entities provide negative multiplicities without range checking the timestamp). +This ensures the assumptions for `LT` are satisfied. + We additionally also check that the address does not overflow for more significant bytes of the access. #render_constraint_table(chip, config, groups: "overflow") @@ -46,4 +51,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) -- Check if `old_timestamp` is already range_checked by inclusion in the memory argument +- Adding `μ_sum`/`w2`/`w4`/`write8` multiplicities to the `IS_HALFWORD` lookups may make some GKR things faster if there are known zeroes. diff --git a/spec/src/memw.toml b/spec/src/memw.toml index 48d25fe89..9aa9cd592 100644 --- a/spec/src/memw.toml +++ b/spec/src/memw.toml @@ -107,8 +107,8 @@ desc = "`IS_BIT`" desc = "`IS_BIT`" [[assumptions]] -desc = "`IS_HALFWORD[timestamp[i]]`" -iter = ["i", 0, 3] +desc = "`IS_WORD[timestamp[i]]`" +iter = ["i", 0, 1] [[constraint_groups]] @@ -156,15 +156,6 @@ iters = [ ["j", 0, 3], ] -[[constraints.consistency]] -kind = "interaction" -tag = "IS_HALFWORD" -input = [["idx", ["idx", "old_timestamp", "i"], "j"]] -iters = [ - ["i", 0, 7], - ["j", 0, 3], -] - [[constraints.consistency]] kind = "interaction" tag = "LT" @@ -198,7 +189,7 @@ multiplicity = "write8" [[constraint_groups]] name = "overflow" -prefix = "O" +prefix = "R" [[constraints.overflow]] kind = "interaction" From b793a4b8eadcddef9e7acefeb264ce45a26384d6 Mon Sep 17 00:00:00 2001 From: Robin Jadoul Date: Thu, 15 Jan 2026 14:31:37 +0100 Subject: [PATCH 9/9] More updates after review --- spec/memw.typ | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/spec/memw.typ b/spec/memw.typ index 1dea04670..bcf6a64b0 100644 --- a/spec/memw.typ +++ b/spec/memw.typ @@ -24,6 +24,11 @@ The `MEMW` chip is comprised of #nr_variables variables that are expressed using #render_chip_assumptions(chip, config) +Our assumptions do not explicitly cover any range checks for the `is_register` and `value` columns, +as these are not necessary for the correctness of this chip in isolation. +These properties are necessary for the consistency of the system as a whole, and therefore +we document it here, keeping the type information as a reading help. + == Constraints #render_constraint_table(chip, config, groups: "consistency") @@ -33,7 +38,7 @@ in the memory argument automatically ensures appropriate range checking (as long as no external entities provide negative multiplicities without range checking the timestamp). This ensures the assumptions for `LT` are satisfied. -We additionally also check that the address does not overflow +We additionally check that the address does not overflow for more significant bytes of the access. #render_constraint_table(chip, config, groups: "overflow")