3. Hashing

Goal: exact compatibility with Unison’s hashing, so UCM can act as an oracle. The facts below were each verified against UCM 1.4.0; docs/hashing-notes.md has the full list.

Step 0: Core to a kernel term

The kernel wants a small term language with names as strings. add becomes (curried):

{ "name": "add",
  "type": { "k": "arrow", "from": {"k":"builtin","name":"Int"},
            "to": { "k": "arrow", "from": {"k":"builtin","name":"Int"}, "to": {"k":"builtin","name":"Int"} } },
  "term": { "k": "lam", "v": "a", "paramType": {"k":"builtin","name":"Int"},
    "body": { "k": "lam", "v": "b", "paramType": {"k":"builtin","name":"Int"},
      "body": { "k": "app",
        "f": { "k": "app", "f": {"k":"builtin","name":"Int.+"}, "a": {"k":"var","name":"a"} },
        "a": {"k":"var","name":"b"} } } } }

Multi-argument functions and calls are curried here, matching Unison. twice refers to add with {"k":"ref","name":"add"}, which the kernel resolves to add’s hash.

Step 1: tokens and accumulate

Everything hashed is a byte sequence built from a few token kinds:

const tag  = (n) => Buffer.from([n]);                    // 1 byte
const nat  = (n) => u64be(n);                            // 8 bytes big-endian
const int  = (n) => i64be(n);                            // 8 bytes big-endian
const text = (s) => cat(nat(utf8len(s)), utf8(s));       // length-prefixed
// a Hashed token is the raw 64-byte digest of something already hashed

const acc = (...tokens) => sha3_512(cat(tag(2), ...tokens));   // "accumulate"

The hash is SHA3-512 (not Blake2b, an early wrong guess), Merkle-style: a node’s hash is built from its children’s hashes, so a change anywhere changes everything above it.

Step 2: by hand, for let x = 1 (type Int)

const termInt = acc(tag(1), tag(65), acc(int(1n)));          // the literal +1
const tyInt   = acc(tag(0), tag(0), acc(tag(0), text("Int")));
const def     = acc(tag(1), tag(4), termInt, tyInt);         // TermAnn: term AND its type
const named   = acc(tag(1), def, acc(nat(0n)));             // component of one member, slot 0
const overall = acc(named);
const id      = base32hex_lower_unpadded(overall);

Running that and the kernel on the same definition prints the identical string, byte for byte:

by hand: 13j0nj3f1fpejjkfbqfj0h7tr9ps4cfaadnb0tiv7gdqud2bhkq1fo20cel7e5go24jepmpc4k2fcbt718hc4ke404pfabkeq094kg8
kernel : 13j0nj3f1fpejjkfbqfj0h7tr9ps4cfaadnb0tiv7gdqud2bhkq1fo20cel7e5go24jepmpc4k2fcbt718hc4ke404pfabkeq094kg8

Two traps the first attempt fell into:

• Even a single definition goes through the component step (named, overall). Skipping it gives a wrong hash.
• A definition is hashed together with its type (TermAnn). So same = add has a different hash from add. Only a reference to add inside other code is just add’s hash.

Variables, and recursion

Variables are de Bruijn indices, so lam a. lam b. a + b and any renaming of it hash the same: names never reach a hash. Mutually recursive definitions form one component (found with Tarjan’s SCC), hashed together; members are ordered by their hash and referenced as #hash, #hash.1, … Two structurally identical members cannot be ordered, an error in both Unison and the kernel.

Results for the running example

add   = cu9eebq1q7omesk7klune6m5kmsc721st2rqmie2oojikesim6nl4um7earv2ogd93rqiliqn6vb9p4ljv4chqofqg4829qd047qlug
twice = uroib53bchrqo3c8t0h4bt6qntkloklp5mtameqvccb2qnsc3sgkjevqnlup6hteug7v9qfot042jqa43jr4g1b1kuv2ui1phu0j2n8

twice’s hash contains add’s hash, not the name “add”. Rename add to plus and twice keeps its identity.

Implementations: packages/kernel (TypeScript, now a CI-only differential check) and packages/kernel-rs (Rust, the real one, also compiled to wasm). Both replay the same fixtures recorded from UCM.

Next: Typechecking.