Verus attributes for executable code

The #[verus_spec] attribute macro can help add Verus specifications and proofs to existing executable code without sacrificing readability.

When to use #[verus_spec] instead of the verus! macro

The default way to write Verus code is by using the verus! macro. However, using verus! to embed specifications and proofs directly in executable code may not always be ideal for production settings. This is particularly true when developers want to integrate verification into an existing Rust project and aim to:

1. Minimize changes to executable code — avoid modifying function APIs to include tracked or ghost arguments, and preserve native Rust syntax for maintainability.
2. Adopt verification incrementally — apply Verus gradually to a large, existing codebase without requiring a full rewrite of the function APIs.
3. Maintain readability — ensure the verified code remains clean and understandable for developers who are not familiar with Verus or want to ignore verification-related annotations.
4. Optimize dependency management — use Verus components (verus_builtin, verus_builtin_macros, and vstd) in a modular way, allowing projects to define custom stub macros and control Verus dependencies via feature flags.

Adding specifications to a function

Use #[verus_spec(requires ... ensures ...)] to attach a specification to a function signature.

Here is an example:

#[verus_spec(sum => 
     requires 
         x < 100, 
         y < 100, 
     ensures 
         sum < 200, 
)]
fn my_exec_fun(x: u32, y: u32) -> u32 
{ 
    x + y 
}

Adding verification hints

Use #[verus_verify(...)] to provide hints to the verifier to mark a function as external, external_body, spinoff_prover, or specify a different resource limit via rlimit(amount).

In addition, you can create a dual mode (spec + exec) function the via verus_verify(dual_spec) attribute, which will attempt to generate a spec function from an executable function.

Adding proofs inside function

When a function has the #[verus_spec(...)] attribute, we can introduce proofs directly inside executable functions using the proof macros described below.

When Rust builds the code (without using Verus), the #[verus_spec(...)] attribute will ensure all proof code is erased.

Simple proof blocks

Use proof! to add a proof block; this is equivalent to using proof { ... } inside the verus! macro. This implies that ghost/tracked variables defined inside of proof! are local to that proof block and cannot be used in other proof blocks.

Ghost/Tracked variables across proof blocks

Use proof_decl! when you need to use ghost or tracked variables across different proof blocks. It will allow you to introduce a proof block and declare function-scoped ghost/tracked variables, as shown in this example:

#[verus_spec]
fn exec_with_proof() {
   proof_decl!{
     let ghost mut i = 0int;
     assert(true);
   }
   test_for_loop(10);
   proof!{
     assert(i == 0);
   }
}

Adding ghost/tracked variables to executable function calls

• #[verus_spec(with ...)]: Adds tracked or ghost variables as parameters or return values in an executable function.

  This generates two versions of the original function:

  • A verified version (with ghost/tracked parameters), used in verified code.
  • An unverified version (with the original signature), callable from unverified code.

• proof_with! Works in combination with verus_spec to pass tracked/ghost variables to a callee.

  When proof_with! precedes a function call, the verified version is used; otherwise, the unverified version is chosen. The unverified version includes a requires false precondition, ensuring that improper use of proof_with! will cause a verification failure when called from verified code.

Here is an example:

#[verus_spec(ret =>
with
  Tracked(y): Tracked<&mut u32>,
  Ghost(w): Ghost<u32> 
     -> z: Ghost<u32>
requires
  x < 100,
  *old(y) < 100,
ensures
  *y == x,
  ret == x + 1,
  z@ == x,
)]
fn exec_tracked(x: u32) -> u32 {
  proof! {
    *y = x;
  }
  proof_with!(|= Ghost(x));
  (x + 1)
}


#[verus_spec]
fn exec_tracked_test(x: u32) {
  proof_decl!{
    let ghost mut z = 0u32;
    let tracked mut y = 0u32;
  }

  proof_with!{Tracked(&mut y), Ghost(0) => Ghost(z)}
  let x = exec_tracked(1);

  proof!{
    assert(y == 1);
    assert(z == 1);
    assert(x == 2);
  }
}

fn exec_external_test(x: u32) -> u32 {
   exec_tracked(1)
}

Using a mix of #[verus_spec] and verus!

The preferred way to use #[verus_spec] and verus! is to use #[verus_spec] for all executable functions, and use verus! for spec/proof functions.

NOTE: The combination of #[verus_spec(with ...)] + proof_with! currently has compatibility issues with executable functions defined in verus! if the functions involved receive or return ghost/tracked variables.

Specifically, proof_with! works with exec functions verified via #[verus_spec]. Using proof_with! to pass ghost/tracked variables to an exec function verified via verus! will result in this error:

[E0425]: cannot find function `_VERUS_VERIFIED_xxx` in this scope.

This is because verus! always requires a real change to the function’s signature and has a single function definition, while #[verus_spec] expects a verified and an unverified version of the function.

To use a function verified by verus!, a workaround is to create a trusted wrapper function and then use it.

#[verus_verify(external_body)]
#[verus_spec(v =>
   with Tracked(perm): Tracked<&mut PointsTo<T>>
   requires
        old(perm).ptr() == ptr,
        old(perm).is_init(),
    ensures
        perm.ptr() == ptr,
        perm.is_uninit(),
        v == old(perm).value(),
)]
fn ptr_mut_read<'a, T>(ptr: *const T)  -> T
{
   vstd::raw_ptr::ptr_mut_read(ptr, Tracked::assume_new())
}

More examples and tests

#![feature(proc_macro_hygiene)]
#![allow(unused_imports)]

use verus_builtin::*;
use verus_builtin_macros::*;
use vstd::{modes::*, prelude::*, seq::*, *};

fn main() {}

/// functions may be declared exec (default), proof, or spec, which contain
/// exec code, proof code, and spec code, respectively.
///   - exec code: compiled, may have requires/ensures
///   - proof code: erased before compilation, may have requires/ensures
///   - spec code: erased before compilation, no requires/ensures, but may have recommends
/// exec and proof functions may name their return values inside parentheses, before the return type
#[verus_spec(sum =>
    requires
        x < 100,
        y < 100,
    ensures
        sum < 200,
)]
fn my_exec_fun(x: u32, y: u32) -> u32
{
    x + y
}

verus! {

proof fn my_proof_fun(x: int, y: int) -> (sum: int)
    requires
        x < 100,
        y < 100,
    ensures
        sum < 200,
{
    x + y
}

spec fn my_spec_fun(x: int, y: int) -> int
    recommends
        x < 100,
        y < 100,
{
    x + y
}

} // verus!

/// exec code cannot directly call proof functions or spec functions.
/// However, exec code can contain proof blocks (proof { ... }),
/// which contain proof code.
/// This proof code can call proof functions and spec functions.
#[verus_spec(
    requires
        x < 100,
        y < 100,
)]
fn test_my_funs(x: u32, y: u32)
{
    // my_proof_fun(x, y); // not allowed in exec code
    // let u = my_spec_fun(x, y); // not allowed exec code
    proof! {
        let u = my_spec_fun(x as int, y as int);  // allowed in proof code
        my_proof_fun(u / 2, y as int);  // allowed in proof code
    }
}

verus! {

/// spec functions with pub or pub(...) must specify whether the body of the function
/// should also be made publicly visible (open function) or not visible (closed function).
pub open spec fn my_pub_spec_fun1(x: int, y: int) -> int {
    // function and body visible to all
    x / 2 + y / 2
}

/* TODO
pub open(crate) spec fn my_pub_spec_fun2(x: u32, y: u32) -> u32 {
    // function visible to all, body visible to crate
    x / 2 + y / 2
}
*/

// TODO(main_new) pub(crate) is not being handled correctly
// pub(crate) open spec fn my_pub_spec_fun3(x: int, y: int) -> int {
//     // function and body visible to crate
//     x / 2 + y / 2
// }
pub closed spec fn my_pub_spec_fun4(x: int, y: int) -> int {
    // function visible to all, body visible to module
    x / 2 + y / 2
}

pub(crate) closed spec fn my_pub_spec_fun5(x: int, y: int) -> int {
    // function visible to crate, body visible to module
    x / 2 + y / 2
}

} // verus!

/// Recursive functions must have decreases clauses so that Verus can verify that the functions
/// terminate.
#[verus_spec(
    requires
        0 < x < 100,
        y < 100 - x,
    decreases x,
)]
fn test_rec(x: u64, y: u64)
{
    if x > 1 {
        test_rec(x - 1, y + 1);
    }
}

verus! {

/// Multiple decreases clauses are ordered lexicographically, so that later clauses may
/// increase when earlier clauses decrease.
spec fn test_rec2(x: int, y: int) -> int
    decreases x, y,
{
    if y > 0 {
        1 + test_rec2(x, y - 1)
    } else if x > 0 {
        2 + test_rec2(x - 1, 100)
    } else {
        3
    }
}

/// To help prove termination, recursive spec functions may have embedded proof blocks
/// that can make assertions, use broadcasts, and call lemmas.
spec fn test_rec_proof_block(x: int, y: int) -> int
    decreases x,
{
    if x < 1 {
        0
    } else {
        proof {
            assert(x - 1 >= 0);
        }
        test_rec_proof_block(x - 1, y + 1) + 1
    }
}

/// Decreases and recommends may specify additional clauses:
///   - decreases .. "when" restricts the function definition to a condition
///     that makes the function terminate
///   - decreases .. "via" specifies a proof function that proves the termination
///     (although proof blocks are usually simpler; see above)
///   - recommends .. "when" specifies a proof function that proves the
///     recommendations of the functions invoked in the body
spec fn add0(a: nat, b: nat) -> nat
    recommends
        a > 0,
    via add0_recommends
{
    a + b
}

spec fn dec0(a: int) -> int
    decreases a,
    when a > 0
    via dec0_decreases
{
    if a > 0 {
        dec0(a - 1)
    } else {
        0
    }
}

#[via_fn]
proof fn add0_recommends(a: nat, b: nat) {
    // proof
}

#[via_fn]
proof fn dec0_decreases(a: int) {
    // proof
}

} // verus!

/// variables may be exec, tracked, or ghost
///   - exec: compiled
///   - tracked: erased before compilation, checked for lifetimes (advanced feature, discussed later)
///   - ghost: erased before compilation, no lifetime checking, can create default value of any type
/// Different variable modes may be used in different code modes:
///   - variables in exec code are always exec
///   - variables in proof code are ghost by default (tracked variables must be marked "tracked")
///   - variables in spec code are always ghost
/// For example:
#[verus_spec(
    requires
        a < 100,
        b < 100,
)]
fn test_my_funs2(
    a: u32,  // exec variable
    b: u32,  // exec variable
)
{
    let s = a + b;  // s is an exec variable
    proof! {
        let u = a + b;  // u is a ghost variable
        my_proof_fun(u / 2, b as int);  // my_proof_fun(x, y) takes ghost parameters x and y
    }
}

verus! {

/// assume and assert are treated as proof code even outside of proof blocks.
/// "assert by" may be used to provide proof code that proves the assertion.
#[verifier::opaque]
spec fn f1(i: int) -> int {
    i + 1
}

} // verus!

#[verus_spec()]
fn assert_by_test() {
    proof! {
        assert(f1(3) > 3) by {
            reveal(f1);  // reveal f1's definition just inside this block
        }
        assert(f1(3) > 3);
    }
}

/// "assert by" can also invoke specialized provers for bit-vector reasoning or nonlinear arithmetic.
#[verus_spec()]
fn assert_by_provers(x: u32) {
    proof! {
        assert(x ^ x == 0u32) by (bit_vector);
        assert(2 <= x && x < 10 ==> x * x > x) by (nonlinear_arith);
    }
}

verus! {

/// "let ghost" currently requires the verus! macro
/// Variables in exec code may be exec, ghost, or tracked.
fn test_ghost(x: u32, y: u32)
    requires
        x < 100,
        y < 100,
{
    let ghost u: int = my_spec_fun(x as int, y as int);
    let ghost mut v = u + 1;
    assert(v == x + y + 1);
    proof {
        v = v + 1;  // proof code may assign to ghost mut variables
    }
    let ghost w = {
        let temp = v + 1;
        temp + 1
    };
    assert(w == x + y + 4);
}

/// Ghost(...) expressions and patterns currently require the verus! macro
/// Ghost(...) and Tracked(...) patterns can unwrap Ghost<...> and Tracked<...> values:
fn test_ghost_unwrap(
    x: u32,
    Ghost(y): Ghost<u32>,
)  // unwrap so that y has typ u32, not Ghost<u32>
    requires
        x < 100,
        y < 100,
{
    // Ghost(u) pattern unwraps Ghost<...> values and gives u and v type int:
    let Ghost(u): Ghost<int> = Ghost(my_spec_fun(x as int, y as int));
    let Ghost(mut v): Ghost<int> = Ghost(u + 1);
    assert(v == x + y + 1);
    proof {
        v = v + 1;  // assign directly to ghost mut v
    }
    let Ghost(w): Ghost<int> = Ghost(
        {
            // proof block that returns a ghost value
            let temp = v + 1;
            temp + 1
        },
    );
    assert(w == x + y + 4);
}

} // verus!

/// Trait functions may have specifications
trait T {
    #[verus_spec(r =>
        requires
            0 <= i < 10,
            0 <= j < 10,
        ensures
            i <= r,
            j <= r,
    )]
    fn my_uninterpreted_fun2(&self, i: u8, j: u8) -> u8;
}

#[verus_spec(ret =>
    with
        Tracked(y): Tracked<&mut u32>, Ghost(w): Ghost<u64> -> z: Ghost<u32>
    requires
        x < 100,
        *old(y) < 100,
    ensures
        *y == x,
        ret == x,
        z == x,
)]
fn test_mut_tracked(x: u32) -> u32 {
    proof!{
        *y = x;
    }
    #[verus_spec(with |=Ghost(x))]
    x
}

fn test_cal_mut_tracked(x: u32) {
    proof_decl!{
        let ghost mut z;
        let tracked mut y = 0u32;
        z = 0u32;
    }
    #[verus_spec(with Tracked(&mut y), Ghost(0) => Ghost(z))]
    let _ = test_mut_tracked(0u32);

    (#[verus_spec(with Tracked(&mut y), Ghost(0))]
    test_mut_tracked(0u32));

    return;
}

#![feature(rustc_private)]
#[macro_use]
mod common;
use common::*;

test_verify_one_file_with_options! {
    #[test] verus_verify_basic_while ["exec_allows_no_decreases_clause"] =>  code! {
        #[verus_spec]
        fn test1() {
            let mut i = 0;
            #[verus_spec(
                invariant
                    i <= 10
            )]
            while i < 10
            {
                i = i + 1;
            }
            proof!{assert(i == 10);}
        }
    } => Ok(())
}

test_verify_one_file_with_options! {
    #[test] verus_verify_basic_loop ["exec_allows_no_decreases_clause"] => code! {
        #[verus_spec]
        fn test1() {
            let mut i = 0;
            let mut ret = 0;
            #[verus_spec(
                invariant i <= 10,
                invariant_except_break i <= 9,
                ensures i == 10, ret == 10
            )]
            loop
            {
                i = i + 1;
                if (i == 10) {
                    ret = i;
                    break;
                }
            }
            proof!{assert(ret == 10);}
        }
    } => Ok(())
}

test_verify_one_file_with_options! {
    #[test] verus_verify_basic_for_loop_verus_spec ["exec_allows_no_decreases_clause"] =>  code! {
        use vstd::prelude::*;
        #[verus_spec(v =>
            ensures
                v.len() == n,
                forall|i: int| 0 <= i < n ==> v[i] == i
        )]
        fn test_for_loop(n: u32) -> Vec<u32>
        {
            let mut v: Vec<u32> = Vec::new();
            #[verus_spec(
                invariant
                    v@ =~= Seq::new(i as nat, |k| k as u32),
            )]
            for i in 0..n
            {
                v.push(i);
            }
            v
        }
    } => Ok(())
}

test_verify_one_file_with_options! {
    #[test] verus_verify_for_loop_verus_spec_naming_iter ["exec_allows_no_decreases_clause"] =>  code! {
        use vstd::prelude::*;
        #[verus_spec(v =>
            ensures
                v.len() == n,
                forall|i: int| 0 <= i < n ==> v[i] == 0
        )]
        fn test(n: u32) -> Vec<u32>
        {
            let mut v: Vec<u32> = Vec::new();
            #[verus_spec(iter =>
                invariant
                    v@ =~= Seq::new(iter.cur as nat, |k| 0u32),
            )]
            for _ in 0..n
            {
                v.push(0);
            }
            v
        }
    } => Ok(())
}

test_verify_one_file_with_options! {
    #[test] verus_verify_basic_while_fail1 ["exec_allows_no_decreases_clause"] => code! {
        #[verus_spec]
        fn test1() {
            let mut i = 0;
            while i < 10 {
                i = i + 1;
            }
            proof!{assert(i == 10);} // FAILS
        }
    } => Err(err) => assert_one_fails(err)
}

test_verify_one_file_with_options! {
    #[test] basic_while_false_invariant ["exec_allows_no_decreases_clause"] => code! {
        #[verus_verify]
        fn test1() {
            let mut i = 0;
            #[verus_spec(
                invariant
                    i <= 10, false
            )]
            while i < 10 {
                i = i + 1;
            }
        }
    } => Err(err) => assert_any_vir_error_msg(err, "invariant not satisfied before loop")
}

test_verify_one_file_with_options! {
    #[test] verus_verify_invariant_on_func ["exec_allows_no_decreases_clause"] => code! {
        #[verus_spec(
            invariant true
        )]
        fn test1() {}
    } => Err(err) => assert_any_vir_error_msg(err, "unexpected token")
}

test_verify_one_file! {
    #[test] test_use_macro_attributes code!{
        struct Abc<T> {
            t: T,
        }

        trait SomeTrait {
            #[verus_spec(ret =>
                requires true
                ensures ret
            )]
            fn f(&self) -> bool;
        }

        impl<S> Abc<S> {
            fn foo(&self)
                where S: SomeTrait
            {
                let ret = self.t.f();
                proof!{assert(ret);}
            }
        }
    } => Ok(())
}

test_verify_one_file! {
    #[test] test_bad_macro_attributes_in_trait code!{
        trait SomeTrait {
            #[verus_spec(
                ensures
                    true
            )]
            type T;
        }
    } => Err(err) => assert_any_vir_error_msg(err, "Misuse of #[verus_spec]")
}

test_verify_one_file_with_options! {
    #[test] test_no_verus_verify_attributes_in_trait_impl ["--no-external-by-default"] => code!{
        struct Abc<T> {
            t: T,
        }

        #[verus_verify]
        trait SomeTrait {
            #[verus_spec(requires true)]
            fn f(&self) -> bool;
        }

        impl<S> Abc<S> {
            fn foo(&self)
                where S: SomeTrait
            {
                let ret = self.t.f();
                proof!{assert(ret);}
            }
        }
    } => Err(err) => assert_vir_error_msg(err, "assertion failed")
}

test_verify_one_file! {
    #[test] test_failed_ensures_macro_attributes code!{
        #[verus_verify]
        trait SomeTrait {
            #[verus_spec(ret =>
                requires true
                ensures true, ret
            )]
            fn f(&self) -> bool;
        }

        #[verus_verify]
        impl SomeTrait for bool {
            fn f(&self) -> bool {
                *self
            }
        }
    } => Err(err) => assert_any_vir_error_msg(err, "postcondition not satisfied")
}

test_verify_one_file! {
    #[test] test_default_fn_use_macro_attributes code!{
        #[verus_verify]
        struct Abc<T> {
            t: T,
        }

        #[verus_verify]
        trait SomeTrait {
            #[verus_spec(ret =>
                requires true
                ensures ret
            )]
            fn f(&self) -> bool {
                true
            }
        }

        #[verus_verify]
        impl<S> Abc<S> {
            fn foo(&self)
                where S: SomeTrait
            {
                let ret = self.t.f();
                proof!{assert(ret);}
            }
        }
    } => Ok(())
}

test_verify_one_file! {
    #[test] test_default_failed_fn_use_macro_attributes code!{
        #[verus_verify]
        struct Abc<T> {
            t: T,
        }

        #[verus_verify(rlimit(2))]
        trait SomeTrait {
            #[verus_spec(ret =>
                requires true
                ensures ret, !ret
            )]
            fn f(&self) -> bool {
                true
            }
        }
    } => Err(err) => assert_vir_error_msg(err, "postcondition not satisfied")
}

test_verify_one_file! {
    #[test] test_external_body code!{
        #[verus_verify(external_body)]
        #[verus_spec(ret =>
            requires true
            ensures ret
        )]
        fn f() -> bool {
            false
        }

        fn g() {
            let r = f();
            proof!{assert(r);}
        }
    } => Ok(())
}

test_verify_one_file! {
    #[test] test_external_with_unsupported_features code!{
        #[verus_verify(external)]
        fn f<'a>(v: &'a mut [usize]) -> &'a mut usize {
            unimplemented!()
        }
    } => Ok(())
}

test_verify_one_file! {
    #[test] test_prover_attributes code!{
        #[verus_verify(spinoff_prover, rlimit(2))]
        #[verus_spec(
            ensures
                true
        )]
        fn test()
        {}
    } => Ok(())
}

test_verify_one_file! {
    #[test] test_invalid_combination_attr code!{
        #[verus_verify(external, spinoff_prover)]
        fn f<'a>(v: &'a mut [usize]) -> &'a mut usize {
            unimplemented!()
        }
    } => Err(e) => assert_any_vir_error_msg(e, "conflict parameters")
}

test_verify_one_file! {
    #[test] test_proof_decl code!{
        #[verus_spec]
        fn f() {}
        #[verus_spec]
        fn test() {
            proof!{
                let x = 1 as int;
                assert(x == 1);
            }
            proof_decl!{
                let ghost mut x;
                let tracked y = false;
                x = 2int;
                assert(!y);
                if x == 1 {
                    assert(false);
                }
            }

            f();
            proof!{
                assert(!y);
                assert(x == 2);
            }
        }
    } => Ok(())
}

test_verify_one_file! {
    #[test] test_proof_decl_reject_exec code!{
        #[verus_spec]
        fn f() {}
        #[verus_spec]
        fn test() {
            proof_decl!{
                f();
            }
            f();
        }
    } => Err(e) => assert_vir_error_msg(e, "cannot call function `crate::f` with mode exec")
}

test_verify_one_file! {
    #[test] test_proof_decl_reject_exec_local code!{
        #[verus_spec]
        fn test() {
            proof_decl!{
                let x = true;
            }
        }
    } => Err(e) => assert_vir_error_msg(e, "Exec local is not allowed in proof_decl")
}

test_verify_one_file! {
    #[test] test_with code!{
        #[verus_spec(ret =>
            with
                Tracked(y): Tracked<&mut u32>,
                Ghost(w): Ghost<u32>,
                -> z: Ghost<u32>
            requires
                x < 100,
                *old(y) < 100,
            ensures
                *y == x,
                ret == x,
                z@ == x,
        )]
        fn test_mut_tracked(x: u32) -> u32 {
            proof!{
                *y = x;
            }
            #[verus_spec(with |= Ghost(x))]
            x
        }

        #[verus_spec]
        fn test_call_mut_tracked(x: u32) {
            proof_decl!{
                let tracked mut y = 0u32;
            }
            {#[verus_spec(with Tracked(&mut y), Ghost(0) => _)]
            test_mut_tracked(1);
            };

            if x < 100 && #[verus_spec(with Tracked(&mut y), Ghost(0) => _)]test_mut_tracked(x) == 0 {
                return;
            }

            #[verus_spec(with Tracked(&mut y), Ghost(0) => Ghost(z))]
            let _ = test_mut_tracked(1);

            proof!{
                assert(y == 1);
                assert(z == 1);
            }
        }
    } => Ok(())
}

test_verify_one_file! {
    #[test] test_trait_signature code!{
        trait X {
            #[verus_spec(ret =>
                with
                    Tracked(y): Tracked<&mut u32>,
                    Ghost(w): Ghost<u32>,
                    -> z: Ghost<u32>
            )]
            fn f(&self, x: u32) -> bool;
        }
    } => Err(e) => assert_any_vir_error_msg(e, "`with` does not support trait")
}

test_verify_one_file! {
    #[test] test_unverified_code_signature code!{
        #[verus_spec(ret =>
            with
                Tracked(y): Tracked<&mut u32>,
                Ghost(w): Ghost<u32>,
                -> z: Ghost<u32>
        )]
        fn test_mut_tracked(x: u32) -> u32 {
            proof!{
                *y = x;
            }
            #[verus_spec(with |= Ghost(x))]
            x
        }

        #[verifier::external]
        fn external_call_with_dummy(x: u32) -> u32 {
            #[verus_spec(with Tracked::assume_new(), Ghost::assume_new() => _)]
            test_mut_tracked(0)
        }

        #[verifier::external]
        fn external_call_untouched(x: u32) -> u32 {
            test_mut_tracked(0)
        }
    } => Ok(())
}

test_verify_one_file! {
    #[test] test_verified_call_unverified_signature code!{
        #[verus_spec(ret =>
            with
                Tracked(y): Tracked<&mut u32>,
                Ghost(w): Ghost<u32>,
                -> z: Ghost<u32>
        )]
        fn test_mut_tracked(x: u32) -> u32 {
            proof!{
                *y = x;
            }
            #[verus_spec(with |= Ghost(x))]
            x
        }

        #[verus_spec]
        fn verified_call_unverified(x: u32) {
            test_mut_tracked(0); // FAILS
        }
    } => Err(e) => {
        assert!(e.errors[0].rendered.contains("with"));
        assert_one_fails(e)
    }
}

test_verify_one_file! {
    #[test] test_with2 code!{
        #[verus_spec(ret =>
            with
                Tracked(y): Tracked<&mut u32>,
                Ghost(w): Ghost<u32>,
                ->  z: Ghost<u32>
            requires
                x < 100,
                *old(y) < 100,
            ensures
                *y == x,
                ret == x,
                z@ == x,
        )]
        fn test_mut_tracked(x: u32) -> u32 {
            proof!{
                *y = x;
            }
            #[verus_spec(with |= Ghost(x))]
            x
        }

        #[verus_spec]
        fn test_cal_mut_tracked(x: u32) {
            proof_decl!{
                let ghost mut z = 0u32;
                let tracked mut y = 0u32;
            }
            if #[verus_spec(with Tracked(&mut y), Ghost(0) => Ghost(z))] test_mut_tracked(1) == 0 {
                proof!{
                    assert(z == 1);
                }
                return;
            }

            proof!{
                assert(y == 1);
            }
        }
    } => Ok(())
}

test_verify_one_file! {
    #[test] test_proof_with code!{
        #[verus_spec(ret =>
            with
                Tracked(y): Tracked<&mut u32>,
                Ghost(w): Ghost<u32>,
                ->  z: Ghost<u32>
            requires
                x < 100,
                *old(y) < 100,
            ensures
                *y == x,
                ret == x,
                z@ == x,
        )]
        fn test_mut_tracked(x: u32) -> u32 {
            proof!{
                *y = x;
            }
            proof_with!{|= Ghost(x)}
            x
        }

        #[verus_spec]
        fn test_cal_mut_tracked(x: u32) {
            proof_decl!{
                let ghost mut z = 0u32;
                let tracked mut y = 0u32;
            }
            if {
                proof_with!{Tracked(&mut y), Ghost(0) => Ghost(z)} test_mut_tracked(1)
            } == 0 {
                proof!{
                    assert(z == 1);
                }
                return;
            }

            proof!{
                assert(y == 1);
            }
        }
    } => Ok(())
}

test_verify_one_file! {
    #[test] test_proof_with_try code!{
        use vstd::prelude::*;
        #[verus_spec(
            with Tracked(y): Tracked<&mut u32>
        )]
        fn f() -> Result<(), ()> {
            Ok(())
        }

        #[verus_spec(
            with Tracked(y): Tracked<&mut u32>
        )]
        fn test_try_call() -> Result<(), ()> {
            proof_with!{Tracked(y)}
            let _ = f()?;
            Ok(())
        }
    } => Ok(())
}

test_verify_one_file! {
    #[test] test_proof_with_err code!{
        #[verus_spec]
        fn test_mut_tracked(x: u32) -> u32 {
            proof_declare!{
                let ghost y = x;
            }
            proof_with!{Ghost(y)}
            x
        }
    } => Err(e) => assert_any_vir_error_msg(e, "with ghost inputs/outputs cannot be applied to a non-call expression")
}

test_verify_one_file! {
    #[test] test_dual_spec code!{
        #[verus_verify(dual_spec(spec_f))]
        #[verus_spec(
            requires
                x < 100,
                y < 100,
            returns f(x, y)
        )]
        fn f(x: u32, y: u32) -> u32 {
            proof!{
                assert(true);
            }
            {
                proof!{assert(true);}
                x + y
            }
        }

        #[verus_verify(dual_spec)]
        #[verus_spec(
            requires
                x < 100,
            returns
                f2(x),
        )]
        pub fn f2(x: u32) -> u32 {
            f(x, 1)
        }

        #[verus_verify]
        struct S;

        impl S {
            #[verus_verify(dual_spec)]
            #[verus_spec(
                returns
                    self.foo(x),
            )]
            fn foo(&self, x: u32) -> u32 {
                x
            }
        }

        verus!{
        proof fn lemma_f(x: u32, y: u32)
        requires
            x < 100,
        ensures
            y == 1 ==> f(x, y) == f2(x),
            f(x, y) == spec_f(x, y),
            f2(x) == __VERUS_SPEC_f2(x),
            f(x, y) == (x + y) as u32,
            __VERUS_SPEC_f2(x) == x + 1,
        {}

        mod inner {
            use super::*;
            proof fn lemma_f(x: u32)
            requires
                x < 100,
            ensures
                f2(x) == __VERUS_SPEC_f2(x),
                __VERUS_SPEC_f2(x) == (x + 1),
            {}
        }
        }
    } => Ok(())
}

test_verify_one_file! {
    #[test] test_dual_spec_unsupported_body code!{
        #[verus_verify(dual_spec(spec_f))]
        #[verus_spec(
            requires
                x < 100,
                y < 100,
            returns
                f(x, y),
        )]
        fn f(x: &mut u32, y: u32) -> u32 {
            *x = *x + y;
            *x
        }
    } => Err(e) => assert_vir_error_msg(e, "The verifier does not yet support the following Rust feature")
}

test_verify_one_file! {
    #[test] test_dual_spec_unsupported_trait code!{
        trait X {
            fn f(&self) -> u32;
        }

        impl X for u32 {
            #[verus_verify(dual_spec(spec_f))]
            #[verus_spec(
                ensures
                    self.spec_f(),
            )]
            fn f(&self) -> u32{
                *self
            }
        }

    } => Err(e) => assert_rust_error_msg(e, "method `spec_f` is not a member of trait `X`")
}

test_verify_one_file! {
    #[test] test_macro_inside_proof_decl code!{
        macro_rules! inline_proof {
            ($val: expr => $x: ident, $y: ident) => {
                proof_decl!{
                    let tracked $x: int = $val;
                    let ghost $y: int = $val;
                    assert($x == $y);
                }
             }
        }

        fn test_inline_proof_via_macro() {
            proof_decl!{
                inline_proof!(0 => x, y);
                assert(x == 0);
            }
        }

    } => Ok(())
}

test_verify_one_file! {
    #[test] basic_test code! {
        use vstd::prelude::*;

        fn testfn() {

            let f =
            #[verus_spec(z: u64 =>
                requires y == 2
                ensures z == 2
            )]
            |y: u64| { y };

            proof!{
                assert(f.requires((2,)));
                assert(!f.ensures((2,),3));
            }

            let t = f(2);
            proof!{
                assert(t == 2);
            }
        }
    } => Ok(())
}

test_verify_one_file! {
    #[test] test_no_ret_fails code! {
        use vstd::prelude::*;

        fn testfn() {

            let f =
            #[verus_spec(
                requires y == 2
            )]
            |y: u64| {  };
        }
    } => Err(e) => assert_any_vir_error_msg(e, "Closure must have a return type")
}

test_verify_one_file! {
    #[test] test_no_ret_ok code! {
        use vstd::prelude::*;

        fn testfn() {

            let f1 =
            #[verus_spec(
                requires y == 2
            )]
            |y: u64| -> () {  };

            let f2 =
            #[verus_spec(ret: () =>
                requires y == 2
            )]
            |y: u64| {  };
        }
    } => Ok(())
}

test_verify_one_file! {
    #[test] test_const_fn_eval_via_proxy code!{
        use vstd::prelude::*;
        #[verus_spec(ret =>
            ensures ret == x
        )]
        #[allow(unused_variables)]
        pub const fn const_fn(x: u64) -> u64 {
            proof!{
                assert(true);
            }
            {
                proof!{assert(true);}
            }
            x
        }

        pub const X: u64 = const_fn(1);
    } => Ok(())
}

test_verify_one_file! {
    #[test] test_const_fn_with_ghost code!{
        use vstd::prelude::*;
        #[verus_spec(ret =>
            with Ghost(g): Ghost<u64>
        )]
        #[allow(unused_variables)]
        pub const fn const_fn(x: u64) -> u64 {
            proof!{
                assert(true);
            }
            {
                proof!{assert(true);}
            }
            x
        }

        #[verus_spec(
            with Ghost(g): Ghost<u64>
        )]
        pub const fn call_const_fn(x: u64) -> u64 {
            proof_with!{Ghost(g)}
            const_fn(x)
        }


        // external call to const_fn does not need ghost var.
        pub const X: u64 = const_fn(1);
    } => Ok(())
}