Repository navigation
filesystem: absence is established, never inferred (DP-M5) - #12982
Conversation
Delete data row filesystem_absence_establishment_adoption_standing by converting all six of its identities: each site that concluded Absent from a failed read or a false shell Test.IsFile now routes through filesystem_file_observation / filesystem_entry_presence, so could-not-look becomes typed refusal (FilesystemFileIndeterminate / SubjectRefused) and only an unobserved listing establishes absence. - host_effect_nbd_proxy_serve: session-token read is a 3-arm BmcwebSessionTokenObservation with a rewritten reader - fleet_converge_plan_cli observe_cap_members_wet: already converted on main (verified by reading the site) - product_receipt_stage: manifest/producer reads carry ManifestUnobservable/ProducerUnobservable causes - merge_admission_walk: tested-subject and floor-receipt wire reads refuse as RefreshTestedSubjectWireUnreadable/RefreshFloorReceiptWireUnreadable - codex_supervised_turn: generation-store read folded through the filesystem observation; Unreadable refuses as duplicate-execution guard instead of admitting - opaque_realization_census: declaration-body standing gains DeclarationSourceUnreadable(path, cause), resolved-wins scan Sibling row filesystem_read_outcome_adoption_standing re-measured at identity grain with a named instrument (calibrated against b21b710); emitted_tree_read_then converted opportunistically.
The transport witness file had no imports before this branch, so its bare-provider channel was on and srv3_nbd_proxy_lease_key was pulled implicitly. Adding the filesystem_io and host_effect_nbd_proxy_serve imports for the absence-establishment conversion switched the file to imported mode, where every provider name must be pulled by name; the required floor refused the now-unrostered lease key. Import it from gunbc.srv3_nbd_proxy_serve_intent as the gate prescribes.
The v2 Rust emitter models source annotations only at module-item grain: the four-line observation note inside run_product_receipt_stage and the three-line coproduct note inside emitted_tree_read_then each produced an EmissionRefused hard diagnostic (7 total) in the self-host compile. Both notes move above the declaration they describe, with the census note reworded to state the fold law it documents.
FilesystemEstablishedAbsence is sole_constructor -- constructible only inside the interface module -- so the three claim sites that wrote the record literal (codex turn x2, census x1) are repaired to DERIVE the absence through the modeled route: filesystem_listing_observation with success and an entry list that omits the name, folded through filesystem_file_observation, matched as FilesystemFileAbsent(a). The same route the wet reader takes, which is the point of the mint. product_receipt_stage: the ManifestUnobserved arm referenced manifest_unobserved_cause, a variable that was never bound; the arm now binds the cause it matches on.
Same module-item-grain rule as the previous repair, applied to the comments the mint rewrite itself placed inside the claim bodies: the emitter compiles the whole corpus, so an annotation inside any .dag declaration body refuses emission. The notes move above the test fns they describe.
The established-absence control matched DeclarationSourceUnresolved -- the STANDING decode's arm -- against the DeclarationCandidateScan the fold returns, whose unresolved arm is DeclarationScanUnresolved.
…s, own the observe-a-file composition once Finding 1: filesystem_absence_establishment_adoption_standing was deleted when its roster emptied, but the row's own NEXT-RUNG TRIGGER ties deletion to the capability (raw List/Read projections ceasing to be reachable outside filesystem_io's folds), not to an empty roster. Restored with an empty roster, the same trigger, and the three in-module comment citations re-grafted now that the target resolves again. Verified against the six identities the row carried on 6305a51: five converted by this PR, observe_cap_members_wet already converted on main. CI blocker (NonFoldResidueRosterDiverged unrostered=2): manifest_overlay_resolved now matches all three ManifestFileObservation arms, and merge_target_refresh enumerates all six MergeAdmissionVerdict arms with identical semantics instead of a wildcard over the closed coproduct. Finding 2: the list-directory/read-named-entry/match composition was spelled verbatim in four wet readers. It is now owned once, in gunbc.filesystem_file_observe filesystem_file_observation_of_path, called by gunbc.codex_supervised_turn, gunbc.host_effect_nbd_proxy_serve, tools.merge_admission_walk, and tools.opaque_realization_census. The home is deliberately NOT extdeps.filesystem.filesystem_io, which is pure over outcomes the caller already obtained by its own annotation; the helper is the wet side of that boundary, which narrows the raw-call population without retiring the row's trigger.
|
Addressing review 74161 (REQUEST_CHANGES on c527aea), fixed in 420f15b: Finding 1 — the absence row was deleted before its trigger fired. The row's own NEXT-RUNG TRIGGER ties deletion to the capability ("the raw List and Read result projections cease to be reachable outside this module's folds"), not to an empty roster; emptying the roster was necessary but not sufficient, and deleting on an empty roster is exactly the failure the trigger paragraph exists to prevent. Finding 2 — the observe-a-file composition was spelled four times. It is now owned once: CI blocker on the previous head (NonFoldResidueRosterDiverged, unrostered=2). Both sites are in files this PR touched, so the diff-scoped residue check now sees them. Rather than adding roster rows (that roster is not this change's to extend), both matches were totalled: CI on 420f15b is green: floor 37m57s, generated 22m11s, emit-build 29m44s, witnesses pass (run 37027899988). |
Finding 1: v2.workflow.product_receipt_stage run_product_receipt_stage
spelled the same list/read/fold composition the PR centralizes -- a fifth
copy. It now calls gunbc.filesystem_file_observe
filesystem_file_observation_of_path and imports no fold functions. The
two scm wet readers (initialize_repository_at, observe_workspace_file)
and harness_completion_observe are NOT copies: they start from an
admitted directory and an admitted FilesystemEntryName, so re-splitting
a joined path would discard the admission they begin from, and the
harness site answers presence only, with no read. Their shapes are
documented as the boundary of the shared helper in the helper's
annotation.
Finding 2: the sibling row's RE-MEASURED paragraph transcribed a
one-off instrument run's numbers into an untyped String row and named
this PR as a receipt, which DESIGN 6 ('Name the instrument, never
transcribe its output') and 4c (typed carriers for counts and receipts)
refuse. The paragraph is removed; the row is back at its main content
(baseline, subject, re-derivation recipe, trigger), and the
re-measurement delta is reported in the PR description where session
reporting belongs. The restored absence row no longer names the PR
either; it uses the same 'converted by the change that empties this
roster' phrasing the row's original text used.
|
Addressing review 74191 (REQUEST_CHANGES on 420f15b), fixed in a43da72: Finding 1 — the fifth copy. Finding 2 — transcribed measurement, PR-as-receipt. Agreed on both: DESIGN §6 ("Name the instrument, never transcribe its output") and §4c (typed carriers for counts and receipts) refuse both, and the paragraph was mine. The RE-MEASURED paragraph is removed from CI on a43da72 is running; checks will land here. |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
The six consumer conversions are directionally correct: their pure policy seams preserve could-not-look separately from established absence, and the new claims cover those arms. The shared wet helper is not yet correct over its declared input domain, though.
filesystem_file_observation_of_path(path: String) manually derives the parent with split/take/join. For /token, the parts are ["", "token"], so the computed directory is "" rather than /; the listing and read then observe different subjects. A one-component relative path has the same empty-parent problem instead of naming the current directory (or being explicitly refused). None of the new witnesses exercises this wet decomposition—they all construct FilesystemFileObservation directly—so the green suite cannot catch it.
Please move parent/name derivation behind one pure, typed/admitted path decomposition and add controls for nested absolute, root-level absolute, nested relative, and one-component relative paths; alternatively narrow the helper's accepted type so unsupported shapes are unwritable/refused before either host operation.
Also update the PR description: it still says filesystem_absence_establishment_adoption_standing is deleted, while this head keeps it with an empty roster under its still-open raw-operation trigger.
… host call
The wet helper split/take/joined the path operand inside the wet operation:
for /token the parent joined to the empty string, so the listing observed a
DIFFERENT subject than the read named (List("") vs Read("/token")), and a
bare operand decomposed to the same empty directory. No test executed the
decomposition.
filesystem_path_decomposition is now the one authority, computed before any
Filesystem.List or Read: it derives / for a root-level operand, derives .
for a dot-prefixed one, and refuses -- as FilesystemFileSubjectRefused with
no call attempted -- the empty operand, a bare entry name, an operand ending
in a separator, and a '.' or '..' cursor entry name, each with its own cause.
The wet operation holds no split/take/join path semantics; it matches the
decomposition and only a Decomposed result reaches the host calls.
Controls in test.claim.filesystem_file_observe_witness_test execute the
authority for /tmp/token, /token, target/token, and token, plus the refused
shapes; all ten pass under claim_batch --entry against the dag+src/v2 roots.
The emitter models source annotations at module-item grain only: the two comments I had placed inside the decomposition branch and the refusal arm parsed as 4 hard diagnostics (floor parse FAIL at lines 83/84/94/95, and the emit lane refused 00_compile.dag's closure with EmissionRefused). The root-derivation comment was already stated in the annotation above filesystem_path_decomposition, so it is deleted; the no-subject-fields note moves above filesystem_file_observation_of_path, where it belongs. No code changes; all ten witness controls still pass.
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Approved at 0b36ff0c71.
The requested repair is complete:
filesystem_path_decompositionis the single pure authority. The wet operation evaluates it as the match scrutinee before either host operation; the undecomposable arm returnsFilesystemFileSubjectRefusedand contains noFilesystem.ListorFilesystem.Read./tokendecomposes to directory/; nested absolute and relative paths preserve the directory/name subject; the baretokenpolicy is an explicit pre-I/O refusal, which was one of the allowed dispositions.- The wet operation contains no split/take/join path decomposition.
test.claim.filesystem_file_observe_witness_testdirectly executes the authority for/tmp/token,/token,target/token,./token, and the six refused shapes including baretoken, empty, trailing separators,.and..entry names.- The PR body now correctly says
filesystem_absence_establishment_adoption_standingremains with an empty roster under its still-open raw-operation trigger.
All four required jobs are green. No blocker.
…sence-establishment conversion
The composed run refused NonFoldResidueRosterDiverged stale=1: main's NFR census (#12980) added a FrontierRow for dag/gunbc/instruments/merge_admission_walk.dag::merge_target_refresh, but this PR's change already totalled that fold -- all six MergeAdmissionVerdict arms are spelled, no wildcard arm, so no non-fold residue exists for the subject and the roster row is stale on the composed tree. The row is deleted; roster and residue agree again. manifest_overlay_resolved was checked too: main added no row for it, and its three arms are totalled here, so nothing to delete there.
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Re-reviewed only the composed-tree delta since my approval at 0b36ff0.
Approved. fe4cfb3 is the merge of the previously approved head with main@26e99a9c7f; the only subsequent content commit, d5aca36, deletes exactly the stale merge_admission_walk.dag::merge_target_refresh FrontierRow. That deletion is correct at identity grain: MergeAdmissionVerdict has exactly six arms, and merge_target_refresh now spells all six (MergeAdmitted, stale-base, stale-roster, not-success, wrong-attempt, subject-mismatch) with no wildcard. The row therefore no longer describes a non-fold residue on the composed tree. manifest_overlay_resolved has no roster row to adjust. All four jobs are green on this head. No blocker.
|
On the reviewer's non-blocking note (the tracking row |
…d port #12982's citation Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ity; inline the keyring converge Side-chat findings on a560dca, both addressed: 1. The unreadable refusal overclaimed existence ('exists but could not be read') -- a failed read establishes nothing about what is on the disk. The record read now goes through #12982's filesystem_file_observation_of_path: a listing-established absence is its own AppKeyMintRecordMissing fact and its own AppKeyMintObservationMissing refusal (text makes no existence claim and the witness pins that); a record whose content could not be obtained stays AppKeyMintRecordUnread with text that no longer speaks of existence. app_key_mint_record_from_read is deleted -- the raw read it decoded no longer exists on this path. 2. approval_keyring_converge_with_staged_keys was an unrestricted top-level fn taking paths and contents separately. Inlined back into approval_keyring_converge_on_host, where each installed content is the content bound by that path's own successful read arm -- the two cannot diverge, and no unsealed caller exists. Witness: the unreadable red now drives the classifier with a FilesystemFileIndeterminate observation; the readable control drives it with FilesystemFileRead; the new missing-path control pins that the missing refusal says 'no record is there', that neither missing nor unreadable text contains 'exists', and that the three refusal texts are distinct. The listing-absence classifier arm is a one-line match the claim module cannot drive directly: FilesystemEstablishedAbsence is a sole_constructor of filesystem_io, not constructible from a test module.
1 participant
Empties the roster of
data filesystem_absence_establishment_adoption_standingindag/extdeps/filesystem/filesystem_io.dagby converting all six of its enumerated identities. THE ROW IS RETAINED, not deleted: an empty roster is not an expired trigger. The row's NEXT-RUNG TRIGGER names a capability — rawFilesystem.Read/Listprojections ceasing to be reachable outsidefilesystem_io's folds — and that capability still exists, so the row stays with an empty roster, a restoration note, and the same trigger (deleting it when its enumeration emptied rather than when the trigger expired was the mistake this PR repairs). Each site that concluded Absent from a FAILED read or a false shellTest.IsFilenow routes throughfilesystem_file_observation/filesystem_entry_presence, so could-not-look becomes typed refusal (FilesystemFileIndeterminate/FilesystemFileSubjectRefused) and only an unobserved listing establishes absence.Identities (6/6)
gunbc.host_effect_nbd_proxy_serve— session-token read rewritten as a 3-armBmcwebSessionTokenObservation(present-with-content / established-absent / indeterminate-with-cause); empty content is present-but-empty refusal, not Absent.gunbc.fleet_converge_plan_cli(observe_cap_members_wet) — already converted on main; verified by reading the site, not the row's claim.v2.workflow.product_receipt_stage— manifest/producer reads carryManifestUnobservable{cause}/ProducerUnobservable{cause}; pure boundary-standing functions.tools.merge_admission_walk— tested-subject and floor-receipt wire reads refuse asRefreshTestedSubjectWireUnreadable{cause}/RefreshFloorReceiptWireUnreadable{cause}instead of Absent.gunbc.codex_supervised_turn— generation-store read folds a listing+read through the observation; could-not-look answersGenerationStoreUnreadable→ turn start refused as duplicate-execution guard, where the old fail-open admitted.tools.opaque_realization_census—DeclarationBodyStandinggainsDeclarationSourceUnreadable{path, cause}; resolved-wins candidate scan keeps the happy path unchanged and carries the first recorded fault.Shared composition
Five of the six wet readers (1, 3, 4, 5, and product_receipt_stage's manifest read) now call ONE composition,
gunbc.filesystem_file_observe.filesystem_file_observation_of_path, instead of carrying verbatim copies. The helper fronts a PURE path-decomposition authority,filesystem_path_decomposition, computed BEFORE any host call: it derives the directory operand so the listing always observes the same subject the read names (/tmp/tokenlists/tmp;/tokenlists/— the root itself, not the empty string), refuses before any I/O the operands it cannot decompose (empty; bare entry name with no directory operand; trailing separator, which names a directory;./..cursor entry names), and refuses asFilesystemFileSubjectRefusedwith noListorReadattempted. No raw split/take/join path semantics remain inside the wet operation. Controls intest.claim.filesystem_file_observe_witness_testexecute the authority for/tmp/token,/token,target/token,token, and the refused shapes.fleet_converge_plan_clikeeps its own already-converted composition (it lists its directory once for many members, a different question), and consumers holding an admitted directory + admittedFilesystemEntryNamekeep their compositions too — re-decomposing a joined path would discard the admission.Sibling row
filesystem_read_outcome_adoption_standingre-measured at identity grain with a named instrument (/tmp/read_outcome_recount.py, calibrated at b21b710): 242Filesystem.Readbindings, 28 converted / 205 unconverted across 103 files (39 of the 205 are claim fixtures). Per DESIGN §6/§4c the row itself names the instrument and does not transcribe its output; the measured numbers are recorded in this PR's review-thread comment as session reporting.emitted_tree_read_thenconverted opportunistically (one binding, one fold).Verification
cargo build --release -p v1-compiler --bin claim_executor --bin gunbc).witnesseslane: the session runner (7.3 GiB, no swap) cannot hold a 7.2k-file corpus load (per-claimgunbc run, the witnesses lane, andclaim_batchare all OOM-killed at the corpus phases), so CI is the instrument.