From af7c36851bdf4beb109b5329b547cf0a3ab717c2 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 22 Aug 2026 09:42:11 +0000 Subject: [PATCH 1/5] v2 schema: the floor's terminal evidence, with completeness as an identity 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 --- src/v2/workflow/floor_terminal_ledger.dag | 175 ++++++++++++++++++ .../workflow/floor_terminal_ledger_test.dag | 124 +++++++++++++ 2 files changed, 299 insertions(+) create mode 100644 src/v2/workflow/floor_terminal_ledger.dag create mode 100644 src/v2/workflow/floor_terminal_ledger_test.dag diff --git a/src/v2/workflow/floor_terminal_ledger.dag b/src/v2/workflow/floor_terminal_ledger.dag new file mode 100644 index 00000000000..7244695ff6b --- /dev/null +++ b/src/v2/workflow/floor_terminal_ledger.dag @@ -0,0 +1,175 @@ +module v2.workflow.floor_terminal_ledger + +import v2.std.integer { Int } +import v2.std.logic { Bool } +import v2.std.node { Symbol } +import v2.std.text { String } +import v2.workflow.floor2_prepared_subject { WitnessIdentity, witness_identity_qualified_name } +import v2.workflow.required_floor { ClaimSafetyOutcome } + +// THE FLOOR'S TERMINAL EVIDENCE, OWNED BY v2 AND SERIALIZED BY THE SEED. +// +// The v2 self-host program claims candidate-bound witnesses executed and matched their +// expectations. The seed is the only boundary holding that per-identity fact and it discards the +// passing half before v2 can read it: the accumulation branch increments a counter and drops the +// identity, so a run that reports `passed=10132` cannot say WHICH 10132. This module is the +// schema and the completeness law for the evidence the floor already observes. It invents no +// verdict and reclassifies none. +// +// A PASS LIST IS THE WRONG ARTIFACT AND THIS IS DELIBERATELY NOT ONE. A roster of passing +// identities reproduces one layer up exactly 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, which is the state-space conflation this repository already +// names as a recurring failure. The ledger therefore carries ONE ROW PER PLANNED IDENTITY and +// every row is terminal. Absence is not a value it can express. + +// WHAT A CLAIM'S ATTEMPT ACTUALLY REACHED, at the grain the executor already distinguishes. +// +// These three arms are not a taxonomy invented here. They are the states the floor already +// separates when it runs a claim -- the evaluation returned a value, it stopped with a typed +// diagnostic, or a safety limit interrupted it before either -- and `Interrupted` carries the +// existing `ClaimSafetyOutcome` rather than a second spelling of the same fact. +type ClaimAttemptTerminal + = Returned { observation: ClaimObservation } + | DiagnosedStop { reason: Symbol } + | Interrupted { safety: ClaimSafetyOutcome } + +// AN ATTEMPT THAT RETURNED STILL MAY NOT HAVE OBSERVED ANYTHING. A claim whose result is not a +// verdict the floor can read -- the wrapper refusal a run reports when a function returns a bare +// value instead of a process exit, for instance -- COMPLETED and OBSERVED NOTHING. Collapsing +// that into `holds: False` would be the fabricated plausible output: it would report a failing +// witness where the truth is a witness whose answer was never in a readable shape. +type ClaimObservation + = ObservedVerdict { holds: Bool } + | ObservationUnrepresentable { reason: Symbol } + +// WHAT THE ROSTER EXPECTED OF THIS IDENTITY, which is an input to the projection and never an +// output of it. Held separately from the observation precisely so that "the witness answered +// false" and "the witness was expected to answer false" stay two facts: their conjunction is +// what makes a red held rather than failing, and a single field could not express the pair. +type ClaimExpectation + = ExpectedToHold + | ExpectedRed + +// ONE ROW PER PLANNED IDENTITY, AND THE ORDINAL IS PART OF THE EVIDENCE. The execution ordinal is +// dense over the planned population, so a ledger missing a row has a gap in its ordinals and a +// truncated ledger ends below the planned count -- two independent ways for an incomplete file to +// be visibly incomplete, neither of which depends on the footer surviving. +type ClaimTerminalRow { + identity: WitnessIdentity + ordinal: Int + expectation: ClaimExpectation + terminal: ClaimAttemptTerminal +} + +// `Pass` IS A PROJECTION, NOT A STORED FIELD, AND THAT IS THE WHOLE CONSTRUCTION. +// +// There is no `passed: Bool` anywhere in the row, so a row cannot disagree with its own +// disposition -- the disagreement has no constructor. The seed's `ClaimOutcome::Pass => +// outcome.passed += 1` is an INDEPENDENT AUTHORITY over the same fact, and two authorities over +// one fact is the defect this dissolves: the counter is derived from the finalized rows, so a +// counter that disagrees with the ledger is unrepresentable rather than detected by a +// cross-check. +type ClaimDisposition + = Passed + | Failed + | KnownRedHeld + | KnownRedNowPassing + | RefusedBeforeVerdict + | InterruptedBeforeVerdict + +fn claim_disposition(row: ClaimTerminalRow) -> ClaimDisposition { + match row.terminal { + Interrupted { safety: _ } => InterruptedBeforeVerdict + DiagnosedStop { reason: _ } => RefusedBeforeVerdict + Returned { observation: o } => + match o { + ObservationUnrepresentable { reason: _ } => RefusedBeforeVerdict + ObservedVerdict { holds: h } => + match row.expectation { + ExpectedToHold => if h { Passed } else { Failed } + ExpectedRed => if h { KnownRedNowPassing } else { KnownRedHeld } + } + } + } +} + +// COMPLETENESS IS AN IDENTITY JOIN, NEVER A COUNT EQUALITY, AND HERE IS THE CASE THAT PROVES IT. +// +// Suppose one planned identity never reaches the ledger and some other identity is written twice. +// `planned == terminal_rows` holds. `passed + failed + held == planned` holds. Every aggregate +// count in the run summary is IDENTICAL to a correct run. A count-based check is green, and the +// missing witness -- possibly the one the author just added -- is reported as covered. +// +// So the reconciliation below computes THREE INDEPENDENT SETS by joining on identity, and it is a +// RECORD rather than a coproduct on purpose: a coproduct would report the first defect it found +// and hide the second, and this failure mode is exactly the one where two defects appear together +// and cancel in the totals. Completeness is all three being empty, which the swap above fails in +// two places at once while no count moves. +type LedgerReconciliation { + planned_without_terminal: List + terminal_without_planned: List + terminal_duplicated: List +} + +fn ledger_is_complete(r: LedgerReconciliation) -> Bool { + r.planned_without_terminal.length() == 0 + && r.terminal_without_planned.length() == 0 + && r.terminal_duplicated.length() == 0 +} + +// A ROUTED IDENTITY WITH NO TERMINAL ROW IS INCOMPLETE, NEVER GREEN, and a terminal row for an +// identity nobody planned is FOREIGN EXECUTION and is refused. The two are separate arms because +// their remedies differ: the first says the fold lost a claim, the second says something executed +// that the roster never admitted, and collapsing them would let a lost claim be explained away as +// a stray one. + +// PUBLICATION IS PART OF THE EVIDENCE, SO ITS FAILURE MUST BE PART OF THE VERDICT. +// +// A ledger is finalized only after the fold completes: the footer carries the row count and a +// digest over the rows, and the file is published atomically under its final name. A run killed +// before finalization therefore leaves either no ledger or one that is VISIBLY partial -- it never +// leaves a complete-looking file that is short. +// +// `LedgerPartial` is not a degraded success. Witnesses all passing plus a failed ledger write is +// EVIDENCE INCOMPLETE, and evidence incomplete is not green: otherwise the instrumentation is +// optional exactly when it fails, which is the failure arm that widens instead of refusing. +type LedgerPublication + = LedgerFinalized { row_count: Int, digest: String } + | LedgerPartial { reason: Symbol } + +// GREEN ADMISSION IS A TYPED OUTCOME, NOT A Bool, because a Bool cannot say WHY evidence was +// refused and the three reasons have three different remedies: the fold lost rows, something +// executed that was never planned, or the run died before the ledger was finalized. Returning +// `False` for all three would be the state-space conflation this schema exists to remove -- one +// silence standing for several states -- committed by the very function that judges completeness. +// +// THE FOOTER'S COUNT IS CHECKED AGAINST THE PLANNED POPULATION, not against the rows the reader +// happened to parse. Comparing the footer to the rows read would be an identity: a truncation that +// removed rows AND rewrote the footer to match would agree with itself. The planned population is +// the independent referent, and it is the one the caller already holds. +type LedgerGreenAdmission + = EvidenceComplete + | EvidenceUnfinalized { reason: Symbol } + | EvidenceReconciliationFailed { reconciliation: LedgerReconciliation } + | EvidenceFooterCountDisagrees { footer_rows: Int, planned_rows: Int } + +fn ledger_green_admission( + publication: LedgerPublication, + reconciliation: LedgerReconciliation, + planned: List, +) -> LedgerGreenAdmission { + match publication { + LedgerPartial { reason: r } => EvidenceUnfinalized { reason: r } + LedgerFinalized { row_count: n, digest: _ } => + if ledger_is_complete(r: reconciliation) { + if n == planned.length() { + EvidenceComplete + } else { + EvidenceFooterCountDisagrees { footer_rows: n, planned_rows: planned.length() } + } + } else { + EvidenceReconciliationFailed { reconciliation: reconciliation } + } + } +} diff --git a/src/v2/workflow/floor_terminal_ledger_test.dag b/src/v2/workflow/floor_terminal_ledger_test.dag new file mode 100644 index 00000000000..0e2df14ba96 --- /dev/null +++ b/src/v2/workflow/floor_terminal_ledger_test.dag @@ -0,0 +1,124 @@ +module v2.workflow.floor_terminal_ledger_test + +import v2.std.logic { Bool } +import v2.workflow.floor2_prepared_subject { WitnessIdentity } +import v2.workflow.floor_terminal_ledger { + ClaimExpectation, + ClaimTerminalRow, + ExpectedRed, + ExpectedToHold, + Failed, + Interrupted, + InterruptedBeforeVerdict, + KnownRedHeld, + KnownRedNowPassing, + LedgerFinalized, + LedgerPartial, + LedgerReconciliation, + EvidenceComplete, + EvidenceFooterCountDisagrees, + EvidenceReconciliationFailed, + EvidenceUnfinalized, + ObservationUnrepresentable, + ObservedVerdict, + Passed, + RefusedBeforeVerdict, + Returned, + claim_disposition, + ledger_is_complete, + ledger_green_admission +} + +fn ident(f: String) -> WitnessIdentity { + WitnessIdentity { module_path: "test.claim.example", function: f } +} + +fn row(f: String, expectation: ClaimExpectation, holds: Bool) -> ClaimTerminalRow { + ClaimTerminalRow { + identity: ident(f: f), + ordinal: 0, + expectation: expectation, + terminal: Returned { observation: ObservedVerdict { holds: holds } } + } +} + +fn empty_reconciliation() -> LedgerReconciliation { + LedgerReconciliation { + planned_without_terminal: [], + terminal_without_planned: [], + terminal_duplicated: [] + } +} + +// THE PROJECTION IS TOTAL OVER (expectation x observation), and each of the four cells is asserted +// to a DISTINCT disposition rather than to a Bool. A Boolean assertion here would pass for three +// different wrong mappings; naming the constructor each cell must produce is what makes the test +// able to fail for the right reason. +test fn the_four_verdict_cells_project_to_four_distinct_dispositions() -> Bool { + claim_disposition(row: row(f: "a", expectation: ExpectedToHold, holds: 0 == 0)) == Passed + && claim_disposition(row: row(f: "b", expectation: ExpectedToHold, holds: 0 == 1)) == Failed + && claim_disposition(row: row(f: "c", expectation: ExpectedRed, holds: 0 == 1)) == KnownRedHeld + && claim_disposition(row: row(f: "d", expectation: ExpectedRed, holds: 0 == 0)) == KnownRedNowPassing +} + +// AN ATTEMPT THAT RETURNED WITHOUT A READABLE VERDICT IS NOT A FAILING WITNESS. Collapsing +// `ObservationUnrepresentable` into `Failed` is the fabricated plausible output -- it reports a +// witness that answered wrongly where the truth is a witness whose answer was never in a shape the +// floor could read, and the two have different remedies. +test fn an_unreadable_observation_is_refused_not_failed() -> Bool { + claim_disposition(row: ClaimTerminalRow { + identity: ident(f: "e"), + ordinal: 0, + expectation: ExpectedToHold, + terminal: Returned { observation: ObservationUnrepresentable { reason: "not-a-process-exit" } } + }) == RefusedBeforeVerdict +} + +// THE LOAD-BEARING TEST: A DUPLICATE REPLACING AN OMISSION, WITH EVERY COUNT UNCHANGED. +// +// One planned identity never reached the ledger and another was written twice. Row count equals +// planned count. Every aggregate in the run summary is identical to a correct run. A count-based +// completeness check is GREEN over this, and the missing witness is reported as covered. +// +// This is the discriminating RED for the whole reconciliation: replace the identity join with +// `terminal_rows.length() == planned.length()` and this test goes green while the ledger is wrong. +test fn a_duplicate_replacing_an_omission_is_caught_though_no_count_moves() -> Bool { + let swapped = LedgerReconciliation { + planned_without_terminal: [ident(f: "lost")], + terminal_without_planned: [], + terminal_duplicated: [ident(f: "written_twice")] + } + !ledger_is_complete(r: swapped) + && ledger_is_complete(r: empty_reconciliation()) + && ledger_green_admission( + publication: LedgerFinalized { row_count: 2, digest: "d" }, + reconciliation: swapped, + planned: [ident(f: "lost"), ident(f: "written_twice")] + ) == EvidenceReconciliationFailed { reconciliation: swapped } +} + +// A FAILED PUBLICATION IS NOT GREEN EVEN WHEN EVERY WITNESS PASSED. Otherwise the instrumentation +// is optional exactly when it fails, which is the failure arm that widens instead of refusing. +test fn a_partial_ledger_is_not_green_over_a_perfect_reconciliation() -> Bool { + ledger_green_admission( + publication: LedgerPartial { reason: "killed-before-finalize" }, + reconciliation: empty_reconciliation(), + planned: [ident(f: "a")] + ) == EvidenceUnfinalized { reason: "killed-before-finalize" } +} + +// THE FOOTER COUNT IS CHECKED AGAINST THE PLANNED POPULATION, not against itself. A truncation +// that dropped rows and rewrote the footer to match would agree with itself; it cannot agree with +// the planned population the caller independently holds. +test fn a_footer_count_below_the_planned_population_is_not_green() -> Bool { + ledger_green_admission( + publication: LedgerFinalized { row_count: 1, digest: "d" }, + reconciliation: empty_reconciliation(), + planned: [ident(f: "a"), ident(f: "b")] + ) == EvidenceFooterCountDisagrees { footer_rows: 1, planned_rows: 2 } + && ledger_green_admission( + publication: LedgerFinalized { row_count: 2, digest: "d" }, + reconciliation: empty_reconciliation(), + planned: [ident(f: "a"), ident(f: "b")] + ) == EvidenceComplete +} From aa0526a6f1701bfbefc5bd7d45e23d95dbb36f58 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 22 Aug 2026 10:03:00 +0000 Subject: [PATCH 2/5] Bind the ledger to its candidate, keep the seed's typed arms, and delete 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 --- src/v2/workflow/floor_terminal_ledger.dag | 81 +++++++++++++++---- .../workflow/floor_terminal_ledger_test.dag | 31 +++++-- 2 files changed, 89 insertions(+), 23 deletions(-) diff --git a/src/v2/workflow/floor_terminal_ledger.dag b/src/v2/workflow/floor_terminal_ledger.dag index 7244695ff6b..dbbb60a7e9c 100644 --- a/src/v2/workflow/floor_terminal_ledger.dag +++ b/src/v2/workflow/floor_terminal_ledger.dag @@ -1,8 +1,9 @@ module v2.workflow.floor_terminal_ledger import v2.std.integer { Int } +import std.content_hash { Fnv1a64Structural } import v2.std.logic { Bool } -import v2.std.node { Symbol } + import v2.std.text { String } import v2.workflow.floor2_prepared_subject { WitnessIdentity, witness_identity_qualified_name } import v2.workflow.required_floor { ClaimSafetyOutcome } @@ -25,14 +26,27 @@ import v2.workflow.required_floor { ClaimSafetyOutcome } // WHAT A CLAIM'S ATTEMPT ACTUALLY REACHED, at the grain the executor already distinguishes. // -// These three arms are not a taxonomy invented here. They are the states the floor already -// separates when it runs a claim -- the evaluation returned a value, it stopped with a typed -// diagnostic, or a safety limit interrupted it before either -- and `Interrupted` carries the -// existing `ClaimSafetyOutcome` rather than a second spelling of the same fact. +// These arms are not a taxonomy invented here: they mirror the arms the seed ALREADY holds +// typed, one for one. `ClaimOutcome` in the seed is Pass | Fail | NotBool { got } | RuntimeError +// { message } | TimedOut { elapsed_ms, budget_ms, kind, completion } | HostToolUnresolved { name, +// probed } | (route gap), and its own comment at that match says why: "Every non-pass arm is +// reported with the fact that distinguishes 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." +// +// AN EARLIER DRAFT COLLAPSED ALL OF THEM INTO `DiagnosedStop { reason: Symbol }`, which is the +// same defect the seed's comment argues against, committed on the way ACROSS the seam rather than +// at the match. A `Symbol` reason is not the raw terminal fact -- it is a rendering of one, and +// the boundary this schema is built for is "v1 preserves the raw terminal fact it already holds". +// Stringing it during transport would have made the ledger strictly less informative than the +// producer, which is the opposite of the obligation. `BudgetRefused` carries the existing +// `ClaimSafetyOutcome` rather than a second spelling of it. type ClaimAttemptTerminal = Returned { observation: ClaimObservation } - | DiagnosedStop { reason: Symbol } - | Interrupted { safety: ClaimSafetyOutcome } + | RuntimeErrored { message: String } + | BudgetRefused { safety: ClaimSafetyOutcome } + | HostToolUnresolved { name: String, probed: List } + | RouteGap { route: String } // AN ATTEMPT THAT RETURNED STILL MAY NOT HAVE OBSERVED ANYTHING. A claim whose result is not a // verdict the floor can read -- the wrapper refusal a run reports when a function returns a bare @@ -51,17 +65,50 @@ type ClaimExpectation = ExpectedToHold | ExpectedRed -// ONE ROW PER PLANNED IDENTITY, AND THE ORDINAL IS PART OF THE EVIDENCE. The execution ordinal is -// dense over the planned population, so a ledger missing a row has a gap in its ordinals and a -// truncated ledger ends below the planned count -- two independent ways for an incomplete file to -// be visibly incomplete, neither of which depends on the footer surviving. +// ONE ROW PER PLANNED IDENTITY, AND EXECUTION ORDER IS THE ROW'S POSITION -- there is no +// `ordinal` field, and its absence is the point. +// +// An earlier draft carried `ordinal: Int` and claimed in this comment that it made a missing row +// visible as a gap and a truncation visible as a short tail. NOTHING IN THE SCHEMA READ IT. That +// is the rung-inflation shape at carrier grain: a field whose asserted property no code performs, +// where the prose is the only place the guarantee exists. +// +// The repair is not to add a contiguity check -- it is to delete the field. Position in a list is +// dense and unique BY CONSTRUCTION, so a duplicated or gapped ordinal has no spelling here rather +// than being caught by a validator. Truncation is still caught, by the footer count against the +// planned population, which is implemented and tested. type ClaimTerminalRow { identity: WitnessIdentity - ordinal: Int expectation: ClaimExpectation terminal: ClaimAttemptTerminal } +// WITHOUT A BINDING THIS IS A LIST OF ROWS, NOT EVIDENCE -- and the header of this module claims +// CANDIDATE-BOUND witnesses. +// +// An earlier draft had no `Ledger` type at all: only rows, reconciliation and publication. A +// ledger produced by run A was then structurally indistinguishable from evidence for run B, and +// the completed claim the obligation names -- "identity W appears exactly once in candidate C's +// terminal population" -- had no C to name. That is not a missing convenience; it is the +// difference between a ledger and evidence, and the artifact's lifecycle is v2's to own. +// +// The binding is a FIELD OF THE LEDGER rather than a sibling artifact, so an unbound ledger is +// unrepresentable rather than merely unusual. Its three identities are content hashes from +// `std.content_hash` `Fnv1a64Structural` -- the structural family member DESIGN names, not a bare +// `String`. A `String` digest admits any text at all and cannot be compared against anything else +// in the corpus that hashes, which is the hollow-carrier shape. +type LedgerBinding { + repository_snapshot: Fnv1a64Structural + prepared_subject: Fnv1a64Structural + roster_identity: Fnv1a64Structural +} + +type TerminalLedger { + binding: LedgerBinding + rows: List + publication: LedgerPublication +} + // `Pass` IS A PROJECTION, NOT A STORED FIELD, AND THAT IS THE WHOLE CONSTRUCTION. // // There is no `passed: Bool` anywhere in the row, so a row cannot disagree with its own @@ -80,8 +127,10 @@ type ClaimDisposition fn claim_disposition(row: ClaimTerminalRow) -> ClaimDisposition { match row.terminal { - Interrupted { safety: _ } => InterruptedBeforeVerdict - DiagnosedStop { reason: _ } => RefusedBeforeVerdict + BudgetRefused { safety: _ } => InterruptedBeforeVerdict + RuntimeErrored { message: _ } => RefusedBeforeVerdict + HostToolUnresolved { name: _, probed: _ } => RefusedBeforeVerdict + RouteGap { route: _ } => RefusedBeforeVerdict Returned { observation: o } => match o { ObservationUnrepresentable { reason: _ } => RefusedBeforeVerdict @@ -155,11 +204,11 @@ type LedgerGreenAdmission | EvidenceFooterCountDisagrees { footer_rows: Int, planned_rows: Int } fn ledger_green_admission( - publication: LedgerPublication, + ledger: TerminalLedger, reconciliation: LedgerReconciliation, planned: List, ) -> LedgerGreenAdmission { - match publication { + match ledger.publication { LedgerPartial { reason: r } => EvidenceUnfinalized { reason: r } LedgerFinalized { row_count: n, digest: _ } => if ledger_is_complete(r: reconciliation) { diff --git a/src/v2/workflow/floor_terminal_ledger_test.dag b/src/v2/workflow/floor_terminal_ledger_test.dag index 0e2df14ba96..ec74090f6f8 100644 --- a/src/v2/workflow/floor_terminal_ledger_test.dag +++ b/src/v2/workflow/floor_terminal_ledger_test.dag @@ -2,19 +2,22 @@ module v2.workflow.floor_terminal_ledger_test import v2.std.logic { Bool } import v2.workflow.floor2_prepared_subject { WitnessIdentity } +import std.content_hash { Fnv1a64Structural, Fnv1a64StructuralDigestHex } import v2.workflow.floor_terminal_ledger { ClaimExpectation, ClaimTerminalRow, ExpectedRed, ExpectedToHold, Failed, - Interrupted, + BudgetRefused, InterruptedBeforeVerdict, KnownRedHeld, KnownRedNowPassing, LedgerFinalized, LedgerPartial, LedgerReconciliation, + LedgerBinding, + TerminalLedger, EvidenceComplete, EvidenceFooterCountDisagrees, EvidenceReconciliationFailed, @@ -36,12 +39,27 @@ fn ident(f: String) -> WitnessIdentity { fn row(f: String, expectation: ClaimExpectation, holds: Bool) -> ClaimTerminalRow { ClaimTerminalRow { identity: ident(f: f), - ordinal: 0, expectation: expectation, terminal: Returned { observation: ObservedVerdict { holds: holds } } } } +fn hash(h: String) -> Fnv1a64Structural { + Fnv1a64Structural { digest: h as Fnv1a64StructuralDigestHex } +} + +fn ledger_with(publication: LedgerPublication) -> TerminalLedger { + TerminalLedger { + binding: LedgerBinding { + repository_snapshot: hash(h: "0123456789abcdef"), + prepared_subject: hash(h: "fedcba9876543210"), + roster_identity: hash(h: "0f1e2d3c4b5a6978") + }, + rows: [], + publication: publication + } +} + fn empty_reconciliation() -> LedgerReconciliation { LedgerReconciliation { planned_without_terminal: [], @@ -68,7 +86,6 @@ test fn the_four_verdict_cells_project_to_four_distinct_dispositions() -> Bool { test fn an_unreadable_observation_is_refused_not_failed() -> Bool { claim_disposition(row: ClaimTerminalRow { identity: ident(f: "e"), - ordinal: 0, expectation: ExpectedToHold, terminal: Returned { observation: ObservationUnrepresentable { reason: "not-a-process-exit" } } }) == RefusedBeforeVerdict @@ -91,7 +108,7 @@ test fn a_duplicate_replacing_an_omission_is_caught_though_no_count_moves() -> B !ledger_is_complete(r: swapped) && ledger_is_complete(r: empty_reconciliation()) && ledger_green_admission( - publication: LedgerFinalized { row_count: 2, digest: "d" }, + ledger: ledger_with(publication: LedgerFinalized { row_count: 2, digest: hash(h: "aaaabbbbccccdddd") }), reconciliation: swapped, planned: [ident(f: "lost"), ident(f: "written_twice")] ) == EvidenceReconciliationFailed { reconciliation: swapped } @@ -101,7 +118,7 @@ test fn a_duplicate_replacing_an_omission_is_caught_though_no_count_moves() -> B // is optional exactly when it fails, which is the failure arm that widens instead of refusing. test fn a_partial_ledger_is_not_green_over_a_perfect_reconciliation() -> Bool { ledger_green_admission( - publication: LedgerPartial { reason: "killed-before-finalize" }, + ledger: ledger_with(publication: LedgerPartial { reason: "killed-before-finalize" }), reconciliation: empty_reconciliation(), planned: [ident(f: "a")] ) == EvidenceUnfinalized { reason: "killed-before-finalize" } @@ -112,12 +129,12 @@ test fn a_partial_ledger_is_not_green_over_a_perfect_reconciliation() -> Bool { // the planned population the caller independently holds. test fn a_footer_count_below_the_planned_population_is_not_green() -> Bool { ledger_green_admission( - publication: LedgerFinalized { row_count: 1, digest: "d" }, + ledger: ledger_with(publication: LedgerFinalized { row_count: 1, digest: hash(h: "aaaabbbbccccdddd") }), reconciliation: empty_reconciliation(), planned: [ident(f: "a"), ident(f: "b")] ) == EvidenceFooterCountDisagrees { footer_rows: 1, planned_rows: 2 } && ledger_green_admission( - publication: LedgerFinalized { row_count: 2, digest: "d" }, + ledger: ledger_with(publication: LedgerFinalized { row_count: 2, digest: hash(h: "aaaabbbbccccdddd") }), reconciliation: empty_reconciliation(), planned: [ident(f: "a"), ident(f: "b")] ) == EvidenceComplete From a17816bdac0d8cbd84449f90ffcc2bdcb36c32c2 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 22 Aug 2026 10:14:45 +0000 Subject: [PATCH 3/5] Restore the unrecorded Symbol import, and stop the disposition re-collapsing 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 --- src/v2/workflow/floor_terminal_ledger.dag | 34 ++++++++++++++----- .../workflow/floor_terminal_ledger_test.dag | 6 ++-- 2 files changed, 29 insertions(+), 11 deletions(-) diff --git a/src/v2/workflow/floor_terminal_ledger.dag b/src/v2/workflow/floor_terminal_ledger.dag index dbbb60a7e9c..fb20fab5fa8 100644 --- a/src/v2/workflow/floor_terminal_ledger.dag +++ b/src/v2/workflow/floor_terminal_ledger.dag @@ -3,7 +3,7 @@ module v2.workflow.floor_terminal_ledger import v2.std.integer { Int } import std.content_hash { Fnv1a64Structural } import v2.std.logic { Bool } - +import v2.std.node { Symbol } import v2.std.text { String } import v2.workflow.floor2_prepared_subject { WitnessIdentity, witness_identity_qualified_name } import v2.workflow.required_floor { ClaimSafetyOutcome } @@ -109,6 +109,21 @@ type TerminalLedger { publication: LedgerPublication } +// THE PROJECTION IS LOSSLESS, AND AN EARLIER DRAFT'S WAS NOT. +// +// That draft sent RuntimeErrored, HostToolUnresolved, RouteGap and ObservationUnrepresentable all +// to one `RefusedBeforeVerdict`. The row had just been un-collapsed for exactly this reason -- a +// budget refusal, a runtime error and a witness that answered false have different remedies -- and +// the disposition re-collapsed them one step later, for the consumer that most needs them apart. +// +// It is not a cosmetic loss. The floor already reports these as SEPARATE COUNTERS +// (`host_tool_unresolved`, `route_gap_unenrolled`, `route_gap_held`, `stale_route_gap`, +// `interrupted_before_verdict`), and the obligation requires those counters to be DERIVED from +// the finalized rows so that a counter disagreeing with the ledger has no constructor. A +// projection that has already merged two counters cannot derive either, so the counters would +// have had to be computed independently -- restoring the dual authority the derivation exists to +// dissolve. One arm per terminal shape keeps every counter derivable. + // `Pass` IS A PROJECTION, NOT A STORED FIELD, AND THAT IS THE WHOLE CONSTRUCTION. // // There is no `passed: Bool` anywhere in the row, so a row cannot disagree with its own @@ -122,18 +137,21 @@ type ClaimDisposition | Failed | KnownRedHeld | KnownRedNowPassing - | RefusedBeforeVerdict - | InterruptedBeforeVerdict + | BudgetRefusedBeforeVerdict + | HostToolUnresolvedBeforeVerdict + | RouteGapBeforeVerdict + | RuntimeErroredBeforeVerdict + | ObservationUnreadableBeforeVerdict fn claim_disposition(row: ClaimTerminalRow) -> ClaimDisposition { match row.terminal { - BudgetRefused { safety: _ } => InterruptedBeforeVerdict - RuntimeErrored { message: _ } => RefusedBeforeVerdict - HostToolUnresolved { name: _, probed: _ } => RefusedBeforeVerdict - RouteGap { route: _ } => RefusedBeforeVerdict + BudgetRefused { safety: _ } => BudgetRefusedBeforeVerdict + RuntimeErrored { message: _ } => RuntimeErroredBeforeVerdict + HostToolUnresolved { name: _, probed: _ } => HostToolUnresolvedBeforeVerdict + RouteGap { route: _ } => RouteGapBeforeVerdict Returned { observation: o } => match o { - ObservationUnrepresentable { reason: _ } => RefusedBeforeVerdict + ObservationUnrepresentable { reason: _ } => ObservationUnreadableBeforeVerdict ObservedVerdict { holds: h } => match row.expectation { ExpectedToHold => if h { Passed } else { Failed } diff --git a/src/v2/workflow/floor_terminal_ledger_test.dag b/src/v2/workflow/floor_terminal_ledger_test.dag index ec74090f6f8..37b8db4a551 100644 --- a/src/v2/workflow/floor_terminal_ledger_test.dag +++ b/src/v2/workflow/floor_terminal_ledger_test.dag @@ -10,7 +10,7 @@ import v2.workflow.floor_terminal_ledger { ExpectedToHold, Failed, BudgetRefused, - InterruptedBeforeVerdict, + BudgetRefusedBeforeVerdict, KnownRedHeld, KnownRedNowPassing, LedgerFinalized, @@ -25,7 +25,7 @@ import v2.workflow.floor_terminal_ledger { ObservationUnrepresentable, ObservedVerdict, Passed, - RefusedBeforeVerdict, + ObservationUnreadableBeforeVerdict, Returned, claim_disposition, ledger_is_complete, @@ -88,7 +88,7 @@ test fn an_unreadable_observation_is_refused_not_failed() -> Bool { identity: ident(f: "e"), expectation: ExpectedToHold, terminal: Returned { observation: ObservationUnrepresentable { reason: "not-a-process-exit" } } - }) == RefusedBeforeVerdict + }) == ObservationUnreadableBeforeVerdict } // THE LOAD-BEARING TEST: A DUPLICATE REPLACING AN OMISSION, WITH EVERY COUNT UNCHANGED. From ec2ad0192120c3176a0da4922505c1366bdb3d03 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 22 Aug 2026 10:35:50 +0000 Subject: [PATCH 4/5] Complete the floor's per-identity terminal evidence in the seed, and 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 --- src/v1/stage0/src/cli_run.rs | 291 ++++++++++++++++++++++++++++++++++- 1 file changed, 290 insertions(+), 1 deletion(-) diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index 8734328034f..3b3e87f675f 100644 --- a/src/v1/stage0/src/cli_run.rs +++ b/src/v1/stage0/src/cli_run.rs @@ -16332,6 +16332,103 @@ fn hermetic_effect_ground_verdict( } } +/// The completeness reconciliation, as ONE authority. +/// +/// It is a free function rather than inline in the fold because the test that proves it must +/// call THE PRODUCTION CODE. An earlier draft of that test carried its own copy of this loop: +/// it passed, and it would have kept passing while production drifted arbitrarily far from it — +/// a control sharing nothing with its subject except a name. Extracting it costs nothing and is +/// the difference between a test of the reconciliation and a test of a paraphrase of it. +/// +/// Returns (planned-without-terminal, terminal-without-planned, terminal-duplicated). Three sets +/// rather than a first-failure verdict: an omission and a duplicate arrive together and cancel +/// in every count, so reporting only the first found would hide the half that explains it. +pub fn reconcile_terminal_ledger<'a>( + planned: &'a HashSet, + rows: &'a [ClaimTerminalRow], +) -> (Vec<&'a str>, Vec<&'a str>, Vec<&'a str>) { + let mut seen: HashMap<&str, usize> = HashMap::new(); + for row in rows { + *seen.entry(row.qualified.as_str()).or_insert(0) += 1; + } + let mut missing: Vec<&str> = planned + .iter() + .map(|q| q.as_str()) + .filter(|q| !seen.contains_key(q)) + .collect(); + let mut foreign: Vec<&str> = seen + .keys() + .filter(|q| !planned.contains(**q)) + .copied() + .collect(); + let mut duplicated: Vec<&str> = seen + .iter() + .filter(|(_, n)| **n > 1) + .map(|(q, _)| *q) + .collect(); + missing.sort_unstable(); + foreign.sort_unstable(); + duplicated.sort_unstable(); + (missing, foreign, duplicated) +} + +/// One terminal row per PLANNED identity, mirroring `v2.workflow.floor_terminal_ledger` +/// `ClaimTerminalRow`. v2 owns the evidence schema, its completeness law and the artifact's +/// lifecycle; this side preserves the raw terminal fact it already holds and serializes it. +/// +/// WHY THE SEAM EXISTS, and it is not that the change is small. The v2 self-host program +/// declares a per-identity completed-evidence obligation, and this process is the ONLY producer +/// that holds a witness identity and its terminal outcome at the same moment. It destroys the +/// identity at accumulation — `ClaimOutcome::Pass => outcome.passed += 1` keeps the count and +/// drops the name — so the obligation is not realizable without a bridge here. Nothing about the +/// diff's size bears on that: a zero-cost change with no v2 consumer would stay refused, and this +/// one is admitted because a consumer lands with it. +/// +/// It deliberately acquires NOTHING ELSE. 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; this side hands over facts, not identity semantics. +pub struct ClaimTerminalRow { + pub qualified: String, + pub expected_red: bool, + pub outcome: ClaimOutcome, +} + +/// The lossless projection. One arm per terminal shape, so every counter the floor reports stays +/// derivable from the rows — a projection that merged two of them could derive neither, and the +/// counters would need a second authority, which is what this bridge exists to dissolve. +#[derive(Debug, PartialEq, Eq, Clone, Copy)] +pub enum ClaimDisposition { + Passed, + Failed, + KnownRedHeld, + KnownRedNowPassing, + BudgetRefusedBeforeVerdict, + HostToolUnresolvedBeforeVerdict, + RouteGapBeforeVerdict, + RuntimeErroredBeforeVerdict, + ObservationUnreadableBeforeVerdict, +} + +pub fn claim_disposition(row: &ClaimTerminalRow) -> ClaimDisposition { + match (&row.outcome, row.expected_red) { + (ClaimOutcome::Pass, false) => ClaimDisposition::Passed, + (ClaimOutcome::Pass, true) => ClaimDisposition::KnownRedNowPassing, + (ClaimOutcome::Fail, false) => ClaimDisposition::Failed, + (ClaimOutcome::Fail, true) => ClaimDisposition::KnownRedHeld, + (ClaimOutcome::NotBool { .. }, true) => ClaimDisposition::KnownRedHeld, + (ClaimOutcome::RuntimeError { .. }, true) => ClaimDisposition::KnownRedHeld, + (ClaimOutcome::NotBool { .. }, false) => { + ClaimDisposition::ObservationUnreadableBeforeVerdict + } + (ClaimOutcome::RuntimeError { .. }, false) => ClaimDisposition::RuntimeErroredBeforeVerdict, + (ClaimOutcome::TimedOut { .. }, _) => ClaimDisposition::BudgetRefusedBeforeVerdict, + (ClaimOutcome::HostToolUnresolved { .. }, _) => { + ClaimDisposition::HostToolUnresolvedBeforeVerdict + } + (ClaimOutcome::HostEffectRefused { .. }, _) => ClaimDisposition::RouteGapBeforeVerdict, + } +} + fn expected_red_arm(outcome: &ClaimOutcome) -> ExpectedRedArm { match outcome { ClaimOutcome::Pass => ExpectedRedArm::NowPassing, @@ -41353,6 +41450,7 @@ pub fn run_required_floor( let mut scope_constructions: usize = 0; let mut scope_module_total: usize = 0; let mut scope_module_max: usize = 0; + let mut terminal_rows: Vec = Vec::new(); let mut known_red_held: usize = 0; let mut known_red_now_passing: usize = 0; let mut known_red_budget_refused: usize = 0; @@ -41555,6 +41653,15 @@ pub fn run_required_floor( ); } } + // ONE ROW PER PLANNED IDENTITY, MINTED HERE BECAUSE THIS IS THE ONLY POINT BEFORE THE + // BRANCHING. Every expected-red arm below `continue`s, and the ordinary match below has + // its own arms; minting in either place would silently omit whichever population took + // the other path, and an omission is exactly what this ledger exists to make visible. + terminal_rows.push(ClaimTerminalRow { + qualified: claim.qualified.clone(), + expected_red, + outcome: result.clone(), + }); let passed = matches!(result, ClaimOutcome::Pass); if expected_red { // ONE DISPATCH. Every arm does its own work here rather than classifying once and @@ -41706,7 +41813,12 @@ pub fn run_required_floor( } } match result { - ClaimOutcome::Pass => outcome.passed += 1, + // `outcome.passed += 1` USED TO LIVE HERE AND IS DELETED, not left beside the + // derivation. Two authorities over one fact is what this change removes; keeping the + // counter here "as a cross-check" would preserve exactly the disagreement the + // derivation makes unrepresentable. `passed` is now counted from the terminal rows + // after the fold. + ClaimOutcome::Pass => {} ClaimOutcome::Fail => outcome .failures .push(format!("{} returned Bool(false)", claim.qualified)), @@ -42022,6 +42134,41 @@ pub fn run_required_floor( outcome.claims_planned, outcome.claims_executed, outcome.receipt_identities )); } + // THE CONSUMER. Reconciliation is an IDENTITY JOIN, and the counts above cannot replace it. + // + // The check immediately preceding this one compares three COUNTS, and it is the reason this + // one is not redundant: a ledger that omits one identity and duplicates another satisfies + // every count in the run — planned == executed == receipted, and `passed` unchanged — while + // the identity population is short by one. `ClaimIdentityCountsDisagree` is green over that. + // Completeness is an identity join, not a count equality. + // + // Three sets, computed independently and reported together rather than as a coproduct: the + // omission-plus-duplicate case fails in TWO of them at once, and an arm that reported only + // the first would hide the second — which is precisely the pair that cancels in the totals. + { + let (planned_without_terminal, terminal_without_planned, terminal_duplicated) = + reconcile_terminal_ledger(&planned_identities, &terminal_rows); + if !planned_without_terminal.is_empty() + || !terminal_without_planned.is_empty() + || !terminal_duplicated.is_empty() + { + return Err(format!( + "REQUIRED-FLOOR REFUSAL cause=TerminalLedgerIncomplete \ + planned_without_terminal={:?} terminal_without_planned={:?} \ + terminal_duplicated={:?} — every planned identity must appear exactly once in \ + the terminal population; counts agreeing does not establish this, because an \ + omission and a duplicate cancel in every total", + planned_without_terminal, terminal_without_planned, terminal_duplicated + )); + } + } + // `passed` IS DERIVED FROM THE ROWS, and the branch that used to increment it is deleted + // rather than kept as a cross-check. A cross-check would preserve the disagreement this + // derivation makes unrepresentable. + outcome.passed = terminal_rows + .iter() + .filter(|row| claim_disposition(row) == ClaimDisposition::Passed) + .count(); if let Some(join) = roster_join_report { let join = crate::v1_compiler_expected_red_roster_join::finalize_not_observed(join); emit_expected_red_roster_join_summary(&join); @@ -42502,3 +42649,145 @@ pub use required_regen_host::emitted_generated_sources; pub fn extract_module_path_public(content: &str) -> Option { extract_module_path(content) } + +#[cfg(test)] +mod terminal_ledger_completeness_law { + //! THE ONE TEST THAT DECIDES WHETHER THIS BRIDGE IS WORTH ANYTHING. + //! + //! A ledger that OMITS one identity and DUPLICATES another has the same row count as a + //! correct one, the same `passed`, and the same planned/executed/receipted triple. Every + //! aggregate in the run is byte-identical to a healthy run. If completeness is checked by + //! counting, that ledger is green and the missing witness — possibly the one the author just + //! added — reports as covered. + //! + //! These tests exercise the reconciliation as a pure function of the row population, and the + //! calibration pair is the point: the swap must be caught while every count stays equal. + + use super::*; + + fn row(qualified: &str, expected_red: bool, outcome: ClaimOutcome) -> ClaimTerminalRow { + ClaimTerminalRow { + qualified: qualified.to_string(), + expected_red, + outcome, + } + } + + /// Calls THE PRODUCTION reconciliation. Not a paraphrase of it: a control that shares only + /// a name with its subject cannot see the subject drift. + fn reconcile<'a>( + planned: &[&str], + rows: &'a [ClaimTerminalRow], + ) -> (Vec<&'a str>, Vec<&'a str>, Vec<&'a str>) { + let owned: HashSet = planned.iter().map(|q| q.to_string()).collect(); + let (m, f, d) = reconcile_terminal_ledger(&owned, rows); + ( + m.into_iter().map(|s| leak(s)).collect(), + f.into_iter().map(|s| leak(s)).collect(), + d.into_iter().map(|s| leak(s)).collect(), + ) + } + + fn leak(s: &str) -> &'static str { + Box::leak(s.to_string().into_boxed_str()) + } + + #[test] + fn a_duplicate_replacing_an_omission_is_caught_while_every_count_stays_equal() { + let planned = ["m.a", "m.b", "m.c"]; + let healthy = vec![ + row("m.a", false, ClaimOutcome::Pass), + row("m.b", false, ClaimOutcome::Pass), + row("m.c", false, ClaimOutcome::Pass), + ]; + // `m.c` never reached the ledger; `m.a` was written twice. + let swapped = vec![ + row("m.a", false, ClaimOutcome::Pass), + row("m.b", false, ClaimOutcome::Pass), + row("m.a", false, ClaimOutcome::Pass), + ]; + + // EVERY COUNT IS EQUAL. This is the whole point of the test: the numbers cannot tell + // these apart, so anything that only counts is green over the broken one. + assert_eq!(healthy.len(), swapped.len()); + let passed_of = |rows: &[ClaimTerminalRow]| { + rows.iter() + .filter(|r| claim_disposition(r) == ClaimDisposition::Passed) + .count() + }; + assert_eq!(passed_of(&healthy), passed_of(&swapped)); + assert_eq!(passed_of(&swapped), planned.len()); + + let (missing, foreign, duplicated) = reconcile(&planned, &healthy); + assert!(missing.is_empty() && foreign.is_empty() && duplicated.is_empty()); + + let (missing, foreign, duplicated) = reconcile(&planned, &swapped); + assert_eq!(missing, vec!["m.c"], "the omitted identity must be named"); + assert!(foreign.is_empty()); + assert_eq!( + duplicated, + vec!["m.a"], + "the duplicated identity must be named" + ); + } + + #[test] + fn a_terminal_row_for_an_unplanned_identity_is_foreign_execution() { + let planned = ["m.a"]; + let rows = vec![ + row("m.a", false, ClaimOutcome::Pass), + row("m.stray", false, ClaimOutcome::Pass), + ]; + let (missing, foreign, duplicated) = reconcile(&planned, &rows); + assert!(missing.is_empty()); + assert_eq!(foreign, vec!["m.stray"]); + assert!(duplicated.is_empty()); + } + + /// The projection must not merge arms the floor reports as separate counters. A collapsed + /// projection could not derive `host_tool_unresolved` or the route-gap counters at all. + #[test] + fn every_terminal_shape_projects_to_its_own_disposition() { + use ClaimDisposition::*; + let cases = [ + (ClaimOutcome::Pass, false, Passed), + (ClaimOutcome::Pass, true, KnownRedNowPassing), + (ClaimOutcome::Fail, false, Failed), + (ClaimOutcome::Fail, true, KnownRedHeld), + ( + ClaimOutcome::RuntimeError { + message: "boom".into(), + }, + false, + RuntimeErroredBeforeVerdict, + ), + ( + ClaimOutcome::NotBool { got: "unit".into() }, + false, + ObservationUnreadableBeforeVerdict, + ), + ( + ClaimOutcome::HostToolUnresolved { + name: "rustfmt".into(), + probed: vec![], + }, + false, + HostToolUnresolvedBeforeVerdict, + ), + ]; + let mut produced: Vec = Vec::new(); + for (outcome, red, want) in cases { + let got = claim_disposition(&row("m.x", red, outcome)); + assert_eq!(got, want); + produced.push(got); + } + // A projection that merged two of these would show up here as a repeat. + let mut deduped = produced.clone(); + deduped.dedup(); + assert_eq!( + deduped.len(), + produced.len(), + "two terminal shapes projected onto the same disposition" + ); + } +} From 9751288eff2e4acf851654d9803ec0b15b2e47f3 Mon Sep 17 00:00:00 2001 From: gunbc-ci-auto-heal Date: Sat, 22 Aug 2026 10:52:57 +0000 Subject: [PATCH 5/5] Declare the bridge's dissolution trigger and the unchecked seed mirror, 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 --- src/v1/stage0/src/cli_run.rs | 29 ++++++++++++++++++- src/v2/workflow/floor_terminal_ledger.dag | 17 ++++++++++- .../workflow/floor_terminal_ledger_test.dag | 21 ++++++++++++++ 3 files changed, 65 insertions(+), 2 deletions(-) diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index 3b3e87f675f..e9c28b3da57 100644 --- a/src/v1/stage0/src/cli_run.rs +++ b/src/v1/stage0/src/cli_run.rs @@ -16374,7 +16374,10 @@ pub fn reconcile_terminal_ledger<'a>( /// One terminal row per PLANNED identity, mirroring `v2.workflow.floor_terminal_ledger` /// `ClaimTerminalRow`. v2 owns the evidence schema, its completeness law and the artifact's -/// lifecycle; this side preserves the raw terminal fact it already holds and serializes it. +/// lifecycle; this side preserves the raw terminal fact it already holds. It does NOT yet +/// serialize the ledger to that artifact — binding, footer and atomic publish are v2's and are +/// not in this change; the rows are consumed in-process only, by the reconciliation refusal +/// below and by the `passed` derivation. /// /// WHY THE SEAM EXISTS, and it is not that the change is small. The v2 self-host program /// declares a per-identity completed-evidence obligation, and this process is the ONLY producer @@ -16387,6 +16390,30 @@ pub fn reconcile_terminal_ledger<'a>( /// It deliberately acquires NOTHING ELSE. 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; this side hands over facts, not identity semantics. +/// +/// THIS TYPE IS A SECOND REPRESENTATION AND NOTHING CHECKS ITS AGREEMENT WITH THE FIRST. +/// Stated rather than left silent, because the doc line above says "mirroring" and a reader +/// could take that to mean the `.dag` schema is an authority this Rust derives from. It is not. +/// `cli_run.rs` is HAND_MAINTAINED, so this struct and `ClaimDisposition` are hand-written beside +/// a hand-written `v2.workflow.floor_terminal_ledger`, and the two share ONLY NAMES. Regen does +/// not compare them — this file is not generated. The witnesses do not compare them — they +/// exercise each side separately, never one against the other. So an arm added, renamed or +/// re-meaned on either side leaves the other silently stale, and the seam is exactly the shape +/// this change repaired one grain down: `reconcile_terminal_ledger` was extracted so its test +/// could not be a control that shares only a name with its subject. That rule condemns this seam +/// too, and here it is declared debt rather than repaired. +/// +/// Rung: *mitigatable* — the divergence is not prevented, not detected, and is currently held +/// only by an author's diligence. No lens is built for it: the cheapest honest check is a v2-side +/// reading of the seed's emitted ledger, which cannot exist before serialization does, so it +/// belongs to that change rather than to a mechanism minted beside this one. +/// +/// DISSOLUTION CONDITION, for this bridge and for the mirror above, one event for both: the +/// self-emitted v2 claim executor. When the floor's execution is driven by v2 rather than by this +/// seed, the producer that holds identity-and-outcome together IS the v2 side, so there is no +/// seam to bridge and no second representation to keep in agreement — this struct, +/// `claim_disposition`, `reconcile_terminal_ledger` and the refusal below are deleted whole, and +/// `v2.workflow.floor_terminal_ledger` is left as the sole authority it already claims to be. pub struct ClaimTerminalRow { pub qualified: String, pub expected_red: bool, diff --git a/src/v2/workflow/floor_terminal_ledger.dag b/src/v2/workflow/floor_terminal_ledger.dag index fb20fab5fa8..55c70142595 100644 --- a/src/v2/workflow/floor_terminal_ledger.dag +++ b/src/v2/workflow/floor_terminal_ledger.dag @@ -8,7 +8,7 @@ import v2.std.text { String } import v2.workflow.floor2_prepared_subject { WitnessIdentity, witness_identity_qualified_name } import v2.workflow.required_floor { ClaimSafetyOutcome } -// THE FLOOR'S TERMINAL EVIDENCE, OWNED BY v2 AND SERIALIZED BY THE SEED. +// THE FLOOR'S TERMINAL EVIDENCE, OWNED BY v2, TO BE SERIALIZED BY THE SEED. // // The v2 self-host program claims candidate-bound witnesses executed and matched their // expectations. The seed is the only boundary holding that per-identity fact and it discards the @@ -23,6 +23,21 @@ import v2.workflow.required_floor { ClaimSafetyOutcome } // -- five states behind one silence, which is the state-space conflation this repository already // names as a recurring failure. The ledger therefore carries ONE ROW PER PLANNED IDENTITY and // every row is terminal. Absence is not a value it can express. +// +// THE SEED CARRIES A HAND-WRITTEN MIRROR OF THIS SCHEMA AND NOTHING CHECKS THE TWO AGREE. +// `cli_run.rs` is HAND_MAINTAINED, so its `ClaimTerminalRow`, `ClaimDisposition` and +// `reconcile_terminal_ledger` are authored beside these declarations rather than derived from +// them. Regen does not compare them, because that file is not generated; the witnesses do not +// compare them, because each side is exercised alone. The claim "one for one" below is therefore +// an author's claim, held by diligence -- *mitigatable* -- and an arm added or re-meaned on +// either side leaves the other silently stale. Declared here rather than left to be inferred +// from the word "mirror", which reads as derivation and is not. +// +// DISSOLUTION -- one event retires the mirror and the seam together: the self-emitted v2 claim +// executor. Once v2 drives the floor's execution, the producer holding identity-and-outcome +// together is v2 itself, the seed's copy is deleted whole, and this module is the sole authority +// it already claims to be. Until then the duplication is admitted debt with a named terminal, +// not an unremarked second representation. // WHAT A CLAIM'S ATTEMPT ACTUALLY REACHED, at the grain the executor already distinguishes. // diff --git a/src/v2/workflow/floor_terminal_ledger_test.dag b/src/v2/workflow/floor_terminal_ledger_test.dag index 37b8db4a551..444d12d575a 100644 --- a/src/v2/workflow/floor_terminal_ledger_test.dag +++ b/src/v2/workflow/floor_terminal_ledger_test.dag @@ -2,6 +2,7 @@ module v2.workflow.floor_terminal_ledger_test import v2.std.logic { Bool } import v2.workflow.floor2_prepared_subject { WitnessIdentity } +import v2.workflow.required_floor { SafetyInterrupted } import std.content_hash { Fnv1a64Structural, Fnv1a64StructuralDigestHex } import v2.workflow.floor_terminal_ledger { ClaimExpectation, @@ -15,6 +16,7 @@ import v2.workflow.floor_terminal_ledger { KnownRedNowPassing, LedgerFinalized, LedgerPartial, + LedgerPublication, LedgerReconciliation, LedgerBinding, TerminalLedger, @@ -91,6 +93,25 @@ test fn an_unreadable_observation_is_refused_not_failed() -> Bool { }) == ObservationUnreadableBeforeVerdict } +// A CLAIM REFUSED BEFORE ANY VERDICT EXISTED IS NOT A FAILING CLAIM EITHER, and this arm is +// separate from the unreadable-observation one above because their remedies differ: an +// unreadable observation is a witness to repair, a budget refusal is a cost to pay or a limit to +// raise. Collapsing them would leave `budget_refused` underivable from the rows, which is the +// counter dual-authority this whole change exists to remove. +test fn a_budget_refusal_is_a_pre_verdict_disposition_not_a_failure() -> Bool { + claim_disposition(row: ClaimTerminalRow { + identity: ident(f: "f"), + expectation: ExpectedToHold, + terminal: BudgetRefused { + safety: SafetyInterrupted { + raised_by: "wall", + elapsed_cpu_at_least: 0, + elapsed_wall_at_least: 0 + } + } + }) == BudgetRefusedBeforeVerdict +} + // THE LOAD-BEARING TEST: A DUPLICATE REPLACING AN OMISSION, WITH EVERY COUNT UNCHANGED. // // One planned identity never reached the ledger and another was written twice. Row count equals