verdict_parser/x509/
macros.rs

1use vstd::prelude::*;
2
3verus! {
4
5/// Generate a combinator for an ASN.1 SEQUENCE (with default or optional fields)
6///
7/// For example
8/// ```ignore
9/// asn1_sequence! {
10///     sequence Test {
11///         typ: ASN1<ObjectIdentifier> = ASN1(ObjectIdentifier),
12///         value: DirectoryString = DirectoryString,
13///     }
14/// }
15/// ```
16///
17/// NOTE: all sub-combinators have to be prefix secure (for Pair to work)
18/// NOTE: we have the restriction that an OrdChoice combinator cannot
19/// be following an optional or default field.
20#[allow(unused_macros)]
21#[macro_export]
22macro_rules! asn1_sequence {
23    // This assumes the view of $field_combinator is also $field_combinator
24    (
25        seq $name:ident {
26            $(
27                $(#[$modifier:ident $(($modifier_arg:expr))?])? $field_name:ident : $field_combinator_type:ty = $field_combinator:expr
28            ),*
29
30            $(,)?
31        }
32    ) => {
33        crate::x509::macros::asn1_sequence! {
34            seq $name {
35                $($(#[$modifier $(($modifier_arg))?])? $field_name : $field_combinator_type = $field_combinator, spec $field_combinator),*
36            }
37        }
38    };
39
40    (
41        seq $name:ident {
42            $(
43                $(#[$modifier:ident $(($modifier_arg:expr))?])? $field_name:ident : $field_combinator_type:ty = $field_combinator:expr, spec $spec_field_combinator:expr
44            ),*
45
46            $(,)?
47        }
48    ) => {
49        ::paste::paste! {
50            ::builtin_macros::verus! {
51                // Only export the combinator, and the spec/normal/owned result types
52                pub use [< internal_ $name >]::$name;
53                pub use [< internal_ $name >]::SpecValue as [< Spec $name Value >];
54                pub use [< internal_ $name >]::Value as [< $name Value >];
55                pub use [< internal_ $name >]::ValueOwned as [< $name ValueOwned >];
56
57                mod [< internal_ $name >] {
58                    // Since snake-case field names are directly used as type parameters
59                    #![allow(non_camel_case_types)]
60                    #![allow(non_snake_case)]
61
62                    use super::*;
63                    use crate::x509::macros::*;
64                    use crate::asn1::*;
65                    use crate::common::*;
66
67                    // Wrap the final combinator in a unit struct called $name
68                    wrap_combinator! {
69                        pub struct $name: Mapped<LengthWrapped<
70                                gen_inner_combinator_type!($(($($modifier $(($modifier_arg))?)?, $field_combinator_type));*)
71                            >, Mapper> =>
72                            spec SpecValue,
73                            exec<'a> Value<'a>,
74                            owned ValueOwned,
75                        = Mapped {
76                                inner: LengthWrapped(gen_inner_combinator!($(($($modifier $(($modifier_arg))?)?, $field_combinator));*)),
77                                mapper: Mapper,
78                            };
79                    }
80
81                    asn1_tagged!($name, tag_of!(SEQUENCE));
82
83                    // Add an indirection here since we can't put it inside the struct definition
84                    $(
85                        pub type [<FieldType_ $field_name>]<$field_name> = gen_field_poly_type!(($($modifier $(($modifier_arg))?)?, $field_name));
86                    )*
87
88                    // Mapper from the inner nested pair type to a struct
89                    mapper! {
90                        pub struct Mapper;
91
92                        for <$($field_name),*>
93                        from FromType where
94                            type FromType<$($field_name),*> = gen_inner_combinator_poly_result_type!($(($($modifier $(($modifier_arg))?)?, $field_name));*);
95                        to PolyType where
96                            #[derive(Eq, PartialEq)]
97                            pub struct PolyType<$($field_name),*> {
98                                $(pub $field_name: [<FieldType_ $field_name>]<$field_name>,)*
99                            }
100
101                        spec SpecValue with <$(<<$field_combinator_type as View>::V as SpecCombinator>::SpecResult),*>;
102                        exec Value<'a> with <$(<$field_combinator_type as Combinator>::Result<'a>),*>;
103                        owned ValueOwned with <$(<$field_combinator_type as Combinator>::Owned),*>;
104
105                        forward(x) {
106                            gen_forward_body!(x; $(($($modifier $(($modifier_arg))?)?, $field_name)),*);
107                            PolyType { $($field_name),* }
108                        } by {
109                            assert(get_end_field!(x; $(($($modifier $(($modifier_arg))?)?, $field_name)),*) == EndValue);
110                        }
111
112                        backward(y) {
113                            gen_backward_body!(y; $(($($modifier $(($modifier_arg))?)?, $field_name)),*)
114                        }
115                    }
116                }
117            }
118        }
119    };
120}
121pub use asn1_sequence;
122
123/// gen_inner_combinator_type!((optional, type1); (, type2); (default(v), type3))
124#[allow(unused_macros)]
125#[macro_export]
126macro_rules! gen_inner_combinator_type {
127    () => { End };
128
129    ((, $first:ty) $(; ($($modifier:ident $(($modifier_arg:expr))?)?, $rest:ty))*) => {
130        Pair<$first, gen_inner_combinator_type!($(($($modifier $(($modifier_arg))?)?, $rest));*)>
131    };
132
133    ((optional, $first:ty) $(; ($($modifier:ident $(($modifier_arg:expr))?)?, $rest:ty))*) => {
134        Optional<$first, gen_inner_combinator_type!($(($($modifier $(($modifier_arg))?)?, $rest));*)>
135    };
136
137    ((default($_:expr), $first:ty) $(; ($($modifier:ident $(($modifier_arg:expr))?)?, $rest:ty))*) => {
138        Default<<$first as Combinator>::Owned, $first, gen_inner_combinator_type!($(($($modifier $(($modifier_arg))?)?, $rest));*)>
139    };
140
141    ((tail, $first:ty)) => {
142        $first
143    };
144}
145pub use gen_inner_combinator_type;
146
147#[allow(unused_macros)]
148#[macro_export]
149macro_rules! gen_inner_combinator {
150    () => { End };
151
152    ((, $first:expr) $(; ($($modifier:ident $(($modifier_arg:expr))?)?, $rest:expr))*) => {
153        Pair($first, gen_inner_combinator!($(($($modifier $(($modifier_arg))?)?, $rest));*))
154    };
155
156    ((optional, $first:expr) $(; ($($modifier:ident $(($modifier_arg:expr))?)?, $rest:expr))*) => {
157        Optional($first, gen_inner_combinator!($(($($modifier $(($modifier_arg))?)?, $rest));*))
158    };
159
160    ((default($default:expr), $first:expr) $(; ($($modifier:ident $(($modifier_arg:expr))?)?, $rest:expr))*) => {
161        Default($default, $first, gen_inner_combinator!($(($($modifier $(($modifier_arg))?)?, $rest));*))
162    };
163
164    ((tail, $first:expr)) => {
165        $first
166    };
167}
168pub use gen_inner_combinator;
169
170#[allow(unused_macros)]
171#[macro_export]
172macro_rules! gen_inner_combinator_poly_result_type {
173    () => { EndValue };
174
175    ((, $first:ident) $(; ($($modifier:ident $(($modifier_arg:expr))?)?, $rest:ident))*) => {
176        PairValue<$first, gen_inner_combinator_poly_result_type!($(($($modifier $(($modifier_arg))?)?, $rest));*)>
177    };
178
179    ((optional, $first:ident) $(; ($($modifier:ident $(($modifier_arg:expr))?)?, $rest:ident))*) => {
180        PairValue<OptionDeep<$first>, gen_inner_combinator_poly_result_type!($(($($modifier $(($modifier_arg))?)?, $rest));*)>
181    };
182
183    ((default($_:expr), $first:ident) $(; ($($modifier:ident $(($modifier_arg:expr))?)?, $rest:ident))*) => {
184        PairValue<$first, gen_inner_combinator_poly_result_type!($(($($modifier $(($modifier_arg))?)?, $rest));*)>
185    };
186
187    ((tail, $first:ident)) => {
188        $first
189    };
190}
191pub use gen_inner_combinator_poly_result_type;
192
193#[allow(unused_macros)]
194#[macro_export]
195macro_rules! gen_forward_body {
196    ($prev_sel:expr ;) => {};
197
198    // Special case: if the last field is marked with tail, we use it directly without doing Pair(last combinator, End)
199    ($prev_sel:expr ; (tail, $first:ident)) => {
200        let $first = $prev_sel;
201    };
202
203    ($prev_sel:expr ; ($($modifier:ident $(($modifier_arg:expr))?)?, $first:ident) $(, ($($rest_modifier:ident $(($rest_modifier_arg:expr))?)?, $rest:ident))*) => {
204        let $first = $prev_sel.0;
205        gen_forward_body!($prev_sel.1 ; $(($($rest_modifier $(($rest_modifier_arg))?)?, $rest)),*)
206    };
207}
208pub use gen_forward_body;
209
210#[allow(unused_macros)]
211#[macro_export]
212macro_rules! get_end_field {
213    ($prev_sel:expr ;) => {
214        $prev_sel
215    };
216
217    // Special case: if the last field is marked with tail, we use it directly without doing Pair(last combinator, End)
218    // No proof required for the forward direction
219    ($prev_sel:expr ; (tail, $first:ident)) => {
220        EndValue
221    };
222
223    ($prev_sel:expr ; ($($modifier:ident $(($modifier_arg:expr))?)?, $first:ident) $(, ($($rest_modifier:ident $(($rest_modifier_arg:expr))?)?, $rest:ident))*) => {
224        get_end_field!($prev_sel.1 ; $(($($rest_modifier $(($rest_modifier_arg))?)?, $rest)),*)
225    };
226}
227pub use get_end_field;
228
229#[allow(unused_macros)]
230#[macro_export]
231macro_rules! gen_backward_body {
232    ($src:expr ;) => {
233        EndValue
234    };
235
236    ($src:expr ; (tail, $first:ident)) => {
237        $src.$first
238    };
239
240    ($src:expr ; ($($modifier:ident $(($modifier_arg:expr))?)?, $first:ident) $(, ($($rest_modifier:ident $(($rest_modifier_arg:expr))?)?, $rest:ident))*) => {
241        PairValue($src.$first, gen_backward_body!($src ; $(($($rest_modifier $(($rest_modifier_arg))?)?, $rest)),*))
242    };
243}
244pub use gen_backward_body;
245
246#[allow(unused_macros)]
247#[macro_export]
248macro_rules! gen_field_poly_type {
249    ((, $field:ident)) => {
250        $field
251    };
252
253    ((optional, $field:ident)) => {
254        OptionDeep<$field>
255    };
256
257    ((default($_:expr), $field:ident)) => {
258        $field
259    };
260
261    ((tail, $field:ident)) => {
262        $field
263    };
264}
265pub use gen_field_poly_type;
266
267/// Generate a continuation that matches the input
268/// against a set of values and for each value,
269/// the result is parsed with different a combinator
270/// and stored in the suitable variant.
271///
272/// This generates the following types:
273/// - `[< $name Cont >]`: a continuation struct to be used in Depend
274/// - `[< Spec $name Value >]`: the spec result enum
275/// - `[< $name Value >]`: the normal result enum
276/// - `[< $name ValueOwned >]`: the owned result enum
277///
278/// Example:
279/// ```ignore
280/// match_continuation! {
281///     continuation ExtensionParam<'a>(ObjectIdentifierValue, spec SpecObjectIdentifierValue) {
282///         oid!(2, 5, 29, 35), spec spec_oid!(2, 5, 29, 35) => AuthorityKeyIdentifier, ASN1<OctetString>, ASN1(OctetString),
283///         _ => Other, ASN1<OctetString>, ASN1(OctetString),
284///     }
285/// }
286/// ```
287#[allow(unused_macros)]
288#[macro_export]
289macro_rules! match_continuation {
290    (
291        continuation $name:ident<$lt:lifetime>($input_type:ty, spec $spec_input_type:ty) {
292            $(
293                $value:expr, spec $spec_value:expr => $variant:ident, $combinator_type:ty, $combinator:expr,
294            )*
295
296            _ => $last_variant:ident, $last_combinator_type:ty, $last_combinator:expr,
297
298            $(,)?
299        }
300    ) => {
301        ::paste::paste! {
302            ::builtin_macros::verus! {
303                pub use [< internal_ $name >]::Cont as [< $name Cont >];
304                pub use [< internal_ $name >]::SpecValue as [< Spec $name Value >];
305                pub use [< internal_ $name >]::Value as [< $name Value >];
306                pub use [< internal_ $name >]::ValueOwned as [< $name ValueOwned >];
307
308                mod [< internal_ $name >] {
309                    #![allow(non_camel_case_types)]
310                    #![allow(non_snake_case)]
311
312                    use super::*;
313                    use crate::x509::macros::*;
314                    use crate::asn1::*;
315                    use crate::common::*;
316
317                    #[derive(Debug, View)]
318                    pub struct Cont;
319
320                    impl Cont {
321                        gen_match_continuation_spec_apply! {
322                            Mapper, Cont, $spec_input_type;
323                            $(($spec_value, $combinator),)*
324                            (, $last_combinator)
325                        }
326                    }
327
328                    impl Continuation for Cont {
329                        type Input<$lt> = $input_type;
330                        type Output = Mapped<ord_choice_type!(
331                            $(
332                                Cond<$combinator_type>,
333                            )*
334                            Cond<$last_combinator_type>,
335
336                            // Since we can't generate match arms with macros
337                            // the gen_* macros are using a sequence of if let's
338                            // and Rust doesn't know that the if let's are exhaustive
339                            // so we have a "wildcard" case in the end that should
340                            // never be reached
341                            Unreachable,
342                        ), Mapper>;
343
344                        gen_match_continuation_apply! {
345                            Mapper;
346                            $(($value, $spec_value, $combinator),)*
347                            (, $last_combinator)
348                        }
349
350                        open spec fn requires<'a>(&self, i: Self::Input<'a>) -> bool {
351                            true
352                        }
353
354                        open spec fn ensures<'a>(&self, i: Self::Input<'a>, o: Self::Output) -> bool {
355                            &&& o@ == Self::spec_apply(i@)
356                        }
357                    }
358
359                    mapper! {
360                        pub struct Mapper;
361
362                        for <$($variant,)* $last_variant>
363                        from FromType where type FromType<$($variant,)* $last_variant> = ord_choice_result!($($variant,)* $last_variant, ());
364                        to PolyType where pub enum PolyType<$($variant,)* $last_variant> {
365                            $($variant($variant),)*
366                            $last_variant($last_variant),
367                            Unreachable,
368                        }
369
370                        spec SpecValue with <
371                            $(<<$combinator_type as View>::V as SpecCombinator>::SpecResult,)*
372                            <<$last_combinator_type as View>::V as SpecCombinator>::SpecResult
373                        >;
374                        exec Value<'a> with <
375                            $(<$combinator_type as Combinator>::Result<'a>,)*
376                            <$last_combinator_type as Combinator>::Result<'a>
377                        >;
378                        owned ValueOwned with <
379                            $(<$combinator_type as Combinator>::Owned,)*
380                            <$last_combinator_type as Combinator>::Owned
381                        >;
382
383                        forward(x) {
384                            gen_choice_forward! {
385                                x;
386                                $($variant,)* $last_variant
387                            }
388                        } by {
389                            // One extra * for the last variant
390                            if let gen_choice_last_field_pat!(p, (*,); $($variant),*) = x {
391                                assert(p == ());
392                            }
393                        }
394
395                        backward(y) {
396                            gen_choice_backward! {
397                                y;
398                                $($variant,)* $last_variant
399                            }
400                        }
401                    }
402                }
403            }
404        }
405    };
406}
407pub use match_continuation;
408
409/// Special case for matching against OIDs
410///
411/// In addition to match_continuation, this macro also generates
412/// a lemma that the OIDs are disjoint.
413///
414/// NOTE: the provided OIDs are assumed to be disjoint (due to
415/// the missing proof in gen_lemma_disjoint), otherwise we may
416/// have a soundness issue
417#[allow(unused_macros)]
418#[macro_export]
419macro_rules! oid_match_continuation {
420    (
421        continuation $name:ident {
422            $(
423                oid($($arc:expr),+) => $variant:ident($combinator:expr): $combinator_type:ty,
424            )*
425
426            _ => $last_variant:ident($last_combinator:expr): $last_combinator_type:ty,
427
428            $(,)?
429        }
430    ) => {
431        crate::x509::macros::match_continuation! {
432            continuation $name<'a>(ObjectIdentifierValue, spec SpecObjectIdentifierValue) {
433                $(
434                    crate::x509::oid!($($arc),+), spec crate::x509::spec_oid!($($arc),+) => $variant, $combinator_type, $combinator,
435                )*
436
437                _ => $last_variant, $last_combinator_type, $last_combinator,
438            }
439        }
440    }
441}
442pub use oid_match_continuation;
443
444#[allow(unused_macros)]
445#[macro_export]
446macro_rules! gen_match_continuation_spec_apply_helper {
447    ($input:expr, $last_cond:expr; (, $last_combinator:expr)) => {
448        OrdChoice(
449            Cond { cond: $last_cond, inner: $last_combinator },
450            Unreachable,
451        )
452    };
453
454    ($input:expr, $last_cond:expr; ($first_spec_value:expr, $first_combinator:expr), $(($rest_spec_value:expr, $rest_combinator:expr),)* (, $last_combinator:expr)) => {
455        OrdChoice(
456            Cond { cond: ext_equal($input, $first_spec_value), inner: $first_combinator },
457            gen_match_continuation_spec_apply_helper!($input, $last_cond; $(($rest_spec_value, $rest_combinator),)* (, $last_combinator))
458        )
459    };
460}
461pub use gen_match_continuation_spec_apply_helper;
462
463#[allow(unused_macros)]
464#[macro_export]
465macro_rules! gen_match_continuation_spec_apply {
466    ($mapper:expr, $cont_name:ident, $spec_input_type:ty; $(($spec_value:expr, $combinator:expr),)* (, $last_combinator:expr)) => {
467        ::builtin_macros::verus! {
468            pub open spec fn spec_apply(i: $spec_input_type) -> <$cont_name as Continuation>::Output {
469                let other = $(!ext_equal(i, $spec_value) &&)* true;
470                Mapped {
471                    inner: gen_match_continuation_spec_apply_helper!(i, other; $(($spec_value, $combinator),)* (, $last_combinator)),
472                    mapper: $mapper,
473                }
474            }
475        }
476    };
477}
478pub use gen_match_continuation_spec_apply;
479
480#[allow(unused_macros)]
481#[macro_export]
482macro_rules! gen_match_continuation_apply_helper {
483    ($input:expr, $last_cond:expr; (, $last_combinator:expr)) => {
484        OrdChoice(
485            Cond { cond: $last_cond, inner: $last_combinator },
486            Unreachable,
487        )
488    };
489
490    ($input:expr, $last_cond:expr; ($first_value:expr, $first_combinator:expr), $(($rest_value:expr, $rest_combinator:expr),)* (, $last_combinator:expr)) => {
491        OrdChoice(
492            Cond { cond: $input.polyfill_eq(&$first_value), inner: $first_combinator },
493            gen_match_continuation_apply_helper!($input, $last_cond; $(($rest_value, $rest_combinator),)* (, $last_combinator))
494        )
495    };
496}
497pub use gen_match_continuation_apply_helper;
498
499#[allow(unused_macros)]
500#[macro_export]
501macro_rules! gen_match_continuation_apply {
502    ($mapper:expr; $(($value:expr, $spec_value:expr, $combinator:expr),)* (, $last_combinator:expr)) => {
503        ::builtin_macros::verus! {
504            #[inline(always)]
505            fn apply<'a>(&self, i: Self::Input<'a>) -> (o: Self::Output) {
506                let other = $(!i.polyfill_eq(&$value) &&)* true;
507                $({ #[allow(unused_variables)] let v = $value; assert(ext_equal(v.view(), $spec_value)); })*
508
509                Mapped {
510                    inner: gen_match_continuation_apply_helper!(i, other; $(($value, $combinator),)* (, $last_combinator)),
511                    mapper: $mapper,
512                }
513            }
514        }
515    };
516}
517pub use gen_match_continuation_apply;
518
519/// Given variants, generate if let branches to transform $src
520/// from a nested Either term to a specific variant
521#[allow(unused_macros)]
522#[macro_export]
523macro_rules! gen_choice_forward {
524    ($src:expr; $($variant:ident),*) => {
525        gen_choice_forward_branches! {
526            $src, (); $($variant),*
527        }
528    };
529}
530pub use gen_choice_forward;
531
532#[allow(unused_macros)]
533#[macro_export]
534macro_rules! gen_choice_forward_branches {
535    ($src:expr, ($($stars:tt,)*); $last_variant:ident) => {
536        if let inj_ord_choice_pat!($($stars,)* p, *) = $src {
537            PolyType::$last_variant(p)
538        } else {
539            PolyType::Unreachable
540        }
541    };
542
543    ($src:expr, ($($stars:tt,)*); $first_variant:ident $(, $rest_variant:ident)+) => {
544        if let inj_ord_choice_pat!($($stars,)* p, *) = $src {
545            PolyType::$first_variant(p)
546        } else {
547            gen_choice_forward_branches! {
548                $src, ($($stars,)* *,); $($rest_variant),*
549            }
550        }
551    };
552}
553pub use gen_choice_forward_branches;
554
555/// Generate inj_ord_choice_pat!(*, ..., *, p) with |$variant| stars before p
556#[allow(unused_macros)]
557#[macro_export]
558macro_rules! gen_choice_last_field_pat {
559    ($pat:pat, ($($stars:tt,)*);) => {
560        inj_ord_choice_pat!($($stars),*, $pat)
561    };
562
563    ($pat:pat, ($($stars:tt,)*); $_:ident $(, $rest:ident)*) => {
564        gen_choice_last_field_pat!($pat, ($($stars,)* *,); $($rest),*)
565    };
566}
567pub use gen_choice_last_field_pat;
568
569/// Given variants, generate if let branches to transform $src
570/// to a nested Either term
571/// if let variant1(p) = x {
572///    inj_ord_choice_result!(...)
573/// } else if let variant2(p) = x {
574///    ...
575/// } ...
576#[allow(unused_macros)]
577#[macro_export]
578macro_rules! gen_choice_backward {
579    ($src:expr; $($variant:ident),+) => {
580        gen_choice_backward_branches! {
581            $src, (); $($variant),+
582        }
583    };
584}
585pub use gen_choice_backward;
586
587#[allow(unused_macros)]
588#[macro_export]
589macro_rules! gen_choice_backward_branches {
590    ($src:expr, ($($stars:tt,)*); $last_variant:ident) => {
591        if let PolyType::$last_variant(p) = $src {
592            inj_ord_choice_result!($($stars,)* p, *)
593        } else {
594            inj_ord_choice_result!($($stars,)* *, ())
595        }
596    };
597
598    ($src:expr, ($($stars:tt,)*); $first_variant:ident $(, $rest_variant:ident)+) => {
599        if let PolyType::$first_variant(p) = $src {
600            inj_ord_choice_result!($($stars,)* p, *)
601        } else {
602            gen_choice_backward_branches! {
603                $src, ($($stars,)* *,); $($rest_variant),*
604            }
605        }
606    };
607}
608pub use gen_choice_backward_branches;
609
610/// Generate a combinator for an ASN.1 CHOICE
611///
612/// For example
613/// ```ignore
614/// asn1_choice! {
615///     choice Test {
616///         PrintableString(ASN1(PrintableString)): ASN1<PrintableString>,
617///         UTF8String(ASN1(UTF8String)): ASN1<UTF8String>,
618///     }
619/// }
620/// ```
621///
622/// This essentially generates an `OrdChoice` combinator over all the choices
623///
624/// NOTE: Since we can't generate match branches in macros, there is a small
625/// artifact in the definition of the result type: a last variant with name
626/// `Unreachable`, which should never be produced at runtime as the combinator
627/// of Unreachable always fails
628#[allow(unused_macros)]
629#[macro_export]
630macro_rules! asn1_choice {
631    // This assumes the view of $field_combinator is also $field_combinator
632    (
633        choice $name:ident {
634            $( $variant:ident($combinator:expr): $combinator_type:ty ),+
635            $(,)?
636        }
637    ) => {
638        ::paste::paste! {
639            ::builtin_macros::verus! {
640                pub use [< internal_ $name >]::$name;
641                pub use [< internal_ $name >]::SpecValue as [< Spec $name Value >];
642                pub use [< internal_ $name >]::Value as [< $name Value >];
643                pub use [< internal_ $name >]::ValueOwned as [< $name ValueOwned >];
644
645                mod [< internal_ $name >] {
646                    #![allow(non_camel_case_types)]
647                    #![allow(non_snake_case)]
648
649                    use super::*;
650                    use crate::x509::macros::*;
651                    use crate::asn1::*;
652                    use crate::common::*;
653
654                    wrap_combinator! {
655                        pub struct $name: Mapped<ord_choice_type!(
656                                $($combinator_type,)+
657                                Unreachable,
658                            ), Mapper> =>
659                            spec SpecValue,
660                            exec<'a> Value<'a>,
661                            owned ValueOwned,
662                        = Mapped {
663                                inner: ord_choice!(
664                                    $($combinator,)+
665                                    Unreachable,
666                                ),
667                                mapper: Mapper,
668                            };
669                    }
670
671                    mapper! {
672                        // Implement a mapper from nested Eithers to a specific variant
673                        // TODO: same as the mapper in match_continuation, merge?
674                        pub struct Mapper;
675
676                        for <$($variant),+>
677                        from FromType where type FromType<$($variant),+> = ord_choice_result!($($variant),+, ());
678                        to PolyType where #[derive(Eq, PartialEq)] pub enum PolyType<$($variant),+> {
679                            $($variant($variant),)+
680                            Unreachable,
681                        }
682
683                        spec SpecValue with <
684                            $(<<$combinator_type as View>::V as SpecCombinator>::SpecResult),+
685                        >;
686                        exec Value<'a> with <
687                            $(<$combinator_type as Combinator>::Result<'a>),+
688                        >;
689                        owned ValueOwned with <
690                            $(<$combinator_type as Combinator>::Owned),+
691                        >;
692
693                        forward(x) {
694                            gen_choice_forward! { x; $($variant),+ }
695                        } by {
696                            if let gen_choice_last_field_pat!(p, (); $($variant),+) = x {
697                                assert(p == ());
698                            }
699                        }
700
701                        backward(y) {
702                            gen_choice_backward! { y; $($variant),+ }
703                        }
704                    }
705                }
706            }
707        }
708    };
709}
710pub use asn1_choice;
711
712/// Generate a combinator for an ASN.1 SEQUENCE OF
713#[allow(unused_macros)]
714#[macro_export]
715macro_rules! asn1_sequence_of {
716    (
717        seq of $name:ident($combinator:expr): $combinator_type:ty;
718    ) => {
719        ::paste::paste! {
720            ::builtin_macros::verus! {
721                pub use [< internal_ $name >]::$name;
722                pub use [< internal_ $name >]::SpecValue as [< Spec $name Value >];
723                pub use [< internal_ $name >]::Value as [< $name Value >];
724                pub use [< internal_ $name >]::ValueOwned as [< $name ValueOwned >];
725
726                mod [< internal_ $name >] {
727                    #![allow(non_camel_case_types)]
728                    #![allow(non_snake_case)]
729
730                    use super::*;
731                    use crate::x509::macros::*;
732                    use crate::asn1::*;
733                    use crate::common::*;
734
735                    wrap_combinator! {
736                        pub struct $name: SequenceOf<$combinator_type> =>
737                            spec SpecValue,
738                            exec<'a> Value<'a>,
739                            owned ValueOwned,
740                        = SequenceOf($combinator);
741                    }
742
743                    asn1_tagged!($name, tag_of!(SEQUENCE));
744
745                    pub type SpecValue = Seq<<<$combinator_type as View>::V as SpecCombinator>::SpecResult>;
746                    pub type Value<'a> = VecDeep<<$combinator_type as Combinator>::Result<'a>>;
747                    pub type ValueOwned = VecDeep<<$combinator_type as Combinator>::Owned>;
748                }
749            }
750        }
751    };
752}
753pub use asn1_sequence_of;
754
755/// Same as above, but for SET OF
756#[allow(unused_macros)]
757#[macro_export]
758macro_rules! asn1_set_of {
759    (
760        set of $name:ident($combinator:expr): $combinator_type:ty;
761    ) => {
762        ::paste::paste! {
763            ::builtin_macros::verus! {
764                pub use [< internal_ $name >]::$name;
765                pub use [< internal_ $name >]::SpecValue as [< Spec $name Value >];
766                pub use [< internal_ $name >]::Value as [< $name Value >];
767                pub use [< internal_ $name >]::ValueOwned as [< $name ValueOwned >];
768
769                mod [< internal_ $name >] {
770                    #![allow(non_camel_case_types)]
771                    #![allow(non_snake_case)]
772
773                    use super::*;
774                    use crate::x509::macros::*;
775                    use crate::asn1::*;
776                    use crate::common::*;
777
778                    wrap_combinator! {
779                        pub struct $name: SequenceOf<$combinator_type> =>
780                            spec SpecValue,
781                            exec<'a> Value<'a>,
782                            owned ValueOwned,
783                        = SequenceOf($combinator);
784                    }
785
786                    asn1_tagged!($name, tag_of!(SET));
787
788                    pub type SpecValue = Seq<<<$combinator_type as View>::V as SpecCombinator>::SpecResult>;
789                    pub type Value<'a> = VecDeep<<$combinator_type as Combinator>::Result<'a>>;
790                    pub type ValueOwned = VecDeep<<$combinator_type as Combinator>::Owned>;
791                }
792            }
793        }
794    };
795}
796pub use asn1_set_of;
797
798/// Allows multiple definitions involving SEQUENCE, SEQUENCE OF, SET OF, and CHOICE
799#[allow(unused_macros)]
800#[macro_export]
801macro_rules! asn1 {
802    () => {};
803
804    (seq $def:tt { $($body:tt)* } $($rest:tt)*) => {
805        crate::x509::macros::asn1_sequence! { seq $def { $($body)* } }
806        crate::x509::macros::asn1! { $($rest)* }
807    };
808
809    (choice $def:tt { $($body:tt)* } $($rest:tt)*) => {
810        crate::x509::macros::asn1_choice! { choice $def { $($body)* } }
811        crate::x509::macros::asn1! { $($rest)* }
812    };
813
814    (seq of $name:ident($combinator:expr): $combinator_type:ty; $($rest:tt)*) => {
815        crate::x509::macros::asn1_sequence_of! { seq of $name($combinator): $combinator_type; }
816        crate::x509::macros::asn1! { $($rest)* }
817    };
818
819    (set of $name:ident($combinator:expr): $combinator_type:ty; $($rest:tt)*) => {
820        crate::x509::macros::asn1_set_of! { set of $name($combinator): $combinator_type; }
821        crate::x509::macros::asn1! { $($rest)* }
822    };
823}
824pub use asn1;
825
826}
verdict_parser/x509/macros.rs

verdict_parser/x509/
macros.rs
