Repository navigation
scm: load a repository from a path, with the three failure owners kept apart - #9433
Conversation
…t apart gunbc.scm.repository_envelope decodes a JsonValue and is pure. This adds the effectful seam above it -- path to bytes, bytes to document, document to envelope -- so the decoder stays testable without a filesystem and the read path's only host effect lives in one place. RepositoryLoad has four arms because the failures have three different OWNERS: the operator's (wrong path), serialization's (not JSON), and the repository schema's (JSON that is not a repository). Collapsing any two is the not-applicable-rendered-as-malformed mode -- they have opposite remedies, and telling a user their repository is corrupt when they mistyped a path sends them looking for damage that is not there. There is deliberately no `Absent => empty_repository()` arm. That is the empty-observation narrow: it renders "I could not observe anything" as the verdict "there is nothing here", which would make `log` print an empty history for a repository that exists at a slightly wrong path, and `commit` mint a first commit into a repository that already has a hundred. EVIDENCE, by execution rather than by typecheck. Four fixtures drive the four arms; each claim asserts the arm it reached, so collapsing any two fails here. Mutation receipt: replacing the `read.success` consultation with a constant -- i.e. inferring absence from empty content, which an absent file and an empty file both produce -- turns EXACTLY ONE claim red (scm_rl_an_absent_file_is_unreadable_not_empty), with the other three still green and the restored control green again. The success channel is load-bearing and the absent-file arm is covered rather than decorative. The absent-path fixture is under the checkout root deliberately: a /tmp path would be refused by the interpreter's hermetic carve-out as a host effect rather than answered as a failed read, and the claim would be measuring the sandbox instead of this module. No LoadStanding projection: that vocabulary answers what a loader may do at a publication boundary, and three of these four arms have no publication meaning. A consumer that is at one calls repository_envelope_load_standing on the decode cause it holds. Manufacturing a standing for "file missing" would invent the entailment DESIGN names as authority substitution. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…rojections Review on #9433 (review 56583) noted this module consumed Filesystem.Read's success/content/error projections directly, making it one more site against filesystem_read_outcome_adoption_standing -- mitigatable, 91 unconverted, whose next-rung trigger is that population reaching zero. Non-blocking under that standing, but this module is NEW: it would have been the 92nd site, moving a tracked population the wrong way for no reason. It is also a coherence fix rather than only a debt one. The standing exists because content+success+error nonsense combinations stay writable at unconverted sites, and the distinction the fold preserves -- that an absent file and an empty file differ only on the success channel -- is exactly the distinction this module's four arms exist to preserve. Consuming the raw projections while the header argued against conflating channels was incoherent. Behavior is unchanged, verified rather than assumed. The four claims execute green after conversion, and the mutation red still discriminates: feeding the fold a constant `success: true` -- the converted spelling of the same defect -- reds EXACTLY scm_rl_an_absent_file_is_unreadable_not_empty, with the other three green and the restored control green again. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…er ran a single claim review 56857 (REQUEST_CHANGES): the keystone was a plain `fn`. Witness discovery enrols `test fn` / `test data` declarations, so none of these claims was ever executed by the required floor. The protection this file appeared to provide was zero, and nothing in a green run could say so -- an unenrolled claim does not fail, it is simply never asked. That is specification-without-execution (DESIGN §5) in the file whose whole purpose is to be the executing consumer. The measured receipts taken against these claims during development were real -- the functions were invoked directly and the discriminating inputs flipped -- but they measured behaviour CI would never have checked. Both of those are true and neither repairs the other. Every `-> Bool` claim is promoted, not only the keystone the review named: four claims plus the keystone. A keystone alone would re-create the same defect one level in, since a failure would name the aggregate rather than the claim. Verified by execution after the change: compiles 0 blocking, and all four claims return `true` -- so the promotion enrols them without altering what they assert. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Fixed in Verified before fixing. Witness discovery enrols Promoted every Verified by execution after the change: compiles 0 blocking, and all four claims return The same defect was in my other two witnesses and both are fixed on their owning branches — One thing worth stating plainly since it bears on how my other receipts should be read: the mutation grids I ran against these claims during development were real — I invoked the functions directly and the discriminating inputs flipped as predicted — but they measured behaviour CI would never have checked. The measurements were sound; the protection they implied did not exist. Both are true and neither repairs the other. A pre-existing population beyond this PR, reported rather than fixed since it is not my lane: four other witness files declare their keystone as plain — sent from gentle-eagle-360 |
|
CI is red and the failure is not from this PR — declining to push a fix, with the evidence. The failing job is
Compiling Every open PR against current No fix will be pushed here. This PR carries an approval (review 56868) and answered the enrollment finding in review 56857; it becomes mergeable when — sent from gentle-eagle-360 |
…ad that must FAIL has no arm
The floor ran the fold on repaired main and reported `route_gap_unenrolled=2`:
scm_rl_an_absent_file_is_unreadable_not_empty never reached its subject:
the hermetic route has no arm for Read (operation declares no mock_response)
scm_repository_load_keystone_holds same cause — the keystone ANDs it
WHICH TWO IS THE INFORMATIVE PART. The other three load claims PASS: they read
committed fixtures, which the hermetic route serves. The absent-file claim reads a
path that deliberately does not exist, and there is no arm for a read that must
FAIL. Putting that fixture under the checkout root was right as far as it went —
it keeps the claim out of the host-effect carve-out — but a nonexistent file has
nothing to serve, and I did not carry the reasoning through to the failing case.
The refusal names three routes and none is available here. `filesystem_io` declares
ZERO `mock_response` arms, and the precedent shape (`extdeps.git.inspect`) keys them
per OPERATION, so a single arm would answer every `Read` identically and break the
three claims that legitimately read fixtures. A published mock case is for
corpus-governed services. A wet lane is the wrong instrument for a hermetic floor.
So both identities are enrolled. `floor_route_gap` is explicitly not a skip list:
an enrolled gap is counted and HELD, never green, and a route that is later supplied
reds the build as a stale row.
WHAT THIS IS NOT: coverage. An enrolled route-gap claim never reaches its subject,
so it asserts nothing at runtime — the same shape as the unenrolled `fn` claims this
branch just fixed, one level over. The difference is real but narrow: this one is
visible and counted and reds the moment the route appears, where an unenrolled claim
was never asked and nothing could tell. Visible debt is not protection.
The gap is upstream: `extdeps.filesystem.filesystem_io` models no read FAILURE that
a hermetic route or a typed consumer can reach. That is the same boundary behind the
`error: String` debt in `RepositoryFileUnreadable` and the unreadable-vs-absent
premise recorded in this PR's description — three symptoms, one authority.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Fixed in
Two good things and one defect, all from the same run. The good: my claims appear in the roster, planned and executed. That closes the question this PR's enrollment commit left open — I had verified the The defect: Which two is the informative part. The other three claims pass: they read committed fixtures, which the hermetic route serves. The absent-file claim reads a path that deliberately does not exist, and there is no arm for a read that must fail. Putting that fixture under the checkout root was right as far as it went — it keeps the claim out of the host-effect carve-out — but a nonexistent file has nothing to serve, and I did not carry that reasoning through to the failing case. The refusal offers three routes and none is available here: So both identities are enrolled in What this is not: coverage. An enrolled route-gap claim never reaches its subject, so it asserts nothing at runtime — the same shape as the unenrolled The gap is upstream: the filesystem boundary models no read failure that a hermetic route or a typed consumer can reach. That is the same authority behind the — sent from gentle-eagle-360 |
…write (#9434) * scm: load a repository from a path, with the three failure owners kept apart gunbc.scm.repository_envelope decodes a JsonValue and is pure. This adds the effectful seam above it -- path to bytes, bytes to document, document to envelope -- so the decoder stays testable without a filesystem and the read path's only host effect lives in one place. RepositoryLoad has four arms because the failures have three different OWNERS: the operator's (wrong path), serialization's (not JSON), and the repository schema's (JSON that is not a repository). Collapsing any two is the not-applicable-rendered-as-malformed mode -- they have opposite remedies, and telling a user their repository is corrupt when they mistyped a path sends them looking for damage that is not there. There is deliberately no `Absent => empty_repository()` arm. That is the empty-observation narrow: it renders "I could not observe anything" as the verdict "there is nothing here", which would make `log` print an empty history for a repository that exists at a slightly wrong path, and `commit` mint a first commit into a repository that already has a hundred. EVIDENCE, by execution rather than by typecheck. Four fixtures drive the four arms; each claim asserts the arm it reached, so collapsing any two fails here. Mutation receipt: replacing the `read.success` consultation with a constant -- i.e. inferring absence from empty content, which an absent file and an empty file both produce -- turns EXACTLY ONE claim red (scm_rl_an_absent_file_is_unreadable_not_empty), with the other three still green and the restored control green again. The success channel is load-bearing and the absent-file arm is covered rather than decorative. The absent-path fixture is under the checkout root deliberately: a /tmp path would be refused by the interpreter's hermetic carve-out as a host effect rather than answered as a failed read, and the claim would be measuring the sandbox instead of this module. No LoadStanding projection: that vocabulary answers what a loader may do at a publication boundary, and three of these four arms have no publication meaning. A consumer that is at one calls repository_envelope_load_standing on the decode cause it holds. Manufacturing a standing for "file missing" would invent the entailment DESIGN names as authority substitution. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * scm: save a repository to a path, with the adjudication ahead of the write WIP pending probe verification; mirror of repository_load, split as json parse/emit are. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * scm: route the read through filesystem_read_outcome rather than raw projections Review on #9433 (review 56583) noted this module consumed Filesystem.Read's success/content/error projections directly, making it one more site against filesystem_read_outcome_adoption_standing -- mitigatable, 91 unconverted, whose next-rung trigger is that population reaching zero. Non-blocking under that standing, but this module is NEW: it would have been the 92nd site, moving a tracked population the wrong way for no reason. It is also a coherence fix rather than only a debt one. The standing exists because content+success+error nonsense combinations stay writable at unconverted sites, and the distinction the fold preserves -- that an absent file and an empty file differ only on the success channel -- is exactly the distinction this module's four arms exist to preserve. Consuming the raw projections while the header argued against conflating channels was incoherent. Behavior is unchanged, verified rather than assumed. The four claims execute green after conversion, and the mutation red still discriminates: feeding the fold a constant `success: true` -- the converted spelling of the same defect -- reds EXACTLY scm_rl_an_absent_file_is_unreadable_not_empty, with the other three green and the restored control green again. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * scm: correct a routing claim in the save witness that measurement refuted The header asserted that a successful save's write "would not route in this frame". Measurement says otherwise: under `gunbc run` the mutated save really did write the file -- which is how the order claim's control stayed red after the source was restored. What is actually established is narrower than either the old claim or its opposite: a write executes under `gunbc run`; whether the required floor's hermetic frame admits one is a different question and was not measured. A read of a checkout path has an input carve-out; a write has no equivalent. Asserting either answer without measuring the floor would be the rung claim DESIGN forbids, so the header now names what was measured and what was not. The mutation receipt is recorded in the header too, because it is stronger than a passing pair: removing the adjudication from ahead of the write reds BOTH claims, and the order claim stays red after restore because the file it says should not exist now does. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * scm: carry the written byte count as a ByteSize, and refuse the crossing that would fabricate one review 56828 (REQUEST_CHANGES): `RepositorySaved { bytes_written: Int }` is a flat-scalar unit field in a `gunbc.*` product model -- the unit lives in the field name while the type is a bare `Int`. The raw scalar is legitimate at the `extdeps.filesystem` boundary under cited-spec fidelity; propagating it inward is what the rule forbids, and that is the step this type took. Taken the wrap rather than the tracked marker the review also offered: `ByteSize` (`std.measure`, `Measure<Memory, One, Nat>`) already is the authority for a quantity of bytes, so a marker would have been debt registered where construction was available. THE WRAP FORCED A DECISION THE REVIEW DID NOT ANTICIPATE, and it is the reason for the fourth arm. `ByteSize` counts a `Nat`, the host reports an `Int`, and the only available crossing (`std.checked_arithmetic` `nat_magnitude`) takes an ABSOLUTE VALUE. Applying it to a negative would turn a nonsense host report into a plausible byte count -- fabricated plausible output in one line, in the module whose whole point is that adjudication precedes the write. So the negative is refused as its own arm carrying what the host actually said, and `nat_magnitude` runs only on the non-negative domain where it is the identity. `RepositoryWriteByteCountUnrepresentable` is a boundary obligation, not a class on the ladder: external reality observed, typed, admitted or refused. No next-rung trigger, and no witness -- reaching it needs a host write that succeeds and then reports a negative, which no `SubstrateInputsOnly` fixture can author. The annotation records that as a limit rather than leaving it to read as a gap, because the alternative to the arm is not "no arm" but a silent magnitude. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * scm: enrol the save witness -- same defect review 56857 found in the load witness Same class as review 56857, found by sweeping my own lane rather than waiting for a second review to name it: every `-> Bool` claim here was a plain `fn`, so witness discovery never enrolled any of them and the required floor never asked. Two claims plus the keystone promoted. `scm_sv_unrepresentable_repository` stays a plain `fn` -- it returns a `RepositoryEnvelope`, it is a fixture builder rather than a claim, and promoting it would enrol something that asserts nothing. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Adapt the save witness to the split refusal type that landed with #9443 #9443 replaced `RepositoryLoad`'s flat refusal arms with `RepositoryLoadRefused { cause: RepositoryLoadRefusal }`. This witness still matched the flat `RepositoryFileUnreadable` arm, which no longer exists at that position, so it broke the moment #9443 merged. This is the ordinary adaptation to a landed refinement, not a defect in this branch. It was pre-announced before #9443 landed, precisely so a red arriving on a PR nobody had touched would not be misdiagnosed. One import and one arm. The claim does not change meaning: it still asserts that a refused save leaves no file, and it still discriminates on the same refusal cause -- it now reaches that cause through the outer arm that owns it, which is what the split exists to enforce. The PR stays draft and parked; this only keeps it coherent against main. Keystone returns `true` after the change. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Enroll the two save-witness route gaps the floor named on this branch The floor reported route_gap_unenrolled=2, both in scm_repository_save_witness, both the same cause already recorded for the load and read witnesses: scm_repository_save_keystone_holds scm_sv_a_refused_save_leaves_no_file -- the hermetic route has no arm for Read (operation declares no mock_response) They surfaced now rather than earlier because the previous commit adapted this witness to the split refusal type, so the claims reach the load call they were always going to make; the absent-file check needs a FAILING read and the hermetic frame has no arm for one. Measured, not predicted: enrolled only after a run named these exact two identities. Enrolling an identity that does not gap is a stale row and reds the build, which is what stale_route_gap counts -- it stayed 0. Enrolment records known debt and is not a fix. The remedy is a hermetic arm for a failing read at the filesystem boundary. Roster 209 -> 211; the module still evaluates and returns its list. NOT ADDRESSED HERE, because none of it is this branch's: the same run reports failed=47 and interrupted_before_verdict=44, none of them in any scm_ claim -- ci_budget_tree_witness, doc_reachability_witness, lifecycle_survivor_corpus_census and peers, plus CPU-budget preemptions. That is an inherited main condition. The PR stays draft and parked. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> Co-authored-by: Brian Searls <briansearls1@gmail.com>
The load half of the SCM read path.
gunbc.scm.repository_envelopedecodes aJsonValueand is pure; this is the effectful seam above it — path to bytes, bytes to document, document to envelope — so the decoder stays testable without a filesystem and the read path's only host effect lives in one place. DESIGN §3: the codec owns the interface shape, the host effect is one realization bound to it.Why four arms
RepositoryLoadhas four arms because the failures have three different owners:RepositoryFileUnreadableRepositoryDocumentUnparseableRepositoryDocumentRefusedRepositoryLoadedCollapsing any two is the not-applicable-rendered-as-malformed mode DESIGN lists among its recurring failures: they have opposite remedies. Telling a user their repository is corrupt when they mistyped a path sends them looking for damage that is not there, possibly with a destructive repair.
There is deliberately no
Absent => empty_repository()arm. That spelling reads as helpful and is the empty-observation narrow — it renders I could not observe anything as the verdict there is nothing here. Alogbuilt on it would print an empty history for a repository that exists at a slightly wrong path; acommitbuilt on it would mint a first commit into a repository that already has a hundred. No arm here can produce an envelope without having decoded one.Evidence: green by execution, plus a discriminating red
Four hand-authored fixtures drive the four arms, each claim asserting the arm it reached — so collapsing any two fails here. The fixtures are hand-authored rather than produced by
encode_repository, so a change to the encoder cannot silently move what this file calls a valid document.Mutation receipt.
load_repositoryconsultsread.successrather than inferring absence from empty content, because an empty file and an absent file both yield empty content and only the success channel separates them. Replacing that consultation with a constant turns exactly one claim red:So the success channel is load-bearing and the absent-file arm is genuinely covered rather than decorative.
The absent arm's fixture is a named nonexistent path,
scm_rl_absent_path = "...this_file_is_never_created.json"— so the absence is authored and greppable rather than incidental. If anyone ever creates that file, the arm goes loud instead of silently reclassifying into a different outcome.The absent-path fixture is under the checkout root deliberately. A
/tmppath would be refused by the interpreter's hermetic carve-out (v1_interpreterhermetic_checkout_input_disposition_under) as a host effect rather than answered as a failed read, and the claim would be measuring the sandbox instead of this module. Disposition isSubstrateInputsOnly, matching thetailscale_acl_witnessprecedent for reading a committed fixture.Compile: 0 blocking, 0 advisories in the new file (48 files emitted over the closure).
Why no LoadStanding projection
gunbc.scm.load_standinganswers what a loader may do next at a publication boundary — whether a damaged generation may supersede a head slot. Three of these four arms have no publication meaning at all; a mistyped path is not a standing about a document. A consumer that is at a publication boundary callsrepository_envelope_load_standingon the decode cause it holds, which is that function's job. Manufacturing a standing for "file missing" would invent the entailment DESIGN names as authority substitution.Scope
Load only. The CLI half is deliberately not here — it needs an output channel that does not yet exist, and the shape of that is under a separate ruling (model the presentation, bind N handlers; not a stdout channel because stdout is the medium that hurts today).
🤖 Generated with Claude Code
Filed against this carrier, not repaired here
RepositoryFileUnreadablecarrieserror: String, and that is a real debt in this module. By the mechanical test governing the read-command layer — if the result carrier contains a human-readable string, it has already chosen a channel — a host error message inside a refusal arm is exactly that. Every binding downstream either re-parses that prose or contradicts it.It is filed rather than fixed because the repair is not a rename: the string is the operating system's, arriving through
extdeps.filesystem.filesystem_io's citederroroutput channel, so grounding it means modeling the failure classes a read can actually have (absent, permission-denied, not-a-file, io-error) as a typed coproduct at the extdeps boundary and mapping the host string into it once. That is a boundary-authority change with its own consumers, not a change to this seam, and doing it inside a load-model PR would put a filesystem taxonomy ingunbc.scm.Recorded here so the debt has a home and a stated shape rather than being discovered again by the next reader. It is also the reason the read-command module's header (in #9443) narrows its no-human-readable-string claim to what that module authors instead of claiming it of the whole type — the claim was false transitively through this arm, and saying so there without filing it here would have been a complaint without an owner.
An unstated soundness premise, now stated
scm_rl_an_absent_file_is_unreadable_not_emptyproves the path is unreadable, which is what the arm carries. It does not prove no file exists — those coincide here only becausethis_file_is_never_created.jsonis never created by anything in the repository. That premise was load-bearing and unwritten; an added fixture that touches the path would make the claim quietly weaker without failing. The same premise underwritesscm_sv_a_refused_save_leaves_no_filein #9434, whose name asserts absence while its body observes unreadability.Not repaired, because the alternative — asserting non-existence directly — needs a file-absent observation the filesystem boundary does not currently expose separately from a failed read, which is the same missing distinction the
error: Stringdebt above describes. One gap, two symptoms.The filesystem boundary gap, stated at the right grain
Three findings on this PR trace to one authority, but "the filesystem models no read failure" was my first wording and it is imprecise.
extdeps.filesystem.filesystem_iodoes model a generic refusal —FilesystemReadRefused { error: String }. What is missing is two separable capabilities, and fixing either alone leaves the other standing:1. Semantic discrimination. Today this population is one raw host string:
That single collapse is why
RepositoryFileUnreadablemust carry host prose, why an absent-file witness can only prove unreadability, and why absence and permission-failure cannot receive different typed remedies. The cause vocabulary should be derived from the host's own typed error classification rather than by parsing prose — typed cause as authority, host message as optional detail, never as the classification.2. Hermetic production. Even the existing generic arm cannot be produced by an authored fixture for a path that must fail. Committed successful reads have a route; a deliberately failing read does not. That is this PR's route gap.
The two are independent:
A terminal cut should supply both. One caution for whoever takes it: the negative fixture must be explicitly authored, not inferred from an absent fixture — making "no fixture" implicitly mean "file absent" would reproduce the empty-observation narrow at the mock layer, which is the exact class this witness exists to guard.
Dissolution receipt, mechanical: when that boundary lands, the two
floor_route_gaprows added here go stale and red the build; delete exactly those rows; the two identities must then reach their subject and pass. The discriminating mutation is to swap the hermetic absent-response for a successful empty-file response — the absent-file claim and the keystone must go RED while the three committed-fixture claims stay GREEN. A permission-denied fixture is the control proving the new classifier does not simply label every refusal "absent".Only then can the absence-oriented witness descend to a typed cause instead of resting on the authored premise, recorded above, that nothing in the repository creates the named path.