vstd/
function.rs

Help
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)]
24pub struct ExFnProofOptions<
25    const USAGE: u8,
26    ReqEns,
27    const COPY: u8,
28    const SEND: u8,
29    const SYNC: u8,
30>(FOpts<USAGE, ReqEns, COPY, SEND, SYNC>);
31
32#[verifier::external_trait_specification]
33pub trait ExProofFnSpecification<Args, Output> {
34    type ExternalTraitSpecificationFor: ProofFnReqEnsDef<Args, Output>;
35
36    spec fn req(_args: Args) -> bool;
37
38    spec fn ens(_args: Args, _output: Output) -> bool;
39}
40
41#[doc(hidden)]
42#[verifier::external_type_specification]
43#[verifier::external_body]
44#[verifier::reject_recursive_types(R)]
45pub struct ExFnProofOptionReqEns<R>(RqEn<R>);
46
47#[doc(hidden)]
48#[verifier::external_type_specification]
49#[verifier::external_body]
50pub struct ExFnProofOptionTracked(Trk);
51
52#[verifier::external_trait_specification]
53pub trait ExProofFnOnce {
54    type ExternalTraitSpecificationFor: ProofFnOnce;
55}
56
57#[verifier::external_trait_specification]
58pub trait ExProofFnMut: ProofFnOnce {
59    type ExternalTraitSpecificationFor: ProofFnMut;
60}
61
62#[verifier::external_trait_specification]
63pub trait ExProofFn: ProofFnMut {
64    type ExternalTraitSpecificationFor: ProofFn;
65}
66
67#[verifier::external_trait_specification]
68pub trait ExProofFnReqEnsAssoc {
69    type ExternalTraitSpecificationFor: ProofFnReqEnsAssoc;
70
71    type ReqEns;
72}
73
74#[verifier::external_trait_specification]
75pub trait ExProofFnReqEns<R>: ProofFnReqEnsAssoc<ReqEns = R> {
76    type ExternalTraitSpecificationFor: ProofFnReqEns<R>;
77}
78
79#[doc(hidden)]
80pub broadcast axiom fn axiom_proof_fn_requires<
81    F,
82    ArgModes,
83    OutMode,
84    Args: core::marker::Tuple,
85    Output,
86>(f: FnProof<F, ArgModes, OutMode, Args, Output>, args: Args) where
87    F: ProofFnOnce,
88    F: ProofFnReqEnsAssoc,
89    <F as ProofFnReqEnsAssoc>::ReqEns: ProofFnReqEnsDef<Args, Output>,
90
91    ensures
92        #[trigger] f.requires(args) <==> <F as ProofFnReqEnsAssoc>::ReqEns::req(args),
93;
94
95#[doc(hidden)]
96pub broadcast axiom fn axiom_proof_fn_ensures<
97    F,
98    ArgModes,
99    OutMode,
100    Args: core::marker::Tuple,
101    Output,
102>(f: FnProof<F, ArgModes, OutMode, Args, Output>, args: Args, output: Output) where
103    F: ProofFnOnce,
104    F: ProofFnReqEnsAssoc,
105    <F as ProofFnReqEnsAssoc>::ReqEns: ProofFnReqEnsDef<Args, Output>,
106
107    ensures
108        #[trigger] f.ensures(args, output) <==> <F as ProofFnReqEnsAssoc>::ReqEns::ens(
109            args,
110            output,
111        ),
112;
113
114/// Retype a proof_fn, introducing `ReqEns<R>`
115pub axiom fn proof_fn_as_req_ens<
116    R: ProofFnReqEnsDef<Args, Output>,
117    const USAGE: u8,
118    ReqEns,
119    const COPY: u8,
120    const SEND: u8,
121    const SYNC: u8,
122    ArgModes,
123    OutMode,
124    Args: core::marker::Tuple,
125    Output,
126>(
127    tracked f: FnProof<FOpts<USAGE, ReqEns, COPY, SEND, SYNC>, ArgModes, OutMode, Args, Output>,
128) -> tracked FnProof<FOpts<USAGE, RqEn<R>, COPY, SEND, SYNC>, ArgModes, OutMode, Args, Output>
129    requires
130        forall|args: Args| #[trigger] R::req(args) ==> f.requires(args),
131        forall|args: Args, output: Output|
132            f.ensures(args, output) ==> #[trigger] R::ens(args, output),
133;
134
135pub broadcast group group_function_axioms {
136    axiom_proof_fn_requires,
137    axiom_proof_fn_ensures,
138}
139
140} // verus!
vstd/function.rs

vstd/
function.rs
