Repository navigation
Publish the floor's terminal ledger by calling the v2 grammar, atomically, or refuse with the rows intact - #8909
Merged
Conversation
…ntity join THE OBLIGATION, WHICH IS WHY THIS EXISTS -- not the size of anything. The v2 self-host program claims candidate-bound witnesses executed and matched their expectations. The seed is the only producer that simultaneously holds a witness identity and its terminal Pass, and it destroys the identity at accumulation: `ClaimOutcome::Pass => outcome.passed += 1`. So a run reporting `passed=10132` cannot say WHICH. The v2 obligation is not realizable without a seam there. This commit is the v2 half: the schema and the completeness law. It touches no seed and no Rust. A PASS LIST IS THE WRONG ARTIFACT AND THIS IS DELIBERATELY NOT ONE. A roster of passing identities reproduces one layer up the ambiguity it was built to remove: an identity ABSENT from a pass list is failed, interrupted, unrouted, never executed, or lost to truncation -- five states behind one silence. The ledger carries ONE ROW PER PLANNED IDENTITY and every row is terminal, so absence is not a value it can express. `Pass` IS A PROJECTION, NOT A STORED FIELD. There is no `passed: Bool` in the row, so a row cannot disagree with its own disposition -- the disagreement has no constructor. `claim_disposition` derives from (expectation x observation) over the Returned / DiagnosedStop / Interrupted grain, and `Interrupted` carries the existing `ClaimSafetyOutcome` rather than a second spelling of it. An attempt that RETURNED may still have observed nothing, so `ClaimObservation` separates `ObservedVerdict` from `ObservationUnrepresentable`. Collapsing the second into `holds: False` would report a failing witness where the truth is a witness whose answer was never in a readable shape. COMPLETENESS IS AN IDENTITY JOIN, AND HERE IS THE CASE THAT FORCES IT. One planned identity never reaches the ledger; another is written twice. Row count equals planned count. Every aggregate in the run summary is IDENTICAL to a correct run. A count-based check is green and the missing witness -- possibly the one just added -- reports as covered. `LedgerReconciliation` is therefore a RECORD of three independently-joined sets, not a coproduct: a coproduct would report the first defect and hide the second, and this failure mode is exactly the one where two defects appear together and cancel. Measured, same test, two trees: identity join returned `true` count comparison the swap satisfies (control) returned `false` GREEN ADMISSION IS A TYPED OUTCOME, NOT A Bool. `LedgerGreenAdmission` has four arms -- EvidenceComplete, EvidenceUnfinalized, EvidenceReconciliationFailed, EvidenceFooterCountDisagrees -- because a Bool cannot say WHY evidence was refused and the three refusals have three different remedies. THE FIRST DRAFT RETURNED A Bool AND IT MADE A PARTIAL LEDGER READ GREEN. The arm was `LedgerPartial => bool_boolean_algebra.bottom`, which typechecked, ran, and answered the opposite of what it says -- the exact "instrumentation optional precisely when it fails" arm this schema exists to forbid. It was caught by a test written to fail in both directions, not by review. The substrate defect underneath it (v2 has two non-interoperating representations of Bool) is filed separately against v2.std.logic and is NOT fixed here: it is std's, and bundling a substrate repair into a self-host evidence vertical makes both harder to review. The footer count is checked against the PLANNED population, never against the rows the reader parsed -- a truncation that dropped rows and rewrote the footer to match would agree with itself. Five tests, all green, each with the discriminating arm named in its own carrier. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…ete the field nothing read
Four review findings, all correct, all measured rather than argued.
1. THERE WAS NO CANDIDATE BINDING, and this module's own header claimed
CANDIDATE-BOUND witnesses. There was no `Ledger` type at all -- only rows,
reconciliation and publication -- so a ledger from run A was structurally
indistinguishable from evidence for run B, and the obligation's completed claim
("identity W appears exactly once in candidate C's terminal population") had no C
to name. That is the difference between a ledger and evidence.
`TerminalLedger { binding, rows, publication }` with `LedgerBinding
{ repository_snapshot, prepared_subject, roster_identity }`. The binding is a
FIELD, not a sibling artifact, so an unbound ledger is unrepresentable rather
than merely unusual, and `ledger_green_admission` now takes the ledger.
2. `DiagnosedStop { reason: Symbol }` COLLAPSED ARMS THE SEED ALREADY HOLDS
TYPED, and the seed's own comment argues against it: "A collapsed `failed` would
make a budget refusal, a runtime error and a witness that answered false read
alike, and those three have different remedies." A Symbol reason is a RENDERING
of the terminal fact, not the fact -- and the boundary is "v1 preserves the raw
terminal fact it already holds". Stringing it during transport would make the
ledger strictly less informative than its producer, which inverts the obligation.
Now RuntimeErrored { message } | BudgetRefused { safety } | HostToolUnresolved
{ name, probed } | RouteGap { route }, mirroring ClaimOutcome one for one.
3. `digest: String` was a hollow carrier -- it admits any text and cannot be
compared against anything else in the corpus that hashes. Now
`std.content_hash` `Fnv1a64Structural`, the structural family member DESIGN
names.
4. `ordinal: Int` WAS CARRIED AND NEVER READ, while this comment claimed it made
a missing row visible as a gap. Nothing in the schema touched it. That is
rung inflation at carrier grain: the guarantee existed only in the prose.
The repair is not a contiguity check -- it is DELETING THE FIELD. Position in a
list is dense and unique by construction, so a duplicated or gapped ordinal has
no spelling rather than being caught by a validator. Truncation is still caught,
by the footer count against the planned population, which is implemented and
tested.
A stale import of the renamed variant was caught by the resolver, not by me.
Five tests, all green after the rework.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…lapsing what the row un-collapsed A. `Symbol` WAS USED THREE TIMES WITH NO IMPORT LINE. It typechecked and every test passed because v2 resolves bare symbols against the whole pool, so the module carried a real dependency that no import recorded -- the exact class of invisible edge the census lane measures, authored fresh in a module whose purpose is making evidence inspectable. The gap was mine: a `sed` removing the line when `DiagnosedStop` was replaced. Worth recording because it shaped my confidence: the resolver DID catch a stale import of a renamed variant one commit ago, so I read it as covering imports. It covers WRONG imports, not MISSING ones. A passing test suite established nothing here. B. THE DISPOSITION RE-COLLAPSED THE ARMS THE ROW HAD JUST SEPARATED. Four terminal shapes -- RuntimeErrored, HostToolUnresolved, RouteGap and ObservationUnrepresentable -- all projected onto one `RefusedBeforeVerdict`, one step after the row was un-collapsed for precisely the reason that a budget refusal, a runtime error and a witness answering false have different remedies. It is not cosmetic. The floor reports these as SEPARATE COUNTERS today -- `host_tool_unresolved`, `route_gap_unenrolled`, `route_gap_held`, `stale_route_gap`, `interrupted_before_verdict` -- and the obligation requires the counters to be DERIVED from finalized rows so a counter disagreeing with the ledger has no constructor. A projection that has already merged two counters can derive neither, so they would have had to be computed independently: the dual authority the derivation exists to dissolve, reintroduced by the projection meant to replace it. `ClaimDisposition` now has one arm per terminal shape -- BudgetRefused, HostToolUnresolved, RouteGap, RuntimeErrored and ObservationUnreadable, each `BeforeVerdict` -- so every counter the floor reports stays derivable. Losslessness was chosen over a declared coarseness because coarse-but-declared would still have forced the counters to a second authority. Five tests green. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…derive `passed` from it The v2 self-host program declares a per-identity completed-evidence obligation over the required floor. This process is the only producer that holds a witness identity and its terminal outcome at the same moment, and it destroys the pairing at accumulation -- `ClaimOutcome::Pass => outcome.passed += 1` keeps the count and drops the name -- so the obligation is not realizable without a bridge here. Collection and consumer land together. Every planned identity mints exactly one `ClaimTerminalRow` before the branching, `reconcile_terminal_ledger` joins that population against the planned one by identity, and a mismatch is a typed `TerminalLedgerIncomplete` refusal naming the three sets. `passed` is then derived from the rows and the old increment is DELETED, not kept beside it: two authorities over one fact is what this removes. Completeness is an identity join, not a count equality. A ledger that omits one identity and duplicates another has the same row count, the same `passed`, and the same planned/executed/receipted triple as a healthy run -- the preceding `ClaimIdentityCountsDisagree` check is green over it. The discriminating RED is `a_duplicate_replacing_an_omission_is_caught_while_every_count_stays_equal`, which asserts the counts equal before asserting the join refuses; replacing the join with `planned.len() == rows.len()` turns it and its sibling red, measured. The seed stays narrow: it preserves raw terminal facts it already holds. No candidate digest, no expectation join, no artifact verification, no general evidence API. The binding -- which candidate this evidence is for -- is v2's to compute and mean. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…r, and close the test's missing import Two carrier findings from review, and one from the automated pass. DISSOLUTION CONDITION. The ruling admitted this bridge on conditions and one of them had no representation in the diff: nothing named what retires the seam. It is named now, on both carriers, and it is ONE event for both findings -- the self-emitted v2 claim executor. Once v2 drives the floor's execution, the producer holding identity-and-outcome together IS v2, so `ClaimTerminalRow`, `claim_disposition`, `reconcile_terminal_ledger` and the refusal are deleted whole. THE MIRROR IS A SECOND AUTHORITY AND NOTHING CHECKS IT. `cli_run.rs` is HAND_MAINTAINED, so the Rust types are authored beside the `.dag` schema, not derived from it. Regen does not compare them -- the file is not generated. The witnesses do not compare them -- each side is exercised alone. So the two share only names, which is exactly the seam this change repaired one grain down when it extracted `reconcile_terminal_ledger` so its test could not be a control sharing only a name with its subject. That rule condemns this seam too; here it is declared debt at *mitigatable* with a named terminal rather than silently repaired. No lens is built: the cheapest honest check reads the seed's emitted ledger, which cannot exist before serialization does. Also corrected: both headers claimed the seed SERIALIZES the ledger. It does not yet -- the rows are consumed in-process by the reconciliation refusal and the `passed` derivation, and binding, footer and atomic publish land with the artifact. MISSING IMPORT. `LedgerPublication` was used as a parameter type and never imported; whole-pool resolution accepted it and every test passed. Imported now. The same sweep found `BudgetRefused` / `BudgetRefusedBeforeVerdict` imported and unexercised, so the arm gets the test it was missing rather than losing the import: a budget refusal is a pre-verdict disposition, not a failure, and collapsing the two would leave `budget_refused` underivable from the rows. Calibrated -- mutating that arm to `Failed` turns the new test red and leaves its sibling green, which is why the arm needed its own test. 6/6 PASS on the .dag roster; 3 passed on the Rust law. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…irections
The schema said a ledger "is published atomically under its final name" with "a
footer carrying the row count and a digest over the rows". No such artifact existed;
the sentence described an intention. This is the wire form.
ONE GRAMMAR, BOTH DIRECTIONS (§4). `render_*` selects a production forward, `parse_*`
selects the same productions backward. A separately-authored reader would be the N x M
adapter pair §4 refuses, and two hand-written halves of one grammar agree until the
day they do not.
THE FIDELITY BOUNDARY IS A TYPE, NOT A FOOTNOTE. `LedgerReadbackRow` is a different
type from `ClaimTerminalRow` rather than a partially-filled one: the wire preserves
identity, expectation and terminal shape exactly, and does not carry
`SafetyInterrupted`'s timings or `HostToolUnresolved`'s probe list. A reconstructed
row with zeros there would be a fabricated plausible value -- a reader could not tell
an interruption at 0ms from one whose timing the file never held.
FAIL-CLOSED AT EVERY ARM. A field carrying the separator makes the ledger
UNRENDERABLE rather than being sanitized (the neighbouring disposition writer does
`.replace(['\t','\n'], " ")`, which publishes a different fact than the one observed).
An unrecognized format refuses instead of reading as an empty ledger. An unrecognised
terminal tag refuses instead of defaulting. The footer count is compared to the
PLANNED population, never to the rows the reader parsed, because a truncation that
rewrote its own footer agrees with itself.
NO `parse_int` ON THE FOOTER. The host primitive answers `Value::Null` for text it
cannot read, so every interpretation of a damaged count is a fabrication. The expected
count is rendered and the text compared -- total, no failure arm.
FIELDS ARE EXTRACTED BY MATCHING, NEVER BY CASTING AN OPTIONAL. `fields.first() as
String` type-checks and renders the WRAPPER, so a field would silently become
`Present { value: … }` with no diagnostic anywhere.
THE DEFECT THIS ALREADY CAUGHT, IN THIS MODULE, MEASURED: the first parser searched
the mapped list for an absent element (`filter(parsed, r => match r { Absent => true
… })`). It found nothing while `flat_map` over the SAME list dropped the row, so a
ledger with one damaged line parsed as a shorter well-formed one -- `read:1` where it
should have refused. The empty-observation narrow, committed by the function whose own
comment forbids it, and caught by `one_unparseable_line_refuses_the_whole_file` going
red. The repair compares recovered rows to lines read, which cannot disagree with
itself.
6/6 tests green by execution, including the disposition surviving the round trip for
EVERY terminal shape rather than a sample -- a tag collision shows up in exactly one
arm and nowhere else.
The seed-side production consumer (host write, atomic publish) is not in this commit
and this is not yet a PR.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Once the ledger's bytes come from evaluating this module, an interpreter defect makes the ledger unwritable, and unwritable evidence is not green -- so a run whose witnesses all passed still reds. That is the intended direction, not an oversight: the alternative is a green run whose evidence is silently missing, which is the instrumentation being optional exactly when it fails. Declared because undeclared it reads as fragility rather than as a chosen trade. The opposite failure -- wrong bytes rather than none -- is caught by the round trip, since the digest is recomputed from the rows a reader parses and compared to the footer the writer emitted. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The seed holds the rows and does the host write; the bytes are produced here. Something must still cross the boundary -- two type systems have to meet somewhere -- and the seed says which terminal arm a claim reached in THIS module's vocabulary rather than its own. That crossing is irreducible. It being UNCHECKED is not. `cli_run.rs` derives a disposition from `ClaimOutcome` and `expected_red`; this module derives one from the wire tag and the expectation. Two independent derivations of one fact over one row, so the seed sends both its tag and its disposition and a row whose answers disagree makes the whole ledger UNRENDERABLE with a typed reason. That is the mirror comparator the schema's debt note names, running in production on every row rather than as an offline audit. Stated at its honest scope: it does NOT retire the declared debt -- the two `ClaimDisposition` declarations are still authored beside each other and this catches a divergence in the MAPPINGS, not in the type declarations -- but for the part it covers the seam moves from "nothing detects a divergence" to "a divergence stops the line", mitigatable to mechanically preventable. TWO RENDERERS WOULD BE A FOURTH REPRESENTATION, so the seed-facing renderer is asserted to produce byte-identical output to the typed one over EVERY terminal shape, not a sample. Discriminating REDs, both green by execution: a row whose disposition disagrees with its tag refuses naming the offending identity, and a tag this module does not know refuses rather than rendering a row whose meaning a reader would derive differently. Also: an import sweep of both modules against the declarations they import -- the check I filed as a §4b row this morning, run by hand. It found no missing import and three imported-but-unused names (`ClaimObservation`, `WitnessIdentity`, `ClaimDisposition`, `CompletedWithinSafetyLimits`), now removed. 9/9 tests green after the removal. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…evidence I had NOT done this and the objection is right. `LedgerUnrenderable` carried only a reason and one offending identity, so the seed would have written nothing at all: an operator holding a refusal that names ONE identity has no way to tell whether the defect is isolated to that row or spans every row of a whole terminal shape, because the ten thousand rows that answer it went with the file. That is the instrumentation-optional-exactly-when-it-fails shape one turn up -- the diagnosis disappears on precisely the run where something went wrong. The mechanism already existed in the ruling: refuse to finalize, and keep the rows under a partial marking. So `LedgerUnrenderable` now carries a `diagnosis` -- every row the sender sent, in the sender's own words, plus a `#refused` line naming the reason and the offending identity. The floor still goes non-green and nothing here mints a receipt; only the evidence for diagnosing it survives. A PARTIAL FILE CITED AS A LEDGER HAS NO SPELLING, rather than being forbidden by a convention someone must remember. The diagnosis opens with a different format token, so `parse_ledger` refuses it as `ledger-format-unrecognized` -- it cannot be read as a short run. It carries no footer, so nothing about it can look finalized. Seed rows are rendered with five fields rather than four, so a line from it is not even shaped like a ledger row. Fields are written RAW, including the separator-carrying field that may have caused the refusal: a diagnostician needs the byte that broke the grammar, and a sanitized diagnosis of a sanitization defect is useless. 10/10 tests green by execution, counted against the roster in the file. The new one asserts all three rows survive, that the offending identity is named, and that reading the diagnosis back refuses ON THE FORMAT rather than on its contents. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…eady owns The seed can supply a prepared-subject digest and a git sha. `LedgerBinding` typed all three fields as `Fnv1a64Structural`, which is `String where lower_hex_16` -- so a 40-hex commit id would have REFUSED AT CONSTRUCTION. Option "derive a digest and keep the type" was not merely dishonest, it was unconstructible, and the corpus settled it before the question was asked. NO NEW REF TYPE. `extdeps.git.object_store` `GitObjectId` exists, is cited to the upstream authority, enforces family, length and lowercase syntax through validating constructors, and v2 ALREADY binds artifacts to it -- `v2.compiler.self_host` `frontier_probe_types` carries `source_commit` and `source_tree` as `GitObjectId` for exactly this purpose. Minting a `RepositoryRef` beside it would be the §3 nicknaming violation committed inside a change whose subject is single authority. "local" IS NOT A REF, AND THAT DISTINCTION IS EVIDENTIAL. The completed claim is "witness W terminated in candidate C"; a run with no published commit has no C, so its ledger is not candidate-bound and must not be citable as though it were. So the absence is an ARM -- `UnpublishedWorkingTree` -- and `ledger_is_candidate_bound` answers from the shape rather than by string-comparing a magic value that a future edit could respell. An unrecognised snapshot REFUSES rather than being read as unpublished: "anything I could not decode is a local run" would silently downgrade candidate-bound evidence, which is the direction that loses evidence quietly. TWO FACTS, TWO FIELDS. The ref says which commit a human opens; the prepared-subject digest says what was admitted. They diverge on every run of this floor, because preparation declines sites. One deliberate departure, declared on the carrier: `git_object_id_untagged_hex_note` says our own wires stay family-prefixed via `render/parse_git_object_id_wire`. THOSE FUNCTIONS DO NOT EXIST -- a stale citation of the §3 class -- and following the sentence would mean minting the pair here, in a change about something else. The wire reuses the authority in both directions instead: `git_object_id_wire_hex` forward, `git_object_id_from_untagged_hex` backward, the latter being the module's own decoder for text git itself produced, which is exactly what GITHUB_SHA is. Also caught in my own fixture: `git_object_id_from_untagged_hex(...) as GitObjectId` on an absent arm type-checks and RENDERS THE OPTIONAL WRAPPER -- the trap this module refuses in its parser, sitting unreachable in a test until the day it was reached. The fixture now routes through the production admission and degrades to `UnpublishedWorkingTree`, which a test asserts against, so a bad fixture fails loudly instead of fabricating. 12/12 green by execution, roster read from the file. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…he product layer My previous carrier note said `render_git_object_id_wire` / `parse_git_object_id_wire` DO NOT EXIST. They do -- `gunbc.merge_admission_subject` lines 97 and 104, imported by `gunbc.merge_admission_produce` and called at eight sites in `merge_admission_attempt_witness_test`. My grep searched ONE FILE, the extdeps module, and I read a single-file absence as a corpus-wide one. Landing that note would have authored the stale-citation class I thought I was reporting. The decision survives; the reason is replaced with the true and better one: the pair lives in a PRODUCT-layer module, so a `v2.workflow` module reaching for it would take a dependency on merge admission in order to render a git object id -- a worse coupling than using the extdeps authority the type already belongs to. The real defect underneath is smaller and different: the note cites those symbols WITHOUT NAMING THEIR MODULE, and they live downstream of the carrier doing the citing. That is the §3 'name the module and symbol' rule, and the bare name is precisely what made a narrow grep read as absence. It wants its own change.
…refuses The last piece: the artifact the schema described now exists on disk, and the seed does not render a byte of it. WHAT THE SEED DOES: builds a context for `v2.workflow.floor_terminal_ledger_wire`, hands over each row in that module's vocabulary, and writes what comes back. The bytes are produced by evaluating the `.dag` authority — the same shape `cli_run` already uses for `wire_fnv1a64_content_hash_hex` — so the artifact is not a third representation beside the schema and the seed's declared mirror. THE MIRROR COMPARATOR RUNS IN PRODUCTION, ON EVERY ROW. `claim_disposition` derives a disposition from `ClaimOutcome`; the module derives one from the wire tag and the expectation. Two independent paths — `(outcome -> disposition)` and `(outcome -> tag -> disposition)` — so the seed sends both and a disagreement refuses the ledger naming the identity. Honest scope: this catches divergence in the MAPPINGS; the two `ClaimDisposition` declarations are still authored beside each other. THE COST, PRINTED RATHER THAN ASSERTED. The context is built after the fold, not held across it: `run_required_floor` drops its `hermetic` frame before the fold under a measured note (6.58GB -> 9.15GB, a runner that throttles at `memory.high`, a last run ~1MB under the watermark), and holding a resolved context would pay in MEMORY on a run already at the line, in a shared cgroup where the kernel kills the largest task — a death that is non-deterministic, unattributable, and can land on someone else's work. Paying in TIME instead is deterministic and degrades by being slow. The corpus walk is not re-paid: this resolve goes through the shared `MultiEntryIndex` the floor already warms during preparation. Every run prints `phase=terminal-ledger-publish resolve_ms=… total_ms=…`, so the number is an instrument rather than a claim in a PR body. PUBLICATION IS UNCONDITIONAL AND ATOMIC. No env var gates it; evidence written only when convenient is the instrumentation-optional shape. Bytes go to a temporary and are renamed, so a reader never observes a half-written ledger. A grammar refusal writes every row to the diagnosis path instead and REFUSES the floor — the run that went wrong keeps its evidence, under a format token the ledger reader rejects. `ROSTER IDENTITY IS DERIVED, NOT SUPPLIED`, and `LedgerBinding` no longer has the field: a stored roster identity can disagree with the population it names, and nothing in the floor computes one. Both renderers fold it from the identities being published, which is also what makes the byte-equality law between them load-bearing. EXECUTION, not typecheck: 4 Rust tests calling the real `publish_terminal_ledger` — real resolve, real interpreter, real bytes, real rename — including the discriminating RED where a disposition disagreeing with its tag refuses and the diagnosis keeps both rows. Wire `.dag` 12/12, schema `.dag` 7/7, rosters read from the files. Two environment defects found by their own refusals rather than by debugging: the entry was spelled relative to the workspace root and refused for any other CWD (now resolved under the declared roots), and the tests first wrote into a non-ignored `target/` beside the crate (now a temp dir, one path per test so four parallel tests cannot read each other's bytes). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…47-ledger-artifact # Conflicts: # src/v1/stage0/src/cli_run.rs # src/v2/workflow/floor_terminal_ledger.dag # src/v2/workflow/floor_terminal_ledger_test.dag
…space gaps The `format!` literal was a single line carrying runs of ~22 spaces where line breaks were intended, so the refusal reached an operator looking as though it had been wrapped and then un-wrapped. Replaced with `\` continuations, each carrying its space before the backslash so the message renders space-joined rather than run together. Cosmetic in the sense that the refusal was already typed and located; not cosmetic in the sense that a refusal is read by a human under time pressure, and this one was hard to read at exactly that moment. Found by review 54771. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The doc comment three lines above said "Every shape this cannot read is a REFUSAL, never a default." The code then read `reason` and `offending` with `unwrap_or_default()`, so a `LedgerUnrenderable` missing either field produced a refusal reporting an empty cause. The reviewer called this harmless because the `.dag` variant is fixed-shape, and that is true exactly while the two sides agree. But a shape disagreement between the seed and the grammar is the ONE thing `read_render` exists to catch, so the default fired only in the case the function was written for — and swallowed it, publishing a blank where the cause belongs. Both now refuse, matching `diagnosis`'s existing treatment, and the code matches its own stated contract. Found by review 54780, which filed it as a minor note. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
…s, and design the calibration that distinguishes them ONE ROW OVER THE WHOLE MIRROR WAS WRONG IN BOTH DIRECTIONS. It under-rated what the production comparator guarantees and over-rated what the hand-written declarations do, so the two halves are now named separately: TerminalDispositionWireAgreement mechanically preventable SeedDagTerminalSchemaDeclarationLockstep mitigatable Class 1 carries its guarantee (the seed's disposition equals the one decoded from the tag it emitted; a disagreement refuses the ledger naming the identity), why it is not structural (the invalid pair is still constructible, it just cannot become accepted evidence), its stated NON-CLAIM (neither derivation is proven correct in isolation — two mappings jointly wrong in the same direction agree, so it catches divergence and never error), and its coverage bound (the join runs over the OBSERVED population, not over every declared arm; an arm no live row reaches is unexercised and the join is silent about it). Class 2 enumerates the six things that still pass unnoticed rather than leaving "the declarations are unchecked" as a gesture. The wire-side note is re-pointed to NAME both classes instead of restating the rung it had half-stated. Two accounts of one standing drift apart, and the one a reader finds first wins rather than the one that is right. docs/plans/terminal-ledger-calibration.md designs the population that closes the coverage bound: nine rows, one per disposition, authored from the declared vocabulary rather than harvested from a run — a population measured out of the current tree is not an oracle. Two things the design adds beyond the sketch. Mutations 1 and 2 must be applied INDEPENDENTLY: together they cancel, both sides move the same way, the comparator agrees, and the green would read as a pass when it is exactly the jointly-wrong case Class 1 declares it cannot catch. And mutation 5 — change a payload contract while keeping every tag — must NOT red, doing double duty as the positive control on Class 1's scope and the standing RED for Class 2. Without it the two rows are indistinguishable by any executed evidence and Class 2 is decoration. Verified the schema module still resolves and evaluates after the comment edit: `the_fixture_binding_is_candidate_bound` returns `true`. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Contributor
Author
|
The It is not inert. And it refuses in both directions, which I checked separately because a one-directional guard would leave the more likely drift silent:
The asymmetry that would have broken this doesn't exist: the token is a word and the alternative is 40 lowercase hex characters, so no drifted value can be mistaken for the other branch. So the class is §3 duplication with a verified live structural refusal on drift — worth naming, correctly not blocking, and I agree with your read of the fix (expose the token through the same interpreter call surface the render already uses, once a general wire-constants-from-the-grammar pattern exists rather than as a one-off). Not fixing it in this PR, for a reason beyond scope: Two things I'd flag as more load-bearing than this one when the follow-up lands, both from this same review cycle: — sent from fierce-lynx-647 |
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 22, 2026
…on is unilateral The consequence I published from §4m was "a deletion PR that merges main cleanly is not verified by that merge, so deleters owe a resolve pass". True, and it told a sibling lane it was clear when it was not. bright-ferret-335 checked its subtree against that rule, found no deletion lanes (#8877, #8909, #8882 are purely additive) and concluded it had nothing to check. #8909 adds three files that all import v2.workflow.floor2_prepared_subject -- the module §4m restores. THE HAZARD IS SYMMETRIC AND THE ADDER IS THE WORSE SIDE. A deleter that merges main discovers an added consumer in its own resolve. An adder is already green when the deletion lands later and breaks it, and an additive PR feels safe by construction, so its author has no reason to ask whether anything it imports is scheduled for deletion in someone else's open branch. The party in danger is the party without a prompt. The proposed repair was an intersection requiring one side to publish a list, premised on neither side being able to run it alone. THE DELETER-CANNOT-SEE HALF IS FALSE, and I falsified it by running it: open PR heads are on the remote, so the intersection went against all three sibling PRs from this side with no list. Zero real exposure -- no qualified import of any of the 55, and of the 664 symbols declared solely by the 55 with no surviving declarer, one token hit: render_footer in #8909, which declares its own and never depended on the deleted tools.readme. Deleting it REMOVES a two-declarer whole-pool ambiguity rather than creating a break. So the obligation is unilateral, which is the point of restating it: a rule requiring publication is a rule requiring coordination, and coordination fails silently when a lane is busy, blocked or archived. A rule one party can execute alone has no such failure mode. The deleter owes the intersection against every open PR head at merge time; the adder owes nothing but pushing. An adder who cannot be expected to look cannot be expected to publish either. Residue, strictly smaller than the coordinated version: this reaches PUSHED work only. Never-pushed worktree state is unreachable by any mechanism, and that alone is what publication would buy. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 22, 2026
…mprove resolution safety From bright-ferret-335, reading the intersection result rather than the rule. The render_footer hit read as a hazard -- a name declared by a module being deleted and used in an open PR -- and inverted on inspection: #8909's consumer declares its own, and while tools.readme stands the name has TWO whole-pool declarers. It is AMBIGUOUS, and the deletion REMOVES the ambiguity. So the same intersection that finds breaks also finds improvements, and a reviewer who reads any token hit as danger will misclassify this direction. It matters beyond one row because it is the ambient-pool defect in miniature: a name resolving by whole-pool uniqueness is one deletion away from binding differently, so its meaning is a function of the corpus denominator rather than of anything written at the declaration or the use. This deletion moves that name from two declarers to one. NOTHING STRUCTURAL GUARANTEES THE NEXT ONE MOVES THAT WAY -- the mechanism that disambiguates here can elsewhere silently rebind a use from one surviving declarer to another. Not created by this change, not closed by it, and visible from here only because an intersection over deletions is one of the few operations that looks straight at it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
added 3 commits
August 22, 2026 21:08
…47-ledger-artifact
…e §4c admits them The required floor refused this branch: thirteen lines -- eight in floor_terminal_ledger_wire.dag and five in floor_terminal_ledger_wire_test.dag sat inside declaration bodies, and §4c models annotation capture at module-item grain only. The refusal is correct and the diff was wrong. Both blocks are hoisted above the declarations they describe rather than deleted, because both carry irreducible rationale a reader cannot recover from the code: the wire block records that the shortfall check is a length comparison because the obvious search shipped green and WRONG (`filter` over the mapped list found nothing while `flat_map` dropped a row -- the empty-observation narrow, committed inside the very function the annotation describes), and the test blocks name what each assertion line is checking, in order, which is the part a `&&` chain does not say. One wording fix followed from the move: the wire block said "the function whose comment above forbids it" while sitting below that comment. Hoisted, it IS the comment above, so the sentence now names the function the annotation describes. Verified by execution rather than by grep: the test function that carried three of the five now parses and evaluates, refusing only at the exit-code wall (`returned `true`, not `ProcessExit``) -- which is the assertion passing.
…ready owns that name The floor refused with `unresolved type 'SnapshotRefused'` at dag/gunbc/devboot/build.dag:229 -- a file this branch does not touch. The cause is in this branch anyway: floor_terminal_ledger_wire.dag minted a variant named SnapshotRefused while gunbc.devboot.produce already declared one, so the name had two authorities and an unrelated module's resolution broke. That is the §3 nicknaming violation, and the blast radius landing outside the diff is exactly why it is a correctness concern rather than a style one. Renamed to SnapshotWireUnrecognized, which also says more: this variant is about a snapshot field on the WIRE that did not admit, not about a snapshot operation refusing. The sibling SnapshotAdmitted was checked and is unique to this module. NOT VERIFIED BY THE LOCAL CONTROL, and the reason is worth stating: an entry-scoped run resolves only the entry's import closure, and build.dag's closure never reaches this module, so re-introducing the collision produced output identical to the fixed tree. A control that cannot go red is not evidence. The verdict comes from a whole-corpus --required-ci run.
briansrls
pushed a commit
that referenced
this pull request
Aug 23, 2026
…-first, batched, refusals reported as the census (#8862) * B1 — the RESIDUE-EMPTY control batch: 6 modules with no content to strand The census's control batch, run first for the reason it was chosen as one: a module that declares no symbol cannot be bare-referenced, so RESIDUE-EMPTY scored 0-of-8 consumed on the defect-6 re-score and is the batch that proves the deletion mechanics without risking working code. Every file here is a module line plus at most an import or a single unread String; none declares a symbol, none is named by any .dag, .rs, .yml or .toml in the tree. v2.bin.main's main_rs_trampoline_authority is the one row carrying content, and it is dead data in DESIGN 4c's sense: the only other occurrence of that text in the tree is a parse specimen in gap4_parse_tokens_remain_test.dag, which embeds the literal as a fixture rather than referencing this module. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * B2 — 66 modules unreachable from every root and named bare by nothing The remainder of the residue that carries no obligation to anything outside itself: not reachable from any discovery path, entry row or v1 seed mirror; no uniquely-owned symbol named bare by any .dag file in the corpus; and no mention in any .dag, .rs, .yml, .yaml, .toml or .sh source. Their only occurrences tree-wide are in .md prose, repaired in the next commit. None of the 66 declares a test fn, so no assertion stops executing with them, and none has a src/v1/stage0/src mirror, so the seed population is unchanged. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Restore gunbc.scm.commit_closure_store: the census deferred it by name, and it is not residue The census's finding on this row is that it is a replacement-migration leftover, not residue: gunbc.scm.repository_envelope took its grain one day later and left the Filesystem save/load half unattached. Which way that resolves -- the envelope grows save/load, or this module is the persistence layer the envelope should consume -- turns on the #8820 author's intent, and the census explicitly declined to disposition it for that reason. Sweeping it here on an unreachability score would answer that question by deletion. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Repair the two doc citations the deletion would have stranded Both rows describe a deleted module as a live subject: model-grounding-lens-extract names gunbc.tools.grounding_confirm as the CONFIRM judge, and review-surface-subject-map weighs gunbc.pr_digests.MergeReadinessVerdict as a second required aggregate. The analysis in each stands; only its premise about what exists in the tree does not, so the row is marked rather than rewritten. Three further mentions are deliberately left untouched. floor-cut-replacement-plan names dag/gunbc/floor_resolve_realization.dag on a 'delete as reachability confirms' list, so this deletion DISCHARGES that row rather than stranding it. Two receipts embed the literal git-status line 'A src/v2/workflow/host_discovered_owned_data_manifest.dag' inside a transcript; editing a transcript to match a later tree would falsify the receipt. algebra-grounding-unification-design names std.list as a road not taken, not as an authority it cites -- and the stub's deletion corroborates it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Record the disposition: 71 deleted, 68 held with a typed reason each The census answers what is unconsumed; this records what was done to it. Every held row carries the reason it survived, because a refusal is the deliverable here as much as a deletion is. Three results worth the document rather than the commit message. The instrument was re-derived rather than inherited, and it reproduces the census within four days of drift (131 residue -> 139), which is what makes the deletion auditable against the tree it ran on rather than against a row list. Re-scoring AFTER the cut is the discriminating evidence: reachable and CONSUMED-DECISIVE are both unchanged, so nothing with a live caller moved, while population fell by exactly the file count. And seven modules moved from DEAD-CONSUMER-ONLY to STILL-UNCONSUMED as their island neighbours went -- the census predicted the mechanic and this measures it, so the residue list is a fixed point reached by iteration, not a set reached in one pass. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Point the census at its execution record One line, at the top, because the two documents answer different questions and a reader who finds the census must not conclude the population is untouched. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Keep the instrument beside the census, drop the working blobs The script is what makes the numbers checkable; the JSON it emitted is derived data with no consumer, so it is ignored rather than committed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Specify the instrument in prose: the repository excludes *.py, so the method ships instead Committing the script was the first attempt and .gitignore refused it tree-wide. Rather than route around that, the method is written out to the grain a reader can re-implement, and the section-2 counters are noted as checkable without it at all. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * The deletion's one real strand: two pinned exclude lists named a file that no longer exists Found by widening the mention scan past the source extensions to .txt/.json, which is where it was hiding: docs/probes/census_extra_excludes.txt and its seeds file both listed dag/examples/gunbhub_serve_program/gunbhub_serve_program.dag, and census_exclude_derive.rs loads both -- the seeds drive the derived closure and the oracle is its drift witness, so a row naming a deleted path skews the symmetric diff between them in the direction that reads as drift rather than as staleness. The row is removed from both rather than the file being restored: the exclusion existed to keep a module out of a resolve walk, and a module that is gone needs no exclusion. The two count literals that pin those files (83 -> 82, 27 -> 26) move with them; they are not oracles in DESIGN 5's sense either before or after, and this change does not make them one. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Record the .txt strand in the disposition, and what it says about the precondition A source-extension mention scan is not a complete consumption surface. The finding is small -- one row in two pinned lists -- but the lesson is the reusable part, so it goes in the document rather than only in the commit that fixed it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Record what the manifest deletion actually removed, and why its exclusion rows stay Review cleared two surviving references to a deleted filename as harmless string patterns, which is right. Checking why turned up two things worth the row. The deleted module was a committed instance of an artifact the generator that produces it stamps DO NOT COMMIT -- a second module path holding an all-zero copy -- so the deletion has a better justification than unreachability. And the exclusion rows are LIVE, not dead: path_excluded is a substring match over the full path, so the pattern still matches the ephemeral file the generator writes. Tidying them away, which 'a pattern matching nothing' invites, would re-admit a generated transport into discovery. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Restore gunbc.pr_digests and the deficit filing: one instrument defect, one KEEP disposition TWO RESTORES, DIFFERENT CAUSES, AND ONLY THE FIRST IS A DEFECT IN THE MEASUREMENT. gunbc.pr_digests is instrument defect 7, and the floor found it: "unresolved type MergeReadinessVerdict" plus eight "undefined variable Ready" in gunbc.code_change_workflow and its witness. The re-score's declared-symbol extraction read fn/data/type/const declarations and NOT COPRODUCT VARIANT CONSTRUCTORS, so the variants of type MergeReadinessVerdict = Ready | NotReady {...} contributed no owned symbols. code_change_workflow names Ready bare with no import -- exactly the whole-pool resolution the re-score exists to see -- and the instrument was blind to the constructor half of it. Counting variants moves CONSUMED-DECISIVE from 89 to 94 at this branch's base and reclassifies pr_digests as consumed. Same class as the census's own defect 6, one level down: a surface decoded for declarations and not for their variants. gunbc.generic_binder_field_projection_deficit is NOT a measurement error -- it scores STILL-UNCONSUMED correctly. It is dispositioned KEEP-WITH-REASON in #8851 as a DESIGN 4b deficit filing: declared rung, ceiling, next-rung trigger. An unconsumed deficit row is 4b(2) working as specified, since a class below its ceiling is REQUIRED to name its trigger and nothing consumes that filing by design. Deleting it would have removed a safety-ledger row and lowered a rung with none of the declaration 4b(3) demands. Unreachability is simply the wrong predicate for this class of row, and the census said so before I ran. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Record instrument defect 7 and the deficit-filing restore in the disposition The floor's refusal is the section that matters: the two counters I offered as discriminating evidence were computed by the instrument that had the defect, so they could not see the case they were blind to. A control derived from the measurement it controls does not discriminate that measurement's blind spot. The floor did. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * File defect 7 in the census, and the count-literal finding beside the v1 edit Defect 7 goes in the census document rather than only here, because it is a defect in that document's METHOD -- an extractor that reads fn/data/type/const and not variant constructors cannot answer the bare-symbol question defect 6 poses. Its scope is stated precisely: measured in this lane's re-implementation, unmeasured in the census's own, so the 91 and 96 are to be checked rather than assumed either way. The lesson is carried verbatim, because it generalizes past this row: a control derived from the measurement it controls does not discriminate that measurement's blind spot. Both counters this lane offered as safety evidence came from the instrument carrying the defect, and they read as reassurance precisely because they were consistent. The count literals moved for the pin are filed as a change detector with a receipt -- one row moved for an unrelated reason and both literals had to be hand-followed -- and deliberately not fixed, since the pin has its own lane and its own declared dissolution. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Restore 13 more: the corrected extractor moves them to AMBIGUOUS, and the src/v1 edit dissolves with them silent-deer-368 sent four discriminating cases for the declared-symbol extractor. Mine passed three and FAILED the fourth: a same-line coproduct, type X = A | B, where the variants sit on the type line itself and a start-of-line variant scan never sees them. That is a fourth under-extraction bug in the same family as defect 7, and under-extraction creates FALSE UNIQUENESS, which is the delete-a-live-module direction rather than the keep-a-dead-one direction. Adopted their region-based extractor, which fixes all four at the root instead of patching a regex per bug: a type's region runs to the next TOP-LEVEL declaration (so a multi-line variant record cannot truncate it), a leading generic <...> is stripped before testing for =, and operation/service/resource are counted as declarations in the flat service namespace. All four discriminators now pass, and the (c) tell passes too: extdeps.transports.sql is AMBIGUOUS rather than consumed-by-filesystem_io, which linked only through operation Delete. THE RE-DERIVATION IS NOT A NULL RESULT. 13 of the 69 leave the residue, and every one lands in AMBIGUOUS-SHARED-ONLY -- no longer provably unconsumed, and NOT proven consumed. That bucket needs a per-row read, so none of them may be deleted on this evidence: nine formatters, the language_model rust root, generic_instantiation, roadmap_dispatch, and gunbhub_serve_program. Restored. 56 remain, still a strict subset of the corrected 114-row residue, still zero island violations. The src/v1 edit dissolves rather than being justified. It existed only because a deleted path left a dangling row in census_extra_excludes; gunbhub_serve_program is back, so the row is correct again and the two count literals go back to 83 and 27. This PR no longer touches the frozen seed at all. The change-detector finding about those literals stands on its own and stays filed -- it was always a property of the pin, not of this deletion. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Close the island: rust_leaf_model_claim's consumer came back with the 13 Restoring v2.test.language_model.rust re-created an in-population consumer for v2.std.rust_leaf_model_claim, so deleting the latter would split the island the restore had just re-formed. This is the island constraint behaving exactly as the census describes it -- eligibility is a property of the SET, so changing the set changes who is eligible, and a restore can create a violation as readily as a deletion can. Computed as a fixed point rather than a single pass: repeatedly drop from the deletion set any module with a surviving in-population consumer, until nothing drops. One iteration, one module. 55 deletions, zero island violations, still a strict subset of the corrected residue. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Delete commit_closure_store on its author's answer, with the cause they gave gentle-eagle-360 (#8820's author) answered the arm the census deferred, and corrected the premise of BOTH arms it offered. The correction is the part worth the row: the envelope did NOT supersede this module -- it holds zero Filesystem operations and not one func, it is a pure codec -- and it should NOT consume it either, because a commit-closure carrier demands a root and a repository's init has none, so wiring them would force init to invent a phantom commit. A census that records a false cause for a true deletion still carries a false row. Cause: STAGED ORPHAN AT THE WRONG GRAIN. Deleted rather than held for the repository-grain layer because a surviving X is an attractor -- every nearby persistence question keeps getting answered in vocabulary already scheduled to die. That is an author volunteering their own module on the doctrine. They also volunteered a defect that strengthens it: the header claims persistence is verified by direct execution in Wet mode, and the probe it names is enrolled nowhere and executes nothing. Unconsumed AND overclaiming its own evidence is a stronger warrant than unreachable. Island check re-run with it in the set, since eligibility is a property of the set: 56 deletions, fixed point, zero violations, still a strict subset of the corrected residue. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Bring the record's headline numbers and deleted table in line with the final 56 Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Rewrite the record's stale sections against the final set Four sections described a tree this branch no longer produces. Rewritten rather than annotated, because two accounts of one fact is the defect this document polices elsewhere: section 2's counters are re-measured on the corrected instrument and DEMOTED to necessary- but-not-sufficient with the reason; 4b records the .txt strand as a surface finding whose repair dissolved when its module came back; 4d grows from one defect to four with the mechanism they share and the 13 rows re-deriving cost; 4g makes the island fixed point its own section, since it fired in both directions and is the reason this is one PR. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Regenerate the held table against the final set, and name the ambiguous 97 beside it Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Section 7: state the limits against the final set, including the ones this lane created Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Record the discriminator roster, the count/set rule, and the two-population skew The reusable result from the cross-lane exchange is that a discriminator travels and a description does not: three relayed bug descriptions found one bug in this extractor, and the four test cases that came with them found a second nobody had named. (e) is contributed back with a specimen whose declared set is EMPTY under an unfixed extractor rather than merely incomplete, which puts it directly on the delete-a-live-module precondition. silent-deer-368's count/set rule is recorded verbatim because it resolves what looked like a discrepancy between two implementations into a property worth stating: a residue COUNT from the precise implementation, a deletion SET from the conservative one. And the skew is stated as a finding rather than bookkeeping, because the natural summary of it is wrong in the dangerous direction. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Record (f) and its second half: a generic parameter is a binder on both sides of the instrument The sixth case from silent-deer-368 still failed here after implementing (f) exactly as described, because the construct produces TWO independent false references: the parameter list in the header, and uses of the bound name in the declaration's body on the next line. Only region-scoped shadowing moved v2.std.projection to AMBIGUOUS. Scoping is the safety-critical part and the obvious implementation is wrong in the dangerous direction: dropping a bound name file-wide REMOVES references, which moves live modules into the residue. Shadow is scoped to the binding declaration's region. Also withdrew the service short-name credit -- my pattern never matched dotted forms but did match undotted ones, which is exactly the class that produced a false consumption claim on the other lane. Both defects inflate consumption, so neither could have caused a wrong deletion; the deletion set is unchanged at 56 with all six discriminators passing. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Correct this document's own reason for dropping the service credit The reason given was a false-consumption claim measured on the other lane's instrument, and it was never true on this one -- their specimen is a DOTTED service name that this lane's pattern never matched. Restored and re-run with (f) fixed, the credit moves nothing here, so the honest reason is 'no measured effect on this population'. And the evidence points the other way: artifact_store_fs bare-resolves Filesystem.Write with no import, and Filesystem is declared undotted by two modules. A consumer DOES name a service short name bare, so a wholesale withdrawal stops filesystem_io owning a symbol it visibly declares -- the own-nothing direction (e) exists to catch. Recorded as the seventh discriminator. Adopting a peer's conclusion is not the same as reproducing their measurement, and writing their reason into this document as though it were mine was the same error this lane already filed once: a claim carried rather than checked. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Restore the service credit on correctness of ownership, the basis that actually settles it Third and final revision of this reason, and the churn is the point: 'it causes false consumption' was another lane's measurement I had not reproduced; 'no measured effect' is true but settles nothing, since nil effect argues for either choice. Correctness of ownership does settle it -- filesystem_io declares service Filesystem, so an instrument denying it is wrong whether or not a row moves. And withholding the credit was worse than a missing fact: Filesystem is declared twice, service in filesystem_io and resource in std.resources, so dropping the service side handed std.resources FALSE SOLE OWNERSHIP -- manufactured uniqueness, the mechanism behind every wrong attribution in this chain, created by the fix meant to avoid it. Dotted forms now credited by last segment too. Zero exposure in this corpus, same basis. Deletion set unchanged at 56, subset, zero islands, counts identical. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Roster OwnedDataDiscoveryReceipt: the floor's second refusal, and it is correct Deleting the committed copy of the DO-NOT-COMMIT manifest (4c) removed the only non-test reference to this carrier, so it became inert and unrostered and the inert-carrier lens refused. Verified directly on the symbol's references before and after, not through the re-implementation I first reached for -- that re-implementation shared ZERO names with the live roster under two different readings, so its stable delta was suggestive and not evidence. Rostered rather than restoring the module. The carrier's real consumer is generated at runtime and stamped DO NOT COMMIT, so in the committed tree it is inert BY CONSTRUCTION and no corpus scan can see otherwise; re-committing a file its own generator forbids committing, in order to green a hygiene lens, would be the tail wagging the dog. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Record the OccurrenceId-keyed reproduction hazard as a class finding Not a claim about this change, which fixed nothing, and not about the original defect, which was root-caused at the declaration with a caller census and is green on main by that repair. The claim is about the CLASS: a defect keyed on a specific OccurrenceId value stops reproducing under any change that perturbs allocation, so a bisect across trees of different module counts measures luck rather than the defect. This branch is the specimen precisely because it contains no fix -- 16 identities red at the base, the same 16 green on a tree differing only by 56 deletions, planned identical at 10425 so roster change is ruled out and corpus size is the isolated variable. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Record what the static instrument was worth, and the rule for editing the set Two findings the lane owes its next reader. First, measured rather than asserted: across seven instrument defects and four extractor corrections, the static census never identified a live module -- it identified unknowns, correctly, and the one true positive came from one execution. DESIGN 3 as a measurement against a static alternative that had four rounds of sharpening. Second, the zero-near-miss reading carried verbatim, because it is the antidote to a later reader relaxing at a zero: AMBIGUOUS means unresolved, a live module would present exactly as those 13 do, so the honest statement is thirteen rows of unknown status I would have deleted. The same standard is turned on the 56 being deleted -- LowerBoundOnly, best-evidenced, not proof -- which is the argument FOR landing and reading refusals. And the editing rule: 69-13+1 reconciles by the wrong route, since 13 left evidentially and one left structurally. Anyone editing this set re-runs the fixed point rather than adjusting the count; the failure mode is silent because the arithmetic keeps agreeing. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Downgrade the hazard-(b) control: a matching count does not rule out roster change An earlier revision claimed 'planned is identical at 10425, which rules out roster change'. It does not -- identical counts are consistent with an unchanged roster and do not establish one. And the caveat is not theoretical: on the next run offered moved 11798 -> 11812 and routed 10425 -> 10439 across two commits changing only a markdown file and one inert_row data row, declines unchanged. Fourteen witnesses entered discovery with no corpus change, cause not yet attributed, so the discovered roster is not a pure function of the committed tree. The comparison survives as corroboration -- the two runs agree on every reported discovery figure and differ by exactly the 56 deletions -- but the isolated-variable claim is downgraded. This is the failure the document records elsewhere, committed in its own write-up: a count treated as a check. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Remove .census/s.json: session scratch with no consumer, and the .gitignore hand-edit it caused .census/s.json is the disposition instrument's raw output, swept into 19d6301 by a broad `git add` rather than authored as a repository fact. Nothing in the tree cites it -- not the census, not the disposition record, not a lens. That is DESIGN.md's experimental-residue tell exactly: a new artifact with no final consumer, in a PR whose whole subject is removing artifacts with no consumers. The accident had a second half. To stop the directory reappearing I had hand-added `.census/` to `.gitignore` -- which is a GENERATED artifact, emitted from gunbc.gitignore_authority. That is manual application committed as source (DESIGN.md §6): the line survives until the next regen and then vanishes without anyone editing it, so the rule it states is not a fact the authority holds. The merge with origin/main surfaced it as a driver refusal on that path, which is the driver working as specified. Both halves are dropped rather than legislated. The scratch directory is session-local and belongs in the session scratchpad, not the repo, so the authority has nothing to say about it and no row is added to it. .gitignore is taken at origin/main's regenerated bytes. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Restore v2.workflow.floor2_prepared_subject: the merge was a third census, and it refused #8896 landed src/v2/workflow/floor_terminal_ledger.dag on main while this branch was open. It imports WitnessIdentity and witness_identity_qualified_name from v2.workflow.floor2_prepared_subject by name, and its test does the same. This branch deletes that module. THE TWO BRANCHES TOUCH DISJOINT FILES, SO GIT MERGED THEM CLEAN. No textual conflict, no marker, no driver refusal -- and the merged tree does not compile. A three-way textual merge answers "did the same bytes change twice"; the question that decides this case is "does the merged tree still resolve", which is not a question about bytes. A merge preserves bytes, not measurements: every count in the disposition record is a statement about a tree, and the merge produced a tree none of them were measured against. The measurement was not wrong. The module was STILL-UNCONSUMED at base 90986d1 on every decoded surface and still is at that commit; it acquired a consumer afterwards. This is the census's second blind spot and it is not fixable by improving the instrument: a static census reads a tree, and the part that had not been written yet is as invisible as the part it decoded wrongly. Found by re-scoring the deleted set against the MERGED tree rather than against main -- a deliberately over-generous token match that flagged nine, of which eight were prose, annotation, or substring collisions (`Binding` inside CapabilityBinding prose, `YamlBool` whose live declarer is a coproduct VARIANT -- defect 7's own shape, in the triage regex this time -- `grade` and `readme` in citation text) and one was real. §4l's rule was followed rather than the count adjusted: the restore's imports were checked for in-population consumers, the fixed point closed at one restore, no cascade followed. 56 deleted becomes 55. The near-miss ledger reads 2, both found by execution and neither by the census: gunbc.pr_digests and this one. §4m records it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Correct §4m's rule: the adder is the exposed side, and the intersection is unilateral The consequence I published from §4m was "a deletion PR that merges main cleanly is not verified by that merge, so deleters owe a resolve pass". True, and it told a sibling lane it was clear when it was not. bright-ferret-335 checked its subtree against that rule, found no deletion lanes (#8877, #8909, #8882 are purely additive) and concluded it had nothing to check. #8909 adds three files that all import v2.workflow.floor2_prepared_subject -- the module §4m restores. THE HAZARD IS SYMMETRIC AND THE ADDER IS THE WORSE SIDE. A deleter that merges main discovers an added consumer in its own resolve. An adder is already green when the deletion lands later and breaks it, and an additive PR feels safe by construction, so its author has no reason to ask whether anything it imports is scheduled for deletion in someone else's open branch. The party in danger is the party without a prompt. The proposed repair was an intersection requiring one side to publish a list, premised on neither side being able to run it alone. THE DELETER-CANNOT-SEE HALF IS FALSE, and I falsified it by running it: open PR heads are on the remote, so the intersection went against all three sibling PRs from this side with no list. Zero real exposure -- no qualified import of any of the 55, and of the 664 symbols declared solely by the 55 with no surviving declarer, one token hit: render_footer in #8909, which declares its own and never depended on the deleted tools.readme. Deleting it REMOVES a two-declarer whole-pool ambiguity rather than creating a break. So the obligation is unilateral, which is the point of restating it: a rule requiring publication is a rule requiring coordination, and coordination fails silently when a lane is busy, blocked or archived. A rule one party can execute alone has no such failure mode. The deleter owes the intersection against every open PR head at merge time; the adder owes nothing but pushing. An adder who cannot be expected to look cannot be expected to publish either. Residue, strictly smaller than the coordinated version: this reaches PUSHED work only. Never-pushed worktree state is unreachable by any mechanism, and that alone is what publication would buy. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Record the sign-reversed token hit as its own class: a deletion can improve resolution safety From bright-ferret-335, reading the intersection result rather than the rule. The render_footer hit read as a hazard -- a name declared by a module being deleted and used in an open PR -- and inverted on inspection: #8909's consumer declares its own, and while tools.readme stands the name has TWO whole-pool declarers. It is AMBIGUOUS, and the deletion REMOVES the ambiguity. So the same intersection that finds breaks also finds improvements, and a reviewer who reads any token hit as danger will misclassify this direction. It matters beyond one row because it is the ambient-pool defect in miniature: a name resolving by whole-pool uniqueness is one deletion away from binding differently, so its meaning is a function of the corpus denominator rather than of anything written at the declaration or the use. This deletion moves that name from two declarers to one. NOTHING STRUCTURAL GUARANTEES THE NEXT ONE MOVES THAT WAY -- the mechanism that disambiguates here can elsewhere silently rebind a use from one surviving declarer to another. Not created by this change, not closed by it, and visible from here only because an intersection over deletions is one of the few operations that looks straight at it. 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 was referenced Aug 23, 2026
Merged
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.
The obligation
#8896 made the floor able to say what terminally happened to each planned identity — in process. The rows were consumed by a reconciliation refusal and a
passedderivation and then discarded. The schema said a ledger "is published atomically under its final name" with "a footer carrying the row count and a digest over the rows"; no such artifact existed, so that sentence described an intention. This lands it.The seed does not render a byte of it
The seed holds the rows and performs the host write. The bytes come from evaluating
v2.workflow.floor_terminal_ledger_wire— the same shapecli_runalready uses forwire_fnv1a64_content_hash_hexrather than hashing in Rust beside it. The seed's hand-written mirror of the v2 schema is already declared debt at mitigatable; answering it by minting a third copy of the grammar would have been the fix that deepens the defect.One grammar, both directions (§4):
render_*selects a production forward,parse_*selects the same productions backward. A separately-authored reader would be the N×M adapter pair §4 refuses — and undetectable, since two hand-written halves of one grammar agree until the day they do not.The mirror comparator, running in production on every row
Something must cross the boundary: two type systems have to meet. That crossing is irreducible; it being unchecked is not.
cli_runderives a disposition fromClaimOutcome+expected_red.Two independent paths over one row —
(outcome → disposition)and(outcome → tag → disposition)— so the seed sends both, and a row whose answers disagree makes the whole ledger unrenderable, naming the offending identity.Honest scope: this catches divergence in the mappings, not in the two
ClaimDispositiondeclarations, which are still authored beside each other. For what it covers, the seam moves from nothing detects a divergence to a divergence stops the line.Guarded against the obvious trap: two renderers would be a fourth representation, so the seed-facing renderer is asserted byte-identical to the typed one over every terminal shape.
Fail-closed at every arm
.replace(['\t','\n'], " "), publishing a different fact than the one observed)No
parse_inton the footer. The host primitive answersValue::Nullfor text it cannot read, so every interpretation of a damaged count is a fabrication. The expected count is rendered and compared as text — total, no failure arm.Fields extracted by matching, never by casting an Optional.
fields.first() as Stringtype-checks and renders the wrapper, so a field would silently becomePresent { value: … }with no diagnostic.A refusal keeps its rows
A refusal that named one identity and destroyed the file would take with it the only rows that say whether the defect is isolated or spans a whole terminal shape. So
LedgerUnrenderablecarries a diagnosis — every row the sender sent, in the sender's own words, plus a#refusedline naming reason, offending identity, and how many rows follow.A partial file cited as a ledger has no spelling, rather than being forbidden by convention: it opens with a different format token (so
parse_ledgerrefuses it asledger-format-unrecognized), carries no footer, and its rows have five fields rather than four. Fields go in raw — including the separator-carrying field that may have caused the refusal — because a diagnostician needs the byte that broke the grammar; the stated row count is what makes a forged#refusedline detectable without escaping anything.The binding names a commit and an absence
Fnv1a64StructuralDigestHexisString where lower_hex_16, so typing the commit as a structural digest would have refused at construction — the corpus settled this before the question was asked.GitObjectIdis not a new type: it is cited to the upstream authority, enforces family/length/lowercase through validating constructors, andv2.compiler.self_hostfrontier_probe_typesalready bindssource_commit/source_treeto it."local"is not a commit and is not rendered as one. A run with no published commit has no candidate, so its ledger is not candidate-bound andledger_is_candidate_boundanswers from the shape rather than by string-comparing a magic value. An unrecognised snapshot refuses rather than reading as unpublished — that direction loses evidence quietly.Roster identity is derived, not supplied, and is no longer a field: a stored one can disagree with the population it names, and nothing in the floor computes one. Both renderers fold it from the identities being published, which is what makes the byte-equality law load-bearing.
Cost, printed rather than asserted
The context is built after the fold, not held across it.
run_required_floordrops itshermeticframe before the fold under a measured note — 6.58GB → 9.15GB, a runner that throttles atmemory.high, a last run ~1MB under the watermark. Holding a resolved context would pay in memory on a run already at the line, in a shared cgroup where the kernel kills the largest task: non-deterministic, unattributable, and it can land on someone else's work. Paying in time is deterministic and degrades by being slow.Measured out of context, a cold process resolving this entry alone took 93.4s wall / 1.93 GB peak RSS on a contended session container — an upper bound, not the in-context figure, and CI hosts differ. In context the corpus walk is not re-paid: this resolve goes through the shared
MultiEntryIndexthe floor already warms during preparation, precisely so no single claim pays for it. Rather than assert the difference, every run prints:A cost that is stated is a cost someone can decide to remove; a cost that is printed is an instrument.
(A near-miss worth recording: I almost quoted 1.3s from an earlier receipt where that entry was the second in a run whose pool the first had already built — a warm-pool figure wearing a narrow-closure label.)
Verification — by execution, not typecheck
publish_terminal_ledger: real resolve, real interpreter, real bytes, real rename. Includes the discriminating RED — a disposition disagreeing with its tag refuses, and the diagnosis keeps both rows..dagtests, 7/7 schema.dagtests, rosters read from the files rather than grepped for FAIL.cargo fmt --all --checkclean.Two environment defects surfaced by their own refusals rather than by debugging: the grammar's entry was spelled relative to the workspace root and refused for any other CWD (now resolved under the declared roots), and the tests first wrote into a non-ignored
target/beside the crate (now a temp dir, one path per test so four parallel tests cannot read each other's bytes).Dissolution
Same trigger as the rest of the bridge: the self-emitted v2 claim executor. When v2 drives the floor's execution it holds identity and outcome together, renders its own ledger, and
terminal_ledger_publish.rsis deleted whole.Scaffold admission: what authority this rests on, and what it does NOT have
Raised by review 54771, and answered honestly rather than by asserting an approval I do not hold.
src/v1/stage0/src/cli_run/terminal_ledger_publish.rsis a new hand-Rust module in the v1 seed. Its header names its dissolution trigger — when the self-emitted v2 claim executor takes over the floor, this file is deleted whole. A trigger is a lifecycle fact, not a permit (§5, 2026-08-10), so the trigger is not what admits it.What I am relying on: the v1 maintenance standing's admission test, which is PURPOSE rather than shape — a change is admitted when it serves the v2 self-host program (operator ruling 2026-08-20,
gunbc.v1_maintenance_standingv1_seed_standing). This module exists so the seed calls the v2 grammar instead of re-implementing it in Rust: rendering, parsing, and the disposition vocabulary all live inv2.workflow.floor_terminal_ledger_wire, and the Rust here is the host seam that resolves that module and marshals values across. It moves authority toward.dag, not away from it.What I do not have: a per-PR operator verdict naming this specific module. I am not claiming one, and I am not treating the purpose test as a substitute for one where a reviewer or the operator judges that a distinct admission is owed. If that judgement goes the other way, the remedy is a decision, not a rewrite — the module's shape is already the one the trigger describes.
Why the seam cannot currently be zero-Rust: the floor is invoked by the seed binary, and the seed is what holds the terminal rows. Until the claim executor is itself self-emitted, something in Rust has to call into the grammar. What this PR refuses to do is let that something duplicate the grammar — hence the comparator: the seed derives a disposition from
ClaimOutcomedirectly, the module derives one from the emitted tag, and a disagreement refuses the ledger naming the identity rather than publishing a plausible one.