diff --git a/spec/chip.typ b/spec/chip.typ index c6cce5073..29dc02387 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 @@ -251,7 +251,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) = { @@ -264,10 +264,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) @@ -301,11 +303,22 @@ /// Render the contraint's tag. let tag(constraint, group) = { - 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 with_index(it.counter.display())]) - cref(constraint)[#figure(kind: chip.name + "constraint", numbering: (i) => [#lbl#i], supplement: [], [])] + 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(".") + + 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-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: [], [])] + ], + ) } /// Generates a representation of `constraint` @@ -346,13 +359,23 @@ } (..for poly in polys { - (table.cell(align: right, colspan: 2, [_polynomial constraint_]), $#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 @@ -365,21 +388,27 @@ show figure: set block(breakable: true) figure(table( - columns: (auto, auto, 1fr, auto), - inset: 6pt, - align: (top + left, top + left, top + left, top + center), + columns: (auto, auto, if do_display_range {auto} else {0pt}, 1fr, if do_display_multiplicity {auto} else {0pt}), + 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( + [], [*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() { 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: ""))], @@ -390,6 +419,7 @@ if has_polynomial_constraints(constraint) { render_polynomial_constraints(constraint) } + (table.hline(stroke: stroke(thickness: .25pt)),) } } )) 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 d553629ff..456a6a132 100644 --- a/spec/src.typ +++ b/spec/src.typ @@ -115,6 +115,152 @@ } } +/// 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() +} + +/// 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() +} + +/// 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; + + // 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 + 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("\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: (:)) + + // 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": ("tag", "iter", "input", "output", "multiplicity"), + "template": ("tag", "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(" ", "") + } + + // 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 @@ -122,5 +268,5 @@ #let load_chip(path, config) = { let chip = toml(path) _check_chip(chip, config) - return chip + return _add_constraint_ids(chip) } diff --git a/spec/src/branch.toml b/spec/src/branch.toml index a98974678..7e296aa93 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 b8f2d91c2..64cb4b6cd 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 548cb5151..ba5d1e160 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 f8a974c9a..1e346a3e9 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 1cc0dd3c2..5ff6d3b9b 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 93a636aba..6903e8066 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 730e9bda5..2e1e99e1f 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 4cd4de9ba..9aaaaf24b 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 79664a797..e32359a2b 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 8ec93ea36..4ec70f563 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 bbe22a5d9..f441ccbe8 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" diff --git a/spec/tooling/chip.py b/spec/tooling/chip.py index 7f7ecca81..6b8e6a565 100644 --- a/spec/tooling/chip.py +++ b/spec/tooling/chip.py @@ -970,6 +970,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] @@ -986,6 +987,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("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()