koruc assumes: What Your Program Rests On

Lean lets you ask #print axioms: point at a theorem, get the transitive set of unproven assumptions its proof rests on. Koru can answer a better version of that question, because the language already carries claimed facts — and it can carry the absence of a claim too.

koruc main.k assumes <name> walks the call graph of a declaration and reports everything its flows can reach, each graded by the claim it asserts about itself. The row you have to sit up for is not the graded one. It is the one without a grade.

Facts and claims are different objects

Before the ladder, the engine under it — because this is where Lean points the wrong way and Koru turns it around.

Koru’s compiler decides a fixed family of small mechanical questions. Did the obligation discharge. Does the borrow outlive its owner. Does a proc stay pure across everything it can reach. Each is closed: the answer holds not just inside the declaration that was checked, but across every caller. That closure is what makes a borrow safe to pass through three frames, and it is what the purity checker does for a whole program when it marks a property pure only if everything transitively reachable is pure — propagating to a fixed point over the call graph, not trusting a single body.

That is Koru’s meaning of “locally consistent, and it extrapolates.” Not a theorem about what the program does. A small decidable property, verified cheaply, that provably holds at every reachable call because the property is closed — the call cannot break it. Lean, to keep up, needs a type theory to embed the program under, and a proof you write for each proposition. Koru has no type theory in that sense — its shapes and resource states are not propositions — and never asked for one. What it has instead is its own better fit: a handful of closed invariants decided once and guaranteed across the whole reachable closure, at no marginal cost.

A claim is something else again — an author’s assertion about a declaration, written in the vertical annotation block where the definition already is, carrying a stamp that says how well the claim is currently known:

[
  - proven contract-honest
    Declared by the same shape checker that discharges the obligation.
]tor leaf { v: i64 } -> i64

tor mid { n: i64 }
mid = leaf(v: 42)

tor root { n: i64 }
root = mid(n: 7)

One stamp, one tor: leaf claims proven — a closed invariant discharged it. The chain above it — root, mid — claims nothing at all. That asymmetry is the point: the stamps are a ladder, not a taxonomy — proven (a closed invariant discharged it) → measured (something ran) → inferred (some engine declared it) → aspirational (nothing yet, the honest sorry) — and unclaimed is not a rung on that ladder, it is the absence of a rung, which is the only thing more interesting than a low rung. The registry guaranteeing every claim a unique key ships with the vocabulary — a claim that cannot be told apart from another can never be judged by any engine.

What a stamp does not say

The ladder answers how well a claim is known. It says nothing — on purpose, so far — about how it is known. And the two questions are not the same.

proven names a rung, not a mechanism. It was discharged by a closed invariant, but the export cannot tell you which invariant the checker used to get there, which compiler revision ran the walk, or against which revision the walk was computed. Two proven stamps from two different engines are indistinguishable in the export — the exact failure the registry exists to prevent for keys, now present for bases. That is the provenance the audit does not yet carry: not the level, but the basis.

Most of that basis is recoverable later — re-run the checker on the same source and you get the same walk. But one piece of it cannot be recovered after the fact, by any downstream engine, Lean included: the author’s intent. Whether “comments are written in English” is a permanent rule or a debt the author means to discharge is undecidable by re-reading the rule at any later time. It must be stated the moment it is written or it is lost forever.

That is what the other half of this design is for. A sibling surface, std/invariants, gives the declared rungs — inferred and aspirational — a home, precisely because they are the rungs where the capturable-only-at-writing bit lives. Two tors, not one with a field: inferred (permanent by nature, growth is good) and aspirational (debt by construction, growth is a smell). Nobody can tell them apart later, so the author chooses the word at the moment of writing, and the distinction is stored in the only medium that still has it.

The two surfaces are one gradient, not two worlds. assumes walks the subjected closure and reports what each claim rests on. invariants walks the subject-less census and stores what only the author could know. They are the same ladder, projected onto two attachments — the walk is the projection of reachable claims; the disposition is the record of intent. Neither names a verification mechanism, because the mechanism is the language’s own closed invariants beneath them. A proof kernel would add theorems; what the design actually needed was a place to record, at the moment of writing, the one fact no theorem can ever re-derive.

The walk

Give assumes a name and it does the one cheap, mechanical thing: walks the flows — their continuations, their branches, their invocations — collecting every declaration reachable, transitively. Then it grades each one.

$ koru main assumes root

📋 assumes — input:root
  input:root  [unclaimed]
  ↓ effective: unclaimed
  input:mid  [unclaimed]
  ↓ effective: unclaimed
  input:leaf  [proven] contract-honest
  ↓ effective: proven

The root flow calls mid. mid calls leaf. And leaf is the only thing in the chain that says anything about itself — one claim, proven, with its stamp. The audit reports the reachable whole, graded each, and adds a line the stamps alone would hide: the effective grade, the weakest claim anywhere beneath a declaration. root is unclaimed, so its effective is unclaimed; leaf is proven, so its effective is proven. The middleman mid is the finding — reachable, calling a proven leaf, and itself asserting nothing.

This is the actual output over the code above (run through the regression test’s own harness). The machine-readable form is the same walk emitting a catalog, ready for a consumer:

{"subject":"input:root","reaches":[{"key":"input:root","stamp":"unclaimed","effective":"unclaimed"},{"key":"input:mid","stamp":"unclaimed","effective":"unclaimed"},{"key":"input:leaf","stamp":"proven","effective":"proven"}]}

The finding is the silence

Everything in that chain except leaf came back unclaimed — root, mid, even the fact that walked through to get to the claimed one. Look at the output again: the raised hands are the ones with no stamp.

That is the whole point of the command, and it is closer to an audit than a census. A measured flow whose callees are all unclaimed is telling you its measurement did not cover them. A proven tor that calls five things that never asserted anything is telling you its proof had premises nobody wrote down. assumes does not judge claims; what it refuses to do is hide the parts of the program that have none. Silence becomes data: what a claim rests on, including every time a claim rests on nothing at all.

The alternative would have been worse in a characteristic way: list only the claimed callees, and a chain that is mostly unclaimed looks identical to a chain that is fully claimed. The audit exists to make that distinction visible. And the same refusal applies at the boundary of the closed invariants themselves — a proven flow reaching an impure or unclaimed callee does not pretend its closure is proven; the closed invariant is the engine, and the walk makes the engine’s own debt visible too.

What it is not

assumes is not a verifier, and it is not a proof kernel. It does not judge whether a claim is true; its whole job is adjacent — record reach, and reach is a fact about the program, not a belief about it. What gates — a consumer that wants a tree green only when everything reachable is at least measured, say — reads the same export. The command emits; the gate deliberates. A name that could not gate would be decoration; a name that always gated would have made the language decide — and it never should. The verdict is the gate’s; the audit’s only job is to make the absence visible enough to decide from.

The regression pins that hold all of this are small and deliberate:

The companion behavior — the missing subject error, the ambiguity refusal when a bare name could mean several declarations, and the bad-format wall — arrived in the same commit, but the regression tests are the star: they are the programs that, if the silent-drop bug returned, would show it red on the board.

The going answer

assumes is the compiler’s own #print axioms-moment, and it has the quality a design only earns on real soil: the concept — “point at a declaration, get the transitive set of what its correctness rests on” — survived contact with the AST, and what surprised me was the shape of the unclaimed. The interesting new fact is not how claims walk; it is that the walk gives claims a demand to be born. The easiest way to get a green assumes report is to write claims in direct proportion to reachability — and that is a nudge a compiler can give that a reviewer never can.

It is also, in the end, the honest answer to the proof-kernel temptation. Lean offers a root of trust, but only at the price of a type theory Koru will not pay, and it cannot say a single thing about the one fact that matters — whether the author held a rule as permanent or owed it as debt, said at the moment it became a fact. Koru’s audit keeps the only trusts it can honestly honor: the closed invariants checked and guaranteed across the closure, the absence never hidden, and the intent recorded while it is still legible. That is what the program rests on; everything else is the language deciding.