diff --git a/dag/gunbc/floor_cost_distribution.dag b/dag/gunbc/floor_cost_distribution.dag index 5040e31832e..93a402d1767 100644 --- a/dag/gunbc/floor_cost_distribution.dag +++ b/dag/gunbc/floor_cost_distribution.dag @@ -1,7 +1,7 @@ module gunbc.floor_cost_distribution import std.types { Bool, Int, String, NonEmptyStr } -import std.measure { Millisecond, millisecond, millisecond_count } +import std.measure { Millisecond, millisecond, millisecond_count, EvalStepCount, eval_step_count, eval_step_count_value } // THE DERIVATIONS BEHIND docs/plans/floor-cost-distribution-near-the-ceiling.md, SO THAT DOCUMENT // CITES A PRODUCER INSTEAD OF CARRYING COPIED FIGURES. @@ -96,10 +96,35 @@ import std.measure { Millisecond, millisecond, millisecond_count } // cost. Where it DIFFERS is any question about the ceiling: there is none to compare against, so a // consumer asking "how far under its limit did this run" has no answer here rather than a // misleading one. +// THE STEP COUNT LIVES INSIDE THE ARMS (gunbc#11366 Phase 1), which discharges +// `eval_steps_outside_the_reading_coproduct_stall`, a `gunbc.guarantee_stall` row RETIRED BY THIS +// CHANGE and therefore no longer resolvable. Its trigger asked for +// exactly this: a performed count and an observed-so-far-before-censor count reached through +// DIFFERENT CONSTRUCTORS, so no fold can compare them without first matching which it holds. +// +// IT IS INSIDE THE ARM RATHER THAN A SIBLING COPRODUCT, and the difference is the whole climb. A +// sibling `EvalStepReading` beside this one satisfies the trigger's letter -- two constructors, no +// bare `Int` -- while leaving the incoherent row CONSTRUCTIBLE: an `ObservedCpuReading` beside a +// before-censor step count. Whether the claim reached its end is ONE fact about ONE occurrence and +// it discriminates both readings, so carrying the count in the arm makes disagreement +// unconstructible, which is the stall's declared `StructurallyImpossible` ceiling rather than one +// rung below it. +// +// THIS IS NOT THE CLOCK FUSION `std.measure` `measure_clock_basis_note` FORBIDS, stated because +// gunbc#11195 was reworked twice over that rule. Fusion is COMPARING magnitudes read from different +// clocks. This CO-LOCATES three observations of one occurrence under the discriminator they +// genuinely share, and no arm compares a step count to a millisecond. type ClaimCostReading - = ObservedCpuReading { cpu_ms: Millisecond } - | RightCensoredCpuReading { cpu_lower_bound_ms: Millisecond, censoring_ceiling_ms: Millisecond } - | CpuLowerBoundWithoutCeiling { cpu_lower_bound_ms: Millisecond } + = ObservedCpuReading { cpu_ms: Millisecond, eval_steps: EvalStepCount } + | RightCensoredCpuReading { + cpu_lower_bound_ms: Millisecond + censoring_ceiling_ms: Millisecond + eval_steps_before_censor: EvalStepCount + } + | CpuLowerBoundWithoutCeiling { + cpu_lower_bound_ms: Millisecond + eval_steps_before_censor: EvalStepCount + } // The cost figure a derivation is ENTITLED to treat as a POINT, and `Absent` for a censored row. // Every consumer asking a POINT question goes through this, so a bound cannot reach a site that @@ -115,9 +140,34 @@ type ClaimCostReading // crossing guard falsifies. fn observed_cpu_ms(reading: ClaimCostReading) -> Millisecond? { match reading { - ObservedCpuReading { cpu_ms: c } => Present { value: c } - RightCensoredCpuReading { cpu_lower_bound_ms: _, censoring_ceiling_ms: _ } => none - CpuLowerBoundWithoutCeiling { cpu_lower_bound_ms: _ } => none + ObservedCpuReading { cpu_ms: c, eval_steps: _ } => Present { value: c } + RightCensoredCpuReading { cpu_lower_bound_ms: _, censoring_ceiling_ms: _, eval_steps_before_censor: _ } => none + CpuLowerBoundWithoutCeiling { cpu_lower_bound_ms: _, eval_steps_before_censor: _ } => none + } +} + +// THE STEP COUNT A DERIVATION IS ENTITLED TO TREAT AS PERFORMED WORK, and `Absent` for a row that +// was stopped. The exact mirror of `observed_cpu_ms` above, and for the same reason: a bound cannot +// reach a site that treats it as work the claim actually did without the caller writing an `Absent` +// arm. This is the accessor an EQUAL-WORK question must go through -- pairing two rows on step +// equality is only meaningful when both PERFORMED the steps they report. +fn observed_eval_steps(reading: ClaimCostReading) -> EvalStepCount? { + match reading { + ObservedCpuReading { cpu_ms: _, eval_steps: s } => Present { value: s } + RightCensoredCpuReading { cpu_lower_bound_ms: _, censoring_ceiling_ms: _, eval_steps_before_censor: _ } => none + CpuLowerBoundWithoutCeiling { cpu_lower_bound_ms: _, eval_steps_before_censor: _ } => none + } +} + +// THE LOWER BOUND ON STEPS PERFORMED, total over all three arms -- the step mirror of +// `cpu_at_least_ms`. An observed row's bound is its own count. This is the one step question a +// stopped row answers soundly: "this claim performed at least N steps" is true on every arm, while +// "this claim performed N steps" is true on one. +fn eval_steps_at_least(reading: ClaimCostReading) -> EvalStepCount { + match reading { + ObservedCpuReading { cpu_ms: _, eval_steps: s } => s + RightCensoredCpuReading { cpu_lower_bound_ms: _, censoring_ceiling_ms: _, eval_steps_before_censor: b } => b + CpuLowerBoundWithoutCeiling { cpu_lower_bound_ms: _, eval_steps_before_censor: b } => b } } @@ -126,17 +176,17 @@ fn observed_cpu_ms(reading: ClaimCostReading) -> Millisecond? { // is sound: "this row cost at least N" is true on both arms, "this row cost N" is true on one. fn cpu_at_least_ms(reading: ClaimCostReading) -> Millisecond { match reading { - ObservedCpuReading { cpu_ms: c } => c - RightCensoredCpuReading { cpu_lower_bound_ms: b, censoring_ceiling_ms: _ } => b - CpuLowerBoundWithoutCeiling { cpu_lower_bound_ms: b } => b + ObservedCpuReading { cpu_ms: c, eval_steps: _ } => c + RightCensoredCpuReading { cpu_lower_bound_ms: b, censoring_ceiling_ms: _, eval_steps_before_censor: _ } => b + CpuLowerBoundWithoutCeiling { cpu_lower_bound_ms: b, eval_steps_before_censor: _ } => b } } fn reading_is_censored(reading: ClaimCostReading) -> Bool { match reading { - ObservedCpuReading { cpu_ms: _ } => false - RightCensoredCpuReading { cpu_lower_bound_ms: _, censoring_ceiling_ms: _ } => true - CpuLowerBoundWithoutCeiling { cpu_lower_bound_ms: _ } => true + ObservedCpuReading { cpu_ms: _, eval_steps: _ } => false + RightCensoredCpuReading { cpu_lower_bound_ms: _, censoring_ceiling_ms: _, eval_steps_before_censor: _ } => true + CpuLowerBoundWithoutCeiling { cpu_lower_bound_ms: _, eval_steps_before_censor: _ } => true } } @@ -191,7 +241,6 @@ type FloorCostRow { module: String verdict_reached: Bool cost: ClaimCostReading - eval_steps: Int reachability: PreemptionReachability? } @@ -340,7 +389,15 @@ fn claim_cost_columns(header_line: String) -> ClaimCostColumns? { fn observed_cost_reading(fields: List, columns: ClaimCostColumns) -> ClaimCostReading? { match parse_int(s: fields[columns.observed_cpu_ms]) { Absent => none - Present { value: cpu } => Present { value: ObservedCpuReading { cpu_ms: millisecond(count: cpu) } } + Present { value: cpu } => match parse_int(s: fields[columns.eval_steps]) { + Absent => none + Present { value: steps } => Present { + value: ObservedCpuReading { + cpu_ms: millisecond(count: cpu), + eval_steps: eval_step_count(count: steps) + } + } + } } } @@ -363,16 +420,23 @@ fn observed_cost_reading(fields: List, columns: ClaimCostColumns) -> Cla fn right_censored_cost_reading(fields: List, columns: ClaimCostColumns) -> ClaimCostReading? { match parse_int(s: fields[columns.cpu_at_least_ms]) { Absent => none - Present { value: bound } => match columns.censoring_cpu_limit_ms { - Absent => Present { - value: CpuLowerBoundWithoutCeiling { cpu_lower_bound_ms: millisecond(count: bound) } - } - Present { value: ceiling_ix } => match parse_int(s: fields[ceiling_ix]) { - Absent => none - Present { value: ceiling } => Present { - value: RightCensoredCpuReading { + Present { value: bound } => match censored_eval_steps(fields: fields, columns: columns) { + Absent => none + Present { value: steps } => match columns.censoring_cpu_limit_ms { + Absent => Present { + value: CpuLowerBoundWithoutCeiling { cpu_lower_bound_ms: millisecond(count: bound), - censoring_ceiling_ms: millisecond(count: ceiling) + eval_steps_before_censor: eval_step_count(count: steps) + } + } + Present { value: ceiling_ix } => match parse_int(s: fields[ceiling_ix]) { + Absent => none + Present { value: ceiling } => Present { + value: RightCensoredCpuReading { + cpu_lower_bound_ms: millisecond(count: bound), + censoring_ceiling_ms: millisecond(count: ceiling), + eval_steps_before_censor: eval_step_count(count: steps) + } } } } @@ -380,24 +444,23 @@ fn right_censored_cost_reading(fields: List, columns: ClaimCostColumns) } } -// THE STEP COUNT, READ FROM THE COLUMN THAT MATCHES THE ROW'S READING (gunbc#11195). -// -// A COMPLETED ROW PERFORMED ITS STEPS and carries them in `eval_steps`. A CENSORED ROW DID NOT: its -// count is quantised by whatever stopped it, so the producer now writes it in `eval_steps_at_least` -// and leaves `eval_steps` empty. Reading the bound out of the performed column is what let this -// module pair a censored row with a completed one in its equal-work cohort -- the harm -// `gunbc.guarantee_stall` `eval_steps_outside_the_reading_coproduct_stall` is on file for. +// THE BEFORE-CENSOR STEP COUNT OF A STOPPED ROW. Called only by `right_censored_cost_reading`, +// which is what it was always about: a CENSORED row's count is quantised by whatever stopped it, so +// the producer writes it in `eval_steps_at_least` and leaves the performed column empty. // -// THIS IS A HALF-STEP TOWARD THAT STALL'S TRIGGER AND IS NOT IT. The trigger asks for the count to -// move INSIDE the `ClaimCostReading` arms so no fold can compare a bound with a performed count -// without first matching which it holds; this only stops the two arriving through the same column. -// A fold that reads `FloorCostRow.eval_steps` still cannot tell them apart from the field alone, -// which is why the stall row stays standing and is not retired by this change. +// IT USED TO BE `parse_row_eval_steps` AND TO SERVE BOTH ARMS, returning a bare `Int` that the row +// carried beside its reading. That was the half-applied construction +// the retired `gunbc.guarantee_stall` row `eval_steps_outside_the_reading_coproduct_stall` was +// filed against: the +// column split stopped the two counts ARRIVING through one column, but a fold reading +// `FloorCostRow.eval_steps` still could not tell a performed count from a bound. Phase 1 of +// gunbc#11366 moves the count into the arms, so the question "which count is this" is answered by +// the constructor and the stall retires. // // AN OLD-VINTAGE CENSORED ROW STILL READS ITS COUNT FROM `eval_steps`, because before the split // that is where the producer wrote it. Refusing those rows would retire the reader against every // run before the split, which is the same trade the optional ceiling column already makes. -fn parse_row_eval_steps(fields: List, columns: ClaimCostColumns) -> Int? { +fn censored_eval_steps(fields: List, columns: ClaimCostColumns) -> Int? { match parse_int(s: fields[columns.eval_steps]) { Present { value: performed } => Present { value: performed } Absent => match columns.eval_steps_at_least { @@ -472,31 +535,26 @@ fn parse_claim_cost_line(line: String, columns: ClaimCostColumns) -> FloorCostRo } else { match parse_claim_cost_reading(fields: fields, columns: columns) { Absent => none - Present { value: reading } => match parse_row_eval_steps(fields: fields, columns: columns) { + Present { value: reading } => match parse_verdict_reached(value: fields[columns.verdict_reached]) { Absent => none - Present { value: steps } => match parse_verdict_reached(value: fields[columns.verdict_reached]) { - Absent => none - Present { value: reached } => match parse_row_reachability(fields: fields, columns: columns) { - ReachabilityColumnUnreadable => none - ReachabilityColumnUnrecorded => Present { - value: FloorCostRow { - identity: fields[columns.identity], - module: fields[columns.module], - verdict_reached: reached, - cost: reading, - eval_steps: steps, - reachability: none - } + Present { value: reached } => match parse_row_reachability(fields: fields, columns: columns) { + ReachabilityColumnUnreadable => none + ReachabilityColumnUnrecorded => Present { + value: FloorCostRow { + identity: fields[columns.identity], + module: fields[columns.module], + verdict_reached: reached, + cost: reading, + reachability: none } - ReachabilityColumnRead { value: reach } => Present { - value: FloorCostRow { - identity: fields[columns.identity], - module: fields[columns.module], - verdict_reached: reached, - cost: reading, - eval_steps: steps, - reachability: Present { value: reach } - } + } + ReachabilityColumnRead { value: reach } => Present { + value: FloorCostRow { + identity: fields[columns.identity], + module: fields[columns.module], + verdict_reached: reached, + cost: reading, + reachability: Present { value: reach } } } } @@ -747,15 +805,15 @@ type RowCrossing // guessing in either direction. fn row_crossing(row: FloorCostRow, ceiling_ms: Millisecond) -> RowCrossing { match row.cost { - ObservedCpuReading { cpu_ms: c } => + ObservedCpuReading { cpu_ms: c, eval_steps: _ } => if millisecond_count(m: c) >= millisecond_count(m: ceiling_ms) { RowCrossed } else { RowBelowLine } - CpuLowerBoundWithoutCeiling { cpu_lower_bound_ms: b } => + CpuLowerBoundWithoutCeiling { cpu_lower_bound_ms: b, eval_steps_before_censor: _ } => if millisecond_count(m: b) >= millisecond_count(m: ceiling_ms) { RowCrossed } else { RowCrossingUndecidable } - RightCensoredCpuReading { cpu_lower_bound_ms: b, censoring_ceiling_ms: _ } => + RightCensoredCpuReading { cpu_lower_bound_ms: b, censoring_ceiling_ms: _, eval_steps_before_censor: _ } => if millisecond_count(m: b) >= millisecond_count(m: ceiling_ms) { RowCrossed } else { @@ -1040,13 +1098,34 @@ fn implied_clean_run_budget(ceiling_ms: Millisecond, inflation_permille: Int) -> // here while its real variation lives outside the evaluator. `v2.workflow.required_floor` already // carries a declared rung drop for exactly that region, so the population this instrument is // cleanest over is the one that is CPU-bound in the evaluator. +// EQUAL WORK MEANS BOTH ROWS PERFORMED THE SAME COUNT, and a bound agrees with nothing -- not even +// with an identical bound. This is the precise site `gunbc.guarantee_stall` +// the retired stall `eval_steps_outside_the_reading_coproduct_stall` was filed against: while the +// count was a bare +// `Int`, a censored row whose before-censor count happened to equal a completed row's performed +// count JOINED the equal-work cohort, and the cohort then attributed the whole difference between +// them to inflation when the two had not done the same work at all. +// +// IT REFUSES RATHER THAN WIDENING. Two bounds are not admitted on the grounds that they are equal: +// a bound says "at least N", so two rows that both stopped at N may have had any amount of work +// left, and pairing them would manufacture exactly the equal-work claim this function's name makes. +fn performed_steps_agree(a: ClaimCostReading, b: ClaimCostReading) -> Bool { + match observed_eval_steps(reading: a) { + Absent => false + Present { value: sa } => match observed_eval_steps(reading: b) { + Absent => false + Present { value: sb } => eval_step_count_value(s: sa) == eval_step_count_value(s: sb) + } + } +} + fn identity_inflation_permille_at_equal_work( base: RunCost, other: RunCost, min_base_ms: Millisecond ) -> List { base.rows - |> flat_map(b => match other.rows |> filter(o => o.identity == b.identity && o.eval_steps == b.eval_steps) |> first { + |> flat_map(b => match other.rows |> filter(o => o.identity == b.identity && performed_steps_agree(a: o.cost, b: b.cost)) |> first { Absent => [] Present { value: o } => [InflationPair { base_row: b, other_row: o }] }) @@ -1175,6 +1254,15 @@ type SameHeadAttemptPair { // ROW available in the cost artifact (identity, module, attempts and both counts). The artifact carries no expression trace, // so claiming a first divergent evaluator point here would fabricate precision the producer does // not expose. +// `CompletedIdentityStepsNotPerformed` IS A ROW THAT REACHED A VERDICT WHOSE STEPS ARE NOT A +// PERFORMED COUNT. Added by gunbc#11366 Phase 1, and it is a consequence of the carrier rather than +// a new policy: `verdict_reached` and the cost reading are INDEPENDENT AXES, as this file says in +// terms where both are declared, so "reached a verdict" does not by itself entitle a fold to a +// performed step count. Before the count moved inside the arms this case was invisible -- the bare +// `Int` answered for every row -- and a determinism comparison silently treated a bound as work +// performed, which is the harm the retired stall `eval_steps_outside_the_reading_coproduct_stall` +// was filed for. It +// refuses rather than widens. type EvalStepDeterminismViolation = AttemptHeadsDiffer { left_head: NonEmptyStr @@ -1202,6 +1290,11 @@ type EvalStepDeterminismViolation right_attempt: NonEmptyStr right_steps: Int } + | CompletedIdentityStepsNotPerformed { + identity: String + module: String + attempt: NonEmptyStr + } fn completed_left_violations(pair: SameHeadAttemptPair) -> List { pair.left_rows @@ -1221,16 +1314,33 @@ fn completed_left_violations(pair: SameHeadAttemptPair) -> List [CompletedIdentityStepsNotPerformed { + identity: left.identity, + module: left.module, + attempt: pair.left_attempt + }] + Present { value: ls } => match observed_eval_steps(reading: right.cost) { + Absent => [CompletedIdentityStepsNotPerformed { + identity: right.identity, + module: right.module, + attempt: pair.right_attempt + }] + Present { value: rs } => + if eval_step_count_value(s: ls) != eval_step_count_value(s: rs) { + [CompletedIdentityStepsDiffer { + identity: left.identity, + module: left.module, + left_attempt: pair.left_attempt, + left_steps: eval_step_count_value(s: ls), + right_attempt: pair.right_attempt, + right_steps: eval_step_count_value(s: rs) + }] + } else { [] } + } + } + } }) } @@ -1343,10 +1453,16 @@ type IdentityEnvelope { // no verdict -- but those are two independent axes by construction (a host panic reaches no verdict // and its clocks are EXACT), and a guard that holds by an upstream coincidence is the incidental // denominator this ledger already names. The exclusion is done on the axis it is about. +// THE PERFORMED STEP COUNT IS CARRIED HERE, EXTRACTED AT THE SAME BOUNDARY AS THE CPU +// (gunbc#11366 Phase 1). Both come from the observed arm, so one case split at the point of tagging +// admits the row or excludes it, and every later reader of this row has a count it is ENTITLED to +// treat as work performed. Reaching back into `row.cost` downstream would re-ask a question this +// boundary already answered. type RunTaggedRow { run: NonEmptyStr row: FloorCostRow cpu: Millisecond + steps: EvalStepCount } // THE SCAN STATE IS A COPRODUCT AND NOT A `started: Bool`, WHICH IS THE ONE PLACE THIS FAMILY @@ -1394,7 +1510,7 @@ fn envelope_scan_open(t: RunTaggedRow, carry: List) -> Envelop hi: t.cpu, lo_run: t.run, hi_run: t.run, - steps: t.row.eval_steps, + steps: eval_step_count_value(s: t.steps), steps_equal: true, done: carry } @@ -1406,7 +1522,10 @@ fn identity_envelopes(runs: List) -> List { |> filter(r => r.verdict_reached) |> flat_map(r => match observed_cpu_ms(reading: r.cost) { Absent => [] - Present { value: c } => [RunTaggedRow { run: run.run, row: r, cpu: c }] + Present { value: c } => match observed_eval_steps(reading: r.cost) { + Absent => [] + Present { value: st } => [RunTaggedRow { run: run.run, row: r, cpu: c, steps: st }] + } })) |> sort_by(t => t.row.identity) let scanned = fold( @@ -1427,7 +1546,7 @@ fn identity_envelopes(runs: List) -> List { lo_run: if colder { t.run } else { cool }, hi_run: if hotter { t.run } else { hot }, steps: st, - steps_equal: same_work && st == t.row.eval_steps, + steps_equal: same_work && st == eval_step_count_value(s: t.steps), done: prior } } else { diff --git a/dag/gunbc/guarantee_stall/eval_steps_outside_the_reading_coproduct_stall.dag b/dag/gunbc/guarantee_stall/eval_steps_outside_the_reading_coproduct_stall.dag deleted file mode 100644 index 9a3a65abb3a..00000000000 --- a/dag/gunbc/guarantee_stall/eval_steps_outside_the_reading_coproduct_stall.dag +++ /dev/null @@ -1,13 +0,0 @@ -module gunbc.guarantee_stall.eval_steps_outside_the_reading_coproduct_stall - -import gunbc.guarantee_rung { OutsideTheLadder, StructurallyImpossible } -import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, BoundedPopulation, climbs_when } - -data eval_steps_outside_the_reading_coproduct_stall: GuaranteeStall = GuaranteeStall { - subject: "gunbc.floor_cost_distribution FloorCostRow carries eval_steps as a bare Int BESIDE the ClaimCostReading coproduct rather than inside its arms, so a right-censored row's observed-steps-before-censor and a completed row's performed-steps share one type and one constructor; a fold may compare them for equality and manufacture an equal-work cohort out of two observations that measured different things — a HALF-APPLIED construction, because the same file already models the CPU half correctly as ObservedCpuReading | RightCensoredCpuReading with an option-returning observed_cpu_ms beside a total cpu_at_least_ms, and one field did not follow the decision its sibling already made", - current: OutsideTheLadder, - ceiling: StructurallyImpossible, - blocker: ClimbableButUnbuilt, - population: BoundedPopulation { members: ["gunbc.floor_cost_distribution"] }, - next_rung_trigger: climbs_when(capability: "eval_steps moves INSIDE the ClaimCostReading arms, so an observed step count and an observed-so-far-before-censor count are reached through different constructors and no fold can compare them without first matching which it holds — sufficient that the equal-work pairing in identity_inflation_permille_at_equal_work cannot be written over a censored row at all, rather than being discouraged from it. TWO THINGS A LATER AUTHOR MUST NOT SKIP. FIRST, THE KNOWLEDGE ALREADY EXISTS IN THE WRONG CARRIER: this module's own prose states that an interrupted row's eval_steps is quantised by the deadline poll rather than by work. The instrument KNOWS, in a comment, while the type stays a bare Int — DESIGN 4c, an invariant belongs in a typed carrier and prose whose sole job is to hold a rule the type cannot enforce is misplaced data. That is also why a reader believes the instrument is safe: the discipline is written down, in the one place that cannot execute it. SECOND, THIS IS A REPLACEMENT MIGRATION AND NOT A REFINEMENT: eval_steps has 23 references inside this module and 31 outside it, and DESIGN 3's doctrine requires the root cut rather than a leaf-upward edit, because every intermediate state would leave two carriers answering one question. It needs a consumer census and a plan, not a rider on an unrelated change.") -} diff --git a/dag/gunbc/guarantee_stall/roster.dag b/dag/gunbc/guarantee_stall/roster.dag index 5c006cff2a3..caf240269ef 100644 --- a/dag/gunbc/guarantee_stall/roster.dag +++ b/dag/gunbc/guarantee_stall/roster.dag @@ -61,7 +61,6 @@ import gunbc.guarantee_stall.testgen_anchor_generator_totality_stall { testgen_a import gunbc.guarantee_stall.synthesis_established_bound_patch_stall { synthesis_established_bound_patch_stall } import gunbc.guarantee_stall.fn_index_depth_agreement_floor_enrollment_stall { fn_index_depth_agreement_floor_enrollment_stall } import gunbc.guarantee_stall.wet_route_model_lags_seed_stall { wet_route_model_lags_seed_stall } -import gunbc.guarantee_stall.eval_steps_outside_the_reading_coproduct_stall { eval_steps_outside_the_reading_coproduct_stall } import gunbc.guarantee_stall.algebra_application_owner_resolution_stall { algebra_application_owner_resolution_stall } import gunbc.guarantee_stall.algebra_expansion_positional_argument_stall { algebra_expansion_positional_argument_stall } import gunbc.guarantee_stall.generic_lambda_parameter_receiver_evidence_stall { generic_lambda_parameter_receiver_evidence_stall } @@ -222,7 +221,6 @@ data all_guarantee_stalls: List = [ synthesis_established_bound_patch_stall, fn_index_depth_agreement_floor_enrollment_stall, wet_route_model_lags_seed_stall, - eval_steps_outside_the_reading_coproduct_stall, emission_provenance_missing_consumer, emit_returns_medium_not_contribution_stall, emission_apply_generic_r_uninstantiated_stall, diff --git a/dag/gunbc/instruments/floor_cost_distribution_instrument.dag b/dag/gunbc/instruments/floor_cost_distribution_instrument.dag index 196a3bf0718..8f367ea8b9b 100644 --- a/dag/gunbc/instruments/floor_cost_distribution_instrument.dag +++ b/dag/gunbc/instruments/floor_cost_distribution_instrument.dag @@ -16,9 +16,8 @@ import v2.workflow.floor_eval_step_calibration { } import gunbc.floor_cost_distribution { FloorCostRow, - ObservedCpuReading, - RightCensoredCpuReading, - CpuLowerBoundWithoutCeiling, + observed_eval_steps, + eval_steps_at_least, IdentityEnvelope, RunCost, RunExtremeCount, @@ -70,6 +69,7 @@ import gunbc.floor_cost_distribution { CompletedIdentityAbsent, CompletedIdentityUnavailable, CompletedIdentityStepsDiffer, + CompletedIdentityStepsNotPerformed, same_head_eval_step_violations } @@ -976,6 +976,11 @@ fn eval_step_violation_line(v: EvalStepDeterminismViolation) -> String { concat("\tABSENT ", concat(i, concat(" completed on ", concat(c as String, concat(", not present on ", a as String))))) CompletedIdentityUnavailable { identity: i, module: _, completed_attempt: c, unavailable_attempt: u } => concat("\tUNAVAILABLE ", concat(i, concat(" completed on ", concat(c as String, concat(", reached no verdict on ", u as String))))) + CompletedIdentityStepsNotPerformed { identity: i, module: _, attempt: a } => + concat( + "\tSTEPS-NOT-PERFORMED ", + concat(i, concat(concat(" on ", a as String), " reached a verdict but its step count is a bound, not work performed -- the two attempts cannot be compared")) + ) CompletedIdentityStepsDiffer { identity: i, module: _, left_attempt: la, left_steps: ls, right_attempt: ra, right_steps: rs } => concat( "\tSTEPS-DIFFER ", @@ -1137,18 +1142,25 @@ fn calibration_specimen_grounding_for(root: String, run: NonEmptyStr) -> Calibra fn specimen_row_grounding(rows: List, run: NonEmptyStr) -> CalibrationSpecimenGrounding { let wanted = calibration_specimen_identity(calibration: floor_eval_step_calibration) as String let all_matched = rows |> filter(r => r.identity == wanted) - let matched = all_matched |> filter(r => row_step_count_is_complete(row: r)) + let matched = all_matched |> flat_map(r => match observed_eval_steps(reading: r.cost) { + Absent => [] + Present { value: s } => [eval_step_count_value(s: s)] + }) if count(all_matched) == 0 { SpecimenAbsentFromRun { identity: wanted, run: run } } else if count(matched) == 0 { SpecimenStepsRightCensored { identity: wanted, - lower_bound: fold(all_matched |> map(r => r.eval_steps), init: 0, f: (m, n) => if n > m { n } else { m }), + lower_bound: first(reverse( + all_matched + |> map(r => eval_step_count_value(s: eval_steps_at_least(reading: r.cost))) + |> sort_by(n => n) + )), } } else { - let steps = matched |> map(r => r.eval_steps) - let low = fold(steps, init: max_of(xs: steps), f: (m, n) => if n < m { n } else { m }) - let high = fold(steps, init: 0, f: (m, n) => if n > m { n } else { m }) + let steps = matched |> sort_by(n => n) + let low = first(steps) + let high = first(reverse(steps)) if low != high { SpecimenStepsNotDeterministic { identity: wanted, low: low, high: high } } else { @@ -1164,10 +1176,6 @@ fn specimen_row_grounding(rows: List, run: NonEmptyStr) -> Calibra // The seed for the minimum fold. `fold` needs an init that is already a member, and 0 is not one -- // it would make every population's minimum 0 and hide exactly the disagreement above. -fn max_of(xs: List) -> Int { - fold(xs, init: 0, f: (m, n) => if n > m { n } else { m }) -} - fn calibration_specimen_grounding_line(g: CalibrationSpecimenGrounding) -> String { match g { SpecimenJoined { grounding: gr } => match gr { @@ -1187,17 +1195,6 @@ fn calibration_specimen_grounding_line(g: CalibrationSpecimenGrounding) -> Strin } } -// A ROW WHOSE STEP COUNT IS A COMPLETED OBSERVATION RATHER THAN A BOUND. The reading arm is the -// discriminator the artifact already carries: an interrupted claim's figures are lower bounds on -// BOTH clocks and on the step counter, so the same arm that censors the cost censors the steps. -fn row_step_count_is_complete(row: FloorCostRow) -> Bool { - match row.cost { - ObservedCpuReading { cpu_ms: _ } => true - RightCensoredCpuReading { cpu_lower_bound_ms: _, censoring_ceiling_ms: _ } => false - CpuLowerBoundWithoutCeiling { cpu_lower_bound_ms: _ } => false - } -} - fn calibration_specimen_grounding_holds(g: CalibrationSpecimenGrounding) -> Bool { match g { SpecimenJoined { grounding: gr } => specimen_steps_grounding_holds(grounding: gr) diff --git a/dag/test/claim/floor_cost_distribution_witness_test.dag b/dag/test/claim/floor_cost_distribution_witness_test.dag index 328a3b6b124..6bc8ee16027 100644 --- a/dag/test/claim/floor_cost_distribution_witness_test.dag +++ b/dag/test/claim/floor_cost_distribution_witness_test.dag @@ -1,7 +1,7 @@ module test.claim.floor_cost_distribution_witness import std.types { Bool, Int, String, NonEmptyStr } -import std.measure { Millisecond, millisecond, millisecond_count } +import std.measure { Millisecond, millisecond, millisecond_count, eval_step_count, eval_step_count_value } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } import tools.floor_cost_distribution_instrument { RunLoad, @@ -68,12 +68,16 @@ import gunbc.floor_cost_distribution { ClaimCostReading, ObservedCpuReading, RightCensoredCpuReading, + CpuLowerBoundWithoutCeiling, WorstCost, WorstObserved, WorstIsLowerBound, worst_cost_at_least_ms, observed_cpu_ms, cpu_at_least_ms, + observed_eval_steps, + eval_steps_at_least, + performed_steps_agree, censored_rows, RowCrossing, RowCrossed, @@ -125,13 +129,13 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // Shape: two runs over the same three identities in two modules, one of which ("hot") crosses the // 500ms ceiling on run B only. That is the exact shape the real analysis turns on -- a row whose // membership in the crossing set depends on the run rather than on the row. -data row_a1: FloorCostRow = FloorCostRow { identity: "m.hot.x", module: "m.hot", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 400) }, eval_steps: 9000, reachability: none } -data row_a2: FloorCostRow = FloorCostRow { identity: "m.mid.y", module: "m.mid", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 200) }, eval_steps: 4000, reachability: none } -data row_a3: FloorCostRow = FloorCostRow { identity: "m.mid.z", module: "m.mid", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 50) }, eval_steps: 900, reachability: none } +data row_a1: FloorCostRow = FloorCostRow { identity: "m.hot.x", module: "m.hot", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 400), eval_steps: eval_step_count(count: 9000) }, reachability: none } +data row_a2: FloorCostRow = FloorCostRow { identity: "m.mid.y", module: "m.mid", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 200), eval_steps: eval_step_count(count: 4000) }, reachability: none } +data row_a3: FloorCostRow = FloorCostRow { identity: "m.mid.z", module: "m.mid", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 50), eval_steps: eval_step_count(count: 900) }, reachability: none } -data row_b1: FloorCostRow = FloorCostRow { identity: "m.hot.x", module: "m.hot", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 600) }, eval_steps: 9000, reachability: none } -data row_b2: FloorCostRow = FloorCostRow { identity: "m.mid.y", module: "m.mid", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 300) }, eval_steps: 4400, reachability: none } -data row_b3: FloorCostRow = FloorCostRow { identity: "m.mid.z", module: "m.mid", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 100) }, eval_steps: 900, reachability: none } +data row_b1: FloorCostRow = FloorCostRow { identity: "m.hot.x", module: "m.hot", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 600), eval_steps: eval_step_count(count: 9000) }, reachability: none } +data row_b2: FloorCostRow = FloorCostRow { identity: "m.mid.y", module: "m.mid", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 300), eval_steps: eval_step_count(count: 4400) }, reachability: none } +data row_b3: FloorCostRow = FloorCostRow { identity: "m.mid.z", module: "m.mid", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 100), eval_steps: eval_step_count(count: 900) }, reachability: none } // THE CENSORED FIXTURE ROW, and it is deliberately given a bound of 502ms against a 500ms // ceiling -- the shape every interrupted row in the real artifact has, because a row is stopped @@ -146,8 +150,7 @@ data row_c_censored: FloorCostRow = FloorCostRow { identity: "m.hot.k", module: "m.hot", verdict_reached: false, - cost: RightCensoredCpuReading { cpu_lower_bound_ms: millisecond(count: 502), censoring_ceiling_ms: millisecond(count: 500) }, - eval_steps: 163840, + cost: RightCensoredCpuReading { cpu_lower_bound_ms: millisecond(count: 502), censoring_ceiling_ms: millisecond(count: 500), eval_steps_before_censor: eval_step_count(count: 163840) }, reachability: none } @@ -292,7 +295,10 @@ test fn a_reordered_header_is_followed_rather_than_the_old_positions() -> Bool { Present { value: r } => match observed_cpu_ms(reading: r.cost) { Absent => false - Present { value: c } => millisecond_count(m: c) == 400 && r.eval_steps == 1000 + Present { value: c } => millisecond_count(m: c) == 400 && match observed_eval_steps(reading: r.cost) { + Absent => false + Present { value: st } => eval_step_count_value(s: st) == 1000 + } } } } @@ -453,7 +459,10 @@ test fn a_parsed_row_takes_eval_steps_from_the_steps_column() -> Bool { Present { value: r } => match observed_cpu_ms(reading: r.cost) { Absent => false - Present { value: c } => r.eval_steps == 1000 && millisecond_count(m: c) == 400 + Present { value: c } => millisecond_count(m: c) == 400 && match observed_eval_steps(reading: r.cost) { + Absent => false + Present { value: st } => eval_step_count_value(s: st) == 1000 + } } } } @@ -702,8 +711,7 @@ test fn a_missing_or_interrupted_counterpart_refuses_instead_of_shrinking_the_co identity: "m.hot.x", module: "m.hot", verdict_reached: false, - cost: RightCensoredCpuReading { cpu_lower_bound_ms: millisecond(count: 500), censoring_ceiling_ms: millisecond(count: 500) }, - eval_steps: 8000, + cost: RightCensoredCpuReading { cpu_lower_bound_ms: millisecond(count: 500), censoring_ceiling_ms: millisecond(count: 500), eval_steps_before_censor: eval_step_count(count: 8000) }, reachability: none } let missing = SameHeadAttemptPair { @@ -868,9 +876,9 @@ test fn the_same_runs_without_the_refused_member_do_produce_figures() -> Bool { // so the third run is what makes the discriminating red authorable at all: `m.hot.x` reaches its // maximum on run C, so a pair of A and B reports 1500 permille where the three-run envelope // reports 2250. -data row_c1: FloorCostRow = FloorCostRow { identity: "m.hot.x", module: "m.hot", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 900) }, eval_steps: 9000, reachability: none } -data row_c2: FloorCostRow = FloorCostRow { identity: "m.mid.y", module: "m.mid", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 250) }, eval_steps: 4000, reachability: none } -data row_c3: FloorCostRow = FloorCostRow { identity: "m.mid.z", module: "m.mid", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 60) }, eval_steps: 900, reachability: none } +data row_c1: FloorCostRow = FloorCostRow { identity: "m.hot.x", module: "m.hot", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 900), eval_steps: eval_step_count(count: 9000) }, reachability: none } +data row_c2: FloorCostRow = FloorCostRow { identity: "m.mid.y", module: "m.mid", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 250), eval_steps: eval_step_count(count: 4000) }, reachability: none } +data row_c3: FloorCostRow = FloorCostRow { identity: "m.mid.z", module: "m.mid", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 60), eval_steps: eval_step_count(count: 900) }, reachability: none } // PRESENT IN TWO RUNS OF THREE, and enormously spread across the two it is present in. An envelope // computed over "however many runs happened to carry the row" would report 5000 permille for it and @@ -882,8 +890,8 @@ data row_c3: FloorCostRow = FloorCostRow { identity: "m.mid.z", module: "m.mid", // completeness witness stayed GREEN under a mutation that broke the completeness predicate, because // the guarantee it was named for was being supplied by its NEIGHBOUR. Measured, not reasoned: // relaxing `runs_observed == runs_expected` to `>= 1` reddened two other witnesses and not that one. -data row_a4: FloorCostRow = FloorCostRow { identity: "m.part.p", module: "m.part", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 200) }, eval_steps: 100, reachability: none } -data row_b4: FloorCostRow = FloorCostRow { identity: "m.part.p", module: "m.part", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 1000) }, eval_steps: 100, reachability: none } +data row_a4: FloorCostRow = FloorCostRow { identity: "m.part.p", module: "m.part", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 200), eval_steps: eval_step_count(count: 100) }, reachability: none } +data row_b4: FloorCostRow = FloorCostRow { identity: "m.part.p", module: "m.part", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 1000), eval_steps: eval_step_count(count: 100) }, reachability: none } // PRESENT IN ALL THREE RUNS AND WITHOUT A VERDICT IN ONE. `verdict_reached: false` says only that // the row reached no verdict; it says NOTHING about whether the cost beside it is exact, and this @@ -896,16 +904,16 @@ data row_b4: FloorCostRow = FloorCostRow { identity: "m.part.p", module: "m.part // cost-axis case is `m.bound.b` below, which reaches its verdict and still carries a bound. // // Admitting this row would report a 120x envelope for a row nobody completed. -data row_a5: FloorCostRow = FloorCostRow { identity: "m.noverdict.c", module: "m.noverdict", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 100) }, eval_steps: 2000, reachability: none } -data row_b5: FloorCostRow = FloorCostRow { identity: "m.noverdict.c", module: "m.noverdict", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 120) }, eval_steps: 2000, reachability: none } -data row_c5: FloorCostRow = FloorCostRow { identity: "m.noverdict.c", module: "m.noverdict", verdict_reached: false, cost: ObservedCpuReading { cpu_ms: millisecond(count: 1) }, eval_steps: 5, reachability: none } +data row_a5: FloorCostRow = FloorCostRow { identity: "m.noverdict.c", module: "m.noverdict", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 100), eval_steps: eval_step_count(count: 2000) }, reachability: none } +data row_b5: FloorCostRow = FloorCostRow { identity: "m.noverdict.c", module: "m.noverdict", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 120), eval_steps: eval_step_count(count: 2000) }, reachability: none } +data row_c5: FloorCostRow = FloorCostRow { identity: "m.noverdict.c", module: "m.noverdict", verdict_reached: false, cost: ObservedCpuReading { cpu_ms: millisecond(count: 1), eval_steps: eval_step_count(count: 5) }, reachability: none } // A ROW THE ARTIFACT RECORDS AS COSTING NOTHING, present in every run. It is a real shape -- the // per-claim cost artifact records whole milliseconds and 1388 rows measured zero on one sampled run // -- and max-over-min is undefined for it, which is what makes the refusal arm authorable here. -data row_a6: FloorCostRow = FloorCostRow { identity: "m.zero.q", module: "m.zero", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 0) }, eval_steps: 12, reachability: none } -data row_b6: FloorCostRow = FloorCostRow { identity: "m.zero.q", module: "m.zero", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 0) }, eval_steps: 12, reachability: none } -data row_c6: FloorCostRow = FloorCostRow { identity: "m.zero.q", module: "m.zero", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 0) }, eval_steps: 12, reachability: none } +data row_a6: FloorCostRow = FloorCostRow { identity: "m.zero.q", module: "m.zero", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 0), eval_steps: eval_step_count(count: 12) }, reachability: none } +data row_b6: FloorCostRow = FloorCostRow { identity: "m.zero.q", module: "m.zero", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 0), eval_steps: eval_step_count(count: 12) }, reachability: none } +data row_c6: FloorCostRow = FloorCostRow { identity: "m.zero.q", module: "m.zero", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 0), eval_steps: eval_step_count(count: 12) }, reachability: none } // CENSORED ON THE COST AXIS ALONE, AND THAT IS THE ENTIRE POINT OF THE ROW. `m.noverdict.c` above is // excluded by `verdict_reached: false` while its reading is EXACT, so the envelope's verdict filter @@ -917,9 +925,9 @@ data row_c6: FloorCostRow = FloorCostRow { identity: "m.zero.q", module: "m.zero // inputs rather than one fact spelled two ways -- each holds one input fixed and varies the other. Its bound is deliberately far below the observed pair: // admitting it would report a 120x envelope for a row nobody measured, and 1ms describes the // ceiling that stopped the instrument rather than what the row cost. -data row_a7: FloorCostRow = FloorCostRow { identity: "m.bound.b", module: "m.bound", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 100) }, eval_steps: 2000, reachability: none } -data row_b7: FloorCostRow = FloorCostRow { identity: "m.bound.b", module: "m.bound", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 120) }, eval_steps: 2000, reachability: none } -data row_c7: FloorCostRow = FloorCostRow { identity: "m.bound.b", module: "m.bound", verdict_reached: true, cost: RightCensoredCpuReading { cpu_lower_bound_ms: millisecond(count: 1), censoring_ceiling_ms: millisecond(count: 1) }, eval_steps: 5, reachability: none } +data row_a7: FloorCostRow = FloorCostRow { identity: "m.bound.b", module: "m.bound", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 100), eval_steps: eval_step_count(count: 2000) }, reachability: none } +data row_b7: FloorCostRow = FloorCostRow { identity: "m.bound.b", module: "m.bound", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 120), eval_steps: eval_step_count(count: 2000) }, reachability: none } +data row_c7: FloorCostRow = FloorCostRow { identity: "m.bound.b", module: "m.bound", verdict_reached: true, cost: RightCensoredCpuReading { cpu_lower_bound_ms: millisecond(count: 1), censoring_ceiling_ms: millisecond(count: 1), eval_steps_before_censor: eval_step_count(count: 5) }, reachability: none } data env_run_a: RunCost = RunCost { run: "runA" as NonEmptyStr, rows: [row_a1, row_a2, row_a3, row_a4, row_a5, row_a6, row_a7] } data env_run_b: RunCost = RunCost { run: "runB" as NonEmptyStr, rows: [row_b1, row_b2, row_b3, row_b4, row_b5, row_b6, row_b7] } @@ -1234,8 +1242,7 @@ fn reach_row(identity: String, cpu: Int, reach: PreemptionReachability) -> Floor identity: identity, module: "m.cross", verdict_reached: true, - cost: ObservedCpuReading { cpu_ms: millisecond(count: cpu) }, - eval_steps: 1000, + cost: ObservedCpuReading { cpu_ms: millisecond(count: cpu), eval_steps: eval_step_count(count: 1000) }, reachability: Present { value: reach } } } @@ -1247,8 +1254,7 @@ data cross_unrecorded: FloorCostRow = FloorCostRow { identity: "m.cross.unrecorded", module: "m.cross", verdict_reached: true, - cost: ObservedCpuReading { cpu_ms: millisecond(count: 503) }, - eval_steps: 1000, + cost: ObservedCpuReading { cpu_ms: millisecond(count: 503), eval_steps: eval_step_count(count: 1000) }, reachability: none } data cross_below: FloorCostRow = reach_row(identity: "m.cross.below", cpu: 499, reach: ReachabilityCooperativelyPollable) @@ -1256,16 +1262,14 @@ data cross_censored: FloorCostRow = FloorCostRow { identity: "m.cross.censored", module: "m.cross", verdict_reached: false, - cost: RightCensoredCpuReading { cpu_lower_bound_ms: millisecond(count: 502), censoring_ceiling_ms: millisecond(count: 500) }, - eval_steps: 9, + cost: RightCensoredCpuReading { cpu_lower_bound_ms: millisecond(count: 502), censoring_ceiling_ms: millisecond(count: 500), eval_steps_before_censor: eval_step_count(count: 9) }, reachability: Present { value: ReachabilityCooperativelyPollable } } data cross_undecidable: FloorCostRow = FloorCostRow { identity: "m.cross.undecidable", module: "m.cross", verdict_reached: false, - cost: RightCensoredCpuReading { cpu_lower_bound_ms: millisecond(count: 300), censoring_ceiling_ms: millisecond(count: 8000) }, - eval_steps: 9, + cost: RightCensoredCpuReading { cpu_lower_bound_ms: millisecond(count: 300), censoring_ceiling_ms: millisecond(count: 8000), eval_steps_before_censor: eval_step_count(count: 9) }, reachability: Present { value: ReachabilityCooperativelyPollable } } @@ -1396,16 +1400,14 @@ data both_preempted: FloorCostRow = FloorCostRow { identity: "m.cross.both", module: "m.cross", verdict_reached: false, - cost: RightCensoredCpuReading { cpu_lower_bound_ms: millisecond(count: 500), censoring_ceiling_ms: millisecond(count: 500) }, - eval_steps: 9, + cost: RightCensoredCpuReading { cpu_lower_bound_ms: millisecond(count: 500), censoring_ceiling_ms: millisecond(count: 500), eval_steps_before_censor: eval_step_count(count: 9) }, reachability: Present { value: ReachabilityCooperativelyPollable } } data only_preempted: FloorCostRow = FloorCostRow { identity: "m.cross.onlypreempted", module: "m.cross", verdict_reached: false, - cost: RightCensoredCpuReading { cpu_lower_bound_ms: millisecond(count: 500), censoring_ceiling_ms: millisecond(count: 500) }, - eval_steps: 9, + cost: RightCensoredCpuReading { cpu_lower_bound_ms: millisecond(count: 500), censoring_ceiling_ms: millisecond(count: 500), eval_steps_before_censor: eval_step_count(count: 9) }, reachability: Present { value: ReachabilityCooperativelyPollable } } @@ -1441,8 +1443,7 @@ data panicked_exact: FloorCostRow = FloorCostRow { identity: "m.cross.panicked", module: "m.cross", verdict_reached: false, - cost: ObservedCpuReading { cpu_ms: millisecond(count: 12) }, - eval_steps: 40, + cost: ObservedCpuReading { cpu_ms: millisecond(count: 12), eval_steps: eval_step_count(count: 40) }, reachability: Present { value: ReachabilityCooperativelyPollable } } @@ -1495,19 +1496,18 @@ data attempt_pair_cross_tree: FloorAttemptPair = FloorAttemptPair { left: attemp // THE PAIR FIXTURE: one identity whose steps AGREE while its cpu moves, one whose steps DIFFER, and // one that completed on the right and was preempted on the left. So the violation report has an // arm to exercise in three directions and the envelope has exactly one admissible member. -data pair_l_stable: FloorCostRow = FloorCostRow { identity: "m.p.stable", module: "m.p", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 503) }, eval_steps: 90000, reachability: none } -data pair_r_stable: FloorCostRow = FloorCostRow { identity: "m.p.stable", module: "m.p", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 349) }, eval_steps: 90000, reachability: none } -data pair_l_drift: FloorCostRow = FloorCostRow { identity: "m.p.drift", module: "m.p", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 200) }, eval_steps: 155648, reachability: none } -data pair_r_drift: FloorCostRow = FloorCostRow { identity: "m.p.drift", module: "m.p", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 200) }, eval_steps: 171124, reachability: none } +data pair_l_stable: FloorCostRow = FloorCostRow { identity: "m.p.stable", module: "m.p", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 503), eval_steps: eval_step_count(count: 90000) }, reachability: none } +data pair_r_stable: FloorCostRow = FloorCostRow { identity: "m.p.stable", module: "m.p", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 349), eval_steps: eval_step_count(count: 90000) }, reachability: none } +data pair_l_drift: FloorCostRow = FloorCostRow { identity: "m.p.drift", module: "m.p", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 200), eval_steps: eval_step_count(count: 155648) }, reachability: none } +data pair_r_drift: FloorCostRow = FloorCostRow { identity: "m.p.drift", module: "m.p", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 200), eval_steps: eval_step_count(count: 171124) }, reachability: none } data pair_l_preempted: FloorCostRow = FloorCostRow { identity: "m.p.preempted", module: "m.p", verdict_reached: false, - cost: RightCensoredCpuReading { cpu_lower_bound_ms: millisecond(count: 504), censoring_ceiling_ms: millisecond(count: 500) }, - eval_steps: 9, + cost: RightCensoredCpuReading { cpu_lower_bound_ms: millisecond(count: 504), censoring_ceiling_ms: millisecond(count: 500), eval_steps_before_censor: eval_step_count(count: 9) }, reachability: none } -data pair_r_preempted: FloorCostRow = FloorCostRow { identity: "m.p.preempted", module: "m.p", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 380) }, eval_steps: 175664, reachability: none } +data pair_r_preempted: FloorCostRow = FloorCostRow { identity: "m.p.preempted", module: "m.p", verdict_reached: true, cost: ObservedCpuReading { cpu_ms: millisecond(count: 380), eval_steps: eval_step_count(count: 175664) }, reachability: none } data pair_left_run: RunCost = RunCost { run: "33846875188/attempt-1" as NonEmptyStr, rows: [pair_l_stable, pair_l_drift, pair_l_preempted] } data pair_right_run: RunCost = RunCost { run: "33846875188/attempt-2" as NonEmptyStr, rows: [pair_r_stable, pair_r_drift, pair_r_preempted] } @@ -1607,8 +1607,7 @@ data specimen_row_observed: FloorCostRow = FloorCostRow { identity: specimen_identity_fixture, module: "test.claim.floor_eval_step_calibration_specimen_test", verdict_reached: true, - cost: ObservedCpuReading { cpu_ms: millisecond(count: 57) }, - eval_steps: 55011, + cost: ObservedCpuReading { cpu_ms: millisecond(count: 57), eval_steps: eval_step_count(count: 55011) }, reachability: none } @@ -1618,9 +1617,7 @@ data specimen_row_censored: FloorCostRow = FloorCostRow { verdict_reached: false, cost: RightCensoredCpuReading { cpu_lower_bound_ms: millisecond(count: 8000), - censoring_ceiling_ms: millisecond(count: 8000) - }, - eval_steps: 55011, + censoring_ceiling_ms: millisecond(count: 8000), eval_steps_before_censor: eval_step_count(count: 55011) }, reachability: none } @@ -1643,3 +1640,67 @@ test fn a_censored_specimen_row_refuses_rather_than_matching_the_pin() -> Bool { SpecimenRunUnavailable { load: _ } => false } } + +// ── PHASE 1 EVIDENCE: A BOUND IS NOT WORK PERFORMED ──────────────────────────────────────────── +// +// THE DISCRIMINATING RED, AND IT IS RED ONLY BECAUSE THE COUNT MOVED INSIDE THE ARMS. Before +// gunbc#11366 the step count was a bare `Int` on the row, so two rows carrying 4096 compared EQUAL +// whatever had produced those counts -- a claim that performed 4096 steps and a claim that was +// stopped after 4096. `performed_steps_agree` now answers false for the second pair, and no +// re-spelling of the comparison can recover the old answer, because the bound is not reachable +// through `observed_eval_steps` at all. +// +// TWO EQUAL BOUNDS ARE THE SHARPEST CASE and are the reason this is not merely a rename. It is +// tempting to admit them -- the numbers match -- but "at least 4096" twice says nothing about +// whether the two claims did the same work, and the cohort that consumes this would attribute the +// whole difference between them to inflation. +test fn two_equal_bounds_do_not_agree_on_performed_work() -> Bool { + let bound_a = CpuLowerBoundWithoutCeiling { + cpu_lower_bound_ms: millisecond(count: 500), + eval_steps_before_censor: eval_step_count(count: 4096) + } + let bound_b = CpuLowerBoundWithoutCeiling { + cpu_lower_bound_ms: millisecond(count: 900), + eval_steps_before_censor: eval_step_count(count: 4096) + } + let performed = ObservedCpuReading { + cpu_ms: millisecond(count: 500), + eval_steps: eval_step_count(count: 4096) + } + (performed_steps_agree(a: bound_a, b: bound_b) == false) + && (performed_steps_agree(a: performed, b: bound_b) == false) + && performed_steps_agree(a: performed, b: performed) +} + +// THE POSITIVE CONTROL FOR THE ACCESSOR PAIR, so neither is a decoration: the point question is +// answerable on exactly one arm, and the lower-bound question on all three. +test fn the_point_question_answers_on_one_arm_and_the_bound_question_on_every_arm() -> Bool { + let performed = ObservedCpuReading { + cpu_ms: millisecond(count: 500), + eval_steps: eval_step_count(count: 4096) + } + let censored = RightCensoredCpuReading { + cpu_lower_bound_ms: millisecond(count: 500), + censoring_ceiling_ms: millisecond(count: 500), + eval_steps_before_censor: eval_step_count(count: 77) + } + let unbounded = CpuLowerBoundWithoutCeiling { + cpu_lower_bound_ms: millisecond(count: 500), + eval_steps_before_censor: eval_step_count(count: 88) + } + match observed_eval_steps(reading: performed) { + Absent => false + Present { value: p } => + eval_step_count_value(s: p) == 4096 + && match observed_eval_steps(reading: censored) { + Present { value: _ } => false + Absent => match observed_eval_steps(reading: unbounded) { + Present { value: _ } => false + Absent => + eval_step_count_value(s: eval_steps_at_least(reading: performed)) == 4096 + && eval_step_count_value(s: eval_steps_at_least(reading: censored)) == 77 + && eval_step_count_value(s: eval_steps_at_least(reading: unbounded)) == 88 + } + } + } +} diff --git a/docs/plans/enrolment-margin-eval-step-denomination.md b/docs/plans/enrolment-margin-eval-step-denomination.md new file mode 100644 index 00000000000..6950420b314 --- /dev/null +++ b/docs/plans/enrolment-margin-eval-step-denomination.md @@ -0,0 +1,190 @@ +# Denominating the enrolment margin in eval steps + +Governed by DESIGN §5 (fail-closed, oracles, construction over validation) and §4b +(the guarantee ladder). This plan discharges clause (iv) of the §4b(3) drop +`gunbc.rung_drop` `floor_cost_cpu_regression_at_constant_eval_steps`, which is the +only clause of that row gunbc#11195 left standing. + +## The defect this closes, stated as the drop already states it + +gunbc#11195 moved the required floor's **claim ceiling** off CPU and onto eval steps, +and made CPU observed-only for every claim. It did not move every per-subject budget. +`v2.workflow.floor_enrolment_margin` still derives a 302ms budget from +`required_floor_per_subject_cpu_line_ms` and compares an **observed CPU reading** +against it, so a newly enrolled witness can still be refused on a figure that is a +property of the machine rather than of the claim. + +That is exactly what the drop's restoration trigger forbids, in its own words: + +> NO PER-SUBJECT BUDGET MAY CONSUME A RUN-LEVEL READING + +The trigger is stated at **budget grain and not at denomination grain** deliberately, +and gunbc#11195 records why: an earlier revision quantified over the *primitives* a +cost-fidelity report must cover and said nothing about *which budgets* must stop being +vulnerable, so it could have been discharged by denominating one ceiling while another +per-subject budget kept charging a run-level cost to an arbitrary claim. Denominating +the claim ceiling was one step toward the trigger and is not the trigger. + +## Why the first phase is not the enrolment margin + +`floor_enrolment_margin` consumes `gunbc.floor_cost_distribution` `ClaimCostReading` +directly — `EnrolmentCostReading = EnrolmentCostMeasured { reading: ClaimCostReading } | …`. +Every arm of that coproduct is CPU-shaped: + +``` +type ClaimCostReading + = ObservedCpuReading { cpu_ms } + | RightCensoredCpuReading { cpu_lower_bound_ms, censoring_ceiling_ms } + | CpuLowerBoundWithoutCeiling { cpu_lower_bound_ms } +``` + +So the gate **cannot see a step count at all** until the carrier carries one. The step +count exists today only as `FloorCostRow.eval_steps: Int`, a bare scalar beside the +coproduct, and a consumer reaching for it inherits a defect the corpus has already +filed against itself. + +## The filed stall this phase discharges + +`gunbc.guarantee_stall.eval_steps_outside_the_reading_coproduct_stall` — `current: +OutsideTheLadder`, `ceiling: StructurallyImpossible`, `blocker: ClimbableButUnbuilt`, +population `["gunbc.floor_cost_distribution"]`. Its subject, in its own words: the bare +`Int` means a right-censored row's observed-steps-**before-censor** and a completed +row's **performed** steps share one type and one constructor, so a fold may compare +them for equality and manufacture an equal-work cohort out of two observations that +measured different things — a **half-applied construction**, because the same file +already models the CPU half correctly and one field did not follow the decision its +sibling already made. + +Its `next_rung_trigger` is this phase, verbatim: *eval_steps moves INSIDE the +`ClaimCostReading` arms, so an observed step count and an observed-so-far-before-censor +count are reached through different constructors and no fold can compare them.* + +This plan therefore **does not invent its own first phase**. It executes a trigger the +corpus declared before this lane existed. + +## Phase 1 — the carrier (the model) + +``` +type ClaimCostReading + = ObservedCpuReading { + cpu_ms: Millisecond + eval_steps: EvalStepCount + } + | RightCensoredCpuReading { + cpu_lower_bound_ms: Millisecond + censoring_ceiling_ms: Millisecond + eval_steps_before_censor: EvalStepCount + } + | CpuLowerBoundWithoutCeiling { + cpu_lower_bound_ms: Millisecond + eval_steps_before_censor: EvalStepCount + } +``` + +with two accessors mirroring the CPU pair the file already carries, and named for the +same distinction: + +- `observed_eval_steps(reading) -> EvalStepCount?` — `Present` on the observed arm + only. The point question. A bound cannot reach a site that treats it as performed + work without the caller writing an `Absent` arm. +- `eval_steps_at_least(reading) -> EvalStepCount` — total over all three arms. The one + question a censored row can answer soundly: *this claim performed at least N steps*. + +`FloorCostRow.eval_steps: Int` is **deleted**, not deprecated. DESIGN §3's replacement +migrations cut over at the root, and a surviving bare `Int` is the attractor that rule +exists to prevent: while it stands, every nearby question is answered in its vocabulary. + +### Why inside the arms rather than a sibling coproduct + +A sibling `EvalStepReading` beside `cost: ClaimCostReading` would satisfy the trigger's +*letter* — two constructors, no bare `Int` — while leaving the incoherent state +constructible: a row claiming an **observed** CPU reading beside a +**before-censor** step count. Whether the claim reached its end is ONE fact about ONE +occurrence, and it discriminates both readings. Carrying the step count inside the arm +makes disagreement unconstructible, which is the stall's declared ceiling +(`StructurallyImpossible`) rather than one rung below it. + +This is not the clock fusion `std.measure` `measure_clock_basis_note` forbids, and the +distinction is worth stating because gunbc#11195 was reworked twice over exactly it. +Fusion is *comparing* magnitudes read from different clocks. This is *co-locating* +three observations of one occurrence under the discriminator they genuinely share. No +arm compares a step count to a millisecond. + +### Phase 1 blast radius, measured rather than estimated + +Measured on `origin/main` at `3a0f2d4b585`: + +| surface | sites | +| --- | --- | +| `ObservedCpuReading {` | 41 | +| `RightCensoredCpuReading {` | 21 | +| `CpuLowerBoundWithoutCeiling {` | 11 | +| `FloorCostRow {` | 41 | + +across 7 `.dag` files (`floor_cost_distribution` and its witness test and instrument, +`floor_enrolment_margin` and its test, `floor_cost_debt_admission` and its test) plus +the seed mirror in `required_floor_runner.rs`, `cli_run.rs` and `v1_interpreter.rs`. + +The type change admits **no partial state** — every constructor site moves in the same +commit or the corpus does not compile. That is why this is its own phase and why this +PR opens with the plan rather than a half-migration. + +**The step value at each site is authored, not mechanical.** A fixture's step count is +part of what the fixture asserts, so these are not a `sed`. Fixtures whose subject is +the CPU half take a step count that is declared as incidental beside the reading they +actually exercise. + +### Phase 1 evidence + +- **RED** — a fold that compares a performed step count to a before-censor one must + become unwritable. The discriminating probe is the *source* handed to the compiler by + a fixture, per §4b: the invalid program is authorable there even once it is + unwritable in the accepted corpus, and declining the fixture would be + specification-without-execution. +- **CONTROL** — `observed_eval_steps` answers `Absent` on both bound arms and `Present` + on the observed one, executing, so the accessor is not a decoration. + +## Phase 2 — the enrolment margin consumes it + +`floor_enrolment_margin_budget_ms` becomes an `EvalStepCount` derived through the **same** +pinned calibration the claim ceiling uses (`v2.workflow.floor_eval_step_calibration` +`eval_step_budget_for`), from a declared policy in milliseconds of work. It is not a +second calibration and not a literal: §5's oracle rule admits the budget only because it +is grounded in a controlled fixture, and a second rate would be a §3 fork of that +authority. + +`EnrolmentMarginStanding` keeps its arms and changes their denomination: +`EnrolmentWithinMargin` / `EnrolmentOverMargin` carry `EvalStepCount`, and the CPU +reading is **carried beside the verdict as an observation** rather than deciding it — +the same shape gunbc#11195 gave the claim ceiling. + +`EnrolmentBoundWithoutCeiling` survives unchanged in meaning: a preempted row's steps +are a lower bound with no ceiling, exactly as its CPU is. + +### Phase 2 evidence + +- **RED** — a claim whose eval steps exceed the enrolment budget refuses. +- **CONTROL** — a claim far over the 302ms CPU line with in-budget steps is admitted, + with the CPU observation recorded. This is the same pair gunbc#11195 enrolled for the + claim ceiling, and it must be re-authored here rather than cited: a different budget + is a different subject. + +## Phase 3 — retire the CPU line, or say why it stays + +`required_floor_per_subject_cpu_line_ms` exists only because two per-subject gates still +read a CPU clock. When Phase 2 lands, the enrolment margin is not one of them, and the +remaining consumer is `v2.workflow.floor_cost_debt_admission`. Phase 3 decides that one: +either it is denominated too and the symbol is deleted with its own dissolution +condition discharged, or the symbol survives with a population of exactly one, stated. + +**Only when no per-subject budget reads a run-level figure does the drop's clause (iv) +retire**, and the drop is retired by its trigger and by nothing else. + +## What this plan deliberately does not do + +- It does not re-arm a CPU ceiling anywhere. gunbc#11195's evidence stands: three + prose-only heads measured the same floor at 36.7s / 40.8s / 44.7s of summed CPU, and + one identity at an identical 2884 eval steps read 34ms, 455ms and 511ms. A CPU line + refuses on the environment, not on the claim. +- It does not normalise per runner, and does not enrol slow identities as cost-debt + rows. Both are refused designs of record, for the reasons the floor authority states. diff --git a/src/v2/test/floor_cost_debt_admission_test.dag b/src/v2/test/floor_cost_debt_admission_test.dag index 4bf22a12dcd..9528fdccfa3 100644 --- a/src/v2/test/floor_cost_debt_admission_test.dag +++ b/src/v2/test/floor_cost_debt_admission_test.dag @@ -14,7 +14,7 @@ import gunbc.floor_cost_distribution { } import v2.std.logic { Bool } import v2.std.integer { Int } -import std.measure { Millisecond, millisecond, millisecond_count } +import std.measure { Millisecond, millisecond, millisecond_count, EvalStepCount, eval_step_count } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly @@ -26,14 +26,25 @@ fn ceiling() -> Millisecond { millisecond(count: 500) } +// THE STEP COUNT THESE FIXTURES CARRY IS INCIDENTAL AND IS DECLARED AS SUCH (gunbc#11366 Phase 1). +// Every witness in this file exercises the CPU half -- the margin, the ceiling, the censoring +// discriminator -- so the count is present because the arm requires one and not because any +// assertion here reads it. When Phase 2 denominates this gate in eval steps these fixtures gain a +// step parameter and the value stops being incidental; saying so now is what keeps a later reader +// from mistaking an arbitrary figure for a measured one. fn observed(cpu_ms: Int) -> ClaimCostReading { - ObservedCpuReading { cpu_ms: millisecond(count: cpu_ms) } + ObservedCpuReading { cpu_ms: millisecond(count: cpu_ms), eval_steps: fixture_incidental_steps() } +} + +fn fixture_incidental_steps() -> EvalStepCount { + eval_step_count(count: 1000) } fn censored(cpu_lower_bound_ms: Millisecond, censoring_ceiling_ms: Millisecond) -> ClaimCostReading { RightCensoredCpuReading { cpu_lower_bound_ms: cpu_lower_bound_ms, censoring_ceiling_ms: censoring_ceiling_ms, + eval_steps_before_censor: fixture_incidental_steps(), } } @@ -95,7 +106,7 @@ fn standing_censored( test fn a_bound_with_no_ceiling_is_refused_and_does_not_fabricate_a_ceiling() -> Bool { let standing = floor_cost_debt_row( identity: "fixture.bound_no_ceiling", - reading: CpuLowerBoundWithoutCeiling { cpu_lower_bound_ms: millisecond(count: 514) }, + reading: CpuLowerBoundWithoutCeiling { cpu_lower_bound_ms: millisecond(count: 514), eval_steps_before_censor: fixture_incidental_steps() }, ceiling_ms: ceiling(), verdict: FloorCostDebtNeverReachedAVerdict, ) diff --git a/src/v2/test/floor_enrolment_margin_test.dag b/src/v2/test/floor_enrolment_margin_test.dag index 810b750c54d..eddadbca49e 100644 --- a/src/v2/test/floor_enrolment_margin_test.dag +++ b/src/v2/test/floor_enrolment_margin_test.dag @@ -32,7 +32,7 @@ import gunbc.floor_cost_distribution { import v2.std.collection { List } import v2.std.logic { Bool } import v2.std.integer { Int } -import std.measure { Millisecond, millisecond, millisecond_count } +import std.measure { Millisecond, millisecond, millisecond_count, EvalStepCount, eval_step_count } import v2.std.live_tree { LiveTreeDisposition, SubstrateInputsOnly } // Every fixture below is authored in this source; the module reaches nothing outside the @@ -48,17 +48,31 @@ data live_tree_disposition: LiveTreeDisposition = SubstrateInputsOnly // the `v2.test.` gate prefix, so the PR that lands them must show them measured and inside the // margin. A gate whose own witnesses could not clear it would be self-refuting. +// THE STEP COUNT THESE FIXTURES CARRY IS INCIDENTAL AND IS DECLARED AS SUCH (gunbc#11366 Phase 1). +// Every witness in this file exercises the CPU half -- the margin, the ceiling, the censoring +// discriminator -- so the count is present because the arm requires one and not because any +// assertion here reads it. When Phase 2 denominates this gate in eval steps these fixtures gain a +// step parameter and the value stops being incidental; saying so now is what keeps a later reader +// from mistaking an arbitrary figure for a measured one. fn observed(cpu_ms: Int) -> EnrolmentCostReading { EnrolmentCostMeasured { - reading: ObservedCpuReading { cpu_ms: millisecond(count: cpu_ms) } + reading: ObservedCpuReading { + cpu_ms: millisecond(count: cpu_ms), + eval_steps: fixture_incidental_steps() + } } } +fn fixture_incidental_steps() -> EvalStepCount { + eval_step_count(count: 1000) +} + fn censored(lower_bound_ms: Int, ceiling_ms: Int) -> EnrolmentCostReading { EnrolmentCostMeasured { reading: RightCensoredCpuReading { cpu_lower_bound_ms: millisecond(count: lower_bound_ms), censoring_ceiling_ms: millisecond(count: ceiling_ms), + eval_steps_before_censor: fixture_incidental_steps(), } } } @@ -67,6 +81,7 @@ fn bound_without_ceiling(lower_bound_ms: Int) -> EnrolmentCostReading { EnrolmentCostMeasured { reading: CpuLowerBoundWithoutCeiling { cpu_lower_bound_ms: millisecond(count: lower_bound_ms), + eval_steps_before_censor: fixture_incidental_steps(), } } } @@ -470,7 +485,7 @@ test fn an_observed_row_at_325ms_is_refused_against_the_required_floor_ceiling() !floor_cost_debt_row_is_admitted( standing: floor_cost_debt_row( identity: "fixture.tripwire_325", - reading: ObservedCpuReading { cpu_ms: millisecond(count: 325) }, + reading: ObservedCpuReading { cpu_ms: millisecond(count: 325), eval_steps: fixture_incidental_steps() }, ceiling_ms: required_floor_per_subject_cpu_line_ms(), verdict: FloorCostDebtReachedAVerdict, ) diff --git a/src/v2/workflow/floor_cost_debt_admission.dag b/src/v2/workflow/floor_cost_debt_admission.dag index 54fb08673ef..3633319425c 100644 --- a/src/v2/workflow/floor_cost_debt_admission.dag +++ b/src/v2/workflow/floor_cost_debt_admission.dag @@ -101,7 +101,7 @@ fn floor_cost_debt_row( verdict: FloorCostDebtVerdictAxis, ) -> FloorCostDebtRowStanding { match reading { - RightCensoredCpuReading { cpu_lower_bound_ms: b, censoring_ceiling_ms: c } => + RightCensoredCpuReading { cpu_lower_bound_ms: b, censoring_ceiling_ms: c, eval_steps_before_censor: steps } => match verdict { FloorCostDebtNeverReachedAVerdict => if millisecond_count(m: c) == millisecond_count(m: ceiling_ms) @@ -112,6 +112,7 @@ fn floor_cost_debt_row( reading: RightCensoredCpuReading { cpu_lower_bound_ms: b, censoring_ceiling_ms: c, + eval_steps_before_censor: steps, }, }, } @@ -129,17 +130,17 @@ fn floor_cost_debt_row( censoring_ceiling_ms: c, } } - CpuLowerBoundWithoutCeiling { cpu_lower_bound_ms: b } => + CpuLowerBoundWithoutCeiling { cpu_lower_bound_ms: b, eval_steps_before_censor: _ } => FloorCostDebtRowRefusedBoundWithoutCeiling { identity: identity, cpu_lower_bound_ms: b, } - ObservedCpuReading { cpu_ms: c } => + ObservedCpuReading { cpu_ms: c, eval_steps: steps } => if millisecond_count(m: c) > millisecond_count(m: ceiling_ms) { FloorCostDebtRowAdmitted { row: FloorCostDebtRow { identity: identity, - reading: ObservedCpuReading { cpu_ms: c }, + reading: ObservedCpuReading { cpu_ms: c, eval_steps: steps }, }, } } else { diff --git a/src/v2/workflow/floor_enrolment_margin.dag b/src/v2/workflow/floor_enrolment_margin.dag index 696333c3bb6..53ed3e23e7a 100644 --- a/src/v2/workflow/floor_enrolment_margin.dag +++ b/src/v2/workflow/floor_enrolment_margin.dag @@ -325,15 +325,15 @@ fn enrolment_margin_standing( } EnrolmentExpensivenessNotDeclared => match r { - ObservedCpuReading { cpu_ms: c } => + ObservedCpuReading { cpu_ms: c, eval_steps: _ } => if millisecond_count(m: c) > millisecond_count(m: budget_ms) { EnrolmentOverMargin { exact_cpu_ms: c, budget_ms: budget_ms } } else { EnrolmentWithinMargin { exact_cpu_ms: c, budget_ms: budget_ms } } - CpuLowerBoundWithoutCeiling { cpu_lower_bound_ms: b } => + CpuLowerBoundWithoutCeiling { cpu_lower_bound_ms: b, eval_steps_before_censor: _ } => EnrolmentBoundWithoutCeiling { cpu_lower_bound_ms: b } - RightCensoredCpuReading { cpu_lower_bound_ms: b, censoring_ceiling_ms: ceiling } => + RightCensoredCpuReading { cpu_lower_bound_ms: b, censoring_ceiling_ms: ceiling, eval_steps_before_censor: _ } => EnrolmentCeilingCensored { cpu_lower_bound_ms: b, censoring_ceiling_ms: ceiling,