§ 08 · draft · depth 0 · edit the source

The rites

Six verbs. The one that is missing is the point.

8.0 There is no run

An implementation MUST NOT provide a command that executes a Nether C program without producing a trace, under any name.

nether run MUST exit with code 64 and explain what to use instead.

$ nether run hello.nc
nether: there is no `run`.

  A Nether C program is not executed. It is buried — evaluated as far as the
  world allows — and what remains is a trace and the holes the world still
  owes an answer to.

  You probably want:

    nether bury <file.nc>     to evaluate it
    nether exhume <cairn>     to answer its holes
    nether lamp <cairn>       to see what it left behind

It is spelled out here, in the specification, so that it is a rule rather than a joke, and so that anyone proposing to add it has something to argue against.

This is the only frozen requirement in this draft.

8.1 Common behaviour

Every rite:

• accepts --json and, when given it, writes a single JSON object to stdout and nothing else;
• writes human-readable output to stdout and diagnostics to stderr;
• treats a cairn argument as a full cairn or an unambiguous hexadecimal prefix, and MUST fail on an ambiguous prefix rather than choosing;
• names a source position by the cairn of the source and not by a path, because that is all a span holds (§7.3);
• exits with a code from §8.8.

No rite writes to the ledger except bury, exhume and graft, and each of those writes before it prints.

8.2 bury

nether bury <file.nc> [--grant <cap>]... [--fuel <n>] [--json]

Evaluates as far as the granted capabilities allow; writes a trace; prints a summary of what was written.

$ nether bury build.nc
buried   build.nc → 76c4b655   depth 3   holes 1   4 nodes
  hole ①  read("main.nc")                stratum 3  disk

--grant names exactly one capability and MAY be given any number of times. One implies no other, in either direction: --grant net does not permit a read and does not permit a post. An operator who wants a burial to read files and fetch URLs writes both, which is the whole of the audit (§2.1).

With no --grant, burial holds no capabilities and every world-touching expression becomes a hole. This is the default because it is the only default that cannot surprise anyone.

Until §8.3 is built, an implementation that cannot honour a grant MUST refuse one rather than accept it and evaluate as though it were not there. A flag that validates its argument and changes nothing looks like it worked, which is the failure §8.0 is about in a smaller place.

--fuel sets the budget of §6.4. Its default MUST be finite, and the rite MUST report what it was when asked.

It is not recorded in the trace, because it cannot have affected one. Running out of fuel produces a halt and no trace at all (§6.4), so a budget has exactly two outcomes: the burial finished, or there is nothing to record it in. A budget that did not bind left no mark, and a budget that bound left no trace.

Nor is what the burial spent, and for the same reason one step further on. How many steps a burial took is a fact about that burial rather than about the program it produced, and a trace that recorded it could not be replayed: §6.7 asks a sealed trace to come back byte-identical, and replaying buries a residue that is already folded, which is a cheaper burial. A rite reports what it spent, because that is where it is a fact.

8.2.1 Burying what is already buried

A burial with no --grant is a function of two things: the source, and the implementation burying it. Nothing else can reach it — it holds no capability, and §6.4 makes its fuel deterministic — so burying the same bytes twice with the same implementation produces the same trace, to the cairn, and the second time is work the first already did.

An implementation MAY remember. It keeps a memo from the pair (its own identity, the source's cairn) to the trace that burial wrote and the steps it spent. The memo is an index in §7.4's sense, not part of the ledger: it holds no fact the store does not, and losing it loses time and nothing else.

Its identity MUST change whenever what it would bury could, and a version number nobody remembered to bump does not. The cairn of the implementation's own executable is one that cannot be forgotten.

A remembered burial MUST be indistinguishable from a fresh one in everything but time:

• It is honoured only if the trace is there. The memo names a cairn, and get on it MUST return a Trace whose source is that source and which names no witness. Anything else is a stale entry, and the rite buries.
• It is honoured only within budget. A fresh burial that needed more steps than --fuel allows halts at the step where the budget ran out, and §6.4 requires every implementation to halt there. So a memo whose steps exceed the budget is not honoured, and the burial runs out exactly where it would have.
• It reports what the burial costs. The steps the rite reports are the ones recorded, which are the ones a fresh burial spends, so two implementations agree on them whether or not either remembered. The rite MUST also say that it remembered, because that is the fact about this invocation.
• It writes nothing new. Everything the trace names is already in the store, or the first rule refused the entry.

Burying §8.2's program a second time:

$ nether bury build.nc
buried   build.nc → 76c4b655   depth 3   holes 1   4 nodes   remembered
  hole ①  read("main.nc")                stratum 3  disk

Burial still holds no capability. Reading a memo is the rite consulting its own index before it buries, the way writing the trace afterwards is the rite and not the program; the program asks the same questions of the same world either way, and a burial with a --grant is never remembered, because the world it asked may answer differently next time.

8.3 exhume

nether exhume <cairn> [--grant <cap>]... [--declare <name>=<value>]...
                      [--clock <seconds>] [--target <triple>] [--root <path>]
                      [--reach <host>]... [--load <path>]... [--replay] [--json]

Grants capabilities, answers holes, records every answer, re-buries the residue, and writes a new trace.

--replay grants nothing and serves only from the ledger. It MUST fail rather than reach the world if an answer is missing, and it MUST report the first node whose cairn differs from the original.

--grant and --replay are mutually exclusive.

8.3.1 Declaring an environment

The three flags are the declaration §9.4 puts outside the program. They are the whole of what env may answer from, and an implementation MUST NOT read the process environment, the wall clock or the host triple to fill any of them in.

--declare MAY be given any number of times, including with an empty value: --declare CC= declares CC and leaves it unset, which is the refusal §9.4 distinguishes from the collapse. A name given twice is an error rather than a last-one-wins, because the two invocations differ and only one of them can be what was meant.

--clock is whole seconds since the Unix epoch and --target is a triple, and both are required whenever env is granted. There is no default. A default would be the host's, and a rite whose answer depends on which machine ran it is the thing §6.7 exists to prevent.

Granting env and declaring nothing is legal and means an environment in which every name is undeclared. Declaring without granting env is an error: the declaration could not be read, so accepting it would be §8.0's failure in a smaller place.

8.3.2 Declaring a reach

--reach names one host net and net! may open a socket to. It MAY be given any number of times, and a host nobody named is denied (§9.6).

The reasoning is the one an implementation already applies to the disk. §09 says nothing about where a path is rooted, and an implementation that rooted it nowhere would be one nobody could grant a capability to; a socket is the same argument with a longer reach. --grant net says which stratum, and --reach says how far.

A host is a name and optionally a port: example.com, or example.com:8080. Without a port it matches whatever port the URL asks for, because the port is a detail of the service and the host is the party being trusted. It matches that host exactly — a subdomain is a different party, and a reach that spread to one would be a reach nobody declared.

That default is the widest thing any flag in this section does, and it is worth saying rather than implying: --reach example.com permits 22 and 25 and 6379 on that host as readily as 443, and the program chooses which. What it declares is the party trusted, not the service used. An operator who means one service writes the port, and §90.2 records the narrower default that was considered.

Granting net and reaching nothing is legal and means a network with nothing in it, which is the right default for the same reason as no --grant at all. Reaching without granting net is an error, on §8.3.1's reasoning.

8.3.3 Declaring what may be loaded

--load names one shared object unrecorded may load. It MAY be given any number of times, and a symbol found in nothing named is denied.

A symbol is looked for in the objects in the order they were given, and the first that has it answers. Order is the invocation's and not the loader's, because two objects that both define a symbol is a question only the person running the rite can settle.

Granting unrecorded and loading nothing is legal and means no foreign code, which is the one case where the useless invocation is also the safe one. Loading without granting unrecorded is an error, on §8.3.1's reasoning.

This is the same argument as §8.3.2 in the place it matters most. A stratum-8 call that may load any object on the machine is ambient authority, and §1.7 already says this stratum is the one that has to be quarantined loudly.

8.3.4 Declaring a root

--root names the one directory disk and disk! resolve every path against. It is required whenever either is granted, and there is no default, on §8.3.1's reasoning: the only default available is the directory the rite happened to be run in, and a rite whose answer depends on where it was run is what §6.7 exists to prevent. Rooting without granting disk is an error, on the same reasoning again.

This is the flag §8.3.2 was already arguing from. It makes its case for --reach by pointing at the disk — §09 says nothing about where a path is rooted, and an implementation that rooted it nowhere would be one nobody could grant a capability to — and then the disk was the one capability the invocation could not bound. Two implementations answered read("main.nc") differently while the hole's call was byte-identical, and §6.3 makes that call the whole of what the question is.

A path is resolved against the root and MUST NOT climb out of it. A path that would — .., an absolute path, a drive letter — is denied and not absent: the file may well be there, and what refused is this build. That is §9.9's distinction, and §9.5 gives both refusals to every path-taking function for exactly this.

Textual resolution is not enough on its own, and an implementation MUST also refuse a path that leaves the root through a symbolic link. Nothing textual can see one, and a program buried with disk! can make one for itself to read back through.

--root MAY be given once. A path does not name its root the way a URL names its host, so a second root makes every path ambiguous and a write undecidable — which is why --reach repeats and this does not.

8.4 lamp

nether lamp <cairn> [--provenance] [--depth <n>] [--json]

Carries light down. With no flags, renders the value at that cairn — including every Deposit node in a trace, in the order they were made, which is how a program's output is read.

That order is the trace's own deposit list (§7.3.1). A trace exhumed from another names the earlier trace's deposits first and then what burying its residue deposited, each in evaluation order, so the list is the order they were made in. lamp MUST NOT reorder it. Two spellings of one program that make the same deposits read the same, whatever their sources' cairns are.

$ nether lamp efed9b2a
Hello from the nether

A value deposited more than once is rendered more than once. The trace holds one entry per deposit (§7.3.1) and lamp renders one line per entry, so a loop that deposits on every turn reads as the program wrote it rather than as the ledger stored it:

$ nether lamp cbd2ade7
tick
tick
tick
tick

--provenance walks backwards instead: from a value to the nodes that produced it, to their inputs, to the literals and holes at the bottom.

$ nether lamp 21ca4ef0 --provenance
21ca4ef0  hole     read("main.nc")   stratum 3
└─ trace    depth 3   residue 61a6cc41   1 hole(s)   0 witness(es)   0 deposit(s)

That is the walk over the trace from §8.2, which has a hole and no answers yet: the hole, and the trace waiting on it. Once §8.3 has recorded a witness the same walk reaches it, which is what §7.4 means by the forward edge read backwards — a hole records no dependents and does not need to.

lamp is a tool the operator carries, not a capability the program holds. A program cannot invoke it, cannot reach a terminal, and has no way to know whether anyone is looking. This separation makes it structurally impossible for a Nether C program to leak to a log.

8.4.1 Inspecting a byte offset in an editor

nether lamp <cairn> --at <byte> [--source <path>] [--depth <n>] [--json]

Inspects an already buried Trace node at a 0-based UTF-8 byte offset <byte> into its source (§7.3). An editor adapter calls this rite instead of reimplementing the depth checker or running a stateful language server.

1. Named source versus stale buffer. A trace's spans are byte offsets into the Bytes value named by trace.source. When --source <path> is given, lamp hashes the bytes at <path> as a canonical Bytes value (§7.1) and compares that cairn against trace.source. If the two cairns differ, the editor buffer is stale with respect to the trace, and lamp MUST refuse with exit code 1 naming both short cairns rather than guessing shifted offsets.
2. Absent objects and bounds. lamp reads the Bytes value at trace.source from the store. If trace.source or any reachable trace node covering <byte> is absent or corrupt, lamp MUST fail with exit code 1 reporting the store error. If <byte> is at or past the byte length of trace.source, or falls outside every expression in the unit, lamp MUST fail with exit code 1 rather than clamping the offset.
3. Depth, origin and provenance from the compiler and ledger. lamp runs the parser, lowerer and depth checker on trace.source and reports for <byte>:
4. the innermost expression whose byte span start..end contains <byte>, its derived depth 0..8, its type, and its byte span start..end;
5. the innermost enclosing descend κ span (if any) and the deepest call inside the expression (if any) responsible for its depth; and
6. any recorded Deposit, Hole or Witness node under <cairn> whose span covers <byte>, together with its cairn, summary and backward provenance walk (§7.4) up to --depth <n>.

8.5 cairn

nether cairn <path> | --verify <cairn> [--json]

Names a thing by its content, or checks that a name still holds. --verify MUST report what differs, not merely that something does.

8.6 strata

nether strata <cairn> [--json]

Blame for depth. Reports the deepest stratum a trace reached and the source span that took it there.

$ nether strata 76c4b655
depth 3   disk

  3  read("main.nc")           8106589a:10:35   pending
  0  everything else

  replayable: yes
  of that, 0 (pure) has happened; the rest is what exhuming will cost.

Holes are reported apart from witnesses, because they are not the same depth: a hole is a stratum the trace will need and a witness is one it reached (§7.3.2). A trace that has answered nothing has reached nothing, and that is the line under the list rather than the number above it: the transcript is one of those traces — one read, still pending — and its number is what §7.3.2 says a trace's depth is.

If the trace is marked as having reached stratum 8, or if any witness under it reached stratum 8, strata MUST say so without being asked, and MUST report replayable: no. A hole or a witness deeper than the recorded depth, or a stratum-8 witness under a trace whose unrecorded mark is false, is a malformed trace (§7.3.2), and strata MUST reject it with exit code 65.

A trace's claims fall into three classes:

• Derivable from verified objects in the store: the Trace node and every node reachable from it are checked against their content addresses on get (§7.5.1); strata walks forward nodes() edges and never the reverse index. From the nodes present, it checks the hole and witness halves of depth, the unrecorded mark against reachable Witness nodes, and the open holes list. The residue half of depth and the well-formedness of residue and source are checked when exhume re-buries residue.
• Bounded by missing objects, refused on corrupt ones: a store does not require a trace's entire graph to be present (§7.3.2). When a reachable node is absent, strata reports how many nodes are missing and states that its survey is a lower bound rather than an unqualified certificate. When a reachable node is present and fails verification on get, that is a corrupt object (§7.5.1) rather than an absent one, and strata MUST fail with exit code 65 instead of counting it as missing.
• Externally trusted: content addressing proves a Witness node is intact and names the call and answer cairns it was written with; it cannot prove the writer obtained answer from the world rather than inventing it. Checking the world's answer means re-running exhume against the world or comparing witnesses across independent stores.

"Why is this value at depth 5" has to be a command, not an investigation.

8.7 graft

nether graft <cairn> --replace <cairn> --with <cairn> [--json]

Answers a hole differently and re-buries only what changed, which §6.5 guarantees is sound. --replace names a hole the trace still has, and --with the value to answer it with.

A graft replaces a hole and nothing else. If --replace names an answer the trace was already given, graft MUST refuse and exit 1: that answer has been consumed, what it produced is in the trace's deposits rather than its residue, and burying the residue again cannot change them. To answer it differently, graft or exhume the trace that still has the hole.

graft MUST report how many nodes were reused and how many were recomputed. That ratio is the whole argument for content addressing, and a build tool that hides it is asking to be trusted rather than measured.

8.8 Exit codes