49 Proofs about hashes — calling things by content, not name

49.1 Hash functions and Merkle DAGs#

The hash function BLAKE3-256 reduces bytes of any length to 32 bytes. One property is needed — no pair of different inputs giving the same output can be found (collision resistance). So “the hashes are equal” may be used as “the contents are equal”. This is not proven mathematically but an assumption, and it enters the trusted base (chapter 50). Still, in practice it is sturdier than any other assumption.

49.2 Called by content, not by name#

Ordinary build systems judge caches by file names and modification times. So a file touched with unchanged content is rebuilt needlessly (a loss), and changed content with the same time uses a stale result (a danger). Content addressing drops names and calls things by the hash of their content. lowentc --emit-db gives two hashes per op — iface, the surface observable from outside (signature and contracts), and def, the whole definition. The hash function is BLAKE3-256.

A hash embeds its dependencies by their hashes. Then a definition’s hash reflects the content of everything it depends on, and when one op deep down changes, the hashes above change along with it. The hash itself is dependency tracking. This is a Merkle DAG.

Ops calling each other create cycles. If hash(A) contains hash(B) and hash(B) contains hash(A), the definition goes round. So the cyclic ones are grouped into one bundle (a strongly connected component, SCC). A nameless preliminary hash fixes the canonical order within the bundle, calls inside the bundle carry that order’s number instead of a name, the bundle is hashed once, and each member’s hash is (bundle hash, its number). Contracting strongly connected components leaves an acyclic graph — the same idea as chapter 39′s fixed points appears again.

 A ⇄ B (they call each other)      C ──▶ A

 1  group {A, B} into one block (an SCC)
 2  order the block with nameless preliminary hashes        A = 0 · B = 1
 3  calls inside the block carry the number, not the name   A calls B → "number 1"
 4  hash the block once                                     → H
 5  hash each member as (H, its number)                     hash(A) = h(H, 0) · hash(B) = h(H, 1)
    C carries hash(A) — the graph that is left has no cycles

49.3 What changes a hash and what does not#

module hashed .
rem db

export fn twice input a u64 . output u64 .
do
  return add a a .
end

$ lowentc --emit-db h1_plain.low
fn twice/1 iface:6630705cb68be394 def:73e3a88345444202

module hashed .
rem db

rem adding a comment leaves the hash unchanged
export fn twice input a u64 . output u64 .
do
  rem a comment here too
  return add a a .
end

$ lowentc --emit-db h1_comment.low
fn twice/1 iface:6630705cb68be394 def:73e3a88345444202

H1 — comments change nothing. Both hashes are the same. Fixing a comment does not rebuild the whole project. And a machine keeps the definition of “the same program” as meaning, not bytes.

module hashed .
rem db

export fn twice input a u64 . output u64 .
do
  return mul a 2 .
end

$ lowentc --emit-db h2_body.low
fn twice/1 iface:6630705cb68be394 def:64a7865b02486293

H2 — changing only the body changes only def. Changing add a a to mul a 2 left iface as it was and changed only def. This is the heart of incremental builds. When only an op’s body changes, its users are recompiled, but their iface stays the same too, so the next dependants hit the cache. Signature changes spread along the chain; body-only changes stop after one step.

 main ──calls──▶ util ──calls──▶ leaf        only leaf's body changed

 leaf   def changes · iface stays
 util   recompiled · its iface stays too
 main   cache hit — it stops here

module hashed .
rem db

proc greet input out cap io . input al cap allocator . output u64 . effects io alloc .
do
  let g option mut slice u8 be alloc_bytes al capacity 4 .
  return write_out out 1 "hi" .
end

$ lowentc --emit-db h3_effects_a.low
proc greet/2 iface:d864e930303f7437 def:bebc1fcf6231d282

module hashed .
rem db

proc greet input out cap io . input al cap allocator . output u64 . effects alloc io .
do
  let g option mut slice u8 be alloc_bytes al capacity 4 .
  return write_out out 1 "hi" .
end

$ lowentc --emit-db h3_effects_b.low
proc greet/2 iface:d864e930303f7437 def:bebc1fcf6231d282

H3 — effects are a set. effects io alloc and effects alloc io give the same hash. They once differed, because the clause’s source text was hashed. Then content addressing addressed spelling, not meaning. The grammar says effects are a set, so they are hashed in normalised order.

module hashed .
rem db

export fn twice input a u64 . output u64 .
  requires le a 100 .
do
  return add a a .
end

$ lowentc --emit-db h4_contract.low
fn twice/1 iface:31247d9015a6c804 def:a088ec347ad280ef

Contracts are surface too. Adding requires le a 100 . changed iface. Callers trust and check the contracts of the ops they call, and as seen in chapter 41, contracts are the grounds for removing bounds checks. If a contract changed but the hash stayed the same, the cache would keep using results that trusted the old contract — like reusing a proof after its premises changed. The implementation once hashed only signatures and had this hole; it was fixed.

49.4 What can and cannot be proven#

LowentHash.v separates the two exactly. BLAKE3′s collision resistance is a cryptographic assumption, not a subject of proof. What can be proven comes before it — what the canonical encoding erases and what it keeps.

Unlike effects, contract clauses are not normalised but hashed in written order. So requires A . requires B . and requires B . requires A . have the same meaning but different hashes. It is imprecise. But it is the safe direction. Same meaning with different hashes only runs one more rebuild, while different meanings with the same hash make the cache lie. That this direction is safe is proven too. The asymmetry seen in the interval analysis (chapter 41) and borrow checking (chapter 42) — when unsure, go wide — decided the judgement here too.

49.5 What hashes stop#

The last two lines are the grounds of reproducible builds. Making “the same source gives the same result” comparable is the value of content addressing — it stops being something believed and becomes something compared.

49.6 What is not proven#

• The theorems are about a model. LowentHash.v proves H1, H2 and H3 for the canonical encoding. That the implementation uses that encoding is confirmed by tests on a few examples.
• Normalisation is incomplete. It is sensitive to contract clause order, and how far local variable names or numeric literal spellings (0x10 vs 16) are normalised was not exhaustively checked.
• BLAKE3′s collision resistance is an assumption. If wrong, the cache sees different contents as the same.
• That bundle (SCC) hashes come out the same across implementations is a specification-level promise and not settled. There are several ways to handle cycles.
• What tests guard is not hash values but the relations same and different. If the encoding changes, values change, but the relations must stay.