vest_lib/asn1/
bitstring.rs

1//! ASN.1 BIT STRING contents values and primitive contents format.
2use crate::core::exec::output::*;
3use crate::core::exec::{parser::*, serializer::*, ParseError, ParseErrorKind};
4use crate::{
5    combinators::{
6        bytes::ExactLen, length::AsLen, mapped::spec::FnSpecMapper, Bind, Mapped, Pair, Refined,
7        Tail, U8,
8    },
9    core::{proof::*, spec::*},
10};
11#[cfg(feature = "alloc")]
12use alloc::vec::Vec;
13use vstd::prelude::*;
14use OutputBuf;
15
16verus! {
17
18/// The ASN.1 BIT STRING.
19///
20/// Represented as:
21/// `(number_of_unused_bits_in_final_octet, payload_octets)`.
22pub struct BitString<'a, const DER: bool = true> {
23    /// Number of unused bits in the final octet of the BIT STRING.
24    unused: u8,
25    /// The payload octets of the BIT STRING.
26    bits: &'a [u8],
27}
28
29/// Owned BIT STRING value used when BER segments must be flattened.
30#[cfg(feature = "alloc")]
31pub struct BitStringOwned {
32    unused: u8,
33    bits: Vec<u8>,
34}
35
36#[verifier::ext_equal]
37pub struct BitStringSpec {
38    pub unused: u8,
39    pub bits: Seq<u8>,
40}
41
42impl<'a, const DER: bool> DeepView for BitString<'a, DER> {
43    type V = BitStringSpec;
44
45    closed spec fn deep_view(&self) -> Self::V {
46        BitStringSpec { unused: self.unused, bits: self.bits.deep_view() }
47    }
48}
49
50#[cfg(feature = "alloc")]
51impl DeepView for BitStringOwned {
52    type V = BitStringSpec;
53
54    closed spec fn deep_view(&self) -> Self::V {
55        BitStringSpec { unused: self.unused, bits: self.bits.deep_view() }
56    }
57}
58
59impl<'a, const DER: bool> BitString<'a, DER> {
60    #[verifier::type_invariant]
61    spec fn wf(&self) -> bool {
62        self.deep_view().wf::<DER>()
63    }
64
65    pub fn new(unused: u8, bits: &'a [u8]) -> (bs: Self)
66        requires
67            unused <= 7,
68            bits.len() == 0 ==> unused == 0,
69            DER ==> bits.len() > 0 ==> bits@.last().trailing_zeros() >= unused,
70        ensures
71            (bs.deep_view() == BitStringSpec { unused, bits: bits.deep_view() }),
72    {
73        BitString { unused, bits }
74    }
75
76    pub fn unused(&self) -> (unused: u8)
77        ensures
78            unused == self.deep_view().unused,
79            self.deep_view().wf::<DER>(),
80    {
81        proof {
82            use_type_invariant(self);
83        }
84        self.unused
85    }
86
87    pub fn bits(&self) -> (bits: &'a [u8])
88        ensures
89            bits.deep_view() == self.deep_view().bits,
90    {
91        self.bits
92    }
93}
94
95#[cfg(feature = "alloc")]
96impl BitStringOwned {
97    #[verifier::type_invariant]
98    spec fn wf(&self) -> bool {
99        self.deep_view().wf::<false>()
100    }
101
102    pub fn new(unused: u8, bits: Vec<u8>) -> (value: Self)
103        requires
104            unused <= 7,
105            bits.len() == 0 ==> unused == 0,
106        ensures
107            value.deep_view() == (BitStringSpec { unused, bits: bits.deep_view() }),
108    {
109        Self { unused, bits }
110    }
111
112    pub fn unused(&self) -> (unused: u8)
113        ensures
114            unused == self.deep_view().unused,
115            self.deep_view().wf::<false>(),
116    {
117        proof {
118            use_type_invariant(self);
119        }
120        self.unused
121    }
122
123    pub fn bits(&self) -> (bits: &[u8])
124        ensures
125            bits.deep_view() == self.deep_view().bits,
126    {
127        self.bits.as_slice()
128    }
129}
130
131impl BitStringSpec {
132    #[verusfmt::skip]
133    pub open spec fn wf<const DER: bool>(&self) -> bool {
134        &&& self.unused <= 7
135        // 8.6.2.3 If the bitstring is empty, there shall be no subsequent octets, and the initial octet shall be zero.
136        &&& (self.bits.len() == 0 ==> self.unused == 0)
137        // 11.2.1 Each unused bit in the final octet of the encoding of a bit string value shall be set to zero.
138        &&& (DER ==> self.bits.len() > 0 ==> self.bits.last().trailing_zeros() >= self.unused)
139    }
140}
141
142type BitStringFmt<const DER: bool> = Mapped<
143    Refined<Pair<U8, Tail>, PredFnSpec<(u8, Seq<u8>)>>,
144    FnSpecMapper<(u8, Seq<u8>), BitStringSpec>,
145>;
146
147pub(super) open(super) spec fn bitstring_fmt<const DER: bool>() -> BitStringFmt<DER> {
148    Mapped {
149        inner: Refined(
150            Pair(U8, Tail),
151            |r: (u8, Seq<u8>)|
152                {
153                    let (unused, bits) = r;
154                    BitStringSpec { unused, bits }.wf::<DER>()
155                },
156        ),
157        mapper: (
158            |r: (u8, Seq<u8>)|
159                {
160                    let (unused, bits) = r;
161                    BitStringSpec { unused, bits }
162                },
163            |spec: BitStringSpec| (spec.unused, spec.bits),
164        ),
165    }
166}
167
168/// Exposes the serialization model used by the allocation-free DER ordering cursor.
169pub(crate) proof fn lemma_bit_string_fmt_serialization<const DER: bool>(value: BitStringSpec)
170    ensures
171        super::BitStringFmt::<DER>.spec_serialize(value) == Pair(U8, Tail).spec_serialize(
172            (value.unused, value.bits),
173        ),
174        super::BitStringFmt::<DER>.byte_len(value) == Pair(U8, Tail).byte_len(
175            (value.unused, value.bits),
176        ),
177{
178}
179
180mod derived_specs {
181    use super::*;
182    use super::super::BitStringFmt;
183
184    impl<const DER: bool> SpecParser for BitStringFmt<DER> {
185        type PVal = BitStringSpec;
186
187        open(super) spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
188            bitstring_fmt::<DER>().spec_parse(ibuf)
189        }
190    }
191
192    impl<const DER: bool> Consistency for BitStringFmt<DER> {
193        type Val = BitStringSpec;
194
195        open(super) spec fn consistent(&self, v: Self::Val) -> bool {
196            bitstring_fmt::<DER>().consistent(v)
197        }
198    }
199
200    impl<const DER: bool> SpecSerializerDps for BitStringFmt<DER> {
201        type SValue = BitStringSpec;
202
203        open(super) spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
204            bitstring_fmt::<DER>().spec_serialize_dps(v, obuf)
205        }
206    }
207
208    impl<const DER: bool> SpecSerializer for BitStringFmt<DER> {
209        type SVal = BitStringSpec;
210
211        open(super) spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
212            bitstring_fmt::<DER>().spec_serialize(v)
213        }
214    }
215
216    impl<const DER: bool> SpecByteLen for BitStringFmt<DER> {
217        type T = BitStringSpec;
218
219        open(super) spec fn byte_len(&self, v: Self::T) -> nat {
220            bitstring_fmt::<DER>().byte_len(v)
221        }
222    }
223
224}
225
226mod derived_proofs {
227    use super::*;
228    use super::super::BitStringFmt;
229
230    impl<const DER: bool> SafeParser for BitStringFmt<DER> {
231        proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
232            bitstring_fmt::<DER>().lemma_parse_safe(ibuf);
233        }
234    }
235
236    impl<const DER: bool> Productive for BitStringFmt<DER> {
237        proof fn lemma_productive(&self, s: Seq<u8>) {
238            bitstring_fmt::<DER>().lemma_productive(s);
239        }
240    }
241
242    impl<const DER: bool> SoundParser for BitStringFmt<DER> {
243        proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
244            bitstring_fmt::<DER>().lemma_parse_sound_consumption(ibuf);
245        }
246
247        proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
248            bitstring_fmt::<DER>().lemma_parse_sound_value(ibuf);
249        }
250    }
251
252    impl<const DER: bool> GoodSerializer for BitStringFmt<DER> {
253        proof fn lemma_serialize_len(&self, v: Self::SVal) {
254            bitstring_fmt::<DER>().lemma_serialize_len(v);
255        }
256    }
257
258    impl<const DER: bool> SPRoundTripDps for BitStringFmt<DER> {
259        proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
260            bitstring_fmt::<DER>().theorem_serialize_dps_parse_roundtrip(v, obuf);
261        }
262    }
263
264    impl<const DER: bool> NonMalleable for BitStringFmt<DER> {
265        proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
266            bitstring_fmt::<DER>().lemma_parse_non_malleable(buf1, buf2);
267        }
268    }
269
270    impl<const DER: bool> EquivSerializers for BitStringFmt<DER> {
271        proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
272            bitstring_fmt::<DER>().lemma_serialize_equiv_on_empty(v);
273        }
274    }
275
276}
277
278impl<'i, const DER: bool> Parser<&'i [u8]> for super::BitStringFmt<DER> {
279    type PT = BitString<'i, DER>;
280
281    fn parse(&self, ibuf: &&'i [u8]) -> PResult<Self::PT> {
282        let (n, (unused, bits)): (usize, (u8, &[u8])) = Pair(U8, Tail).parse(ibuf)?;
283        if unused > 7 {
284            return Err(ParseError::custom("Invalid number of unused bits in BIT STRING"));
285        }
286        if bits.len() == 0 && unused != 0 {
287            return Err(ParseError::custom("Invalid number of unused bits in BIT STRING"));
288        }
289        if DER && bits.len() > 0 && bits[bits.len() - 1].trailing_zeros() < unused as u32 {
290            return Err(ParseError::custom("Non-canonical encoding of BIT STRING."));
291        }
292        Ok((n, BitString::new(unused, bits)))
293    }
294}
295
296impl<Output: OutputBuf, 'i, const DER: bool> Serializer<
297    Output,
298    BitString<'i, DER>,
299> for super::BitStringFmt<DER> {
300    fn serialize_into(&self, v: &BitString<'i, DER>, obuf: &mut Output) {
301        broadcast use crate::core::exec::output::outbuf_lemmas;
302
303        U8.serialize_into(&v.unused, obuf);
304        Tail.serialize_into(&v.bits, obuf);
305    }
306}
307
308impl<'i, const DER: bool> Prepare<BitString<'i, DER>> for super::BitStringFmt<DER> {
309    fn prepare(&self, v: &BitString<'i, DER>) -> Result<usize, PreSerializeError> {
310        proof {
311            use_type_invariant(v);
312        }
313        let n1 = U8.prepare(&v.unused)?;
314        let n2 = Tail.prepare(&v.bits)?;
315        let total_len = n1.checked_add(n2).ok_or(PreSerializeError::length_too_large())?;
316        Ok(total_len)
317    }
318}
319
320impl<'i, const DER: bool> ByteLen<BitString<'i, DER>> for super::BitStringFmt<DER> {
321    fn length(&self, v: &BitString<'i, DER>) -> usize {
322        let n1 = U8.length(&v.unused);
323        let n2 = Tail.length(&v.bits);
324        n1 + n2
325    }
326}
327
328#[cfg(feature = "alloc")]
329impl<Output: OutputBuf> Serializer<Output, BitStringOwned> for super::BitStringFmt<false> {
330    fn serialize_into(&self, v: &BitStringOwned, obuf: &mut Output) {
331        broadcast use crate::core::exec::output::outbuf_lemmas;
332
333        proof {
334            use_type_invariant(v);
335        }
336        U8.serialize_into(&v.unused, obuf);
337        Tail.serialize_into(&v.bits.as_slice(), obuf);
338    }
339}
340
341#[cfg(feature = "alloc")]
342impl Prepare<BitStringOwned> for super::BitStringFmt<false> {
343    fn prepare(&self, v: &BitStringOwned) -> Result<usize, PreSerializeError> {
344        proof {
345            use_type_invariant(v);
346        }
347        let n1 = U8.prepare(&v.unused)?;
348        let n2 = Tail.prepare(&v.bits.as_slice())?;
349        n1.checked_add(n2).ok_or(PreSerializeError::length_too_large())
350    }
351}
352
353#[cfg(feature = "alloc")]
354impl ByteLen<BitStringOwned> for super::BitStringFmt<false> {
355    fn length(&self, v: &BitStringOwned) -> usize {
356        U8.length(&v.unused) + Tail.length(&v.bits.as_slice())
357    }
358}
359
360} // verus!
vest_lib/asn1/bitstring.rs

vest_lib/asn1/
bitstring.rs
