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

Koru screams proven facts at the type level: obligations discharge, borrows do not outlive their owners, a phantom erases at codegen exactly the way Lean erases Prop. Those are checked by the compiler, always, everywhere.

A claim is something else. It is 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 — the shape checker discharged it. The chain above it — root, mid — claims nothing at all. That asymmetry is the point, and it is worth naming before the walk: the stamps are a ladder, not a taxonomy — proven (the type system discharged it) → measured (something ran) → inferred (something 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.

The walk

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

$ koru main.k 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.

What it is not

assumes is not a verifier. 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.

The regression pin that holds all of this is 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 test is the star: it is the program 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.