verdict_parser/asn1/
octet_string.rs

1use super::*;
2use vstd::prelude::*;
3
4verus! {
5
6/// Combainator for OCTET STRING in ASN.1
7#[derive(Debug, View)]
8pub struct OctetString;
9
10asn1_tagged!(OctetString, tag_of!(OCTET_STRING));
11
12impl SpecCombinator for OctetString {
13    type SpecResult = Seq<u8>;
14
15    closed spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()> {
16        match new_spec_octet_string_inner().spec_parse(s) {
17            Ok((len, (_, v))) => Ok((len, v)),
18            Err(..) => Err(()),
19        }
20    }
21
22    proof fn spec_parse_wf(&self, s: Seq<u8>) {
23        new_spec_octet_string_inner().spec_parse_wf(s)
24    }
25
26    closed spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()> {
27        new_spec_octet_string_inner().spec_serialize((v.len() as LengthValue, v))
28    }
29}
30
31impl SecureSpecCombinator for OctetString {
32    open spec fn is_prefix_secure() -> bool {
33        true
34    }
35
36    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult) {
37        new_spec_octet_string_inner().theorem_serialize_parse_roundtrip((v.len() as LengthValue, v));
38    }
39
40    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
41        new_spec_octet_string_inner().theorem_parse_serialize_roundtrip(buf);
42    }
43
44    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
45        new_spec_octet_string_inner().lemma_prefix_secure(s1, s2);
46    }
47}
48
49impl Combinator for OctetString {
50    type Result<'a> = &'a [u8];
51    type Owned = Vec<u8>;
52
53    closed spec fn spec_length(&self) -> Option<usize> {
54        None
55    }
56
57    fn length(&self) -> Option<usize> {
58        None
59    }
60
61    #[inline(always)]
62    fn parse<'a>(&self, s: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) {
63        let (len, (_, v)) = new_octet_string_inner().parse(s)?;
64        Ok((len, v))
65    }
66
67    #[inline(always)]
68    fn serialize(&self, v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> (res: Result<usize, SerializeError>) {
69        new_octet_string_inner().serialize((v.len() as LengthValue, v), data, pos)
70    }
71}
72
73/// The function |i| Bytes(i)
74struct BytesCont;
75
76impl Continuation for BytesCont {
77    type Input<'a> = LengthValue;
78    type Output = Bytes;
79
80    #[inline(always)]
81    fn apply<'a>(&self, i: Self::Input<'a>) -> (o: Self::Output) {
82        Bytes(i as usize)
83    }
84
85    closed spec fn requires<'a>(&self, i: Self::Input<'a>) -> bool {
86        true
87    }
88
89    closed spec fn ensures<'a>(&self, i: Self::Input<'a>, o: Self::Output) -> bool {
90        &&& o == Bytes(i as usize)
91        &&& o.parse_requires()
92        &&& o.serialize_requires()
93    }
94}
95
96#[allow(dead_code)]
97type SpecOctetStringInner = SpecDepend<Length, Bytes>;
98type OctetStringInner = Depend<Length, Bytes, BytesCont>;
99
100closed spec fn new_spec_octet_string_inner() -> SpecOctetStringInner {
101    SpecDepend {
102        fst: Length,
103        snd: |l| {
104            Bytes(l as usize)
105        },
106    }
107}
108
109closed spec fn spec_new_octet_string_inner() -> OctetStringInner
110{
111    Depend {
112        fst: Length,
113        snd: BytesCont,
114        spec_snd: Ghost(|l| {
115            Bytes(l as usize)
116        }),
117    }
118}
119
120#[inline(always)]
121fn new_octet_string_inner() -> (res: OctetStringInner)
122    ensures
123        res@ == new_spec_octet_string_inner(),
124        res == spec_new_octet_string_inner(),
125{
126    Depend {
127        fst: Length,
128        snd: BytesCont,
129        spec_snd: Ghost(|l| {
130            Bytes(l as usize)
131        }),
132    }
133}
134
135}
136
137#[cfg(test)]
138mod test {
139    use super::*;
140    use der::Encode;
141
142    fn serialize_octet_string(v: &[u8]) -> Result<Vec<u8>, SerializeError> {
143        let mut data = vec![0; v.len() + 10];
144        data[0] = 0x04; // Prepend the tag byte
145        let len = OctetString.serialize(v, &mut data, 1)?;
146        data.truncate(len + 1);
147        Ok(data)
148    }
149
150    #[test]
151    fn diff_with_der() {
152        let diff = |bytes: &[u8]| {
153            let res1 = serialize_octet_string(bytes).map_err(|_| ());
154            let res2 = der::asn1::OctetString::new(bytes)
155                .unwrap()
156                .to_der()
157                .map_err(|_| ());
158            assert_eq!(res1, res2);
159        };
160
161        diff(&[]);
162        diff(&[0]);
163        diff(&[0; 256]);
164        diff(&[0; 257]);
165        diff(&[0; 65536]);
166    }
167}
verdict_parser/asn1/octet_string.rs

verdict_parser/asn1/
octet_string.rs
