vest_lib/asn1/
set_of.rs

1//! ASN.1 DER `SET OF` contents.
2//!
3//! The enclosing universal tag and DER length are supplied by [`ASN1Fmt`](crate::asn1::ASN1Fmt). Elements are
4//! ordered by their complete encodings, as required by X.690 §11.6.
5use super::DerOrd;
6use crate::combinators::{star::spec::*, Star};
7use crate::core::exec::output::*;
8use crate::core::{
9    exec::{
10        input::InputBuf,
11        parser::{PResult, Parser},
12        serializer::{ByteLen, PreSerializeError, Prepare, Serializer},
13        ParseError,
14    },
15    proof::*,
16    spec::*,
17};
18#[cfg(feature = "alloc")]
19use alloc::vec::Vec;
20use vstd::{prelude::*, relations::*};
21use OutputBuf;
22
23verus! {
24
25/// DER `SET OF` contents whose elements are encoded by `C`.
26///
27/// `C` must encode a complete DER element, including its tag and length. The parsed value is a
28/// `Vec<C::PT>` in canonical DER order. Duplicate encodings are permitted.
29#[derive(Copy)]
30pub struct SetOfFmt<C>(pub C);
31
32impl<C: Clone> Clone for SetOfFmt<C> {
33    fn clone(&self) -> (cloned: Self)
34        ensures
35            call_ensures(C::clone, (&self.0,), cloned.0),
36    {
37        SetOfFmt(self.0.clone())
38    }
39}
40
41/// The byte used at `i` when comparing DER encodings. X.690 §11.6 logically
42/// pads the shorter encoding with zero octets at its trailing end.
43pub open spec fn der_octet_at(bytes: Seq<u8>, i: nat) -> u8 {
44    if i < bytes.len() {
45        bytes[i as int]
46    } else {
47        0u8
48    }
49}
50
51pub open spec fn der_octets_drop_head(bytes: Seq<u8>) -> Seq<u8> {
52    if bytes.len() == 0 {
53        bytes
54    } else {
55        bytes.skip(1)
56    }
57}
58
59/// Whether complete element encodings are in nondecreasing DER order.
60/// Uses the encoded-component ordering from X.690 §11.6.
61pub open spec fn der_octets_leq(a: Seq<u8>, b: Seq<u8>) -> bool
62    decreases a.len() + b.len(),
63{
64    if a.len() == 0 && b.len() == 0 {
65        true
66    } else {
67        let left = der_octet_at(a, 0);
68        let right = der_octet_at(b, 0);
69        ||| left < right
70        ||| (left == right && der_octets_leq(der_octets_drop_head(a), der_octets_drop_head(b)))
71    }
72}
73
74pub open spec fn der_encodings_sorted(encodings: Seq<Seq<u8>>) -> bool {
75    sorted_by(encodings, |a: Seq<u8>, b: Seq<u8>| der_octets_leq(a, b))
76}
77
78/// Whether values are in the canonical order required by DER `SET OF`.
79pub open spec fn set_of_values_sorted<C: SpecSerializer>(inner: C, values: Seq<C::SVal>) -> bool {
80    der_encodings_sorted(values.map_values(|v: C::SVal| inner.spec_serialize(v)))
81}
82
83/// Expose the one-octet transition used by executable DER cursors.
84pub proof fn lemma_der_octets_leq_step(a: Seq<u8>, b: Seq<u8>)
85    requires
86        a.len() > 0 || b.len() > 0,
87    ensures
88        der_octet_at(a, 0) < der_octet_at(b, 0) ==> der_octets_leq(a, b),
89        der_octet_at(a, 0) > der_octet_at(b, 0) ==> !der_octets_leq(a, b),
90        der_octet_at(a, 0) == der_octet_at(b, 0) ==> {
91            der_octets_leq(a, b) == der_octets_leq(der_octets_drop_head(a), der_octets_drop_head(b))
92        },
93{
94}
95
96/// Padded DER octet ordering is transitive.
97pub proof fn lemma_der_octets_leq_transitive(a: Seq<u8>, b: Seq<u8>, c: Seq<u8>)
98    requires
99        der_octets_leq(a, b),
100        der_octets_leq(b, c),
101    ensures
102        der_octets_leq(a, c),
103    decreases a.len() + b.len() + c.len(),
104{
105    if a.len() > 0 || b.len() > 0 || c.len() > 0 {
106        if a.len() > 0 || b.len() > 0 {
107            lemma_der_octets_leq_step(a, b);
108        }
109        if b.len() > 0 || c.len() > 0 {
110            lemma_der_octets_leq_step(b, c);
111        }
112        if a.len() > 0 || c.len() > 0 {
113            lemma_der_octets_leq_step(a, c);
114        }
115        let ai = der_octet_at(a, 0);
116        let bi = der_octet_at(b, 0);
117        let ci = der_octet_at(c, 0);
118        if ai == bi && bi == ci {
119            lemma_der_octets_leq_transitive(
120                der_octets_drop_head(a),
121                der_octets_drop_head(b),
122                der_octets_drop_head(c),
123            );
124        }
125    }
126}
127
128proof fn lemma_sorted_by_index<T>(values: Seq<T>, leq: spec_fn(T, T) -> bool, i: int, j: int)
129    requires
130        sorted_by(values, leq),
131        0 <= i < j < values.len(),
132    ensures
133        leq(values[i], values[j]),
134{
135}
136
137pub proof fn lemma_der_encodings_sorted_index(encodings: Seq<Seq<u8>>, i: int, j: int)
138    requires
139        der_encodings_sorted(encodings),
140        0 <= i < j < encodings.len(),
141    ensures
142        der_octets_leq(encodings[i], encodings[j]),
143{
144    lemma_sorted_by_index(encodings, |a: Seq<u8>, b: Seq<u8>| der_octets_leq(a, b), i, j);
145}
146
147pub proof fn lemma_der_encodings_sorted_take(encodings: Seq<Seq<u8>>, n: int)
148    requires
149        der_encodings_sorted(encodings),
150        0 <= n <= encodings.len(),
151    ensures
152        der_encodings_sorted(encodings.take(n)),
153{
154    assert forall|i: int, j: int|
155        0 <= i < j < encodings.take(n).len() implies #[trigger] der_octets_leq(
156        encodings.take(n)[i],
157        encodings.take(n)[j],
158    ) by {
159        lemma_der_encodings_sorted_index(encodings, i, j);
160    }
161}
162
163/// Appending an encoding to a sorted prefix preserves sortedness exactly when it follows the
164/// previous last encoding. This uses transitivity of padded DER ordering, so callers only need an
165/// adjacent comparison.
166pub proof fn lemma_der_encodings_sorted_push(encodings: Seq<Seq<u8>>, current: Seq<u8>)
167    requires
168        der_encodings_sorted(encodings),
169    ensures
170        der_encodings_sorted(encodings.push(current)) <==> (encodings.len() == 0 || der_octets_leq(
171            encodings.last(),
172            current,
173        )),
174{
175    let extended = encodings.push(current);
176    if encodings.len() > 0 {
177        if der_octets_leq(encodings.last(), current) {
178            assert forall|i: int, j: int|
179                0 <= i < j < extended.len() implies #[trigger] der_octets_leq(
180                extended[i],
181                extended[j],
182            ) by {
183                if j < encodings.len() {
184                    lemma_der_encodings_sorted_index(encodings, i, j);
185                } else if i < encodings.len() - 1 {
186                    lemma_der_encodings_sorted_index(encodings, i, encodings.len() as int - 1);
187                    lemma_der_octets_leq_transitive(encodings[i], encodings.last(), current);
188                }
189            }
190        } else {
191            assert(!der_encodings_sorted(extended)) by {
192                if der_encodings_sorted(extended) {
193                    lemma_der_encodings_sorted_index(
194                        extended,
195                        encodings.len() as int - 1,
196                        encodings.len() as int,
197                    );
198                }
199            }
200        }
201    }
202}
203
204impl<C: SpecParser> SetOfFmt<C> {
205    /// Parses all remaining elements while maintaining a canonically sorted encoding prefix.
206    pub open spec fn parse_ordered(&self, ibuf: Seq<u8>, previous: Seq<Seq<u8>>) -> Option<
207        Seq<C::PVal>,
208    >
209        decreases ibuf.len(),
210    {
211        if !der_encodings_sorted(previous) {
212            None
213        } else if ibuf.len() == 0 {
214            Some(Seq::empty())
215        } else {
216            match self.0.spec_parse(ibuf) {
217                Some((n, v)) if 0 < n <= ibuf.len() && der_encodings_sorted(
218                    previous.push(ibuf.take(n)),
219                ) => {
220                    match self.parse_ordered(ibuf.skip(n), previous.push(ibuf.take(n))) {
221                        Some(values) => Some(seq![v] + values),
222                        None => None,
223                    }
224                },
225                _ => None,
226            }
227        }
228    }
229}
230
231impl<C: SoundParser> SetOfFmt<C> {
232    proof fn lemma_parse_ordered_byte_len(&self, ibuf: Seq<u8>, previous: Seq<Seq<u8>>)
233        requires
234            self.0.sound_inv(),
235            der_encodings_sorted(previous),
236        ensures
237            self.parse_ordered(ibuf, previous) matches Some(values) ==> {
238                ibuf.len() == Star(self.0).byte_len(values)
239            },
240        decreases ibuf.len(),
241    {
242        reveal(<Star<_> as SpecByteLen>::byte_len);
243
244        if ibuf.len() > 0 {
245            match self.0.spec_parse(ibuf) {
246                Some((n, value)) if 0 < n <= ibuf.len() && der_encodings_sorted(
247                    previous.push(ibuf.take(n)),
248                ) => {
249                    self.0.lemma_parse_sound_consumption(ibuf);
250                    self.lemma_parse_ordered_byte_len(ibuf.skip(n), previous.push(ibuf.take(n)));
251
252                    if let Some(rest_values) = self.parse_ordered(
253                        ibuf.skip(n),
254                        previous.push(ibuf.take(n)),
255                    ) {
256                        Star(self.0).lemma_byte_len_cons(value, rest_values);
257                    }
258                },
259                _ => {},
260            }
261        }
262    }
263}
264
265impl<C: SoundParser + PSRoundTrip> SetOfFmt<C> {
266    proof fn lemma_parse_ordered_consistent(&self, ibuf: Seq<u8>, previous: Seq<Seq<u8>>)
267        requires
268            self.0.sound_inv(),
269            self.0.ps_roundtrip_inv(),
270            der_encodings_sorted(previous),
271        ensures
272            self.parse_ordered(ibuf, previous) matches Some(values) ==> {
273                &&& Star(self.0).consistent(values)
274                &&& der_encodings_sorted(
275                    previous + values.map_values(|v: C::PVal| self.0.spec_serialize(v)),
276                )
277            },
278        decreases ibuf.len(),
279    {
280        reveal(<Star<_> as Consistency>::consistent);
281        broadcast use vstd::seq::group_seq_axioms;
282
283        if ibuf.len() > 0 {
284            match self.0.spec_parse(ibuf) {
285                Some((n, value)) if 0 < n <= ibuf.len() && der_encodings_sorted(
286                    previous.push(ibuf.take(n)),
287                ) => {
288                    self.0.lemma_parse_sound_value(ibuf);
289                    self.0.theorem_parse_serialize_roundtrip(ibuf);
290                    self.lemma_parse_ordered_consistent(ibuf.skip(n), previous.push(ibuf.take(n)));
291
292                    if let Some(rest_values) = self.parse_ordered(
293                        ibuf.skip(n),
294                        previous.push(ibuf.take(n)),
295                    ) {
296                        let values = seq![value] + rest_values;
297                        let serialize = |v: C::PVal| self.0.spec_serialize(v);
298                        assert(values.map_values(serialize) == seq![ibuf.take(n)]
299                            + rest_values.map_values(serialize));
300                        assert(previous + values.map_values(serialize) == previous.push(
301                            ibuf.take(n),
302                        ) + rest_values.map_values(serialize));
303                    }
304                },
305                _ => {},
306            }
307        }
308    }
309}
310
311impl<C: NonMalleable> SetOfFmt<C> {
312    proof fn lemma_parse_ordered_non_malleable(
313        &self,
314        buf1: Seq<u8>,
315        previous1: Seq<Seq<u8>>,
316        buf2: Seq<u8>,
317        previous2: Seq<Seq<u8>>,
318    )
319        requires
320            self.0.nonmal_inv(),
321            self.0.safe_inv(),
322            der_encodings_sorted(previous1),
323            der_encodings_sorted(previous2),
324        ensures
325            self.parse_ordered(buf1, previous1) matches Some(values1) ==> self.parse_ordered(
326                buf2,
327                previous2,
328            ) matches Some(values2) ==> values1 == values2 ==> buf1 == buf2,
329        decreases buf1.len(),
330    {
331        broadcast use vstd::seq_lib::group_seq_properties;
332
333        if let Some(values1) = self.parse_ordered(buf1, previous1) {
334            if let Some(values2) = self.parse_ordered(buf2, previous2) {
335                if values1 == values2 && values1.len() > 0 {
336                    let (n1, value1) = self.0.spec_parse(buf1)->0;
337                    let (n2, value2) = self.0.spec_parse(buf2)->0;
338                    let rest1 = self.parse_ordered(buf1.skip(n1), previous1.push(buf1.take(n1)))->0;
339                    let rest2 = self.parse_ordered(buf2.skip(n2), previous2.push(buf2.take(n2)))->0;
340
341                    assert(value1 == value2) by {
342                        assert(value1 == values1[0]);
343                        assert(value2 == values2[0]);
344                    }
345                    assert(rest1 == rest2) by {
346                        assert(rest1 == values1.skip(1));
347                        assert(rest2 == values2.skip(1));
348                    }
349
350                    self.0.lemma_parse_non_malleable(buf1, buf2);
351                    self.lemma_parse_ordered_non_malleable(
352                        buf1.skip(n1),
353                        previous1.push(buf1.take(n1)),
354                        buf2.skip(n2),
355                        previous2.push(buf2.take(n2)),
356                    );
357                    assert(buf1 == buf1.take(n1) + buf1.skip(n1));
358                    assert(buf2 == buf2.take(n2) + buf2.skip(n2));
359                }
360            }
361        }
362    }
363}
364
365impl<C> SetOfFmt<C> where
366    C: SPRoundTripDps + NonTailFmt + EquivSerializersGeneral + Productive,
367    C: SpecSerializer<SVal = C::T>,
368 {
369    proof fn lemma_serialize_parse_ordered(&self, values: Seq<C::T>, previous: Seq<Seq<u8>>)
370        requires
371            self.0.unambiguous(),
372            self.0.serialize_dps_inv(),
373            self.0.equiv_general_inv(),
374            self.0.safe_inv(),
375            self.0.productive_inv(),
376            Star(self.0).consistent(values),
377            der_encodings_sorted(previous + values.map_values(|v: C::T| self.0.spec_serialize(v))),
378        ensures
379            self.parse_ordered(Star(self.0).spec_serialize_dps(values, Seq::empty()), previous)
380                == Some(values),
381        decreases values.len(),
382    {
383        reveal(<Star<_> as Consistency>::consistent);
384        reveal(<Star<_> as SpecSerializerDps>::spec_serialize_dps);
385        broadcast use vstd::seq::group_seq_axioms;
386
387        let encodings = values.map_values(|v: C::T| self.0.spec_serialize(v));
388        lemma_der_encodings_sorted_take(previous + encodings, previous.len() as int);
389        assert((previous + encodings).take(previous.len() as int) == previous);
390        assert(der_encodings_sorted(previous));
391        if values.len() > 0 {
392            let value = values[0];
393            let rest = values.skip(1);
394            let rest_buf = Star(self.0).spec_serialize_dps(rest, Seq::empty());
395            let serialized = Star(self.0).spec_serialize_dps(values, Seq::empty());
396            let n = self.0.byte_len(value) as int;
397
398            assert(values == seq![value] + rest);
399            assert(encodings == seq![self.0.spec_serialize(value)] + rest.map_values(
400                |v: C::T| self.0.spec_serialize(v),
401            ));
402            assert(serialized == self.0.spec_serialize_dps(value, rest_buf));
403            self.0.theorem_serialize_dps_parse_roundtrip(value, rest_buf);
404            self.0.lemma_serialize_dps_prepend(value, rest_buf);
405            self.0.lemma_serialize_dps_len(value, rest_buf);
406            self.0.lemma_serialize_equiv(value, rest_buf);
407            self.0.lemma_productive(serialized);
408            assert(serialized.take(n) == self.0.spec_serialize(value));
409            assert(serialized.skip(n) == rest_buf);
410
411            lemma_der_encodings_sorted_take(previous + encodings, previous.len() as int + 1);
412            assert((previous + encodings).take(previous.len() as int + 1) == previous.push(
413                self.0.spec_serialize(value),
414            ));
415            assert(previous.push(self.0.spec_serialize(value)) + rest.map_values(
416                |v: C::T| self.0.spec_serialize(v),
417            ) == previous + encodings);
418
419            self.lemma_serialize_parse_ordered(rest, previous.push(self.0.spec_serialize(value)));
420        }
421    }
422}
423
424mod derived_specs {
425    use super::*;
426
427    impl<C: SpecParser> SpecParser for SetOfFmt<C> {
428        type PVal = Seq<C::PVal>;
429
430        open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
431            match self.parse_ordered(ibuf, Seq::empty()) {
432                Some(values) => Some((ibuf.len() as int, values)),
433                _ => None,
434            }
435        }
436    }
437
438    impl<C> Consistency for SetOfFmt<C> where C: Consistency + SpecSerializer<SVal = C::Val> {
439        type Val = Seq<C::Val>;
440
441        open spec fn consistent(&self, values: Self::Val) -> bool {
442            &&& Star(self.0).consistent(values)
443            &&& set_of_values_sorted(self.0, values)
444        }
445    }
446
447    impl<C: SpecSerializerDps> SpecSerializerDps for SetOfFmt<C> {
448        type SValue = Seq<C::SValue>;
449
450        open spec fn spec_serialize_dps(&self, v: Self::SValue, _obuf: Seq<u8>) -> Seq<u8> {
451            Star(self.0).spec_serialize_dps(v, Seq::empty())
452        }
453    }
454
455    impl<C: SpecSerializer> SpecSerializer for SetOfFmt<C> {
456        type SVal = Seq<C::SVal>;
457
458        open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
459            Star(self.0).spec_serialize(v)
460        }
461    }
462
463    impl<C: SpecByteLen> SpecByteLen for SetOfFmt<C> {
464        type T = Seq<C::T>;
465
466        open spec fn byte_len(&self, v: Self::T) -> nat {
467            Star(self.0).byte_len(v)
468        }
469    }
470
471}
472
473mod derived_proofs {
474    use super::*;
475
476    impl<C: SafeParser> SafeParser for SetOfFmt<C> {
477        open spec fn safe_inv(&self) -> bool {
478            self.0.safe_inv()
479        }
480
481        proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
482            reveal(<SetOfFmt<_> as SpecParser>::spec_parse);
483        }
484    }
485
486    impl<C: SoundParser + PSRoundTrip> SoundParser for SetOfFmt<C> {
487        open spec fn sound_inv(&self) -> bool {
488            self.0.sound_inv() && self.0.ps_roundtrip_inv()
489        }
490
491        proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
492            reveal(<SetOfFmt<_> as SpecParser>::spec_parse);
493            reveal(<SetOfFmt<_> as SpecByteLen>::byte_len);
494            self.lemma_parse_ordered_byte_len(ibuf, Seq::empty());
495        }
496
497        proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
498            reveal(<SetOfFmt<_> as SpecParser>::spec_parse);
499            reveal(<SetOfFmt<_> as Consistency>::consistent);
500            self.lemma_parse_ordered_consistent(ibuf, Seq::empty());
501        }
502    }
503
504    impl<C: NonMalleable> NonMalleable for SetOfFmt<C> {
505        open spec fn nonmal_inv(&self) -> bool {
506            self.0.nonmal_inv() && self.0.safe_inv()
507        }
508
509        proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
510            reveal(<SetOfFmt<_> as SpecParser>::spec_parse);
511            self.lemma_parse_ordered_non_malleable(buf1, Seq::empty(), buf2, Seq::empty());
512        }
513    }
514
515    impl<C: SafeParser> Productive for SetOfFmt<C> {
516        open spec fn productive_inv(&self) -> bool {
517            false
518        }
519
520        proof fn lemma_productive(&self, _ibuf: Seq<u8>) {
521        }
522    }
523
524    impl<C: GoodSerializer> GoodSerializer for SetOfFmt<C> {
525        open spec fn serialize_inv(&self) -> bool {
526            self.0.serialize_inv()
527        }
528
529        proof fn lemma_serialize_len(&self, values: Self::SVal) {
530            reveal(<SetOfFmt<_> as SpecSerializer>::spec_serialize);
531            reveal(<SetOfFmt<_> as SpecByteLen>::byte_len);
532            reveal(<Star<_> as SpecSerializer>::spec_serialize);
533            reveal(<Star<_> as SpecByteLen>::byte_len);
534            Star(self.0).lemma_serialize_len(values);
535        }
536    }
537
538    impl<C: EquivSerializersGeneral> EquivSerializers for SetOfFmt<C> {
539        open spec fn equiv_inv(&self) -> bool {
540            self.0.equiv_general_inv()
541        }
542
543        proof fn lemma_serialize_equiv_on_empty(&self, values: Self::SVal) {
544            reveal(<SetOfFmt<_> as SpecSerializerDps>::spec_serialize_dps);
545            reveal(<SetOfFmt<_> as SpecSerializer>::spec_serialize);
546            reveal(<Star<_> as SpecSerializer>::spec_serialize);
547            Star(self.0).lemma_serialize_equiv_on_empty(values);
548        }
549    }
550
551    impl<C> SPRoundTripDps for SetOfFmt<C> where
552        C: SPRoundTripDps + NonTailFmt + EquivSerializersGeneral + Productive,
553        C: SpecSerializer<SVal = C::T>,
554     {
555        open spec fn unambiguous(&self) -> bool {
556            &&& self.0.unambiguous()
557            &&& self.0.serialize_dps_inv()
558            &&& self.0.equiv_general_inv()
559            &&& self.0.safe_inv()
560            &&& self.0.productive_inv()
561        }
562
563        proof fn theorem_serialize_dps_parse_roundtrip(&self, values: Self::T, _obuf: Seq<u8>) {
564            reveal(<SetOfFmt<_> as Consistency>::consistent);
565            reveal(<SetOfFmt<_> as SpecSerializerDps>::spec_serialize_dps);
566            reveal(<SetOfFmt<_> as SpecParser>::spec_parse);
567            reveal(<SetOfFmt<_> as SpecByteLen>::byte_len);
568
569            let star = Star(self.0);
570            self.lemma_serialize_parse_ordered(values, Seq::empty());
571            star.lemma_serialize_dps_len(values, Seq::empty());
572            assert(star.spec_serialize_dps(values, Seq::empty()).len() == star.byte_len(values));
573        }
574    }
575
576}
577
578/// Executable octet comparison for X.690 §11.6 ordering.
579pub fn der_leq(a: &[u8], b: &[u8]) -> (leq: bool)
580    ensures
581        leq == der_octets_leq(a.deep_view(), b.deep_view()),
582{
583    let mut left = 0usize;
584    let mut right = 0usize;
585    assert(a.deep_view().skip(0) == a.deep_view());
586    assert(b.deep_view().skip(0) == b.deep_view());
587    while left < a.len() || right < b.len()
588        invariant
589            left <= a.len(),
590            right <= b.len(),
591            der_octets_leq(a.deep_view(), b.deep_view()) == der_octets_leq(
592                a.deep_view().skip(left as int),
593                b.deep_view().skip(right as int),
594            ),
595        decreases a.len() - left + b.len() - right,
596    {
597        let ghost old_left = a.deep_view().skip(left as int);
598        let ghost old_right = b.deep_view().skip(right as int);
599        proof {
600            lemma_der_octets_leq_step(old_left, old_right);
601        }
602        let ai = if left < a.len() {
603            a[left]
604        } else {
605            0u8
606        };
607        let bi = if right < b.len() {
608            b[right]
609        } else {
610            0u8
611        };
612        if ai < bi {
613            return true;
614        }
615        if ai > bi {
616            return false;
617        }
618        if left < a.len() {
619            left += 1;
620        }
621        if right < b.len() {
622            right += 1;
623        }
624        assert(der_octets_drop_head(old_left) == a.deep_view().skip(left as int));
625        assert(der_octets_drop_head(old_right) == b.deep_view().skip(right as int));
626    }
627    true
628}
629
630#[cfg(feature = "alloc")]
631impl<'i, C> Parser<&'i [u8]> for SetOfFmt<C> where
632    C: Parser<&'i [u8]> + SafeParser + Productive + Copy,
633 {
634    type PT = Vec<C::PT>;
635
636    open spec fn exec_inv(&self) -> bool {
637        &&& self.0.exec_inv()
638        &&& self.0.safe_inv()
639        &&& self.0.productive_inv()
640    }
641
642    fn parse(&self, ibuf: &&'i [u8]) -> (r: PResult<Self::PT>) {
643        reveal(<SetOfFmt<_> as SpecParser>::spec_parse);
644        broadcast use vstd::seq::group_seq_axioms;
645
646        let _len = ibuf.len();
647        let mut consumed = 0usize;
648        let mut rest = *ibuf;
649        let mut values = Vec::new();
650        let mut encodings = Vec::new();
651
652        assert(values.deep_view() == Seq::empty());
653        assert(encodings.deep_view() == Seq::empty());
654
655        while rest.len() > 0
656            invariant
657                self.exec_inv(),
658                consumed + rest@.len() == _len,
659                values.len() == encodings.len(),
660                der_encodings_sorted(encodings.deep_view()),
661                self.parse_ordered(rest@, encodings.deep_view()) matches Some(suffix)
662                    ==> self.spec_parse(ibuf@) == Some((_len as int, values.deep_view() + suffix)),
663                self.parse_ordered(rest@, encodings.deep_view()) is None ==> self.spec_parse(
664                    ibuf@,
665                ) is None,
666            decreases rest.len(),
667        {
668            broadcast use crate::core::spec::SafeParser::lemma_parse_safe;
669
670            let (n, value): (usize, C::PT) = self.0.parse(&rest)?;
671            proof {
672                self.0.lemma_productive(rest@);
673            }
674            let encoding = &rest[0..n];
675
676            proof {
677                assert(encoding.deep_view() == rest@.take(n as int));
678                lemma_der_encodings_sorted_push(encodings.deep_view(), encoding.deep_view());
679            }
680            if encodings.len() > 0 {
681                let previous = encodings[encodings.len() - 1];
682                if !der_leq(previous, encoding) {
683                    return Err(ParseError::non_canonical());
684                }
685            }
686            let ghost old_rest = rest@;
687            let ghost old_encodings = encodings.deep_view();
688            values.push(value);
689            encodings.push(encoding);
690            rest = &rest[n..rest.len()];
691            consumed += n;
692
693            assert(encodings.deep_view() == old_encodings.push(old_rest.take(n as int)));
694        }
695
696        Ok((consumed, values))
697    }
698}
699
700impl<Output: OutputBuf, C, Elem> Serializer<Output, [Elem]> for SetOfFmt<C> where
701    Elem: DeepView,
702    C: SpecCombinator<T = <Elem as DeepView>::V> + Serializer<Output, Elem> + Copy,
703 {
704    #[verifier::prophetic]
705    open spec fn exec_inv(&self) -> bool {
706        self.0.exec_inv()
707    }
708
709    fn serialize_into(&self, v: &[Elem], obuf: &mut Output) {
710        Star(self.0).serialize_into(v, obuf)
711    }
712}
713
714impl<C, Elem> ByteLen<[Elem]> for SetOfFmt<C> where
715    C: SpecByteLen<T = <Elem as DeepView>::V> + ByteLen<Elem> + Copy,
716    Elem: DeepView,
717 {
718    open spec fn exec_inv(&self) -> bool {
719        self.0.exec_inv()
720    }
721
722    fn length(&self, v: &[Elem]) -> (len: usize) {
723        Star(self.0).length(v)
724    }
725}
726
727impl<C, Elem> Prepare<[Elem]> for SetOfFmt<C> where
728    Elem: DeepView,
729    C: SpecCombinator<T = <Elem as DeepView>::V> + Prepare<Elem> + DerOrd<Elem> + Copy,
730 {
731    open spec fn exec_inv(&self) -> bool {
732        self.0.exec_inv()
733    }
734
735    fn prepare(&self, values: &[Elem]) -> (checked: Result<usize, PreSerializeError>) {
736        reveal(<Star<_> as Consistency>::consistent);
737        let total = Star(self.0).prepare(values)?;
738
739        for i in 0..values.len()
740            invariant
741                <Self as Prepare<[Elem]>>::exec_inv(self),
742                forall|k: int|
743                    0 <= k < values.deep_view().len() ==> self.0.consistent(
744                        #[trigger] values.deep_view()[k],
745                    ),
746                total == Star(self.0).byte_len(values.deep_view()),
747                set_of_values_sorted(self.0, values.deep_view().take(i as int)),
748        {
749            if i > 0 {
750                assert(self.0.consistent(values.deep_view()[i as int - 1]));
751                assert(self.0.consistent(values.deep_view()[i as int]));
752                if !self.0.der_leq(&values[i - 1], &values[i]) {
753                    return Err(
754                        PreSerializeError::custom("SET OF elements are not in canonical DER order"),
755                    );
756                }
757            }
758            proof {
759                let vs = values.deep_view();
760                let serialize = |v: C::T| self.0.spec_serialize(v);
761                let prefix_encodings = vs.take(i as int).map_values(serialize);
762                let current_encoding = serialize(vs[i as int]);
763                lemma_der_encodings_sorted_push(prefix_encodings, current_encoding);
764                vs.lemma_map_take_succ(serialize, i as int);
765            }
766        }
767        assert(values.deep_view().take(values.deep_view().len() as int) == values.deep_view());
768
769        Ok(total)
770    }
771}
772
773#[cfg(feature = "alloc")]
774impl<Output: OutputBuf, C, Elem> Serializer<Output, Vec<Elem>> for SetOfFmt<C> where
775    Elem: DeepView,
776    C: SpecCombinator<T = <Elem as DeepView>::V> + Serializer<Output, Elem> + Copy,
777 {
778    #[verifier::prophetic]
779    open spec fn exec_inv(&self) -> bool {
780        self.0.exec_inv()
781    }
782
783    fn serialize_into(&self, values: &Vec<Elem>, obuf: &mut Output) {
784        <Self as Serializer<Output, [Elem]>>::serialize_into(self, values.as_slice(), obuf)
785    }
786}
787
788#[cfg(feature = "alloc")]
789impl<C, Elem> ByteLen<Vec<Elem>> for SetOfFmt<C> where
790    C: SpecByteLen<T = <Elem as DeepView>::V> + ByteLen<Elem> + Copy,
791    Elem: DeepView,
792 {
793    open spec fn exec_inv(&self) -> bool {
794        self.0.exec_inv()
795    }
796
797    fn length(&self, values: &Vec<Elem>) -> (len: usize) {
798        <Self as ByteLen<[Elem]>>::length(self, values.as_slice())
799    }
800}
801
802#[cfg(feature = "alloc")]
803impl<C, Elem> Prepare<Vec<Elem>> for SetOfFmt<C> where
804    Elem: DeepView,
805    C: SpecCombinator<T = <Elem as DeepView>::V> + Prepare<Elem> + DerOrd<Elem> + Copy,
806 {
807    open spec fn exec_inv(&self) -> bool {
808        self.0.exec_inv()
809    }
810
811    fn prepare(&self, values: &Vec<Elem>) -> (checked: Result<usize, PreSerializeError>) {
812        <Self as Prepare<[Elem]>>::prepare(self, values.as_slice())
813    }
814}
815
816} // verus!
817#[cfg(all(test, feature = "alloc"))]
818mod tests {
819    use crate::asn1::der::{INTEGER8, SET_OF};
820    use crate::core::exec::{Parser, Prepare, SerializerExt};
821
822    #[test]
823    fn der_set_of_integer8_roundtrip_and_ordering() {
824        let format = SET_OF(INTEGER8);
825        let canonical = [0x31, 0x06, 0x02, 0x01, 0x01, 0x02, 0x01, 0x02];
826        let (consumed, values) = format.parse(&&canonical[..]).unwrap();
827        assert_eq!(consumed, canonical.len());
828        assert_eq!(values, vec![1, 2]);
829
830        assert_eq!(format.prepare(&values), Ok(canonical.len()));
831        let mut encoded = vec![0; format.prepare(&values).unwrap()];
832        format.serialize(&values, &mut encoded);
833        assert_eq!(encoded, canonical);
834
835        let unordered = [0x31, 0x06, 0x02, 0x01, 0x02, 0x02, 0x01, 0x01];
836        assert!(format.parse(&&unordered[..]).is_err());
837        assert!(format.prepare(&vec![2, 1]).is_err());
838    }
839
840    #[test]
841    fn der_set_of_allows_duplicate_encodings() {
842        let format = SET_OF(INTEGER8);
843        let duplicate = [0x31, 0x06, 0x02, 0x01, 0x01, 0x02, 0x01, 0x01];
844        let (_, values) = format.parse(&&duplicate[..]).unwrap();
845        assert_eq!(values, vec![1, 1]);
846        assert_eq!(format.prepare(&values), Ok(duplicate.len()));
847    }
848}
vest_lib/asn1/set_of.rs

vest_lib/asn1/
set_of.rs
