vstd/
future.rs

1#![feature(rustc_attrs)]
2#![allow(unused_imports)]
3
4use super::prelude::*;
5use core::future::*;
6verus! {
7
8#[verifier::external_trait_specification]
9pub trait ExFuture {
10    type ExternalTraitSpecificationFor: core::future::Future;
11
12    type Output;
13}
14
15pub trait FutureAdditionalSpecFns<T>: Future<Output = T> {
16    #[verifier::prophetic]
17    spec fn view(&self) -> T;
18
19    #[verifier::prophetic]
20    spec fn awaited(&self) -> bool;
21}
22
23impl<V, T: Future<Output = V>> FutureAdditionalSpecFns<V> for T {
24    #[verifier::prophetic]
25    uninterp spec fn view(&self) -> V;
26
27    #[verifier::prophetic]
28    uninterp spec fn awaited(&self) -> bool;
29}
30
31// Do not call this function. Call the regular Rust `await` keyword instead.
32#[verifier::external_body]
33fn exec_await<F: Future>(
34    #[allow(unused_variables)]
35    future: F,
36) -> (ret: F::Output)
37    ensures
38        future.awaited() == true,
39        ret == future@,
40    opens_invariants any
41{
42    unimplemented!()
43}
44
45} // verus!
vstd/future.rs

vstd/
future.rs
