vstd/std_specs/
control_flow.rs

1use super::super::prelude::*;
2use core::convert::Infallible;
3use core::ops::ControlFlow;
4use core::ops::FromResidual;
5use core::ops::Try;
6
7verus! {
8
9#[verifier::external_type_specification]
10#[verifier::accept_recursive_types(B)]
11#[verifier::reject_recursive_types_in_ground_variants(C)]
12pub struct ExControlFlow<B, C>(ControlFlow<B, C>);
13
14#[verifier::external_type_specification]
15#[verifier::external_body]
16pub struct ExInfallible(Infallible);
17
18pub assume_specification<T, E>[ Result::<T, E>::branch ](result: Result<T, E>) -> (cf: ControlFlow<
19    <Result<T, E> as Try>::Residual,
20    <Result<T, E> as Try>::Output,
21>)
22    ensures
23        cf == match result {
24            Ok(v) => ControlFlow::Continue(v),
25            Err(e) => ControlFlow::Break(Err(e)),
26        },
27    no_unwind
28;
29
30pub assume_specification<T>[ Option::<T>::branch ](option: Option<T>) -> (cf: ControlFlow<
31    <Option<T> as Try>::Residual,
32    <Option<T> as Try>::Output,
33>)
34    ensures
35        cf == match option {
36            Some(v) => ControlFlow::Continue(v),
37            None => ControlFlow::Break(None),
38        },
39    no_unwind
40;
41
42pub assume_specification<T>[ Option::<T>::from_residual ](option: Option<Infallible>) -> (option2:
43    Option<T>)
44    ensures
45        option.is_none(),
46        option2.is_none(),
47    no_unwind
48;
49
50pub uninterp spec fn spec_from<S, T>(value: T, ret: S) -> bool;
51
52pub broadcast proof fn spec_from_blanket_identity<T>(t: T, s: T)
53    ensures
54        #[trigger] spec_from::<T, T>(t, s) ==> t == s,
55{
56    admit();
57}
58
59pub assume_specification<T, E, F: From<E>>[ Result::<T, F>::from_residual ](
60    result: Result<Infallible, E>,
61) -> (result2: Result<T, F>)
62    ensures
63        match (result, result2) {
64            (Err(e), Err(e2)) => spec_from::<F, E>(e, e2),
65            _ => false,
66        },
67    no_unwind
68;
69
70pub broadcast group group_control_flow_axioms {
71    spec_from_blanket_identity,
72}
73
74} // verus!
vstd/std_specs/control_flow.rs

vstd/std_specs/
control_flow.rs
