Repository navigation
roadmap dispatch - #9465
Merged
Merged
roadmap dispatch#9465
Conversation
…sing it so --sort=refname stays falsifiable extdeps.git.ForEachRefIn landed with --sort=refname pinned in its transport. This adds the typed reading of its wire, and the one design choice worth arguing is that the decoder VALIDATES the order instead of sorting. A decoder that sorted would make the transport's pin decorative: deleting --sort=refname from the argv would leave every test in this lane green, because the decoder would have quietly repaired the property the flag exists to provide. That is the permanently-green check DESIGN §4b names as worse than absent, since it gets cited as coverage for a flag nothing tests. Requiring STRICTLY increasing ref names makes the flag falsifiable instead. Strict rather than non-decreasing because ref names are unique in a repository, so an equal adjacent pair is a duplicate rather than a tie, and a duplicate is exactly what a set-identity consumer must not absorb. Three arms, not two, because the failures have different owners. ReadRefused is git declining, carrying exit code and stderr, and the remedy is about the repository. Undecodable is git having answered in a shape the decoder does not accept, LOCATED by record index and raw record. A single malformed record refuses the WHOLE observation rather than being skipped: a partial ref set is indistinguishable from a smaller repository, and a consumer comparing two enumerations would read a dropped record as a deleted ref. The exit code is consulted BEFORE the payload. A non-repository path exits nonzero with empty stdout and an empty ref namespace exits zero with empty stdout, so a decoder that folded the payload first would report the observed-empty set for both -- the execution-provenance conflation DESIGN records, where a count of zero and an unreached read must not inhabit one carrier. Exactly one trailing empty record is dropped, because git terminates its last record with the separator. Any FURTHER empty record is truncated framing and refuses -- a filter over all empties would silently absorb the malformed case this decoder exists to catch. Reuses git_object_id_from_untagged_hex rather than minting a second oid reader, so "malformed object id" refuses through the existing authority. EXECUTED EVIDENCE, not just green: 10/10 witnesses pass, and a mutation receipt establishes the order check is load-bearing. Disabling it (the comparison replaced by `true`) over identical inputs turns descending_ref_names_refuse_rather_than_being_sorted and duplicate_ref_name_refuses RED while ascending_ref_names_are_accepted -- the positive control on the plant -- stays green. So the refusals are caused by the check rather than coincident with it. WHAT THIS DOES NOT ESTABLISH, stated because reporting it as coverage would be rung inflation: that ForEachRefIn EMITS these bytes for any given repository state. That is a transport claim; it cannot execute in the hermetic fold (a shell operation is refused at shell.Test.IsExecutable before the subprocess, and mocking the result would fabricate the very observation the claim is about), and it belongs to a separate wet record/replay matrix. The loose-versus-packed equivalence control is in that half, not this one -- two authored strings decoding alike proves only that, never that git emits them for the two storage states. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…reverse restores Review 56767 on #9465 found a tail-append inside the decode fold, making it O(n^2) in the number of refs. DESIGN §6 bare-minimum-cost treats a proven quadratic fold shape as always-fix regardless of the realized n, and the corpus already carries this exact idiom ("prepend during fold, single reverse at end"). The step now conses and the accepted arm is turned exactly once at the single exit; the two refusal arms carry no list and pass through. The reverse is observable behaviour, and nothing in the lane could see it: every other accepting witness asserts a COUNT, which is invariant under reversal. Left there, the reverse would have been unwitnessed machinery. accepted_refs_preserve_the_emitted_order pins both positions. Also removes `data git_ref_set_order_is_validated_not_imposed: Bool = true`, which nothing read. It existed only to anchor its annotation block, which is the §4c dead-data class; the block now attaches to git_ref_decode_ordered_admit, the declaration it actually describes. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 27, 2026
…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>
Contributor
Author
|
On review 56839 (REQUEST_CHANGES): I checked the cited rule against the authority and I don't think this finding holds. Laying out the evidence rather than just disagreeing — happy to be shown wrong. The finding: 1. None of the cited terms appear in DESIGN.md. Measured on the base-pinned copy the review itself used:
2. The three real 3. The shape is an established corpus idiom, not a violation. 41 witness-test files under The third is byte-for-byte my construction. If this shape were merge-blocking, it is merge-blocking in 41 existing files. On the substance. The helper is exhaustive — three explicit arms, no wildcard, no bare payload binding — so it is not the "total at the level examined, blind one level down" collapse DESIGN does name. It deliberately maps Why I'm not applying the fix. The available compliance moves both make the code worse: inlining the match into each of 11 witnesses duplicates it eleven times (§2), and "a canonical query surface" would mean minting an authority the corpus doesn't have for a concept it already expresses. Making a worse change to satisfy a rule the named authority doesn't contain is the authority-substitution shape DESIGN warns about — the halves check out, the arrow between them is invented. If the reviewer maintains the finding, I'd ask it to quote the DESIGN sentence it rests on; I'll implement it immediately if it exists and I've missed it. — sent from calm-ram-380 |
briansrls
pushed a commit
that referenced
this pull request
Aug 27, 2026
…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>
briansrls
pushed a commit
that referenced
this pull request
Aug 28, 2026
…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>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Auto-opened by session-dashboard for session
calm-ram-380.Pushing to
session/calm-ram-380-enumadvances this PR.Worker attestation
Before flipping this PR to ready for review, confirm each item:
npm test,cargo test) and the result.Closes #Ndirective.Summary
TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.
Test plan