spec: update constraint ID system

spec/.gitignore

@@ -1,3 +1,4 @@
 dist/*
 interaction_count.json
 ebook.pdf
+venv/*

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)),)
       }
     }
   ))

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")

spec/src.typ

@@ -115,12 +115,141 @@
   }
 }
 
+/// 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
 /// - config: configuration data this chip needs to match with
 #let load_chip(path, config) = {
   let chip = toml(path)
   _check_chip(chip, config)
-  return chip
+  return _add_constraint_ids(chip)
 }

spec/src/branch.toml

@@ -1,4 +1,5 @@
 name = "BRANCH"
+code = "BRH"
 
 
 # Input

spec/src/commit.toml

@@ -1,4 +1,5 @@
 name = "COMMIT"
+code = "CMT"
 
 # Variables
 

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"

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]]

spec/src/keccak.toml

@@ -1,4 +1,5 @@
 name = "KECCAK"
+code = "KCK"
 
 [[variables.input]]
 name = "timestamp"

spec/src/keccak_rc.toml

@@ -1,4 +1,5 @@
 name = "KECCAK_RC"
+code = "KCC"
 
 [[variables.input]]
 name = "round"

spec/src/keccak_round.toml

@@ -1,4 +1,5 @@
 name = "KECCAK_RND"
+code = "KCR"
 
 [[variables.input]]
 name = "timestamp"

spec/src/load.toml

@@ -1,4 +1,5 @@
 name = "LOAD"
+code = "LD"
 
 # Input