Implicit derefs (rustc adjustments) are dropped in annotation translation, so any v.len()/v.length/s.0 on a &mut parameter builds an ill-sorted term and ICEs — only the explicit (*v) spelling works #239

Summary

The annotation-to-formula translator (analyze::annot_fn::AnnotFnTranslator::to_formula_or_term,
src/analyze/annot_fn.rs:629) walks the type-checked HIR of a #[thrust::formula_fn] companion
expression by expression, and never consults TypeckResults::expr_adjustments. Rustc does not
represent an auto-deref as a HIR node — it records it as an Adjust::Deref adjustment on the
base/receiver expression. So every implicit dereference written in an annotation is silently
dropped when the term is built.

For a shared reference this is invisible: <&T as Model>::Ty = &T::Ty becomes Sort::Box, and
chc::unbox (src/chc/unbox.rs:74-87, applied in System::solve, src/chc.rs:2045) erases
Sort::Box entirely before the system is encoded — so a missing Box deref never changes the
resulting SMT.

For a mutable reference it is fatal: <&mut T as Model>::Ty = Mut<T::Ty> becomes
Sort::Mut(_), which unbox_sort deliberately keeps (it is a genuine (current, prophecy) pair).
Projecting/indexing/len-ing through it without the MutCurrent step produces an ill-sorted term,
and Thrust aborts with an ICE while computing sorts for the SMT-LIB2 encoding.

The net effect is that the most ordinary way to specify a mutating function —

#[thrust_macros::requires(v.len() > 0)]
fn pop_one(v: &mut Vec<i64>) { .. }

— cannot be written at all. Every annotation on a &mut parameter must spell out (*v) by hand,
including in places where Rust itself inserts the deref for you.

This is not a missing feature: the same annotation text is accepted and correctly translated when
the parameter is &Vec<i64> or Vec<i64>. Only the &mut spelling ICEs.

Reproduction

All five files below are rejected with an ICE. Command as in the README
(--edition 2021 makes no difference):

$ cargo run --quiet -- -Adead_code -C debug-assertions=false <file>.rs

1. Method call on a &mut receiver (requires)

mut_len.rs:

#[thrust_macros::requires(v.len() == 2)]
#[thrust_macros::ensures(true)]
fn f(v: &mut Vec<i64>) {
    assert!(v.len() == 2);
}

fn main() {
    let mut v: Vec<i64> = Vec::new();
    v.push(1);
    v.push(2);
    f(&mut v);
}

thread 'rustc' panicked at src/chc.rs:213:18:
invalid tuple_elem
   2: thrust::chc::Sort::tuple_elem            at ./src/chc.rs:213:18
   3: thrust::chc::Term<V>::sort               at ./src/chc.rs:670:55
   4: thrust::chc::Clause::term_sort           at ./src/chc.rs:1923:14
   5: thrust::chc::format_context::term_sorts  at ./src/chc/format_context.rs:29:25
   6: thrust::chc::format_context::atom_sorts  at ./src/chc/format_context.rs:73:9
   7: thrust::chc::format_context::collect_sorts
   8: thrust::chc::format_context::FormatContext::from_system
   9: thrust::chc::smtlib2::System::new        at ./src/chc/smtlib2.rs:704:19

v is bound to a term of sort Mut (Tuple (Array Int Int) Int). Seq::len is translated at
src/analyze/annot_fn.rs:826-830 as to_term(receiver).tuple_proj(1), i.e. tuple_elem applied
directly to the Mut sort.

2. Same, in ensures

ensures_len.rs — identical ICE, so the defect is not specific to the precondition path:

#[thrust_macros::requires(true)]
#[thrust_macros::ensures(v.len() == 2)]
fn f(v: &mut Vec<i64>) {}

fn main() {}

3. Named field access through a &mut (v.length)

mut_field.rs:

#[thrust_macros::requires(v.length == 2)]
#[thrust_macros::ensures(true)]
fn f(v: &mut Vec<i64>) {
    assert!(v.len() == 2);
}

fn main() {
    let mut v: Vec<i64> = Vec::new();
    v.push(1);
    v.push(2);
    f(&mut v);
}

thread 'rustc' panicked at src/analyze/annot_fn.rs:789:30:
unknown named field in formula

Here the failure is one step earlier: ExprKind::Field (src/analyze/annot_fn.rs:775-793) resolves
the field name against self.expr_ty(expr).ty_adt_def(), which is the unadjusted type
model::Mut<Seq<Int>>. Mut is pub struct Mut<T: ?Sized>(PhantomData<T>), so it has no field
named length and the lookup .expect("unknown named field in formula") fires. (v.array[i]
inside a requires fails the same way.)

4. Numeric field on a user struct behind &mut

mut_tuple_field.rs — invalid tuple_elem, showing this is not Vec/Seq-specific:

struct S { a: i64, b: i64 }
impl thrust_models::Model for S {
    type Ty = (thrust_models::model::Int, thrust_models::model::Int);
}

#[thrust_macros::requires(s.0 == 1)]
#[thrust_macros::ensures(true)]
fn f(s: &mut S) {
    assert!(s.a == 1);
}

fn main() {
    let mut s = S { a: 1, b: 2 };
    f(&mut s);
}

&mut [T] behaves identically (#[requires(s.len() == 2)] fn f(s: &mut [i64]) → invalid tuple_elem).

5. invariant! — the realistic case

mut_invariant.rs. This is the shape any in-place loop over a &mut container takes, and it ICEs
before verification even starts:

fn zero_all(v: &mut Vec<i64>) {
    let mut i = 0_usize;
    while i < v.len() {
        thrust_macros::invariant!(|i: usize, v: &mut Vec<i64>| i <= v.len());
        v[i] = 0;
        i += 1;
    }
}

fn main() {
    let mut v: Vec<i64> = Vec::new();
    v.push(1);
    zero_all(&mut v);
    assert!(v.len() == 1);
}

thread 'rustc' panicked at src/chc.rs:213:18:
invalid tuple_elem

#[thrust_macros::param(v: { w: &mut Vec<i64> | w.len() == 2 })] reaches the same ICE, so
requires, ensures, param and invariant! are all affected — every surface that lowers to a
formula_fn.

Controls

The defect is specific to the reference mutability of the annotated parameter, not to the
annotation text. Keeping requires(v.len() == 2) byte-for-byte identical and changing only the
parameter type:

fn f(v: &Vec<i64>)      // accepted, translated correctly
fn f(v: Vec<i64>)       // accepted, translated correctly
fn f(v: &mut Vec<i64>)  // ICE

And writing the deref that rustc would have inserted makes the &mut version work:

#[thrust_macros::requires((*v).len() == 2)]   // accepted
#[thrust_macros::requires((*v).length == 2)]  // accepted
fn f(v: &mut Vec<i64>) { assert!(v.len() == 2); }

The &-version is genuinely translated, not vacuously accepted — calling it with a 1-element vector
is correctly rejected:

$ # fn f(v: &Vec<i64>) with requires(v.len() == 2), called as f(&v) where v.len() == 1
error: verification error: Unsat

as is the explicit-deref &mut version.

Root cause

AnnotFnTranslator::to_formula_or_term (src/analyze/annot_fn.rs:629) matches on ExprKind alone.
grep -rn 'expr_adjustments\|Adjustment\|adjusted' src/ returns nothing: adjustments are never read
anywhere in the analyzer.

The three affected arms all take to_term(base) unchanged:

ExprKind::Field(expr, field) => {           // src/analyze/annot_fn.rs:775
    let index = /* looked up on self.expr_ty(expr) — the UNADJUSTED type */;
    let term = self.to_term(expr);
    FormulaOrTerm::Term(term.tuple_proj(index))
}
ExprKind::Index(array, index, _) => {       // src/analyze/annot_fn.rs:795
    let array_ty = self.expr_ty(array);     // unadjusted
    let array_term = self.to_term(array);
    ...
}
ExprKind::MethodCall(method, receiver, args, _) => {   // src/analyze/annot_fn.rs:809
    if Some(def_id) == self.def_ids.seq_len() {
        let t = self.to_term(receiver);     // no MutCurrent
        return FormulaOrTerm::Term(t.tuple_proj(1));
    }
    ...
}

model::Mut<T> declares impl<T> std::ops::Deref for Mut<T> { type Target = T; } (std.rs:84),
which is exactly what makes v.len() / v.length / s.0 type-check inside a formula — rustc
resolves them through one auto-deref step. That step is the "current value" projection the analyzer
spells Term::MutCurrent, and it is precisely what gets lost.

Only ExprKind::Unary(UnOp::Deref) (src/analyze/annot_fn.rs:697-719) ever emits mut_current() /
box_current(), which is why the explicit (*v) spelling is the only one that works.

Why the bug is invisible for &T and Box<T>: unbox_sort (src/chc/unbox.rs:74) collapses
Sort::Box(inner) => unbox_sort(*inner) but keeps Sort::Mut(inner) => Sort::Mut(..), and
unbox_term likewise erases Term::Box/Term::BoxCurrent while preserving Term::Mut/
Term::MutCurrent/Term::MutFinal. A dropped Box deref is therefore a no-op after unboxing; a
dropped Mut deref leaves a tuple_elem/deref/select standing on a Sort::Mut, which
Sort::tuple_elem (src/chc.rs:213) and Sort::deref (src/chc.rs:206) reject.

Why it matters

Specifying a function that mutates through &mut is the primary use of requires/ensures in
Thrust, and &mut Vec<T> / &mut [T] / &mut MyStruct parameters are the norm in real programs.
Today every such annotation has to be written in a dialect that deviates from Rust — (*v).length
instead of v.len() — with no diagnostic pointing that out: the user gets an ICE with no span, and
nothing in the message mentions the annotation, the parameter, or the missing deref. The same
expression working for &Vec<i64> and failing for &mut Vec<i64> makes it look like &mut
parameters are unsupported rather than that one token is missing.

The invariant! case (repro 5) is the sharpest: writing an invariant over a &mut container — the
only way to verify an in-place loop — has no non-ICE-ing natural spelling.

Expected behavior

The HIR→formula translation should apply the adjustments rustc recorded for an expression before
using its term. Concretely, to_term/to_formula_or_term should consult
self.typeck.expr_adjustments(expr) and, for each Adjust::Deref, wrap the term in
Term::MutCurrent or Term::BoxCurrent according to the adjusted-from type (mirroring the
ExprKind::Unary(UnOp::Deref) arm), and use the adjusted type wherever the current code calls
self.expr_ty(base) to classify the base (field-name lookup at :781-789, the is_seq test at
:799-801). Adjust::Borrow needs no term change, matching how AddrOf-free autorefs behave today.

Failing that, an unhandled adjustment should at minimum produce a diagnostic on the annotation's
span rather than an ICE deep in the SMT encoder.

Relation to existing issues

• Incompleteness: an explicit invariant! on a loop that writes through a &mut drops the reference's prophecy link, so the referent is havoc'd after the borrow ends — safe programs wrongly rejected (no workaround; the inference path handles it) #205 (invariant! on a loop writing through a &mut drops the prophecy link) is downstream of
  this one for repro 5: rewriting the invariant as (*v).length gets past the ICE, and the program
  is then rejected with Unsat by Incompleteness: an explicit invariant! on a loop that writes through a &mut drops the reference's prophecy link, so the referent is havoc'd after the borrow ends — safe programs wrongly rejected (no workaround; the inference path handles it) #205. They are independent — this issue is in the annotation
  translation, Incompleteness: an explicit invariant! on a loop that writes through a &mut drops the reference's prophecy link, so the referent is havoc'd after the borrow ends — safe programs wrongly rejected (no workaround; the inference path handles it) #205 in the loop-precondition machinery — but a user hitting repro 5 will meet both.
• Incompleteness: refinement on a reference's pointee (&{ v | φ } / &mut { v | φ }) in parameter position is not assumed by the callee #166 (a refinement on a reference's pointee, &mut { v | φ }, is not assumed by the callee)
  concerns where an already-built refinement is placed; here the refinement cannot be built at all.
• Boolean comparisons (<, <=, >, >=) emit ill-typed SMT (< Bool Bool), so any program comparing bools fails to verify #136 / Quantifier (forall/exists) binder sorts are never declared in SMT-LIB, so any spec quantifying over a datatype/tuple-sorted variable emits an undefined sort #142 / Ordering comparisons (<, >) on tuple/aggregate values emit ill-typed SMT (< Tuple Tuple) via the generic PartialOrd::lt/gt extern specs, so safe programs comparing tuples are falsely rejected #195 / Ill-typed SMT: a closure that mutates a captured variable, passed to a generic HOF spec'd with pre!/post!, has its pre/postcondition predicate declared at the FnMut receiver sort Mut<env> but applied at the bare env sort, so verification aborts with a solver sort mismatch #206 are the other "ill-typed SMT reaches the solver" reports. This one
  differs in that the ill-sorted term is caught earlier, inside FormatContext::from_system, and
  the trigger is an ordinary Rust auto-deref rather than an operator or quantifier.
• Panic in const_value_ty when analyzing integer constants larger than i64::MAX #116 / Stack overflow (non-termination) in dropping_formula_for_term when a recursive ADT's self-pointer is nested inside a tuple/struct field #178 are unrelated ICEs (const_value_ty, dropping_formula_for_term).

Environment

• thrust @ cd6b330
• rustc nightly-2025-09-08 (per rust-toolchain.toml)
• Z3 5.0.0 (irrelevant here — every repro aborts before the solver is invoked)