Repository navigation
read-outcome adoption, gunbc/auth batch: a refused read is a typed outcome, never a defaulted none - #13106
Conversation
…tcome, never a defaulted none filesystem sibling of DP-M5; converts all 8 unconverted Filesystem.Read consumption sites in dag/gunbc/auth to the modeled fold filesystem_read_outcome (extdeps.filesystem.filesystem_io), per the row filesystem_read_outcome_adoption_standing: - ci_app_key_rotation: THE RED -- an unreadable observation record collapsed into the absent arm (silent none, same as env-unset). Now observe_app_key_mint_record returns AppKeyMintRecordRead? via app_key_mint_record_from_read; a refused read is a new typed refusal AppKeyMintObservationUnreadable, distinct from Absent (which now means only 'env unset'). Red witness + positive controls appended to dag/test/claim/ci_app_key_rotation_witness_test.dag. - credentials, approval_gate, approval_keyring_converge, access_token_source, profile_projection (new on main): manual if/else and match-on-success routed through the fold; refusal texts preserved verbatim; classify_supplied_token now takes FilesystemReadOutcome. Instrument (named re-runnable, per the row's RE-DERIVATION): tools/read_outcome_recount.sh, identity grain; calibrated -- at b21b710 it reproduces the row's recorded baseline exactly (92 sites / 48 files, 0 converted), and at DP-M5's head 6471587 it agrees with the final-semantics recount (207 raw unconverted / 43 dag/test/claim fixtures / 98 files). Sites whose projections all feed filesystem_exact_read are reported as their own class (exact_read_typed): already typed outcomes, not this debt. After this batch: 219 unconverted (44 dag/test/claim fixtures, 175 non-fixture) across 100 files; was 227/183/106 at fresh main 0456f1c.
…trument header carries method, not transcribed counts
The bare record literal as a match-arm body did not parse ('expected
expression, found Colon'), which made every later comment in the module
report 'source annotation names no subject' (37 CI parse errors). The
Refused arm now binds refused_file and returns it.
tools/read_outcome_recount.sh header: calibration numbers were
transcribed output in prose (DESIGN section 6); the header now carries
the method only, and the numbers live where the count is used (the PR
carrying the row update).
|
Addressing review 38602 (dashboard review artifact): Finding 2 (transcribed counts in the tool header) — fixed in cf5d322: the header now carries the method only; calibration numbers live where the count is used (this PR's description), per DESIGN §6's name-the-instrument rule. Finding 1 (unmodeled shell instrument) — agreed, and this is the blocking item. Verified against the current code: the reviewer's reading of §6 is right that a hand-written shell parser is on the scaffold tell list ('raw shell implementing semantics already expressible in .dag'), and the row now names it, which raises the stakes exactly as described. The durable fix is the .dag instrument, not a marker: the substrate already has the modeled shape this census needs (v2.std.decl_index decl_facts carries every declaration with its node; v2.std.node_query has the field-projection shape; v1_consumer_discovery is the precedented tools.* template), so 'expressible in .dag' is satisfied and the shell has no dissolution story worth defending. I am building the census as a .dag instrument (module tools.read_outcome_census, a gunbc-test label) and will replace the shell: the shell gets deleted once the .dag instrument lands in this PR (delete-first, no parallel authorities), and the row's RE-DERIVATION will name the .dag instrument. Identity grain moves from path:line to declaration identity, which is strictly stronger; the b21b710 anchor is recalibrated with the .dag instrument and the deltas from the text-grain numbers are reported in this PR, not hidden. One scope note, stated plainly: a faithful census needs the binding→projection→fold-argument relation, which is structural, so the instrument walks nodes and edges (NodeFold), not just atom lexemes like v1_consumer_discovery; its whole-corpus run is CI-verified (session runners OOM on whole-corpus .dag runs, per the trial lessons). Calibration at b21 runs the same way. |
Per review 38602 finding 1 and the trial parent's ruling: a hand-written
shell parser is DESIGN section 6 scaffold ('raw shell implementing
semantics already expressible in .dag'), and the row must not name it.
The census moves to its own PR as a .dag instrument
(tools.read_outcome_census over decl_facts/NodeFold, gunbc-test label,
recalibrated at b21b710 with text-grain to node-grain deltas reported
there); the row will name it when it lands. The batch's population
delta in this PR's description is produced by the row's existing
RE-DERIVATION recipe as it stands on main.
…content params in the extracted converge The conversion's fold calls referenced filesystem_read_outcome and the two arm names without importing them, and the extracted approval_keyring_converge_with_staged_keys still read the caller's cap/sub/rcpt records instead of its own staged-content parameters. Both resolution failures are fixed; the extracted body now consumes the typed read outcomes its caller decoded.
briansrls
left a comment
There was a problem hiding this comment.
Reviewed closely at a560dca836.
The ordinary adoption edits are correct: access-token classification preserves both prior SuppliedTokenUnavailable texts and has no stale caller; approval filing preserves its unreadable-key refusal; credentials preserves GcpAdcReadRefused with the host error; profile projection still records an explicit ProfileStoreSkipped { reason: "read failed: ..." }; and the keyring caller maps cap/sub/receipt paths and contents to the matching parameters in the original refusal order (receipt, capability, submission). The seven-file diff also confirms the recount shell script is not in this PR.
Two things block approval:
-
AppKeyMintObservationUnreadableclaims a fact the selected fold cannot establish.filesystem_read_outcomehas onlySucceededandRefused; everysuccess=falseresult reachesFilesystemReadRefused, including a missing path, an unsearchable parent, permission denial, and ordinary I/O failure. Butapp_key_refusal_textsays the observation record “exists but could not be read.” A setAPP_KEY_VERIFY_RECORDpointing at a nonexistent file will therefore produce a plausible but false existence claim. The conversion should say only what is known — e.g.AppKeyMintObservationReadRefused/ “the record path was supplied but the read failed: …” — or use the host failure-kind/exact-read or listing observation if the model genuinely needs absent versus present-but-unreadable. Add a missing-path control; the current witness exercises onlypermission deniedand cannot catch this overclaim. -
The extracted keyring success continuation is now an unsealed top-level actuation entry. Before extraction, the install sequence was lexically reachable only after all three successful-read arms.
approval_keyring_converge_with_staged_keysis now importable with noadmit_callers, accepts the three paths and three contents as independentStrings, verifies digests of the paths, and then installs the independently supplied contents. Another declaration can call it with paths to valid staged files (digest checks pass) and unrelated content strings, bypassing every new read-outcome refusal. The current caller’s parameter mapping is correct, so the earlier stale-local defect is fixed; the new global call surface is the issue. Inline the continuation again, or caller-seal it toapproval_keyring_converge_on_hostand carry path/content pairings in a construction that can only be minted from the threeFilesystemReadSucceededarms.
All four CI lanes are green, but neither issue is a compile-time failure in the current shape.
…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.
…ctors explicitly review 75025: app_key_mint_record_from_observation used FilesystemFileObservation and its five constructors with no import. They do resolve implicitly (the scoped compile passed with only the pre-existing secret_rotation error, and merge_admission_walk on main matches the same arms without importing them), but the sibling files in this diff and the witness import these names explicitly, so the module now does too.
|
Fixed on 930b969: the One factual note for the record: the six names did resolve before this commit — the scoped |
briansrls
left a comment
There was a problem hiding this comment.
One blocker remains.
The keyring bypass is fixed: the helper is gone, and each installed payload is now lexically bound from the corresponding FilesystemReadSucceeded arm in approval_keyring_converge_on_host. I found no remaining way to pair an independently supplied path with independently supplied content there.
The mint-record observation model is also the right shape: env-unset, listing-established absence, and could-not-observe are distinct; raw Read decoding is gone; the FilesystemFileAbsent arm carries the sealed absence fact rather than inferring absence from a failed read.
But the new "missing-path control" does not exercise that new FilesystemFileAbsent -> AppKeyMintRecordMissing mapping. It constructs AppKeyMintObservationMissing directly and tests only refusal rendering. The comment says the classifier arm cannot be driven because FilesystemEstablishedAbsence is sole_constructor; the seal prevents hand-minting the token, not deriving it through its owner.
Please drive the arm through extdeps.filesystem.filesystem_io's public producers: filesystem_listing_observation with a successful listing whose entries omit the record name, then filesystem_file_observation with that listing + the matching name/path + a refused read. That produces FilesystemFileAbsent through the sole constructor's owning route; feed the resulting observation to app_key_mint_record_from_observation and assert AppKeyMintRecordMissing, ideally also pinning its rendered refusal against the unreadable arm.
That is stronger than constructing the sealed carrier and tests exactly the semantic link this PR adds. Existing filesystem witnesses use this pattern for the same reason. Once that control lands, I have no other blocker at this head.
… records the excluded classes Side-chat finding: the missing-path control constructed AppKeyMintObservationMissing directly and only checked rendering, so the FilesystemFileAbsent classifier arm was never exercised. The new control drives the full chain with no forged carrier: filesystem_listing_observation (succeeded listing omitting the record) plus a refused read go through filesystem_file_observation -- the sole_constructor absence is produced inside filesystem_io -- and the witness pins AppKeyMintRecordMissing from the mint classifier and the rendered AppKeyMintObservationMissing text (no existence claim). Row: the exact_read_typed exclusion was lost when the RE-DERIVATION prose was restored in 6e0af31; both it and the new domain_read_fold class are now recorded on the row. domain_read_fold covers sites routing raw reads through a domain fold of the same shape (machine_intake proc_read_outcome -> ProcRead | ProcReadRefused, carrying error_kind): typed outcomes, excluded from this lane; the second read-outcome fold is a DESIGN 3 fork to be unified by growing the shared fold. In-scope population at current main: 139 sites across 70 files (161 non-fixture before exclusions).
briansrls
left a comment
There was a problem hiding this comment.
Approved at fd6f322.
The remaining blocker is resolved at the requested grain. The new control does not forge FilesystemEstablishedAbsence: it supplies a successful directory listing that omits observation.json and a refused read to filesystem_file_observation. That owner-side fold necessarily produces FilesystemFileAbsent; app_key_mint_record_from_observation then must produce AppKeyMintRecordMissing, and the control checks the final AppKeyMintObservationMissing rendering says “no record is there” without claiming that anything “exists.” This now exercises the exact production link that the prior direct-construction control missed.
The adoption-row edit is also acceptable. It names exact_read_typed as already using the canonical typed outcome and domain_read_fold as already preserving success/refusal through ProcRead | ProcReadRefused. Crucially, it does not present the latter as closure: it records the second fold as a DESIGN §3 fork, preserves error_kind as the reason it cannot simply be replaced here, and makes later unification into the shared fold the disposition. The existing next-rung trigger still requires the raw projections to become reachable only through the shared filesystem_read_outcome, so this exclusion does not falsely retire the fork.
Post-930b969 history is one commit changing only the witness and the standing row. Exact-head CI passed floor, generated, emit-build, and aggregate witnesses.
Nonblocking PR-body cleanup: the RED-witness paragraph still says the FilesystemFileAbsent classifier arm “cannot be driven directly” from the claim module. The final tree now correctly drives it indirectly through the owner’s public producers; update that sentence to match the landed evidence before merge.
# Conflicts: # dag/extdeps/filesystem/filesystem_io.dag
Debt paydown: read-outcome adoption — the filesystem sibling of DP-M5 (#12982). Converts all 8 unconverted
Filesystem.Readconsumption sites indag/gunbc/authto typed read outcomes (extdeps.filesystem.filesystem_io), per the rowfilesystem_read_outcome_adoption_standing.THE RED — ci_app_key_rotation.dag:389.
observe_app_key_mint_recordreturnednonewhen the observation record could not be read — the same value as when the record env var is unset. A refused read silently read as "no record". After this PR the observation is a typed outcome with its facts kept apart:filesystem_file_observation_of_path) →AppKeyMintRecordMissing/ refusal armAppKeyMintObservationMissing;AppKeyMintRecordUnread/AppKeyMintObservationUnreadable— text makes no existence claim (side-chat finding: a failed read establishes nothing about what is on the disk);AppKeyMintRecordDecoded.AppKeyMintObservationAbsentnow means only "env unset".app_key_mint_record_from_read(the raw-read decoder from the first revision) is deleted — the raw read no longer exists on this path.RED witness:
dag/test/claim/ci_app_key_rotation_witness_test.dag::an_unreadable_mint_record_is_refused_as_unreadable_never_collapsed_into_absentdrives the classifier with aFilesystemFileIndeterminateobservation (the classifier does not exist on main — the witness goes red there). Positive controls: the readable observation still decodes (FilesystemFileRead→ status 200), and the missing-path control pins that the missing refusal says "no record is there", that neither the missing nor the unreadable text contains "exists", and that the three refusal texts are distinct. The listing-absence classifier arm (FilesystemFileAbsent→ Missing) is a one-line match the claim module cannot drive directly:FilesystemEstablishedAbsenceis a sole_constructor of filesystem_io, not constructible from a test module.The other 7 sites (each read individually, none pattern-matched):
credentials.dag:76— GCP ADC:match read.success→ fold match; refusal staysGcpAdcReadRefused(cause verbatim).approval_gate.dag:254— submission MAC key: manual if/else → fold match;ApprovalFilingRefusedreason text preserved verbatim.approval_keyring_converge.dag:244-246— three staged MAC keys (receipt, capability, submission, checked in that order): refusal texts preserved verbatim. An intermediate revision extracted the success continuation into a top-levelapproval_keyring_converge_with_staged_keys; review found that to be an unsealed bypass (paths and contents as independent parameters). Inlined back intoon_host— each installed content is the content bound by that path's own successful read arm, so the two cannot diverge, and no unsealed caller exists.access_token_source.dag:240—classify_supplied_tokentakes the typed read outcome instead of raw projections; bothSuppliedTokenUnavailablecauses preserved verbatim.profile_projection.dag:376(new on main) — profile-store read: fold match;ProfileStoreSkippedreason text preserved verbatim.Instrument ruling and delta. An interim checked-in shell recount (
tools/read_outcome_recount.sh) was deleted per the trial parent's ruling (a.dagcensus overdecl_facts/NodeFoldbelongs in its own PR; the row's RE-DERIVATION prose is restored to main's text). The recount reported here was produced by that recipe and calibrated at the row's baseline commit b21b710 (92 sites / 48 files, 0 converted — exact agreement).Population delta at identity grain (same recipe, recounted at current main a0e8a12, which has since converted sites itself):
dag/gunbc/authrows remain after it.Verification (scoped
gunbc compile --entry, remote, target rust):dag/gunbc/auth/ci_app_key_rotation.dag,dag/gunbc/auth/approval_keyring_converge.dag, and the witness module each compile with only pre-existing errors in modules this PR does not touch (secret_rotation.dag:731"unprojectable construct", last touched #12969;extdeps/gunbc/gunbc.dag:108-110shell-transport stderr channels, untouched by this PR). Every module touched by the PR was scope-compiled — lesson from review 38602, which caught what a witness-closure-only check missed. No whole-corpus .dag run was performed (session runners OOM); CI's witness lane is the verifier.Not done here (deliberately): the
exact_read_typedsites (8 at DP-M5 head) are already typed outcomes and are excluded per the ruling recorded on the row. Finding, recorded ON THE ROW as typed excluded classes (review 75126): the exclusion classes are no longer prose —FileSystemReadOutcomeExcludedClasscarries them as constructors (FileSystemReadOutcomeExactReadTyped,FileSystemReadOutcomeDomainReadFold) andfilesystem_read_outcome_adoption_excluded_classesenumerates them; the census instrument must classify every non-target site into one of these and refuse an unclassified site.domain_read_foldcovers sites routing raw reads through a domain fold of the same shape (machine_intakeproc_read_outcome→ProcRead | ProcReadRefused, carryingerror_kind): typed outcomes, not silent defaults, excluded from this lane. The second read-outcome fold is a DESIGN 3 fork whose next-rung trigger is now named on the row (§4b(2)): the shared fold's refused side grows an admitted error-kind projection — the one factproc_read_outcomeholds thatfilesystem_read_outcomelacks — after which the machine_intake sites re-express through it and the class retires; the owner isextdeps.filesystem.filesystem_io, which owns the fold that must grow. The row's REMAINDER is re-measured at this head (fd6f322, same recipe and grain as the baseline): 215 unconverted consumption sites across 138 files, of which 63 aredag/test/claimfixtures excluded from the target by the classes, not by the count. With both excluded classes applied, the in-scope population is 139 sites across 70 files (161 non-fixture at current main before exclusions; 22 of them are the machine_intake domain fold). Remaining subsystem batches: roadmap (25), instruments (22), fleet (19), src (9).