1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140

use super::prelude::*;

verus! {

#[verifier::external_type_specification]
#[verifier::external_body]
#[verifier::reject_recursive_types(Options)]
#[verifier::reject_recursive_types(ArgModes)]
#[verifier::reject_recursive_types(OutMode)]
#[verifier::reject_recursive_types(Args)]
#[verifier::accept_recursive_types(Output)]
pub struct ExFnProof<'a, Options, ArgModes, OutMode, Args, Output>(
    FnProof<'a, Options, ArgModes, OutMode, Args, Output>,
);

#[doc(hidden)]
#[verifier::external_type_specification]
#[verifier::external_body]
#[verifier::reject_recursive_types(USAGE)]
#[verifier::reject_recursive_types(ReqEns)]
#[verifier::reject_recursive_types(COPY)]
#[verifier::reject_recursive_types(SEND)]
#[verifier::reject_recursive_types(SYNC)]
pub struct ExFnProofOptions<
    const USAGE: u8,
    ReqEns,
    const COPY: u8,
    const SEND: u8,
    const SYNC: u8,
>(FOpts<USAGE, ReqEns, COPY, SEND, SYNC>);

#[verifier::external_trait_specification]
pub trait ExProofFnSpecification<Args, Output> {
    type ExternalTraitSpecificationFor: ProofFnReqEnsDef<Args, Output>;

    spec fn req(_args: Args) -> bool;

    spec fn ens(_args: Args, _output: Output) -> bool;
}

#[doc(hidden)]
#[verifier::external_type_specification]
#[verifier::external_body]
#[verifier::reject_recursive_types(R)]
pub struct ExFnProofOptionReqEns<R>(RqEn<R>);

#[doc(hidden)]
#[verifier::external_type_specification]
#[verifier::external_body]
pub struct ExFnProofOptionTracked(Trk);

#[verifier::external_trait_specification]
pub trait ExProofFnOnce {
    type ExternalTraitSpecificationFor: ProofFnOnce;
}

#[verifier::external_trait_specification]
pub trait ExProofFnMut: ProofFnOnce {
    type ExternalTraitSpecificationFor: ProofFnMut;
}

#[verifier::external_trait_specification]
pub trait ExProofFn: ProofFnMut {
    type ExternalTraitSpecificationFor: ProofFn;
}

#[verifier::external_trait_specification]
pub trait ExProofFnReqEnsAssoc {
    type ExternalTraitSpecificationFor: ProofFnReqEnsAssoc;

    type ReqEns;
}

#[verifier::external_trait_specification]
pub trait ExProofFnReqEns<R>: ProofFnReqEnsAssoc<ReqEns = R> {
    type ExternalTraitSpecificationFor: ProofFnReqEns<R>;
}

#[doc(hidden)]
pub broadcast axiom fn axiom_proof_fn_requires<
    F,
    ArgModes,
    OutMode,
    Args: core::marker::Tuple,
    Output,
>(f: FnProof<F, ArgModes, OutMode, Args, Output>, args: Args) where
    F: ProofFnOnce,
    F: ProofFnReqEnsAssoc,
    <F as ProofFnReqEnsAssoc>::ReqEns: ProofFnReqEnsDef<Args, Output>,

    ensures
        #[trigger] f.requires(args) <==> <F as ProofFnReqEnsAssoc>::ReqEns::req(args),
;

#[doc(hidden)]
pub broadcast axiom fn axiom_proof_fn_ensures<
    F,
    ArgModes,
    OutMode,
    Args: core::marker::Tuple,
    Output,
>(f: FnProof<F, ArgModes, OutMode, Args, Output>, args: Args, output: Output) where
    F: ProofFnOnce,
    F: ProofFnReqEnsAssoc,
    <F as ProofFnReqEnsAssoc>::ReqEns: ProofFnReqEnsDef<Args, Output>,

    ensures
        #[trigger] f.ensures(args, output) <==> <F as ProofFnReqEnsAssoc>::ReqEns::ens(
            args,
            output,
        ),
;

/// Retype a proof_fn, introducing ReqEns<R>
pub axiom fn proof_fn_as_req_ens<
    R: ProofFnReqEnsDef<Args, Output>,
    const USAGE: u8,
    ReqEns,
    const COPY: u8,
    const SEND: u8,
    const SYNC: u8,
    ArgModes,
    OutMode,
    Args: core::marker::Tuple,
    Output,
>(
    tracked f: FnProof<FOpts<USAGE, ReqEns, COPY, SEND, SYNC>, ArgModes, OutMode, Args, Output>,
) -> tracked FnProof<FOpts<USAGE, RqEn<R>, COPY, SEND, SYNC>, ArgModes, OutMode, Args, Output>
    requires
        forall|args: Args| #[trigger] R::req(args) ==> f.requires(args),
        forall|args: Args, output: Output|
            f.ensures(args, output) ==> #[trigger] R::ens(args, output),
;

pub broadcast group group_seq_axioms {
    axiom_proof_fn_requires,
    axiom_proof_fn_ensures,
}

} // verus!