vstd/std_specs/
pin.rs

1use super::super::mut_ref::MutRef;
2use super::super::prelude::*;
3use core::pin::Pin;
4
5verus! {
6
7#[verifier::external_type_specification]
8#[verifier::external_body]
9#[verifier::accept_recursive_types(P)]
10pub struct ExPin<P>(Pin<P>);
11
12pub trait PinAdditionalSpecFns<'a, T: ?Sized> {
13    spec fn mut_ref(&self) -> MutRef<'a, T>;
14}
15
16impl<'a, T: ?Sized> PinAdditionalSpecFns<'a, T> for Pin<&'a mut T> {
17    uninterp spec fn mut_ref(&self) -> MutRef<'a, T>;
18}
19
20pub assume_specification<'a, T: Unpin + ?Sized>[ Pin::<&'a mut T>::get_mut ](
21    pin: Pin<&'a mut T>,
22) -> (r: &'a mut T)
23    ensures
24        MutRef::unpack(r) == pin.mut_ref(),
25        &*r == pin.mut_ref().current,
26        &*final(r) == pin.mut_ref().future.value(),
27;
28
29pub broadcast axiom fn axiom_pin_has_resolved<'a, T: ?Sized>(pin: Pin<&'a mut T>)
30    ensures
31        has_resolved::<Pin<&'a mut T>>(pin) ==> (#[trigger] pin.mut_ref()).future.value()
32            == pin.mut_ref().current,
33;
34
35pub broadcast group group_pin_axioms {
36    axiom_pin_has_resolved,
37}
38
39} // verus!
vstd/std_specs/pin.rs

vstd/std_specs/
pin.rs
