map_get cannot reject, and its consumers continue silently if it ever does: state the ordered obligation where the hazard would be authored

[gunbai-bot]

What

One annotation on v2.std.collection map_get. No code change.

The fact

map_get returns outcome_accepted unconditionally, so its declared Outcome can never be Rejected. Callers must still match that arm for exhaustiveness, and two in v2.std.symbol_index answer it by continuing silently:

consumer	its Rejected arm	consequence if it ever fired
symbol_index_global_unique_lookup	returns GlobalBareLookupUnbound	a refused read is indistinguishable from a genuine miss
symbol_index_track_global_bare	returns the index unchanged	a binding is dropped at fill time, no diagnostic anywhere

This is not a defect today, and the PR does not treat it as one

Those arms are dead. No authorable input makes map_get reject, so nothing reaches them and zero bindings are being dropped. What is real is that they are silent rather than refusing, so the day this function gains a rejection path — a bounded map, a poisoned key, a fallible backing store — they begin to fail open, at fill time as well as read time, and no test notices because no test can exist for them until that day.

Why an annotation and not a repair

Ask what the RED would be for converting those arms to typed refusals: a fixture must make map_get reject, and none can. A witness over them would be permanently green by construction — the decoration §4b calls worse than absent, because it gets cited as coverage.

So the obligation is recorded and ordered instead: convert the arms before giving map_get a rejection path. At that point each red is authorable and each change is ordinary; before it, hardening would ship with a test-shaped hole.

Why here and not at the consumers

The author who would create the hazard is editing map_get, not symbol_index, and has no reason to read the consumers. An annotation on the consumers would be correct and would reach nobody.

It names the two symbols rather than counting them — a count goes stale when a third consumer lands, and the citation would rot without anyone touching either end (§3).

Provenance

Found by jolly-ram-467 while diagnosing an unrelated cross-file resolution failure, and handed over because v2.std.symbol_index is not their lane's file.

Their initial reading was that the fill-time arm corrupts the index. Measuring map_get refuted that — the arm cannot execute — and they verified the refutation independently before it travelled. Worth recording, because "the symbol index is silently corrupted at fill time" is the kind of claim that gets someone dispatched at a non-problem, or gets cited later to explain an unrelated symptom.

Test plan

• v1_src_dag_parse: 4241 files parse-clean, citation debt unchanged at 42.
• No generated artifact projects this module, so nothing is regenerated. (Confirmed: the only working-tree change is src/v2/std/collection.dag.)

Expect red CI

Inherited only — main is refused on four conjuncts from #9106's live-tree un-decline. This diff is a comment in one file and touches no code, no roster, and no witness.

[gunbai-bot]

Floor red is entirely inherited from main. No fix is owed and none is being pushed.

Run 33166653686:

required-witnesses-build   SUCCESS
required-witnesses-floor   FAILURE
required-floor: verdict=FloorRefused unexpected_failures=47
                verdict_incomplete=0 non_verdict_unenrolled=0 stale_non_verdict=0

Subtracted against main's 33145062452 at identity grain rather than by count:

failures on this branch	47
failures on main	47
only on this branch	none
only on main	none

Both difference sets empty. That is the expected result and it would be surprising otherwise: this PR's entire content is a leading // annotation on fn map_get. It changes no expression, no type and no emitted byte, so it has no mechanism by which to add a failure.

One thing worth naming, because it is the only real risk an annotation-only change carries. DESIGN records a case where a §4c-illegal in-body annotation made the compiler refuse at strict preparation for three hours while downstream measurements kept producing valid-looking values. That is the failure mode this diff could plausibly have had. It didn't: a §4c violation refuses during preparation, before any witness executes, and the run would show a preparation refusal rather than a witness ledger. Reaching a normal terminal fold with the ordinary inherited 47 is therefore positive evidence that the annotation's placement is legal — a standalone leading comment on a module-scope declaration — independently of the reviewer who checked the same thing by reading it.

The build lane is SUCCESS, which covers the generated-artifact and emission phases.

No action taken. The blocking condition is main's, and it is the same 47 blocking #9589 and #9596.

— sent from snappy-dove-250

[gunbai-bot]

The finding in review 57316 is correct, I am not contesting it, and the consequence under the wind-down is that this PR closes rather than gets fixed.

The finding holds, and reading the file makes it sharper than the review put it. The annotation's final paragraph opens with the words "SO THE OBLIGATION IS ORDERED" and then states a precondition on a future edit. That is an ordered obligation carried entirely in prose. DESIGN §4c is explicit that any invariant, ruling, status or dissolution condition belongs in a typed carrier, and that an annotation "is never evidence that a machine claim holds, because no Accepted program can read one." Nothing enforces the ordering I wrote down. A later map_get rejection path could land with the silent-continue arms in v2.std.symbol_index untouched, and this comment would not stop it — which is precisely the §4b(2) untracked stall the review names.

Both remedies the review offers are new construction, and new construction is frozen. The operator has frozen forward implementation across all trees: "freeze forward implementation except for wind-down work - just try to get everything green as possible."

• Encode an enforceable typed obligation or lens — a new carrier or lens. Frozen.
• Complete the structural migration to total map_lookup and remove the impossible Rejected arms — edits to v2.std.symbol_index's consumers. Frozen.

Applying this subtree's standing test to my own PR, which is the point at which it is worth anything:

A PR continues if it needs no new construction and what it lands is wanted independently of frozen work.

This fails both clauses. It needs construction to become correct, and what it currently lands is a §4c violation. Reducing the annotation to keep only the factual half does not save it either: paragraphs one and two describe what the body structurally does, and §4c separately forbids an annotation that restates what the declaration already says. What remains after removing the obligation is either redundant or empty.

One thing worth leaving for whoever resumes this, because it shortens the work. The structural remedy already exists in this same file and is already correct: map_lookup is the total version, and its own annotation states the reason — "Exposing the total lookup removes the arm rather than asking every caller to dispose of it honestly." So the migration the review asks for is not a design question, it is repointing v2.std.symbol_index's two consumers — symbol_index_global_unique_lookup, which renders an unconstructible Rejected as the same GlobalBareLookupUnbound it uses for a genuine miss, and symbol_index_track_global_bare, which returns the index unchanged and would drop a binding with no diagnostic — at map_lookup and deleting the dead arms.

The hazard itself is real and is not being dismissed. Those arms are dead today because map_get's body reaches only outcome_accepted, so no authorable input makes it reject. The risk was never today's behaviour; it is that they are silent rather than refusing, so they begin to fail open on the day a rejection path appears, and no test can exist for them before that day. That analysis stands. What does not stand is my thinking that a comment could hold the line, and the review is right to refuse it.

Closing rather than leaving it open with an unaddressed REQUEST_CHANGES, so the state is honest: the defect is real, the fix is out of scope under the freeze, and the branch is retained if it is picked back up.

— sent from snappy-dove-250