vest_lib/asn1/
der_ord.rs

1//! Allocation-free comparison of values by their complete DER encodings.
2#![allow(unused_variables)]
3
4use crate::asn1::set_of::*;
5use crate::asn1::tag::TAG_FMT_MAX_BYTE_LEN;
6use crate::asn1::{
7    ASN1Fmt, Any, AnyFmt, AnySpec, BitString, BitStringFmt, BitStringSpec, BmpStringFmt,
8    BmpStringSpec, BoolFmt, DefaultedFmt, EnumeratedFmt, GeneralizedTime, GeneralizedTimeFmt,
9    GeneralizedTimeSpec, Ia5String, Ia5StringFmt, Ia5StringSpec, ImplicitlyTaggedFmt, Integer,
10    Integer16Fmt, Integer8Fmt, IntegerFmt, LengthFmt, ObjectIdentifierFmt, ObjectIdentifierSpec,
11    PrintableString, PrintableStringFmt, PrintableStringSpec, Real, RealFmt, Retaggable, SetOfFmt,
12    Tag, TagFmt, TeletexString, TeletexStringFmt, TeletexStringSpec, UniversalStringFmt, UtcTime,
13    UtcTimeFmt, Utf8StringFmt,
14};
15#[cfg(feature = "alloc")]
16use crate::asn1::{BmpString, ObjectIdentifier, UniversalString};
17use crate::combinators::choice::Sum;
18use crate::combinators::mapped::spec::{BiMap, SpecMap};
19use crate::combinators::{
20    Choice, Empty, Eof, Mapped, Opt, Optional, Pair, Ref, Refined, RepeatTillEnd, Star, Tail, U8,
21};
22use crate::core::exec::fns::{Map, Pred};
23use crate::core::exec::serializer::{ByteLen, SerializerExt};
24use crate::core::spec::{Consistency, GoodSerializer, SpecByteLen, SpecSerializer};
25use crate::primitives::base128::{Base128Fmt, BASE128_MAX_BYTES};
26#[cfg(feature = "alloc")]
27use alloc::vec::Vec;
28use vstd::calc;
29use vstd::prelude::*;
30#[cfg(feature = "alloc")]
31use vstd::string::StrSliceExecFns;
32
33verus! {
34
35/// Cursor-state type for a format. It is format-specific rather than value-type-specific.
36pub trait DerState {
37    type State: Copy + Default;
38}
39
40/// Executable values whose deep view is the value itself.
41///
42/// ASN.1 `DEFAULT` needs this law to make its executable equality test line up with the
43/// spec-level decision to omit the field. Generated ENUMERATED value types implement it.
44pub trait DeepViewIdentity: DeepView<V = Self> + Copy {
45    proof fn lemma_deep_view_identity(&self)
46        ensures
47            self.deep_view() == *self,
48    ;
49}
50
51impl DeepViewIdentity for bool {
52    proof fn lemma_deep_view_identity(&self) {
53    }
54}
55
56impl DeepViewIdentity for i8 {
57    proof fn lemma_deep_view_identity(&self) {
58    }
59}
60
61impl DeepViewIdentity for i16 {
62    proof fn lemma_deep_view_identity(&self) {
63    }
64}
65
66impl DeepViewIdentity for u8 {
67    proof fn lemma_deep_view_identity(&self) {
68    }
69}
70
71impl DeepViewIdentity for UtcTime {
72    proof fn lemma_deep_view_identity(&self) {
73        crate::asn1::utctime::lemma_utc_time_deep_view(self);
74    }
75}
76
77/// A format whose executable values can be traversed in serialization order without producing
78/// an intermediate byte buffer.
79///
80/// `State` contains only traversal state; it must not own a serialization of the value.
81pub trait DerOrd<T>: DerState + SpecSerializer<SVal = T::V> + SpecByteLen<T = T::V> + Consistency<
82    Val = T::V,
83> where T: DeepView + ?Sized {
84    /// DER cursors range over the same number of octets as the format's byte-length model.
85    ///
86    /// Unlike [`crate::core::spec::GoodSerializer::lemma_serialize_len`], this law is
87    /// unconditional once the value is consistent.
88    proof fn lemma_der_serialize_len(&self, value: T::V)
89        requires
90            self.consistent(value),
91        ensures
92            self.spec_serialize(value).len() == self.byte_len(value),
93    ;
94
95    /// The portion of `spec_serialize(value)` not yet returned by the cursor.
96    spec fn der_remaining(&self, value: T::V, state: <Self as DerState>::State) -> Seq<u8>;
97
98    /// The format-specific cursor invariant.
99    spec fn der_state_valid(&self, value: T::V, state: <Self as DerState>::State) -> bool;
100
101    /// Start traversing the encoding of `value`.
102    fn der_start(&self, value: &T) -> (state: <Self as DerState>::State)
103        requires
104            self.consistent(value.deep_view()),
105        ensures
106            self.der_state_valid(value.deep_view(), state),
107            self.der_remaining(value.deep_view(), state) == self.spec_serialize(value.deep_view()),
108    ;
109
110    /// Return the next encoded octet, or `None` exactly at the end of the encoding.
111    fn der_next(&self, value: &T, state: &mut <Self as DerState>::State) -> (next: Option<u8>)
112        requires
113            self.consistent(value.deep_view()),
114            self.der_state_valid(value.deep_view(), *old(state)),
115        ensures
116            self.der_state_valid(value.deep_view(), *final(state)),
117            match next {
118                Some(byte) => {
119                    self.der_remaining(value.deep_view(), *old(state)) == seq![byte]
120                        + self.der_remaining(value.deep_view(), *final(state))
121                },
122                None => {
123                    &&& self.der_remaining(value.deep_view(), *old(state)).len() == 0
124                    &&& self.der_remaining(value.deep_view(), *final(state)).len() == 0
125                },
126            },
127    ;
128
129    /// Compare two values by the complete DER TLV octets produced by this format.
130    #[verifier::loop_isolation(false)]
131    fn der_leq(&self, left: &T, right: &T) -> (leq: bool)
132        requires
133            self.consistent(left.deep_view()),
134            self.consistent(right.deep_view()),
135        ensures
136            leq == der_octets_leq(
137                self.spec_serialize(left.deep_view()),
138                self.spec_serialize(right.deep_view()),
139            ),
140    {
141        let mut left_state = self.der_start(left);
142        let mut right_state = self.der_start(right);
143        let ghost leftvv = left.deep_view();
144        let ghost rightvv = right.deep_view();
145        let ghost left_encoding = self.spec_serialize(leftvv);
146        let ghost right_encoding = self.spec_serialize(right.deep_view());
147
148        loop
149            invariant
150                self.der_state_valid(leftvv, left_state),
151                self.der_state_valid(right.deep_view(), right_state),
152                der_octets_leq(left_encoding, right_encoding) == der_octets_leq(
153                    self.der_remaining(leftvv, left_state),
154                    self.der_remaining(rightvv, right_state),
155                ),
156            decreases
157                    self.der_remaining(leftvv, left_state).len() + self.der_remaining(
158                        rightvv,
159                        right_state,
160                    ).len(),
161        {
162            let ghost old_l = self.der_remaining(leftvv, left_state);
163            let ghost old_r = self.der_remaining(rightvv, right_state);
164            let left_next = self.der_next(left, &mut left_state);
165            let right_next = self.der_next(right, &mut right_state);
166            let left_byte = match left_next {
167                Some(byte) => byte,
168                None => 0,
169            };
170            let right_byte = match right_next {
171                Some(byte) => byte,
172                None => 0,
173            };
174
175            if left_next.is_none() && right_next.is_none() {
176                return true;
177            }
178            proof {
179                assert(der_octets_drop_head(old_l) == self.der_remaining(leftvv, left_state));
180                assert(der_octets_drop_head(old_r) == self.der_remaining(rightvv, right_state));
181                lemma_der_octets_leq_step(old_l, old_r);
182            }
183
184            if left_byte < right_byte {
185                return true;
186            }
187            if left_byte > right_byte {
188                return false;
189            }
190        }
191    }
192}
193
194} // verus!
195/// Prove that the cursor is valid and positioned at the start of the value's complete DER encoding.
196#[allow(unused_macros)]
197macro_rules! good_start {
198    ($fmt:expr, $value:expr, $state:expr) => {
199        ::vstd::prelude::assert_(::vstd::prelude::ext_equal(
200            $fmt.der_remaining($value, $state),
201            $fmt.spec_serialize($value),
202        ));
203        ::vstd::prelude::assert_($fmt.der_state_valid($value, $state));
204    };
205}
206
207verus! {
208
209/// Stack-resident serialization cursor for a DER tag.
210#[derive(Copy, Clone)]
211pub struct TagDerState {
212    pub bytes: [u8; TAG_FMT_MAX_BYTE_LEN],
213    pub len: usize,
214    pub pos: usize,
215}
216
217impl Default for TagDerState {
218    fn default() -> (state: Self) {
219        Self { bytes: [0u8;TAG_FMT_MAX_BYTE_LEN], len: 0, pos: 0 }
220    }
221}
222
223/// Stack-resident serialization cursor for a DER length.
224///
225/// Nine octets cover the one-octet prefix plus every byte of a 64-bit `usize`, and are also
226/// sufficient on narrower targets.
227#[derive(Copy, Clone)]
228pub struct LengthDerState {
229    pub bytes: [u8; 9],
230    pub len: usize,
231    pub pos: usize,
232}
233
234impl Default for LengthDerState {
235    fn default() -> (state: Self) {
236        Self { bytes: [0u8;9], len: 0, pos: 0 }
237    }
238}
239
240impl DerState for TagFmt {
241    type State = TagDerState;
242}
243
244impl DerOrd<Tag> for TagFmt {
245    proof fn lemma_der_serialize_len(&self, tag: Tag) {
246        self.lemma_serialize_len(tag);
247    }
248
249    open spec fn der_remaining(&self, tag: Tag, state: TagDerState) -> Seq<u8> {
250        self.spec_serialize(tag).skip(state.pos as int)
251    }
252
253    open spec fn der_state_valid(&self, tag: Tag, state: TagDerState) -> bool {
254        &&& state.pos <= state.len
255        &&& state.len <= state.bytes@.len()
256        &&& state.len == self.spec_serialize(tag).len()
257        &&& state.bytes@.take(state.len as int) == self.spec_serialize(tag)
258    }
259
260    fn der_start(&self, t: &Tag) -> (state: TagDerState) {
261        proof {
262            crate::asn1::tag::lemma_tag_fmt_byte_len_bound(*t);
263            self.lemma_serialize_len(*t);
264        }
265        let len = self.length(t);
266        let mut bytes = [0u8;TAG_FMT_MAX_BYTE_LEN];
267        let (encoded, tail) = bytes.split_at_mut(len);
268        self.serialize(t, encoded);
269        let state = TagDerState { bytes, len, pos: 0 };
270        proof {
271            vstd::seq_lib::lemma_seq_append_take_skip(encoded@, tail@, len as int);
272            good_start!(self, *t, state);
273        }
274        state
275    }
276
277    fn der_next(&self, t: &Tag, state: &mut TagDerState) -> (next: Option<u8>) {
278        if state.pos == state.len {
279            None
280        } else {
281            let byte = state.bytes[state.pos];
282            state.pos += 1;
283            Some(byte)
284        }
285    }
286}
287
288impl DerState for LengthFmt<true> {
289    type State = LengthDerState;
290}
291
292impl DerOrd<usize> for LengthFmt<true> {
293    proof fn lemma_der_serialize_len(&self, value: usize) {
294        self.lemma_serialize_len(value);
295    }
296
297    open spec fn der_remaining(&self, value: usize, state: LengthDerState) -> Seq<u8> {
298        self.spec_serialize(value).skip(state.pos as int)
299    }
300
301    open spec fn der_state_valid(&self, value: usize, state: LengthDerState) -> bool {
302        &&& state.pos <= state.len
303        &&& state.len <= 9
304        &&& state.len == self.spec_serialize(value).len()
305        &&& state.bytes@.take(state.len as int) == self.spec_serialize(value)
306    }
307
308    fn der_start(&self, l: &usize) -> (state: LengthDerState) {
309        proof {
310            crate::asn1::length::lemma_length_fmt_byte_len_bound::<true>(*l);
311            self.lemma_serialize_len(*l);
312        }
313        let len = self.length(l);
314        let mut bytes = [0u8;9];
315        let (encoded, tail) = bytes.split_at_mut(len);
316        self.serialize(l, encoded);
317        let state = LengthDerState { bytes, len, pos: 0 };
318        proof {
319            vstd::seq_lib::lemma_seq_append_take_skip(encoded@, tail@, len as int);
320            good_start!(self, *l, state);
321        }
322        state
323    }
324
325    fn der_next(&self, l: &usize, state: &mut LengthDerState) -> (next: Option<u8>) {
326        if state.pos == state.len {
327            None
328        } else {
329            let byte = state.bytes[state.pos];
330            state.pos += 1;
331            Some(byte)
332        }
333    }
334}
335
336/// Stack-resident cursor for one minimally encoded OBJECT IDENTIFIER subidentifier.
337#[derive(Copy, Clone)]
338pub struct Base128DerState {
339    pub bytes: [u8; BASE128_MAX_BYTES],
340    pub len: usize,
341    pub pos: usize,
342}
343
344impl Default for Base128DerState {
345    fn default() -> (state: Self) {
346        Self { bytes: [0u8;BASE128_MAX_BYTES], len: 0, pos: 0 }
347    }
348}
349
350impl DerState for Base128Fmt<true> {
351    type State = Base128DerState;
352}
353
354impl DerOrd<u64> for Base128Fmt<true> {
355    proof fn lemma_der_serialize_len(&self, value: u64) {
356        assert(self.serialize_inv());
357        self.lemma_serialize_len(value);
358    }
359
360    open spec fn der_remaining(&self, value: u64, state: Base128DerState) -> Seq<u8> {
361        self.spec_serialize(value).skip(state.pos as int)
362    }
363
364    open spec fn der_state_valid(&self, value: u64, state: Base128DerState) -> bool {
365        &&& state.pos <= state.len
366        &&& state.len <= state.bytes@.len()
367        &&& state.len == self.spec_serialize(value).len()
368        &&& state.bytes@.take(state.len as int) == self.spec_serialize(value)
369    }
370
371    fn der_start(&self, i: &u64) -> (state: Base128DerState) {
372        proof {
373            self.lemma_der_serialize_len(*i);
374            crate::primitives::base128::lemma_base128_fmt_consistent_byte_len_bound::<true>(*i);
375        }
376        let len = self.length(i);
377        let mut bytes = [0u8;BASE128_MAX_BYTES];
378        let (encoded, tail) = bytes.split_at_mut(len);
379        self.serialize(i, encoded);
380        let state = Base128DerState { bytes, len, pos: 0 };
381        proof {
382            vstd::seq_lib::lemma_seq_append_take_skip(encoded@, tail@, len as int);
383            good_start!(self, *i, state);
384        }
385        state
386    }
387
388    fn der_next(&self, i: &u64, state: &mut Base128DerState) -> (next: Option<u8>) {
389        if state.pos == state.len {
390            None
391        } else {
392            let byte = state.bytes[state.pos];
393            state.pos += 1;
394            Some(byte)
395        }
396    }
397}
398
399/// Cursor for a complete DER tag-length-value encoding.
400#[verifier::allow(autoderive_clone_without_spec)]
401#[derive(Copy, Clone, Default)]
402pub struct TlvDerState<Content> {
403    pub tag: TagDerState,
404    pub length: LengthDerState,
405    pub content: Content,
406    pub content_len: usize,
407    /// `0`: tag, `1`: length, `2`: content.
408    pub phase: u8,
409}
410
411impl<Content: DerState> DerState for ASN1Fmt<Content, true> {
412    type State = TlvDerState<Content::State>;
413}
414
415impl<Content, T> DerOrd<T> for ASN1Fmt<Content, true> where
416    T: DeepView + ?Sized,
417    Content: crate::core::spec::SpecCombinator<T = T::V> + DerOrd<T>,
418 {
419    proof fn lemma_der_serialize_len(&self, value: T::V) {
420        self.1.lemma_der_serialize_len(value);
421        TagFmt.lemma_der_serialize_len(self.0);
422        LengthFmt::<true>.lemma_der_serialize_len(self.1.byte_len(value) as usize);
423    }
424
425    #[verusfmt::skip]
426    open spec fn der_remaining(&self, value: T::V, state: TlvDerState<Content::State>) -> Seq<u8> {
427        match state.phase {
428            0 => {
429                TagFmt.der_remaining(self.0, state.tag)
430                + LengthFmt::<true>.der_remaining(state.content_len, state.length)
431                + self.1.der_remaining(value, state.content)
432            },
433            1 => {
434                LengthFmt::<true>.der_remaining(state.content_len, state.length)
435                + self.1.der_remaining(value, state.content)
436            },
437            _ => self.1.der_remaining(value, state.content),
438        }
439    }
440
441    #[verusfmt::skip]
442    open spec fn der_state_valid(&self, value: T::V, state: TlvDerState<Content::State>) -> bool {
443        &&& TagFmt.der_state_valid(self.0, state.tag)
444        &&& LengthFmt::<true>.der_state_valid(state.content_len, state.length)
445        &&& self.1.der_state_valid(value, state.content)
446        &&& state.content_len as nat == self.1.byte_len(value)
447        &&& state.phase <= 2
448        &&& state.phase >= 1 ==> TagFmt.der_remaining(self.0, state.tag).len() == 0
449        &&& state.phase >= 2 ==> LengthFmt::<true>.der_remaining(state.content_len, state.length).len() == 0
450    }
451
452    fn der_start(&self, v: &T) -> (state: TlvDerState<Content::State>) {
453        /// Count a cursor's encoded octets without materializing them.
454        #[verifier::loop_isolation(false)]
455        fn der_len<F, T>(fmt: &F, v: &T) -> (len: usize) where T: DeepView + ?Sized, F: DerOrd<T>
456            requires
457                fmt.consistent(v.deep_view()),
458                fmt.spec_serialize(v.deep_view()).len() <= usize::MAX,
459            ensures
460                len == fmt.spec_serialize(v.deep_view()).len(),
461        {
462            let mut state = fmt.der_start(v);
463            let mut len = 0usize;
464            let ghost encoding = fmt.spec_serialize(v.deep_view());
465            loop
466                invariant
467                    fmt.der_state_valid(v.deep_view(), state),
468                    len as nat + fmt.der_remaining(v.deep_view(), state).len() == encoding.len(),
469                decreases fmt.der_remaining(v.deep_view(), state).len(),
470            {
471                if let None = fmt.der_next(v, &mut state) {
472                    return len;
473                }
474                len += 1;
475            }
476        }
477        proof {
478            self.1.lemma_der_serialize_len(v.deep_view());
479        }
480        let content_len = der_len(&self.1, v);
481        let state = TlvDerState {
482            tag: TagFmt.der_start(&self.0),
483            length: LengthFmt::<true>.der_start(&content_len),
484            content: self.1.der_start(v),
485            content_len,
486            phase: 0,
487        };
488        proof {
489            good_start!(self, v.deep_view(), state);
490        }
491        state
492    }
493
494    fn der_next(&self, v: &T, state: &mut TlvDerState<Content::State>) -> (next: Option<u8>) {
495        if state.phase == 0 {
496            match TagFmt.der_next(&self.0, &mut state.tag) {
497                Some(byte) => {
498                    return Some(byte);
499                },
500                None => {
501                    state.phase = 1;
502                },
503            }
504        }
505        if state.phase == 1 {
506            match LengthFmt::<true>.der_next(&state.content_len, &mut state.length) {
507                Some(byte) => {
508                    return Some(byte);
509                },
510                None => {
511                    state.phase = 2;
512                },
513            }
514        }
515        let next = self.1.der_next(v, &mut state.content);
516        next
517    }
518}
519
520impl DerState for BoolFmt<true> {
521    type State = bool;
522}
523
524impl DerOrd<bool> for BoolFmt<true> {
525    proof fn lemma_der_serialize_len(&self, value: bool) {
526        self.lemma_serialize_len(value);
527    }
528
529    open spec fn der_remaining(&self, value: bool, state: bool) -> Seq<u8> {
530        if state {
531            Seq::empty()
532        } else {
533            self.spec_serialize(value)
534        }
535    }
536
537    open spec fn der_state_valid(&self, _value: bool, _state: bool) -> bool {
538        true
539    }
540
541    fn der_start(&self, b: &bool) -> (state: bool) {
542        let state = false;
543        proof {
544            good_start!(self, *b, state);
545        }
546        state
547    }
548
549    fn der_next(&self, b: &bool, state: &mut bool) -> (next: Option<u8>) {
550        if *state {
551            None
552        } else {
553            *state = true;
554            let mut bytes = [0u8;1];
555            self.serialize(b, &mut bytes);
556            Some(bytes[0])
557        }
558    }
559}
560
561impl DerState for Integer8Fmt {
562    type State = bool;
563}
564
565impl DerOrd<i8> for Integer8Fmt {
566    proof fn lemma_der_serialize_len(&self, value: i8) {
567        self.lemma_serialize_len(value);
568    }
569
570    open spec fn der_remaining(&self, value: i8, state: bool) -> Seq<u8> {
571        if state {
572            Seq::empty()
573        } else {
574            self.spec_serialize(value)
575        }
576    }
577
578    open spec fn der_state_valid(&self, _value: i8, _state: bool) -> bool {
579        true
580    }
581
582    fn der_start(&self, i: &i8) -> (state: bool) {
583        let state = false;
584        proof {
585            good_start!(self, *i, state);
586        }
587        state
588    }
589
590    fn der_next(&self, i: &i8, state: &mut bool) -> (next: Option<u8>) {
591        if *state {
592            None
593        } else {
594            *state = true;
595            let mut bytes = [0u8;1];
596            self.serialize(i, &mut bytes);
597            Some(bytes[0])
598        }
599    }
600}
601
602/// Stack cursor for the specialized small INTEGER content formats.
603#[derive(Copy, Clone)]
604pub struct Integer16DerState {
605    pub bytes: [u8; 2],
606    pub len: usize,
607    pub pos: usize,
608}
609
610impl Default for Integer16DerState {
611    fn default() -> (state: Self) {
612        Self { bytes: [0u8;2], len: 0, pos: 0 }
613    }
614}
615
616impl DerState for Integer16Fmt {
617    type State = Integer16DerState;
618}
619
620impl DerOrd<i16> for Integer16Fmt {
621    proof fn lemma_der_serialize_len(&self, value: i16) {
622        self.lemma_serialize_len(value);
623    }
624
625    open spec fn der_remaining(&self, value: i16, state: Integer16DerState) -> Seq<u8> {
626        self.spec_serialize(value).skip(state.pos as int)
627    }
628
629    open spec fn der_state_valid(&self, value: i16, state: Integer16DerState) -> bool {
630        &&& state.pos <= state.len <= 2
631        &&& state.len == self.spec_serialize(value).len()
632        &&& state.bytes@.take(state.len as int) == self.spec_serialize(value)
633    }
634
635    fn der_start(&self, i: &i16) -> (state: Integer16DerState) {
636        proof {
637            crate::asn1::integer::lemma_integer16_fmt_byte_len_bound(*i);
638            self.lemma_serialize_len(*i);
639        }
640        let len = self.length(i);
641        let mut bytes = [0u8;2];
642        let (encoded, tail) = bytes.split_at_mut(len);
643        self.serialize(i, encoded);
644        let state = Integer16DerState { bytes, len, pos: 0 };
645        proof {
646            vstd::seq_lib::lemma_seq_append_take_skip(encoded@, tail@, len as int);
647            good_start!(self, *i, state);
648        }
649        state
650    }
651
652    fn der_next(&self, i: &i16, state: &mut Integer16DerState) -> (next: Option<u8>) {
653        if state.pos == state.len {
654            None
655        } else {
656            let byte = state.bytes[state.pos];
657            state.pos += 1;
658            Some(byte)
659        }
660    }
661}
662
663#[derive(Copy, Clone)]
664pub struct UtcTimeDerState {
665    pub bytes: [u8; 13],
666    pub pos: usize,
667}
668
669impl Default for UtcTimeDerState {
670    fn default() -> (state: Self) {
671        Self { bytes: [0u8;13], pos: 0 }
672    }
673}
674
675impl DerState for UtcTimeFmt<true> {
676    type State = UtcTimeDerState;
677}
678
679/// DER always emits UTCTime with seconds and the trailing `Z`, for 13 content octets.
680proof fn lemma_utc_time_der_serialized_len(value: UtcTime)
681    requires
682        UtcTimeFmt::<true>.consistent(value),
683    ensures
684        UtcTimeFmt::<true>.spec_serialize(value).len() == 13,
685        UtcTimeFmt::<true>.byte_len(value) == 13,
686{
687}
688
689impl DerOrd<UtcTime> for UtcTimeFmt<true> {
690    proof fn lemma_der_serialize_len(&self, value: UtcTime) {
691        lemma_utc_time_der_serialized_len(value);
692    }
693
694    open spec fn der_remaining(&self, value: UtcTime, state: UtcTimeDerState) -> Seq<u8> {
695        self.spec_serialize(value).skip(state.pos as int)
696    }
697
698    open spec fn der_state_valid(&self, value: UtcTime, state: UtcTimeDerState) -> bool {
699        &&& state.pos <= 13
700        &&& state.bytes@ == self.spec_serialize(value)
701    }
702
703    fn der_start(&self, t: &UtcTime) -> (state: UtcTimeDerState) {
704        proof {
705            t.lemma_deep_view_identity();
706            assert(UtcTimeFmt::<true>.consistent(*t));
707            lemma_utc_time_der_serialized_len(*t);
708        }
709        let mut bytes = [0u8;13];
710        self.serialize(t, &mut bytes);
711        let state = UtcTimeDerState { bytes, pos: 0 };
712        proof {
713            good_start!(self, t.deep_view(), state);
714        }
715        state
716    }
717
718    fn der_next(&self, t: &UtcTime, state: &mut UtcTimeDerState) -> (next: Option<u8>) {
719        if state.pos == 13 {
720            None
721        } else {
722            let byte = state.bytes[state.pos];
723            state.pos += 1;
724            Some(byte)
725        }
726    }
727}
728
729#[derive(Copy, Clone)]
730pub struct GeneralizedTimeDerState {
731    pub prefix: [u8; 14],
732    pub pos: usize,
733}
734
735impl Default for GeneralizedTimeDerState {
736    fn default() -> (state: Self) {
737        Self { prefix: [0u8;14], pos: 0 }
738    }
739}
740
741impl DerState for GeneralizedTimeFmt<true> {
742    type State = GeneralizedTimeDerState;
743}
744
745impl<'a> DerOrd<GeneralizedTime<'a>> for GeneralizedTimeFmt<true> {
746    proof fn lemma_der_serialize_len(&self, value: GeneralizedTimeSpec) {
747        crate::asn1::generalizedtime::lemma_der_generalized_time_model(value);
748    }
749
750    open spec fn der_remaining(
751        &self,
752        value: GeneralizedTimeSpec,
753        state: GeneralizedTimeDerState,
754    ) -> Seq<u8> {
755        self.spec_serialize(value).skip(state.pos as int)
756    }
757
758    open spec fn der_state_valid(
759        &self,
760        value: GeneralizedTimeSpec,
761        state: GeneralizedTimeDerState,
762    ) -> bool {
763        &&& state.pos <= self.spec_serialize(value).len()
764        &&& state.prefix@ == crate::asn1::generalizedtime::generalized_time_prefix(value)
765    }
766
767    fn der_start(&self, t: &GeneralizedTime<'a>) -> (state: GeneralizedTimeDerState) {
768        proof {
769            crate::asn1::generalizedtime::lemma_der_generalized_time_model(t.deep_view());
770        }
771        let prefix = crate::asn1::generalizedtime::generalized_time_der_prefix_bytes(t);
772        let state = GeneralizedTimeDerState { prefix, pos: 0 };
773        proof {
774            good_start!(self, t.deep_view(), state);
775        }
776        state
777    }
778
779    fn der_next(&self, t: &GeneralizedTime<'a>, state: &mut GeneralizedTimeDerState) -> (next:
780        Option<u8>) {
781        let ghost old_pos = state.pos;
782        proof {
783            crate::asn1::generalizedtime::lemma_der_generalized_time_model(t.deep_view());
784            crate::asn1::generalizedtime::lemma_der_generalized_time_layout(
785                t.deep_view(),
786                state.pos,
787            );
788        }
789        let fraction = t.fraction();
790        let total = if fraction.len() == 0 {
791            15usize
792        } else {
793            fraction.len() + 16
794        };
795        if state.pos == total {
796            None
797        } else {
798            let byte;
799            if state.pos < 14 {
800                byte = state.prefix[state.pos];
801            } else if fraction.len() == 0 {
802                byte = 0x5a;
803            } else if state.pos == 14 {
804                byte = 0x2e;
805            } else if state.pos < fraction.len() + 15 {
806                byte = fraction[state.pos - 15];
807            } else {
808                byte = 0x5a;
809            }
810            state.pos += 1;
811            Some(byte)
812        }
813    }
814}
815
816/// Cursor for arbitrary-size INTEGER contents. Small values cache at most nine content octets;
817/// large values retain the zero-copy representation and are traversed directly.
818#[derive(Copy, Clone)]
819pub struct IntegerDerState {
820    pub bytes: [u8; 9],
821    pub len: usize,
822    pub pos: usize,
823    pub small: bool,
824}
825
826impl Default for IntegerDerState {
827    fn default() -> (state: Self) {
828        Self { bytes: [0u8;9], len: 0, pos: 0, small: false }
829    }
830}
831
832impl DerState for IntegerFmt {
833    type State = IntegerDerState;
834}
835
836impl<'a> DerOrd<Integer<'a>> for IntegerFmt {
837    proof fn lemma_der_serialize_len(&self, value: int) {
838        self.lemma_serialize_len(value);
839    }
840
841    open spec fn der_remaining(&self, value: int, state: IntegerDerState) -> Seq<u8> {
842        self.spec_serialize(value).skip(state.pos as int)
843    }
844
845    open spec fn der_state_valid(&self, value: int, state: IntegerDerState) -> bool {
846        &&& state.pos <= state.len
847        &&& state.len == self.spec_serialize(value).len()
848        &&& state.small == (i64::MIN as int <= value <= i64::MAX as int)
849        &&& state.small ==> {
850            &&& state.len <= 9
851            &&& state.bytes@.take(state.len as int) == self.spec_serialize(value)
852        }
853    }
854
855    fn der_start(&self, i: &super::Integer<'a>) -> (state: IntegerDerState) {
856        let state = match i {
857            super::Integer::Small { v } => {
858                let len = crate::asn1::integer::i64_to_be_bytes_len(*v);
859                let mut bytes = [0u8;9];
860                let (encoded, tail) = bytes.split_at_mut(len);
861                crate::asn1::integer::i64_to_be_bytes_in_place(*v, encoded);
862                proof {
863                    crate::asn1::integer::lemma_integer_small_view(*v);
864                    vstd::seq_lib::lemma_seq_append_take_skip(encoded@, tail@, len as int);
865                }
866                IntegerDerState { bytes, len, pos: 0, small: true }
867            },
868            super::Integer::Big { raw } => {
869                let bytes = raw.as_slice();
870                proof {
871                    use_type_invariant(raw);
872                    crate::asn1::integer::lemma_large_integer_outside_i64(raw.view());
873                    crate::asn1::integer::lemma_integer_big_view(*raw);
874                    crate::asn1::integer::lemma_integer_from_to_bytes(bytes.deep_view());
875                }
876                IntegerDerState { bytes: [0u8;9], len: bytes.len(), pos: 0, small: false }
877            },
878        };
879        proof {
880            good_start!(self, i.deep_view(), state);
881        }
882        state
883    }
884
885    fn der_next(&self, i: &super::Integer<'a>, state: &mut IntegerDerState) -> (next: Option<u8>) {
886        if state.pos == state.len {
887            None
888        } else {
889            let byte = match i {
890                super::Integer::Small { v: _v } => {
891                    proof {
892                        crate::asn1::integer::lemma_integer_small_view(*_v);
893                    }
894                    state.bytes[state.pos]
895                },
896                super::Integer::Big { raw } => {
897                    let bytes = raw.as_slice();
898                    proof {
899                        use_type_invariant(raw);
900                        crate::asn1::integer::lemma_large_integer_outside_i64(raw.view());
901                        crate::asn1::integer::lemma_integer_big_view(*raw);
902                        crate::asn1::integer::lemma_integer_from_to_bytes(bytes.deep_view());
903                    }
904                    bytes[state.pos]
905                },
906            };
907            state.pos += 1;
908            Some(byte)
909        }
910    }
911}
912
913impl DerState for EnumeratedFmt {
914    type State = IntegerDerState;
915}
916
917impl<'a> DerOrd<Integer<'a>> for EnumeratedFmt {
918    proof fn lemma_der_serialize_len(&self, value: int) {
919        IntegerFmt.lemma_der_serialize_len(value);
920    }
921
922    open spec fn der_remaining(&self, value: int, state: IntegerDerState) -> Seq<u8> {
923        IntegerFmt.der_remaining(value, state)
924    }
925
926    open spec fn der_state_valid(&self, value: int, state: IntegerDerState) -> bool {
927        IntegerFmt.der_state_valid(value, state)
928    }
929
930    fn der_start(&self, i: &Integer<'a>) -> (state: IntegerDerState) {
931        let state = IntegerFmt.der_start(i);
932        proof {
933            good_start!(self, i.deep_view(), state);
934        }
935        state
936    }
937
938    fn der_next(&self, i: &Integer<'a>, state: &mut IntegerDerState) -> (next: Option<u8>) {
939        IntegerFmt.der_next(i, state)
940    }
941}
942
943/// Cursor for a direct byte sequence.
944#[derive(Copy, Clone, Default)]
945pub struct BytesDerState {
946    pub pos: usize,
947}
948
949impl DerState for Tail {
950    type State = BytesDerState;
951}
952
953impl DerOrd<[u8]> for Tail {
954    proof fn lemma_der_serialize_len(&self, value: Seq<u8>) {
955    }
956
957    open spec fn der_remaining(&self, value: Seq<u8>, state: BytesDerState) -> Seq<u8> {
958        value.skip(state.pos as int)
959    }
960
961    open spec fn der_state_valid(&self, value: Seq<u8>, state: BytesDerState) -> bool {
962        state.pos <= value.len()
963    }
964
965    fn der_start(&self, b: &[u8]) -> (state: BytesDerState) {
966        let state = BytesDerState { pos: 0 };
967        proof {
968            assert(<Self as DerOrd<[u8]>>::der_remaining(self, b@, state) == self.spec_serialize(
969                b@,
970            ));
971            assert(<Self as DerOrd<[u8]>>::der_state_valid(self, b@, state));
972        }
973        state
974    }
975
976    fn der_next(&self, b: &[u8], state: &mut BytesDerState) -> (next: Option<u8>) {
977        if state.pos == b.len() {
978            None
979        } else {
980            let byte = b[state.pos];
981            state.pos += 1;
982            Some(byte)
983        }
984    }
985}
986
987impl<'a> DerOrd<&'a [u8]> for Tail {
988    proof fn lemma_der_serialize_len(&self, value: Seq<u8>) {
989    }
990
991    open spec fn der_remaining(&self, value: Seq<u8>, state: BytesDerState) -> Seq<u8> {
992        value.skip(state.pos as int)
993    }
994
995    open spec fn der_state_valid(&self, value: Seq<u8>, state: BytesDerState) -> bool {
996        state.pos <= value.len()
997    }
998
999    fn der_start(&self, b: &&'a [u8]) -> (state: BytesDerState) {
1000        let state = BytesDerState { pos: 0 };
1001        proof {
1002            assert(<Self as DerOrd<&'a [u8]>>::der_remaining(self, b.deep_view(), state)
1003                == self.spec_serialize(b.deep_view()));
1004            assert(<Self as DerOrd<&'a [u8]>>::der_state_valid(self, b.deep_view(), state));
1005        }
1006        state
1007    }
1008
1009    fn der_next(&self, b: &&'a [u8], state: &mut BytesDerState) -> (next: Option<u8>) {
1010        if state.pos == b.len() {
1011            None
1012        } else {
1013            let byte = b[state.pos];
1014            state.pos += 1;
1015            Some(byte)
1016        }
1017    }
1018}
1019
1020impl DerState for RealFmt<true> {
1021    type State = BytesDerState;
1022}
1023
1024impl<'a> DerOrd<Real<'a, true>> for RealFmt<true> {
1025    proof fn lemma_der_serialize_len(&self, value: Seq<u8>) {
1026        assert(self.serialize_inv());
1027        self.lemma_serialize_len(value);
1028    }
1029
1030    open spec fn der_remaining(&self, value: Seq<u8>, state: BytesDerState) -> Seq<u8> {
1031        self.spec_serialize(value).skip(state.pos as int)
1032    }
1033
1034    open spec fn der_state_valid(&self, value: Seq<u8>, state: BytesDerState) -> bool {
1035        state.pos <= self.spec_serialize(value).len()
1036    }
1037
1038    fn der_start(&self, r: &Real<'a, true>) -> (state: BytesDerState) {
1039        let bytes = r.contents();
1040        let state = BytesDerState { pos: 0 };
1041        proof {
1042            good_start!(self, r.deep_view(), state);
1043        }
1044        state
1045    }
1046
1047    fn der_next(&self, r: &Real<'a, true>, state: &mut BytesDerState) -> (next: Option<u8>) {
1048        let bytes = r.contents();
1049        if state.pos == bytes.len() {
1050            None
1051        } else {
1052            let byte = bytes[state.pos];
1053            state.pos += 1;
1054            Some(byte)
1055        }
1056    }
1057}
1058
1059impl DerState for Utf8StringFmt {
1060    type State = BytesDerState;
1061}
1062
1063impl<'a> DerOrd<&'a str> for Utf8StringFmt {
1064    proof fn lemma_der_serialize_len(&self, value: Seq<char>) {
1065        assert(self.serialize_inv());
1066        self.lemma_serialize_len(value);
1067    }
1068
1069    open spec fn der_remaining(&self, value: Seq<char>, state: BytesDerState) -> Seq<u8> {
1070        self.spec_serialize(value).skip(state.pos as int)
1071    }
1072
1073    open spec fn der_state_valid(&self, value: Seq<char>, state: BytesDerState) -> bool {
1074        state.pos <= self.spec_serialize(value).len()
1075    }
1076
1077    fn der_start(&self, s: &&'a str) -> (state: BytesDerState) {
1078        let bytes = s.as_bytes();
1079        let state = BytesDerState { pos: 0 };
1080        proof {
1081            good_start!(self, s.deep_view(), state);
1082        }
1083        state
1084    }
1085
1086    fn der_next(&self, s: &&'a str, state: &mut BytesDerState) -> (next: Option<u8>) {
1087        let bytes = s.as_bytes();
1088        if state.pos == bytes.len() {
1089            None
1090        } else {
1091            let byte = bytes[state.pos];
1092            state.pos += 1;
1093            Some(byte)
1094        }
1095    }
1096}
1097
1098impl DerState for PrintableStringFmt {
1099    type State = BytesDerState;
1100}
1101
1102impl<'a> DerOrd<PrintableString<'a>> for PrintableStringFmt {
1103    proof fn lemma_der_serialize_len(&self, value: PrintableStringSpec) {
1104        assert(self.serialize_inv());
1105        self.lemma_serialize_len(value);
1106    }
1107
1108    open spec fn der_remaining(&self, value: PrintableStringSpec, state: BytesDerState) -> Seq<u8> {
1109        self.spec_serialize(value).skip(state.pos as int)
1110    }
1111
1112    open spec fn der_state_valid(&self, value: PrintableStringSpec, state: BytesDerState) -> bool {
1113        state.pos <= self.spec_serialize(value).len()
1114    }
1115
1116    fn der_start(&self, s: &PrintableString<'a>) -> (state: BytesDerState) {
1117        let inner = s.inner();
1118        let bytes = inner.as_bytes();
1119        let state = BytesDerState { pos: 0 };
1120        proof {
1121            good_start!(self, s.deep_view(), state);
1122        }
1123        state
1124    }
1125
1126    fn der_next(&self, s: &PrintableString<'a>, state: &mut BytesDerState) -> (next: Option<u8>) {
1127        let inner = s.inner();
1128        let bytes = inner.as_bytes();
1129        if state.pos == bytes.len() {
1130            None
1131        } else {
1132            let byte = bytes[state.pos];
1133            state.pos += 1;
1134            Some(byte)
1135        }
1136    }
1137}
1138
1139impl DerState for Ia5StringFmt {
1140    type State = BytesDerState;
1141}
1142
1143impl<'a> DerOrd<Ia5String<'a>> for Ia5StringFmt {
1144    proof fn lemma_der_serialize_len(&self, value: Ia5StringSpec) {
1145        assert(self.serialize_inv());
1146        self.lemma_serialize_len(value);
1147    }
1148
1149    open spec fn der_remaining(&self, value: Ia5StringSpec, state: BytesDerState) -> Seq<u8> {
1150        self.spec_serialize(value).skip(state.pos as int)
1151    }
1152
1153    open spec fn der_state_valid(&self, value: Ia5StringSpec, state: BytesDerState) -> bool {
1154        state.pos <= self.spec_serialize(value).len()
1155    }
1156
1157    fn der_start(&self, s: &Ia5String<'a>) -> (state: BytesDerState) {
1158        let inner = s.inner();
1159        let bytes = inner.as_bytes();
1160        let state = BytesDerState { pos: 0 };
1161        proof {
1162            good_start!(self, s.deep_view(), state);
1163        }
1164        state
1165    }
1166
1167    fn der_next(&self, s: &Ia5String<'a>, state: &mut BytesDerState) -> (next: Option<u8>) {
1168        let inner = s.inner();
1169        let bytes = inner.as_bytes();
1170        if state.pos == bytes.len() {
1171            None
1172        } else {
1173            let byte = bytes[state.pos];
1174            state.pos += 1;
1175            Some(byte)
1176        }
1177    }
1178}
1179
1180impl DerState for TeletexStringFmt {
1181    type State = BytesDerState;
1182}
1183
1184impl<'a> DerOrd<TeletexString<'a>> for TeletexStringFmt {
1185    proof fn lemma_der_serialize_len(&self, value: TeletexStringSpec) {
1186        assert(self.serialize_inv());
1187        self.lemma_serialize_len(value);
1188    }
1189
1190    open spec fn der_remaining(&self, value: TeletexStringSpec, state: BytesDerState) -> Seq<u8> {
1191        self.spec_serialize(value).skip(state.pos as int)
1192    }
1193
1194    open spec fn der_state_valid(&self, value: TeletexStringSpec, state: BytesDerState) -> bool {
1195        state.pos <= self.spec_serialize(value).len()
1196    }
1197
1198    fn der_start(&self, s: &TeletexString<'a>) -> (state: BytesDerState) {
1199        let inner = s.inner();
1200        let bytes = inner.as_bytes();
1201        let state = BytesDerState { pos: 0 };
1202        proof {
1203            good_start!(self, s.deep_view(), state);
1204        }
1205        state
1206    }
1207
1208    fn der_next(&self, s: &TeletexString<'a>, state: &mut BytesDerState) -> (next: Option<u8>) {
1209        let inner = s.inner();
1210        let bytes = inner.as_bytes();
1211        if state.pos == bytes.len() {
1212            None
1213        } else {
1214            let byte = bytes[state.pos];
1215            state.pos += 1;
1216            Some(byte)
1217        }
1218    }
1219}
1220
1221impl DerState for U8 {
1222    type State = bool;
1223}
1224
1225impl DerOrd<u8> for U8 {
1226    proof fn lemma_der_serialize_len(&self, value: u8) {
1227    }
1228
1229    open spec fn der_remaining(&self, value: u8, state: bool) -> Seq<u8> {
1230        if state {
1231            Seq::empty()
1232        } else {
1233            seq![value]
1234        }
1235    }
1236
1237    open spec fn der_state_valid(&self, _value: u8, _state: bool) -> bool {
1238        true
1239    }
1240
1241    fn der_start(&self, v: &u8) -> (state: bool) {
1242        let state = false;
1243        proof {
1244            good_start!(self, *v, state);
1245        }
1246        state
1247    }
1248
1249    fn der_next(&self, v: &u8, state: &mut bool) -> (next: Option<u8>) {
1250        if *state {
1251            None
1252        } else {
1253            *state = true;
1254            Some(*v)
1255        }
1256    }
1257}
1258
1259impl DerState for Eof {
1260    type State = bool;
1261}
1262
1263impl DerOrd<()> for Eof {
1264    proof fn lemma_der_serialize_len(&self, _value: ()) {
1265    }
1266
1267    open spec fn der_remaining(&self, _value: (), _state: bool) -> Seq<u8> {
1268        Seq::empty()
1269    }
1270
1271    open spec fn der_state_valid(&self, _value: (), _state: bool) -> bool {
1272        true
1273    }
1274
1275    fn der_start(&self, _v: &()) -> (state: bool) {
1276        let state = false;
1277        proof {
1278            good_start!(self, *_v, state);
1279        }
1280        state
1281    }
1282
1283    fn der_next(&self, _v: &(), _state: &mut bool) -> (next: Option<u8>) {
1284        None
1285    }
1286}
1287
1288impl DerState for Empty {
1289    type State = bool;
1290}
1291
1292impl DerOrd<()> for Empty {
1293    proof fn lemma_der_serialize_len(&self, _value: ()) {
1294    }
1295
1296    open spec fn der_remaining(&self, _value: (), _state: bool) -> Seq<u8> {
1297        Seq::empty()
1298    }
1299
1300    open spec fn der_state_valid(&self, _value: (), _state: bool) -> bool {
1301        true
1302    }
1303
1304    fn der_start(&self, _v: &()) -> (state: bool) {
1305        let state = false;
1306        proof {
1307            good_start!(self, *_v, state);
1308        }
1309        state
1310    }
1311
1312    fn der_next(&self, _v: &(), _state: &mut bool) -> (next: Option<u8>) {
1313        None
1314    }
1315}
1316
1317/// Cursor for sequential composition.
1318#[verifier::allow(autoderive_clone_without_spec)]
1319#[derive(Copy, Clone, Default)]
1320pub struct PairDerState<Left, Right> {
1321    pub left: Left,
1322    pub right: Right,
1323    pub in_left: bool,
1324}
1325
1326impl<A: DerState, B: DerState> DerState for Pair<A, B> {
1327    type State = PairDerState<A::State, B::State>;
1328}
1329
1330impl<A, B, TA, TB> DerOrd<(TA, TB)> for Pair<A, B> where
1331    TA: DeepView,
1332    TB: DeepView,
1333    A: DerOrd<TA>,
1334    B: DerOrd<TB>,
1335 {
1336    proof fn lemma_der_serialize_len(&self, value: (TA::V, TB::V)) {
1337        self.0.lemma_der_serialize_len(value.0);
1338        self.1.lemma_der_serialize_len(value.1);
1339    }
1340
1341    open spec fn der_remaining(
1342        &self,
1343        value: (TA::V, TB::V),
1344        state: PairDerState<A::State, B::State>,
1345    ) -> Seq<u8> {
1346        if state.in_left {
1347            self.0.der_remaining(value.0, state.left) + self.1.der_remaining(value.1, state.right)
1348        } else {
1349            self.1.der_remaining(value.1, state.right)
1350        }
1351    }
1352
1353    open spec fn der_state_valid(
1354        &self,
1355        value: (TA::V, TB::V),
1356        state: PairDerState<A::State, B::State>,
1357    ) -> bool {
1358        &&& self.0.der_state_valid(value.0, state.left)
1359        &&& self.1.der_state_valid(value.1, state.right)
1360        &&& !state.in_left ==> self.0.der_remaining(value.0, state.left).len() == 0
1361    }
1362
1363    fn der_start(&self, v: &(TA, TB)) -> (state: PairDerState<A::State, B::State>) {
1364        let left = self.0.der_start(&v.0);
1365        let right = self.1.der_start(&v.1);
1366        let state = PairDerState { left, right, in_left: true };
1367        proof {
1368            good_start!(self, v.deep_view(), state);
1369        }
1370        state
1371    }
1372
1373    fn der_next(&self, v: &(TA, TB), state: &mut PairDerState<A::State, B::State>) -> (next: Option<
1374        u8,
1375    >) {
1376        if state.in_left {
1377            match self.0.der_next(&v.0, &mut state.left) {
1378                Some(byte) => {
1379                    return Some(byte);
1380                },
1381                None => state.in_left = false,
1382            }
1383        }
1384        let next = self.1.der_next(&v.1, &mut state.right);
1385        next
1386    }
1387}
1388
1389impl DerState for BitStringFmt<true> {
1390    type State = PairDerState<bool, BytesDerState>;
1391}
1392
1393impl<'a> DerOrd<BitString<'a, true>> for BitStringFmt<true> {
1394    proof fn lemma_der_serialize_len(&self, value: BitStringSpec) {
1395        <Pair<U8, Tail> as DerOrd<(u8, &'a [u8])>>::lemma_der_serialize_len(
1396            &Pair(U8, Tail),
1397            (value.unused, value.bits),
1398        );
1399        crate::asn1::bitstring::lemma_bit_string_fmt_serialization::<true>(value);
1400    }
1401
1402    open spec fn der_remaining(
1403        &self,
1404        value: BitStringSpec,
1405        state: PairDerState<bool, BytesDerState>,
1406    ) -> Seq<u8> {
1407        <Pair<U8, Tail> as DerOrd<(u8, &'a [u8])>>::der_remaining(
1408            &Pair(U8, Tail),
1409            (value.unused, value.bits),
1410            state,
1411        )
1412    }
1413
1414    open spec fn der_state_valid(
1415        &self,
1416        value: BitStringSpec,
1417        state: PairDerState<bool, BytesDerState>,
1418    ) -> bool {
1419        <Pair<U8, Tail> as DerOrd<(u8, &'a [u8])>>::der_state_valid(
1420            &Pair(U8, Tail),
1421            (value.unused, value.bits),
1422            state,
1423        )
1424    }
1425
1426    fn der_start(&self, b: &BitString<'a, true>) -> (state: PairDerState<bool, BytesDerState>) {
1427        let pair = (b.unused(), b.bits());
1428        proof {
1429            crate::asn1::bitstring::lemma_bit_string_fmt_serialization::<true>(b.deep_view());
1430        }
1431        let state = Pair(U8, Tail).der_start(&pair);
1432        proof {
1433            good_start!(self, b.deep_view(), state);
1434        }
1435        state
1436    }
1437
1438    fn der_next(
1439        &self,
1440        b: &BitString<'a, true>,
1441        state: &mut PairDerState<bool, BytesDerState>,
1442    ) -> (next: Option<u8>) {
1443        let pair = (b.unused(), b.bits());
1444        let next = Pair(U8, Tail).der_next(&pair, state);
1445        next
1446    }
1447}
1448
1449type AnyDerInnerFmt = Pair<TagFmt, Pair<LengthFmt<true>, Tail>>;
1450
1451pub type AnyDerState = PairDerState<TagDerState, PairDerState<LengthDerState, BytesDerState>>;
1452
1453impl DerState for AnyFmt<true> {
1454    type State = AnyDerState;
1455}
1456
1457impl<'a> DerOrd<Any<'a>> for AnyFmt<true> {
1458    proof fn lemma_der_serialize_len(&self, value: AnySpec) {
1459        <AnyDerInnerFmt as DerOrd<(Tag, (usize, &'a [u8]))>>::lemma_der_serialize_len(
1460            &Pair(TagFmt, Pair(LengthFmt::<true>, Tail)),
1461            (value.tag, (value.content.len() as usize, value.content)),
1462        );
1463    }
1464
1465    open spec fn der_remaining(&self, value: AnySpec, state: AnyDerState) -> Seq<u8> {
1466        <AnyDerInnerFmt as DerOrd<(Tag, (usize, &'a [u8]))>>::der_remaining(
1467            &Pair(TagFmt, Pair(LengthFmt::<true>, Tail)),
1468            (value.tag, (value.content.len() as usize, value.content)),
1469            state,
1470        )
1471    }
1472
1473    open spec fn der_state_valid(&self, value: AnySpec, state: AnyDerState) -> bool {
1474        <AnyDerInnerFmt as DerOrd<(Tag, (usize, &'a [u8]))>>::der_state_valid(
1475            &Pair(TagFmt, Pair(LengthFmt::<true>, Tail)),
1476            (value.tag, (value.content.len() as usize, value.content)),
1477            state,
1478        )
1479    }
1480
1481    fn der_start(&self, a: &Any<'a>) -> (state: AnyDerState) {
1482        let tag = a.tag();
1483        let content = a.content();
1484        let len = content.len();
1485        let pair = (tag, (len, content));
1486        let state = Pair(TagFmt, Pair(LengthFmt::<true>, Tail)).der_start(&pair);
1487        proof {
1488            good_start!(self, a.deep_view(), state);
1489        }
1490        state
1491    }
1492
1493    fn der_next(&self, a: &Any<'a>, state: &mut AnyDerState) -> (next: Option<u8>) {
1494        let tag = a.tag();
1495        let content = a.content();
1496        let len = content.len();
1497        let pair = (tag, (len, content));
1498        let next = Pair(TagFmt, Pair(LengthFmt::<true>, Tail)).der_next(&pair, state);
1499        next
1500    }
1501}
1502
1503/// Cursor for a binary choice.
1504#[verifier::allow(autoderive_clone_without_spec)]
1505#[derive(Copy, Clone)]
1506pub enum ChoiceDerState<Left, Right> {
1507    Left(Left),
1508    Right(Right),
1509}
1510
1511impl<Left: Default, Right> Default for ChoiceDerState<Left, Right> {
1512    fn default() -> (state: Self) {
1513        ChoiceDerState::Left(Left::default())
1514    }
1515}
1516
1517impl<A: DerState, B: DerState> DerState for Choice<A, B> {
1518    type State = ChoiceDerState<A::State, B::State>;
1519}
1520
1521impl<A, B, TA, TB> DerOrd<Sum<TA, TB>> for Choice<A, B> where
1522    TA: DeepView,
1523    TB: DeepView,
1524    A: DerOrd<TA>,
1525    B: DerOrd<TB>,
1526 {
1527    proof fn lemma_der_serialize_len(&self, value: Sum<TA::V, TB::V>) {
1528        match value {
1529            Sum::Inl(value) => self.0.lemma_der_serialize_len(value),
1530            Sum::Inr(value) => self.1.lemma_der_serialize_len(value),
1531        }
1532    }
1533
1534    open spec fn der_remaining(
1535        &self,
1536        value: Sum<TA::V, TB::V>,
1537        state: ChoiceDerState<A::State, B::State>,
1538    ) -> Seq<u8> {
1539        match (value, state) {
1540            (Sum::Inl(value), ChoiceDerState::Left(state)) => { self.0.der_remaining(value, state)
1541            },
1542            (Sum::Inr(value), ChoiceDerState::Right(state)) => { self.1.der_remaining(value, state)
1543            },
1544            _ => Seq::empty(),
1545        }
1546    }
1547
1548    open spec fn der_state_valid(
1549        &self,
1550        value: Sum<TA::V, TB::V>,
1551        state: ChoiceDerState<A::State, B::State>,
1552    ) -> bool {
1553        match (value, state) {
1554            (Sum::Inl(value), ChoiceDerState::Left(state)) => { self.0.der_state_valid(value, state)
1555            },
1556            (Sum::Inr(value), ChoiceDerState::Right(state)) => {
1557                self.1.der_state_valid(value, state)
1558            },
1559            _ => false,
1560        }
1561    }
1562
1563    fn der_start(&self, v: &Sum<TA, TB>) -> (state: ChoiceDerState<A::State, B::State>) {
1564        let state = match v {
1565            Sum::Inl(value) => ChoiceDerState::Left(self.0.der_start(value)),
1566            Sum::Inr(value) => ChoiceDerState::Right(self.1.der_start(value)),
1567        };
1568        proof {
1569            good_start!(self, v.deep_view(), state);
1570        }
1571        state
1572    }
1573
1574    fn der_next(&self, v: &Sum<TA, TB>, state: &mut ChoiceDerState<A::State, B::State>) -> (next:
1575        Option<u8>) {
1576        let next = match (v, &mut *state) {
1577            (Sum::Inl(value), ChoiceDerState::Left(state)) => self.0.der_next(value, state),
1578            (Sum::Inr(value), ChoiceDerState::Right(state)) => self.1.der_next(value, state),
1579            _ => {
1580                proof {
1581                    assert(false);
1582                }
1583                None
1584            },
1585        };
1586        next
1587    }
1588}
1589
1590/// Cursor for an optional value.
1591#[verifier::allow(autoderive_clone_without_spec)]
1592#[derive(Copy, Clone)]
1593pub enum OptDerState<Inner> {
1594    Some(Inner),
1595    None,
1596}
1597
1598impl<Inner> Default for OptDerState<Inner> {
1599    fn default() -> (state: Self) {
1600        OptDerState::None
1601    }
1602}
1603
1604impl<A: DerState> DerState for Opt<A> {
1605    type State = OptDerState<A::State>;
1606}
1607
1608impl<A, T> DerOrd<Option<T>> for Opt<A> where T: DeepView, A: DerOrd<T> {
1609    proof fn lemma_der_serialize_len(&self, value: Option<T::V>) {
1610        if let Some(value) = value {
1611            self.0.lemma_der_serialize_len(value);
1612        }
1613    }
1614
1615    open spec fn der_remaining(&self, value: Option<T::V>, state: OptDerState<A::State>) -> Seq<
1616        u8,
1617    > {
1618        match (value, state) {
1619            (Some(value), OptDerState::Some(state)) => self.0.der_remaining(value, state),
1620            (None, OptDerState::None) => Seq::empty(),
1621            _ => Seq::empty(),
1622        }
1623    }
1624
1625    open spec fn der_state_valid(&self, value: Option<T::V>, state: OptDerState<A::State>) -> bool {
1626        match (value, state) {
1627            (Some(value), OptDerState::Some(state)) => self.0.der_state_valid(value, state),
1628            (None, OptDerState::None) => true,
1629            _ => false,
1630        }
1631    }
1632
1633    fn der_start(&self, o: &Option<T>) -> (state: OptDerState<A::State>) {
1634        let state = match o {
1635            Some(value) => OptDerState::Some(self.0.der_start(value)),
1636            None => OptDerState::None,
1637        };
1638        proof {
1639            good_start!(self, o.deep_view(), state);
1640        }
1641        state
1642    }
1643
1644    fn der_next(&self, o: &Option<T>, state: &mut OptDerState<A::State>) -> (next: Option<u8>) {
1645        let next = match (o, &mut *state) {
1646            (Some(value), OptDerState::Some(state)) => self.0.der_next(value, state),
1647            (None, OptDerState::None) => None,
1648            _ => {
1649                proof {
1650                    assert(false);
1651                }
1652                None
1653            },
1654        };
1655        next
1656    }
1657}
1658
1659impl<A: DerState, B: DerState> DerState for Optional<A, B> {
1660    type State = PairDerState<OptDerState<A::State>, B::State>;
1661}
1662
1663impl<A, B, TA, TB> DerOrd<(Option<TA>, TB)> for Optional<A, B> where
1664    TA: DeepView,
1665    TB: DeepView,
1666    A: DerOrd<TA>,
1667    B: DerOrd<TB>,
1668 {
1669    proof fn lemma_der_serialize_len(&self, value: (Option<TA::V>, TB::V)) {
1670        if let Some(left) = value.0 {
1671            self.0.lemma_der_serialize_len(left);
1672        }
1673        self.1.lemma_der_serialize_len(value.1);
1674    }
1675
1676    open spec fn der_remaining(
1677        &self,
1678        value: (Option<TA::V>, TB::V),
1679        state: PairDerState<OptDerState<A::State>, B::State>,
1680    ) -> Seq<u8> {
1681        if state.in_left {
1682            (match (&value.0, &state.left) {
1683                (Some(value), OptDerState::Some(inner)) => { self.0.der_remaining(*value, *inner) },
1684                (None, OptDerState::None) => Seq::empty(),
1685                _ => Seq::empty(),
1686            }) + self.1.der_remaining(value.1, state.right)
1687        } else {
1688            self.1.der_remaining(value.1, state.right)
1689        }
1690    }
1691
1692    open spec fn der_state_valid(
1693        &self,
1694        value: (Option<TA::V>, TB::V),
1695        state: PairDerState<OptDerState<A::State>, B::State>,
1696    ) -> bool {
1697        &&& match (&value.0, &state.left) {
1698            (Some(value), OptDerState::Some(inner)) => self.0.der_state_valid(*value, *inner),
1699            (None, OptDerState::None) => true,
1700            _ => false,
1701        }
1702        &&& self.1.der_state_valid(value.1, state.right)
1703        &&& !state.in_left ==> {
1704            match (&value.0, &state.left) {
1705                (Some(value), OptDerState::Some(inner)) => {
1706                    self.0.der_remaining(*value, *inner).len() == 0
1707                },
1708                (None, OptDerState::None) => true,
1709                _ => false,
1710            }
1711        }
1712    }
1713
1714    fn der_start(&self, o: &(Option<TA>, TB)) -> (state: PairDerState<
1715        OptDerState<A::State>,
1716        B::State,
1717    >) {
1718        let left = match &o.0 {
1719            Some(value) => OptDerState::Some(self.0.der_start(value)),
1720            None => OptDerState::None,
1721        };
1722        let right = self.1.der_start(&o.1);
1723        let state = PairDerState { left, right, in_left: true };
1724        proof {
1725            good_start!(self, o.deep_view(), state);
1726        }
1727        state
1728    }
1729
1730    fn der_next(
1731        &self,
1732        o: &(Option<TA>, TB),
1733        state: &mut PairDerState<OptDerState<A::State>, B::State>,
1734    ) -> (next: Option<u8>) {
1735        if state.in_left {
1736            let field = match (&o.0, &mut state.left) {
1737                (Some(value), OptDerState::Some(inner)) => self.0.der_next(value, inner),
1738                (None, OptDerState::None) => None,
1739                _ => {
1740                    proof {
1741                        assert(false);
1742                    }
1743                    None
1744                },
1745            };
1746            match field {
1747                Some(byte) => {
1748                    return Some(byte);
1749                },
1750                None => state.in_left = false,
1751            }
1752        }
1753        let next = self.1.der_next(&o.1, &mut state.right);
1754        next
1755    }
1756}
1757
1758/// Cursor for a concatenated collection.
1759#[verifier::allow(autoderive_clone_without_spec)]
1760#[derive(Copy, Clone, Default)]
1761pub struct StarDerState<Inner> {
1762    pub index: usize,
1763    pub current: Inner,
1764}
1765
1766impl<A: DerState> DerState for Star<A> {
1767    type State = StarDerState<A::State>;
1768}
1769
1770broadcast proof fn lemma_star_consistent_index<A: Consistency>(
1771    inner: A,
1772    values: Seq<A::Val>,
1773    index: int,
1774)
1775    requires
1776        Star(inner).consistent(values),
1777        0 <= index < values.len(),
1778    ensures
1779        #[trigger] inner.consistent(values[index]),
1780{
1781    reveal(<Star<_> as Consistency>::consistent);
1782}
1783
1784proof fn lemma_star_der_serialize_len<A, T>(inner: A, values: Seq<T::V>) where
1785    T: DeepView,
1786    A: DerOrd<T> + Copy,
1787
1788    requires
1789        Star(inner).consistent(values),
1790    ensures
1791        Star(inner).spec_serialize(values).len() == Star(inner).byte_len(values),
1792    decreases values.len(),
1793{
1794    reveal(<Star<_> as Consistency>::consistent);
1795    reveal(<Star<_> as SpecSerializer>::spec_serialize);
1796    reveal(<Star<_> as SpecByteLen>::byte_len);
1797    broadcast use lemma_star_consistent_index;
1798
1799    if values.len() > 0 {
1800        let prefix = values.drop_last();
1801        let last = values.last();
1802        lemma_star_der_serialize_len::<A, T>(inner, prefix);
1803        inner.lemma_der_serialize_len(last);
1804    }
1805}
1806
1807#[cfg(feature = "alloc")]
1808impl<A, T> DerOrd<Vec<T>> for Star<A> where T: DeepView, A: DerOrd<T> + Copy {
1809    proof fn lemma_der_serialize_len(&self, vs: Seq<T::V>) {
1810        lemma_star_der_serialize_len::<A, T>(self.0, vs);
1811    }
1812
1813    open spec fn der_remaining(&self, vs: Seq<T::V>, state: StarDerState<A::State>) -> Seq<u8> {
1814        if state.index < vs.len() {
1815            self.0.der_remaining(vs[state.index as int], state.current) + Star(
1816                self.0,
1817            ).spec_serialize(vs.skip(state.index as int + 1))
1818        } else {
1819            Seq::empty()
1820        }
1821    }
1822
1823    open spec fn der_state_valid(&self, vs: Seq<T::V>, state: StarDerState<A::State>) -> bool {
1824        &&& state.index <= vs.len()
1825        &&& state.index < vs.len() ==> {
1826            self.0.der_state_valid(vs[state.index as int], state.current)
1827        }
1828    }
1829
1830    fn der_start(&self, v: &Vec<T>) -> (state: StarDerState<A::State>) {
1831        reveal(<Star<_> as SpecSerializer>::spec_serialize);
1832
1833        let state = if v.len() == 0 {
1834            let current = A::State::default();
1835            StarDerState { index: 0, current }
1836        } else {
1837            proof {
1838                lemma_star_consistent_index(self.0, v.deep_view(), 0);
1839            }
1840            let state = StarDerState { index: 0, current: self.0.der_start(&v[0]) };
1841            proof {
1842                let vv = v.deep_view();
1843                Star(self.0).lemma_spec_serialize_suffix_step(vv, 0);
1844                assert(self.0.der_remaining(vv[0], state.current) == self.0.spec_serialize(vv[0]));
1845                assert(vv.skip(0) == vv);
1846            }
1847            state
1848        };
1849        proof {
1850            good_start!(self, v.deep_view(), state);
1851        }
1852        state
1853    }
1854
1855    #[verifier::loop_isolation(false)]
1856    fn der_next(&self, v: &Vec<T>, state: &mut StarDerState<A::State>) -> (next: Option<u8>) {
1857        broadcast use lemma_star_consistent_index;
1858
1859        let ghost vv = v.deep_view();
1860
1861        loop
1862            invariant
1863                self.der_state_valid(vv, *state),
1864                self.der_remaining(vv, *state) == self.der_remaining(vv, *old(state)),
1865                state.index <= v.len(),
1866            decreases v.len() - state.index,
1867        {
1868            if state.index == v.len() {
1869                return None;
1870            }
1871            let idx = state.index;
1872            if let Some(byte) = self.0.der_next(&v[idx], &mut state.current) {
1873                return Some(byte);
1874            } else {
1875                let new_idx = idx + 1;
1876                state.index = new_idx;
1877                if new_idx < v.len() {
1878                    proof {
1879                        lemma_star_consistent_index(self.0, vv, new_idx as int);
1880                    }
1881                    state.current = self.0.der_start(&v[new_idx]);
1882                }
1883                proof {
1884                    if new_idx < vv.len() {
1885                        assert(self.0.der_remaining(vv[new_idx as int], state.current)
1886                            == self.0.spec_serialize(vv[new_idx as int]));
1887                        Star(self.0).lemma_spec_serialize_suffix_step(vv, new_idx as int);
1888                    } else {
1889                        reveal(<Star<_> as SpecSerializer>::spec_serialize);
1890                    }
1891                }
1892            }
1893        }
1894    }
1895}
1896
1897impl<Inner: DerState, P> DerState for Refined<Inner, P> {
1898    type State = Inner::State;
1899}
1900
1901impl<Inner, P, T> DerOrd<T> for Refined<Inner, P> where T: DeepView, Inner: DerOrd<T>, P: Pred<T> {
1902    proof fn lemma_der_serialize_len(&self, value: T::V) {
1903        self.0.lemma_der_serialize_len(value);
1904    }
1905
1906    open spec fn der_remaining(&self, value: T::V, state: Inner::State) -> Seq<u8> {
1907        self.0.der_remaining(value, state)
1908    }
1909
1910    open spec fn der_state_valid(&self, value: T::V, state: Inner::State) -> bool {
1911        self.0.der_state_valid(value, state)
1912    }
1913
1914    fn der_start(&self, v: &T) -> (state: Inner::State) {
1915        let state = self.0.der_start(v);
1916        proof {
1917            good_start!(self, v.deep_view(), state);
1918        }
1919        state
1920    }
1921
1922    fn der_next(&self, v: &T, state: &mut Inner::State) -> (next: Option<u8>) {
1923        let next = self.0.der_next(v, state);
1924        next
1925    }
1926}
1927
1928impl<Inner: DerState> DerState for Ref<Inner> {
1929    type State = Inner::State;
1930}
1931
1932impl<Inner, T> DerOrd<&T> for Ref<Inner> where T: DeepView + ?Sized, Inner: DerOrd<T> {
1933    proof fn lemma_der_serialize_len(&self, value: T::V) {
1934        self.0.lemma_der_serialize_len(value);
1935    }
1936
1937    open spec fn der_remaining(&self, value: T::V, state: Inner::State) -> Seq<u8> {
1938        self.0.der_remaining(value, state)
1939    }
1940
1941    open spec fn der_state_valid(&self, value: T::V, state: Inner::State) -> bool {
1942        self.0.der_state_valid(value, state)
1943    }
1944
1945    fn der_start(&self, v: &&T) -> (state: Inner::State) {
1946        let state = self.0.der_start(*v);
1947        proof {
1948            good_start!(self, v.deep_view(), state);
1949        }
1950        state
1951    }
1952
1953    fn der_next(&self, v: &&T, state: &mut Inner::State) -> (next: Option<u8>) {
1954        let next = self.0.der_next(*v, state);
1955        next
1956    }
1957}
1958
1959impl<Inner: DerState, M, MRev> DerState for Mapped<Inner, BiMap<M, MRev>> {
1960    type State = Inner::State;
1961}
1962
1963impl<Inner, M, MRev, T> DerOrd<T> for Mapped<Inner, BiMap<M, MRev>> where
1964    T: DeepView,
1965    M: SpecMap<Input = MRev::Output, Output = T::V>,
1966    MRev: SpecMap<Input = T::V> + for <'x>Map<&'x T>,
1967    Inner: DerState,
1968    for <'x>Inner: DerOrd<<MRev as Map<&'x T>>::O>,
1969 {
1970    proof fn lemma_der_serialize_len(&self, value: T::V) {
1971        let inner = self.mapper.1.spec_map(value);
1972        self.inner.lemma_der_serialize_len(inner);
1973    }
1974
1975    open spec fn der_remaining(&self, value: T::V, state: Inner::State) -> Seq<u8> {
1976        self.inner.der_remaining(self.mapper.1.spec_map(value), state)
1977    }
1978
1979    open spec fn der_state_valid(&self, value: T::V, state: Inner::State) -> bool {
1980        self.inner.der_state_valid(self.mapper.1.spec_map(value), state)
1981    }
1982
1983    fn der_start(&self, v: &T) -> (state: Inner::State) {
1984        let inner = self.mapper.1.map(v);
1985        let state = self.inner.der_start(&inner);
1986        proof {
1987            good_start!(self, v.deep_view(), state);
1988        }
1989        state
1990    }
1991
1992    fn der_next(&self, v: &T, state: &mut Inner::State) -> (next: Option<u8>) {
1993        let inner = self.mapper.1.map(v);
1994        let next = self.inner.der_next(&inner, state);
1995        next
1996    }
1997}
1998
1999#[cfg(feature = "alloc")]
2000impl<A: DerState> DerState for RepeatTillEnd<A> {
2001    type State = StarDerState<A::State>;
2002}
2003
2004#[cfg(feature = "alloc")]
2005impl<A, T> DerOrd<Vec<T>> for RepeatTillEnd<A> where T: DeepView, A: DerOrd<T> + Copy {
2006    proof fn lemma_der_serialize_len(&self, values: Seq<T::V>) {
2007        Star(self.0).lemma_der_serialize_len(values);
2008    }
2009
2010    open spec fn der_remaining(&self, values: Seq<T::V>, state: StarDerState<A::State>) -> Seq<u8> {
2011        Star(self.0).der_remaining(values, state)
2012    }
2013
2014    open spec fn der_state_valid(&self, values: Seq<T::V>, state: StarDerState<A::State>) -> bool {
2015        Star(self.0).der_state_valid(values, state)
2016    }
2017
2018    fn der_start(&self, v: &Vec<T>) -> (state: StarDerState<A::State>) {
2019        let state = Star(self.0).der_start(v);
2020        proof {
2021            good_start!(self, v.deep_view(), state);
2022        }
2023        state
2024    }
2025
2026    fn der_next(&self, v: &Vec<T>, state: &mut StarDerState<A::State>) -> (next: Option<u8>) {
2027        let next = Star(self.0).der_next(v, state);
2028        next
2029    }
2030}
2031
2032#[cfg(feature = "alloc")]
2033#[derive(Copy, Clone, Default)]
2034pub struct BmpStringDerState {
2035    pub char_index: usize,
2036    pub second_octet: bool,
2037}
2038
2039#[cfg(feature = "alloc")]
2040impl DerState for BmpStringFmt {
2041    type State = BmpStringDerState;
2042}
2043
2044#[cfg(feature = "alloc")]
2045pub open spec fn bmp_string_der_position(state: BmpStringDerState) -> nat {
2046    state.char_index as nat * 2 + if state.second_octet {
2047        1nat
2048    } else {
2049        0nat
2050    }
2051}
2052
2053#[cfg(feature = "alloc")]
2054impl DerOrd<BmpString> for BmpStringFmt {
2055    proof fn lemma_der_serialize_len(&self, value: BmpStringSpec) {
2056        crate::asn1::bmpstring::lemma_bmp_string_fmt_serialization(value);
2057    }
2058
2059    open spec fn der_remaining(&self, value: BmpStringSpec, state: BmpStringDerState) -> Seq<u8> {
2060        self.spec_serialize(value).skip(bmp_string_der_position(state) as int)
2061    }
2062
2063    open spec fn der_state_valid(&self, value: BmpStringSpec, state: BmpStringDerState) -> bool {
2064        &&& state.char_index <= value.inner.len()
2065        &&& state.char_index == value.inner.len() ==> !state.second_octet
2066    }
2067
2068    fn der_start(&self, s: &BmpString) -> (state: BmpStringDerState) {
2069        let state = BmpStringDerState { char_index: 0, second_octet: false };
2070        proof {
2071            crate::asn1::bmpstring::lemma_bmp_string_fmt_serialization(s.deep_view());
2072            good_start!(self, s.deep_view(), state);
2073        }
2074        state
2075    }
2076
2077    fn der_next(&self, s: &BmpString, state: &mut BmpStringDerState) -> (next: Option<u8>) {
2078        proof {
2079            crate::asn1::bmpstring::lemma_bmp_string_fmt_serialization(s.deep_view());
2080        }
2081        let inner = s.inner();
2082        let len = inner.unicode_len();
2083        if state.char_index == len {
2084            None
2085        } else {
2086            let c = inner.get_char(state.char_index);
2087            let encoded = crate::combinators::uints::exec::u16_to_be_bytes(c as u16);
2088            let byte;
2089            if state.second_octet {
2090                byte = encoded[1];
2091                state.char_index += 1;
2092                state.second_octet = false;
2093            } else {
2094                byte = encoded[0];
2095                state.second_octet = true;
2096            }
2097            Some(byte)
2098        }
2099    }
2100}
2101
2102#[cfg(feature = "alloc")]
2103#[derive(Copy, Clone, Default)]
2104pub struct UniversalStringDerState {
2105    pub char_index: usize,
2106    pub octet_index: u8,
2107}
2108
2109#[cfg(feature = "alloc")]
2110impl DerState for UniversalStringFmt {
2111    type State = UniversalStringDerState;
2112}
2113
2114#[cfg(feature = "alloc")]
2115pub open spec fn universal_string_der_position(state: UniversalStringDerState) -> nat {
2116    state.char_index as nat * 4 + state.octet_index as nat
2117}
2118
2119#[cfg(feature = "alloc")]
2120impl DerOrd<UniversalString> for UniversalStringFmt {
2121    proof fn lemma_der_serialize_len(&self, value: Seq<char>) {
2122        crate::asn1::universalstring::lemma_universal_string_fmt_serialization(value);
2123    }
2124
2125    open spec fn der_remaining(&self, value: Seq<char>, state: UniversalStringDerState) -> Seq<u8> {
2126        self.spec_serialize(value).skip(universal_string_der_position(state) as int)
2127    }
2128
2129    open spec fn der_state_valid(&self, value: Seq<char>, state: UniversalStringDerState) -> bool {
2130        &&& state.char_index <= value.len()
2131        &&& state.octet_index < 4
2132        &&& state.char_index == value.len() ==> state.octet_index == 0
2133    }
2134
2135    fn der_start(&self, value: &UniversalString) -> (state: UniversalStringDerState) {
2136        let state = UniversalStringDerState { char_index: 0, octet_index: 0 };
2137        proof {
2138            crate::asn1::universalstring::lemma_universal_string_fmt_serialization(
2139                value.deep_view(),
2140            );
2141            good_start!(self, value.deep_view(), state);
2142        }
2143        state
2144    }
2145
2146    fn der_next(&self, value: &UniversalString, state: &mut UniversalStringDerState) -> (next:
2147        Option<u8>) {
2148        proof {
2149            crate::asn1::universalstring::lemma_universal_string_fmt_serialization(
2150                value.deep_view(),
2151            );
2152        }
2153        let inner = value.as_str();
2154        let len = inner.unicode_len();
2155        if state.char_index == len {
2156            None
2157        } else {
2158            let c = inner.get_char(state.char_index);
2159            let encoded = crate::combinators::uints::exec::u32_to_be_bytes(c as u32);
2160            let byte = encoded[state.octet_index as usize];
2161            if state.octet_index == 3 {
2162                state.char_index += 1;
2163                state.octet_index = 0;
2164            } else {
2165                state.octet_index += 1;
2166            }
2167            Some(byte)
2168        }
2169    }
2170}
2171
2172#[cfg(feature = "alloc")]
2173pub type ObjectIdentifierDerState = PairDerState<Base128DerState, StarDerState<Base128DerState>>;
2174
2175#[cfg(feature = "alloc")]
2176impl DerState for ObjectIdentifierFmt {
2177    type State = ObjectIdentifierDerState;
2178}
2179
2180#[cfg(feature = "alloc")]
2181impl DerOrd<ObjectIdentifier> for ObjectIdentifierFmt {
2182    proof fn lemma_der_serialize_len(&self, value: ObjectIdentifierSpec) {
2183        <crate::asn1::oid::ObjectIdentifierInnerFmt as DerOrd<
2184            (u64, Vec<u64>),
2185        >>::lemma_der_serialize_len(
2186            &crate::asn1::oid::object_identifier_inner(),
2187            crate::asn1::oid::oid_to_subidentifiers(value),
2188        );
2189    }
2190
2191    open spec fn der_remaining(
2192        &self,
2193        value: ObjectIdentifierSpec,
2194        state: ObjectIdentifierDerState,
2195    ) -> Seq<u8> {
2196        if state.in_left {
2197            Base128Fmt::<true>.der_remaining(
2198                crate::asn1::oid::oid_first_subidentifier(value),
2199                state.left,
2200            ) + RepeatTillEnd(Base128Fmt::<true>).der_remaining(value.rest, state.right)
2201        } else {
2202            RepeatTillEnd(Base128Fmt::<true>).der_remaining(value.rest, state.right)
2203        }
2204    }
2205
2206    open spec fn der_state_valid(
2207        &self,
2208        value: ObjectIdentifierSpec,
2209        state: ObjectIdentifierDerState,
2210    ) -> bool {
2211        &&& Base128Fmt::<true>.der_state_valid(
2212            crate::asn1::oid::oid_first_subidentifier(value),
2213            state.left,
2214        )
2215        &&& RepeatTillEnd(Base128Fmt::<true>).der_state_valid(value.rest, state.right)
2216        &&& !state.in_left ==> Base128Fmt::<true>.der_remaining(
2217            crate::asn1::oid::oid_first_subidentifier(value),
2218            state.left,
2219        ).len() == 0
2220    }
2221
2222    fn der_start(&self, o: &ObjectIdentifier) -> (state: ObjectIdentifierDerState) {
2223        let combined = o.combined_first_subidentifier();
2224        let rest = o.rest_vec();
2225        let left = Base128Fmt::<true>.der_start(&combined);
2226        let right = RepeatTillEnd(Base128Fmt::<true>).der_start(rest);
2227        let state = PairDerState { left, right, in_left: true };
2228        proof {
2229            good_start!(self, o.deep_view(), state);
2230        }
2231        state
2232    }
2233
2234    fn der_next(&self, o: &ObjectIdentifier, state: &mut ObjectIdentifierDerState) -> (next: Option<
2235        u8,
2236    >) {
2237        let combined = o.combined_first_subidentifier();
2238        let rest = o.rest_vec();
2239        if state.in_left {
2240            match Base128Fmt::<true>.der_next(&combined, &mut state.left) {
2241                Some(byte) => {
2242                    return Some(byte);
2243                },
2244                None => state.in_left = false,
2245            }
2246        }
2247        let next = RepeatTillEnd(Base128Fmt::<true>).der_next(rest, &mut state.right);
2248        next
2249    }
2250}
2251
2252#[cfg(feature = "alloc")]
2253impl<A: DerState> DerState for SetOfFmt<A> {
2254    type State = StarDerState<A::State>;
2255}
2256
2257#[cfg(feature = "alloc")]
2258impl<A, T> DerOrd<Vec<T>> for SetOfFmt<A> where T: DeepView, A: DerOrd<T> + Copy {
2259    proof fn lemma_der_serialize_len(&self, values: Seq<T::V>) {
2260        Star(self.0).lemma_der_serialize_len(values);
2261    }
2262
2263    open spec fn der_remaining(&self, values: Seq<T::V>, state: StarDerState<A::State>) -> Seq<u8> {
2264        Star(self.0).der_remaining(values, state)
2265    }
2266
2267    open spec fn der_state_valid(&self, values: Seq<T::V>, state: StarDerState<A::State>) -> bool {
2268        Star(self.0).der_state_valid(values, state)
2269    }
2270
2271    fn der_start(&self, v: &Vec<T>) -> (state: StarDerState<A::State>) {
2272        let state = Star(self.0).der_start(v);
2273        proof {
2274            good_start!(self, v.deep_view(), state);
2275        }
2276        state
2277    }
2278
2279    fn der_next(&self, v: &Vec<T>, state: &mut StarDerState<A::State>) -> (next: Option<u8>) {
2280        let next = Star(self.0).der_next(v, state);
2281        next
2282    }
2283}
2284
2285impl<F> DerState for ImplicitlyTaggedFmt<F> where F: Retaggable + DerState {
2286    type State = <F as DerState>::State;
2287}
2288
2289impl<F, T> DerOrd<T> for ImplicitlyTaggedFmt<F> where
2290    T: DeepView + ?Sized,
2291    F: Retaggable + DerOrd<T>,
2292 {
2293    proof fn lemma_der_serialize_len(&self, value: T::V) {
2294        self.1.spec_retagged(self.0).lemma_der_serialize_len(value);
2295    }
2296
2297    open spec fn der_remaining(&self, value: T::V, state: <F as DerState>::State) -> Seq<u8> {
2298        self.1.spec_retagged(self.0).der_remaining(value, state)
2299    }
2300
2301    open spec fn der_state_valid(&self, value: T::V, state: <F as DerState>::State) -> bool {
2302        self.1.spec_retagged(self.0).der_state_valid(value, state)
2303    }
2304
2305    fn der_start(&self, v: &T) -> (state: <F as DerState>::State) {
2306        let retagged = self.1.retagged(self.0);
2307        let state = retagged.der_start(v);
2308        proof {
2309            good_start!(self, v.deep_view(), state);
2310        }
2311        state
2312    }
2313
2314    fn der_next(&self, v: &T, state: &mut <F as DerState>::State) -> (next: Option<u8>) {
2315        let retagged = self.1.retagged(self.0);
2316        let next = retagged.der_next(v, state);
2317        next
2318    }
2319}
2320
2321impl<Field: DerState, Rest: DerState, Default> DerState for DefaultedFmt<
2322    Field,
2323    Default,
2324    Rest,
2325    true,
2326> {
2327    type State = PairDerState<OptDerState<Field::State>, Rest::State>;
2328}
2329
2330impl<Field, Default, Rest, R> DerOrd<(Default, R)> for DefaultedFmt<
2331    Field,
2332    Default,
2333    Rest,
2334    true,
2335> where
2336    Default: DeepViewIdentity + PartialEq + Structural,
2337    R: DeepView,
2338    Field: DerOrd<Default>,
2339    Rest: DerOrd<R>,
2340 {
2341    proof fn lemma_der_serialize_len(&self, value: (Default, R::V)) {
2342        if value.0 != self.1 {
2343            self.0.lemma_der_serialize_len(value.0);
2344        }
2345        self.2.lemma_der_serialize_len(value.1);
2346    }
2347
2348    open spec fn der_remaining(
2349        &self,
2350        value: (Default, R::V),
2351        state: PairDerState<OptDerState<Field::State>, Rest::State>,
2352    ) -> Seq<u8> {
2353        if state.in_left {
2354            (match (&value.0, &state.left) {
2355                (field, OptDerState::Some(inner)) if *field != self.1 => {
2356                    self.0.der_remaining(*field, *inner)
2357                },
2358                (field, OptDerState::None) if *field == self.1 => Seq::empty(),
2359                _ => Seq::empty(),
2360            }) + self.2.der_remaining(value.1, state.right)
2361        } else {
2362            self.2.der_remaining(value.1, state.right)
2363        }
2364    }
2365
2366    open spec fn der_state_valid(
2367        &self,
2368        value: (Default, R::V),
2369        state: PairDerState<OptDerState<Field::State>, Rest::State>,
2370    ) -> bool {
2371        &&& match (&value.0, &state.left) {
2372            (field, OptDerState::Some(inner)) if *field != self.1 => {
2373                self.0.der_state_valid(*field, *inner)
2374            },
2375            (field, OptDerState::None) if *field == self.1 => true,
2376            _ => false,
2377        }
2378        &&& self.2.der_state_valid(value.1, state.right)
2379        &&& !state.in_left ==> {
2380            match (&value.0, &state.left) {
2381                (field, OptDerState::Some(inner)) if *field != self.1 => {
2382                    self.0.der_remaining(*field, *inner).len() == 0
2383                },
2384                (field, OptDerState::None) if *field == self.1 => true,
2385                _ => false,
2386            }
2387        }
2388    }
2389
2390    fn der_start(&self, v: &(Default, R)) -> (state: PairDerState<
2391        OptDerState<Field::State>,
2392        Rest::State,
2393    >) {
2394        proof {
2395            v.0.lemma_deep_view_identity();
2396            self.1.lemma_deep_view_identity();
2397        }
2398        let left = if v.0 == self.1 {
2399            OptDerState::None
2400        } else {
2401            OptDerState::Some(self.0.der_start(&v.0))
2402        };
2403        let state = PairDerState { left, right: self.2.der_start(&v.1), in_left: true };
2404        proof {
2405            good_start!(self, v.deep_view(), state);
2406        }
2407        state
2408    }
2409
2410    fn der_next(
2411        &self,
2412        v: &(Default, R),
2413        state: &mut PairDerState<OptDerState<Field::State>, Rest::State>,
2414    ) -> (next: Option<u8>) {
2415        proof {
2416            v.0.lemma_deep_view_identity();
2417            self.1.lemma_deep_view_identity();
2418        }
2419        if state.in_left {
2420            let next = match (&v.0, &mut state.left) {
2421                (field, OptDerState::Some(inner)) => self.0.der_next(field, inner),
2422                (_, OptDerState::None) => None,
2423            };
2424            match next {
2425                Some(byte) => {
2426                    return Some(byte);
2427                },
2428                None => state.in_left = false,
2429            }
2430        }
2431        let next = self.2.der_next(&v.1, &mut state.right);
2432        next
2433    }
2434}
2435
2436} // verus!
vest_lib/asn1/der_ord.rs

vest_lib/asn1/
der_ord.rs
