diff --git a/dag/extdeps/filesystem/filesystem_io.dag b/dag/extdeps/filesystem/filesystem_io.dag index eeee7e62d67..df47ab5a7e6 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-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 -- 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 // those two worlds have opposite correct actions -- proceed, versus stop and preserve. Any consumer @@ -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 under filesystem_absence_establishment_adoption_standing). +// 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 != "") } @@ -645,7 +648,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..59bb48b953b 100644 --- a/dag/gunbc/codex_supervised_turn.dag +++ b/dag/gunbc/codex_supervised_turn.dag @@ -42,7 +42,16 @@ 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, +} +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, @@ -126,7 +135,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 +289,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 +309,40 @@ 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, - ) - } + 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..060b52c620b --- /dev/null +++ b/dag/gunbc/filesystem_file_observe.dag @@ -0,0 +1,112 @@ +module gunbc.filesystem_file_observe + +import std.types { String } +import extdeps.filesystem.filesystem_io { + Filesystem, + FilesystemFileObservation, + FilesystemFileSubjectRefused, + filesystem_read_outcome, + filesystem_listing_observation, + filesystem_file_observation, +} + +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 +// 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-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 +// 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_path_decomposition(path: String) -> FilesystemPathDecomposition { + let parts = split(s: path, delimiter: "/") + let name = match parts.last() { + Present { value: value } => value + Absent => "" + } + 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: "/") { + 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 } => + 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/gunbc/host/host_effect_nbd_proxy_serve.dag b/dag/gunbc/host/host_effect_nbd_proxy_serve.dag index 98bedad27af..dd80363d0af 100644 --- a/dag/gunbc/host/host_effect_nbd_proxy_serve.dag +++ b/dag/gunbc/host/host_effect_nbd_proxy_serve.dag @@ -21,7 +21,16 @@ 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 { + FilesystemEstablishedAbsence, + FilesystemFileObservation, + FilesystemFileAbsent, + FilesystemFileRead, + FilesystemFileIndeterminate, + FilesystemFileObservationsDisagree, + FilesystemFileSubjectRefused, +} +import gunbc.filesystem_file_observe { filesystem_file_observation_of_path } import extdeps.gunbc import gunbc.session_lease { ProcessPortScope, @@ -202,15 +211,62 @@ 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 { + 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 +// 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 +313,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 +330,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..a7c79d90d09 100644 --- a/dag/gunbc/instruments/merge_admission_walk.dag +++ b/dag/gunbc/instruments/merge_admission_walk.dag @@ -5,7 +5,17 @@ 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, +} +import gunbc.filesystem_file_observe { filesystem_file_observation_of_path } import extdeps.github.checks { CheckConclusion, Success } import gunbc.merge_admission { MergeAdmissionReceiptV2, @@ -74,28 +84,59 @@ 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) - ) - if !read.success { - none - } else { - parse_tested_subject_wire(text: read.content) +// 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 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: 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: filesystem_file_observation_of_path( + 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 +161,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 +200,9 @@ type MergeTargetRefreshRefusal = RefreshFetchRefused { stderr: String } | RefreshAttemptIdentityAbsent | RefreshTestedSubjectWireMissing + | RefreshTestedSubjectWireUnreadable { cause: String } | RefreshFloorReceiptWireMissing + | RefreshFloorReceiptWireUnreadable { cause: String } | RefreshTargetCommitObservationRefused | RefreshVerdictDenied { verdict: String } @@ -167,7 +215,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 +240,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 +316,46 @@ 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 + 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 + } + } } - } else { - MergeTargetRefreshed - } } } } diff --git a/dag/gunbc/instruments/opaque_realization_census.dag b/dag/gunbc/instruments/opaque_realization_census.dag index 43bcc1e7d2f..e886f5f556f 100644 --- a/dag/gunbc/instruments/opaque_realization_census.dag +++ b/dag/gunbc/instruments/opaque_realization_census.dag @@ -7,7 +7,19 @@ 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, +} +import gunbc.filesystem_file_observe { filesystem_file_observation_of_path } import tools.host_prelude { witness_bin, witness_bin_ensure_built_typed, @@ -145,10 +157,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 +192,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 +753,97 @@ fn declaration_body_standing_in(content: String, name: String) -> DeclarationBod } } +// 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 +// 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: filesystem_file_observation_of_path(path: path), + name: name, + path: path, + ) ) + declaration_standing_from_scan(scan: scan) } // --------------------------------------------------------------------------------------------- @@ -753,20 +862,28 @@ 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 } => 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 +1192,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/gunbc/non_fold_residue.dag b/dag/gunbc/non_fold_residue.dag index 1b11c9769f2..7c32c01f45f 100644 --- a/dag/gunbc/non_fold_residue.dag +++ b/dag/gunbc/non_fold_residue.dag @@ -1290,7 +1290,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 }, diff --git a/dag/test/claim/codex_supervised_turn_witness_test.dag b/dag/test/claim/codex_supervised_turn_witness_test.dag index e722df02fd2..80a987721ac 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,17 @@ import std.temporal_effect { LeaseRunningExpected, } +import extdeps.filesystem.filesystem_io { + 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." 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 +315,156 @@ 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. +// 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 { - match codex_supervised_generation_read_from_store( - store_present: false, - read_success: true, - content: "", + 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", + ), + ) { + FilesystemFileAbsent(a) => + match codex_supervised_generation_read_from_observation(o: FilesystemFileAbsent(a)) { + GenerationAbsent => true + _ => false + } + _ => false + } +} + +// 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 { + 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) => { + let read = codex_supervised_generation_read_from_observation(o: FilesystemFileAbsent(a)) + match codex_supervised_turn_generation_admission(read: read) { + CodexTurnStartAdmitted => true + _ => false + } + } + _ => 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 +477,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 +495,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/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 + } +} 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..ef6fbaebdce 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,21 @@ 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, +} +import gunbc.srv3_nbd_proxy_serve_intent { + srv3_nbd_proxy_lease_key, +} + data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly @@ -261,3 +277,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..9740ffeee27 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 extdeps.filesystem.filesystem_io { + FilesystemFileAbsent, FilesystemFileRead, FilesystemFileIndeterminate, + FilesystemFileObservationsDisagree, FilesystemFileSubjectRefused, + filesystem_listing_observation, filesystem_file_observation, filesystem_read_outcome, +} 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,151 @@ 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 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 +// 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. +// 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 { + let listing = filesystem_listing_observation(directory: "dag", success: true, entries: "", error: "") + match filesystem_file_observation( + listing: listing, + name: "x.dag", + path: "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", + ) { + DeclarationScanUnresolved { attempted: att, unobserved: _ } => att == "dag/x.dag" + _ => false + } + _ => 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..80dd9cfc001 100644 --- a/src/v2/workflow/product_receipt_stage.dag +++ b/src/v2/workflow/product_receipt_stage.dag @@ -1,7 +1,17 @@ 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, +} +import gunbc.filesystem_file_observe { filesystem_file_observation_of_path } import extdeps.git import extdeps.git.inspect import extdeps.gunbc @@ -76,10 +86,12 @@ import v2.workflow.product_receipt { ManifestPopulationAdmitted, ManifestPopulationEmpty, ManifestPopulationPartial, + ManifestUnobservable, AdmissionReasonUnrecognized, ManifestSourceReadFailed, PopulationDigestMismatch, ProducerReportedNoArtifact, + ProducerUnobservable, ProductBoundary, ProductReceipt, RefsHashVerified, @@ -165,6 +177,93 @@ 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) + ManifestAbsent(_) => false + ManifestUnobserved { cause: _ } => 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 +271,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 @@ -487,6 +587,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) @@ -494,16 +598,13 @@ 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 } - } + 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) - 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 overlay_resolved = manifest_overlay_resolved(o: manifest_observation) let admission = closure_emit_population_admission( refs: host_source_root_closure_refs, @@ -521,34 +622,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: c } => + stage_refused( + boundary: ManifestPopulationAdmitted, + cause: ManifestUnobservable { cause: c }, + 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 +716,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 },