diff --git a/dag/gunbc/floor_component_receipt.dag b/dag/gunbc/floor_component_receipt.dag index 51124de6071..9412588f96d 100644 --- a/dag/gunbc/floor_component_receipt.dag +++ b/dag/gunbc/floor_component_receipt.dag @@ -69,7 +69,7 @@ data floor_component_receipt_note: String = "The floor's per-COMPONENT receipt, data floor_component_receipt_role_note: String = "Components are identified by STRUCTURAL ROLE, never by batch index. Indices are not stable: gunbc_falsifier_batches composes conditionally on enrollment flags (falsifier_self_host_wet_batch_enrolled and siblings), so one flag flip shifts every later index — which is why the silent-pick gate reports as batch 4 today while sitting fifth in source order. An alert keyed on 'batch 1' would relocate the hardcoded assumption rather than remove it. The affected-set cold control is instead identified by the property that DEFINES it: node_frontier_selection = SelectionPredictOnly, reusing the std.realization_schedule authority (the per-PR corpus counterpart is SelectionApplied). Ambiguity fails closed: zero predict-only components yields ControlAbsent and two or more yields ControlAmbiguous, never a guess." -data floor_component_receipt_timed_out_frontier_note: String = "TimedOut is MODELLED and PROJECTED here but the floor does not yet emit it, and that gap is declared rather than papered over. A whole-receipt wall-budget kill carries its numbers structurally at the point it is raised — v1_interpreter InterpError::WitnessWallBudgetExceeded { elapsed_ms, budget_ms } — but ClaimOutcome::RuntimeError flattens them to a formatted String before the walk sees them, so the executor cannot fill TimedOut's budget and elapsed without re-parsing its own prose. It therefore emits Refused with the interpreter's own located diagnostic, which is not a downgrade: a kill at a declared ceiling IS the deliberate, located stop that observation_refused_distinct_note defines Refused to mean. Fabricating 0 for budget and elapsed to reach the more specific arm would be the fabricated-plausible-output DESIGN section 5 forbids. Dissolve-on: ClaimOutcome carries the typed WitnessWallBudgetExceeded pair through to ClaimResult, at which point the budget arm becomes TimedOut and this note deletes. The projection side needs no change then — floor_component_outcome_of_tag already admits the tag and floor_component_outcome_members already renders the fields, proven by execution today. The arm now also names its CLOCK (std.measure ClockBasis, operator ruling 2026-08-05), and the wall-budget kill this note is about is exactly why: a whole-receipt wall ceiling and the fast-lane thread-CPU fail-stop both surface as TimedOut, so the clock is what tells them apart. floor_component_outcome_of_tag takes the basis as a parameter rather than assuming one, because the tag alone has never carried it." +data floor_component_receipt_timed_out_frontier_note: String = "TimedOut is MODELLED and PROJECTED here but the floor does not yet emit it, and that gap is declared rather than papered over. A whole-receipt wall-budget kill carries its numbers structurally at the point it is raised — v1_interpreter InterpError::WitnessWallBudgetExceeded { elapsed_ms, budget_ms } — but ClaimOutcome::RuntimeError flattens them to a formatted String before the walk sees them, so the executor cannot fill TimedOut's budget and elapsed without re-parsing its own prose. It therefore emits Refused with the interpreter's own located diagnostic, which is not a downgrade: a kill at a declared ceiling IS the deliberate, located stop that observation_refused_distinct_note defines Refused to mean. Fabricating 0 for budget and elapsed to reach the more specific arm would be the fabricated-plausible-output DESIGN section 5 forbids. Dissolve-on: ClaimOutcome carries the typed WitnessWallBudgetExceeded pair through to ClaimResult, at which point the budget arm becomes TimedOut and this note deletes. THAT TRIGGER HAS FIRED (2026-08-18): the seed no longer flattens a raised budget refusal into RuntimeError prose — both raised forms map onto ClaimOutcome::TimedOut at the eval seam with the pair typed. This note is therefore no longer a modelling frontier; it is unwired work. BUT DO NOT WIRE IT AS IT STANDS, and this is the whole reason the note is being amended rather than deleted. The seed now carries a THIRD axis this arm has no field for: BudgetCompletion, Interrupted or CompletedOverBudget. An armed deadline aborts the witness, so its elapsed is a right-censored LOWER BOUND — a row that would cost 2s and one that would cost 40s report the same figure, because the figure is the ceiling plus poll granularity. The completion-side backstop instead reclassifies a witness that RAN TO COMPLETION, so its elapsed is exact. Projecting both into one TimedOut { basis, budget, elapsed } re-erases at the authority layer precisely the distinction the seed was just corrected to keep, and it does it silently, because a censored figure and a measured one are the same shape. The precedent is this arm own basis field, added by operator ruling 2026-08-05 for the identical reason one axis over: two things surfaced as one arm and the tag alone never carried what told them apart. That is now twice on one arm, which is the tell that it is a product wearing a coproduct clothes. PREREQUISITE, and it is a std change rather than a floor one: std.observation TimedOut gains completion beside basis, with the same ONE-governs-BOTH argument observation_timed_out_basis_note already makes — a bound and a measurement cannot be compared, so a reader must be able to tell which it holds before it uses either number. The projection side needs no change then — floor_component_outcome_of_tag already admits the tag and floor_component_outcome_members already renders the fields, proven by execution today. The arm now also names its CLOCK (std.measure ClockBasis, operator ruling 2026-08-05), and the wall-budget kill this note is about is exactly why: a whole-receipt wall ceiling and the fast-lane thread-CPU fail-stop both surface as TimedOut, so the clock is what tells them apart. floor_component_outcome_of_tag takes the basis as a parameter rather than assuming one, because the tag alone has never carried it." data floor_component_receipt_seed_transport_deferral_note: String = "PURE BOOTSTRAP RECEIPT for the seed-side transport this module is consumed by (review 45058 asked for it, correctly — new hand-Rust owes a named deferral, not a description). WHAT IS ADDED: no new Rust file and no parallel authority — functions inside the existing claim_executor bin that locate this module, resolve it, call floor_component_row_of_failure_mode / floor_component_receipt_document, and write the returned bytes. WHAT IS NOT IN RUST: the receipt's shape, its schema, the failure-mode-to-outcome mapping, the role identification, and every judgment about success — all of that is here, under dag/test/claim/floor_component_receipt_witness_test.dag. The seed side carries no classification of its own; its `_ => failed` catch-all was removed in favour of floor_component_outcome_of_failure_mode's refusal arm. BOUNDARY SHAPE: the seed calls millisecond(count:) through the interpreter and hands back the resulting Millisecond, so no carrier is constructed in Rust and no flat-scalar duration crosses the seam. The sibling seam gunbc.observation_seed_render (render_phase_concluded_line, same bin) still takes elapsed_ms: Nat; that is un-migrated debt on its own lane and was deliberately NOT copied here. DEFERRED TO: the v1 exit finish line ZeroHandMaintainedRust, roadmap node v1-zero-hand-maintained-rust (gunbc.v1_deletion_plan v1_exit_finish_lines). CONCRETE DISSOLUTION: the transport deletes when the floor's receipt write is issued from .dag as a typed host effect (Filesystem.Write through host_effect_apply, the shell-to-intent Phase 2 routing for runtime-present sites) instead of std::fs::write in the seed — at that point the resolve-and-call marshalling has no reason to exist and this module's document function is invoked directly by the emitted walk." @@ -102,6 +102,27 @@ fn floor_component_subject(run_id: NonEmptyStr, index: Nat, label: NonEmptyStr) } } +// GROWTH ON A DOOMED SURFACE — read the parameter count as the tell, not as the design. +// +// This function reconstructs an outcome from a TAG plus the fields the tag lost. That is a lossy +// projection followed by re-supply, and it is structurally the same defect the frontier note +// describes one layer down: ClaimOutcome::RuntimeError flattened the typed budget pair into a +// formatted String, so the executor could not fill TimedOut's fields without re-parsing its own +// prose. The String form was deleted at the seam (2026-08-18); the tag form is the residue of +// the same shape. +// +// It carries the same trap at every axis. The note already names it for the first pair — +// fabricating 0 for budget and elapsed to reach the more specific arm is the fabricated +// plausible output DESIGN §5 forbids — and a completion parameter has exactly that trap one +// axis over, because a caller that does not hold the fact will pass whichever value compiles +// and CompletedOverBudget is the one that reads as normal. +// +// `basis` became a parameter because the tag never carried it. `completion` would be the +// SECOND axis threaded around the same tag, and two is the count at which "this is how the +// function works" starts being mistaken for a design. The terminal shape is the transport +// carrying the typed outcome across the seam, at which point this function has nothing to +// reconstruct and is deleted — so a THIRD discriminating axis triggers that deletion, not a +// third parameter. Paying once rather than per axis forever (§3). fn floor_component_outcome_of_tag( tag: NonEmptyStr, detail: NonEmptyStr, diff --git a/dag/gunbc/plans/discrete_cost_derivation.dag b/dag/gunbc/plans/discrete_cost_derivation.dag index 1970b39d518..64d35b1f8fe 100644 --- a/dag/gunbc/plans/discrete_cost_derivation.dag +++ b/dag/gunbc/plans/discrete_cost_derivation.dag @@ -172,7 +172,7 @@ fn discrete_cost_derivation_body() -> List { li(text: "**Exact cycles on real hardware is not claimable.** Cache behaviour, branch prediction, instruction scheduling, co-tenancy, frequency scaling and I/O latency are outside the modeled guarantee — the DESIGN §4b column that is deliberately *not* a ladder rung. An exact deterministic cycle count is claimable only against a specified abstract machine or simulator, and that is a different `RealizationTarget`, declared as such. For native hardware, cycles are an **observation that calibrates**, and the honest ceiling for the projection is a distribution, not a scalar."), li(text: "**The basis is dated and cited, per `gunbc.witness_row_cost`'s existing rule** — a basis row names an arm64 srv-fleet run id, never a local x86 measurement, and a re-basis is an appended dated row, never a silent widen."), ]), - p(text: "The measured corpus for calibration already exists and is populated: `dag/gunbc/witness_row_cost_basis.tsv` with `WitnessRowCostVerdict` drift comparison. C4 does not need to build a measurement pipeline; it needs to join to one."), + p(text: "The measured corpus for calibration exists but its provenance is NOT sound, and C4 must not be planned as though it were. `dag/gunbc/witness_row_cost_basis.tsv` carries 1,173 rows seeded before `ClaimOutcome::TimedOut` could distinguish a killed run from a completed one, so an unknown subset of them are right-censored figures — a deadline ceiling recorded as if it were a cost. For exactly those rows the 2x comparator returned `WithinBasis` against the ceiling, which is not merely unvouched but wrong in the fail-open direction. C4 therefore joins to a corpus of unknown provenance, not to a measurement pipeline. Its real prerequisite is the completion axis reaching the basis rows and the provenance_unknown population draining; calibrating before then calibrates against censored values."), h2(text: "10. Why a large input is or is not honest"), p(text: "Cost alone cannot answer whether a witness is merely proving that the computer can compute. That is a second, orthogonal question — **what semantic fact does the extra work establish?** — and it is the question the directory heuristic never asks. A large input is justified only when it is one of:"), diff --git a/src/v1/stage0/src/bin/claim_batch.rs b/src/v1/stage0/src/bin/claim_batch.rs index f159caa3813..d712d74f3ed 100644 --- a/src/v1/stage0/src/bin/claim_batch.rs +++ b/src/v1/stage0/src/bin/claim_batch.rs @@ -320,21 +320,38 @@ fn report_outcome(function: &str, outcome: ClaimOutcome, any_failed: &mut bool) println!("FAIL {} (runtime error: {})", function, message); *any_failed = true; } - // Named as a kill, not a duration: the row stopped AT the budget, so elapsed is a - // ceiling. The clock is named because a cpu-budget kill and a wall-budget kill have - // different remedies. + // The clock is named because a cpu-budget kill and a wall-budget kill have different + // remedies — and `completion` is named because whether the number BOUNDS the cost or + // MEASURES it differs by arm. This line used to say "killed ... elapsed is a ceiling" + // unconditionally, which is true of an interrupted row and false of one that ran to + // completion, passed, and was reclassified on cost. Same fabrication as the executor's + // renderer carried; fixed in the same motion so the two transports cannot disagree + // about one outcome. ClaimOutcome::TimedOut { elapsed_ms, budget_ms, kind, + completion, } => { println!( - "FAIL {} (killed at its {} budget: {}ms elapsed > {}ms budget; elapsed is a \ - ceiling, not a completed duration)", + "FAIL {} ({})", function, - kind.label(), - elapsed_ms, - budget_ms + match completion { + v1_compiler::cli_run::BudgetCompletion::Interrupted => format!( + "killed at its {} budget: at least {}ms elapsed against a {}ms budget \ + (interrupted, so elapsed bounds the cost and does not measure it)", + kind.label(), + elapsed_ms, + budget_ms + ), + v1_compiler::cli_run::BudgetCompletion::CompletedOverBudget => format!( + "completed over its {} budget: exactly {}ms elapsed against a {}ms \ + budget (ran to completion and passed, then was reclassified on cost)", + kind.label(), + elapsed_ms, + budget_ms + ), + } ); *any_failed = true; } diff --git a/src/v1/stage0/src/bin/claim_executor.rs b/src/v1/stage0/src/bin/claim_executor.rs index 9cab37a52cd..e0b1532dbde 100644 --- a/src/v1/stage0/src/bin/claim_executor.rs +++ b/src/v1/stage0/src/bin/claim_executor.rs @@ -2096,7 +2096,31 @@ impl ExpectedRedDisposition { match outcome { ClaimOutcome::Fail => Self::AgreementAssertionReturnedFalse, ClaimOutcome::Pass => Self::StaleQuarantineAssertionReturnedTrue, - ClaimOutcome::TimedOut { .. } => Self::BudgetFailure, + // SPLIT ON completion, because the two arms differ in whether a verdict exists. + // An INTERRUPTED row produced none — budget failure is the honest reading. A + // CompletedOverBudget row RAN TO COMPLETION AND PASSED (both converters match only + // `ClaimOutcome::Pass`), so reporting "no verdict" about it is the same + // state-space conflation this PR removes on the required-floor path, left standing + // one function away. + // + // It maps to the stale-quarantine arm rather than a new one deliberately. The + // verdict-bearing half — the enrolled claim is passing and the roster row is stale + // — is exactly what that arm means, and it is the half a consumer of this tally + // acts on. The cost half is NOT represented here: this surface has one channel per + // row, where `run_required_floor` reports such a row to both `stale_quarantine` + // and `budget_refused`. Minting a `StaleAndOverBudget` arm to carry it would be + // growth on a surface the floor cut is retiring — `--required-floor` returns + // before any caller of `run_batch_unit`, so CI does not execute this path at all. + // Losing a cost signal on a retiring surface is the right trade; reporting a + // passing row as undecided is not. + ClaimOutcome::TimedOut { + completion: v1_compiler::cli_run::BudgetCompletion::Interrupted, + .. + } => Self::BudgetFailure, + ClaimOutcome::TimedOut { + completion: v1_compiler::cli_run::BudgetCompletion::CompletedOverBudget, + .. + } => Self::StaleQuarantineAssertionReturnedTrue, ClaimOutcome::RuntimeError { .. } | ClaimOutcome::NotBool { .. } => { Self::InfrastructureOrReferentFailure } @@ -2306,6 +2330,11 @@ struct BudgetRefusal { elapsed_ms: u64, budget_ms: u64, kind: BudgetKind, + /// Carried, not dropped. Without it the erasure the classifier just stopped doing simply + /// moves one layer down: this carrier feeds the durable component and alert path, so a + /// completed-and-passed row would arrive there as an indistinguishable "budget refusal" + /// and its exact elapsed would be read as a ceiling. + completion: v1_compiler::cli_run::BudgetCompletion, } #[derive(Debug, Clone, PartialEq, Eq)] @@ -2634,21 +2663,37 @@ fn claim_result_for_outcome( elapsed_ms, budget_ms, kind, + completion, } => ClaimResult { function, entry: entry.clone(), ok: false, - // The detail still names the budget in prose for the human reading a log, but - // `budget_refusal` beside it is what classification reads — so the mode no - // longer depends on this wording. "ceiling" is deliberate: the row was killed - // AT the budget, so elapsed bounds the cost, it does not measure it. - detail: format!( - "killed at its {} budget: {}ms elapsed > {}ms budget (elapsed is a ceiling, \ - not a completed duration)", - kind.label(), - elapsed_ms, - budget_ms - ), + // The detail names the budget in prose for the human reading a log; `budget_refusal` + // beside it is what classification reads, so the mode does not depend on this + // wording. What the wording MUST get right is whether the number is a bound or a + // measurement, and it used to say "killed ... elapsed is a ceiling" unconditionally. + // That is true of an interrupted row and FALSE of a completed one: a + // `CompletedOverBudget` row ran to completion, passed, and has an exact elapsed, so + // asserting it was killed and censored is a fabricated fact in a durable receipt. + // The old comment defended the wording ("'ceiling' is deliberate"), which is how it + // survived — a considered-looking justification for a claim that only held on one + // arm. + detail: match completion { + v1_compiler::cli_run::BudgetCompletion::Interrupted => format!( + "killed at its {} budget: at least {}ms elapsed against a {}ms budget \ + (interrupted, so elapsed bounds the cost and does not measure it)", + kind.label(), + elapsed_ms, + budget_ms + ), + v1_compiler::cli_run::BudgetCompletion::CompletedOverBudget => format!( + "completed over its {} budget: exactly {}ms elapsed against a {}ms budget \ + (ran to completion and passed, then was reclassified on cost)", + kind.label(), + elapsed_ms, + budget_ms + ), + }, wall_nanos, resolve_nanos, corpus_resolve_nanos: 0, @@ -2661,6 +2706,7 @@ fn claim_result_for_outcome( elapsed_ms, budget_ms, kind, + completion, }), host_dependency_refusal: None, resolve_realization, @@ -4017,10 +4063,12 @@ fn discovery_budget_refusal(summary: &DiscoverySummary) -> Option elapsed_ms, budget_ms, kind, + completion, } => Some(BudgetRefusal { elapsed_ms, budget_ms, kind, + completion, }), _ => None, }) @@ -4092,13 +4140,23 @@ fn scoped_witness_summary_outcome( elapsed_ms, budget_ms, kind, + completion, } => ( - "budget-killed", + // "budget-killed" was unconditional and is only true of an interrupted row; a + // completed one passed and was reclassified on an exact cost. The tag is what + // downstream reads, so a wrong tag is worse than wrong prose. + match completion { + v1_compiler::cli_run::BudgetCompletion::Interrupted => "budget-killed", + v1_compiler::cli_run::BudgetCompletion::CompletedOverBudget => { + "budget-exceeded-completed" + } + }, format!( - "{} elapsed_ms={} budget_ms={}", + "{} elapsed_ms={} budget_ms={} elapsed_is={}", kind.label(), elapsed_ms, - budget_ms + budget_ms, + completion.elapsed_reading() ), ), }); @@ -10375,18 +10433,35 @@ fn run() -> Result { ); eprintln!( "required-floor: planned={} executed={} terminal={} passed={} \ - known_red_held={} failed={}", + known_red_held={} failed={} stale_quarantine={} budget_refused={}", outcome.claims_planned, outcome.claims_executed, outcome.receipt_identities, outcome.passed, outcome.known_red_held, - outcome.failures.len() + outcome.failures.len(), + outcome.stale_quarantine.len(), + outcome.budget_refused.len() ); for failure in &outcome.failures { eprintln!("required-floor: FAIL {failure}"); } - if outcome.failures.is_empty() { + // THREE CAUSES, THREE COUNTS, ONE STOPPED LINE. All three refuse the run, and + // they are reported apart because their remedies differ: a FAIL is a defect to + // fix, a STALE-QUARANTINE is a fix that already landed and a roster row to + // delete, a BUDGET-REFUSED is a cost to reduce. Summing them into `failed` + // would make an un-quarantine indistinguishable from a regression in the alert + // signature, which is the conflation `std.witness_admission` rules out. + for stale in &outcome.stale_quarantine { + eprintln!("required-floor: STALE-QUARANTINE {stale}"); + } + for refused in &outcome.budget_refused { + eprintln!("required-floor: BUDGET-REFUSED {refused}"); + } + if outcome.failures.is_empty() + && outcome.stale_quarantine.is_empty() + && outcome.budget_refused.is_empty() + { Ok(ExitCode::SUCCESS) } else { Err(ExitCode::from(1)) @@ -11294,6 +11369,15 @@ fn run() -> Result { /// Typed terminal failure class for the falsifier/floor walk (brief Step 2, 2026-07-25): /// names BudgetExceeded{wall,budget} vs WitnessRed{claims} vs Infra{spawn/toolchain/eviction} /// so "falsifier dark" is one of three modes, never an undifferentiated exit 1. +// STALE SIGNAL, NOT MERELY DEAD CODE. These substrings matched a budget refusal back when a +// raised one reached the claim seam as a `RuntimeError` carrying the refusal as prose. It now +// arrives as `ClaimOutcome::TimedOut` with the pair typed, so nothing renders this text on the +// required-floor path any more. That matters more for the RESTORE than for today: this function +// sits past the required-floor early return, on the falsifier lane whose workflows the floor cut +// deleted, and a dead `.contains` does not fail loudly when a lane comes back — it matches +// nothing and reports NO budget findings, which says "there are none" where it should say "I +// cannot tell". Whoever re-adds this lane reads the variant, not the prose; the classification +// is deletion population otherwise. fn falsifier_failure_mode(details: &[String]) -> &'static str { if details.iter().any(|d| { d.contains("BudgetExceeded{") @@ -13008,6 +13092,11 @@ mod tests { elapsed_ms: 5001, budget_ms: 5000, kind: BudgetKind::Cpu, + // Interrupted, so 5001 is a lower bound. Named rather than defaulted: the + // CompletedOverBudget row is a DIFFERENT case with its own arm, and a fixture that + // did not say which one it built would be asserting about whichever the compiler + // picked. + completion: v1_compiler::cli_run::BudgetCompletion::Interrupted, }); assert!( t.agreements.is_empty(), @@ -13085,6 +13174,7 @@ mod tests { elapsed_ms: 1, budget_ms: 1, kind: BudgetKind::Wall, + completion: v1_compiler::cli_run::BudgetCompletion::Interrupted, }, ClaimOutcome::RuntimeError { message: "boom".into(), @@ -13552,6 +13642,7 @@ mod tests { elapsed_ms: 900_001, budget_ms: 900_000, kind: BudgetKind::Wall, + completion: v1_compiler::cli_run::BudgetCompletion::Interrupted, }), host_dependency_refusal: None, resolve_realization: None, @@ -16654,6 +16745,7 @@ mod tests { elapsed_ms: 900_001, budget_ms: 900_000, kind: BudgetKind::Wall, + completion: v1_compiler::cli_run::BudgetCompletion::Interrupted, }; // Both arms: the receipt projection may succeed or refuse, and a receipt refusal must diff --git a/src/v1/stage0/src/cli_run.rs b/src/v1/stage0/src/cli_run.rs index 1f8031c8e52..82627d636f5 100644 --- a/src/v1/stage0/src/cli_run.rs +++ b/src/v1/stage0/src/cli_run.rs @@ -7656,6 +7656,66 @@ pub enum BudgetKind { Wall, } +/// WHETHER THE NUMBER IS A MEASUREMENT OR A LOWER BOUND — the axis `BudgetKind` does not carry. +/// +/// `BudgetKind` says which clock was consulted. It does not say whether the witness FINISHED, +/// and those are different facts with different arithmetic: +/// +/// - `Interrupted` — an armed deadline fired and the witness was aborted. `elapsed_ms` is +/// right-censored: the true cost is at least that and is otherwise unknown. A row that would +/// have taken two seconds and one that would have taken forty report the same number, because +/// the number is the ceiling plus poll granularity rather than a property of the row. +/// - `CompletedOverBudget` — the witness ran to completion and passed, and the completion-side +/// backstop then reclassified it. `elapsed_ms` is exact. +/// +/// Keeping the two apart is what makes a cost distribution computable at all: a spread taken +/// across a censoring boundary is an artifact of where the ceiling sits, not a fact about the +/// witnesses. It is also the condition named in `claim_executor.rs`'s cost-basis seeding guard, +/// which refuses to seed a basis from a deadline-killed row "until ClaimOutcome::TimedOut can +/// distinguish killed from completed". +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum BudgetCompletion { + Interrupted, + CompletedOverBudget, +} + +// WHY THIS IS A FIELD AND NOT A SIBLING VARIANT — the actual trade, recorded so the next person +// weighing it has the argument rather than the outcome. +// +// The discriminator sits INSIDE `TimedOut`, which is exactly what made the erasure writable: a +// `TimedOut { .. }` wildcard absorbs it, and the classifier did precisely that. Had +// passed-over-budget been a sibling `ClaimOutcome` variant, that wildcard would not have +// compiled against it and the bug would have been a type error instead of a review miss. +// +// It is still a field, for a reason that is not inertia. The variant split this replaced was on +// RAISE MECHANISM — in-eval poll versus completion-side backstop — which is not a distinction +// any consumer should act on, and unifying it is what closed the absorption in the first place. +// Passed-versus-interrupted IS a real distinction because it determines the remedy. Splitting +// the variant again would re-fragment an event vocabulary that was just deliberately closed, so +// the axis lives on the arm and the wildcard hazard is paid for by review. +// +// NEXT-RUNG TRIGGER, falsifiable rather than a site count: `elapsed: Measured | LowerBound` +// makes the bad read UNCONSTRUCTIBLE rather than merely reviewable — you cannot obtain the +// number without deciding which kind you hold. It is not justified by today's population +// (seven consuming sites), because that is the wrong denominator: the value scales with the +// RATE at which consuming sites appear and the cost of one miss. So the trigger is a condition, +// not a threshold — THE NEXT CONSUMING SITE ADDED THAT DROPS THE AXIS is the evidence that +// arm-level is insufficient and the climb is earned. Today's rate evidence, for whoever reads +// this next: four sites dropped it in one PR, authored by the person who wrote the converters, +// on the day he was most primed to look for it, one of them a fabricated receipt protected by +// its own justifying comment. + +impl BudgetCompletion { + /// How the elapsed number may be READ. Rendered beside every budget figure so a reader + /// never has to know which mechanism produced it. + pub fn elapsed_reading(self) -> &'static str { + match self { + BudgetCompletion::Interrupted => "at least", + BudgetCompletion::CompletedOverBudget => "exactly", + } + } +} + impl BudgetKind { pub fn label(self) -> &'static str { match self { @@ -7690,6 +7750,7 @@ pub enum ClaimOutcome { elapsed_ms: u64, budget_ms: u64, kind: BudgetKind, + completion: BudgetCompletion, }, } @@ -15830,8 +15891,34 @@ pub fn run_claim(ctx: &v1_interpreter::InterpContext, function: &str) -> ClaimOu // relocating-the-file-does-not-discharge-it text) reaches the witness author. Mapping // here rather than in the kernel is what keeps a served HTTP route from receiving // witness guidance it cannot act on. - Err(e) => ClaimOutcome::RuntimeError { - message: format!("{}", v1_interpreter::map_budget_error_to_witness_refusal(e)), + // ONE EVENT, ONE VARIANT. A budget refusal reaches this seam two ways — the in-eval + // stride poll raises it as an error, while the completion-side backstop produces + // `TimedOut` directly — and until now the first arrived as a `RuntimeError` carrying + // the refusal as prose. That is one fact in two representations, and it is not + // cosmetic: any consumer partitioning on the outcome sees a budget refusal as an + // ordinary runtime error, so a partition that means to treat the two apart cannot. + // Mapping both raised forms onto `TimedOut` here makes the outcome vocabulary closed + // over the event, so a total match is total in fact and not only in shape. + Err(e) => match v1_interpreter::map_budget_error_to_witness_refusal(e) { + v1_interpreter::InterpError::EvalBudgetExceeded { cpu_ms, budget_ms } => { + ClaimOutcome::TimedOut { + elapsed_ms: cpu_ms, + budget_ms, + kind: BudgetKind::Cpu, + completion: BudgetCompletion::Interrupted, + } + } + v1_interpreter::InterpError::WitnessWallBudgetExceeded { wall_ms, budget_ms } => { + ClaimOutcome::TimedOut { + elapsed_ms: wall_ms, + budget_ms, + kind: BudgetKind::Wall, + completion: BudgetCompletion::Interrupted, + } + } + other => ClaimOutcome::RuntimeError { + message: format!("{other}"), + }, }, } } @@ -15957,6 +16044,56 @@ pub fn run_claims_in_process( /// replacing a genuine finding with the budget message would discard it. `cpu_nanos` is /// THREAD CPU time (not wall), matching the stride-poll metric — a witness whose wall time /// was inflated by cold-I/O or governor time-slicing is not misclassified as over-budget. +/// WHICH ARM OF THE EXPECTED-RED PARTITION AN ENROLLED ROW LANDS IN. +/// +/// A total function over the outcome, so the partition is a value the caller matches on rather +/// than three `continue`s whose exhaustiveness holds only by reading the loop. The three arms +/// are mutually exclusive by construction here; the caller's sum check then verifies that the +/// roster is covered exactly once. +#[derive(Debug, PartialEq, Eq)] +enum ExpectedRedArm { + /// Enrolled and failed. Agreement. + Held, + /// Enrolled and passed. The debt was repaid and the roster is stale — reds the build. + NowPassing, + /// Enrolled and INTERRUPTED at a budget. NOT agreement: an interruption is a lower bound on + /// cost, never a verdict, so the enrolled claim was never decided. + BudgetRefused, + /// Enrolled, PASSED, and then reclassified because its exact cost exceeded the budget. + /// + /// This arm exists because the row is true on two axes at once and the other three arms + /// each force a choice between them. Semantically the claim WAS decided and it passed, so + /// the roster row is stale and must be removed. On cost it is over budget with an EXACT + /// elapsed, so a real cost debt remains. Reporting it as `BudgetRefused` says the claim + /// went undecided, which is false — that is "a budget outcome is never stale", the same + /// absorption as "a budget outcome is always held" one arm over, and it hides precisely the + /// signal the roster exists to surface: that the debt was repaid. Reporting it as + /// `NowPassing` would drop the cost fact instead. So it reports BOTH, and the reader gets + /// two remedies rather than whichever one the code happened to pick. + /// + /// Reachability is not incidental: `budget_completion_outcome` and its wall sibling rewrite + /// only `ClaimOutcome::Pass`, so `CompletedOverBudget` cannot occur for a failing witness. + /// The arm therefore means "passed, then reclassified on cost", not merely "completed". + PassedOverBudget, +} + +fn expected_red_arm(outcome: &ClaimOutcome) -> ExpectedRedArm { + match outcome { + ClaimOutcome::Pass => ExpectedRedArm::NowPassing, + ClaimOutcome::TimedOut { + completion: BudgetCompletion::Interrupted, + .. + } => ExpectedRedArm::BudgetRefused, + ClaimOutcome::TimedOut { + completion: BudgetCompletion::CompletedOverBudget, + .. + } => ExpectedRedArm::PassedOverBudget, + ClaimOutcome::Fail | ClaimOutcome::NotBool { .. } | ClaimOutcome::RuntimeError { .. } => { + ExpectedRedArm::Held + } + } +} + fn budget_completion_outcome( budget: Option, outcome: ClaimOutcome, @@ -15968,6 +16105,7 @@ fn budget_completion_outcome( elapsed_ms: (cpu_nanos / 1_000_000) as u64, budget_ms, kind: BudgetKind::Cpu, + completion: BudgetCompletion::CompletedOverBudget, } } (_, o) => o, @@ -15988,6 +16126,7 @@ fn wall_budget_completion_outcome( elapsed_ms: (wall_nanos / 1_000_000) as u64, budget_ms, kind: BudgetKind::Wall, + completion: BudgetCompletion::CompletedOverBudget, } } (_, o) => o, @@ -16012,10 +16151,20 @@ mod budget_completion_tests { elapsed_ms, budget_ms, kind, + completion, } => { assert_eq!(budget_ms, 5); assert_eq!(elapsed_ms, 6); assert_eq!(kind, BudgetKind::Cpu, "CPU budget must not report as wall"); + // Binding `completion` rather than `..` is the point: this fn is one of the two + // producers of CompletedOverBudget, so if it ever emitted Interrupted the + // elapsed above would silently become a lower bound and 6 would stop being a + // measurement. A `..` here would have accepted that. + assert_eq!( + completion, + BudgetCompletion::CompletedOverBudget, + "the completion-side backstop observes an exact elapsed, never a bound" + ); } other => panic!("expected TimedOut, got {other:?}"), } @@ -16100,10 +16249,16 @@ mod budget_completion_tests { elapsed_ms, budget_ms, kind, + completion, } => { assert_eq!(budget_ms, 600); assert_eq!(elapsed_ms, 601_000); assert_eq!(kind, BudgetKind::Wall, "wall budget must not report as CPU"); + assert_eq!( + completion, + BudgetCompletion::CompletedOverBudget, + "the completion-side backstop observes an exact elapsed, never a bound" + ); } other => panic!("expected TimedOut, got {other:?}"), } @@ -17926,10 +18081,25 @@ pub fn project_witness_cost_receipt( // the authored `millisecond` constructor across the boundary rather than // assembling a Value::Record here, so the constructor stays the single // authority for the carrier's shape. + // THE ONE DELIBERATE DROP — and per DESIGN §5 it is AcknowledgePreexistingDebt, + // not new debt, which is a distinction worth naming rather than leaving to a + // reader's charity. `std.observation` `TimedOut` never carried this axis, so the + // gap predates this change; what the change did was make it VISIBLE by creating + // an axis there was previously nothing to drop. Filing that as newly-introduced + // debt would teach the next author that surfacing a gap costs an approval, and + // the cheap move becomes leaving it unsurfaced — which is the incentive that + // verdict exists to remove. + // `std.observation` `TimedOut` carries { basis, budget, elapsed } and has no + // completion field yet, so there is nowhere on the carrier to put it — and + // fabricating a value to reach a more specific arm is exactly what the floor + // component receipt note already forbids for the first pair. This is the last + // `completion: _` in the seed and it dissolves when that std arm gains + // `completion` beside `basis`; every other consumer now reads the axis. ClaimOutcome::TimedOut { elapsed_ms, budget_ms, kind, + completion: _, } => { // The clock the deadline was enforced on travels WITH the pair, so a // reader of the event can tell a thread-CPU fail-stop from a wall @@ -23638,12 +23808,13 @@ fn run_discovery_rows( elapsed_ms, budget_ms, kind, + completion, } => summary.failures.push(format!( - "{} ({}) killed at its {} budget: {}ms elapsed > {}ms budget \ - (elapsed is a ceiling, not a completed duration)", + "{} ({}) over its {} budget: cost is {} {}ms against a {}ms budget", row.function, row.entry, kind.label(), + completion.elapsed_reading(), elapsed_ms, budget_ms )), @@ -41104,6 +41275,14 @@ pub struct RequiredFloorOutcome { /// witness, and a headline number that rises as debt is added has no direction left to /// report repayment in. pub known_red_held: usize, + /// UNEXPECTED GREEN IS NOT A WITNESS RED. An enrolled row that passed means someone fixed + /// the bug and the roster is stale; folding it into `failures` makes an un-quarantine + /// indistinguishable from a regression in the alert signature, which is the conflation + /// `std.witness_admission` already ruled on for exactly this case. + pub stale_quarantine: Vec, + /// AND A BUDGET REFUSAL IS NEITHER. The row went undecided; the remedy is cost, not a + /// roster edit and not a bug fix. Three causes with three remedies get three counts. + pub budget_refused: Vec, pub over_warn: usize, pub failures: Vec, } @@ -42053,6 +42232,8 @@ pub fn run_required_floor( receipt_identities: 0, passed: 0, known_red_held: 0, + stale_quarantine: Vec::new(), + budget_refused: Vec::new(), over_warn: 0, failures: Vec::new(), }; @@ -42114,6 +42295,8 @@ pub fn run_required_floor( let mut scope_module_max: usize = 0; let mut known_red_held: usize = 0; let mut known_red_now_passing: usize = 0; + let mut known_red_budget_refused: usize = 0; + let mut known_red_passed_over_budget: usize = 0; let mut expected_red_seen: HashSet = HashSet::new(); let mut claim_rss_kb_max: u64 = 0; let mut claim_rss_kb_max_row = String::new(); @@ -42275,24 +42458,98 @@ pub fn run_required_floor( expected_red_seen.insert(claim.qualified.clone()); } let passed = matches!(result, ClaimOutcome::Pass); - if expected_red && passed { - known_red_now_passing += 1; - outcome.failures.push(format!( - "{} is enrolled as expected-red and PASSED — remove it from \ - v2.workflow.floor_expected_red", - claim.qualified - )); - continue; - } if expected_red { - known_red_held += 1; - // NOT COUNTED AS A PASS. A held row did not pass — it failed exactly as enrolled, - // and agreement about a failure is not the same fact as a passing witness. Folding - // it into `passed` would make the headline number rise as debt is ADDED, which is - // the direction that flatters, and would leave no count that falls when the debt is - // repaid. The identity accounting (planned = executed = receipted) is unaffected - // because it counts receipts, not verdicts. - continue; + // ONE DISPATCH. Every arm does its own work here rather than classifying once and + // re-deriving the answer below: two dispatches over one value agree only as long + // as nobody adds a variant, and the second test is always the narrower one, so the + // new variant reaches the fallthrough and is silently held. That is precisely the + // absorption this join exists to remove, and it would read as correct in review + // because the helper LOOKS like it classifies. With one match the compiler makes + // the next variant get classified here or not compile, and the caller's sum check + // is then checking three counters produced by one mechanism rather than two. + match expected_red_arm(&result) { + ExpectedRedArm::NowPassing => { + known_red_now_passing += 1; + outcome.stale_quarantine.push(format!( + "{} is enrolled as expected-red and PASSED — remove it from \ + v2.workflow.floor_expected_red", + claim.qualified + )); + continue; + } + // A BUDGET REFUSAL IS NOT AN ENROLLED FAILURE, and conflating the two is what + // let the most expensive row in the corpus hide behind its own enrollment. + // Enrollment records that this branch expects the claim to FAIL — a statement + // about the witness's verdict. A budget refusal is not a verdict: it is an + // interruption plus a measured lower bound on cost, so the enrolled claim was + // never decided at all. Holding it reports agreement about a failure that + // nobody observed. + ExpectedRedArm::BudgetRefused => { + known_red_budget_refused += 1; + let detail = match &result { + ClaimOutcome::TimedOut { + elapsed_ms, + budget_ms, + kind, + completion, + } => format!( + "{kind:?}, cost {} {elapsed_ms}ms against {budget_ms}ms", + completion.elapsed_reading() + ), + other => format!("{other:?}"), + }; + outcome.budget_refused.push(format!( + "{} is enrolled as expected-red but was BUDGET-REFUSED, not failed: \ + {}. Enrollment asserts an expected verdict and a budget refusal \ + produces none, so the enrolled claim went undecided. Reduce the row's \ + cost, or move it to a lane that declares its own ceiling — removing it \ + from the roster would not help, because it is not passing either.", + claim.qualified, detail + )); + continue; + } + // NOT COUNTED AS A PASS. A held row did not pass — it failed as enrolled, and + // agreement about a failure is not the same fact as a passing witness. Folding + // it into `passed` would make the headline number rise as debt is ADDED, which + // is the direction that flatters, and would leave no count that falls when the + // debt is repaid. The identity accounting (planned = executed = receipted) is + // unaffected because it counts receipts, not verdicts. + // BOTH REMEDIES, because the row is true on both axes. The semantic half goes + // to stale_quarantine (the claim passed, so the roster row must come out) and + // the cost half to budget_refused (an exact overrun that still has to be paid + // down). Choosing one would silently drop the other, and the one the code used + // to drop was the repaid-debt signal the roster exists to surface. + ExpectedRedArm::PassedOverBudget => { + known_red_passed_over_budget += 1; + let cost = match &result { + ClaimOutcome::TimedOut { + elapsed_ms, + budget_ms, + kind, + .. + } => format!("{kind:?}, cost exactly {elapsed_ms}ms against {budget_ms}ms"), + other => format!("{other:?}"), + }; + outcome.stale_quarantine.push(format!( + "{} is enrolled as expected-red and PASSED (then exceeded its budget: \ + {}) — remove it from v2.workflow.floor_expected_red; the cost debt is \ + reported separately and is not a reason to keep the row", + claim.qualified, cost + )); + outcome.budget_refused.push(format!( + "{} PASSED but exceeded its budget: {}. This is an exact measurement, \ + not a bound — the witness ran to completion — so the cost is known and \ + actionable. Reduce it, or move the row to a lane declaring its own \ + ceiling.", + claim.qualified, cost + )); + continue; + } + ExpectedRedArm::Held => { + known_red_held += 1; + continue; + } + } } match result { ClaimOutcome::Pass => outcome.passed += 1, @@ -42313,9 +42570,11 @@ pub fn run_required_floor( elapsed_ms, budget_ms, kind, + completion, } => outcome.failures.push(format!( - "{} exceeded its {kind:?} budget ({elapsed_ms}ms elapsed against {budget_ms}ms)", - claim.qualified + "{} exceeded its {kind:?} budget (cost is {} {elapsed_ms}ms against {budget_ms}ms)", + claim.qualified, + completion.elapsed_reading() )), } } @@ -42375,8 +42634,13 @@ pub fn run_required_floor( // than quietly absorbing it. eprintln!( "[floor-known-red] {} enrolled identity(ies) held as expected-red; {} enrolled \ - identity(ies) now PASS and must be removed from the roster", - known_red_held, known_red_now_passing + identity(ies) now PASS and must be removed from the roster; {} enrolled \ + identity(ies) were BUDGET-REFUSED and so went undecided; {} PASSED but exceeded \ + budget (stale roster row AND a real cost debt)", + known_red_held, + known_red_now_passing, + known_red_budget_refused, + known_red_passed_over_budget ); eprintln!( "[floor-claim-memory] worst single claim grew rss by {:.2}GB at={}", @@ -42439,12 +42703,20 @@ pub fn run_required_floor( // observed exactly once, so it landed in precisely one of the two arms. Checking the sum is // therefore checking that the two arms are the whole roster and do not overlap — cheap, and // it fails loudly if a later edit adds a third arm that quietly swallows rows. - if known_red_held + known_red_now_passing != expected_red_roster.len() { + if known_red_held + + known_red_now_passing + + known_red_budget_refused + + known_red_passed_over_budget + != expected_red_roster.len() + { return Err(format!( "REQUIRED-FLOOR REFUSAL cause=ExpectedRedPartitionInexact held={} now_passing={} \ - roster={} — every enrolled identity must be exactly one of held or now-passing", + budget_refused={} passed_over_budget={} roster={} — every enrolled identity must \ + be exactly one of held, now-passing, budget-refused or passed-over-budget", known_red_held, known_red_now_passing, + known_red_budget_refused, + known_red_passed_over_budget, expected_red_roster.len() )); }