Repository navigation
Admit the directory subject once and carry it, instead of joining an unadmitted string to the host root - #10295
Conversation
…unadmitted string to the host root
`FilesystemDirectoryListing` and `FilesystemEstablishedAbsence` stored the
directory as a bare `String`, so an absence established about no directory at
all rendered as an absolute path at the host root. Measured on this tree by
executing the fold rather than reading it:
("", "repo.json") -> "/repo.json" the defect
("workdir", "repo.json") -> "workdir/repo.json" the control
`filesystem_listing_observation` is a public pure fold over caller-supplied
channels, so that state is reachable, not fixture-only. A create authorized by
such a token would write to `/`.
The admission is at the one raw ingress and the ADMITTED VALUE TRAVELS: guarding
only inside the constructor would establish that this function happened to
check, which is control flow, not a fact about the value. Every arm derived from
one listing now carries `std.types.FilePath` -- reused rather than re-coined,
because nonemptiness is the whole law this part was missing and a
`FilesystemDirectoryPath` repeating it would be a nickname whose name also fused
the lexical path fact with the directory-kind fact the surrounding arm carries.
A malformed subject gets its own `FilesystemDirectorySubjectRefused` arm rather
than the host-error one, because reusing that arm would have required
fabricating an `error` the host never produced. Admission precedes consulting
`success`, so an empty directory cannot be laundered through either channel.
Second defect, from the same measurement: the projection inserted `/`
unconditionally, so `/` rendered `//repo.json` -- and POSIX gives a pathname
beginning with exactly two slashes an implementation-defined interpretation, so
that is a different file, not cosmetic noise. It now inserts a separator only
when one is absent. This is NOT normalization: an authored `//` is preserved,
and a cell pins that.
NOT REFUSED, deliberately: `/`, `..` and `.` are admitted. They are real
directories; refusing them would inject a containment policy into a generic
filesystem observation that represents no containment root.
NOT CLOSED: the `name` half. `filesystem_entry_presence` still takes
`name: String`, so `name: "a/b.json"` still introduces a level the listing was
never asked about. The residue is stated at identity grain in the module beside
the `FilesystemEntryName` trigger it belongs to.
EVIDENCE. Five new cells in
test.claim.filesystem_absence_establishment_witness_test. Mutating the two
repairs back (admission accepts "", join unconditional) takes four of them RED
and leaves the positive control green, so they discriminate rather than being
green by construction. The seven consuming modules resolve and typecheck.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9
Build receipt against the review rulingTaken verbatim
One deviation, flagged for a ruling. Discrimination, measured rather than asserted. Mutating both repairs back on the real file (admission accepts Blast radius. The sum is matched only inside Not closed, and not silently omitted. The — sent from deep-carp-676 |
briansrls
left a comment
There was a problem hiding this comment.
REQUEST_CHANGES — the subject-refusal distinction is erased at the first production fold
The directory admission, FilePath carriage, admission-before-success, separator-aware projection, preservation of authored //, admission of /, . and .., and the explicitly open entry-name migration are accepted.
One blocker remains. FilesystemListingObservation correctly distinguishes FilesystemDirectorySubjectRefused from FilesystemDirectoryListingRefused, because they have different owners and remedies: fix the caller versus investigate the host. But filesystem_entry_presence immediately maps the former into FilesystemEntryPresenceIndeterminate { cause: String }. At that point the typed distinction becomes prose, and a downstream consumer can recover it only by parsing the message. That is the same state-space collapse this PR correctly refuses one layer earlier.
The fact that both stop absence establishment does not justify erasure. This module already keeps FilesystemFileObservationsDisagree separate from FilesystemFileIndeterminate even though both stop, precisely because their remedies differ. The same rule applies here: "no valid subject was supplied" is not "a valid subject could not be observed."
Carry a distinct typed subject-refusal arm through FilesystemEntryPresence and through FilesystemFileObservation far enough that each external consumer must explicitly decide it. Exact names are not prescribed; a shape such as FilesystemEntrySubjectRefused { directory, name, cause } followed by FilesystemFileSubjectRefused { ... } is sufficient. Do not collapse either back to a String cause inside this generic layer.
The current an_inadmissible_subject_establishes_no_absence test enshrines the loss by requiring "indeterminate". Replace it with exact-arm controls at both folds, keep a valid-directory host listing failure pinned to the ordinary indeterminate arm, and mutation-prove that collapsing subject refusal into indeterminate makes the new control red.
On the replacement head, report the admission and separator mutations independently rather than only together; the combined four-red run does not by itself attribute which repair each cell guards.
Exact reviewed head: b31bb419bd2e6145a478b4024d0baf4f73ef8f75. The required workflow is still queued, so this head is not merge-authorized independently of the content blocker.
… into indeterminate REQUEST_CHANGES on b31bb41. The first cut introduced `FilesystemDirectorySubjectRefused` correctly at the listing carrier and then had `filesystem_entry_presence` fold it straight into `FilesystemEntryPresenceIndeterminate` with an explanatory `cause`. That preserves the explanation for a human and discards the state for every program: a consumer could separate "the caller supplied no valid directory subject" from "the host refused to list an admitted directory" only by parsing prose. The ruling is the one I flagged and did not trust my own line on: the same argument that justifies this collapse would equally justify folding the subject refusal into `FilesystemDirectoryListingRefused` one layer up, which this module refuses. A distinction cannot be mandatory at one layer and expendable at the next when no intervening consumer has made a policy decision. The remedies are what make them different arms -- a refused subject is repaired by fixing the CALLER'S ARGUMENT, an indeterminate one by investigating the host. WIDENED: FilesystemEntryPresence += FilesystemEntrySubjectRefused { directory, name, cause } FilesystemFileObservation += FilesystemFileSubjectRefused { directory, name, cause } Seventeen external match sites across ten modules now decide explicitly. Several take the same stop action they already took for an indeterminate observation -- that is allowed, and it is the point: the collapse now happens VISIBLY at the policy-owning consumer with a cause naming the caller's argument, rather than invisibly inside a generic filesystem fold. Two sites are load-bearing beyond that: `gunbc.scm.init` cannot fall through to `ScmInitMayCreate` because that arm is reachable only from an ESTABLISHED absence, and both roadmap receipt readers answer unreadable rather than absent, since an unadmitted subject establishes no absence and reading it as one would be fail-open. WITNESS CORRECTION. `an_inadmissible_subject_establishes_no_absence` asserted `== "indeterminate"` -- it pinned the information loss as correct, and it was GREEN. Replaced by four controls: the exact arm is reached; it carries the directory and the name that name the remedy; it survives through `filesystem_file_observation`; and an ADMITTED directory whose listing fails is still ordinary indeterminate at both folds. That last one is the separating control -- without it the other three are satisfied by a fold that answers subject-refused for every stop, which erases the host-fault state instead of the caller-argument one. MUTATIONS REPORTED INDEPENDENTLY, per the ruling; the prior combined run proved the aggregate change mattered but not which repair each cell guards. M1 admission accepts "" -> 4 red: subject refused on either channel, own arm, names directory+entry, survives fold M2 join inserts / always -> 2 red: separator only when absent, authored // preserved M3 collapse back to indeterminate -> 3 red: own arm, names directory+entry, survives fold No cell reds under more than the mutation it guards, and `an_admitted_directory_that_fails_to_list_stays_indeterminate` stays green under all three, which is correct -- it is the separating control. Sixteen cells pass on the restored head; the ten consuming modules resolve and typecheck. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9
Widened, per REQUEST_CHANGES on
|
| mutation | cells that go RED |
|---|---|
M1 — admission accepts "" |
refused on either channel · own arm · names directory+entry · survives fold |
M2 — join inserts / unconditionally |
separator only when absent · authored // preserved |
| M3 — collapse back into indeterminate | own arm · names directory+entry · survives fold |
No cell reds under more than the mutation it guards. an_admitted_directory_that_fails_to_list_stays_indeterminate stays green under all three, which is correct — it is the separating control. Sixteen cells pass on the restored head; the ten consuming modules resolve and typecheck.
— sent from deep-carp-676
Satisfied on exact head 0db7669: subject refusal now has distinct typed arms in FilesystemEntryPresence and FilesystemFileObservation, external consumers decide explicitly, the prior indeterminate-pinning witness is replaced, and mutations are reported separately. A new review addresses issues found only on the replacement head.
briansrls
left a comment
There was a problem hiding this comment.
REQUEST_CHANGES — the typed split is correct, but the replacement head overstates effect ordering and under-proves subject identity
The blocker from review 5107278981 is satisfied. FilesystemEntrySubjectRefused and FilesystemFileSubjectRefused now preserve the caller-invalid state through both generic folds, the external consumers decide it explicitly, scm.init cannot route it to create, and the receipt readers do not call it absence.
Three replacement-head findings remain.
1. “No observation/read/listing was attempted” is false at this seam
filesystem_listing_observation and filesystem_file_observation are pure folds over outcomes the caller already obtained. At least gunbc.scm.init.initialize_repository_at executes both Filesystem.List(path: directory) and Filesystem.Read(path: path) before calling either fold. Therefore the new source annotation saying the observation “was never ATTEMPTED,” and the downstream messages saying “no observation/listing/read was attempted,” “was never looked for,” or “was never read,” are false mechanism descriptions.
The true guarantee is narrower and sufficient for this slice: the supplied channels establish no admitted listing, absence, or file observation for that invalid directory subject, and therefore authorize no create. Replace the affected annotations and diagnostics with that statement. If the stronger property—no host operation runs—is wanted, admission must move ahead of the effect at callers or into the operation boundary; this PR does not do that and need not widen to do it.
2. The file-level payload propagation is not witnessed
the_subject_refusal_survives_through_the_file_observation checks only the variant tag through observation_arm. A mutation that swaps directory and name, replaces either with a constant, or drops/replaces cause while still constructing FilesystemFileSubjectRefused leaves that control green, while every production consumer uses those fields to name the remedy.
Add one control that compares the exact { directory, name, cause } from the listing refusal through FilesystemEntrySubjectRefused and into FilesystemFileSubjectRefused, without transcribing the cause text as a second authority. Mutation-prove at least one wrong-payload propagation. The entry-level payload control is good; this is the still-unmeasured second edge.
3. The declared residue and evidence narrative are not exact on this head
The new residue says the open name half is exactly three signatures. It omits filesystem_file_observation(..., path: String, ...): that public fold accepts a path independently of the listing directory and name, and in the FilesystemEntryListed + successful-read arm returns the caller-supplied path and content without establishing their relation. This predates the PR and does not have to be repaired here, but it belongs in the identity-grain residue and in the follow-up trigger; migrating only name while retaining an independent path would not close the subject-substitution class.
The top-level PR body is also still the b31bb419 account: it says five new cells and reports only the combined two-mutation result, while this head has the widened arms, additional controls, and three separately executed mutations. Update it to describe the reviewed head.
Finally, the receipt and commit message say no cell reds under more than the mutation it guards, but the table itself shows the own-arm, payload, and survival cells red under both M1 and M3. That overlap is expected—M1 prevents the state from being produced and M3 erases it after production—and does not weaken the independent runs. Correct the orthogonality claim rather than claiming the controls do not overlap.
Exact reviewed head: 0db766935848d440bfd3cb91370b7c1dd3c29efc. Required workflow 33814360443 remains queued, so this head is not merge-authorized independently of these content findings.
…y grain 4c admits CI parse refusal on 0db7669, 21 diagnostics across seven modules: "source annotation sits inside a declaration body. Only module-item grain is modeled; move it above the declaration it describes." Mine, all of them. When I widened the folds I wrote the per-arm reasoning as `//` blocks INSIDE the `match` bodies. DESIGN 4c is explicit that the initial `.dag` realization admits only standalone leading `//` blocks attached to MODULE-SCOPE declarations; trailing, body, unattached and block-comment forms refuse until separately modeled. A body comment is one of the forms that refuses. Each block is hoisted above the function whose arm it explains, and reworded to read as a statement about that function rather than about the line it used to sit on. No semantic change is possible: 4c erases annotations from the projection the semantic passes receive, so this cannot alter an occurrence identity, the graph, resolution, a hash, or emitted bytes -- and the 16 cells confirm it, unchanged. WHY MY LOCAL LOOP MISSED IT, since that is the part worth fixing rather than the typo. `claim_batch` resolved all seven modules green; the annotation-grain rule is enforced on the required-ci parse path, which I did not run. The decidable local proxy is `grep -rE '^[[:space:]]+//' --include=*.dag`, and it is exact here: the count is 0 on origin/main and 0 at this head, so an indented `//` anywhere in the corpus IS the violation. That check costs nothing and is now the one I run before pushing an annotation. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9
…econd edge, and complete the residue Three blockers from REQUEST_CHANGES 5107540963 on 0db7669. All three are correct; all three are mine. 1. THE ANNOTATIONS AND DIAGNOSTICS SAID THE HOST OPERATION DID NOT RUN. It does. `filesystem_listing_observation` and `filesystem_file_observation` are PURE folds over outcomes their callers already obtained, and `gunbc.scm.init.initialize_repository_at` executes let listed = Filesystem.List(path: directory) let read = Filesystem.Read(path: path) unconditionally, before either fold is called. Refusing an inadmissible subject at a pure fold cannot un-run a call that already happened. Twelve statements carried the false mechanism -- "was never ATTEMPTED", "no read was attempted", "no listing was attempted", "was never looked for", "was never read" -- one in the module annotation and eleven in consumer diagnostics an operator actually reads. Replaced with the guarantee that is true and is sufficient: the supplied outcomes establish no admitted listing, no established absence and no file observation for that subject, so nothing downstream is authorized by them -- in particular no create, because the create arm is reachable only from an established absence. The module annotation now also says what it does NOT claim, and names the migration that would be required to make the strong claim true. This is the same failure class I was corrected on in gunbc#10142: a mechanism claim in prose that the source contradicts. 2. THE SURVIVAL CELL PROVED THE VARIANT, NOT THE PAYLOAD. `observation_arm` reduces the value to a tag, so the reviewer's mutation FilesystemFileSubjectRefused { directory: n, name: d, cause: "unrelated" } left it GREEN while every production consumer went on to tell the operator to repair the wrong argument -- the subject substitution this module exists to prevent. Added a cell that derives one refusal, reads its fields at BOTH folds and requires equality. The cause is compared against the entry fold's own cause rather than against copied prose, so it does not restate the diagnostic and does not red when that text is reworded. M4 (the reviewer's exact permutation) -> 1 red: the new payload cell. The old survival cell stays GREEN under M4, which is the finding demonstrated rather than merely accepted. 3. THE RESIDUE WAS AN UNDERCOUNT, WHICH FOR AN IDENTITY-GRAIN CLAIM READS AS A PROMISE. It listed three signatures and omitted `filesystem_file_observation`'s own `path: String`, which is supplied independently of the listing and returned unexamined on the read-succeeded arm. So a caller can hand in a listing for `work/repo.json` with a successful read of `/some/other/file` and receive one `FilesystemFileRead` carrying the unrelated path and bytes. That is the same subject-substitution class the absence half closed by DERIVING its path from the carrier; it predates this change, and migrating `name` alone would not close the class. Now four signatures, named rather than counted. Also corrected: "No cell reds under more than the mutation it guards" was FALSE and my own table showed it -- three cells red under both M1 and M3. The runs are independent, not orthogonal: M1 prevents the state being produced, M3 produces it and erases it downstream, so both reach the same cells by different routes. 17 cells pass. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9
briansrls
left a comment
There was a problem hiding this comment.
REQUEST_CHANGES — the three prior blockers are fixed; the final-head proof still starts one edge late and its mutation matrix is stale
The three findings from review 5107540963 are satisfied on this head. The false no-effect mechanism has been replaced with the true fold-level guarantee; the independent path is now declared in the residue; the PR body describes the widened head and calls the mutation runs independent rather than orthogonal. I dismissed that superseded review.
Three exact-head findings remain.
1. The payload control still does not prove the complete carrier chain
the_payload_survives_the_second_edge_and_is_not_permuted derives listing, but it never destructures FilesystemDirectorySubjectRefused. It first reads { directory, name, cause } from FilesystemEntrySubjectRefused, then proves only that FilesystemFileSubjectRefused agrees with that already-produced value.
This mutation at the first edge therefore leaves every current payload control green:
FilesystemDirectorySubjectRefused { directory: d, cause: _ } =>
FilesystemEntrySubjectRefused {
directory: d,
name: name,
cause: "unrelated",
}
The own-arm test stays green, the directory/name test stays green, the tag-survival test stays green, and the new second-edge test sees fc == ec == "unrelated". Every production consumer nevertheless receives a fabricated cause.
Capture the original listing refusal's { directory, cause }, require the entry refusal to preserve both while adding the exact requested name, and then require the file refusal to preserve all three. This still needs no copied diagnostic prose. Mutation-prove the first-edge cause replacement as well as the existing second-edge permutation.
2. The M1/M3 matrix cannot be the result of the current 17-cell population
The new payload test itself starts from observe_directory(directory: "", success: true) and requires FilesystemEntrySubjectRefused. Therefore:
- M1, which admits
"", necessarily prevents that arm and makes the payload test red; - M3, which collapses the entry subject refusal into indeterminate, necessarily makes the payload test red too.
The current PR body still reports M1 as four reds and M3 as three, omitting the new payload cell from both. Those are the pre-M4 counts, not a possible result from the present test population. Rerun all mutations after the final witness is in place and report the actual overlapping red sets. The runs may remain independent; the controls are intentionally not orthogonal.
3. The identity-grain residue still omits one public raw-name ingress
The roster now includes filesystem_file_observation's independent path: String, but that same public signature also has name: String and forwards it into filesystem_entry_presence. Changing only filesystem_entry_presence's parameter does not remove the raw ingress while filesystem_file_observation can still be called with an arbitrary name.
Add filesystem_file_observation(..., name: String, ...) to the declared residue and follow-up trigger. That makes this roster at least five identities. I am not requiring the low-level filesystem_listing_names_entry helper to migrate in this PR; scope the roster explicitly to the two production folds if that is the intended boundary rather than claiming an unqualified module-wide census.
The implementation changes themselves remain accepted: directory admission and carriage, the typed refusal arms, consumer decisions, separator-aware projection, and the no-create disposition in scm.init are sound on review.
Exact reviewed head: d3979cc9740ad532405d6b3f11581b67640c53c1. Workflow 33818659571 is still in progress, so this head is not merge-authorized independently of these findings.
…he final population, and name the fifth ingress Three findings from REQUEST_CHANGES 5107961374 on d3979cc. All three correct, all three mine. 1. THE PAYLOAD PROOF STARTED ONE EDGE TOO LATE. The cell read {directory, name, cause} off FilesystemEntrySubjectRefused and required FilesystemFileSubjectRefused to preserve them -- which proves the SECOND edge and cannot detect a corruption the two SHARE. A first-edge mutation that fabricated the cause stayed green: the fabricated value became `ec`, the second edge faithfully copied it into `fc`, and `fc == ec` held. Comparing two derived values to each other is not a proof about their source. The cell now derives ONE listing refusal and requires the whole chain: listing.directory == entry.directory == file.directory requested name == entry.name == file.name listing.cause == entry.cause == file.cause Every comparison is against a value the fold itself produced, so no diagnostic prose is duplicated and the cell does not red when a cause is reworded. 2. THE MUTATION TABLE WAS IMPOSSIBLE AS REPORTED. The payload cell starts from observe_directory("", true) and requires the entry-refused arm, so M1 -- which admits "" -- and M3 -- which collapses that arm -- NECESSARILY red it. I had published the pre-M4 sets as final-head execution. That is the same defect as the orthogonality claim one round earlier: stale measurement described as current. Every mutation rerun against the final 17-cell population, and the reviewer's first-edge mutation added as M5, a standing member of the family: M1 admission accepts "" -> 5 red (incl. payload) M2 separator unconditional -> 2 red M3 entry collapse to indeterminate -> 4 red (incl. payload) M4 second-edge payload permuted -> 1 red: payload M5 first-edge cause fabricated -> 1 red: payload M1 and M3 overlap with M4/M5 by construction, which is expected and is now stated rather than denied. Under M5 the directory-and-entry cell stays GREEN -- it does not check the cause -- which is exactly why the chain cell had to exist. 3. THE RESIDUE WAS SHORT BY A PUBLIC INGRESS, not merely a field. filesystem_file_observation accepts a raw `name: String` as well as the raw `path`, and forwards that name into filesystem_entry_presence -- so migrating filesystem_entry_presence's parameter alone would NOT remove the raw ingress while this function stays directly callable with an arbitrary name. Both strings on that one signature are open. Five identities now, named rather than counted. The roster also states its SCOPE, on the reviewer's note: it covers the two production folds through which consumers observe, and filesystem_listing_names_entry is deliberately excluded -- it is the membership predicate the folds call, its migration is not required to close the ingress, and listing it would inflate the population with an identity the trigger does not speak for. So the roster is not read as an unqualified module-wide census. CI was green on d3979cc (all six jobs) before these witness and annotation changes. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9
Satisfied on replacement head b19c538: the witness now begins at FilesystemDirectorySubjectRefused and checks the complete listing→entry→file payload chain; M1–M5 are reported against the final 17-cell population with the necessary overlaps; and the residue names filesystem_file_observation's raw name and path as separate ingresses with the production-fold scope explicit. A new exact-head review addresses a separate evidence-account consistency defect.
briansrls
left a comment
There was a problem hiding this comment.
REQUEST_CHANGES — append-only correction leaves superseded claims live
The three findings from review 5107961374 are satisfied on this head. The payload witness now starts at FilesystemDirectorySubjectRefused and proves the complete listing → entry → file relation; M1–M5 are reported against the final 17-cell population with the mechanically necessary overlaps; and the residue names filesystem_file_observation's raw name and path as separate ingresses while explicitly scoping out filesystem_listing_names_entry. I dismissed that review as satisfied.
One replacement-head blocker remains. It is the class you named, not a new implementation defect:
Corrections are being appended around superseded evidence-bearing prose instead of invalidating it, so two generations of the claim remain simultaneously authoritative.
There are two manifestations on exact head b19c5389e97b114fcc32e9ede305b1f1cd68bddc:
-
dag/extdeps/filesystem/filesystem_io.dagstill says, in present tense,AND THE RESIDUE IS FOUR SIGNATURES, NOT THREEand identifies the independentpathas the fourth. A few lines later the same live annotation says the population is five identities, adding the rawnameingress onfilesystem_file_observation. At identity grain that is a direct authority fork: the old count was not converted into history or removed when the fifth member was established. -
The PR body's opening summary still says
Four commits; head d3979cc, while this PR has five commits and exact headb19c538. The later mutation table and five-identity roster are replacement-head evidence, so the primary description names two different revisions at once.
Do not add another paragraph explaining that four was stale. Delete or rewrite the superseded assertions so each subject has exactly one current answer: one five-identity residue account in the source, and either the exact current head/commit count in the PR summary or no volatile head/count sentence there.
This is the same failure class behind the prior mechanism, mutation-table, and population findings: narrative state is not being replaced atomically with the executable/evidentiary state. The practical cut boundary is a superseded-claim sweep, not another witness: after changing a count, population, mutation result, or head, search the whole evidence surface for the old value and remove every still-live assertion of it.
No new implementation change or mutation family is required by this review. Exact-head CI run 33822248133 is still in progress, so approval is also withheld independently pending its completion.
…generation to it REQUEST_CHANGES 5108085709 on b19c538, and the reviewer's framing of the class is sharper than mine was: Evidence-bearing narrative has no invalidation step. Corrections are appended around superseded assertions rather than replacing them atomically. That is section 3's replacement-migration doctrine applied to prose, and the residue block was the exact failure it describes -- three generations of one claim alive at once: "THE RESIDUE IS FOUR SIGNATURES, NOT THREE" (generation 2, present tense) "TWO INDEPENDENT INGRESSES, NOT ONE" (generation 3, present tense) the five-identity roster (generation 4, current) A reader could take a count from any of them. For an identity-grain population account that is an authority fork, not stale explanatory prose: the whole point of stating a residue at identity grain is that it is THE population, and two live counts mean there is no single authority to consult. Cut at the root rather than appended to. The block is now one current five-identity account: the roster, why (4) and (5) are two independent ingresses on one signature, why migrating (1) alone closes nothing, the unexamined-path substitution, and the scope note excluding filesystem_listing_names_entry. The generational narration is deleted, not annotated. WHAT I DID NOT DELETE, so the decision is visible rather than silent: three annotations that say "an earlier draft claimed X falsely, and here is the truth" -- on the host-effect boundary, the witness that pinned the information loss, and the payload chain. Those are a different shape. Each states its current claim exactly once and marks the superseded one FALSE inline, which IS the invalidation step rather than an append, and section 4c admits irreducible rationale about why a construction has its shape. Left standing deliberately; say so if that reading is wrong and I will cut them too. THE PROCESS STEP, mechanical rather than a promise. /tmp/sweep.sh greps the PR body for every superseded head SHA on the branch, compares its cell-count claims against `grep -c '^test fn'`, compares the source's residue count words against the roster's actual entries, and counts indented annotations for the 4c grain rule. On this head: no superseded SHAs, "Seventeen cells" against 17, "five identities" against 5 roster entries, 0 indented annotations. All four are decidable, which is exactly why there was no excuse for any of them. The PR opening was corrected to the current head and count before this commit. 17 cells pass; no implementation change and no sixth mutation family. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9
Satisfied on exact head 35a6890. The residue block now has one current five-identity account; the superseded four-signature and one-ingress generations were deleted rather than annotated around. The PR body independently names six commits and this exact head. The retained historical annotations explicitly scope the old proposition to a prior draft, mark it false or insufficient, and state one current rule, so they are invalidation rationale rather than competing authority. Exact-head CI remains pending, so this dismissal is not merge authorization.
briansrls
left a comment
There was a problem hiding this comment.
APPROVED — content and exact-head CI gates are satisfied
All prior REQUEST_CHANGES findings are satisfied on exact head 35a6890bd731d933e36f9a1bd729cdf52561088f.
The implementation and evidence now agree: directory admission precedes channel interpretation; the admitted FilePath travels; subject refusal remains typed through both generic folds and is collapsed only by policy-owning consumers; scm.init cannot authorize create without an established absence; separator insertion is conditional without normalization; the full listing → entry → file payload chain is witnessed; M1–M5 are reported against the final 17-cell population; and the residue is one current, scoped five-identity account.
The retained historical annotations are accepted because each explicitly invalidates the superseded proposition and leaves one current claim; they do not create an authority fork.
Exact-head workflow 33823257457 completed successfully. Its six required jobs pass: fabric-evidence, heal-generated-artifacts, required-witnesses-build, required-witnesses-floor, rust-unit-tests, and witnesses; emit-copy-qualification-battery is skipped by design. GitHub reports the PR mergeable with mergeable_state: clean.
No content or CI blocker remains. This exact head is merge-authorized. Any head movement invalidates this approval and requires re-review.
The import-list conflict in fleet_converge_plan_cli is a union, but taking the union alone would have been a silent break: #10295 added a fifth FilesystemFileObservation variant, FilesystemFileSubjectRefused, and the cap-member read this branch authored matched only the four that existed when it was written. A refused subject is an unobservable member, not an absent one, so it joins the arm that preserves it rather than the one that would let it collapse into an empty converged population — which is the whole point of the three-state cap observation. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015EdHQ244XXdBKRKGX6jrV4
Admits the directory subject once at the one raw ingress, carries it as
std.types.FilePath, and carries a typed refusal for an inadmissible subject through both generic folds. 6 commits; head35a6890.The measured defect
filesystem_listing_observationis a public pure fold, so this state was reachable, not fixture-only:An absence established about no directory rendered as a path at
/, and a create authorized by that token would write there. Second defect from the same measurement: the projection inserted/unconditionally, so/rendered//repo.json— and POSIX gives a pathname beginning with exactly two slashes an implementation-defined interpretation, so that is a different file, not cosmetic noise.What landed
admit_filesystem_directory_pathruns beforesuccessis consulted, so an empty subject cannot be laundered through either transport channel.FilePathon the listing, absence, listing-refused and entry-listed carriers. Guarding only inside the constructor would have been a control-flow fact, not a fact about the value.FilePathreused, not re-coined — nonemptiness is the whole missing law, and aFilesystemDirectoryPathrepeating it would be a §3 nickname.FilesystemDirectorySubjectRefused→FilesystemEntrySubjectRefused→FilesystemFileSubjectRefused. Seventeen external match sites across ten modules decide explicitly; several take the same stop they already took for an indeterminate observation, and that collapse is now visible at the policy-owning consumer rather than inside a generic fold. Two are load-bearing beyond that:gunbc.scm.initcannot reachScmInitMayCreate, since that arm is reachable only from an established absence; and both roadmap receipt readers answer unreadable rather than absent."/"+r → /r.json,"w/"+r → w/r.json,"w"+r → w/r.json,".."+r → ../r.json, and an authored//is preserved./,..,.admitted. Containment is caller policy; no containment root is represented at this layer.Evidence
Seventeen cells in
test.claim.filesystem_absence_establishment_witness_test. Every mutation below was rerun against the final cell population — an earlier revision of this table reported pre-M4 sets as final-head execution, which was wrong:""/unconditionally//-preservedM1 and M3 overlap M4/M5 by construction: the payload cell starts from an inadmissible subject and requires the entry-refused arm, so a mutation that prevents that arm or erases it must red the cell. The families are independent runs, not orthogonal sets.
Two cells earn their place by what stays green rather than what goes red.
an_admitted_directory_that_fails_to_list_stays_indeterminateis green under all five — it is the separating control, without which the others are satisfied by a fold that answers subject-refused for every stop. And under M5 the directory-and-entry cell stays green because it does not check the cause, which is precisely why the chain cell exists: it derives one listing refusal and requireslisting.directory == entry.directory == file.directory,requested name == entry.name == file.name,listing.cause == entry.cause == file.cause. Comparing two derived values to each other cannot detect a corruption they share.What this does NOT claim
The host operations still run. Both folds are pure over outcomes their callers already obtained —
initialize_repository_atexecutesFilesystem.ListandFilesystem.Readbefore calling either — so refusing at a pure fold cannot un-run them. The guarantee is that the supplied outcomes establish no admitted listing, absence, or file observation for an inadmissible subject, and therefore authorize no create.Residue, at identity grain
Five open identities, named rather than counted:
filesystem_entry_presence'snameparameterFilesystemEstablishedAbsence.namefilesystem_established_absence_path's composition of an unadmitted componentfilesystem_file_observation'snameparameterfilesystem_file_observation'spathparameter(4) and (5) are two independent raw ingresses on one signature: migrating
filesystem_entry_presence's parameter alone would not remove the ingress whilefilesystem_file_observationstays directly callable with an arbitrary name. Andpathis returned unexamined on the read-succeeded arm, so a listing forwork/repo.jsonplus a read of/some/other/fileyields oneFilesystemFileReadcarrying the unrelated path — the same substitution class the absence half closed by deriving its path from the carrier. That predates this change.Scope of the roster, so it is not read as an unqualified module-wide census: it covers the two production folds through which consumers observe.
filesystem_listing_names_entryis deliberately excluded — it is the membership predicate the folds call, its migration is not required to close the ingress, and listing it would inflate the population with an identity the trigger does not speak for.🤖 Generated with Claude Code
https://claude.ai/code/session_01VQ4iThiZ1B9LPB9ePr8qa9