Generate predicate variables only where something is left to infer

[coord-e]

Three of the predicate variables we generate stood for facts the constraints already state elsewhere, leaving a solver to infer what is written down. Each commit removes one.

ca7d6c0 Take the type of a call from the callee

A call bound its result to a template and related the return type of the callee to it by subtyping. The callee already says everything known about its result, so its return type is instantiated at the arguments and bound directly.

Adapting the arguments to the parameter list of the callee now works on PlaceTypes, which lets a rust-call tuple be untupled by projection instead of by rewriting refinements, and keeps the arguments as terms so no variable stands between a call and its result.

9429b01 Take the precondition of the entry block from the signature

The entry block took a template that assert_entry then bounded from below by the precondition of the function. It is installed directly instead, equating each parameter with the value it has on entry. The parameter types come from the signature too, so that refinements written there — one nested in a type (Vec<{ v: i32 | v > 0 }>), or the contract of a function-typed parameter — still reach the block once assert_entry is gone.

2e4e840 Take the state at a join as the disjunction of the states behind it

A block reached by more than one edge took a template inferred from a clause per incoming edge. The states its predecessors leave say exactly what it is entered in, so their disjunction is its precondition, and only a loop header still has one to infer: the state carried by its back edge is not yet known when it is analyzed.

A disjunction is no conjunct of a Horn clause body, so this holds only as long as no predicate variable appears in the states. Where one does, the disjunction is named by a predicate variable of its own, bounded from below by each state — which is what the block had all along.

Effect

Over tests/ui/pass (160 files):

	predicate variables	constraints
main	1691	—
after the first two commits	734	917 KiB
after the third	676	832 KiB

The path explosion the third commit invites did not show up: the constraints came out 9% smaller, since naming a state costs an argument list at every use, which the disjunction rarely exceeds. The worst case was loop_invariant_multi.rs at 1.23x (2.4 KiB to 2.9 KiB) and the best result_mut.rs at 0.35x (59 KiB to 21 KiB).

What is left generates a predicate variable only where something is genuinely unknown: the type of a function without an annotation, and a loop header without an invariant!. A fully annotated program with no loop now generates constraints with none at all — an annotated fn abs(x: i64) -> i64 { if x >= 0 { x } else { -x } } comes out as a plain SMT problem and verifies.

Notes for review

• ca7d6c0 fails tests/ui/pass/mut_recursive.rs. The predicate variable it removes also served as a cut point, and z3 needs far longer than its timeout on that test until the entry block gives up its own in 9429b01. Every other commit is green, and so is the head of the branch (316 passing). Worth knowing before bisecting.
• The single hardest hunk is adapt_args_to_abi in ca7d6c0: the rust-call expansion both moved out of relate_fn_param_sub_types_with_builder and was rewritten, so git shows it as a delete plus an add.
• Two steps carry the soundness of 9429b01 and are worth a second pair of eyes: the equation between each parameter and its OuterFnParam copy (the least solution of the removed predicate variable), and install_signature_types, without which a nested refinement or a function-typed parameter's contract would be lost — silently, and unsoundly for the latter.
• Nothing pins the counts above. The generated constraints changing shape is invisible to the ui tests: while writing this I had Refinement::disjunction demand a predicate-variable-free form even for a single state, which quietly put a predicate variable back on every block that inherits, and all 316 tests still passed. A unit test over Refinement::disjunction would cover the case that broke; happy to add one.

---

Generated by Claude Code