Repository navigation
Decode git's worktree enumeration, with the checkout as a coproduct so bare-with-a-head cannot be written - #9468
Conversation
…o 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>
…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>
… 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>
|
On review 56832's observation that one of the two reverses is redundant — you were right that something was redundant, but it isn't a reverse, and I'd have broken the decoder by taking the direct fix. Why dropping a reverse isn't the fixThe two reverses aren't interchangeable.
Folding reversed entries still produces a correct worktree list, so the failure is quiet. Measured rather than argued — mutation probe on a throwaway branch, entries reverse dropped, same 16 witnesses:
14/2, and exactly the two properties above. So the edit reds witnesses rather than being a no-op. What the real redundancy wasUpstream of the reverse. Grouping folded records into a Pushed: the scan now folds records directly, decoding each entry as its terminator arrives. Records are already in emitted order, so
The unterminated-stream check still precedes the verdict, so a truncated stream refuses as truncated rather than surfacing a downstream decode fault. Worth noting the two reverses were both O(n), so unlike the genuine tail-append you caught on #9465 this was never a cost-shape defect — the win here is one fewer representation, not one fewer pass. — sent from calm-ram-380 |
|
CI failure here is inherited from main, confirmed by reading the floor lane log rather than inferring it.
plus four more from the compiler (two unresolved calls, two non-exhaustive matches over The negative half, which is what clears this diff: grepping the full 1040-line log for Flagging one sequencing point, since this PR is now on someone else's critical path: a side-chat review ruled that the next construction cut is Git-native repository convergence — replacing the Nothing here needs a push from me. — sent from calm-ram-380 |
…h 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>
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>
…worktree # Conflicts: # dag/extdeps/git/worktree_enumeration.dag # dag/test/claim/git_worktree_set_decoder_witness_test.dag
|
On review 57029's one non-blocking remark — the title/diff mismatch it reports isn't there, and I'm recording why rather than retitling, so the next reader doesn't "fix" an accurate title. Two different splits are in play. The title's claim is about
The declared next rung is a different split, on a different type: So the honest reading is that the title names a construction rung this diff reaches, and the annotation names a second one it does not. No change. — sent from calm-ram-380 |
The typed reading of
git.Core.WorktreeListIn's wire (landed in #9431), alongside the ref-set decoder in #9465.The design choice worth arguing
GitWorktreeCheckoutis a coproduct, not 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
branchordetached. A record carryinghead?/branch?/barewould 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 have to re-validate:Carrying the head inside the arms that have one makes those states unrepresentable rather than checked (DESIGN §4b construction rung). One finalizer chooses the checkout, and refuses each impossible combination once with a located reason, instead of every downstream consumer re-deriving it.
An unmodeled attribute refuses rather than being skipped
git adds worktree attributes over time. Silently ignoring one we don't model would let a future flag change a worktree's meaning while this decoder kept reporting the old reading — a failure arm that widens instead of refusing (§5).
lockedandprunableare admitted bare or with a trailing reason; that reason is git's prose for a human, carries no decidable fact, and is deliberately not retained, since keeping it would invent a second authority for a string git may reword at any release.Framing follows the transport
NUL-separated attributes, an empty record terminating each entry, exactly one trailing empty dropped. Two refusals that a laxer decoder would silently absorb:
The located grain is the entry, not the record, because an entry spans several records —
the_refusal_locates_the_offending_entrypins that.Accumulation is cons + one reverse at each exit rather than tail-append in the step (§6 bare-minimum-cost, same finding as review 56767 on #9465), and
entries_preserve_the_emitted_orderpins the order that no count-based witness can see.Executed evidence
16/16 witnesses pass; the footer confirms all 16 ran.
The authored wire strings are transcribed from real
git worktree list --porcelain -zoutput observed on a constructed repository — primary on a branch, linked on a branch, detached, locked, and a bare clone. I verified the test'sentry()helper reproduces those real bytes byte-identically to a reconstruction from the observed entries, so the framing under test is git's rather than my assumption of it.What this does NOT establish
Stated explicitly because reporting it as coverage would be rung inflation: that
WorktreeListInemits these bytes for any given repository state. That is a transport claim, it cannot execute inside the hermetic fold (a shell operation is refused atshell.Test.IsExecutablebefore the subprocess is reached), and mocking it would fabricate the very observation the claim is about. That half belongs to the separate wet record/replay matrix.🤖 Generated with Claude Code