From 616cd8f9d8363455fbea54d6128a0afd2a17a452 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Thu, 27 Aug 2026 23:30:34 +0000 Subject: [PATCH 1/3] scm: a typed read-command result that names no destination Recut onto current main so the diff matches the scope this PR claims. WHY THE RECUT. The previous composition reached main through the save branch's ancestry, so it carried repository_save.dag and its witness -- neither of which is on main, and both of which belong to #9434, which is draft. Merging this PR would therefore have landed the parked save half as a consequence of branch topology rather than as a decision anyone made. Nobody would have done anything wrong; the ancestry would simply have outranked the park. The park is respected rather than routed around. No convert_to_draft event exists on #9434 and draft is not this tooling's default, so the hold is unexplained rather than accidental -- and the correct response to an unexplained hold is to leave it standing. WHAT REMAINS, and why the load refinement is not scope creep: splitting RepositoryLoadRefusal out of RepositoryLoad is what lets ScmReadRepositoryUnavailable carry a refusal that CANNOT hold a success. Without it this module's unavailable arm would be constructible holding RepositoryLoaded, with nothing to refuse the pair. It is the enabling half of this change, not a neighbour travelling with it. The dependency runs one way, checked before cutting: the save witness imports RepositoryLoadRefused, and nothing read-side references save. So dropping save costs this PR nothing. Both keystones return `true` on this tree over current main. Co-Authored-By: Claude Opus 5 (1M context) --- dag/gunbc/scm/read_command.dag | 121 ++++++++++++++++++ dag/gunbc/scm/repository_load.dag | 44 ++++++- .../claim/scm_read_command_witness_test.dag | 118 +++++++++++++++++ .../scm_repository_load_witness_test.dag | 10 +- 4 files changed, 284 insertions(+), 9 deletions(-) create mode 100644 dag/gunbc/scm/read_command.dag create mode 100644 dag/test/claim/scm_read_command_witness_test.dag diff --git a/dag/gunbc/scm/read_command.dag b/dag/gunbc/scm/read_command.dag new file mode 100644 index 00000000000..05778ed94ac --- /dev/null +++ b/dag/gunbc/scm/read_command.dag @@ -0,0 +1,121 @@ +module gunbc.scm.read_command + +// WHAT A READ-SIDE SCM COMMAND PRODUCES, WITH NO IDEA WHERE IT IS GOING. +// +// Every read verb is the same two steps: load a repository from a path, then ask it a question. +// Both steps can fail and they fail for different reasons, so this module exists to compose them +// ONCE rather than have each verb restate the three ways a load can refuse. +// +// NOTHING HERE NAMES A DESTINATION. No terminal, no stream, no exit code, no formatting. A caller +// binds this value to whatever medium it has -- a terminal, an HTTP response, a file, a captured +// fixture -- and that binding is the realization, kept peripheral exactly as +// `gunbc.cli_dispatch_surface` keeps it: the surface names no realization, and the dispatch that +// selects one is itself realization. +// +// THIS MODULE CHOOSES NO PHRASING. Wording, layout, ordering, plurals, colour and truncation are +// the binding's business and none of them appear below. THE CLAIM IS ABOUT WHAT THIS MODULE +// AUTHORS, NOT ABOUT THE WHOLE TYPE, and an earlier revision of this header stated it at the wrong +// grain -- "there is no human-readable string in any arm", which is true of the arms declared here +// and FALSE of `ScmReadResult` as a type, because `ScmReadRepositoryUnavailable` carries a +// `RepositoryLoadRefusal` whose `RepositoryFileUnreadable` arm carries an `error: String` from the +// host. That is DESIGN's total-at-the-level-examined class landing in the one sentence that was +// supposed to be this module's mechanical test. The prose inside that refusal is a real finding +// against `gunbc.scm.repository_load` and is filed there rather than repaired here. +// +import std.types { String } +import gunbc.scm.repository_load { + RepositoryLoaded, + RepositoryLoadRefused, + RepositoryLoadRefusal, + load_repository, +} +import gunbc.scm.log { CommitLog, repository_log } +import gunbc.scm.status { RepositoryStatus, repository_status } +import gunbc.scm.merge { Proposal } + +// THE VERB IS A TYPE ARGUMENT, NOT AN ARM. Selecting a verb from argv is dispatch, and dispatch is +// realization (DESIGN section 3), so a `ScmReadCommand = Log | Status` coproduct here would pull +// the CLI's own concern into the value layer. A `ScmReadAnswer = ScmLogAnswer | ScmStatusAnswer` +// coproduct did exactly that in an earlier revision while a header paragraph denied it: the roster +// was not removed, it was MOVED FROM THE REQUEST TO THE RESPONSE, one arm per verb. The test that +// this revision fixed it rather than relocating it again is mechanical -- the coproduct below names +// no verb at all, and adding a third read verb adds no arm to any type here. +type ScmReadResult + = ScmReadAnswered { path: String, answer: T } + | ScmReadRepositoryUnavailable { cause: RepositoryLoadRefusal } + +// WHAT THE TYPE ARGUMENT DOES NOT BUY, MEASURED RATHER THAN ASSUMED. The reason for the generic is +// the paragraph above -- the coproduct names no verb -- and that reason is structural, discharged by +// the declaration itself. It is NOT a claim that the payload type is enforced here, and the +// difference was measured rather than reasoned about. Mutation: make `scm_read_status` answer with +// `repository_log(...)`, so a `CommitLog` sits in a declared `ScmReadResult` +// position. Result: the compile produced 0 blocking errors AND no diagnostic of any severity at +// this module's construction site. The neighbouring advisory about generic formals is real but +// belongs to other call sites; nothing was reported against these two functions at all. +// +// SO THE HONEST RUNG IS mitigatable, NOT structurally guaranteed (DESIGN section 4b). A reader who +// took the generic for a wall would be doing the rung inflation that section names as worse than +// sitting low, because an inflated class never ranks for climbing. What the generic ACTUALLY +// removed is a state the old shape could NAME: under `ScmReadAnswer = ScmLogAnswer | ScmStatusAnswer` +// a log answer from the status verb was a well-typed value with an arm of its own, and here it has +// no arm -- which is a real narrowing of what the module can SAY, independent of what the compiler +// currently CHECKS. +// +// THE MECHANISM IS MEASURED, NOT GUESSED, AND THE TRIGGER IS NAMED AT ITS GRAIN. Three probes, +// serialized, each asserting the source state it ran under: a kernel at a NON-GENERIC record field +// REFUSES (`type mismatch: expected 'Product(RepositoryStatus)', got 'Primitive(Int)'`); an +// UNDEFINED NAME at this module's generic `answer` field REFUSES, which proves inference reaches +// this exact position rather than skipping it; and a kernel at that same generic field ADMITS. So +// the judgment is REACHED and DECLINES, and it declines because the formal is the type VARIABLE +// `T`. Declining there is CORRECT in general -- `T` can be instantiated at `Int`, so refusing a +// kernel at an uninstantiated formal would be wrong. The gap is therefore one level up from the +// judgment: at this construction the instantiation is fully concrete (`ScmReadResult`), +// so `T` is known, and if the argument were substituted before judging, the generic field would +// refuse for exactly the reason the non-generic one does. +// +// NEXT-RUNG TRIGGER: THE TYPE ARGUMENT SUBSTITUTED INTO THE FORMAL BEFORE THE INHABITANCE JUDGMENT +// RUNS. That is the capability, stated in the words the loss is stated in -- not "a check at +// generic positions", which is an artifact that could be built while this stayed dead. It is a +// compiler capability and not a thing this module can construct. + +// THE VERDICT IS THE SHAPE. There is no `answered: Bool` and no `verdict:` field, deliberately: a +// stored verdict is a second representation of something the arms already determine, so a value +// could be constructed whose flag says answered and whose payload is a refusal, and nothing would +// refuse it. Here that pair has no spelling. The construction is the one +// `gunbc.live_deploy.spec` `deployment_step_ownership` uses, whose authority note gives the reason +// in general form: the classification is DERIVED, never stored, so an inconsistent pair is +// unwritable -- DESIGN section 5, construction over validation. +// +// AND NO `Bool` PROJECTION OVER IT IS EXPORTED. An earlier revision offered +// `scm_read_produced_answer`, whose only consumers were the two witnesses asserting it returns true +// and false -- an artifact with no final consumer (DESIGN section 6). `gunbc.scm.checkout` records +// this exact helper shape being removed twice before, once as `checkout_succeeded` and once from +// `gunbc.scm.ancestry` under review 56207, for the reason that survives here: consumers match the +// arms, so a new arm fails to compile at every site rather than being silently absorbed into a +// false. A binding needing both did-it-answer and did-the-intent-complete derives BOTH from the arm +// it is in; one Bool cannot express two questions, and a second Bool would be the same mistake +// twice. +// +// AN EMPTY REPOSITORY IS AN ANSWER, NOT A FAILURE. `CommitLog`'s `NoCommitsYet` sits INSIDE +// ScmReadAnswered: a repository with no commits was read successfully and truthfully has nothing to +// report. Filing it beside "the document was unparseable" would be the +// not-applicable-rendered-as-malformed conflation -- opposite owners, opposite repairs, one symbol. + +fn scm_read_log(path: String) -> ScmReadResult { + match load_repository(path: path) { + RepositoryLoadRefused { cause: cause } => ScmReadRepositoryUnavailable { cause: cause } + RepositoryLoaded { path: p, envelope: envelope } => + ScmReadAnswered { path: p, answer: repository_log(envelope: envelope) } + } +} + +// STATUS TAKES THE PENDING PROPOSAL AS A PARAMETER rather than reading it from somewhere, because +// `repository_status` does: what is staged is not a fact the repository document carries, and +// inventing a source for it here would be this module deciding a question its authority left open. +fn scm_read_status(path: String, pending: Proposal) -> ScmReadResult { + match load_repository(path: path) { + RepositoryLoadRefused { cause: cause } => ScmReadRepositoryUnavailable { cause: cause } + RepositoryLoaded { path: p, envelope: envelope } => + ScmReadAnswered { path: p, answer: repository_status(envelope: envelope, pending: pending) } + } +} diff --git a/dag/gunbc/scm/repository_load.dag b/dag/gunbc/scm/repository_load.dag index 135298f11ec..03cc3159ef7 100644 --- a/dag/gunbc/scm/repository_load.dag +++ b/dag/gunbc/scm/repository_load.dag @@ -65,12 +65,43 @@ import gunbc.scm.repository_envelope { RepositoryDecodeRefusal, } -type RepositoryLoad - = RepositoryLoaded { path: String, envelope: RepositoryEnvelope } - | RepositoryFileUnreadable { path: String, error: String } +// THE REFUSALS ARE THEIR OWN TYPE SO A CONSUMER CAN CARRY ONE WITHOUT BEING ABLE TO HOLD A SUCCESS. +// A layer above this -- a command surface, a serving handler -- needs to say "the repository was not +// available, and here is which of the three owners is responsible". If that layer's arm carried a +// whole `RepositoryLoad`, its unavailable case could be constructed holding `RepositoryLoaded`, and +// nothing would refuse it. Splitting the refusals off makes that pair unwritable rather than merely +// unwise, which is DESIGN section 5's construction-over-validation at the seam where the value +// travels. +// +// IT ALSO MAKES THIS MODULE MATCH ITS NEIGHBOURS. `RepositoryDecodeOutcome`, +// `RepositoryEncodeOutcome` and `CheckoutOutcome` are all `X | XRefused { cause: XRefusal }`, and a +// fourth spelling for the same shape in the module that composes with all three would be a second +// idiom for one concept. +// +// EVERY REFUSAL STILL CARRIES ITS PATH, and now it carries it INTO whatever holds it: a refusal that +// travels to a caller without saying what it was reading is not located, and locating it at the +// outcome instead would strip the location off exactly when the refusal leaves this module. +type RepositoryLoadRefusal + = RepositoryFileUnreadable { path: String, error: String } | RepositoryDocumentUnparseable { path: String, gap: JsonDocumentGap } | RepositoryDocumentRefused { path: String, cause: RepositoryDecodeRefusal } +type RepositoryLoad + = RepositoryLoaded { path: String, envelope: RepositoryEnvelope } + | RepositoryLoadRefused { cause: RepositoryLoadRefusal } + +// DERIVED, NEVER STORED. There is no `loaded: Bool` field anywhere in this module: the arm IS the +// answer, so a value whose flag disagrees with its shape has no spelling. Same construction as +// `gunbc.live_deploy.spec` `deployment_step_ownership`, whose authority note states the rule -- an +// inconsistent ownership/payload pair is unwritable because ownership is projected, not recorded. +fn repository_load_refusal_path(refusal: RepositoryLoadRefusal) -> String { + match refusal { + RepositoryFileUnreadable { path: p, error: _ } => p + RepositoryDocumentUnparseable { path: p, gap: _ } => p + RepositoryDocumentRefused { path: p, cause: _ } => p + } +} + // THE ONLY HOST EFFECT IN THE READ PATH, AND IT IS FOLDED BEFORE IT IS READ. The scalar transport // observation -- content, success, error together -- is handed to `filesystem_read_outcome` rather // than projected field by field, so the arms below never see a content/success/error combination @@ -86,17 +117,18 @@ type RepositoryLoad fn load_repository(path: String) -> RepositoryLoad { let read = Filesystem.Read(path: path) match filesystem_read_outcome(content: read.content, success: read.success, error: read.error) { - FilesystemReadRefused { error: e } => RepositoryFileUnreadable { path: path, error: e } + FilesystemReadRefused { error: e } => + RepositoryLoadRefused { cause: RepositoryFileUnreadable { path: path, error: e } } FilesystemReadSucceeded { content: content } => match parse_json_document(s: content) { JsonDocumentUnreadable { gap: gap } => - RepositoryDocumentUnparseable { path: path, gap: gap } + RepositoryLoadRefused { cause: RepositoryDocumentUnparseable { path: path, gap: gap } } JsonDocumentParsed { value: v } => match decode_repository(v: v) { RepositoryDecoded { envelope: envelope } => RepositoryLoaded { path: path, envelope: envelope } RepositoryDecodeRefused { cause: cause } => - RepositoryDocumentRefused { path: path, cause: cause } + RepositoryLoadRefused { cause: RepositoryDocumentRefused { path: path, cause: cause } } } } } diff --git a/dag/test/claim/scm_read_command_witness_test.dag b/dag/test/claim/scm_read_command_witness_test.dag new file mode 100644 index 00000000000..6abcd148fcf --- /dev/null +++ b/dag/test/claim/scm_read_command_witness_test.dag @@ -0,0 +1,118 @@ +module test.claim.scm_read_command_witness + +// THE READ-COMMAND COMPOSITION, AND THE ONE DISTINCTION IT EXISTS TO HOLD. +// +// `scm_read_log` and `scm_read_status` each do two things that fail for different reasons, and the +// claim that matters is that they stay apart at the seam where a binding will read them: a +// repository that could not be loaded is NOT an answer, and a repository with nothing in it IS one. +// +// THE CENTRAL CLAIM IS scm_rc_an_empty_repository_is_an_answer_not_a_failure. It is the one that +// would go red if someone ever decided an empty log was a degenerate failure -- the +// not-applicable-rendered-as-malformed conflation, which has opposite owners and opposite repairs +// on each side. Every other claim here supports it. +// +// NOTHING IN THIS FILE ASSERTS A RENDERING, deliberately. There is no expected string anywhere: this +// layer produces facts and a binding decides how they read, so a claim about wording here would be +// this file inventing the channel the module refuses to name. The one string compared below is a +// format tag THIS FILE'S OWN FIXTURE AUTHORS, which is a controlled input rather than phrasing. +// +// EVERY NAME HERE WAS RE-READ AGAINST ITS BODY, because two claims in this lane were found asserting +// more in the name than the body checked -- a disagreement no lens and no green run can see, since a +// lens reads the body and a run reads the result and neither reads the name as a claim. Two claims +// were repaired in opposite directions: the same-cause claim's NAME came down to what its body can +// honestly check, and the schema-refusal claim's BODY came up to what its name always said. + +import std.types { Bool, String } +import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } +import gunbc.scm.authoring { empty_proposal } +import gunbc.scm.log { NoCommitsYet } +import gunbc.scm.repository_envelope { RepositoryFormatUnrecognized } +import gunbc.scm.repository_load { + RepositoryFileUnreadable, + RepositoryDocumentRefused, +} +import gunbc.scm.read_command { + ScmReadAnswered, + ScmReadRepositoryUnavailable, + scm_read_log, + scm_read_status, +} + +data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly + +data scm_rc_empty_repository_path: String = "dag/test/fixture/scm_repository_load/empty_repository.json" +data scm_rc_unknown_format_path: String = "dag/test/fixture/scm_repository_load/unknown_format.json" +data scm_rc_absent_path: String = "dag/test/fixture/scm_repository_load/this_file_is_never_created.json" + +// THE FORMAT TAG THE FIXTURE AUTHORS. Compared below so the schema claim proves the cause reached +// the command layer INTACT rather than merely that some refusal did. This is a controlled fixture +// value, not host prose: it is authored two files away in this same repository, so a claim pinned to +// it cannot rot when a libc message changes. +data scm_rc_unknown_format_tag: String = "gunbc-scm-repository-v99" + +// THE CENTRAL CLAIM. A repository that holds no commits was read successfully and truthfully has +// nothing to report, so it must land in the ANSWERED arm carrying NoCommitsYet -- never beside a +// load refusal. The two have opposite remedies: nothing to do, versus fix your repository. +test fn scm_rc_an_empty_repository_is_an_answer_not_a_failure() -> Bool { + match scm_read_log(path: scm_rc_empty_repository_path) { + ScmReadAnswered { path: p, answer: NoCommitsYet } => p == scm_rc_empty_repository_path + _ => false + } +} + +test fn scm_rc_an_absent_repository_is_unavailable_not_an_empty_answer() -> Bool { + match scm_read_log(path: scm_rc_absent_path) { + ScmReadRepositoryUnavailable { cause: RepositoryFileUnreadable { path: p, error: _ } } => + p == scm_rc_absent_path + _ => false + } +} + +// THE LOAD REFUSAL REACHES THE COMMAND LAYER INTACT, carrying the schema's own cause rather than a +// flattened "something went wrong". A binding that wants to distinguish a damaged document from a +// missing one can, because nothing here collapsed them. The body descends to the FORMAT TAG: an +// earlier revision bound `cause: _` and so proved only that some schema refusal arrived, which is +// exactly the claim the name does not make. +test fn scm_rc_a_schema_refusal_survives_composition_with_its_cause() -> Bool { + match scm_read_log(path: scm_rc_unknown_format_path) { + ScmReadRepositoryUnavailable { + cause: RepositoryDocumentRefused { + path: p, + cause: RepositoryFormatUnrecognized { found: found }, + }, + } => p == scm_rc_unknown_format_path && found == scm_rc_unknown_format_tag + _ => false + } +} + +// BOTH VERBS REFUSE IN THE SAME ARM ON THE SAME PATH, which is what this body can honestly check and +// now all its name claims. It does NOT establish that the two causes are equal: the arm carries a +// host `error` string, and comparing that would pin a merge-blocking claim to a libc message, which +// is a worse defect than the imprecision it would remove. So the name states arm and path, and the +// error field is bound and ignored VISIBLY rather than silently. +test fn scm_rc_status_refuses_in_the_same_arm_on_the_same_path_as_log() -> Bool { + match scm_read_log(path: scm_rc_absent_path) { + ScmReadRepositoryUnavailable { cause: RepositoryFileUnreadable { path: lp, error: _ } } => + match scm_read_status(path: scm_rc_absent_path, pending: empty_proposal()) { + ScmReadRepositoryUnavailable { cause: RepositoryFileUnreadable { path: sp, error: _ } } => + lp == sp && lp == scm_rc_absent_path + _ => false + } + _ => false + } +} + +test fn scm_rc_status_answers_on_a_loadable_repository() -> Bool { + match scm_read_status(path: scm_rc_empty_repository_path, pending: empty_proposal()) { + ScmReadAnswered { path: p, answer: _ } => p == scm_rc_empty_repository_path + _ => false + } +} + +test fn scm_read_command_keystone_holds() -> Bool { + scm_rc_an_empty_repository_is_an_answer_not_a_failure() && + scm_rc_an_absent_repository_is_unavailable_not_an_empty_answer() && + scm_rc_a_schema_refusal_survives_composition_with_its_cause() && + scm_rc_status_refuses_in_the_same_arm_on_the_same_path_as_log() && + scm_rc_status_answers_on_a_loadable_repository() +} diff --git a/dag/test/claim/scm_repository_load_witness_test.dag b/dag/test/claim/scm_repository_load_witness_test.dag index b29a8485d70..f84355b9f7b 100644 --- a/dag/test/claim/scm_repository_load_witness_test.dag +++ b/dag/test/claim/scm_repository_load_witness_test.dag @@ -20,6 +20,8 @@ import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } import gunbc.scm.repository_load { RepositoryLoad, RepositoryLoaded, + RepositoryLoadRefused, + RepositoryLoadRefusal, RepositoryFileUnreadable, RepositoryDocumentUnparseable, RepositoryDocumentRefused, @@ -48,14 +50,16 @@ test fn scm_rl_a_well_formed_document_loads() -> Bool { test fn scm_rl_an_absent_file_is_unreadable_not_empty() -> Bool { match load_repository(path: scm_rl_absent_path) { - RepositoryFileUnreadable { path: p, error: _ } => p == scm_rl_absent_path + RepositoryLoadRefused { cause: RepositoryFileUnreadable { path: p, error: _ } } => + p == scm_rl_absent_path _ => false } } test fn scm_rl_a_truncated_document_is_unparseable() -> Bool { match load_repository(path: scm_rl_malformed_document_path) { - RepositoryDocumentUnparseable { path: p, gap: _ } => p == scm_rl_malformed_document_path + RepositoryLoadRefused { cause: RepositoryDocumentUnparseable { path: p, gap: _ } } => + p == scm_rl_malformed_document_path _ => false } } @@ -65,7 +69,7 @@ test fn scm_rl_a_truncated_document_is_unparseable() -> Bool { // bytes are damaged" rather than "this is a repository of a version I do not know". test fn scm_rl_a_parseable_non_repository_is_refused_by_schema() -> Bool { match load_repository(path: scm_rl_unknown_format_path) { - RepositoryDocumentRefused { path: p, cause: c } => + RepositoryLoadRefused { cause: RepositoryDocumentRefused { path: p, cause: c } } => p == scm_rl_unknown_format_path && match c { RepositoryFormatUnrecognized { found: f } => f == "gunbc-scm-repository-v99" From 2a0d65a70e00c6060be0364c0c6b2da499204cfc Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Thu, 27 Aug 2026 23:48:25 +0000 Subject: [PATCH 2/3] Drop the refusal-path accessor: the third instance of a shape this PR documents as twice-removed `repository_load_refusal_path` had exactly one occurrence in the tree -- its own definition. No consumer, so DESIGN section 6 residue. WHAT MAKES THIS WORSE THAN ORDINARY DEAD CODE: read_command.dag's own header, in this same PR, cites this exact helper shape being removed twice before -- once as `checkout_succeeded`, once from `gunbc.scm.ancestry` under review 56207 -- and states the reason that survives. This change re-added the third instance while documenting the first two. Neither a lens nor a green run can see that; only reading the two files against each other does. The surviving rationale in the deleted comment block was about the TYPES (why no `loaded: Bool` exists), not about the accessor, so it moves to `type RepositoryLoad` rather than being deleted along with the function. A prose row removed for one reason must not silently take its contents with it. It gains the reason the shape keeps recurring, which was written down nowhere: with no consumer the accessor is residue, and WITH one it is worse -- a fourth refusal arm would be absorbed by the projection instead of failing to compile at each site that must decide about it. Both keystones return `true` after the deletion. Reported by review 57012. Co-Authored-By: Claude Opus 5 (1M context) --- dag/gunbc/scm/repository_load.dag | 21 ++++++++++----------- 1 file changed, 10 insertions(+), 11 deletions(-) diff --git a/dag/gunbc/scm/repository_load.dag b/dag/gunbc/scm/repository_load.dag index 03cc3159ef7..ab033c53a41 100644 --- a/dag/gunbc/scm/repository_load.dag +++ b/dag/gunbc/scm/repository_load.dag @@ -86,21 +86,20 @@ type RepositoryLoadRefusal | RepositoryDocumentUnparseable { path: String, gap: JsonDocumentGap } | RepositoryDocumentRefused { path: String, cause: RepositoryDecodeRefusal } -type RepositoryLoad - = RepositoryLoaded { path: String, envelope: RepositoryEnvelope } - | RepositoryLoadRefused { cause: RepositoryLoadRefusal } - // DERIVED, NEVER STORED. There is no `loaded: Bool` field anywhere in this module: the arm IS the // answer, so a value whose flag disagrees with its shape has no spelling. Same construction as // `gunbc.live_deploy.spec` `deployment_step_ownership`, whose authority note states the rule -- an // inconsistent ownership/payload pair is unwritable because ownership is projected, not recorded. -fn repository_load_refusal_path(refusal: RepositoryLoadRefusal) -> String { - match refusal { - RepositoryFileUnreadable { path: p, error: _ } => p - RepositoryDocumentUnparseable { path: p, gap: _ } => p - RepositoryDocumentRefused { path: p, cause: _ } => p - } -} +// +// AND NO PROJECTION OVER THE REFUSAL EITHER. Every refusal carries `path`, so a +// `refusal -> String` accessor is authorable and was authored here and removed: with no consumer it +// is DESIGN section 6 residue, and with one it is worse -- a fourth refusal arm would be absorbed by +// the projection instead of failing to compile at each site that must decide about it. This exact +// shape has now been removed three times (`checkout_succeeded`, `gunbc.scm.ancestry` under review +// 56207, and here). Consumers match the arms. +type RepositoryLoad + = RepositoryLoaded { path: String, envelope: RepositoryEnvelope } + | RepositoryLoadRefused { cause: RepositoryLoadRefusal } // THE ONLY HOST EFFECT IN THE READ PATH, AND IT IS FOLDED BEFORE IT IS READ. The scalar transport // observation -- content, success, error together -- is handed to `filesystem_read_outcome` rather From 3ac6feb69e85cfab63b3653a93c1c557a4f4222d Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Fri, 28 Aug 2026 04:01:30 +0000 Subject: [PATCH 3/3] Enroll the three read-command route gaps the floor actually reported The floor reported route_gap_unenrolled=3 on this branch, all three in scm_read_command_witness, all with one cause: the hermetic route has no arm for Read (operation declares no mock_response) scm_rc_an_absent_repository_is_unavailable_not_an_empty_answer scm_rc_status_refuses_in_the_same_arm_on_the_same_path_as_log scm_read_command_keystone_holds Same boundary already recorded for the load witness: extdeps.filesystem declares no mock_response, so the hermetic frame has no arm for a FAILING read. All three claims exercise the absent-repository path, and the keystone inherits the gap by composing them. They pass under `gunbc run`, which performs the real read; they cannot reach their subject hermetically. MEASURED, NOT PREDICTED. These were foreseeable and were deliberately NOT pre-enrolled: enrolling an identity that does not gap is a stale row and reds the build, which is what stale_route_gap counts. The rows are added now because a run reported these exact three identities. Enrolment records the gap as known debt. It does not make the gap acceptable and it is not a fix: the remedy is a hermetic arm for a failing read, which belongs to the filesystem boundary and not to this PR. Roster 112 -> 115; the module still evaluates and returns its list. Co-Authored-By: Claude Opus 5 (1M context) --- src/v2/workflow/floor_route_gap.dag | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/v2/workflow/floor_route_gap.dag b/src/v2/workflow/floor_route_gap.dag index 1399293fcc5..571a69b5c9a 100644 --- a/src/v2/workflow/floor_route_gap.dag +++ b/src/v2/workflow/floor_route_gap.dag @@ -241,6 +241,12 @@ fn floor_route_gap_chunk_01() -> List { tail: Cons { head: "test.claim.run_verdict_exit_status_witness_test.run_success_verdict_reaches_zero_exit", tail: Cons { + head: "test.claim.scm_read_command_witness.scm_rc_an_absent_repository_is_unavailable_not_an_empty_answer", + tail: Cons { + head: "test.claim.scm_read_command_witness.scm_rc_status_refuses_in_the_same_arm_on_the_same_path_as_log", + tail: Cons { + head: "test.claim.scm_read_command_witness.scm_read_command_keystone_holds", + tail: Cons { head: "test.claim.scm_repository_load_witness.scm_rl_an_absent_file_is_unreadable_not_empty", tail: Cons { head: "test.claim.scm_repository_load_witness.scm_repository_load_keystone_holds", @@ -287,6 +293,9 @@ fn floor_route_gap_chunk_01() -> List { } } } + } + } + } } fn floor_route_gap_chunk_02() -> List {