Incompleteness: dropping a recursively-defined ADT does not resolve `&mut` prophecies stored in its recursive-position field, so safe programs are wrongly rejected

[coord-e]

Summary

When a value of a recursively-defined enum (e.g. a cons-list) is dropped, dropping_formula_for_term in src/refine/env.rs skips the recursive-variant field entirely (the Box<Self> tail). Any &mut reference packed into that recursive-position field therefore never has its prophecy resolved (!r == *r) at drop time. The reference's final (prophecy) value is left as an unconstrained existential, so a function whose specification depends on that reference being unchanged cannot be verified — even when the function provably never mutates it.

This is the incompleteness direction (a safe program with a correct spec is rejected as Unsat), analogous in spirit to — but distinct from — #167, which fixed a panic when dropping an aggregate of &mut inside an enum. Here nothing panics: the drop silently emits WARN thrust::refine::env: skipping recursive variant and verification returns Unsat.

Reproduced on af7cd99 with z3 4.16.0.

Reproduction

The two functions below are identical except for which parameter the (correct) postcondition constrains. check never dereferences or writes through a or b; it only packs them into a list and immediately drops it, so both a and b are unchanged and both postconditions are true.

Rejected — postcondition on b (stored at recursive depth 1, inside the Box<List> tail)

use thrust_models::model::Mut;

enum List<'a> { Cons(&'a mut i32, Box<List<'a>>), Nil }
impl<'a> thrust_models::Model for List<'a> { type Ty = Self; }

#[thrust_macros::ensures(b == Mut::new(*b, *b))]   // b is unchanged — TRUE
fn check(a: &mut i32, b: &mut i32) {
    let _list = List::Cons(a, Box::new(List::Cons(b, Box::new(List::Nil))));
}

fn main() {}

$ cargo run -- -Adead_code -C debug-assertions=false rec_drop_b.rs && echo safe
 WARN thrust::refine::env: skipping recursive variant
error: verification error: Unsat

Accepted — same function, postcondition on a (stored at depth 0, the non-recursive field)

use thrust_models::model::Mut;

enum List<'a> { Cons(&'a mut i32, Box<List<'a>>), Nil }
impl<'a> thrust_models::Model for List<'a> { type Ty = Self; }

#[thrust_macros::ensures(a == Mut::new(*a, *a))]   // a is unchanged — TRUE
fn check(a: &mut i32, b: &mut i32) {
    let _list = List::Cons(a, Box::new(List::Cons(b, Box::new(List::Nil))));
}

fn main() {}

$ cargo run -- -Adead_code -C debug-assertions=false rec_drop_a.rs && echo safe
safe

The only difference is depth-0 (a) vs. recursive-position (b); a non-recursive enum with the same shape (enum Holder<'a> { H(&'a mut i32) }) verifies the postcondition fine, so this is specific to the recursive field being skipped, not to enums-of-&mut in general.

Expected vs. actual

• Expected: both programs verify (safe) — check leaves both referents untouched.
• Actual: the b variant is rejected (Unsat) because !b is never tied to *b.

Root cause

src/refine/env.rs, dropping_formula_for_term (around L1144–L1155): when a field of the enum is a pointer to the same enum, the whole field is skipped instead of having its contents' prophecies resolved:

if let Some(p) = field_type.as_pointer() {
    if matches!(&p.elem.ty, rty::Type::Enum(e) if e.symbol == ety.symbol) {
        // TODO: we need recursively defined drop_pred for the recursive ADTs!
        tracing::warn!("skipping recursive variant");
        continue;
    }
}

Because the recursive tail is skipped, every prophecy owned by a &mut reachable only through that tail is never resolved (!r == *r is not emitted), leaving !r an unconstrained existential. The drop of the depth-0 field is still resolved, which is why a verifies and b does not.

Note this only removes a drop assumption, so it is the safe (incompleteness) direction — valid programs are rejected, not unsafe programs accepted.

Suggested direction

As the in-code TODO notes, the drop assumption for recursive ADTs needs a recursively-defined drop predicate (a define-fun-rec that walks the recursive structure and conjoins !r == *r for each &mut field at every depth), rather than terminating the walk at the first recursive pointer. That would let the prophecies of references stored anywhere in the structure be resolved on drop.