Incompleteness: an existentially-quantified precondition (`requires(exists ..)`) emits a quantifier into the Horn clause body, so the default `z3` solver returns `unknown` — `Result::unwrap`/`unwrap_err` are unverifiable

[coord-e]

Summary

When a callee's precondition contains an existential quantifier (#[requires(thrust_models::exists(..))]), the caller-side proof obligation places expected.refinement in the head of the subtyping clause (src/rty/subtyping.rs:151-152). For a concrete (non-predicate) refinement this is emitted as a query clause of the form body ∧ ¬head ⟹ false, so the existential head becomes (not (exists ..)) — i.e. a universal quantifier inside the Horn clause body. z3's HORN engine (spacer) cannot decide such a clause and returns unknown, which Thrust surfaces as verification error: Unknown.

Because the shipped std model uses this exact form for Result::unwrap (std.rs:611) and Result::unwrap_err (std.rs:621), any call to Result::unwrap() fails to verify under the documented default solver (z3). The parallel Option::unwrap (std.rs:475) was written quantifier-free (requires(opt != None)) and verifies correctly, so this is a concrete, avoidable inconsistency between two core stdlib specs — not a fundamental limitation.

This is incompleteness (a trivially-safe program is rejected), not unsoundness.

Reproduction

All three run with the default solver and -Adead_code -C debug-assertions=false.

(1) Result::unwrap on a literal Ok — rejected, but obviously safe:

fn main() {
    let r: Result<i32, i32> = Ok(7);
    let v = r.unwrap();
    assert!(v == 7);
}

error: verification error: Unknown { stdout: "unknown\n" }

(2) The Option analogue — verifies (safe):

fn main() {
    let o: Option<i32> = Some(7);
    let v = o.unwrap();
    assert!(v == 7);
}

(3) Minimal root cause — a user requires(exists ..) satisfied by a constant:

use thrust_models::exists;
#[thrust_macros::requires(exists(|x: i32| n == 2 * x))]
fn needs_even(n: i32) -> i32 { n }
fn main() { let _ = needs_even(4); }   // 4 == 2*2, trivially satisfiable

error: verification error: Unknown { stdout: "unknown\n" }

program	precondition form	verdict	correct verdict
Some(7).unwrap()	opt != None (quantifier-free)	safe ✓	safe
Ok(7).unwrap()	exists(|x| res == Ok(x))	Unknown ✗	safe
needs_even(4)	exists(|x| n == 2*x)	Unknown ✗	safe

Root cause & evidence

sub_refined_type builds the refinement-subtyping obligation with the super-type's refinement as the clause head (src/rty/subtyping.rs:151-152):

let cs = self
    .build_clause()
    .with_value_var(&got.ty)
    .add_body(got.refinement.clone())
    .head(expected.refinement.clone());   // <-- callee precondition goes to the head

When expected.refinement is a concrete existential formula, the emitted SMT-LIB negates it into the body. Dumped via THRUST_OUTPUT_DIR for reproduction (3):

; c1  — the caller's "precondition must hold" obligation
(assert (forall ((v0 Int) (v1 Int))
  (=> (and p3 (= v1 4) (not (exists ((x Int)) (= v1 (* 2 x))))) false)))

and for Ok(7).unwrap() (reproduction 1):

(assert (forall (..)
  (=> (and (= v0 (std.result.Result.Ok<Int-Int> 7)) p2 (= v2 v0)
           (not (exists ((x Int)) (= v2 (std.result.Result.Ok<Int-Int> x))))) false)))

The (not (exists ..)) in the clause body is a universal quantifier over the body — outside the fragment z3's HORN/spacer engine decides.

Running the exact default invocation (z3 fp.spacer.global=true fp.validate=true) on the generated files:

• reproduction (1) Result::unwrap → unknown
• reproduction (3) exists precond → unknown
• reproduction (2) Option::unwrap → sat (i.e. safe; its SMT contains zero exists)

For contrast, z3 solves the underlying obligation instantly when it is not buried in a Horn-clause body:

$ echo '(declare-const x Int)(assert (= 4 (* 2 x)))(check-sat)' | z3 -in
sat

So the math is trivial; only the CHC encoding of an existential head defeats the solver.

Why this is distinct from #142

#142 is about collect_sorts never visiting quantifier binder sorts, so a binder of datatype/tuple sort emits an undeclared sort and the solver rejects the query as ill-typed at parse time. Here the binder is Int (its sort is declared), the SMT is well-formed, and the solver actually runs and returns a genuine unknown. Different code path (sub_refined_type obligation encoding vs. collect_sorts), different failure mode (unknown vs. parse error). Fixing #142 would not fix this.

Impact

Result::unwrap / Result::unwrap_err — extremely common operations — cannot be verified at all under the default (z3) solver, and any user-written existential precondition has the same problem. No test in tests/ui/pass/ currently exercises Result::unwrap, so this is uncovered.

Suggested fixes (either)

1. Reformulate the Result specs quantifier-free, mirroring Option::unwrap. e.g. give res an is_ok-style discriminant projection so unwrap's precondition avoids exists entirely.
2. Handle existential head refinements in the CHC encoding — e.g. Skolemize the existential when moving expected.refinement into a query clause, so no quantifier remains in the clause body — so that requires(exists ..) is generally supported by the default solver rather than only under pcsat.