vstd 0.0.0-2026-04-20-1748

Verus Standard Library: Useful specifications and lemmas for verifying Rust code
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42

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

use super::prelude::*;
use core::future::*;
verus! {

#[verifier::external_trait_specification]
pub trait ExFuture {
    type ExternalTraitSpecificationFor: core::future::Future;

    type Output;
}

pub trait FutureAdditionalSpecFns<T>: Future<Output = T> {
    #[verifier::prophetic]
    spec fn view(&self) -> T;

    #[verifier::prophetic]
    spec fn awaited(&self) -> bool;
}

impl<V, T: Future<Output = V>> FutureAdditionalSpecFns<V> for T {
    #[verifier::prophetic]
    uninterp spec fn view(&self) -> V;

    #[verifier::prophetic]
    uninterp spec fn awaited(&self) -> bool;
}

// Do not call this function. Call the regular Rust `await` keyword instead.
#[verifier::external_body]
fn exec_await<F: Future>(future: F) -> (ret: F::Output)
    ensures
        future.awaited() == true,
        ret == future@,
    opens_invariants any
{
    unimplemented!()
}

} // verus!