NO-FALLBACK-1: mount is a bounded establishment, and a green after a terminal refusal is a defect

[gunbai-bot]

Second of the two no-fallback follow-ups ruled during #9690's review. Stacked on #9779 (base is that branch, so this diff is only the NO-FALLBACK-1 change).

The defect

Read as prose, "wait for the listing to change" and "keep asking until it agrees" are the same sentence. The executed MegaRAC sequence contains a genuine asynchronous pending phase — media config accepted, the daemon's own retry interval elapses, the images listing goes from refusing to listing the image — and that phase existed only in a comment. A documented pending state is legitimate; repeating an operation until an observation finally agrees is not; and nothing in the model could tell them apart.

The repair

gunbc.machine_intake_mount_establishment makes the difference structural:

MountRequested → MountPending → MountEstablished
                              | MountTimedOut
                              | MountObservationContradictory

• Pending is representable only inside a declared bounded window. The deadline is a function of the request, so "wait a bit longer" has nowhere to live.
• Every exit is terminal, and the fold has no arm that replaces a terminal standing with a newer observation — last-wins is unwritable rather than discouraged.
• A listing arriving after the deadline is TimedOutThenListed, carrying the deadline it missed and the bytes it was read from, because discarding an earlier terminal refusal because a later poll agreed is the instability this refuses.
• An absence after establishment is EstablishedThenAbsent, not a return to pending.
• Out-of-order and before-the-request observations are defects, not newer readings — the last-wins hazard at its root.
• An empty observation list is MountRequested and not established: a mount nobody looked at is not a mount that worked.

The carrier is workflow-layer, not extdeps, per DESIGN §3's external-upstream rule: AMI owns the operation contract in extdeps.bmc.megarac; what our polling saw is a receipt of our attempt.

Also repaired

My #9690 merge resolution left the boot-from-ISO recipe annotation duplicated in megarac.dag — main's #9752 conversion and my own copy both landed. Two prose blocks for one fact is exactly the §3 violation that conversion existed to remove. One survives, and it now points at the carrier above instead of describing the wait in prose that reads as permission to poll.

Evidence

All twenty-three witnesses evaluate true. The mutation is the point: making a listing after the timeout an accepted late success — precisely retry-until-green — turns a_listing_after_the_timeout_is_a_contradiction_not_a_late_success false while a_listing_inside_the_window_establishes_the_mount stays true. The pair discriminates the unsafe behaviour specifically rather than any change at all: the legitimate asynchronous path stays green and only the retry-past-terminal path reds. Corpus parse-clean at 4408 files.

🤖 Generated with Claude Code

https://claude.ai/code/session_019fKvi5dnJ8TcE514qbmWTk

Corrections from review (this branch)

Equal timestamps are unordered. The out-of-order check refused only a strict decrease, so two observations sharing one millisecond were resolved by the order the caller passed them — absent-then-listed established the mount, listed-then-absent contradicted it. One clock, two verdicts, decided by an argument's index. ObservationTimestampCollision refuses the pair in either order, byte-identical included: the defect is that the ordering is unknown, not that the observations disagree.

The window is half-open. requested_at <= observed_at < deadline, so an observation exactly at the deadline is outside it and a budget cannot be spent at its own boundary. A zero budget is therefore an immediately-closed window, which is the honest meaning of Milliseconds' declared range rather than a claim the carrier does not support.

Time closes the window. The fold answered only over observations actually taken, so a pending attempt nobody re-polled stayed pending indefinitely past its own deadline — the declared bound was enforced only against callers that kept looking. MountEvaluationBoundary carries its own clock evidence rather than reading a clock, so the same observations plus the same boundary always give the same standing.

The boundary refusal is total across every standing. This was a real wrong answer, caught in review. The frontier was reconstructed from the standing, but only MountPending carries one: MountEstablished records when it was established, not the last thing seen after it, and the other terminal arms carry no frontier at all. So a boundary earlier than the evidence behind any terminal standing was silently accepted — a verdict read as of a moment before the observations that produced it. A per-arm timestamp projection cannot fix this, because "established at 2000" and "last observed at 4000" are different facts and only the fold holds the second. The fold is now the answer and the standing its projection; the two wrong-construction helpers are deleted rather than left beside the fix. EvaluationBoundaryBeforeRequest covers the no-observations case, where the coherent lower bound is the request itself.

Terminal means no revival, not immutability. The prose claimed no later observation can overwrite a terminal standing, which is false and was hiding correct behaviour: Established and TimedOut may be refined into Contradictory, because evidence that an answer was wrong must not be discarded to protect the answer. What no observation may do is revive a terminal standing into pending or success.

Eleven further controls, four of which reach a terminal standing and then observe again so the frontier is later than anything the standing carries — shapes a per-standing patch cannot satisfy.

Round 4 — two facts, and a timeout that invents nothing

MountFold carried one timestamp answering two questions. previous_at answers "is this observation out of order or colliding", which is about the immediately preceding element; the boundary check asked it "what is the latest moment this fold has evidence about", which is about the maximum. Those coincide only while timestamps strictly increase, and this module exists to represent populations where they do not — listed@2000 / absent@3000 / absent@2500 retracted the frontier to 2500 and then accepted a boundary at 2600 over evidence timestamped 3000. frontier_at is now a separate monotone maximum, advanced on every supplied observation including refused ones: it is the high-water mark of what the fold has seen, not of what it accepted, because evidence that provoked a refusal is still evidence in hand.

That same population also lost its contradiction. The temporal prechecks run before advance_mount_standing, so a malformed observation arriving after a contradiction replaced it with its own cause — the declared law that Contradictory maps to the identical Contradictory standing held only for well-formed successors. mount_fold_step now opens with a contradiction guard.

boundary_incoherence checks the two lower bounds independently. The request bound previously lived inside the no-observations arm, so an observation at 500 against a request at 1000, read as of 750, returned an as-of verdict about an attempt that had not yet begun.

And the unobserved timeout fabricated its own evidence: it recorded last_observed_at = window.requested_at, which is when the request was made and not a moment anything was seen. MountTimedOut is now { window, basis } over MountTimeoutBasis, so a clock-only close carries the boundary that closed it with an honestly absent frontier, and a close established by an observed absence carries that observation and its bytes — distinguishable by a consumer, which they were not. The witness covering the unobserved timeout ignored the field and so greened over the fabrication; it now reads it.

Five further controls: contradiction preservation under a malformed successor, 3000 then 2000 read at 2600, a before-request boundary with observations, and the observed-absence basis naming its observation.