NETHER C / PUBLIC TERMINALREAD ONLY
█   █ █████ █████ █   █ █████ ████     ████
██  █ █       █   █   █ █     █   █   █
█ █ █ ████    █   █████ ████  ████    █
█  ██ █       █   █   █ █     █  █    █
█   █ █████   █   █   █ █████ █   █    ████

a C dialect in which nothing runs_

07 The ledger

§ 07 · draft · depth 5 · edit the source

The ledger

The format is the contract. Everything else in this specification is negotiable; an ambiguity here is a reproducibility bug that will be found years from now by somebody who cannot fix it.

7.1 Canonical encoding

Frozen. Every value has exactly one encoding, on every platform, forever. Changing anything in this section changes the domain separator in §7.2, which changes every cairn that has ever existed. Treat it as immovable and mean it.

A value is a tag byte followed by a payload. There is no length prefix on the value as a whole and no terminator: every payload's extent is determined by the tag and by lengths inside it.

TagTypePayload
0x00U0empty
0x01Boolone byte, 0x00 or 0x01, and nothing else
0x02I64eight bytes, two's complement, big-endian
0x03Bytesu64 length, then exactly that many bytes
0x04Stru64 length, then exactly that many bytes of well-formed UTF-8
0x05Cairnthirty-two bytes
0x06Shadeone byte origin stratum, then the thirty-two byte cairn of the value
0x07Answerone byte, 0x00 given or 0x01 refused, then the value or the refusal
0x08Refusalone byte, 0x00..0x05, in the order §5.1.1 lists them
0x10Structu64 name length, the name in UTF-8, u64 field count, then the fields
0x11Arrayu64 element count, then the elements
0x20Nodesee §7.3

Rules an implementation MUST follow:

  1. Integers are fixed-width big-endian. There is no variable-length integer encoding anywhere in the format, including lengths.
  2. Lengths and counts are u64 big-endian, even where the value is small. Eight bytes to say 0 is the price of there being one encoding.
  3. Struct fields are encoded in declaration order, not alphabetical order, and the struct's type name is encoded with it. Nominal typing means the name is part of the value.
  4. There is no map type, and therefore no question of key ordering. An association is an array of pairs, and its order is the program's.
  5. There is no floating-point type. See §3.6.
  6. The encoder does not transform what it is given. It does not normalise text, reorder anything, or trim anything. A store that silently alters the bytes you handed it is not content-addressed; it is content-addressed to something else. See §7.1.1.

7.1.1 What a decoder MUST reject

Lenient decoding of a canonical format is how two implementations start disagreeing, so rejection is specified rather than left to judgement. A decoder MUST reject:

  • a tag byte not in the table above;
  • a Bool payload other than 0x00 or 0x01;
  • a Str payload that is not well-formed UTF-8;
  • a Shade origin byte greater than 8;
  • an Answer discriminant other than 0x00 or 0x01;
  • a Refusal code greater than 0x05;
  • a Struct whose name is empty, or whose name is not well-formed UTF-8;
  • any length or count that exceeds the bytes remaining;
  • trailing bytes after a complete value.

A decoder MUST NOT accept an input and then re-encode it differently. For every byte string b that decodes to a value v, encode(v) MUST equal b. That round trip is the definition of canonical and is the property worth testing first.

7.2 Cairns

cairn(v) = blake3( DOMAIN || encode(v) )
DOMAIN   = b"netherc/cairn/v4\x00"

A cairn is 32 bytes. Its text form is lowercase hexadecimal. Tools MAY display a prefix; the first 8 hexadecimal characters are the RECOMMENDED short form, and any tool that accepts a short form MUST reject an ambiguous one rather than picking a match.

The domain separator is versioned. Changing what an existing tag means changes the domain, which changes every cairn, which is the correct and honest consequence: values encoded under different rules are not the same values.

Adding a tag that was previously unassigned does not. A decoder under v1 rejected 0x07 as unknown and still does not accept anything it accepted before; every byte string that had a meaning keeps exactly the meaning it had. Nothing is reinterpreted, so nothing is renamed.

This is the narrower rule, and it is narrower because the broad one made the format unable to grow without discarding everything ever written under it. §90.2 records what was given up to narrow it.

The domain is at v4. It has moved three times, every time because Trace changed what it holds (§7.3.1): to v2 when a residue stopped being nodes, to v3 when a trace began naming its witnesses, and to v4 when it stopped recording what the burial spent. Each is the bumping case and not the exempt one — a byte string that decoded to a trace under one domain decodes to a different trace under the next, and the two are not the same value however similar they look. Nothing had been buried any of those times, so the bumps cost nothing. That is the only reason they were affordable, and it is why the rule is worth having before it is not.

7.3 Nodes

A node is the unit the ledger stores. Every node is content-addressed by its cairn.

NodeContents
Literala value
Applya function cairn, argument cairns, and the resulting value cairn
Holethe fields listed in §6.3
Deposita value cairn and the source span that deposited it
Witnessa stratum, a call, the answer, and the span that asked
Tracethe residue, the holes, the witnesses, the deposits, the source, the depth, and the stratum-8 mark

Nodes reference other nodes only by cairn. The graph is therefore acyclic by construction: a node cannot name a node that does not yet exist, and a node that exists cannot change.

7.3.1 Node encoding

Frozen, on the same terms as §7.1. A node is the tag 0x20, then a kind byte, then the kind's payload.

KindNodePayload
0x00Literalone value
0x01Applycairn of the function, cairn-list of arguments, cairn of the result
0x02Holecall, one byte stratum, span
0x03Depositcairn of the value, span
0x04Witnessone byte stratum, call, cairn of the answer, span
0x05Tracecairn of the residue source, cairn-list of holes, cairn-list of witnesses, cairn-list of deposits, cairn of the source buried, one byte depth, one byte stratum-8 mark

Three shapes appear inside more than one of them:

ShapeEncoding
cairn-listu64 count, then that many thirty-two byte cairns
spancairn of the source, u64 start, u64 end
callu64 name length, the name in UTF-8, cairn-list of arguments

A Trace's three cairn-lists are not all the same kind of list, and the difference is worth stating because both readings decode.

The deposit list holds one entry per deposit the program made, and may name the same cairn more than once. A value deposited a thousand times from one span is one Deposit node — same value, same span, so one content address — and a thousand entries. The node is what the program said; the list is what it did, and §4.7 makes a bare expression statement an act of the program rather than a declaration about it.

The hole list holds one entry per question the burial left open, and is the same kind of list for the same reason. At a read stratum two asks are one hole and one entry; at 4, 6, 7 and 8 they are two acts and two entries, and two acts written in one place are two entries naming one node. §6.3 is which of those a given pair is.

A decoder MUST reject, in addition to the clauses in §7.1.1:

  • a kind byte not in the table above;
  • a stratum or depth greater than 8;
  • a stratum-8 mark other than 0x00 or 0x01;
  • a call with an empty name;
  • a span whose end is before its start.

A span names its source by cairn rather than by path. A path is a fact about one machine at one moment; the trace has to mean the same thing on a machine that has never seen that filesystem.

7.3.2 What a decoder cannot check

A Trace's depth is how deep it goes, counting both directions at once: the join of the depth of its residue, the greatest stratum of any Hole it names, and the greatest stratum of any Witness it names.

All three are needed and no two are enough. A stage-one burial has answered nothing, so its witnesses say 0 and its residue and holes say how deep the program still reaches — which is why §8.2's transcript reads depth 3 over a program with one unanswered read. A sealed trace has no holes left, so its residue says 0 and its witnesses say how deep it went — which is why §6.6's reads depth 3 holes 0. One rule, both transcripts.

seal is the case that rules out the residue alone. §1.5 makes seal e depth 0 whatever e is, so a program that reaches the world only through a seal demands something pure and still owes a hole:

nether c
// owed.nc — a trace that owes the network. spec/07-ledger.md §7.3.2.
//
// The fetch is demanded only through a seal, and §1.5 makes a seal pure, so
// the residue is at depth 0 and the hole is at 5. The trace's depth is the
// join of both.
Bytes@5 page = must(descend net { get("https://example.invalid/x") });
Cairn   c    = seal page;
demand c;
shell
$ nether bury owed.nc
buried   owed.nc → 8baa0677   depth 5   holes 1   4 nodes
  hole ①  get("https://example.invalid/x") stratum 5  net

That trace cannot take a step without a network fetch, and calling it pure would be the strongest claim the language makes, made falsely.

opaque is the case that rules out the holes alone: a world-question inside an opaque barrier is never evaluated and never becomes a hole, and the expression is still at its stratum.

The stratum-8 mark is the other half of §1.7 and is not the same test. It is set exactly when a Witness the trace names is at stratum 8 — reached, not owed. A trace whose only stratum-8 call is still a hole has depth 8 and is not marked, because nothing has happened off the record yet.

Neither claim is checkable on put. A decoder sees one node, and both are facts about a graph that may not be wholly present. An implementation MUST NOT be required to enforce them there. §8.6 is where the hole and witness halves are caught, because strata is the rite that has the whole graph in hand. The residue half needs lowering the residue, which is burying it, and that is bury's job rather than strata's.

7.4 Provenance

Provenance is not a separate index. It is the Apply and Witness nodes themselves, read backwards: given a value's cairn, the ledger can find every node that produced it, and from those, their inputs, down to literals and holes.

An implementation MUST maintain a reverse index sufficient to answer what produced this cairn in time proportional to the answer, not to the size of the store. nether lamp --provenance is unusable otherwise, and it is the rite that makes the language comprehensible.

7.5 The store

The store is a set of (cairn, bytes) pairs, where the bytes are the canonical encoding of a value or a node. Both have cairns and both are addressed the same way: a Deposit names the value it deposited directly, rather than naming a Literal node that wraps it.

put(stored)  -> Cairn      idempotent
get(Cairn)   -> Stored     fails if absent
has(Cairn)   -> Bool
resolve(hex_prefix) -> Cairn | Ambiguous | Absent

put MUST be atomic: a reader MUST never observe a partially written node. An implementation SHOULD write to a temporary path and rename.

Because writing is idempotent and content-addressed, concurrent writers need no coordination beyond atomicity of the individual write. Two burials that compute the same value write the same bytes to the same place.

7.5.1 What survives a crash

A store is crash-consistent and not durable. A put that returned may not be on the disk after a power loss, and an implementation MAY fsync but is not required to.

What a store MUST NOT do is serve bytes that are not what the name says. That is what makes the weaker promise enough. After a crash an object is in one of two states, and both are safe:

  • absent, which is indistinguishable from never having been written, and which a later put repairs by writing it again;
  • present and wrong, which get catches, because the name is the content and checking costs one hash of bytes it has already read.

So a crash can lose work and cannot manufacture a fact. That is the property the reproducibility claims in this document rest on, and it is weaker than durability on purpose: a build tool that paid for an fsync per node would pay it thousands of times for a single burial, to protect work it can simply do again.

An implementation MUST NOT skip the check in get on the grounds that it fsyncs. The check is against bit rot and a bad disk as much as against a crash, and those do not announce themselves.

The reverse index of §7.4 is a set of fixed-size records. An implementation MUST detect a partial one rather than read past it — a record half written is a record that would otherwise be read as a different cairn, and a wrong edge in a provenance walk is worse than a missing one.

7.5.2 What a damaged store can still tell you

get checks one object when something asks for it. A read-only audit of the whole store walks every entry on disk without modifying anything and separates four kinds of damage:

  1. Corrupt objects — files under objects/ whose names are valid cairns and whose bytes either do not decode or do not hash to that name.
  2. Missing references — cairns named by the forward references of a verified node (§7.4) that are absent from objects/.
  3. Malformed filenames — entries under objects/ or refs/ whose path is not a two-hex-digit fan-out directory followed by a sixty-two-hex-digit file.
  4. Derived-index errors — ragged files in refs/ (§7.5.1) or forward edges of verified nodes that are missing from refs/.

Which traces are affected MUST be derived from verified forward edges and not from refs/: a broken reverse index does not damage a trace, and a missing reverse edge would hide one that is damaged. When a trace's holes, witnesses or deposits list names a corrupt or absent node, what that node in turn referenced cannot be read, and the audit MUST mark the trace's reachability as incomplete rather than claiming its listed faults are the whole of what was lost. Healthy objects and healthy traces remain readable while damaged ones are reported.

7.5.3 A second store, and what they owe each other

Two stores under the same domain separator (§7.2) have a set-difference problem and nothing else: a cairn is either present or absent, and if it is present and verified (§7.5.1), it names the same canonical bytes in both.

Possessing or naming a cairn establishes byte identity and nothing else:

  • It does not establish availability. A store holding a Trace node may lack the nodes or values its lists name (§7.3.2).
  • It does not establish authentication or mutation authority. Knowing a cairn is not permission to write to another store, and a store that accepts writes from a peer does so under its own capability gate, never because the peer knew a name.
  • It does not establish agreement about what the world said. Two stores that exhumed the same stage-one trace against different worlds hold different Witness nodes and therefore different sealed Trace cairns. Reconciling them keeps both traces and both witnesses without conflict, because their cairns differ.

Root closure and bounded comparison

Reconciliation is defined over an explicit set of root cairns $R$, never over an unrooted enumeration of a peer's store. For a verified object at cairn $c$, its immediate forward references $\operatorname{refs}(c)$ are empty when $c$ decodes to a Value (0x00..0x11) and are the cairn fields of its payload (§7.3.1) when $c$ decodes to a Node (0x20). The root closure $\operatorname{cl}(R)$ is the least set containing $R$ and closed under $\operatorname{refs}$. Because the node graph is acyclic by construction (§7.3), $\operatorname{cl}(R)$ is finite.

An exchange proceeds top-down in bounded rounds from a frontier Queue initialized to $\{r \in R \mid \neg\text{has}(r)\}$:

  1. Domain handshake. Both sides state their domain separator (netherc/cairn/v4\x00, §7.2). A peer speaking any other domain MUST be refused before any cairn is requested or any object is read (§7.7).
  2. Bounded want batch. The requester pops at most MAX_WANT (1,024) full 32-byte cairns from its frontier and asks the peer for them.
  3. Bounded response. For each requested cairn $c$ in batch order, the peer checks its own copy via get(c) and replies with either:
  4. object(c, bytes), where len(bytes) does not exceed MAX_OBJECT_BYTES (16 MiB), or
  5. absent(c) if the peer does not hold $c$. A peer whose local copy of $c$ fails verification MUST NOT transmit the corrupt bytes; it MUST treat $c$ as locally corrupt and refuse to serve it.
  6. Receiver verification and frontier expansion. For each object(c, bytes) received, the requester MUST:
  7. reject the response if $c$ was not in the current want batch or if len(bytes) > MAX_OBJECT_BYTES;
  8. decode bytes under §7.1.1 and §7.3.1, verifying encode(decode(bytes)) == bytes;
  9. verify cairn(bytes) == c under DOMAIN;
  10. commit (c, bytes) via put (§7.5), which derives the local reverse index entries in refs/ before atomically placing the object in objects/;
  11. for each $d \in \operatorname{refs}(c)$ with $\neg\text{has}(d)$, push $d$ onto the frontier.

Only canonical objects are exchanged. The reverse index refs/ (§7.4) and burial memo (§8.2.1) MUST NOT be transmitted or accepted from another store; every receiver derives its own index from objects it has verified itself.

Interruption, resume and discovery privacy

Because each verified object is committed atomically via put before its children enter the frontier, an interrupted exchange leaves the receiving store clean (§7.5.2) with a verified upper prefix of $\operatorname{cl}(R)$ already on disk. Repeating the exchange for $R$ tests has at each step, skips the prefix already present, and asks only for the remaining frontier.

A peer answers only about full 32-byte cairns named in a want batch. Prefix resolution (resolve, §7.2) and store-wide listing are local operations and MUST NOT be answered for an untrusted peer, so a stranger cannot enumerate private traces by probing two-character fan-out prefixes. Asking want(c) still discloses to the peer that the requester knows the cairn $c$ (§90.3).

Strata of exchange

Reading objects from a second directory on the local filesystem is a stratum-3 (disk) read coupled with a stratum-4 (disk!) write to commit verified objects into the receiving store. Fetching missing objects from a remote store over a socket is a stratum-5 (net) read coupled with stratum 4 (disk!) locally. Actively pushing (send) objects to a remote store is a stratum-6 (net!) act, because it alters state outside the machine and cannot be unsent (§1.8).

Exchange transcripts

Four transcripts fix the observable behaviour across equal, partial, divergent and hostile peers:

text
# 1. Equal stores: local already holds cl({efed9b2a}) (6 objects)
domain  netherc/cairn/v4
root    efed9b2a
round 0 want 0 (6 already present)
result  reconciled efed9b2a: 6 present, 0 fetched, 0 absent
text
# 2. Partial peer: local has nothing; peer holds efed9b2a but lacks witness 9a40c112
domain  netherc/cairn/v4
root    efed9b2a
round 0 want [efed9b2a]
        recv object efed9b2a (Trace, verified)
round 1 want [61a6cc41, 9a40c112, 3f08d119, 8106589a]
        recv object 61a6cc41 (Bytes, verified)
        recv absent 9a40c112
        recv object 3f08d119 (Deposit, verified)
        recv object 8106589a (Bytes, verified)
round 2 want [04e2b771]
        recv object 04e2b771 (Str, verified)
result  incomplete efed9b2a: 5 fetched, 1 absent (9a40c112)
text
# 3. Divergent stores: two exhumations of 76c4b655 with different world answers
domain  netherc/cairn/v4
roots   efed9b2a 4c19e08d
round 0 want [4c19e08d] (efed9b2a already present: 6 objects)
        recv object 4c19e08d (Trace, verified)
round 1 want [d17a8803, 5b2209ce] (residue 61a6cc41 and source 8106589a shared)
        recv object d17a8803 (Witness, verified)
        recv object 5b2209ce (Deposit, verified)
round 2 want [7e91a440]
        recv object 7e91a440 (Bytes, verified)
result  reconciled 2 roots: 6 shared, 4 fetched, 0 absent
text
# 4. Hostile peer: serves tampered bytes for 21ca4ef0 (hash is b8019f44)
domain  netherc/cairn/v4
root    76c4b655
round 0 want [76c4b655]
        recv object 76c4b655 (Trace, verified)
round 1 want [61a6cc41, 21ca4ef0, 8106589a]
        recv object 61a6cc41 (Bytes, verified)
        recv object 21ca4ef0 -> refused: corrupt from peer (asked 21ca4ef0, found b8019f44)
result  aborted 76c4b655: peer served corrupt bytes for 21ca4ef0 (2 committed, 21ca4ef0 not written)

7.5.4 Moving a store

Moving a store to another machine by copying its directory copies refs/, memo/ and tmp/, none of which is canonical, and verifies nothing at the destination. A portable bundle carries only verified canonical objects in a single self-checking stream:

text
BUNDLE = DOMAIN                      # b"netherc/cairn/v4\x00" (17 bytes, §7.2)
       || b"bundle\x00"              # 7-byte stream marker
       || u64_be(count)              # number of objects in the bundle
       || ENTRY * count
       || blake3(all preceding bytes) # 32-byte whole-stream trailer
ENTRY  = cairn (32 bytes)
       || u64_be(len)                # byte length of canonical payload
       || payload (len bytes)
  • Export (export). Walks objects/, verifies every object against its cairn and the canonical decoder (§7.1.1, §7.3.1), and refuses to export if any object is corrupt or any filename under objects/ is malformed (§7.5.2). Verified objects are emitted in topological dependency order (every referenced object in the store before the nodes that reference it, with ties broken lexicographically by cairn) so any prefix of the stream is closed under in-store forward references. refs/, memo/ and tmp/ are omitted.
  • Import (import). Checks the 24-byte header, refusing an unknown magic or a mismatched domain version (§7.7) before reading entries. For each of the count entries, import enforces len <= MAX_OBJECT_BYTES (16 MiB) before allocating, rejects duplicate cairns within the bundle, verifies canonical decoding and cairn(payload) == cairn before touching the destination store, and then commits the object:
  • if the destination store does not yet hold cairn, via put (§7.5), which writes reverse edges to refs/ first and atomically renames the object into objects/;
  • if the destination store already holds cairn, by verifying the existing on-disk object via get(cairn) without overwriting it, and ensuring all of its reverse edges are present in refs/. After all count entries are read, import verifies the 32-byte blake3 trailer over the stream and requires end-of-stream with no trailing bytes.
  • Interrupted or truncated import. Because entries are ordered leaves-before-referrers and each entry is verified before it is committed, an import interrupted or truncated at any byte offset leaves the destination store clean (§7.5.2) with a verified, dependency-closed prefix of the bundle. Re-running import with the complete bundle verifies the already-present prefix in place without overwriting it and commits the remainder.

7.5.5 Packages

A package is an ordinary canonical Struct value (§7.1, tag 0x10) stored in the ledger and addressed by its cairn. There is no central registry and no version-range solver: a dependency is the exact cairn of another package value, and resolution is an offline lookup in a verified store.

A package root is a Struct with type name "Package" and three fields in declaration order:

FieldTypeMeaning
domainStr"netherc/cairn/v4" — the canonical domain (§7.2, without the trailing NUL) under which the package and its closure were formed
entrypointCairnthe cairn of a Bytes value in the store holding the package's well-formed UTF-8 source unit (§3.1)
depsArray of Struct "Dep"direct dependencies, sorted in strictly ascending byte order of alias

Each element of deps is a Struct with type name "Dep" and two fields in declaration order:

FieldTypeMeaning
aliasStrlocal human-readable alias (non-empty, unique within this package's deps)
cairnCairnexact 32-byte cairn of the dependency "Package" value

An implementation that writes or resolves a package MUST enforce five rules:

  1. Canonical dependency order. Within a "Package" value, deps MUST be ordered by strictly ascending UTF-8 bytes of alias with no empty or duplicate alias, so a given entrypoint and dependency set have exactly one encoding and one cairn.
  2. Local aliases, global cairns. An alias is local to the "Package" value that declares it. Two packages in one closure MAY bind the same alias to different dependency cairns or different aliases to the same dependency cairn; global identity is always the 32-byte cairn.
  3. Compatibility check. Before walking entrypoint or deps, resolution MUST check that domain equals "netherc/cairn/v4". A package whose domain names any other version (§7.7) MUST be refused explicitly as incompatible rather than interpreted.
  4. Offline closure and topological order. Resolution reads every reachable "Package" and entrypoint Bytes object from the local store via get (§7.5.1), walking deps depth-first in deps order and emitting each distinct package cairn once in topological post-order (every dependency before the packages that depend on it, ending with the root package). The resolved source unit is the concatenation of each package's verified entrypoint bytes in that topological order, addressed by the cairn of the resulting Bytes value.
  5. Explicit failure on missing, corrupt or malformed objects. A cairn establishes byte identity, not availability. If the root package, any transitive dependency package, or any entrypoint Bytes object is absent from the store, fails verification on get, is not a well-formed "Package" or UTF-8 Bytes value, or forms a dependency cycle, resolution MUST fail explicitly naming the offending cairn and reason. It MUST NOT fetch from the network or substitute an empty unit.

7.6 Garbage

There is none.

A content-addressed store of immutable values has no unreachable objects, only objects nothing currently points at — and the entire premise of the language is that something might point at them later. Deleting a node destroys a provenance chain that another trace may depend on, and there is no way to know that it does not without reading every trace that will ever exist.

An implementation MAY provide an explicit, operator-invoked prune with a stated reachability root. It MUST NOT prune automatically, and it MUST NOT prune Witness nodes at all: a witness is the only copy of something the world said once and may never say again.

This is a real cost, stated plainly: a Nether C store grows monotonically. Whether that is affordable is a question the roadmap item The store: layout, index, and garbage has to answer with measurements rather than opinions.

7.7 Versioning

The format carries no version field inside a node. The version is the domain separator in §7.2.

An implementation encountering a cairn it cannot verify under its own domain MUST report that the node was written under a different format version and refuse it. It MUST NOT attempt to interpret it. There is no migration path between format versions and there is not meant to be one: a value encoded under different rules is a different value, and pretending otherwise would make every reproducibility claim in this document conditional.

END OF BUFFERBack to text ^