Refuse casting an optional at the compiler: the leaked-Optional construction wall

[gunbai-bot]

The wall found 30 live leaked-Optional casts across 11 files on its first whole-corpus run, and all 30 are eliminated with a match — none silenced, none exempted, no roster. Among them: an unset BMC_HOST was being dialled at a host whose name was the literal text Absent; shell.Env.Get(...).value as Secret minted a credential whose contents were the word Absent; and required.first() as String would have written required tach health is absent: Present { value: fan0 } into a converge receipt — the identical defect this wall was commissioned for, in a module nobody was looking at.

What this is

probed_at_word's declared next-rung trigger, built. A cast does not eliminate absence — it re-types the node and leaves the value alone — so reading as String over a NonEmptyStr? rendered the wrapper, and srv5/srv6 receipts carried probed_at=Present { value: 2026-08-20T21:11:38Z }. #8377 fixed the fourteen sites; test.claim.probed_at_word_witness_test recorded the honest rung (mitigatable — reverting any one of those sites left both witnesses green). This makes the reverted spelling not compile.

OptionalCastNotEliminated { source_type, target_type, span } is a typed located refusal fired from the ExprCast arm of inference (src/v1/04_infer.dag optional_cast_diags), beside the existing sole-constructor and where-refinement cast walls.

The two open questions in the brief

Cast judgment, or the wider "Optional in a text position"? The cast judgment — and wider than text within it: it refuses a cast off an optional source for every target, because the loss is the elimination that never happened, not the target's spelling. A cast whose target is itself optional is not this class and is left to validate_cast. The corpus settled it: of the 30 live sites the wall found, 6 have a non-text target (NonEmptyStr, Secret), so a text-only wall would have left a fifth of the measured population writable — including shell.Env.Get(...).value as Secret, which minted a credential whose contents were the word Absent. Interpolation and String-typed argument positions are not covered here; they are different sites with different judgments, and that bound is written on the probed_at_word carrier rather than left to be assumed away.

Which path? Source → .dag-acceptance. The refusal sits in inference, so a refused module never reaches emission or interpretation — but that is a consequence of where the wall sits, not a second measurement, and it is not claimed as one. The interpreter's Display for Value still renders Present { value: … } for optionals reaching text by a route the wall does not judge.

The corpus census — 30 live sites, not zero

The brief asked for the number plainly.

Named observation, because sibling lanes running corpus-wide censuses will otherwise each rediscover it: gunbc compile with no --entry cannot be used as a corpus census instrument. It refuses with WholeCorpusCompileBudgetBelowMeasuredDemand — both in a session container and on a BuildBuddy runner. That is a refusal, not a measurement: the two numbers it prints (a 7.1 GiB readable budget against 7.5 GiB of measured demand) are one sample under one host's pressure and should not be treated as stable. Locally, before that wall existed, the same run was SIGKILLed in reconcile — which is exactly why the refusal exists, since a count grepped from a killed process is a memorial rather than a census. What does work: CI's own required floor resolves the whole tree (modules_resolved=3813) and prints every typed diagnostic with path:line:col. That is where this census came from, on the first push:

file	sites
dag/extdeps/filesystem/linux.dag	10
dag/gunbc/bmc_fan_converge.dag	7
dag/test/claim/spark_serving_runtime_install_witness_test.dag	2
dag/test/claim/secret_rotation_witness_test.dag	2
dag/test/claim/commit_check_demand_witness_test.dag	2
dag/extdeps/bmc/openbmc_fan_control.dag	2
dag/gunbc/tools/bmc_first_contact.dag	1
dag/gunbc/systemctl_list_units.dag	1
dag/gunbc/spark/serving_observe.dag	1
dag/gunbc/roadmap_dispatch_actuator.dag	1
dag/extdeps/shell/credentials.dag	1

Every one is eliminated with a match in the second commit, not silenced. Where the caller already refuses the absent case one line above, the arm is a loud word (probed_at_word's precedent) so a failure can never read as data; where a refusal already exists downstream — an empty required field, a failing parse_int, an existing refusal-detail message — absence routes into it rather than minting a second refusal beside it. Worth naming individually: an unset BMC_HOST was being dialled as the literal host Absent; required.first() as String would have written required tach health is absent: Present { value: fan0 } into a converge receipt — the identical defect to the one this wall was commissioned for, in a module nobody was looking at.

The credential site carries its absence, it does not paper over it. env_credential answers token: Secret?, and github_token() answers a GitHubAuthTokenRead coproduct — so GitHubAuthToken.token keeps its non-optional Secret and a value of that type still means a token was actually read. An earlier revision of this branch substituted the empty secret and deferred the surface change on the reasoning that "every consumer must reject it"; that is an unverified universal and the deferral was reversed on a measurement instead: env_credential has exactly one consumer (github_token) and that consumer has zero callers — the three grep hits are prose. So the empty secret could not reach anything today, which is the checkable version of the claim, and the migration cost is at its global minimum now rather than after the first caller inherits a silent empty credential.

Rung

Structurally guaranteed on the source → .dag-acceptance path — the invalid state is refused at acceptance by derived structure, not detected by an enrolled mechanism. Not claimed for any other path: emission and interpretation are untouched by consequence of where the arm sits, and that consequence is not a second measurement.

The v1 seed change, classified rather than assumed

First, what the seed diff actually is. The hand-authored change is the .dag authority, src/v1/04_infer.dag. The 49 lines in src/v1/stage0/src/v1_compiler_infer.rs are the emitter's output — installed from target/stage0-regen-candidate, verified by required-regen: first_generation_equal=true. No seed Rust was grown by hand: that file changed because the authority changed and the emitter re-derived it, which is the self-host mechanism working rather than someone editing a frozen file.

The authority is still in the seed, so the standing carrier gunbc.v1_maintenance_standing v1_seed_standing (SemanticsFrozen { maintenance: MaintenanceActive }) applies and the classification is owed.

Claimed: SupportsV2SelfHostProgram { instance: DefectRepairDiagnosticsMayMove }.

Why that class and not "this is a safety improvement" — which would be growth for its own sake, exactly what the freeze refuses. The seed is not merely missing a check here. Its ExprCast arm affirmatively stamps inferred: Resolved { node: target_type } on the cast node, so it asserts that the value has the target type when it does not, and the interpreter then renders Present { value: … } into a field the type system says is a String. That is a specific incorrect behavior the seed exhibits today, evidenced the way v1_maintenance_defect_repair_note demands: 30 live sites and two srv5/srv6 production receipts. The repair moves diagnostics, which is what the class name anticipates. On the governing 2026-08-20 purpose test it also passes on its own terms — v1 is the compiler that compiles the v2 corpus, and every one of the 30 sites is in that corpus, two of them in v2's own witness tests.

The counter-reading, stated because I would rather it be argued than discovered: v1_maintenance_defect_repair_note draws the line as "the seed FAILING TO DO something it never did is SeedFeatureCompletion, refused", and v1 never performed an optional-cast judgment. Read that way this is a refused class, and refusals dominate every admission. My argument against that reading is the paragraph above — the defect is a wrong assertion the seed makes, not an absent one it omits — and I think it is the better reading, but it is a reading. If the standing's owner or a reviewer lands on SeedFeatureCompletion, refusal dominates and the seed half of this PR needs re-deciding rather than defending; I am not treating my own classification as the verdict (v1_maintenance_rung_note puts this carrier at mitigatable precisely because the classification is authored, not derived).

Evidence

dag/test/claim/optional_cast_wall_witness_test.dag, run on a post-regen binary (claim_batch, all four PASS):

• RED arm — w_reverted_probed_at_call_site_is_refused: the reverted production call site (clock_now_probed_at() as String) is refused.
• GREEN — w_sanctioned_probed_at_call_site_is_accepted: probed_at_word(reading: now) still compiles.
• GREEN — w_required_source_cast_is_accepted: a cast off a required source of the same type still compiles. This is what makes the RED discriminating rather than a wall that refuses every cast.
• RED arm — w_optional_cast_to_a_non_text_target_is_refused: the non-text half of the class.

All four stay enrolled (§4b(4)); the two probed_at_word witnesses stay enrolled as permanent controls on the rendering authority itself. Its rung note is rewritten to say what changed and what is still writable.

Test plan

• claim_batch --entry dag/test/claim/optional_cast_wall_witness_test.dag --functions … → 4/4 PASS.
• claim_executor --required-regen → mirror regenerated from the .dag authority (the hand-written seed patch was replaced by the emitted bytes); cargo fmt --all --check clean.
• Per-entry compiles of the fixed modules → 0 refusals, 0 errors.
• Whole-corpus verdict: CI green on 68e3ffa — parse OK 50 file(s), regen first_generation_equal=true, floor modules_resolved=3813 planned=10253 executed=10253 terminal=10253 passed=9946 failed=0. Zero remaining leaked-Optional casts in the tree.