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/* diff --git a/spec/chip.typ b/spec/chip.typ index 1c89dcc55..fc4fc279c 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 @@ -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) = { @@ -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 = 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)) + + 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,16 +303,24 @@ 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 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 tag(constraint) = { + 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) + 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 ( + 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` @@ -351,13 +361,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 @@ -370,21 +390,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), [#iters(constraint)], [#repr_constraint(constraint)], [#expr_to_math(constraint.at("multiplicity", default: ""))], @@ -395,6 +421,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..960164408 100644 --- a/spec/src.typ +++ b/spec/src.typ @@ -115,6 +115,135 @@ } } +/// 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 (lo, hi) = (0x84222325, 0xCBF29CE4) + for b in bytes { + // hash := hash XOR byte_of_data + // hash := hash × FNV_prime + (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) + lo = lo.bit-and(0xFFFFFFFF) + hi = (hi + carry).bit-and(0xFFFFFFFF) + } + + (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(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; + 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: "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) + let digest_to_id(digest) = { + assert( + digest.len() >= MIN_DIGEST_BYTES, + message: "too few bytes to digest: " + str(digest.len()) + "<" + str(MIN_DIGEST_BYTES) + ) + + 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) + (ID_CHAR_SET.at(idx), ) + }.sum() + } + + // Digest variables + let variable_digests = chip + .variables + .pairs() + .map(((group, variables)) => variables + .map(var => (var.name: digest((chip.name, group, var.name, var.type)))) + .sum(default: (:)) + ).sum(default: (:)) + + // Replace variable names with their ID + let _EXCLUDED_LABELS = ("desc", "ref", "constraint") + let digest_constraint(c) = { + // filter out excluded fields + let filtered = c.keys().filter(k => k not in _EXCLUDED_LABELS).map(k => c.at(k)) + + // replace iter variables with stub + 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 leaf-transform(x) = bytes((iter_map + variable_digests).at(x, default: x)) + + digest(filtered, leaf-transform: leaf-transform) + } + + // Add an ID to each constraint + chip.constraints = chip.at("constraints", default: (:)) + .pairs() + .map(((group, constraints)) => { + ( + (group): + constraints + .map(c => { + c.id = digest_to_id(digest_constraint(c)) + c + }) + ) + }).sum(default: (:)) + + chip +} + /// Load a chip object from file /// /// - path(str): path to file containing chip data @@ -122,5 +251,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 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/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/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..955e63698 100644 --- a/spec/src/memw.toml +++ b/spec/src/memw.toml @@ -1,4 +1,5 @@ name = "MEMW" +code = "MMW" # Input @@ -214,7 +215,6 @@ multiplicity = "write8" [[constraint_groups]] name = "memory" -prefix = "M" [[constraints.memory]] kind = "interaction" @@ -271,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 0e0e20d5d..2fc94571c 100644 --- a/spec/src/memw_aligned.toml +++ b/spec/src/memw_aligned.toml @@ -1,4 +1,5 @@ name = "MEMW_A" +code = "MWA" # Input @@ -179,7 +180,6 @@ multiplicity = "μ_sum" [[constraint_groups]] name = "memory" -prefix = "M" [[constraints.memory]] kind = "interaction" @@ -236,7 +236,6 @@ iter = ["i", 4, 7] [[constraint_groups]] name = "output" -prefix = "O" [[constraints.output]] kind = "interaction" 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" diff --git a/spec/tooling/chip.py b/spec/tooling/chip.py index 44cbbed83..fd6e20f45 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,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", self.name) + 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()