vstd/
future.rs

1#![feature(rustc_attrs)]
2#![allow(unused_imports)]
3
4use super::prelude::*;
5#[cfg(verus_keep_ghost)]
6use super::std_specs::pin::PinAdditionalSpecFns;
7use core::future::*;
8use core::pin::Pin;
9use core::task::{Context, Poll};
10
11verus! {
12
13#[verifier::external_trait_specification]
14#[verifier::external_trait_extension(FutureSpec via FutureSpecImpl)]
15pub trait ExFuture {
16    type ExternalTraitSpecificationFor: core::future::Future;
17
18    type Output;
19
20    /// Whether this future obeys the specification below on `poll`,
21    /// so that awaiting it returns `view()`.
22    spec fn obeys_future_laws(&self) -> bool;
23
24    /// The value that awaiting this future will return.
25    #[verifier::prophetic]
26    spec fn view(&self) -> Self::Output;
27
28    fn poll(self: Pin<&mut Self>, cx: &mut Context<'_>) -> (r: Poll<Self::Output>)
29        ensures
30            ({
31                let m = self.mut_ref();
32                &&& m.future.value().obeys_future_laws() == m.current.obeys_future_laws()
33                &&& m.current.obeys_future_laws() ==> match r {
34                    Poll::Ready(v) => v == m.current.view(),
35                    Poll::Pending => m.future.value().view() == m.current.view(),
36                }
37            }),
38    ;
39}
40
41#[verifier::external_trait_specification]
42pub trait ExIntoFuture {
43    type ExternalTraitSpecificationFor: core::future::IntoFuture;
44
45    type Output;
46
47    type IntoFuture: Future<Output = Self::Output>;
48
49    fn into_future(self) -> Self::IntoFuture;
50}
51
52pub assume_specification<F: Future>[ <F as IntoFuture>::into_future ](f: F) -> (r:
53    <F as IntoFuture>::IntoFuture)
54    ensures
55        r == f,
56;
57
58pub trait FutureAdditionalSpecFns<T>: Future<Output = T> {
59    #[verifier::prophetic]
60    spec fn awaited(&self) -> bool;
61}
62
63impl<V, T: Future<Output = V>> FutureAdditionalSpecFns<V> for T {
64    #[verifier::prophetic]
65    uninterp spec fn awaited(&self) -> bool;
66}
67
68// Do not call this function. Call the regular Rust `await` keyword instead.
69#[verifier::external_body]
70fn exec_await<F: Future>(
71    #[allow(unused_variables)]
72    future: F,
73) -> (ret: F::Output)
74    ensures
75        future.awaited() == true,
76        future.obeys_future_laws() ==> ret == future@,
77    opens_invariants any
78{
79    unimplemented!()
80}
81
82} // verus!
vstd/future.rs

vstd/
future.rs
