verdict_parser/common/
wrapped.rs

1use super::*;
2use std::marker::PhantomData;
3use vstd::prelude::*;
4
5verus! {
6
7/// Sometimes it is useful to wrap an existing combinator
8/// within a Mapped combinator so that the SpecFrom trait
9/// works better
10pub type Wrapped<C> = Mapped<C, IdentityMapper<C>>;
11
12pub open spec fn spec_new_wrapped<C: Combinator>(c: C) -> Wrapped<C> where
13    C::V: SecureSpecCombinator<SpecResult = <C::Owned as View>::V>,
14{
15    Mapped {
16        inner: c,
17        mapper: IdentityMapper(PhantomData),
18    }
19}
20
21pub fn new_wrapped<C: Combinator>(c: C) -> Wrapped<C> where
22    C::V: SecureSpecCombinator<SpecResult = <C::Owned as View>::V>,
23{
24    Mapped {
25        inner: c,
26        mapper: IdentityMapper::new(),
27    }
28}
29
30/// An identity mapper that does not change the parsed object
31/// Used in situations when we need prove U: DisjointFrom<Mapped<...>>
32/// in which case we can wrap U in Mapped and use existing impls
33#[derive(Debug)]
34pub struct IdentityMapper<C>(pub PhantomData<C>);
35
36impl<C: View> View for IdentityMapper<C> {
37    type V = IdentityMapper<C::V>;
38
39    open spec fn view(&self) -> Self::V {
40        IdentityMapper(PhantomData)
41    }
42}
43
44impl<C> IdentityMapper<C> {
45    pub fn new() -> Self {
46        IdentityMapper(PhantomData)
47    }
48}
49
50impl<C: SpecCombinator> SpecIso for IdentityMapper<C> {
51    type Src = C::SpecResult;
52    type Dst = C::SpecResult;
53
54    proof fn spec_iso(s: Self::Src) {}
55    proof fn spec_iso_rev(s: Self::Dst) {}
56}
57
58impl<C: Combinator> Iso for IdentityMapper<C> where
59    C::V: SecureSpecCombinator<SpecResult = <C::Owned as View>::V>,
60{
61    type Src<'a> = C::Result<'a>;
62    type Dst<'a> = C::Result<'a>;
63
64    type SrcOwned = C::Owned;
65    type DstOwned = C::Owned;
66}
67
68/// Wrap a non-parametric combinator in a new unit struct
69/// e.g.
70/// wrap_combinator! {
71///     struct AlgorithmIdentifier: AlgorithmIdentifierInner =
72///         Mapped {
73///             inner: ASN1(ExplicitTag(TagValue {
74///                 class: TagClass::Universal,
75///                 form: TagForm::Constructed,
76///                 num: 0x10,
77///             }, (ASN1(ObjectIdentifier), Tail))),
78///             mapper: AlgorithmIdentifierMapper,
79///         }
80/// }
81///
82/// TODO: Due to a Verus issue, everything here is unproved
83/// NOTE: $inner_expr is used both in exec and spec mode
84#[allow(unused_macros)]
85macro_rules! wrap_combinator {
86    // NOTE: use the other alternative to reduce type checking time
87    ($vis:vis struct $name:ident $({ $($field_vis:vis $field_name:ident: $field_type:ty),* $(,)? })?: $inner_type:ty = $inner_expr:expr ;) => {
88        wrap_combinator! {
89           $vis struct $name $({ $($field_vis $field_name: $field_type),* })?: $inner_type =>
90                spec <<$inner_type as View>::V as SpecCombinator>::SpecResult,
91                exec<'a> <$inner_type as Combinator>::Result<'a>,
92                owned <$inner_type as Combinator>::Owned,
93            = $inner_expr;
94        }
95    };
96
97    ($vis:vis struct $name:ident: $inner_type:ty =>
98        spec $spec_result:ty,
99        exec<$lt:lifetime> $result:ty,
100        owned $owned:ty $(,)?
101        = $inner_expr:expr ;) => {
102        ::builtin_macros::verus! {
103            #[derive(Debug, View)]
104            $vis struct $name;
105
106            wrap_combinator_impls! {
107                $vis struct $name {} : $inner_type =>
108                    spec $spec_result,
109                    exec<$lt> $result,
110                    owned $owned
111                = $inner_expr;
112            }
113        }
114    };
115
116    ($vis:vis struct $name:ident { $($field_vis:vis $field_name:ident: $field_type:ty),* $(,)? } : $inner_type:ty =>
117        spec $spec_result:ty,
118        exec<$lt:lifetime> $result:ty,
119        owned $owned:ty $(,)?
120        = $inner_expr:expr ;) => {
121        ::builtin_macros::verus! {
122            #[derive(Debug, View)]
123            $vis struct $name { $($field_vis $field_name: $field_type),* }
124
125            wrap_combinator_impls! {
126                $vis struct $name { $($field_vis $field_name: $field_type),* } : $inner_type =>
127                    spec $spec_result,
128                    exec<$lt> $result,
129                    owned $owned
130                = $inner_expr;
131            }
132        }
133    };
134}
135pub(crate) use wrap_combinator;
136
137#[allow(unused_macros)]
138macro_rules! wrap_combinator_impls {
139    ($vis:vis struct $name:ident { $($field_vis:vis $field_name:ident: $field_type:ty),* } : $inner_type:ty =>
140        spec $spec_result:ty,
141        exec<$lt:lifetime> $result:ty,
142        owned $owned:ty $(,)?
143        = $inner_expr:expr ;) => {
144        ::builtin_macros::verus! {
145            impl $name {
146                /// Due to a Verus/SMT instability issue,
147                /// specifying the actual definitions of, e.g., spec_parse
148                /// results in proof failures in a large number of irrelevant places
149                ///
150                /// So instead, we just separately check a number of sufficient conditions
151                /// for the wrapped combinator in this function
152                ///
153                /// TODO: remove this once the Verus issue is fixed
154                #[allow(dead_code)]
155                fn check_valid_inner_combinator() {
156                    // Type check
157                    #[allow(unused_variables)]
158                    let c: $inner_type = $inner_expr;
159
160                    // For future compatibility, check that $inner_expr is also a valid spec expr
161                    let ghost _ = $inner_expr.view();
162
163                    // Check that $inner_expr is a Combinator
164                    let _ = $inner_expr.length();
165
166                    // The inner combinator has to be prefix secure
167                    assert(<<$inner_type as View>::V as SecureSpecCombinator>::is_prefix_secure());
168
169                    // Check that parse_requires and serialize_requires are satisfied
170                    assert(c.parse_requires());
171                    assert(c.serialize_requires());
172                }
173            }
174
175            impl SpecCombinator for $name {
176                type SpecResult = $spec_result;
177
178                // $inner_expr.view().spec_parse(s)
179                uninterp spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()>;
180
181                // $inner_expr.view().spec_parse_wf(s)
182                #[verifier::external_body]
183                proof fn spec_parse_wf(&self, s: Seq<u8>) {}
184
185                // $inner_expr.view().spec_serialize(v)
186                uninterp spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()>;
187            }
188
189            impl SecureSpecCombinator for $name {
190                // $inner_type::is_prefix_secure()
191                open spec fn is_prefix_secure() -> bool {
192                    true // sound since it's checked in check_valid_inner_combinator
193                }
194
195                #[verifier::external_body]
196                proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult) {
197                    // $inner_expr.view().theorem_serialize_parse_roundtrip(v)
198                }
199
200                #[verifier::external_body]
201                proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
202                    // $inner_expr.view().theorem_parse_serialize_roundtrip(buf)
203                }
204
205                #[verifier::external_body]
206                proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
207                    // $inner_expr.view().lemma_prefix_secure(s1, s2)
208                }
209            }
210
211            impl Combinator for $name {
212                type Result<$lt> = $result;
213                type Owned =  $owned;
214
215                uninterp spec fn spec_length(&self) -> Option<usize>;
216
217                #[verifier::external_body]
218                fn length(&self) -> Option<usize> {
219                    $(let $field_name: $field_type = self.$field_name;)*
220                    $inner_expr.length()
221                }
222
223                open spec fn parse_requires(&self) -> bool {
224                    true // sound since it's checked in check_valid_inner_combinator
225                }
226
227                #[verifier::external_body]
228                #[inline(always)]
229                #[allow(unexpected_cfgs)]
230                fn parse<'a>(&self, s: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) {
231                    $(let $field_name: $field_type = self.$field_name;)*
232                    let res = $inner_expr.parse(s);
233                    #[cfg(feature = "trace")] {
234                        use verdict_polyfill::*;
235                        eprintln_join!("[", stringify!($name), "] ", format_dbg(&res));
236                    }
237                    res
238                }
239
240                open spec fn serialize_requires(&self) -> bool {
241                    true // sound since it's checked in check_valid_inner_combinator
242                }
243
244                #[verifier::external_body]
245                #[inline(always)]
246                fn serialize(&self, v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> (res: Result<usize, SerializeError>) {
247                    $(let $field_name: $field_type = self.$field_name;)*
248                    $inner_expr.serialize(v, data, pos)
249                }
250            }
251        }
252    };
253}
254pub(crate) use wrap_combinator_impls;
255
256}
verdict_parser/common/wrapped.rs

verdict_parser/common/
wrapped.rs
