From 7d70a0d3b7269d1f6fd957e5e05a9b192e22ee76 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Thu, 23 Apr 2026 17:26:25 +0200 Subject: [PATCH 01/25] spec/constraint_id: introduce FNV-1a hash --- spec/src.typ | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/spec/src.typ b/spec/src.typ index d553629ff..dc253fae4 100644 --- a/spec/src.typ +++ b/spec/src.typ @@ -115,6 +115,38 @@ } } +/// Fowler-Noll-Vo (FNV) hash function, version 1a +/// Src: https://en.wikipedia.org/wiki/Fowler-Noll-Vo_hash_function +/// +/// Note: this is a non-cryptographic hash function; it is optimized +/// for speed at the expense of unpredictability. +/// +/// This implementation operates on two 32-bit limbs, rather than a single +/// 64-bit limb, since Typst does not support u64s. +#let FNV-1a(bytes) = { + // FNV_prime := 0x00000100000001B3 + let prime = (0x000001B3, 0x00000100) + + // hash := FNV_offset_basis = 0xCBF29CE484222325 + let hash = (0x84222325, 0xCBF29CE4) + for b in bytes { + // hash := hash XOR byte_of_data + hash.at(0) = hash.at(0).bit-xor(b) + + // hash := hash × FNV_prime + let lo = hash.at(0) * prime.at(0) + let hi = hash.at(0) * prime.at(1) + hash.at(1) * prime.at(0) + + // Carry result + let carry = lo.bit-rshift(32) + let lo = lo.bit-and(0xFFFFFFFF) + let hi = (hi + carry).bit-and(0xFFFFFFFF) + hash = (lo, hi) + } + + hash.map(int.to-bytes).join() +} + /// Load a chip object from file /// /// - path(str): path to file containing chip data From 2c8a21f8e989f7f38fcbccc370bd267d9559e5d7 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Thu, 23 Apr 2026 15:19:26 +0200 Subject: [PATCH 02/25] spec/constraint_id: compute constraint ID upon load --- spec/src.typ | 110 ++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 109 insertions(+), 1 deletion(-) diff --git a/spec/src.typ b/spec/src.typ index dc253fae4..61ba8a90f 100644 --- a/spec/src.typ +++ b/spec/src.typ @@ -147,6 +147,114 @@ hash.map(int.to-bytes).join() } +/// Converts a byte array to a hexadecimal string +#let bytes-to-hex(bytes) = { + /// Pads a string with 0s on the left to reach a certain length + let z-fill(string) = "0" * (2 - string.len()) + string + + array(bytes) + .map(b => str(b, base: 16)) + .map(z-fill) + .sum() +} + +/// Tag constraints with an identifier +#let _add_constraint_ids(chip) = { + + /// A NON-CRYPTOGRAPHIC hash function. + let nchf(str) = FNV-1a(bytes(str)) + + // number of characters in constraint ID + let CONSTRAINT_ID_CHAR_COUNT = 4; + + /// Digests a variable based on its location and type. + let digest_variable(chip, group, idx, var) = { + /// Flatten the type of a variable into a string + let flatten_vartype(typ) = { + if type(typ) == array { + "(" + typ.map(flatten_vartype).join(",") + ")" + } else { + str(typ) + } + } + + let flattened_type = lower(flatten_vartype(var.type)) + let input = (chip, group, str(idx), flattened_type).join(",") + let digest = bytes-to-hex(nchf(input)) + digest.slice(0, count: 8) + } + + // Map variables to their ID + let variable_to_ID = chip + .variables + .pairs() + .map(((group, variables)) => { + variables + .enumerate() + .map(((idx, var)) => { + (var.name: digest_variable(chip.name, group, idx, var)) + }).sum() + }).sum() + + // replace variable with ID in LISP + let replace_variable_with_ID(lisp) = { + if type(lisp) == array { + "(" + lisp.map(replace_variable_with_ID).join(",") + ")" + } else { + variable_to_ID.at(str(lisp), default: str(lisp)) + } + } + + // Replace variable names with their ID + let digestable_constraint(c) = { + let CONSTRAINT_CAT_TO_SCOPE = ( + "interaction": ("iter", "input", "output", "multiplicity"), + "template": ("iter", "input", "output", "cond"), + "arith": ("iter", "poly") + ) + + assert(c.kind in CONSTRAINT_CAT_TO_SCOPE) + let id_tagged = CONSTRAINT_CAT_TO_SCOPE + .at(c.kind) + .filter(cat => cat in c.keys()) + .map(cat => (str(cat): replace_variable_with_ID(c.at(cat)))) + .sum(default: (:)) + + repr(id_tagged) + .replace("\n", "") + .replace(" ", "") + } + + // Map hash digest to ID + let digest_to_id(hash_bytes) = { + let CHARS = "123456789ABDEFGHJKLMNPQRSTUVWXYZ".codepoints() + assert(CHARS.len() == 32, message: "invalid CHARS length") + + let int = int.from-bytes(hash_bytes.slice(0, count: 8)) + for i in range(CONSTRAINT_ID_CHAR_COUNT) { + let idx = int.bit-and(31) + int = int.bit-rshift(5) + (CHARS.at(idx), ) + }.sum() + } + + // Add an ID to each constraint + chip.constraints = chip.at("constraints", default: (:)) + .pairs() + .map(((group, constraints)) => { + ( + str(group): + constraints + .map(c => { + c.id = digest_to_id(nchf(digestable_constraint(c))) + c + }) + ) + }).sum(default: (:)) + + chip +} + /// Load a chip object from file /// /// - path(str): path to file containing chip data @@ -154,5 +262,5 @@ #let load_chip(path, config) = { let chip = toml(path) _check_chip(chip, config) - return chip + return _add_constraint_ids(chip) } From 122ed2dea32e595b1123b61fe0efa8580f867ccc Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Fri, 24 Apr 2026 11:54:18 +0200 Subject: [PATCH 03/25] spec/constraint_id: attempt at new id --- spec/chip.typ | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/spec/chip.typ b/spec/chip.typ index 1c89dcc55..a74151de9 100644 --- a/spec/chip.typ +++ b/spec/chip.typ @@ -306,11 +306,11 @@ /// Render the contraint's tag. let tag(constraint, group) = { - let with_index(x) = ((x,) + iters_of(constraint).map(it => it.at(0))).join(".") + let with_index(x) = ((raw(x),) + iters_of(constraint).map(it => raw(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 with_index(it.counter.display())]) - cref(constraint)[#figure(kind: chip.name + "constraint", numbering: (i) => [#lbl#i], supplement: [], [])] + let tag(x) = [#raw(chip.name + "-" + prefix + "" + constraint.id + "/")#with_index(x)] + show figure: (it) => align(left, context tag(it.counter.display())) + cref(constraint)[#figure(kind: chip.name + "constraint", numbering: (i) => tag(str(i)), supplement: [], [])] } /// Generates a representation of `constraint` From 5241b9759f165f52f6df5b522f9e8ed5a345a529 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Fri, 24 Apr 2026 14:57:59 +0200 Subject: [PATCH 04/25] spec: drop "constraint" from "polynomial constraint" --- spec/chip.typ | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/chip.typ b/spec/chip.typ index a74151de9..efb523c1e 100644 --- a/spec/chip.typ +++ b/spec/chip.typ @@ -351,7 +351,7 @@ } (..for poly in polys { - (table.cell(align: right, colspan: 2, [_polynomial constraint_]), $#expr_to_math(poly) = 0$, []) + (table.cell(align: right, colspan: 2, [_polynomial_]), $#expr_to_math(poly) = 0$, []) },) } From 86e4f97e5c34bd6cf11a7a09655fd86243f3b99f Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 28 Apr 2026 14:50:46 +0200 Subject: [PATCH 05/25] spec/constraint_id: refactor ID --- spec/chip.typ | 40 ++++++++++++++++++++++++++++++---------- 1 file changed, 30 insertions(+), 10 deletions(-) diff --git a/spec/chip.typ b/spec/chip.typ index efb523c1e..a42124251 100644 --- a/spec/chip.typ +++ b/spec/chip.typ @@ -306,11 +306,20 @@ /// Render the contraint's tag. let tag(constraint, group) = { - let with_index(x) = ((raw(x),) + iters_of(constraint).map(it => raw(it.at(0)))).join(".") - let prefix = if "prefix" in group { group.prefix } - let tag(x) = [#raw(chip.name + "-" + prefix + "" + constraint.id + "/")#with_index(x)] - show figure: (it) => align(left, context tag(it.counter.display())) - cref(constraint)[#figure(kind: chip.name + "constraint", numbering: (i) => tag(str(i)), supplement: [], [])] + let counter-kind = chip.name + "constraint" + let tag = chip.name + "-" + constraint.id + + let indices = (("",) + iters_of(constraint).map(it => it.at(0))).join(".") + + let z-fill(s) = "0" * (2 - s.len()) + s + let ref-tag(i) = raw(tag) + sub("/" + z-fill(str(i))) + return ( + context super[#emph(z-fill(str(counter(figure.where(kind: counter-kind)).get().at(0) + 1)))], + [ + #show figure: (it) => align(left, raw(tag + indices)) + #cref(constraint)[#figure(kind: counter-kind, numbering: (i) => ref-tag(i), supplement: [], [])] + ], + ) } /// Generates a representation of `constraint` @@ -351,13 +360,23 @@ } (..for poly in polys { - (table.cell(align: right, colspan: 2, [_polynomial_]), $#expr_to_math(poly) = 0$, []) + ( + [], + table.cell(align: right, colspan: 2, [_polynomial_]), + table.cell(align: left, colspan: 1, $#expr_to_math(poly) = 0$), + [] + ) },) } // Rendering the additional "desc" field for arith constraints let render_extra_description(constraint) = { - (table.cell(align: right, colspan: 2, [_description_]), eval(constraint.desc, mode: "markup"), []) + ( + [], + table.cell(align: right, colspan: 2, [_description_]), + table.cell(align: left, colspan: 1, eval(constraint.desc, mode: "markup")), + [] + ) } // Whether there is at least one constraint with a range @@ -370,11 +389,12 @@ show figure: set block(breakable: true) figure(table( - columns: (auto, auto, 1fr, auto), + columns: (auto, auto, auto, 1fr, auto), inset: 6pt, - align: (top + left, top + left, top + left, top + center), + align: (top + left, top + left, top + left, top + left, top + center), stroke: none, table.header( +[], [*Tag*], if do_display_range {[*Range*]} else {[]}, [*Description*], @@ -384,7 +404,7 @@ ..for (group, group_constraints) in selected_constraints.pairs() { for constraint in group_constraints { ( - [#tag(constraint, lookup_group(group))], + ..tag(constraint, lookup_group(group)), [#iters(constraint)], [#repr_constraint(constraint)], [#expr_to_math(constraint.at("multiplicity", default: ""))], From 44746720269a23852d28be6bef544dbc926ca5de Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 28 Apr 2026 14:52:28 +0200 Subject: [PATCH 06/25] spec: completely hide unused constraint table columns --- spec/chip.typ | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/chip.typ b/spec/chip.typ index a42124251..512dff973 100644 --- a/spec/chip.typ +++ b/spec/chip.typ @@ -389,7 +389,7 @@ show figure: set block(breakable: true) figure(table( - columns: (auto, auto, auto, 1fr, auto), + columns: (auto, auto, if do_display_range {auto} else {0pt}, 1fr, if do_display_multiplicity {auto} else {0pt}), inset: 6pt, align: (top + left, top + left, top + left, top + left, top + center), stroke: none, From 79727a9aded07d948ee7462351f25a5da8d4b63a Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 28 Apr 2026 14:52:58 +0200 Subject: [PATCH 07/25] spec: squish column table iter notation --- spec/chip.typ | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spec/chip.typ b/spec/chip.typ index 512dff973..9f6dddcde 100644 --- a/spec/chip.typ +++ b/spec/chip.typ @@ -256,7 +256,7 @@ // 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") + 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) = { @@ -394,7 +394,7 @@ align: (top + left, top + left, top + left, top + left, top + center), stroke: none, table.header( -[], + [], [*Tag*], if do_display_range {[*Range*]} else {[]}, [*Description*], From 21a4485769e07c4a97f67c29271d15910af906b8 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 28 Apr 2026 14:58:00 +0200 Subject: [PATCH 08/25] spec: reduce some constraint table column widths --- spec/chip.typ | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) diff --git a/spec/chip.typ b/spec/chip.typ index 9f6dddcde..fab8c031c 100644 --- a/spec/chip.typ +++ b/spec/chip.typ @@ -390,7 +390,12 @@ show figure: set block(breakable: true) figure(table( columns: (auto, auto, if do_display_range {auto} else {0pt}, 1fr, if do_display_multiplicity {auto} else {0pt}), - inset: 6pt, + inset: (x,_) => ( + left: if x == 0 or x == 1 {0pt} else {6pt}, + right: if x == 4 {0pt} else {6pt}, + top: 6pt, + bottom: 6pt + ), align: (top + left, top + left, top + left, top + left, top + center), stroke: none, table.header( @@ -398,7 +403,7 @@ [*Tag*], if do_display_range {[*Range*]} else {[]}, [*Description*], - if do_display_multiplicity {[*Multiplicity*]} else {[]}, + if do_display_multiplicity {[*Multip.*]} else {[]}, ), table.hline(stroke: stroke(thickness: 2pt)), ..for (group, group_constraints) in selected_constraints.pairs() { From 369f1d254fb5ef7666d69c4982a61ebf29fae27a Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 28 Apr 2026 14:58:43 +0200 Subject: [PATCH 09/25] spec: introduce thin lines between constraints --- spec/chip.typ | 1 + 1 file changed, 1 insertion(+) diff --git a/spec/chip.typ b/spec/chip.typ index fab8c031c..fe52e4029 100644 --- a/spec/chip.typ +++ b/spec/chip.typ @@ -420,6 +420,7 @@ if has_polynomial_constraints(constraint) { render_polynomial_constraints(constraint) } + (table.hline(stroke: stroke(thickness: .25pt)),) } } )) From eb53bdf150f829de1d7c74feadf4e3406cffb023 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 28 Apr 2026 15:08:44 +0200 Subject: [PATCH 10/25] spec: use chip codes as shorthand in constraint notation --- spec/chip.typ | 5 +++-- spec/src/branch.toml | 1 + spec/src/commit.toml | 1 + spec/src/keccak.toml | 1 + spec/src/keccak_rc.toml | 1 + spec/src/keccak_round.toml | 1 + spec/src/load.toml | 1 + spec/src/memw.toml | 1 + spec/src/memw_aligned.toml | 1 + spec/src/memw_register.toml | 1 + spec/src/rotxor.toml | 1 + spec/src/sha256.toml | 1 + spec/src/sha256consts.toml | 1 + spec/src/sha256msgsched.toml | 1 + spec/src/sha256round.toml | 1 + spec/src/shift.toml | 1 + spec/src/sign.toml | 1 + 17 files changed, 19 insertions(+), 2 deletions(-) diff --git a/spec/chip.typ b/spec/chip.typ index fe52e4029..5ec978713 100644 --- a/spec/chip.typ +++ b/spec/chip.typ @@ -306,8 +306,9 @@ /// Render the contraint's tag. let tag(constraint, group) = { - let counter-kind = chip.name + "constraint" - let tag = chip.name + "-" + constraint.id + let code = chip.at("code", default: chip.name) + let counter-kind = code + "constraint" + let tag = code + "-" + constraint.id let indices = (("",) + iters_of(constraint).map(it => it.at(0))).join(".") diff --git a/spec/src/branch.toml b/spec/src/branch.toml index 92b93d015..45e6d5618 100644 --- a/spec/src/branch.toml +++ b/spec/src/branch.toml @@ -1,4 +1,5 @@ name = "BRANCH" +code = "BRH" # Input diff --git a/spec/src/commit.toml b/spec/src/commit.toml index 89fa133c6..912b61369 100644 --- a/spec/src/commit.toml +++ b/spec/src/commit.toml @@ -1,4 +1,5 @@ name = "COMMIT" +code = "CMT" # Variables diff --git a/spec/src/keccak.toml b/spec/src/keccak.toml index 1c3bade44..7ab53b581 100644 --- a/spec/src/keccak.toml +++ b/spec/src/keccak.toml @@ -1,4 +1,5 @@ name = "KECCAK" +code = "KCK" [[variables.input]] name = "timestamp" diff --git a/spec/src/keccak_rc.toml b/spec/src/keccak_rc.toml index 7844dfbee..c15566a25 100644 --- a/spec/src/keccak_rc.toml +++ b/spec/src/keccak_rc.toml @@ -1,4 +1,5 @@ name = "KECCAK_RC" +code = "KCC" [[variables.input]] name = "round" diff --git a/spec/src/keccak_round.toml b/spec/src/keccak_round.toml index 6ee05e29a..b2986ce7b 100644 --- a/spec/src/keccak_round.toml +++ b/spec/src/keccak_round.toml @@ -1,4 +1,5 @@ name = "KECCAK_RND" +code = "KCR" [[variables.input]] name = "timestamp" diff --git a/spec/src/load.toml b/spec/src/load.toml index e6cf56f00..cf50ef18c 100644 --- a/spec/src/load.toml +++ b/spec/src/load.toml @@ -1,4 +1,5 @@ name = "LOAD" +code = "LD" # Input diff --git a/spec/src/memw.toml b/spec/src/memw.toml index c04fe5d34..d2af9771a 100644 --- a/spec/src/memw.toml +++ b/spec/src/memw.toml @@ -1,4 +1,5 @@ name = "MEMW" +code = "MMW" # Input diff --git a/spec/src/memw_aligned.toml b/spec/src/memw_aligned.toml index 0e0e20d5d..cc6af39b9 100644 --- a/spec/src/memw_aligned.toml +++ b/spec/src/memw_aligned.toml @@ -1,4 +1,5 @@ name = "MEMW_A" +code = "MWA" # Input diff --git a/spec/src/memw_register.toml b/spec/src/memw_register.toml index 3e7cdcf28..6858c4ca9 100644 --- a/spec/src/memw_register.toml +++ b/spec/src/memw_register.toml @@ -1,4 +1,5 @@ name = "MEMW_R" +code = "MWR" # Variables diff --git a/spec/src/rotxor.toml b/spec/src/rotxor.toml index c3c5ce343..9f0e398b4 100644 --- a/spec/src/rotxor.toml +++ b/spec/src/rotxor.toml @@ -1,4 +1,5 @@ name = "ROTXOR" +code = "RTXR" [[variables.input]] name = "a" diff --git a/spec/src/sha256.toml b/spec/src/sha256.toml index 8ef356578..a4bdb768f 100644 --- a/spec/src/sha256.toml +++ b/spec/src/sha256.toml @@ -1,4 +1,5 @@ name = "SHA256" +code = "SHA" [[variables.input]] name = "timestamp" diff --git a/spec/src/sha256consts.toml b/spec/src/sha256consts.toml index 17fe6fb0f..ab9354801 100644 --- a/spec/src/sha256consts.toml +++ b/spec/src/sha256consts.toml @@ -1,4 +1,5 @@ name = "SHA256_K" +code = "SHK" [[variables.input]] name = "index" diff --git a/spec/src/sha256msgsched.toml b/spec/src/sha256msgsched.toml index 402f7459a..c767e8b26 100644 --- a/spec/src/sha256msgsched.toml +++ b/spec/src/sha256msgsched.toml @@ -1,4 +1,5 @@ name = "SHA256MSGSCHED" +code = "SHM" [[variables.input]] name = "timestamp" diff --git a/spec/src/sha256round.toml b/spec/src/sha256round.toml index 45da4d452..a48e53cc5 100644 --- a/spec/src/sha256round.toml +++ b/spec/src/sha256round.toml @@ -1,4 +1,5 @@ name = "SHA256ROUND" +code = "SHR" [[variables.input]] name = "timestamp" diff --git a/spec/src/shift.toml b/spec/src/shift.toml index a7f3a5f43..6a001e96b 100644 --- a/spec/src/shift.toml +++ b/spec/src/shift.toml @@ -1,4 +1,5 @@ name = "SHIFT" +code = "SHF" # Input diff --git a/spec/src/sign.toml b/spec/src/sign.toml index 24e99bd0e..929404208 100644 --- a/spec/src/sign.toml +++ b/spec/src/sign.toml @@ -1,4 +1,5 @@ name = "SIGN" +code = "SGN" [[variables.input]] name = "X" From 2921edf5666490ab7d7da9ba9587f6803ec8b9aa Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 28 Apr 2026 15:26:30 +0200 Subject: [PATCH 11/25] spec: fix tooling --- spec/tooling/chip.py | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/spec/tooling/chip.py b/spec/tooling/chip.py index 44cbbed83..d31ab629b 100644 --- a/spec/tooling/chip.py +++ b/spec/tooling/chip.py @@ -977,6 +977,7 @@ def build_constraint(config, data: dict) -> Constraint: class Chip: config: Config name: str + code: str variables: list[Variable] assumptions: list[Assumption] constraints: list[Constraint] @@ -993,6 +994,11 @@ def __init__(self, config: Config, data: dict): isinstance(self.name, str), f"name is not a string: {self.name!r}" ) reporter.asserts(self.name.isidentifier(), f"Invalid identifier: {self.name!r}") + self.code = data.get("name", "") + reporter.asserts( + isinstance(self.code, str), f"code is not a string: {self.code!r}" + ) + reporter.asserts(self.code.isidentifier(), f"Invalid identifier: {self.name!r}") self.variables = [ (Variable if cat != "virtual" else VirtualVariable)(config, cat, var) for cat, vars in data["variables"].items() From 118c838bbca8536dd82b13ec9631fadf7066c7e1 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 28 Apr 2026 15:37:42 +0200 Subject: [PATCH 12/25] spec: update assumption naming --- spec/chip.typ | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/spec/chip.typ b/spec/chip.typ index 5ec978713..cc7a85367 100644 --- a/spec/chip.typ +++ b/spec/chip.typ @@ -269,10 +269,12 @@ #let render_chip_assumptions(chip, config) = { let tag(assumption) = { - 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 with_index(it.counter.display())]) - cref(assumption)[#figure(kind: chip.name + "assumption", numbering: (i) => [#lbl#i], supplement: [], [])] + let code = if "code" in chip {chip.code} else {chip.name} + let index = (("",) + iters_of(assumption).map(it => it.at(0))).join(`.`) + let lbl(idx) = raw(code + "-A" + str(idx)) + + show figure: (it) => align(left, block[#context lbl(it.counter.get().at(0))#index]) + cref(assumption)[#figure(kind: code + "assumption", numbering: (i) => lbl(i), supplement: [], [])] } show figure: set block(breakable: true) From 726d17d24dbde4820ebb772672a48a4248c3c75e Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 28 Apr 2026 15:43:25 +0200 Subject: [PATCH 13/25] spec/chip: fix missing sum defaults --- spec/chip.typ | 2 +- spec/signatures.typ | 2 +- spec/src.typ | 5 +++-- 3 files changed, 5 insertions(+), 4 deletions(-) diff --git a/spec/chip.typ b/spec/chip.typ index cc7a85367..1456d23ca 100644 --- a/spec/chip.typ +++ b/spec/chip.typ @@ -24,7 +24,7 @@ config.variables.types.filter(type => type.label == var_type).first().subtypes.len() * factor }) - .sum() + .sum(default: 0) } // Given a constraint, compute the number of interactions it induces diff --git a/spec/signatures.typ b/spec/signatures.typ index 2839a74c6..4d0840a66 100644 --- a/spec/signatures.typ +++ b/spec/signatures.typ @@ -43,7 +43,7 @@ let lbl = v config.variables.types.filter(type => type.label == lbl).first().subtypes.len() * factor }) - .sum() + .sum(default: 0) } #let interactions = signatures.signatures.filter(s => s.kind == "interaction") diff --git a/spec/src.typ b/spec/src.typ index 61ba8a90f..981816141 100644 --- a/spec/src.typ +++ b/spec/src.typ @@ -193,8 +193,8 @@ .enumerate() .map(((idx, var)) => { (var.name: digest_variable(chip.name, group, idx, var)) - }).sum() - }).sum() + }).sum(default: (:)) + }).sum(default: (:)) // replace variable with ID in LISP let replace_variable_with_ID(lisp) = { @@ -230,6 +230,7 @@ let CHARS = "123456789ABDEFGHJKLMNPQRSTUVWXYZ".codepoints() assert(CHARS.len() == 32, message: "invalid CHARS length") + assert(hash_bytes.len() >= 8, message: "too few bytes to digest: " + repr(hash_bytes)) let int = int.from-bytes(hash_bytes.slice(0, count: 8)) for i in range(CONSTRAINT_ID_CHAR_COUNT) { let idx = int.bit-and(31) From 1588a009425d43e6e8d9964ad9ca9c553c7ec90f Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 28 Apr 2026 15:46:38 +0200 Subject: [PATCH 14/25] spec: fix z-fill bug --- spec/chip.typ | 2 +- spec/src.typ | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/spec/chip.typ b/spec/chip.typ index 1456d23ca..97b59b19a 100644 --- a/spec/chip.typ +++ b/spec/chip.typ @@ -314,7 +314,7 @@ let indices = (("",) + iters_of(constraint).map(it => it.at(0))).join(".") - let z-fill(s) = "0" * (2 - s.len()) + s + let z-fill(s) = "0" * calc.max(2 - s.len(), 0) + s let ref-tag(i) = raw(tag) + sub("/" + z-fill(str(i))) return ( context super[#emph(z-fill(str(counter(figure.where(kind: counter-kind)).get().at(0) + 1)))], diff --git a/spec/src.typ b/spec/src.typ index 981816141..12951e389 100644 --- a/spec/src.typ +++ b/spec/src.typ @@ -150,7 +150,7 @@ /// Converts a byte array to a hexadecimal string #let bytes-to-hex(bytes) = { /// Pads a string with 0s on the left to reach a certain length - let z-fill(string) = "0" * (2 - string.len()) + string + let z-fill(str) = "0" * calc.max(2 - str.len(), 0) + str array(bytes) .map(b => str(b, base: 16)) From 916bb112d0d14778188d48bb3c15ab4fb6137f6e Mon Sep 17 00:00:00 2001 From: Erik <159244975+erik-3milabs@users.noreply.github.com> Date: Tue, 28 Apr 2026 15:49:13 +0200 Subject: [PATCH 15/25] spec/constraint_id: use \x00 as domain separator Co-authored-by: claude[bot] <209825114+claude[bot]@users.noreply.github.com> --- spec/src.typ | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/spec/src.typ b/spec/src.typ index 12951e389..2557b5333 100644 --- a/spec/src.typ +++ b/spec/src.typ @@ -179,7 +179,7 @@ } let flattened_type = lower(flatten_vartype(var.type)) - let input = (chip, group, str(idx), flattened_type).join(",") + let input = (chip, group, str(idx), flattened_type).join("\x00") let digest = bytes-to-hex(nchf(input)) digest.slice(0, count: 8) } From 21ab75d37453e5b47555f361ace5638c7369b393 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 28 Apr 2026 15:51:13 +0200 Subject: [PATCH 16/25] spec/chip: fix reading "code" --- spec/tooling/chip.py | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) diff --git a/spec/tooling/chip.py b/spec/tooling/chip.py index d31ab629b..3247a65cb 100644 --- a/spec/tooling/chip.py +++ b/spec/tooling/chip.py @@ -994,11 +994,12 @@ def __init__(self, config: Config, data: dict): isinstance(self.name, str), f"name is not a string: {self.name!r}" ) reporter.asserts(self.name.isidentifier(), f"Invalid identifier: {self.name!r}") - self.code = data.get("name", "") - reporter.asserts( - isinstance(self.code, str), f"code is not a string: {self.code!r}" - ) - reporter.asserts(self.code.isidentifier(), f"Invalid identifier: {self.name!r}") + self.code = data.get("code", "") + if self.code: + reporter.asserts( + isinstance(self.code, str), f"code is not a string: {self.code!r}" + ) + reporter.asserts(self.code.isidentifier(), f"Invalid identifier: {self.code!r}") self.variables = [ (Variable if cat != "virtual" else VirtualVariable)(config, cat, var) for cat, vars in data["variables"].items() From 67142b867f24f3eefcd924b81de6d9bfbfb43f03 Mon Sep 17 00:00:00 2001 From: Erik <159244975+erik-3milabs@users.noreply.github.com> Date: Tue, 28 Apr 2026 15:54:24 +0200 Subject: [PATCH 17/25] spec/constraint_id: include `tag` in constraint-ID derivation --- spec/src.typ | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/spec/src.typ b/spec/src.typ index 2557b5333..dd7aa0021 100644 --- a/spec/src.typ +++ b/spec/src.typ @@ -208,8 +208,8 @@ // Replace variable names with their ID let digestable_constraint(c) = { let CONSTRAINT_CAT_TO_SCOPE = ( - "interaction": ("iter", "input", "output", "multiplicity"), - "template": ("iter", "input", "output", "cond"), + "interaction": ("tag", "iter", "input", "output", "multiplicity"), + "template": ("tag", "iter", "input", "output", "cond"), "arith": ("iter", "poly") ) From fca21464d814305c62487d5d575b0438b3fd6cd5 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Wed, 29 Apr 2026 10:05:59 +0200 Subject: [PATCH 18/25] spec/constraint_id: support indexing for chips beyond 99 constraints --- spec/chip.typ | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/spec/chip.typ b/spec/chip.typ index 97b59b19a..1d801eaa9 100644 --- a/spec/chip.typ +++ b/spec/chip.typ @@ -314,10 +314,11 @@ let indices = (("",) + iters_of(constraint).map(it => it.at(0))).join(".") - let z-fill(s) = "0" * calc.max(2 - s.len(), 0) + s - let ref-tag(i) = raw(tag) + sub("/" + z-fill(str(i))) + let pad-width() = calc.max(calc.ceil(calc.log(counter(figure.where(kind: counter-kind)).final().at(0))), 2) + let z-pad(s) = context "0" * calc.max(pad-width() - s.len(), 0) + s + let ref-tag(i) = raw(tag) + sub("/" + z-pad(str(i))) return ( - context super[#emph(z-fill(str(counter(figure.where(kind: counter-kind)).get().at(0) + 1)))], + context super[#emph(z-pad(str(counter(figure.where(kind: counter-kind)).get().at(0) + 1)))], [ #show figure: (it) => align(left, raw(tag + indices)) #cref(constraint)[#figure(kind: counter-kind, numbering: (i) => ref-tag(i), supplement: [], [])] From b657685981f8d8c41136b523c4d5c8e6b880c2ed Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Wed, 29 Apr 2026 10:19:07 +0200 Subject: [PATCH 19/25] spec/constraint_id: drop bytes-to-hex --- spec/src.typ | 37 +++++++++++++++++++++---------------- 1 file changed, 21 insertions(+), 16 deletions(-) diff --git a/spec/src.typ b/spec/src.typ index dd7aa0021..456a6a132 100644 --- a/spec/src.typ +++ b/spec/src.typ @@ -167,6 +167,26 @@ // number of characters in constraint ID let CONSTRAINT_ID_CHAR_COUNT = 4; + // Map hash digest to ID + let digest_to_id(hash_bytes) = { + // Character set used to represent ID + let CHARS = "123456789ABDEFGHJKLMNPQRSTUVWXYZ".codepoints() + assert(CHARS.len() == 32, message: "invalid CHARS length") + + let min_bytes_len = 2 * CONSTRAINT_ID_CHAR_COUNT + assert( + hash_bytes.len() >= min_bytes_len, + message: "too few bytes to digest: " + repr(hash_bytes) + " has " + str(hash_bytes.len()) + " where " + str(min_bytes_len) + " is required." + ) + + let int = int.from-bytes(hash_bytes.slice(0, count: min_bytes_len)) + for _ in range(CONSTRAINT_ID_CHAR_COUNT) { + let idx = int.bit-and(31) + int = int.bit-rshift(5) + (CHARS.at(idx), ) + }.sum() + } + /// Digests a variable based on its location and type. let digest_variable(chip, group, idx, var) = { /// Flatten the type of a variable into a string @@ -180,8 +200,7 @@ let flattened_type = lower(flatten_vartype(var.type)) let input = (chip, group, str(idx), flattened_type).join("\x00") - let digest = bytes-to-hex(nchf(input)) - digest.slice(0, count: 8) + digest_to_id(nchf(input)) } // Map variables to their ID @@ -225,20 +244,6 @@ .replace(" ", "") } - // Map hash digest to ID - let digest_to_id(hash_bytes) = { - let CHARS = "123456789ABDEFGHJKLMNPQRSTUVWXYZ".codepoints() - assert(CHARS.len() == 32, message: "invalid CHARS length") - - assert(hash_bytes.len() >= 8, message: "too few bytes to digest: " + repr(hash_bytes)) - let int = int.from-bytes(hash_bytes.slice(0, count: 8)) - for i in range(CONSTRAINT_ID_CHAR_COUNT) { - let idx = int.bit-and(31) - int = int.bit-rshift(5) - (CHARS.at(idx), ) - }.sum() - } - // Add an ID to each constraint chip.constraints = chip.at("constraints", default: (:)) .pairs() From 38c64bbe180af669afb96f8d8fa152aaf8404d8c Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Tue, 23 Jun 2026 14:05:22 +0200 Subject: [PATCH 20/25] spec/constraint_id: tweaks --- spec/chip.typ | 4 +- spec/src.typ | 152 ++++++++++++++++++++++++-------------------------- 2 files changed, 76 insertions(+), 80 deletions(-) diff --git a/spec/chip.typ b/spec/chip.typ index 1d801eaa9..01acc0703 100644 --- a/spec/chip.typ +++ b/spec/chip.typ @@ -269,7 +269,7 @@ #let render_chip_assumptions(chip, config) = { let tag(assumption) = { - let code = if "code" in chip {chip.code} else {chip.name} + let code = chip.at("code", default: chip.name) let index = (("",) + iters_of(assumption).map(it => it.at(0))).join(`.`) let lbl(idx) = raw(code + "-A" + str(idx)) @@ -314,7 +314,7 @@ let indices = (("",) + iters_of(constraint).map(it => it.at(0))).join(".") - let pad-width() = calc.max(calc.ceil(calc.log(counter(figure.where(kind: counter-kind)).final().at(0))), 2) + let pad-width() = calc.max(calc.ceil(calc.log(counter(figure.where(kind: counter-kind)).final().at(0) + 1)), 2) let z-pad(s) = context "0" * calc.max(pad-width() - s.len(), 0) + s let ref-tag(i) = raw(tag) + sub("/" + z-pad(str(i))) return ( diff --git a/spec/src.typ b/spec/src.typ index 456a6a132..f80f419b2 100644 --- a/spec/src.typ +++ b/spec/src.typ @@ -128,34 +128,22 @@ let prime = (0x000001B3, 0x00000100) // hash := FNV_offset_basis = 0xCBF29CE484222325 - let hash = (0x84222325, 0xCBF29CE4) + let (lo, hi) = (0x84222325, 0xCBF29CE4) for b in bytes { // hash := hash XOR byte_of_data - hash.at(0) = hash.at(0).bit-xor(b) + lo = lo.bit-xor(b) // hash := hash × FNV_prime - let lo = hash.at(0) * prime.at(0) - let hi = hash.at(0) * prime.at(1) + hash.at(1) * prime.at(0) + lo = lo * prime.at(0) + hi = lo * prime.at(1) + hi * prime.at(0) // Carry result let carry = lo.bit-rshift(32) - let lo = lo.bit-and(0xFFFFFFFF) - let hi = (hi + carry).bit-and(0xFFFFFFFF) - hash = (lo, hi) + lo = lo.bit-and(0xFFFFFFFF) + hi = (hi + carry).bit-and(0xFFFFFFFF) } - hash.map(int.to-bytes).join() -} - -/// Converts a byte array to a hexadecimal string -#let bytes-to-hex(bytes) = { - /// Pads a string with 0s on the left to reach a certain length - let z-fill(str) = "0" * calc.max(2 - str.len(), 0) + str - - array(bytes) - .map(b => str(b, base: 16)) - .map(z-fill) - .sum() + (lo + hi.bit-lshift(32)).to-bytes() } /// Tag constraints with an identifier @@ -164,82 +152,90 @@ /// A NON-CRYPTOGRAPHIC hash function. let nchf(str) = FNV-1a(bytes(str)) - // number of characters in constraint ID - let CONSTRAINT_ID_CHAR_COUNT = 4; - + // ID settings + let ID_CHAR_LEN = 4; + let ID_CHAR_SET = "123456789ABDEFGHJKLMNPQRSTUVWXYZ".codepoints() + + // Constants + let LOG_ID_RADIX = 5 + let RADIX = calc.pow(2, LOG_ID_RADIX) + assert(ID_CHAR_SET.len() == RADIX, message: "ID_CHAR_SET <> RADIX mismatch") + assert(ID_CHAR_LEN * LOG_ID_RADIX <= 64, message: "ID_CHAR_LEN and RADIX incompatible") + // Map hash digest to ID - let digest_to_id(hash_bytes) = { - // Character set used to represent ID - let CHARS = "123456789ABDEFGHJKLMNPQRSTUVWXYZ".codepoints() - assert(CHARS.len() == 32, message: "invalid CHARS length") - - let min_bytes_len = 2 * CONSTRAINT_ID_CHAR_COUNT + let MIN_DIGEST_BYTES = calc.ceil((LOG_ID_RADIX * ID_CHAR_LEN) / 8) + let digest_to_id(digest) = { assert( - hash_bytes.len() >= min_bytes_len, - message: "too few bytes to digest: " + repr(hash_bytes) + " has " + str(hash_bytes.len()) + " where " + str(min_bytes_len) + " is required." + digest.len() >= MIN_DIGEST_BYTES, + message: "too few bytes to digest: " + str(digest.len()) + "<" + str(MIN_DIGEST_BYTES) ) - let int = int.from-bytes(hash_bytes.slice(0, count: min_bytes_len)) - for _ in range(CONSTRAINT_ID_CHAR_COUNT) { + let int = int.from-bytes(digest.slice(0, count: MIN_DIGEST_BYTES)) + for _ in range(ID_CHAR_LEN) { let idx = int.bit-and(31) int = int.bit-rshift(5) - (CHARS.at(idx), ) + (ID_CHAR_SET.at(idx), ) }.sum() } - /// Digests a variable based on its location and type. - let digest_variable(chip, group, idx, var) = { - /// Flatten the type of a variable into a string - let flatten_vartype(typ) = { - if type(typ) == array { - "(" + typ.map(flatten_vartype).join(",") + ")" - } else { - str(typ) - } + // Recursively flatten nested object + let flatten(obj, terminator: str, braces: ("(", ")"), sep: ",") = { + if type(obj) == dictionary { + obj = obj.keys().sorted().map(k => ((k), ":", obj.at(k))) + } + if type(obj) == array { + braces.at(0) + obj.map(a => flatten(a, terminator: terminator, braces: braces, sep: sep)).join(sep) + braces.at(1) + } else { + terminator(obj) } - - let flattened_type = lower(flatten_vartype(var.type)) - let input = (chip, group, str(idx), flattened_type).join("\x00") - digest_to_id(nchf(input)) } - // Map variables to their ID - let variable_to_ID = chip - .variables - .pairs() - .map(((group, variables)) => { - variables - .enumerate() - .map(((idx, var)) => { - (var.name: digest_variable(chip.name, group, idx, var)) - }).sum(default: (:)) - }).sum(default: (:)) + /// Converts a byte array to a hexadecimal string + let bytes-to-hex(bytes) = { + /// Pads a string with 0s on the left to reach a certain length + let z-fill(str) = "0" * calc.max(2 - str.len(), 0) + str - // replace variable with ID in LISP - let replace_variable_with_ID(lisp) = { - if type(lisp) == array { - "(" + lisp.map(replace_variable_with_ID).join(",") + ")" - } else { - variable_to_ID.at(str(lisp), default: str(lisp)) - } + (("0x",) + array(bytes) + .map(b => upper(str(b, base: 16))) + .map(z-fill)) + .sum() } - // Replace variable names with their ID - let digestable_constraint(c) = { - let CONSTRAINT_CAT_TO_SCOPE = ( - "interaction": ("tag", "iter", "input", "output", "multiplicity"), - "template": ("tag", "iter", "input", "output", "cond"), - "arith": ("iter", "poly") - ) + /// Digests a variable based on its location and type. + let digest_variable(chip, group, idx, var) = { + let input = (chip, group, str(idx), flatten(var.type)).join("\x00") + bytes-to-hex(nchf(input)) + } - assert(c.kind in CONSTRAINT_CAT_TO_SCOPE) - let id_tagged = CONSTRAINT_CAT_TO_SCOPE - .at(c.kind) - .filter(cat => cat in c.keys()) - .map(cat => (str(cat): replace_variable_with_ID(c.at(cat)))) + // Assign variables an ID + let variable_IDs = chip + .variables + .pairs() + .map(((group, variables)) => variables + .enumerate() + .map(((idx, var)) => (var.name: digest_variable(chip.name, group, idx, var))) + .sum(default: (:)) + ).sum(default: (:)) + + // Replace variable names with their ID + let EXCLUDED_LABELS = ("desc", "ref", "constraint") + let digestable_constraint(c) = { + // filter out excluded fields + let filtered = c + .pairs() + .filter(((label, value)) => label not in EXCLUDED_LABELS) + .map(((label, value)) => ((label): value)) .sum(default: (:)) - repr(id_tagged) + // replace iter variables with stub + let var_map = c.at("iters", default: if "iter" in c {(c.iter,)} else {()}) + .enumerate() + .map(((idx, iter)) => ((iter.at(0)): "iter" + str(idx))) + .sum(default: (:)) + + let terminator(x) = variable_IDs.at(str(x), default: var_map.at(str(x), default: str(x))) + + flatten(filtered, terminator: terminator) .replace("\n", "") .replace(" ", "") } @@ -249,7 +245,7 @@ .pairs() .map(((group, constraints)) => { ( - str(group): + (group): constraints .map(c => { c.id = digest_to_id(nchf(digestable_constraint(c))) From feb34c57acff4a40de78970cae64b2172530b44c Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Thu, 25 Jun 2026 16:52:08 +0200 Subject: [PATCH 21/25] spec/constraint_id: remove group prefixes --- spec/chip.typ | 7 ++----- spec/src/cpu.toml | 5 ----- spec/src/cpu32.toml | 3 --- spec/src/memw.toml | 2 -- spec/src/memw_aligned.toml | 2 -- 5 files changed, 2 insertions(+), 17 deletions(-) diff --git a/spec/chip.typ b/spec/chip.typ index 01acc0703..fc4fc279c 100644 --- a/spec/chip.typ +++ b/spec/chip.typ @@ -303,11 +303,8 @@ assert(groups.all(group => group in all_groups), message: "unknown group: " + repr(groups)) let selected_constraints = groups.map(g => ((g): chip.constraints.at(g))).join() - // Find the group definition in the constraint_groups - let lookup_group(name) = chip.constraint_groups.filter((g) => g.name == name).at(0, default: (name: name)) - /// Render the contraint's tag. - let tag(constraint, group) = { + let tag(constraint) = { let code = chip.at("code", default: chip.name) let counter-kind = code + "constraint" let tag = code + "-" + constraint.id @@ -413,7 +410,7 @@ ..for (group, group_constraints) in selected_constraints.pairs() { for constraint in group_constraints { ( - ..tag(constraint, lookup_group(group)), + ..tag(constraint), [#iters(constraint)], [#repr_constraint(constraint)], [#expr_to_math(constraint.at("multiplicity", default: ""))], diff --git a/spec/src/cpu.toml b/spec/src/cpu.toml index 85c3aaf70..b9b109919 100644 --- a/spec/src/cpu.toml +++ b/spec/src/cpu.toml @@ -285,7 +285,6 @@ multiplicity = "word_instr" [[constraint_groups]] name = "range" -prefix = "R" [[constraints.range]] kind = "template" @@ -390,7 +389,6 @@ iter = ["i", 0, 3] [[constraint_groups]] name = "alu" -prefix = "A" [[constraints.alu]] kind = "arith" @@ -427,7 +425,6 @@ multiplicity = "ALU" [[constraint_groups]] name = "mem" -prefix = "M" [[constraints.mem]] kind = "interaction" @@ -501,7 +498,6 @@ multiplicity = -1 [[constraint_groups]] name = "branch" -prefix = "B" [[constraints.branch]] kind = "arith" @@ -538,7 +534,6 @@ desc = "Compute the next instruction address in `rvd` when BRANCH is active to e [[constraint_groups]] name = "sys" -prefix = "S" [[constraints.sys]] kind = "interaction" diff --git a/spec/src/cpu32.toml b/spec/src/cpu32.toml index e226c847c..755de1657 100644 --- a/spec/src/cpu32.toml +++ b/spec/src/cpu32.toml @@ -200,7 +200,6 @@ multiplicity = "μ" [[constraint_groups]] name = "range" -prefix = "R" [[constraints.range]] kind = "template" @@ -287,7 +286,6 @@ iter = ["i", 0, 3] [[constraint_groups]] name = "alu" -prefix = "A" [[constraints.alu]] kind = "template" @@ -312,7 +310,6 @@ multiplicity = "ALU" [[constraint_groups]] name = "mem" -prefix = "M" [[constraints.mem]] diff --git a/spec/src/memw.toml b/spec/src/memw.toml index d2af9771a..955e63698 100644 --- a/spec/src/memw.toml +++ b/spec/src/memw.toml @@ -215,7 +215,6 @@ multiplicity = "write8" [[constraint_groups]] name = "memory" -prefix = "M" [[constraints.memory]] kind = "interaction" @@ -272,7 +271,6 @@ iter = ["i", 4, 7] [[constraint_groups]] name = "output" -prefix = "O" [[constraints.output]] kind = "interaction" diff --git a/spec/src/memw_aligned.toml b/spec/src/memw_aligned.toml index cc6af39b9..2fc94571c 100644 --- a/spec/src/memw_aligned.toml +++ b/spec/src/memw_aligned.toml @@ -180,7 +180,6 @@ multiplicity = "μ_sum" [[constraint_groups]] name = "memory" -prefix = "M" [[constraints.memory]] kind = "interaction" @@ -237,7 +236,6 @@ iter = ["i", 4, 7] [[constraint_groups]] name = "output" -prefix = "O" [[constraints.output]] kind = "interaction" From 095e56ef8c0045cf5bf1d6f08816a6589021b85f Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Thu, 25 Jun 2026 16:52:22 +0200 Subject: [PATCH 22/25] spec/constraint_id: fix FNV-1a bug --- spec/src.typ | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/spec/src.typ b/spec/src.typ index f80f419b2..ceb5ccffe 100644 --- a/spec/src.typ +++ b/spec/src.typ @@ -131,11 +131,11 @@ let (lo, hi) = (0x84222325, 0xCBF29CE4) for b in bytes { // hash := hash XOR byte_of_data - lo = lo.bit-xor(b) - // hash := hash × FNV_prime - lo = lo * prime.at(0) - hi = lo * prime.at(1) + hi * prime.at(0) + (lo, hi) = ( + lo.bit-xor(b) * prime.at(0), + lo * prime.at(1) + hi * prime.at(0) + ) // Carry result let carry = lo.bit-rshift(32) From 4205ad70f3fe797c36d8bc9f0105d342026bd664 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Thu, 25 Jun 2026 17:16:53 +0200 Subject: [PATCH 23/25] .gitignore: venv --- spec/.gitignore | 1 + 1 file changed, 1 insertion(+) diff --git a/spec/.gitignore b/spec/.gitignore index b5ca9ae62..f425d1fde 100644 --- a/spec/.gitignore +++ b/spec/.gitignore @@ -1,3 +1,4 @@ dist/* interaction_count.json ebook.pdf +venv/* From 018ed555572ec125b84dfb0b640dee9f12debaf9 Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Fri, 26 Jun 2026 09:41:11 +0200 Subject: [PATCH 24/25] spec/constraint_id: update object digestion --- spec/src.typ | 80 ++++++++++++++++++++++------------------------------ 1 file changed, 34 insertions(+), 46 deletions(-) diff --git a/spec/src.typ b/spec/src.typ index ceb5ccffe..1424efd0a 100644 --- a/spec/src.typ +++ b/spec/src.typ @@ -146,11 +146,33 @@ (lo + hi.bit-lshift(32)).to-bytes() } +// Recursively map nested object to bytes +#let _SEP = bytes(",") +#let to-bytes(leaf-transform, val) = { + let recurse = to-bytes.with(leaf-transform) + let t = type(val) + let (tag, val) = if t == bytes { + ("b", val) + } else if t == str { + ("s", leaf-transform(val)) + } else if t == dictionary { + ("d", val.pairs().map(recurse).sum(default: _SEP)) + } else if t == array { + ("a", val.map(recurse).join(_SEP, default: _SEP)) + } else if t == int { + ("i", val.to-bytes()) + } + bytes("(") + bytes(tag) + val + bytes(")") +} + /// Tag constraints with an identifier #let _add_constraint_ids(chip) = { /// A NON-CRYPTOGRAPHIC hash function. - let nchf(str) = FNV-1a(bytes(str)) + let nchf(bytes) = FNV-1a(bytes) + + /// Digests an object + let digest(obj, leaf-transform: bytes) = nchf(to-bytes(leaf-transform, obj)) // ID settings let ID_CHAR_LEN = 4; @@ -178,66 +200,32 @@ }.sum() } - // Recursively flatten nested object - let flatten(obj, terminator: str, braces: ("(", ")"), sep: ",") = { - if type(obj) == dictionary { - obj = obj.keys().sorted().map(k => ((k), ":", obj.at(k))) - } - if type(obj) == array { - braces.at(0) + obj.map(a => flatten(a, terminator: terminator, braces: braces, sep: sep)).join(sep) + braces.at(1) - } else { - terminator(obj) - } - } - - /// Converts a byte array to a hexadecimal string - let bytes-to-hex(bytes) = { - /// Pads a string with 0s on the left to reach a certain length - let z-fill(str) = "0" * calc.max(2 - str.len(), 0) + str - - (("0x",) + array(bytes) - .map(b => upper(str(b, base: 16))) - .map(z-fill)) - .sum() - } - - /// Digests a variable based on its location and type. - let digest_variable(chip, group, idx, var) = { - let input = (chip, group, str(idx), flatten(var.type)).join("\x00") - bytes-to-hex(nchf(input)) - } - - // Assign variables an ID - let variable_IDs = chip + // Digest variables + let variable_digests = chip .variables .pairs() .map(((group, variables)) => variables .enumerate() - .map(((idx, var)) => (var.name: digest_variable(chip.name, group, idx, var))) + .map(((idx, var)) => (var.name: digest((chip.name, group, idx, var.type)))) .sum(default: (:)) ).sum(default: (:)) // Replace variable names with their ID - let EXCLUDED_LABELS = ("desc", "ref", "constraint") - let digestable_constraint(c) = { + let _EXCLUDED_LABELS = ("desc", "ref", "constraint") + let digest_constraint(c) = { // filter out excluded fields - let filtered = c - .pairs() - .filter(((label, value)) => label not in EXCLUDED_LABELS) - .map(((label, value)) => ((label): value)) - .sum(default: (:)) + let filtered = c.keys().filter(k => k not in _EXCLUDED_LABELS).map(k => c.at(k)) // replace iter variables with stub - let var_map = c.at("iters", default: if "iter" in c {(c.iter,)} else {()}) + let iters = if "iters" in c {c.iters} else if "iter" in c {(c.iter,)} else {()} + let iter_map = iters .enumerate() .map(((idx, iter)) => ((iter.at(0)): "iter" + str(idx))) .sum(default: (:)) - let terminator(x) = variable_IDs.at(str(x), default: var_map.at(str(x), default: str(x))) + let leaf-transform(x) = bytes((iter_map + variable_digests).at(x, default: x)) - flatten(filtered, terminator: terminator) - .replace("\n", "") - .replace(" ", "") + digest(filtered, leaf-transform: leaf-transform) } // Add an ID to each constraint @@ -248,7 +236,7 @@ (group): constraints .map(c => { - c.id = digest_to_id(nchf(digestable_constraint(c))) + c.id = digest_to_id(digest_constraint(c)) c }) ) From aedadc0c64a02d8e857546be0d193ad84892d42b Mon Sep 17 00:00:00 2001 From: Erik Takke Date: Fri, 26 Jun 2026 09:55:10 +0200 Subject: [PATCH 25/25] spec/constraint_id: address review comments --- spec/src.typ | 5 ++--- spec/tooling/chip.py | 2 +- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/spec/src.typ b/spec/src.typ index 1424efd0a..960164408 100644 --- a/spec/src.typ +++ b/spec/src.typ @@ -182,7 +182,7 @@ let LOG_ID_RADIX = 5 let RADIX = calc.pow(2, LOG_ID_RADIX) assert(ID_CHAR_SET.len() == RADIX, message: "ID_CHAR_SET <> RADIX mismatch") - assert(ID_CHAR_LEN * LOG_ID_RADIX <= 64, message: "ID_CHAR_LEN and RADIX incompatible") + assert(ID_CHAR_LEN * LOG_ID_RADIX <= 64, message: "digest size too small for configured ID entropy") // Map hash digest to ID let MIN_DIGEST_BYTES = calc.ceil((LOG_ID_RADIX * ID_CHAR_LEN) / 8) @@ -205,8 +205,7 @@ .variables .pairs() .map(((group, variables)) => variables - .enumerate() - .map(((idx, var)) => (var.name: digest((chip.name, group, idx, var.type)))) + .map(var => (var.name: digest((chip.name, group, var.name, var.type)))) .sum(default: (:)) ).sum(default: (:)) diff --git a/spec/tooling/chip.py b/spec/tooling/chip.py index 3247a65cb..fd6e20f45 100644 --- a/spec/tooling/chip.py +++ b/spec/tooling/chip.py @@ -994,7 +994,7 @@ def __init__(self, config: Config, data: dict): isinstance(self.name, str), f"name is not a string: {self.name!r}" ) reporter.asserts(self.name.isidentifier(), f"Invalid identifier: {self.name!r}") - self.code = data.get("code", "") + self.code = data.get("code", self.name) if self.code: reporter.asserts( isinstance(self.code, str), f"code is not a string: {self.code!r}"