diff --git a/dag/gunbc/guarantee_stall.dag b/dag/gunbc/guarantee_stall.dag index 47be6dc9ac0..2aac34d1120 100644 --- a/dag/gunbc/guarantee_stall.dag +++ b/dag/gunbc/guarantee_stall.dag @@ -1,12 +1,8 @@ module gunbc.guarantee_stall import std.types { String, List, Bool, Int } -import v2.std.algebra { Cons, Empty, fold_list } -import gunbc.guarantee_rung { - GuaranteeRung, OutsideTheLadder, Mitigatable, MechanicallyPreventable, - StructurallyGuaranteed, StructurallyImpossible, - guarantee_rung_label, guarantee_rung_index, -} +import v2.std.algebra { fold_list } +import gunbc.guarantee_rung { GuaranteeRung, guarantee_rung_label, guarantee_rung_index } // THE CARRIER FOR A DESIGN section 4b(2) STALL, and it is a different fact from a section 4b(3) // DROP (gunbc.rung_drop) rather than a variant of it. A DROP is an event: something that held a @@ -44,6 +40,15 @@ import gunbc.guarantee_rung { // makes nothing unwritable about prose: a class stalling in an annotation stays exactly as // writable as it was, and nothing detects one. That is a scope statement, not a climb, and stating // it here is what keeps a reader from counting this module as coverage it does not provide. +// +// THIS MODULE CARRIES THE SHAPE AND THE FOLDS; THE ROWS ARE ONE MODULE EACH under +// gunbc.guarantee_stall., and gunbc.guarantee_stall.roster is the enumeration. The split is +// the one gunbc#10206 made for gunbc.recurring_failure_mode and it is made here for the same +// measured reason: every row PR appended at the same two points -- the declaration tail and the +// roster tail -- so row lanes conflicted with each other BY CONSTRUCTION, and no amount of timing +// changes that. Appending a stall now writes a new file and one roster line. The direction is +// forced by acyclicity rather than chosen: a row module imports GuaranteeStall from here, so the +// enumeration cannot live here. // THE THREE-WAY DISTINCTION section 4b(2) NAMES, modeled as a closed coproduct because that is // what makes "only the first is permanent" a fold rather than a reading. AwaitsOneGrounding @@ -115,653 +120,6 @@ fn stall_report_message(s: GuaranteeStall) -> String { ) } -// THE FIRST ROW IS THIS MODULE'S OWN CLASS, and it is homed here for the reason every other row is -// homed with its class: the stall is in the stall machinery itself, whose authority is this file. -// The population is UncountedNotEnumerable rather than the 133 sites the sweep found, deliberately. -// A measured figure copied into a row is a transcription of an instrument's output, which this -// repository rules against, and it would additionally be the wrong number: 133 counts PHRASE -// OCCURRENCES, and a class that mentions its trigger three times is one stall, while a witness -// asserting the phrase is none. The population has no identity to count at, and that is the finding -// rather than a gap in the sweep. -// A REFERENCE THAT RESOLVES UNDER ONE IMPORT LIST AND REFUSES UNDER A SUPERSET OF IT. -// Filed as a class because the specimen is user-visible and nobody had filed it: adding an import -// of an UNRELATED module silently breaks a bare reference that resolved without it. The failure is -// loud at the reference -- an undefined-variable diagnostic -- but the CAUSAL relation is -// unreachable from it, since nothing in the message connects the new import line to the broken -// name and no author's model of what an import does predicts it. Loud failure with an unreachable -// cause is the shape that costs the most time per incident. -// -// MECHANISM, measured rather than inferred. cli_run build_both_closure_edge_index skips a file -// before populating bare_out for it when source_declares_import_lines is true, and the struct -// field's own doc calls bare_scan_eligible the import-stripped files that may originate -// bare-reference edges. So a bare reference is a closure edge ONLY from a zero-import file. -// Confirmed by discriminator rather than by reading the predicate: one four-file fixture, one -// binary, one line varied -- with no import the provider is pulled and the name resolves clean; -// with one import of an unrelated carrier the provider is not pulled and the name refuses. -// -// WHY THE CEILING IS GUARANTEED AND NOT IMPOSSIBLE: eligibility is decided from the file text the -// compiler already holds, so a closure relation that does not vary with import-declaration is -// derivable. It is not IMPOSSIBLE, because both programs remain writable -- the source can express -// a file with imports and one without; what a repair removes is the DIVERGENCE between them, not -// the ability to author either. -// ON THE GROUNDING FIELD, recorded because the first version of this row got it wrong in a way -// nothing in this repository would have caught. It cited "the ClosureBoundResolution ruling" as -// the authority the class waits on. No such authority exists: the name was coined in cross-session -// correspondence and its only occurrences in the tree were this row and its own trigger. That is -// DESIGN section 3's cite-the-symbol violation in its purest form -- a citation naming a symbol -// that does not resolve -- and it is the exposure the 2026-08-23 cited-symbol drop declared as -// unbounded, arriving inside two days of the census being decommissioned. Caught by review 55910, -// which is the mitigation that drop names and is strictly weaker than the wall it replaced. -// -// THE FINDING DOES NOT CARRY THE RECLASSIFICATION IT PROPOSED, and the distinction is the point of -// the coproduct. The review concluded that an unauthored authority makes this ClimbableButUnbuilt. -// It does not: waiting on a DECISION and waiting on CONSTRUCTION rank differently for work, and -// this class genuinely waits on the first -- the repair direction is undetermined, so building is -// not merely unstarted but unspecifiable. What the finding correctly kills is the pretence that -// the decision had a home. A blocker may name an open question; it may not name a phantom ruling. - -// TWO Nat AUTHORITIES ARE ONE NAME ANSWERING FOR TWO CONCEPTS, and this row exists because review -// 57758 correctly refused a version of it that was narrated in prose beside one of the two nat_max -// declarations. The fork predates this lane; what this lane changed is that the Peano side now -// carries real operations, so the fork is load-bearing rather than latent. -// -// ClimbableButUnbuilt, NOT AwaitsOneGrounding, and review 57807 was right to refuse the first -// version of this row for saying otherwise. The modeling direction is already decided and its -// prerequisites discharged: gunbc.plans.dag_v2_defork_audit records the nat census complete with -// the per-concept design DESIGN READY (FreeMonoid shadow #6341 merged, generic-alias coproduct -// keystone green) and names the atomic wave file-by-file -- dag/std/nat.dag takes the coproduct and -// the Peano ops, the semiring alias is deleted, v2.std.nat becomes a thin reimport plus the law -// roster, integer and float repoint GroupCompletion to std.nat.Nat, every importer in the same -// push. Classifying that as awaiting a ruling would convert scheduled work into an indefinite -// decision stall, which is exactly the untracked stall DESIGN section 4b forbids, and would dilute -// the canonical plan by implying the question is still open. -data two_nat_authorities_stall: GuaranteeStall = GuaranteeStall { - subject: "std.nat Nat (CommutativeSemiring, realizing natively as a machine scalar) and v2.std.nat Nat (the Peano coproduct Zero | Succ) are two declarations answering for one name, so nat_add / nat_mul / nat_max / nat_compare each exist twice and a bare reference in a closure containing both modules is ambiguous", - current: Mitigatable, - ceiling: StructurallyImpossible, - blocker: ClimbableButUnbuilt, - population: UncountedNotEnumerable { - reason: "the declaration half IS enumerable -- std.nat and v2.std.nat both declaring Nat, with the per-operation forks nat_add / nat_mul / nat_max / nat_compare that no single function can serve because the two are different types -- but the exposure half is not, and one carrier answers for the whole population. The exposed set is every reference site whose CLOSURE contains both modules, and closure membership is transitive: a module importing one neighbour that reaches std.nat and another that reaches v2.std.nat has both without importing either. So a direct-import scan is not that set -- it currently names four dual-importing files and understates the real exposure -- and rendering those four as a BoundedPopulation would read as bounded while measuring the wrong property, which is the empty-observation narrow this carrier's second variant exists to prevent. It is bounded in principle by the corpus and shrinks to zero with the trigger below, but no enumeration here would be true when written", - }, - next_rung_trigger: "the atomic Nat unification wave specified in gunbc.plans.dag_v2_defork_audit: dag/std/nat.dag carrying the coproduct and the Peano operations with the semiring alias deleted, v2.std.nat reduced to a thin reimport plus the node-bound law roster, integer and float repointing GroupCompletion to std.nat.Nat, and every importer repointed in the same push -- retired by that wave landing and by nothing less, since deleting either declaration without deriving its operations would remove the operations its consumers call rather than unify the authority" -} - -data import_eligibility_resolution_stall: GuaranteeStall = GuaranteeStall { - subject: "a bare reference resolves under one import list and refuses under a superset of it, because bare-reference closure edges originate only from zero-import files", - current: Mitigatable, - ceiling: StructurallyGuaranteed, - blocker: AwaitsOneGrounding { - grounding: "an undecided QUESTION, stated here rather than cited, because no authority in this tree answers it yet: is candidacy for a subject asked against the CENSUS population or the CLOSURE population. The class cannot climb until that is decided, because the repair direction depends on the answer -- bounding lookup leaves the loader still admitting providers by bare reference, and bounding load changes which files enter the subject at all. So this stall waits on a DECISION rather than on construction, which is what separates it from ClimbableButUnbuilt -- and the separation is structural rather than a matter of degree: the two answers land in DIFFERENT LANES, bounding lookup being a semantic-authority repair and bounding load a proof-authority one, so the answer decides WHO BUILDS as well as WHAT. That is why the work here is not merely unstarted but UNSPECIFIABLE, and why filing this as ClimbableButUnbuilt would be worse than imprecise: it would tell a reader to go build something at a moment when no owner can be named, converting a blocked decision into misdirected effort. The question was coined in cross-session correspondence under a name that has no carrier here, and naming it as though a ruling existed would have been a citation to a symbol that does not resolve" - }, - population: UncountedNotEnumerable { - reason: "the AFFECTED population is references whose resolution would change, and nothing enumerates them -- a reference that resolves today emits no diagnostic to count and a reference that refuses is indistinguishable in the message from a genuinely absent declaration. What CAN be measured is the ELIGIBLE FILE count -- .dag files carrying no import line -- and that is a denominator for where the mechanism can ORIGINATE, never a count of what it affects. Quoting the eligible count as the class size is the conflation this row exists to prevent. No figure is carried here, and the omission is deliberate rather than an oversight: the count is a minority of the corpus that MOVES with every merge, no entry point re-derives it, and a transcribed number is a positional citation of a run's output -- unreachable from the thing that owns it, so it rots without anyone touching either end. A row whose whole subject is that a number is the WRONG denominator would be the worst possible place to freeze that number into source. The eligible count is also RISING by construction: the namespace cut takes modules to zero imports, so each wave switches bare-edge origination on for the modules it strips" - }, - next_rung_trigger: "the census-or-closure candidacy question is decided AND its answer lands as a namespace-cut PREREQUISITE rather than a post-cut repair, bounding which modules may supply a resolution candidate for a subject. Reclassified from post-cut to prerequisite because the cut is what makes the mechanism universal -- a repair scheduled after the event that generalises it is scheduled backwards. Not satisfied by bounding lookup alone: the closure constructor extends by bare reference to a fixpoint before any lookup runs, so a wall placed only at lookup sits downstream of the door that already opened" -} - -data next_rung_trigger_enforcement_stall: GuaranteeStall = GuaranteeStall { - subject: "DESIGN section 4b(2) next-rung trigger enforcement", - current: Mitigatable, - ceiling: MechanicallyPreventable, - blocker: ClimbableButUnbuilt, - population: UncountedNotEnumerable { - reason: "a next-rung trigger is authored as prose, so it has no identity to count at. The majority of sites sit inside // annotations, which DESIGN section 4c makes unreadable to any Accepted program, so no lens can enumerate them however it is written -- the shortfall is the representation, not the sweep" - }, - next_rung_trigger: "every class this repository declares below its ceiling declares it through gunbc.guarantee_stall GuaranteeStall rather than in prose, at which point the population becomes a fold over rows and a stall missing its trigger has no spelling. Not satisfied by this carrier existing: one row is a carrier with a consumer, not a migrated population, and the 4b(2) obligation stays review diligence for every class still stalling in an annotation" -} - -// DECLINED-LIVE-TREE CENSUS, observed by required-floor run 32882641450 after the root decline -// stopped hiding these subjects. The fifteen executing identities below project TEN facts. They -// are stalls rather than drops: no guarantee stopped holding in this change; the facts were outside -// the ladder because no required consumer executed them. `ClimbableButUnbuilt` states that each -// repair is specifiable. Assignment is a dashboard routing fact and deliberately does not live in -// this semantic carrier. - -// THE GENERATED-ARTIFACT REGISTRY IS GUARDED INDIRECTLY, AND THIS ROW EXISTS BECAUSE THE MUTATION -// WAS RUN RATHER THAN REASONED ABOUT. Deleting a member from generated_artifact_registry and -// running the gate produced EXACTLY ONE finding, and it was `.gitattributes` drift -- the -// merge-driver enrollment projection enumerates registry members, so dropping one changes its -// bytes. Nothing said what an author would actually want said: that a COMMITTED file at a -// generated location is now adjudicated by nobody. The wall is real and it is one step removed -// from its subject, so an artifact excluded from the .gitattributes projection for any reason -// would leave the registry silently. Current rung is the honest one for a guard that holds by -// side effect; the trigger names the direct capability, a census joining committed files at -// generated-artifact locations back to registry membership, because a guard that answers about -// enrollment bytes is not the guard that answers about orphaned artifacts. -// FILED AS A STALL AND NOT AS A RUNG DROP, WHICH IS A CORRECTION TO THIS SUBJECT'S FIRST FILING -// ON THIS BRANCH (2026-09-03). A section 4b(3) drop ASSERTS A REGRESSION -- a change lowered a rung -// that was held -- and nothing here regressed. GitHub's required-status-checks rule has evaluated -// reported check runs the same way since ruleset 16178731 was created, so the capability below was -// NEVER held and declaring a previous rung of `MechanicallyPreventable` would be inventing a rung -// to drop from, exactly as `gunbc.rung_drop` `floor_cost_claim_qualification_unavailable` refused -// to do for its own subject. What actually existed was section 4b(1) rung INFLATION: this -// repository's "required lane" vocabulary, and `gunbc.merge_lifecycle`'s own prose naming -// `PerPrGateOnly` the live policy, described a wall that does not stand for an unreported context. -// The inflation is corrected in `gunbc.merge_admission` by making the live policy representable; -// what remains is a class below its ceiling, which is a 4b(2) stall and belongs here. -// -// THE OPERATOR HAS RULED, AND THAT IS WHY THE BLOCKER IS `ClimbableButUnbuilt` RATHER THAN A -// MISSING CAPABILITY. Escalated 2026-09-03 with three options -- enable the merge queue, make -// unreported required contexts blocking, or hold the hole open -- and the ruling was the third: -// "Leave the hole open for now - i know merging is not sound." That is an INFORMED ACCEPTANCE by -// the principal who can actuate the fix, recorded in those terms deliberately. A row whose reason -// reads "we could not fix this" ages into an excuse; one that records a decision taken with the -// population in view stays a decision, and can be revisited by the person who took it. Nothing in -// this repository can actuate it in any case: the branch-protection and rule-suites endpoints -// answer 403 to session tokens. -// -// WHAT IT COST, ON THE NIGHT IT WAS DECLARED, BECAUSE "for now" IS ONLY HONEST BESIDE ITS PRICE. -// gunbc#10236 merged at 19:49:43Z, three seconds after its `witnesses` run was created and before -// any job reported; that run concluded with `required-witnesses-build` and -// `required-witnesses-floor` both FAILURE, and the head landed as cfe19ea7 carrying two duplicate -// declarations that refused main at resolve. main stayed refusing until the repair merged. -// -// AND THE SECOND COMMIT THAT LANDED BROKEN THAT NIGHT CAME THROUGH THE OTHER HOLE, NOT THIS ONE -- -// stated because conflating them would inflate this row. gunbc#9981 merged at 20:29:53Z with a -// `witnesses` run on its own head that had COMPLETED SUCCESSFULLY at 20:26:54Z, so it is not this -// class. Its run was created at 19:37:37Z, twelve minutes before cfe19ea7 landed, so it carried a -// green receipt at a base that no longer existed and squashed onto a broken tip. That is -// `gunbc.merge_lifecycle`'s stale-base class -- admitted under `PerPrGateOnly`, refused under -// `KeyedReceipt` as `MergeDeniedStaleBase` -- whose standing instruction is to add a line rather -// than escalate, and the line is added there. TWO HOLES, ONE EACH, FORTY MINUTES APART. -data merge_admission_terminal_verdict_stall: GuaranteeStall = GuaranteeStall { - subject: "a merge into main lands a head that no required context has reached a terminal verdict on", - current: Mitigatable, - ceiling: StructurallyGuaranteed, - blocker: ClimbableButUnbuilt, - population: UncountedNotEnumerable { reason: "every future merge into refs/heads/main is exposed, so the population is open rather than a list. IT IS STILL MEASURABLE, AND THE PREDICATE IS THE INSTRUMENT RATHER THAN ANY COUNT: for a merged pull request, did a required `witnesses` run on ITS OWN head reach a terminal verdict before its `merged_at`. That predicate is decidable per merge from the runs and pulls endpoints and can be re-measured at any time; a reading of it on 2026-09-03 over the forty most recently merged pull requests found six that had none. THE SIX ARE A READING, NOT THE POPULATION, and this row states the difference because its neighbour `gunbc.rung_drop` `floor_cost_claim_qualification_unavailable` had to correct itself for exactly that conflation: a set selected by a measurement is a VIEW whose membership is a property of the measurement, and letting it stand in for the population joins two objects by an assumption. A frozen count would also be a change detector rather than an instrument -- automating its update collapses it to measure() == measure()" }, - next_rung_trigger: "NO HEAD LANDS ON main WITHOUT A TERMINAL VERDICT FROM EVERY REQUIRED CONTEXT ON THE CONTENT BEING MERGED -- terminal rather than merely non-failing, because the state this row is about is a context that has reached NO VERDICT AT ALL at the instant of the merge, and a trigger reading `every required context reported non-failure` is satisfied by that state vacuously. Demonstrated by a RED on a merge attempted before its run reports, not by a configuration screenshot. TWO ARTIFACTS WOULD DELIVER IT AND NEITHER IS THE TRIGGER: GitHub's merge queue, which establishes it by construction because the queue runs the required workflow on the queued ref and nothing lands without that run; or making an unreported required context blocking. IF EITHER IS NAMED IN A LATER CLAIM THAT THIS STALL HAS CLIMBED, THE CLAIM MUST STATE WHAT THE ARTIFACT WAS SUFFICIENT FOR -- enabling a queue for one branch pattern while the pull-request path stays merge-able past an unreported context satisfies the artifact and leaves the capability dead, which is the grain mismatch a corpus-shaped loss with a setting-shaped trigger always produces" -} - -data generated_artifact_registry_membership_stall: GuaranteeStall = GuaranteeStall { - subject: "a committed generated artifact leaves generated_artifact_registry and stops being adjudicated", - current: MechanicallyPreventable, - ceiling: StructurallyGuaranteed, - blocker: ClimbableButUnbuilt, - population: BoundedPopulation { members: Cons { head: "gunbc.generated_artifact generated_artifact_registry", tail: Cons { head: "gunbc.generated_artifact_merge_driver", tail: Empty {} } } }, - next_rung_trigger: "a census that enumerates committed files at every artifact_location and refuses one with no generated_artifact_registry member, so registry departure is refused by its own subject rather than by .gitattributes drift" -} - -data doc_graph_orphan_population_stall: GuaranteeStall = GuaranteeStall { - subject: "the derived documentation graph contains orphan documents", - current: OutsideTheLadder, - ceiling: MechanicallyPreventable, - blocker: ClimbableButUnbuilt, - population: BoundedPopulation { members: Cons { head: "test.claim.doc_reachability_witness.doc_graph_has_no_orphan_docs", tail: Cons { head: "v2.test.lens_doc_reachability.doc_reachability_test.doc_graph_has_no_orphan_docs", tail: Cons { head: "v2.test.lens_doc_reachability.doc_reachability_test.doc_graph_is_clean", tail: Empty {} } } } }, - next_rung_trigger: "the derived orphan-document identity population is empty and every enrolled projection reports NowPassing" -} - -data doc_graph_dangling_link_population_stall: GuaranteeStall = GuaranteeStall { - subject: "the derived documentation graph contains dangling links", - current: OutsideTheLadder, - ceiling: MechanicallyPreventable, - blocker: ClimbableButUnbuilt, - population: BoundedPopulation { members: Cons { head: "test.claim.doc_reachability_witness.doc_graph_has_no_dangling_links", tail: Cons { head: "v2.test.lens_doc_reachability.doc_reachability_test.doc_graph_has_no_dangling_links", tail: Cons { head: "v2.test.lens_doc_reachability.doc_reachability_test.doc_graph_is_clean", tail: Empty {} } } } }, - next_rung_trigger: "the derived dangling-link identity population is empty and every enrolled projection reports NowPassing" -} - -data enforcement_live_closure_gate_stall: GuaranteeStall = GuaranteeStall { - subject: "the live enforcement closure and its question-zero gate are non-green", - current: OutsideTheLadder, - ceiling: MechanicallyPreventable, - blocker: ClimbableButUnbuilt, - population: BoundedPopulation { members: Cons { head: "v2.test.claim.enforcement.lens_module_gate_witness.lens_closure_question_zero_holds_live", tail: Cons { head: "v2.test.claim.enforcement.lens_module_gate_witness.lens_module_gate_holds_live", tail: Cons { head: "v2.test.claim.enforcement.lens_module_gate_witness.question_zero_verdict_live_holds", tail: Empty {} } } } }, - next_rung_trigger: "the live closure question returns zero and both gate projections report true" -} - -data mandatory_tag_live_corpus_stall: GuaranteeStall = GuaranteeStall { - subject: "the live corpus contains a mandatory-tag violation", - current: OutsideTheLadder, - ceiling: MechanicallyPreventable, - blocker: ClimbableButUnbuilt, - population: BoundedPopulation { members: Cons { head: "v2.lens.mandatory_tag.corpus_scan_witness_test.corpus_live_clean_tree_wall_holds", tail: Empty {} } }, - next_rung_trigger: "the derived mandatory-tag violation population is empty" -} - -data parse_ingest_grammar_relation_stall: GuaranteeStall = GuaranteeStall { - subject: "parse and ingest disagree over the same grammar round trip", - current: OutsideTheLadder, - ceiling: StructurallyGuaranteed, - blocker: ClimbableButUnbuilt, - population: BoundedPopulation { members: Cons { head: "v2.test.execution.emit_ingest_grammar_relation_round_trip.same_grammar_parse_ingest_bridge_holds", tail: Empty {} } }, - next_rung_trigger: "the same-grammar parse-to-ingest round trip holds" -} - -// The candidate-tree producer drop is retired separately in gunbc.rung_drop: executed clean and -// drift arms both produced and named the candidate before adjudication. That restoration does not -// make the hand-maintained host mirror structural. Keeping this as its own stall prevents a new -// climb obligation from extending the lifetime of the retired producer drop. -data required_regen_host_derivation_stall: GuaranteeStall = GuaranteeStall { - subject: "required-regen host ordering is hand-maintained beside its modeled carrier", - current: Mitigatable, - ceiling: StructurallyGuaranteed, - blocker: ClimbableButUnbuilt, - population: BoundedPopulation { members: Cons { head: "v1_compiler.required_regen_host.run_required_regen", tail: Empty {} } }, - next_rung_trigger: "v1_compiler.required_regen_host run_required_regen is derived from v2.workflow.required_regen required_regen_run, with that derivation SUFFICIENT FOR preserving the carrier's exhaustive verdict mapping: every host verdict after successful emission carries the CandidateTree adjudicated for that verdict, and only an emission that produced no tree reaches a tree-less host arm. A generator that merely emits the host, or agreement on one verdict arm, does not satisfy this trigger; the whole host mapping must be constructed from the carrier so candidate production before adjudication has one authority rather than a modeled carrier and a hand-maintained host mirror" -} - -data self_host_candidate_generation_add_slice_stall: GuaranteeStall = GuaranteeStall { - subject: "self-host candidate generation, translation, and emission disagree on the add slice", - current: OutsideTheLadder, - ceiling: MechanicallyPreventable, - blocker: ClimbableButUnbuilt, - population: BoundedPopulation { members: Cons { head: "v2.test.execution.self_host_candidate_generation.candidate_generation_translate_self_emit_dag_add_slice_holds", tail: Cons { head: "v2.test.execution.emit_ingest_python_same_language_round_trip.emit_ingest_python_same_language_round_trip_holds", tail: Cons { head: "v2.test.execution.emit_ingest_python_same_language_round_trip.python_same_language_source_emit_round_trip_holds", tail: Cons { head: "v2.test.execution.emit_ingest_typescript_same_language_round_trip.emit_ingest_typescript_same_language_round_trip_holds", tail: Cons { head: "v2.test.execution.emit_ingest_typescript_same_language_round_trip.typescript_same_language_source_emit_round_trip_holds", tail: Empty {} } } } } } }, - next_rung_trigger: "candidate generation, translation, and self-emission agree on the add slice: infer derives grounding for the Arrow, Conj and Atom kinds of the add fn, so cross_language_compile stops carrying infer_grounding_not_derived over the same-language python and typescript parse fixtures" -} - -data non_fold_residue_roster_stall: GuaranteeStall = GuaranteeStall { - subject: "the live non-fold residue contains an unrostered or stale identity", - current: OutsideTheLadder, - ceiling: MechanicallyPreventable, - blocker: ClimbableButUnbuilt, - population: BoundedPopulation { members: Cons { head: "v2.test.lens_non_fold_residue.non_fold_residue_test.non_fold_residue_no_unrostered_or_stale", tail: Empty {} } }, - next_rung_trigger: "the derived unrostered and stale non-fold-residue populations are both empty" -} - -data retained_rust_live_tree_migration_stall: GuaranteeStall = GuaranteeStall { - subject: "live Rust-test discovery disagrees with the retained-kernel migration authority", - current: OutsideTheLadder, - ceiling: MechanicallyPreventable, - blocker: ClimbableButUnbuilt, - population: BoundedPopulation { members: Cons { head: "v2.test.lens_test_migration_debt.test_migration_debt_test.retained_rust_kernel_wall_holds_against_live_tree", tail: Empty {} } }, - next_rung_trigger: "live Rust-test discovery and the retained-kernel authority join exactly" -} - -// REQUIRED-FLOOR RUN 32918791246 exposed these four pre-existing facts after the -// DeclinedLiveTree arm stopped withholding their nine witness identities. None of their carriers -// is changed by that deletion. They are declared rung drops rather than expected-red enrolments: -// the witnesses remain ordinary, executing failures until the separately routed repair lands. -// The work-item identity is part of each next-rung trigger, so ownership survives a squash merge -// beside the bounded population and the semantic condition that ends the drop. - -// THE THREE CITED WORK ITEMS ARE ALREADY status=done AND THEIR CONDITIONS ARE NOT MET, measured -// 2026-08-28 against the dashboard and against required-floor run 33140608194. adhoc-89fcf94a-bdd, -// adhoc-3cb769e0-0a6 and adhoc-a3b0e05f-374 all report done, while frontier_cover_of_live_extdeps_tree_holds -// is one of that run's 47 FAIL rows and a direct count puts 21 live dag/extdeps modules outside the -// scope frontier's union of scope_carrier_paths, scope_machinery_exempt_paths and the legacy manifest. -// So the node ids are PROVENANCE for who was asked, never evidence that the climb happened: a closed -// work item beside an unmet condition is the reported-results-versus-committed-claims gap, and reading -// "it lands" as satisfied would inflate three classes that are still at the bottom of the ladder. -// EACH TRIGGER'S OPERATIVE HALF IS THE SEMANTIC CLAUSE AFTER THE COLON, which is what a later reader -// must re-measure; the rows are authored that way and survive their work items unchanged. -data external_model_scope_live_cover_stall: GuaranteeStall = GuaranteeStall { - subject: "the live external-model scope cover does not cover the extdeps tree", - current: OutsideTheLadder, - ceiling: MechanicallyPreventable, - blocker: ClimbableButUnbuilt, - population: BoundedPopulation { members: Cons { head: "test.claim.external_model_scope_live_cover_witness.frontier_cover_of_live_extdeps_tree_holds", tail: Empty {} } }, - next_rung_trigger: "node://adhoc-89fcf94a-bdd lands: the live extdeps-tree cover is exact and its routed witness returns true" -} - -data observation_heartbeat_lockstep_stall: GuaranteeStall = GuaranteeStall { - subject: "the observation heartbeat implementation and its declared cadence are out of lockstep", - current: OutsideTheLadder, - ceiling: StructurallyGuaranteed, - blocker: ClimbableButUnbuilt, - population: BoundedPopulation { members: Cons { head: "test.claim.observation_lockstep_witness_test.w_heartbeat_period_matches_the_seed_cadence", tail: Cons { head: "test.claim.observation_lockstep_witness_test.w_heartbeat_source_still_refuses_to_fabricate", tail: Empty {} } } }, - next_rung_trigger: "node://adhoc-3cb769e0-0a6 lands: the heartbeat period is derived from one declared cadence and the source refuses fabricated heartbeat observations" -} - -data operation_argv_binding_wall_stall: GuaranteeStall = GuaranteeStall { - subject: "the operation-argv binding wall does not materialize the previously unbindable operation", - current: OutsideTheLadder, - ceiling: StructurallyGuaranteed, - blocker: ClimbableButUnbuilt, - population: BoundedPopulation { members: Cons { head: "test.claim.operation_argv_binding_wall_witness.operation_argv_previously_unbindable_operation_now_materializes", tail: Empty {} } }, - next_rung_trigger: "node://adhoc-a3b0e05f-374 lands: the operation-argv binding wall materializes the controlled previously-unbindable operation" -} - -data variant_owner_identity_stall: GuaranteeStall = GuaranteeStall { - subject: "runtime variant equality and native-representation selection derive from exact owner-module plus declaration identity, never parent/arm lexemes", - current: OutsideTheLadder, - ceiling: StructurallyImpossible, - blocker: ClimbableButUnbuilt, - population: BoundedPopulation { members: Cons { head: "v1_interpreter::cross_claim_memo_tests::same_spelled_variants_from_distinct_owners_reproduce_identity_residual", tail: Cons { head: "v1_interpreter::cross_claim_memo_tests::typed_bool_literals_do_not_need_lexeme_shorthands_but_zero_still_does", tail: Empty {} } } }, - next_rung_trigger: "NS-0B threads its exact owner-module plus declaration-name identity through VariantValueBinding, Value::Variant, hashing, and PortableValue::Variant; the same-spelled-owner residual changes from reproducing equality to requiring inequality, and the intentional Nat Zero native representation is selected by that identity rather than by the raw Zero lexeme" -} - -// REQUIRED-FLOOR RUN 32942047138 first executed this ReadsLiveTree carrier after #9284 landed. -// The direct byte-equality witness and its aggregate both returned false: one underlying fact, -// namely that the committed .gitattributes no longer equals its emitting authority. This is real -// generated-artifact drift, not a stale expectation. The floor cut's generated-artifact drift -// gates are currently absent, so nothing refused the authority/artifact disagreement when it was -// introduced; this bounded row keeps the two projections attached to the one repair obligation. -data gitattributes_committed_emit_drift_stall: GuaranteeStall = GuaranteeStall { - subject: "the committed .gitattributes differs from the bytes derived by its emitting authority", - current: OutsideTheLadder, - ceiling: MechanicallyPreventable, - blocker: ClimbableButUnbuilt, - population: BoundedPopulation { members: Cons { head: "test.claim.gitattributes_emit_witness.witness_committed_matches_emit_holds", tail: Cons { head: "test.claim.gitattributes_emit_witness.witness_holds", tail: Empty {} } } }, - next_rung_trigger: "node://adhoc-16f7520a-85f lands: identify the authority edit that introduced the drift, regenerate .gitattributes from that authority, and restore a required generated-artifact drift gate so later authority/artifact disagreement refuses" -} - -// THE WALL DEADLINE STILL CHARGES A SHARED-ARTIFACT FILL TO WHICHEVER CLAIM PAID IT, and this row -// exists because a comment beside the code would go stale on the day the population changes while -// this row cannot. The 2026-08-27 attribution ruling has now been applied to three homes one at a -// time -- the completion-side CPU split, the completion-side WALL split, and the CPU evaluation -// deadline -- and each application was made only after that home's omission had cost something. -// The wall deadline is the fourth home and it is unrepaired. -// -// WHY IT IS SCOPED OUT RATHER THAN FIXED HERE: measured on run 33185280160, all 44 interruptions -// are on the `Cpu` clock, 44 of 44, so the wall arm is currently unexercised. That is a fact about -// today's population and NOT about the mechanism, which is exactly why the obligation is declared -// as a countable row rather than left as a note. The trigger is deliberately an OBSERVATION rather -// than a promise: the first wall-clock interruption to appear in the floor's ledger is the event -// that makes this reachable, and it fires without anyone remembering this row exists. -data wall_deadline_shared_fill_attribution_stall: GuaranteeStall = GuaranteeStall { - subject: "the wall evaluation deadline charges shared-artifact fill to the claim that paid it, so a wall interruption is a function of discovery order rather than of the row", - current: Mitigatable, - ceiling: StructurallyGuaranteed, - blocker: ClimbableButUnbuilt, - population: BoundedPopulation { members: Cons { head: "v1_interpreter.arm_wall_deadline", tail: Cons { head: "v1_interpreter.wall_deadline_remaining_ms", tail: Cons { head: "v1_interpreter.wall_deadline_exceeded_error", tail: Empty {} } } } }, - next_rung_trigger: "the required floor's ledger reports any INTERRUPTED-BEFORE-VERDICT row whose clock is Wall, at which point the wall deadline must read a fill-netted clock exactly as v1_interpreter.budgeted_cpu_nanos does for the CPU deadline" -} - -data heterogeneous_child_list_stall: GuaranteeStall = GuaranteeStall { - subject: "a type's child list may hold BOTH a type node and a field node, and v1.04_types child_type_node tells them apart by whether `inferred` is populated -- a stamp v1.02_parse field_to_child_node writes at PARSE TIME as Resolved, before any resolution has run. A child list that mixes the two kinds makes that accessor return the FIELD node where its caller expects the TYPE, with no diagnostic", - current: OutsideTheLadder, - ceiling: StructurallyImpossible, - blocker: ClimbableButUnbuilt, - population: BoundedPopulation { - members: [ - "v1.02_parse variant_to_child_node", - "v1.02_parse outputs_to_inferred", - "v1.02_parse parse_type_after_kw", - "v1.02_parse parse_type_body_from_prefix", - "v1.02_parse parse_type_expr" - ] - }, - next_rung_trigger: "v1.04_types child_type_node no longer INFERS SHAPE FROM PROVENANCE -- it discriminates a type child from a field child by something that states the kind, rather than by whether a derived-data slot happens to be occupied. The trigger is that CAPABILITY and not any artifact that would contribute to one: a tag added while the accessor still reads `inferred`-presence satisfies an artifact and leaves the hazard exactly where it is, which is the direction DESIGN section 4b(3) says this machinery structurally cannot see. Emptying the slot BEFORE that lands is the failure this row exists to prevent, not the repair -- it would silently reclassify every field child into the wrong arm at once" -} - -// THE ROSTER, AND WHY IT IS A FOLD RATHER THAN ONE EXEMPLAR PER ROW. -// -// Every GuaranteeStall above was a DECLARATION nothing observed. The witness exercised ONE of them -// by name, so the rest were typed prose -- correct in shape, consumed by nothing, and exactly the -// inert-carrier failure DESIGN section 5 names: coverage by illusion, worse than absent because a -// registered-looking row is cited as registration. Found in review of the third row, and true of -// the first two since they landed. -// -// A PER-ROW WITNESS WOULD BE THE SAME DEFECT WEARING MORE TESTS: N copies of one assertion, each -// proving the FUNCTIONS work and none proving THAT ROW is enrolled, with the coverage tracking how -// many authors remembered rather than how many rows exist. The fold makes the obligation scale -// with the population instead. -// -// THE ROSTER IS HAND-MAINTAINED AND THAT IS A REAL WEAKNESS, stated rather than buried. A row -// added above and not added here is invisible to the fold -- the same staleness these rows warn -// about, one level up. Declaration IDENTITIES are derivable today: v2.std.decl_index -// data_decl_type_facts enumerates every top-level data declaration with its declared type. The -// VALUES needed by this List are not. DeclFact.node is an initializer-identity -// projection. gunbc.seed_closed_vocabulary_wildcard_census files the NotVariantValue answer for -// initializer forms outside that projection's ExprRecordLit and ExprVar arms as -// FabricatedSubstitution. Independently, a measured ExprRecordLit takes -// marshal_plain_record_projection, whose marshal_field_initializer_projection path collapses field -// values needed to reconstruct the GuaranteeStall, including primitive string and list payloads -// nested under ClimbBlocker and StallPopulation, to NotVariantValue through -// variant_value_from_typechecked_expr; no census row currently files that field-value site. So the -// alternative today is still this authored roster or no consumer, but -// declaration enumeration is no longer the blocker. -// TRIGGER: fail-closed typed data-value reflection enumerates exactly every top-level data -// declaration in gunbc.guarantee_stall whose declared type is GuaranteeStall, and no declaration -// outside that module, and projects each fully evaluated value in deterministic source order, -// SUFFICIENT FOR reconstructing every field of every GuaranteeStall row and refusing any initializer -// form or field value it cannot project rather than substituting NotVariantValue. At that point this -// list is DERIVED and an unenrolled row has no spelling. A declaration-identity, -// initializer-shape, or corpus-wide GuaranteeStall surface alone does not satisfy the trigger. -data builtin_parameter_name_forked_across_hand_authored_sites_stall: GuaranteeStall = GuaranteeStall { - subject: "a builtin parameter's name is authored independently in two more places than its declaration", - current: OutsideTheLadder, - ceiling: StructurallyImpossible, - blocker: ClimbableButUnbuilt, - population: BoundedPopulation { members: Cons { head: "src/v1/stage0/src/v1_interpreter.rs expect_int/expect_value_str diagnostic literals (\"substring start\", \"substring end\", \"char_at pos\")", tail: Cons { head: "src/v1/runtime_rust.dag emitted Rust signatures for 47 of the 132 registry builtins", tail: Empty } } }, - next_rung_trigger: "a builtin parameter's name is DERIVED from the declared BuiltinParam at both sites -- the interpreter's diagnostic text and the emitted runtime's signature -- rather than authored as a literal in either. ONE trigger, not two: the capability is identical for both sites and splitting it would let each look closable while the capability that closes them stayed dead." -} - -data algebra_operation_associativity_undeclarable_stall: GuaranteeStall = GuaranteeStall { - subject: "no declared operation in the tree can be said to be associative", - current: OutsideTheLadder, - ceiling: StructurallyGuaranteed, - blocker: AwaitsOneGrounding { grounding: "std.algebra's Semigroup carries the law its name asserts, so that it is distinguishable from Magma" }, - population: UncountedNotEnumerable { reason: "every n-ary application of a binary operation in the corpus depends on associativity and none of them can say so. concat alone is roughly 1200 free-call sites above binary across 64 measured arities, but the class is not concat: it is every operation whose surface arity exceeds its declared arity, and nothing enumerates those because nothing can currently ask the question." }, - next_rung_trigger: "associativity of a declared operation is expressible and checkable -- SUFFICIENT FOR n-ary application of a binary operation declared associative to fold to nested binary application, which is what gunbc.rung_drop concat_binary_signature_exempt_from_arg_binding waits on. Magma is { op: fn(T, T) -> T } and Semigroup is { op: fn(T, T) -> T }: structurally identical, differing by a blank line where the law would sit, so the type whose ENTIRE content is the associativity law carries no law. This is a DESIGN section 5 wall-after-grounding rather than a ratchet -- associativity of a DECLARED operation is a modeled fact, not an undecidable property of an arbitrary function." -} - - -// THE MICROVM GUEST SIZE, filed by the change that removed the wrong derivation rather than by a -// later reviewer. This is AwaitsOneGrounding and not ClimbableButUnbuilt: the obstacle is not -// unwritten code, it is that the quantity to subtract may not exist as a constant at all -- a -// VMM's resident footprint scales with guest size through page tables, with the device model, and -// with host page size, so what upstream documents is typically a MEASURED overhead for one stated -// configuration, which is an observation about one boot rather than a property of the realization. -// A trigger reading "model the overhead" would presume that number exists and would be -// unsatisfiable in exactly the way this carrier's own rows warn about. -// -// THE POPULATION WAS RE-CENSUSED, NOT SPOT-REPAIRED, AND THE MEMBERSHIP RULE IS WRITTEN DOWN SO -// COMPLETENESS IS CHECKABLE. An earlier version of this row named runner_microvm_sizing_of_cores, -// which the same commit deleted, and gave the witness module as test.claim.runner.runner_microvm_ -// witness_test when the module declares test.claim.runner_microvm_witness_test with no intermediate -// segment. A phantom member beside an omitted live one means the row never carried the BOUNDED -// population DESIGN 4b requires, and two spot fixes would have left completeness unestablished -- -// so the row was re-derived from the module's declarations rather than edited. -// -// MEMBERSHIP RULE: a symbol is a member when, IN PRODUCTION, it cannot reach its intended answer -// because of the two missing quantities. That deliberately includes guest_memory_fits, which is -// correct code that always returns MemoryFitUnresolved on the production path, and deliberately -// excludes guest_resources_of_machine_config and the topology and credential arms, which decide -// fully today. It also includes fabric_cell_slice_desired_directives, which is not in this module: -// the CPU obstacle is owed there, and a row scoped to the file rather than the class would be -// satisfied while the capability stayed dead. -// -// THE TRIGGER CARRIES TWO CLAUSES AND BOTH ARE REQUIRED, because satisfying the first alone would -// take the admission's accept arm live having never executed. Retargeting the microVM witnesses -// onto the refusal path left the success path with NO executed coverage: RunnerMicroVmAdmitted is -// unreachable while sizing refuses, so every witness now proves a gate is passed on the way to a -// refusal and none proves an admissible VM is admitted. A gate whose accept arm has never run is -// not a gate that has been tested. -// -// THE CPU AXIS IS NOT A SECOND COPY OF THE MEMORY ONE, WHICH IS WHY THE TRIGGER SPLITS THEM. On -// memory the quantity may exist and be uncited. On CPU the cell realizes no absolute entitlement at -// all: fabric_cell_slice_desired_directives emits CPUWeight, a relative share that guarantees no -// amount of anything under contention. The absolute ceiling this fleet does declare is written by -// host_converge onto the RUNNER UNIT, a different systemd object from the cell slice -- so a guest -// vCPU count derived from the cell would equal a number the cell never enforces. That is the -// failure gunbc.ci.ci_runner_placement already records once: "the arithmetic said six threads per -// slot and the host was never told." -// -// AND THE CONTROLS MUST COME BACK AS FIT CONTROLS. The pair this row replaced asserted EQUALITY to -// the envelope in both directions -- it admitted a guest sized at the whole ceiling and refused a -// 4 GiB guest against a 16 GiB cell. Under containment the smaller guest FITS, so both arms were -// wrong in opposite directions while the pair looked discriminating. A nonconstant predicate with -// both polarities observed can still be answering a question nobody asked. -data runner_microvm_guest_size_derivation_stall: GuaranteeStall = GuaranteeStall { - subject: "gunbc.runner_microvm cannot derive a guest's resource envelope from the bounded cell on EITHER axis: memory needs a subtrahend for the Firecracker VMM's own footprint that is not cited anywhere, and CPU needs an absolute entitlement the cell does not carry", - current: Mitigatable, - ceiling: StructurallyGuaranteed, - blocker: AwaitsOneGrounding { - grounding: "what quantities, if any, relate a cell's declared envelope to an admissible guest. On MEMORY that may be a cited VMM footprint, or the finding that guest RAM is an operator-declared input BOUNDED BY the envelope rather than derived from it. On CPU it is prior: gunbc.fabric.fabric_cell_effect emits CPUWeight, a RELATIVE share that guarantees no amount of anything, so there is no absolute cell entitlement for a guest vCPU count to be derived from -- the absolute ceiling this fleet does declare, gunbc.host.host_converge runner_cpu_boundary_knobs writing CapacityQuota as a CPUQuota drop-in, lands on the RUNNER UNIT and not on the cell slice. One bounded execution context, two realizations, different axes enforced", - }, - population: BoundedPopulation { - members: [ - "gunbc.runner_microvm guest_memory_fits", - "gunbc.runner_microvm gunbc_runner_microvm_realization_reserve", - "gunbc.runner_microvm gunbc_runner_microvm_cell_cpu_entitlement", - "gunbc.runner_microvm runner_microvm_sizing", - "gunbc.runner_microvm runner_microvm_size_from_cell_envelope", - "gunbc.runner_microvm runner_microvm_admission_after_credential", - "gunbc.runner_microvm gunbc_runner_microvm_admission", - "gunbc.runner_microvm gunbc_runner_microvm_vm_config", - "gunbc.fabric.fabric_cell_effect fabric_cell_slice_desired_directives", - "test.claim.runner_microvm_witness_test", - ], - }, - next_rung_trigger: "BOTH of: (1) a quantity sufficient to DERIVE an admissible guest RAM from a cell envelope, or a decision that guest RAM is a declared input bounded by that envelope; AND (2) the cell realizing an ABSOLUTE CPU entitlement that a guest vCPU count can be derived from -- a CPUQuota or CPU set on the CELL SLICE, not the CPUQuota gunbc.host.host_converge already writes onto the runner UNIT -- or guest topology renamed as a separately declared product decision that is NOT derived from the cell. The clauses are separate because the obstacles differ in kind: the memory quantity may exist and merely be uncited, while the cell grants no CPU quantity at all, so a trigger naming only the memory subtrahend would be satisfied while the CPU axis stayed unfounded. THE THIRD CLAUSE THIS ROW CARRIED IS DISCHARGED: RunnerMicroVmAdmitted is reachable again and executed, because the realization reserve is a PARAMETER of the admission rather than a global, so a witness declaring one drives the accept arm while production still refuses. What is NOT discharged and is not claimed here is that PRODUCTION can reach that arm -- it cannot, and clauses 1 and 2 are what would change that" -} - -// THIS IS A PRE-EXISTING CAPABILITY GAP, NOT A RUNG LOWERED BY THE CUT-OVER. The legacy transport -// did put HEAD/objects/refs beside working bytes in an empty directory, but omitted the index and -// therefore could not produce the consistent repository state this deployment claims. Calling that -// a bootstrap would count mutation as success and repeat the exact conflation RLM-2c removes. -// Git-native convergence now refuses the unobservable pre-state through -// ConvergencePreStateUnobservable, and placement carries that located cause to the outer deploy in -// its durable receipt. The refusal is evidence of the gap; it is not the missing capability. -// THE POPULATION IS ONE PRODUCTION SUBJECT, NOT A SNAPSHOT OF AN OPEN SET. There is one production -// constructor, deployment_spec_srv1, and the realization binding is global rather than a field a -// future spec can silently choose. Any later production spec therefore inherits GitNativeConvergence; -// at a fresh root it reaches the same typed ConvergencePreStateUnobservable wall and cannot proceed. -// The boundary is the refusal construction, not a hand-maintained roster count. -data deployed_repository_empty_root_bootstrap_stall: GuaranteeStall = GuaranteeStall { - subject: "an empty deployed repository root cannot be brought to one consistent candidate revision by live deploy", - current: OutsideTheLadder, - ceiling: StructurallyGuaranteed, - blocker: ClimbableButUnbuilt, - population: BoundedPopulation { members: Cons { head: "gunbc.live_deploy.spec deployment_spec_srv1 at a fresh repository root", tail: Empty {} } }, - next_rung_trigger: "a modeled Git-native bootstrap sufficient to initialize an empty deployed repository from the admitted runner checkout at the exact candidate, with HEAD, index and tracked worktree read back as that one revision before any later deployment member runs; copying any .git path as files, relaxing ConvergencePreStateUnobservable, or merely creating an empty git directory does not satisfy the capability" -} - -// THE PROSE HALF OF THE DROP ROSTER, DECLARED AS A STALL BECAUSE THAT IS WHAT IT IS. 26 of -// gunbc.rung_drop's rows state their DESIGN section 4b(3) fields -- previous rung, temporary rung, -// reason, population, restoration trigger -- only inside an `authored` paragraph, so for those rows -// the obligation 4b(3) states is met by a human reading and by nothing a program can fold. The four -// rows consolidated from the deleted gunbc.guarantee_rung_drop carry the fields typed, which is -// what makes this a stall with a known repair rather than a limit. -// -// GROWTH OF THE ARM IS VISIBLE BUT NOT PREVENTED, AND THIS ROW SAID OTHERWISE FIRST. Its first -// version asserted that a further prose row was structurally impossible because -// gunbc.rung_drop LegacyProseIdentity had no constructor for one. That was falsified within hours by -// spark_serving_local_artifact_not_reproducible, authored on another lane against the -// pre-consolidation shape and landed in main mid-consolidation; admitting it cost one arm. The -// enumeration makes growth UNSILENT -- an edit to a named list, visible in review, counted by a fold -// -- and that is mechanically preventable, not structural. What stalls is the SHRINKING of the arm, -// which is per-row work with no mechanical oracle: -// deciding which sentence of a paragraph is its reason and which its population is semantic -// rewriting, and several of these paragraphs argue at length about that very question. Each split -// deletes one arm from that coproduct, so the arm count IS the remaining debt and nothing has to be -// counted separately. -// -// THE TRIGGER NAMES THE CAPABILITY, not the last row. A trigger reading "the final row is split" -// would be satisfiable by a split that fabricated fields, which is the failure the prose arm exists -// to avoid; the capability is that every drop's five fields are readable AS DATA, which no -// fabricated split delivers. -data prose_declared_rung_drop_stall: GuaranteeStall = GuaranteeStall { - subject: "a declared section 4b(3) rung drop states its five fields only as prose, so its reason, population and restoration trigger are unreadable by any fold", - current: Mitigatable, - ceiling: StructurallyImpossible, - blocker: ClimbableButUnbuilt, - population: BoundedPopulation { - members: [ - "gunbc.rung_drop spark_serving_local_artifact_not_reproducible", - "gunbc.rung_drop floor_cut", - "gunbc.rung_drop measurement_bankruptcy", - "gunbc.rung_drop regen_producer", - "gunbc.rung_drop cited_symbol_census", - "gunbc.rung_drop emit_stage_blocking", - "gunbc.rung_drop lens_enforcement_censuses", - "gunbc.rung_drop required_gate_bankruptcy", - "gunbc.rung_drop text_boundary_identity_wall", - "gunbc.rung_drop fabric_evidence_gating", - "gunbc.rung_drop emitted_bytes_witness_required_lane", - "gunbc.rung_drop direct_call_arg_seam_v2_exemption", - "gunbc.rung_drop floor_cost_claim_qualification_unavailable", - "gunbc.rung_drop spark_role_scoped_retirement_production_root", - "gunbc.rung_drop floor_cut_heal", - "gunbc.rung_drop floor_cut_effect_gates", - "gunbc.rung_drop floor_cut_fmt_gate", - "gunbc.rung_drop floor_cut_merge_admission_stamping", - "gunbc.rung_drop floor_cut_falsifier_cadence", - "gunbc.rung_drop builtin_signature_arity_pairing_fabricates", - "gunbc.rung_drop concat_binary_signature_exempt_from_arg_binding", - "gunbc.rung_drop namespace_admission_consumed_row_deletion", - "gunbc.rung_drop dashboard_merge_ready_semantic_admissibility", - "gunbc.rung_drop floor_cut_behavioural_regression_differential", - "gunbc.rung_drop floor_cut_receipt_discriminating_arms", - "gunbc.rung_drop floor_cut_regen_second_generation_agreement" - ] - }, - next_rung_trigger: "EVERY row in gunbc.rung_drop rung_drop_roster carries TypedDeclaration -- its previous rung, temporary rung, reason, bounded population and restoration trigger readable as data and not as a paragraph -- with each split reviewed as its own readable diff against the paragraph it replaces, at which point LegacyProseIdentity and the AuthoredProse arm are both deleted and the class is structurally impossible rather than empty" -} - -// ONE EXPRESSION, TWO EVALUATORS -- AND WHY THIS IS A STALL RATHER THAN A DROP, which is the whole -// reason it is in this carrier. Nothing ever required this comparison, so no rung was lowered and -// there is no previous rung to restore; a `RungDrop` row would make the declared-drop ledger report -// a newly discovered gap as a regression, which is the rung inflation section 4b(1) forbids applied -// to the compiler's own self-description. It was drafted as a drop on gunbc#10154 and moved here -// (codex review 59064) rather than kept with a disclaimer, because a row denying the meaning of the -// carrier it sits in is a meaning fork, not a caveat. -// -// WHY IT IS NOT `gunbc.recurring_failure_mode` `realization_arms_diverge_on_whether_the_program_refuses`, -// stated with a specimen on each side because the question a reader actually has is which row owns a -// given specimen. The two subjects CROSS. IN THIS ROW AND NOT IN THAT ONE: .dag evaluates both -// operands of a conjunction and emitted Rust short-circuits, so where the right operand is total the -// two arms agree on every answer and differ only in WHAT RAN -- no refusal fires, so there is no -// refusal divergence for that row to see and every result-comparison oracle is green through it. IN -// THAT ROW AND NOT IN THIS ONE: a divergence between two realization arms NEITHER of which is the -// authority, which is not an authority-versus-target relation at all. Neither contains the other. -// -// THE CEILING IS 2 AND NOT HIGHER BECAUSE THIS ROW OWNS DETECTION, NOT CONSTRUCTION. Making the -// divergence unwritable -- evaluation order modeled as a property of a connective and consulted by -// both realizations -- is that failure-mode row's trigger. This row is the executed check over -// whatever construction does not yet cover, which is the order section 5 states, so the two coexist. -// -// THE POPULATION IS HONESTLY UNCOUNTABLE AND A GREP UNDERSTATES IT BY CONSTRUCTION: the interpreter -// is the STRICTER arm, so any author who wrote the guard idiom over a refusing right operand hit the -// refusal while authoring and rewrote it. The surviving matches are the cases that do NOT carry the -// consequence, so a low count is not evidence the class is small. -data authority_target_same_expression_equivalence_stall: GuaranteeStall = GuaranteeStall { - subject: "one expression evaluated by the .dag authority and by the emitted target is never compared by execution, so the two may agree on the returned value and differ on which subexpressions ran", - current: OutsideTheLadder, - ceiling: MechanicallyPreventable, - blocker: ClimbableButUnbuilt, - population: UncountedNotEnumerable { reason: "the affected population is every expression whose two realizations could diverge, and it is survivorship-filtered: the interpreter is the stricter arm, so sites where the divergence carried a consequence were rewritten while authoring and only the harmless matches survive to be grepped" }, - next_rung_trigger: "a lane that runs ONE expression through BOTH realizations and refuses a divergence, sufficient for an emission differing from its authority in value OR in what it evaluates being caught, demonstrated by a red on a fixture where the two agree on the returned value and differ on which subexpressions ran; the fixture is already executed and dated on gunbc#10139, so what is owed is enrolment and not a harness, and enrolling behavioral_differential discharges the seed-Rust versus emitted-Rust axis ONLY and does not touch this row" -} - -// THE DELIBERATELY DROPPED HALF OF gunbc#10258'S DISPLAY CONTRACT. That lane printed module -// identity beside source path from ResolvedGraph, but only after typed resolution. The -// loader-boundary preflight that replaced it answers the actual landing decision at its native -// grain -- repository-path intersection -- and cannot project resolved module identity because -// SourceFile carries only path and content. Reparsing the content or reconstructing a plausible -// path-to-name mapping would mint a second identity authority, so the replacement refuses that -// tempting widening and records the absent capability here instead. -data pre_resolve_entry_closure_module_identity_stall: GuaranteeStall = GuaranteeStall { - subject: "a routed entry's exact loader-boundary closure can be enumerated by repository path before typed resolution, but cannot be enumerated by resolved module identity at that same pre-resolution boundary", - current: OutsideTheLadder, - ceiling: StructurallyGuaranteed, - blocker: ClimbableButUnbuilt, - population: BoundedPopulation { members: ["claim_batch --print-entry-closure"] }, - next_rung_trigger: "the modeled routed-entry execution path exposes module identity joined to every loader-boundary source path before typed resolution, derived from its existing module-declaration facts rather than by reparsing source text or reconstructing identity from path spelling" -} - -data all_guarantee_stalls: List = [ - pre_resolve_entry_closure_module_identity_stall, - merge_admission_terminal_verdict_stall, - generated_artifact_registry_membership_stall, - authority_target_same_expression_equivalence_stall, - runner_microvm_guest_size_derivation_stall, - import_eligibility_resolution_stall, - next_rung_trigger_enforcement_stall, - heterogeneous_child_list_stall, - doc_graph_orphan_population_stall, - doc_graph_dangling_link_population_stall, - enforcement_live_closure_gate_stall, - mandatory_tag_live_corpus_stall, - parse_ingest_grammar_relation_stall, - required_regen_host_derivation_stall, - self_host_candidate_generation_add_slice_stall, - non_fold_residue_roster_stall, - retained_rust_live_tree_migration_stall, - variant_owner_identity_stall, - gitattributes_committed_emit_drift_stall, - wall_deadline_shared_fill_attribution_stall, - builtin_parameter_name_forked_across_hand_authored_sites_stall, - algebra_operation_associativity_undeclarable_stall, - deployed_repository_empty_root_bootstrap_stall, - prose_declared_rung_drop_stall, - two_nat_authorities_stall, - external_model_scope_live_cover_stall, - observation_heartbeat_lockstep_stall, - operation_argv_binding_wall_stall, -] - // A STALL AT ITS CEILING IS NOT A STALL: the row would describe a class that already arrived, and // every consumer reading it as outstanding work reads a false claim. fn every_stall_is_below_its_ceiling(ss: List) -> Bool { @@ -794,48 +152,3 @@ fn stall_roster_size(ss: List) -> Int { cons: fn(acc, s) { acc + 1 }, ) } - -// THE FOUR SUBJECTS RESTORED TO THE ROSTER, PINNED BY IDENTITY SO THEIR LOSS REFUSES. -// -// These four stalls were DECLARED in this module and absent from all_guarantee_stalls, so the three -// walls written over that roster ranged over 21 of the 25 rows this file declares. The walls were -// green because their input was short, which is exactly the shape -// gunbc.recurring_failure_mode check_subject_narrower_than_its_declared_claim names: a green check -// whose declared subject is a strict superset of the population it actually ranges over. -// -// WHAT THIS CHECK COVERS AND WHAT IT DOES NOT, stated because a check that does not state its own -// denominator cannot be distinguished from a complete one. It covers exactly these four subjects: -// if any is dropped from the roster again, the fold refuses. It does NOT detect a NEW stall -// declared and left unrostered -- that requires a corpus-wide census of GuaranteeStall -// declarations joined against the roster, which is a separate obligation and is gated on whether -// its RED is authorable at all (a stall declared in a module the roster cannot import may not be -// expressible in any fixture, and a check whose RED has nowhere to live is a decoration). -// -// PRESENCE-EXACTLY-ONCE, NOT SET EQUALITY, and the asymmetry is deliberate: a new stall row must -// be admitted without editing this list, while a lost one must refuse. Exactly-once also refuses -// a DOUBLE entry, which set membership would accept and which reads as a merge that applied twice. -// PINNED BY REFERENCE TO THE DECLARATIONS, NOT BY TRANSCRIBING THEIR SUBJECTS. An earlier draft -// listed the four subjects as string literals and got all four WRONG -- the real subjects are full -// sentences, so the fold would have found zero matches and refused, or worse, been "fixed" by -// copying the prose in. A copied string is a second authority for text this file already declares, -// and it rots the moment a subject is reworded. Naming the declaration is the section 3 move. -data restored_stalls: List = [ - two_nat_authorities_stall, - external_model_scope_live_cover_stall, - observation_heartbeat_lockstep_stall, - operation_argv_binding_wall_stall, -] - -fn every_restored_stall_is_rostered_once(ss: List) -> Bool { - fold_list( - xs: restored_stalls, - empty: true, - cons: fn(acc, want) { - acc && fold_list( - xs: ss, - empty: 0, - cons: fn(n, s) { if s.subject == want.subject { n + 1 } else { n } }, - ) == 1 - }, - ) -} diff --git a/dag/gunbc/guarantee_stall/algebra_operation_associativity_undeclarable_stall.dag b/dag/gunbc/guarantee_stall/algebra_operation_associativity_undeclarable_stall.dag new file mode 100644 index 00000000000..199a87785e3 --- /dev/null +++ b/dag/gunbc/guarantee_stall/algebra_operation_associativity_undeclarable_stall.dag @@ -0,0 +1,13 @@ +module gunbc.guarantee_stall.algebra_operation_associativity_undeclarable_stall + +import gunbc.guarantee_rung { OutsideTheLadder, StructurallyGuaranteed } +import gunbc.guarantee_stall { GuaranteeStall, AwaitsOneGrounding, UncountedNotEnumerable } + +data algebra_operation_associativity_undeclarable_stall: GuaranteeStall = GuaranteeStall { + subject: "no declared operation in the tree can be said to be associative", + current: OutsideTheLadder, + ceiling: StructurallyGuaranteed, + blocker: AwaitsOneGrounding { grounding: "std.algebra's Semigroup carries the law its name asserts, so that it is distinguishable from Magma" }, + population: UncountedNotEnumerable { reason: "every n-ary application of a binary operation in the corpus depends on associativity and none of them can say so. concat alone is roughly 1200 free-call sites above binary across 64 measured arities, but the class is not concat: it is every operation whose surface arity exceeds its declared arity, and nothing enumerates those because nothing can currently ask the question." }, + next_rung_trigger: "associativity of a declared operation is expressible and checkable -- SUFFICIENT FOR n-ary application of a binary operation declared associative to fold to nested binary application, which is what gunbc.rung_drop concat_binary_signature_exempt_from_arg_binding waits on. Magma is { op: fn(T, T) -> T } and Semigroup is { op: fn(T, T) -> T }: structurally identical, differing by a blank line where the law would sit, so the type whose ENTIRE content is the associativity law carries no law. This is a DESIGN section 5 wall-after-grounding rather than a ratchet -- associativity of a DECLARED operation is a modeled fact, not an undecidable property of an arbitrary function." +} diff --git a/dag/gunbc/guarantee_stall/authority_target_same_expression_equivalence_stall.dag b/dag/gunbc/guarantee_stall/authority_target_same_expression_equivalence_stall.dag new file mode 100644 index 00000000000..9903671afce --- /dev/null +++ b/dag/gunbc/guarantee_stall/authority_target_same_expression_equivalence_stall.dag @@ -0,0 +1,39 @@ +module gunbc.guarantee_stall.authority_target_same_expression_equivalence_stall + +import gunbc.guarantee_rung { OutsideTheLadder, MechanicallyPreventable } +import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, UncountedNotEnumerable } + +// ONE EXPRESSION, TWO EVALUATORS -- AND WHY THIS IS A STALL RATHER THAN A DROP, which is the whole +// reason it is in this carrier. Nothing ever required this comparison, so no rung was lowered and +// there is no previous rung to restore; a `RungDrop` row would make the declared-drop ledger report +// a newly discovered gap as a regression, which is the rung inflation section 4b(1) forbids applied +// to the compiler's own self-description. It was drafted as a drop on gunbc#10154 and moved here +// (codex review 59064) rather than kept with a disclaimer, because a row denying the meaning of the +// carrier it sits in is a meaning fork, not a caveat. +// +// WHY IT IS NOT `gunbc.recurring_failure_mode` `realization_arms_diverge_on_whether_the_program_refuses`, +// stated with a specimen on each side because the question a reader actually has is which row owns a +// given specimen. The two subjects CROSS. IN THIS ROW AND NOT IN THAT ONE: .dag evaluates both +// operands of a conjunction and emitted Rust short-circuits, so where the right operand is total the +// two arms agree on every answer and differ only in WHAT RAN -- no refusal fires, so there is no +// refusal divergence for that row to see and every result-comparison oracle is green through it. IN +// THAT ROW AND NOT IN THIS ONE: a divergence between two realization arms NEITHER of which is the +// authority, which is not an authority-versus-target relation at all. Neither contains the other. +// +// THE CEILING IS 2 AND NOT HIGHER BECAUSE THIS ROW OWNS DETECTION, NOT CONSTRUCTION. Making the +// divergence unwritable -- evaluation order modeled as a property of a connective and consulted by +// both realizations -- is that failure-mode row's trigger. This row is the executed check over +// whatever construction does not yet cover, which is the order section 5 states, so the two coexist. +// +// THE POPULATION IS HONESTLY UNCOUNTABLE AND A GREP UNDERSTATES IT BY CONSTRUCTION: the interpreter +// is the STRICTER arm, so any author who wrote the guard idiom over a refusing right operand hit the +// refusal while authoring and rewrote it. The surviving matches are the cases that do NOT carry the +// consequence, so a low count is not evidence the class is small. +data authority_target_same_expression_equivalence_stall: GuaranteeStall = GuaranteeStall { + subject: "one expression evaluated by the .dag authority and by the emitted target is never compared by execution, so the two may agree on the returned value and differ on which subexpressions ran", + current: OutsideTheLadder, + ceiling: MechanicallyPreventable, + blocker: ClimbableButUnbuilt, + population: UncountedNotEnumerable { reason: "the affected population is every expression whose two realizations could diverge, and it is survivorship-filtered: the interpreter is the stricter arm, so sites where the divergence carried a consequence were rewritten while authoring and only the harmless matches survive to be grepped" }, + next_rung_trigger: "a lane that runs ONE expression through BOTH realizations and refuses a divergence, sufficient for an emission differing from its authority in value OR in what it evaluates being caught, demonstrated by a red on a fixture where the two agree on the returned value and differ on which subexpressions ran; the fixture is already executed and dated on gunbc#10139, so what is owed is enrolment and not a harness, and enrolling behavioral_differential discharges the seed-Rust versus emitted-Rust axis ONLY and does not touch this row" +} diff --git a/dag/gunbc/guarantee_stall/builtin_parameter_name_forked_across_hand_authored_sites_stall.dag b/dag/gunbc/guarantee_stall/builtin_parameter_name_forked_across_hand_authored_sites_stall.dag new file mode 100644 index 00000000000..4ede27d39b2 --- /dev/null +++ b/dag/gunbc/guarantee_stall/builtin_parameter_name_forked_across_hand_authored_sites_stall.dag @@ -0,0 +1,14 @@ +module gunbc.guarantee_stall.builtin_parameter_name_forked_across_hand_authored_sites_stall + +import v2.std.algebra { Cons, Empty } +import gunbc.guarantee_rung { OutsideTheLadder, StructurallyImpossible } +import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, BoundedPopulation } + +data builtin_parameter_name_forked_across_hand_authored_sites_stall: GuaranteeStall = GuaranteeStall { + subject: "a builtin parameter's name is authored independently in two more places than its declaration", + current: OutsideTheLadder, + ceiling: StructurallyImpossible, + blocker: ClimbableButUnbuilt, + population: BoundedPopulation { members: Cons { head: "src/v1/stage0/src/v1_interpreter.rs expect_int/expect_value_str diagnostic literals (\"substring start\", \"substring end\", \"char_at pos\")", tail: Cons { head: "src/v1/runtime_rust.dag emitted Rust signatures for 47 of the 132 registry builtins", tail: Empty } } }, + next_rung_trigger: "a builtin parameter's name is DERIVED from the declared BuiltinParam at both sites -- the interpreter's diagnostic text and the emitted runtime's signature -- rather than authored as a literal in either. ONE trigger, not two: the capability is identical for both sites and splitting it would let each look closable while the capability that closes them stayed dead." +} diff --git a/dag/gunbc/guarantee_stall/deployed_repository_empty_root_bootstrap_stall.dag b/dag/gunbc/guarantee_stall/deployed_repository_empty_root_bootstrap_stall.dag new file mode 100644 index 00000000000..10239c16683 --- /dev/null +++ b/dag/gunbc/guarantee_stall/deployed_repository_empty_root_bootstrap_stall.dag @@ -0,0 +1,26 @@ +module gunbc.guarantee_stall.deployed_repository_empty_root_bootstrap_stall + +import v2.std.algebra { Cons, Empty } +import gunbc.guarantee_rung { OutsideTheLadder, StructurallyGuaranteed } +import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, BoundedPopulation } + +// THIS IS A PRE-EXISTING CAPABILITY GAP, NOT A RUNG LOWERED BY THE CUT-OVER. The legacy transport +// did put HEAD/objects/refs beside working bytes in an empty directory, but omitted the index and +// therefore could not produce the consistent repository state this deployment claims. Calling that +// a bootstrap would count mutation as success and repeat the exact conflation RLM-2c removes. +// Git-native convergence now refuses the unobservable pre-state through +// ConvergencePreStateUnobservable, and placement carries that located cause to the outer deploy in +// its durable receipt. The refusal is evidence of the gap; it is not the missing capability. +// THE POPULATION IS ONE PRODUCTION SUBJECT, NOT A SNAPSHOT OF AN OPEN SET. There is one production +// constructor, deployment_spec_srv1, and the realization binding is global rather than a field a +// future spec can silently choose. Any later production spec therefore inherits GitNativeConvergence; +// at a fresh root it reaches the same typed ConvergencePreStateUnobservable wall and cannot proceed. +// The boundary is the refusal construction, not a hand-maintained roster count. +data deployed_repository_empty_root_bootstrap_stall: GuaranteeStall = GuaranteeStall { + subject: "an empty deployed repository root cannot be brought to one consistent candidate revision by live deploy", + current: OutsideTheLadder, + ceiling: StructurallyGuaranteed, + blocker: ClimbableButUnbuilt, + population: BoundedPopulation { members: Cons { head: "gunbc.live_deploy.spec deployment_spec_srv1 at a fresh repository root", tail: Empty {} } }, + next_rung_trigger: "a modeled Git-native bootstrap sufficient to initialize an empty deployed repository from the admitted runner checkout at the exact candidate, with HEAD, index and tracked worktree read back as that one revision before any later deployment member runs; copying any .git path as files, relaxing ConvergencePreStateUnobservable, or merely creating an empty git directory does not satisfy the capability" +} diff --git a/dag/gunbc/guarantee_stall/doc_graph_dangling_link_population_stall.dag b/dag/gunbc/guarantee_stall/doc_graph_dangling_link_population_stall.dag new file mode 100644 index 00000000000..6f29ef2122e --- /dev/null +++ b/dag/gunbc/guarantee_stall/doc_graph_dangling_link_population_stall.dag @@ -0,0 +1,14 @@ +module gunbc.guarantee_stall.doc_graph_dangling_link_population_stall + +import v2.std.algebra { Cons, Empty } +import gunbc.guarantee_rung { OutsideTheLadder, MechanicallyPreventable } +import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, BoundedPopulation } + +data doc_graph_dangling_link_population_stall: GuaranteeStall = GuaranteeStall { + subject: "the derived documentation graph contains dangling links", + current: OutsideTheLadder, + ceiling: MechanicallyPreventable, + blocker: ClimbableButUnbuilt, + population: BoundedPopulation { members: Cons { head: "test.claim.doc_reachability_witness.doc_graph_has_no_dangling_links", tail: Cons { head: "v2.test.lens_doc_reachability.doc_reachability_test.doc_graph_has_no_dangling_links", tail: Cons { head: "v2.test.lens_doc_reachability.doc_reachability_test.doc_graph_is_clean", tail: Empty {} } } } }, + next_rung_trigger: "the derived dangling-link identity population is empty and every enrolled projection reports NowPassing" +} diff --git a/dag/gunbc/guarantee_stall/doc_graph_orphan_population_stall.dag b/dag/gunbc/guarantee_stall/doc_graph_orphan_population_stall.dag new file mode 100644 index 00000000000..16f89df58e5 --- /dev/null +++ b/dag/gunbc/guarantee_stall/doc_graph_orphan_population_stall.dag @@ -0,0 +1,14 @@ +module gunbc.guarantee_stall.doc_graph_orphan_population_stall + +import v2.std.algebra { Cons, Empty } +import gunbc.guarantee_rung { OutsideTheLadder, MechanicallyPreventable } +import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, BoundedPopulation } + +data doc_graph_orphan_population_stall: GuaranteeStall = GuaranteeStall { + subject: "the derived documentation graph contains orphan documents", + current: OutsideTheLadder, + ceiling: MechanicallyPreventable, + blocker: ClimbableButUnbuilt, + population: BoundedPopulation { members: Cons { head: "test.claim.doc_reachability_witness.doc_graph_has_no_orphan_docs", tail: Cons { head: "v2.test.lens_doc_reachability.doc_reachability_test.doc_graph_has_no_orphan_docs", tail: Cons { head: "v2.test.lens_doc_reachability.doc_reachability_test.doc_graph_is_clean", tail: Empty {} } } } }, + next_rung_trigger: "the derived orphan-document identity population is empty and every enrolled projection reports NowPassing" +} diff --git a/dag/gunbc/guarantee_stall/enforcement_live_closure_gate_stall.dag b/dag/gunbc/guarantee_stall/enforcement_live_closure_gate_stall.dag new file mode 100644 index 00000000000..2119fe59cf9 --- /dev/null +++ b/dag/gunbc/guarantee_stall/enforcement_live_closure_gate_stall.dag @@ -0,0 +1,14 @@ +module gunbc.guarantee_stall.enforcement_live_closure_gate_stall + +import v2.std.algebra { Cons, Empty } +import gunbc.guarantee_rung { OutsideTheLadder, MechanicallyPreventable } +import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, BoundedPopulation } + +data enforcement_live_closure_gate_stall: GuaranteeStall = GuaranteeStall { + subject: "the live enforcement closure and its question-zero gate are non-green", + current: OutsideTheLadder, + ceiling: MechanicallyPreventable, + blocker: ClimbableButUnbuilt, + population: BoundedPopulation { members: Cons { head: "v2.test.claim.enforcement.lens_module_gate_witness.lens_closure_question_zero_holds_live", tail: Cons { head: "v2.test.claim.enforcement.lens_module_gate_witness.lens_module_gate_holds_live", tail: Cons { head: "v2.test.claim.enforcement.lens_module_gate_witness.question_zero_verdict_live_holds", tail: Empty {} } } } }, + next_rung_trigger: "the live closure question returns zero and both gate projections report true" +} diff --git a/dag/gunbc/guarantee_stall/external_model_scope_live_cover_stall.dag b/dag/gunbc/guarantee_stall/external_model_scope_live_cover_stall.dag new file mode 100644 index 00000000000..6bf31d0ef92 --- /dev/null +++ b/dag/gunbc/guarantee_stall/external_model_scope_live_cover_stall.dag @@ -0,0 +1,14 @@ +module gunbc.guarantee_stall.external_model_scope_live_cover_stall + +import v2.std.algebra { Cons, Empty } +import gunbc.guarantee_rung { OutsideTheLadder, MechanicallyPreventable } +import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, BoundedPopulation } + +data external_model_scope_live_cover_stall: GuaranteeStall = GuaranteeStall { + subject: "the live external-model scope cover does not cover the extdeps tree", + current: OutsideTheLadder, + ceiling: MechanicallyPreventable, + blocker: ClimbableButUnbuilt, + population: BoundedPopulation { members: Cons { head: "test.claim.external_model_scope_live_cover_witness.frontier_cover_of_live_extdeps_tree_holds", tail: Empty {} } }, + next_rung_trigger: "node://adhoc-89fcf94a-bdd lands: the live extdeps-tree cover is exact and its routed witness returns true" +} diff --git a/dag/gunbc/guarantee_stall/generated_artifact_registry_membership_stall.dag b/dag/gunbc/guarantee_stall/generated_artifact_registry_membership_stall.dag new file mode 100644 index 00000000000..5e94982e16b --- /dev/null +++ b/dag/gunbc/guarantee_stall/generated_artifact_registry_membership_stall.dag @@ -0,0 +1,25 @@ +module gunbc.guarantee_stall.generated_artifact_registry_membership_stall + +import v2.std.algebra { Cons, Empty } +import gunbc.guarantee_rung { MechanicallyPreventable, StructurallyGuaranteed } +import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, BoundedPopulation } + +// THE GENERATED-ARTIFACT REGISTRY IS GUARDED INDIRECTLY, AND THIS ROW EXISTS BECAUSE THE MUTATION +// WAS RUN RATHER THAN REASONED ABOUT. Deleting a member from generated_artifact_registry and +// running the gate produced EXACTLY ONE finding, and it was `.gitattributes` drift -- the +// merge-driver enrollment projection enumerates registry members, so dropping one changes its +// bytes. Nothing said what an author would actually want said: that a COMMITTED file at a +// generated location is now adjudicated by nobody. The wall is real and it is one step removed +// from its subject, so an artifact excluded from the .gitattributes projection for any reason +// would leave the registry silently. Current rung is the honest one for a guard that holds by +// side effect; the trigger names the direct capability, a census joining committed files at +// generated-artifact locations back to registry membership, because a guard that answers about +// enrollment bytes is not the guard that answers about orphaned artifacts. +data generated_artifact_registry_membership_stall: GuaranteeStall = GuaranteeStall { + subject: "a committed generated artifact leaves generated_artifact_registry and stops being adjudicated", + current: MechanicallyPreventable, + ceiling: StructurallyGuaranteed, + blocker: ClimbableButUnbuilt, + population: BoundedPopulation { members: Cons { head: "gunbc.generated_artifact generated_artifact_registry", tail: Cons { head: "gunbc.generated_artifact_merge_driver", tail: Empty {} } } }, + next_rung_trigger: "a census that enumerates committed files at every artifact_location and refuses one with no generated_artifact_registry member, so registry departure is refused by its own subject rather than by .gitattributes drift" +} diff --git a/dag/gunbc/guarantee_stall/gitattributes_committed_emit_drift_stall.dag b/dag/gunbc/guarantee_stall/gitattributes_committed_emit_drift_stall.dag new file mode 100644 index 00000000000..b93e9dfaf72 --- /dev/null +++ b/dag/gunbc/guarantee_stall/gitattributes_committed_emit_drift_stall.dag @@ -0,0 +1,20 @@ +module gunbc.guarantee_stall.gitattributes_committed_emit_drift_stall + +import v2.std.algebra { Cons, Empty } +import gunbc.guarantee_rung { OutsideTheLadder, MechanicallyPreventable } +import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, BoundedPopulation } + +// REQUIRED-FLOOR RUN 32942047138 first executed this ReadsLiveTree carrier after #9284 landed. +// The direct byte-equality witness and its aggregate both returned false: one underlying fact, +// namely that the committed .gitattributes no longer equals its emitting authority. This is real +// generated-artifact drift, not a stale expectation. The floor cut's generated-artifact drift +// gates are currently absent, so nothing refused the authority/artifact disagreement when it was +// introduced; this bounded row keeps the two projections attached to the one repair obligation. +data gitattributes_committed_emit_drift_stall: GuaranteeStall = GuaranteeStall { + subject: "the committed .gitattributes differs from the bytes derived by its emitting authority", + current: OutsideTheLadder, + ceiling: MechanicallyPreventable, + blocker: ClimbableButUnbuilt, + population: BoundedPopulation { members: Cons { head: "test.claim.gitattributes_emit_witness.witness_committed_matches_emit_holds", tail: Cons { head: "test.claim.gitattributes_emit_witness.witness_holds", tail: Empty {} } } }, + next_rung_trigger: "node://adhoc-16f7520a-85f lands: identify the authority edit that introduced the drift, regenerate .gitattributes from that authority, and restore a required generated-artifact drift gate so later authority/artifact disagreement refuses" +} diff --git a/dag/gunbc/guarantee_stall/heterogeneous_child_list_stall.dag b/dag/gunbc/guarantee_stall/heterogeneous_child_list_stall.dag new file mode 100644 index 00000000000..260a70a6efc --- /dev/null +++ b/dag/gunbc/guarantee_stall/heterogeneous_child_list_stall.dag @@ -0,0 +1,21 @@ +module gunbc.guarantee_stall.heterogeneous_child_list_stall + +import gunbc.guarantee_rung { OutsideTheLadder, StructurallyImpossible } +import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, BoundedPopulation } + +data heterogeneous_child_list_stall: GuaranteeStall = GuaranteeStall { + subject: "a type's child list may hold BOTH a type node and a field node, and v1.04_types child_type_node tells them apart by whether `inferred` is populated -- a stamp v1.02_parse field_to_child_node writes at PARSE TIME as Resolved, before any resolution has run. A child list that mixes the two kinds makes that accessor return the FIELD node where its caller expects the TYPE, with no diagnostic", + current: OutsideTheLadder, + ceiling: StructurallyImpossible, + blocker: ClimbableButUnbuilt, + population: BoundedPopulation { + members: [ + "v1.02_parse variant_to_child_node", + "v1.02_parse outputs_to_inferred", + "v1.02_parse parse_type_after_kw", + "v1.02_parse parse_type_body_from_prefix", + "v1.02_parse parse_type_expr" + ] + }, + next_rung_trigger: "v1.04_types child_type_node no longer INFERS SHAPE FROM PROVENANCE -- it discriminates a type child from a field child by something that states the kind, rather than by whether a derived-data slot happens to be occupied. The trigger is that CAPABILITY and not any artifact that would contribute to one: a tag added while the accessor still reads `inferred`-presence satisfies an artifact and leaves the hazard exactly where it is, which is the direction DESIGN section 4b(3) says this machinery structurally cannot see. Emptying the slot BEFORE that lands is the failure this row exists to prevent, not the repair -- it would silently reclassify every field child into the wrong arm at once" +} diff --git a/dag/gunbc/guarantee_stall/import_eligibility_resolution_stall.dag b/dag/gunbc/guarantee_stall/import_eligibility_resolution_stall.dag new file mode 100644 index 00000000000..b0c77b67e57 --- /dev/null +++ b/dag/gunbc/guarantee_stall/import_eligibility_resolution_stall.dag @@ -0,0 +1,53 @@ +module gunbc.guarantee_stall.import_eligibility_resolution_stall + +import gunbc.guarantee_rung { Mitigatable, StructurallyGuaranteed } +import gunbc.guarantee_stall { GuaranteeStall, AwaitsOneGrounding, UncountedNotEnumerable } + +// A REFERENCE THAT RESOLVES UNDER ONE IMPORT LIST AND REFUSES UNDER A SUPERSET OF IT. +// Filed as a class because the specimen is user-visible and nobody had filed it: adding an import +// of an UNRELATED module silently breaks a bare reference that resolved without it. The failure is +// loud at the reference -- an undefined-variable diagnostic -- but the CAUSAL relation is +// unreachable from it, since nothing in the message connects the new import line to the broken +// name and no author's model of what an import does predicts it. Loud failure with an unreachable +// cause is the shape that costs the most time per incident. +// +// MECHANISM, measured rather than inferred. cli_run build_both_closure_edge_index skips a file +// before populating bare_out for it when source_declares_import_lines is true, and the struct +// field's own doc calls bare_scan_eligible the import-stripped files that may originate +// bare-reference edges. So a bare reference is a closure edge ONLY from a zero-import file. +// Confirmed by discriminator rather than by reading the predicate: one four-file fixture, one +// binary, one line varied -- with no import the provider is pulled and the name resolves clean; +// with one import of an unrelated carrier the provider is not pulled and the name refuses. +// +// WHY THE CEILING IS GUARANTEED AND NOT IMPOSSIBLE: eligibility is decided from the file text the +// compiler already holds, so a closure relation that does not vary with import-declaration is +// derivable. It is not IMPOSSIBLE, because both programs remain writable -- the source can express +// a file with imports and one without; what a repair removes is the DIVERGENCE between them, not +// the ability to author either. +// ON THE GROUNDING FIELD, recorded because the first version of this row got it wrong in a way +// nothing in this repository would have caught. It cited "the ClosureBoundResolution ruling" as +// the authority the class waits on. No such authority exists: the name was coined in cross-session +// correspondence and its only occurrences in the tree were this row and its own trigger. That is +// DESIGN section 3's cite-the-symbol violation in its purest form -- a citation naming a symbol +// that does not resolve -- and it is the exposure the 2026-08-23 cited-symbol drop declared as +// unbounded, arriving inside two days of the census being decommissioned. Caught by review 55910, +// which is the mitigation that drop names and is strictly weaker than the wall it replaced. +// +// THE FINDING DOES NOT CARRY THE RECLASSIFICATION IT PROPOSED, and the distinction is the point of +// the coproduct. The review concluded that an unauthored authority makes this ClimbableButUnbuilt. +// It does not: waiting on a DECISION and waiting on CONSTRUCTION rank differently for work, and +// this class genuinely waits on the first -- the repair direction is undetermined, so building is +// not merely unstarted but unspecifiable. What the finding correctly kills is the pretence that +// the decision had a home. A blocker may name an open question; it may not name a phantom ruling. +data import_eligibility_resolution_stall: GuaranteeStall = GuaranteeStall { + subject: "a bare reference resolves under one import list and refuses under a superset of it, because bare-reference closure edges originate only from zero-import files", + current: Mitigatable, + ceiling: StructurallyGuaranteed, + blocker: AwaitsOneGrounding { + grounding: "an undecided QUESTION, stated here rather than cited, because no authority in this tree answers it yet: is candidacy for a subject asked against the CENSUS population or the CLOSURE population. The class cannot climb until that is decided, because the repair direction depends on the answer -- bounding lookup leaves the loader still admitting providers by bare reference, and bounding load changes which files enter the subject at all. So this stall waits on a DECISION rather than on construction, which is what separates it from ClimbableButUnbuilt -- and the separation is structural rather than a matter of degree: the two answers land in DIFFERENT LANES, bounding lookup being a semantic-authority repair and bounding load a proof-authority one, so the answer decides WHO BUILDS as well as WHAT. That is why the work here is not merely unstarted but UNSPECIFIABLE, and why filing this as ClimbableButUnbuilt would be worse than imprecise: it would tell a reader to go build something at a moment when no owner can be named, converting a blocked decision into misdirected effort. The question was coined in cross-session correspondence under a name that has no carrier here, and naming it as though a ruling existed would have been a citation to a symbol that does not resolve" + }, + population: UncountedNotEnumerable { + reason: "the AFFECTED population is references whose resolution would change, and nothing enumerates them -- a reference that resolves today emits no diagnostic to count and a reference that refuses is indistinguishable in the message from a genuinely absent declaration. What CAN be measured is the ELIGIBLE FILE count -- .dag files carrying no import line -- and that is a denominator for where the mechanism can ORIGINATE, never a count of what it affects. Quoting the eligible count as the class size is the conflation this row exists to prevent. No figure is carried here, and the omission is deliberate rather than an oversight: the count is a minority of the corpus that MOVES with every merge, no entry point re-derives it, and a transcribed number is a positional citation of a run's output -- unreachable from the thing that owns it, so it rots without anyone touching either end. A row whose whole subject is that a number is the WRONG denominator would be the worst possible place to freeze that number into source. The eligible count is also RISING by construction: the namespace cut takes modules to zero imports, so each wave switches bare-edge origination on for the modules it strips" + }, + next_rung_trigger: "the census-or-closure candidacy question is decided AND its answer lands as a namespace-cut PREREQUISITE rather than a post-cut repair, bounding which modules may supply a resolution candidate for a subject. Reclassified from post-cut to prerequisite because the cut is what makes the mechanism universal -- a repair scheduled after the event that generalises it is scheduled backwards. Not satisfied by bounding lookup alone: the closure constructor extends by bare reference to a fixpoint before any lookup runs, so a wall placed only at lookup sits downstream of the door that already opened" +} diff --git a/dag/gunbc/guarantee_stall/mandatory_tag_live_corpus_stall.dag b/dag/gunbc/guarantee_stall/mandatory_tag_live_corpus_stall.dag new file mode 100644 index 00000000000..67d0751a6b4 --- /dev/null +++ b/dag/gunbc/guarantee_stall/mandatory_tag_live_corpus_stall.dag @@ -0,0 +1,14 @@ +module gunbc.guarantee_stall.mandatory_tag_live_corpus_stall + +import v2.std.algebra { Cons, Empty } +import gunbc.guarantee_rung { OutsideTheLadder, MechanicallyPreventable } +import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, BoundedPopulation } + +data mandatory_tag_live_corpus_stall: GuaranteeStall = GuaranteeStall { + subject: "the live corpus contains a mandatory-tag violation", + current: OutsideTheLadder, + ceiling: MechanicallyPreventable, + blocker: ClimbableButUnbuilt, + population: BoundedPopulation { members: Cons { head: "v2.lens.mandatory_tag.corpus_scan_witness_test.corpus_live_clean_tree_wall_holds", tail: Empty {} } }, + next_rung_trigger: "the derived mandatory-tag violation population is empty" +} diff --git a/dag/gunbc/guarantee_stall/merge_admission_terminal_verdict_stall.dag b/dag/gunbc/guarantee_stall/merge_admission_terminal_verdict_stall.dag new file mode 100644 index 00000000000..14584d28598 --- /dev/null +++ b/dag/gunbc/guarantee_stall/merge_admission_terminal_verdict_stall.dag @@ -0,0 +1,49 @@ +module gunbc.guarantee_stall.merge_admission_terminal_verdict_stall + +import gunbc.guarantee_rung { Mitigatable, StructurallyGuaranteed } +import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, UncountedNotEnumerable } + +// FILED AS A STALL AND NOT AS A RUNG DROP, WHICH IS A CORRECTION TO THIS SUBJECT'S FIRST FILING +// ON THIS BRANCH (2026-09-03). A section 4b(3) drop ASSERTS A REGRESSION -- a change lowered a rung +// that was held -- and nothing here regressed. GitHub's required-status-checks rule has evaluated +// reported check runs the same way since ruleset 16178731 was created, so the capability below was +// NEVER held and declaring a previous rung of `MechanicallyPreventable` would be inventing a rung +// to drop from, exactly as `gunbc.rung_drop` `floor_cost_claim_qualification_unavailable` refused +// to do for its own subject. What actually existed was section 4b(1) rung INFLATION: this +// repository's "required lane" vocabulary, and `gunbc.merge_lifecycle`'s own prose naming +// `PerPrGateOnly` the live policy, described a wall that does not stand for an unreported context. +// The inflation is corrected in `gunbc.merge_admission` by making the live policy representable; +// what remains is a class below its ceiling, which is a 4b(2) stall and belongs here. +// +// THE OPERATOR HAS RULED, AND THAT IS WHY THE BLOCKER IS `ClimbableButUnbuilt` RATHER THAN A +// MISSING CAPABILITY. Escalated 2026-09-03 with three options -- enable the merge queue, make +// unreported required contexts blocking, or hold the hole open -- and the ruling was the third: +// "Leave the hole open for now - i know merging is not sound." That is an INFORMED ACCEPTANCE by +// the principal who can actuate the fix, recorded in those terms deliberately. A row whose reason +// reads "we could not fix this" ages into an excuse; one that records a decision taken with the +// population in view stays a decision, and can be revisited by the person who took it. Nothing in +// this repository can actuate it in any case: the branch-protection and rule-suites endpoints +// answer 403 to session tokens. +// +// WHAT IT COST, ON THE NIGHT IT WAS DECLARED, BECAUSE "for now" IS ONLY HONEST BESIDE ITS PRICE. +// gunbc#10236 merged at 19:49:43Z, three seconds after its `witnesses` run was created and before +// any job reported; that run concluded with `required-witnesses-build` and +// `required-witnesses-floor` both FAILURE, and the head landed as cfe19ea7 carrying two duplicate +// declarations that refused main at resolve. main stayed refusing until the repair merged. +// +// AND THE SECOND COMMIT THAT LANDED BROKEN THAT NIGHT CAME THROUGH THE OTHER HOLE, NOT THIS ONE -- +// stated because conflating them would inflate this row. gunbc#9981 merged at 20:29:53Z with a +// `witnesses` run on its own head that had COMPLETED SUCCESSFULLY at 20:26:54Z, so it is not this +// class. Its run was created at 19:37:37Z, twelve minutes before cfe19ea7 landed, so it carried a +// green receipt at a base that no longer existed and squashed onto a broken tip. That is +// `gunbc.merge_lifecycle`'s stale-base class -- admitted under `PerPrGateOnly`, refused under +// `KeyedReceipt` as `MergeDeniedStaleBase` -- whose standing instruction is to add a line rather +// than escalate, and the line is added there. TWO HOLES, ONE EACH, FORTY MINUTES APART. +data merge_admission_terminal_verdict_stall: GuaranteeStall = GuaranteeStall { + subject: "a merge into main lands a head that no required context has reached a terminal verdict on", + current: Mitigatable, + ceiling: StructurallyGuaranteed, + blocker: ClimbableButUnbuilt, + population: UncountedNotEnumerable { reason: "every future merge into refs/heads/main is exposed, so the population is open rather than a list. IT IS STILL MEASURABLE, AND THE PREDICATE IS THE INSTRUMENT RATHER THAN ANY COUNT: for a merged pull request, did a required `witnesses` run on ITS OWN head reach a terminal verdict before its `merged_at`. That predicate is decidable per merge from the runs and pulls endpoints and can be re-measured at any time; a reading of it on 2026-09-03 over the forty most recently merged pull requests found six that had none. THE SIX ARE A READING, NOT THE POPULATION, and this row states the difference because its neighbour `gunbc.rung_drop` `floor_cost_claim_qualification_unavailable` had to correct itself for exactly that conflation: a set selected by a measurement is a VIEW whose membership is a property of the measurement, and letting it stand in for the population joins two objects by an assumption. A frozen count would also be a change detector rather than an instrument -- automating its update collapses it to measure() == measure()" }, + next_rung_trigger: "NO HEAD LANDS ON main WITHOUT A TERMINAL VERDICT FROM EVERY REQUIRED CONTEXT ON THE CONTENT BEING MERGED -- terminal rather than merely non-failing, because the state this row is about is a context that has reached NO VERDICT AT ALL at the instant of the merge, and a trigger reading `every required context reported non-failure` is satisfied by that state vacuously. Demonstrated by a RED on a merge attempted before its run reports, not by a configuration screenshot. TWO ARTIFACTS WOULD DELIVER IT AND NEITHER IS THE TRIGGER: GitHub's merge queue, which establishes it by construction because the queue runs the required workflow on the queued ref and nothing lands without that run; or making an unreported required context blocking. IF EITHER IS NAMED IN A LATER CLAIM THAT THIS STALL HAS CLIMBED, THE CLAIM MUST STATE WHAT THE ARTIFACT WAS SUFFICIENT FOR -- enabling a queue for one branch pattern while the pull-request path stays merge-able past an unreported context satisfies the artifact and leaves the capability dead, which is the grain mismatch a corpus-shaped loss with a setting-shaped trigger always produces" +} diff --git a/dag/gunbc/guarantee_stall/next_rung_trigger_enforcement_stall.dag b/dag/gunbc/guarantee_stall/next_rung_trigger_enforcement_stall.dag new file mode 100644 index 00000000000..2f2f2c7bd24 --- /dev/null +++ b/dag/gunbc/guarantee_stall/next_rung_trigger_enforcement_stall.dag @@ -0,0 +1,25 @@ +module gunbc.guarantee_stall.next_rung_trigger_enforcement_stall + +import gunbc.guarantee_rung { Mitigatable, MechanicallyPreventable } +import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, UncountedNotEnumerable } + +// THIS ROW IS THE STALL CARRIER'S OWN CLASS, and it sits in its own module for the reason every +// other row does: the stall is in the stall machinery itself, whose type authority is +// `gunbc.guarantee_stall`, and a row that lived inside that module would make the enumeration +// cyclic. +// The population is UncountedNotEnumerable rather than the 133 sites the sweep found, deliberately. +// A measured figure copied into a row is a transcription of an instrument's output, which this +// repository rules against, and it would additionally be the wrong number: 133 counts PHRASE +// OCCURRENCES, and a class that mentions its trigger three times is one stall, while a witness +// asserting the phrase is none. The population has no identity to count at, and that is the finding +// rather than a gap in the sweep. +data next_rung_trigger_enforcement_stall: GuaranteeStall = GuaranteeStall { + subject: "DESIGN section 4b(2) next-rung trigger enforcement", + current: Mitigatable, + ceiling: MechanicallyPreventable, + blocker: ClimbableButUnbuilt, + population: UncountedNotEnumerable { + reason: "a next-rung trigger is authored as prose, so it has no identity to count at. The majority of sites sit inside // annotations, which DESIGN section 4c makes unreadable to any Accepted program, so no lens can enumerate them however it is written -- the shortfall is the representation, not the sweep" + }, + next_rung_trigger: "every class this repository declares below its ceiling declares it through gunbc.guarantee_stall GuaranteeStall rather than in prose, at which point the population becomes a fold over rows and a stall missing its trigger has no spelling. Not satisfied by this carrier existing: one row is a carrier with a consumer, not a migrated population, and the 4b(2) obligation stays review diligence for every class still stalling in an annotation" +} diff --git a/dag/gunbc/guarantee_stall/non_fold_residue_roster_stall.dag b/dag/gunbc/guarantee_stall/non_fold_residue_roster_stall.dag new file mode 100644 index 00000000000..9b3dbbe5478 --- /dev/null +++ b/dag/gunbc/guarantee_stall/non_fold_residue_roster_stall.dag @@ -0,0 +1,14 @@ +module gunbc.guarantee_stall.non_fold_residue_roster_stall + +import v2.std.algebra { Cons, Empty } +import gunbc.guarantee_rung { OutsideTheLadder, MechanicallyPreventable } +import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, BoundedPopulation } + +data non_fold_residue_roster_stall: GuaranteeStall = GuaranteeStall { + subject: "the live non-fold residue contains an unrostered or stale identity", + current: OutsideTheLadder, + ceiling: MechanicallyPreventable, + blocker: ClimbableButUnbuilt, + population: BoundedPopulation { members: Cons { head: "v2.test.lens_non_fold_residue.non_fold_residue_test.non_fold_residue_no_unrostered_or_stale", tail: Empty {} } }, + next_rung_trigger: "the derived unrostered and stale non-fold-residue populations are both empty" +} diff --git a/dag/gunbc/guarantee_stall/observation_heartbeat_lockstep_stall.dag b/dag/gunbc/guarantee_stall/observation_heartbeat_lockstep_stall.dag new file mode 100644 index 00000000000..a7c74c2ca61 --- /dev/null +++ b/dag/gunbc/guarantee_stall/observation_heartbeat_lockstep_stall.dag @@ -0,0 +1,14 @@ +module gunbc.guarantee_stall.observation_heartbeat_lockstep_stall + +import v2.std.algebra { Cons, Empty } +import gunbc.guarantee_rung { OutsideTheLadder, StructurallyGuaranteed } +import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, BoundedPopulation } + +data observation_heartbeat_lockstep_stall: GuaranteeStall = GuaranteeStall { + subject: "the observation heartbeat implementation and its declared cadence are out of lockstep", + current: OutsideTheLadder, + ceiling: StructurallyGuaranteed, + blocker: ClimbableButUnbuilt, + population: BoundedPopulation { members: Cons { head: "test.claim.observation_lockstep_witness_test.w_heartbeat_period_matches_the_seed_cadence", tail: Cons { head: "test.claim.observation_lockstep_witness_test.w_heartbeat_source_still_refuses_to_fabricate", tail: Empty {} } } }, + next_rung_trigger: "node://adhoc-3cb769e0-0a6 lands: the heartbeat period is derived from one declared cadence and the source refuses fabricated heartbeat observations" +} diff --git a/dag/gunbc/guarantee_stall/operation_argv_binding_wall_stall.dag b/dag/gunbc/guarantee_stall/operation_argv_binding_wall_stall.dag new file mode 100644 index 00000000000..1f1cf46a046 --- /dev/null +++ b/dag/gunbc/guarantee_stall/operation_argv_binding_wall_stall.dag @@ -0,0 +1,14 @@ +module gunbc.guarantee_stall.operation_argv_binding_wall_stall + +import v2.std.algebra { Cons, Empty } +import gunbc.guarantee_rung { OutsideTheLadder, StructurallyGuaranteed } +import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, BoundedPopulation } + +data operation_argv_binding_wall_stall: GuaranteeStall = GuaranteeStall { + subject: "the operation-argv binding wall does not materialize the previously unbindable operation", + current: OutsideTheLadder, + ceiling: StructurallyGuaranteed, + blocker: ClimbableButUnbuilt, + population: BoundedPopulation { members: Cons { head: "test.claim.operation_argv_binding_wall_witness.operation_argv_previously_unbindable_operation_now_materializes", tail: Empty {} } }, + next_rung_trigger: "node://adhoc-a3b0e05f-374 lands: the operation-argv binding wall materializes the controlled previously-unbindable operation" +} diff --git a/dag/gunbc/guarantee_stall/parse_ingest_grammar_relation_stall.dag b/dag/gunbc/guarantee_stall/parse_ingest_grammar_relation_stall.dag new file mode 100644 index 00000000000..92f6435cb83 --- /dev/null +++ b/dag/gunbc/guarantee_stall/parse_ingest_grammar_relation_stall.dag @@ -0,0 +1,14 @@ +module gunbc.guarantee_stall.parse_ingest_grammar_relation_stall + +import v2.std.algebra { Cons, Empty } +import gunbc.guarantee_rung { OutsideTheLadder, StructurallyGuaranteed } +import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, BoundedPopulation } + +data parse_ingest_grammar_relation_stall: GuaranteeStall = GuaranteeStall { + subject: "parse and ingest disagree over the same grammar round trip", + current: OutsideTheLadder, + ceiling: StructurallyGuaranteed, + blocker: ClimbableButUnbuilt, + population: BoundedPopulation { members: Cons { head: "v2.test.execution.emit_ingest_grammar_relation_round_trip.same_grammar_parse_ingest_bridge_holds", tail: Empty {} } }, + next_rung_trigger: "the same-grammar parse-to-ingest round trip holds" +} diff --git a/dag/gunbc/guarantee_stall/pre_resolve_entry_closure_module_identity_stall.dag b/dag/gunbc/guarantee_stall/pre_resolve_entry_closure_module_identity_stall.dag new file mode 100644 index 00000000000..e77457eb963 --- /dev/null +++ b/dag/gunbc/guarantee_stall/pre_resolve_entry_closure_module_identity_stall.dag @@ -0,0 +1,20 @@ +module gunbc.guarantee_stall.pre_resolve_entry_closure_module_identity_stall + +import gunbc.guarantee_rung { OutsideTheLadder, StructurallyGuaranteed } +import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, BoundedPopulation } + +// THE DELIBERATELY DROPPED HALF OF gunbc#10258'S DISPLAY CONTRACT. That lane printed module +// identity beside source path from ResolvedGraph, but only after typed resolution. The +// loader-boundary preflight that replaced it answers the actual landing decision at its native +// grain -- repository-path intersection -- and cannot project resolved module identity because +// SourceFile carries only path and content. Reparsing the content or reconstructing a plausible +// path-to-name mapping would mint a second identity authority, so the replacement refuses that +// tempting widening and records the absent capability here instead. +data pre_resolve_entry_closure_module_identity_stall: GuaranteeStall = GuaranteeStall { + subject: "a routed entry's exact loader-boundary closure can be enumerated by repository path before typed resolution, but cannot be enumerated by resolved module identity at that same pre-resolution boundary", + current: OutsideTheLadder, + ceiling: StructurallyGuaranteed, + blocker: ClimbableButUnbuilt, + population: BoundedPopulation { members: ["claim_batch --print-entry-closure"] }, + next_rung_trigger: "the modeled routed-entry execution path exposes module identity joined to every loader-boundary source path before typed resolution, derived from its existing module-declaration facts rather than by reparsing source text or reconstructing identity from path spelling" +} diff --git a/dag/gunbc/guarantee_stall/prose_declared_rung_drop_stall.dag b/dag/gunbc/guarantee_stall/prose_declared_rung_drop_stall.dag new file mode 100644 index 00000000000..c906971d048 --- /dev/null +++ b/dag/gunbc/guarantee_stall/prose_declared_rung_drop_stall.dag @@ -0,0 +1,66 @@ +module gunbc.guarantee_stall.prose_declared_rung_drop_stall + +import gunbc.guarantee_rung { Mitigatable, StructurallyImpossible } +import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, BoundedPopulation } + +// THE PROSE HALF OF THE DROP ROSTER, DECLARED AS A STALL BECAUSE THAT IS WHAT IT IS. 26 of +// gunbc.rung_drop's rows state their DESIGN section 4b(3) fields -- previous rung, temporary rung, +// reason, population, restoration trigger -- only inside an `authored` paragraph, so for those rows +// the obligation 4b(3) states is met by a human reading and by nothing a program can fold. The four +// rows consolidated from the deleted gunbc.guarantee_rung_drop carry the fields typed, which is +// what makes this a stall with a known repair rather than a limit. +// +// GROWTH OF THE ARM IS VISIBLE BUT NOT PREVENTED, AND THIS ROW SAID OTHERWISE FIRST. Its first +// version asserted that a further prose row was structurally impossible because +// gunbc.rung_drop LegacyProseIdentity had no constructor for one. That was falsified within hours by +// spark_serving_local_artifact_not_reproducible, authored on another lane against the +// pre-consolidation shape and landed in main mid-consolidation; admitting it cost one arm. The +// enumeration makes growth UNSILENT -- an edit to a named list, visible in review, counted by a fold +// -- and that is mechanically preventable, not structural. What stalls is the SHRINKING of the arm, +// which is per-row work with no mechanical oracle: +// deciding which sentence of a paragraph is its reason and which its population is semantic +// rewriting, and several of these paragraphs argue at length about that very question. Each split +// deletes one arm from that coproduct, so the arm count IS the remaining debt and nothing has to be +// counted separately. +// +// THE TRIGGER NAMES THE CAPABILITY, not the last row. A trigger reading "the final row is split" +// would be satisfiable by a split that fabricated fields, which is the failure the prose arm exists +// to avoid; the capability is that every drop's five fields are readable AS DATA, which no +// fabricated split delivers. +data prose_declared_rung_drop_stall: GuaranteeStall = GuaranteeStall { + subject: "a declared section 4b(3) rung drop states its five fields only as prose, so its reason, population and restoration trigger are unreadable by any fold", + current: Mitigatable, + ceiling: StructurallyImpossible, + blocker: ClimbableButUnbuilt, + population: BoundedPopulation { + members: [ + "gunbc.rung_drop spark_serving_local_artifact_not_reproducible", + "gunbc.rung_drop floor_cut", + "gunbc.rung_drop measurement_bankruptcy", + "gunbc.rung_drop regen_producer", + "gunbc.rung_drop cited_symbol_census", + "gunbc.rung_drop emit_stage_blocking", + "gunbc.rung_drop lens_enforcement_censuses", + "gunbc.rung_drop required_gate_bankruptcy", + "gunbc.rung_drop text_boundary_identity_wall", + "gunbc.rung_drop fabric_evidence_gating", + "gunbc.rung_drop emitted_bytes_witness_required_lane", + "gunbc.rung_drop direct_call_arg_seam_v2_exemption", + "gunbc.rung_drop floor_cost_claim_qualification_unavailable", + "gunbc.rung_drop spark_role_scoped_retirement_production_root", + "gunbc.rung_drop floor_cut_heal", + "gunbc.rung_drop floor_cut_effect_gates", + "gunbc.rung_drop floor_cut_fmt_gate", + "gunbc.rung_drop floor_cut_merge_admission_stamping", + "gunbc.rung_drop floor_cut_falsifier_cadence", + "gunbc.rung_drop builtin_signature_arity_pairing_fabricates", + "gunbc.rung_drop concat_binary_signature_exempt_from_arg_binding", + "gunbc.rung_drop namespace_admission_consumed_row_deletion", + "gunbc.rung_drop dashboard_merge_ready_semantic_admissibility", + "gunbc.rung_drop floor_cut_behavioural_regression_differential", + "gunbc.rung_drop floor_cut_receipt_discriminating_arms", + "gunbc.rung_drop floor_cut_regen_second_generation_agreement" + ] + }, + next_rung_trigger: "EVERY row in gunbc.rung_drop rung_drop_roster carries TypedDeclaration -- its previous rung, temporary rung, reason, bounded population and restoration trigger readable as data and not as a paragraph -- with each split reviewed as its own readable diff against the paragraph it replaces, at which point LegacyProseIdentity and the AuthoredProse arm are both deleted and the class is structurally impossible rather than empty" +} diff --git a/dag/gunbc/guarantee_stall/required_regen_host_derivation_stall.dag b/dag/gunbc/guarantee_stall/required_regen_host_derivation_stall.dag new file mode 100644 index 00000000000..59cd5d25cce --- /dev/null +++ b/dag/gunbc/guarantee_stall/required_regen_host_derivation_stall.dag @@ -0,0 +1,18 @@ +module gunbc.guarantee_stall.required_regen_host_derivation_stall + +import v2.std.algebra { Cons, Empty } +import gunbc.guarantee_rung { Mitigatable, StructurallyGuaranteed } +import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, BoundedPopulation } + +// The candidate-tree producer drop is retired separately in gunbc.rung_drop: executed clean and +// drift arms both produced and named the candidate before adjudication. That restoration does not +// make the hand-maintained host mirror structural. Keeping this as its own stall prevents a new +// climb obligation from extending the lifetime of the retired producer drop. +data required_regen_host_derivation_stall: GuaranteeStall = GuaranteeStall { + subject: "required-regen host ordering is hand-maintained beside its modeled carrier", + current: Mitigatable, + ceiling: StructurallyGuaranteed, + blocker: ClimbableButUnbuilt, + population: BoundedPopulation { members: Cons { head: "v1_compiler.required_regen_host.run_required_regen", tail: Empty {} } }, + next_rung_trigger: "v1_compiler.required_regen_host run_required_regen is derived from v2.workflow.required_regen required_regen_run, with that derivation SUFFICIENT FOR preserving the carrier's exhaustive verdict mapping: every host verdict after successful emission carries the CandidateTree adjudicated for that verdict, and only an emission that produced no tree reaches a tree-less host arm. A generator that merely emits the host, or agreement on one verdict arm, does not satisfy this trigger; the whole host mapping must be constructed from the carrier so candidate production before adjudication has one authority rather than a modeled carrier and a hand-maintained host mirror" +} diff --git a/dag/gunbc/guarantee_stall/retained_rust_live_tree_migration_stall.dag b/dag/gunbc/guarantee_stall/retained_rust_live_tree_migration_stall.dag new file mode 100644 index 00000000000..ba2a3fdc6c0 --- /dev/null +++ b/dag/gunbc/guarantee_stall/retained_rust_live_tree_migration_stall.dag @@ -0,0 +1,14 @@ +module gunbc.guarantee_stall.retained_rust_live_tree_migration_stall + +import v2.std.algebra { Cons, Empty } +import gunbc.guarantee_rung { OutsideTheLadder, MechanicallyPreventable } +import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, BoundedPopulation } + +data retained_rust_live_tree_migration_stall: GuaranteeStall = GuaranteeStall { + subject: "live Rust-test discovery disagrees with the retained-kernel migration authority", + current: OutsideTheLadder, + ceiling: MechanicallyPreventable, + blocker: ClimbableButUnbuilt, + population: BoundedPopulation { members: Cons { head: "v2.test.lens_test_migration_debt.test_migration_debt_test.retained_rust_kernel_wall_holds_against_live_tree", tail: Empty {} } }, + next_rung_trigger: "live Rust-test discovery and the retained-kernel authority join exactly" +} diff --git a/dag/gunbc/guarantee_stall/roster.dag b/dag/gunbc/guarantee_stall/roster.dag new file mode 100644 index 00000000000..15a1cf297dc --- /dev/null +++ b/dag/gunbc/guarantee_stall/roster.dag @@ -0,0 +1,189 @@ +module gunbc.guarantee_stall.roster + +// THE ROSTER IS THE ENUMERATION AND THE FOLDS OVER IT, held apart from `gunbc.guarantee_stall` +// because the import graph's one structural law is acyclicity: every row module imports the +// `GuaranteeStall` type from that module, so the module carrying the type cannot import the rows +// back. The type is the shape, the files are the facts, and this module is the list. +// +// ORDER IS SOURCE ORDER AND IS LOAD-BEARING for the same reason the failure-mode roster's is: a +// consumer that renders rows renders them in roster order, so sorting this list would reorder +// every projection derived from it. Append at the end. + +import std.types { List, Bool } +import v2.std.algebra { fold_list } +import gunbc.guarantee_stall { GuaranteeStall } +import gunbc.guarantee_stall.pre_resolve_entry_closure_module_identity_stall { pre_resolve_entry_closure_module_identity_stall } +import gunbc.guarantee_stall.merge_admission_terminal_verdict_stall { merge_admission_terminal_verdict_stall } +import gunbc.guarantee_stall.generated_artifact_registry_membership_stall { generated_artifact_registry_membership_stall } +import gunbc.guarantee_stall.authority_target_same_expression_equivalence_stall { authority_target_same_expression_equivalence_stall } +import gunbc.guarantee_stall.runner_microvm_guest_size_derivation_stall { runner_microvm_guest_size_derivation_stall } +import gunbc.guarantee_stall.import_eligibility_resolution_stall { import_eligibility_resolution_stall } +import gunbc.guarantee_stall.next_rung_trigger_enforcement_stall { next_rung_trigger_enforcement_stall } +import gunbc.guarantee_stall.heterogeneous_child_list_stall { heterogeneous_child_list_stall } +import gunbc.guarantee_stall.doc_graph_orphan_population_stall { doc_graph_orphan_population_stall } +import gunbc.guarantee_stall.doc_graph_dangling_link_population_stall { doc_graph_dangling_link_population_stall } +import gunbc.guarantee_stall.enforcement_live_closure_gate_stall { enforcement_live_closure_gate_stall } +import gunbc.guarantee_stall.mandatory_tag_live_corpus_stall { mandatory_tag_live_corpus_stall } +import gunbc.guarantee_stall.parse_ingest_grammar_relation_stall { parse_ingest_grammar_relation_stall } +import gunbc.guarantee_stall.required_regen_host_derivation_stall { required_regen_host_derivation_stall } +import gunbc.guarantee_stall.self_host_candidate_generation_add_slice_stall { self_host_candidate_generation_add_slice_stall } +import gunbc.guarantee_stall.non_fold_residue_roster_stall { non_fold_residue_roster_stall } +import gunbc.guarantee_stall.retained_rust_live_tree_migration_stall { retained_rust_live_tree_migration_stall } +import gunbc.guarantee_stall.variant_owner_identity_stall { variant_owner_identity_stall } +import gunbc.guarantee_stall.gitattributes_committed_emit_drift_stall { gitattributes_committed_emit_drift_stall } +import gunbc.guarantee_stall.wall_deadline_shared_fill_attribution_stall { wall_deadline_shared_fill_attribution_stall } +import gunbc.guarantee_stall.builtin_parameter_name_forked_across_hand_authored_sites_stall { builtin_parameter_name_forked_across_hand_authored_sites_stall } +import gunbc.guarantee_stall.algebra_operation_associativity_undeclarable_stall { algebra_operation_associativity_undeclarable_stall } +import gunbc.guarantee_stall.deployed_repository_empty_root_bootstrap_stall { deployed_repository_empty_root_bootstrap_stall } +import gunbc.guarantee_stall.prose_declared_rung_drop_stall { prose_declared_rung_drop_stall } +import gunbc.guarantee_stall.two_nat_authorities_stall { two_nat_authorities_stall } +import gunbc.guarantee_stall.external_model_scope_live_cover_stall { external_model_scope_live_cover_stall } +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 } + +// 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 +// is DEICTIC -- "the fifteen executing identities below", "these four pre-existing facts" -- and +// nothing in the rows themselves records which cohort a row arrived in, so a per-row assignment +// would be an authored guess about a measurement nobody can re-derive. They are moved rather than +// reworded, and the roster is the one module that sees every row at once, which is the only place +// a claim about a SET of rows can be true. + +// DECLINED-LIVE-TREE CENSUS, observed by required-floor run 32882641450 after the root decline +// stopped hiding these subjects. The fifteen executing identities below project TEN facts. They +// are stalls rather than drops: no guarantee stopped holding in this change; the facts were outside +// the ladder because no required consumer executed them. `ClimbableButUnbuilt` states that each +// repair is specifiable. Assignment is a dashboard routing fact and deliberately does not live in +// this semantic carrier. + +// REQUIRED-FLOOR RUN 32918791246 exposed these four pre-existing facts after the +// DeclinedLiveTree arm stopped withholding their nine witness identities. None of their carriers +// is changed by that deletion. They are declared rung drops rather than expected-red enrolments: +// the witnesses remain ordinary, executing failures until the separately routed repair lands. +// The work-item identity is part of each next-rung trigger, so ownership survives a squash merge +// beside the bounded population and the semantic condition that ends the drop. + +// THE THREE CITED WORK ITEMS ARE ALREADY status=done AND THEIR CONDITIONS ARE NOT MET, measured +// 2026-08-28 against the dashboard and against required-floor run 33140608194. adhoc-89fcf94a-bdd, +// adhoc-3cb769e0-0a6 and adhoc-a3b0e05f-374 all report done, while frontier_cover_of_live_extdeps_tree_holds +// is one of that run's 47 FAIL rows and a direct count puts 21 live dag/extdeps modules outside the +// scope frontier's union of scope_carrier_paths, scope_machinery_exempt_paths and the legacy manifest. +// So the node ids are PROVENANCE for who was asked, never evidence that the climb happened: a closed +// work item beside an unmet condition is the reported-results-versus-committed-claims gap, and reading +// "it lands" as satisfied would inflate three classes that are still at the bottom of the ladder. +// EACH TRIGGER'S OPERATIVE HALF IS THE SEMANTIC CLAUSE AFTER THE COLON, which is what a later reader +// must re-measure; the rows are authored that way and survive their work items unchanged. + +// THE ROSTER, AND WHY IT IS A FOLD RATHER THAN ONE EXEMPLAR PER ROW. +// +// Every GuaranteeStall row was a DECLARATION nothing observed. The witness exercised ONE of them +// by name, so the rest were typed prose -- correct in shape, consumed by nothing, and exactly the +// inert-carrier failure DESIGN section 5 names: coverage by illusion, worse than absent because a +// registered-looking row is cited as registration. Found in review of the third row, and true of +// the first two since they landed. +// +// A PER-ROW WITNESS WOULD BE THE SAME DEFECT WEARING MORE TESTS: N copies of one assertion, each +// proving the FUNCTIONS work and none proving THAT ROW is enrolled, with the coverage tracking how +// many authors remembered rather than how many rows exist. The fold makes the obligation scale +// with the population instead. +// +// THE ROSTER IS HAND-MAINTAINED AND THAT IS A REAL WEAKNESS, stated rather than buried. A row +// added above and not added here is invisible to the fold -- the same staleness these rows warn +// about, one level up. Declaration IDENTITIES are derivable today: v2.std.decl_index +// data_decl_type_facts enumerates every top-level data declaration with its declared type. The +// VALUES needed by this List are not. DeclFact.node is an initializer-identity +// projection. gunbc.seed_closed_vocabulary_wildcard_census files the NotVariantValue answer for +// initializer forms outside that projection's ExprRecordLit and ExprVar arms as +// FabricatedSubstitution. Independently, a measured ExprRecordLit takes +// marshal_plain_record_projection, whose marshal_field_initializer_projection path collapses field +// values needed to reconstruct the GuaranteeStall, including primitive string and list payloads +// nested under ClimbBlocker and StallPopulation, to NotVariantValue through +// variant_value_from_typechecked_expr; no census row currently files that field-value site. So the +// alternative today is still this authored roster or no consumer, but +// declaration enumeration is no longer the blocker. +// TRIGGER: fail-closed typed data-value reflection enumerates exactly every top-level data +// declaration under the gunbc.guarantee_stall module tree whose declared type is GuaranteeStall, +// and no declaration outside it, and projects each fully evaluated value in deterministic roster +// order, +// SUFFICIENT FOR reconstructing every field of every GuaranteeStall row and refusing any initializer +// form or field value it cannot project rather than substituting NotVariantValue. At that point this +// list is DERIVED and an unenrolled row has no spelling. A declaration-identity, +// initializer-shape, or corpus-wide GuaranteeStall surface alone does not satisfy the trigger. + +data all_guarantee_stalls: List = [ + pre_resolve_entry_closure_module_identity_stall, + merge_admission_terminal_verdict_stall, + generated_artifact_registry_membership_stall, + authority_target_same_expression_equivalence_stall, + runner_microvm_guest_size_derivation_stall, + import_eligibility_resolution_stall, + next_rung_trigger_enforcement_stall, + heterogeneous_child_list_stall, + doc_graph_orphan_population_stall, + doc_graph_dangling_link_population_stall, + enforcement_live_closure_gate_stall, + mandatory_tag_live_corpus_stall, + parse_ingest_grammar_relation_stall, + required_regen_host_derivation_stall, + self_host_candidate_generation_add_slice_stall, + non_fold_residue_roster_stall, + retained_rust_live_tree_migration_stall, + variant_owner_identity_stall, + gitattributes_committed_emit_drift_stall, + wall_deadline_shared_fill_attribution_stall, + builtin_parameter_name_forked_across_hand_authored_sites_stall, + algebra_operation_associativity_undeclarable_stall, + deployed_repository_empty_root_bootstrap_stall, + prose_declared_rung_drop_stall, + two_nat_authorities_stall, + external_model_scope_live_cover_stall, + observation_heartbeat_lockstep_stall, + operation_argv_binding_wall_stall, +] + +// THE FOUR SUBJECTS RESTORED TO THE ROSTER, PINNED BY IDENTITY SO THEIR LOSS REFUSES. +// +// These four stalls were DECLARED in the stall carrier and absent from all_guarantee_stalls, so the three +// walls written over that roster ranged over 21 of the 25 rows the carrier then declared. The walls were +// green because their input was short, which is exactly the shape +// gunbc.recurring_failure_mode check_subject_narrower_than_its_declared_claim names: a green check +// whose declared subject is a strict superset of the population it actually ranges over. +// +// WHAT THIS CHECK COVERS AND WHAT IT DOES NOT, stated because a check that does not state its own +// denominator cannot be distinguished from a complete one. It covers exactly these four subjects: +// if any is dropped from the roster again, the fold refuses. It does NOT detect a NEW stall +// declared and left unrostered -- that requires a corpus-wide census of GuaranteeStall +// declarations joined against the roster, which is a separate obligation and is gated on whether +// its RED is authorable at all (a stall declared in a module the roster cannot import may not be +// expressible in any fixture, and a check whose RED has nowhere to live is a decoration). +// +// PRESENCE-EXACTLY-ONCE, NOT SET EQUALITY, and the asymmetry is deliberate: a new stall row must +// be admitted without editing this list, while a lost one must refuse. Exactly-once also refuses +// a DOUBLE entry, which set membership would accept and which reads as a merge that applied twice. +// PINNED BY REFERENCE TO THE DECLARATIONS, NOT BY TRANSCRIBING THEIR SUBJECTS. An earlier draft +// listed the four subjects as string literals and got all four WRONG -- the real subjects are full +// sentences, so the fold would have found zero matches and refused, or worse, been "fixed" by +// copying the prose in. A copied string is a second authority for text this file already declares, +// and it rots the moment a subject is reworded. Naming the declaration is the section 3 move, and +// after the one-file-per-row split the declaration is named by IMPORT, which refuses at resolve if +// the row module is renamed or deleted rather than silently matching nothing. +data restored_stalls: List = [ + two_nat_authorities_stall, + external_model_scope_live_cover_stall, + observation_heartbeat_lockstep_stall, + operation_argv_binding_wall_stall, +] + +fn every_restored_stall_is_rostered_once(ss: List) -> Bool { + fold_list( + xs: restored_stalls, + empty: true, + cons: fn(acc, want) { + acc && fold_list( + xs: ss, + empty: 0, + cons: fn(n, s) { if s.subject == want.subject { n + 1 } else { n } }, + ) == 1 + }, + ) +} diff --git a/dag/gunbc/guarantee_stall/runner_microvm_guest_size_derivation_stall.dag b/dag/gunbc/guarantee_stall/runner_microvm_guest_size_derivation_stall.dag new file mode 100644 index 00000000000..09c90025fca --- /dev/null +++ b/dag/gunbc/guarantee_stall/runner_microvm_guest_size_derivation_stall.dag @@ -0,0 +1,74 @@ +module gunbc.guarantee_stall.runner_microvm_guest_size_derivation_stall + +import gunbc.guarantee_rung { Mitigatable, StructurallyGuaranteed } +import gunbc.guarantee_stall { GuaranteeStall, AwaitsOneGrounding, BoundedPopulation } + +// THE MICROVM GUEST SIZE, filed by the change that removed the wrong derivation rather than by a +// later reviewer. This is AwaitsOneGrounding and not ClimbableButUnbuilt: the obstacle is not +// unwritten code, it is that the quantity to subtract may not exist as a constant at all -- a +// VMM's resident footprint scales with guest size through page tables, with the device model, and +// with host page size, so what upstream documents is typically a MEASURED overhead for one stated +// configuration, which is an observation about one boot rather than a property of the realization. +// A trigger reading "model the overhead" would presume that number exists and would be +// unsatisfiable in exactly the way this carrier's own rows warn about. +// +// THE POPULATION WAS RE-CENSUSED, NOT SPOT-REPAIRED, AND THE MEMBERSHIP RULE IS WRITTEN DOWN SO +// COMPLETENESS IS CHECKABLE. An earlier version of this row named runner_microvm_sizing_of_cores, +// which the same commit deleted, and gave the witness module as test.claim.runner.runner_microvm_ +// witness_test when the module declares test.claim.runner_microvm_witness_test with no intermediate +// segment. A phantom member beside an omitted live one means the row never carried the BOUNDED +// population DESIGN 4b requires, and two spot fixes would have left completeness unestablished -- +// so the row was re-derived from the module's declarations rather than edited. +// +// MEMBERSHIP RULE: a symbol is a member when, IN PRODUCTION, it cannot reach its intended answer +// because of the two missing quantities. That deliberately includes guest_memory_fits, which is +// correct code that always returns MemoryFitUnresolved on the production path, and deliberately +// excludes guest_resources_of_machine_config and the topology and credential arms, which decide +// fully today. It also includes fabric_cell_slice_desired_directives, which is not in this module: +// the CPU obstacle is owed there, and a row scoped to the file rather than the class would be +// satisfied while the capability stayed dead. +// +// THE TRIGGER CARRIES TWO CLAUSES AND BOTH ARE REQUIRED, because satisfying the first alone would +// take the admission's accept arm live having never executed. Retargeting the microVM witnesses +// onto the refusal path left the success path with NO executed coverage: RunnerMicroVmAdmitted is +// unreachable while sizing refuses, so every witness now proves a gate is passed on the way to a +// refusal and none proves an admissible VM is admitted. A gate whose accept arm has never run is +// not a gate that has been tested. +// +// THE CPU AXIS IS NOT A SECOND COPY OF THE MEMORY ONE, WHICH IS WHY THE TRIGGER SPLITS THEM. On +// memory the quantity may exist and be uncited. On CPU the cell realizes no absolute entitlement at +// all: fabric_cell_slice_desired_directives emits CPUWeight, a relative share that guarantees no +// amount of anything under contention. The absolute ceiling this fleet does declare is written by +// host_converge onto the RUNNER UNIT, a different systemd object from the cell slice -- so a guest +// vCPU count derived from the cell would equal a number the cell never enforces. That is the +// failure gunbc.ci.ci_runner_placement already records once: "the arithmetic said six threads per +// slot and the host was never told." +// +// AND THE CONTROLS MUST COME BACK AS FIT CONTROLS. The pair this row replaced asserted EQUALITY to +// the envelope in both directions -- it admitted a guest sized at the whole ceiling and refused a +// 4 GiB guest against a 16 GiB cell. Under containment the smaller guest FITS, so both arms were +// wrong in opposite directions while the pair looked discriminating. A nonconstant predicate with +// both polarities observed can still be answering a question nobody asked. +data runner_microvm_guest_size_derivation_stall: GuaranteeStall = GuaranteeStall { + subject: "gunbc.runner_microvm cannot derive a guest's resource envelope from the bounded cell on EITHER axis: memory needs a subtrahend for the Firecracker VMM's own footprint that is not cited anywhere, and CPU needs an absolute entitlement the cell does not carry", + current: Mitigatable, + ceiling: StructurallyGuaranteed, + blocker: AwaitsOneGrounding { + grounding: "what quantities, if any, relate a cell's declared envelope to an admissible guest. On MEMORY that may be a cited VMM footprint, or the finding that guest RAM is an operator-declared input BOUNDED BY the envelope rather than derived from it. On CPU it is prior: gunbc.fabric.fabric_cell_effect emits CPUWeight, a RELATIVE share that guarantees no amount of anything, so there is no absolute cell entitlement for a guest vCPU count to be derived from -- the absolute ceiling this fleet does declare, gunbc.host.host_converge runner_cpu_boundary_knobs writing CapacityQuota as a CPUQuota drop-in, lands on the RUNNER UNIT and not on the cell slice. One bounded execution context, two realizations, different axes enforced", + }, + population: BoundedPopulation { + members: [ + "gunbc.runner_microvm guest_memory_fits", + "gunbc.runner_microvm gunbc_runner_microvm_realization_reserve", + "gunbc.runner_microvm gunbc_runner_microvm_cell_cpu_entitlement", + "gunbc.runner_microvm runner_microvm_sizing", + "gunbc.runner_microvm runner_microvm_size_from_cell_envelope", + "gunbc.runner_microvm runner_microvm_admission_after_credential", + "gunbc.runner_microvm gunbc_runner_microvm_admission", + "gunbc.runner_microvm gunbc_runner_microvm_vm_config", + "gunbc.fabric.fabric_cell_effect fabric_cell_slice_desired_directives", + "test.claim.runner_microvm_witness_test", + ], + }, + next_rung_trigger: "BOTH of: (1) a quantity sufficient to DERIVE an admissible guest RAM from a cell envelope, or a decision that guest RAM is a declared input bounded by that envelope; AND (2) the cell realizing an ABSOLUTE CPU entitlement that a guest vCPU count can be derived from -- a CPUQuota or CPU set on the CELL SLICE, not the CPUQuota gunbc.host.host_converge already writes onto the runner UNIT -- or guest topology renamed as a separately declared product decision that is NOT derived from the cell. The clauses are separate because the obstacles differ in kind: the memory quantity may exist and merely be uncited, while the cell grants no CPU quantity at all, so a trigger naming only the memory subtrahend would be satisfied while the CPU axis stayed unfounded. THE THIRD CLAUSE THIS ROW CARRIED IS DISCHARGED: RunnerMicroVmAdmitted is reachable again and executed, because the realization reserve is a PARAMETER of the admission rather than a global, so a witness declaring one drives the accept arm while production still refuses. What is NOT discharged and is not claimed here is that PRODUCTION can reach that arm -- it cannot, and clauses 1 and 2 are what would change that" +} diff --git a/dag/gunbc/guarantee_stall/self_host_candidate_generation_add_slice_stall.dag b/dag/gunbc/guarantee_stall/self_host_candidate_generation_add_slice_stall.dag new file mode 100644 index 00000000000..4a21d4d6a8f --- /dev/null +++ b/dag/gunbc/guarantee_stall/self_host_candidate_generation_add_slice_stall.dag @@ -0,0 +1,14 @@ +module gunbc.guarantee_stall.self_host_candidate_generation_add_slice_stall + +import v2.std.algebra { Cons, Empty } +import gunbc.guarantee_rung { OutsideTheLadder, MechanicallyPreventable } +import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, BoundedPopulation } + +data self_host_candidate_generation_add_slice_stall: GuaranteeStall = GuaranteeStall { + subject: "self-host candidate generation, translation, and emission disagree on the add slice", + current: OutsideTheLadder, + ceiling: MechanicallyPreventable, + blocker: ClimbableButUnbuilt, + population: BoundedPopulation { members: Cons { head: "v2.test.execution.self_host_candidate_generation.candidate_generation_translate_self_emit_dag_add_slice_holds", tail: Cons { head: "v2.test.execution.emit_ingest_python_same_language_round_trip.emit_ingest_python_same_language_round_trip_holds", tail: Cons { head: "v2.test.execution.emit_ingest_python_same_language_round_trip.python_same_language_source_emit_round_trip_holds", tail: Cons { head: "v2.test.execution.emit_ingest_typescript_same_language_round_trip.emit_ingest_typescript_same_language_round_trip_holds", tail: Cons { head: "v2.test.execution.emit_ingest_typescript_same_language_round_trip.typescript_same_language_source_emit_round_trip_holds", tail: Empty {} } } } } } }, + next_rung_trigger: "candidate generation, translation, and self-emission agree on the add slice: infer derives grounding for the Arrow, Conj and Atom kinds of the add fn, so cross_language_compile stops carrying infer_grounding_not_derived over the same-language python and typescript parse fixtures" +} diff --git a/dag/gunbc/guarantee_stall/two_nat_authorities_stall.dag b/dag/gunbc/guarantee_stall/two_nat_authorities_stall.dag new file mode 100644 index 00000000000..7b9268d6be6 --- /dev/null +++ b/dag/gunbc/guarantee_stall/two_nat_authorities_stall.dag @@ -0,0 +1,30 @@ +module gunbc.guarantee_stall.two_nat_authorities_stall + +import gunbc.guarantee_rung { Mitigatable, StructurallyImpossible } +import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, UncountedNotEnumerable } + +// TWO Nat AUTHORITIES ARE ONE NAME ANSWERING FOR TWO CONCEPTS, and this row exists because review +// 57758 correctly refused a version of it that was narrated in prose beside one of the two nat_max +// declarations. The fork predates this lane; what this lane changed is that the Peano side now +// carries real operations, so the fork is load-bearing rather than latent. +// +// ClimbableButUnbuilt, NOT AwaitsOneGrounding, and review 57807 was right to refuse the first +// version of this row for saying otherwise. The modeling direction is already decided and its +// prerequisites discharged: gunbc.plans.dag_v2_defork_audit records the nat census complete with +// the per-concept design DESIGN READY (FreeMonoid shadow #6341 merged, generic-alias coproduct +// keystone green) and names the atomic wave file-by-file -- dag/std/nat.dag takes the coproduct and +// the Peano ops, the semiring alias is deleted, v2.std.nat becomes a thin reimport plus the law +// roster, integer and float repoint GroupCompletion to std.nat.Nat, every importer in the same +// push. Classifying that as awaiting a ruling would convert scheduled work into an indefinite +// decision stall, which is exactly the untracked stall DESIGN section 4b forbids, and would dilute +// the canonical plan by implying the question is still open. +data two_nat_authorities_stall: GuaranteeStall = GuaranteeStall { + subject: "std.nat Nat (CommutativeSemiring, realizing natively as a machine scalar) and v2.std.nat Nat (the Peano coproduct Zero | Succ) are two declarations answering for one name, so nat_add / nat_mul / nat_max / nat_compare each exist twice and a bare reference in a closure containing both modules is ambiguous", + current: Mitigatable, + ceiling: StructurallyImpossible, + blocker: ClimbableButUnbuilt, + population: UncountedNotEnumerable { + reason: "the declaration half IS enumerable -- std.nat and v2.std.nat both declaring Nat, with the per-operation forks nat_add / nat_mul / nat_max / nat_compare that no single function can serve because the two are different types -- but the exposure half is not, and one carrier answers for the whole population. The exposed set is every reference site whose CLOSURE contains both modules, and closure membership is transitive: a module importing one neighbour that reaches std.nat and another that reaches v2.std.nat has both without importing either. So a direct-import scan is not that set -- it currently names four dual-importing files and understates the real exposure -- and rendering those four as a BoundedPopulation would read as bounded while measuring the wrong property, which is the empty-observation narrow this carrier's second variant exists to prevent. It is bounded in principle by the corpus and shrinks to zero with the trigger below, but no enumeration here would be true when written", + }, + next_rung_trigger: "the atomic Nat unification wave specified in gunbc.plans.dag_v2_defork_audit: dag/std/nat.dag carrying the coproduct and the Peano operations with the semiring alias deleted, v2.std.nat reduced to a thin reimport plus the node-bound law roster, integer and float repointing GroupCompletion to std.nat.Nat, and every importer repointed in the same push -- retired by that wave landing and by nothing less, since deleting either declaration without deriving its operations would remove the operations its consumers call rather than unify the authority" +} diff --git a/dag/gunbc/guarantee_stall/variant_owner_identity_stall.dag b/dag/gunbc/guarantee_stall/variant_owner_identity_stall.dag new file mode 100644 index 00000000000..55605486bc3 --- /dev/null +++ b/dag/gunbc/guarantee_stall/variant_owner_identity_stall.dag @@ -0,0 +1,14 @@ +module gunbc.guarantee_stall.variant_owner_identity_stall + +import v2.std.algebra { Cons, Empty } +import gunbc.guarantee_rung { OutsideTheLadder, StructurallyImpossible } +import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, BoundedPopulation } + +data variant_owner_identity_stall: GuaranteeStall = GuaranteeStall { + subject: "runtime variant equality and native-representation selection derive from exact owner-module plus declaration identity, never parent/arm lexemes", + current: OutsideTheLadder, + ceiling: StructurallyImpossible, + blocker: ClimbableButUnbuilt, + population: BoundedPopulation { members: Cons { head: "v1_interpreter::cross_claim_memo_tests::same_spelled_variants_from_distinct_owners_reproduce_identity_residual", tail: Cons { head: "v1_interpreter::cross_claim_memo_tests::typed_bool_literals_do_not_need_lexeme_shorthands_but_zero_still_does", tail: Empty {} } } }, + next_rung_trigger: "NS-0B threads its exact owner-module plus declaration-name identity through VariantValueBinding, Value::Variant, hashing, and PortableValue::Variant; the same-spelled-owner residual changes from reproducing equality to requiring inequality, and the intentional Nat Zero native representation is selected by that identity rather than by the raw Zero lexeme" +} diff --git a/dag/gunbc/guarantee_stall/wall_deadline_shared_fill_attribution_stall.dag b/dag/gunbc/guarantee_stall/wall_deadline_shared_fill_attribution_stall.dag new file mode 100644 index 00000000000..2e12507997b --- /dev/null +++ b/dag/gunbc/guarantee_stall/wall_deadline_shared_fill_attribution_stall.dag @@ -0,0 +1,27 @@ +module gunbc.guarantee_stall.wall_deadline_shared_fill_attribution_stall + +import v2.std.algebra { Cons, Empty } +import gunbc.guarantee_rung { Mitigatable, StructurallyGuaranteed } +import gunbc.guarantee_stall { GuaranteeStall, ClimbableButUnbuilt, BoundedPopulation } + +// THE WALL DEADLINE STILL CHARGES A SHARED-ARTIFACT FILL TO WHICHEVER CLAIM PAID IT, and this row +// exists because a comment beside the code would go stale on the day the population changes while +// this row cannot. The 2026-08-27 attribution ruling has now been applied to three homes one at a +// time -- the completion-side CPU split, the completion-side WALL split, and the CPU evaluation +// deadline -- and each application was made only after that home's omission had cost something. +// The wall deadline is the fourth home and it is unrepaired. +// +// WHY IT IS SCOPED OUT RATHER THAN FIXED HERE: measured on run 33185280160, all 44 interruptions +// are on the `Cpu` clock, 44 of 44, so the wall arm is currently unexercised. That is a fact about +// today's population and NOT about the mechanism, which is exactly why the obligation is declared +// as a countable row rather than left as a note. The trigger is deliberately an OBSERVATION rather +// than a promise: the first wall-clock interruption to appear in the floor's ledger is the event +// that makes this reachable, and it fires without anyone remembering this row exists. +data wall_deadline_shared_fill_attribution_stall: GuaranteeStall = GuaranteeStall { + subject: "the wall evaluation deadline charges shared-artifact fill to the claim that paid it, so a wall interruption is a function of discovery order rather than of the row", + current: Mitigatable, + ceiling: StructurallyGuaranteed, + blocker: ClimbableButUnbuilt, + population: BoundedPopulation { members: Cons { head: "v1_interpreter.arm_wall_deadline", tail: Cons { head: "v1_interpreter.wall_deadline_remaining_ms", tail: Cons { head: "v1_interpreter.wall_deadline_exceeded_error", tail: Empty {} } } } }, + next_rung_trigger: "the required floor's ledger reports any INTERRUPTED-BEFORE-VERDICT row whose clock is Wall, at which point the wall deadline must read a fill-netted clock exactly as v1_interpreter.budgeted_cpu_nanos does for the CPU deadline" +} diff --git a/dag/gunbc/merge_lifecycle.dag b/dag/gunbc/merge_lifecycle.dag index 0da10f072df..1c5734a6947 100644 --- a/dag/gunbc/merge_lifecycle.dag +++ b/dag/gunbc/merge_lifecycle.dag @@ -167,7 +167,7 @@ import gunbc.merge_admission { // AND IT IS NOT BEING BUILT, BY RULING RATHER THAN BY OMISSION (2026-09-03). Escalated with three // options -- enable the queue, make unreported required contexts blocking, or hold the hole open -- // and the operator ruled the third: "Leave the hole open for now - i know merging is not sound." -// The class is therefore carried as `gunbc.guarantee_stall` `merge_admission_terminal_verdict_stall` +// The class is therefore carried as `gunbc.guarantee_stall.merge_admission_terminal_verdict_stall` // with the capability as its trigger, an informed acceptance rather than an unowned gap. A STALL // AND NOT A `gunbc.rung_drop` ROW: 4b(3) asserts a regression, and nothing regressed here. diff --git a/dag/test/claim/guarantee_stall_witness_test.dag b/dag/test/claim/guarantee_stall_witness_test.dag index 5c794c9b17d..0f99899271d 100644 --- a/dag/test/claim/guarantee_stall_witness_test.dag +++ b/dag/test/claim/guarantee_stall_witness_test.dag @@ -10,10 +10,11 @@ import gunbc.guarantee_stall { CannotClimbFurther, AwaitsOneGrounding, ClimbableButUnbuilt, BoundedPopulation, UncountedNotEnumerable, stall_is_below_ceiling, stall_report_message, - next_rung_trigger_enforcement_stall, - all_guarantee_stalls, every_stall_is_below_its_ceiling, every_stall_names_a_trigger, - every_restored_stall_is_rostered_once, restored_stalls, - heterogeneous_child_list_stall, stall_roster_size, + every_stall_is_below_its_ceiling, every_stall_names_a_trigger, stall_roster_size, +} +import gunbc.guarantee_stall.next_rung_trigger_enforcement_stall { next_rung_trigger_enforcement_stall } +import gunbc.guarantee_stall.roster { + all_guarantee_stalls, restored_stalls, every_restored_stall_is_rostered_once, } // Local one-liner over the builtin rather than an import: three test files already declare their diff --git a/src/v1/stage0/src/namespace_wave_admission.rs b/src/v1/stage0/src/namespace_wave_admission.rs index b225ec0349e..809275fc827 100644 --- a/src/v1/stage0/src/namespace_wave_admission.rs +++ b/src/v1/stage0/src/namespace_wave_admission.rs @@ -885,6 +885,40 @@ pub struct TransitionAdmission { /// "SAME RULE"). FIFTEENTH is the highest in use, so this is SIXTEENTH. A third duplicate would /// have made the entry uncitable by its own name -- which is what an ordinal is for. +/// TWENTIETH TRANSITION (2026-09-04), gunbc#10328, AND IT IS THE NINETEENTH'S OWN SHAPE APPLIED TO +/// THE SECOND LEDGER. `gunbc.guarantee_stall` is split one file per row, exactly as gunbc#10206 +/// split `gunbc.recurring_failure_mode`, and for the same measured reason: every row PR appended at +/// the declaration tail and the roster tail, so row lanes conflicted with each other by +/// construction. The direction is forced by acyclicity rather than chosen -- a row module imports +/// `GuaranteeStall` from the type module, so the type module cannot import the rows back -- which +/// is why the enumeration leaves for `gunbc.guarantee_stall.roster` and each row for +/// `gunbc.guarantee_stall.`. +/// +/// TEN DELTAS, TEN ROWS, ENUMERATED BY IDENTITY AND NOT MATCHED BY PATTERN, on the rule the +/// eighteenth transition states: a wildcard over "anything that moved under +/// gunbc.guarantee_stall" would also admit the next relocation nobody reviewed. All ten are +/// bindings in ONE consumer, `test.claim.guarantee_stall_witness_test`, and they split two ways -- +/// six whose spelling now resolves to the roster module (`all_guarantee_stalls`, +/// `restored_stalls`, `every_restored_stall_is_rostered_once`), four whose spelling now resolves to +/// one row module (`next_rung_trigger_enforcement_stall`). The three folds that take a +/// `List` PARAMETER did not move and produce no delta, which is the check on the +/// claim: had they moved too, this ledger would be showing thirteen. +/// +/// THE MEMBERSHIP ADDITIONS ARE NOT HERE AND THAT IS NOT AN OMISSION. The witness reaching the two +/// new modules classified `ExplicitlyEvaluatedZeroDelta` and auto-admits; only `TargetChanged` +/// refuses. A row for an auto-admitted disposition would be a decoration that later reports stale. +/// +/// THESE ROWS ARE DATA IN AN EXISTING DECLARED ROSTER, NOT NEW MACHINERY -- no branch, no dispatch, +/// no code path; the mechanism that reads them is unchanged. What would be a scaffold is a second +/// route around the adjudicator, and there is none. +/// +/// DISSOLVE-ON is gunbc#10328 merging, and the trigger names the CAPABILITY rather than an +/// artifact: once main carries the split, base and head both have it and NO RUN CAN PRODUCE THESE +/// TEN DELTAS. They will report CONSUMED rather than stale, born consumed like the #10206, SJT-1 +/// and DCH-1 cohorts, because a row authored in the same PR that performs its own move is satisfied +/// at the BASE of every later run. Their deletion is charged to WHOEVER NEXT TOUCHES THIS ROSTER, +/// which is this module's standing convention and not a follow-up PR anyone could forget. +/// /// EMPTY IS THE RESTING STATE between transitions, and it is not permissive: a run with a real /// delta still refuses it as UNADJUDICATED, closed by authoring a row and never by a silent /// admission. That is a claim about the MECHANISM and it holds whatever the roster contains. @@ -927,17 +961,122 @@ pub struct TransitionAdmission { /// ITS CONSUMPTION IS DECIDABLE ON THAT SAME RULE: once gunbc#10218 merges, the base binds the /// spelling to product.placement_supply, the delta stops being producible, and this row is owed /// deletion by the next roster-touching change. -pub const NAMESPACE_TRANSITION_ADMISSIONS: &[TransitionAdmission] = &[TransitionAdmission { - label: "gunbc#10218 identity-equality re-home: PhysicalAssetIdentity comparison moves to \ - the module that owns the type", - subject: AdmissionSubject::Binding { - module: "product.printed_chassis.manufacturing_manifest", - in_declaration: "scan_printer_assets", - spelling: "physical_asset_identity_eq", - target: "product.placement_supply", +/// +/// TWENTY-FOURTH DISSOLUTION (2026-09-04), PAID ON THE RULE THE TWENTY-THIRD JUST WROTE DOWN. The +/// one `gunbc#10218 identity-equality re-home` row is deleted, and its consumption was READ FROM +/// THE BASE rather than waited on: main declares `physical_asset_identity_eq` in +/// `product.placement_supply` (dag/gunbc/product/placement_supply.dag) and +/// `product.printed_chassis.manufacturing_manifest` imports it from there by name, so the base +/// already binds that spelling to that target and the delta is not producible. That is exactly the +/// check the entry above says costs a required run whenever it is guessed instead. +/// +/// THE SIX ROWS THIS BRANCH ALSO DELETED ARE NOT RECORDED TWICE. An earlier head of this branch +/// removed the four `gunbc#10028` and two `gunbc#10206` rows and wrote its own dissolution entry +/// for them; main removed the same six independently and recorded it as the TWENTY-THIRD. One +/// event, one record: my entry is dropped in favour of main's, because a second narration of the +/// same deletion is the double-record this ledger already refuses once above. +pub const NAMESPACE_TRANSITION_ADMISSIONS: &[TransitionAdmission] = &[ + TransitionAdmission { + label: "gunbc#10328 guarantee_stall split: the roster moves to its own module (every_live_stall_is_below_its_ceiling::`all_guarantee_stalls`)", + subject: AdmissionSubject::Binding { + module: "test.claim.guarantee_stall_witness_test", + in_declaration: "every_live_stall_is_below_its_ceiling", + spelling: "all_guarantee_stalls", + target: "gunbc.guarantee_stall.roster", + }, + disposition: NamespaceDeltaDisposition::TargetChanged, + }, + TransitionAdmission { + label: "gunbc#10328 guarantee_stall split: the roster moves to its own module (every_live_stall_names_a_next_rung_trigger::`all_guarantee_stalls`)", + subject: AdmissionSubject::Binding { + module: "test.claim.guarantee_stall_witness_test", + in_declaration: "every_live_stall_names_a_next_rung_trigger", + spelling: "all_guarantee_stalls", + target: "gunbc.guarantee_stall.roster", + }, + disposition: NamespaceDeltaDisposition::TargetChanged, + }, + TransitionAdmission { + label: "gunbc#10328 guarantee_stall split: the roster moves to its own module (every_restored_stall_is_still_rostered::`all_guarantee_stalls`)", + subject: AdmissionSubject::Binding { + module: "test.claim.guarantee_stall_witness_test", + in_declaration: "every_restored_stall_is_still_rostered", + spelling: "all_guarantee_stalls", + target: "gunbc.guarantee_stall.roster", + }, + disposition: NamespaceDeltaDisposition::TargetChanged, + }, + TransitionAdmission { + label: "gunbc#10328 guarantee_stall split: the roster moves to its own module (every_restored_stall_is_still_rostered::`every_restored_stall_is_rostered_once`)", + subject: AdmissionSubject::Binding { + module: "test.claim.guarantee_stall_witness_test", + in_declaration: "every_restored_stall_is_still_rostered", + spelling: "every_restored_stall_is_rostered_once", + target: "gunbc.guarantee_stall.roster", + }, + disposition: NamespaceDeltaDisposition::TargetChanged, + }, + TransitionAdmission { + label: "gunbc#10328 guarantee_stall split: the roster moves to its own module (every_restored_stall_is_still_rostered::`restored_stalls`)", + subject: AdmissionSubject::Binding { + module: "test.claim.guarantee_stall_witness_test", + in_declaration: "every_restored_stall_is_still_rostered", + spelling: "restored_stalls", + target: "gunbc.guarantee_stall.roster", + }, + disposition: NamespaceDeltaDisposition::TargetChanged, }, - disposition: NamespaceDeltaDisposition::TargetChanged, -}]; + TransitionAdmission { + label: "gunbc#10328 guarantee_stall split: the roster moves to its own module (the_stall_roster_is_not_empty::`all_guarantee_stalls`)", + subject: AdmissionSubject::Binding { + module: "test.claim.guarantee_stall_witness_test", + in_declaration: "the_stall_roster_is_not_empty", + spelling: "all_guarantee_stalls", + target: "gunbc.guarantee_stall.roster", + }, + disposition: NamespaceDeltaDisposition::TargetChanged, + }, + TransitionAdmission { + label: "gunbc#10328 guarantee_stall split: the row moves to its own module (live_stall_is_below_its_ceiling::`next_rung_trigger_enforcement_stall`)", + subject: AdmissionSubject::Binding { + module: "test.claim.guarantee_stall_witness_test", + in_declaration: "live_stall_is_below_its_ceiling", + spelling: "next_rung_trigger_enforcement_stall", + target: "gunbc.guarantee_stall.next_rung_trigger_enforcement_stall", + }, + disposition: NamespaceDeltaDisposition::TargetChanged, + }, + TransitionAdmission { + label: "gunbc#10328 guarantee_stall split: the row moves to its own module (stall_permanence_follows_the_blocker::`next_rung_trigger_enforcement_stall`)", + subject: AdmissionSubject::Binding { + module: "test.claim.guarantee_stall_witness_test", + in_declaration: "stall_permanence_follows_the_blocker", + spelling: "next_rung_trigger_enforcement_stall", + target: "gunbc.guarantee_stall.next_rung_trigger_enforcement_stall", + }, + disposition: NamespaceDeltaDisposition::TargetChanged, + }, + TransitionAdmission { + label: "gunbc#10328 guarantee_stall split: the row moves to its own module (stall_report_names_subject_and_trigger::`next_rung_trigger_enforcement_stall`)", + subject: AdmissionSubject::Binding { + module: "test.claim.guarantee_stall_witness_test", + in_declaration: "stall_report_names_subject_and_trigger", + spelling: "next_rung_trigger_enforcement_stall", + target: "gunbc.guarantee_stall.next_rung_trigger_enforcement_stall", + }, + disposition: NamespaceDeltaDisposition::TargetChanged, + }, + TransitionAdmission { + label: "gunbc#10328 guarantee_stall split: the row moves to its own module (uncounted_population_does_not_render_as_empty::`next_rung_trigger_enforcement_stall`)", + subject: AdmissionSubject::Binding { + module: "test.claim.guarantee_stall_witness_test", + in_declaration: "uncounted_population_does_not_render_as_empty", + spelling: "next_rung_trigger_enforcement_stall", + target: "gunbc.guarantee_stall.next_rung_trigger_enforcement_stall", + }, + disposition: NamespaceDeltaDisposition::TargetChanged, + }, +]; /// The denominators a green must name (DESIGN ยง5): a run that cannot say what it covered is an /// instrument failure wearing coverage's clothes. diff --git a/src/v2/std/nat.dag b/src/v2/std/nat.dag index 774b39f2c6b..5dd8c53b218 100644 --- a/src/v2/std/nat.dag +++ b/src/v2/std/nat.dag @@ -125,7 +125,7 @@ fn nat_lte(a: Nat, b: Nat) -> Bool { // v2.lens.cost.valuation does exactly that. // // That two Nat authorities exist at all is the real defect, and it is tracked as a guarantee stall -// rather than narrated here: gunbc.guarantee_stall two_nat_authorities_stall carries the rung, +// rather than narrated here: gunbc.guarantee_stall.two_nat_authorities_stall carries the rung, // ceiling and next-rung trigger. This annotation records only why the fork is not closable from a // max function. fn nat_max(a: Nat, b: Nat) -> Nat { diff --git a/src/v2/workflow/floor_expected_red.dag b/src/v2/workflow/floor_expected_red.dag index be85c42817a..8e2d964c0c9 100644 --- a/src/v2/workflow/floor_expected_red.dag +++ b/src/v2/workflow/floor_expected_red.dag @@ -1027,7 +1027,7 @@ fn floor_expected_red_chunk_interpreter_first_optional_divergence() -> List