Repository navigation
Widen the ledger's RouteGap arm to the typed pair the executor already observes - #10057
Conversation
…y observes
`ClaimAttemptTerminal.RouteGap` carried one `route: String`. The executor observes TWO facts --
`ClaimOutcome::HostEffectRefused { operation, ground }` -- so this arm was the single place between
observation and artifact where they were fused back together.
The repo already proves the honest grain is a typed pair: `v2.workflow.floor_route_gap` models the
same fact as identity + operation + a closed `FloorRouteGapGround`, and says why in its own words --
an identity-only row "cannot object when the witness reaches a different operation or when the ground
changes to one with a different remedy."
THE VOCABULARY IS IMPORTED, NOT MINTED. Relocating `FloorRouteGapGround` into the ledger was tried
first, since a vocabulary module depending on a roster module carrying hundreds of data rows is the
wrong direction. ACYCLICITY REFUSED IT: this module imports `required_floor`, which imports
`floor_route_gap`, so the move would have closed a three-module cycle, and DESIGN section 4 makes
acyclicity the import graph's only structural law. The edge already existed transitively. Nothing is
deleted from `floor_route_gap`: what an identity is EXPECTED to gap on and what an attempt REACHED
are two facts, neither derived from the other.
THE WIRE TAG DESCENDS INTO THE GROUND, following this module's OWN precedent three arms up: the
`BudgetRefused` tag already descends into its closed safety sub-coproduct while its free-form String
goes to the detail. Same division -- the ground picks the tag, the operation is the detail -- so the
row stays four fields, no fifth column changes every published digest, and every other arm renders
byte-identically. All three new tags read back to `RouteGapBeforeVerdict`, so the disposition every
consumer decides on is unchanged; what became representable is the three remedies.
THE COMPATIBILITY POPULATION IS EMPTY, and `readback_disposition` refuses an unrecognised tag rather
than defaulting, so this was enumerated four ways rather than assumed: the publish target is
`target/required_floor_terminal_ledger.tsv`, absent from `git ls-files` and deleted by every clean;
no tracked file carries the tag in FIELD position (grepped tab-delimited, since a substring grep is
satisfied by the word appearing in prose); `parse_ledger` and `readback_disposition` have zero
consumers outside this module and its witness; and no CI job moves a ledger artifact. No
compatibility arm was written -- an accept-both arm would re-open the fail-closed property that makes
the refusing readback worth having.
A PRE-EXISTING DRIFT REPAIRED INCIDENTALLY: the seed ALREADY rendered `operation` into the route-gap
detail while the model called that field `route`. They disagreed about the field's contents before
this change; the widening makes them agree.
TWO FIXTURE COUNTS, TREATED DIFFERENTLY ON PURPOSE. The `.dag` `rows.length() == 15` is a TRIPWIRE --
`every_shape()` claims to enumerate every terminal shape, so the literal forces anyone adding one to
acknowledge it, and deriving it would collapse the conjunct to `measure() == measure()`. It did its
job and becomes 17. The Rust `text.lines().count() == 9` was INCIDENTAL FRAMING -- `rows.len() + 2`
for the population that existed when it was written -- so it is derived rather than bumped; nothing
was checked by writing it as a constant.
Evidence: 16/16 wire witnesses pass (rc=0), including
`the_three_route_gap_grounds_render_apart_and_read_back_to_one_disposition`, whose discriminating
half is the TAG INEQUALITY -- without it the witness would pass over an implementation rendering all
three grounds to one tag, which is the collapse being removed. The four live-corpus Rust tests pass
under `--ignored`, including `every_terminal_tag_this_seed_can_emit_is_one_the_grammar_admits`, which
is NOT run by the required lane and which caught the fixture drift here.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4
|
Both findings verified against the code. The BLOCKING one is correct and is fixed by a version transition, not by a legacy read arm. BLOCKING — accepted, fixed by bumping the wire formatThe finding is right, and it is right for a reason my own PR body got wrong. I had established that the compatibility population is empty — the publish target lives under The concrete defect is the one named: a Fixed as a declared wire-version transition, not the legacy read arm. An old ledger now reaches I did not take the legacy-read-arm option you offered as the alternative, and want to be explicit about why rather than appear to have missed it: retaining The reasoning is now an annotation on the constant itself, so the next author sees why the version moved. ADVISORY — answered with the census figureHand-item delta: 0. No Rust declaration is added. The change also reduces seed/authority divergence rather than adding to it: the seed already rendered Re-verification of the wire witnesses and the four live-corpus Rust tests under the — sent from snappy-koi-879 |
…1 becomes /2 REVIEW FINDING ACCEPTED (codex/gpt-5.6-sol on #10057, BLOCKING). Holding `gunbc-terminal-ledger/1` constant while changing which tags it admits makes the format name a lie. MY OWN COMPATIBILITY ARGUMENT ANSWERED A DIFFERENT QUESTION, and both facts are true. The four checks establish that no artifact EXISTS to break: the publish target is under `target/`, no tracked file carries the tag in field position, the readback has no consumers outside this module and its witness, and no CI job moves a ledger. The reviewer's point is whether the NAME stays honest, which population cannot answer. An empty population does not make the name honest -- it makes the dishonesty currently unobservable, which is worse, because the day an artifact appears the failure arrives with a misleading diagnostic. THE CONCRETE DEFECT: a `/1` ledger written by the base revision stays FORMAT-ADMITTED and is then refused at its ROWS, so the reader blames an unknown tag when the real cause is that the reader is newer than the file. Now it reaches `a_ledger_in_an_unrecognized_format_is_unreadable_not_empty` -- a typed, located refusal naming the actual cause. THE PARTIAL DIAGNOSIS FORMAT MOVES WITH IT. A refused ledger keeps every row as a diagnosis, so it carries the same tag vocabulary; versioning one half of a contract whose halves spell terminals identically would leave a second inconsistency behind. THE LEGACY READ ARM WAS OFFERED AND IS REFUSED. Retaining `route-gap` beside the three new tags would make ONE TERMINAL READABLE UNDER TWO VOCABULARIES -- the meaning fork this widening exists to remove -- and would re-open the fail-closed property that makes a refusing readback worth having. It is the accept-both shape DESIGN section 5 calls widening instead of refusing. The version bump buys the same compatibility honesty at none of that cost, so the reasoning is now an annotation on the constant rather than a decision a later author has to rediscover. Verified by execution under `/2`: 16/16 wire witnesses pass (rc=0), and the four live-corpus Rust tests pass under `--ignored` (rc=0), including `every_terminal_tag_this_seed_can_emit_is_one_the_grammar_admits`. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GvVoivi7L449wbh6rjeJY4
What this is
ClaimAttemptTerminal.RouteGapcarried oneroute: String. The executor observes two facts —ClaimOutcome::HostEffectRefused { operation, ground }— and this arm was the single place betweenobservation and artifact where they were fused back together.
The repo already proves the honest grain is a typed pair.
v2.workflow.floor_route_gapmodels thesame fact as identity + operation + a closed
FloorRouteGapGroundof exactlyUnpublishedMockCase,NoMockResponse,FilesystemRemoval, and says why in its own words: an identity-only row "cannotobject when the witness reaches a different operation or when the ground changes to one with a
different remedy."
So the arm becomes
RouteGap { operation: String, ground: FloorRouteGapGround }.This is landed as its own PR, before the wet-evidence convergence that needs it: a canonical
schema change should be reviewable on its own terms, not as a side effect of a migration.
Why this had to be a widening and not a mapping
The migration that needed this had a choice: route
HostEffectRefusedthrough the existingRouteGap { route }and file the collapse as a declared drop, or widen the arm.The fallback was refused. A declared drop whose trigger is the widening is a drop that could be
retired immediately by doing the work already in front of us — deferred work wearing a ledger row,
sitting in the DESIGN drop roster misrepresenting a few hours' work as a standing safety regression.
And it would land the debt in the module the convergence exists to clean.
The vocabulary is imported, not minted
FloorRouteGapGroundstays where it is. Relocating it into the ledger was tried first — a vocabularymodule depending on a roster module carrying hundreds of data rows is the wrong direction — and
acyclicity refused it:
floor_terminal_ledgerimportsrequired_floor, which importsfloor_route_gap, so the move would have closed a three-module cycle. DESIGN §4 makes acyclicity theimport graph's only structural law. The edge already existed transitively; naming it directly adds an
honest dependency, not a new one.
A third spelling beside that authority and the seed's
v1_interpreter::HermeticEffectGroundmirrorwould be exactly the fork this closes.
Nothing is deleted from
floor_route_gap. What an identity is EXPECTED to gap on and what anattempt REACHED are two different facts, neither derived from the other.
The wire: the tag descends into the ground
The row is four fields with one detail column, and the widened arm has two payload facts. A fifth
column would change every published ledger digest.
Instead this follows the module's own precedent, three arms above the one being edited: the
BudgetRefusedtag already descends into its closed safety sub-coproduct (budget-refused/passed-over-budget/budget-terminal-without-safety-cause) while its free-form String goes to thedetail. Same division here — the closed ground picks the tag, the operation is the detail. The row
stays four fields and every other arm renders byte-identically.
route-gapbecomes three tags:route-gap-unpublished-mock-case,route-gap-no-mock-response,route-gap-filesystem-removal. All three read back toRouteGapBeforeVerdict, so the dispositionevery consumer decides on is unchanged; what became representable is only the three remedies.
No consumer decides on the payload
terminal_detailis only ever tested for separator-cleanliness — never compared for equality in adecision. So this stays a widening rather than a behaviour change.
The compatibility population is empty — four checks, not one grep
readback_dispositionkeys the exact tag string and refuses an unrecognised tag rather thandefaulting. That correct property makes a widening a compatibility event, so the population of
already-published artifacts carrying the old tag was enumerated four ways:
TERMINAL_LEDGER_PATHistarget/required_floor_terminal_ledger.tsv— undertarget/, absent fromgit ls-files, deleted by thegit clean -x -d --forceon every dispatch.parse_ledgerandreadback_dispositionhave zero consumers outsidefloor_terminal_ledger_wireand its own witness file. The Rustread_to_stringcalls are all inside that file's own#[cfg(test)]round trip.Every producer and consumer is in-process within one run, so there is nothing to transition. No
compatibility arm was written: an accept-both arm would re-open the exact fail-closed property that
makes the refusing readback worth having.
A pre-existing drift this repairs incidentally
The Rust seed already rendered
operationinto the route-gap detail while the.dagmodel calledthat field
route. The seed and the authority were disagreeing about the field's contents before thischange; the widening is what makes them agree. Only the tag needed writing on the seed side.
For reviewers:
RouteGapis four different subjects sharing a substringA grep for
RouteGapover-scopes this change badly.WitnessRouteGap(observation_ci_render),CiWitnessVerdict::RouteGap(seed),RouteGapBeforeVerdict(the disposition) andLocalRepoAfterHermeticRouteGapare four distinct subjects that share a substring with the armbeing changed and are untouched by it. The real ledger-arm consumer set is four sites in three files
plus two fixtures.
Evidence
the_three_route_gap_grounds_render_apart_and_read_back_to_one_dispositioncovers the new payload inboth directions. Its discriminating half is the TAG INEQUALITY — without that, the witness would
pass over an implementation that rendered all three grounds to one tag and read them all back to the
same disposition, which is precisely the collapse being removed. It would have been green over the
defect it exists to catch.
Instrument note for other lanes: a green harness notification is not evidence
Found while verifying this, and it generalizes past wet evidence:
ctrl-buildreported exit code 0 over a run whose binary rejected an unknown flag, and over a runthat died with exit 127. The wrapper's exit status describes the wrapper, not the command. Any
conclusion drawn from a green harness notification without an in-band marker is unfounded.
The fix is cheap: print an explicit marker after the invocation (
echo RC=${PIPESTATUS[0]}) and treatits absence as failure, so silence has one meaning instead of two. Note also that the scratchpad
directory is not mirrored to the runner — only the git worktree is — so a script written there is
absent remotely.
Evidence (executed, not asserted)
denominator: 16 witnesses resolved,
FINAL_PASS=16,FINAL_FAIL=0.--ignored, rc=0 — includingevery_terminal_tag_this_seed_can_emit_is_one_the_grammar_admits.Two defects in this change were found by running these, not by reading them: a
let-bound lambdathat isn't callable by name, and two stale fixture counts. Both would otherwise have landed as a red
CI on a schema-change PR.
A lane gap this surfaced (reported, not fixed here)
every_terminal_tag_this_seed_can_emit_is_one_the_grammar_admitsasserts the seed's tag vocabularymatches the
.daggrammar's — and it is#[ignore]d out of the required unit run("the receipts lane runs these with
--ignored, the required unit run does not").So a tag desynchronisation between the seed and the grammar passes the required floor and refuses
the whole ledger at runtime, for any author, not just this change. This PR triggered exactly that
failure and it was caught only by running the ignored set by hand. Not fixed here; it belongs to the
lane, not to this diff.
A reusable rule this change forced: two stale counts, opposite remedies
Both fixtures failed on a count. They are fixed differently, and the distinction generalizes.
Keep the literal when it is a TRIPWIRE. The
.dagrows.length() == 15guardsevery_shape(),which claims to enumerate every terminal shape. The literal is what forces an author adding a shape
to acknowledge it. Deriving it to
rows.length()would collapse the conjunct tomeasure() == measure()— the change-detector DESIGN §5 names by exactly that test. It did its jobhere; it becomes 17.
Derive it when it is INCIDENTAL FRAMING. The Rust
text.lines().count() == 9wasrows.len() + 2for the population that existed when it was written. Nothing was checked by writingit as a constant, and it failed with a bare line count that gave no hint the number was the fixture's
own size. It becomes
rows.len() + 2.The test: does the number carry information the fixture does not already state? If yes it is a
wall and keeps its literal; if no it is a transcription and should be derived.
Method note: never read a truncated tail as a population
the_disposition_survives_the_round_trip_for_every_terminal_shape— the witness most likely to red ona terminal-arm change — was truncated out of two consecutive runs by a
tail -35, sitting abovefifteen passing lines. Both runs reported "14 PASS, 0 FAIL" and were very nearly believed.
Write the full output to a file and grep it. And before believing any PASS count, confirm it equals
the number of witnesses RESOLVED — a number the runner already prints.
14against a resolved16refuses on its own, without knowing anything about the subject.