From f6196fc08deb0c5cfdc5c64b326c450f078933cf Mon Sep 17 00:00:00 2001 From: deep-owl-19 Date: Fri, 2 Oct 2026 08:39:45 +0000 Subject: [PATCH 01/11] filesystem: absence is established, never inferred (DP-M5) Delete data row filesystem_absence_establishment_adoption_standing by converting all six of its identities: each site that concluded Absent from a failed read or a false shell Test.IsFile now routes through filesystem_file_observation / filesystem_entry_presence, so could-not-look becomes typed refusal (FilesystemFileIndeterminate / SubjectRefused) and only an unobserved listing establishes absence. - host_effect_nbd_proxy_serve: session-token read is a 3-arm BmcwebSessionTokenObservation with a rewritten reader - fleet_converge_plan_cli observe_cap_members_wet: already converted on main (verified by reading the site) - product_receipt_stage: manifest/producer reads carry ManifestUnobservable/ProducerUnobservable causes - merge_admission_walk: tested-subject and floor-receipt wire reads refuse as RefreshTestedSubjectWireUnreadable/RefreshFloorReceiptWireUnreadable - codex_supervised_turn: generation-store read folded through the filesystem observation; Unreadable refuses as duplicate-execution guard instead of admitting - opaque_realization_census: declaration-body standing gains DeclarationSourceUnreadable(path, cause), resolved-wins scan Sibling row filesystem_read_outcome_adoption_standing re-measured at identity grain with a named instrument (calibrated against b21b710d); emitted_tree_read_then converted opportunistically. --- dag/extdeps/filesystem/filesystem_io.dag | 11 +- dag/gunbc/auth/approval_decision_store.dag | 5 +- dag/gunbc/codex_supervised_turn.dag | 83 +++++-- .../host/host_effect_nbd_proxy_serve.dag | 104 +++++++-- .../instruments/merge_admission_walk.dag | 209 +++++++++++++----- .../instruments/opaque_realization_census.dag | 190 +++++++++++++--- .../codex_supervised_turn_witness_test.dag | 162 +++++++++++--- .../merge_admission_attempt_witness_test.dag | 172 +++++++++++++- ...nbd_proxy_serve_transport_witness_test.dag | 124 +++++++++++ ...e_census_declaration_scan_witness_test.dag | 139 ++++++++++++ .../claim/workflow/product_receipt_test.dag | 154 +++++++++++++ src/v2/workflow/product_receipt.dag | 6 + src/v2/workflow/product_receipt_stage.dag | 185 +++++++++++++--- 13 files changed, 1343 insertions(+), 201 deletions(-) diff --git a/dag/extdeps/filesystem/filesystem_io.dag b/dag/extdeps/filesystem/filesystem_io.dag index fcb2d2a4c87..f6c64f0a85f 100644 --- a/dag/extdeps/filesystem/filesystem_io.dag +++ b/dag/extdeps/filesystem/filesystem_io.dag @@ -157,7 +157,7 @@ fn filesystem_create_new( } } -data filesystem_read_outcome_adoption_standing: String ="RUNG: mitigatable. filesystem_read_outcome provides the single modeled fold from Filesystem.Read's scalar transport observation into FilesystemReadSucceeded | FilesystemReadRefused, but nothing forces callers through it. gunbc.ci_yaml_validate is the first converted consumer and preserves read refusal separately from YAML parse refusal. The raw operation remains directly consumed elsewhere, so content+success+error nonsense combinations remain writable at those sites. SUBJECT: an unconverted consumption site is a Filesystem Read call whose bound result has any success, error, or content projection outside the three arguments of filesystem_read_outcome. The call and those three projections remain after conversion because they supply the fold; adoption changes where they are consumed, not whether they exist. BASELINE measured on origin/main b21b710d5378387ae0c841f07323292c5d72faba: 92 unconverted consumption sites across 48 .dag files. REMAINDER after the first conversion: 91 unconverted consumption sites across 47 files. RE-DERIVATION: enumerate Filesystem Read assignment calls in tracked .dag source, excluding this adoption-standing data declaration so the instrument cannot count its own prose; for each bound result, classify it converted only when every success, error, and content projection is an argument of filesystem_read_outcome, otherwise classify it unconverted; count unconverted rows and distinct paths. NEXT-RUNG TRIGGER: the unconverted population reaches zero -- every Filesystem Read result projection occurs only as an argument to filesystem_read_outcome. The compiler-only filesystem_read intrinsic is a separate replacement migration and is not part of this population or this fold." +data filesystem_read_outcome_adoption_standing: String ="RUNG: mitigatable. filesystem_read_outcome provides the single modeled fold from Filesystem.Read's scalar transport observation into FilesystemReadSucceeded | FilesystemReadRefused, but nothing forces callers through it. gunbc.ci_yaml_validate is the first converted consumer and preserves read refusal separately from YAML parse refusal. The raw operation remains directly consumed elsewhere, so content+success+error nonsense combinations remain writable at those sites. SUBJECT: an unconverted consumption site is a Filesystem Read call whose bound result has any success, error, or content projection outside the three arguments of filesystem_read_outcome. The call and those three projections remain after conversion because they supply the fold; adoption changes where they are consumed, not whether they exist. BASELINE measured on origin/main b21b710d5378387ae0c841f07323292c5d72faba: 92 unconverted consumption sites across 48 .dag files. REMAINDER after the first conversion: 91 unconverted consumption sites across 47 files. RE-MEASURED 2026-10-02 on session/deep-owl-19 (origin/main d85c2d8fadecee55c2a9ca5b3c536d159b8f86e6 plus the six absence-establishment conversions and the opaque_realization_census emitted-tree fold this branch carries), same subject, the instrument implemented as spelled here with two mechanical precisions: a projection counts as an argument of the fold iff it sits inside the paren span of a filesystem_read_outcome( call, so multi-line calls classify correctly, and comment lines are not consumption sites -- the same rule that keeps this declaration out of its own count. CALIBRATION: the same implementation reproduces 90 unconverted sites across 46 files at b21b710d against the 92/48 the baseline sentence above records; the difference is filesystem_exact_read sites, which the literal reading classifies unconverted -- that is the sibling modeled fold carrying error_kind, not this fold. MEASURED: 205 unconverted consumption sites across 103 .dag files, with 28 bindings converted and 9 bindings carrying no projection at all; the corpus grew 472 to 7392 tracked .dag files since the baseline head, so the population grew in absolute terms while adoption improved in proportion, and 39 of the 205 are dag/test/claim fixtures. RE-DERIVATION: enumerate Filesystem Read assignment calls in tracked .dag source, excluding this adoption-standing data declaration so the instrument cannot count its own prose; for each bound result, classify it converted only when every success, error, and content projection is an argument of filesystem_read_outcome, otherwise classify it unconverted; count unconverted rows and distinct paths. NEXT-RUNG TRIGGER: the unconverted population reaches zero -- every Filesystem Read result projection occurs only as an argument to filesystem_read_outcome. The compiler-only filesystem_read intrinsic is a separate replacement migration and is not part of this population or this fold." // ABSENCE IS ESTABLISHED BY A SUCCESSFUL LISTING, NEVER BY A FAILED READ. `Read` answers // success=false both for a path that does not exist and for one that exists and cannot be read, and @@ -197,7 +197,7 @@ fn filesystem_listing_names_entry(listing: String, name: String) -> Bool { // SCOPE, STATED RATHER THAN IMPLIED. This carrier is ADOPTED AT ITS FIRST CONSUMER and is not yet // the type of `filesystem_entry_presence`'s `name` parameter, which is still `String` and still // reachable by every existing caller. Widening it is a replacement migration over that whole -// population and belongs with `filesystem_absence_establishment_adoption_standing` above, not +// population in its own change, not // smuggled into the change that introduces the carrier. What is true today: a consumer that admits // the name and then uses the SAME admitted value for both the membership test and the path // construction cannot put those two out of step. A consumer that does not adopt it is exactly as @@ -346,8 +346,8 @@ fn admit_filesystem_entry_name(name: String) -> FilesystemEntryNameAdmission { // that a `sole_constructor` type's emitted mirror is a public struct with public fields and is // forgeable. Next-rung trigger: the emitted mirror carrying the construction confinement, which is // that section's open item and not this module's to close. And it is a wall over the consumers that -// ROUTE THROUGH IT, not over the corpus: the raw operations remain callable, so adoption is the -// separate obligation recorded in `filesystem_absence_establishment_adoption_standing`. +// ROUTE THROUGH IT, not over the corpus: the raw operations remain callable, so adoption at each +// consumer is the obligation the fold cannot enforce for it. // THE WALL ABOVE IS MEASURED RATHER THAN ASSERTED, and it is recorded here because no enrolled // witness can hold it: the claim is about what the COMPILER REFUSES, its subject is source text // rather than a value, and a hermetic witness that asserted it would be a permanently-green arm @@ -422,7 +422,7 @@ type FilesystemDirectoryListing sole_constructor { // joins names with newlines, so this is the split -- blank lines dropped, every other line one // name as the host spelled it. A consumer that split `entries` itself would be the second // decoder of one wire format (review 69704 of gunbc#12000 found one; extdeps.realization -// artifact_store_fs carries an older one under filesystem_absence_establishment_adoption_standing). +// artifact_store_fs carries an older one). fn filesystem_listing_entry_names(listing: FilesystemDirectoryListing) -> List { listing.entries.split(delimiter: "\n").filter(n => n != "") } @@ -645,7 +645,6 @@ fn filesystem_established_absence_path(absence: FilesystemEstablishedAbsence) -> } } -data filesystem_absence_establishment_adoption_standing: String = "RUNG: structurally guaranteed for the consumers that route through filesystem_file_observation, on the source-to-.dag acceptance path only, and MITIGATABLE NOWHERE ELSE -- the raw Filesystem.Read and Filesystem.List operations stay callable, so a module that has not adopted the carrier can still write the conflation. This row states the unconverted population at identity grain rather than as a count, because a count is not a plan and a one-sided ratchet over a number measured on the current tree is the oracle section 5 rejects. SUBJECT: a site that concludes ABSENCE, NOT-PRESENT or a dropped element from a FAILED read or a FAILED boolean path test, rather than from a listing that succeeded. It is not every Filesystem.Read consumer -- most read a file they already know exists, and those are the separate filesystem_read_outcome adoption population above. ENUMERATED SITES, each one read rather than pattern-matched, on origin/main at the head this row lands against, with the two converted by the change that lands this row already removed (gunbc.roadmap_verification_receipt current_verification_selection_observe and exact_verification_receipt_source_read, and gunbc.devboot.build read_text_file): gunbc.host_effect_nbd_proxy_serve host_effect_nbd_proxy_serve_read_session_token (read refusal answers Absent, and an empty content does too); gunbc.fleet_converge_plan_cli observe_cap_members_wet (a cap member whose dropin could not be read is DROPPED from the observed list, so the converge plan is computed over a silently narrowed population); v2.workflow.product_receipt_stage run_product_receipt_stage (an unreadable manifest answers ArtifactIdentityAbsent { ProducerReportedNoArtifact }, attributing to the producer a report it never made); tools.merge_admission_walk read_tested_subject and read_floor_receipt (a read refusal answers the Optional's absent arm); gunbc.codex_supervised_turn codex_supervised_turn_generation_observation (GenerationAbsent is concluded from shell.Test.IsFile answering false. THIS ROW IS CLASSIFIED FROM THE PRODUCER RATHER THAN FROM THE CALL SITE, on a caution from the lane that shipped this defect today: a predicate whose job is to answer the presence question would not belong here. extdeps.shell Test.IsFile is `test -f` with its own declared exit table reading `1 => Path is missing or not a regular file`, so ONE exit code carries missing, wrong-kind, and -- since `test -f` is false when the parent directory cannot be searched -- could-not-look. It answers false on an unreadable-but-present path, so it is the same defect with a different producer, and it is the construction gunbc.fabric_cell_acquire retired for exactly this reason); tools.opaque_realization_census declaration_body_standing (a file that could not be read leaves the fold state unchanged, so it is indistinguishable from a file that did not hold the declaration). WHAT IS DELIBERATELY NOT ON THE LIST: gunbc.roadmap_belt_actuate belt_read_or_empty, whose collapse is scoped and argued in belt_read_or_empty_scope_note -- both branches take the same action at every remaining caller -- and gunbc.fabric_cell_acquire, which already establishes absence from the parent enumeration through its own four-state observation and would gain nothing but a second spelling. MONOTONE DIRECTION: the roster above may only shrink. A row leaves it when the site routes through filesystem_file_observation or filesystem_entry_presence, or when the site is deleted; a NEW site of this shape is a defect to repair rather than a row to add. NEXT-RUNG TRIGGER, and it names the capability rather than an artifact: the raw List and Read result projections cease to be reachable outside this module's folds, so a consumer cannot spell the conflation at all -- at which point the enumeration above has no subject and this row is deleted. That is the same trigger filesystem_read_outcome_adoption_standing carries, one question further in: it asks that every read projection be folded, this asks that every ABSENCE be established." // WriteCreateNew: CREATE-ONLY IS A DIFFERENT FACT FROM OWNER-ONLY, and this annotation sits here // rather than above the operation because only module-item grain is modeled (DESIGN section 4c) -- diff --git a/dag/gunbc/auth/approval_decision_store.dag b/dag/gunbc/auth/approval_decision_store.dag index ae8ed9a9d07..b4be17b88fa 100644 --- a/dag/gunbc/auth/approval_decision_store.dag +++ b/dag/gunbc/auth/approval_decision_store.dag @@ -118,8 +118,9 @@ data approval_mac_key_suite: MacSuite = HmacSha256 // nothing renders it. data approval_mac_key_path: NonEmptyStr = "/etc/gunbc-roadmap/approval-mac-key" -// ABSENT AND UNREADABLE ARE TWO REFUSALS WITH TWO REMEDIES (review 66990; -// extdeps.filesystem.filesystem_io filesystem_absence_establishment_adoption_standing): an absent +// ABSENT AND UNREADABLE ARE TWO REFUSALS WITH TWO REMEDIES (review 66990; the doctrine +// extdeps.filesystem.filesystem_io filesystem_file_observation carries: absence is established by a +// listing that succeeded, never by a failed read): an absent // key means the materialization frontier has not run; an unreadable one means it ran and the unit // cannot read what it wrote -- a permission on the file, not a missing step. Reading `content` // alone and calling "" absent would report the second as the first, which fails toward good news. diff --git a/dag/gunbc/codex_supervised_turn.dag b/dag/gunbc/codex_supervised_turn.dag index 58c55b6338a..b1046302c7b 100644 --- a/dag/gunbc/codex_supervised_turn.dag +++ b/dag/gunbc/codex_supervised_turn.dag @@ -42,7 +42,18 @@ import gunbc.codex_app_server_press { AccountStandingIncomplete, AccountStandingInitializeUnusable, } -import extdeps.filesystem.filesystem_io { Filesystem } +import extdeps.filesystem.filesystem_io { + Filesystem, + FilesystemFileObservation, + FilesystemFileAbsent, + FilesystemFileRead, + FilesystemFileIndeterminate, + FilesystemFileObservationsDisagree, + FilesystemFileSubjectRefused, + filesystem_read_outcome, + filesystem_listing_observation, + filesystem_file_observation, +} import extdeps.shell import gunbc.provider_standing_probe_bridge { provider_standing_bundle_from_codex_press_receipt, @@ -126,7 +137,7 @@ import extdeps.languages.json.parse { data codex_supervised_client_command_id_file_name: String = "/codex_supervised_client_command_id" -data codex_supervised_turn_generation_file_name: String = "/codex_supervised_turn_generation" +data codex_supervised_turn_generation_file_name: String = "codex_supervised_turn_generation" // OPERATOR VERDICT #8166 (2026-08-16): RejectAndFinishNow on concat-built bash coprocess scaffold. // codex_supervised_turn_script DELETED. Supervised turn executes only through host_effect_apply @@ -280,7 +291,7 @@ fn codex_supervised_turn_client_command_id_store_path(evidence_root: FilePath) - } fn codex_supervised_turn_generation_store_path(evidence_root: FilePath) -> String { - concat(evidence_root as String, codex_supervised_turn_generation_file_name) + concat(evidence_root as String, concat("/", codex_supervised_turn_generation_file_name)) } fn codex_supervised_generation_read_from_content(content: String) -> CodexSupervisedGenerationRead { @@ -300,34 +311,58 @@ fn codex_supervised_generation_read_from_content(content: String) -> CodexSuperv } } -fn codex_supervised_generation_read_from_store( - store_present: Bool, - read_success: Bool, - content: String, +// ABSENCE IS ESTABLISHED BY THE LISTING, NEVER BY THE READ, AND NEVER BY SHELL TEST. This site used +// to answer GenerationAbsent from `test -f`, whose one exit code carries "missing", "not a regular +// file", and "could not look" -- so an unreadable-but-present generation store admitted a fresh +// supervised turn exactly as if no prior turn had ever run, which is the duplicate-execution hazard +// the store exists to fence. The listing and the read are now one observation through +// filesystem_file_observation: GenerationAbsent is reachable only from a listing that succeeded and +// did not name the store, and every could-not-look shape refuses as GenerationStoreUnreadable with +// its cause. `codex_supervised_turn_generation_file_name` carries the bare entry name (it is +// admitted as a directory entry, and entry admission refuses "/"); the store path re-adds the +// separator, so persisted paths are unchanged. +fn codex_supervised_generation_read_from_observation( + o: FilesystemFileObservation, ) -> CodexSupervisedGenerationRead { - if store_present == false { - GenerationAbsent - } else if read_success == false { - GenerationStoreUnreadable { - reason: "supervised turn generation store unreadable" as NonEmptyStr, - } - } else { - codex_supervised_generation_read_from_content(content: content) + match o { + FilesystemFileRead { path: _, content: content } => + codex_supervised_generation_read_from_content(content: content) + FilesystemFileAbsent(_) => GenerationAbsent + FilesystemFileIndeterminate { cause: c } => codex_supervised_generation_unobserved(cause: c) + FilesystemFileObservationsDisagree { path: _, cause: c } => + codex_supervised_generation_unobserved(cause: c) + FilesystemFileSubjectRefused { directory: _, name: _, cause: c } => + codex_supervised_generation_unobserved(cause: c) + } +} + +fn codex_supervised_generation_unobserved(cause: String) -> CodexSupervisedGenerationRead { + GenerationStoreUnreadable { + reason: join(["the generation store could not be observed: ", cause], "") as NonEmptyStr, } } fn read_codex_supervised_turn_prior_generation(evidence_root: FilePath) -> CodexSupervisedGenerationRead { let path = codex_supervised_turn_generation_store_path(evidence_root: evidence_root) - if shell.Test.IsFile(path: path as FilePath).is_file == false { - GenerationAbsent - } else { - let read = Filesystem.Read(path: path) - codex_supervised_generation_read_from_store( - store_present: true, - read_success: read.success, - content: read.content, - ) + let parts = split(s: path, delimiter: "/") + let name = match parts.last() { + Present { value: value } => value + Absent => "" } + let directory = join(parts.take(n: length(parts) - 1), "/") + let listing = Filesystem.List(path: directory) + let read = Filesystem.Read(path: path) + codex_supervised_generation_read_from_observation(o: filesystem_file_observation( + listing: filesystem_listing_observation( + directory: directory, + success: listing.success, + entries: listing.entries, + error: listing.error, + ), + name: name, + path: path, + read: filesystem_read_outcome(content: read.content, success: read.success, error: read.error), + )) } fn codex_supervised_turn_generation_admission( diff --git a/dag/gunbc/host/host_effect_nbd_proxy_serve.dag b/dag/gunbc/host/host_effect_nbd_proxy_serve.dag index 98bedad27af..570da8c21bc 100644 --- a/dag/gunbc/host/host_effect_nbd_proxy_serve.dag +++ b/dag/gunbc/host/host_effect_nbd_proxy_serve.dag @@ -21,7 +21,19 @@ import extdeps.bmc.webui.nbd_proxy_serve { import extdeps.exec.command { ArgvCommand, argv_words } import extdeps.tools.nbdkit { nbdkit_readonly_file_serve_command } import extdeps.tools.websocat { websocat_nbd_proxy_bridge_command } -import extdeps.filesystem.filesystem_io { Filesystem } +import extdeps.filesystem.filesystem_io { + Filesystem, + FilesystemEstablishedAbsence, + FilesystemFileObservation, + FilesystemFileAbsent, + FilesystemFileRead, + FilesystemFileIndeterminate, + FilesystemFileObservationsDisagree, + FilesystemFileSubjectRefused, + filesystem_read_outcome, + filesystem_listing_observation, + filesystem_file_observation, +} import extdeps.gunbc import gunbc.session_lease { ProcessPortScope, @@ -202,15 +214,81 @@ fn host_effect_nbd_proxy_serve_apply_drains_stale_matching( } } -fn host_effect_nbd_proxy_serve_read_session_token() -> String? { - let read = Filesystem.Read(path: srv3_bmcweb_token_path) - match read.success { - true => - match read.content != "" { - true => Present { value: read.content } - false => Absent +// ABSENCE IS ESTABLISHED BY THE LISTING, NEVER BY THE READ, AND NEVER BY SHELL TEST. This site +// used to answer `Absent` on a refused read AND on an empty content, so an unreadable-but-present +// token file (a permission on the file, not a missing step) reported exactly what a token the +// materialization never wrote reports: "session token absent". Those two worlds have opposite +// remedies, so the read and the listing are now one observation through +// filesystem_file_observation, and Absent is reachable only from a listing that succeeded and did +// not name the file. An empty content is a THIRD fact and is carried as one: the file exists and +// holds no token, which is a broken materialization, not an absent one. +type BmcwebSessionTokenObservation + = BmcwebSessionTokenRead { token: String } + | BmcwebSessionTokenAbsent(FilesystemEstablishedAbsence) + | BmcwebSessionTokenUnobservable { cause: String } + +fn bmcweb_session_token_observation_of(o: FilesystemFileObservation) -> BmcwebSessionTokenObservation { + match o { + FilesystemFileRead { path: _, content: token } => BmcwebSessionTokenRead { token: token } + FilesystemFileAbsent(established) => BmcwebSessionTokenAbsent(established) + FilesystemFileIndeterminate { cause: c } => BmcwebSessionTokenUnobservable { cause: c } + FilesystemFileObservationsDisagree { path: _, cause: c } => BmcwebSessionTokenUnobservable { cause: c } + FilesystemFileSubjectRefused { directory: _, name: _, cause: c } => + BmcwebSessionTokenUnobservable { cause: c } + } +} + +fn host_effect_nbd_proxy_serve_read_session_token() -> BmcwebSessionTokenObservation { + let path = srv3_bmcweb_token_path + let parts = split(s: path, delimiter: "/") + let name = match parts.last() { + Present { value: value } => value + Absent => "" + } + let directory = join(parts.take(n: length(parts) - 1), "/") + let listing = Filesystem.List(path: directory) + let read = Filesystem.Read(path: path) + bmcweb_session_token_observation_of(o: filesystem_file_observation( + listing: filesystem_listing_observation( + directory: directory, + success: listing.success, + entries: listing.entries, + error: listing.error, + ), + name: name, + path: path, + read: filesystem_read_outcome(content: read.content, success: read.success, error: read.error), + )) +} + +// THE START DECISION IS PURE SO IT IS CLAIMABLE. The wet read above runs the host operations; this +// function is total over what they reported, and the unit-start caller consumes its verdict +// verbatim -- so the claim suite can hold the policy (an unobservable token refuses with its cause, +// an established absence refuses as absent, an empty file refuses as present-but-empty, and only a +// non-empty token starts the units) without starting any unit. +type BmcwebSessionTokenStartDecision + = BmcwebSessionTokenUsable { token: NonEmptyStr } + | BmcwebSessionTokenStartRefused { reason: NonEmptyStr } + +fn bmcweb_session_token_start_decision(o: BmcwebSessionTokenObservation) -> BmcwebSessionTokenStartDecision { + match o { + BmcwebSessionTokenRead { token: t } => + if t == "" { + BmcwebSessionTokenStartRefused { + reason: "the BMCWEB session token file is present and holds no token" as NonEmptyStr, + } + } else { + BmcwebSessionTokenUsable { token: t as NonEmptyStr } + } + BmcwebSessionTokenAbsent(_) => + BmcwebSessionTokenStartRefused { reason: "BMCWEB session token absent" as NonEmptyStr } + BmcwebSessionTokenUnobservable { cause: c } => + BmcwebSessionTokenStartRefused { + reason: join( + ["the BMCWEB session token could not be observed, so the units were not started: ", c], + "", + ) as NonEmptyStr, } - false => Absent } } @@ -257,9 +335,9 @@ fn host_effect_nbd_proxy_serve_start_units( ) -> String? { let nbdkit_unit = nbd_proxy_serve_nbdkit_unit_name(lease_key: binding.lease_key) let websocat_unit = nbd_proxy_serve_websocat_unit_name(lease_key: binding.lease_key) - match host_effect_nbd_proxy_serve_read_session_token() { - Absent => Present { value: "BMCWEB session token absent" } - Present { value: token } => + match bmcweb_session_token_start_decision(o: host_effect_nbd_proxy_serve_read_session_token()) { + BmcwebSessionTokenStartRefused { reason: why } => Present { value: why as String } + BmcwebSessionTokenUsable { token: token } => match host_effect_nbd_proxy_serve_systemd_run_transient( unit: nbdkit_unit, command_argv: argv_words(command: nbdkit_readonly_file_serve_command( @@ -274,7 +352,7 @@ fn host_effect_nbd_proxy_serve_start_units( unit: websocat_unit, command_argv: argv_words(command: host_effect_nbd_proxy_serve_websocat_command_materialized( intent: binding.intent, - token: token as NonEmptyStr, + token: token, )), transport: transport, ) diff --git a/dag/gunbc/instruments/merge_admission_walk.dag b/dag/gunbc/instruments/merge_admission_walk.dag index da632b34ce5..905c43b18a6 100644 --- a/dag/gunbc/instruments/merge_admission_walk.dag +++ b/dag/gunbc/instruments/merge_admission_walk.dag @@ -5,7 +5,19 @@ import extdeps.git { git_remote_ref_parts } import extdeps.git import extdeps.git.inspect import extdeps.shell -import extdeps.filesystem.filesystem_io { Filesystem } +import extdeps.filesystem.filesystem_io { + Filesystem, + FilesystemEstablishedAbsence, + FilesystemFileObservation, + FilesystemFileAbsent, + FilesystemFileRead, + FilesystemFileIndeterminate, + FilesystemFileObservationsDisagree, + FilesystemFileSubjectRefused, + filesystem_read_outcome, + filesystem_listing_observation, + filesystem_file_observation, +} import extdeps.github.checks { CheckConclusion, Success } import gunbc.merge_admission { MergeAdmissionReceiptV2, @@ -74,28 +86,81 @@ data merge_admission_fetch_stall_deadline_seconds: Seconds = 240 // FetchNoTags's located failure result while time remains to write the stage receipt; the 60-minute // workflow wrapper is not the fetch watchdog. -fn read_tested_subject(root: String, attempt_id: WalkAttemptId) -> TestedSubject? { - let read = Filesystem.Read( - path: merge_admission_tested_subject_path(root: root, attempt_id: attempt_id) +// BOTH WIRES ARE OBSERVED THROUGH THE FILESYSTEM OBSERVATION FOLD, AND ABSENCE COMES ONLY FROM A +// LISTING THAT SUCCEEDED. Both readers used to answer the Optional's absent arm on a refused read, +// so a stage receipt that exists and cannot be read reported exactly what a stage that never wrote +// reports -- and the two have opposite remedies (investigate the host versus re-run the stage). +// The `decoded` field is an Optional DELIBERATELY: observing the file and decoding its content are +// two facts, and a present-but-undecodable wire keeps its existing disposition instead of being +// re-labelled by this change. +type TestedSubjectWireObservation + = TestedSubjectWireRead { decoded: TestedSubject? } + | TestedSubjectWireAbsent(FilesystemEstablishedAbsence) + | TestedSubjectWireUnobservable { cause: String } + +type FloorReceiptWireObservation + = FloorReceiptWireRead { decoded: MergeAdmissionReceiptV2? } + | FloorReceiptWireAbsent(FilesystemEstablishedAbsence) + | FloorReceiptWireUnobservable { cause: String } + +fn wire_file_observation(path: String) -> FilesystemFileObservation { + let parts = split(s: path, delimiter: "/") + let name = match parts.last() { + Present { value: value } => value + Absent => "" + } + let directory = join(parts.take(n: length(parts) - 1), "/") + let listing = Filesystem.List(path: directory) + let read = Filesystem.Read(path: path) + filesystem_file_observation( + listing: filesystem_listing_observation( + directory: directory, + success: listing.success, + entries: listing.entries, + error: listing.error, + ), + name: name, + path: path, + read: filesystem_read_outcome(content: read.content, success: read.success, error: read.error), ) - if !read.success { - none - } else { - parse_tested_subject_wire(text: read.content) +} + +fn tested_subject_wire_observation_of(o: FilesystemFileObservation) -> TestedSubjectWireObservation { + match o { + FilesystemFileRead { path: _, content: text } => + TestedSubjectWireRead { decoded: parse_tested_subject_wire(text: text) } + FilesystemFileAbsent(established) => TestedSubjectWireAbsent(established) + FilesystemFileIndeterminate { cause: c } => TestedSubjectWireUnobservable { cause: c } + FilesystemFileObservationsDisagree { path: _, cause: c } => TestedSubjectWireUnobservable { cause: c } + FilesystemFileSubjectRefused { directory: _, name: _, cause: c } => + TestedSubjectWireUnobservable { cause: c } } } -fn read_floor_receipt(root: String, attempt_id: WalkAttemptId) -> MergeAdmissionReceiptV2? { - let read = Filesystem.Read( - path: merge_admission_floor_receipt_path(root: root, attempt_id: attempt_id) - ) - if !read.success { - none - } else { - parse_receipt_wire_v2(text: read.content) +fn floor_receipt_wire_observation_of(o: FilesystemFileObservation) -> FloorReceiptWireObservation { + match o { + FilesystemFileRead { path: _, content: text } => + FloorReceiptWireRead { decoded: parse_receipt_wire_v2(text: text) } + FilesystemFileAbsent(established) => FloorReceiptWireAbsent(established) + FilesystemFileIndeterminate { cause: c } => FloorReceiptWireUnobservable { cause: c } + FilesystemFileObservationsDisagree { path: _, cause: c } => FloorReceiptWireUnobservable { cause: c } + FilesystemFileSubjectRefused { directory: _, name: _, cause: c } => + FloorReceiptWireUnobservable { cause: c } } } +fn read_tested_subject(root: String, attempt_id: WalkAttemptId) -> TestedSubjectWireObservation { + tested_subject_wire_observation_of(o: wire_file_observation( + path: merge_admission_tested_subject_path(root: root, attempt_id: attempt_id) + )) +} + +fn read_floor_receipt(root: String, attempt_id: WalkAttemptId) -> FloorReceiptWireObservation { + floor_receipt_wire_observation_of(o: wire_file_observation( + path: merge_admission_floor_receipt_path(root: root, attempt_id: attempt_id) + )) +} + // THE CONCLUSION IS AN OPERAND, NOT A CONSTANT, AND THAT IS THE WHOLE POINT OF THIS SHAPE. // // stamp_tested_floor took no conclusion and wrote `conclusion: Success` literally. That was not a @@ -120,21 +185,26 @@ fn stamp_tested_floor_with_conclusion(conclusion: CheckConclusion) -> Bool { Present { value: attempt_id } => let root = git.Inspect.Toplevel().path as String match read_tested_subject(root: root, attempt_id: attempt_id) { - Absent => false - Present { value: subject } => - let _pr_number_note = merge_admission_pr_number_deferred_note - let receipt = MergeAdmissionReceiptV2 { - attempt_id: attempt_id, - pr_number: none, - tested_head_sha: subject.head_sha, - tested_base_commit_sha: subject.base_commit_sha, - gate_roster_hash: current_gate_roster_hash, - conclusion: conclusion, + TestedSubjectWireAbsent(_) => false + TestedSubjectWireUnobservable { cause: _ } => false + TestedSubjectWireRead { decoded: d } => + match d { + Absent => false + Present { value: subject } => + let _pr_number_note = merge_admission_pr_number_deferred_note + let receipt = MergeAdmissionReceiptV2 { + attempt_id: attempt_id, + pr_number: none, + tested_head_sha: subject.head_sha, + tested_base_commit_sha: subject.base_commit_sha, + gate_roster_hash: current_gate_roster_hash, + conclusion: conclusion, + } + Filesystem.Write( + path: merge_admission_floor_receipt_path(root: root, attempt_id: attempt_id), + content: render_receipt_wire_v2(receipt: receipt) + ).success } - Filesystem.Write( - path: merge_admission_floor_receipt_path(root: root, attempt_id: attempt_id), - content: render_receipt_wire_v2(receipt: receipt) - ).success } } } @@ -154,7 +224,9 @@ type MergeTargetRefreshRefusal = RefreshFetchRefused { stderr: String } | RefreshAttemptIdentityAbsent | RefreshTestedSubjectWireMissing + | RefreshTestedSubjectWireUnreadable { cause: String } | RefreshFloorReceiptWireMissing + | RefreshFloorReceiptWireUnreadable { cause: String } | RefreshTargetCommitObservationRefused | RefreshVerdictDenied { verdict: String } @@ -167,7 +239,11 @@ fn merge_target_refresh_refusal_label(cause: MergeTargetRefreshRefusal) -> Strin RefreshFetchRefused { stderr: stderr } => concat("fetch-refused stderr=", stderr) RefreshAttemptIdentityAbsent => "attempt-identity-absent" RefreshTestedSubjectWireMissing => "tested-subject-wire-missing" + RefreshTestedSubjectWireUnreadable { cause: why } => + concat("tested-subject-wire-unreadable ", why) RefreshFloorReceiptWireMissing => "floor-receipt-wire-missing" + RefreshFloorReceiptWireUnreadable { cause: why } => + concat("floor-receipt-wire-unreadable ", why) RefreshTargetCommitObservationRefused => "target-commit-observation-refused" RefreshVerdictDenied { verdict: verdict } => concat("verdict-denied verdict=", verdict) } @@ -188,13 +264,14 @@ data merge_admission_refresh_refusal_wire_relpath: String = "target/merge-admiss // a future cut needs it and it is cheaper to write now than to re-derive. This module is // REFERENCED: merge_admission_fetch_stall_deadline_seconds is imported by // gunbc.instruments.merge_admission_current_context and asserted by the enrolled witness -// merge_admission_attempt_witness_test, so deleting the module reds a live witness. Two of its -// functions are also ENUMERATED SITES of a monotone debt roster -- -// extdeps.filesystem.filesystem_io filesystem_absence_establishment_adoption_standing names -// read_tested_subject and read_floor_receipt for concluding absence from a failed read -- and that -// roster permits a row to leave by deletion, so a cut would discharge two of its rows as a side -// effect. Neither fact argues against cutting; both say a cut is its own change with its own -// reviewer, not a cleanup a census lane performs in passing. +// merge_admission_attempt_witness_test, so deleting the module reds a live witness. Its two +// wire readers -- read_tested_subject and read_floor_receipt -- used to conclude absence from a +// failed read, the defect class extdeps.filesystem.filesystem_io filesystem_file_observation +// closes (absence is established by a listing that succeeded, never by a failed read); both now +// route through that fold, which is what the debt roster that once enumerated them required +// before it could be deleted with its roster empty. The fold is no longer a reason to keep this +// module alive, and neither is it a reason a cut would be a cleanup: a cut remains its own change +// with its own reviewer, not something a census lane performs in passing. // TYPED CAUSE FOR THE STAGE-2 CLAIM BOUNDARY (review 47542 finding 3, made blocking by CI run // 30764945450: refresh_current_target_and_gate returned bare Bool false on srv4-04 with all seven @@ -263,30 +340,42 @@ fn merge_target_refresh() -> MergeTargetRefresh { Present { value: attempt_id } => let root = git.Inspect.Toplevel().path as String match read_tested_subject(root: root, attempt_id: attempt_id) { - Absent => MergeTargetRefreshRefused { cause: RefreshTestedSubjectWireMissing } - Present { value: subject } => - match read_floor_receipt(root: root, attempt_id: attempt_id) { - Absent => MergeTargetRefreshRefused { cause: RefreshFloorReceiptWireMissing } - Present { value: receipt } => - let current_commit = git.Inspect.ResolveRefCommit(ref: merge_admission_merge_base_ref as GitRef) - if !current_commit.success { - MergeTargetRefreshRefused { cause: RefreshTargetCommitObservationRefused } - } else { - let verdict = classify_merge_admission_verdict_v2( - current_attempt_id: attempt_id, - tested_subject: subject, - receipt: receipt, - merge_target_commit_sha: current_commit.sha, - current_roster_hash: current_gate_roster_hash - ) - if merge_freshness_verdict_is_consumed_to_block() { - match verdict { - MergeAdmitted => MergeTargetRefreshed - _ => MergeTargetRefreshRefused { cause: RefreshVerdictDenied { verdict: merge_admission_verdict_label(v: verdict) } } + TestedSubjectWireAbsent(_) => MergeTargetRefreshRefused { cause: RefreshTestedSubjectWireMissing } + TestedSubjectWireUnobservable { cause: c } => + MergeTargetRefreshRefused { cause: RefreshTestedSubjectWireUnreadable { cause: c } } + TestedSubjectWireRead { decoded: d } => + match d { + Absent => MergeTargetRefreshRefused { cause: RefreshTestedSubjectWireMissing } + Present { value: subject } => + match read_floor_receipt(root: root, attempt_id: attempt_id) { + FloorReceiptWireAbsent(_) => MergeTargetRefreshRefused { cause: RefreshFloorReceiptWireMissing } + FloorReceiptWireUnobservable { cause: c } => + MergeTargetRefreshRefused { cause: RefreshFloorReceiptWireUnreadable { cause: c } } + FloorReceiptWireRead { decoded: rd } => + match rd { + Absent => MergeTargetRefreshRefused { cause: RefreshFloorReceiptWireMissing } + Present { value: receipt } => + let current_commit = git.Inspect.ResolveRefCommit(ref: merge_admission_merge_base_ref as GitRef) + if !current_commit.success { + MergeTargetRefreshRefused { cause: RefreshTargetCommitObservationRefused } + } else { + let verdict = classify_merge_admission_verdict_v2( + current_attempt_id: attempt_id, + tested_subject: subject, + receipt: receipt, + merge_target_commit_sha: current_commit.sha, + current_roster_hash: current_gate_roster_hash + ) + if merge_freshness_verdict_is_consumed_to_block() { + match verdict { + MergeAdmitted => MergeTargetRefreshed + _ => MergeTargetRefreshRefused { cause: RefreshVerdictDenied { verdict: merge_admission_verdict_label(v: verdict) } } + } + } else { + MergeTargetRefreshed + } + } } - } else { - MergeTargetRefreshed - } } } } diff --git a/dag/gunbc/instruments/opaque_realization_census.dag b/dag/gunbc/instruments/opaque_realization_census.dag index 43bcc1e7d2f..28ef90c1d46 100644 --- a/dag/gunbc/instruments/opaque_realization_census.dag +++ b/dag/gunbc/instruments/opaque_realization_census.dag @@ -7,7 +7,20 @@ import extdeps.shell import extdeps.gunbc import extdeps.git import extdeps.git.inspect -import extdeps.filesystem.filesystem_io { Filesystem } +import extdeps.filesystem.filesystem_io { + Filesystem, + FilesystemFileObservation, + FilesystemFileAbsent, + FilesystemFileRead, + FilesystemFileIndeterminate, + FilesystemFileObservationsDisagree, + FilesystemFileSubjectRefused, + FilesystemReadSucceeded, + FilesystemReadRefused, + filesystem_read_outcome, + filesystem_listing_observation, + filesystem_file_observation, +} import tools.host_prelude { witness_bin, witness_bin_ensure_built_typed, @@ -145,10 +158,24 @@ type ReferenceRealizationPolicyStanding // from a body the author wrote). Those are indistinguishable in the artifact and they are different // subjects, so the source declaration is read for this and only this. A source file that cannot be // located refuses rather than defaulting to either answer. +// +// AND UNLOCATABLE HAS TWO MEANINGS THAT ONE ARM USED TO CARRY. `DeclarationSourceUnresolved` answered +// both "we looked at every candidate spelling and none holds the declaration" (an established +// absence, one listing at a time) and "a candidate could not be looked at at all" (the listing or +// the read was refused -- could-not-look), which is the same conflation filesystem_file_observation +// exists to close everywhere else. The candidate scan now +// runs through filesystem_file_observation: the unresolved arm is reachable only from candidates +// whose parent listing SUCCEEDED and did not name the file (or whose content, read, does not declare +// the name), and any could-not-look shape surfaces as DeclarationSourceUnreadable with the path and +// the host's cause. A resolved candidate still wins over a recorded fault -- the fault names a +// different candidate spelling, and a file that was actually read and declares the name answers the +// question -- so the census's happy path is unchanged and only the terminal all-unresolved case +// gained the distinction. type DeclarationBodyStanding = DeclaredOpaque | DeclaredWithBody | DeclarationSourceUnresolved { attempted: String } + | DeclarationSourceUnreadable { path: String, cause: String } // The declaration scan's own state. It exists because the body question cannot be answered from the // declaration line alone: a line ending after the name is undecided until the following non-blank @@ -166,6 +193,19 @@ type OpaqueSubjectRow { standing: DeclarationBodyStanding } +// THE CANDIDATE FOLD'S CARRIER, so the wet reader stays one small function and the policy over what +// the candidates reported is pure and claimable. `unobserved` holds the FIRST could-not-look +// candidate in candidate order; a later fault does not displace it -- one fault is enough to answer +// "could the absence have been established at all", and `attempted` still names every candidate. +type UnobservedDeclarationCandidate { + path: String + cause: String +} + +type DeclarationCandidateScan + = DeclarationScanResolved { standing: DeclarationBodyStanding } + | DeclarationScanUnresolved { attempted: String, unobserved: UnobservedDeclarationCandidate? } + // --------------------------------------------------------------------------------------------- // WHERE THE EMITTED TREE CAME FROM IS A FACT THE MEASUREMENT CARRIES, never an assumption. A census @@ -714,27 +754,115 @@ fn declaration_body_standing_in(content: String, name: String) -> DeclarationBod } } +// THE ONE WET READER the candidate fold is allowed, and the pure policy over what it reported. The +// observation is ONE fact per candidate -- the listing decides presence, the read supplies content +// only for a listed file -- so the fold below cannot sequence the two channels differently from any +// other consumer of this module. +fn declaration_candidate_observation(path: String) -> FilesystemFileObservation { + let parts = split(s: path, delimiter: "/") + let name = match parts.last() { + Present { value: value } => value + Absent => "" + } + let directory = join(parts.take(n: length(parts) - 1), "/") + let listing = Filesystem.List(path: directory) + let read = Filesystem.Read(path: path) + filesystem_file_observation( + listing: filesystem_listing_observation( + directory: directory, + success: listing.success, + entries: listing.entries, + error: listing.error, + ), + name: name, + path: path, + read: filesystem_read_outcome(content: read.content, success: read.success, error: read.error), + ) +} + +// THE FOLD STEP IS TOTAL OVER THE OBSERVATION, which is what makes the policy claimable: the witness +// suite constructs each transport shape and holds the rules -- resolved wins, an established absence +// keeps the search unresolved, the first could-not-look is recorded and the search continues -- over +// constructed values, without touching a host filesystem. `attempted` rides through unchanged so the +// terminal arm still names every candidate spelling. +fn declaration_candidate_scan_then_with( + acc: DeclarationCandidateScan, + o: FilesystemFileObservation, + name: String, + path: String, +) -> DeclarationCandidateScan { + match acc { + DeclarationScanResolved { standing: _ } => acc + DeclarationScanUnresolved { attempted: a, unobserved: u } => + match o { + FilesystemFileRead { path: _, content: c } => + match declaration_body_standing_in(content: c, name: name) { + Present { value: v } => DeclarationScanResolved { standing: v } + Absent => DeclarationScanUnresolved { attempted: a, unobserved: u } + } + FilesystemFileAbsent(_) => DeclarationScanUnresolved { attempted: a, unobserved: u } + FilesystemFileIndeterminate { cause: c } => + DeclarationScanUnresolved { + attempted: a, + unobserved: first_unobserved_candidate(u: u, path: path, cause: c), + } + FilesystemFileObservationsDisagree { path: p, cause: c } => + DeclarationScanUnresolved { + attempted: a, + unobserved: first_unobserved_candidate(u: u, path: p, cause: c), + } + FilesystemFileSubjectRefused { directory: d, name: n, cause: c } => + DeclarationScanUnresolved { + attempted: a, + unobserved: first_unobserved_candidate( + u: u, + path: join([d, n], "/"), + cause: c, + ), + } + } + } +} + +fn first_unobserved_candidate( + u: UnobservedDeclarationCandidate?, + path: String, + cause: String, +) -> UnobservedDeclarationCandidate? { + match u { + Present { value: _ } => u + Absent => Present { value: UnobservedDeclarationCandidate { path: path, cause: cause } } + } +} + +// THE TERMINAL DECODE IS ALSO PURE AND CLAIMABLE: a resolved scan answers; an unresolved scan with +// a recorded could-not-look refuses as unreadable; only a scan whose every candidate was looked at +// and found absent (or read without declaring the name) answers unresolved. +fn declaration_standing_from_scan(scan: DeclarationCandidateScan) -> DeclarationBodyStanding { + match scan { + DeclarationScanResolved { standing: s } => s + DeclarationScanUnresolved { attempted: a, unobserved: u } => + match u { + Present { value: bad } => DeclarationSourceUnreadable { path: bad.path, cause: bad.cause } + Absent => DeclarationSourceUnresolved { attempted: a } + } + } +} + fn declaration_body_standing(source_module: String, name: String, roots: List) -> DeclarationBodyStanding { let candidates = module_candidate_paths(source_module: source_module, roots: roots) - fold( + let scan = fold( candidates, - init: DeclarationSourceUnresolved { attempted: join(candidates, " ") }, + init: DeclarationScanUnresolved { attempted: join(candidates, " "), unobserved: none }, f: (acc, path) => - match acc { - DeclaredOpaque => acc - DeclaredWithBody => acc - DeclarationSourceUnresolved { attempted: a } => - let read = Filesystem.Read(path: path) - if !read.success { - acc - } else { - match declaration_body_standing_in(content: read.content, name: name) { - Present { value: v } => v - Absent => acc - } - } - } + declaration_candidate_scan_then_with( + acc: acc, + o: declaration_candidate_observation(path: path), + name: name, + path: path, + ) ) + declaration_standing_from_scan(scan: scan) } // --------------------------------------------------------------------------------------------- @@ -757,16 +885,24 @@ fn emitted_tree_read_then(acc: EmittedTreeRead, path: String) -> EmittedTreeRead match acc { EmittedTreeUnreadable { cause: c } => EmittedTreeUnreadable { cause: c } EmittedTreeFiles { files: so_far } => + // The read's scalar channels are folded through the interface's own coproduct + // (filesystem_read_outcome) rather than branched on `success` directly, so this site consumes + // the modeled result like every converted consumer of the transport. let read = Filesystem.Read(path: path) - if !read.success { - EmittedTreeUnreadable { - cause: concat( - "an emitted file could not be read, so the subject is incomplete and any population over the rest would be a fraction reported as a whole: ", - concat(path, concat(" — ", read.error)) - ) - } - } else { - EmittedTreeFiles { files: list_push(so_far, read_emitted_file(path: path, content: read.content)) } + match filesystem_read_outcome( + content: read.content, + success: read.success, + error: read.error, + ) { + FilesystemReadRefused { error: e } => + EmittedTreeUnreadable { + cause: concat( + "an emitted file could not be read, so the subject is incomplete and any population over the rest would be a fraction reported as a whole: ", + concat(path, concat(" — ", e)) + ) + } + FilesystemReadSucceeded { content: c } => + EmittedTreeFiles { files: list_push(so_far, read_emitted_file(path: path, content: c)) } } } } @@ -1075,6 +1211,8 @@ fn standing_text(s: DeclarationBodyStanding) -> String { DeclaredOpaque => "opaque" DeclaredWithBody => "has-body" DeclarationSourceUnresolved { attempted: a } => concat("source-unresolved(", concat(a, ")")) + DeclarationSourceUnreadable { path: p, cause: c } => + concat("source-unreadable(", concat(p, concat(": ", concat(c, ")")))) } } diff --git a/dag/test/claim/codex_supervised_turn_witness_test.dag b/dag/test/claim/codex_supervised_turn_witness_test.dag index e722df02fd2..0e08cce3c66 100644 --- a/dag/test/claim/codex_supervised_turn_witness_test.dag +++ b/dag/test/claim/codex_supervised_turn_witness_test.dag @@ -26,7 +26,9 @@ import gunbc.codex_supervised_turn { codex_supervised_turn_client_command_id, codex_supervised_turn_session_policy, codex_supervised_turn_start_line_template, - codex_supervised_generation_read_from_store, + codex_supervised_turn_generation_file_name, + codex_supervised_generation_read_from_observation, + codex_supervised_turn_generation_store_path, codex_supervised_turn_generation_admission, codex_turn_start_admission, codex_runner_turn_terminal_receipt, @@ -54,6 +56,15 @@ import std.temporal_effect { LeaseRunningExpected, } +import extdeps.filesystem.filesystem_io { + FilesystemEstablishedAbsence, + FilesystemFileAbsent, + FilesystemFileRead, + FilesystemFileIndeterminate, + FilesystemFileObservationsDisagree, + FilesystemFileSubjectRefused, +} + data witness_note: String = "Hermetic witnesses for the supervised-runner slice: std.temporal_effect HeldLease fences one WorkerTurn attempt; thread idle without a runner terminal receipt refuses turn/start (continuity receipt trap); busy thread refuses until the runner writes a receipt; parse_supervised_turn_stdout correlates thread/start and turn/start ids and turn/completed notifications into a terminal receipt with client_command_id." data supervised_turn_fixture_stdout: String = "{\"jsonrpc\":\"2.0\",\"id\":4,\"result\":{\"thread\":{\"id\":\"thread-uuid-1\"}}}\n{\"jsonrpc\":\"2.0\",\"id\":5,\"result\":{\"turn\":{\"id\":\"turn-uuid-1\"}}}\n{\"jsonrpc\":\"2.0\",\"method\":\"turn/completed\",\"params\":{}}\n" @@ -302,22 +313,121 @@ test fn witness_nonzero_exit_without_turn_start_is_not_observed() -> Bool { } } +// THE GENERATION STORE WITNESSES RUN AT THE OBSERVATION FOLD, not through the wet reader: the fold +// is total over FilesystemFileObservation, so each transport shape is a constructed value and the +// claim suite holds the policy without touching a host filesystem. Three of these are REDS against +// the former site, which answered `test -f` false with GenerationAbsent and ADMITTED the turn: an +// unlistable evidence directory, an inadmissible store name, and a listing/read disagreement are +// could-not-look shapes that now refuse with their cause. Established absence -- a listing that +// succeeded and did not name the store -- is the only Absent route, and it still admits. test fn witness_missing_generation_store_reads_as_zero() -> Bool { - match codex_supervised_generation_read_from_store( - store_present: false, - read_success: true, - content: "", + match codex_supervised_generation_read_from_observation( + o: FilesystemFileAbsent( + FilesystemEstablishedAbsence { + directory: "/tmp/gunbc-supervised-evidence" as FilePath, + name: codex_supervised_turn_generation_file_name, + }, + ), ) { GenerationAbsent => true _ => false } } +test fn witness_established_generation_absence_admits_supervised_turn_start() -> Bool { + let read = codex_supervised_generation_read_from_observation( + o: FilesystemFileAbsent( + FilesystemEstablishedAbsence { + directory: "/tmp/gunbc-supervised-evidence" as FilePath, + name: codex_supervised_turn_generation_file_name, + }, + ), + ) + match codex_supervised_turn_generation_admission(read: read) { + CodexTurnStartAdmitted => true + _ => false + } +} + +test fn witness_unlistable_evidence_directory_refuses_supervised_turn_start() -> Bool { + let read = codex_supervised_generation_read_from_observation( + o: FilesystemFileIndeterminate { + cause: "the directory /tmp/gunbc-supervised-evidence could not be listed, so the absence of codex_supervised_turn_generation is not established -- permission denied", + }, + ) + match read { + GenerationStoreUnreadable { reason: _ } => + match codex_supervised_turn_generation_admission(read: read) { + CodexTurnStartRefusedDuplicateExecution { reason: _ } => true + _ => false + } + _ => false + } +} + +test fn witness_listed_but_unreadable_generation_store_refuses_supervised_turn_start() -> Bool { + let read = codex_supervised_generation_read_from_observation( + o: FilesystemFileIndeterminate { + cause: "/tmp/gunbc-supervised-evidence/codex_supervised_turn_generation is listed and could not be read, so it exists and its content is unavailable -- permission denied", + }, + ) + match read { + GenerationStoreUnreadable { reason: _ } => + match codex_supervised_turn_generation_admission(read: read) { + CodexTurnStartRefusedDuplicateExecution { reason: _ } => true + _ => false + } + _ => false + } +} + +test fn witness_inadmissible_generation_store_name_refuses_supervised_turn_start() -> Bool { + let read = codex_supervised_generation_read_from_observation( + o: FilesystemFileSubjectRefused { + directory: "/tmp/gunbc-supervised-evidence", + name: "", + cause: "the entry name \"\" is not admissible", + }, + ) + match read { + GenerationStoreUnreadable { reason: _ } => + match codex_supervised_turn_generation_admission(read: read) { + CodexTurnStartRefusedDuplicateExecution { reason: _ } => true + _ => false + } + _ => false + } +} + +test fn witness_generation_store_observation_disagreement_refuses_supervised_turn_start() -> Bool { + let read = codex_supervised_generation_read_from_observation( + o: FilesystemFileObservationsDisagree { + path: "/tmp/gunbc-supervised-evidence/codex_supervised_turn_generation", + cause: "no codex_supervised_turn_generation is listed in /tmp/gunbc-supervised-evidence, and a read of that path then succeeded -- the two observations describe different instants", + }, + ) + match read { + GenerationStoreUnreadable { reason: _ } => + match codex_supervised_turn_generation_admission(read: read) { + CodexTurnStartRefusedDuplicateExecution { reason: _ } => true + _ => false + } + _ => false + } +} + +test fn witness_generation_store_path_is_root_slash_bare_name() -> Bool { + codex_supervised_turn_generation_store_path( + evidence_root: "/tmp/gunbc-supervised-evidence" as FilePath, + ) == "/tmp/gunbc-supervised-evidence/codex_supervised_turn_generation" +} + test fn witness_corrupt_generation_store_refuses_prior_read() -> Bool { - let read = codex_supervised_generation_read_from_store( - store_present: true, - read_success: true, - content: "garbage", + let read = codex_supervised_generation_read_from_observation( + o: FilesystemFileRead { + path: "/tmp/gunbc-supervised-evidence/codex_supervised_turn_generation", + content: "garbage", + }, ) match read { GenerationStoreMalformed { content: _ } => @@ -330,10 +440,11 @@ test fn witness_corrupt_generation_store_refuses_prior_read() -> Bool { } test fn witness_negative_generation_store_refuses_prior_read() -> Bool { - let read = codex_supervised_generation_read_from_store( - store_present: true, - read_success: true, - content: "-3", + let read = codex_supervised_generation_read_from_observation( + o: FilesystemFileRead { + path: "/tmp/gunbc-supervised-evidence/codex_supervised_turn_generation", + content: "-3", + }, ) match read { GenerationStoreNegative { value: v } => @@ -347,29 +458,14 @@ test fn witness_negative_generation_store_refuses_prior_read() -> Bool { } test fn witness_whitespace_generation_store_is_malformed_not_absent() -> Bool { - match codex_supervised_generation_read_from_store( - store_present: true, - read_success: true, - content: " ", + match codex_supervised_generation_read_from_observation( + o: FilesystemFileRead { + path: "/tmp/gunbc-supervised-evidence/codex_supervised_turn_generation", + content: " ", + }, ) { GenerationStoreMalformed { content: _ } => true GenerationAbsent => false _ => false } } - -test fn witness_unreadable_generation_store_refuses_prior_read() -> Bool { - let read = codex_supervised_generation_read_from_store( - store_present: true, - read_success: false, - content: "", - ) - match read { - GenerationStoreUnreadable { reason: _ } => - match codex_supervised_turn_generation_admission(read: read) { - CodexTurnStartRefusedDuplicateExecution { reason: _ } => true - _ => false - } - _ => false - } -} diff --git a/dag/test/claim/merge_admission_attempt_witness_test.dag b/dag/test/claim/merge_admission_attempt_witness_test.dag index 368050d4cdb..48b6aab2033 100644 --- a/dag/test/claim/merge_admission_attempt_witness_test.dag +++ b/dag/test/claim/merge_admission_attempt_witness_test.dag @@ -4,7 +4,26 @@ import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } import std.types { NonEmptyStr, CommitSha, String } import extdeps.git.object_store { GitObjectId, git_object_id_eq, git_object_id_wire_hex, git_sha1_object_id } import extdeps.github.checks { Success, Failure } -import tools.merge_admission_walk { merge_admission_fetch_stall_deadline_seconds } +import extdeps.filesystem.filesystem_io { + FilesystemFileObservation, + filesystem_read_outcome, + filesystem_listing_observation, + filesystem_file_observation, +} +import tools.merge_admission_walk { + merge_admission_fetch_stall_deadline_seconds, + TestedSubjectWireRead, + TestedSubjectWireAbsent, + TestedSubjectWireUnobservable, + FloorReceiptWireRead, + FloorReceiptWireAbsent, + FloorReceiptWireUnobservable, + tested_subject_wire_observation_of, + floor_receipt_wire_observation_of, + merge_target_refresh_refusal_label, + RefreshTestedSubjectWireUnreadable, + RefreshFloorReceiptWireUnreadable, +} import gunbc.merge_admission_subject { TestedSubject, WalkAttemptId, @@ -776,3 +795,154 @@ test fn subject_wire_refuses_a_blank_base_commit_line() -> Bool { base_commit: "", )) } + +// ---- THE STAGE WIRE OBSERVATIONS (tools.merge_admission_walk) ---- +// +// read_tested_subject and read_floor_receipt execute Filesystem.List and Filesystem.Read against +// the stage's wire paths; these claims hold the translation that consumes what they reported, +// built over authored channel values through the filesystem observation fold. +// +// THE RED CELLS ARE THE DEFECT AS FOUND. Both readers used to answer the Optional's absent arm on +// a refused read, so a stage receipt that exists and cannot be read reported exactly what a stage +// that never wrote reports. Absence now comes only from a listing that succeeded. +fn stage_wire_observation( + listing_success: Bool, + entries: String, + listing_error: String, + read_success: Bool, + content: String, + read_error: String +) -> FilesystemFileObservation { + filesystem_file_observation( + listing: filesystem_listing_observation( + directory: "/repo/target/merge-admission", + success: listing_success, + entries: entries, + error: listing_error, + ), + name: "tested-subject.txt", + path: "/repo/target/merge-admission/tested-subject.txt", + read: filesystem_read_outcome(content: content, success: read_success, error: read_error) + ) +} + +test fn an_unreadable_but_listed_subject_wire_is_unobservable_not_missing() -> Bool { + match tested_subject_wire_observation_of(o: stage_wire_observation( + listing_success: true, + entries: "tested-subject.txt\n", + listing_error: "", + read_success: false, + content: "", + read_error: "Permission denied (os error 13)" + )) { + TestedSubjectWireUnobservable { cause: c } => + string_contains(s: c, pattern: "Permission denied") + && string_contains( + s: merge_target_refresh_refusal_label(cause: RefreshTestedSubjectWireUnreadable { cause: c }), + pattern: "unreadable", + ) + TestedSubjectWireAbsent(_) => false + TestedSubjectWireRead { decoded: _ } => false + } +} + +test fn an_unlistable_stage_wire_directory_is_unobservable_not_missing() -> Bool { + match tested_subject_wire_observation_of(o: stage_wire_observation( + listing_success: false, + entries: "", + listing_error: "Permission denied (os error 13)", + read_success: false, + content: "", + read_error: "Permission denied (os error 13)" + )) { + TestedSubjectWireUnobservable { cause: _ } => true + TestedSubjectWireAbsent(_) => false + TestedSubjectWireRead { decoded: _ } => false + } +} + +test fn a_subject_wire_absent_from_the_listing_is_the_only_missing_route() -> Bool { + match tested_subject_wire_observation_of(o: stage_wire_observation( + listing_success: true, + entries: "other.txt\n", + listing_error: "", + read_success: false, + content: "", + read_error: "No such file or directory (os error 2)" + )) { + TestedSubjectWireAbsent(_) => true + TestedSubjectWireUnobservable { cause: _ } => false + TestedSubjectWireRead { decoded: _ } => false + } +} + +test fn a_listed_and_decodable_subject_wire_reads() -> Bool { + match tested_subject_wire_observation_of(o: stage_wire_observation( + listing_success: true, + entries: "tested-subject.txt\n", + listing_error: "", + read_success: true, + content: render_tested_subject_wire(subject: subject_fx(attempt: attempt_a(), head: head_sha_fx)), + read_error: "" + )) { + TestedSubjectWireRead { decoded: d } => + match d { + Present { value: subject } => subject.head_sha == head_sha_fx + Absent => false + } + TestedSubjectWireAbsent(_) => false + TestedSubjectWireUnobservable { cause: _ } => false + } +} + +test fn an_unreadable_but_listed_floor_receipt_is_unobservable_not_missing() -> Bool { + match floor_receipt_wire_observation_of(o: filesystem_file_observation( + listing: filesystem_listing_observation( + directory: "/repo/target/merge-admission", + success: true, + entries: "floor-receipt.txt\n", + error: "", + ), + name: "floor-receipt.txt", + path: "/repo/target/merge-admission/floor-receipt.txt", + read: filesystem_read_outcome( + content: "", + success: false, + error: "Permission denied (os error 13)" + ) + )) { + FloorReceiptWireUnobservable { cause: c } => + string_contains( + s: merge_target_refresh_refusal_label(cause: RefreshFloorReceiptWireUnreadable { cause: c }), + pattern: "unreadable", + ) + FloorReceiptWireAbsent(_) => false + FloorReceiptWireRead { decoded: _ } => false + } +} + +test fn a_listed_and_decodable_floor_receipt_reads() -> Bool { + match floor_receipt_wire_observation_of(o: filesystem_file_observation( + listing: filesystem_listing_observation( + directory: "/repo/target/merge-admission", + success: true, + entries: "floor-receipt.txt\n", + error: "", + ), + name: "floor-receipt.txt", + path: "/repo/target/merge-admission/floor-receipt.txt", + read: filesystem_read_outcome( + content: render_receipt_wire_v2(receipt: receipt_fx(attempt: attempt_a(), head: head_sha_fx)), + success: true, + error: "" + ) + )) { + FloorReceiptWireRead { decoded: d } => + match d { + Present { value: receipt } => receipt.tested_head_sha == head_sha_fx + Absent => false + } + FloorReceiptWireAbsent(_) => false + FloorReceiptWireUnobservable { cause: _ } => false + } +} diff --git a/dag/test/claim/nbd_proxy_serve_transport_witness_test.dag b/dag/test/claim/nbd_proxy_serve_transport_witness_test.dag index c21b4e637aa..dbf36c02b52 100644 --- a/dag/test/claim/nbd_proxy_serve_transport_witness_test.dag +++ b/dag/test/claim/nbd_proxy_serve_transport_witness_test.dag @@ -1,5 +1,18 @@ module test.claim.nbd_proxy_serve_transport +import extdeps.filesystem.filesystem_io { + filesystem_read_outcome, + filesystem_listing_observation, + filesystem_file_observation, +} +import gunbc.host_effect_nbd_proxy_serve { + BmcwebSessionTokenObservation, + BmcwebSessionTokenUsable, + BmcwebSessionTokenStartRefused, + bmcweb_session_token_observation_of, + bmcweb_session_token_start_decision, +} + data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly @@ -261,3 +274,114 @@ test fn witness_systemctl_stop_operation_argv_matches_authority() -> Bool { test fn witness_systemctl_is_active_operation_argv_matches_authority() -> Bool { systemctl_is_active_operation_argv_matches_authority(unit: "nbd-proxy-srv3-nbd-proxy-10809-ws" as NonEmptyStr) } + +// ---- THE BMCWEB SESSION TOKEN READ (gunbc.host_effect_nbd_proxy_serve) ---- +// +// The wet reader runs Filesystem.List and Filesystem.Read against the real token path; these +// claims hold the POLICY seam that consumes what they reported. The observations below are built +// through the filesystem observation fold over authored channel values, which is what the wet path +// hands it. What they deliberately do not establish is that the host emits those bytes for /tmp -- +// that is transport coverage the hermetic fold cannot carry, and the fold's own witness +// (test.claim.filesystem_absence_establishment_witness_test) records the same boundary. +// +// THE TWO RED CELLS ARE THE DEFECT AS FOUND. Before the observation fold, a refused read AND an +// unreadable-but-present token both answered Absent, and the unit-start caller reported "BMCWEB +// session token absent" for a file that was there. Both arms now refuse with their cause. +fn token_observation( + listing_success: Bool, + entries: String, + listing_error: String, + read_success: Bool, + content: String, + read_error: String, +) -> BmcwebSessionTokenObservation { + bmcweb_session_token_observation_of(o: filesystem_file_observation( + listing: filesystem_listing_observation( + directory: "/run/bmcweb", + success: listing_success, + entries: entries, + error: listing_error, + ), + name: "srv3_bmcweb_token", + path: "/run/bmcweb/srv3_bmcweb_token", + read: filesystem_read_outcome(content: content, success: read_success, error: read_error), + )) +} + +fn token_decision_reason(o: BmcwebSessionTokenObservation) -> String { + match bmcweb_session_token_start_decision(o: o) { + BmcwebSessionTokenUsable { token: _ } => "usable" + BmcwebSessionTokenStartRefused { reason: why } => why as String + } +} + +test fn an_unreadable_but_listed_token_refuses_instead_of_absent() -> Bool { + string_contains( + s: token_decision_reason(o: token_observation( + listing_success: true, + entries: "srv3_bmcweb_token\nother\n", + listing_error: "", + read_success: false, + content: "", + read_error: "Permission denied (os error 13)", + )), + pattern: "could not be observed", + ) +} + +test fn an_unlistable_token_directory_refuses_instead_of_absent() -> Bool { + string_contains( + s: token_decision_reason(o: token_observation( + listing_success: false, + entries: "", + listing_error: "Permission denied (os error 13)", + read_success: false, + content: "", + read_error: "Permission denied (os error 13)", + )), + pattern: "could not be observed", + ) +} + +// POSITIVE CONTROL, absence arm: the same refused read, over a listing that does not name the +// file, is the only route to "absent" -- the arms are decided by the LISTING, not the read. +test fn a_token_absent_from_the_listing_still_refuses_as_absent() -> Bool { + token_decision_reason(o: token_observation( + listing_success: true, + entries: "other\n", + listing_error: "", + read_success: false, + content: "", + read_error: "No such file or directory (os error 2)", + )) == "BMCWEB session token absent" +} + +test fn a_listed_and_read_token_starts_the_units() -> Bool { + match bmcweb_session_token_start_decision(o: token_observation( + listing_success: true, + entries: "srv3_bmcweb_token\n", + listing_error: "", + read_success: true, + content: "tok-123", + read_error: "", + )) { + BmcwebSessionTokenUsable { token: t } => t as String == "tok-123" + BmcwebSessionTokenStartRefused { reason: _ } => false + } +} + +// The empty content is a third fact and is carried as one: the file exists, was read, and holds +// no token -- a broken materialization, not an absent one. +test fn an_empty_token_file_refuses_as_present_not_absent() -> Bool { + string_contains( + s: token_decision_reason(o: token_observation( + listing_success: true, + entries: "srv3_bmcweb_token\n", + listing_error: "", + read_success: true, + content: "", + read_error: "", + )), + pattern: "holds no token", + ) +} diff --git a/dag/test/claim/opaque_census_declaration_scan_witness_test.dag b/dag/test/claim/opaque_census_declaration_scan_witness_test.dag index 4bf201e5040..df02234ce10 100644 --- a/dag/test/claim/opaque_census_declaration_scan_witness_test.dag +++ b/dag/test/claim/opaque_census_declaration_scan_witness_test.dag @@ -2,9 +2,17 @@ module test.claim.opaque_census_declaration_scan_witness import tools.opaque_realization_census { DeclarationBodyStanding, DeclaredOpaque, DeclaredWithBody, declaration_body_standing_in, + DeclarationSourceUnresolved, DeclarationSourceUnreadable, + DeclarationScanUnresolved, DeclarationScanResolved, + declaration_candidate_scan_then_with, declaration_standing_from_scan, EmittedByThisRun, OpaqueCensusUnestablished, census_compiler_binary_unestablished, census_stage_text } import tools.host_prelude { WitnessBinArtifactNotExecutable, WitnessBinArtifactEmpty } +import std.types { FilePath } +import extdeps.filesystem.filesystem_io { + FilesystemFileAbsent, FilesystemFileRead, FilesystemFileIndeterminate, + FilesystemFileObservationsDisagree, FilesystemFileSubjectRefused, FilesystemEstablishedAbsence, +} import v2.std.optional { Absent, Present } import v2.std.logic { Bool } @@ -30,6 +38,7 @@ fn opaque_census_scan_answers(content: String, name: String) -> String { DeclaredOpaque => "OPAQUE" DeclaredWithBody => "BODY" DeclarationSourceUnresolved { attempted: _ } => "UNRESOLVED" + DeclarationSourceUnreadable { path: _, cause: _ } => "UNREADABLE" } } } @@ -64,6 +73,136 @@ test fn opaque_census_declaration_scan_witnesses() -> Bool { && witness_a_same_line_body_is_still_a_body() } +// THE CANDIDATE FOLD'S POLICY, held over constructed observations. The wet reader is one small +// function (declaration_candidate_observation, per candidate path); everything below constructs the +// transport shapes by hand and steps the SAME fold the wet caller runs, so the suite holds the +// rules -- resolved wins, an established absence keeps the search unresolved, a could-not-look is +// recorded and finally refuses as unreadable -- without a host filesystem. The three reds are +// against the former fold, which folded every failed read into the same terminal arm as an +// established absence. +test fn witness_unlistable_candidate_root_refuses_the_standing_question() -> Bool { + let scan = declaration_candidate_scan_then_with( + acc: DeclarationScanUnresolved { attempted: "dag/x.dag src/v2/x.dag", unobserved: none }, + o: FilesystemFileIndeterminate { + cause: "the directory src/v2 could not be listed, so the absence of x.dag is not established -- permission denied", + }, + name: "X", + path: "src/v2/x.dag", + ) + match declaration_standing_from_scan(scan: scan) { + DeclarationSourceUnreadable { path: p, cause: c } => + p == "src/v2/x.dag" && string_contains(s: c, pattern: "could not be listed") + _ => false + } +} + +test fn witness_refused_candidate_subject_refuses_the_standing_question() -> Bool { + let scan = declaration_candidate_scan_then_with( + acc: DeclarationScanUnresolved { attempted: "dag/x.dag", unobserved: none }, + o: FilesystemFileSubjectRefused { + directory: "dag", + name: "", + cause: "the entry name \"\" is not admissible", + }, + name: "X", + path: "dag/x.dag", + ) + match declaration_standing_from_scan(scan: scan) { + DeclarationSourceUnreadable { path: p, cause: _ } => p == "dag/" + _ => false + } +} + +test fn witness_moved_candidate_subject_refuses_the_standing_question() -> Bool { + let scan = declaration_candidate_scan_then_with( + acc: DeclarationScanUnresolved { attempted: "dag/x.dag", unobserved: none }, + o: FilesystemFileObservationsDisagree { + path: "dag/x.dag", + cause: "no x.dag is listed in dag, and a read of dag/x.dag then succeeded -- the two observations describe different instants and neither is discarded", + }, + name: "X", + path: "dag/x.dag", + ) + match declaration_standing_from_scan(scan: scan) { + DeclarationSourceUnreadable { path: p, cause: _ } => p == "dag/x.dag" + _ => false + } +} + +test fn witness_first_recorded_fault_is_the_one_carried() -> Bool { + let first = declaration_candidate_scan_then_with( + acc: DeclarationScanUnresolved { attempted: "dag/x.dag src/v2/x.dag", unobserved: none }, + o: FilesystemFileIndeterminate { cause: "the directory dag could not be listed -- first fault" }, + name: "X", + path: "dag/x.dag", + ) + let second = declaration_candidate_scan_then_with( + acc: first, + o: FilesystemFileIndeterminate { cause: "the directory src/v2 could not be listed -- second fault" }, + name: "X", + path: "src/v2/x.dag", + ) + match declaration_standing_from_scan(scan: second) { + DeclarationSourceUnreadable { path: p, cause: c } => + p == "dag/x.dag" && string_contains(s: c, pattern: "first fault") + _ => false + } +} + +// POSITIVE CONTROL: an established absence -- a listing that succeeded and did not name the file -- +// is the one shape that still answers unresolved, because that is a location genuinely looked at. +test fn witness_established_candidate_absence_still_answers_unresolved() -> Bool { + let scan = declaration_candidate_scan_then_with( + acc: DeclarationScanUnresolved { attempted: "dag/x.dag", unobserved: none }, + o: FilesystemFileAbsent( + FilesystemEstablishedAbsence { directory: "dag" as FilePath, name: "x.dag" }, + ), + name: "X", + path: "dag/x.dag", + ) + match declaration_standing_from_scan(scan: scan) { + DeclarationSourceUnresolved { attempted: a } => a == "dag/x.dag" + _ => false + } +} + +// POSITIVE CONTROL: a candidate that was actually read and declares the name answers the question +// even though a DIFFERENT candidate spelling could not be looked at -- the fault names another +// path, and the census's happy path must not regress to a refusal. +test fn witness_resolved_candidate_wins_over_a_recorded_fault() -> Bool { + let faulted = declaration_candidate_scan_then_with( + acc: DeclarationScanUnresolved { attempted: "src/v2/x.dag dag/x.dag", unobserved: none }, + o: FilesystemFileIndeterminate { cause: "the directory src/v2 could not be listed -- permission denied" }, + name: "X", + path: "src/v2/x.dag", + ) + let resolved = declaration_candidate_scan_then_with( + acc: faulted, + o: FilesystemFileRead { path: "dag/x.dag", content: "type X = Int\n" }, + name: "X", + path: "dag/x.dag", + ) + match declaration_standing_from_scan(scan: resolved) { + DeclaredWithBody => true + _ => false + } +} + +// POSITIVE CONTROL: a readable candidate that does not declare the name keeps the search going as +// unresolved -- the file was looked at, so this is an absence, not a fault. +test fn witness_readable_candidate_without_the_declaration_stays_unresolved() -> Bool { + let scan = declaration_candidate_scan_then_with( + acc: DeclarationScanUnresolved { attempted: "dag/x.dag", unobserved: none }, + o: FilesystemFileRead { path: "dag/x.dag", content: "type Y = Int\n" }, + name: "X", + path: "dag/x.dag", + ) + match declaration_standing_from_scan(scan: scan) { + DeclarationSourceUnresolved { attempted: a } => a == "dag/x.dag" + _ => false + } +} + // A compiler binary that could not be made Ready is carried into the census's own // OpaqueCensusUnestablished with its bin, path and WitnessBinRefusalReason. The refusal is supplied // (its producer's arms are probed on disk by tools.build_step_transport); two reasons are asserted diff --git a/src/v2/test/claim/workflow/product_receipt_test.dag b/src/v2/test/claim/workflow/product_receipt_test.dag index be0c730d459..0aeb8be4cbe 100644 --- a/src/v2/test/claim/workflow/product_receipt_test.dag +++ b/src/v2/test/claim/workflow/product_receipt_test.dag @@ -29,6 +29,24 @@ import v2.workflow.product_receipt { import v2.std.algebra { Empty, length } import v2.std.logic { Bool } import v2.std.text { String } +import extdeps.filesystem.filesystem_io { + filesystem_read_outcome, + filesystem_listing_observation, + filesystem_file_observation, +} +import v2.workflow.product_receipt { + ManifestUnobservable, + ProducerUnobservable, + ProducerReportedNoArtifact, + ManifestNotProduced, + boundary_refusal_cause_label, +} +import v2.workflow.product_receipt_stage { + ManifestFileObservation, + manifest_file_observation_of, + manifest_boundary1_standing, + manifest_boundary2_consumed, +} // Every fixture below is CONSTRUCTED, never a live run, because this file // tests the receipt ALGEBRA -- the question "does this shape of evidence @@ -247,3 +265,139 @@ test fn repeated_reasons_collapse_into_one_row_and_the_total_is_preserved() -> B ) (length(xs: tally) == 2) && (diagnostic_tally_total(tally: tally) == 3) } + +// ---- THE MANIFEST OBSERVATION (v2.workflow.product_receipt_stage) ---- +// +// The wet stage executes Filesystem.List and Filesystem.Read against the transaction's manifest +// path; these claims hold the boundary decisions that consume what they reported. Observations are +// built through the filesystem observation fold over authored channel values. What they do not +// establish is that the host emits those bytes for a real transaction directory -- that is +// transport coverage outside the hermetic fold. +// +// THE TWO RED CELLS ARE THE DEFECT AS FOUND. Before the observation fold, an unreadable manifest +// answered `ArtifactIdentityAbsent { ProducerReportedNoArtifact }` -- attributing to the producer +// a report it never made -- and boundary 1 read its standing straight off `manifest_read.success`. +fn manifest_observation( + listing_success: Bool, + entries: String, + listing_error: String, + read_success: Bool, + content: String, + read_error: String +) -> ManifestFileObservation { + manifest_file_observation_of(o: filesystem_file_observation( + listing: filesystem_listing_observation( + directory: "/txn/manifest", + success: listing_success, + entries: entries, + error: listing_error, + ), + name: "host_source_root_ingest_manifest.dag", + path: "/txn/manifest/host_source_root_ingest_manifest.dag", + read: filesystem_read_outcome(content: content, success: read_success, error: read_error) + )) +} + +fn boundary1_refusal_cause_text(o: ManifestFileObservation) -> String { + match manifest_boundary1_standing(o: o) { + BoundaryRefused { cause: c } => boundary_refusal_cause_label(cause: c) + _ => "not-refused" + } +} + +// RED: a manifest that is LISTED and cannot be read is neither produced nor absent; it refuses +// with its cause, and the consumed identity is unobservable -- never the producer's report. +test fn an_unreadable_but_listed_manifest_is_unobservable_not_producer_reported() -> Bool { + let o = manifest_observation( + listing_success: true, + entries: "host_source_root_ingest_manifest.dag\n", + listing_error: "", + read_success: false, + content: "", + read_error: "Permission denied (os error 13)" + ) + string_contains(s: boundary1_refusal_cause_text(o: o), pattern: "could not be observed") + && match manifest_boundary2_consumed(o: o) { + ArtifactIdentityAbsent { cause: ProducerUnobservable { cause: c } } => + string_contains(s: c, pattern: "Permission denied") + _ => false + } +} + +// RED, second arm: a manifest directory that cannot be listed establishes nothing. +test fn an_unlistable_manifest_directory_refuses_instead_of_reporting() -> Bool { + string_contains( + s: boundary1_refusal_cause_text(o: manifest_observation( + listing_success: false, + entries: "", + listing_error: "Permission denied (os error 13)", + read_success: false, + content: "", + read_error: "Permission denied (os error 13)" + )), + pattern: "could not be observed", + ) +} + +// RED, third arm: a successful read cannot rescue a listing that does not name the manifest -- +// the two observations describe different instants, and the disagreement refuses. +test fn a_successful_read_does_not_rescue_an_unlisted_manifest() -> Bool { + string_contains( + s: boundary1_refusal_cause_text(o: manifest_observation( + listing_success: true, + entries: "unrelated.txt\n", + listing_error: "", + read_success: true, + content: "manifest-bytes", + read_error: "" + )), + pattern: "could not be observed", + ) +} + +// POSITIVE CONTROL, absence arm: the manifest the listing does not name is the only route to +// ProducerReportedNoArtifact, which the established absence finally justifies. +test fn an_absent_manifest_still_reports_the_producer_none() -> Bool { + let o = manifest_observation( + listing_success: true, + entries: "unrelated.txt\n", + listing_error: "", + read_success: false, + content: "", + read_error: "No such file or directory (os error 2)" + ) + match manifest_boundary1_standing(o: o) { + BoundaryRefused { cause: ManifestNotProduced } => + match manifest_boundary2_consumed(o: o) { + ArtifactIdentityAbsent { cause: ProducerReportedNoArtifact } => true + _ => false + } + _ => false + } +} + +// POSITIVE CONTROL, observed arm: bytes in hand complete boundary 1 and carry a known identity. +test fn an_observed_manifest_completes_boundary_1() -> Bool { + match manifest_boundary1_standing(o: manifest_observation( + listing_success: true, + entries: "host_source_root_ingest_manifest.dag\n", + listing_error: "", + read_success: true, + content: "manifest-bytes", + read_error: "" + )) { + BoundaryCompleted => + match manifest_boundary2_consumed(o: manifest_observation( + listing_success: true, + entries: "host_source_root_ingest_manifest.dag\n", + listing_error: "", + read_success: true, + content: "manifest-bytes", + read_error: "" + )) { + ArtifactIdentityKnown { digest: _, file_count: files } => files == 1 + _ => false + } + _ => false + } +} diff --git a/src/v2/workflow/product_receipt.dag b/src/v2/workflow/product_receipt.dag index d8017db3eb1..040f2d1e72a 100644 --- a/src/v2/workflow/product_receipt.dag +++ b/src/v2/workflow/product_receipt.dag @@ -113,6 +113,7 @@ fn diagnostic_tally_render(tally: List) -> String { type BoundaryRefusalCause = ManifestNotProduced + | ManifestUnobservable { cause: String } | ManifestOverlayNotResolved | ManifestPopulationEmpty | ManifestCoverageIncomplete @@ -135,6 +136,7 @@ type BoundaryStanding type ArtifactIdentityAbsentCause = BoundaryNotReached | ProducerReportedNoArtifact + | ProducerUnobservable { cause: String } // The identity carries a FILE COUNT beside the digest, and that is a field // rather than a caveat in a probe document. Two producers can hand the same @@ -208,6 +210,8 @@ fn product_boundary_label(boundary: ProductBoundary) -> String { fn boundary_refusal_cause_label(cause: BoundaryRefusalCause) -> String { match cause { ManifestNotProduced => "manifest not produced" + ManifestUnobservable { cause: why } => + concat("the manifest could not be observed, so neither produced nor absent is established: ", why) ManifestOverlayNotResolved => "the run resolved the committed stub, not the manifest this transaction produced" ManifestPopulationEmpty => "manifest population empty" ManifestCoverageIncomplete => "manifest coverage incomplete" @@ -256,6 +260,8 @@ fn artifact_identity_label(identity: ArtifactIdentity) -> String { match cause { BoundaryNotReached => "" ProducerReportedNoArtifact => "" + ProducerUnobservable { cause: why } => + concat("")) } } } diff --git a/src/v2/workflow/product_receipt_stage.dag b/src/v2/workflow/product_receipt_stage.dag index 2d9759d34fb..061251b7982 100644 --- a/src/v2/workflow/product_receipt_stage.dag +++ b/src/v2/workflow/product_receipt_stage.dag @@ -1,7 +1,19 @@ module v2.workflow.product_receipt_stage import extdeps.cargo_build -import extdeps.filesystem.filesystem_io { Filesystem } +import extdeps.filesystem.filesystem_io { + Filesystem, + FilesystemEstablishedAbsence, + FilesystemFileObservation, + FilesystemFileAbsent, + FilesystemFileRead, + FilesystemFileIndeterminate, + FilesystemFileObservationsDisagree, + FilesystemFileSubjectRefused, + filesystem_read_outcome, + filesystem_listing_observation, + filesystem_file_observation, +} import extdeps.git import extdeps.git.inspect import extdeps.gunbc @@ -76,10 +88,12 @@ import v2.workflow.product_receipt { ManifestPopulationAdmitted, ManifestPopulationEmpty, ManifestPopulationPartial, + ManifestUnobservable, AdmissionReasonUnrecognized, ManifestSourceReadFailed, PopulationDigestMismatch, ProducerReportedNoArtifact, + ProducerUnobservable, ProductBoundary, ProductReceipt, RefsHashVerified, @@ -165,6 +179,92 @@ fn stage_admission_cause(reason: Symbol) -> BoundaryRefusalCause { } } +// THE MANIFEST IS OBSERVED THROUGH THE FILESYSTEM OBSERVATION FOLD, AND ABSENCE IS ESTABLISHED BY +// THE LISTING, NEVER BY THE READ. Boundary 1 (the host derives the manifest) used to be decided by +// `manifest_read.success` alone, and an unreadable manifest answered +// `ArtifactIdentityAbsent { ProducerReportedNoArtifact }` -- attributing to the producer a report +// it never made. A read that refused cannot say whether the manifest was there; only a listing +// that succeeded and did not name it can. The three worlds now travel as three arms: observed +// (bytes in hand), absent (established by the listing), unobservable (a typed refusal carrying the +// cause). `ManifestSourceReadFailed` is deliberately NOT reused here: it is the closure-admission +// ladder's cause for ITS source reads, and one name with two meanings is the fork section 3 +// forbids. +type ManifestFileObservation + = ManifestObserved { content: String } + | ManifestAbsent(FilesystemEstablishedAbsence) + | ManifestUnobserved { cause: String } + +fn manifest_file_observation_of(o: FilesystemFileObservation) -> ManifestFileObservation { + match o { + FilesystemFileRead { path: _, content: c } => ManifestObserved { content: c } + FilesystemFileAbsent(established) => ManifestAbsent(established) + FilesystemFileIndeterminate { cause: c } => ManifestUnobserved { cause: c } + FilesystemFileObservationsDisagree { path: _, cause: c } => ManifestUnobserved { cause: c } + FilesystemFileSubjectRefused { directory: _, name: _, cause: c } => ManifestUnobserved { cause: c } + } +} + +// THE BOUNDARY DECISIONS ARE TOTAL OVER THE OBSERVATION, which is what makes them claimable: the +// wet stage executes the listing and the read and then consumes these verdicts verbatim, so the +// claim suite can hold the policy (observed completes boundary 1 and feeds boundary 2's ladder; an +// established absence refuses boundary 1 and 2 as not produced; an unobserved manifest refuses +// both with its cause and is never attributed to the producer) without running a transaction. +fn manifest_boundary1_standing(o: ManifestFileObservation) -> BoundaryStanding { + match o { + ManifestObserved { content: _ } => BoundaryCompleted + ManifestAbsent(_) => BoundaryRefused { cause: ManifestNotProduced } + ManifestUnobserved { cause: c } => BoundaryRefused { cause: ManifestUnobservable { cause: c } } + } +} + +fn manifest_boundary2_consumed(o: ManifestFileObservation) -> ArtifactIdentity { + match o { + ManifestObserved { content: c } => product_artifact_identity(value: c, file_count: 1) + ManifestAbsent(_) => ArtifactIdentityAbsent { cause: ProducerReportedNoArtifact } + ManifestUnobserved { cause: c } => + ArtifactIdentityAbsent { cause: ProducerUnobservable { cause: c } } + } +} + +fn manifest_overlay_resolved(o: ManifestFileObservation) -> Bool { + match o { + ManifestObserved { content: c } => + host_source_root_ingest_content_hash != "" + && string_contains(s: c, pattern: host_source_root_ingest_content_hash) + _ => false + } +} + +fn observed_manifest_b2_standing( + overlay_resolved: Bool, + admitted: Bool, + admission_cause: BoundaryRefusalCause, + consumed: ArtifactIdentity, + population_digest: ArtifactIdentity +) -> BoundaryObservation { + if !overlay_resolved { + stage_refused( + boundary: ManifestPopulationAdmitted, + cause: ManifestOverlayNotResolved, + consumed: consumed + ) + } else { + if admitted || stage_cause_belongs_to_read(cause: admission_cause) { + stage_completed( + boundary: ManifestPopulationAdmitted, + consumed: consumed, + produced: population_digest + ) + } else { + stage_refused( + boundary: ManifestPopulationAdmitted, + cause: admission_cause, + consumed: consumed + ) + } + } +} + // Boundary 2 owns the population checks and boundary 3 owns the read. The // admission ladder short-circuits, so a refusal on a boundary-2 cause leaves // boundary 3 NotExercised -- which is the honest answer, not a failure. @@ -172,6 +272,7 @@ fn stage_cause_belongs_to_read(cause: BoundaryRefusalCause) -> Bool { match cause { ManifestSourceReadFailed => true IngestRowShortfall => true + ManifestUnobservable { cause: _ } => false AdmissionReasonUnrecognized { reason: _ } => false ManifestNotProduced => false ManifestOverlayNotResolved => false @@ -494,16 +595,37 @@ fn run_product_receipt_stage(txn: String, manifest_identity: String, entry: Stri let b1_produced = stage_identity_from_hex(hex: manifest_identity, file_count: 1) - let manifest_read = Filesystem.Read(path: manifest_path) - let b2_consumed = if manifest_read.success { - product_artifact_identity(value: manifest_read.content, file_count: 1) - } else { - ArtifactIdentityAbsent { cause: ProducerReportedNoArtifact } + // ONE OBSERVATION, THREE WORLDS. The listing establishes what the read cannot: a manifest that + // was never written is ABSENT (the producer's transaction holds no manifest, which is what + // `ProducerReportedNoArtifact` may finally assert); a manifest that is there and cannot be read + // is UNOBSERVED and refuses with the cause; only bytes in hand are OBSERVED. + let manifest_parts = split(s: manifest_path, delimiter: "/") + let manifest_name = match manifest_parts.last() { + Present { value: value } => value + Absent => "" } + let manifest_directory = join(manifest_parts.take(n: length(manifest_parts) - 1), "/") + let manifest_listing = Filesystem.List(path: manifest_directory) + let manifest_read = Filesystem.Read(path: manifest_path) + let manifest_observation = manifest_file_observation_of(o: filesystem_file_observation( + listing: filesystem_listing_observation( + directory: manifest_directory, + success: manifest_listing.success, + entries: manifest_listing.entries, + error: manifest_listing.error, + ), + name: manifest_name, + path: manifest_path, + read: filesystem_read_outcome( + content: manifest_read.content, + success: manifest_read.success, + error: manifest_read.error + ), + )) - let overlay_resolved = manifest_read.success - && host_source_root_ingest_content_hash != "" - && string_contains(s: manifest_read.content, pattern: host_source_root_ingest_content_hash) + let b2_consumed = manifest_boundary2_consumed(o: manifest_observation) + + let overlay_resolved = manifest_overlay_resolved(o: manifest_observation) let admission = closure_emit_population_admission( refs: host_source_root_closure_refs, @@ -521,34 +643,27 @@ fn run_product_receipt_stage(txn: String, manifest_identity: String, entry: Stri let population_digest = stage_population_digest_identity() - let b2 = if !manifest_read.success { - stage_refused( - boundary: ManifestPopulationAdmitted, - cause: ManifestNotProduced, - consumed: b2_consumed - ) - } else { - if !overlay_resolved { + let b2 = match manifest_observation { + ManifestAbsent(_) => stage_refused( boundary: ManifestPopulationAdmitted, - cause: ManifestOverlayNotResolved, + cause: ManifestNotProduced, consumed: b2_consumed ) - } else { - if admitted || stage_cause_belongs_to_read(cause: admission_cause) { - stage_completed( - boundary: ManifestPopulationAdmitted, - consumed: b2_consumed, - produced: population_digest - ) - } else { - stage_refused( - boundary: ManifestPopulationAdmitted, - cause: admission_cause, - consumed: b2_consumed - ) - } - } + ManifestUnobserved { cause: _ } => + stage_refused( + boundary: ManifestPopulationAdmitted, + cause: ManifestUnobservable { cause: manifest_unobserved_cause }, + consumed: b2_consumed + ) + ManifestObserved { content: _ } => + observed_manifest_b2_standing( + overlay_resolved: overlay_resolved, + admitted: admitted, + admission_cause: admission_cause, + consumed: b2_consumed, + population_digest: population_digest + ) } let b2_ok = match b2.standing { @@ -622,9 +737,7 @@ fn run_product_receipt_stage(txn: String, manifest_identity: String, entry: Stri observations: [ BoundaryObservation { boundary: HostDerivesManifest, - standing: if manifest_read.success { BoundaryCompleted } else { - BoundaryRefused { cause: ManifestNotProduced } - }, + standing: manifest_boundary1_standing(o: manifest_observation), consumed: ArtifactIdentityAbsent { cause: BoundaryNotReached }, produced: b1_produced }, From ba273f07ab1d23e0c9da02f3cca76cf75e1bb8eb Mon Sep 17 00:00:00 2001 From: deep-owl-19 Date: Fri, 2 Oct 2026 09:36:28 +0000 Subject: [PATCH 02/11] nbd proxy witness: import srv3_nbd_proxy_lease_key explicitly The transport witness file had no imports before this branch, so its bare-provider channel was on and srv3_nbd_proxy_lease_key was pulled implicitly. Adding the filesystem_io and host_effect_nbd_proxy_serve imports for the absence-establishment conversion switched the file to imported mode, where every provider name must be pulled by name; the required floor refused the now-unrostered lease key. Import it from gunbc.srv3_nbd_proxy_serve_intent as the gate prescribes. --- dag/test/claim/nbd_proxy_serve_transport_witness_test.dag | 3 +++ 1 file changed, 3 insertions(+) diff --git a/dag/test/claim/nbd_proxy_serve_transport_witness_test.dag b/dag/test/claim/nbd_proxy_serve_transport_witness_test.dag index dbf36c02b52..ef6fbaebdce 100644 --- a/dag/test/claim/nbd_proxy_serve_transport_witness_test.dag +++ b/dag/test/claim/nbd_proxy_serve_transport_witness_test.dag @@ -12,6 +12,9 @@ import gunbc.host_effect_nbd_proxy_serve { bmcweb_session_token_observation_of, bmcweb_session_token_start_decision, } +import gunbc.srv3_nbd_proxy_serve_intent { + srv3_nbd_proxy_lease_key, +} data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly From 669548dabfd3c35a866a534ad31efef3b14b448a Mon Sep 17 00:00:00 2001 From: deep-owl-19 Date: Fri, 2 Oct 2026 10:07:54 +0000 Subject: [PATCH 03/11] lift in-body source annotations to module-item grain The v2 Rust emitter models source annotations only at module-item grain: the four-line observation note inside run_product_receipt_stage and the three-line coproduct note inside emitted_tree_read_then each produced an EmissionRefused hard diagnostic (7 total) in the self-host compile. Both notes move above the declaration they describe, with the census note reworded to state the fold law it documents. --- dag/gunbc/instruments/opaque_realization_census.dag | 6 +++--- src/v2/workflow/product_receipt_stage.dag | 8 ++++---- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/dag/gunbc/instruments/opaque_realization_census.dag b/dag/gunbc/instruments/opaque_realization_census.dag index 28ef90c1d46..d7240fea918 100644 --- a/dag/gunbc/instruments/opaque_realization_census.dag +++ b/dag/gunbc/instruments/opaque_realization_census.dag @@ -881,13 +881,13 @@ type EmittedTreeRead = EmittedTreeFiles { files: List } | EmittedTreeUnreadable { cause: String } +// THE FOLD'S READ IS THE INTERFACE'S COPRODUCT, NOT A BRANCH ON `success`. The read's scalar +// channels are folded through filesystem_read_outcome rather than branched on directly, so this +// site consumes the modeled result like every converted consumer of the transport. fn emitted_tree_read_then(acc: EmittedTreeRead, path: String) -> EmittedTreeRead { match acc { EmittedTreeUnreadable { cause: c } => EmittedTreeUnreadable { cause: c } EmittedTreeFiles { files: so_far } => - // The read's scalar channels are folded through the interface's own coproduct - // (filesystem_read_outcome) rather than branched on `success` directly, so this site consumes - // the modeled result like every converted consumer of the transport. let read = Filesystem.Read(path: path) match filesystem_read_outcome( content: read.content, diff --git a/src/v2/workflow/product_receipt_stage.dag b/src/v2/workflow/product_receipt_stage.dag index 061251b7982..72be2fe0e19 100644 --- a/src/v2/workflow/product_receipt_stage.dag +++ b/src/v2/workflow/product_receipt_stage.dag @@ -588,6 +588,10 @@ fn product_receipt_tail( } } +// ONE OBSERVATION, THREE WORLDS. The listing establishes what the read cannot: a manifest that +// was never written is ABSENT (the producer's transaction holds no manifest, which is what +// `ProducerReportedNoArtifact` may finally assert); a manifest that is there and cannot be read +// is UNOBSERVED and refuses with the cause; only bytes in hand are OBSERVED. fn run_product_receipt_stage(txn: String, manifest_identity: String, entry: String) -> ProcessExit { let manifest_path = concat(txn, product_receipt_stage_manifest_rel) let candidate_dir = concat(txn, product_receipt_stage_candidate_rel) @@ -595,10 +599,6 @@ fn run_product_receipt_stage(txn: String, manifest_identity: String, entry: Stri let b1_produced = stage_identity_from_hex(hex: manifest_identity, file_count: 1) - // ONE OBSERVATION, THREE WORLDS. The listing establishes what the read cannot: a manifest that - // was never written is ABSENT (the producer's transaction holds no manifest, which is what - // `ProducerReportedNoArtifact` may finally assert); a manifest that is there and cannot be read - // is UNOBSERVED and refuses with the cause; only bytes in hand are OBSERVED. let manifest_parts = split(s: manifest_path, delimiter: "/") let manifest_name = match manifest_parts.last() { Present { value: value } => value From a987d19c4b5572419726c8e1e5d95dac9a6bf7b8 Mon Sep 17 00:00:00 2001 From: deep-owl-19 Date: Fri, 2 Oct 2026 11:17:00 +0000 Subject: [PATCH 04/11] witness claims: mint established absence, never write it FilesystemEstablishedAbsence is sole_constructor -- constructible only inside the interface module -- so the three claim sites that wrote the record literal (codex turn x2, census x1) are repaired to DERIVE the absence through the modeled route: filesystem_listing_observation with success and an entry list that omits the name, folded through filesystem_file_observation, matched as FilesystemFileAbsent(a). The same route the wet reader takes, which is the point of the mint. product_receipt_stage: the ManifestUnobserved arm referenced manifest_unobserved_cause, a variable that was never bound; the arm now binds the cause it matches on. --- .../codex_supervised_turn_witness_test.dag | 71 ++++++++++++++----- ...e_census_declaration_scan_witness_test.dag | 36 +++++++--- src/v2/workflow/product_receipt_stage.dag | 4 +- 3 files changed, 81 insertions(+), 30 deletions(-) diff --git a/dag/test/claim/codex_supervised_turn_witness_test.dag b/dag/test/claim/codex_supervised_turn_witness_test.dag index 0e08cce3c66..90aa09d84d0 100644 --- a/dag/test/claim/codex_supervised_turn_witness_test.dag +++ b/dag/test/claim/codex_supervised_turn_witness_test.dag @@ -57,12 +57,14 @@ import std.temporal_effect { } import extdeps.filesystem.filesystem_io { - FilesystemEstablishedAbsence, FilesystemFileAbsent, FilesystemFileRead, FilesystemFileIndeterminate, FilesystemFileObservationsDisagree, FilesystemFileSubjectRefused, + filesystem_listing_observation, + filesystem_file_observation, + filesystem_read_outcome, } data witness_note: String = "Hermetic witnesses for the supervised-runner slice: std.temporal_effect HeldLease fences one WorkerTurn attempt; thread idle without a runner terminal receipt refuses turn/start (continuity receipt trap); busy thread refuses until the runner writes a receipt; parse_supervised_turn_stdout correlates thread/start and turn/start ids and turn/completed notifications into a terminal receipt with client_command_id." @@ -321,30 +323,65 @@ test fn witness_nonzero_exit_without_turn_start_is_not_observed() -> Bool { // could-not-look shapes that now refuse with their cause. Established absence -- a listing that // succeeded and did not name the store -- is the only Absent route, and it still admits. test fn witness_missing_generation_store_reads_as_zero() -> Bool { - match codex_supervised_generation_read_from_observation( - o: FilesystemFileAbsent( - FilesystemEstablishedAbsence { - directory: "/tmp/gunbc-supervised-evidence" as FilePath, - name: codex_supervised_turn_generation_file_name, - }, + // The established absence is MINTED, never written: FilesystemEstablishedAbsence is + // sole_constructor and constructible only inside the interface module, so the fixture derives + // the observation from a listed directory whose entries omit the store name -- the same + // modeled route the wet reader takes. + let listing = filesystem_listing_observation( + directory: "/tmp/gunbc-supervised-evidence", + success: true, + entries: "", + error: "", + ) + match filesystem_file_observation( + listing: listing, + name: codex_supervised_turn_generation_file_name, + path: codex_supervised_turn_generation_store_path( + evidence_root: "/tmp/gunbc-supervised-evidence" as FilePath, + ), + read: filesystem_read_outcome( + content: "", + success: false, + error: "not read: the listing did not name the entry", ), ) { - GenerationAbsent => true + FilesystemFileAbsent(a) => + match codex_supervised_generation_read_from_observation(o: FilesystemFileAbsent(a)) { + GenerationAbsent => true + _ => false + } _ => false } } test fn witness_established_generation_absence_admits_supervised_turn_start() -> Bool { - let read = codex_supervised_generation_read_from_observation( - o: FilesystemFileAbsent( - FilesystemEstablishedAbsence { - directory: "/tmp/gunbc-supervised-evidence" as FilePath, - name: codex_supervised_turn_generation_file_name, - }, - ), + // MINTED, never written: the absence comes from a listed directory whose entries omit the + // store name, the only route the sole_constructor carrier authorizes. + let listing = filesystem_listing_observation( + directory: "/tmp/gunbc-supervised-evidence", + success: true, + entries: "", + error: "", ) - match codex_supervised_turn_generation_admission(read: read) { - CodexTurnStartAdmitted => true + match filesystem_file_observation( + listing: listing, + name: codex_supervised_turn_generation_file_name, + path: codex_supervised_turn_generation_store_path( + evidence_root: "/tmp/gunbc-supervised-evidence" as FilePath, + ), + read: filesystem_read_outcome( + content: "", + success: false, + error: "not read: the listing did not name the entry", + ), + ) { + FilesystemFileAbsent(a) => { + let read = codex_supervised_generation_read_from_observation(o: FilesystemFileAbsent(a)) + match codex_supervised_turn_generation_admission(read: read) { + CodexTurnStartAdmitted => true + _ => false + } + } _ => false } } diff --git a/dag/test/claim/opaque_census_declaration_scan_witness_test.dag b/dag/test/claim/opaque_census_declaration_scan_witness_test.dag index df02234ce10..a5946657818 100644 --- a/dag/test/claim/opaque_census_declaration_scan_witness_test.dag +++ b/dag/test/claim/opaque_census_declaration_scan_witness_test.dag @@ -8,10 +8,10 @@ import tools.opaque_realization_census { EmittedByThisRun, OpaqueCensusUnestablished, census_compiler_binary_unestablished, census_stage_text } import tools.host_prelude { WitnessBinArtifactNotExecutable, WitnessBinArtifactEmpty } -import std.types { FilePath } import extdeps.filesystem.filesystem_io { FilesystemFileAbsent, FilesystemFileRead, FilesystemFileIndeterminate, - FilesystemFileObservationsDisagree, FilesystemFileSubjectRefused, FilesystemEstablishedAbsence, + FilesystemFileObservationsDisagree, FilesystemFileSubjectRefused, + filesystem_listing_observation, filesystem_file_observation, filesystem_read_outcome, } import v2.std.optional { Absent, Present } import v2.std.logic { Bool } @@ -152,16 +152,30 @@ test fn witness_first_recorded_fault_is_the_one_carried() -> Bool { // POSITIVE CONTROL: an established absence -- a listing that succeeded and did not name the file -- // is the one shape that still answers unresolved, because that is a location genuinely looked at. test fn witness_established_candidate_absence_still_answers_unresolved() -> Bool { - let scan = declaration_candidate_scan_then_with( - acc: DeclarationScanUnresolved { attempted: "dag/x.dag", unobserved: none }, - o: FilesystemFileAbsent( - FilesystemEstablishedAbsence { directory: "dag" as FilePath, name: "x.dag" }, - ), - name: "X", + // The established absence is MINTED, never written: FilesystemEstablishedAbsence is + // sole_constructor and constructible only inside the interface module, so the fixture derives + // the observation from a listed directory whose entries omit the candidate's name. + let listing = filesystem_listing_observation(directory: "dag", success: true, entries: "", error: "") + match filesystem_file_observation( + listing: listing, + name: "x.dag", path: "dag/x.dag", - ) - match declaration_standing_from_scan(scan: scan) { - DeclarationSourceUnresolved { attempted: a } => a == "dag/x.dag" + read: filesystem_read_outcome( + content: "", + success: false, + error: "not read: the listing did not name the entry", + ), + ) { + FilesystemFileAbsent(a) => + match declaration_candidate_scan_then_with( + acc: DeclarationScanUnresolved { attempted: "dag/x.dag", unobserved: none }, + o: FilesystemFileAbsent(a), + name: "X", + path: "dag/x.dag", + ) { + DeclarationSourceUnresolved { attempted: att } => att == "dag/x.dag" + _ => false + } _ => false } } diff --git a/src/v2/workflow/product_receipt_stage.dag b/src/v2/workflow/product_receipt_stage.dag index 72be2fe0e19..6b522a98be9 100644 --- a/src/v2/workflow/product_receipt_stage.dag +++ b/src/v2/workflow/product_receipt_stage.dag @@ -650,10 +650,10 @@ fn run_product_receipt_stage(txn: String, manifest_identity: String, entry: Stri cause: ManifestNotProduced, consumed: b2_consumed ) - ManifestUnobserved { cause: _ } => + ManifestUnobserved { cause: c } => stage_refused( boundary: ManifestPopulationAdmitted, - cause: ManifestUnobservable { cause: manifest_unobserved_cause }, + cause: ManifestUnobservable { cause: c }, consumed: b2_consumed ) ManifestObserved { content: _ } => From a997c5fb487f7554098bf0b5f99e474ab1a2123f Mon Sep 17 00:00:00 2001 From: deep-owl-19 Date: Fri, 2 Oct 2026 11:35:53 +0000 Subject: [PATCH 05/11] lift the mint notes above their test declarations Same module-item-grain rule as the previous repair, applied to the comments the mint rewrite itself placed inside the claim bodies: the emitter compiles the whole corpus, so an annotation inside any .dag declaration body refuses emission. The notes move above the test fns they describe. --- .../claim/codex_supervised_turn_witness_test.dag | 12 ++++++------ .../opaque_census_declaration_scan_witness_test.dag | 6 +++--- 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/dag/test/claim/codex_supervised_turn_witness_test.dag b/dag/test/claim/codex_supervised_turn_witness_test.dag index 90aa09d84d0..80a987721ac 100644 --- a/dag/test/claim/codex_supervised_turn_witness_test.dag +++ b/dag/test/claim/codex_supervised_turn_witness_test.dag @@ -322,11 +322,11 @@ test fn witness_nonzero_exit_without_turn_start_is_not_observed() -> Bool { // unlistable evidence directory, an inadmissible store name, and a listing/read disagreement are // could-not-look shapes that now refuse with their cause. Established absence -- a listing that // succeeded and did not name the store -- is the only Absent route, and it still admits. +// The established absence is MINTED, never written: FilesystemEstablishedAbsence is +// sole_constructor and constructible only inside the interface module, so the fixture derives +// the observation from a listed directory whose entries omit the store name -- the same +// modeled route the wet reader takes. test fn witness_missing_generation_store_reads_as_zero() -> Bool { - // The established absence is MINTED, never written: FilesystemEstablishedAbsence is - // sole_constructor and constructible only inside the interface module, so the fixture derives - // the observation from a listed directory whose entries omit the store name -- the same - // modeled route the wet reader takes. let listing = filesystem_listing_observation( directory: "/tmp/gunbc-supervised-evidence", success: true, @@ -354,9 +354,9 @@ test fn witness_missing_generation_store_reads_as_zero() -> Bool { } } +// MINTED, never written: the absence comes from a listed directory whose entries omit the +// store name, the only route the sole_constructor carrier authorizes. test fn witness_established_generation_absence_admits_supervised_turn_start() -> Bool { - // MINTED, never written: the absence comes from a listed directory whose entries omit the - // store name, the only route the sole_constructor carrier authorizes. let listing = filesystem_listing_observation( directory: "/tmp/gunbc-supervised-evidence", success: true, diff --git a/dag/test/claim/opaque_census_declaration_scan_witness_test.dag b/dag/test/claim/opaque_census_declaration_scan_witness_test.dag index a5946657818..c5317810982 100644 --- a/dag/test/claim/opaque_census_declaration_scan_witness_test.dag +++ b/dag/test/claim/opaque_census_declaration_scan_witness_test.dag @@ -151,10 +151,10 @@ test fn witness_first_recorded_fault_is_the_one_carried() -> Bool { // POSITIVE CONTROL: an established absence -- a listing that succeeded and did not name the file -- // is the one shape that still answers unresolved, because that is a location genuinely looked at. +// The established absence is MINTED, never written: FilesystemEstablishedAbsence is +// sole_constructor and constructible only inside the interface module, so the fixture derives +// the observation from a listed directory whose entries omit the candidate's name. test fn witness_established_candidate_absence_still_answers_unresolved() -> Bool { - // The established absence is MINTED, never written: FilesystemEstablishedAbsence is - // sole_constructor and constructible only inside the interface module, so the fixture derives - // the observation from a listed directory whose entries omit the candidate's name. let listing = filesystem_listing_observation(directory: "dag", success: true, entries: "", error: "") match filesystem_file_observation( listing: listing, From c527aeac2c20f69ad6dfe84e2ac5e8cbb4ba62bd Mon Sep 17 00:00:00 2001 From: deep-owl-19 Date: Fri, 2 Oct 2026 12:02:37 +0000 Subject: [PATCH 06/11] census witness: match the scan carrier's own arm The established-absence control matched DeclarationSourceUnresolved -- the STANDING decode's arm -- against the DeclarationCandidateScan the fold returns, whose unresolved arm is DeclarationScanUnresolved. --- dag/test/claim/opaque_census_declaration_scan_witness_test.dag | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/dag/test/claim/opaque_census_declaration_scan_witness_test.dag b/dag/test/claim/opaque_census_declaration_scan_witness_test.dag index c5317810982..dc98db39352 100644 --- a/dag/test/claim/opaque_census_declaration_scan_witness_test.dag +++ b/dag/test/claim/opaque_census_declaration_scan_witness_test.dag @@ -173,7 +173,7 @@ test fn witness_established_candidate_absence_still_answers_unresolved() -> Bool name: "X", path: "dag/x.dag", ) { - DeclarationSourceUnresolved { attempted: att } => att == "dag/x.dag" + DeclarationScanUnresolved { attempted: att, unobserved: _ } => att == "dag/x.dag" _ => false } _ => false From 420f15bd34b3a0b55944578f418f7426d1b2831b Mon Sep 17 00:00:00 2001 From: deep-owl-19 Date: Fri, 2 Oct 2026 15:33:25 +0000 Subject: [PATCH 07/11] Address review 74161: restore the absence row, total the two wildcards, own the observe-a-file composition once Finding 1: filesystem_absence_establishment_adoption_standing was deleted when its roster emptied, but the row's own NEXT-RUNG TRIGGER ties deletion to the capability (raw List/Read projections ceasing to be reachable outside filesystem_io's folds), not to an empty roster. Restored with an empty roster, the same trigger, and the three in-module comment citations re-grafted now that the target resolves again. Verified against the six identities the row carried on 6305a5174c: five converted by this PR, observe_cap_members_wet already converted on main. CI blocker (NonFoldResidueRosterDiverged unrostered=2): manifest_overlay_resolved now matches all three ManifestFileObservation arms, and merge_target_refresh enumerates all six MergeAdmissionVerdict arms with identical semantics instead of a wildcard over the closed coproduct. Finding 2: the list-directory/read-named-entry/match composition was spelled verbatim in four wet readers. It is now owned once, in gunbc.filesystem_file_observe filesystem_file_observation_of_path, called by gunbc.codex_supervised_turn, gunbc.host_effect_nbd_proxy_serve, tools.merge_admission_walk, and tools.opaque_realization_census. The home is deliberately NOT extdeps.filesystem.filesystem_io, which is pure over outcomes the caller already obtained by its own annotation; the helper is the wet side of that boundary, which narrows the raw-call population without retiring the row's trigger. --- dag/extdeps/filesystem/filesystem_io.dag | 11 ++-- dag/gunbc/codex_supervised_turn.dag | 24 +-------- dag/gunbc/filesystem_file_observe.dag | 50 +++++++++++++++++++ .../host/host_effect_nbd_proxy_serve.dag | 26 +--------- .../instruments/merge_admission_walk.dag | 36 +++---------- .../instruments/opaque_realization_census.dag | 37 ++++---------- ...e_census_declaration_scan_witness_test.dag | 5 +- src/v2/workflow/product_receipt_stage.dag | 3 +- 8 files changed, 83 insertions(+), 109 deletions(-) create mode 100644 dag/gunbc/filesystem_file_observe.dag diff --git a/dag/extdeps/filesystem/filesystem_io.dag b/dag/extdeps/filesystem/filesystem_io.dag index f6c64f0a85f..be27c3a150c 100644 --- a/dag/extdeps/filesystem/filesystem_io.dag +++ b/dag/extdeps/filesystem/filesystem_io.dag @@ -159,6 +159,8 @@ fn filesystem_create_new( data filesystem_read_outcome_adoption_standing: String ="RUNG: mitigatable. filesystem_read_outcome provides the single modeled fold from Filesystem.Read's scalar transport observation into FilesystemReadSucceeded | FilesystemReadRefused, but nothing forces callers through it. gunbc.ci_yaml_validate is the first converted consumer and preserves read refusal separately from YAML parse refusal. The raw operation remains directly consumed elsewhere, so content+success+error nonsense combinations remain writable at those sites. SUBJECT: an unconverted consumption site is a Filesystem Read call whose bound result has any success, error, or content projection outside the three arguments of filesystem_read_outcome. The call and those three projections remain after conversion because they supply the fold; adoption changes where they are consumed, not whether they exist. BASELINE measured on origin/main b21b710d5378387ae0c841f07323292c5d72faba: 92 unconverted consumption sites across 48 .dag files. REMAINDER after the first conversion: 91 unconverted consumption sites across 47 files. RE-MEASURED 2026-10-02 on session/deep-owl-19 (origin/main d85c2d8fadecee55c2a9ca5b3c536d159b8f86e6 plus the six absence-establishment conversions and the opaque_realization_census emitted-tree fold this branch carries), same subject, the instrument implemented as spelled here with two mechanical precisions: a projection counts as an argument of the fold iff it sits inside the paren span of a filesystem_read_outcome( call, so multi-line calls classify correctly, and comment lines are not consumption sites -- the same rule that keeps this declaration out of its own count. CALIBRATION: the same implementation reproduces 90 unconverted sites across 46 files at b21b710d against the 92/48 the baseline sentence above records; the difference is filesystem_exact_read sites, which the literal reading classifies unconverted -- that is the sibling modeled fold carrying error_kind, not this fold. MEASURED: 205 unconverted consumption sites across 103 .dag files, with 28 bindings converted and 9 bindings carrying no projection at all; the corpus grew 472 to 7392 tracked .dag files since the baseline head, so the population grew in absolute terms while adoption improved in proportion, and 39 of the 205 are dag/test/claim fixtures. RE-DERIVATION: enumerate Filesystem Read assignment calls in tracked .dag source, excluding this adoption-standing data declaration so the instrument cannot count its own prose; for each bound result, classify it converted only when every success, error, and content projection is an argument of filesystem_read_outcome, otherwise classify it unconverted; count unconverted rows and distinct paths. NEXT-RUNG TRIGGER: the unconverted population reaches zero -- every Filesystem Read result projection occurs only as an argument to filesystem_read_outcome. The compiler-only filesystem_read intrinsic is a separate replacement migration and is not part of this population or this fold." +data filesystem_absence_establishment_adoption_standing: String = "RUNG: structurally guaranteed for the consumers that route through filesystem_file_observation, on the source-to-.dag acceptance path only, and MITIGATABLE NOWHERE ELSE -- the raw Filesystem.Read and Filesystem.List operations stay callable, so a module that has not adopted the carrier can still write the conflation. This row states the unconverted population at identity grain rather than as a count, because a count is not a plan and a one-sided ratchet over a number measured on the current tree is the oracle section 5 rejects. SUBJECT: a site that concludes ABSENCE, NOT-PRESENT or a dropped element from a FAILED read or a FAILED boolean path test, rather than from a listing that succeeded. It is not every Filesystem.Read consumer -- most read a file they already know exists, and those are the separate filesystem_read_outcome adoption population above. ENUMERATED SITES, each one read rather than pattern-matched: the roster is EMPTY as of this row's restoration. The six identities the row carried on origin/main 6305a5174c all route through the carrier now -- gunbc.host_effect_nbd_proxy_serve host_effect_nbd_proxy_serve_read_session_token, v2.workflow.product_receipt_stage run_product_receipt_stage, tools.merge_admission_walk read_tested_subject and read_floor_receipt, gunbc.codex_supervised_turn codex_supervised_turn_generation_observation, and tools.opaque_realization_census declaration_body_standing converted by PR 12982, each preserving could-not-look as its own typed refusal rather than an absence, and gunbc.fleet_converge_plan_cli observe_cap_members_wet already converted on main -- so a could-not-look at any of them can no longer masquerade as an established absence. THE ROW STAYS NONE THE LESS, and an empty roster is not a deleted row: the raw operations remain callable outside this module, so the class shape can be re-spelled at a new site at any time, and what the row guards is the CLASS, not its former members. A site of this shape found anywhere is a defect to repair by adoption, not a row to add. The mistake this restoration repairs was deleting the row because its enumeration emptied rather than because the trigger below expired, which is exactly the failure the NEXT-RUNG TRIGGER paragraph exists to prevent. WHAT IS DELIBERATELY NOT ON THE LIST: gunbc.roadmap_belt_actuate belt_read_or_empty, whose collapse is scoped and argued in the annotation above its definition -- both branches take the same action at every remaining caller -- and gunbc.fabric_cell_acquire, which already establishes absence from the parent enumeration through its own four-state observation and would gain nothing but a second spelling. MONOTONE DIRECTION: the roster above may only shrink. A row leaves it when the site routes through filesystem_file_observation or filesystem_entry_presence, or when the site is deleted; a NEW site of this shape is a defect to repair rather than a row to add. NEXT-RUNG TRIGGER, and it names the capability rather than an artifact: the raw List and Read result projections cease to be reachable outside this module's folds, so a consumer cannot spell the conflation at all -- at which point the enumeration above has no subject and this row is deleted. That is the same trigger filesystem_read_outcome_adoption_standing carries, one question further in: it asks that every read projection be folded, this asks that every ABSENCE be established." + // ABSENCE IS ESTABLISHED BY A SUCCESSFUL LISTING, NEVER BY A FAILED READ. `Read` answers // success=false both for a path that does not exist and for one that exists and cannot be read, and // those two worlds have opposite correct actions -- proceed, versus stop and preserve. Any consumer @@ -197,7 +199,7 @@ fn filesystem_listing_names_entry(listing: String, name: String) -> Bool { // SCOPE, STATED RATHER THAN IMPLIED. This carrier is ADOPTED AT ITS FIRST CONSUMER and is not yet // the type of `filesystem_entry_presence`'s `name` parameter, which is still `String` and still // reachable by every existing caller. Widening it is a replacement migration over that whole -// population in its own change, not +// population and belongs with `filesystem_absence_establishment_adoption_standing` above, not // smuggled into the change that introduces the carrier. What is true today: a consumer that admits // the name and then uses the SAME admitted value for both the membership test and the path // construction cannot put those two out of step. A consumer that does not adopt it is exactly as @@ -346,8 +348,8 @@ fn admit_filesystem_entry_name(name: String) -> FilesystemEntryNameAdmission { // that a `sole_constructor` type's emitted mirror is a public struct with public fields and is // forgeable. Next-rung trigger: the emitted mirror carrying the construction confinement, which is // that section's open item and not this module's to close. And it is a wall over the consumers that -// ROUTE THROUGH IT, not over the corpus: the raw operations remain callable, so adoption at each -// consumer is the obligation the fold cannot enforce for it. +// ROUTE THROUGH IT, not over the corpus: the raw operations remain callable, so adoption is the +// separate obligation recorded in `filesystem_absence_establishment_adoption_standing`. // THE WALL ABOVE IS MEASURED RATHER THAN ASSERTED, and it is recorded here because no enrolled // witness can hold it: the claim is about what the COMPILER REFUSES, its subject is source text // rather than a value, and a hermetic witness that asserted it would be a permanently-green arm @@ -422,7 +424,8 @@ type FilesystemDirectoryListing sole_constructor { // joins names with newlines, so this is the split -- blank lines dropped, every other line one // name as the host spelled it. A consumer that split `entries` itself would be the second // decoder of one wire format (review 69704 of gunbc#12000 found one; extdeps.realization -// artifact_store_fs carries an older one). +// artifact_store_fs carries an older one under +// filesystem_absence_establishment_adoption_standing). fn filesystem_listing_entry_names(listing: FilesystemDirectoryListing) -> List { listing.entries.split(delimiter: "\n").filter(n => n != "") } diff --git a/dag/gunbc/codex_supervised_turn.dag b/dag/gunbc/codex_supervised_turn.dag index b1046302c7b..59bb48b953b 100644 --- a/dag/gunbc/codex_supervised_turn.dag +++ b/dag/gunbc/codex_supervised_turn.dag @@ -50,10 +50,8 @@ import extdeps.filesystem.filesystem_io { FilesystemFileIndeterminate, FilesystemFileObservationsDisagree, FilesystemFileSubjectRefused, - filesystem_read_outcome, - filesystem_listing_observation, - filesystem_file_observation, } +import gunbc.filesystem_file_observe { filesystem_file_observation_of_path } import extdeps.shell import gunbc.provider_standing_probe_bridge { provider_standing_bundle_from_codex_press_receipt, @@ -344,25 +342,7 @@ fn codex_supervised_generation_unobserved(cause: String) -> CodexSupervisedGener fn read_codex_supervised_turn_prior_generation(evidence_root: FilePath) -> CodexSupervisedGenerationRead { let path = codex_supervised_turn_generation_store_path(evidence_root: evidence_root) - let parts = split(s: path, delimiter: "/") - let name = match parts.last() { - Present { value: value } => value - Absent => "" - } - let directory = join(parts.take(n: length(parts) - 1), "/") - let listing = Filesystem.List(path: directory) - let read = Filesystem.Read(path: path) - codex_supervised_generation_read_from_observation(o: filesystem_file_observation( - listing: filesystem_listing_observation( - directory: directory, - success: listing.success, - entries: listing.entries, - error: listing.error, - ), - name: name, - path: path, - read: filesystem_read_outcome(content: read.content, success: read.success, error: read.error), - )) + codex_supervised_generation_read_from_observation(o: filesystem_file_observation_of_path(path: path)) } fn codex_supervised_turn_generation_admission( diff --git a/dag/gunbc/filesystem_file_observe.dag b/dag/gunbc/filesystem_file_observe.dag new file mode 100644 index 00000000000..67e41d3cc06 --- /dev/null +++ b/dag/gunbc/filesystem_file_observe.dag @@ -0,0 +1,50 @@ +module gunbc.filesystem_file_observe + +import std.types { String } +import extdeps.filesystem.filesystem_io { + Filesystem, + FilesystemFileObservation, + filesystem_read_outcome, + filesystem_listing_observation, + filesystem_file_observation, +} + +// ONE WET COMPOSITION FOR ONE QUESTION. "Observe the file at this path" is: split the path into +// directory and entry name, list the directory, read the named entry, and fold both transport +// channels through filesystem_file_observation, so a could-not-look arrives as its own typed +// refusal instead of masquerading as an established absence. This spelling was carried verbatim in +// four wet readers (review 74161 finding 2) and is owned here now: gunbc.codex_supervised_turn, +// gunbc.host_effect_nbd_proxy_serve, tools.merge_admission_walk, and tools.opaque_realization_census +// call it instead of re-spelling the composition. A consumer whose question is not this question +// composes the filesystem_io folds itself rather than varying a copy of this one. +// +// WHY THE HELPER IS HERE AND NOT IN extdeps.filesystem.filesystem_io: that module is pure over +// outcomes the caller already obtained -- its own annotation on the FilesystemFileObservation arms +// says the folds execute no host operations and that preventing the calls themselves is a separate +// migration the module does not claim. This module is the wet side of that boundary: it owns raw +// Filesystem.List and Filesystem.Read calls so consumers do not have to. The +// absence-establishment row's next-rung trigger (the raw projections ceasing to be reachable +// outside filesystem_io's folds) is recorded in +// filesystem_absence_establishment_adoption_standing and remains open; centralizing the calls here +// narrows the population that can spell the conflation without retiring that trigger. +fn filesystem_file_observation_of_path(path: String) -> FilesystemFileObservation { + let parts = split(s: path, delimiter: "/") + let name = match parts.last() { + Present { value: value } => value + Absent => "" + } + let directory = join(parts.take(n: length(parts) - 1), "/") + let listing = Filesystem.List(path: directory) + let read = Filesystem.Read(path: path) + filesystem_file_observation( + listing: filesystem_listing_observation( + directory: directory, + success: listing.success, + entries: listing.entries, + error: listing.error, + ), + name: name, + path: path, + read: filesystem_read_outcome(content: read.content, success: read.success, error: read.error), + ) +} diff --git a/dag/gunbc/host/host_effect_nbd_proxy_serve.dag b/dag/gunbc/host/host_effect_nbd_proxy_serve.dag index 570da8c21bc..dd80363d0af 100644 --- a/dag/gunbc/host/host_effect_nbd_proxy_serve.dag +++ b/dag/gunbc/host/host_effect_nbd_proxy_serve.dag @@ -22,7 +22,6 @@ import extdeps.exec.command { ArgvCommand, argv_words } import extdeps.tools.nbdkit { nbdkit_readonly_file_serve_command } import extdeps.tools.websocat { websocat_nbd_proxy_bridge_command } import extdeps.filesystem.filesystem_io { - Filesystem, FilesystemEstablishedAbsence, FilesystemFileObservation, FilesystemFileAbsent, @@ -30,10 +29,8 @@ import extdeps.filesystem.filesystem_io { FilesystemFileIndeterminate, FilesystemFileObservationsDisagree, FilesystemFileSubjectRefused, - filesystem_read_outcome, - filesystem_listing_observation, - filesystem_file_observation, } +import gunbc.filesystem_file_observe { filesystem_file_observation_of_path } import extdeps.gunbc import gunbc.session_lease { ProcessPortScope, @@ -239,26 +236,7 @@ fn bmcweb_session_token_observation_of(o: FilesystemFileObservation) -> BmcwebSe } fn host_effect_nbd_proxy_serve_read_session_token() -> BmcwebSessionTokenObservation { - let path = srv3_bmcweb_token_path - let parts = split(s: path, delimiter: "/") - let name = match parts.last() { - Present { value: value } => value - Absent => "" - } - let directory = join(parts.take(n: length(parts) - 1), "/") - let listing = Filesystem.List(path: directory) - let read = Filesystem.Read(path: path) - bmcweb_session_token_observation_of(o: filesystem_file_observation( - listing: filesystem_listing_observation( - directory: directory, - success: listing.success, - entries: listing.entries, - error: listing.error, - ), - name: name, - path: path, - read: filesystem_read_outcome(content: read.content, success: read.success, error: read.error), - )) + bmcweb_session_token_observation_of(o: filesystem_file_observation_of_path(path: srv3_bmcweb_token_path)) } // THE START DECISION IS PURE SO IT IS CLAIMABLE. The wet read above runs the host operations; this diff --git a/dag/gunbc/instruments/merge_admission_walk.dag b/dag/gunbc/instruments/merge_admission_walk.dag index 905c43b18a6..a7c79d90d09 100644 --- a/dag/gunbc/instruments/merge_admission_walk.dag +++ b/dag/gunbc/instruments/merge_admission_walk.dag @@ -14,10 +14,8 @@ import extdeps.filesystem.filesystem_io { FilesystemFileIndeterminate, FilesystemFileObservationsDisagree, FilesystemFileSubjectRefused, - filesystem_read_outcome, - filesystem_listing_observation, - filesystem_file_observation, } +import gunbc.filesystem_file_observe { filesystem_file_observation_of_path } import extdeps.github.checks { CheckConclusion, Success } import gunbc.merge_admission { MergeAdmissionReceiptV2, @@ -103,28 +101,6 @@ type FloorReceiptWireObservation | FloorReceiptWireAbsent(FilesystemEstablishedAbsence) | FloorReceiptWireUnobservable { cause: String } -fn wire_file_observation(path: String) -> FilesystemFileObservation { - let parts = split(s: path, delimiter: "/") - let name = match parts.last() { - Present { value: value } => value - Absent => "" - } - let directory = join(parts.take(n: length(parts) - 1), "/") - let listing = Filesystem.List(path: directory) - let read = Filesystem.Read(path: path) - filesystem_file_observation( - listing: filesystem_listing_observation( - directory: directory, - success: listing.success, - entries: listing.entries, - error: listing.error, - ), - name: name, - path: path, - read: filesystem_read_outcome(content: read.content, success: read.success, error: read.error), - ) -} - fn tested_subject_wire_observation_of(o: FilesystemFileObservation) -> TestedSubjectWireObservation { match o { FilesystemFileRead { path: _, content: text } => @@ -150,13 +126,13 @@ fn floor_receipt_wire_observation_of(o: FilesystemFileObservation) -> FloorRecei } fn read_tested_subject(root: String, attempt_id: WalkAttemptId) -> TestedSubjectWireObservation { - tested_subject_wire_observation_of(o: wire_file_observation( + tested_subject_wire_observation_of(o: filesystem_file_observation_of_path( path: merge_admission_tested_subject_path(root: root, attempt_id: attempt_id) )) } fn read_floor_receipt(root: String, attempt_id: WalkAttemptId) -> FloorReceiptWireObservation { - floor_receipt_wire_observation_of(o: wire_file_observation( + floor_receipt_wire_observation_of(o: filesystem_file_observation_of_path( path: merge_admission_floor_receipt_path(root: root, attempt_id: attempt_id) )) } @@ -369,7 +345,11 @@ fn merge_target_refresh() -> MergeTargetRefresh { if merge_freshness_verdict_is_consumed_to_block() { match verdict { MergeAdmitted => MergeTargetRefreshed - _ => MergeTargetRefreshRefused { cause: RefreshVerdictDenied { verdict: merge_admission_verdict_label(v: verdict) } } + MergeDeniedStaleBase => MergeTargetRefreshRefused { cause: RefreshVerdictDenied { verdict: merge_admission_verdict_label(v: verdict) } } + MergeDeniedStaleRoster => MergeTargetRefreshRefused { cause: RefreshVerdictDenied { verdict: merge_admission_verdict_label(v: verdict) } } + MergeDeniedNotSuccess => MergeTargetRefreshRefused { cause: RefreshVerdictDenied { verdict: merge_admission_verdict_label(v: verdict) } } + MergeDeniedWrongAttempt => MergeTargetRefreshRefused { cause: RefreshVerdictDenied { verdict: merge_admission_verdict_label(v: verdict) } } + MergeDeniedSubjectMismatch => MergeTargetRefreshRefused { cause: RefreshVerdictDenied { verdict: merge_admission_verdict_label(v: verdict) } } } } else { MergeTargetRefreshed diff --git a/dag/gunbc/instruments/opaque_realization_census.dag b/dag/gunbc/instruments/opaque_realization_census.dag index d7240fea918..e886f5f556f 100644 --- a/dag/gunbc/instruments/opaque_realization_census.dag +++ b/dag/gunbc/instruments/opaque_realization_census.dag @@ -18,9 +18,8 @@ import extdeps.filesystem.filesystem_io { FilesystemReadSucceeded, FilesystemReadRefused, filesystem_read_outcome, - filesystem_listing_observation, - filesystem_file_observation, } +import gunbc.filesystem_file_observe { filesystem_file_observation_of_path } import tools.host_prelude { witness_bin, witness_bin_ensure_built_typed, @@ -754,31 +753,13 @@ fn declaration_body_standing_in(content: String, name: String) -> DeclarationBod } } -// THE ONE WET READER the candidate fold is allowed, and the pure policy over what it reported. The -// observation is ONE fact per candidate -- the listing decides presence, the read supplies content -// only for a listed file -- so the fold below cannot sequence the two channels differently from any -// other consumer of this module. -fn declaration_candidate_observation(path: String) -> FilesystemFileObservation { - let parts = split(s: path, delimiter: "/") - let name = match parts.last() { - Present { value: value } => value - Absent => "" - } - let directory = join(parts.take(n: length(parts) - 1), "/") - let listing = Filesystem.List(path: directory) - let read = Filesystem.Read(path: path) - filesystem_file_observation( - listing: filesystem_listing_observation( - directory: directory, - success: listing.success, - entries: listing.entries, - error: listing.error, - ), - name: name, - path: path, - read: filesystem_read_outcome(content: read.content, success: read.success, error: read.error), - ) -} +// THE CANDIDATE FOLD'S ONE WET READ, and the pure policy over what it reported. The wet read is one +// call into the shared composition -- gunbc.filesystem_file_observe +// filesystem_file_observation_of_path, per candidate path; this module owns no raw filesystem call +// for the candidate fold -- and the observation is ONE fact per candidate: the listing decides +// presence, the read supplies content only for a listed file. Because the composition is shared, +// the fold below cannot sequence the two channels differently from any other consumer of the +// transport. // THE FOLD STEP IS TOTAL OVER THE OBSERVATION, which is what makes the policy claimable: the witness // suite constructs each transport shape and holds the rules -- resolved wins, an established absence @@ -857,7 +838,7 @@ fn declaration_body_standing(source_module: String, name: String, roots: List declaration_candidate_scan_then_with( acc: acc, - o: declaration_candidate_observation(path: path), + o: filesystem_file_observation_of_path(path: path), name: name, path: path, ) diff --git a/dag/test/claim/opaque_census_declaration_scan_witness_test.dag b/dag/test/claim/opaque_census_declaration_scan_witness_test.dag index dc98db39352..9740ffeee27 100644 --- a/dag/test/claim/opaque_census_declaration_scan_witness_test.dag +++ b/dag/test/claim/opaque_census_declaration_scan_witness_test.dag @@ -73,8 +73,9 @@ test fn opaque_census_declaration_scan_witnesses() -> Bool { && witness_a_same_line_body_is_still_a_body() } -// THE CANDIDATE FOLD'S POLICY, held over constructed observations. The wet reader is one small -// function (declaration_candidate_observation, per candidate path); everything below constructs the +// THE CANDIDATE FOLD'S POLICY, held over constructed observations. The wet read is one call into +// the shared composition (gunbc.filesystem_file_observe filesystem_file_observation_of_path, per +// candidate path); everything below constructs the // transport shapes by hand and steps the SAME fold the wet caller runs, so the suite holds the // rules -- resolved wins, an established absence keeps the search unresolved, a could-not-look is // recorded and finally refuses as unreadable -- without a host filesystem. The three reds are diff --git a/src/v2/workflow/product_receipt_stage.dag b/src/v2/workflow/product_receipt_stage.dag index 6b522a98be9..a99116de256 100644 --- a/src/v2/workflow/product_receipt_stage.dag +++ b/src/v2/workflow/product_receipt_stage.dag @@ -231,7 +231,8 @@ fn manifest_overlay_resolved(o: ManifestFileObservation) -> Bool { ManifestObserved { content: c } => host_source_root_ingest_content_hash != "" && string_contains(s: c, pattern: host_source_root_ingest_content_hash) - _ => false + ManifestAbsent(_) => false + ManifestUnobserved { cause: _ } => false } } From a43da7255dbb827d85aa0174585808b01fff9e5e Mon Sep 17 00:00:00 2001 From: deep-owl-19 Date: Fri, 2 Oct 2026 16:58:13 +0000 Subject: [PATCH 08/11] Address review 74191: fifth copy retired, measurements untranscribed Finding 1: v2.workflow.product_receipt_stage run_product_receipt_stage spelled the same list/read/fold composition the PR centralizes -- a fifth copy. It now calls gunbc.filesystem_file_observe filesystem_file_observation_of_path and imports no fold functions. The two scm wet readers (initialize_repository_at, observe_workspace_file) and harness_completion_observe are NOT copies: they start from an admitted directory and an admitted FilesystemEntryName, so re-splitting a joined path would discard the admission they begin from, and the harness site answers presence only, with no read. Their shapes are documented as the boundary of the shared helper in the helper's annotation. Finding 2: the sibling row's RE-MEASURED paragraph transcribed a one-off instrument run's numbers into an untyped String row and named this PR as a receipt, which DESIGN 6 ('Name the instrument, never transcribe its output') and 4c (typed carriers for counts and receipts) refuse. The paragraph is removed; the row is back at its main content (baseline, subject, re-derivation recipe, trigger), and the re-measurement delta is reported in the PR description where session reporting belongs. The restored absence row no longer names the PR either; it uses the same 'converted by the change that empties this roster' phrasing the row's original text used. --- dag/extdeps/filesystem/filesystem_io.dag | 4 ++-- dag/gunbc/filesystem_file_observe.dag | 12 ++++++---- src/v2/workflow/product_receipt_stage.dag | 28 +++-------------------- 3 files changed, 13 insertions(+), 31 deletions(-) diff --git a/dag/extdeps/filesystem/filesystem_io.dag b/dag/extdeps/filesystem/filesystem_io.dag index be27c3a150c..3e549d27947 100644 --- a/dag/extdeps/filesystem/filesystem_io.dag +++ b/dag/extdeps/filesystem/filesystem_io.dag @@ -157,9 +157,9 @@ fn filesystem_create_new( } } -data filesystem_read_outcome_adoption_standing: String ="RUNG: mitigatable. filesystem_read_outcome provides the single modeled fold from Filesystem.Read's scalar transport observation into FilesystemReadSucceeded | FilesystemReadRefused, but nothing forces callers through it. gunbc.ci_yaml_validate is the first converted consumer and preserves read refusal separately from YAML parse refusal. The raw operation remains directly consumed elsewhere, so content+success+error nonsense combinations remain writable at those sites. SUBJECT: an unconverted consumption site is a Filesystem Read call whose bound result has any success, error, or content projection outside the three arguments of filesystem_read_outcome. The call and those three projections remain after conversion because they supply the fold; adoption changes where they are consumed, not whether they exist. BASELINE measured on origin/main b21b710d5378387ae0c841f07323292c5d72faba: 92 unconverted consumption sites across 48 .dag files. REMAINDER after the first conversion: 91 unconverted consumption sites across 47 files. RE-MEASURED 2026-10-02 on session/deep-owl-19 (origin/main d85c2d8fadecee55c2a9ca5b3c536d159b8f86e6 plus the six absence-establishment conversions and the opaque_realization_census emitted-tree fold this branch carries), same subject, the instrument implemented as spelled here with two mechanical precisions: a projection counts as an argument of the fold iff it sits inside the paren span of a filesystem_read_outcome( call, so multi-line calls classify correctly, and comment lines are not consumption sites -- the same rule that keeps this declaration out of its own count. CALIBRATION: the same implementation reproduces 90 unconverted sites across 46 files at b21b710d against the 92/48 the baseline sentence above records; the difference is filesystem_exact_read sites, which the literal reading classifies unconverted -- that is the sibling modeled fold carrying error_kind, not this fold. MEASURED: 205 unconverted consumption sites across 103 .dag files, with 28 bindings converted and 9 bindings carrying no projection at all; the corpus grew 472 to 7392 tracked .dag files since the baseline head, so the population grew in absolute terms while adoption improved in proportion, and 39 of the 205 are dag/test/claim fixtures. RE-DERIVATION: enumerate Filesystem Read assignment calls in tracked .dag source, excluding this adoption-standing data declaration so the instrument cannot count its own prose; for each bound result, classify it converted only when every success, error, and content projection is an argument of filesystem_read_outcome, otherwise classify it unconverted; count unconverted rows and distinct paths. NEXT-RUNG TRIGGER: the unconverted population reaches zero -- every Filesystem Read result projection occurs only as an argument to filesystem_read_outcome. The compiler-only filesystem_read intrinsic is a separate replacement migration and is not part of this population or this fold." +data filesystem_read_outcome_adoption_standing: String ="RUNG: mitigatable. filesystem_read_outcome provides the single modeled fold from Filesystem.Read's scalar transport observation into FilesystemReadSucceeded | FilesystemReadRefused, but nothing forces callers through it. gunbc.ci_yaml_validate is the first converted consumer and preserves read refusal separately from YAML parse refusal. The raw operation remains directly consumed elsewhere, so content+success+error nonsense combinations remain writable at those sites. SUBJECT: an unconverted consumption site is a Filesystem Read call whose bound result has any success, error, or content projection outside the three arguments of filesystem_read_outcome. The call and those three projections remain after conversion because they supply the fold; adoption changes where they are consumed, not whether they exist. BASELINE measured on origin/main b21b710d5378387ae0c841f07323292c5d72faba: 92 unconverted consumption sites across 48 .dag files. REMAINDER after the first conversion: 91 unconverted consumption sites across 47 files. RE-DERIVATION: enumerate Filesystem Read assignment calls in tracked .dag source, excluding this adoption-standing data declaration so the instrument cannot count its own prose; for each bound result, classify it converted only when every success, error, and content projection is an argument of filesystem_read_outcome, otherwise classify it unconverted; count unconverted rows and distinct paths. NEXT-RUNG TRIGGER: the unconverted population reaches zero -- every Filesystem Read result projection occurs only as an argument to filesystem_read_outcome. The compiler-only filesystem_read intrinsic is a separate replacement migration and is not part of this population or this fold." -data filesystem_absence_establishment_adoption_standing: String = "RUNG: structurally guaranteed for the consumers that route through filesystem_file_observation, on the source-to-.dag acceptance path only, and MITIGATABLE NOWHERE ELSE -- the raw Filesystem.Read and Filesystem.List operations stay callable, so a module that has not adopted the carrier can still write the conflation. This row states the unconverted population at identity grain rather than as a count, because a count is not a plan and a one-sided ratchet over a number measured on the current tree is the oracle section 5 rejects. SUBJECT: a site that concludes ABSENCE, NOT-PRESENT or a dropped element from a FAILED read or a FAILED boolean path test, rather than from a listing that succeeded. It is not every Filesystem.Read consumer -- most read a file they already know exists, and those are the separate filesystem_read_outcome adoption population above. ENUMERATED SITES, each one read rather than pattern-matched: the roster is EMPTY as of this row's restoration. The six identities the row carried on origin/main 6305a5174c all route through the carrier now -- gunbc.host_effect_nbd_proxy_serve host_effect_nbd_proxy_serve_read_session_token, v2.workflow.product_receipt_stage run_product_receipt_stage, tools.merge_admission_walk read_tested_subject and read_floor_receipt, gunbc.codex_supervised_turn codex_supervised_turn_generation_observation, and tools.opaque_realization_census declaration_body_standing converted by PR 12982, each preserving could-not-look as its own typed refusal rather than an absence, and gunbc.fleet_converge_plan_cli observe_cap_members_wet already converted on main -- so a could-not-look at any of them can no longer masquerade as an established absence. THE ROW STAYS NONE THE LESS, and an empty roster is not a deleted row: the raw operations remain callable outside this module, so the class shape can be re-spelled at a new site at any time, and what the row guards is the CLASS, not its former members. A site of this shape found anywhere is a defect to repair by adoption, not a row to add. The mistake this restoration repairs was deleting the row because its enumeration emptied rather than because the trigger below expired, which is exactly the failure the NEXT-RUNG TRIGGER paragraph exists to prevent. WHAT IS DELIBERATELY NOT ON THE LIST: gunbc.roadmap_belt_actuate belt_read_or_empty, whose collapse is scoped and argued in the annotation above its definition -- both branches take the same action at every remaining caller -- and gunbc.fabric_cell_acquire, which already establishes absence from the parent enumeration through its own four-state observation and would gain nothing but a second spelling. MONOTONE DIRECTION: the roster above may only shrink. A row leaves it when the site routes through filesystem_file_observation or filesystem_entry_presence, or when the site is deleted; a NEW site of this shape is a defect to repair rather than a row to add. NEXT-RUNG TRIGGER, and it names the capability rather than an artifact: the raw List and Read result projections cease to be reachable outside this module's folds, so a consumer cannot spell the conflation at all -- at which point the enumeration above has no subject and this row is deleted. That is the same trigger filesystem_read_outcome_adoption_standing carries, one question further in: it asks that every read projection be folded, this asks that every ABSENCE be established." +data filesystem_absence_establishment_adoption_standing: String = "RUNG: structurally guaranteed for the consumers that route through filesystem_file_observation, on the source-to-.dag acceptance path only, and MITIGATABLE NOWHERE ELSE -- the raw Filesystem.Read and Filesystem.List operations stay callable, so a module that has not adopted the carrier can still write the conflation. This row states the unconverted population at identity grain rather than as a count, because a count is not a plan and a one-sided ratchet over a number measured on the current tree is the oracle section 5 rejects. SUBJECT: a site that concludes ABSENCE, NOT-PRESENT or a dropped element from a FAILED read or a FAILED boolean path test, rather than from a listing that succeeded. It is not every Filesystem.Read consumer -- most read a file they already know exists, and those are the separate filesystem_read_outcome adoption population above. ENUMERATED SITES, each one read rather than pattern-matched: the roster is EMPTY as of this row's restoration. The six identities the row carried on origin/main 6305a5174c all route through the carrier now -- gunbc.host_effect_nbd_proxy_serve host_effect_nbd_proxy_serve_read_session_token, v2.workflow.product_receipt_stage run_product_receipt_stage, tools.merge_admission_walk read_tested_subject and read_floor_receipt, gunbc.codex_supervised_turn codex_supervised_turn_generation_observation, and tools.opaque_realization_census declaration_body_standing -- the five converted by the change that empties this roster -- each preserving could-not-look as its own typed refusal rather than an absence, and gunbc.fleet_converge_plan_cli observe_cap_members_wet already converted on main -- so a could-not-look at any of them can no longer masquerade as an established absence. THE ROW STAYS NONE THE LESS, and an empty roster is not a deleted row: the raw operations remain callable outside this module, so the class shape can be re-spelled at a new site at any time, and what the row guards is the CLASS, not its former members. A site of this shape found anywhere is a defect to repair by adoption, not a row to add. The mistake this restoration repairs was deleting the row because its enumeration emptied rather than because the trigger below expired, which is exactly the failure the NEXT-RUNG TRIGGER paragraph exists to prevent. WHAT IS DELIBERATELY NOT ON THE LIST: gunbc.roadmap_belt_actuate belt_read_or_empty, whose collapse is scoped and argued in the annotation above its definition -- both branches take the same action at every remaining caller -- and gunbc.fabric_cell_acquire, which already establishes absence from the parent enumeration through its own four-state observation and would gain nothing but a second spelling. MONOTONE DIRECTION: the roster above may only shrink. A row leaves it when the site routes through filesystem_file_observation or filesystem_entry_presence, or when the site is deleted; a NEW site of this shape is a defect to repair rather than a row to add. NEXT-RUNG TRIGGER, and it names the capability rather than an artifact: the raw List and Read result projections cease to be reachable outside this module's folds, so a consumer cannot spell the conflation at all -- at which point the enumeration above has no subject and this row is deleted. That is the same trigger filesystem_read_outcome_adoption_standing carries, one question further in: it asks that every read projection be folded, this asks that every ABSENCE be established." // ABSENCE IS ESTABLISHED BY A SUCCESSFUL LISTING, NEVER BY A FAILED READ. `Read` answers // success=false both for a path that does not exist and for one that exists and cannot be read, and diff --git a/dag/gunbc/filesystem_file_observe.dag b/dag/gunbc/filesystem_file_observe.dag index 67e41d3cc06..8460d1d11cb 100644 --- a/dag/gunbc/filesystem_file_observe.dag +++ b/dag/gunbc/filesystem_file_observe.dag @@ -13,10 +13,14 @@ import extdeps.filesystem.filesystem_io { // directory and entry name, list the directory, read the named entry, and fold both transport // channels through filesystem_file_observation, so a could-not-look arrives as its own typed // refusal instead of masquerading as an established absence. This spelling was carried verbatim in -// four wet readers (review 74161 finding 2) and is owned here now: gunbc.codex_supervised_turn, -// gunbc.host_effect_nbd_proxy_serve, tools.merge_admission_walk, and tools.opaque_realization_census -// call it instead of re-spelling the composition. A consumer whose question is not this question -// composes the filesystem_io folds itself rather than varying a copy of this one. +// five wet readers (review 74161 finding 2, extended by review 74191 to the fifth) and is owned +// here now: gunbc.codex_supervised_turn, gunbc.host_effect_nbd_proxy_serve, +// tools.merge_admission_walk, tools.opaque_realization_census, and +// v2.workflow.product_receipt_stage call it instead of re-spelling the composition. A consumer +// whose question is not this question composes the filesystem_io folds itself rather than varying +// a copy of this one -- in particular a consumer that already holds an admitted directory and an +// admitted FilesystemEntryName keeps its own composition, because re-splitting a joined path would +// discard the admission it starts from. // // WHY THE HELPER IS HERE AND NOT IN extdeps.filesystem.filesystem_io: that module is pure over // outcomes the caller already obtained -- its own annotation on the FilesystemFileObservation arms diff --git a/src/v2/workflow/product_receipt_stage.dag b/src/v2/workflow/product_receipt_stage.dag index a99116de256..80dd9cfc001 100644 --- a/src/v2/workflow/product_receipt_stage.dag +++ b/src/v2/workflow/product_receipt_stage.dag @@ -10,10 +10,8 @@ import extdeps.filesystem.filesystem_io { FilesystemFileIndeterminate, FilesystemFileObservationsDisagree, FilesystemFileSubjectRefused, - filesystem_read_outcome, - filesystem_listing_observation, - filesystem_file_observation, } +import gunbc.filesystem_file_observe { filesystem_file_observation_of_path } import extdeps.git import extdeps.git.inspect import extdeps.gunbc @@ -600,28 +598,8 @@ fn run_product_receipt_stage(txn: String, manifest_identity: String, entry: Stri let b1_produced = stage_identity_from_hex(hex: manifest_identity, file_count: 1) - let manifest_parts = split(s: manifest_path, delimiter: "/") - let manifest_name = match manifest_parts.last() { - Present { value: value } => value - Absent => "" - } - let manifest_directory = join(manifest_parts.take(n: length(manifest_parts) - 1), "/") - let manifest_listing = Filesystem.List(path: manifest_directory) - let manifest_read = Filesystem.Read(path: manifest_path) - let manifest_observation = manifest_file_observation_of(o: filesystem_file_observation( - listing: filesystem_listing_observation( - directory: manifest_directory, - success: manifest_listing.success, - entries: manifest_listing.entries, - error: manifest_listing.error, - ), - name: manifest_name, - path: manifest_path, - read: filesystem_read_outcome( - content: manifest_read.content, - success: manifest_read.success, - error: manifest_read.error - ), + let manifest_observation = manifest_file_observation_of(o: filesystem_file_observation_of_path( + path: manifest_path )) let b2_consumed = manifest_boundary2_consumed(o: manifest_observation) From 4a7d6934cff6c37dc018bebb13d75217ba488312 Mon Sep 17 00:00:00 2001 From: deep-owl-19 Date: Fri, 2 Oct 2026 20:36:33 +0000 Subject: [PATCH 09/11] filesystem_file_observe: pure path-decomposition authority before any host call The wet helper split/take/joined the path operand inside the wet operation: for /token the parent joined to the empty string, so the listing observed a DIFFERENT subject than the read named (List("") vs Read("/token")), and a bare operand decomposed to the same empty directory. No test executed the decomposition. filesystem_path_decomposition is now the one authority, computed before any Filesystem.List or Read: it derives / for a root-level operand, derives . for a dot-prefixed one, and refuses -- as FilesystemFileSubjectRefused with no call attempted -- the empty operand, a bare entry name, an operand ending in a separator, and a '.' or '..' cursor entry name, each with its own cause. The wet operation holds no split/take/join path semantics; it matches the decomposition and only a Decomposed result reaches the host calls. Controls in test.claim.filesystem_file_observe_witness_test execute the authority for /tmp/token, /token, target/token, and token, plus the refused shapes; all ten pass under claim_batch --entry against the dag+src/v2 roots. --- dag/gunbc/filesystem_file_observe.dag | 95 +++++++++++++++---- .../filesystem_file_observe_witness_test.dag | 89 +++++++++++++++++ 2 files changed, 166 insertions(+), 18 deletions(-) create mode 100644 dag/test/claim/filesystem_file_observe_witness_test.dag diff --git a/dag/gunbc/filesystem_file_observe.dag b/dag/gunbc/filesystem_file_observe.dag index 8460d1d11cb..7d7d9b7264b 100644 --- a/dag/gunbc/filesystem_file_observe.dag +++ b/dag/gunbc/filesystem_file_observe.dag @@ -4,12 +4,17 @@ import std.types { String } import extdeps.filesystem.filesystem_io { Filesystem, FilesystemFileObservation, + FilesystemFileSubjectRefused, filesystem_read_outcome, filesystem_listing_observation, filesystem_file_observation, } -// ONE WET COMPOSITION FOR ONE QUESTION. "Observe the file at this path" is: split the path into +type FilesystemPathDecomposition + = FilesystemPathDecomposed { directory: String, name: String } + | FilesystemPathUndecomposable { cause: String } + +// ONE WET COMPOSITION FOR ONE QUESTION. "Observe the file at this path" is: decompose the path into // directory and entry name, list the directory, read the named entry, and fold both transport // channels through filesystem_file_observation, so a could-not-look arrives as its own typed // refusal instead of masquerading as an established absence. This spelling was carried verbatim in @@ -19,8 +24,24 @@ import extdeps.filesystem.filesystem_io { // v2.workflow.product_receipt_stage call it instead of re-spelling the composition. A consumer // whose question is not this question composes the filesystem_io folds itself rather than varying // a copy of this one -- in particular a consumer that already holds an admitted directory and an -// admitted FilesystemEntryName keeps its own composition, because re-splitting a joined path would -// discard the admission it starts from. +// admitted FilesystemEntryName keeps its own composition, because re-decomposing a joined path +// would discard the admission it starts from. +// +// PATH DECOMPOSITION IS A PURE AUTHORITY COMPUTED BEFORE ANY HOST CALL. filesystem_path_decomposition +// is the one place that turns a path operand into a directory and an entry name, and the wet +// operation below holds no split, take, or join path semantics of its own: it decomposes first, and +// only a FilesystemPathDecomposed result reaches Filesystem.List or Filesystem.Read. The authority +// derives the directory operand so that the listing always observes the same subject the read names: +// "/tmp/token" lists "/tmp", and "/token" lists "/" -- the root itself, not the empty string that +// joining the nothing before the root separator would yield, because a listing of "" is a different +// subject than a read of "/token". An operand it cannot decompose into one directory and one entry +// name is refused before any call, each shape with its own cause: the empty operand; a bare entry +// name, which has no directory operand to list; an operand ending in a separator, which names a +// directory rather than an entry in one; and an entry name that is the "." or ".." directory +// cursor. A "./token" operand decomposes to directory "." and entry name "token", which list and +// read the same subject the operand names. The controls in +// test.claim.filesystem_file_observe_witness_test execute the authority for /tmp/token, /token, +// target/token, and token, and for the refused shapes. // // WHY THE HELPER IS HERE AND NOT IN extdeps.filesystem.filesystem_io: that module is pure over // outcomes the caller already obtained -- its own annotation on the FilesystemFileObservation arms @@ -31,24 +52,62 @@ import extdeps.filesystem.filesystem_io { // outside filesystem_io's folds) is recorded in // filesystem_absence_establishment_adoption_standing and remains open; centralizing the calls here // narrows the population that can spell the conflation without retiring that trigger. -fn filesystem_file_observation_of_path(path: String) -> FilesystemFileObservation { +fn filesystem_path_decomposition(path: String) -> FilesystemPathDecomposition { let parts = split(s: path, delimiter: "/") let name = match parts.last() { Present { value: value } => value Absent => "" } - let directory = join(parts.take(n: length(parts) - 1), "/") - let listing = Filesystem.List(path: directory) - let read = Filesystem.Read(path: path) - filesystem_file_observation( - listing: filesystem_listing_observation( - directory: directory, - success: listing.success, - entries: listing.entries, - error: listing.error, - ), - name: name, - path: path, - read: filesystem_read_outcome(content: read.content, success: read.success, error: read.error), - ) + let parent_parts = parts.take(n: length(parts) - 1) + if path == "" { + FilesystemPathUndecomposable { + cause: "the path operand is empty, so no directory and no entry name can be named", + } + } else if name == "" { + FilesystemPathUndecomposable { + cause: "the path operand ends in a directory separator, so it names a directory rather than an entry in one", + } + } else if name == "." { + FilesystemPathUndecomposable { + cause: "the path operand's entry name is the '.' directory cursor, not an entry name", + } + } else if name == ".." { + FilesystemPathUndecomposable { + cause: "the path operand's entry name is the '..' directory cursor, not an entry name", + } + } else if length(parts) == 1 { + FilesystemPathUndecomposable { + cause: "the path operand is a bare entry name with no directory operand to list", + } + } else if length(parent_parts) == 1 && starts_with(s: path, prefix: "/") { + // The operand is "/": its only separator is the root separator, so the directory operand + // is the root itself, not the empty string that joining the nothing before it would yield. + FilesystemPathDecomposed { directory: "/", name: name } + } else { + FilesystemPathDecomposed { directory: join(parent_parts, "/"), name: name } + } +} + +fn filesystem_file_observation_of_path(path: String) -> FilesystemFileObservation { + match filesystem_path_decomposition(path: path) { + FilesystemPathUndecomposable { cause: cause } => + // The operand was refused before any filesystem call ran, so no directory and no entry name + // was ever established to carry in the arm's fields; the cause is the whole refusal. + FilesystemFileSubjectRefused { directory: "", name: "", cause: cause } + FilesystemPathDecomposed { directory: directory, name: name } => { + let listing = Filesystem.List(path: directory) + let read = Filesystem.Read(path: path) + filesystem_file_observation( + listing: filesystem_listing_observation( + directory: directory, + success: listing.success, + entries: listing.entries, + error: listing.error, + ), + name: name, + path: path, + read: filesystem_read_outcome(content: read.content, success: read.success, error: read.error), + ) + } + } } diff --git a/dag/test/claim/filesystem_file_observe_witness_test.dag b/dag/test/claim/filesystem_file_observe_witness_test.dag new file mode 100644 index 00000000000..aca8dfe9c63 --- /dev/null +++ b/dag/test/claim/filesystem_file_observe_witness_test.dag @@ -0,0 +1,89 @@ +module test.claim.filesystem_file_observe_witness_test + +import gunbc.filesystem_file_observe { + filesystem_path_decomposition, + FilesystemPathDecomposed, + FilesystemPathUndecomposable, +} + +// These execute the pure path-decomposition authority that fronts every +// filesystem_file_observation_of_path call (review on the head of the helper's introduction). The +// authority must name, as directory plus entry name, the same subject the caller's read names -- so +// a single-component absolute operand observes the root, not the empty string -- and it must refuse +// the operand shapes it cannot decompose BEFORE the wet operation lists or reads anything. Native +// acquisition is exercised by the wet operation's own callers; the wet operation holds no path +// semantics of its own to discriminate here. + +test fn a_two_component_absolute_path_decomposes_to_its_directory_and_entry() -> Bool { + match filesystem_path_decomposition(path: "/tmp/token") { + FilesystemPathDecomposed { directory: d, name: n } => d == "/tmp" && n == "token" + FilesystemPathUndecomposable { cause: _ } => false + } +} + +test fn a_root_level_absolute_path_decomposes_to_the_root_not_the_empty_string() -> Bool { + match filesystem_path_decomposition(path: "/token") { + FilesystemPathDecomposed { directory: d, name: n } => d == "/" && n == "token" + FilesystemPathUndecomposable { cause: _ } => false + } +} + +test fn a_two_component_relative_path_decomposes_to_its_directory_and_entry() -> Bool { + match filesystem_path_decomposition(path: "target/token") { + FilesystemPathDecomposed { directory: d, name: n } => d == "target" && n == "token" + FilesystemPathUndecomposable { cause: _ } => false + } +} + +test fn a_dot_prefixed_path_decomposes_to_the_dot_directory_and_entry() -> Bool { + match filesystem_path_decomposition(path: "./token") { + FilesystemPathDecomposed { directory: d, name: n } => d == "." && n == "token" + FilesystemPathUndecomposable { cause: _ } => false + } +} + +test fn a_bare_entry_name_is_refused_for_having_no_directory_operand() -> Bool { + match filesystem_path_decomposition(path: "token") { + FilesystemPathUndecomposable { cause: c } => + string_contains(s: c, pattern: "no directory operand to list") + FilesystemPathDecomposed { directory: _, name: _ } => false + } +} + +test fn the_empty_operand_is_refused() -> Bool { + match filesystem_path_decomposition(path: "") { + FilesystemPathUndecomposable { cause: c } => string_contains(s: c, pattern: "operand is empty") + FilesystemPathDecomposed { directory: _, name: _ } => false + } +} + +test fn an_operand_ending_in_a_separator_is_refused_for_naming_a_directory() -> Bool { + match filesystem_path_decomposition(path: "/") { + FilesystemPathUndecomposable { cause: c } => + string_contains(s: c, pattern: "names a directory rather than an entry in one") + FilesystemPathDecomposed { directory: _, name: _ } => false + } +} + +test fn a_relative_operand_ending_in_a_separator_is_refused_the_same_way() -> Bool { + match filesystem_path_decomposition(path: "a/") { + FilesystemPathUndecomposable { cause: c } => + string_contains(s: c, pattern: "names a directory rather than an entry in one") + FilesystemPathDecomposed { directory: _, name: _ } => false + } +} + +test fn a_dot_cursor_entry_name_is_refused() -> Bool { + match filesystem_path_decomposition(path: "a/.") { + FilesystemPathUndecomposable { cause: c } => string_contains(s: c, pattern: "'.' directory cursor") + FilesystemPathDecomposed { directory: _, name: _ } => false + } +} + +test fn a_dot_dot_cursor_entry_name_is_refused() -> Bool { + match filesystem_path_decomposition(path: "a/..") { + FilesystemPathUndecomposable { cause: c } => + string_contains(s: c, pattern: "'..' directory cursor") + FilesystemPathDecomposed { directory: _, name: _ } => false + } +} From 0b36ff0c713487d63f220bcf19c802cbb0fd75fb Mon Sep 17 00:00:00 2001 From: deep-owl-19 Date: Fri, 2 Oct 2026 21:07:04 +0000 Subject: [PATCH 10/11] filesystem_file_observe: annotations out of declaration bodies The emitter models source annotations at module-item grain only: the two comments I had placed inside the decomposition branch and the refusal arm parsed as 4 hard diagnostics (floor parse FAIL at lines 83/84/94/95, and the emit lane refused 00_compile.dag's closure with EmissionRefused). The root-derivation comment was already stated in the annotation above filesystem_path_decomposition, so it is deleted; the no-subject-fields note moves above filesystem_file_observation_of_path, where it belongs. No code changes; all ten witness controls still pass. --- dag/gunbc/filesystem_file_observe.dag | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/dag/gunbc/filesystem_file_observe.dag b/dag/gunbc/filesystem_file_observe.dag index 7d7d9b7264b..060b52c620b 100644 --- a/dag/gunbc/filesystem_file_observe.dag +++ b/dag/gunbc/filesystem_file_observe.dag @@ -80,19 +80,18 @@ fn filesystem_path_decomposition(path: String) -> FilesystemPathDecomposition { cause: "the path operand is a bare entry name with no directory operand to list", } } else if length(parent_parts) == 1 && starts_with(s: path, prefix: "/") { - // The operand is "/": its only separator is the root separator, so the directory operand - // is the root itself, not the empty string that joining the nothing before it would yield. FilesystemPathDecomposed { directory: "/", name: name } } else { FilesystemPathDecomposed { directory: join(parent_parts, "/"), name: name } } } +// THE UNDECOMPOSABLE REFUSAL CARRIES NO SUBJECT FIELDS. The operand was refused before any +// filesystem call ran, so no directory and no entry name was ever established to carry in the arm's +// fields -- they are empty because no subject was ever named, and the cause is the whole refusal. fn filesystem_file_observation_of_path(path: String) -> FilesystemFileObservation { match filesystem_path_decomposition(path: path) { FilesystemPathUndecomposable { cause: cause } => - // The operand was refused before any filesystem call ran, so no directory and no entry name - // was ever established to carry in the arm's fields; the cause is the whole refusal. FilesystemFileSubjectRefused { directory: "", name: "", cause: cause } FilesystemPathDecomposed { directory: directory, name: name } => { let listing = Filesystem.List(path: directory) From d5aca36b75849153cfff26af0df9b40fa114face Mon Sep 17 00:00:00 2001 From: deep-owl-19 Date: Sat, 3 Oct 2026 01:47:04 +0000 Subject: [PATCH 11/11] non_fold_residue: delete the stale row for merge_target_refresh The composed run refused NonFoldResidueRosterDiverged stale=1: main's NFR census (#12980) added a FrontierRow for dag/gunbc/instruments/merge_admission_walk.dag::merge_target_refresh, but this PR's change already totalled that fold -- all six MergeAdmissionVerdict arms are spelled, no wildcard arm, so no non-fold residue exists for the subject and the roster row is stale on the composed tree. The row is deleted; roster and residue agree again. manifest_overlay_resolved was checked too: main added no row for it, and its three arms are totalled here, so nothing to delete there. --- dag/gunbc/non_fold_residue.dag | 1 - 1 file changed, 1 deletion(-) diff --git a/dag/gunbc/non_fold_residue.dag b/dag/gunbc/non_fold_residue.dag index 9bd2b89160d..efc3371f6ca 100644 --- a/dag/gunbc/non_fold_residue.dag +++ b/dag/gunbc/non_fold_residue.dag @@ -1304,7 +1304,6 @@ data non_fold_residue_frontier: List = [ FrontierRow { subject: PathSubject { path: "dag/gunbc/instruments/frontier_ingestion_probe.dag::take_census_over" }, reason: nfr_reason_typed_census_ca5ed1724b, dissolution: nfr_dissolve_owning_fold }, FrontierRow { subject: PathSubject { path: "dag/gunbc/instruments/frontier_ingestion_probe.dag::verify_roster" }, reason: nfr_reason_typed_census_ca5ed1724b, dissolution: nfr_dissolve_owning_fold }, FrontierRow { subject: PathSubject { path: "dag/gunbc/instruments/json_parse_ladder.dag::weight_map_members" }, reason: nfr_reason_typed_census_ca5ed1724b, dissolution: nfr_dissolve_owning_fold }, - FrontierRow { subject: PathSubject { path: "dag/gunbc/instruments/merge_admission_walk.dag::merge_target_refresh" }, reason: nfr_reason_typed_census_ca5ed1724b, dissolution: nfr_dissolve_owning_fold }, FrontierRow { subject: PathSubject { path: "dag/gunbc/instruments/native_app_attest.dag::chain_untrusted" }, reason: nfr_reason_typed_census_ca5ed1724b, dissolution: nfr_dissolve_owning_fold }, FrontierRow { subject: PathSubject { path: "dag/gunbc/instruments/native_app_attest.dag::counter_refusal_is" }, reason: nfr_reason_typed_census_ca5ed1724b, dissolution: nfr_dissolve_owning_fold }, FrontierRow { subject: PathSubject { path: "dag/gunbc/instruments/publication_publisher.dag::newly_public_subject_receipt_refusal" }, reason: nfr_reason_typed_census_ca5ed1724b, dissolution: nfr_dissolve_owning_fold },