5. The oracle and the store

The write path

clay add (or Save in the editor) does this, in order:

1. parse strictly            -> AST
2. lower                     -> Core
3. Rust kernel: typecheck    -> types, or a Clay-worded error   (nothing written)
4. Rust kernel: hash         -> hash H_k
5. emit Unison text          -> UCM: typecheck + hash            -> hash H_u
6. if the verdicts or hashes differ: TYPECHECK DISAGREEMENT / HASH DISAGREEMENT, write nothing
7. store objects + names + journal entry, atomically

The emitted text for the running example (this is exactly what UCM receives):

add : builtins.Int -> builtins.Int -> builtins.Int
add a b =
  (builtins.Int.+) a b

twice : builtins.Int -> builtins.Int
twice n =
  add n n

Note the fully qualified builtins. names and explicit signatures: the emitter is boring on purpose. Nothing about UCM’s behaviour is assumed from memory. To add a language feature you first write the Unison program, record UCM’s answer as a fixture, and only then make the kernel agree (the “oracle-first rule”).

Why keep UCM online

The kernel could be trusted alone after enough fixtures, but each write is a fresh, free differential test against the reference implementation. The cost is that writing needs Node and UCM; reading, checking and hashing run in the browser.

The store

packages/compiler/src/store.ts. Three ideas:

• Objects are write-once and never deleted, keyed by hash. That makes rename, undo and forking nearly free.
• Names are labels on hashes, kept per branch. Rename repoints a label and rewrites typed source text scope-aware, refusing anything that would change what a name refers to.
• Every change is a journaled transaction, atomic, one undo step. Undo repoints names back.

objects   : hash -> { core, type, source text }          (immutable, grow-only)
branches  : name -> { names: label -> hash, journal: [...] }

Files and folders are a view: a “file” is an unhashed label on a term. Saving a file means “this file now contains exactly these terms”: editing re-derives dependents, removal is refused while a term is in use.

clay verify re-hashes every stored object without UCM and compares to its key, so a corrupted store is detectable offline. Because objects are immutable and unions of object sets are valid, the same design maps onto a bring-your-own object bucket with one compare-and-swap pointer per branch (packages/storage).

Next: Data types.