vstd/std_specs/
control_flow.rs

Help
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;
28
29pub assume_specification<T>[ Option::<T>::branch ](option: Option<T>) -> (cf: ControlFlow<
30    <Option<T> as Try>::Residual,
31    <Option<T> as Try>::Output,
32>)
33    ensures
34        cf === match option {
35            Some(v) => ControlFlow::Continue(v),
36            None => ControlFlow::Break(None),
37        },
38;
39
40pub assume_specification<T>[ Option::<T>::from_residual ](option: Option<Infallible>) -> (option2:
41    Option<T>)
42    ensures
43        option.is_none(),
44        option2.is_none(),
45;
46
47pub uninterp spec fn spec_from<S, T>(value: T, ret: S) -> bool;
48
49pub broadcast proof fn spec_from_blanket_identity<T>(t: T, s: T)
50    ensures
51        #[trigger] spec_from::<T, T>(t, s) ==> t == s,
52{
53    admit();
54}
55
56pub assume_specification<T, E, F: From<E>>[ Result::<T, F>::from_residual ](
57    result: Result<Infallible, E>,
58) -> (result2: Result<T, F>)
59    ensures
60        match (result, result2) {
61            (Err(e), Err(e2)) => spec_from::<F, E>(e, e2),
62            _ => false,
63        },
64;
65
66pub broadcast group group_control_flow_axioms {
67    spec_from_blanket_identity,
68}
69
70} // verus!
vstd/std_specs/control_flow.rs

vstd/std_specs/
control_flow.rs
