Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 4 additions & 2 deletions dag/extdeps/filesystem/filesystem_io.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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<String> {
listing.entries.split(delimiter: "\n").filter(n => n != "")
}
Expand Down Expand Up @@ -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) --
Expand Down
5 changes: 3 additions & 2 deletions dag/gunbc/auth/approval_decision_store.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
65 changes: 40 additions & 25 deletions dag/gunbc/codex_supervised_turn.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 {
Expand All @@ -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(
Expand Down
Loading