Allocate a precondition pvar only for blocks that need one

[coord-e]

• A basic block needs a precondition of its own only if it is START_BLOCK or is reached by more than one CFG edge — multiple predecessors, or multiple edges from a single predecessor (e.g. SwitchInt arms that share a target). Every other block has a unique incoming edge, so its precondition is exactly the predecessor's outgoing env state and needs no fresh predicate variable. (This is also the set of CFG cutpoints, so it still cuts every cycle — a loop header always has in-degree ≥ 2.) The predicate is needs_own_precondition(bb).
• refine_basic_blocks builds every block's layout eagerly. Blocks that need their own precondition get a pvar via for_template().build_basic_block(..) and are registered with register_basic_block_ty_with_precondition (has_precondition = true). The rest are built with a top precondition (no pvar — TypeBuilder::build_basic_block, guarded by a FakeRegistry that panics on any template/pvar registration) and registered with register_basic_block_ty_without_precondition (has_precondition = false).
• At each type_goto(target): if the target needs its own precondition, behavior is unchanged (subtyping clauses against the target's pvar). Otherwise install_inherited_bb_ty derives the target's precondition from the current env state — PrecondCapture (the focused successor of the removed UnbindAtoms) records param == env-value equations and folds in the env's refined vars + assumptions — and calls register_basic_block_precondition, which fills the last param's refinement (set_precondition, remapping Free(last_param) → Value) and flips has_precondition = true. No subtyping clause is emitted on the edge.
• analyze_basic_blocks iterates in reverse postorder so each inheriting block is analyzed after the predecessor that materialized its precondition. Cleanup/unwind blocks are skipped (data.is_cleanup). basic_block_ty_with_precondition asserts the precondition was actually materialized, and register_basic_block_precondition asserts it happens exactly once.

Net result: fewer predicate variables in the CHC system on every function with straight-line block sequences, with no change to what is verified.

https://claude.ai/code/session_01WB28auaD8dSQrckqBwJWBt

---

Generated by Claude Code

[Copilot]

Pull request overview

This PR reduces the number of predicate variables introduced into the CHC system by only allocating a fresh basic-block precondition pvar for CFG cutpoints (START block, join points, and multi-edge targets). Blocks with a unique incoming edge instead inherit their precondition from the predecessor’s outgoing environment state, materialized lazily at goto time.

Changes:

• Add needs_own_precondition to identify blocks that must own a precondition pvar (CFG cutpoints).
• Build/register BB types in two modes: with a precondition pvar vs. pvar-free “top” precondition, and lazily install inherited preconditions via PrecondCapture.
• Update analysis to require materialized preconditions (and iterate in reverse postorder) before analyzing each block.

Reviewed changes

Copilot reviewed 6 out of 6 changed files in this pull request and generated no comments.

Show a summary per file

File	Description
src/refine/template.rs	Adds a pvar-free TypeBuilder::build_basic_block path and refactors BB building to optionally accept an explicit precondition refinement.
src/refine/env.rs	Exposes refined vars and assumptions (vars(), assumptions()) needed to capture env state into inherited preconditions.
src/refine/basic_block.rs	Adds BasicBlockType::set_precondition to overwrite the last param refinement when materializing inherited preconditions.
src/analyze/local_def.rs	Registers BB types with/without preconditions and analyzes blocks in reverse postorder while requiring a materialized precondition.
src/analyze/basic_block.rs	Implements needs_own_precondition, PrecondCapture, and lazy precondition installation on goto edges for inheriting blocks.
src/analyze.rs	Tracks whether a BB has a materialized precondition (BasicBlockDef) and supports one-time lazy precondition registration.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[coord-e]

it is left as TODO to remove bb0 pvar