Repository navigation
Model git's two enumeration reads: the substrate could create a worktree and not list one, resolve a ref and not enumerate refs - #9431
Conversation
…ree and not list one, resolve a ref and not enumerate refs extdeps.git declares 66 operations and neither `for-each-ref` nor `worktree list`. The asymmetry is the finding: worktree ADD is modeled in both its branch and detached forms, so a linked worktree can be CREATED and never ENUMERATED; ObserveRef resolves one ref the caller already names, and RemoteBranches returns remote-tracking names only, offline, with no object id. Neither gap is a defect in those operations -- they answer "where is this ref" and "which remote branches does this clone know about". The missing question is "what is the COMPLETE set, and where does each member point", and a check built without it is a check over an authored list, which by construction cannot see an addition. ForEachRefIn formats NUL-separated fields on newline-separated records. That is safety rather than convenience: git-check-ref-format(1) forbids space, newline and ASCII control characters inside a ref name, so a record cannot be split by its own content, and the symref field is empty for an ordinary ref -- a trailing empty field must stay observable rather than collapse into the separator. It is deliberately a LOGICAL ref read, not a storage read. Whether a ref lives loose under .git/refs or inside packed-refs is git storage policy that changes under ordinary maintenance with no ref having moved. Both directions were measured on srv1: a digest over storage reports a difference where nothing changed, and misses one where a loose ref shadows a stale packed entry. WorktreeListIn uses --porcelain -z, the form git-worktree(1) directs callers to rather than interpreting paths under GIT_DIR themselves. Each entry carries absolute path, HEAD, branch-or-detached, and the locked and prunable standings -- the tuple a preservation comparison needs, none of it recoverable from the filesystem without re-deciding git's own layout. Both are readonly and report exit_code + stderr rather than a success Bool, per this module's integration_write_operations_note: the seed derives exit_success as exactly exit_code == 0, so carrying both would represent one fact twice. Verified: 4123 files parse-clean; declaration count moves 79434 -> 79438, exactly the four top-level declarations added. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…shes the same ref set two ways The projection was already fixed to refname/objectname/symref rather than taken as a caller format string. The ORDER was not, and for the consumer this operation exists to serve that is the same defect one step later: a consumer comparing two enumerations digests them, so an unpinned order makes the digest a function of git's default ordering rather than of the ref set, and the same set can hash two ways. --sort=refname is pinned in the operation for that reason, and refname specifically because it is the one field guaranteed unique across the set -- which makes the order total rather than merely deterministic. Also records why there is no -z here. git-for-each-ref(1) documents no -z option; the NUL separator comes from %00 inside its own format language. Spelling a -z that upstream does not have would be a fabricated interface: it would fail at the transport rather than in review, and the extdeps duty is to model what the tool actually accepts. WorktreeListIn does carry -z because git-worktree(1) documents it. Verified: 4123 files parse-clean; declaration count unchanged at 79438, as expected for a string extension plus one argv element. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…TACHMENT POINT (review 56593) review 56593 is correct: two `data ..._note: String` rows carrying nothing but commentary are exactly what DESIGN §4c names as misplaced or dead semantic data, and §4c's own history says why -- the corpus already tried hoisting comments into String rows (#6262) and the first cleanup that forced swept 215 dead prose rows across ~130 files (#6424). The interesting part is how they got there, because the symptom pointed at the wrong fix. The first cut wrote these as `//` blocks, and the parser refused them: they sat INSIDE the `service git.Core { ... }` body, and §4c admits only standalone leading `//` attached to MODULE-SCOPE declarations. I concluded `//` was unavailable and changed the carrier. The actual defect was the attachment point -- git.dag already carries 48 module-scope `//` blocks, so the annotation channel was available the whole time and I had measured only that one position was not. Both rationales now attach to the module-scope ExternalAuthority anchors for the git commands they describe, which are the declarations whose subject they actually are. Verified by execution, and the counter moves in the direction that proves the point rather than merely not breaking: 4123 files parse-clean, and the declaration count drops 79438 -> 79436, exactly the two String rows removed. The prose left the semantic program instead of being reworded inside it -- §4c's annotation capture is disjoint from semantic occurrence allocation, so an annotation must not appear in that count at all. Diff confined to the three intended regions; an incidental whole-file newline collapse that had removed a blank line under the module header was reverted. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Fixed in The first cut wrote both rationales as That is the same class this repository keeps recording: a nearby probe with a plausible answer standing in for the producer's answer. One refused position is not evidence about the channel. Both rationales now attach to the module-scope Verified by execution, with the counter moving in the direction that proves the point rather than merely not breaking:
That drop is the substantive check. §4c makes annotation capture disjoint from semantic occurrence allocation, so a correctly-carried annotation must not appear in the declaration count at all. Had I merely reworded the prose inside Also confined the diff to the three intended regions — an incidental whole-file newline collapse had removed a blank line under the module header, and that is reverted. Not claimed: neither operation has an executing witness in this PR. Per the ruling this slice is following, typed observations, pure decoders, and discriminating parser controls (including a loose-versus-packed equivalence control) are the next increment. — sent from calm-ram-380 |
…one execution, and no lease fixes that (#9506) * Decode git's worktree enumeration, with the checkout as a coproduct so bare-with-a-head cannot be written The typed reading of git.Core.WorktreeListIn's wire (landed in #9431), alongside the ref-set decoder in #9465. The load-bearing choice is that GitWorktreeCheckout is a coproduct rather than a record of optionals. git reports a bare worktree with NO HEAD line at all, and every non-bare worktree with a HEAD plus exactly one of `branch` or `detached`. A record carrying head?/branch?/bare would make four impossible states writable -- bare-with-a-head, non-bare with no head, both-branch-and- detached, and neither -- each of which every consumer would then re-validate. Carrying the head inside the arms that have one makes those states unrepresentable rather than checked (DESIGN §4b construction rung), and the one place a checkout is chosen refuses each of them with a located reason. An unmodeled attribute REFUSES rather than being skipped: git adds attributes over time, and ignoring one would let a future flag change a worktree's meaning while this decoder kept reporting the old reading (§5 -- a failure arm refuses, never widens). `locked`/`prunable` are admitted bare or with a trailing reason; the reason is git's prose for a human, carries no decidable fact, and is deliberately not retained. Framing follows the transport: NUL-separated attributes, an empty record terminating each entry, exactly one trailing empty dropped. An unterminated final entry refuses rather than being dropped, which would report fewer worktrees than the repository has. One malformed entry refuses the whole observation, for the same reason as the ref decoder: a partial set is indistinguishable from a repository with fewer worktrees. The located grain is the ENTRY, since an entry spans several records. Accumulation is cons + one reverse at each exit, not tail-append in the step (§6 bare-minimum-cost), and `entries_preserve_the_emitted_order` pins the order that no count-based witness can see. The 16 witnesses' authored strings are transcribed from real `git worktree list --porcelain -z` output observed on a constructed repository (primary on a branch, linked on a branch, detached, locked, and a bare clone), verified byte-identical to a reconstruction from those entries -- so the framing under test is git's, not an invention. They establish the DECODE only; that git emits these bytes is a transport claim owned by the wet matrix. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Move the locked/prunable annotation to module scope: §4c admits only module-item grain CI's v2-emission phase refused with four hard diagnostics -- one per line of a single four-line `//` block sitting inside git_worktree_attribute_step's body. DESIGN §4c admits only standalone leading blocks attached to module-scope declarations; body, trailing, and unattached forms refuse until separately modeled. The block now sits above the declaration it describes, unchanged in content. Worth recording because it is a real coverage gap rather than a typo: the 16 witnesses passed 16/16 under claim_batch on the offending commit. Witness-green is not §4c-green -- the annotation grain is enforced at emission, which no witness run reaches. The whole-file check is `grep -n '^\s\+//'`, which is now 0 in both files of this PR and was already 0 in #9465's two. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Fuse grouping into the decode: one pass over records, no intermediate entry list Review 56832 observed that two reverses looked redundant. Dropping either is not the fix -- the entries reverse is what keeps the decode in git's EMITTED order, which numbers entry_index as a reader counts entries and makes the FIRST malformed entry the reported one; folding reversed entries still yields a correct worktree list and silently inverts both. A mutation probe on a throwaway branch confirms the naive edit reds witnesses rather than being a no-op. The real redundancy was upstream of the reverse: grouping folded records into a List<List<String>> and then folded that into worktrees, materializing an intermediate representation only to consume it immediately (DESIGN §2). The scan now folds records directly, decoding each entry as its terminator arrives. Records are already in emitted order, so entry_index numbering and first-fault-wins are preserved by construction rather than restored by a reverse. Net: GitWorktreeGroupState, git_worktree_group_step and git_worktree_group are deleted, reverse sites drop 4 -> 3, and no List<List<String>> is ever built. The unterminated-stream check still precedes the verdict, so a truncated stream refuses as truncated rather than reporting a downstream decode fault. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Model git's compare-and-swap update-ref, reflog read, and reset --hard * The convergence adjudication: preservation by identity, and a reflog that proves git moved it * Nine witnesses: one green control and seven discriminating reds over the preservation properties * Build convergence fixtures through the decoders: GitObjectId has a sole constructor, not a cast * wip: diagnostics * GitObjectId is a coproduct, not a branded string: compare with git_object_id_eq * for-each-ref emits sorted and the decoder enforces it: order the fixture records * Remove the decode diagnostics: they located the ordering defect and would now be permanently green * The wet composition: observe, import, compare-and-swap, transition, read back * §4c: operation annotations move to module scope, each on its own cited authority * Split the CAS refusal: a lost swap and an unwritable ref have different owners * Witness the CAS split: the distinction a review found was untested until now * Refuse untracked residue, and stop reporting the primary's own branch as lost Two findings from side-chat review, one of which turned out to be masked by the other. UNTRACKED RESIDUE. `reset --hard` moves HEAD, the index and the TRACKED bytes; files git does not track survive it untouched. So a tree that carries strays afterwards is candidate-union-residue, not the candidate, and reporting ConvergenceCompleted over it is a fabricated plausible output. This matters concretely on the deployed tree, whose 5650-path divergence was produced by a sync that wrote files git never tracked. The listing is observed via `git ls-files --others --exclude-standard -z` and the consumer REFUSES rather than running `git clean`, which would widen and destroy operator state nobody adjudicated. The observation is a coproduct, not the bare String head and reflog get away with: an unreadable listing and a clean tree both produce no paths, and the empty one is the ADMITTING answer, so a String would have been the empty-observation narrow. THE PRIMARY'S OWN BRANCH. convergence_first_lost_ref exempted only base_ref, and `reset --hard` on a branch-attached primary necessarily advances that branch -- so on any real repository a SUCCESSFUL convergence reported ConvergenceRefDisappeared for refs/heads/main. The witnesses could not see it because the fixtures omitted the attached branch refs entirely: a worktree bound to a branch absent from the ref set is not a state git can be in, so the fixture was an impossible repository and the live defect had nowhere to surface. An unrealistic fixture does not merely fail to test a case, it can make a real defect unreachable. The exemption is PAIRED with a positive check rather than standing alone: the branch is required to be at the candidate, since exempting it from the loss join and stopping there would admit it moving anywhere at all. 15 witnesses PASS. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Name the partial transition, and read the reflog's newest entry rather than its text Three more findings from side-chat review of this PR. PARTIAL TRANSITION. If the CAS succeeds and `reset --hard` then fails, the base ref stands advanced over an untransitioned tree -- and the code returned immediately, skipping the post-observation its own annotation promised was unconditional. That state is consumable by another actuator, since `git worktree add` resolves through the advanced ref, so it needs a name rather than a diagnostic about a refused command. Every failure after the first mutation now observes the post-state and reports ConvergencePartialTransitionLeft carrying the advanced ref and the observed HEAD. THE ATOMICITY OVERCLAIM WAS MINE AND IS RETRACTED. The extdeps annotation said partial application "is not a state `reset --hard` can produce". Git documents that command as updating HEAD, index and working tree; it does not document a transaction that rolls back, and a kill mid-sequence leaves exactly the state the sentence denied. `update-ref`'s compare-and-swap covers the ref it owns and does not extend across a later reset. One git-owned command over three representations is a real improvement over three uncoordinated transports and is not crash-atomicity. THE REFLOG LAW WAS TOO WEAK. `before != after` is satisfied by any unrelated append, truncation or rewrite -- including one made by a concurrent actor while this transition did nothing. The law now requires the newest entry to name the candidate as the object HEAD arrived at. The added witness is one the previous check could not have caught: reflog grew, HEAD at candidate, newest entry naming an unrelated object, which went green before. 16 witnesses PASS. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Declare what this module does not establish The PR is approved and the side-chat review's findings 1 and 5 are not closed. They are not defects left standing by a reviewer -- they are obligations this construction knowingly does not discharge, and a capability whose limits are unstated gets cited for the whole claim. That is the rung inflation DESIGN 4b calls worse than sitting low. Five declared, at the module head where a reader arrives: 1. NO WET EXECUTION EVIDENCE. Every witness is pure adjudication over observations the test authors; none calls repository_converge_wet. The hermetic floor cannot supply it, and mocking would fabricate the exact observation the claim is about. A deterministic scratch-repository matrix is owed, with a control proving replay did not reach live git. 2. THE POST-STATE IS NOT PROVED COHERENT. The measured defect is a three-way disagreement among HEAD, index and working tree; this observes HEAD, refs, worktrees, reflog and untracked residue, and cannot assert index-tree or tracked-cleanliness equality. 3. AlreadyAtCandidate IS WEAKER THAN IT READS -- the reset runs anyway, so a repair of a stale index reports "no transition performed". 4. PRE-MUTATION OBSERVABILITY IS PARTIAL: only refs are adjudicated readable before the first mutation. 5. THE PRESERVATION JOIN IS ONE-WAY AND LOSSY: a retargeted symref passes, added refs are unnoticed, worktree HEAD/locked/prunable are discarded, and primary_path is caller-supplied rather than derived. NOTHING HERE IS BOUND -- no production caller reaches this module and apply refuses through the interlock -- so these are prerequisites of the BINDING change rather than standing risks. That ordering is why they may be declared rather than fixed here; it is not an excuse for having declared them. 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>
…o bare-with-a-head cannot be written (#9468) * Decode git's worktree enumeration, with the checkout as a coproduct so bare-with-a-head cannot be written The typed reading of git.Core.WorktreeListIn's wire (landed in #9431), alongside the ref-set decoder in #9465. The load-bearing choice is that GitWorktreeCheckout is a coproduct rather than a record of optionals. git reports a bare worktree with NO HEAD line at all, and every non-bare worktree with a HEAD plus exactly one of `branch` or `detached`. A record carrying head?/branch?/bare would make four impossible states writable -- bare-with-a-head, non-bare with no head, both-branch-and- detached, and neither -- each of which every consumer would then re-validate. Carrying the head inside the arms that have one makes those states unrepresentable rather than checked (DESIGN §4b construction rung), and the one place a checkout is chosen refuses each of them with a located reason. An unmodeled attribute REFUSES rather than being skipped: git adds attributes over time, and ignoring one would let a future flag change a worktree's meaning while this decoder kept reporting the old reading (§5 -- a failure arm refuses, never widens). `locked`/`prunable` are admitted bare or with a trailing reason; the reason is git's prose for a human, carries no decidable fact, and is deliberately not retained. Framing follows the transport: NUL-separated attributes, an empty record terminating each entry, exactly one trailing empty dropped. An unterminated final entry refuses rather than being dropped, which would report fewer worktrees than the repository has. One malformed entry refuses the whole observation, for the same reason as the ref decoder: a partial set is indistinguishable from a repository with fewer worktrees. The located grain is the ENTRY, since an entry spans several records. Accumulation is cons + one reverse at each exit, not tail-append in the step (§6 bare-minimum-cost), and `entries_preserve_the_emitted_order` pins the order that no count-based witness can see. The 16 witnesses' authored strings are transcribed from real `git worktree list --porcelain -z` output observed on a constructed repository (primary on a branch, linked on a branch, detached, locked, and a bare clone), verified byte-identical to a reconstruction from those entries -- so the framing under test is git's, not an invention. They establish the DECODE only; that git emits these bytes is a transport claim owned by the wet matrix. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Move the locked/prunable annotation to module scope: §4c admits only module-item grain CI's v2-emission phase refused with four hard diagnostics -- one per line of a single four-line `//` block sitting inside git_worktree_attribute_step's body. DESIGN §4c admits only standalone leading blocks attached to module-scope declarations; body, trailing, and unattached forms refuse until separately modeled. The block now sits above the declaration it describes, unchanged in content. Worth recording because it is a real coverage gap rather than a typo: the 16 witnesses passed 16/16 under claim_batch on the offending commit. Witness-green is not §4c-green -- the annotation grain is enforced at emission, which no witness run reaches. The whole-file check is `grep -n '^\s\+//'`, which is now 0 in both files of this PR and was already 0 in #9465's two. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Fuse grouping into the decode: one pass over records, no intermediate entry list Review 56832 observed that two reverses looked redundant. Dropping either is not the fix -- the entries reverse is what keeps the decode in git's EMITTED order, which numbers entry_index as a reader counts entries and makes the FIRST malformed entry the reported one; folding reversed entries still yields a correct worktree list and silently inverts both. A mutation probe on a throwaway branch confirms the naive edit reds witnesses rather than being a no-op. The real redundancy was upstream of the reverse: grouping folded records into a List<List<String>> and then folded that into worktrees, materializing an intermediate representation only to consume it immediately (DESIGN §2). The scan now folds records directly, decoding each entry as its terminator arrives. Records are already in emitted order, so entry_index numbering and first-fault-wins are preserved by construction rather than restored by a reverse. Net: GitWorktreeGroupState, git_worktree_group_step and git_worktree_group are deleted, reverse sites drop 4 -> 3, and no List<List<String>> is ever built. The unterminated-stream check still precedes the verdict, so a truncated stream refuses as truncated rather than reporting a downstream decode fault. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Refuse an empty successful worktree enumeration, and a repeated branch attribute Two decoder findings from side-chat review. EMPTY SUCCESS IS MALFORMED, NOT AN EMPTY SET. On exit zero with no records the decoder answered GitWorktreeSetObserved with zero worktrees. Git's porcelain contract lists the main worktree first and every repository has one, bare included, so there is no repository for which git answers zero: a zero-entry success is a truncated or redirected stream wearing the shape of an answer. The consequence is why this is a refusal rather than a curiosity. A consumer joining worktree rosters before and after an operation finds nothing missing from an empty before-set, so every preservation check over that observation passes VACUOUSLY -- the bad observation does not yield a wrong worktree, it yields an unconditional yes from anything that asks. That is the empty-observation narrow arriving through the decoder rather than through the consumer, and it propagates directly into the convergence consumer. Declared honestly as MECHANICALLY PREVENTABLE, not structural: the invalid state is still representable and a check rejects it. The structural form splits the observed arm into `primary` beside `linked: List<...>`, which makes zero-worktree success unwritable and additionally lets a consumer derive the primary from git's own roster rather than accepting a caller-supplied path. That changes the type consumers destructure, so it lands with the rebase that stacks the convergence consumer on this module -- doing it here would break an open branch that is not stacked on this one. A REPEATED KNOWN ATTRIBUTE IS AS MALFORMED AS AN UNKNOWN ONE. A second `branch` record silently overwrote the first, so an entry naming two branches decoded as whichever git emitted last. HEAD already refused this; the asymmetry was the tell -- an unknown attribute refused loudly while a known attribute in an impossible arrangement was accepted quietly. 19 witnesses PASS, including a positive control so the empty-success arm cannot be satisfied by a decoder that refuses every successful read. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Refuse repetition of ALL six singleton attributes, not two of them review 56981 (codex/gpt-5.6-sol, REQUEST_CHANGES) is correct and the defect is mine: the previous commit stated a duplicate-attribute invariant and applied it to HEAD and branch only, leaving detached, bare, locked and prunable setting their field to true unconditionally. Two `detached` records still decoded into a SUCCESSFUL observation. It was invisible for the reason repetition defects usually are: setting a flag twice is idempotent, so nothing downstream looks wrong. The WIRE was malformed, and a decoder that quietly normalizes malformed input is not lenient -- it is answering a question nobody asked. The asymmetry was the tell: an unknown attribute refused loudly while a known attribute in an impossible arrangement was accepted quietly. THE FIRST CUT OF THE WITNESSES WAS NON-DISCRIMINATING AND IS RECORDED HERE BECAUSE IT WENT GREEN. Every fixture was worktree + HEAD + the doubled attribute, and three of four then refused FOR THE WRONG REASON: `bare` with a HEAD is already refused by the bare-carries-no-head rule, and `locked` or `prunable` alone describe no checkout, so the entry failed the exactly-one-of check before duplication was consulted. Four green witnesses testing almost nothing. Each fixture is now a VALID entry that duplication alone spoils, PAIRED with the same entry carrying one occurrence, which must decode. A duplicate arm whose single-occurrence twin also refuses is not evidence about duplication. 23 witnesses PASS. 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>
extdeps.gitdeclares 66 operations and neitherfor-each-refnorworktree list.The asymmetry is the finding: worktree ADD is modeled in both its branch and detached forms, so a linked worktree can be created and never enumerated.
ObserveRefresolves one ref the caller already names;RemoteBranchesreturns remote-tracking names only, offline, with no object id. Neither gap is a defect in those operations — they answer "where is this ref" and "which remote branches does this clone know about". The missing question is "what is the COMPLETE set, and where does each member point", and a check built without it is a check over an authored list, which by construction cannot see an addition.Why now
Found while specifying a bounded repair to a retired deployment repository. That repair's admission requires re-observing a worktree roster and a logical ref set at execution time; neither observation was expressible, so the wall could not be built at the grain its own ruling required.
Design notes
ForEachRefInformats NUL-separated fields on newline-separated records. Safety rather than convenience:git-check-ref-format(1)forbids space, newline and ASCII control characters inside a ref name, so a record cannot be split by its own content. The symref field is empty for an ordinary ref, so fields are NUL-separated to keep a trailing empty field observable instead of collapsing into the separator.It is deliberately a logical ref read, not a storage read. Whether a ref lives loose under
.git/refsor insidepacked-refsis git storage policy that changes under ordinary maintenance with no ref having moved. Both failure directions were measured on a live tree: a digest over storage reports a difference where nothing changed, and misses one where a loose ref shadows a stale packed entry.WorktreeListInuses--porcelain -z, the formgit-worktree(1)directs callers to rather than interpreting paths under\$GIT_DIRthemselves. Each entry carries absolute path, HEAD, branch-or-detached, and the locked/prunable standings — the tuple a preservation comparison needs, none of it recoverable from the filesystem without re-deciding git's own layout.Both are
readonlyand reportexit_code+stderrrather than asuccessBool, per this module's ownintegration_write_operations_note: the seed derivesexit_successas exactlyexit_code == 0, so carrying both would represent one fact twice.Verification
v1_src_dag_parse: 4123 files parse-cleanAn earlier cut placed the rationale as
//blocks inside theservice git.Corebody; the parser refused them per DESIGN §4c (module-item grain only), and they were moved to top-leveldata …_notedeclarations matching this module's existing convention.Not claimed
No consumer yet — these are the enumeration surface, not a use of it. Neither operation has an executing witness in this PR.
🤖 Generated with Claude Code