Skip to content
Merged
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
9 changes: 6 additions & 3 deletions dag/gunbc/kernel_grounding_interpreter_seed_growth.dag
Original file line number Diff line number Diff line change
Expand Up @@ -15,9 +15,12 @@ data kernel_grounding_interpreter_seed_growth_justification: SeedGrowthJustifica
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_record_lit", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "NativeVariantReading", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "native_variant_reading", field: WholeDeclaration },
DeclarationRef { module_path: "v1_compiler.v1_interpreter", decl_name: "InterpContext", 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. 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.",
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. THE BOOL ARMS (gunbc#12567, landed through #12559; same lane, same trigger): native_variant_reading and its NativeVariantReading result read a True/False arm against a host bool from the identity inference carried (v1.compiler.coercion rust_variant_value_realization, the one decision the Rust emitter also consumes -- no second table), so a natively realized Bool arm matches or constructs the host value and an undecidable one refuses instead of matching by spelling; InterpContext carries the variant_realization_refusal side-channel that turns that refusal, raised inside the Optional-returning match_pattern, into InterpError VariantRealizationRefused at the match that owns it. eval_var (its VariantValueBinding arm), match_pattern and InterpError carry the matching edits and are already cited by gunbc.scope_rank_view and gunbc.interpreter_eval_correctness_seed_growth.",
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",
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. The Bool arms dissolve on the same trigger: a self-emitted interpreter reads the identity-stamped tree and needs no side-channel, and a match_pattern that returns a typed refusal retires variant_realization_refusal together with the eval_match pre-check.",
current_boundary: "src/v1/stage0/src/v1_interpreter.rs eval_expr_inner, eval_match, eval_record_lit, match_pattern, eval_var, NativeVariantReading, native_variant_reading, InterpContext variant_realization_refusal; src/v1/04_infer.dag ground_kernel_views; dag/gunbc/kernel_grounding_interpreter_seed_growth.dag",
}