Skip to content
Closed
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
2 changes: 1 addition & 1 deletion DESIGN.md
Original file line number Diff line number Diff line change
Expand Up @@ -121,7 +121,7 @@ Every newly discovered error class — incident, review finding, runtime excepti
- **Rust fmt as a merge-path gate** — declared 2026-09-01
- **Merge-admission stamping: the receipt has no producer** — declared 2026-09-01
- **Falsifier cadence: exposure open, disposition NOT decided** — declared 2026-09-01
- **Stable per-claim cost qualification under a shared execution envelope** — declared 2026-09-01
- **Per-claim cost qualification is unavailable at the subject grain the gate consumes** — declared 2026-09-01
- **Emitted-bytes fixture witnesses in a required lane** — declared 2026-09-01
- **Direct-call argument TYPE-COMPAT judgment inside v2.* modules (one of two arms; inhabitance still runs)** — declared 2026-09-01
- **CI required-run composition** — declared 2026-08-15
Expand Down
2 changes: 1 addition & 1 deletion dag/gunbc/doc_graph_roots.dag
Original file line number Diff line number Diff line change
Expand Up @@ -239,7 +239,7 @@ data hand_authored_doc_bind_incomings: List<HandAuthoredDocBind> = [
slug: "required-floor-in-flight-shared-fill-findings",
primary_work: DeclarationRef { module_path: "v2.workflow.required_floor", decl_name: "changed_witness_cpu_deadline", field: WholeDeclaration },
additional_works: [
DeclarationRef { module_path: "gunbc.rung_drop", decl_name: "floor_cost_contention_verdict", field: WholeDeclaration },
DeclarationRef { module_path: "gunbc.rung_drop", decl_name: "floor_cost_claim_qualification_unavailable", field: WholeDeclaration },
],
dissolution: PlanRetiresWhen { condition: unbound_dissolution(description: "the required floor's in-flight shared-fill ownership and deadline accounting are changed so this characterization no longer describes the shipped mechanism; the row deletes with the superseded findings document. Registered at subject grain: changed_witness_cpu_deadline is the modeled CPU enforcement decision whose bootstrap realization this document characterizes.") },
},
Expand Down
4 changes: 2 additions & 2 deletions dag/gunbc/recurring_failure_mode.dag

Large diffs are not rendered by default.

4 changes: 2 additions & 2 deletions dag/gunbc/rung_drop.dag

Large diffs are not rendered by default.

4 changes: 3 additions & 1 deletion dag/gunbc/witness/witness_floor_workflow.dag
Original file line number Diff line number Diff line change
Expand Up @@ -915,7 +915,9 @@ data long_home_storage_agreement_artifact_name: String = "long-home-storage-agre
// The three rows above record files the floor wrote on every run and nobody collected. This one is
// a rung below: `cli_run.rs` reads GUNBC_REQUIRED_FLOOR_CLAIM_COST and calls
// `write_required_floor_claim_cost_tsv` -- one row per EXECUTED claim, carrying identity, module,
// outcome, verdict_reached, and BOTH clocks (wall_ms and cpu_ms) -- but this job never set the
// outcome, verdict_reached, BOTH clocks (wall_ms and cpu_ms) and the evaluator-step work measure
// (eval_steps, marginal of stored shared fills, the one column that is not a clock and therefore
// the one column invariant across the execution envelope) -- but this job never set the
// variable, so the writer was never armed and the population was recomputed and discarded on every
// required run since the floor cut.
//
Expand Down
8 changes: 4 additions & 4 deletions docs/design-ledgers.md

Large diffs are not rendered by default.

Original file line number Diff line number Diff line change
Expand Up @@ -64,7 +64,7 @@ exceeds the deadline has not necessarily crossed the enforced quantity.
## Exposure authority

The near-ceiling concept and its distribution already belong to `gunbc.rung_drop`
`floor_cost_contention_verdict`, which names it the exposed attention subset. That authority makes
`floor_cost_claim_qualification_unavailable`, which names it the exposed attention subset. That authority makes
the load-bearing distinction: the closed population is every required identity whose CPU deadline
is armed under the shared-runner envelope; a threshold-selected set is only a view whose membership
moves with each measurement. It also declares the current carrier gap: the attention constant is
Expand Down
1 change: 1 addition & 0 deletions src/v1/stage0/src/bin/claim_batch.rs
Original file line number Diff line number Diff line change
Expand Up @@ -1111,6 +1111,7 @@ mod witness_report_line_tests {
wall_nanos: wall_ms * 1_000_000,
cpu_nanos: cpu_ms * 1_000_000,
eval_self_nanos: 0,
eval_steps: 0,
sample_count: 1,
}
}
Expand Down
19 changes: 17 additions & 2 deletions src/v1/stage0/src/cli_run.rs
Original file line number Diff line number Diff line change
Expand Up @@ -18243,12 +18243,17 @@ mod budget_completion_tests {
"claim",
9_000_000,
4_000_000,
77,
);
assert_eq!(
receipt.wall_nanos, 9_000_000,
"wall is the measurement basis"
);
assert_eq!(receipt.cpu_nanos, 4_000_000, "cpu is the enforcement basis");
assert_eq!(
receipt.eval_steps, 77,
"the work measure is carried beside both clocks, not derived from either"
);
assert_ne!(
receipt.wall_nanos, receipt.cpu_nanos,
"the two clocks must be carried independently, not aliased"
Expand Down Expand Up @@ -29173,6 +29178,7 @@ mod discovery_summary_merge_tests {
wall_nanos: 1_000,
cpu_nanos: 1_000,
eval_self_nanos: 1_000,
eval_steps: 0,
sample_count: 1,
},
PerformanceReceipt {
Expand All @@ -29181,6 +29187,7 @@ mod discovery_summary_merge_tests {
wall_nanos: 50_000,
cpu_nanos: 50_000,
eval_self_nanos: 50_000,
eval_steps: 0,
sample_count: 1,
},
PerformanceReceipt {
Expand All @@ -29189,6 +29196,7 @@ mod discovery_summary_merge_tests {
wall_nanos: 5_000,
cpu_nanos: 5_000,
eval_self_nanos: 5_000,
eval_steps: 0,
sample_count: 1,
},
],
Expand Down Expand Up @@ -39541,6 +39549,12 @@ pub struct WitnessExecutionOccurrence {
pub outcome: String,
pub wall_nanos: u128,
pub cpu_nanos: u128,
/// Evaluator steps this claim took, marginal of stored shared-artifact fills — the
/// deterministic work measure beside the two clocks, invariant across the execution
/// envelope in a way neither clock is. Recorded, published, and compared against nothing:
/// `gunbc.rung_drop` `floor_cost_claim_qualification_unavailable` stays standing, and this column is the
/// evidence a step-denominated verdict would later be built on, not that verdict.
pub eval_steps: u64,
/// Whether the claim reached a verdict rather than being safety-interrupted. Retained
/// because `exceeds_completed_cost_line` only judges COMPLETED claims: an interrupted
/// claim has no cost to be over, and inferring that from the duration would make a slow
Expand Down Expand Up @@ -40213,19 +40227,20 @@ fn write_required_floor_claim_cost_tsv(
.map_err(|e| format!("write_required_floor_claim_cost_tsv: write {path}: {e}"))?;
writeln!(
file,
"identity\tmodule\toutcome\tverdict_reached\twall_ms\tcpu_ms\tcost_line_ms"
"identity\tmodule\toutcome\tverdict_reached\twall_ms\tcpu_ms\teval_steps\tcost_line_ms"
)
.map_err(|e| format!("write_required_floor_claim_cost_tsv: write {path}: {e}"))?;
for row in rows {
writeln!(
file,
"{}\t{}\t{}\t{}\t{}\t{}\t{}",
"{}\t{}\t{}\t{}\t{}\t{}\t{}\t{}",
row.identity.replace(['\t', '\n'], " "),
row.module_path.replace(['\t', '\n'], " "),
row.outcome,
row.verdict_reached,
row.wall_nanos / 1_000_000,
row.cpu_nanos / 1_000_000,
row.eval_steps,
row.cost_line_ms
)
.map_err(|e| format!("write_required_floor_claim_cost_tsv: write {path}: {e}"))?;
Expand Down
22 changes: 20 additions & 2 deletions src/v1/stage0/src/cli_run/required_floor_runner.rs
Original file line number Diff line number Diff line change
Expand Up @@ -351,6 +351,8 @@ pub fn run_claim_measured(
}
let started = std::time::Instant::now();
let cpu_started_nanos = v1_interpreter::thread_cpu_nanos();
let steps_started = v1_interpreter::evaluator_steps();
let fill_steps_before = v1_interpreter::shared_artifact_fill_eval_steps();
let fill_before_nanos = shared_artifact_fill_cpu_nanos();
let fill_wall_before_nanos = shared_artifact_fill_wall_nanos();
let outcome = run_claim(ctx, function);
Expand Down Expand Up @@ -380,6 +382,15 @@ pub fn run_claim_measured(
// `measured_wall_nanos`.
let fill_wall_nanos = shared_artifact_fill_wall_nanos().saturating_sub(fill_wall_before_nanos);
let wall_nanos = marginal_wall_nanos(measured_wall_nanos, fill_wall_nanos);
// THE WORK MEASURE, SPLIT BY THE SAME RULE AS THE TWO CLOCKS. Evaluator steps are counted
// unconditionally by `eval_expr`, so this delta is a property of what the claim evaluated
// and carries no term for the machine it evaluated on. Netting the stored fills is what
// keeps that true across execution ORDER as well: without it the claim that happened to
// fill a shared memo would carry the fill's steps and every later reader would carry none.
let measured_eval_steps = v1_interpreter::evaluator_steps().wrapping_sub(steps_started);
let fill_eval_steps =
v1_interpreter::shared_artifact_fill_eval_steps().wrapping_sub(fill_steps_before);
let eval_steps = measured_eval_steps.saturating_sub(fill_eval_steps);
// EITHER clock, not the CPU one. A fill that blocked on I/O can spend wall time while
// charging almost no CPU, and under a `fill_cpu_nanos > 0` guard that fill would be
// subtracted from the enforced wall figure and reported nowhere — a cost dropped rather
Expand All @@ -394,13 +405,17 @@ pub fn run_claim_measured(
eprintln!(
"[floor-shared-fill] claim={function} marginal_cpu_ms={} fill_cpu_ms={} \
measured_cpu_ms={} marginal_wall_ms={} fill_wall_ms={} measured_wall_ms={} \
marginal_eval_steps={} fill_eval_steps={} measured_eval_steps={} \
provenance=filled-shared-artifact triggered_by={function}",
cpu_nanos / 1_000_000,
fill_cpu_nanos / 1_000_000,
measured_cpu_nanos / 1_000_000,
wall_nanos / 1_000_000,
fill_wall_nanos / 1_000_000,
measured_wall_nanos / 1_000_000,
eval_steps,
fill_eval_steps,
measured_eval_steps,
);
}
ctx.clear_eval_deadline();
Expand All @@ -418,6 +433,7 @@ pub fn run_claim_measured(
function,
wall_nanos,
cpu_nanos,
eval_steps,
);
(outcome, receipt)
}
Expand Down Expand Up @@ -3629,7 +3645,7 @@ pub fn run_required_floor(
// `v2.test.languages_consumer_census.corpus.rust_language_external_consumer
// corpus_rust_language_has_external_consumer` at 412ms against the 500ms
// `required_floor_claim_cpu_safety_limit_ms` — red on any runner a fifth slower, which is the
// class `gunbc.rung_drop floor_cost_contention_verdict` now carries with its measurements and
// class `gunbc.rung_drop floor_cost_claim_qualification_unavailable` now carries with its measurements and
// its restoration trigger; this comment states the instance and does not restate the class — while its
// sibling in the same file, reading the identical memo milliseconds later, measured 0ms.
// The `OnceLock` miss is not bracketed by `record_shared_artifact_fill_cpu`, so
Expand Down Expand Up @@ -5555,6 +5571,7 @@ pub fn run_required_floor(
outcome: witness_execution_outcome_label(&result).to_string(),
wall_nanos: receipt.wall_nanos,
cpu_nanos: receipt.cpu_nanos,
eval_steps: receipt.eval_steps,
verdict_reached: matches!(terminality, ClaimTerminality::VerdictReached { .. }),
cost_line_ms: claim.cost_line_ms,
});
Expand Down Expand Up @@ -6776,10 +6793,11 @@ pub fn run_required_floor(
const OVER_COST_PRINT_LIMIT: usize = 25;
for row in ranked.iter().take(OVER_COST_PRINT_LIMIT) {
eprintln!(
"[over-cost] {} wall_ms={} cpu_ms={} line_ms={} outcome={}",
"[over-cost] {} wall_ms={} cpu_ms={} eval_steps={} line_ms={} outcome={}",
row.identity,
row.wall_nanos / 1_000_000,
row.cpu_nanos / 1_000_000,
row.eval_steps,
row.cost_line_ms,
row.outcome
);
Expand Down
Loading
Loading