verdict_parser/asn1/
len.rs

1use super::*;
2use vstd::prelude::*;
3
4verus! {
5
6/// Combinator for the length field in a TLV tuple
7#[derive(Debug, View)]
8pub struct Length;
9
10/// NOTE: this should fit into a VarUIntResult
11pub type LengthValue = usize;
12
13impl SpecCombinator for Length {
14    type SpecResult = LengthValue;
15
16    closed spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()>
17    {
18        if s.len() == 0 {
19            Err(())
20        } else if s[0] < 0x80 {
21            // One-byte length
22            Ok((1, s[0] as LengthValue))
23        } else {
24            // Multi-byte length
25            let bytes = (s[0] - 0x80) as LengthValue;
26            match VarUInt(bytes as usize).spec_parse(s.drop_first()) {
27                Ok((n, v)) => {
28                    // Need to check for minimal encoding for non-malleability
29                    // For 1-byte length, v > 0x7f
30                    // For (2+)-byte length, v can not be represented by fewer bytes
31                    if bytes > 0 && !fits_n_bytes_unsigned!(v, bytes - 1) && v > 0x7f && v <= LengthValue::MAX {
32                        Ok(((n + 1) as usize, v as LengthValue))
33                    } else {
34                        Err(())
35                    }
36                }
37                Err(()) => Err(()),
38            }
39        }
40    }
41
42    proof fn spec_parse_wf(&self, s: Seq<u8>) {
43        if s.len() != 0 && s[0] >= 0x80 {
44            let bytes = (s[0] - 0x80) as LengthValue;
45            VarUInt(bytes as usize).spec_parse_wf(s.drop_first());
46        }
47    }
48
49    closed spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()>
50    {
51        if v < 0x80 {
52            Ok(seq![v as u8])
53        } else {
54            // Find the minimum number of bytes required to represent v
55            let bytes = min_num_bytes_unsigned(v as VarUIntResult);
56
57            match VarUInt(bytes as usize).spec_serialize(v as VarUIntResult) {
58                Ok(buf) => Ok(seq![(0x80 + bytes) as u8] + buf),
59                Err(()) => Err(()),
60            }
61        }
62    }
63}
64
65impl SecureSpecCombinator for Length {
66    open spec fn is_prefix_secure() -> bool {
67        true
68    }
69
70    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult) {
71        if let Ok(buf) = self.spec_serialize(v) {
72            if v >= 0x80 {
73                let bytes = min_num_bytes_unsigned(v as VarUIntResult);
74                let var_uint = VarUInt(bytes as usize);
75
76                lemma_min_num_bytes_unsigned(v as VarUIntResult);
77
78                var_uint.theorem_serialize_parse_roundtrip(v as VarUIntResult);
79                var_uint.lemma_serialize_ok_len(v as VarUIntResult);
80
81                let buf2 = var_uint.spec_serialize(v as VarUIntResult).unwrap();
82                assert(buf.drop_first() == buf2);
83            }
84        }
85    }
86
87    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
88        if let Ok((n, v)) = self.spec_parse(buf) {
89            if buf[0] < 0x80 {
90                assert(seq![ buf[0] ] == buf.subrange(0, 1));
91            } else {
92                let bytes = (buf[0] - 0x80) as UInt;
93                let var_uint = VarUInt(bytes as usize);
94
95                // Base lemmas from VarUInt
96                var_uint.theorem_parse_serialize_roundtrip(buf.drop_first());
97                var_uint.lemma_parse_ok(buf.drop_first());
98                var_uint.lemma_parse_ok_bound(buf.drop_first());
99
100                // Parse the inner VarUInt
101                let (len, v2) = var_uint.spec_parse(buf.drop_first()).unwrap();
102
103                assert(is_min_num_bytes_unsigned(v2, bytes));
104                lemma_min_num_bytes_unsigned(v2);
105
106                // Some sequence facts
107                assert(var_uint.spec_serialize(v as VarUIntResult).is_ok());
108                let buf2 = var_uint.spec_serialize(v as VarUIntResult).unwrap();
109                assert(seq![(0x80 + bytes) as u8] + buf2 == buf.subrange(0, 1 + bytes));
110            }
111        }
112    }
113
114    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
115        if s1.len() > 0 {
116            let bytes = (s1[0] - 0x80) as UInt;
117            VarUInt(bytes as usize).lemma_prefix_secure(s1.drop_first(), s2);
118            assert((s1 + s2).drop_first() =~= s1.drop_first() + s2);
119        }
120    }
121}
122
123impl Combinator for Length {
124    type Result<'a> = LengthValue;
125    type Owned = LengthValue;
126
127    closed spec fn spec_length(&self) -> Option<usize> {
128        None
129    }
130
131    fn length(&self) -> Option<usize> {
132        None
133    }
134
135    #[inline]
136    fn parse<'a>(&self, s: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) {
137        if s.len() == 0 {
138            return Err(ParseError::UnexpectedEndOfInput);
139        }
140
141        if s[0] < 0x80 {
142            // One-byte length
143            return Ok((1, s[0] as LengthValue));
144        }
145
146        let bytes = (s[0] - 0x80) as UInt;
147
148        let (len, v) = VarUInt(bytes as usize).parse(slice_drop_first(s))?;
149
150        if bytes > 0 && !fits_n_bytes_unsigned!(v, bytes - 1) && v > 0x7f && v <= LengthValue::MAX as VarUIntResult {
151            Ok(((len + 1) as usize, v as LengthValue))
152        } else {
153            Err(ParseError::Other("Invalid length encoding".to_string()))
154        }
155    }
156
157    #[inline]
158    fn serialize(&self, v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> (res: Result<usize, SerializeError>) {
159        if v < 0x80 {
160            if pos < data.len() {
161                data.set(pos, v as u8);
162                assert(data@ =~= seq_splice(old(data)@, pos, seq![v as u8]));
163                return Ok(1);
164            } else {
165                return Err(SerializeError::InsufficientBuffer);
166            }
167        }
168
169        let bytes = min_num_bytes_unsigned_exec(v as VarUIntResult);
170
171        // Check if out of bound
172        if pos >= data.len() || pos > usize::MAX - 1 {
173            return Err(SerializeError::InsufficientBuffer);
174        }
175
176        data.set(pos, (0x80 + bytes) as u8);
177        let len = VarUInt(bytes as usize).serialize(v as VarUIntResult, data, pos + 1)?;
178
179        proof {
180            lemma_min_num_bytes_unsigned(v as VarUIntResult);
181            assert(data@ =~= seq_splice(old(data)@, pos, self@.spec_serialize(v).unwrap()));
182        }
183
184        Ok(len + 1)
185    }
186}
187
188}
189
190#[cfg(test)]
191mod test {
192    use super::*;
193
194    #[test]
195    fn parse() {
196        assert_eq!(Length.parse(&[0x0]).unwrap(), (1, 0));
197        assert_eq!(Length.parse(&[0x7f]).unwrap(), (1, 0x7f));
198        assert_eq!(Length.parse(&[0x81, 0x80]).unwrap(), (2, 0x80));
199        assert_eq!(Length.parse(&[0x82, 0x0f, 0xff]).unwrap(), (3, 0x0fff));
200
201        assert!(Length.parse(&[0x80]).is_err());
202        assert!(Length.parse(&[0x81, 0x7f]).is_err());
203        assert!(Length.parse(&[0x82, 0x00, 0xff]).is_err());
204    }
205}
verdict_parser/asn1/len.rs

verdict_parser/asn1/
len.rs
