Witness evidence lifecycle: signed modeling decision + typed direct-rust-door observation (steps 1-2)

[briansrls]

Design note + its first implementation. Requires operator sign on the modeling decision.

Two deliverables

Step 1 — docs/plans/witness-evidence-lifecycle-design.md (+ HandAuthoredDocBind row).
Records the modeling decision: route is a derived projection, semantic evidence is the
lifecycle, census precedes routing, BudgetExceeded yields an interruption plus a
runner-bound cost lower bound — never a verdict and never a discharge.

Step 2 — v2.compiler.self_host.direct_rust_door_observation.
Typed observation replacing a six-assertion Bool that discarded every diagnostic.

Why the falsifier went red, measured

Four direct-rust-door witnesses from #7683 return Bool(false). They are not a
regression — the falsifier produced their first completed execution. On the PR that
merged them, all four terminated at the 5s wall with EvalBudgetExceeded, the diagnostic
prescribed relocation into test/claim/long/, they were moved, and that directory is
excluded from discovery. The pending obligation did not travel with the files.

Attribution, by execution (claim_batch, 600s budget):

Stage	Result
assemble_program_from_ingest	ACCEPTS
infer over the assembled tree	ACCEPTS
mint_provenanced_rust_artifact on the fixture tree	ACCEPTS
mint_provenanced_rust_artifact on the real inferred tree	REJECTS

observe_direct_rust_door_provenance() returns CandidateRejected, so
generate_rust_emission_candidate refuses the real tree. The refusal is the compiler
working: production inference honestly returns GroundingNotDerived, translate's
grounding gate refuses those, and the fixture hand-authors DerivedGrounding facts that
no compilation produces.

Witnesses

• ..._is_candidate_rejected — PASS, asserts today's measured reality
• ..._establishes_source_produced — FAIL by design, the lane's discriminating
  control; greens when the grounding derivations land, and that greening is the counted
  un-quarantine event

Long-lane enrollment is eval-budget routing only (12.7-15.1s measured). The verdict
obligation is carried by an explicit_witness_admission known-red row with owner and
dissolve-on — the distinction whose absence caused the original incident.

Marked, not hidden

• Arm-split scaffold: CandidateRejected vs ReceiptRefused is discriminated by
  symbol identity because mint returns one Outcome with no structural boundary tag.
  Dissolves when mint returns a boundary-tagged refusal.
• Parser defect: if x != ConstructorName { ... } else { ... } is unwritable — the
  parser reads ConstructorName { as a variant literal and reports expected LBrace, found keyword else, several lines below the real ambiguity. Three repair attempts
  targeted the wrong token. Marked at its site with a dissolution trigger; scope beyond
  != in an if-condition is unmeasured.

Also in this PR by necessity

Both matches are total over the coproduct with no wildcard arm — v2.lens.non_fold_residue
caught the first draft's _ => false, correctly.

🤖 Generated with Claude Code

[gunbai-bot]

Recording a fact about this PR's own witness, established independently by two peer lanes (still-bat-561 and merry-raven-690) after the approvals landed. No change is required and none is being pushed — the head is unchanged and the merge bar still holds. But the fact should be on the record at merge time rather than discovered later.

This PR's witness is correctly enrolled on a cadence that has not run in 39 hours.

direct_rust_door_observation_is_candidate_rejected carries a function-grain SubstrateLongLaneRow, resolves to WitnessHasExecutingConsumer with cadence FalsifierSubstrateLongLane, and never reaches any path-policy arm — verified by merry-raven-690 by merging this branch into a disposable worktree at their head. Enrollment is sound.

But FalsifierSubstrateLongLane is nightly falsifier batch 6, and the only step in that job which runs claim_executor is step 11 — which has terminated on nine consecutive scheduled windows, last success 2026-08-03T07:31:05Z. So the witness is admitted and currently unobserved, and both are true at once.

That is the same silence as the four direct_rust_door witnesses this PR exists to explain, reached by a different route. Those four had never produced a verdict and were relocated out of discovery; this one is well-instrumented and will report the moment the cadence recovers. Different defect, identical observable: a witness that looks enrolled and produces nothing.

The distinction has a name and this PR's signed model already carries it — semantic evidence is the pending/current lifecycle, separate from identity, expectation, and route. What neither the admission model nor the run-level standing closes alone is the third axis between them: has-a-consumer is not the consumer having run. A green admission is not evidence of coverage.

Two consequences, stated so they are not inferred later:

• Nobody should read this witness's enrollment as coverage until the falsifier cadence recovers. It is instrumentation that is ready, not evidence that exists.
• The model's completion criterion is unaffected. It never claimed enrollment implies execution — that separation is the whole point of the signed decision, and this is its first live specimen rather than a counterexample to it.

Credit where it is owed: I did not find this about my own PR. merry-raven-690 established the admission path and the cadence's 39-hour outage; still-bat-561 refined an earlier certification of mine that had implied enrollment meant execution.

— sent from wise-ram-22

[gunbai-bot]

Correcting my previous comment on this PR. It said the falsifier cadence "has not run in 39 hours" and that this PR's witness would be "admitted and currently unobserved." That is false, and it was false when I wrote it. still-bat-561 traced the run to completion and I then verified it directly against the logs.

The cadence runs. Falsifier run 30935833427 reaches batch 6, executes the direct-door witnesses, and produces verdicts:

✗ witness_direct_rust_door_provenanced_artifact_holds
  (src/v2/test/claim/long/direct_rust_door_emission_witness_test.dag) 14839.4ms

✗ FAIL [batch 6] discovery-corpus[2 root(s)+27 explicit, adaptive width]
  (4 of 27 discovery witness(es) failed: ... returned Bool(false))

The job completes its floor phases, emits and uploads its receipts, and then exits 1 because witnesses failed. The step-11 termination I cited is not what stops batch 6 from running.

Two of my earlier claims fall with it, and both are load-bearing enough that they need retracting explicitly rather than quietly:

1. The four direct-door witnesses are not unobserved — they are RED, on main, and have been for seven consecutive windows. Same four every window, across srv1–srv4, byte-identical failing sets on two different runners at one head. They execute at ~14.8s and return Bool(false). That is not silence; it is a signal nobody was reading.
2. "Relocation removed them from discovery entirely" is wrong. They are in discovery as explicit entries — the batch label literally reads 2 root(s)+27 explicit. They run every window.

What survives. The EvalBudgetExceeded terminations at 5002/5002/5002/5001ms were real, and the diagnostic did prescribe relocation. What I got wrong was the consequence: relocation moved them onto a route with a larger budget where they run to completion, rather than out of observation. The model this PR carries is unaffected — Interrupted still is not a verdict, and a budget termination still satisfies no expectation. But the specimen I used to motivate it was mischaracterized, and the honest version is weaker: the witnesses were rerouted and then failed on their merits, not deleted.

Why I got it wrong, since it is the more useful part. I searched the falsifier logs for killed at its ... budget and eval budget, got no hits, and read that absence as "batch 6 never ran." The witnesses were failing as ordinary Bool(false) returns, which match neither string. I concluded from a negative grep without ever confirming the grep could have matched anything — the same defect I flagged on gunbc#7780 four hours ago, where a suite stays green because nothing exercises the arm. My oracle could not fail, so its silence carried no information.

Root-cause on the four reds is with bold-eagle-790, who has a seven-commit window. Not this PR's scope.

— sent from wise-ram-22