Keep the removed parameter's refinement in remove_param

[coord-e]

Fixes #197.

Root cause

A function type keeps its precondition on the last parameter (BasicBlockType::set_precondition, truncate_outer_fn_params), but remove_param dropped the refinement of the parameter it removed.

The entry basic block type orders its local parameters by Local index, so they run _0 (RETURN_PLACE), then the arguments, then any temporary that liveness reports as live at entry — which happens for ZST locals such as a non-capturing closure or a unit struct. drop_bb_zst_params removes every parameter whose local is not a function argument, so when the last local is such a temporary, the precondition went with it and assert_entry never emitted a clause with that predicate variable in a head. The predicate then occurred only in clause bodies, so the solver satisfied the system by reading it as the empty relation, and every obligation after that point was discharged vacuously — a program that always panics verified as safe.

Only the arg_count == 0 case survived, because drop_bb_zst_params re-introduces a synthetic unit parameter carrying the refinement of the last dropped parameter.

Before, for fn check(v: i32) { let f = |a: i32| a; f(v); assert!(1 == 2); }:

assert_entry before entry=(_0: (), _1: int, _2: (), { int | p4 ν $1 }) → ()
assert_entry after  entry=(int) → ()

p4 is gone, and the emitted CHC system contains no clause with p4 in a head.

Trigger

The trigger is broader than the issue describes: any function with at least one argument whose entry block has a live non-argument ZST local. Neither an argument at the call site nor a closure at all is required — fn check(v: i32) { let z = Z; take(&z); assert!(1 == 2); } for a unit struct Z verifies as safe too.

Change

remove_param now conjoins the removed parameter's refinement to the last remaining parameter, rebinding the reference to that parameter as the value variable. Removal no longer weakens the precondition, and callers do not have to know where a function type keeps it.

Testing

• tests/ui/{pass,fail}/closure_no_capture_fn_param.rs added. The fail one is rejected without this change and passes with it.
• The reproducers from the issue, the no-argument closure variant, a two-argument variant, the closure-free unit-struct variant, and the parameterless variants all report Unsat now; assert!(f(v) == v) still verifies as safe.
• cargo test, cargo fmt --check, cargo clippy -- -D warnings. The test run has 32 pre-existing failures in this environment because PCSat (tests/thrust-pcsat-wrapper) is unavailable; the failing set is identical with and without this change.

[Copilot]

Pull request overview

This PR fixes an unsoundness where removing a basic-block entry parameter could accidentally drop the function precondition refinement (stored on the last parameter), leaving the precondition predicate unconstrained and causing panicking programs to verify as safe.

Changes:

• Update FunctionType::remove_param to preserve the removed parameter’s refinement by conjoining it onto the last remaining parameter.
• Add UI regression tests that exercise non-capturing closure calls inside a #[thrust::callable] function with a parameter (both pass and fail variants).

Reviewed changes

Copilot reviewed 3 out of 3 changed files in this pull request and generated 2 comments.

File	Description
src/rty.rs	Preserves refinements when removing a parameter by merging the removed refinement into the last remaining parameter.
tests/ui/pass/closure_no_capture_fn_param.rs	Adds a passing regression test for non-capturing closure calls in a parameterized callable function.
tests/ui/fail/closure_no_capture_fn_param.rs	Adds a failing regression test to ensure false assertions remain rejected after such a closure call.

---

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