§ 01 · draft · depth 3 · edit the source

The strata

Every value in Nether C carries a depth: a natural number between 0 and 8 recording how far into the world its history reaches. Every expression has a depth. Every function's type includes the deepest stratum it may reach.

Depth is not a permission that is checked and forgotten. It is part of the type, it propagates through every operation, and it is recorded permanently in the trace.

1.1 The lattice

The nine strata form a total order, 0 ≤ 1 ≤ … ≤ 8. Depth composes by maximum: an expression built from parts is exactly as deep as its deepest part.

Depth	Name	Grants	Costs	Witness obligation
0	Pure	arithmetic, data, functions	nothing	none
1	Store	reading the ledger by cairn	nothing observable	the cairn read
2	Frozen Environment	declared variables, a pinned clock, the target triple	the value must be declared in advance	the declaration and the value
3	Read the Disk	reading files	the result depends on a filesystem	path, bytes read, and their cairn
4	Write the Disk	creating and modifying files	irreversibility outside the ledger	path and the cairn of what was written
5	Read the Network	fetching	the result depends on a remote party	request, response, and its cairn
6	Write the Network	sending	the world remembers what was said	request and the response, if any
7	Entropy	true randomness	replayability	the drawn value
8	Unrecorded	foreign code	provenance itself	nothing can be recorded

Strata 0 through 7 are recordable: everything the world answered can be written to the ledger and served back later, so a trace that reached them can be replayed exactly. Stratum 8 is not, and is treated separately in §1.7.

1.2 The monotonicity law

Law. No evaluation step lowers the depth of a value.

This is the one invariant the whole design rests on. An implementation MUST NOT provide any operation that produces a value of lower depth than its inputs, except the two escapes defined in §1.5 and §1.6, both of which carry a name or an opacity rather than the value itself.

There is no ascend.

1.3 Descent

nether c

Bytes@3 src = descend disk { read("kernel.nc") };

descend κ { … } is an expression. It acquires the capability named κ for the duration of the block, evaluates the block, and takes the value of the block's tail expression. The body is checked holding δ ∪ {s(κ)}, where δ is what the enclosing scope holds.

It acquires that capability and no other. The strata are ordered by how much of the world has been disturbed (§1.8), which is an order for comparing two histories and not one for implying a permission: net is deeper than disk! and does not carry it.

nether c

Answer<U0> wrote = descend net { write("kernel.nc", b"") };   // needs disk!

That descent supplies net, and the call needs disk!. At the top level of a file there is nobody to ask for it, so an implementation MUST reject this, naming the capability that grants the stratum the call reaches. The program that means it nests — descend net { descend disk! { … } } — and says both out loud.

Inside a function body the same expression is not an error: it is what the function asks of whoever calls it, and the signature comes out @4 (ABS). Either way the capability is named somewhere a reader can find it, which is the whole of why the names are fixed rather than open.

A descend whose tail expression is U0 may be used as a statement.

Descent is lexically scoped: the capability is not available outside the block, and neither are the block's local bindings. Only the tail value leaves, carrying its depth with it.
Descent is one-way within the block: no construct inside the block gives back a capability the block is holding.
Descents nest, and nesting accumulates. descend disk { descend net { … } } has a body holding both, and still nothing else.
A descend for a capability the enclosing scope already holds is legal and has no effect. An implementation SHOULD warn about it.

The capability names and their strata are fixed by this specification and listed in section 09. An implementation MUST NOT define additional capability names; a capability that is not in the prelude cannot be audited by a reader of this document, which defeats the purpose of naming them at all.

1.4 What the trace records

When an expression at depth d > 0 is evaluated, the implementation MUST write to the ledger, before the value is returned to the program:

the witness listed for that stratum in the table in §1.1;
the source span of the expression that reached it;
the depth itself.

The order matters. An answer that is returned before it is recorded is an answer that can be lost, and a ledger with a gap in it cannot support any of the guarantees in section 06.

1.5 Seal

nether c

Cairn id = seal src;    // src : Bytes@3, id : Cairn@0

seal e produces the cairn of e — the content address of its value. The result has depth 0 regardless of the depth of e.

This is sound because a cairn is a name, and a name is pure. Knowing that a file's contents hash to a1f0c93d tells you nothing about the file that you could not have computed yourself given the same bytes; it is a claim about the deep value, not the deep value.

It is worth being exact about what that sentence does and does not say, because seal is the place a reader is most likely to expect more of depth than depth offers.

Depth is a claim about where a value has been, and about nothing else. It says which strata a value's history reached and therefore what the trace owes a witness for. It is not a claim about what a deep value can be made to reveal, and Nether C has no rule that confines that.

seal is the shortest demonstration. The cairn of a depth-3 file is at depth 0, §9.2's hex turns it into a Str at depth 0, and §5.3 makes equality a comparison of cairns:

nether c

Bytes@3 src = must(descend disk { read("secret") });
Bool@0 is_the_one =
  (seal src == #4d9f7b2e0c81a35f6d0e92b7c4a1f80d35e6b92c7f0a4d81b3e5c9270af61d84);

That decides something about a depth-3 value at depth 0, holding nothing and writing no witness for the comparison. Against a low-entropy secret — a version string, a four-digit number, a file that is one of three — guessing settles it.

None of which is a hole in the rule above. Every step is a claim about the deep value rather than the deep value, the history is intact, and the trace still says the file was read. It is a hole in the rule a reader might have inferred instead, which is why the rule is written down here.

A program that must not reveal a deep value is not a program this type system can check. §90.3 says so beside the other things it is worse at.

seal on a shade (§1.6) is legal and names the shade. A shade carries the stratum it came out of, and §7.1 encodes that alongside what it holds, so seal shade e is not seal e. The cairn of what is inside is had by sealing it before shading it, which costs nothing and needs no capability.

1.6 Shade, and the Orpheus rule

nether c

Shade<Bytes> reply = descend net { shade must(get("https://example.invalid/index.json")) };

Cairn witness = seal reply;       // legal: Cairn@0
// ILLEGAL here — see below
I64   n       = len(look(reply));

shade e, where e : T@d, produces a value of type Shade<T> at depth 0. The shade is opaque: it MAY be stored, copied, passed, compared for equality, and sealed. It MUST NOT be destructured, pattern-matched, or otherwise observed.

look s, where s : Shade<T> originating at depth d, has type T@d, and is well-typed only where the capability that grants stratum d is held. That one: a shade out of stratum 3 opens under descend disk, and not under a descend net that happens to be deeper.

The Orpheus rule. You may carry a shade up out of any stratum. You may only look at it by going back down.

The check is local: it asks whether the shade's origin stratum is among the capabilities held at the point of the look. It does not propagate, it does not stain the enclosing scope, and it produces an error that names the origin, what is held, and the descend that would fix it.

error: cannot look at a shade from stratum 5 at depth 0
  --> stamp.nc:14:21
   |
14 | I64   n       = len(look(reply));
   |                     ^^^^^^^^^^^ this shade came from `get` at stratum 5
   |
   = the value is here, but you are not. Wrap the look in `descend net { … }`.

Where something is held and it is the wrong one, the error MUST say so rather than report a number: a shade from stratum 3 looked at under descend net is not a shallower scope, and an implementation that prints at depth 5 has told the reader their scope is deep enough.

What the rule buys, and what it does not

It is a rule about the program's text, and it is worth being exact about that, because a reader meets it among the capabilities and will take it for one.

What it buys is two things. [LOOK] concludes τ @ max(d, d′), so opening a shade does not launder it: the value comes out at the depth it went in, and everything built from it is that deep. And a descend naming the stratum stands at every point in the source where the value is observed, which is what a reader auditing a program actually reads.

What it does not buy is a capability at burial. Nothing about look reaches the world — the value is in hand already — so no grant gates it, and §6.1 says so in as many words. A writer who wants to open a shade writes the descend and burial evaluates it, whatever the invocation held.

So shade is what lets a deep value be held, passed and stored at depth 0 without its depth spreading to everything it touches, and look is what costs naming the stratum again to get it back. Neither is an authority, and §1.4's witness for the stratum was written when the value was first fetched — once, by whoever held the capability then.

This rule is settled. Two alternatives were considered and rejected — re-staining the entire enclosing scope, and tainting only the binding — and both are recorded in §90.2.

1.7 Stratum 8, the Unrecorded

Stratum 8 is foreign code: anything whose behaviour the implementation cannot observe well enough to record a witness for.

It is in the lattice because a language that cannot call C is a language nobody can adopt. It is at the bottom because it is the only stratum that breaks the language's central promise rather than merely deepening it: a trace that reached stratum 8 has a gap in it, and no amount of later care can fill that gap in.

An implementation MUST:

mark any trace that reached stratum 8, permanently and transitively, in the trace itself;
refuse to report such a trace as replayable, in every rite that reports replayability;
surface the mark in nether strata output without being asked.

A value derived from an unrecorded call is itself at depth 8. There is no sealing or shading out of stratum 8 that removes the mark — seal still yields a Cairn@0, but the trace remains marked, because what is unsound is not the name but the claim that the trace is complete.

This is settled: stratum 8 exists, and is quarantined loudly. The alternative — refusing foreign code entirely — is purer, and is recorded in §90.2 along with why a language that cannot call C proves nothing about whether its ideas were good.

1.8 Why write is deeper than read

Strata 4 and 6 sit below 3 and 5 because the ordering is how much of the world you have disturbed, not how much you have learned. A read can be replayed from the ledger with no trace left outside it; a write cannot be taken back, and a message sent cannot be unsent.

This makes the ordering slightly unusual: a program that only reads the network (5) is deeper than one that writes the disk (4), which is arguable. The specification takes the position that reaching outside the machine is a larger commitment than modifying the machine you are already on. An implementation MUST use the ordering in §1.1 regardless of its opinion, since depth comparisons must mean the same thing everywhere.