Repository navigation
FLOOR REPAIR: in-flight shared fill is charged as marginal until store — repair the classification boundary (design first, characterization is landed in docs/plans/required-floor-in-flight-shared-fill-findings.md) #10018
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Changes from all commits
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,35 @@ | ||
| # Required-floor in-flight shared-fill refusal design | ||
|
|
||
| Status: implementation design, following | ||
| `required-floor-in-flight-shared-fill-findings.md`. | ||
|
|
||
| ## Decision | ||
|
|
||
| Keep the required floor's existing 500ms attempt-safety ceiling. When its CPU poll fires during | ||
| an admitted cross-claim fill, classify the interruption as `FillBudgetExceeded` only when the | ||
| claim's marginal CPU without that still-active fill remains within the ceiling. The refusal | ||
| carries the claim entry, prospective producer, fill CPU lower bound, marginal CPU lower bound, | ||
| and unchanged limit. | ||
|
|
||
| This is not pre-publication fill credit. The clock still charges all uncommitted work and stops at | ||
| the same point. The change repairs the subject of the refusal: first-touch order no longer appears | ||
| as intrinsic claim cost when the active prospective fill is what crossed the bound. | ||
|
|
||
| ## Boundary and nesting | ||
|
|
||
| `CrossClaimFillGuard` remains the one lifetime bracket. Its stack frame additionally retains the | ||
| producer and CPU start. At a poll, the outermost active frame identifies the prospective artifact; | ||
| its CPU is inclusive elapsed CPU less already-stored descendants. Those descendants remain netted | ||
| by the existing committed-fill accumulator, exactly as before. | ||
|
|
||
| If marginal CPU alone already exceeds the ceiling, the ordinary evaluation-budget refusal wins. | ||
| If no admitted fill is active, behavior is unchanged. Store, abandon, fill receipts, completion | ||
| accounting, wall accounting, memo admission, and memo serving are unchanged. | ||
|
|
||
| ## Safety and evidence | ||
|
|
||
| The refusal does not make an over-budget fill pass, raise a ceiling, retry a row, or create an | ||
| artifact receipt. Its stable cause token makes the population countable. A real evaluator-path | ||
| test must force the poll while an admitted fill is active and assert the producer is carried; a | ||
| matched unadmitted control must retain the ordinary evaluation-budget refusal. This instrument | ||
| can provide evidence for a separately modeled fill envelope later, but creates no such policy. |
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -8861,6 +8861,10 @@ pub enum WitnessRuntimeCause { | |
| HostToolRelativePathAmbiguous, | ||
| ShellOutputLimitExceeded, | ||
| CallContractMismatch, | ||
| /// An admitted cross-claim producer was the active subject when the unchanged CPU safety | ||
| /// ceiling fired. The token makes the prospective-fill population countable without | ||
| /// treating first-touch order as intrinsic claim cost. | ||
| FillBudgetExceeded, | ||
| /// An `InterpError` with its own `ClaimOutcome` arm reached the untyped classifier anyway. | ||
| /// Loud rather than absorbed: this is a defect in the mapping above, and a run that produces | ||
| /// it should say so on the row rather than presenting the throw as an ordinary one. | ||
|
|
@@ -8893,6 +8897,7 @@ impl WitnessRuntimeCause { | |
| } | ||
| WitnessRuntimeCause::ShellOutputLimitExceeded => "shell-output-limit-exceeded", | ||
| WitnessRuntimeCause::CallContractMismatch => "call-contract-mismatch", | ||
| WitnessRuntimeCause::FillBudgetExceeded => "fill-budget-exceeded", | ||
| WitnessRuntimeCause::MappedOutcomeEscaped => "mapped-outcome-escaped", | ||
| } | ||
| } | ||
|
|
@@ -8926,6 +8931,7 @@ impl WitnessRuntimeCause { | |
| } | ||
| E::ShellOutputLimitExceeded { .. } => WitnessRuntimeCause::ShellOutputLimitExceeded, | ||
| E::CallContractMismatch { .. } => WitnessRuntimeCause::CallContractMismatch, | ||
| E::FillBudgetExceeded { .. } => WitnessRuntimeCause::FillBudgetExceeded, | ||
|
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more.
When an admitted fill crosses the CPU ceiling, Useful? React with 👍 / 👎. |
||
| // The five that should never arrive. See the type comment. | ||
| E::HostToolUnresolved { .. } | ||
| | E::HermeticHostEffectRefused { .. } | ||
|
|
||
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This enum is documented as a one-for-one mirror of
gunbc.observation_ci_render.CiWitnessRuntimeCause, but the authoritative enum indag/gunbc/observation_ci_render.dag:831-851and its token function have no fill-budget arm. Rust can therefore emitcause=fill-budget-exceededwhile the modeled renderer and consumers cannot construct or recognize the corresponding cause, leaving the mirror/parity contract incomplete; add the modeled variant and token alongside this Rust arm.Useful? React with 👍 / 👎.