vest_lib/asn1/
modifiers.rs

1//! Shared ASN.1 component modifiers and notation constructors.
2use crate::asn1::ber::{
3    BerBitStringFmt, BerCharStringFmt, BerOctetStringFmt, BerSequenceFmt, BerSequenceOfFmt,
4};
5use crate::asn1::tag::Class;
6use crate::asn1::{ASN1Fmt, Tag};
7use crate::combinators::mapped::spec::{FnSpecMapper, SpecMapper};
8use crate::combinators::{Choice, Mapped, Optional, Pair, Ref, Refined};
9use crate::core::exec::output::*;
10use crate::core::exec::{
11    input::{InputBuf, InputSlice},
12    parser::{PResult, Parser},
13    serializer::{ByteLen, PreSerializeError, Prepare, Serializer},
14    ParseError,
15};
16use crate::core::{proof::*, spec::*};
17use vstd::prelude::*;
18use OutputBuf;
19
20verus! {
21
22/// Formats whose outer ASN.1 tag can be replaced without changing their semantic value.
23///
24/// The replacement's class and number are authoritative; each format determines the
25/// primitive/constructed bit required by its own wire representation.
26pub trait Retaggable: Copy {
27    spec fn spec_retagged(&self, tag: Tag) -> Self;
28
29    fn retagged(&self, tag: Tag) -> (retagged: Self)
30        returns
31            self.spec_retagged(tag),
32    ;
33}
34
35/// Const-constructible ASN.1 IMPLICIT tagging wrapper.
36#[derive(Copy)]
37pub struct ImplicitlyTaggedFmt<F>(pub Tag, pub F);
38
39impl<F: Clone> Clone for ImplicitlyTaggedFmt<F> {
40    fn clone(&self) -> (cloned: Self)
41        ensures
42            cloned.0 == self.0,
43            call_ensures(F::clone, (&self.1,), cloned.1),
44    {
45        Self(self.0, self.1.clone())
46    }
47}
48
49/// Supports IMPLICIT tagging of an ordinary ASN.1 TLV.
50///
51/// Retagging replaces the tag class and number, preserves the base format's primitive/constructed
52/// form, and leaves its content format unchanged.
53impl<C: Copy, const DER: bool> Retaggable for ASN1Fmt<C, DER> {
54    open spec fn spec_retagged(&self, tag: Tag) -> Self {
55        ASN1Fmt(
56            Tag { class: tag.class, constructed: self.0.constructed, number: tag.number },
57            self.1,
58        )
59    }
60
61    fn retagged(&self, tag: Tag) -> Self {
62        ASN1Fmt(
63            Tag { class: tag.class, constructed: self.0.constructed, number: tag.number },
64            self.1,
65        )
66    }
67}
68
69/// Supports IMPLICIT tagging of a BER `SEQUENCE` or EXPLICIT wrapper without losing its
70/// definite/indefinite-length framing.
71///
72/// Retagging replaces the tag class and number, forces the required constructed form, and
73/// preserves the schema-defined content format.
74impl<C: Copy> Retaggable for BerSequenceFmt<C> {
75    open spec fn spec_retagged(&self, tag: Tag) -> Self {
76        Self(Tag { class: tag.class, constructed: true, number: tag.number }, self.1)
77    }
78
79    fn retagged(&self, tag: Tag) -> Self {
80        Self(Tag { class: tag.class, constructed: true, number: tag.number }, self.1)
81    }
82}
83
84/// Supports IMPLICIT tagging of a BER `SEQUENCE OF`/`SET OF` while retaining its specialized
85/// definite/indefinite-length handling.
86///
87/// Retagging replaces the tag class and number, forces the required constructed form, and
88/// preserves the element format.
89impl<C: Copy> Retaggable for BerSequenceOfFmt<C> {
90    open spec fn spec_retagged(&self, tag: Tag) -> Self {
91        Self(Tag { class: tag.class, constructed: true, number: tag.number }, self.1)
92    }
93
94    fn retagged(&self, tag: Tag) -> Self {
95        Self(Tag { class: tag.class, constructed: true, number: tag.number }, self.1)
96    }
97}
98
99/// Supports IMPLICIT tagging of recursive BER OCTET STRING values.
100///
101/// The stored tag is normalized to the primitive form with the replacement class and number; this
102/// is fine since the parser permits both primitive and constructed forms.
103/// Recursive fragments keep universal tag 4 (see [`BerOctetStringFmt`]).
104impl<const LIMIT: usize> Retaggable for BerOctetStringFmt<LIMIT> {
105    open spec fn spec_retagged(&self, tag: Tag) -> Self {
106        Self(Tag { class: tag.class, constructed: false, number: tag.number })
107    }
108
109    fn retagged(&self, tag: Tag) -> Self {
110        Self(Tag { class: tag.class, constructed: false, number: tag.number })
111    }
112}
113
114/// Supports IMPLICIT tagging of recursive BER BIT STRING values.
115///
116/// The outer identity is replaced and normalized to primitive form; parsing still accepts both
117/// primitive and constructed forms, while nested fragments retain universal tag 3.
118impl<const LIMIT: usize> Retaggable for BerBitStringFmt<LIMIT> {
119    open spec fn spec_retagged(&self, tag: Tag) -> Self {
120        Self(Tag { class: tag.class, constructed: false, number: tag.number })
121    }
122
123    fn retagged(&self, tag: Tag) -> Self {
124        Self(Tag { class: tag.class, constructed: false, number: tag.number })
125    }
126}
127
128/// Supports IMPLICIT tagging of a BER restricted character string layered over OCTET STRING.
129///
130/// The outer tag is normalized to the primitive form with the replacement class and number,
131/// while OCTET STRING fragment tags, the character-content format, and the recursion limit are
132/// preserved.
133impl<C: Copy, const LIMIT: usize> Retaggable for BerCharStringFmt<C, LIMIT> {
134    open spec fn spec_retagged(&self, tag: Tag) -> Self {
135        Self(Tag { class: tag.class, constructed: false, number: tag.number }, self.1)
136    }
137
138    fn retagged(&self, tag: Tag) -> Self {
139        Self(Tag { class: tag.class, constructed: false, number: tag.number }, self.1)
140    }
141}
142
143/// Allows IMPLICIT tagging to compose/chain through an existing IMPLICIT-tag wrapper.
144///
145/// The newer tag replaces the stored outer tag and the underlying format is retained; when used,
146/// the underlying [`Retaggable`] implementation selects the correct primitive/constructed form.
147impl<F: Retaggable> Retaggable for ImplicitlyTaggedFmt<F> {
148    open spec fn spec_retagged(&self, tag: Tag) -> Self {
149        Self(tag, self.1)
150    }
151
152    fn retagged(&self, tag: Tag) -> Self {
153        Self(tag, self.1)
154    }
155}
156
157/// Allows a value constraint to remain attached when its underlying ASN.1 format is retagged.
158///
159/// Retagging is delegated to the inner format and the refinement predicate is preserved.
160impl<F, P> Retaggable for Refined<F, P> where F: Retaggable, P: Copy {
161    open spec fn spec_retagged(&self, tag: Tag) -> Self {
162        Refined(self.0.spec_retagged(tag), self.1)
163    }
164
165    fn retagged(&self, tag: Tag) -> Self {
166        Refined(self.0.retagged(tag), self.1)
167    }
168}
169
170/// Allows a semantic mapping to remain attached when its underlying ASN.1 format is retagged.
171///
172/// Retagging is delegated to the inner format and the mapper is preserved.
173impl<F, M> Retaggable for Mapped<F, M> where F: Retaggable, M: Copy {
174    open spec fn spec_retagged(&self, tag: Tag) -> Self {
175        Mapped { inner: self.inner.spec_retagged(tag), mapper: self.mapper }
176    }
177
178    fn retagged(&self, tag: Tag) -> Self {
179        Mapped { inner: self.inner.retagged(tag), mapper: self.mapper }
180    }
181}
182
183/// Allows references to retaggable formats to pass transparently through IMPLICIT tagging.
184///
185/// Retagging is delegated to the referenced format and the result remains wrapped in [`Ref`].
186impl<F> Retaggable for Ref<F> where F: Retaggable {
187    open spec fn spec_retagged(&self, tag: Tag) -> Self {
188        Ref(self.0.spec_retagged(tag))
189    }
190
191    fn retagged(&self, tag: Tag) -> Self {
192        Ref(self.0.retagged(tag))
193    }
194}
195
196mod implicit_specs {
197    use super::*;
198
199    impl<F> SpecParser for ImplicitlyTaggedFmt<F> where F: Retaggable + SpecParser {
200        type PVal = <F as SpecParser>::PVal;
201
202        open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
203            self.1.spec_retagged(self.0).spec_parse(ibuf)
204        }
205    }
206
207    impl<F> Consistency for ImplicitlyTaggedFmt<F> where F: Retaggable + Consistency {
208        type Val = <F as Consistency>::Val;
209
210        open spec fn consistent(&self, value: Self::Val) -> bool {
211            self.1.spec_retagged(self.0).consistent(value)
212        }
213    }
214
215    impl<F> SpecSerializerDps for ImplicitlyTaggedFmt<F> where F: Retaggable + SpecSerializerDps {
216        type SValue = <F as SpecSerializerDps>::SValue;
217
218        open spec fn spec_serialize_dps(&self, value: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
219            self.1.spec_retagged(self.0).spec_serialize_dps(value, obuf)
220        }
221    }
222
223    impl<F> SpecSerializer for ImplicitlyTaggedFmt<F> where F: Retaggable + SpecSerializer {
224        type SVal = <F as SpecSerializer>::SVal;
225
226        open spec fn spec_serialize(&self, value: Self::SVal) -> Seq<u8> {
227            self.1.spec_retagged(self.0).spec_serialize(value)
228        }
229    }
230
231    impl<F> SpecByteLen for ImplicitlyTaggedFmt<F> where F: Retaggable + SpecByteLen {
232        type T = <F as SpecByteLen>::T;
233
234        open spec fn byte_len(&self, value: Self::T) -> nat {
235            self.1.spec_retagged(self.0).byte_len(value)
236        }
237    }
238
239}
240
241mod implicit_proofs {
242    use super::*;
243
244    impl<F> SafeParser for ImplicitlyTaggedFmt<F> where F: Retaggable + SafeParser {
245        open spec fn safe_inv(&self) -> bool {
246            self.1.spec_retagged(self.0).safe_inv()
247        }
248
249        proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
250            self.1.spec_retagged(self.0).lemma_parse_safe(ibuf);
251        }
252    }
253
254    impl<F> Productive for ImplicitlyTaggedFmt<F> where F: Retaggable + Productive {
255        open spec fn productive_inv(&self) -> bool {
256            self.1.spec_retagged(self.0).productive_inv()
257        }
258
259        proof fn lemma_productive(&self, ibuf: Seq<u8>) {
260            self.1.spec_retagged(self.0).lemma_productive(ibuf);
261        }
262    }
263
264    impl<F> SoundParser for ImplicitlyTaggedFmt<F> where F: Retaggable + SoundParser {
265        open spec fn sound_inv(&self) -> bool {
266            self.1.spec_retagged(self.0).sound_inv()
267        }
268
269        proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
270            self.1.spec_retagged(self.0).lemma_parse_sound_consumption(ibuf);
271        }
272
273        proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
274            self.1.spec_retagged(self.0).lemma_parse_sound_value(ibuf);
275        }
276    }
277
278    impl<F> NonTailFmt for ImplicitlyTaggedFmt<F> where F: Retaggable + NonTailFmt {
279        open spec fn serialize_dps_inv(&self) -> bool {
280            self.1.spec_retagged(self.0).serialize_dps_inv()
281        }
282
283        proof fn lemma_serialize_dps_prepend(&self, value: Self::SValue, obuf: Seq<u8>) {
284            self.1.spec_retagged(self.0).lemma_serialize_dps_prepend(value, obuf);
285        }
286
287        proof fn lemma_serialize_dps_len(&self, value: Self::SValue, obuf: Seq<u8>) {
288            self.1.spec_retagged(self.0).lemma_serialize_dps_len(value, obuf);
289        }
290    }
291
292    impl<F> GoodSerializer for ImplicitlyTaggedFmt<F> where F: Retaggable + GoodSerializer {
293        open spec fn serialize_inv(&self) -> bool {
294            self.1.spec_retagged(self.0).serialize_inv()
295        }
296
297        proof fn lemma_serialize_len(&self, value: Self::SVal) {
298            self.1.spec_retagged(self.0).lemma_serialize_len(value);
299        }
300    }
301
302    impl<F> SPRoundTripDps for ImplicitlyTaggedFmt<F> where F: Retaggable + SPRoundTripDps {
303        open spec fn unambiguous(&self) -> bool {
304            self.1.spec_retagged(self.0).unambiguous()
305        }
306
307        proof fn theorem_serialize_dps_parse_roundtrip(&self, value: Self::T, obuf: Seq<u8>) {
308            self.1.spec_retagged(self.0).theorem_serialize_dps_parse_roundtrip(value, obuf);
309        }
310    }
311
312    impl<F> NonMalleable for ImplicitlyTaggedFmt<F> where F: Retaggable + NonMalleable {
313        open spec fn nonmal_inv(&self) -> bool {
314            self.1.spec_retagged(self.0).nonmal_inv()
315        }
316
317        proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
318            self.1.spec_retagged(self.0).lemma_parse_non_malleable(buf1, buf2);
319        }
320    }
321
322    impl<F> NoLookAhead for ImplicitlyTaggedFmt<F> where F: Retaggable + NoLookAhead {
323        open spec fn no_lookahead_inv(&self) -> bool {
324            self.1.spec_retagged(self.0).no_lookahead_inv()
325        }
326
327        proof fn lemma_no_lookahead(&self, ibuf1: Seq<u8>, ibuf2: Seq<u8>) {
328            self.1.spec_retagged(self.0).lemma_no_lookahead(ibuf1, ibuf2);
329        }
330    }
331
332    impl<F> EquivSerializersGeneral for ImplicitlyTaggedFmt<F> where
333        F: Retaggable + EquivSerializersGeneral,
334     {
335        open spec fn equiv_general_inv(&self) -> bool {
336            self.1.spec_retagged(self.0).equiv_general_inv()
337        }
338
339        proof fn lemma_serialize_equiv(&self, value: Self::SVal, obuf: Seq<u8>) {
340            self.1.spec_retagged(self.0).lemma_serialize_equiv(value, obuf);
341        }
342    }
343
344    impl<F> EquivSerializers for ImplicitlyTaggedFmt<F> where F: Retaggable + EquivSerializers {
345        open spec fn equiv_inv(&self) -> bool {
346            self.1.spec_retagged(self.0).equiv_inv()
347        }
348
349        proof fn lemma_serialize_equiv_on_empty(&self, value: Self::SVal) {
350            self.1.spec_retagged(self.0).lemma_serialize_equiv_on_empty(value);
351        }
352    }
353
354}
355
356impl<Input, F> Parser<Input> for ImplicitlyTaggedFmt<F> where
357    Input: InputBuf,
358    F: Retaggable + Parser<Input>,
359 {
360    type PT = <F as Parser<Input>>::PT;
361
362    open spec fn exec_inv(&self) -> bool {
363        <F as Parser<Input>>::exec_inv(&self.1.spec_retagged(self.0))
364    }
365
366    fn parse(&self, ibuf: &Input) -> PResult<Self::PT> {
367        self.1.retagged(self.0).parse(ibuf)
368    }
369}
370
371impl<Output, F, T> Serializer<Output, T> for ImplicitlyTaggedFmt<F> where
372    Output: OutputBuf,
373    T: DeepView + ?Sized,
374    F: Retaggable + Serializer<Output, T>,
375 {
376    #[verifier::prophetic]
377    open spec fn exec_inv(&self) -> bool {
378        <F as Serializer<Output, T>>::exec_inv(&self.1.spec_retagged(self.0))
379    }
380
381    fn serialize_into(&self, value: &T, obuf: &mut Output) {
382        self.1.retagged(self.0).serialize_into(value, obuf)
383    }
384}
385
386impl<F, T> Prepare<T> for ImplicitlyTaggedFmt<F> where
387    T: DeepView + ?Sized,
388    F: Retaggable + Prepare<T>,
389 {
390    open spec fn exec_inv(&self) -> bool {
391        <F as Prepare<T>>::exec_inv(&self.1.spec_retagged(self.0))
392    }
393
394    fn prepare(&self, value: &T) -> Result<usize, PreSerializeError> {
395        self.1.retagged(self.0).prepare(value)
396    }
397}
398
399impl<F, T> ByteLen<T> for ImplicitlyTaggedFmt<F> where
400    T: DeepView + ?Sized,
401    F: Retaggable + ByteLen<T>,
402 {
403    open spec fn exec_inv(&self) -> bool {
404        <F as ByteLen<T>>::exec_inv(&self.1.spec_retagged(self.0))
405    }
406
407    fn length(&self, value: &T) -> usize {
408        self.1.retagged(self.0).length(value)
409    }
410}
411
412/// Rule-independent format type produced by ASN.1 IMPLICIT tagging.
413pub type ImplicitFmt<F> = ImplicitlyTaggedFmt<F>;
414
415/// Apply an ASN.1 IMPLICIT tag with an arbitrary tag class.
416///
417/// The supplied tag's constructed bit is only a placeholder: the concrete [`Retaggable`]
418/// implementation preserves or selects the encoding form required by the base format.
419#[allow(non_snake_case)]
420#[verifier::allow_in_spec]
421pub const fn implicitly_tagged<C: Copy>(class: Class, number: u64, inner: C) -> ImplicitFmt<C>
422    returns
423        ImplicitlyTaggedFmt(
424            Tag { class, constructed: false, number: super::tag::tag_num_from_uint(number) },
425            inner,
426        ),
427{
428    ImplicitlyTaggedFmt(
429        Tag { class, constructed: false, number: super::tag::tag_num_from_uint(number) },
430        inner,
431    )
432}
433
434/// Apply a context-specific ASN.1 IMPLICIT tag.
435#[allow(non_snake_case)]
436#[verifier::allow_in_spec]
437pub const fn IMPLICIT<C: Copy>(number: u64, inner: C) -> ImplicitFmt<C>
438    returns
439        implicitly_tagged(Class::ContextSpecific, number, inner),
440{
441    implicitly_tagged(Class::ContextSpecific, number, inner)
442}
443
444/// Apply an application-class ASN.1 IMPLICIT tag.
445#[allow(non_snake_case)]
446#[verifier::allow_in_spec]
447pub const fn IMPLICIT_APPLICATION<C: Copy>(number: u64, inner: C) -> ImplicitFmt<C>
448    returns
449        implicitly_tagged(Class::Application, number, inner),
450{
451    implicitly_tagged(Class::Application, number, inner)
452}
453
454/// Apply a private-class ASN.1 IMPLICIT tag.
455#[allow(non_snake_case)]
456#[verifier::allow_in_spec]
457pub const fn IMPLICIT_PRIVATE<C: Copy>(number: u64, inner: C) -> ImplicitFmt<C>
458    returns
459        implicitly_tagged(Class::Private, number, inner),
460{
461    implicitly_tagged(Class::Private, number, inner)
462}
463
464/// Construct an ASN.1 OPTIONAL component with its continuation.
465#[allow(non_snake_case)]
466#[verifier::allow_in_spec]
467pub const fn OPTIONAL<Field, Rest>(field: Field, rest: Rest) -> Optional<Field, Rest>
468    returns
469        Optional(field, rest),
470{
471    Optional(field, rest)
472}
473
474/// Construct a required ASN.1 component with its continuation.
475#[allow(non_snake_case)]
476#[verifier::allow_in_spec]
477pub const fn REQUIRED<Field, Rest>(field: Field, rest: Rest) -> Pair<Field, Rest>
478    returns
479        Pair(field, rest),
480{
481    Pair(field, rest)
482}
483
484/// Construct a binary ASN.1 CHOICE.
485#[allow(non_snake_case)]
486#[verifier::allow_in_spec]
487pub const fn CHOICE<Left, Right>(left: Left, right: Right) -> Choice<Left, Right>
488    returns
489        Choice(left, right),
490{
491    Choice(left, right)
492}
493
494/// Construct the outer tag used by ASN.1 EXPLICIT tagging.
495#[verifier::allow_in_spec]
496pub const fn explicit_tag(class: Class, number: u64) -> Tag
497    returns
498        (Tag { class, constructed: true, number: super::tag::tag_num_from_uint(number) }),
499{
500    Tag { class, constructed: true, number: super::tag::tag_num_from_uint(number) }
501}
502
503/// ASN.1 DEFAULT component with continuation.
504///
505/// The semantic value always contains the component value. On parsing, absence
506/// is replaced by `default`. On serialization, a value equal to `default` is
507/// omitted. DER additionally rejects an explicitly encoded default value.
508#[derive(Copy)]
509pub struct DefaultedFmt<Field, Default, Rest, const DER: bool = true>(
510    pub Field,
511    pub Default,
512    pub Rest,
513);
514
515/// Construct an ASN.1 DEFAULT component for the selected encoding rules.
516#[verifier::allow_in_spec]
517pub const fn defaulted<Field, Rest, const DER: bool>(
518    field: Field,
519    default: Field::T,
520    rest: Rest,
521) -> DefaultedFmt<Field, Field::T, Rest, DER> where Field: SpecByteLen
522    returns
523        DefaultedFmt::<Field, Field::T, Rest, DER>(field, default, rest),
524{
525    DefaultedFmt::<Field, Field::T, Rest, DER>(field, default, rest)
526}
527
528impl<Field: Clone, Default: Clone, Rest: Clone, const DER: bool> Clone for DefaultedFmt<
529    Field,
530    Default,
531    Rest,
532    DER,
533> {
534    fn clone(&self) -> (cloned: Self)
535        ensures
536            call_ensures(Field::clone, (&self.0,), cloned.0),
537            call_ensures(Default::clone, (&self.1,), cloned.1),
538            call_ensures(Rest::clone, (&self.2,), cloned.2),
539    {
540        DefaultedFmt(self.0.clone(), self.1.clone(), self.2.clone())
541    }
542}
543
544pub type DefaultedInnerFmt<Field, Rest, T, U, const DER: bool> = Mapped<
545    Refined<Optional<Field, Rest>, PredFnSpec<(Option<T>, U)>>,
546    FnSpecMapper<(Option<T>, U), (T, U)>,
547>;
548
549pub open spec fn defaulted_fmt<Field: SpecByteLen, Rest: SpecByteLen, const DER: bool>(
550    field: Field,
551    default: Field::T,
552    rest: Rest,
553) -> DefaultedInnerFmt<Field, Rest, Field::T, Rest::T, DER> {
554    Mapped {
555        inner: Refined(
556            Optional(field, rest),
557            |pair: (Option<Field::T>, Rest::T)|
558                DER ==> (pair matches (Some(value), _) ==> value != default),
559        ),
560        mapper: (
561            |parsed: (Option<Field::T>, Rest::T)|
562                (
563                    match parsed.0 {
564                        Some(value) => value,
565                        None => default,
566                    },
567                    parsed.1,
568                ),
569            |value: (Field::T, Rest::T)|
570                (
571                    if value.0 == default {
572                        None
573                    } else {
574                        Some(value.0)
575                    },
576                    value.1,
577                ),
578        ),
579    }
580}
581
582mod derived_specs {
583    use super::*;
584
585    impl<Field, Rest, const DER: bool> SpecParser for DefaultedFmt<
586        Field,
587        Field::PVal,
588        Rest,
589        DER,
590    > where
591        Field: SpecByteLen + SpecParser<PVal = Field::T>,
592        Rest: SpecByteLen + SpecParser<PVal = Rest::T>,
593     {
594        type PVal = (Field::PVal, Rest::PVal);
595
596        open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
597            defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).spec_parse(ibuf)
598        }
599    }
600
601    impl<Field, Rest, const DER: bool> Consistency for DefaultedFmt<
602        Field,
603        Field::Val,
604        Rest,
605        DER,
606    > where
607        Field: SpecByteLen + Consistency<Val = Field::T>,
608        Rest: SpecByteLen + Consistency<Val = Rest::T>,
609     {
610        type Val = (Field::Val, Rest::Val);
611
612        open spec fn consistent(&self, v: Self::Val) -> bool {
613            defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).consistent(v)
614        }
615    }
616
617    impl<Field, Rest, const DER: bool> SpecSerializerDps for DefaultedFmt<
618        Field,
619        Field::SValue,
620        Rest,
621        DER,
622    > where
623        Field: SpecByteLen + SpecSerializerDps<SValue = Field::T>,
624        Rest: SpecByteLen + SpecSerializerDps<SValue = Rest::T>,
625     {
626        type SValue = (Field::SValue, Rest::SValue);
627
628        open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
629            defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).spec_serialize_dps(v, obuf)
630        }
631    }
632
633    impl<Field, Rest, const DER: bool> SpecSerializer for DefaultedFmt<
634        Field,
635        Field::SVal,
636        Rest,
637        DER,
638    > where
639        Field: SpecByteLen + SpecSerializer<SVal = Field::T>,
640        Rest: SpecByteLen + SpecSerializer<SVal = Rest::T>,
641     {
642        type SVal = (Field::SVal, Rest::SVal);
643
644        open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
645            defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).spec_serialize(v)
646        }
647    }
648
649    impl<Field, Rest, const DER: bool> SpecByteLen for DefaultedFmt<
650        Field,
651        Field::T,
652        Rest,
653        DER,
654    > where Field: SpecByteLen, Rest: SpecByteLen {
655        type T = (Field::T, Rest::T);
656
657        open spec fn byte_len(&self, v: Self::T) -> nat {
658            defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).byte_len(v)
659        }
660    }
661
662}
663
664mod derived_proofs {
665    use super::*;
666
667    impl<Field, Rest, const DER: bool> SafeParser for DefaultedFmt<
668        Field,
669        Field::PVal,
670        Rest,
671        DER,
672    > where
673        Field: SpecByteLen + SafeParser<PVal = Field::T>,
674        Rest: SpecByteLen + SafeParser<PVal = Rest::T>,
675     {
676        open spec fn safe_inv(&self) -> bool {
677            defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).safe_inv()
678        }
679
680        proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
681            defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).lemma_parse_safe(ibuf);
682        }
683    }
684
685    impl<Field, Rest, const DER: bool> Productive for DefaultedFmt<
686        Field,
687        Field::PVal,
688        Rest,
689        DER,
690    > where
691        Field: SpecByteLen + Productive<PVal = Field::T>,
692        Rest: SpecByteLen + Productive<PVal = Rest::T>,
693     {
694        open spec fn productive_inv(&self) -> bool {
695            defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).productive_inv()
696        }
697
698        proof fn lemma_productive(&self, s: Seq<u8>) {
699            defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).lemma_productive(s);
700        }
701    }
702
703    impl<Field, Rest, const DER: bool> SoundParser for DefaultedFmt<
704        Field,
705        Field::PVal,
706        Rest,
707        DER,
708    > where Field: SoundParser, Rest: SoundParser {
709        open spec fn sound_inv(&self) -> bool {
710            defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).sound_inv()
711        }
712
713        proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
714            defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).lemma_parse_sound_consumption(
715                ibuf,
716            );
717        }
718
719        proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
720            defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).lemma_parse_sound_value(ibuf);
721        }
722    }
723
724    impl<Field, Rest, const DER: bool> NonTailFmt for DefaultedFmt<
725        Field,
726        Field::SValue,
727        Rest,
728        DER,
729    > where Field: NonTailFmt, Rest: NonTailFmt {
730        open spec fn serialize_dps_inv(&self) -> bool {
731            defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).serialize_dps_inv()
732        }
733
734        proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>) {
735            defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).lemma_serialize_dps_prepend(
736                v,
737                obuf,
738            );
739        }
740
741        proof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>) {
742            defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).lemma_serialize_dps_len(
743                v,
744                obuf,
745            );
746        }
747    }
748
749    impl<Field, Rest, const DER: bool> GoodSerializer for DefaultedFmt<
750        Field,
751        Field::SVal,
752        Rest,
753        DER,
754    > where Field: GoodSerializer, Rest: GoodSerializer {
755        open spec fn serialize_inv(&self) -> bool {
756            defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).serialize_inv()
757        }
758
759        proof fn lemma_serialize_len(&self, v: Self::SVal) {
760            defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).lemma_serialize_len(v);
761        }
762    }
763
764    impl<Field, Rest, const DER: bool> SPRoundTripDps for DefaultedFmt<
765        Field,
766        Field::T,
767        Rest,
768        DER,
769    > where Field: SPRoundTripDps + NonTailFmt, Rest: SPRoundTripDps {
770        open spec fn unambiguous(&self) -> bool {
771            defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).unambiguous()
772        }
773
774        proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
775            defaulted_fmt::<Field, Rest, DER>(
776                self.0,
777                self.1,
778                self.2,
779            ).theorem_serialize_dps_parse_roundtrip(v, obuf);
780        }
781    }
782
783    impl<Field, Rest, const DER: bool> NoLookAhead for DefaultedFmt<
784        Field,
785        Field::PVal,
786        Rest,
787        DER,
788    > where
789        Field: SpecByteLen + NoLookAhead<PVal = Field::T>,
790        Rest: SpecByteLen + NoLookAhead<PVal = Rest::T>,
791     {
792        open spec fn no_lookahead_inv(&self) -> bool {
793            defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).no_lookahead_inv()
794        }
795
796        proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
797            defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).lemma_no_lookahead(i1, i2);
798        }
799    }
800
801    impl<Field, Rest, const DER: bool> NonMalleable for DefaultedFmt<
802        Field,
803        Field::PVal,
804        Rest,
805        DER,
806    > where Field: SoundParser + NonMalleable, Rest: SoundParser + NonMalleable {
807        open spec fn nonmal_inv(&self) -> bool {
808            defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).nonmal_inv()
809        }
810
811        proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
812            defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).lemma_parse_non_malleable(
813                buf1,
814                buf2,
815            );
816        }
817    }
818
819    impl<Field, Rest, const DER: bool> EquivSerializersGeneral for DefaultedFmt<
820        Field,
821        Field::SVal,
822        Rest,
823        DER,
824    > where
825        Field: SpecByteLen + EquivSerializersGeneral<SVal = Field::T>,
826        Rest: SpecByteLen + EquivSerializersGeneral<SVal = Rest::T>,
827     {
828        open spec fn equiv_general_inv(&self) -> bool {
829            defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).equiv_general_inv()
830        }
831
832        proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
833            defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).lemma_serialize_equiv(
834                v,
835                obuf,
836            );
837        }
838    }
839
840    impl<Field, Rest, const DER: bool> EquivSerializers for DefaultedFmt<
841        Field,
842        Field::SVal,
843        Rest,
844        DER,
845    > where
846        Field: SpecByteLen + EquivSerializersGeneral<SVal = Field::T>,
847        Rest: SpecByteLen + EquivSerializers<SVal = Rest::T>,
848     {
849        open spec fn equiv_inv(&self) -> bool {
850            defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).equiv_inv()
851        }
852
853        proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
854            defaulted_fmt::<Field, Rest, DER>(
855                self.0,
856                self.1,
857                self.2,
858            ).lemma_serialize_equiv_on_empty(v);
859        }
860    }
861
862}
863
864/*
865 * TODO: Due to technical reasons, `DefaultedFmt` now only support `Structural` (in the Verus sense) types. To support non-Structural types,
866 * `DefaultedFmt` needs to take both the `exec` default value and the `spec` default value, which is the `DeepView` of the `exec` default value.
867 */
868
869impl<I, Field, Rest, const DER: bool> Parser<I> for DefaultedFmt<Field, Field::T, Rest, DER> where
870    I: InputBuf,
871    Field: Parser<I, PT = Field::T> + SafeParser<PVal = Field::T> + SpecByteLen,
872    Rest: Parser<I> + SafeParser<PVal = Rest::T> + SpecByteLen,
873    Field::T: DeepView<V = Field::T> + PartialEq + Structural + Copy,
874 {
875    type PT = (Field::PT, Rest::PT);
876
877    open spec fn exec_inv(&self) -> bool {
878        &&& self.0.exec_inv()
879        &&& self.0.safe_inv()
880        &&& self.2.exec_inv()
881        &&& self.2.safe_inv()
882        &&& forall|v: Field::T| v.deep_view() == v
883        &&& vstd::laws_eq::obeys_concrete_eq::<Field::T>()
884    }
885
886    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
887        broadcast use crate::core::spec::SafeParser::lemma_parse_safe;
888
889        reveal(vstd::laws_eq::obeys_concrete_eq);
890
891        let (n, (field, rest)) = Optional(&self.0, &self.2).parse(ibuf)?;
892
893        if DER {
894            if let Some(v) = field {
895                if v == self.1 {
896                    return Err(ParseError::non_canonical());
897                }
898            }
899        }
900        let field = match field {
901            Some(v) => v,
902            None => self.1,
903        };
904
905        Ok((n, (field, rest)))
906    }
907}
908
909impl<Output: OutputBuf, Field, Default, Rest, R, const DER: bool> Serializer<
910    Output,
911    (Default, R),
912> for DefaultedFmt<Field, Default, Rest, DER> where
913    Field: SpecByteLen<T = Default> + Serializer<Output, Default>,
914    Rest: SpecByteLen<T = R::V> + Serializer<Output, R>,
915    Default: DeepView<V = Default> + PartialEq + Structural + Copy,
916    R: DeepView,
917 {
918    #[verifier::prophetic]
919    open spec fn exec_inv(&self) -> bool {
920        &&& self.0.exec_inv()
921        &&& self.2.exec_inv()
922        &&& forall|v: Default| v.deep_view() == v
923    }
924
925    fn serialize_into(&self, v: &(Default, R), obuf: &mut Output) {
926        broadcast use crate::core::exec::output::outbuf_lemmas;
927
928        if v.0 != self.1 {
929            self.0.serialize_into(&v.0, obuf);
930        }
931        self.2.serialize_into(&v.1, obuf);
932    }
933}
934
935impl<Field, Default, Rest, R, const DER: bool> Prepare<(Default, R)> for DefaultedFmt<
936    Field,
937    Default,
938    Rest,
939    DER,
940> where
941    Field: SpecByteLen<T = Default> + Prepare<Default>,
942    Rest: SpecByteLen<T = R::V> + Prepare<R>,
943    Default: DeepView<V = Default> + PartialEq + Structural + Copy,
944    R: DeepView,
945 {
946    open spec fn exec_inv(&self) -> bool {
947        &&& self.0.exec_inv()
948        &&& self.2.exec_inv()
949        &&& forall|v: Default| v.deep_view() == v
950    }
951
952    fn prepare(&self, v: &(Default, R)) -> Result<usize, PreSerializeError> {
953        let n0 = if v.0 == self.1 {
954            0
955        } else {
956            self.0.prepare(&v.0)?
957        };
958        let n1 = self.2.prepare(&v.1)?;
959        let total = n0.checked_add(n1).ok_or(PreSerializeError::length_too_large())?;
960        Ok(total)
961    }
962}
963
964impl<Field, Default, Rest, R, const DER: bool> ByteLen<(Default, R)> for DefaultedFmt<
965    Field,
966    Default,
967    Rest,
968    DER,
969> where
970    Field: SpecByteLen<T = Default> + ByteLen<Default>,
971    Rest: SpecByteLen<T = R::V> + ByteLen<R>,
972    Default: DeepView<V = Default> + PartialEq + Structural + Copy,
973    R: DeepView,
974 {
975    open spec fn exec_inv(&self) -> bool {
976        &&& self.0.exec_inv()
977        &&& self.2.exec_inv()
978        &&& forall|v: Default| v.deep_view() == v
979    }
980
981    fn length(&self, v: &(Default, R)) -> usize {
982        let n0 = if v.0 == self.1 {
983            0
984        } else {
985            self.0.length(&v.0)
986        };
987        let n1 = self.2.length(&v.1);
988        n0 + n1
989    }
990}
991
992} // verus!
vest_lib/asn1/modifiers.rs

vest_lib/asn1/
modifiers.rs
