docs: gate framing revision 5 --- pin both emitter pairs, correct print-plan
Revision 4 said it would close the rename hole for the sweep as well as the build, and then did not: its verification bullet required only a singular real-plan pair in the context of build-crdt. The hole is symmetric --- renaming sweep-crdt slips through exactly the same gap --- so section 7 now pins BOTH emitter pairs explicitly, name and exact command, asserted from the emitter where the name still exists. Two older bullets also still claimed named steps appear in --print-plan. They do not; that mode prints commands only, which is the wording that let the attribution witness drift away from the step it names in the first place. --print-plan is now described as the command and order witness, and nothing more. The ledger recorded revision 4 as approved and implemented, and presented the synthetic self-test as the attribution witness. Both were read as done. A recovering machine or a PR preparation from that entry would have shipped this lane without the regression guard it exists to provide. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_016bqGA6s9tTUFzYpbeW3tai
This commit is contained in:
parent
677fd25bcd
commit
74d735ff8d
|
|
@ -265,7 +265,7 @@ also removed: this branch's "R8 NEEDS A LANE" investigation block, and
|
||||||
durable facts are in the retired registry row and the handoff §6
|
durable facts are in the retired registry row and the handoff §6
|
||||||
census.
|
census.
|
||||||
|
|
||||||
## `scripts/gate --protocol` build step — IMPLEMENTED, no PR yet
|
## `scripts/gate --protocol` build step — IMPLEMENTED at `49bc141`, then RE-OPENED by review
|
||||||
|
|
||||||
**Written with the lane's first commit**, per the standing correction
|
**Written with the lane's first commit**, per the standing correction
|
||||||
from #171 and #215.
|
from #171 and #215.
|
||||||
|
|
@ -275,10 +275,24 @@ from #171 and #215.
|
||||||
authoritative tip** — the ref, not a SHA. Recover with
|
authoritative tip** — the ref, not a SHA. Recover with
|
||||||
`git fetch githubsucks && git checkout gate-protocol-build`.
|
`git fetch githubsucks && git checkout gate-protocol-build`.
|
||||||
|
|
||||||
- **Framing `docs/gate-protocol-build-framing.md`, revision 3,
|
- **Framing `docs/gate-protocol-build-framing.md`, revision 5.** The
|
||||||
APPROVED and implemented.** Narrow by design: one missing step in one
|
fix itself is implemented and green at `49bc141`; **the regression
|
||||||
script, plus the boundary question that let it go missing. No `src/`,
|
witness is NOT, and that is an open blocker.** Narrow by design: one
|
||||||
no protocol, no feature work.
|
missing step in one script, plus the boundary question that let it go
|
||||||
|
missing. No `src/`, no protocol, no feature work.
|
||||||
|
- **OPEN BLOCKER — the witnesses do not reach the step they name.**
|
||||||
|
`--print-plan` **strips names** before printing, so the ordering
|
||||||
|
assertion sees only commands; `--self-test` **hardcodes**
|
||||||
|
`build-crdt` inside its own synthetic plan. Review demonstrated the
|
||||||
|
consequence: **renaming the real build step to `sweep-crdt` left both
|
||||||
|
tests passing.** So this lane currently ships without the regression
|
||||||
|
guard it was created to provide. §7 now requires **both** real
|
||||||
|
emitter pairs — `build-crdt` and `sweep-crdt`, name *and* exact
|
||||||
|
command — because the hole is symmetric and revision 4 closed only
|
||||||
|
half of it. The synthetic `--self-test` stays: it witnesses the
|
||||||
|
*runner* (failure naming, `FAILED:` list, log paths, non-zero exit,
|
||||||
|
and continuation via the sentinel), which is a different thing from
|
||||||
|
attributing the real step, and it may no longer stand in for it.
|
||||||
- **The defect, as found.** `--protocol` adds the CRDT workspace sweep,
|
- **The defect, as found.** `--protocol` adds the CRDT workspace sweep,
|
||||||
whose documented precondition is `cargo build --workspace
|
whose documented precondition is `cargo build --workspace
|
||||||
--no-default-features --features luajit,crdt` — documented in handoff
|
--no-default-features --features luajit,crdt` — documented in handoff
|
||||||
|
|
@ -340,11 +354,59 @@ authoritative tip** — the ref, not a SHA. Recover with
|
||||||
cargo test …` reports a *build* failure under the name `sweep-crdt`.
|
cargo test …` reports a *build* failure under the name `sweep-crdt`.
|
||||||
Plus **`--self-test`** (Q#GR-5): a hardcoded three-line synthetic plan
|
Plus **`--self-test`** (Q#GR-5): a hardcoded three-line synthetic plan
|
||||||
— pass, fail-named-`build-crdt`, **pass sentinel** — driven through
|
— pass, fail-named-`build-crdt`, **pass sentinel** — driven through
|
||||||
the *real* runner loop, which is what makes attribution *and*
|
the *real* runner loop, which is what makes the **runner's** failure
|
||||||
continuation observable at all. `PLAN_FILE` is deliberately **not**
|
naming *and* continuation observable at all. (It does **not** witness
|
||||||
|
the real step's name — see the round-two entry below, which is where
|
||||||
|
that gap was found and closed.) `PLAN_FILE` is deliberately **not**
|
||||||
injectable: that would turn the runner's `eval` into a general command
|
injectable: that would turn the runner's `eval` into a general command
|
||||||
executor, the same defect this script's review caught in
|
executor, the same defect this script's review caught in
|
||||||
`--acceptance`.
|
`--acceptance`.
|
||||||
|
- **THE WITNESS DID NOT REACH THE STEP — found in review of the
|
||||||
|
implementation, closed at `677fd25`.** The lane shipped without the
|
||||||
|
regression guard it was created to provide, because **neither witness
|
||||||
|
could see a name**: `--print-plan` renders `emit_plan | cut -f2-`, so
|
||||||
|
the ordering test compared *commands* with the names cut off, and
|
||||||
|
`--self-test` hardcodes the string `build-crdt` in its **own
|
||||||
|
synthetic** plan, so it proves things about the runner and nothing
|
||||||
|
about the real emitter. Review demonstrated it directly: **renaming
|
||||||
|
the real build step to `sweep-crdt` left both tests passing** — a plan
|
||||||
|
that would report a build failure under the sweep's name, sitting
|
||||||
|
green, which is the exact misattribution the separate step exists to
|
||||||
|
prevent.
|
||||||
|
|
||||||
|
**The fix is `--print-plan-named`**: a second *rendering* of the same
|
||||||
|
`emit_plan`, printing the `name<TAB>command` text the runner reads
|
||||||
|
back from `PLAN_FILE`, asserted by **whole-line equality** so name and
|
||||||
|
command are pinned together, and `sweep-crdt`'s pair asserted too
|
||||||
|
(asserting only the build's name leaves the identical hole open in the
|
||||||
|
other direction). **`PLAN_FILE` remains uninjectable** — a test that
|
||||||
|
supplied the runner's plan would turn its `eval` into a general
|
||||||
|
command executor, the defect the `--acceptance` refusal exists to
|
||||||
|
prevent — and **`--self-test` stays**, witnessing the *runner* (failure
|
||||||
|
naming, `FAILED:`, log paths, non-zero exit, continuation via the
|
||||||
|
sentinel), which it may no longer *stand in for* attribution of the
|
||||||
|
real step. A companion test pins `--print-plan` as that rendering
|
||||||
|
minus its names, so the two cannot drift into asserting a name the
|
||||||
|
runner never uses. Both new tests are on the **no-gates** paths.
|
||||||
|
|
||||||
|
**Mutated individually, each now red** (the first is the one the
|
||||||
|
previous round passed): build renamed `build-crdt` → `sweep-crdt`;
|
||||||
|
sweep renamed `sweep-crdt` → `crdt-sweep`; build features
|
||||||
|
`luajit,crdt` → `luajit`; build emitted **after** the sweep. Suite is
|
||||||
|
20 tests.
|
||||||
|
- **AUDITED FOR THE SAME DEFECT ELSEWHERE, and one instance is left
|
||||||
|
open deliberately.** Renaming **every other** plan step — `fmt`,
|
||||||
|
`clippy`, `lib`, `m4`, `gpu`, `sweep`, `diff-check`,
|
||||||
|
`acceptance-<suite>` — leaves all 20 tests green: no test asserts any
|
||||||
|
step name but `build-crdt` and `sweep-crdt`. For most that is only a
|
||||||
|
log filename and a `FAILED:` entry. **`sweep` is not**: the runner's
|
||||||
|
end-of-run listing globs `"$LOGDIR"/*-sweep.log` and
|
||||||
|
`*-sweep-crdt.log`, so renaming that step silently empties the *"read
|
||||||
|
these, do not re-run and grep"* listing that is the U2/U3 remedy, with
|
||||||
|
the suite still green. **Not closed here**: the listing only exists on
|
||||||
|
the *run* path, and every test in this file is deliberately no-gates,
|
||||||
|
so there is no cheap witness for it — recorded rather than papered
|
||||||
|
over.
|
||||||
- **Blocks PR #228 (discovery Stage 2).** That lane's `--protocol`
|
- **Blocks PR #228 (discovery Stage 2).** That lane's `--protocol`
|
||||||
result needs re-establishing on a fresh target dir under the repaired
|
result needs re-establishing on a fresh target dir under the repaired
|
||||||
script. Deliberately **not** folded into that feature branch, and it
|
script. Deliberately **not** folded into that feature branch, and it
|
||||||
|
|
@ -378,12 +440,13 @@ authoritative tip** — the ref, not a SHA. Recover with
|
||||||
registry row; noted here for whoever sees it next.
|
registry row; noted here for whoever sees it next.
|
||||||
- **Gates:** `scripts/gate --acceptance gate_script_acceptance`. Note
|
- **Gates:** `scripts/gate --acceptance gate_script_acceptance`. Note
|
||||||
the recursion — this lane edits the script that runs its own gates,
|
the recursion — this lane edits the script that runs its own gates,
|
||||||
so `--print-plan`, `--help` and `--self-test` were also checked by
|
so `--print-plan`, `--print-plan-named`, `--help` and `--self-test`
|
||||||
hand after each edit: a change that breaks the script cannot be
|
were also checked by hand after each edit: a change that breaks the
|
||||||
reported honestly by the script. The assertions were **mutation
|
script cannot be reported honestly by the script. The assertions were
|
||||||
tested**: wrong features, wrong position, unconditional emission,
|
**mutation tested**: wrong features, wrong position, unconditional
|
||||||
an aborting runner, and the build folded into `sweep-crdt` each fail
|
emission, an aborting runner, the build folded into `sweep-crdt`, and
|
||||||
the suite.
|
— added in the second round — a **rename of either** the build or the
|
||||||
|
sweep step each fail the suite.
|
||||||
|
|
||||||
## QoL arc retirement — PR #224 OPEN (docs only)
|
## QoL arc retirement — PR #224 OPEN (docs only)
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -1,8 +1,9 @@
|
||||||
# `scripts/gate --protocol` — the build its sweep depends on
|
# `scripts/gate --protocol` — the build its sweep depends on
|
||||||
|
|
||||||
**Status: revision 4. APPROVED and IMPLEMENTED at `49bc141`; one
|
**Status: revision 5. APPROVED and IMPLEMENTED at `49bc141`. The
|
||||||
regression-witness gap found in review of that implementation remains
|
regression-witness gap found in review of that implementation is
|
||||||
open (Q#GR-5).**
|
CLOSED at `677fd25` — Q#GR-5's criterion is now witnessed against the
|
||||||
|
REAL emitter rather than around it.**
|
||||||
|
|
||||||
*(Revisions 1-3 read "Pre-implementation. Awaiting approval" while the
|
*(Revisions 1-3 read "Pre-implementation. Awaiting approval" while the
|
||||||
ledger recorded this lane as approved and implemented — the exact
|
ledger recorded this lane as approved and implemented — the exact
|
||||||
|
|
@ -96,9 +97,10 @@ rather than an assumption the fix rests on.
|
||||||
`sweep-crdt` and only under `--protocol`***, running the invocation
|
`sweep-crdt` and only under `--protocol`***, running the invocation
|
||||||
handoff §5 names.
|
handoff §5 names.
|
||||||
|
|
||||||
- **A named step, not a silent prelude.** It appears in
|
- **A named step, not a silent prelude.** It gets its own numbered log
|
||||||
`--print-plan`, gets its own numbered log alongside the others, and
|
alongside the others and fails the suite under its own name.
|
||||||
fails the suite with its own name if the build fails.
|
(It does **not** "appear in `--print-plan`" — that mode prints
|
||||||
|
commands only. §7 says what witnesses the name.)
|
||||||
- **Not folded into the `sweep-crdt` command.** `cargo build … && cargo
|
- **Not folded into the `sweep-crdt` command.** `cargo build … && cargo
|
||||||
test …` would make a *build* failure appear under the name `sweep-crdt`
|
test …` would make a *build* failure appear under the name `sweep-crdt`
|
||||||
in the failure list — a wrong attribution in the one place the script
|
in the failure list — a wrong attribution in the one place the script
|
||||||
|
|
@ -254,15 +256,25 @@ named so it is not mistaken for an oversight.
|
||||||
|
|
||||||
## 7. Verification
|
## 7. Verification
|
||||||
|
|
||||||
- **`--print-plan --protocol` emits `build-crdt` immediately before
|
- **`--print-plan --protocol` witnesses COMMAND and ORDER only** — it
|
||||||
`sweep-crdt`, carrying the EXACT command.** All three asserted —
|
strips names before printing, so it can show that the build command
|
||||||
presence, position, and the literal
|
appears immediately before the crdt sweep command and nothing about
|
||||||
`cargo build --workspace --no-default-features --features luajit,crdt`.
|
which step is called what. Earlier revisions of this section said
|
||||||
Name and position alone would pass on a step that builds the wrong
|
named steps "appear in `--print-plan`"; they do not, and that wording
|
||||||
feature set, which is the failure this lane is fixing: the crdt sweep
|
is what let the attribution witness drift away from the step it
|
||||||
needs *those* features, and a `build-crdt` that ran plain
|
names.
|
||||||
`cargo build` would leave the gate exactly as unsound while looking
|
- **BOTH real emitter pairs are asserted, explicitly and separately:**
|
||||||
repaired.
|
- `("build-crdt", "cargo build --workspace --no-default-features --features luajit,crdt")`
|
||||||
|
- `("sweep-crdt", "cargo test --workspace --features crdt --no-fail-fast -- --skip basedpyright")`
|
||||||
|
|
||||||
|
Both, because the rename hole is symmetric: revision 4 closed it for
|
||||||
|
the build and left the sweep able to be renamed just as invisibly.
|
||||||
|
Asserted from the emitter, where the name still exists.
|
||||||
|
|
||||||
|
The **command** half matters as much as the name: a `build-crdt`
|
||||||
|
running plain `cargo build` would leave the gate exactly as unsound
|
||||||
|
while looking repaired, because the crdt sweep needs *those*
|
||||||
|
features.
|
||||||
- **`--print-plan` WITHOUT `--protocol` does not emit it** (subject to
|
- **`--print-plan` WITHOUT `--protocol` does not emit it** (subject to
|
||||||
Q#GR-1 — if the default sweep turns out to need the binary too, this
|
Q#GR-1 — if the default sweep turns out to need the binary too, this
|
||||||
assertion inverts and §4 changes with it).
|
assertion inverts and §4 changes with it).
|
||||||
|
|
@ -285,6 +297,20 @@ named so it is not mistaken for an oversight.
|
||||||
The synthetic failure/continuation test stays — it tests the runner,
|
The synthetic failure/continuation test stays — it tests the runner,
|
||||||
which is a different thing — but it can no longer stand in for
|
which is a different thing — but it can no longer stand in for
|
||||||
attribution of the actual step.
|
attribution of the actual step.
|
||||||
|
|
||||||
|
**Landed at `677fd25` as `--print-plan-named`**: a second *rendering*
|
||||||
|
of the same `emit_plan`, printing the `name<TAB>command` text the
|
||||||
|
runner reads back from `PLAN_FILE`, asserted by **whole-line
|
||||||
|
equality** so the name and the command are pinned together.
|
||||||
|
**`sweep-crdt`'s own pair is asserted too** — asserting only the
|
||||||
|
build's name leaves the identical hole open in the other direction.
|
||||||
|
`PLAN_FILE` stays uninjectable, and a companion test pins that
|
||||||
|
`--print-plan` *is* that rendering minus its names, so the two cannot
|
||||||
|
drift and the assertion cannot come to pin a name the runner never
|
||||||
|
uses. **Mutation tested, each individually red:** the build renamed
|
||||||
|
to `sweep-crdt` (**the one the previous round passed**), the sweep
|
||||||
|
renamed, the build's features changed, the build emitted after the
|
||||||
|
sweep.
|
||||||
- **The suite CONTINUES past a failed gate** (Q#GR-2) — the sentinel
|
- **The suite CONTINUES past a failed gate** (Q#GR-2) — the sentinel
|
||||||
step after `build-crdt` in the synthetic plan has its own log.
|
step after `build-crdt` in the synthetic plan has its own log.
|
||||||
**Revision 2's two-line plan could not assert this**: with the
|
**Revision 2's two-line plan could not assert this**: with the
|
||||||
|
|
|
||||||
Loading…
Reference in New Issue