Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
23 changes: 22 additions & 1 deletion dag/gunbc/floor_component_receipt.dag
Original file line number Diff line number Diff line change
Expand Up @@ -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."

Expand Down Expand Up @@ -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,
Expand Down
2 changes: 1 addition & 1 deletion dag/gunbc/plans/discrete_cost_derivation.dag
Original file line number Diff line number Diff line change
Expand Up @@ -172,7 +172,7 @@ fn discrete_cost_derivation_body() -> List<MarkdownBlock> {
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:"),
Expand Down
33 changes: 25 additions & 8 deletions src/v1/stage0/src/bin/claim_batch.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
Expand Down
Loading
Loading