verdict_parser/asn1/
bit_string.rs

1use super::*;
2use std::fmt::{self, Debug, Formatter};
3use vstd::prelude::*;
4
5verus! {
6
7/// Combainator for BIT STRING in ASN.1
8/// Essentially a refined version of OctetString
9/// where we require that the first bit correctly
10/// specifies the trailing zeros
11#[derive(Debug, View)]
12pub struct BitString;
13
14asn1_tagged!(BitString, tag_of!(BIT_STRING));
15
16// #[derive(View, PolyfillClone)]
17// pub struct BitStringValuePoly<T>(pub T);
18
19pub type SpecBitStringValue = Seq<u8>;
20
21pub struct BitStringValue<'a>(&'a [u8]);
22#[allow(dead_code)]
23pub struct BitStringValueOwned(Vec<u8>);
24
25impl<'a> PolyfillClone for BitStringValue<'a> {
26    #[inline(always)]
27    fn clone(&self) -> Self {
28        proof {
29            use_type_invariant(self);
30        }
31        BitStringValue(&self.0)
32    }
33}
34
35impl<'a> View for BitStringValue<'a> {
36    type V = Seq<u8>;
37
38    closed spec fn view(&self) -> Self::V {
39        self.0@
40    }
41}
42
43impl View for BitStringValueOwned {
44    type V = Seq<u8>;
45
46    closed spec fn view(&self) -> Self::V {
47        self.0@
48    }
49}
50
51impl<'a> BitStringValue<'a> {
52    #[verifier::type_invariant]
53    closed spec fn inv(self) -> bool {
54        Self::spec_wf(self@)
55    }
56
57    pub open spec fn spec_wf(s: SpecBitStringValue) -> bool {
58        // Empty string
59        ||| s.len() == 1 && s[0] == 0
60
61        // Otherwise, check that all trailing bits (as declared in bytes[0]) are zeros
62        ||| s.len() > 1 && s[0] <= s.last().trailing_zeros()
63    }
64
65    #[inline(always)]
66    pub fn wf(s: &'a [u8]) -> (res: bool)
67        ensures res == Self::spec_wf(s@)
68    {
69        s.len() == 1 && s[0] == 0
70        || s.len() > 1 && s[0] as u32 <= s[s.len() - 1].trailing_zeros()
71    }
72
73    /// Create a BitString from raw bytes
74    /// The first byte of the slice should indicate the number of trailing zeros
75    #[inline(always)]
76    pub fn new_raw(s: &'a [u8]) -> (res: Option<BitStringValue<'a>>)
77        ensures
78            res matches Some(res) ==> res@ == s@ && Self::spec_wf(res@),
79            res.is_none() ==> !Self::spec_wf(s@)
80    {
81        if Self::wf(s) {
82            Some(BitStringValue(s))
83        } else {
84            None
85        }
86    }
87
88    /// Get the number of padded zeros at the end
89    #[inline(always)]
90    pub fn trailing_zeros(&self) -> u8
91    {
92        proof {
93            use_type_invariant(self);
94        }
95        self.0[self.0.len() - 1]
96    }
97
98    pub closed spec fn spec_bytes(s: SpecBitStringValue) -> SpecBitStringValue {
99        s.drop_first()
100    }
101
102    /// Get the actual (zero-padded) bit string
103    #[inline(always)]
104    pub fn bytes(&self) -> (res: &[u8])
105        ensures res@ == Self::spec_bytes(self@)
106    {
107        proof {
108            use_type_invariant(self);
109        }
110        slice_drop_first(self.0)
111    }
112
113    /// Check if the n-th bit is set (counting from 0)
114    /// e.g. the 0-th bit is the most significant bit of the first byte
115    /// the 8-th bit is the most significant bit of the second byte
116    pub closed spec fn spec_has_bit(s: SpecBitStringValue, n: int) -> bool {
117        &&& n >= 0
118        &&& s.len() > 1 + n / 8
119        &&& s[1 + n / 8] & (1u8 << (7 - n % 8)) != 0
120    }
121
122    #[inline(always)]
123    pub fn has_bit(&self, n: usize) -> (res: bool)
124        ensures res == Self::spec_has_bit(self@, n as int)
125    {
126        proof {
127            use_type_invariant(self);
128        }
129        self.0.len() > 1 + n / 8 && self.0[1 + n / 8] & (1u8 << (7 - n as usize % 8)) != 0
130    }
131}
132
133impl SpecCombinator for BitString {
134    type SpecResult = SpecBitStringValue;
135
136    closed spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()> {
137        match OctetString.spec_parse(s) {
138            Ok((len, bytes)) =>
139                if BitStringValue::spec_wf(bytes) {
140                    Ok((len, bytes))
141                } else {
142                    Err(())
143                }
144
145            Err(..) => Err(()),
146        }
147    }
148
149    proof fn spec_parse_wf(&self, s: Seq<u8>) {
150        OctetString.spec_parse_wf(s);
151    }
152
153    closed spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()> {
154        if BitStringValue::spec_wf(v) {
155            OctetString.spec_serialize(v)
156        } else {
157            Err(())
158        }
159    }
160}
161
162impl SecureSpecCombinator for BitString {
163    open spec fn is_prefix_secure() -> bool {
164        true
165    }
166
167    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult) {
168        OctetString.theorem_serialize_parse_roundtrip(v);
169    }
170
171    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
172        OctetString.theorem_parse_serialize_roundtrip(buf);
173    }
174
175    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
176        OctetString.lemma_prefix_secure(s1, s2);
177    }
178}
179
180impl Combinator for BitString {
181    type Result<'a> = BitStringValue<'a>;
182    type Owned = BitStringValueOwned;
183
184    closed spec fn spec_length(&self) -> Option<usize> {
185        None
186    }
187
188    fn length(&self) -> Option<usize> {
189        None
190    }
191
192    #[inline(always)]
193    fn parse<'a>(&self, s: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) {
194        let (len, v) = OctetString.parse(s)?;
195
196        if let Some(s) = BitStringValue::new_raw(v) {
197            Ok((len, s))
198        } else {
199            Err(ParseError::Other("Ill-formed bit string".to_string()))
200        }
201    }
202
203    #[inline(always)]
204    fn serialize(&self, v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> (res: Result<usize, SerializeError>) {
205        proof {
206            use_type_invariant(&v);
207        }
208        OctetString.serialize(v.0, data, pos)
209    }
210}
211
212}
213
214impl<'a> Debug for BitStringValue<'a> {
215    fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
216        write!(
217            f,
218            "BitStringValue([{}] ",
219            (self.0.len() - 1) * 8 - self.0[0] as usize
220        )?;
221
222        // Print the hex values
223        for i in 1..self.0.len() {
224            write!(f, "{:02x}", self.0[i])?;
225        }
226
227        write!(f, ")")
228    }
229}
230
231#[cfg(test)]
232mod test {
233    use super::*;
234    use der::Encode;
235
236    fn serialize_bit_string(v: BitStringValue) -> Result<Vec<u8>, SerializeError> {
237        let mut data = vec![0; v.bytes().len() + 10];
238        data[0] = 0x03; // Prepend the tag byte
239        let len = BitString.serialize(v, &mut data, 1)?;
240        data.truncate(len + 1);
241        Ok(data)
242    }
243
244    #[test]
245    fn diff_with_der() {
246        // The first byte of raw should denote the number of trailing zeros
247        let diff = |raw: &[u8]| {
248            let res1 = serialize_bit_string(BitStringValue::new_raw(raw).unwrap()).map_err(|_| ());
249            let res2 = der::asn1::BitString::new(raw[0], &raw[1..])
250                .unwrap()
251                .to_der()
252                .map_err(|_| ());
253            assert_eq!(res1, res2);
254        };
255
256        diff(&[0]);
257        diff(&[5, 0b11100000]);
258        diff(&[4, 0b11100000]);
259    }
260
261    #[test]
262    fn has_bit() {
263        let (_, s) = BitString.parse(&[0x02, 0x01, 0x86]).unwrap();
264        assert_eq!(s.has_bit(0), true);
265        assert_eq!(s.has_bit(1), false);
266        assert_eq!(s.has_bit(2), false);
267        assert_eq!(s.has_bit(3), false);
268        assert_eq!(s.has_bit(4), false);
269        assert_eq!(s.has_bit(5), true);
270        assert_eq!(s.has_bit(6), true);
271        assert_eq!(s.has_bit(7), false);
272        assert_eq!(s.has_bit(100), false);
273    }
274}
verdict_parser/asn1/bit_string.rs

verdict_parser/asn1/
bit_string.rs
