Incompleteness: a refinement declared on any parameter but the last (`#[param]`/`#[sig]`) is never assumed in the body, so no multi-argument function can be given a refinement-typed signature

[coord-e]

Summary

When a function's parameters are given refinement types directly (#[thrust_macros::param(..)] / #[thrust_macros::sig(..)]), only the last parameter's refinement is assumed while checking the body. The refinement declared on every earlier parameter is dropped outright — it never appears in the emitted CHC system at all — so the body is checked as if those parameters were unrefined and Thrust rejects (Unsat) functions that trivially satisfy their signature.

The equivalent formula annotations (#[requires]/#[ensures]) are unaffected, because requires attaches its whole formula to the last parameter.

This is an incompleteness, not a soundness hole: call sites still check every parameter refinement (see "Soundness is preserved").

The practical effect is that the refinement-type surface syntax the README documents is unusable for any function with more than one argument, unless the fact you need happens to be about the last one.

Reproduction

Same signature, four bodies. Only which parameter the body's correctness depends on changes.

// first.rs
#[thrust_macros::sig(fn(a: { v: i64 | v > 0 }, b: { v: i64 | v > 0 }) -> { r: i64 | r > 0 })]
fn first(a: i64, b: i64) -> i64 { let _ = b; a }
fn main() {}

// second.rs
#[thrust_macros::sig(fn(a: { v: i64 | v > 0 }, b: { v: i64 | v > 0 }) -> { r: i64 | r > 0 })]
fn second(a: i64, b: i64) -> i64 { let _ = a; b }
fn main() {}

// add_sig.rs
#[thrust_macros::sig(fn(a: { v: i64 | v > 0 }, b: { v: i64 | v > 0 }) -> { r: i64 | r > 0 })]
fn add(a: i64, b: i64) -> i64 { a + b }
fn main() {}

// add_requires.rs — the same contract written with requires/ensures
#[thrust_macros::requires(a > 0 && b > 0)]
#[thrust_macros::ensures(result > 0)]
fn add(a: i64, b: i64) -> i64 { a + b }
fn main() {}

$ cargo run -q -- -Adead_code -C debug-assertions=false first.rs && echo safe
error: verification error: Unsat
error: aborting due to 1 previous error

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

$ cargo run -q -- -Adead_code -C debug-assertions=false add_sig.rs && echo safe
error: verification error: Unsat
error: aborting due to 1 previous error

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

first returns a parameter that the signature declares to be > 0 and promises a result > 0. It is rejected. second, byte-identical except that it returns b instead of a, is accepted.

It is exactly "every parameter except the last"

annotation	body	verdict	correct
sig(fn(a:{v>0}) -> {r>0})	a	safe ✓	safe
sig(fn(a:{v>0}, b:{v>0}) -> {r>0})	a	Unsat ✗	safe
sig(fn(a:{v>0}, b:{v>0}) -> {r>0})	b	safe ✓	safe
sig(fn(a:{v>0}, b:{v>0}) -> {r>0})	a + b	Unsat ✗	safe
sig(fn(a:{v>0}, b:{v>0}, c:{v>0}) -> {r>0})	b	Unsat ✗	safe
sig(fn(a:{v>0}, b:{v>0}, c:{v>0}) -> {r>0})	c	safe ✓	safe
requires(a > 0 && b > 0) + ensures(result > 0)	a + b	safe ✓	safe

The same holds for the desugared spelling — separate #[thrust_macros::param(..)] attributes, with or without a #[thrust_macros::ret(..)]:

#[thrust_macros::param(a: { v: i64 | v > 0 })]
#[thrust_macros::param(b: { v: i64 | v > 0 })]
fn f(a: i64, b: i64) -> i64 { assert!(a > 0); a + b }   // Unsat

#[thrust_macros::param(a: { v: i64 | v > 0 })]
#[thrust_macros::param(b: { v: i64 | v > 0 })]
fn f(a: i64, b: i64) -> i64 { assert!(b > 0); a + b }   // safe

Why this has been easy to miss

Annotating only some parameters masks the bug. Any parameter left unannotated still receives an inference template (a predicate variable) in the declared function type, and — since call sites do check the annotated parameters — the solver is free to instantiate that predicate variable with the very facts that were dropped, silently restoring them:

// b unannotated: the pvar standing for b's precondition can absorb `a > 0`
#[thrust_macros::param(a: { v: i64 | v > 0 })]
#[thrust_macros::ret({ r: i64 | r > 0 })]
fn f(a: i64, b: i64) -> i64 { let _ = b; a }
fn main() { let _ = f(1, -5); }                          // safe

The loss only becomes observable once every parameter carries a declared refinement, which is exactly what #[sig(..)] produces. tests/ui has no such case: refine_param_simple.rs, refine_sig.rs, fn_poly_annot*.rs etc. all annotate a single parameter.

SMT evidence

CHCs for first.rs (Unsat) and second.rs (safe), via THRUST_OUTPUT_DIR. The two systems differ only in c0's first conjunct ((= v0 v1) returns a, (= v0 v2) returns b):

; first.rs — Unsat
; c0
(assert (forall ((v0 Int) (v1 Int) (v2 Int) (v3 Int) (v4 Int) (v5 Int) (v6 Int) (v7 Int))
  (=> (and (= v0 v1) (= v3 v1) (= v4 v2) (p2 v4 v1 v2 v3) (= v5 v4) (= v6 v3) (= v7 v0) (not (> v7 0))) false)))
; c1
(assert (forall ((v0 Int) (v1 Int) (v2 Int)) (=> (and  (> v2 0)) (p2 v2 v0 v2 v0))))
;                                                      ^^^^^^^ only ONE parameter refinement

; second.rs — safe
; c0
(assert (forall ((v0 Int) (v1 Int) (v2 Int) (v3 Int) (v4 Int) (v5 Int) (v6 Int) (v7 Int))
  (=> (and (= v0 v2) (= v3 v1) (= v4 v2) (p2 v4 v1 v2 v3) (= v5 v4) (= v6 v3) (= v7 v0) (not (> v7 0))) false)))
; c1
(assert (forall ((v0 Int) (v1 Int) (v2 Int)) (=> (and  (> v2 0)) (p2 v2 v0 v2 v0))))

c1 is the clause that installs the entry precondition predicate p2. It carries a single (> v2 0) — the refinement of the last parameter. a's declared v > 0 occurs nowhere in either system, so in first.rs the returned value is unconstrained and r > 0 cannot be discharged.

Root cause

The entry basic block hosts its precondition in one predicate variable, attached to the last parameter: FunctionTemplateTypeBuilder::build (src/refine/template.rs:603-664, reached from build_basic_block_with_precondition, src/refine/template.rs:451) gives the last parameter a build_refined template and every earlier parameter RefinedType::unrefined.

assert_entry (src/analyze/local_def.rs:1109-1125) then ties the declared signature to that entry type parameter-by-parameter:

let clauses = rty::relate_sub_param_types(&entry_ty.params, &expected.params);

and relate_sub_param_types (src/rty/subtyping.rs:192-214) emits one independent clause per parameter, on a builder that only ever gains the parameters' sorts:

for (param_idx, param_rty) in got.iter_enumerated() {
    let param_sort = param_rty.ty.to_sort();
    if !param_sort.is_singleton() {
        builder.add_mapped_var(param_idx, param_sort);   // adds the var, NOT its refinement
    }
}

for (got_ty, expected_ty) in got.iter().zip(expected.iter()) {
    let cs = builder.relate_sub_refined_type(expected_ty, got_ty);
    clauses.extend(cs);
}

For parameter i, that is the clause expected.params[i].refinement ⟹ entry.params[i].refinement. Since entry.params[i].refinement is true for every i before the last, each of those clauses is φ_i ⟹ true — trivially valid, and φ_i is discarded. Only the last parameter's clause has p2 as its head, so only φ_last reaches the body.

#[requires(..)] escapes this because FunctionTemplateTypeBuilder::param_refinement (src/refine/template.rs:528) rewrites the whole formula onto the last parameter (Free(len-1) → Value, other parameters staying free), so a conjunction over all parameters survives as φ_last.

The canonical hand-written version of the same judgment does accumulate. relate_fn_param_sub_types_with_builder (src/analyze/basic_block.rs:296-313), used on the call-site path, threads one mutable builder and feeds each parameter's refinement back into it:

builder
    .with_mapped_value_var(param_idx)
    .add_body(expected_ty.refinement.clone());

relate_sub_param_types is missing exactly that step.

Verified fix

Mirroring the canonical implementation:

--- a/src/rty/subtyping.rs
+++ b/src/rty/subtyping.rs
@@ fn relate_sub_param_types
-    for (got_ty, expected_ty) in got.iter().zip(expected.iter()) {
+    for ((param_idx, got_ty), expected_ty) in got.iter_enumerated().zip(expected.iter()) {
         let cs = builder.relate_sub_refined_type(expected_ty, got_ty);
         clauses.extend(cs);
+        builder
+            .with_mapped_value_var(param_idx)
+            .add_body(expected_ty.refinement.clone());
     }

Results with that patch applied:

file	before	after
first.rs	Unsat	safe
second.rs	safe	safe
add_sig.rs	Unsat	safe
3-parameter b / c variants	Unsat / safe	safe / safe
param+param with assert!(a > 0)	Unsat	safe
param+param+ret	Unsat	safe
caller f(-1, 2) violating a's refinement	Unsat	Unsat (still rejected)
caller f(1, -2) violating b's refinement	Unsat	Unsat (still rejected)

cargo test is unchanged by the patch: the same 34 tests fail and 308 pass with and without it, and the failing set is identical (diff of the two lists is empty). Those 34 are the pre-existing THRUST_SOLVER=tests/thrust-pcsat-wrapper cases, which need the Docker-hosted solver this environment does not have.

Treat the diff as a diagnosis rather than a finished change — a tests/ui/pass case with a fully refinement-typed multi-parameter signature (plus a fail twin whose body violates the return refinement) would be the guard.

Soundness is preserved

Only the callee's assumption is lost; the declared refinements are still obligations at every call site, so this over-rejects and never accepts a panicking program through this path:

#[thrust_macros::param(a: { v: i64 | v > 0 })]
#[thrust_macros::param(b: { v: i64 | v > 0 })]
fn f(a: i64, b: i64) -> i64 { a + b }

fn main() { let _ = f(1, 2); }    // safe
// fn main() { let _ = f(-1, 2); } // Unsat — a's refinement checked at the call site
// fn main() { let _ = f(1, -2); } // Unsat — b's refinement checked at the call site

Relation to existing issues

• Incompleteness: function-type subtyping in relate_sub_type proves the return obligation without assuming the parameters' preconditions #128 reports the analogous missing accumulation in relate_sub_type's Type::Function arm (the return obligation proved without the parameters' preconditions), and its "Related" paragraph already points at relate_sub_param_types as having "the same shape". That paragraph predicts a narrower symptom — a dependent refinement (parameter j mentioning parameter i) related without assuming φ_i. The defect here is wider and needs no dependency at all: because the entry block carries a refinement on the last parameter only, every earlier φ_i is discarded outright even when it mentions nothing. The two are different functions and different missing add_body calls — fixing Incompleteness: function-type subtyping in relate_sub_type proves the return obligation without assuming the parameters' preconditions #128's Type::Function arm does not fix this — but they are the same class, so please fold them together if you would rather track one.
• Incompleteness: a #[param(name: { v | φ })] precondition is silently dropped when the function also has an #[ensures(..)], so trivially-correct functions are rejected #191 / Unsound: a #[param(name: { v | φ })] precondition combined with #[ensures(..)] is dropped at call sites too, so a #[thrust::trusted] function with a violated precondition verifies panicking programs as safe #196 are about the param × ensures combination with a single parameter; Incompleteness: a #[param(name: { v | φ })] precondition is silently dropped when the function also has an #[ensures(..)], so trivially-correct functions are rejected #191's table records param + ret as verifying, which it does — for one parameter. This report is about the number of refined parameters, and reproduces with param + param and with sig alone, no ensures involved.
• Incompleteness: refinement on a reference's pointee (&{ v | φ } / &mut { v | φ }) in parameter position is not assumed by the callee #166 is the same "declared precondition not assumed" family but for a reference's pointee refinement (&mut { v | φ }); that one reproduces with a single parameter (#[sig(fn(x: &mut { v: i64 | v > 0 }) -> ())] is Unsat even alone), so it is a separate defect.
• Unrelated to the integer-modeling issues (Unsigned integer constants sign-extended incorrectly in const_value_ty, causing wrong CHC terms and potential panic #110/Incompleteness: unsigned integer types (usize/u32/u64) are modeled as unconstrained integers, so their >= 0 lower bound is not assumed and safe programs are wrongly rejected #165/Unsoundness: unsigned subtraction underflow is not modeled, so panicking programs are verified as safe #172/Unsound: unsigned integer constants with the high bit set (e.g. u8 = 200) are decoded as negative in const_value_ty, so always-panicking programs verify as safe #180): the values here are small and in range, and nothing is lost in the encoding of the refinements themselves — they are simply never emitted.

Environment

• thrust @ 2bf022d (Let a ghost term name generic- and Self-typed variables (#232))
• rustc nightly-2025-09-08 (per rust-toolchain.toml), x86_64-unknown-linux-gnu
• Z3 5.0.0, default solver configuration
• Confirmed by running thrust-rustc, not by inspection alone.