Skip to content
Merged
Show file tree
Hide file tree
Changes from 10 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
71 changes: 71 additions & 0 deletions dag/gunbc/guarantee_stall/floor_cost_basis_boundedness_stall.dag
Original file line number Diff line number Diff line change
@@ -0,0 +1,71 @@
module gunbc.guarantee_stall.floor_cost_basis_boundedness_stall

import gunbc.guarantee_rung { OutsideTheLadder, StructurallyGuaranteed }
import gunbc.guarantee_stall { GuaranteeStall, AwaitsOneGrounding, UncountedNotEnumerable }

// NO MEASUREMENT CAMPAIGN CAN DISCHARGE THIS ARM, AND THAT IS WHY IT IS A STALL RATHER THAN UNBUILT
// WORK. `gunbc.rung_drop.floor_cost_claim_qualification_unavailable` states that its restoration
// trigger's conjunct (ii) requires the cost basis to be INVARIANT OR BOUNDED BY CONSTRUCTION. The
// invariance arm is measured and REFUTED. This row is about the other arm, at its own subject grain
// -- not the whole disjunction, because collapsing the two is the exact defect gunbc#10260 repaired
// in that row's own text, and repeating it here would reintroduce it one file away.
//
// THE REACHABILITY RESULT, which is what makes the blocker AwaitsOneGrounding rather than
// ClimbableButUnbuilt. For observed pairwise ratios r1..rn with M = max(r1..rn), the evidence
// establishes only that every bound K valid for those observations satisfies K >= M. Adding samples
// may leave M unchanged or RAISE it; it cannot establish `for every admitted execution pair, ratio
// <= K`. So an observed maximum is a FLOOR on any valid bound, never a bound -- and a percentile, a
// confidence interval, or a long run of non-exceedances is not a substitute for a construction-
// derived one. The rung_drop row already says this of one measurement; what is recorded here is the
// general statement, so a future lane does not read that sentence as an invitation to sample more
// hosts. A 12-run campaign reporting a worst-observed 2.280x is exactly the artifact that would be
// offered, and it does not touch the arm.
//
// WHY THE PREREQUISITE IS A GROUNDING AND NOT AN IMPLEMENTATION: there is no closed admitted
// envelope with every basis-varying component accounted for, so the work is not a decided
// construction merely unstarted -- it is unspecifiable until that authority exists. The four
// conjuncts below are ONE conjunctive grounding, not four alternative routes, and the trigger says
// so, because a trigger satisfiable by any one of them would retire this row with the capability
// still dead -- the section 4b(3) grain mismatch, arriving here as a section 4b(2) trigger.
//
// CEILING IS GUARANTEED AND NOT IMPOSSIBLE: a bound derived from admitted components and caps is a
// proof from modeled structure, but an execution that exceeds it stays authorable. What the climb
// removes is the silent acceptance, not the ability to write the program.
//
// CURRENT IS OutsideTheLadder, AND THE READING THAT MADE IT `Mitigatable` WAS RUNG INFLATION ACROSS A
// SUBJECT BOUNDARY. This row first cited the drop row's `acceptance still fail-closed` clause as
// though it spoke for THIS arm. It does not: that clause is about attempt safety and verdict
// availability, which are a neighbouring path. Read the deciding consumer instead of the prose --
// `v2.workflow.required_floor.claim_safety_outcome` takes seven parameters, none of which is or
// derives from any construction-bound authority, and branches only on `reached_verdict`, then
// `observed_cpu_ms` against `cpu_limit_ms`, then `observed_wall_ms` against `wall_limit_ms`. So the
// absence of the boundedness arm accompanies `CompletedWithinSafetyLimits` and
// `CompletedPastSafetyLimit` ALIKE, and no output of that function varies with it. A refusal there is
// evidence that one execution crossed an attempt-safety limit, never that the arm is missing.
//
// Nothing observes this arm and nothing blocks on it, so no harm is contained at its own grain and
// rung one is not occupied. Section 4b makes a class's current rung the MINIMUM over its in-scope
// paths, so the fail-closed neighbour cannot raise this silent one. The same standard is already
// applied one module away: `v2.workflow.required_floor`'s PREEMPTION-1 drop rules that for an
// `OpaqueHostCallUnbounded` claim the two limits `are not even mitigatable -- they observe nothing
// and block nothing at the moment the cost accrues`. This row now holds itself to the rule its
// neighbour states rather than to a sentence quoted from a different subject.
//
// AND WHY THIS IS A STALL RATHER THAN A SECOND DROP, which the drop row settles in its own words:
// `PREVIOUS RUNG: none for environment-independent claim-cost qualification -- that guarantee was
// never held, and saying it was would be inventing a rung to drop from.` Nothing was lost, so a
// drop's previous/temporary/reason fields have no answer here. The two rows are also different
// facts: the drop states the standing unavailability, this states that one named restoration
// conjunct is unreachable BY MEASUREMENT and what would reach it.
data floor_cost_basis_boundedness_stall: GuaranteeStall = GuaranteeStall {
subject: "the BOUNDEDNESS-BY-CONSTRUCTION arm of conjunct (ii) of gunbc.rung_drop.floor_cost_claim_qualification_unavailable's restoration trigger: repeated execution measurement cannot establish it, because every observed maximum is a LOWER bound on the smallest valid bound rather than an upper bound over the admitted envelope",
current: OutsideTheLadder,
ceiling: StructurallyGuaranteed,
blocker: AwaitsOneGrounding {
grounding: "a typed construction-bound authority for the declared basis and subject grain, consumed by the required-floor verdict at that same grain, which (1) closes the admitted execution envelope; (2) accounts for every component capable of changing the basis, by removing it from the measured subject, charging it to that subject, assigning it an enforced finite cap, or refusing the envelope; (3) derives a finite bound from those admitted components and caps rather than from an observed sample maximum; and (4) carries discriminating execution evidence over the admitted corner cases plus an over-bound control refused on the real acceptance path"
},
population: UncountedNotEnumerable {
reason: "the subject is ONE ARM of conjunct (ii) of a restoration trigger authored as prose inside gunbc.rung_drop.floor_cost_claim_qualification_unavailable. The population this carrier reports is the EXPOSURE, not a roster of the source artifacts that carry or discuss the subject, and the exposed set here is every required identity for which the CPU deadline is armed, derived per run. That set is produced by execution rather than declared in source, so no authored list in this standing row would be true when written. It is finite, not mathematically infinite, and a run may well emit its own occurrence roster; what does not exist is a stable source-level authority this row could name. TWO EARLIER REVISIONS OF THIS FIELD WERE WRONG IN DIFFERENT WAYS, recorded because the second failure is the instructive one. The first list named gunbc.floor_cost_distribution.RunCost.eval_steps, a field that does not exist -- RunCost declares run and rows -- so its BoundedPopulation was not an identity join and the bound was never real. The second revision substituted a symbol that does exist, v2.workflow.required_floor.claim_safety_outcome, and was still wrong, because the defect was the SHAPE rather than the bad member: the list enumerated CARRIERS -- an instrument column, a deciding consumer, and the parent drop -- which is one-carrier-answers-for-the-whole-population, the move `gunbc.guarantee_stall.two_nat_authorities_stall` rejects under this same StallPopulation carrier even though its own declaration half and four direct importers are perfectly enumerable. THE FUTURE BOUNDARY IS NOT A TYPED SPLIT OF THE PARENT TRIGGER. Giving the arm a typed source identity would make the SUBJECT referable and may be worth doing on its own, but it neither enumerates the exposed required identities nor is needed to; naming that new arm identity here would repeat the same rejected move one level down. What would permit an honest BoundedPopulation is a typed PRODUCER of the exposed population at this grain -- a derivation joining a run's required-identity dispositions to the CpuDeadlineArmed policy, or another closed authority that enumerates every affected identity",
},
next_rung_trigger: "the construction-bound authority named in this row's grounding EXISTS and is CONSUMED by the required-floor verdict at the declared subject grain, with its over-bound control refused on the real acceptance path; no volume of execution sampling retires this row, and a widening of the measurement campaign does not move it"
}
2 changes: 2 additions & 0 deletions dag/gunbc/guarantee_stall/roster.dag
Original file line number Diff line number Diff line change
Expand Up @@ -41,6 +41,7 @@ import gunbc.guarantee_stall.external_model_scope_live_cover_stall { external_mo
import gunbc.guarantee_stall.observation_heartbeat_lockstep_stall { observation_heartbeat_lockstep_stall }
import gunbc.guarantee_stall.operation_argv_binding_wall_stall { operation_argv_binding_wall_stall }
import gunbc.guarantee_stall.roster_re_enumerates_its_own_rows_stall { roster_re_enumerates_its_own_rows_stall }
import gunbc.guarantee_stall.floor_cost_basis_boundedness_stall { floor_cost_basis_boundedness_stall }

// THE COHORT PROVENANCE NOTES BELOW WERE AUTHORED WHEN EVERY ROW SAT IN ONE FILE, and they are
// carried here verbatim rather than split across the row modules they describe. Their membership
Expand Down Expand Up @@ -141,6 +142,7 @@ data all_guarantee_stalls: List<GuaranteeStall> = [
observation_heartbeat_lockstep_stall,
operation_argv_binding_wall_stall,
roster_re_enumerates_its_own_rows_stall,
floor_cost_basis_boundedness_stall,
]

// THE FOUR SUBJECTS RESTORED TO THE ROSTER, PINNED BY IDENTITY SO THEIR LOSS REFUSES.
Expand Down
Loading