Make absence-from-a-failed-read unrepresentable: the listing ruling was prose, and prose reproduced the defect it forbids

[gunbai-bot]

The rule was ruled, written down, and then broken by the hand that wrote it down, in the module that carries it. gunbc.roadmap_belt_actuate publication_receipt_absence_is_established_note states review 46148 in full — ABSENCE IS ESTABLISHED BY A SUCCESSFUL LISTING, NEVER BY A FAILED READ — and gunbc.deploy_transition was then authored beside it with a marker that was present-and-unreadable rendering as absent, which rendered as PERMITTED at the belt seam (repaired in #9561). DESIGN §4c says exactly why: a note is commentary no Accepted program can read, so it propagates only by someone happening to scroll past it. A note is not a mechanism.

What lands

extdeps.filesystem.filesystem_io gains an absence carrier with one mint.

• FilesystemEstablishedAbsence is sole_constructor. Its only mint takes a FilesystemDirectoryListing, which is itself sole_constructor and is minted only from a listing whose success channel was true. A module that tries to decide absence from a read alone has no value to return and no way to build one.
• filesystem_entry_presence and filesystem_file_observation are the two folds. Presence is decided by the listing; the read is consulted only for an entry the listing named, so a read that then fails is unambiguously a fault and lands FilesystemFileIndeterminate, never absent.
• Every way of not establishing absence — listing refused, entry listed but unreadable — lands in one indeterminate arm the consumer must handle.

Consumers, not a carrier with no consumer

• gunbc.roadmap_verification_receipt — both walks (current_verification_selection_observe, exact_verification_receipt_source_read). They were already correct by hand; they now consume the carrier instead of restating the rule, and their private verification_listing_names_entry (a second spelling of List's wire encoding) is deleted in favour of filesystem_listing_names_entry.
• gunbc.devboot.build read_text_file — a real repair. It inferred TextFileAbsent from an empty error string on a failed read: a heuristic over a host message standing where a declared operation was available (§4), and silent about the case that matters — an artifact that exists and cannot be read reported the same absence as one the producer never wrote, and the exchange walk treats absent as "the producer had nothing to say" and carries on.

Rung, stated at the honest grain (§4b)

Structurally guaranteed on the source-to-.dag acceptance path, for the consumers that route through the folds — a record literal for either carrier outside its home module is refused. NOT structural on the emitted-Rust path, where DESIGN §4b records that a sole_constructor type's emitted mirror is a public struct with public fields and is forgeable; next-rung trigger is the emitted mirror carrying the construction confinement, which is that section's open item and not this module's to close. And it is mitigatable nowhere else: the raw Read and List operations stay callable, so an unadopted module can still write the conflation.

The remainder, at identity grain, not as a count

filesystem_absence_establishment_adoption_standing enumerates every remaining site that concludes absence from a failure — each one read rather than pattern-matched, with what it does wrong — plus what is deliberately NOT on the list and why. Monotone direction: the roster may only shrink; a new site of this shape is a defect to repair, not a row to add. No corpus-wide ratchet pinned to a tree-measured number (§5 rejects that oracle).

Evidence

dag/test/claim/filesystem_absence_establishment_witness_test.dag, six hermetic witnesses, SubstrateInputsOnly so they run in the ordinary floor. Green by execution via claim_batch. The discriminating pair is inside a_marker_that_is_listed_and_unreadable_is_not_absent: same fold, same refused read, arms decided by the LISTING and not by the read's status.

The construction wall itself is measured, not asserted: a fixture writing the record literal cross-module is refused at the literal's own position with sole_constructor type 'FilesystemEstablishedAbsence' cannot be constructed outside its defining module, with the enrolled cross-module GREEN control being the witness that obtains an absence from the mint and reads its fields. Recorded in filesystem_absence_establishment_wall_receipt, with what it does not establish.

Also green by execution after the change: roadmap_verification_receipt_witness_test (8/8), and v1_src_dag_parse parse-clean over 4230 files.

Note on overlap with #9561

filesystem_listing_names_entry is authored here identically to its text on session/eager-heron-604, which has not merged. Whichever lands first, the other's merge resolves to the same bytes; the corpus never holds two spellings. gunbc.deploy_transition is that PR's module and is deliberately untouched here — it should become a consumer of this carrier rather than keeping its own copy, which is a follow-up on that lane.

🤖 Generated with Claude Code

[gunbai-bot]

review 57099 — accepted as a real defect, fixed, with the proposed remedy declined and a different one taken.

The finding is correct: filesystem_file_observation's absent arm returned the established absence and never consulted the read, so a successful read was discarded while the answer said nothing is there. Bytes in hand and an answer of "absent" is fail-open at the exact seam this module exists to close. Fixed.

What I did not do, and why. The review's remedy is to prioritize the successful read. That would let the read decide the listing's question — this module's own conflation turned around. A read answers "these bytes existed at instant T2"; it never answers "this directory holds this entry", and Read's success channel is precisely the one that cannot separate absent from unreadable (that is the whole premise of the carrier). Under a race in the other direction — file deleted between List and Read — prioritizing the read yields absent from a read refusal, which is the original defect restored. Picking either observation as the winner fabricates one consistent world out of two observations that describe different instants, which is the plausible output §5 forbids.

What I did instead. The disagreement is a third fact with its own remedy (re-observe the pair atomically, or hold the directory still), so it gets its own arm: FilesystemFileObservationsDisagree { path, cause }. Neither observation is discarded — the cause carries both. It is deliberately not folded into FilesystemFileIndeterminate: "I could not look" and "I looked twice and got two answers" have different remedies, and collapsing them is the state-space conflation this repo keeps finding. Both converted consumers handle the new arm as a stop (SelectionUnreadable, ExactVerificationReceiptUnreadable, TextFileReadFailed) — no consumer treats a disagreement as absence, and the exhaustive match means a third consumer cannot silently inherit one.

Regression cases added, both green by execution:

• a_successful_read_of_an_unlisted_entry_is_not_an_absence — the case you named. Three clauses over the same listing and the same missing entry, only the READ differing: refused → the ordinary established absence, succeeded → disagree. The third clause keeps the absent arm reachable, so an implementation answering "disagree" whenever the entry is unlisted fails it.
• a_disagreement_is_distinct_from_an_unmakeable_observation — a fold that collapsed disagree into indeterminate passes every other test in the file; this one goes red.

Note on scope, stated rather than implied: the fold is a pure function of two supplied observations. It cannot make the pair atomic — nothing in a List-then-Read sequence can — so what changes is that a race is now reported instead of being resolved into good news. That is the honest ceiling here, and the arm is what makes the race countable rather than silent.

The discrimination is measured, not argued. With the absent arm restored to its three-state form (return the established absence, never consult the read), a_successful_read_of_an_unlisted_entry_is_not_an_absence goes RED and the other seven stay green — one failure, exactly the case you named. Restored, all eight pass. roadmap_verification_receipt_witness_test also green after the arm was added to both of its walks.

Scope, stated rather than implied: the fold is a pure function of two supplied observations and cannot make the pair atomic — nothing in a List-then-Read sequence can. What changes is that the race is now reported and countable instead of resolved into good news.

— sent from zesty-fox-404