vstd/
function.rs

1use super::prelude::*;
2
3verus! {
4
5#[verifier::external_type_specification]
6#[verifier::external_body]
7#[verifier::reject_recursive_types(Options)]
8#[verifier::reject_recursive_types(ArgModes)]
9#[verifier::reject_recursive_types(OutMode)]
10#[verifier::reject_recursive_types(Args)]
11#[verifier::accept_recursive_types(Output)]
12pub struct ExFnProof<'a, Options, ArgModes, OutMode, Args, Output>(
13    FnProof<'a, Options, ArgModes, OutMode, Args, Output>,
14);
15
16#[doc(hidden)]
17#[verifier::external_type_specification]
18#[verifier::external_body]
19#[verifier::reject_recursive_types(USAGE)]
20#[verifier::reject_recursive_types(ReqEns)]
21#[verifier::reject_recursive_types(COPY)]
22#[verifier::reject_recursive_types(SEND)]
23#[verifier::reject_recursive_types(SYNC)]
24#[verifier::reject_recursive_types(OPENS)]
25pub struct ExFnProofOptions<
26    const USAGE: u8,
27    ReqEns,
28    const COPY: u8,
29    const SEND: u8,
30    const SYNC: u8,
31    const OPENS: u8,
32>(FOpts<USAGE, ReqEns, COPY, SEND, SYNC, OPENS>);
33
34#[verifier::external_trait_specification]
35pub trait ExProofFnSpecification<Args, Output> {
36    type ExternalTraitSpecificationFor: ProofFnReqEnsDef<Args, Output>;
37
38    spec fn req(_args: Args) -> bool;
39
40    spec fn ens(_args: Args, _output: Output) -> bool;
41}
42
43#[doc(hidden)]
44#[verifier::external_type_specification]
45#[verifier::external_body]
46#[verifier::reject_recursive_types(R)]
47pub struct ExFnProofOptionReqEns<R>(RqEn<R>);
48
49#[doc(hidden)]
50#[verifier::external_type_specification]
51#[verifier::external_body]
52pub struct ExFnProofOptionTracked(Trk);
53
54#[verifier::external_trait_specification]
55pub trait ExProofFnNoOpens {
56    type ExternalTraitSpecificationFor: ProofFnNoOpens;
57}
58
59#[verifier::external_trait_specification]
60pub trait ExProofFnOnceOpens {
61    type ExternalTraitSpecificationFor: ProofFnOnceOpens;
62}
63
64#[verifier::external_trait_specification]
65pub trait ExProofFnMutOpens: ProofFnOnceOpens {
66    type ExternalTraitSpecificationFor: ProofFnMutOpens;
67}
68
69#[verifier::external_trait_specification]
70pub trait ExProofFnOpens: ProofFnMutOpens {
71    type ExternalTraitSpecificationFor: ProofFnOpens;
72}
73
74#[verifier::external_trait_specification]
75pub trait ExProofFnOnce: ProofFnOnceOpens + ProofFnNoOpens {
76    type ExternalTraitSpecificationFor: ProofFnOnce;
77}
78
79#[verifier::external_trait_specification]
80pub trait ExProofFnMut: ProofFnOnce + ProofFnMutOpens + ProofFnNoOpens {
81    type ExternalTraitSpecificationFor: ProofFnMut;
82}
83
84#[verifier::external_trait_specification]
85pub trait ExProofFn: ProofFnMut + ProofFnOpens + ProofFnNoOpens {
86    type ExternalTraitSpecificationFor: ProofFn;
87}
88
89#[verifier::external_trait_specification]
90pub trait ExProofFnReqEnsAssoc {
91    type ExternalTraitSpecificationFor: ProofFnReqEnsAssoc;
92
93    type ReqEns;
94}
95
96#[verifier::external_trait_specification]
97pub trait ExProofFnReqEns<R>: ProofFnReqEnsAssoc<ReqEns = R> {
98    type ExternalTraitSpecificationFor: ProofFnReqEns<R>;
99}
100
101#[doc(hidden)]
102pub broadcast axiom fn axiom_proof_fn_requires<
103    F,
104    ArgModes,
105    OutMode,
106    Args: core::marker::Tuple,
107    Output,
108>(f: FnProof<F, ArgModes, OutMode, Args, Output>, args: Args) where
109    F: ProofFnOnceOpens,
110    F: ProofFnReqEnsAssoc,
111    <F as ProofFnReqEnsAssoc>::ReqEns: ProofFnReqEnsDef<Args, Output>,
112
113    ensures
114        #[trigger] f.requires(args) <==> <F as ProofFnReqEnsAssoc>::ReqEns::req(args),
115;
116
117#[doc(hidden)]
118pub broadcast axiom fn axiom_proof_fn_ensures<
119    F,
120    ArgModes,
121    OutMode,
122    Args: core::marker::Tuple,
123    Output,
124>(f: FnProof<F, ArgModes, OutMode, Args, Output>, args: Args, output: Output) where
125    F: ProofFnOnceOpens,
126    F: ProofFnReqEnsAssoc,
127    <F as ProofFnReqEnsAssoc>::ReqEns: ProofFnReqEnsDef<Args, Output>,
128
129    ensures
130        #[trigger] f.ensures(args, output) <==> <F as ProofFnReqEnsAssoc>::ReqEns::ens(
131            args,
132            output,
133        ),
134;
135
136#[doc(hidden)]
137pub broadcast axiom fn axiom_proof_fn_no_opens_invariants<
138    F,
139    ArgModes,
140    OutMode,
141    Args: core::marker::Tuple,
142    Output,
143>(f: FnProof<F, ArgModes, OutMode, Args, Output>, args: Args) where
144    F: ProofFnOnceOpens,
145    F: ProofFnNoOpens,
146
147    ensures
148        #[trigger] call_opens_invariants::<_, _, ISet<int>>(f, args) == ISet::empty(),
149;
150
151/// Retype a proof_fn, introducing `ReqEns<R>`
152pub axiom fn proof_fn_as_req_ens<
153    R: ProofFnReqEnsDef<Args, Output>,
154    const USAGE: u8,
155    ReqEns,
156    const COPY: u8,
157    const SEND: u8,
158    const SYNC: u8,
159    const OPENS: u8,
160    ArgModes,
161    OutMode,
162    Args: core::marker::Tuple,
163    Output,
164>(
165    tracked f: FnProof<
166        FOpts<USAGE, ReqEns, COPY, SEND, SYNC, OPENS>,
167        ArgModes,
168        OutMode,
169        Args,
170        Output,
171    >,
172) -> tracked FnProof<
173    FOpts<USAGE, RqEn<R>, COPY, SEND, SYNC, OPENS>,
174    ArgModes,
175    OutMode,
176    Args,
177    Output,
178>
179    requires
180        forall|args: Args| #[trigger] R::req(args) ==> f.requires(args),
181        forall|args: Args, output: Output|
182            f.ensures(args, output) ==> #[trigger] R::ens(args, output),
183;
184
185pub broadcast axiom fn axiom_fn_mut_call_requires<Args: core::marker::Tuple, F: FnMut<Args>>(
186    f: &mut F,
187    args: Args,
188)
189    requires
190        call_requires::<Args, F>(mut_ref_current(f), args),
191    ensures
192        #[trigger] call_requires::<Args, &mut F>(f, args),
193;
194
195// The output contract concerns the callable's current value. The reference may
196// outlive the call and be used to replace the callable, so its future is unconstrained.
197pub broadcast axiom fn axiom_fn_mut_call_ensures<Args: core::marker::Tuple, F: FnMut<Args>>(
198    f: &mut F,
199    args: Args,
200    output: F::Output,
201)
202    requires
203        #[trigger] call_ensures::<Args, &mut F>(f, args, output),
204    ensures
205        call_ensures::<Args, F>(mut_ref_current(f), args, output),
206;
207
208pub broadcast axiom fn axiom_fn_mut_call_opens_invariants<
209    Args: core::marker::Tuple,
210    F: FnMut<Args>,
211    I,
212>(f: &mut F, args: Args)
213    ensures
214        #[trigger] call_opens_invariants::<Args, &mut F, I>(f, args) == call_opens_invariants::<
215            Args,
216            F,
217            I,
218        >(mut_ref_current(f), args),
219;
220
221pub broadcast group group_function_axioms {
222    axiom_proof_fn_requires,
223    axiom_proof_fn_ensures,
224    axiom_proof_fn_no_opens_invariants,
225    axiom_fn_mut_call_requires,
226    axiom_fn_mut_call_ensures,
227    axiom_fn_mut_call_opens_invariants,
228}
229
230} // verus!
vstd/function.rs

vstd/
function.rs
