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 min_byte_len(&self) -> usize {
201                <_ as Parser<&'i [u8]>>::min_byte_len(&self.exec_inner())
202            }
203
204            fn parse(&self, ibuf: &&'i [u8]) -> (result: PResult<Self::PT>) {
205                proof {
206                    reveal(<$fmt as SpecParser>::spec_parse);
207                }
208                let inner = self.exec_inner();
209                inner.parse(ibuf)
210            }
211        }
212
213        impl<'i, Output: OutputBuf> Serializer<Output, $value<'i>> for $fmt {
214            fn serialize_into(&self, value: &$value<'i>, obuf: &mut Output) {
215                proof {
216                    reveal(<$fmt as Consistency>::consistent);
217                    reveal(<$fmt as SpecSerializer>::spec_serialize);
218                    reveal(<$fmt as SpecByteLen>::byte_len);
219                }
220                let inner = self.exec_inner();
221                inner.serialize_into(value, obuf)
222            }
223        }
224
225        impl<'i> Prepare<$value<'i>> for $fmt {
226            fn prepare(&self, value: &$value<'i>) -> (result: Result<usize, PreSerializeError>) {
227                proof {
228                    reveal(<$fmt as Consistency>::consistent);
229                    reveal(<$fmt as SpecByteLen>::byte_len);
230                }
231                let inner = self.exec_inner();
232                inner.prepare(value)
233            }
234        }
235
236        impl<'i> ByteLen<$value<'i>> for $fmt {
237            fn length(&self, value: &$value<'i>) -> (result: usize) {
238                proof {
239                    reveal(<$fmt as SpecByteLen>::byte_len);
240                }
241                let inner = self.exec_inner();
242                inner.length(value)
243            }
244        }
245
246        } // verus!
247    };
248}
249
250#[doc(hidden)]
251#[macro_export]
252macro_rules! __impl_asn1_nominal_exec_owned {
253    ($fmt:ident, $value:ty) => {
254        verus! {
255
256        impl<'i> Parser<&'i [u8]> for $fmt {
257            type PT = $value;
258
259            fn min_byte_len(&self) -> usize {
260                <_ as Parser<&'i [u8]>>::min_byte_len(&self.exec_inner())
261            }
262
263            fn parse(&self, ibuf: &&'i [u8]) -> (result: PResult<Self::PT>) {
264                proof {
265                    reveal(<$fmt as SpecParser>::spec_parse);
266                }
267                let inner = self.exec_inner();
268                inner.parse(ibuf)
269            }
270        }
271
272        impl<Output: OutputBuf> Serializer<Output, $value> for $fmt {
273            fn serialize_into(&self, value: &$value, obuf: &mut Output) {
274                proof {
275                    reveal(<$fmt as Consistency>::consistent);
276                    reveal(<$fmt as SpecSerializer>::spec_serialize);
277                    reveal(<$fmt as SpecByteLen>::byte_len);
278                }
279                let inner = self.exec_inner();
280                inner.serialize_into(value, obuf)
281            }
282        }
283
284        impl Prepare<$value> for $fmt {
285            fn prepare(&self, value: &$value) -> (result: Result<usize, PreSerializeError>) {
286                proof {
287                    reveal(<$fmt as Consistency>::consistent);
288                    reveal(<$fmt as SpecByteLen>::byte_len);
289                }
290                let inner = self.exec_inner();
291                inner.prepare(value)
292            }
293        }
294
295        impl ByteLen<$value> for $fmt {
296            fn length(&self, value: &$value) -> (result: usize) {
297                proof {
298                    reveal(<$fmt as SpecByteLen>::byte_len);
299                }
300                let inner = self.exec_inner();
301                inner.length(value)
302            }
303        }
304
305        } // verus!
306    };
307}
308
309#[doc(hidden)]
310#[macro_export]
311macro_rules! __impl_asn1_nominal_has_start {
312    (exact($constructed:expr), $fmt:ident) => {
313        $crate::__impl_asn1_nominal_has_start!(@certified $fmt, _this,
314            $crate::asn1::disjoint::asn1_start_exact_uint(_this.0, $constructed, _this.1));
315    };
316    (identity, $fmt:ident) => {
317        $crate::__impl_asn1_nominal_has_start!(@certified $fmt, _this,
318            $crate::asn1::disjoint::asn1_start_identity_uint(_this.0, _this.1));
319    };
320    (mask($domain:expr), $fmt:ident) => {
321        $crate::__impl_asn1_nominal_has_start!(@certified $fmt, _this, $domain);
322    };
323    (any, $fmt:ident) => {
324        $crate::__impl_asn1_nominal_has_start!(@certified $fmt, _this,
325            $crate::asn1::disjoint::asn1_start_any_non_eoc());
326    };
327    (@certified $fmt:ident, $this:ident, $domain:expr) => {
328        verus! {
329
330        impl $crate::asn1::disjoint::HasAsn1Start for $fmt {
331            #[verifier::inline]
332            open spec fn asn1_start(&self) -> $crate::asn1::disjoint::Asn1StartDomain {
333                let $this = self;
334                $domain
335            }
336
337            proof fn lemma_parse_implies_asn1_start(&self, input: Seq<u8>) {
338                self.lemma_schema_unambiguous();
339                reveal(<$fmt as SpecParser>::spec_parse);
340                self.spec_inner().lemma_parse_implies_asn1_start(input);
341            }
342        }
343
344        } // verus!
345    };
346    ($fmt:ident) => {
347        verus! {
348
349        impl $crate::asn1::disjoint::HasAsn1Start for $fmt {
350            #[verifier::inline]
351            open spec fn asn1_start(&self) -> $crate::asn1::disjoint::Asn1StartDomain {
352                self.spec_inner().asn1_start()
353            }
354
355            proof fn lemma_parse_implies_asn1_start(&self, input: Seq<u8>) {
356                reveal(<$fmt as SpecParser>::spec_parse);
357                self.spec_inner().lemma_parse_implies_asn1_start(input);
358            }
359        }
360
361        } // verus!
362    };
363}
364
365#[doc(hidden)]
366#[macro_export]
367macro_rules! __impl_asn1_nominal_tagged {
368    ($fmt:ident) => {
369        verus! {
370
371        impl Retaggable for $fmt {
372            #[verifier::inline]
373            open spec fn spec_retagged(&self, tag: Tag) -> Self {
374                Self(tag.class, $crate::asn1::tag::tag_num_to_uint(tag.number))
375            }
376
377            fn retagged(&self, tag: Tag) -> Self {
378                Self(tag.class, $crate::asn1::tag::tag_number_value(tag.number))
379            }
380        }
381
382        } // verus!
383    };
384}
385
386#[doc(hidden)]
387#[macro_export]
388macro_rules! __impl_asn1_nominal_der_tagged_proofs {
389    ($fmt:ident, $spec:ty $(, $forward:ty, $reverse:ty)?) => {
390        verus! {
391
392        impl $fmt {
393            proof fn lemma_successful_parse_inner_invariants(&self, input: Seq<u8>)
394                requires
395                    self.spec_parse(input) is Some,
396                ensures
397                    self.spec_inner().safe_inv(),
398                    self.spec_inner().sound_inv(),
399                    self.spec_inner().nonmal_inv(),
400            {
401                $(
402                    assert forall|input: <$forward as $crate::combinators::mapped::spec::SpecMap>::Input| #[trigger]
403                        self.spec_inner().inner.consistent(input) implies
404                            self.spec_inner().mapper.lossless(input) by {
405                        if self.spec_inner().inner.consistent(input) {
406                            <$spec>::lemma_into_from(input);
407                        }
408                    }
409                )?
410                reveal(<$fmt as SpecParser>::spec_parse);
411                reveal($fmt::spec_inner);
412                broadcast use $crate::asn1::tag::lemma_tag_wf_implies_tag_consistent;
413                self.spec_inner().lemma_parse_implies_asn1_start(input);
414                reveal($crate::asn1::disjoint::input_starts_with);
415                TagFmt.lemma_parse_sound_value(input);
416            }
417        }
418
419        impl SoundParser for $fmt {
420            proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
421                reveal(<$fmt as SpecParser>::spec_parse);
422                reveal(<$fmt as SpecByteLen>::byte_len);
423                if self.spec_parse(ibuf) is Some {
424                    self.lemma_successful_parse_inner_invariants(ibuf);
425                    self.spec_inner().lemma_parse_sound_consumption(ibuf);
426                }
427            }
428
429            proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
430                reveal(<$fmt as SpecParser>::spec_parse);
431                reveal(<$fmt as Consistency>::consistent);
432                if self.spec_parse(ibuf) is Some {
433                    self.lemma_successful_parse_inner_invariants(ibuf);
434                    self.spec_inner().lemma_parse_sound_value(ibuf);
435                }
436            }
437        }
438
439        impl NonMalleable for $fmt {
440            proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
441                reveal(<$fmt as SpecParser>::spec_parse);
442                if self.spec_parse(buf1) is Some && self.spec_parse(buf2) is Some {
443                    self.lemma_successful_parse_inner_invariants(buf1);
444                    self.spec_inner().lemma_parse_non_malleable(buf1, buf2);
445                }
446            }
447        }
448
449        } // verus!
450    };
451}
452
453#[doc(hidden)]
454#[macro_export]
455macro_rules! __impl_asn1_nominal_der_fixed_proofs {
456    ($fmt:ident, $spec:ty $(, $forward:ty, $reverse:ty)?) => {
457        verus! {
458
459        impl $fmt {
460            proof fn lemma_sound_nonmal_inv(&self)
461                ensures
462                    self.spec_inner().sound_inv(),
463                    self.spec_inner().nonmal_inv(),
464            {
465                $(
466                    assert forall|input: <$forward as $crate::combinators::mapped::spec::SpecMap>::Input| #[trigger]
467                        self.spec_inner().inner.consistent(input) implies
468                            self.spec_inner().mapper.lossless(input) by {
469                        if self.spec_inner().inner.consistent(input) {
470                            <$spec>::lemma_into_from(input);
471                        }
472                    }
473                )?
474                broadcast use $crate::asn1::tag::lemma_tag_wf_implies_tag_consistent;
475            }
476        }
477
478        impl SoundParser for $fmt {
479            proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
480                reveal(<$fmt as SpecParser>::spec_parse);
481                reveal(<$fmt as SpecByteLen>::byte_len);
482                self.lemma_sound_nonmal_inv();
483                self.spec_inner().lemma_parse_sound_consumption(ibuf);
484            }
485
486            proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
487                reveal(<$fmt as SpecParser>::spec_parse);
488                reveal(<$fmt as Consistency>::consistent);
489                self.lemma_sound_nonmal_inv();
490                self.spec_inner().lemma_parse_sound_value(ibuf);
491            }
492        }
493
494        impl NonMalleable for $fmt {
495            proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
496                reveal(<$fmt as SpecParser>::spec_parse);
497                self.lemma_sound_nonmal_inv();
498                self.spec_inner().lemma_parse_non_malleable(buf1, buf2);
499            }
500        }
501
502        } // verus!
503    };
504}
505
506#[doc(hidden)]
507#[macro_export]
508macro_rules! __impl_asn1_nominal_der_ord_borrowed {
509    ($fmt:ident, $inner:ty, $spec:ty, $value:ident $(, $forward:ty, $reverse:ty)?) => {
510        verus! {
511
512        impl DerState for $fmt {
513            type State = <$inner as DerState>::State;
514        }
515
516        impl<'i> DerOrd<$value<'i>> for $fmt {
517            proof fn lemma_der_serialize_len(&self, value: $spec) {
518                $(
519                    reveal(<$reverse as $crate::combinators::mapped::spec::SpecMap>::spec_map);
520                )?
521                reveal(<$fmt as Consistency>::consistent);
522                reveal(<$fmt as SpecSerializer>::spec_serialize);
523                reveal(<$fmt as SpecByteLen>::byte_len);
524                <$inner as DerOrd<$value<'i>>>::lemma_der_serialize_len(
525                    &self.spec_inner(),
526                    value,
527                );
528            }
529
530            open spec fn der_remaining(
531                &self,
532                value: $spec,
533                state: <Self as DerState>::State,
534            ) -> Seq<u8> {
535                <$inner as DerOrd<$value<'i>>>::der_remaining(&self.spec_inner(), value, state)
536            }
537
538            open spec fn der_state_valid(
539                &self,
540                value: $spec,
541                state: <Self as DerState>::State,
542            ) -> bool {
543                <$inner as DerOrd<$value<'i>>>::der_state_valid(&self.spec_inner(), value, state)
544            }
545
546            fn der_start(&self, value: &$value<'i>) -> (state: <Self as DerState>::State) {
547                proof {
548                    $(
549                        reveal(<$reverse as $crate::combinators::mapped::spec::SpecMap>::spec_map);
550                    )?
551                    reveal(<$fmt as Consistency>::consistent);
552                    reveal(<$fmt as SpecSerializer>::spec_serialize);
553                }
554                let inner = self.exec_inner();
555                <$inner as DerOrd<$value<'i>>>::der_start(&inner, value)
556            }
557
558            fn der_next(
559                &self,
560                value: &$value<'i>,
561                state: &mut <Self as DerState>::State,
562            ) -> (next: Option<u8>) {
563                proof {
564                    $(
565                        reveal(<$reverse as $crate::combinators::mapped::spec::SpecMap>::spec_map);
566                    )?
567                    reveal(<$fmt as Consistency>::consistent);
568                }
569                let inner = self.exec_inner();
570                <$inner as DerOrd<$value<'i>>>::der_next(&inner, value, state)
571            }
572        }
573
574        } // verus!
575    };
576}
577
578#[doc(hidden)]
579#[macro_export]
580macro_rules! __impl_asn1_nominal_der_ord_owned {
581    ($fmt:ident, $inner:ty, $spec:ty, $value:ty $(, $forward:ty, $reverse:ty)?) => {
582        verus! {
583
584        impl DerState for $fmt {
585            type State = <$inner as DerState>::State;
586        }
587
588        impl DerOrd<$value> for $fmt {
589            proof fn lemma_der_serialize_len(&self, value: $spec) {
590                $(
591                    reveal(<$reverse as $crate::combinators::mapped::spec::SpecMap>::spec_map);
592                )?
593                reveal(<$fmt as Consistency>::consistent);
594                reveal(<$fmt as SpecSerializer>::spec_serialize);
595                reveal(<$fmt as SpecByteLen>::byte_len);
596                <$inner as DerOrd<$value>>::lemma_der_serialize_len(&self.spec_inner(), value);
597            }
598
599            open spec fn der_remaining(
600                &self,
601                value: $spec,
602                state: <Self as DerState>::State,
603            ) -> Seq<u8> {
604                <$inner as DerOrd<$value>>::der_remaining(&self.spec_inner(), value, state)
605            }
606
607            open spec fn der_state_valid(
608                &self,
609                value: $spec,
610                state: <Self as DerState>::State,
611            ) -> bool {
612                <$inner as DerOrd<$value>>::der_state_valid(&self.spec_inner(), value, state)
613            }
614
615            fn der_start(&self, value: &$value) -> (state: <Self as DerState>::State) {
616                proof {
617                    $(
618                        reveal(<$reverse as $crate::combinators::mapped::spec::SpecMap>::spec_map);
619                    )?
620                    reveal(<$fmt as Consistency>::consistent);
621                    reveal(<$fmt as SpecSerializer>::spec_serialize);
622                }
623                let inner = self.exec_inner();
624                <$inner as DerOrd<$value>>::der_start(&inner, value)
625            }
626
627            fn der_next(
628                &self,
629                value: &$value,
630                state: &mut <Self as DerState>::State,
631            ) -> (next: Option<u8>) {
632                proof {
633                    $(
634                        reveal(<$reverse as $crate::combinators::mapped::spec::SpecMap>::spec_map);
635                    )?
636                    reveal(<$fmt as Consistency>::consistent);
637                }
638                let inner = self.exec_inner();
639                <$inner as DerOrd<$value>>::der_next(&inner, value, state)
640            }
641        }
642
643        } // verus!
644    };
645}
646
647/// Implements the verified DER traits and executable APIs for a generated nominal format.
648#[macro_export]
649macro_rules! impl_der {
650    ($kind:ident $(($constructed:expr))?, borrowed, $fmt:ident, $inner:ty, $spec:ty, $value:ident $(, $forward:ty, $reverse:ty)?) => {
651        $crate::__impl_asn1_nominal_inner!($kind $(($constructed))?, $fmt, $inner);
652        $crate::__impl_asn1_nominal_specs_and_proofs!($fmt, $spec);
653        $crate::__impl_asn1_nominal_exec_borrowed!($fmt, $value);
654        $crate::__impl_asn1_nominal_der_ord_borrowed!($fmt, $inner, $spec, $value $(, $forward, $reverse)?);
655        $crate::impl_der!(@kind $kind $(($constructed))?, $fmt, $spec $(, $forward, $reverse)?);
656    };
657    ($kind:ident $(($constructed:expr))?, owned, $fmt:ident, $inner:ty, $spec:ty, $value:ty $(, $forward:ty, $reverse:ty)?) => {
658        $crate::__impl_asn1_nominal_inner!($kind $(($constructed))?, $fmt, $inner);
659        $crate::__impl_asn1_nominal_specs_and_proofs!($fmt, $spec);
660        $crate::__impl_asn1_nominal_exec_owned!($fmt, $value);
661        $crate::__impl_asn1_nominal_der_ord_owned!($fmt, $inner, $spec, $value $(, $forward, $reverse)?);
662        $crate::impl_der!(@kind $kind $(($constructed))?, $fmt, $spec $(, $forward, $reverse)?);
663    };
664    (@kind tagged($constructed:expr), $fmt:ident, $spec:ty $(, $forward:ty, $reverse:ty)?) => {
665        $crate::__impl_asn1_nominal_has_start!($fmt);
666        $crate::__impl_asn1_nominal_tagged!($fmt);
667        $crate::__impl_asn1_nominal_der_tagged_proofs!($fmt, $spec $(, $forward, $reverse)?);
668    };
669    (@kind tagged_exact($constructed:expr), $fmt:ident, $spec:ty $(, $forward:ty, $reverse:ty)?) => {
670        $crate::__impl_asn1_nominal_has_start!(exact($constructed), $fmt);
671        $crate::__impl_asn1_nominal_tagged!($fmt);
672        $crate::__impl_asn1_nominal_der_tagged_proofs!($fmt, $spec $(, $forward, $reverse)?);
673    };
674    (@kind tagged_identity($constructed:expr), $fmt:ident, $spec:ty $(, $forward:ty, $reverse:ty)?) => {
675        $crate::__impl_asn1_nominal_has_start!(identity, $fmt);
676        $crate::__impl_asn1_nominal_tagged!($fmt);
677        $crate::__impl_asn1_nominal_der_tagged_proofs!($fmt, $spec $(, $forward, $reverse)?);
678    };
679    (@kind untagged_mask($domain:expr), $fmt:ident, $spec:ty $(, $forward:ty, $reverse:ty)?) => {
680        $crate::__impl_asn1_nominal_has_start!(mask($domain), $fmt);
681        $crate::__impl_asn1_nominal_der_fixed_proofs!($fmt, $spec $(, $forward, $reverse)?);
682    };
683    (@kind untagged_any, $fmt:ident, $spec:ty $(, $forward:ty, $reverse:ty)?) => {
684        $crate::__impl_asn1_nominal_has_start!(any, $fmt);
685        $crate::__impl_asn1_nominal_der_fixed_proofs!($fmt, $spec $(, $forward, $reverse)?);
686    };
687    (@kind untagged_start, $fmt:ident, $spec:ty $(, $forward:ty, $reverse:ty)?) => {
688        $crate::__impl_asn1_nominal_has_start!($fmt);
689        $crate::__impl_asn1_nominal_der_fixed_proofs!($fmt, $spec $(, $forward, $reverse)?);
690    };
691    (@kind untagged, $fmt:ident, $spec:ty $(, $forward:ty, $reverse:ty)?) => {
692        $crate::__impl_asn1_nominal_der_fixed_proofs!($fmt, $spec $(, $forward, $reverse)?);
693    };
694}
695
696/// Implements the verified BER traits and executable APIs for a generated nominal format.
697///
698/// BER formats deliberately do not implement `SoundParser`, `NonMalleable`, or DER ordering.
699#[macro_export]
700macro_rules! impl_ber {
701    ($kind:ident $(($constructed:expr))?, borrowed, $fmt:ident, $inner:ty, $spec:ty, $value:ident $(, $forward:ty, $reverse:ty)?) => {
702        $crate::__impl_asn1_nominal_inner!($kind $(($constructed))?, $fmt, $inner);
703        $crate::__impl_asn1_nominal_specs_and_proofs!($fmt, $spec);
704        $crate::__impl_asn1_nominal_exec_borrowed!($fmt, $value);
705        $crate::impl_ber!(@kind $kind $(($constructed))?, $fmt);
706    };
707    ($kind:ident $(($constructed:expr))?, owned, $fmt:ident, $inner:ty, $spec:ty, $value:ty $(, $forward:ty, $reverse:ty)?) => {
708        $crate::__impl_asn1_nominal_inner!($kind $(($constructed))?, $fmt, $inner);
709        $crate::__impl_asn1_nominal_specs_and_proofs!($fmt, $spec);
710        $crate::__impl_asn1_nominal_exec_owned!($fmt, $value);
711        $crate::impl_ber!(@kind $kind $(($constructed))?, $fmt);
712    };
713    (@kind tagged($constructed:expr), $fmt:ident) => {
714        $crate::__impl_asn1_nominal_has_start!($fmt);
715        $crate::__impl_asn1_nominal_tagged!($fmt);
716    };
717    (@kind tagged_exact($constructed:expr), $fmt:ident) => {
718        $crate::__impl_asn1_nominal_has_start!(exact($constructed), $fmt);
719        $crate::__impl_asn1_nominal_tagged!($fmt);
720    };
721    (@kind tagged_identity($constructed:expr), $fmt:ident) => {
722        $crate::__impl_asn1_nominal_has_start!(identity, $fmt);
723        $crate::__impl_asn1_nominal_tagged!($fmt);
724    };
725    (@kind untagged_mask($domain:expr), $fmt:ident) => {
726        $crate::__impl_asn1_nominal_has_start!(mask($domain), $fmt);
727    };
728    (@kind untagged_any, $fmt:ident) => {
729        $crate::__impl_asn1_nominal_has_start!(any, $fmt);
730    };
731    (@kind untagged_start, $fmt:ident) => {
732        $crate::__impl_asn1_nominal_has_start!($fmt);
733    };
734    (@kind untagged, $fmt:ident) => {};
735}
736
737// `#[macro_export]` places macros at the crate root. Re-export them here as well so callers can
738// discover and import them through `vest_lib::asn1::macros`.
739pub use crate::{impl_ber, impl_der};
vest_lib/asn1/macros/mod.rs

vest_lib/asn1/macros/
mod.rs
