From c1e14894ab505c03727ce877d41b6c59e36141ac Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 28 Aug 2026 04:35:14 +0000 Subject: [PATCH 1/2] Route belt publication absence through filesystem evidence --- dag/gunbc/roadmap_belt_actuate.dag | 116 +++++++++--------- .../roadmap_belt_actuate_witness_test.dag | 14 --- 2 files changed, 55 insertions(+), 75 deletions(-) diff --git a/dag/gunbc/roadmap_belt_actuate.dag b/dag/gunbc/roadmap_belt_actuate.dag index da663412c62..327bcca2333 100644 --- a/dag/gunbc/roadmap_belt_actuate.dag +++ b/dag/gunbc/roadmap_belt_actuate.dag @@ -345,7 +345,20 @@ import gunbc.roadmap_presentation { } import extdeps.gunbc import extdeps.shell -import extdeps.filesystem.filesystem_io +import extdeps.filesystem.filesystem_io { + Filesystem, + FilesystemEntryAbsent, + FilesystemEntryListed, + FilesystemEntryPresenceIndeterminate, + FilesystemFileAbsent, + FilesystemFileRead, + FilesystemFileIndeterminate, + FilesystemFileObservationsDisagree, + filesystem_listing_observation, + filesystem_entry_presence, + filesystem_read_outcome, + filesystem_file_observation, +} import extdeps.llm.cli { shape_codex_login_status_env_args_for_program, shape_codex_version_env_args_for_program, @@ -2837,18 +2850,7 @@ fn provider_event_projection_error( } } -data belt_publication_receipt_read_note: String = "THE RECEIPT IS ADDRESSED BY HEAD, SO THERE IS NO PATH TO READ UNTIL THE HEAD IS KNOWN. That ordering is the point: the other receipts on this row live at one path per attempt and can be read before anything is decided, while a publication receipt is one per head, so the subject has to exist before the address does.\\n\\nTHE UNOBSERVED ARM ANSWERS ReceiptSourceAbsent AND THAT IS NOT A FABRICATED ABSENCE. publication_segment refuses on an unobserved subject before it consults the source at all, so this value never reaches a judgment; it exists because the evidence record carries a source for every stage and there is no address to consult for this one. If the projection ever stopped refusing first, this would become a real answer - which is why the refusal there is matched on the subject rather than inferred here.\\n\\nEVERY OTHER ARM ESTABLISHES ITS ANSWER POSITIVELY - see publication_receipt_absence_is_established_note. No arm of this walk turns a failure into an absence, which is the whole difference between it and the read it replaced." - -data listing_membership_is_line_exact_note: String = "Filesystem.List returns entry names joined by newlines, so a plain substring test would answer yes for a name that is merely a PREFIX or suffix of a real entry - `abc.json` would be found inside `abc.json.tmp`, and a head sha would be found inside a longer one. Wrapping both sides in newlines makes the test line-exact without needing a split the interpreter does not offer, and every conclusion drawn from it is a membership fact rather than a coincidence of spelling." - -fn belt_listing_names_entry(listing: String, name: String) -> Bool { - string_contains( - s: join(["\n", listing, "\n"], ""), - pattern: join(["\n", name, "\n"], ""), - ) -} - -data publication_receipt_absence_is_established_note: String = "ABSENCE IS ESTABLISHED BY A SUCCESSFUL LISTING, NEVER BY A FAILED READ (review 46148). Filesystem.Read answers success=false both for a receipt that does not exist and for one that exists and cannot be read, and those two worlds have opposite correct actions - observe and write, versus stop and preserve. This walk therefore never concludes absence from a failure of any kind.\\n\\nTHE LADDER STARTS AT A DIRECTORY THAT IS KNOWN TO EXIST, which is what makes each step decidable. The attempt state directory is created by dispatch when the attempt starts, and this producer only runs for an attempt whose worktree head it has already read, so a failure to list THAT directory is unambiguously a fault rather than a not-yet. From there each answer is positive: the publication directory is absent from a listing that succeeded, or the head's own file is absent from a listing that succeeded. Only when the file is listed does a read happen, and a read that then fails is unambiguously a fault because the entry was just observed to exist.\\n\\nWHAT THIS DELIBERATELY DOES NOT DO is widen on doubt. Every failure arm returns ReceiptSourceUnreadable carrying the path and the host error, which the gate turns into a typed, located, counted refusal that halts the row - it never falls back to `treat it as absent and rewrite`, which is the absorbing fallback DESIGN section 5 forbids and precisely the defect this replaced." +data belt_publication_receipt_read_note: String = "THE RECEIPT IS ADDRESSED BY HEAD, SO THERE IS NO PATH TO READ UNTIL THE HEAD IS KNOWN. That ordering is the point: the other receipts on this row live at one path per attempt and can be read before anything is decided, while a publication receipt is one per head, so the subject has to exist before the address does.\\n\\nTHE UNOBSERVED ARM ANSWERS ReceiptSourceAbsent AND THAT IS NOT A FABRICATED ABSENCE. publication_segment refuses on an unobserved subject before it consults the source at all, so this value never reaches a judgment; it exists because the evidence record carries a source for every stage and there is no address to consult for this one. If the projection ever stopped refusing first, this would become a real answer - which is why the refusal there is matched on the subject rather than inferred here.\\n\\nEVERY OBSERVED ARM CONSUMES THE FILESYSTEM AUTHORITY. filesystem_entry_presence decides whether the publication directory is listed, and filesystem_file_observation decides the head-addressed receipt. ReceiptSourceAbsent can therefore be projected only from FilesystemEstablishedAbsence, whose sole mint consumes a successful directory listing; this module no longer carries either a prose copy of that law or a second spelling of List's membership encoding. Listing refusal, listed-but-unreadable, and observations that disagree all project to ReceiptSourceUnreadable." fn belt_publication_receipt_source( instance: HostDashboardInstance, @@ -2865,63 +2867,55 @@ fn belt_publication_receipt_source( attempt_key: attempt_key, ) let attempt_listing = Filesystem.List(path: attempt_dir) - if !attempt_listing.success { - ReceiptSourceUnreadable { - detail: join([ - "the attempt state directory could not be listed, so whether a publication receipt exists was not established: ", - attempt_dir, - " (", - attempt_listing.error, - ")", - ], ""), - } - } else if !belt_listing_names_entry( - listing: attempt_listing.entries, + match filesystem_entry_presence( + listing: filesystem_listing_observation( + directory: attempt_dir, + success: attempt_listing.success, + entries: attempt_listing.entries, + error: attempt_listing.error, + ), name: publication_receipt_directory_segment, ) { - ReceiptSourceAbsent - } else { - let publication_dir = dispatch_attempt_publication_dir_for_instance( - instance: instance, - node_id: node_id, - attempt_key: attempt_key, - ) - let publication_listing = Filesystem.List(path: publication_dir) - if !publication_listing.success { - ReceiptSourceUnreadable { - detail: join([ - "the publication receipt directory was named by the attempt listing but could not itself be listed: ", - publication_dir, - " (", - publication_listing.error, - ")", - ], ""), - } - } else if !belt_listing_names_entry( - listing: publication_listing.entries, - name: join([observed.expected_head as String, ".json"], ""), - ) { - ReceiptSourceAbsent - } else { + FilesystemEntryPresenceIndeterminate { cause: c } => + ReceiptSourceUnreadable { detail: c } + FilesystemEntryAbsent(_) => ReceiptSourceAbsent + FilesystemEntryListed { directory: _, name: _ } => { + let publication_dir = dispatch_attempt_publication_dir_for_instance( + instance: instance, + node_id: node_id, + attempt_key: attempt_key, + ) + let receipt_basename = join([observed.expected_head as String, ".json"], "") let path = dispatch_attempt_publication_receipt_path_for_instance( instance: instance, node_id: node_id, attempt_key: attempt_key, head_sha: observed.expected_head as String, ) + let publication_listing = Filesystem.List(path: publication_dir) let read = Filesystem.Read(path: path) - if read.success { - ReceiptSourcePresent { text: read.content } - } else { - ReceiptSourceUnreadable { - detail: join([ - "a publication receipt for this head was listed and then could not be read, so it exists and its content is unavailable: ", - path, - " (", - read.error, - ")", - ], ""), - } + match filesystem_file_observation( + listing: filesystem_listing_observation( + directory: publication_dir, + success: publication_listing.success, + entries: publication_listing.entries, + error: publication_listing.error, + ), + name: receipt_basename, + path: path, + read: filesystem_read_outcome( + content: read.content, + success: read.success, + error: read.error, + ), + ) { + FilesystemFileIndeterminate { cause: c } => + ReceiptSourceUnreadable { detail: c } + FilesystemFileObservationsDisagree { path: _, cause: c } => + ReceiptSourceUnreadable { detail: c } + FilesystemFileAbsent(_) => ReceiptSourceAbsent + FilesystemFileRead { path: _, content: text } => + ReceiptSourcePresent { text: text } } } } diff --git a/dag/test/claim/roadmap_belt_actuate_witness_test.dag b/dag/test/claim/roadmap_belt_actuate_witness_test.dag index b0137075f14..781d9095db9 100644 --- a/dag/test/claim/roadmap_belt_actuate_witness_test.dag +++ b/dag/test/claim/roadmap_belt_actuate_witness_test.dag @@ -128,7 +128,6 @@ import gunbc.roadmap_belt_actuate { belt_publication_subject_for, BeltPublishGate, PublishProceed, PublishHalted, belt_publish_gate, - belt_listing_names_entry, belt_publish_write_outcome, BeltPublishOutcome, PublishRecorded, PublishAlreadyRecorded, PublishEvidenceUnreadable, @@ -1597,19 +1596,6 @@ test fn a_present_but_empty_receipt_is_a_fault_not_an_absence() -> Bool { } } -data listing_membership_note: String = "The line-exact membership test is what makes every ABSENCE conclusion in belt_publication_receipt_source a fact rather than a spelling coincidence. A plain substring test would find a head sha inside a longer one, or a receipt name inside its own .tmp sibling, and would then report a receipt PRESENT that is not there - or, worse under the opposite skew, miss one that is. The prefix and suffix cases are asserted, not just the positive." - -test fn listing_membership_is_line_exact_not_substring() -> Bool { - let listing = join(["alpha.json", "beta.json", "beta.json.tmp"], "\n") - belt_listing_names_entry(listing: listing, name: "alpha.json") - && belt_listing_names_entry(listing: listing, name: "beta.json") - && belt_listing_names_entry(listing: listing, name: "beta.json.tmp") - && !belt_listing_names_entry(listing: listing, name: "eta.json") - && !belt_listing_names_entry(listing: listing, name: "beta") - && !belt_listing_names_entry(listing: listing, name: "gamma.json") - && !belt_listing_names_entry(listing: "", name: "alpha.json") -} - test fn an_undecodable_receipt_is_not_overwritten_either() -> Bool { match belt_publish_gate( node_id: "belt-pub-node", From 6d245db1fb7c18fa0e4e47ed68f357303c8402d4 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Fri, 28 Aug 2026 06:20:31 +0000 Subject: [PATCH 2/2] Preserve filesystem service import binding --- dag/gunbc/roadmap_belt_actuate.dag | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dag/gunbc/roadmap_belt_actuate.dag b/dag/gunbc/roadmap_belt_actuate.dag index 327bcca2333..523b2e05bcc 100644 --- a/dag/gunbc/roadmap_belt_actuate.dag +++ b/dag/gunbc/roadmap_belt_actuate.dag @@ -345,8 +345,8 @@ import gunbc.roadmap_presentation { } import extdeps.gunbc import extdeps.shell +import extdeps.filesystem.filesystem_io import extdeps.filesystem.filesystem_io { - Filesystem, FilesystemEntryAbsent, FilesystemEntryListed, FilesystemEntryPresenceIndeterminate,