vest_lib/asn1/macros/
mod.rs

1//! Implementations for generated nominal ASN.1 format types.
2//!
3//! These macros are exported at the crate root as [`impl_der!`](crate::impl_der) and [`impl_ber!`](crate::impl_ber). A generated
4//! nominal format supplies a duel spec-exec `schema()` constructor. Tagged formats
5//! additionally store their outer tag class and number in tuple fields `0` and `1`; the macros
6//! apply that effective tag when constructing the inner format.
7
8#[doc(hidden)]
9#[macro_export]
10macro_rules! __impl_asn1_nominal_inner {
11    (tagged_exact($constructed:expr), $fmt:ident, $inner:ty) => {
12        $crate::__impl_asn1_nominal_inner!(tagged($constructed), $fmt, $inner);
13    };
14    (tagged_identity($constructed:expr), $fmt:ident, $inner:ty) => {
15        $crate::__impl_asn1_nominal_inner!(tagged($constructed), $fmt, $inner);
16    };
17    (untagged_mask($domain:expr), $fmt:ident, $inner:ty) => {
18        $crate::__impl_asn1_nominal_inner!(untagged, $fmt, $inner);
19    };
20    (untagged_any, $fmt:ident, $inner:ty) => {
21        $crate::__impl_asn1_nominal_inner!(untagged, $fmt, $inner);
22    };
23    (tagged($constructed:expr), $fmt:ident, $inner:ty) => {
24        verus! {
25
26        impl $fmt {
27            pub open spec fn spec_inner(&self) -> $inner {
28                Self::schema().spec_retagged($crate::asn1::Tag {
29                    class: self.0,
30                    constructed: $constructed,
31                    number: $crate::asn1::tag::tag_num_from_uint(self.1),
32                })
33            }
34
35            fn exec_inner(&self) -> (fmt: $inner)
36                ensures
37                    fmt == self.spec_inner(),
38            {
39                Self::schema().retagged($crate::asn1::Tag {
40                    class: self.0,
41                    constructed: $constructed,
42                    number: $crate::asn1::tag::tag_num_from_uint(self.1),
43                })
44            }
45        }
46
47        } // verus!
48    };
49    (untagged_start, $fmt:ident, $inner:ty) => {
50        $crate::__impl_asn1_nominal_inner!(untagged, $fmt, $inner);
51    };
52    (untagged, $fmt:ident, $inner:ty) => {
53        verus! {
54
55        impl $fmt {
56            pub open spec fn spec_inner(&self) -> $inner {
57                Self::schema()
58            }
59
60            fn exec_inner(&self) -> (fmt: $inner)
61                ensures
62                    fmt == self.spec_inner(),
63            {
64                Self::schema()
65            }
66        }
67
68        } // verus!
69    };
70}
71
72#[doc(hidden)]
73#[macro_export]
74macro_rules! __impl_asn1_nominal_specs_and_proofs {
75    ($fmt:ident, $spec:ty) => {
76        verus! {
77
78        impl SpecParser for $fmt {
79            type PVal = $spec;
80
81            #[verifier::opaque]
82            open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
83                self.spec_inner().spec_parse(ibuf)
84            }
85        }
86
87        impl Consistency for $fmt {
88            type Val = $spec;
89
90            #[verifier::opaque]
91            open spec fn consistent(&self, value: Self::Val) -> bool {
92                self.spec_inner().consistent(value)
93            }
94        }
95
96        impl SpecSerializerDps for $fmt {
97            type SValue = $spec;
98
99            #[verifier::opaque]
100            open spec fn spec_serialize_dps(&self, value: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
101                self.spec_inner().spec_serialize_dps(value, obuf)
102            }
103        }
104
105        impl SpecSerializer for $fmt {
106            type SVal = $spec;
107
108            #[verifier::opaque]
109            open spec fn spec_serialize(&self, value: Self::SVal) -> Seq<u8> {
110                self.spec_inner().spec_serialize(value)
111            }
112        }
113
114        impl SpecByteLen for $fmt {
115            type T = $spec;
116
117            #[verifier::opaque]
118            open spec fn byte_len(&self, value: Self::T) -> nat {
119                self.spec_inner().byte_len(value)
120            }
121        }
122
123        // The nominal boundary keeps the default `true` invariants. Each proof establishes the
124        // concrete inner obligation locally before delegating.
125        impl SafeParser for $fmt {
126            proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
127                reveal(<$fmt as SpecParser>::spec_parse);
128                self.spec_inner().lemma_parse_safe(ibuf);
129            }
130        }
131
132        impl Productive for $fmt {
133            proof fn lemma_productive(&self, input: Seq<u8>) {
134                reveal(<$fmt as SpecParser>::spec_parse);
135                self.spec_inner().lemma_productive(input);
136            }
137        }
138
139        impl NonTailFmt for $fmt {
140            proof fn lemma_serialize_dps_prepend(&self, value: Self::SValue, obuf: Seq<u8>) {
141                reveal(<$fmt as SpecSerializerDps>::spec_serialize_dps);
142                self.spec_inner().lemma_serialize_dps_prepend(value, obuf);
143            }
144
145            proof fn lemma_serialize_dps_len(&self, value: Self::SValue, obuf: Seq<u8>) {
146                reveal(<$fmt as SpecSerializerDps>::spec_serialize_dps);
147                reveal(<$fmt as SpecByteLen>::byte_len);
148                self.spec_inner().lemma_serialize_dps_len(value, obuf);
149            }
150        }
151
152        impl GoodSerializer for $fmt {
153            proof fn lemma_serialize_len(&self, value: Self::SVal) {
154                reveal(<$fmt as SpecSerializer>::spec_serialize);
155                reveal(<$fmt as SpecByteLen>::byte_len);
156                self.spec_inner().lemma_serialize_len(value);
157            }
158        }
159
160        impl SPRoundTripDps for $fmt {
161            proof fn theorem_serialize_dps_parse_roundtrip(&self, value: Self::T, obuf: Seq<u8>) {
162                reveal(<$fmt as SpecParser>::spec_parse);
163                reveal(<$fmt as Consistency>::consistent);
164                reveal(<$fmt as SpecSerializerDps>::spec_serialize_dps);
165                reveal(<$fmt as SpecByteLen>::byte_len);
166                self.lemma_schema_unambiguous();
167                self.spec_inner().theorem_serialize_dps_parse_roundtrip(value, obuf);
168            }
169        }
170
171        impl EquivSerializersGeneral for $fmt {
172            proof fn lemma_serialize_equiv(&self, value: Self::SVal, obuf: Seq<u8>) {
173                reveal(<$fmt as SpecSerializer>::spec_serialize);
174                reveal(<$fmt as SpecSerializerDps>::spec_serialize_dps);
175                self.spec_inner().lemma_serialize_equiv(value, obuf);
176            }
177        }
178
179        impl EquivSerializers for $fmt {
180            proof fn lemma_serialize_equiv_on_empty(&self, value: Self::SVal) {
181                reveal(<$fmt as SpecSerializer>::spec_serialize);
182                reveal(<$fmt as SpecSerializerDps>::spec_serialize_dps);
183                self.spec_inner().lemma_serialize_equiv_on_empty(value);
184            }
185        }
186
187        } // verus!
188    };
189}
190
191#[doc(hidden)]
192#[macro_export]
193macro_rules! __impl_asn1_nominal_exec_borrowed {
194    ($fmt:ident, $value:ident) => {
195        verus! {
196
197        impl<'i> Parser<&'i [u8]> for $fmt {
198            type PT = $value<'i>;
199
200            fn parse(&self, ibuf: &&'i [u8]) -> (result: PResult<Self::PT>) {
201                proof {
202                    reveal(<$fmt as SpecParser>::spec_parse);
203                }
204                let inner = self.exec_inner();
205                inner.parse(ibuf)
206            }
207        }
208
209        impl<'i, Output: OutputBuf> Serializer<Output, $value<'i>> for $fmt {
210            fn serialize_into(&self, value: &$value<'i>, obuf: &mut Output) {
211                proof {
212                    reveal(<$fmt as Consistency>::consistent);
213                    reveal(<$fmt as SpecSerializer>::spec_serialize);
214                    reveal(<$fmt as SpecByteLen>::byte_len);
215                }
216                let inner = self.exec_inner();
217                inner.serialize_into(value, obuf)
218            }
219        }
220
221        impl<'i> Prepare<$value<'i>> for $fmt {
222            fn prepare(&self, value: &$value<'i>) -> (result: Result<usize, PreSerializeError>) {
223                proof {
224                    reveal(<$fmt as Consistency>::consistent);
225                    reveal(<$fmt as SpecByteLen>::byte_len);
226                }
227                let inner = self.exec_inner();
228                inner.prepare(value)
229            }
230        }
231
232        impl<'i> ByteLen<$value<'i>> for $fmt {
233            fn length(&self, value: &$value<'i>) -> (result: usize) {
234                proof {
235                    reveal(<$fmt as SpecByteLen>::byte_len);
236                }
237                let inner = self.exec_inner();
238                inner.length(value)
239            }
240        }
241
242        } // verus!
243    };
244}
245
246#[doc(hidden)]
247#[macro_export]
248macro_rules! __impl_asn1_nominal_exec_owned {
249    ($fmt:ident, $value:ty) => {
250        verus! {
251
252        impl<'i> Parser<&'i [u8]> for $fmt {
253            type PT = $value;
254
255            fn parse(&self, ibuf: &&'i [u8]) -> (result: PResult<Self::PT>) {
256                proof {
257                    reveal(<$fmt as SpecParser>::spec_parse);
258                }
259                let inner = self.exec_inner();
260                inner.parse(ibuf)
261            }
262        }
263
264        impl<Output: OutputBuf> Serializer<Output, $value> for $fmt {
265            fn serialize_into(&self, value: &$value, obuf: &mut Output) {
266                proof {
267                    reveal(<$fmt as Consistency>::consistent);
268                    reveal(<$fmt as SpecSerializer>::spec_serialize);
269                    reveal(<$fmt as SpecByteLen>::byte_len);
270                }
271                let inner = self.exec_inner();
272                inner.serialize_into(value, obuf)
273            }
274        }
275
276        impl Prepare<$value> for $fmt {
277            fn prepare(&self, value: &$value) -> (result: Result<usize, PreSerializeError>) {
278                proof {
279                    reveal(<$fmt as Consistency>::consistent);
280                    reveal(<$fmt as SpecByteLen>::byte_len);
281                }
282                let inner = self.exec_inner();
283                inner.prepare(value)
284            }
285        }
286
287        impl ByteLen<$value> for $fmt {
288            fn length(&self, value: &$value) -> (result: usize) {
289                proof {
290                    reveal(<$fmt as SpecByteLen>::byte_len);
291                }
292                let inner = self.exec_inner();
293                inner.length(value)
294            }
295        }
296
297        } // verus!
298    };
299}
300
301#[doc(hidden)]
302#[macro_export]
303macro_rules! __impl_asn1_nominal_has_start {
304    (exact($constructed:expr), $fmt:ident) => {
305        $crate::__impl_asn1_nominal_has_start!(@certified $fmt, _this,
306            $crate::asn1::disjoint::asn1_start_exact_uint(_this.0, $constructed, _this.1));
307    };
308    (identity, $fmt:ident) => {
309        $crate::__impl_asn1_nominal_has_start!(@certified $fmt, _this,
310            $crate::asn1::disjoint::asn1_start_identity_uint(_this.0, _this.1));
311    };
312    (mask($domain:expr), $fmt:ident) => {
313        $crate::__impl_asn1_nominal_has_start!(@certified $fmt, _this, $domain);
314    };
315    (any, $fmt:ident) => {
316        $crate::__impl_asn1_nominal_has_start!(@certified $fmt, _this,
317            $crate::asn1::disjoint::asn1_start_any_non_eoc());
318    };
319    (@certified $fmt:ident, $this:ident, $domain:expr) => {
320        verus! {
321
322        impl $crate::asn1::disjoint::HasAsn1Start for $fmt {
323            #[verifier::inline]
324            open spec fn asn1_start(&self) -> $crate::asn1::disjoint::Asn1StartDomain {
325                let $this = self;
326                $domain
327            }
328
329            proof fn lemma_parse_implies_asn1_start(&self, input: Seq<u8>) {
330                self.lemma_schema_unambiguous();
331                reveal(<$fmt as SpecParser>::spec_parse);
332                self.spec_inner().lemma_parse_implies_asn1_start(input);
333            }
334        }
335
336        } // verus!
337    };
338    ($fmt:ident) => {
339        verus! {
340
341        impl $crate::asn1::disjoint::HasAsn1Start for $fmt {
342            #[verifier::inline]
343            open spec fn asn1_start(&self) -> $crate::asn1::disjoint::Asn1StartDomain {
344                self.spec_inner().asn1_start()
345            }
346
347            proof fn lemma_parse_implies_asn1_start(&self, input: Seq<u8>) {
348                reveal(<$fmt as SpecParser>::spec_parse);
349                self.spec_inner().lemma_parse_implies_asn1_start(input);
350            }
351        }
352
353        } // verus!
354    };
355}
356
357#[doc(hidden)]
358#[macro_export]
359macro_rules! __impl_asn1_nominal_tagged {
360    ($fmt:ident) => {
361        verus! {
362
363        impl Retaggable for $fmt {
364            #[verifier::inline]
365            open spec fn spec_retagged(&self, tag: Tag) -> Self {
366                Self(tag.class, $crate::asn1::tag::tag_num_to_uint(tag.number))
367            }
368
369            fn retagged(&self, tag: Tag) -> Self {
370                Self(tag.class, $crate::asn1::tag::tag_number_value(tag.number))
371            }
372        }
373
374        } // verus!
375    };
376}
377
378#[doc(hidden)]
379#[macro_export]
380macro_rules! __impl_asn1_nominal_der_tagged_proofs {
381    ($fmt:ident, $spec:ty $(, $forward:ty, $reverse:ty)?) => {
382        verus! {
383
384        impl $fmt {
385            proof fn lemma_successful_parse_inner_invariants(&self, input: Seq<u8>)
386                requires
387                    self.spec_parse(input) is Some,
388                ensures
389                    self.spec_inner().safe_inv(),
390                    self.spec_inner().sound_inv(),
391                    self.spec_inner().nonmal_inv(),
392            {
393                $(
394                    assert forall|input: <$forward as $crate::combinators::mapped::spec::SpecMap>::Input| #[trigger]
395                        self.spec_inner().inner.consistent(input) implies
396                            self.spec_inner().mapper.lossless(input) by {
397                        if self.spec_inner().inner.consistent(input) {
398                            <$spec>::lemma_into_from(input);
399                        }
400                    }
401                )?
402                reveal(<$fmt as SpecParser>::spec_parse);
403                reveal($fmt::spec_inner);
404                broadcast use $crate::asn1::tag::lemma_tag_wf_implies_tag_consistent;
405                self.spec_inner().lemma_parse_implies_asn1_start(input);
406                reveal($crate::asn1::disjoint::input_starts_with);
407                TagFmt.lemma_parse_sound_value(input);
408            }
409        }
410
411        impl SoundParser for $fmt {
412            proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
413                reveal(<$fmt as SpecParser>::spec_parse);
414                reveal(<$fmt as SpecByteLen>::byte_len);
415                if self.spec_parse(ibuf) is Some {
416                    self.lemma_successful_parse_inner_invariants(ibuf);
417                    self.spec_inner().lemma_parse_sound_consumption(ibuf);
418                }
419            }
420
421            proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
422                reveal(<$fmt as SpecParser>::spec_parse);
423                reveal(<$fmt as Consistency>::consistent);
424                if self.spec_parse(ibuf) is Some {
425                    self.lemma_successful_parse_inner_invariants(ibuf);
426                    self.spec_inner().lemma_parse_sound_value(ibuf);
427                }
428            }
429        }
430
431        impl NonMalleable for $fmt {
432            proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
433                reveal(<$fmt as SpecParser>::spec_parse);
434                if self.spec_parse(buf1) is Some && self.spec_parse(buf2) is Some {
435                    self.lemma_successful_parse_inner_invariants(buf1);
436                    self.spec_inner().lemma_parse_non_malleable(buf1, buf2);
437                }
438            }
439        }
440
441        } // verus!
442    };
443}
444
445#[doc(hidden)]
446#[macro_export]
447macro_rules! __impl_asn1_nominal_der_fixed_proofs {
448    ($fmt:ident, $spec:ty $(, $forward:ty, $reverse:ty)?) => {
449        verus! {
450
451        impl $fmt {
452            proof fn lemma_sound_nonmal_inv(&self)
453                ensures
454                    self.spec_inner().sound_inv(),
455                    self.spec_inner().nonmal_inv(),
456            {
457                $(
458                    assert forall|input: <$forward as $crate::combinators::mapped::spec::SpecMap>::Input| #[trigger]
459                        self.spec_inner().inner.consistent(input) implies
460                            self.spec_inner().mapper.lossless(input) by {
461                        if self.spec_inner().inner.consistent(input) {
462                            <$spec>::lemma_into_from(input);
463                        }
464                    }
465                )?
466                broadcast use $crate::asn1::tag::lemma_tag_wf_implies_tag_consistent;
467            }
468        }
469
470        impl SoundParser for $fmt {
471            proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
472                reveal(<$fmt as SpecParser>::spec_parse);
473                reveal(<$fmt as SpecByteLen>::byte_len);
474                self.lemma_sound_nonmal_inv();
475                self.spec_inner().lemma_parse_sound_consumption(ibuf);
476            }
477
478            proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
479                reveal(<$fmt as SpecParser>::spec_parse);
480                reveal(<$fmt as Consistency>::consistent);
481                self.lemma_sound_nonmal_inv();
482                self.spec_inner().lemma_parse_sound_value(ibuf);
483            }
484        }
485
486        impl NonMalleable for $fmt {
487            proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
488                reveal(<$fmt as SpecParser>::spec_parse);
489                self.lemma_sound_nonmal_inv();
490                self.spec_inner().lemma_parse_non_malleable(buf1, buf2);
491            }
492        }
493
494        } // verus!
495    };
496}
497
498#[doc(hidden)]
499#[macro_export]
500macro_rules! __impl_asn1_nominal_der_ord_borrowed {
501    ($fmt:ident, $inner:ty, $spec:ty, $value:ident $(, $forward:ty, $reverse:ty)?) => {
502        verus! {
503
504        impl DerState for $fmt {
505            type State = <$inner as DerState>::State;
506        }
507
508        impl<'i> DerOrd<$value<'i>> for $fmt {
509            proof fn lemma_der_serialize_len(&self, value: $spec) {
510                $(
511                    reveal(<$reverse as $crate::combinators::mapped::spec::SpecMap>::spec_map);
512                )?
513                reveal(<$fmt as Consistency>::consistent);
514                reveal(<$fmt as SpecSerializer>::spec_serialize);
515                reveal(<$fmt as SpecByteLen>::byte_len);
516                <$inner as DerOrd<$value<'i>>>::lemma_der_serialize_len(
517                    &self.spec_inner(),
518                    value,
519                );
520            }
521
522            open spec fn der_remaining(
523                &self,
524                value: $spec,
525                state: <Self as DerState>::State,
526            ) -> Seq<u8> {
527                <$inner as DerOrd<$value<'i>>>::der_remaining(&self.spec_inner(), value, state)
528            }
529
530            open spec fn der_state_valid(
531                &self,
532                value: $spec,
533                state: <Self as DerState>::State,
534            ) -> bool {
535                <$inner as DerOrd<$value<'i>>>::der_state_valid(&self.spec_inner(), value, state)
536            }
537
538            fn der_start(&self, value: &$value<'i>) -> (state: <Self as DerState>::State) {
539                proof {
540                    $(
541                        reveal(<$reverse as $crate::combinators::mapped::spec::SpecMap>::spec_map);
542                    )?
543                    reveal(<$fmt as Consistency>::consistent);
544                    reveal(<$fmt as SpecSerializer>::spec_serialize);
545                }
546                let inner = self.exec_inner();
547                <$inner as DerOrd<$value<'i>>>::der_start(&inner, value)
548            }
549
550            fn der_next(
551                &self,
552                value: &$value<'i>,
553                state: &mut <Self as DerState>::State,
554            ) -> (next: Option<u8>) {
555                proof {
556                    $(
557                        reveal(<$reverse as $crate::combinators::mapped::spec::SpecMap>::spec_map);
558                    )?
559                    reveal(<$fmt as Consistency>::consistent);
560                }
561                let inner = self.exec_inner();
562                <$inner as DerOrd<$value<'i>>>::der_next(&inner, value, state)
563            }
564        }
565
566        } // verus!
567    };
568}
569
570#[doc(hidden)]
571#[macro_export]
572macro_rules! __impl_asn1_nominal_der_ord_owned {
573    ($fmt:ident, $inner:ty, $spec:ty, $value:ty $(, $forward:ty, $reverse:ty)?) => {
574        verus! {
575
576        impl DerState for $fmt {
577            type State = <$inner as DerState>::State;
578        }
579
580        impl DerOrd<$value> for $fmt {
581            proof fn lemma_der_serialize_len(&self, value: $spec) {
582                $(
583                    reveal(<$reverse as $crate::combinators::mapped::spec::SpecMap>::spec_map);
584                )?
585                reveal(<$fmt as Consistency>::consistent);
586                reveal(<$fmt as SpecSerializer>::spec_serialize);
587                reveal(<$fmt as SpecByteLen>::byte_len);
588                <$inner as DerOrd<$value>>::lemma_der_serialize_len(&self.spec_inner(), value);
589            }
590
591            open spec fn der_remaining(
592                &self,
593                value: $spec,
594                state: <Self as DerState>::State,
595            ) -> Seq<u8> {
596                <$inner as DerOrd<$value>>::der_remaining(&self.spec_inner(), value, state)
597            }
598
599            open spec fn der_state_valid(
600                &self,
601                value: $spec,
602                state: <Self as DerState>::State,
603            ) -> bool {
604                <$inner as DerOrd<$value>>::der_state_valid(&self.spec_inner(), value, state)
605            }
606
607            fn der_start(&self, value: &$value) -> (state: <Self as DerState>::State) {
608                proof {
609                    $(
610                        reveal(<$reverse as $crate::combinators::mapped::spec::SpecMap>::spec_map);
611                    )?
612                    reveal(<$fmt as Consistency>::consistent);
613                    reveal(<$fmt as SpecSerializer>::spec_serialize);
614                }
615                let inner = self.exec_inner();
616                <$inner as DerOrd<$value>>::der_start(&inner, value)
617            }
618
619            fn der_next(
620                &self,
621                value: &$value,
622                state: &mut <Self as DerState>::State,
623            ) -> (next: Option<u8>) {
624                proof {
625                    $(
626                        reveal(<$reverse as $crate::combinators::mapped::spec::SpecMap>::spec_map);
627                    )?
628                    reveal(<$fmt as Consistency>::consistent);
629                }
630                let inner = self.exec_inner();
631                <$inner as DerOrd<$value>>::der_next(&inner, value, state)
632            }
633        }
634
635        } // verus!
636    };
637}
638
639/// Implements the verified DER traits and executable APIs for a generated nominal format.
640#[macro_export]
641macro_rules! impl_der {
642    ($kind:ident $(($constructed:expr))?, borrowed, $fmt:ident, $inner:ty, $spec:ty, $value:ident $(, $forward:ty, $reverse:ty)?) => {
643        $crate::__impl_asn1_nominal_inner!($kind $(($constructed))?, $fmt, $inner);
644        $crate::__impl_asn1_nominal_specs_and_proofs!($fmt, $spec);
645        $crate::__impl_asn1_nominal_exec_borrowed!($fmt, $value);
646        $crate::__impl_asn1_nominal_der_ord_borrowed!($fmt, $inner, $spec, $value $(, $forward, $reverse)?);
647        $crate::impl_der!(@kind $kind $(($constructed))?, $fmt, $spec $(, $forward, $reverse)?);
648    };
649    ($kind:ident $(($constructed:expr))?, owned, $fmt:ident, $inner:ty, $spec:ty, $value:ty $(, $forward:ty, $reverse:ty)?) => {
650        $crate::__impl_asn1_nominal_inner!($kind $(($constructed))?, $fmt, $inner);
651        $crate::__impl_asn1_nominal_specs_and_proofs!($fmt, $spec);
652        $crate::__impl_asn1_nominal_exec_owned!($fmt, $value);
653        $crate::__impl_asn1_nominal_der_ord_owned!($fmt, $inner, $spec, $value $(, $forward, $reverse)?);
654        $crate::impl_der!(@kind $kind $(($constructed))?, $fmt, $spec $(, $forward, $reverse)?);
655    };
656    (@kind tagged($constructed:expr), $fmt:ident, $spec:ty $(, $forward:ty, $reverse:ty)?) => {
657        $crate::__impl_asn1_nominal_has_start!($fmt);
658        $crate::__impl_asn1_nominal_tagged!($fmt);
659        $crate::__impl_asn1_nominal_der_tagged_proofs!($fmt, $spec $(, $forward, $reverse)?);
660    };
661    (@kind tagged_exact($constructed:expr), $fmt:ident, $spec:ty $(, $forward:ty, $reverse:ty)?) => {
662        $crate::__impl_asn1_nominal_has_start!(exact($constructed), $fmt);
663        $crate::__impl_asn1_nominal_tagged!($fmt);
664        $crate::__impl_asn1_nominal_der_tagged_proofs!($fmt, $spec $(, $forward, $reverse)?);
665    };
666    (@kind tagged_identity($constructed:expr), $fmt:ident, $spec:ty $(, $forward:ty, $reverse:ty)?) => {
667        $crate::__impl_asn1_nominal_has_start!(identity, $fmt);
668        $crate::__impl_asn1_nominal_tagged!($fmt);
669        $crate::__impl_asn1_nominal_der_tagged_proofs!($fmt, $spec $(, $forward, $reverse)?);
670    };
671    (@kind untagged_mask($domain:expr), $fmt:ident, $spec:ty $(, $forward:ty, $reverse:ty)?) => {
672        $crate::__impl_asn1_nominal_has_start!(mask($domain), $fmt);
673        $crate::__impl_asn1_nominal_der_fixed_proofs!($fmt, $spec $(, $forward, $reverse)?);
674    };
675    (@kind untagged_any, $fmt:ident, $spec:ty $(, $forward:ty, $reverse:ty)?) => {
676        $crate::__impl_asn1_nominal_has_start!(any, $fmt);
677        $crate::__impl_asn1_nominal_der_fixed_proofs!($fmt, $spec $(, $forward, $reverse)?);
678    };
679    (@kind untagged_start, $fmt:ident, $spec:ty $(, $forward:ty, $reverse:ty)?) => {
680        $crate::__impl_asn1_nominal_has_start!($fmt);
681        $crate::__impl_asn1_nominal_der_fixed_proofs!($fmt, $spec $(, $forward, $reverse)?);
682    };
683    (@kind untagged, $fmt:ident, $spec:ty $(, $forward:ty, $reverse:ty)?) => {
684        $crate::__impl_asn1_nominal_der_fixed_proofs!($fmt, $spec $(, $forward, $reverse)?);
685    };
686}
687
688/// Implements the verified BER traits and executable APIs for a generated nominal format.
689///
690/// BER formats deliberately do not implement `SoundParser`, `NonMalleable`, or DER ordering.
691#[macro_export]
692macro_rules! impl_ber {
693    ($kind:ident $(($constructed:expr))?, borrowed, $fmt:ident, $inner:ty, $spec:ty, $value:ident $(, $forward:ty, $reverse:ty)?) => {
694        $crate::__impl_asn1_nominal_inner!($kind $(($constructed))?, $fmt, $inner);
695        $crate::__impl_asn1_nominal_specs_and_proofs!($fmt, $spec);
696        $crate::__impl_asn1_nominal_exec_borrowed!($fmt, $value);
697        $crate::impl_ber!(@kind $kind $(($constructed))?, $fmt);
698    };
699    ($kind:ident $(($constructed:expr))?, owned, $fmt:ident, $inner:ty, $spec:ty, $value:ty $(, $forward:ty, $reverse:ty)?) => {
700        $crate::__impl_asn1_nominal_inner!($kind $(($constructed))?, $fmt, $inner);
701        $crate::__impl_asn1_nominal_specs_and_proofs!($fmt, $spec);
702        $crate::__impl_asn1_nominal_exec_owned!($fmt, $value);
703        $crate::impl_ber!(@kind $kind $(($constructed))?, $fmt);
704    };
705    (@kind tagged($constructed:expr), $fmt:ident) => {
706        $crate::__impl_asn1_nominal_has_start!($fmt);
707        $crate::__impl_asn1_nominal_tagged!($fmt);
708    };
709    (@kind tagged_exact($constructed:expr), $fmt:ident) => {
710        $crate::__impl_asn1_nominal_has_start!(exact($constructed), $fmt);
711        $crate::__impl_asn1_nominal_tagged!($fmt);
712    };
713    (@kind tagged_identity($constructed:expr), $fmt:ident) => {
714        $crate::__impl_asn1_nominal_has_start!(identity, $fmt);
715        $crate::__impl_asn1_nominal_tagged!($fmt);
716    };
717    (@kind untagged_mask($domain:expr), $fmt:ident) => {
718        $crate::__impl_asn1_nominal_has_start!(mask($domain), $fmt);
719    };
720    (@kind untagged_any, $fmt:ident) => {
721        $crate::__impl_asn1_nominal_has_start!(any, $fmt);
722    };
723    (@kind untagged_start, $fmt:ident) => {
724        $crate::__impl_asn1_nominal_has_start!($fmt);
725    };
726    (@kind untagged, $fmt:ident) => {};
727}
728
729// `#[macro_export]` places macros at the crate root. Re-export them here as well so callers can
730// discover and import them through `vest_lib::asn1::macros`.
731pub use crate::{impl_ber, impl_der};
vest_lib/asn1/macros/mod.rs

vest_lib/asn1/macros/
mod.rs
