Rejections and Lifecycles That Explain Themselves: Derivation-Carrying Diagnostics, Runtime Why and Navigable Refusals

Pitch

When a compiler's global guarantees give every fact a unique supplier and force every cascade to terminate, "why did this happen?" can be derived instead of guessed, at compile time (rejections), at run time (lifecycle transitions) and at the policy layer (refusals), and the one place where explaining would leak is handled by making all refusals look the same.

Abstract

Diagnostics and traces usually report what happened, and leave the cause to the reader or to a monitoring tool that infers it from timing. We describe three explanation mechanisms in revl, a language whose checker enforces unique provision per key and realm (G2) and an acyclic provider graph (G3). First, rejections that come from a whole-program search (an emission fixed point, a dependency cycle, a provider conflict) carry the derivation of the verdict as structured data, and revl explain maps any diagnostic code to its guarantee and fix. Second, a run logs every lifecycle transition with its cause; because a lost provision has exactly one supplier and a cascade terminates, the cause is read from the checked graph rather than inferred. The static prediction of a withdrawal cascade (set and LIFO order) is then diffed against the cascade the runtime actually produced, turning each logged withdrawal into a conformance check, with three named defect kinds. Third, every policy refusal carries the nearest allowed space computed from the tables that refused it, with a proof marker that is sound only on facts immutable at the refusal site. An adversarial review of the first design found that these maps let an untrusted author reconstruct the operator's policy; the fix collapses the untrusted view to one non-discriminating verdict, and a matrix test asserts byte-identity across families. On main today: three mechanisms, 27 runtime-why tests, 28 derivation-trace tests, and 15 plus 32 navigable-refusal tests. We report no user or agent study; that is stated as the main gap.

Problem and claim

Compilers throw away their search. G4 (an emission reaches a method declared plain), G3 (a cycle) and G2 (two providers) are verdicts of whole-composition searches, and the old diagnostic printed the conclusion only. The docs say so directly: the author "had to re-run the search by hand" (docs/why-traces.md, opening paragraphs before the example). At run time the problem is the same one level down: the streamed lifecycle trace carries events with no causes (docs/why-runtime.md:12-17), and an APM can only reconstruct the because from timing. At the policy layer, denials answered unevenly: some named the fix, several named only the violated rule (survey table at docs/design/274-navigable-refusals.md:38-66).

The claim is narrower than "explainable systems are good". It is that three properties of the language make the explanations derived rather than inferred, and that a single constraint (do not leak policy through the explanation) shapes the design of the third mechanism. Provision uniqueness (G2) and acyclicity (G3) make the runtime cause of a withdrawal unique and the cascade finite (docs/why-runtime.md:18-29). Because the cause is a graph fact and the transition is an observation, the two are independent and can be compared; a disagreement is always a defect in one of them (docs/why-runtime.md:158-197).

The honest scope: the oracle checks the withdrawal cascade of one composition on one run, not the whole runtime, and the navigable-refusal maps are verified by structural tests, not by an agent benchmark (the design's own "bench delta" test is not on main).

Contributions

1. Derivation-carrying rejections: G4, G3 and G2 diagnostics carry a WhyTrace of TraceSteps as data (chain or set shape, best-effort locations, shortest deterministic witness), rendered for humans, emitted in --json-diagnostics, and handed over MCP; collecting the evidence is observationally invisible to the verdict. revl explain <code> gives the guarantee and fix per code.
2. Runtime why: a v2 JSONL trace where every settled load, withdraw and emit transition carries a cause (boot, requirements, trigger, provider-withdrawn, liveness-expired, transport-fault), a cause-chain walk (revl why), and an additive schema (v1 events still parse).
3. The withdrawal oracle: the static withdraw prediction (exact set, LIFO order) diffed against the logged cascade, with defects missing-teardown, unexpected-teardown, order-mismatch, exposed as revl run --withdraw and revl why --check.
4. Navigable refusals: a navigate entry beside every wired policy refusal (family, blocked flag, alternatives each tagged by who enacts it, proof marker), covering taint sinks, boundary policy and seven further families, with clears-this-gate forbidden on runtime-mutable operands.
5. The untrusted-author leak analysis and its fix: a single non-discriminating verdict, redaction by fact class, and a byte-identity matrix test across families, including redacted-versus-genuinely-blocked.
6. Structured refusals with a next call (next: {tool, arguments, ready}) and a usage error that is distinct from a composition verdict, in the MCP surface.

Related work

Evidence on main

Numbers that exist

• Test counts, from grep -c '^def test' of test functions: tests/test_why_traces.py 28, tests/test_why_runtime.py 27, tests/test_274_navigable_refusals.py 15, tests/test_274_navigable_slice2.py 32. These count tests, not results of an experiment, and the tests were not run for this count.
• Schema: SCHEMA_VERSION = 2 (src/revl/why_runtime.py:43), 3 event kinds (docs/why-runtime.md:55). Cause kinds: the code emits six (boot, trigger, requirements, provider-withdrawn, liveness-expired, transport-fault; src/revl/why_runtime.py:148-241), while docs/why-runtime.md:55 says four. This paper follows the code.
• 3 searches covered by derivation traces (G4, G3, G2); 14 refusal families in the closed enum (src/revl/navigate.py:37-41; the roadmap says all are wired).
• Behavioural measurements (agent step counts, human debugging time, oracle detection rate on seeded runtime bugs): none yet.

Paper outline

1. Introduction: three places a system throws away its reason, and the uniqueness that lets us keep it.
2. Background: G2/G3/G4 in one page; what "supplier" and "cascade" mean.
3. Derivation-carrying rejections: WhyTrace data model, shortest deterministic witness, the "never changes a verdict" invariant.
4. Runtime why: causes as graph facts, schema v2 and additive evolution, cause-chain walk.
5. The withdrawal oracle: prediction versus observation, independence argument, defect kinds, and what it does not promise.
6. Navigable refusals: nearest allowed space, enactor tags, the immutable-operand rule for the proof marker.
7. The leak: the adversarial review finding, the collapse, the indistinguishability test; the documented exception.
8. Evaluation: tests as spec, oracle mutation study, agent benchmark.
9. Related work and limits.

Threats to validity and limits

• The docs' own limits: the oracle "checks the withdrawal cascade, not the whole run"; "A conforming run is not a proof of the runtime"; a "cascade never triggered is never checked"; --withdraw is a one-shot, not a live command (docs/why-runtime.md:199-215).
• Independence of prediction and observation is the whole value (docs/why-runtime.md:210-215). The cause label is still read from the provider graph, so the oracle cannot catch a wrong graph, only a runtime that disagrees with it.
• Tracing needs the cordis py runtime; the trace vocabulary and oracle are pure but only the py tier writes the trace (docs/why-runtime.md:216-221).
• Derivation traces explain only searches; a direct verdict has no trace (docs/why-traces.md:170-184). Only the first culprit is traced, so the trace is one worked example, not all of them.
• The leak result is a matrix test over a finite set of families and operations, not a proof, and the design review that found it was internal. Byte-identity over a finite matrix is evidence, not proof. The admit-profile family is an acknowledged exception: it enumerates the author's own granted set (docs/roadmap-archive/12-post-v2-0-horizon-strategy-review.md:517).
• The adversarial review itself is not in the tree; the only trace on main is the CRITICAL comment in src/revl/navigate.py and the roadmap text.
• No evidence yet that agents or people benefit; "refusal is a map, not a wall" is a design principle on main, not a measured effect.
• The design doc header lags (slice 1 wording) while the roadmap text says all families landed. This paper follows the roadmap plus the slice-2 tests.

Fact-check

Claims in this draft were checked against revl main at commit 45bec431f: 19 checked, 6 corrected.

Cite this draft

@misc{revlp54,
  author       = {Thomas Moussajee},
  title        = {Rejections and Lifecycles That Explain Themselves: Derivation-Carrying Diagnostics, Runtime Why and Navigable Refusals},
  year         = {2026},
  howpublished = {\url{https://inso1337.github.io/revl/research/P54.html}},
  note         = {Research draft, not peer reviewed. Written against revl commit 45bec431f. Licensed CC BY 4.0.}
}

Text licensed CC BY 4.0, author Thomas Moussajee.