Repository navigation
Floor: repair four out-of-closure witnesses refused by the Optional-at-Required wall; roster the compiler-origin specimen - #11865
Merged
Conversation
…t-Required wall; roster the compiler-origin specimen dag/test/claim/workflow_dispatch_input_witness_test.dag stopped resolving when #11720 landed RefusedOptionalAtRequired: list index is declared T? (and the interpreter agrees), so the witness passing on[0] to a required WorkflowTrigger was the earliest unjustified boundary. Repaired with the guard-is-the-match idiom, plus three sibling sites the same grep census found (fabric_control_plane, altra_memory_controller, nbd_proxy_virtual_media_install). The floor never planned any of them: discovery enumerates the identities and dispositions each DeclinedOutsideGateClosure (run 35509509831: declined_gate_closure=20750), so the drop is located, not silent — but a disposition row cannot tell resolved-and-fine from never-resolved, and the capability that could is the witness_floor_off_the_required_gate restoration trigger. No second floor is built (operating-lane ruling). The class is appended to witness_that_fails_to_compile_is_absent_rather_than_red as its fourth specimen (falsifier = the compiler, carried by no import graph), and the sibling row's trigger is corrected by receipt. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
… specimen of (review 69192) Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Contributor
Author
|
Review 69192 addressed at 1ad31ea (the lane that authored this PR has closed under the wind-down, so I pushed the one-symbol fix): the annotation now cites |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Work item
adhoc-2fe20fe6-5e9(floor: a witness module that fails resolve vanishes from the planned population). Receipt from neat-ibex-471 on the #11667 lane; parent ruling from eager-owl-205 (2026-09-20): do not build a second floor.(1) The chain, and where it was unjustified
fleet_converge_workflow.on[0]is typedT?byv1.compiler.accesscheck_index_access_node(with_optional_cardinality(elem)), andeval_indexanswersNullpast the end — the typing is the runtime's, and indexing is a total operation exactly as DESIGN §5 wants.workflow_trigger_entrydeclares a requiredWorkflowTrigger. The witness asserted a cardinality the language never granted, so the witness is the earliest unjustified boundary; the indexing rule and #11720'sRefusedOptionalAtRequiredwall are both correct and untouched. The repair is the idiom #11720 established: the guard is the match.The same grep census (
xs[i],.first(),.last()at a direct-call argument, witness roots only) found three more out-of-closure modules refused by the same wall, repaired the same way:test.claim.fabric.fabric_control_plane_witness,test.claim.altra_memory_controller_witness,test.claim.nbd_proxy_virtual_media_install_witness. That census is a candidate list over one authored shape, not the population — the wall also judges list elements and undeclared list-literal members, and nothing has resolved the other declined modules.(2) Established: never planned, never resolved — and dispositioned, not silent
From the floor log of run 35509509831 (site-projection line):
declared=21557 sites=807 files=2316 claims=402 declined_long=0 declined_fixture=0 declined_outside_gate=405 declined_gate_closure=20750. The module matches norequired_gate_prefixesrow and was not diff-touched, so discovery enumerates its 18 identities (they are indeclared), preparation never admits its module, and each identity is dispositionedDeclinedOutsideGateClosureat identity grain inrequired_floor_disposition.tsv. A module inside the prepared closure that fails resolve refuses the whole floor (prepare_repository_closureresolvesResolveTypecheckGate::Strict). So resolve failure never removes a discovered witness from the denominator: it is an executed verdict or a located planning refusal — satisfied today by the disposition row.What the disposition row cannot say is whether a declined module resolves. Knowing that requires resolving it, and resolving the declined population is exactly the capability
gunbc.rung_dropwitness_floor_off_the_required_gateretired on 2026-09-20 (3197 modules, 14.3 min strict preparation). A floor refusal for an out-of-closure resolve failure IS that drop's restoration trigger, so this PR does not build one; it makes the row say so.The sharper class: the falsifying change was the compiler. #11720 landed a wall in
v1.compiler.inferwith its census scoped (stated honestly in its body) to "what the required gates compile". A compiler change is a dependency of every witness and an import of none —src/v1is outside the floor's source roots — so no changed-module seed, no arm-set consumer and no future import-transitive selector enumerates its victims.Rows
gunbc.recurring_failure_mode.witness_that_fails_to_compile_is_absent_rather_than_red— fourth specimen (compiler-origin non-compilation), the two-sided discriminator (import-reachable falsifier → covered by transitive selection; compiler / data fixture / required-field growth → this class), and the honest-state receipt.gunbc.recurring_failure_mode.witness_outside_gate_closure_falsified_by_other_file— its trigger named less than the capability; corrected by receipt, cross-referencing the sibling row.gunbc.rung_drop.witness_floor_off_the_required_gate— population gains the resolve-standing member; restoration trigger names the capability: plan the enrolled population.Deferred under the 2026-09-20 wind-down ruling (patch below, ready to lift)
Two pieces were authored and are NOT in this PR because their generated projections (
.github/workflows/witnesses.yml,docs/design-rung-drops.md) could not be regenerated on this host in time (thegunbc runformain_wet_onesat 104 wall-minutes in disk-sleep for 2 CPU-minutes of work):gunbc.compiler_gate_workflow: uploadrequired_floor_disposition.tsvfrom the fleet lane as artifactrequired-floor-disposition(reusingwitness_floor_tsv_upload_step), so the 20750 declined identities are a census by name — what adhoc-3bc1b8e0-982 / sleek-bat-381 need.gunbc.rung_drop.witness_floor_off_the_required_gate: population gains the resolve-standing member; restoration trigger names the capability plan the enrolled population.The row edit
gunbc.recurring_failure_mode.witness_outside_gate_closure_falsified_by_other_filein this PR cross-references that trigger by name, which is correct today (the drop's trigger already says "plans and executes the enrolled witness population").deferred_followup.patch
Evidence
Local
claim_batch(binary/cargo-target/release/claim_batch, sha256387ca007bd64ee2e3cd75be00cc4692dd4176eafcbc4d790ad2567671512182b, copied before use),--source-root dag --source-root src/v2, all 18 test fns of the primary module:4dd944e39ed(byte-identical file):claim_batch: resolve failed for dag/test/claim/workflow_dispatch_input_witness_test.dag: :151:73: error: value does not inhabit its declared type at the direct call argument for parameter 'trigger': declared 'Coproduct(WorkflowTrigger)', produced 'Optional<Coproduct(WorkflowTrigger)>'— exit 1, zero claims executed. This is neat-ibex-471's receipt reproduced.4dd944e39ed, the only difference being this PR's four witness edits): resolve succeeded;18 witness(es), 18 PASS, 0 FAIL, includingPASS workflow_dispatch_choice_input_projects_options_list.[resolve-summary] 1 resolve(s) in 1346407ms wall; 18 witness(es) in 333842ms wall(host load average ~270 during the run).v1_src_dag_parseclean on all four edited files; their repairs are the identical shape at the identical diagnostic class (.first()/[0]at a required direct-call parameter). Their claim_batch runs were queued behind the primary one and killed under the wind-down ruling before reaching a verdict — not executed, stated plainly; the floor does not plan them either (all three are outside the gate closure), so their executing evidence is a follow-up claim_batch run.Floor evidence that the module was never planned: run 35509509831,
[floor-phase] phase=site-projection state=completed ... declared=21557 sites=807 files=2316 claims=402 declined_long=0 declined_fixture=0 declined_outside_gate=405 declined_gate_closure=20750;required-floor: planned=402 executed=402 ... claims_failed=0.Not in this PR
test.claim.runner_throughput_qualification_witness(stale imports after microVM guest network: tap-grain default-deny egress, slot network readback, workspace staging gate #11675's rename) is repaired by Main repair: stale egress-grain import in the qualification witness; Optional first() in the build-cell decoder #11839 (eager-owl-205), which also foundgunbc.fabric_required_build_cellnot resolving under the same wall — recorded in the row as confirmation that the grep census is a candidate list, not the population.T?(jobs[0].idin the same witness) is not judged by the wall today; that is the residual Floor: refuse an Optional where a Required value is declared (#11626) #11720 already names.🤖 Generated with Claude Code