verdict_parser/asn1/
seq_of.rs

1use super::*;
2use vstd::prelude::*;
3
4verus! {
5
6/// SEQUENCE OF in ASN.1
7#[derive(Debug, View)]
8pub struct SequenceOf<C>(pub C);
9
10pub type SequenceOfValue<T> = VecDeep<T>;
11
12impl<C> ASN1Tagged for SequenceOf<C> {
13    open spec fn spec_tag(&self) -> TagValue {
14        tag_of!(SEQUENCE)
15    }
16
17    #[inline(always)]
18    fn tag(&self) -> TagValue {
19        tag_of!(SEQUENCE)
20    }
21}
22
23impl<C: View> ViewWithASN1Tagged for SequenceOf<C> {
24    proof fn lemma_view_preserves_tag(&self) {}
25}
26
27impl<C: SecureSpecCombinator + SpecCombinator> SpecCombinator for SequenceOf<C> {
28    type SpecResult = Seq<C::SpecResult>;
29
30    closed spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()> {
31        ExplicitTag(self.spec_tag(), Repeat(self.0)).spec_parse(s)
32    }
33
34    proof fn spec_parse_wf(&self, s: Seq<u8>) {
35        ExplicitTag(self.spec_tag(), Repeat(self.0)).spec_parse_wf(s)
36    }
37
38    closed spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()> {
39        ExplicitTag(self.spec_tag(), Repeat(self.0)).spec_serialize(v)
40    }
41}
42
43impl<C: SecureSpecCombinator + SpecCombinator> SecureSpecCombinator for SequenceOf<C> {
44    open spec fn is_prefix_secure() -> bool {
45        true
46    }
47
48    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult) {
49        ExplicitTag(self.spec_tag(), Repeat(self.0)).theorem_serialize_parse_roundtrip(v);
50    }
51
52    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
53        ExplicitTag(self.spec_tag(), Repeat(self.0)).theorem_parse_serialize_roundtrip(buf);
54    }
55
56    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
57        ExplicitTag(self.spec_tag(), Repeat(self.0)).lemma_prefix_secure(s1, s2);
58    }
59}
60
61impl<C: Combinator> Combinator for SequenceOf<C> where
62    <C as View>::V: SecureSpecCombinator<SpecResult = <C::Owned as View>::V>,
63    for<'a> C::Result<'a>: PolyfillClone,
64{
65    type Result<'a> = SequenceOfValue<C::Result<'a>>;
66    type Owned = SequenceOfValue<C::Owned>;
67
68    closed spec fn spec_length(&self) -> Option<usize> {
69        None
70    }
71
72    fn length(&self) -> Option<usize> {
73        None
74    }
75
76    open spec fn parse_requires(&self) -> bool {
77        &&& <C as View>::V::is_prefix_secure()
78        &&& self.0.parse_requires()
79    }
80
81    #[inline(always)]
82    fn parse<'a>(&self, s: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) {
83        ExplicitTag(self.tag(), Repeat(&self.0)).parse(s)
84    }
85
86    open spec fn serialize_requires(&self) -> bool {
87        &&& <C as View>::V::is_prefix_secure()
88        &&& self.0.serialize_requires()
89    }
90
91    #[inline(always)]
92    fn serialize(&self, v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> (res: Result<usize, SerializeError>) {
93        ExplicitTag(self.tag(), Repeat(&self.0)).serialize(v, data, pos)
94    }
95}
96
97}
verdict_parser/asn1/seq_of.rs

verdict_parser/asn1/
seq_of.rs
