Incompleteness: refinement on a reference's pointee (`&{ v | φ }` / `&mut { v | φ }`) in parameter position is not assumed by the callee

[coord-e]

Summary

When a function parameter is given a refinement type whose refinement sits on the pointee of a reference — e.g. &{ v: i64 | v >= 0 } or &mut { v: i64 | v >= 0 } — the refinement is silently dropped: the function body does not get to assume it. As a result, valid programs that rely on such a precondition are wrongly rejected with Unsat.

This is a documented feature. The README states:

Refinements may be nested inside generic arguments and reference types, e.g. Box<{ v: i64 | v > 0 }> or &mut { v: i32 | v >= 0 }.

Value-typed refined parameters (x: { v | φ }) work correctly, and the equivalent precondition written with requires/deref (#[requires(*x >= 0)]) works correctly — only the refinement-on-pointee syntax is affected. It reproduces for both & and &mut, and for both the param and sig annotation forms.

Reproduction

Rejected (but should verify):

// `x` is a shared reference whose referent is known to be >= 0,
// so returning `*x` should satisfy the `>= 0` return refinement.
#[thrust_macros::param(x: &{ v: i64 | v >= 0 })]
#[thrust_macros::ret({ r: i64 | r >= 0 })]
fn get(x: &i64) -> i64 { *x }
fn main() {}

$ cargo run -- -Adead_code -C debug-assertions=false repro.rs
error: verification error: Unsat

Equivalent precondition via requires (verifies fine):

#[thrust_macros::requires(*x >= 0)]
#[thrust_macros::ret({ r: i64 | r >= 0 })]
fn get(x: &i64) -> i64 { *x }
fn main() {}

The two functions express the same contract, but only the second verifies.

The same drop happens with &mut and with sig:

// both rejected with Unsat
#[thrust_macros::param(x: &mut { v: i64 | v >= 0 })]
#[thrust_macros::ret({ r: i64 | r >= 0 })]
fn f(x: &mut i64) -> i64 { *x }

#[thrust_macros::sig(fn(x: &mut { v: i64 | v >= 0 }) -> { r: i64 | r >= 0 })]
fn g(x: &mut i64) -> i64 { *x }

For contrast, the value-refinement analogue verifies as expected:

// verifies — value-typed refined param is assumed correctly
#[thrust_macros::param(x: { v: i64 | v >= 0 })]
#[thrust_macros::ret({ r: i64 | r >= 0 })]
fn h(x: i64) -> i64 { x }

Expected vs. actual

• Expected: the callee assumes *x >= 0, so *x satisfies the >= 0 return refinement and the program verifies (as it does through requires(*x >= 0)).
• Actual: the pointee refinement never becomes an assumption; the body is rejected with Unsat.

Evidence (generated SMT)

Dumping CHCs with THRUST_OUTPUT_DIR shows the difference precisely.

For the working requires(*x >= 0) version, the precondition is threaded in as a hypothesis:

; c0
(assert (forall ((v0 A0_Mut<Int>) (v1 A0_Mut<Int>))
  (=> (and (>= (mut_current<Int> v1) 0)) (p3 v1 v1))))

For the broken &mut { v | v >= 0 } version, the parameter's predicate p2 is left unconstrained (p2 v1 v1, i.e. true), the >= 0 fact is absent from the body-obligation clause, and it instead leaks out as a standalone, unsatisfiable obligation ∀ v1. v1 >= 0:

; c1
(assert (forall ((v0 A0_Mut<Int>) (v1 Int)) (=> (and (not (>= v1 0))) false)))
; c2
(assert (forall ((v0 A0_Mut<Int>) (v1 A0_Mut<Int>)) (=> (and true) (p2 v1 v1))))

So the pointee refinement is emitted as a check on an unconstrained value rather than being installed into the parameter's assumed type. c1 (∀ v1. v1 >= 0) is unsatisfiable, hence the spurious Unsat.

Notes on the mechanism

The macro side lowers &mut { v | φ } into a #[thrust::refinement_path($i, 0)] marker at pointee position TypeArg(0) (see thrust-macros/src/rty.rs, the & [lifetime] [mut] T branch of parse_refined_type_annotations), and the plugin's RefinedType::install_refinement_at (src/rty.rs) does place it on p.elem. The refinement does reach the parameter's refined type, but it is not turned into a body hypothesis the way value-param refinements and requires preconditions are — it surfaces as the spurious obligation above instead. The fix likely lives in how a refined reference-parameter type is turned into environment assumptions (around bind_mut / bind_own / bind_var in src/refine/env.rs and the function-template assembly in src/refine/template.rs).

This appears to be incompleteness (the checker stays sound — it rejects valid programs rather than accepting invalid ones), but it makes the documented refined-reference-parameter feature unusable.

Environment

• Commit: 6adb56d (Make seq concatenation operate on sequence tuples (Make seq concatenation operate on sequence tuples #162))
• Z3 4.16.0, default solver args