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            |(unused, bits): (u8, Seq<u8>)| BitStringSpec { unused, bits }.wf::<DER>(),
152        ),
153        mapper: (
154            |(unused, bits): (u8, Seq<u8>)| BitStringSpec { unused, bits },
155            |spec: BitStringSpec| (spec.unused, spec.bits),
156        ),
157    }
158}
159
160/// Exposes the serialization model used by the allocation-free DER ordering cursor.
161pub(crate) proof fn lemma_bit_string_fmt_serialization<const DER: bool>(value: BitStringSpec)
162    ensures
163        super::BitStringFmt::<DER>.spec_serialize(value) == Pair(U8, Tail).spec_serialize(
164            (value.unused, value.bits),
165        ),
166        super::BitStringFmt::<DER>.byte_len(value) == Pair(U8, Tail).byte_len(
167            (value.unused, value.bits),
168        ),
169{
170}
171
172mod derived_specs {
173    use super::*;
174    use super::super::BitStringFmt;
175
176    impl<const DER: bool> SpecParser for BitStringFmt<DER> {
177        type PVal = BitStringSpec;
178
179        open(super) spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
180            bitstring_fmt::<DER>().spec_parse(ibuf)
181        }
182    }
183
184    impl<const DER: bool> Consistency for BitStringFmt<DER> {
185        type Val = BitStringSpec;
186
187        open(super) spec fn consistent(&self, v: Self::Val) -> bool {
188            bitstring_fmt::<DER>().consistent(v)
189        }
190    }
191
192    impl<const DER: bool> SpecSerializerDps for BitStringFmt<DER> {
193        type SValue = BitStringSpec;
194
195        open(super) spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
196            bitstring_fmt::<DER>().spec_serialize_dps(v, obuf)
197        }
198    }
199
200    impl<const DER: bool> SpecSerializer for BitStringFmt<DER> {
201        type SVal = BitStringSpec;
202
203        open(super) spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
204            bitstring_fmt::<DER>().spec_serialize(v)
205        }
206    }
207
208    impl<const DER: bool> SpecByteLen for BitStringFmt<DER> {
209        type T = BitStringSpec;
210
211        open(super) spec fn byte_len(&self, v: Self::T) -> nat {
212            bitstring_fmt::<DER>().byte_len(v)
213        }
214    }
215
216}
217
218mod derived_proofs {
219    use super::*;
220    use super::super::BitStringFmt;
221
222    impl<const DER: bool> SafeParser for BitStringFmt<DER> {
223        proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
224            bitstring_fmt::<DER>().lemma_parse_safe(ibuf);
225        }
226    }
227
228    impl<const DER: bool> Productive for BitStringFmt<DER> {
229        proof fn lemma_productive(&self, s: Seq<u8>) {
230            bitstring_fmt::<DER>().lemma_productive(s);
231        }
232    }
233
234    impl<const DER: bool> SoundParser for BitStringFmt<DER> {
235        proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
236            bitstring_fmt::<DER>().lemma_parse_sound_consumption(ibuf);
237        }
238
239        proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
240            bitstring_fmt::<DER>().lemma_parse_sound_value(ibuf);
241        }
242    }
243
244    impl<const DER: bool> GoodSerializer for BitStringFmt<DER> {
245        proof fn lemma_serialize_len(&self, v: Self::SVal) {
246            bitstring_fmt::<DER>().lemma_serialize_len(v);
247        }
248    }
249
250    impl<const DER: bool> SPRoundTripDps for BitStringFmt<DER> {
251        proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
252            bitstring_fmt::<DER>().theorem_serialize_dps_parse_roundtrip(v, obuf);
253        }
254    }
255
256    impl<const DER: bool> NonMalleable for BitStringFmt<DER> {
257        proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
258            bitstring_fmt::<DER>().lemma_parse_non_malleable(buf1, buf2);
259        }
260    }
261
262    impl<const DER: bool> EquivSerializers for BitStringFmt<DER> {
263        proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
264            bitstring_fmt::<DER>().lemma_serialize_equiv_on_empty(v);
265        }
266    }
267
268}
269
270impl<'i, const DER: bool> Parser<&'i [u8]> for super::BitStringFmt<DER> {
271    type PT = BitString<'i, DER>;
272
273    fn parse(&self, ibuf: &&'i [u8]) -> PResult<Self::PT> {
274        let (n, (unused, bits)): (usize, (u8, &[u8])) = Pair(U8, Tail).parse(ibuf)?;
275        if unused > 7 {
276            return Err(ParseError::custom("Invalid number of unused bits in BIT STRING"));
277        }
278        if bits.len() == 0 && unused != 0 {
279            return Err(ParseError::custom("Invalid number of unused bits in BIT STRING"));
280        }
281        if DER && bits.len() > 0 && bits[bits.len() - 1].trailing_zeros() < unused as u32 {
282            return Err(ParseError::custom("Non-canonical encoding of BIT STRING."));
283        }
284        Ok((n, BitString::new(unused, bits)))
285    }
286}
287
288impl<Output: OutputBuf, 'i, const DER: bool> Serializer<
289    Output,
290    BitString<'i, DER>,
291> for super::BitStringFmt<DER> {
292    fn serialize_into(&self, v: &BitString<'i, DER>, obuf: &mut Output) {
293        broadcast use crate::core::exec::output::outbuf_lemmas;
294
295        U8.serialize_into(&v.unused, obuf);
296        Tail.serialize_into(&v.bits, obuf);
297    }
298}
299
300impl<'i, const DER: bool> Prepare<BitString<'i, DER>> for super::BitStringFmt<DER> {
301    fn prepare(&self, v: &BitString<'i, DER>) -> Result<usize, PreSerializeError> {
302        proof {
303            use_type_invariant(v);
304        }
305        let n1 = U8.prepare(&v.unused)?;
306        let n2 = Tail.prepare(&v.bits)?;
307        let total_len = n1.checked_add(n2).ok_or(PreSerializeError::length_too_large())?;
308        Ok(total_len)
309    }
310}
311
312impl<'i, const DER: bool> ByteLen<BitString<'i, DER>> for super::BitStringFmt<DER> {
313    fn length(&self, v: &BitString<'i, DER>) -> usize {
314        let n1 = U8.length(&v.unused);
315        let n2 = Tail.length(&v.bits);
316        n1 + n2
317    }
318}
319
320#[cfg(feature = "alloc")]
321impl<Output: OutputBuf> Serializer<Output, BitStringOwned> for super::BitStringFmt<false> {
322    fn serialize_into(&self, v: &BitStringOwned, obuf: &mut Output) {
323        broadcast use crate::core::exec::output::outbuf_lemmas;
324
325        proof {
326            use_type_invariant(v);
327        }
328        U8.serialize_into(&v.unused, obuf);
329        Tail.serialize_into(&v.bits.as_slice(), obuf);
330    }
331}
332
333#[cfg(feature = "alloc")]
334impl Prepare<BitStringOwned> for super::BitStringFmt<false> {
335    fn prepare(&self, v: &BitStringOwned) -> Result<usize, PreSerializeError> {
336        proof {
337            use_type_invariant(v);
338        }
339        let n1 = U8.prepare(&v.unused)?;
340        let n2 = Tail.prepare(&v.bits.as_slice())?;
341        n1.checked_add(n2).ok_or(PreSerializeError::length_too_large())
342    }
343}
344
345#[cfg(feature = "alloc")]
346impl ByteLen<BitStringOwned> for super::BitStringFmt<false> {
347    fn length(&self, v: &BitStringOwned) -> usize {
348        U8.length(&v.unused) + Tail.length(&v.bits.as_slice())
349    }
350}
351
352} // verus!
vest_lib/asn1/bitstring.rs

vest_lib/asn1/
bitstring.rs
