Repository navigation
scm: the status verb, with every shape decision derived at its site - #9257
Conversation
The read-side SCM verbs exist (checkout, and the commit lookups); the AUTHORING verbs do not. This is the first of them, written to read as checkout's sibling rather than as a second shape for the same layer. THE ROLE-CONFLICT RULE IS DERIVED, AND IT LANDS OPPOSITE TO merge's, which is the whole content of the change. merge.dag says in the strongest terms: "ONLY THE FIRST AUTHORING RESOLVES THE ROLE ... silently taking the last writer is the fabricated winner this outcome type exists to refuse." Read naively that settles this module too, and add would have to refuse a repeated role. It does not settle it, because the two operations are asked different questions about different populations, and merge's OWN justification is what shows it: MERGE combines proposals from SEVERAL AUTHORS. Two requirements for one role are two parties who each believe theirs is right and neither authored knowing the other. "Last" there is an artifact of the fold order, so picking one fabricates a winner. AUTHORING revises ONE author's OWN proposal in the order THEY performed it. The second add is the same party saying "no, this". "Later" here is the author's own sequence of intent, not a fold artifact. So the merge rule is not overridden -- it does not reach. Its premise is a contest between authors, and an author has no contest with themselves. The mechanical tell: merge states its rule over a LIST of proposals whose order it explicitly refuses to privilege; this is one proposal revised in place. Corroborating rather than deciding: if add accumulated instead, the ordinary loop -- edit, add, notice a mistake, edit, add -- would hand merge a SELF-CONTEST it would correctly refuse, so a staged mistake could only be fixed by discarding the proposal. A verb whose sole response to correction is "start over" has modelled a ledger, not authoring. Nothing is weakened across authors: this produces one proposal per author, and when two meet, merge still sees two competing requirements and still refuses. NO OUTCOME COPRODUCT, unlike checkout, and the contrast is stated at the site. checkout can genuinely refuse -- an object may be missing -- and that arm is the discriminating half of its claim. This has no reachable refusal: any role may be authored, any requirement may replace another for that role, there is no store to consult. A refusal arm that cannot be produced is the permanently-green decoration DESIGN 4b rules worse than absent. add and rm are ONE function over the Requirement coproduct; forking them would mint two shapes for one concept. Which verb was typed is a surface fact. Receipts, by execution: five witnesses PASS, including that a stated ABSENCE supersedes a present binding -- the half merge's silence-means-preserve rule makes load-bearing, since an empty proposal would read as "leave the target alone", the inversion of the request. Mutating replace into accumulate turns TWO witnesses FALSE; restored PASS. Sweep clean at 3994. Witness helpers are name-qualified: top-level definitions are corpus-wide and the resolver silently selects among duplicates (#8707), which this very layer's other witness file already documents having hit. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
They belong to the status verb lane (#9257) and were never part of the parse_json work. They landed here because the previous commit staged with `git add -A` while the files sat untracked in a shared worktree, having followed a branch switch. No review caught it and no check would have: they compile, so the only signal was reading the commit's own file list. This PR is the parse_json cut and is reviewable precisely because it is one thing; two unrelated SCM modules make it neither. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
The verb layer's second authoring-side surface, after `add`. Nothing here is a UI preference: each decision is derived from what RepositoryEnvelope can answer, and THE DERIVATION IS AT THE SITE rather than in a PR body, because a reader who finds "the checked-out commit and a count" with no reason will read it as an arbitrary call and change it. MOST OF THE GIT-STATUS MENTAL MODEL IS NOT EXPRESSIBLE HERE, and that is a property of the model rather than a missing feature. The envelope carries a store, a commit list, and an optional checked-out selection; this layer has NO path, NO branch, NO author, NO timestamp, NO working tree and NO remote anywhere in it. Checked rather than assumed: the only `Branch` under dag/gunbc/scm is the node CONNECTIVE. So modified-files, staged-versus-unstaged BY PATH, ahead/behind and current-branch cannot appear -- not deferred, unproducible. A surface reporting them would be fabricating. THREE STATES, NOT TWO, is the load-bearing one. It is not enough that a stated absence differ from a present binding: it must differ from NOT MENTIONED AT ALL, because merge's silence-means-preserve rule makes "role not stated" and "role stated absent" SEMANTICALLY OPPOSITE -- one preserves the target's binding, the other deletes it. A rendering where a stated absence looks like an empty slot is the not-applicable-versus-malformed conflation carried into a user surface, where someone acts on it. The third state is structural: a role that is not stated has no row, so there is no value meaning "not stated" to get out of step. The other derivations, each stated where it is made: nothing-checked-out is NORMAL, because repository_envelope's own header says init produces no commits and no root and that neither is an error -- rendering it as a warning would contradict a stated authority and fabricate a fault. A dangling checkout is its own arm, because the envelope's encoder refuses on RepositoryCheckoutNotInCommits so the question is DECIDABLE here, and reporting the selection as an ordinary checkout would assert a commit exists when it may not. The commit count rather than the log, because a `log` verb will own what happened and two surfaces for one fact is the redundancy section 2 prices. No store population, because that is a fact about REPRESENTATION and below-boundary representation is opaque. The pending proposal IS in status, because "what have I staged" is the primary question status answers and without it the surface is nearly empty. Structure and rendering are split: a machine consumer must read the FACTS rather than parse prose out of a terminal rendering, which would be a second authority for one answer. Receipts, by execution: six witnesses PASS. Three mutations, each turning ITS OWN witness FALSE -- rendering an absence as a staged binding, rendering the empty staged list as silence, and reporting a dangling checkout as ordinary. I first checked the silence mutation against the three-state witness, which correctly stayed green because that is the other witness's claim, and re-ran it against the right one rather than report a receipt I had not taken. Witness assertions are EXACT renderings rather than substring searches: a substring passes against a surface that also emits fabricated lines beside it. That also avoids adding a third top-level `string_contains` -- the corpus already carries two, and top-level names are corpus-wide with silent duplicate selection (#8707). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
On the prose-density remark (review 56019): I measured it rather than accept the pass — I audited both for the thing §4c actually forbids, which is restating what the declaration structurally says, and found exactly two openers doing it: one describing what a I wrote the two-line trim, then reverted it and am leaving both files alone, for two reasons worth stating rather than quietly acting on:
So: acknowledged as a real measurement, not acted on, and the reason is cost rather than disagreement. If the density is a standing concern rather than an observation, say so and I will do the pass properly across both modules in one commit on the right branch. (Edited to restore a line the shell ate when posting: item 1 lost its subject, — sent from gentle-eagle-360 |
…d at the root (#9241) * parse_json fail-open sites 1-2: the two silent drops become counted refusals absorb_supervised_turn_line dropped an unparseable stream line back into the accumulator unchanged -- a silent drop from a fold -- so a run whose entire transcript was unreadable reported ProviderTurnNotObserved, which ASSERTS the stream carried no terminal event. It now counts unreadable_lines and answers a new ProviderTurnStreamUnreadable, which is neither NotObserved (a claim about the provider's output) nor Failed (a claim about the TURN, attributing our decoder's limitation to the provider). tailscale_serve_status_proxy_targets answered the empty proxy list for a document it could not read -- the empty-observation narrow: not-affected and could-not-observe collapsed onto one value, and the narrow direction is the silently-uncovered one. It now returns TailscaleServeStatusProjection, so an unreadable status is reported rather than projected as a configuration fact. Its witness ASSERTED the swallow (count(...) == 0 on "not-json"); that witness is replaced by one asserting the distinction, with a positive control that a document which parses but carries no Web member is still an empty projection -- without which answering Unreadable for everything would pass. Receipts, by execution (gunbc run, per witness): site 1 repaired PASS -> mutation (Absent => acc) FAIL -> restored PASS site 2 three witnesses PASS -> mutation (Absent => ServeStatusProxies{[]}) turns the malformed witness FALSE -> restored PASS Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * parse_json fail-open site 3: the SDK parser-drop receipt stops answering an upstream fact when our own evidence is missing claude_sdk_parser_drop_receipt_holds returned Bool, and `false` meant BOTH "the receipt was read and it does not establish a parser drop" AND "I could not read the receipt". Those have opposite owners: the first is a claim about the SDK, the second about this repository's evidence. The wet witness is where it bit -- filesystem_read answers the empty string for a path it cannot read, so a deleted or renamed probe artifact made the witness report that the SDK does not drop control_response, sending the next reader to upstream rather than to git status. Renamed to claude_sdk_parser_drop_receipt_standing, returning ParserDropHolds | ParserDropRefuted | ParserDropNotEstablished { cause }, with the gap LOCATED at the member it stalled on. The gap does not re-spell the parse cause: ReceiptBytesUnreadable is a fact about our evidence in our own terms, not a second naming scheme for the codec's (DESIGN section 3). All three callers branch. The two forgery controls, previously `!holds`, now assert the two DIFFERENT arms they were always about -- the dropped-array shortcut is REFUTED (well-formed, conforming, comparison does not show the drop); the absent-member forgery is NOT ESTABLISHED at a named member. A third control asserts unreadable bytes reach a different cause than a nonconforming document, which is the pair the Bool could not tell apart. Receipts, by execution: four hermetic witnesses PASS; mutation collapsing ReceiptBytesUnreadable into the conformance gap turns the discriminating control FALSE; restored PASS. The wet witness is not executed here (Filesystem.Read; the hermetic envelope refuses it by construction). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * parse_json fail-open sites 4-6: the protocol-schema bisect probes and bundle stop attributing our own failures to their subject Sites 4 and 5 are BISECT PROBES over a vendored native executable, asking whether the protocol schema it emits decodes and canonicalizes. Returning Bool made `false` also mean "the file I was asked to read did not read" -- a fact about this harness, not the subject. A bisect run with a wrong staging path would have reported the executable as emitting undecodable schema and converged on a commit chosen by our own path bug. They now answer ProtocolSchemaFileStanding, in which exactly one arm (SchemaFileUnreadable) is ours and the two subject arms stay apart because they indict different things. Site 6 bundled one schema file through five refusals -- read, decode, canonicalize, canonical write, digest -- plus a manifest append, all answering one `false` that its caller folded into `all_ok`. A bundle failing on a full staging disk was indistinguishable from one failing on a non-conforming document. It now answers ProtocolSchemaBundleFileStanding with every arm carrying the path, because this runs inside a fold and a cause without a subject is equally unactionable. The manifest append has its own arm rather than borrowing the canonical-write one. The fold carries the first refusal instead of a Bool, and still short-circuits deliberately: later files are processed against a manifest already known incomplete, so their refusals would be consequences, not findings. WHERE THE WIDENING DIES, stated at the site and not only here: observe_protocol_schema_identity returns ContentHash? and has seven other `none` arms of its own, none of them among the nine. Widening it reaches four callers and is its own cut. The located cause is now computed and reaches that line; the next repair is to stop discarding it, not to argue discarding it is fine. EVIDENCE, honestly: these three have NO executing witness. Every one of them performs Filesystem.Read or a subprocess, which the hermetic envelope refuses by construction, and no fixture harness exists that can hand them a controlled file. That missing harness is this class's next-rung trigger, not a ceiling. What IS established by execution is that the module and its import closure compile and evaluate (the interpreter reaches CallContractMismatch at the entry, which is past typechecking). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * parse_json fail-open site 8 (Optional class): an unreadable /healthz body was reported to deploy operators as a stale surface At an Optional the failure is not merely unreported -- it is INDISTINGUISHABLE FROM THE ORDINARY NEGATIVE RESULT, which is strictly worse than the Bool sites. healthz_surface_projection returned String?, and `none` meant BOTH "this body is not JSON" AND "this body is JSON and does not carry the surface members". Its consumer turned both into false, rendered as ServedSurfaceStale -- a claim that the RIGHT process is serving the WRONG tree. So an endpoint answering an HTML error page (wrong process on the port, proxy error, empty 502) told the operator to rebind the graph when the actual question was what was answering at all. Now HealthzSurfaceProjection: Projected | BodyUnreadable | MembersIncomplete, the last carrying the present count, because the member count is a constant this module owns and "0 of 3" locates a dropped member without re-derivation. roadmap_site_healthz_surface_is_current still answers Bool, and the reason is stated AT THE SITE. Its two sides are not symmetric: the expected side is a document we render ourselves, so its refusals are our emitter's defect and carry no verdict about the service; the observed side's refusals are real observations, and they are not discarded because readiness has already parsed the same body for its release identity and refused on its own cause first, so BodyUnreadable is unreachable from that caller. Reachable from the function -- which is why it exists -- and unoccupied there. A caller reaching the predicate without an upstream parse does not inherit that and must consume the projection directly; that is written down. Receipts, by execution: two new discriminating witnesses PASS (an HTML body is BodyUnreadable; {"ok":true} is MembersIncomplete{0}), the existing projection witness still PASSES, and mutating the Absent arm to answer MembersIncomplete{0} -- exactly the old collapse -- turns the discriminating control FALSE. Restored PASS. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * parse_json fail-open site 9 (Optional class) + §4c annotation-grain repair to sites 4-6 supervised_thread_id_from_line returned NonEmptyStr? behind FOUR causes, and its last arm was `_ => none` over a coproduct whose variants have different remedies -- the shape DESIGN names as total at the level examined, blind one level down. An RPC ERROR is the provider refusing our thread-start; a DUPLICATE is two responses claiming one id, a wire protocol violation; neither is "this line was not the thread-start response", the ordinary answer for almost every line of a stream. At an Optional those are indistinguishable, so a supervised run whose thread-start was REFUSED looked exactly like one whose response had not arrived. A DEFECT FOUND WHILE WRITING THE POSITIVE CONTROL, reported rather than silently repaired: supervised_rpc_from_id_response takes `id: Int` and never inspects the document's id member -- the parameter only builds message text. Any well-formed response carrying result.<entity>.id is read as the thread-start response whatever id it answers. So ThreadIdLineNotThreadStart is unproducible today. The arm is KEPT, because mapping "addressed elsewhere" onto ThreadIdLineUnreadable would put a lie in the decoder to avoid an unreachable arm -- the exact conflation this change removes. No witness is written for it: its RED is unauthorable, and §4b rules such a probe worse than absent. Exhaustiveness needs the arm; evidence does not exist for it; the difference is stated. Next-rung trigger: the id check landing. It IS witnessed at its current wrong behaviour, so that fix turns that witness red at the line explaining why. Not repaired here: id matching is not a parse_json fail-open, and fixing it inside a decoder-honesty pass is the widening this pass exists to stop. §4c REPAIR TO SITES 4-6, AND A CORRECTION TO THAT COMMIT MESSAGE: it claimed package_delivery.dag "compiles and evaluates". It did not -- three annotations I had written INSIDE declaration bodies are refused at module-item grain, which surfaced only when a later entry resolved the same closure. They are hoisted to their declaration headers and the closure now resolves clean. The claim was too strong when made; the evidence it cited came from an entry whose path did not reach the check. Receipts, by execution: five witnesses PASS; mutating the RPC-refusal arm to answer the ordinary skip turns the discriminating control FALSE; restored PASS. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * parse_json fail-open site 7 (Optional class, last of nine): the v1 exact-head receipt decoder locates its refusal instead of summarizing it away verification_receipt_v1_decode returned Optional behind EIGHT decode stages, and the caller was already paying for the collapse: it rendered every one as the single sentence "the v1 exact-head body is not readable". A corrupt file and a receipt that decodes all the way to its verdict and stops got the same diagnostic -- a fabricated summary standing where a located cause existed and was discarded one frame earlier. Now LegacyExactHeadReceiptDecode, whose refusal carries a LegacyExactHeadDecodeGap naming the stage. The gap NAMES A STAGE, NOT A PARSE CAUSE: exactly one arm is about bytes, and it says what this module could not do -- read the receipt -- rather than re-spelling a tokenizer's complaint. The other seven name members of a schema this module owns, a vocabulary no codec can supply. The production caller composes its reason from the gap, so the located cause reaches the diagnostic it always should have. The two fixtures are FACTORED to differ in exactly one member: a hand-authored second document would let an unrelated typo produce the refusal the witness attributes to the missing verdict. That the untouched positive control (v1_decode_preserves_execution_rows) still passes is what establishes the refactor is faithful. Receipts, by execution: three witnesses PASS; mutating the verdict-missing arm to answer BytesUnreadable -- the old indistinguishability -- turns the discriminating control FALSE; restored PASS. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * say unproducible-today, not unreachable, on the mis-addressed-response arm The approving review on #9241 called ThreadIdLineNotThreadStart "the unreachable arm" -- the exact misreading the annotation exists to prevent, so the annotation was not doing its job. The two words read alike and only one is a permanent property. Nothing about this arm is structurally impossible: the moment a reader compares the document's id against the one it asked for, a mis-addressed line has an answer and this arm IS that answer. The consequence of the misreading is concrete rather than pedantic. Read as unreachable, the arm looks like something to delete, and deleting it re-collapses the distinction the id-matching repair depends on. Also: "evidence does not exist for it" -> "evidence cannot yet be authored for it", which is the actual reason there is no witness. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * the two cursor stream classifiers stop hiding an unreadable line among the lines they were always going to skip A CLASSIFIER IS THE WORST PLACE FOR THIS COLLAPSE, which is why these two are worth repairing even though only witnesses call them. A classifier is asked about EVERY line of a stream, so `none` is its ordinary answer and nothing about it looks wrong. Four different facts answered it -- unreadable line, absent type member, duplicated type member, not an object -- so a stream that went malformed halfway through (truncated write, interleaved writer, crash mid-line) was indistinguishable from a stream of lines the classifier simply had nothing to say about. The two share ONE vocabulary parameterised by the kind they yield, rather than two identical coproducts under different names: their failure modes are the same four facts about a JSON line and only the payload differs, which is what a type argument is for. WHAT IS DELIBERATELY NOT AN ARM: an unrecognised `type` VALUE. Both from_wire functions are total and answer their own unknown-kind variant, so "I read this and do not know this kind" is a CLASSIFIED answer, not a reading failure. The untouched unknown_event_stays_unclassified control is what keeps the new witnesses honest -- a decoder that refused an unknown kind would break the classifier while satisfying a naive refusal test. Receipts, by execution: six witnesses PASS (four existing, converted; two new discriminating); mutating all four causes back to one value turns the type-member control FALSE; restored PASS. Parse sweep clean at 3992 files, with the instrument first validated by planting an annotation between a type declaration and its = line and confirming it refused at exactly that file:line. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * the parse_json type cut: delete the Optional at the root, and the offset the parser always computed stops being discarded parse_json returned JsonValue?. The cut replaces it with parse_json_document -> JsonDocumentParse, and DELETES parse_json rather than keeping it beside the new surface: a surviving Optional is the attractor DESIGN's replacement-migration doctrine names, and every nearby question would keep being answered in its vocabulary. All 45 call sites across 28 files migrate in this change; the transition is atomic because there is no interval where both answer. THE CUT INVENTS NOTHING, WHICH IS WHY IT IS SMALL. parse_json_value_at has answered JsonParseFail { at: Int } since it was written, and parse_json matched that arm as `at: _`. Every consumer that wanted to say WHERE a document stopped being readable was one discarded binding away for its entire life -- and the fail-open repairs of the last two PRs each had to reconstruct a prose approximation of a fact the parser had already located. TWO GAPS, AND THE SECOND IS THE ONE THE OPTIONAL HID BEST. `{"a":1} garbage` PARSES, completely, into a valid value, and was then rejected by full consumption with the same `none` as `{ not json`. Opposite remedies: a writer appended to a document or two were concatenated, versus the bytes are damaged. ONE REFUSAL ARM CARRYING THE DISTINCTION INSIDE, not two arms at 45 sites, and the shape is argued rather than chosen for brevity. Two peer arms would force every caller to write both when the honest answer at most sites is one domain fact covering both exactly -- 45 mechanically duplicated arms are 45 places to drift, reading as a considered distinction where none was made. The inverse risk is real and is why the gap is a PAYLOAD rather than erased: this is precisely DESIGN's "total at the level examined, blind one level down", and the defence is that the distinction is CARRIED, not summarised. Binding it `_` and then asserting a cause is what is forbidden. THE RIDE-ALONG, per the ruling: 19 prose causes that re-spelled the parse failure now render the LOCATED gap through one shared json_document_gap_text, rather than a dozen decoders each inventing a spelling for one fact. Each site keeps its own domain subject ("the publication receipt is ...") and gains the offset. json_text_parseable stays Bool and binds the gap as `_` -- the one consumer that honestly discards it, because its entire question IS whether the text parses. There is deliberately NO arm for an empty document: empty text fails at offset 0 like any other malformed input. Receipts, by execution: the two witnesses that previously asserted one fact twice ("refused") now assert the two gaps AND THEIR OFFSETS -- 1 for `{not json` and 3 for `{} extra`. Asserting the offsets rather than only the variants is deliberate: a variant-only claim passes against a decoder that locates everything at 0. Six downstream witnesses across five migrated modules still PASS unchanged. Parse sweep clean at 3992 files. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * the type cut's one real casualty: a witness that depended on the fabricated summary, strengthened rather than patched CI floor on ce3f5c5: failed=1, and it is mine. roadmap_publish_witness_test a_receipt_that_is_not_json_refuses asserted that the refusal reason CONTAINED "complete JSON value" -- prose this decoder used to spell for EVERY unreadable receipt. The cut replaced that one sentence with a located gap, so the phrase now survives only on the trailing-content arm and the substring claim went red. That is the migration working rather than a regression: a consumer depending on a fabricated summary refused the moment the summary became a fact. So the witness is strengthened, not restored. It now asserts the located refusal EXACTLY rather than by substring, and THE OFFSET IS DERIVED RATHER THAN COPIED FROM A RUN: "not a receipt" is not a JSON value at its very first byte, so a parser reporting where the document stopped being readable must say offset 0. Copying an observed number would have made the assertion a change detector against itself. Added the arm the old prose could not distinguish at all: a receipt that PARSES COMPLETELY and is refused only by full consumption. Under the predecessor it produced the identical sentence as garbage, so a reader could not tell "these bytes are damaged" from "a writer appended to this receipt, or two were concatenated" -- opposite remedies, one string. Checked the rest of the corpus for the same dependency rather than assuming this was the only one: the other witnesses matching the old phrases (spark_serving_observe, diff_baseline) CONSTRUCT their own refusal fixtures and never reach the production parse path, so neither was affected. Receipts, by execution: both witnesses PASS, at offsets 0 and 3. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * REQUEST_CHANGES on #9241 (review 55992): the consumers erased the distinctions the coproducts had just modelled. Both findings were correct. FINDING 2 WAS THE SHARPER ONE AND MY ANNOTATION WAS FALSE. It read that an unreadable staging file "is distinguished at the match below rather than counted as a negative bisect result". It was not: the enclosing bisect probes reduced all three standings to `false`, so a staging file THIS HARNESS could not read reported exactly what a subject emitting undecodable schema reports -- the fail- open attribution the coproduct was introduced to repair. Worse than the defect alone, because a reader auditing the file would have found a written claim that the distinction survived. Fixed end to end rather than at the annotation: ProtocolSchemaFileStanding now propagates through both bisect probes, both materialize_ entry points, and into the two WET WITNESSES that terminate the chain, which branch on all four arms. There is no Bool left in that chain to collapse them. The generate-step failure, previously a bare `false`, is now SchemaFileUnreadable -- it is our staging, not the subject. FINDING 1: protocol_schema_bundle_file_admitted was a predicate over a coproduct whose caller turned the Bool into `none`, discarding the located cause one frame after computing it. I had annotated that as a scope boundary; the reviewer is right that "out of scope" is a reason I did not do it, not a reason collapsing is HONEST. The predicate is DELETED and replaced by a renderer, and observe_protocol_schema_identity now answers ProtocolSchemaIdentityObservation -- its eight `none` arms each name what the observation could not do, in this operation's own vocabulary. The bundle's per-file cause, path included, now reaches the receipt consumer, which already had a cause field and was being handed a fabricated generic sentence. Enumerated the six refusal arms rather than using `_`: a wildcard would silently mislabel any future success-like variant as a refusal, which is the total-at-the-level-examined shape this PR keeps repairing. MERGED origin/main AND FOUND A SECOND, UNRELATED BREAK MY OWN CHECKS COULD NOT SEE: extdeps/rust/cargo_diagnostic.dag landed on main AFTER this branch and calls the parse_json this cut deletes. My parse sweep reported 3994 files clean because IT ONLY PARSES -- the failure is name resolution, which the sweep does not do. Migrated it. The durable lesson for a root deletion is merge-then-regrep before pushing, not sweep-and-assume; the corpus-wide grep for the deleted symbol is now clean across every spelling. Receipts, by execution: both json witnesses and both publish witnesses PASS; package_delivery, cargo_diagnostic and both wet witness modules resolve and evaluate; sweep clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * remove the two SCM status files that a `git add -A` swept into this PR They belong to the status verb lane (#9257) and were never part of the parse_json work. They landed here because the previous commit staged with `git add -A` while the files sat untracked in a shared worktree, having followed a branch switch. No review caught it and no check would have: they compile, so the only signal was reading the commit's own file list. This PR is the parse_json cut and is reviewable precisely because it is one thing; two unrelated SCM modules make it neither. 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>
…r refused The floor refused this branch at strict preparation with eight located diagnostics -- `missing required field 'ancestry' in literal of type 'RepositoryCommit'` across scm_log_witness_test.dag and scm_status_witness_test.dag. status (#9257) and log (#9277) merged to main after this branch was cut, and their fixtures construct RepositoryCommit; merging main in succeeded TEXTUALLY while the type had gained a required member. THIS IS THE WALL FIRING ON ITS OWN AUTHOR, and it is the strongest argument the codec change could have made for itself. The required member REFUSED the old literals rather than defaulting them to RootCommit. Had it defaulted -- the convenient choice, and the one this stack argued against in prose one commit earlier -- six commits in the log fixtures would have silently become roots and every witness would have stayed green over a history that was not the one written. The two commits in the log ordering fixture are stated as a real chain, since that fixture is a history and stating one is the honest reading of it. The rest are roots: those witnesses are about positional references, held-ness and staging, and inventing descent to decorate them would be asserting a relation the claims do not test. RECORDED BECAUSE IT COST A CI CYCLE AND WILL AGAIN: the parse sweep reported 4064 files clean on this exact tree. It only PARSES, so it is structurally blind to name and type resolution -- a merge that is textually clean can be semantically broken and the sweep cannot see it. This is the second time in this lane. A main merge needs a resolve check, not a sweep. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… with intrinsic keys across the whole vocabulary, dissolving BOTH the O(n^3) cycle validation and the undischarged append-only wall (#9408) * scm: ancestry, landed before the commit verb that would have baked its absence in The model did not relate one commit to another. Every `parent` in gunbc.scm is TREE-NODE parentage inside the object store; none of it is ancestry. A RepositoryCommit is { root, message } and `commits` is a flat List, so a repository's history was a SEQUENCE and not a graph -- merge-base, ahead/behind, commits-since, log ranges and merge itself had no referent here. IT IS CARRIED, NOT RECOVERED FROM POSITION, and that is forced rather than chosen. Position gives a total order and says nothing about descent: reading index 1 as the child of index 0 assumes history is linear AND append-ordered, neither of which anything establishes -- there is no commit-authoring verb, so nothing defines what appending means. Recovering ancestry from position would not be recovering it, it would be inventing it, and the invention would be invisible because it agrees with position by construction. THE ROOT IS A STRUCTURAL STATE, not a parent field holding a "nothing" value, which would make "this commit begins the history" and "this commit's parent is missing" the same value -- the ordinary first commit and damage. Same refusal `log` made for the empty history, one layer deeper. EXACTLY ONE PARENT, DERIVED FROM THIS MODEL'S OWN MERGE RATHER THAN FROM GIT. `merge` takes ONE target Commit and a LIST OF PROPOSALS and answers ONE commit. A Proposal is a set of authored requirements: not a commit, no root, no message, no identity in history. So a merge here combines one commit with N things that were never commits, and has exactly one commit antecedent. Git's second parent exists because git merges two BRANCHES -- two commits -- and nothing in this model can merge two commits at all. A parent LIST would therefore not be more general, it would be an arm with no producer, which DESIGN 4b rules worse than absent because it is cited as capability the model lacks. WIDENING TRIGGER: if merge ever takes two Commits, this coproduct gains a several-parents arm and the change is a compile error at every consumer rather than a silent reinterpretation. AUTHOR AND TIMESTAMP ARE EXPLICITLY SEPARATED, not left to ride along. Parent is STRUCTURAL -- it relates two things the model holds and is decidable inside it. Author and timestamp are EXTERNAL OBSERVATIONS, and this repository has no modelled clock and no modelled process identity to observe them with; acquiring either is the same frozen-host question gating the store and process output. Modelling them here would mean inventing two facts to fill fields, at exactly the boundary a commit is supposed to be trustworthy. A cycle REFUSES rather than truncating or looping, detected by exhausting the population: a chain longer than the history must have revisited a commit, by pigeonhole, so the refusal is derived from the bound rather than asserted by a visited-set this module would have to keep correct. Receipts, by execution: seven witnesses PASS. THE SHARPEST, and it establishes the carried-not-position claim by execution rather than argument: replacing the walk with a FAITHFUL position-implies-ancestry implementation leaves the linear-history positive control GREEN -- because in a linear history position and ancestry coincide -- and is caught ONLY by the adjacent-roots witness. A second mutation reporting a broken parent as a completed trace reds only the broken-chain witness, leaving the linear trace green. Parse sweep clean. NOT DONE HERE, and named rather than left implicit: binding ancestry into RepositoryCommit is a WIRE-FORMAT change -- that type is codec'd with a member-set guard, and the envelope's header states the v1 body must stay frozen once documents exist. That binding is the versioned-codec step, and it is a different change from settling the model. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * scm/ancestry: the chain accumulates by prepend, reversed once at completion review 56072, and it is correct. `ancestry_walk_step` built the chain with concat-at-end, copying the whole accumulator per step -- O(n^2) over history length. DESIGN section 6 rules this class ALWAYS fixed regardless of the realized n, and preempts the "n is small here" defense by name: n is not a time-stable fact, and this particular n is the length of a repository's history, which is exactly the quantity that grows without bound in use. The fix is prepend plus one reverse at the single completion point, so the exported chain order -- descendant first -- is unchanged and no caller can observe it. The reversal is at completion rather than at each consumer because there is one completion and N consumers. WORTH RECORDING WHERE THIS CAME FROM. gunbc.scm.repository_envelope carries an annotation about having committed this exact defect and had it caught by review, whose stated lesson was that fixing a cost shape at the sites a review names is not the same as not having the defect. This module imports that module and reintroduced the shape anyway. The additional lesson, now in the source: reading the note is not the same either. The second half of the review is noted and not changed. commit_is_ancestor_of folds over the traced chain to find an element, which is O(n) over a bounded chain, not a quadratic shape -- and with the walk now linear the end-to-end cost is O(n) rather than the O(n^2) the review flagged for the pair. Receipts: all seven witnesses green after the change, run against a freshly built compiler rather than the stale local one. The order-sensitive witnesses -- a_linear_history_traces_from_the_start_back_to_the_root and a_stated_ancestor_two_generations_back_is_found -- are what would go red on a missing or doubled reverse. Parse sweep clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * scm/ancestry: an unknown START is the caller's fact, not a truncated history review 56102, and it is correct on both the conflation and its consequence. The outer AncestryUnknownCommit arm answered AncestryBrokenAt { commit: cursor, missing_parent: cursor } naming one commit as BOTH the site of damage and the parent that is missing. Two things were wrong with that, and the second is worse than the first. THE CONFLATION. "The commit you asked me to walk from is not in this history" and "commit c's parent p is missing" have OPPOSITE OWNERS -- a bad argument versus a truncated history -- and opposite remedies. It is the one-reason-symbol-over-two- opposite-states pattern this module's own header prose names, committed in the module that names it. THE FABRICATION. An unknown start supplies no parent, so there was no value to put in `missing_parent` and the walk INVENTED one. A consumer acting on the result would go looking for an object nothing ever claimed exists. That is the fabricated-plausible-output failure at exactly the boundary this module is meant to be trustworthy over, and it is why this could not be left as a naming quibble. The repair is a fourth arm, AncestryStartNotInHistory { start }, carrying only what the input supplied. Its reachability is by CONSTRUCTION rather than convention, and that is now stated in the source: the step advances the cursor only after lookup(parent) has already answered AncestryKnown, so every cursor after the first is a commit this history holds, and the unverified cursor is the starting one and no other. The reviewer derived this independently, which is the part of the finding I would not have caught from the type alone. Receipts: eight witnesses green, run against a freshly built compiler. The new one asserts the START IDENTITY rather than merely that some non-traced arm came back -- an implementation answering this arm for every input would satisfy a bare not-traced claim, and the real-trace and real-truncation witnesses beside it are what stop that reading. Parse sweep clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * scm: bind ancestry into the repository codec, while the wire format is still free THE WINDOW IS THE REASON THIS COMES BEFORE THE STORE BINDING, and it is in the carrier rather than in anyone's preference. repository_envelope states that the v1 body is frozen "once a v1 document exists anywhere" -- a CONDITION, not a date. Measured: encode_repository is referenced in exactly two places, its own module and one witness. Nothing writes a repository to disk anywhere in the tree. So no v1 document exists, the format is not frozen, and THE STORE BINDING IS PRECISELY THE EVENT THAT WILL FREEZE IT. Queuing the codec behind the store would mean waiting for the event that closes the window and then trying to change the format through it. Done in this order, the first document ever written already carries ancestry and needs no migration. That is the same argument as ancestry-before-commit, one layer out: there, no producer of a commit exists, so the shape can still be settled; here, no persisted document exists, so the format can still change. Both windows are open only because nothing has run yet, and both close on the same event. A WITNESS-BUILT DOCUMENT DOES NOT SATISfy THE FREEZE CONDITION, and the clause decides this rather than being read charitably: the same paragraph glosses itself as "once a document exists IN THE WORLD". A witness document is rebuilt from the current encoder every run, so it cannot ever disagree with that encoder -- it is not an artifact anyone must stay compatible with. Freezing over it would be freezing over something that can never produce the incompatibility the freeze exists to prevent. This is therefore an in-place v1 widening and NOT a second format arm; a v2 arm here would be the fabricated migration the module's own header refuses to build. A PARENT IS A COMMIT REFERENCE, NOT A NODE REFERENCE, reusing this module's own prior ruling rather than deciding afresh. The checked_out annotation records why it resolves against the COMMIT LIST: a node reference admits a document naming an arbitrary interior object -- a child three levels down -- as the thing pointed at, with nothing refusing because nothing asks. A parent has exactly that property. `root` may be a node reference because a commit's root IS a node; a parent may not, because a parent is a COMMIT. THE POSITION IS A STORAGE LOCATOR, NEVER AN ORDERING FACT. The reference names WHICH commit; adjacency between positions still means nothing, and a commit carrying no ancestry member refuses rather than defaulting to its neighbour. So this is not the position-implies-ancestry defect the ancestry module exists to prevent -- deriving a parent FROM a position would be, and nothing here does. DECODE IS TWO PHASES, and that is forced rather than tidy. A parent reference is a position in the commits array, and nothing requires a parent to appear earlier than its child; requiring it would impose a storage-order rule on a relation that has none. Phase one reads what the document says, phase two resolves once every position exists. PendingCommit is that intermediate state, and its Optional carries ONE meaning -- an unreadable member refuses in phase one and never reaches it. A MISSING `ancestry` MEMBER REFUSES; IT DOES NOT DEFAULT TO A ROOT. Defaulting would make every commit in an older document read as a beginning of history: a well-formed repository that is not the one that was written, which is the silent reinterpretation the identity-rule tag exists to prevent, arriving through the schema axis. A DANGLING parent refuses for the same reason rather than degrading to a root -- that would undo, at the only boundary where it matters, the structural-root distinction ancestry just established. THE CHECKED ENCODER ADJUDICATES A BROKEN PARENT BEFORE THE WRITE, joining the three refusals already there. encode_repository cannot refuse, so its only honest output is the empty reference decode later rejects -- which surfaces to whoever LOADS the document rather than to whoever caused it. RECEIPTS, BY EXECUTION, against a freshly built compiler: - 36 of 36 witnesses green (envelope + ancestry), parse sweep clean at 4024 files. - MUT dangling-parent-reads-as-root: ONLY a_dangling_parent_reference_refuses reds; the four others stay green. - MUT codec-silently-drops-ancestry: ONLY a_stated_parent_survives_the_round_trip reds -- and the_unmodified_wire_still_loads STAYS GREEN, which is exactly why that witness had to be written: a codec that drops ancestry still round-trips a well-formed repository, so nothing already in the file could have caught it. - Restored: all green. The three new exhaustiveness failures the arms caused in total consumers were repaired by naming the case, not by widening a wildcard -- the closed refusal domains doing the job they were split for. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * scm: state ancestry in the log and status fixtures the required member refused The floor refused this branch at strict preparation with eight located diagnostics -- `missing required field 'ancestry' in literal of type 'RepositoryCommit'` across scm_log_witness_test.dag and scm_status_witness_test.dag. status (#9257) and log (#9277) merged to main after this branch was cut, and their fixtures construct RepositoryCommit; merging main in succeeded TEXTUALLY while the type had gained a required member. THIS IS THE WALL FIRING ON ITS OWN AUTHOR, and it is the strongest argument the codec change could have made for itself. The required member REFUSED the old literals rather than defaulting them to RootCommit. Had it defaulted -- the convenient choice, and the one this stack argued against in prose one commit earlier -- six commits in the log fixtures would have silently become roots and every witness would have stayed green over a history that was not the one written. The two commits in the log ordering fixture are stated as a real chain, since that fixture is a history and stating one is the honest reading of it. The rest are roots: those witnesses are about positional references, held-ness and staging, and inventing descent to decorate them would be asserting a relation the claims do not test. RECORDED BECAUSE IT COST A CI CYCLE AND WILL AGAIN: the parse sweep reported 4064 files clean on this exact tree. It only PARSES, so it is structurally blind to name and type resolution -- a merge that is textually clean can be semantically broken and the sweep cannot see it. This is the second time in this lane. A main merge needs a resolve check, not a sweep. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * scm: refuse a cyclic history at both ends of the persistence boundary review 56207, both findings, and the second is a hole THIS PR OPENED rather than one it inherited. THE CYCLE ADMISSION. The checked encoder verified that every parent occurs in `commits` and then succeeded. A two-commit cycle satisfies that completely -- membership and acyclicity are different properties and the first does not imply the second -- so the persistence boundary would have serialized a state gunbc.scm.ancestry explicitly classifies as a REFUSAL. Before the ancestry member existed a cycle had no spelling on the wire at all; binding it is what created the ability to persist one, which is why this belongs in this diff and not a follow-up. REFUSED AT BOTH ENDS, NOT JUST THE ONE THE REVIEW NAMED. The review named the encoder. The encoder's argument is a value some caller in this process built; a DOCUMENT is bytes from anywhere, and a hand-authored one can state a cycle whether or not any encoder here would produce it. Guarding only the write path would be a wall that fires solely on its own author -- and the untrusted direction is the one that matters. The decode check runs AFTER parents resolve and BEFORE the checkout, because a cycle is only decidable once every reference denotes a commit. THE DETECTION IS BORROWED, NOT REBUILT. ancestry_walk already decides this, by exhausting the population rather than by keeping a visited set. Re-deriving the test inside the codec would have been a second answer to one question, and the two would drift the first time the walk's bound changed. COST, DECLARED RATHER THAN HIDDEN: one walk per commit is O(n^2) over history. A linear alternative needs a keyed visited set, which this layer's positional list does not give, and the walk is the only acyclicity authority. It sits on a boundary crossed once per write rather than inside a fold; the shape is stated at the site with its dissolution trigger (a keyed commit list) instead of being accepted silently. THE PREDICATE FINDING, and I am resolving it on the fact that decides it rather than on the doctrine cited. `ancestry_is_root` had NO PRODUCTION CONSUMER -- its only caller was the witness asserting it works. A helper whose sole consumer is its own test is an artifact with no final consumer, so it moves into the witness and out of the module's exported surface. I am not adopting the "predicate dissolution" framing: DESIGN states no such rule, and gunbc.scm.load_standing carries two functions of exactly that shape on main, which would be violations if it did. The right reason is consumer count, and by that reason the reviewer's conclusion is correct. Receipts, by execution against a freshly built compiler: both new refusals green, and the POSITIVE CONTROL is the load-bearing one -- scm_env_the_cyclic_fixture_has_every_parent_in_the_commit_list establishes that the fixture satisfies the membership check the encoder already had, so the two refusals are about the CYCLE and not some unrelated defect. The decode witness builds its document with the UNCHECKED encoder, so the bytes are exactly what a writer without this wall would have produced. 42 further witnesses across log, status, envelope and ancestry green with no failures. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * scm: the checkout verb at repository grain, and what it deliberately does not consult Checkout already existed at OBJECT grain -- reconstructing a program from a commit's root closure. What was missing is SELECTION: which commit a repository is positioned at. This adds that half. TWO GRAINS OF ONE VERB, IN THE MODULE THAT OWNS IT. Putting the repository-grain half in its own file would have minted a second name for one verb -- the module would have had to be called something that is not "checkout" while being exactly checkout. Import direction was checked rather than assumed: repository_envelope reaches object_store, ancestry, target_reference, json_member and the closure carriers, none of which reach checkout, so the new edge closes no cycle. CHECKOUT SAYS NOTHING ABOUT ANCESTRY, AND THAT IS DERIVED RATHER THAN OMITTED. The silence is stated in the source because a later reader finding no mention of ancestry in a verb that selects a commit would reasonably read it as an oversight and "fix" it. A commit's program is its ROOT CLOSURE. Ancestry is a chain over COMMITS. Two different graphs over two different populations, and reconstruction walks only the first, so no ancestor needs to exist, or be readable, or be consistent, for a checkout to be exactly right. THE CONSEQUENCE IS NOT COSMETIC AND IT HAS A WITNESS PAIR: a commit whose stated parent is missing CHECKS OUT SUCCESSFULLY, while an ancestry walk from that same commit answers AncestryBrokenAt. One repository, one commit, two questions, two different answers, both correct -- the history is truncated and the program is not. The second witness is what makes the first mean something: without it the successful checkout could be a fixture that accidentally has no ancestry rather than checkout correctly ignoring it. Making checkout refuse there would invent a dependency the model does not have, and would mean a damaged history silently costs a user access to programs that are wholly intact. THE REFUSAL ARMS CARRY NO REPOSITORY -- the root-commit discipline one layer out. Had a failed checkout answered an envelope with nothing selected, "this checkout did not happen" and "this repository has nothing checked out" would share a representation, the second being an ordinary state the envelope's own header calls not an error. THE TWO REFUSALS ARE SEPARATE BECAUSE THEIR OWNERS ARE OPPOSITE. An unresolved reference is the CALLER'S fact; an unreconstructable program is the STORE'S. Collapsing them would hand a user "no such commit" for a commit sitting in front of them in the log. IT WRITES NOTHING. A new envelope with the selection moved, argument untouched, so the verb stays a pure transform. Persisting is a separate operation at a boundary this module deliberately does not reach -- the held frozen-host ruling. NO Bool PREDICATE OVER THE COPRODUCT IS EXPORTED. A `checkout_succeeded` convenience was written and REMOVED before this landed: its only consumer would have been the witness asserting it works. That is the same objection review 56207 raised against a sibling helper in gunbc.scm.ancestry, applied here before review had to; the reason is consumer count, and consumers now match the arms so a fourth arm fails to compile at every site rather than being absorbed into a false. Receipts: six witnesses green against a freshly built compiler; parse sweep clean at 4064 files. The mutation is the plausible later "fix" -- make checkout consult ancestry -- and it reds ONLY scm_ck_a_commit_with_a_missing_parent_still_checks_out while the other five stay green, including the companion witness proving that fixture's history really is broken. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * scm/ancestry: an empty history is not a cycle — decide membership before the walk review 56225, and it is correct. `ancestry_walk` over an EMPTY history folds zero times, so `done` stays false and the fallthrough answered AncestryRevisitsACommit -- a CYCLE, concluded from having looked at nothing at all. WHY THE FALLTHROUGH WAS WRONG RATHER THAN MERELY UNLUCKY. It encodes a pigeonhole argument: a chain longer than the population must have revisited a commit. That argument needs at least one step to have been taken. With zero steps it is vacuous -- and an empty population cannot contain a cycle at all, so the answer was not just unproven, it was impossible. That is the fabricated cause this module's own header refuses, committed in its own walker. THE REPAIR IS NOT A SPECIAL CASE FOR EMPTY, and that distinction is the whole content of the fix. The start's membership in `history` is decidable up front, and answering AncestryStartNotInHistory when it is absent is exactly what the first step would have concluded anyway, since lookup would have said so. The empty history then falls out as an INSTANCE -- nothing is a member of nothing -- rather than as a branch a future editor has to remember exists. It also makes the arm's meaning honest. The refusal previously fired from `lookup` returning unknown, which is a statement about the LOOKUP'S DOMAIN; it now also fires from membership in `history`, which is the population the arm is named for. Those two were assumed to agree and nothing said so. Receipts: an_empty_history_is_not_a_cycle asserts the START IDENTITY on the start-not-in-history arm, not merely that the answer is not a cycle -- an implementation answering that arm for every input would satisfy the weaker claim. Its POSITIVE CONTROL, a_start_inside_the_history_still_walks, is the load-bearing half: the empty-history witness supplies a lookup that answers KNOWN for every identity, so a gate that merely trusted `lookup` would have walked happily and passed. The control establishes that the gate did not break the ordinary case. All ancestry witnesses green, plus the codec's cycle refusals which route through this same walker. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * scm: a checked-out selection names a ROW, not a root — the carrier was lossy review 56230, and it found a live defect that predates this branch: the checkout verb exposed it rather than created it. WHAT WAS WRONG. RepositoryEnvelope stored the selection as the commit's ROOT. But `commits` may legitimately hold two rows with the same root and different messages -- gunbc.scm.log's own witness two_commits_sharing_a_root_still_get_distinct_references exists because it can -- so a root is NOT a unique key into that list. Every reader resolved it to the FIRST matching row. MEASURED BEFORE THE REPAIR, by execution: check out the second of two shared-root commits, ask `status` which commit you are on, and it reports the FIRST one's message. Nothing refuses. The user is told they are on a commit they did not select -- a wrong answer delivered as an ordinary success, which is the failure DESIGN section 5 forbids at a user-facing boundary. THE WIRE WAS ALREADY RIGHT AND THE CONVERSION WAS THE DEFECT. This module's own annotation says the encoded reference "means the commit at this position in this document and nothing outside it". Decode threw that away by resolving the position to a root, and encode recovered a position by searching for the first row carrying it -- so a repository selected at position 1 with a shared root ROUND-TRIPPED TO POSITION 0. That is data loss on the persistence path, and it was reachable before ancestry or checkout existed. Carrying the reference end to end DELETES both conversions rather than adding a check -- construction over validation -- and the wire FORMAT is unchanged, so this needs no second format arm. Only which position is emitted becomes faithful. IT DOES NOT REDEFINE COMMIT IDENTITY, and that distinction is load-bearing because the envelope's header explicitly says identity IS the root. A SELECTION is a different question from an IDENTITY: it names a row in this document's list. Both statements survive unchanged. CheckedOutCommitMissing now names the REFERENCE rather than a root, because when a selection does not resolve there is no commit and therefore no root to name. Reporting one would have meant inventing it or echoing a value that denotes nothing here. `commit_with_root` is deleted -- it had no remaining consumer once resolution went by reference, and its only behaviour was the first-match rule that caused this. Receipts: 48 witnesses green across envelope, log, status, checkout and ancestry; parse sweep clean. The two new claims are a PAIR and the pairing is the content -- checking out position 1 must report SECOND, and position 0 must report FIRST. The second is not decoration: without it the first would be satisfied by a reader that always returns the LAST row instead of always the first. Both assert through `status` rather than through the envelope field, because the field being right is not the claim; the claim is that the user is told which commit they are on. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * scm: hoist a §4c in-body annotation out of a witness match body The annotation sat inside the match body of scm_env_a_valid_commit_reference_checks_out. §4c models module-item grain only, so both required lanes refused it — the floor at strict preparation (:420-423, line grain) and the build lane's v2-emission phase at emit (four byte-ranges, which resolve to the four `//` lines of ONE comment block, not four sites). One defect, two lanes, reported in two grains. The annotation is preserved verbatim above the `test fn` declaration; only its position changed. The in-body remainder is now the bare assertion it always was. Verified by execution on a remote dispatch: all 31 witnesses in this file return `true`, including the repaired site. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * scm/ancestry: an ancestry edge names a history RECORD, not a program A commit root identifies a PROGRAM. It does not identify an occurrence of that program in a repository's history, and this model already admits two commit records sharing one root and differing only in message -- which is why `log` derives references from list position rather than root lookup. So `DescendsFrom { parent: ObjectId }` named something that does not uniquely identify what it points at. The decisive history is an ordinary revert: record 0: root A, RootCommit record 1: root B, parent -> record 0 record 2: root A, parent -> record 1 Content addressing correctly gives records 0 and 2 the same root. Root-keyed ancestry then requires A to be simultaneously `RootCommit` and `DescendsFrom{B}` -- a contradiction at the level of the type, one key with two irreconcilable values. Against the first-match lookup this stack was about to grow, a walk from record 2 answers with record 0's `RootCommit` and terminates immediately: record 1 and the revert edge vanish. Not a refusal, a confident wrong answer. THE RECUT. `RepositoryCommitRef` is declared here, and the whole walk API -- `DescendsFrom`, `AncestryStep`, all four `AncestryWalk` arms, the accumulator -- is keyed on it. It is declared HERE because this module's subject IS the relation between history records, so it owns the identity of the thing it relates; the envelope imports ancestry, so declaring it downstream and reaching back would be a cycle. ancestry.dag consequently no longer imports object_store at all. The type's annotation carries the boundary rule rather than a list of sites: an ObjectId is the right key for content-addressed OBJECTS, where uniqueness is the point of the identity; a commit record is a program plus a message plus a position, and only the last is unique. REPRESENTATION IS DEFERRED, and the deferral names both invariants a positional spelling would owe -- append-only for STABILITY, and order-preserving as a CODEC obligation. An earlier-only rule buys acyclicity and is NOT a substitute: against a list whose indices move it holds throughout while every stored reference silently repoints. `commit_is_ancestor_of` is DELETED rather than typed. It answered `false` for four different facts -- a completed trace proving non-ancestry, a broken chain, an unknown start, and a cycle -- of which only the first is a negative answer. There is no production consumer and `AncestryWalk` already carries all four states distinctly, so a typed judgment today would mint an arm with no producer. The witnesses derive their own Bool through a local helper whose annotation carries the rule that matters: any NEGATED use needs a positive control over the SAME fixture, because a negation is satisfied by a walk that failed for any reason, and a control over a different fixture catches a total failure while missing a selective one. The two-root fixture is hoisted so its negation and its new positive companion share it by construction rather than by copying. Verified by execution, all 11 witnesses green, including the two that a root-keyed model cannot satisfy: the revert traces all three records, and the reverted-to record is an ancestor of the revert while not being the same record. Per DESIGN 4b(4) those stay enrolled after greening rather than retiring. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * scm/ancestry: attach the deletion rationale to the surface it describes The block explaining why there is no Boolean ancestor predicate sat at end-of-file with no declaration after it. §4c attaches an annotation to a FOLLOWING module item, so fourteen diagnostics fired -- one per line -- and both required lanes refused before any witness could run. It is an annotation about an ABSENCE, which §4c has no attachment point for: the thing it describes is a function that is not there. It now sits above `ancestry_walk`, which is the surface the block itself points at -- "the walk itself is the surface", "a real consumer derives its answer from ancestry_walk" -- so the deletion rationale reads as part of why that surface has its shape. Content unchanged; only its position. THIS IS THE SECOND §4c AXIS AND THE FIRST ONE'S CHECK DOES NOT COVER IT. The in-body-annotation defect earlier in this stack was found by a brace-depth scan, which by construction cannot see a block whose problem is that NOTHING follows it. Both axes are checked by `v1_src_dag_parse`, which was built and run against this fix -- 4024 files parse-clean -- rather than relied on from memory. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * scm/ancestry: one carrier for the history, so two authorities cannot disagree `ancestry_walk` took a `history` list AND a `lookup` function, and that pairing was the defect. `history` was consumed only as the fold's sequence, its element bound to `_unused`, so it supplied the STEP BUDGET and nothing else while every membership question was answered by `lookup`. Two authorities for one fact (DESIGN §3), free to disagree, and they did: an EMPTY history folded zero times, so the accumulator's INITIAL value survived as the verdict and the walk announced a revisit having observed nothing at all -- a default doing duty as a conclusion; a start ABSENT from history but known to lookup traced normally, so the arm named AncestryStartNotInHistory was decided by a lookup fact rather than the history fact it names; a parent ABSENT from history but known to lookup was traversed rather than reaching BrokenAt. THIS IS PRE-EXISTING, NOT INTRODUCED BY THE IDENTITY RECUT. The pre-recut head d36e7f20b carries the identical fold, the identical `_unused` binding and the identical initial-accumulator-as-verdict; only the type names changed. Recorded because the record matters. THE CARRIER, NOT A CHECK. A membership test before the fold would have closed the empty-history case and left the parent mismatch constructible -- it concedes the bad state is writable and guards one instance of it. RepositoryHistory carries the rows, and membership, relation and step bound all derive from them, so the disagreement is unrepresentable rather than validated (§5, construction before validation). Three things follow rather than being added: CommitAncestryLookup is DELETED. "Is there a row, and what does it say" is exactly `AncestryStep?`; keeping both was two spellings of one question. AN UNREACHABLE ARM DISAPPEARS instead of being handled. The accumulator now carries the RESOLVED row rather than a bare cursor, so the step never re-looks-up the cursor and has no not-found case to answer for. The old shape filled that impossible case with AncestryStartNotInHistory -- wrong mid-walk, where the cursor is not the start. THE PIGEONHOLE ARM BECOMES HONEST. Reaching it now requires at least one fold iteration, which requires a non-empty carrier, so it is a derivation rather than a default that survived. The empty-history specimen is enrolled as a witness and stays enrolled after greening (§4b(4)), with a positive control over history_step_at so that a lookup answering Absent for everything cannot satisfy it. Verified by execution: 13 of 13 witnesses green, under a guard that aborts if the branch changes mid-run. Main merged first so the carrier lands once on a current base. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * scm/ancestry: delete ancestry_is_root, the annotation's own claim made true The module's annotation stated that the same consumer-count reasoning which removed the Boolean ancestor predicate had also deleted ancestry_is_root. It had not: the function was still defined a hundred and sixty lines above the sentence claiming its removal, with the witness as its only consumer. A PR does not get to ship a claim its own diff falsifies. THE DELETION IS INDEPENDENTLY JUSTIFIED and that is what makes it the right repair rather than a rationalisation. Zero production consumers, corpus-wide, on exactly the criterion already applied to commit_is_ancestor_of in this same file -- a criterion that existed before the annotation did. Changing code to match prose is only correct when the code change stands on its own; otherwise it is deleting a working function because a comment claimed it was gone. The witness derives the root state locally, KEEPING THE POSITIVE AND NEGATIVE IN ONE ASSERTION. A local reader asserting only the negative half would reintroduce the vacuous-green hole this file closed earlier: a negation is satisfied by any failure, so it needs a positive over the same fixture and mechanism. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * scm: retract the UNREPRESENTABLE overclaim, and repair the log claim this diff falsifies Two annotation defects, both of them false statements in prose this PR authors. ancestry.dag claimed the RepositoryHistory carrier made the list-versus-lookup disagreement UNREPRESENTABLE. It does not. Two steps may carry the same `at` and history_step_at resolves by first match, so one carrier can still disagree with itself under a duplicated key -- the same first-match class this change removed, one level down. The narrow truth is that the three enumerated disagreements are removed outright, which is what the shape actually buys. The fact now lives in exactly one place. It was stated in two -- here and beside the codec's builder -- and two annotations that agree are still two authorities for one fact. The carrier is the right home because the carrier is what the fact is about; the codec references it rather than restating it. The residual state, its rung (mechanically prevented at each builder, not structurally impossible), why a uniqueness CHECK would be the wrong repair, and the next-rung trigger are all recorded there. UNREPRESENTABLE survives once, as the disavowal. log.dag stated that there is no ancestry relation at all and that nothing else in gunbc.scm names one. This PR makes the second half false. The bullet is replaced rather than struck, because it carried two claims with different fates. RepositoryCommit still has no parent field -- that arrives with the codec -- so a log row still cannot name one and only the reason changes. And merge-base, ahead/behind and commits-since still have no referent: grepping gunbc/scm for them returns prose only, no declaration. Striking the bullet whole would have deleted a true statement in order to repair a false one. status.dag makes a structurally similar claim and is deliberately NOT touched. Its stated reason is NO BRANCH and NO REMOTE, and ahead/behind relates two named endpoints: ancestry is necessary for it and not sufficient. Neither this PR nor the codec PR supplies a second endpoint, so that sentence and its reason stand. Annotation-only: every changed line is a // annotation, so by DESIGN section 4c the semantic projection is untouched. Parse sweep 4083 files clean. * scm: build the ancestry history linearly, and keep the reverse for the reason it is actually load-bearing repository_history appended with `concat(acc.steps, [step])`, which copies the whole accumulator per row and makes building an n-commit history O(n^2). DESIGN section 6 fixes that shape ALWAYS, regardless of the realized n, because "n is small here" is not a time-stable fact. This module had the receipt in front of it: gunbc.scm.merge carries an annotation recording that it committed this exact defect, had it caught, and repaired it this exact way. It was reintroduced here anyway, which is what that rule exists for -- the shape travels. It now prepends, which is the whole of the cost repair. THE TRAILING `reverse` IS KEPT, and the first version of this annotation gave the wrong reason for it -- claiming it restored "the commit order the codec must preserve". No such obligation exists. RepositoryHistory is never encoded; the wire carries commits plus per-commit ancestry, and the positional reference is into `commits`, never into `steps`. Going to build the discriminating red for that sentence is what showed it had none. Step order is not unobservable, which is the correction that decides the line: it is OBSERVABLE BUT UNSPECIFIED. a_cyclic_commit folds these steps and reports the FIRST whose walk finds a cycle, and that commit reaches a user as the actionable example in a cycle refusal. Reversing the sequence names a different commit -- a changed user-visible output that no witness fails on, because the interface deliberately declines to promise WHICH commit. So dropping the reverse would make one commit repair a cost shape AND silently change a refusal's content, with nothing in the corpus to catch the second. Bare-minimum-cost does not object: it targets a cost SHAPE defect, the shape is what this fixes, and one more linear pass over an already-linear construction is a constant factor rather than a shape. No witness is added for it, deliberately. Asserting which commit a cycle is reported from would be a change detector over an explicitly unspecified choice, and would freeze into the interface precisely what that module refuses to promise. The alignment of steps[i] with commits[i] is recorded as a TRAP for the next reader -- what deleting the line would change -- not as an invariant anyone may rely on. The uniqueness fact is no longer restated here. It lives once, on RepositoryHistory in gunbc.scm.ancestry, and this module references it. Receipts: 11 order-, cycle- and parent-sensitive envelope witnesses green against the committed subject, 0 failures. Parse sweep 4083 files clean. * scm: name checked_out in the reference-vocabulary residue the module already declares The merge that re-rooted this branch onto the ancestry recut left one module holding two spellings of one concept: `RepositoryEnvelope.checked_out` is a `String?` naming a history ROW, which is exactly what `RepositoryCommitRef` was minted for. NOBODY AUTHORED THAT DUPLICATE. It was created by INTEGRATION -- neither branch had it alone. RepositoryCommitRef did not exist in the checkout branch's world, and String? was not a duplicate spelling until the row-keyed recut landed beside a checkout selection that had independently stopped being a root. That is worth naming as its own category: it is not a pre-existing weakness, because nobody wrote it, and it is not a claim this diff falsified, because nothing went false. TYPING `checked_out` ALONE WOULD BE THE WRONG REPAIR, which is why this is a declared gap and not a small fix. The decode side already keeps bare-text references and this module's own annotation already calls that a REMAINING conflation. Converting one leaf while the other stays bare relocates the fork rather than removing it, and leaves an intermediate state in which a reader must know which half was converted -- the leaves-upward migration DESIGN's replacement doctrine refuses. The root is the reference vocabulary as a whole: checked_out, the decode-side reference arms, and every other bare-text spelling of a row reference, in one motion. So this extends the EXISTING residue annotation rather than adding a second one. The fact now lives on the module that owns the concept instead of in a review thread, where the next author would have had to rediscover why two spellings sit side by side. Annotation-only: every changed line is a // annotation, so by DESIGN section 4c the semantic projection is untouched. Receipts: 8 of 8 checkout witnesses green after the re-root, 0 failures, including both re-rooted onto the carrier. Parse sweep 4084 files clean. * Classify the two ancestry decode refusals the merge with main left unclassified Integration, not either side, created this obligation. main landed repository_envelope_load_standing total over RepositoryDecodeRefusal as that population stood; this branch widened the population by two (RepositoryCommitParentReferenceUnresolved, RepositoryDecodedAncestryCyclic). Neither change touched the other's lines, so git merged both cleanly and the exhaustive match silently stopped being exhaustive. Both classify as LoadDocumentMalformed. An unresolved parent reference is a document naming a commit it does not contain, the same damage the root and checkout arms already carry. A cycle is not a rule a newer writer might implement and this build might lack -- acyclicity is a substrate law, so no conforming writer emits one at any version; calling it unsupported would tell a reader to stand aside for a document that is damaged. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Delete the unused commits parameter this branch added back, and correct the cycle-validation exponent Two findings from external review, both against claims this branch authored. The commits parameter on encode_commit_record was ADDED by this branch, not left behind by it: main carries encode_commit_record(acc, commit). The branch removed the first-match search from encode_ancestry, annotated that "the parameter that made the search possible does not exist to be misused", and threaded the parameter through the enclosing record encoder unread. An unused population parameter at the exact site that used to search that population is the cheapest route back to the first-match defect, needing no new argument at any call site. The cost annotation said one walk per commit is O(n^2). That counts the walks and takes each walk to be linear without opening it: history_step_at folds the whole step list, ancestry_walk performs one such lookup per step, and a_cyclic_commit runs one walk per start. The total is O(n^3), and the ordinary acyclic case realizes it because no start finds a cycle early. All three factors dissolve on the same keyed-representation trigger, so the figure is corrected and the shape stays declared rather than partly repaired. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * State the cycle-validation shape as a declared cost defect with its trigger named Lane-owner ruling B, after independently deriving the nesting: the corrected figure ships, the shape is fixed on the reference-vocabulary keying cut, and that cut comes forward as one piece over the whole vocabulary rather than as leaf conversions. Also corrects a second understatement authored here: the validation runs on encode and decode, not once per write. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Fix a type error this branch authored: DescendsFrom.parent given an ObjectId review 56439. The log witness fixture passed a.identity -- an ObjectId -- where DescendsFrom.parent declares RepositoryCommitRef. Every other fixture in the branch spells it RepositoryCommitRef { reference: "0" }; this one did not. Position 0 is commit a, which is the intended parent. The compile is NOT the evidence here, and that is worth recording. Measured on this tree: a record literal carrying BOTH this error and a plain-field error (root: String where ObjectId is declared) compiles 0 blocking, while an undefined variable in the same function refuses with EXIT=1. So the function is compiled and checked, and declared field positions are not the part being checked. The witness passed CI because gunbc.scm.log reads neither ancestry nor parent, so the wrong-typed value was written and never read. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Delete RepositoryCommitRecord: this diff made it describe an invalid wire record Reversal of a disposition this PR's body records, taken on an argument better than the one I declined. I declined this as a pre-existing weakness on the test "did my diff falsify a claim about it". That test is right and I applied it too narrowly, looking only for prose claims. A declaration's name and fields ARE a claim, and this diff falsifies it: before the ancestry widening the dead carrier's two fields corresponded to the wire record's two members; the wire now allows and requires ["root", "message", "ancestry"] and decode refuses a missing one, so the carrier can no longer represent any valid record. That transition is caused here. It sits immediately before the real three-field RepositoryCommit, in the module that owns the wire format, with the next work being the first production commit producer -- a well-typed, production-located declaration under exactly the right name describing the superseded shape. Deleted rather than widened: adding ancestry would preserve a second unused representation of the record. Not renamed to a legacy form either -- no durable repository format exists yet, so that would fabricate a compatibility subject. Single occurrence corpus-wide, no annotation attached, nothing lost with it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Declare the append-only wall this codec does not discharge, and its ordering obligation review 56461, whose citation is this repository's own: gunbc.scm.ancestry states that a positional spelling owes an append-only wall and an order-preserving wall. This codec discharges the second -- guarded by the decode-order pair and the root-signature order witness -- and does not discharge the first. RepositoryEnvelope.commits is an unrestricted List, so an insert, delete or reorder retargets every still-valid parent reference at once, and neither the membership nor the cycle check can see it: every reference still resolves, to the wrong row. What makes it not yet harmful is also what makes it urgent, and stating only the first half would be the reachability-read-as-occupancy error. No commit-authoring verb exists anywhere in the corpus, so no operation can mutate the list and the state is reachable only by hand-authoring. The commit producer is the next work, so this is an ordering obligation rather than a backlog item: the wall must exist before the first producer, because the producer is what makes the state reachable. Trigger is the reference-vocabulary keying cut, which dissolves it by removing positions altogether. The binding still lands here because nothing has ever written a repository document: the format is not frozen, so binding costs no migration, and deferring would move the format change to the far side of the event that freezes it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Declare the envelope witness module's live-tree disposition so its 37 claims execute Found while checking whether this PR's own receipts run, rather than whether they pass. A module that declares no live_tree_disposition resolves to ReadsLiveTree by the floor's fail-closed default -- v2.workflow.floor_discovery_producer answers `Absent => EntryLiveTreeResolved { disposition: ReadsLiveTree }` -- and a ReadsLiveTree site is declined before the fold, counted in declined_live and never executed. This module carried no declaration, so its witnesses were discovered, counted, and asserting nothing while reading as coverage. Thirteen sibling gunbc.scm witness modules declare it; this one did not. The omission predates the ancestry work: the module lacks the declaration on main too. What this PR added was 37 claims into a module CI never runs, and a body citing them as receipts. SubstrateInputsOnly is a true statement about this module, not the convenient one: its whole import surface is std.types, the json grammars, v2.std.node and three gunbc.scm carriers, and nothing here opens a file, shells out or reads the tree. This may surface failures or cost diagnostics in claims that have never run in CI. That is the point of enrolling them. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Retract an unmeasured claim from the annotation that added the disposition The previous revision of this annotation asserted that these witnesses "were discovered, counted, asserting nothing" and never executed. THAT WAS NEVER MEASURED. What was measured: the module declared no live_tree_disposition while thirteen siblings do, and the run reported declined_live=902 -- aggregate, and attributable to no module, because the floor's output names no module's disposition anywhere. What was inferred and stated as fact: that these claims were among the 902. The reasoning came from v2.workflow.floor_discovery_producer answering `Absent => ReadsLiveTree`. That is a real code path but not established to be the executing one -- the floor consumer resolves an undeclared module by deriving from its import closure, so a substrate-only module may have been admitted all along. Two computations of one fact, and the annotation read one and asserted it of the other. The declaration stands unchanged and is correct under every mechanism in play, because SubstrateInputsOnly is a true statement about this module's import surface, verified before declaring. Silence is the one answer that cannot be right; that is the reason to declare, and it needs no claim about what the silence did. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Retract the second claim too: this declaration does not change whether these claims execute Read from source, not from a rerun. The floor's automatic route is a column-zero text scan in witness_file_from_source: a line must starts_with("data ") AND contain BOTH LiveTreeDisposition AND ReadsLiveTree. undeclared matches nothing -> reads_live_tree false -> ROUTED SubstrateInputsOnly matches nothing -> reads_live_tree false -> ROUTED Same answer before and after this row. The 37 claims were executing already, so "declaring it is what makes them execute" is false and is withdrawn. My first commit said they were declined; my second retracted that but kept the second- order claim and asserted a derivation the floor does not perform. Where the row does change something is the SELECTION path: parse_entry_live_tree_disposition ends Ok(declared.unwrap_or(true)), so silence reads as live and the module is not selection-eligible. Declaring SubstrateInputsOnly makes it eligible. Real effect, different effect. The reason to declare is therefore ambiguity, not execution: three routes read this fact and disagree about silence, which cli_run.rs records at the scan as "ONE FACT, TWO COMPUTATIONS, IN ONE BINARY -- a section 3 defect". An authored answer removes this module from that disagreement without pretending to resolve it. Also withdrawn, refuted by arithmetic on my own receipt: that claims are missing from the floor's counters. 11647 routed + 541 declined_long + 902 declined_live = 13090 offered, exactly. The partitions are exhaustive and I had the numbers when I said otherwise. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Key SCM commit references by minted identity * Build SCM fixtures through the commit mint * Witness intrinsic key stability under reorder * Migrate checkout to intrinsic commit keys * Restore truncated ancestry checkout witness * Give revert ancestry fixtures distinct keys * Close ancestry witness key vocabulary * Remove unexplained SCM ancestry membership edges --------- 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>
The verb layer's second authoring-side surface. Nothing here is a UI preference — every decision is derived from what
RepositoryEnvelopecan answer, and the derivation is written at its site, because a reader who finds "the checked-out commit and a count" with no reason will read it as an arbitrary call and change it.Most of the git-status mental model is not expressible here
That is a property of the model, not a missing feature. The envelope carries a store, a commit list, and an optional checked-out selection. This layer has no path, no branch, no author, no timestamp, no working tree, no remote anywhere in it — checked rather than assumed: the only
Branchunderdag/gunbc/scmis the node connective.So modified-files, staged-versus-unstaged by path, ahead/behind, and current-branch cannot appear. Not deferred — unproducible. A surface reporting them would be fabricating.
Three states, not two — the load-bearing one
It is not enough that a stated absence differ from a present binding. It must differ from not mentioned at all, because merge's silence-means-preserve rule makes "role not stated" and "role stated absent" semantically opposite: one preserves the target's binding, the other deletes it. A rendering where a stated absence looks like an empty slot is the not-applicable-versus-malformed conflation carried into a user surface, where someone acts on it.
The third state is structural rather than rendered: a role that is not stated has no row, so there is no value meaning "not stated" that can get out of step.
The other derivations
repository_envelope's header statesinitproduces no commits and no root and that neither is an error. Rendering it as a warning would contradict a stated authority and fabricate a fault.RepositoryCheckoutNotInCommits, so the question is decidable here. Reporting the selection as an ordinary checkout would assert a commit exists when it may not.logverb will own what happened; two surfaces for one fact is the redundancy §2 prices, and shrinking a published surface later is harder than growing one.Structure and rendering are split: a machine consumer must read the facts rather than parse prose out of a terminal rendering, which would be a second authority for one answer.
Evidence
Six witnesses pass by execution. Three mutations, each turning its own witness false:
nothing_staged_is_stated…a_dangling_checkout_is_reported_as_missing…I first checked the silence mutation against the three-state witness, which correctly stayed green because that is the other witness's claim, and re-ran it against the right one rather than report a receipt I had not taken.
Witness assertions are exact renderings, not substring searches: a substring passes against a surface that also emits fabricated lines beside it. That also avoids adding a third top-level
string_contains— the corpus already carries two, and top-level names are corpus-wide with silent duplicate selection (#8707).