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[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[0..n]),
153{
154    assert forall|i: int, j: int|
155        0 <= i < j < encodings[0..n].len() implies #[trigger] der_octets_leq(
156        encodings[0..n][i],
157        encodings[0..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[0..n]),
219                ) => {
220                    match self.parse_ordered(ibuf[n..], previous.push(ibuf[0..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[0..n]),
248                ) => {
249                    self.0.lemma_parse_sound_consumption(ibuf);
250                    self.lemma_parse_ordered_byte_len(ibuf[n..], previous.push(ibuf[0..n]));
251
252                    if let Some(rest_values) = self.parse_ordered(
253                        ibuf[n..],
254                        previous.push(ibuf[0..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[0..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[n..], previous.push(ibuf[0..n]));
291
292                    if let Some(rest_values) = self.parse_ordered(
293                        ibuf[n..],
294                        previous.push(ibuf[0..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[0..n]]
299                            + rest_values.map_values(serialize));
300                        assert(previous + values.map_values(serialize) == previous.push(ibuf[0..n])
301                            + rest_values.map_values(serialize));
302                    }
303                },
304                _ => {},
305            }
306        }
307    }
308}
309
310impl<C: NonMalleable> SetOfFmt<C> {
311    proof fn lemma_parse_ordered_non_malleable(
312        &self,
313        buf1: Seq<u8>,
314        previous1: Seq<Seq<u8>>,
315        buf2: Seq<u8>,
316        previous2: Seq<Seq<u8>>,
317    )
318        requires
319            self.0.nonmal_inv(),
320            self.0.safe_inv(),
321            der_encodings_sorted(previous1),
322            der_encodings_sorted(previous2),
323        ensures
324            self.parse_ordered(buf1, previous1) matches Some(values1) ==> self.parse_ordered(
325                buf2,
326                previous2,
327            ) matches Some(values2) ==> values1 == values2 ==> buf1 == buf2,
328        decreases buf1.len(),
329    {
330        broadcast use vstd::seq_lib::group_seq_properties;
331
332        if let Some(values1) = self.parse_ordered(buf1, previous1) {
333            if let Some(values2) = self.parse_ordered(buf2, previous2) {
334                if values1 == values2 && values1.len() > 0 {
335                    let (n1, value1) = self.0.spec_parse(buf1)->0;
336                    let (n2, value2) = self.0.spec_parse(buf2)->0;
337                    let rest1 = self.parse_ordered(buf1[n1..], previous1.push(buf1[0..n1]))->0;
338                    let rest2 = self.parse_ordered(buf2[n2..], previous2.push(buf2[0..n2]))->0;
339
340                    assert(value1 == value2) by {
341                        assert(value1 == values1[0]);
342                        assert(value2 == values2[0]);
343                    }
344                    assert(rest1 == rest2) by {
345                        assert(rest1 == values1[1..]);
346                        assert(rest2 == values2[1..]);
347                    }
348
349                    self.0.lemma_parse_non_malleable(buf1, buf2);
350                    self.lemma_parse_ordered_non_malleable(
351                        buf1[n1..],
352                        previous1.push(buf1[0..n1]),
353                        buf2[n2..],
354                        previous2.push(buf2[0..n2]),
355                    );
356                    assert(buf1 == buf1[0..n1] + buf1[n1..]);
357                    assert(buf2 == buf2[0..n2] + buf2[n2..]);
358                }
359            }
360        }
361    }
362}
363
364impl<C> SetOfFmt<C> where
365    C: SPRoundTripDps + NonTailFmt + EquivSerializersGeneral + Productive,
366    C: SpecSerializer<SVal = C::T>,
367 {
368    proof fn lemma_serialize_parse_ordered(&self, values: Seq<C::T>, previous: Seq<Seq<u8>>)
369        requires
370            self.0.unambiguous(),
371            self.0.serialize_dps_inv(),
372            self.0.equiv_general_inv(),
373            self.0.safe_inv(),
374            self.0.productive_inv(),
375            Star(self.0).consistent(values),
376            der_encodings_sorted(previous + values.map_values(|v: C::T| self.0.spec_serialize(v))),
377        ensures
378            self.parse_ordered(Star(self.0).spec_serialize_dps(values, Seq::empty()), previous)
379                == Some(values),
380        decreases values.len(),
381    {
382        reveal(<Star<_> as Consistency>::consistent);
383        reveal(<Star<_> as SpecSerializerDps>::spec_serialize_dps);
384        broadcast use vstd::seq::group_seq_axioms;
385
386        let encodings = values.map_values(|v: C::T| self.0.spec_serialize(v));
387        lemma_der_encodings_sorted_take(previous + encodings, previous.len() as int);
388        assert((previous + encodings)[0..previous.len()] == previous);
389        assert(der_encodings_sorted(previous));
390        if values.len() > 0 {
391            let value = values[0];
392            let rest = values[1..];
393            let rest_buf = Star(self.0).spec_serialize_dps(rest, Seq::empty());
394            let serialized = Star(self.0).spec_serialize_dps(values, Seq::empty());
395            let n = self.0.byte_len(value) as int;
396
397            assert(values == seq![value] + rest);
398            assert(encodings == seq![self.0.spec_serialize(value)] + rest.map_values(
399                |v: C::T| self.0.spec_serialize(v),
400            ));
401            assert(serialized == self.0.spec_serialize_dps(value, rest_buf));
402            self.0.theorem_serialize_dps_parse_roundtrip(value, rest_buf);
403            self.0.lemma_serialize_dps_prepend(value, rest_buf);
404            self.0.lemma_serialize_dps_len(value, rest_buf);
405            self.0.lemma_serialize_equiv(value, rest_buf);
406            self.0.lemma_productive(serialized);
407            assert(serialized[0..n] == self.0.spec_serialize(value));
408            assert(serialized[n..] == rest_buf);
409
410            lemma_der_encodings_sorted_take(previous + encodings, previous.len() as int + 1);
411            assert((previous + encodings)[0..previous.len() + 1] == previous.push(
412                self.0.spec_serialize(value),
413            ));
414            assert(previous.push(self.0.spec_serialize(value)) + rest.map_values(
415                |v: C::T| self.0.spec_serialize(v),
416            ) == previous + encodings);
417
418            self.lemma_serialize_parse_ordered(rest, previous.push(self.0.spec_serialize(value)));
419        }
420    }
421}
422
423mod derived_specs {
424    use super::*;
425
426    impl<C: SpecParser> SpecParser for SetOfFmt<C> {
427        type PVal = Seq<C::PVal>;
428
429        open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
430            match self.parse_ordered(ibuf, Seq::empty()) {
431                Some(values) => Some((ibuf.len() as int, values)),
432                _ => None,
433            }
434        }
435    }
436
437    impl<C> Consistency for SetOfFmt<C> where C: Consistency + SpecSerializer<SVal = C::Val> {
438        type Val = Seq<C::Val>;
439
440        open spec fn consistent(&self, values: Self::Val) -> bool {
441            &&& Star(self.0).consistent(values)
442            &&& set_of_values_sorted(self.0, values)
443        }
444    }
445
446    impl<C: SpecSerializerDps> SpecSerializerDps for SetOfFmt<C> {
447        type SValue = Seq<C::SValue>;
448
449        open spec fn spec_serialize_dps(&self, v: Self::SValue, _obuf: Seq<u8>) -> Seq<u8> {
450            Star(self.0).spec_serialize_dps(v, Seq::empty())
451        }
452    }
453
454    impl<C: SpecSerializer> SpecSerializer for SetOfFmt<C> {
455        type SVal = Seq<C::SVal>;
456
457        open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
458            Star(self.0).spec_serialize(v)
459        }
460    }
461
462    impl<C: SpecByteLen> SpecByteLen for SetOfFmt<C> {
463        type T = Seq<C::T>;
464
465        open spec fn byte_len(&self, v: Self::T) -> nat {
466            Star(self.0).byte_len(v)
467        }
468    }
469
470}
471
472mod derived_proofs {
473    use super::*;
474
475    impl<C: SafeParser> SafeParser for SetOfFmt<C> {
476        open spec fn safe_inv(&self) -> bool {
477            self.0.safe_inv()
478        }
479
480        proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
481            reveal(<SetOfFmt<_> as SpecParser>::spec_parse);
482        }
483    }
484
485    impl<C: SoundParser + PSRoundTrip> SoundParser for SetOfFmt<C> {
486        open spec fn sound_inv(&self) -> bool {
487            self.0.sound_inv() && self.0.ps_roundtrip_inv()
488        }
489
490        proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
491            reveal(<SetOfFmt<_> as SpecParser>::spec_parse);
492            reveal(<SetOfFmt<_> as SpecByteLen>::byte_len);
493            self.lemma_parse_ordered_byte_len(ibuf, Seq::empty());
494        }
495
496        proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
497            reveal(<SetOfFmt<_> as SpecParser>::spec_parse);
498            reveal(<SetOfFmt<_> as Consistency>::consistent);
499            self.lemma_parse_ordered_consistent(ibuf, Seq::empty());
500        }
501    }
502
503    impl<C: NonMalleable> NonMalleable for SetOfFmt<C> {
504        open spec fn nonmal_inv(&self) -> bool {
505            self.0.nonmal_inv() && self.0.safe_inv()
506        }
507
508        proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
509            reveal(<SetOfFmt<_> as SpecParser>::spec_parse);
510            self.lemma_parse_ordered_non_malleable(buf1, Seq::empty(), buf2, Seq::empty());
511        }
512    }
513
514    impl<C: SafeParser> Productive for SetOfFmt<C> {
515        open spec fn productive_inv(&self) -> bool {
516            false
517        }
518
519        proof fn lemma_productive(&self, _ibuf: Seq<u8>) {
520        }
521    }
522
523    impl<C: GoodSerializer> GoodSerializer for SetOfFmt<C> {
524        open spec fn serialize_inv(&self) -> bool {
525            self.0.serialize_inv()
526        }
527
528        proof fn lemma_serialize_len(&self, values: Self::SVal) {
529            reveal(<SetOfFmt<_> as SpecSerializer>::spec_serialize);
530            reveal(<SetOfFmt<_> as SpecByteLen>::byte_len);
531            reveal(<Star<_> as SpecSerializer>::spec_serialize);
532            reveal(<Star<_> as SpecByteLen>::byte_len);
533            Star(self.0).lemma_serialize_len(values);
534        }
535    }
536
537    impl<C: EquivSerializersGeneral> EquivSerializers for SetOfFmt<C> {
538        open spec fn equiv_inv(&self) -> bool {
539            self.0.equiv_general_inv()
540        }
541
542        proof fn lemma_serialize_equiv_on_empty(&self, values: Self::SVal) {
543            reveal(<SetOfFmt<_> as SpecSerializerDps>::spec_serialize_dps);
544            reveal(<SetOfFmt<_> as SpecSerializer>::spec_serialize);
545            reveal(<Star<_> as SpecSerializer>::spec_serialize);
546            Star(self.0).lemma_serialize_equiv_on_empty(values);
547        }
548    }
549
550    impl<C> SPRoundTripDps for SetOfFmt<C> where
551        C: SPRoundTripDps + NonTailFmt + EquivSerializersGeneral + Productive,
552        C: SpecSerializer<SVal = C::T>,
553     {
554        open spec fn unambiguous(&self) -> bool {
555            &&& self.0.unambiguous()
556            &&& self.0.serialize_dps_inv()
557            &&& self.0.equiv_general_inv()
558            &&& self.0.safe_inv()
559            &&& self.0.productive_inv()
560        }
561
562        proof fn theorem_serialize_dps_parse_roundtrip(&self, values: Self::T, _obuf: Seq<u8>) {
563            reveal(<SetOfFmt<_> as Consistency>::consistent);
564            reveal(<SetOfFmt<_> as SpecSerializerDps>::spec_serialize_dps);
565            reveal(<SetOfFmt<_> as SpecParser>::spec_parse);
566            reveal(<SetOfFmt<_> as SpecByteLen>::byte_len);
567
568            let star = Star(self.0);
569            self.lemma_serialize_parse_ordered(values, Seq::empty());
570            star.lemma_serialize_dps_len(values, Seq::empty());
571            assert(star.spec_serialize_dps(values, Seq::empty()).len() == star.byte_len(values));
572        }
573    }
574
575}
576
577/// Executable octet comparison for X.690 §11.6 ordering.
578pub fn der_leq(a: &[u8], b: &[u8]) -> (leq: bool)
579    ensures
580        leq == der_octets_leq(a.deep_view(), b.deep_view()),
581{
582    let mut left = 0usize;
583    let mut right = 0usize;
584    assert(a.deep_view()[0..] == a.deep_view());
585    assert(b.deep_view()[0..] == b.deep_view());
586    while left < a.len() || right < b.len()
587        invariant
588            left <= a.len(),
589            right <= b.len(),
590            der_octets_leq(a.deep_view(), b.deep_view()) == der_octets_leq(
591                a.deep_view()[left..],
592                b.deep_view()[right..],
593            ),
594        decreases a.len() - left + b.len() - right,
595    {
596        let ghost old_left = a.deep_view()[left..];
597        let ghost old_right = b.deep_view()[right..];
598        proof {
599            lemma_der_octets_leq_step(old_left, old_right);
600        }
601        let ai = if left < a.len() {
602            a[left]
603        } else {
604            0u8
605        };
606        let bi = if right < b.len() {
607            b[right]
608        } else {
609            0u8
610        };
611        if ai < bi {
612            return true;
613        }
614        if ai > bi {
615            return false;
616        }
617        if left < a.len() {
618            left += 1;
619        }
620        if right < b.len() {
621            right += 1;
622        }
623        assert(der_octets_drop_head(old_left) == a.deep_view()[left..]);
624        assert(der_octets_drop_head(old_right) == b.deep_view()[right..]);
625    }
626    true
627}
628
629#[cfg(feature = "alloc")]
630impl<'i, C> Parser<&'i [u8]> for SetOfFmt<C> where
631    C: Parser<&'i [u8]> + SafeParser + Productive + Copy,
632 {
633    type PT = Vec<C::PT>;
634
635    open spec fn exec_inv(&self) -> bool {
636        &&& self.0.exec_inv()
637        &&& self.0.safe_inv()
638        &&& self.0.productive_inv()
639    }
640
641    fn parse(&self, ibuf: &&'i [u8]) -> (r: PResult<Self::PT>) {
642        reveal(<SetOfFmt<_> as SpecParser>::spec_parse);
643        broadcast use vstd::seq::group_seq_axioms;
644
645        let _len = ibuf.len();
646        let mut consumed = 0usize;
647        let mut rest = *ibuf;
648        let mut values = Vec::new();
649        let mut encodings = Vec::new();
650
651        assert(values.deep_view() == Seq::empty());
652        assert(encodings.deep_view() == Seq::empty());
653
654        while rest.len() > 0
655            invariant
656                self.exec_inv(),
657                consumed + rest@.len() == _len,
658                values.len() == encodings.len(),
659                der_encodings_sorted(encodings.deep_view()),
660                self.parse_ordered(rest@, encodings.deep_view()) matches Some(suffix)
661                    ==> self.spec_parse(ibuf@) == Some((_len as int, values.deep_view() + suffix)),
662                self.parse_ordered(rest@, encodings.deep_view()) is None ==> self.spec_parse(
663                    ibuf@,
664                ) is None,
665            decreases rest.len(),
666        {
667            broadcast use crate::core::spec::SafeParser::lemma_parse_safe;
668
669            let (n, value): (usize, C::PT) = self.0.parse(&rest)?;
670            proof {
671                self.0.lemma_productive(rest@);
672            }
673            let encoding = &rest[0..n];
674
675            proof {
676                assert(encoding.deep_view() == rest@[0..n]);
677                lemma_der_encodings_sorted_push(encodings.deep_view(), encoding.deep_view());
678            }
679            if encodings.len() > 0 {
680                let previous = encodings[encodings.len() - 1];
681                if !der_leq(previous, encoding) {
682                    return Err(ParseError::non_canonical());
683                }
684            }
685            let ghost old_rest = rest@;
686            let ghost old_encodings = encodings.deep_view();
687            values.push(value);
688            encodings.push(encoding);
689            rest = &rest[n..rest.len()];
690            consumed += n;
691
692            assert(encodings.deep_view() == old_encodings.push(old_rest[0..n]));
693        }
694
695        Ok((consumed, values))
696    }
697}
698
699impl<Output: OutputBuf, C, Elem> Serializer<Output, [Elem]> for SetOfFmt<C> where
700    Elem: DeepView,
701    C: SpecCombinator<T = <Elem as DeepView>::V> + Serializer<Output, Elem> + Copy,
702 {
703    #[verifier::prophetic]
704    open spec fn exec_inv(&self) -> bool {
705        self.0.exec_inv()
706    }
707
708    fn serialize_into(&self, v: &[Elem], obuf: &mut Output) {
709        Star(self.0).serialize_into(v, obuf)
710    }
711}
712
713impl<C, Elem> ByteLen<[Elem]> for SetOfFmt<C> where
714    C: SpecByteLen<T = <Elem as DeepView>::V> + ByteLen<Elem> + Copy,
715    Elem: DeepView,
716 {
717    open spec fn exec_inv(&self) -> bool {
718        self.0.exec_inv()
719    }
720
721    fn length(&self, v: &[Elem]) -> (len: usize) {
722        Star(self.0).length(v)
723    }
724}
725
726impl<C, Elem> Prepare<[Elem]> for SetOfFmt<C> where
727    Elem: DeepView,
728    C: SpecCombinator<T = <Elem as DeepView>::V> + Prepare<Elem> + DerOrd<Elem> + Copy,
729 {
730    open spec fn exec_inv(&self) -> bool {
731        self.0.exec_inv()
732    }
733
734    #[verifier::loop_isolation(false)]
735    fn prepare(&self, values: &[Elem]) -> (checked: Result<usize, PreSerializeError>) {
736        broadcast use vstd::std_specs::iter::zip_postcondition;
737        broadcast use vstd::std_specs::iter::skip_postcondition;
738
739        reveal(<Star<_> as Consistency>::consistent);
740        let total = Star(self.0).prepare(values)?;
741        let pairs = values.iter().zip(values.iter().skip(1));
742        let count = pairs.len();
743        if count == 0 {
744            return Ok(total);
745        }
746        for (left, right) in iter: pairs
747            invariant
748                iter.seq().len() == count,
749                count + 1 == values.len(),
750                <Self as Prepare<[Elem]>>::exec_inv(self),
751                forall|k: int|
752                    0 <= k < values.deep_view().len() ==> self.0.consistent(
753                        #[trigger] values.deep_view()[k],
754                    ),
755                total == Star(self.0).byte_len(values.deep_view()),
756                set_of_values_sorted(self.0, values.deep_view()[0..iter.index() + 1]),
757        {
758            assert(left.deep_view() == values.deep_view()[iter.index()]);
759            assert(right.deep_view() == values.deep_view()[iter.index() + 1]);
760            if !self.0.der_leq(left, right) {
761                return Err(
762                    PreSerializeError::custom("SET OF elements are not in canonical DER order"),
763                );
764            }
765            proof {
766                let i = iter.index() + 1;
767                let vs = values.deep_view();
768                let serialize = |v: C::T| self.0.spec_serialize(v);
769                let prefix_encodings = vs[0..i].map_values(serialize);
770                let current_encoding = serialize(vs[i]);
771                lemma_der_encodings_sorted_push(prefix_encodings, current_encoding);
772                vs.lemma_map_take_succ(serialize, i);
773            }
774        }
775
776        assert(values.deep_view()[0..values.deep_view().len()] == values.deep_view());
777        Ok(total)
778    }
779}
780
781#[cfg(feature = "alloc")]
782impl<Output: OutputBuf, C, Elem> Serializer<Output, Vec<Elem>> for SetOfFmt<C> where
783    Elem: DeepView,
784    C: SpecCombinator<T = <Elem as DeepView>::V> + Serializer<Output, Elem> + Copy,
785 {
786    #[verifier::prophetic]
787    open spec fn exec_inv(&self) -> bool {
788        self.0.exec_inv()
789    }
790
791    fn serialize_into(&self, values: &Vec<Elem>, obuf: &mut Output) {
792        <Self as Serializer<Output, [Elem]>>::serialize_into(self, values.as_slice(), obuf)
793    }
794}
795
796#[cfg(feature = "alloc")]
797impl<C, Elem> ByteLen<Vec<Elem>> for SetOfFmt<C> where
798    C: SpecByteLen<T = <Elem as DeepView>::V> + ByteLen<Elem> + Copy,
799    Elem: DeepView,
800 {
801    open spec fn exec_inv(&self) -> bool {
802        self.0.exec_inv()
803    }
804
805    fn length(&self, values: &Vec<Elem>) -> (len: usize) {
806        <Self as ByteLen<[Elem]>>::length(self, values.as_slice())
807    }
808}
809
810#[cfg(feature = "alloc")]
811impl<C, Elem> Prepare<Vec<Elem>> for SetOfFmt<C> where
812    Elem: DeepView,
813    C: SpecCombinator<T = <Elem as DeepView>::V> + Prepare<Elem> + DerOrd<Elem> + Copy,
814 {
815    open spec fn exec_inv(&self) -> bool {
816        self.0.exec_inv()
817    }
818
819    fn prepare(&self, values: &Vec<Elem>) -> (checked: Result<usize, PreSerializeError>) {
820        <Self as Prepare<[Elem]>>::prepare(self, values.as_slice())
821    }
822}
823
824} // verus!
825#[cfg(all(test, feature = "alloc"))]
826mod tests {
827    use crate::asn1::der::{INTEGER8, SET_OF};
828    use crate::core::exec::{Parser, Prepare, SerializerExt};
829
830    #[test]
831    fn der_set_of_integer8_roundtrip_and_ordering() {
832        let format = SET_OF(INTEGER8);
833        let canonical = [0x31, 0x06, 0x02, 0x01, 0x01, 0x02, 0x01, 0x02];
834        let (consumed, values) = format.parse(&&canonical[..]).unwrap();
835        assert_eq!(consumed, canonical.len());
836        assert_eq!(values, vec![1, 2]);
837
838        assert_eq!(format.prepare(&values), Ok(canonical.len()));
839        let mut encoded = vec![0; format.prepare(&values).unwrap()];
840        format.serialize(&values, &mut encoded);
841        assert_eq!(encoded, canonical);
842
843        let unordered = [0x31, 0x06, 0x02, 0x01, 0x02, 0x02, 0x01, 0x01];
844        assert!(format.parse(&&unordered[..]).is_err());
845        assert!(format.prepare(&vec![2, 1]).is_err());
846    }
847
848    #[test]
849    fn der_set_of_allows_duplicate_encodings() {
850        let format = SET_OF(INTEGER8);
851        let duplicate = [0x31, 0x06, 0x02, 0x01, 0x01, 0x02, 0x01, 0x01];
852        let (_, values) = format.parse(&&duplicate[..]).unwrap();
853        assert_eq!(values, vec![1, 1]);
854        assert_eq!(format.prepare(&values), Ok(duplicate.len()));
855    }
856}
vest_lib/asn1/set_of.rs

vest_lib/asn1/
set_of.rs
