spec: update constraint ID system

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

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,158 @@
   }
 }
 
+/// 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
 /// - 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/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
 

spec/src/memw.toml

@@ -1,4 +1,5 @@
 name = "MEMW"
+code = "MMW"
 
 # Input
 

spec/src/memw_aligned.toml

@@ -1,4 +1,5 @@
 name = "MEMW_A"
+code = "MWA"
 
 # Input
 

spec/src/memw_register.toml

@@ -1,4 +1,5 @@
 name = "MEMW_R"
+code = "MWR"
 
 # Variables
 

spec/src/rotxor.toml

@@ -1,4 +1,5 @@
 name = "ROTXOR"
+code = "RTXR"
 
 [[variables.input]]
 name = "a"

spec/src/sha256.toml

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

spec/src/sha256consts.toml

@@ -1,4 +1,5 @@
 name = "SHA256_K"
+code = "SHK"
 
 [[variables.input]]
 name = "index"

spec/src/sha256msgsched.toml

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

spec/src/sha256round.toml

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

spec/src/shift.toml

@@ -1,4 +1,5 @@
 name = "SHIFT"
+code = "SHF"
 
 # Input
 

spec/src/sign.toml

@@ -1,4 +1,5 @@
 name = "SIGN"
+code = "SGN"
 
 [[variables.input]]
 name = "X"