You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
Repository navigation
The word grammar's --force rule is unguarded in the same way #354
The review of PR #344 approved the flag-verb half of the --force placement guard and then found that the word half is unguarded in the same way, latently:
workspace_command still phrases the rule as an absolute index (index ≥ 2 ⇒ Trailing). That is equivalent to the flag-verb half's "no name follows it" only because clap caps positionals at 2 — an incidental fact, not a stated invariant, and exactly the kind of coincidence that stops being true without anyone noticing.
The new matrix test's alphabet omits rm — the only token that makes the word grammar produce a forced delete — so the word grammar's half of the property is not actually exercised. The reviewer confirmed it still passes with rm added, so this is latent rather than live.
Fix both: state the word grammar's rule as the same invariant the flag-verb grammar now uses, and widen the matrix alphabet so the word half is genuinely covered. Red first — adding rm to the alphabet must be a real exercise of the property, not a no-op, so demonstrate the widened matrix fails against a deliberately reverted workspace_command.
Three smaller gaps from the same review, in the same area:
aid's leading --rm --force form still loses force. Different crate (rust/aid/src/rewrite.rs), so it was correctly out of Close the --force flag-verb bypass #303's scope.
Globals have no placement rule at all — dl --force --prune is unchecked. Decide whether that is a gap or deliberate: --prune and --purge are not workspace-targeted, so --force may be unambiguous there. If it is deliberate, write down why.
No README/GRAMMAR update accompanied #344 either; the two files must be edited together or it becomes the drift CLAUDE.md forbids.
Claimed 2026-08-29: build in progress from an interactive session (opus agent in an isolated worktree, managed as part of closing out map #299). PR to follow. If you are another session seeing this, do not double-build.
breadcrumb: building this as the guard it is, not a behaviour change.
Seam: resolve(Cli, argv) -> Result<Command, GrammarError> in the dl crate's grammar module. It is pure and total over argv, which is what makes an exhaustive walk of the argv space a test rather than a fixture.
What lands: one enumeration over every ordering of every subset of the alphabet {workspace name, rm, rme, --force, --rm} (each word at most once), resolved through that seam, with the expectation written from Python's own rule ("--force" in args[2:], args[0] the workspace and args[1] the verb) plus the fact that only the two delete verbs have anything to force. The alphabet carries rm and rme deliberately: they are the only tokens that can make the word grammar produce a forced delete, and the matrix that was reviewed on #344 omitted them, which is why the word half of the property was never actually exercised.
Non-vacuity is proved twice: the walk also collects the lines that do force and asserts that set against a literal, and the whole thing is run against a deliberately reverted placement rule to watch it go red.
Two claims in the ticket body I will check first rather than assume, since #369 moved the ground under all of them: aid's leading --rm --force form, and whether the globals really have no placement rule.
The slice: one walk of every ordering of every subset of {ws, rm, rme, --force, --rm} through the grammar's resolve seam, checked against Python's args[2:] rule plus the verb table, with the pair refusal held over the same space. rm and rme are in the alphabet, which is what the #344 matrix was missing and what makes each ordering a live question about whether that line deletes.
Proven non-vacuous against four reverted rules. The one worth naming: make the three-word arm resolve instead of refuse, and dl ws rm --force rme force-deletes ws while 149 other tests pass. Only the guards this PR adds go red on it. That is the ticket's latent hole, made live and then caught.
Three things the body claimed that had already moved:
aid's leading --rm --force form is closed on main, both orderings, with the emitted index asserted.
The lib.rs line reference is stale after the --rm rework and there is nothing wrong at it now.
The globals really have no placement rule, and it is deliberate rather than the same gap: a global line has no slot a --force could be mistaken for a word in, because the one global that takes a word is not one of the two that accept the flag. Written down as a test of that premise rather than as a comment, so it fails if somebody gives a force-accepting command a word.
And one thing nobody had noticed: clap's two-word cap counts values per occurrence, so dl a b --force c hands the grammar three positionals where dl a b c is refused at exit 2. The arm that catches it carried a comment saying a third word never arrives. Nothing forced escapes through it, but it is that arm's refusal doing the work rather than the cap, which is exactly the incidental fact this ticket was about. Corrected and pinned. No behaviour change anywhere in the diff.
wf-review on #506: Request changes — one blocking finding (force_placement's absolute index is still shifted by a leading token, so dl <flag> ws --force rm would force-delete where dl ws --force rm refuses; latent behind five unpinned facts). Enumeration verified total (325 lines, 259 walked), oracle verified independent, non-vacuity replayed. #506 (review)
breadcrumb: review found the leading half of the coincidence still open, and the fix turned this from a guard ticket into a one-line rule change.
The slot was counted over every argv token. A flag the parser has already consumed is gone from the words and still sitting in argv, so it shifted every slot up by one: a workspace line with any flag ahead of it read a verb-slot --force as trailing and force-deleted the workspace, where the same line without the flag refuses. No such flag existed, but only because five unrelated rules each refused or stripped one first. The slot is a place a word goes, so words are what it counts now. Nothing anybody can type reads differently.
What made that worth changing rather than guarding: aid forwards every leading dash-word it does not recognise straight into dl's argv without knowing what any of them mean. The missing flag is not hypothetical when another binary supplies arbitrary ones.
Two things the ticket asked for that were closed on wrong evidence, now corrected. aid's leading pair is real — aid does emit both flags ahead of the workspace, and what makes that safe is dl answering the pair before it reads where force sits, which nothing pinned. Both halves are pinned now, each naming the other. The README item is genuinely empty: the drift the ticket raised was against a change that moved which lines are refused, and neither the README nor the help text describes force's placement at all, so no sentence is now wrong. Recording that here rather than leaving it looking skipped.
Also learned, and worth keeping: an anti-shrink floor on a walk is not a guard. The floor here tolerated losing more than half the space, because every interesting line was short and truncating to the short ones passed everything. Pin the count.
Activity
blooop commentedon Aug 29, 2026
Claimed 2026-08-29: build in progress from an interactive session (opus agent in an isolated worktree, managed as part of closing out map #299). PR to follow. If you are another session seeing this, do not double-build.
blooop commentedon Aug 29, 2026
breadcrumb: building this as the guard it is, not a behaviour change.
Seam:
resolve(Cli, argv) -> Result<Command, GrammarError>in thedlcrate's grammar module. It is pure and total over argv, which is what makes an exhaustive walk of the argv space a test rather than a fixture.What lands: one enumeration over every ordering of every subset of the alphabet
{workspace name, rm, rme, --force, --rm}(each word at most once), resolved through that seam, with the expectation written from Python's own rule ("--force" in args[2:], args[0] the workspace and args[1] the verb) plus the fact that only the two delete verbs have anything to force. The alphabet carriesrmandrmedeliberately: they are the only tokens that can make the word grammar produce a forced delete, and the matrix that was reviewed on #344 omitted them, which is why the word half of the property was never actually exercised.Non-vacuity is proved twice: the walk also collects the lines that do force and asserts that set against a literal, and the whole thing is run against a deliberately reverted placement rule to watch it go red.
Two claims in the ticket body I will check first rather than assume, since #369 moved the ground under all of them: aid's leading
--rm --forceform, and whether the globals really have no placement rule.blooop commentedon Aug 29, 2026
breadcrumb: PR #506 — #506
The slice: one walk of every ordering of every subset of
{ws, rm, rme, --force, --rm}through the grammar's resolve seam, checked against Python'sargs[2:]rule plus the verb table, with the pair refusal held over the same space.rmandrmeare in the alphabet, which is what the #344 matrix was missing and what makes each ordering a live question about whether that line deletes.Proven non-vacuous against four reverted rules. The one worth naming: make the three-word arm resolve instead of refuse, and
dl ws rm --force rmeforce-deleteswswhile 149 other tests pass. Only the guards this PR adds go red on it. That is the ticket's latent hole, made live and then caught.Three things the body claimed that had already moved:
--rm --forceform is closed on main, both orderings, with the emitted index asserted.lib.rsline reference is stale after the--rmrework and there is nothing wrong at it now.--forcecould be mistaken for a word in, because the one global that takes a word is not one of the two that accept the flag. Written down as a test of that premise rather than as a comment, so it fails if somebody gives a force-accepting command a word.And one thing nobody had noticed: clap's two-word cap counts values per occurrence, so
dl a b --force chands the grammar three positionals wheredl a b cis refused at exit 2. The arm that catches it carried a comment saying a third word never arrives. Nothing forced escapes through it, but it is that arm's refusal doing the work rather than the cap, which is exactly the incidental fact this ticket was about. Corrected and pinned. No behaviour change anywhere in the diff.blooop commentedon Aug 29, 2026
wf-review on #506: Request changes — one blocking finding (
force_placement's absolute index is still shifted by a leading token, sodl <flag> ws --force rmwould force-delete wheredl ws --force rmrefuses; latent behind five unpinned facts). Enumeration verified total (325 lines, 259 walked), oracle verified independent, non-vacuity replayed. #506 (review)blooop commentedon Aug 29, 2026
breadcrumb: review found the leading half of the coincidence still open, and the fix turned this from a guard ticket into a one-line rule change.
The slot was counted over every argv token. A flag the parser has already consumed is gone from the words and still sitting in argv, so it shifted every slot up by one: a workspace line with any flag ahead of it read a verb-slot
--forceas trailing and force-deleted the workspace, where the same line without the flag refuses. No such flag existed, but only because five unrelated rules each refused or stripped one first. The slot is a place a word goes, so words are what it counts now. Nothing anybody can type reads differently.What made that worth changing rather than guarding: aid forwards every leading dash-word it does not recognise straight into dl's argv without knowing what any of them mean. The missing flag is not hypothetical when another binary supplies arbitrary ones.
Two things the ticket asked for that were closed on wrong evidence, now corrected. aid's leading pair is real — aid does emit both flags ahead of the workspace, and what makes that safe is dl answering the pair before it reads where force sits, which nothing pinned. Both halves are pinned now, each naming the other. The README item is genuinely empty: the drift the ticket raised was against a change that moved which lines are refused, and neither the README nor the help text describes force's placement at all, so no sentence is now wrong. Recording that here rather than leaving it looking skipped.
Also learned, and worth keeping: an anti-shrink floor on a walk is not a guard. The floor here tolerated losing more than half the space, because every interesting line was short and truncating to the short ones passed everything. Pin the count.