Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 1 addition & 3 deletions dag/gunbc/kernel_grounding_interpreter_seed_growth.dag
Original file line number Diff line number Diff line change
Expand Up @@ -14,11 +14,9 @@ import gunbc.seed_growth { SeedGrowthJustification }
data kernel_grounding_interpreter_seed_growth_justification: SeedGrowthJustification = SeedGrowthJustification {
hand_authored_declarations: [
DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "eval_expr_inner", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "eval_match", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "eval_record_lit", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "match_pattern", field: WholeDeclaration },
],
reason: "The subject is the seed interpreter's own evaluation of three tree forms, which no .dag program can reach: eval_record_lit and match_pattern LOSE their spelling-keyed Zero/Succ arms (a deletion); eval_expr_inner evaluates a Peano-unfolded elaborated literal as its constructor image instead of as the kernel literal, because a Peano unfolding's destination is structural on every route now that a kernel-realized carrier never reaches that arm; and eval_match refuses, located, a constructor pattern matched against a host integer, because with the grounding arms gone such a match could only fall through to a later wildcard silently. The fold that replaces the deleted arms is .dag (v1.compiler.infer ground_kernel_views), so the only hand Rust this adds is the refusal and the image evaluation.",
reason: "The subject is the seed interpreter's own evaluation of three tree forms, which no .dag program can reach: eval_record_lit and match_pattern LOSE their spelling-keyed Zero/Succ arms (a deletion); eval_expr_inner evaluates a Peano-unfolded elaborated literal as its constructor image instead of as the kernel literal, because a Peano unfolding's destination is structural on every route now that a kernel-realized carrier never reaches that arm; and eval_match refuses, located, a constructor pattern matched against a host integer, because with the grounding arms gone such a match could only fall through to a later wildcard silently. The fold that replaces the deleted arms is .dag (v1.compiler.infer ground_kernel_views), so the only hand Rust this adds is the refusal and the image evaluation. ALREADY JUSTIFIED BY THEIR OWN ROWS, and so not repeated here because the roster cites each declaration once: eval_match (gunbc.interpreter_eval_correctness_seed_growth match_arm_guard_seed_growth_justification) and match_pattern (gunbc.interpreter_eval_correctness_seed_growth value_depth_seed_growth_justification) -- each also carries this change's edit described above, and this row's trigger still governs that edit.",
owning_dissolution_lane: "v1-hand-queue-drain" as RoadmapNodeId,
trigger: "Delete the eval_match refusal and the eval_expr_inner image arm when match and literal evaluation are realized by the self-emitted interpreter, which reads the same folded tree and has no constructor-versus-integer case to refuse. Equivalently, when the seed interpreter's pattern matcher returns a typed refusal instead of an Optional, so an unfolded constructor pattern over an integer is refused where it is matched rather than by a pre-check in eval_match. Rewording the refusal or widening its exempt constructor list does not dissolve this row. The exemption (kernel_raw_payload_constructor) is keyed on the pattern's parent carrier spelling, Optional or Witness, because the seed's MatchPattern carries no DeclarationRef (review 73985); a DeclarationRef on the pattern is the next rung for that key.",
current_boundary: "src/v1/stage0/src/v1_interpreter.rs eval_expr_inner, eval_match, eval_record_lit, match_pattern; src/v1/04_infer.dag ground_kernel_views; dag/gunbc/kernel_grounding_interpreter_seed_growth.dag",
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -40,6 +40,7 @@ data witness_outside_gate_closure_falsified_by_other_file: RecurringFailureMode
"THE TRIGGER ABOVE NAMES LESS THAN THE CAPABILITY, AND THIS RECEIPT CORRECTS IT RATHER THAN LETTING THE NARROW TEXT STAND (DESIGN section 4b(3): a trigger naming less than the capability it restores is satisfied while the capability stays dead). Transitive-dependency-based changed-witness selection reaches a falsifier that is a .dag MODULE the witness imports. It cannot reach a falsifier that is the COMPILER: gunbc#11720 landed a wall in `v1.compiler.infer` whose census was scoped to `what the required gates compile`, and `test.claim.workflow_dispatch_input_witness_test` -- outside the gate closure, byte-identical since #11468 -- stopped RESOLVING while main's floor stayed green (run 35509509831: `claims=402 declined_gate_closure=20750`). A compiler change is a dependency of every witness and an import of none, so no selector over the import graph enumerates its victims. That face is rostered on [[witness_that_fails_to_compile_is_absent_rather_than_red]] (fourth specimen), whose trigger is the capability: PLAN THE ENROLLED POPULATION -- compile every claim-root file and refuse one that does not compile -- which is also the restoration trigger of `gunbc.rung_drop` `witness_floor_off_the_required_gate`. The discriminator is two-sided and stays so: a witness whose falsifier is import-reachable is covered by the selector named above once it lands and still reads as covered; a witness whose falsifier is the compiler, a data fixture or a required-field growth is not, and reads as the sibling row.",
"RECEIPT, 2026-09-26, AND IT IS THE CLASS AT POPULATION SCALE RATHER THAN ONE SPECIMEN. Twelve claims across six out-of-closure witness modules under test.claim.fabric, test.claim.runner, test.claim.fleet and test.claim.executor_privileged_operation_witness were red on main f17c19a8fb, found only because gunbc#12339 touched a path that enrolled them as changed witnesses. Six unrelated, correct changes to modules those witnesses IMPORT falsified them, none touching a witness file: #10568 (sudo elevation quoting), #11204 (retirement inhibition text), #11625 (a second fabric host), #11751 (microVM readback grants), #11762 (width derived-or-unresolved), #12011 (the srv1 microVM shakedown slot). The oldest had been silently red for about three weeks. In every case re-derivation found the CLAIM, not the fold, to be the earliest unjustified link -- transcribed counts, a one-member roster, an over-broad prohibition -- repaired in gunbc#12343, #12344, #12346, #12347 and #12348. This row's specimen witness_population_tracks_the_slot_roster reddened AGAIN, by a different term (#11751) than the one its earlier repair derived, which is the recurrence the next-rung trigger above exists to catch: transitive-dependency changed-witness selection would have run each of these on the PR that falsified it.",
"RECEIPT, 2026-10-01 (calm-hawk-793), A DELIBERATE CHANGE IN ONE STAGE REDDENING A CONTROL IN ANOTHER, AND THE CONTROL WAS AN ACCEPTING CONTROL, NOT A WALL. gunbc#12290 (std.kind, 2026-09-26) made a declared-inhabitant roster member's derived type its KIND, an Atom; v2.compiler.infer algebra_ref_is_grounded refused every Atom, so canonical_grounding_for_node refused every roster member before coercion and v2.test.manual.ingest_bridge ingest_identity_coercion_accepts_source_present_in_authored_roster went red (bisected on BuildBuddy, path-restricted: first bad 21f4d0c390). At that commit required_gate_prefixes held no v2.test. prefix, so the control was declined outside the gate closure and #12290 landed green; it stayed red about five days, found only by executing the #12860 population. Re-derivation found the earliest unjustified link in the GROUNDING PREDICATE, under-specified for the case #12290 introduced, not in the kind derivation: the predicate now admits an Atom only when std.kind kind_denoted_by_node recognises it as that authority's mint. Three more specimens in the same population had the same shape, a correct change elsewhere and an out-of-gate claim that never ran: #12625 (a metadata edge entered the roster index), #12566 (an undeclared formal became a counted advisory) and #12048 (imports became chain bindings).",
"RECEIPT, 2026-10-03 (silent-stag-886), AND ITS FIRST READING WAS THAT TWO ROUTES DISAGREED. On gunbc#13090 (feb95f8ed3 and 03b96ed790) `gunbc run --claim-run` over test.claim.seed_growth_admission_witness failed 3 of 7 claims while the required floor was green, and the report framed it as claim_batch and the floor giving different verdicts for one witness. They did not: the floor gave NO verdict. The module matches neither required_gate_prefixes nor required_gate_authored_modules, and the floor run on 03b96ed790 (37110271994) lists its one cost-debt identity as outside this run's universe, preparation never offered it. A green run that declined a claim is not a pass of it, and reading it as one is this class's harm at the reader. The claim route was right: all three reds reduce to seed_growth_roster_mechanical_checks_holds, whose duplicate-key conjunct was false on main ca79f2c660 because gunbc#12846 (Nat de-fork) listed v1_interpreter eval_match and match_pattern in kernel_grounding_interpreter_seed_growth_justification while gunbc#12903 already rostered them (match_arm_guard and value_depth rows), and the roster cites each declaration once. #12846 touched neither the witness nor seed_growth_admission.dag, only a module it imports, which is this row's shape exactly. The earliest unjustified link was the #12846 row, repaired by naming the two items as already justified, the convention the value_drop_binding_adaptation row states. The witness is its own discriminating control: red on ca79f2c660, green after. Gate admission of the module is the class's trigger applied to one module and is left to an operator ruling, because a gate row is a standing claim on every required run.",
],

evidence: [],
Expand Down