vest_lib/asn1/
tlv.rs

1//! Generic ASN.1 tag-length-value wrappers for definite-length contents.
2use crate::asn1::{ASN1Fmt, LengthFmt, Tag, TagFmt};
3use crate::combinators::{
4    bytes::ExactLen, length::AsLen, mapped::spec::FnSpecMapper, Bind, Const, Mapped, PrefixTagged,
5};
6use crate::core::exec::output::*;
7use crate::core::{
8    exec::{
9        input::{InputBuf, InputSlice},
10        parser::{PResult, Parser},
11        serializer::{ByteLen, PreSerializeError, Prepare, Serializer, SerializerExt},
12        ParseError,
13    },
14    proof::*,
15    spec::*,
16};
17#[cfg(feature = "alloc")]
18use alloc::vec;
19use vstd::prelude::*;
20use OutputBuf;
21
22verus! {
23
24pub type ASN1InnerFmt<Content, const DER: bool> = Mapped<
25    PrefixTagged<TagFmt, Tag, Bind<LengthFmt<DER>, spec_fn(usize) -> ExactLen<Content, usize>>>,
26    FnSpecMapper<(usize, <Content as SpecByteLen>::T), <Content as SpecByteLen>::T>,
27>;
28
29pub open spec fn asn1_fmt<Content: SpecCombinator, const DER: bool>(
30    tag: Tag,
31    content: Content,
32) -> ASN1InnerFmt<Content, DER> {
33    Mapped {
34        inner: PrefixTagged(
35            TagFmt,
36            tag,
37            Bind(LengthFmt::<DER>, |len: usize| ExactLen(len, content)),
38        ),
39        mapper: (|i: (usize, Content::T)| i.1, |o: Content::T| (content.byte_len(o) as usize, o)),
40    }
41}
42
43mod derived_specs {
44    use super::*;
45
46    impl<Content: SpecCombinator, const DER: bool> SpecParser for ASN1Fmt<Content, DER> {
47        type PVal = Content::PVal;
48
49        open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
50            asn1_fmt::<Content, DER>(self.0, self.1).spec_parse(ibuf)
51        }
52    }
53
54    impl<Content: SpecCombinator, const DER: bool> Consistency for ASN1Fmt<Content, DER> {
55        type Val = Content::PVal;
56
57        open spec fn consistent(&self, v: Self::Val) -> bool {
58            asn1_fmt::<Content, DER>(self.0, self.1).consistent(v)
59        }
60    }
61
62    impl<Content: SpecCombinator, const DER: bool> SpecSerializerDps for ASN1Fmt<Content, DER> {
63        type SValue = Content::PVal;
64
65        open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
66            asn1_fmt::<Content, DER>(self.0, self.1).spec_serialize_dps(v, obuf)
67        }
68    }
69
70    impl<Content: SpecCombinator, const DER: bool> SpecSerializer for ASN1Fmt<Content, DER> {
71        type SVal = Content::PVal;
72
73        open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
74            asn1_fmt::<Content, DER>(self.0, self.1).spec_serialize(v)
75        }
76    }
77
78    impl<Content: SpecCombinator, const DER: bool> SpecByteLen for ASN1Fmt<Content, DER> {
79        type T = Content::PVal;
80
81        open spec fn byte_len(&self, v: Self::T) -> nat {
82            asn1_fmt::<Content, DER>(self.0, self.1).byte_len(v)
83        }
84    }
85
86}
87
88mod derived_proofs {
89    use super::*;
90
91    impl<Content: SpecCombinator + SafeParser, const DER: bool> SafeParser for ASN1Fmt<
92        Content,
93        DER,
94    > {
95        proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
96            asn1_fmt::<Content, DER>(self.0, self.1).lemma_parse_safe(ibuf);
97        }
98    }
99
100    impl<Content: SpecCombinator + Productive, const DER: bool> Productive for ASN1Fmt<
101        Content,
102        DER,
103    > {
104        proof fn lemma_productive(&self, s: Seq<u8>) {
105            asn1_fmt::<Content, DER>(self.0, self.1).lemma_productive(s);
106        }
107    }
108
109    impl<Content: SpecCombinator + SoundParser> SoundParser for ASN1Fmt<Content, true> {
110        open spec fn sound_inv(&self) -> bool {
111            &&& self.1.sound_inv()
112            &&& TagFmt.consistent(self.0)
113        }
114
115        proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
116            asn1_fmt::<Content, true>(self.0, self.1).lemma_parse_sound_consumption(ibuf);
117        }
118
119        proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
120            asn1_fmt::<Content, true>(self.0, self.1).lemma_parse_sound_value(ibuf);
121        }
122    }
123
124    impl<
125        Content: SpecCombinator + GoodSerializer + EquivSerializers,
126        const DER: bool,
127    > NonTailFmt for ASN1Fmt<Content, DER> {
128        open spec fn serialize_dps_inv(&self) -> bool {
129            &&& self.1.serialize_inv()
130            &&& self.1.equiv_inv()
131        }
132
133        proof fn lemma_serialize_dps_prepend(&self, v: Content::PVal, obuf: Seq<u8>) {
134            asn1_fmt::<Content, DER>(self.0, self.1).lemma_serialize_dps_prepend(v, obuf);
135        }
136
137        proof fn lemma_serialize_dps_len(&self, v: Content::PVal, obuf: Seq<u8>) {
138            asn1_fmt::<Content, DER>(self.0, self.1).lemma_serialize_dps_len(v, obuf);
139        }
140    }
141
142    impl<Content: SpecCombinator + GoodSerializer, const DER: bool> GoodSerializer for ASN1Fmt<
143        Content,
144        DER,
145    > {
146        open spec fn serialize_inv(&self) -> bool {
147            self.1.serialize_inv()
148        }
149
150        proof fn lemma_serialize_len(&self, v: Self::SVal) {
151            asn1_fmt::<Content, DER>(self.0, self.1).lemma_serialize_len(v);
152        }
153    }
154
155    impl<
156        Content: SpecCombinator + EquivSerializers + GoodSerializer + SPRoundTrip,
157        const DER: bool,
158    > SPRoundTripDps for ASN1Fmt<Content, DER> {
159        open spec fn unambiguous(&self) -> bool {
160            &&& self.1.serialize_inv()
161            &&& self.1.equiv_inv()
162            &&& self.1.sp_roundtrip_inv()
163        }
164
165        proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
166            asn1_fmt::<Content, DER>(self.0, self.1).theorem_serialize_dps_parse_roundtrip(v, obuf);
167        }
168    }
169
170    impl<Content: SpecCombinator + SafeParser, const DER: bool> NoLookAhead for ASN1Fmt<
171        Content,
172        DER,
173    > {
174        proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
175            asn1_fmt::<Content, DER>(self.0, self.1).lemma_no_lookahead(i1, i2);
176        }
177    }
178
179    impl<Content: SpecCombinator + SoundParser + NonMalleable> NonMalleable for ASN1Fmt<
180        Content,
181        true,
182    > {
183        open spec fn nonmal_inv(&self) -> bool {
184            &&& self.1.nonmal_inv()
185            &&& self.1.sound_inv()
186            &&& self.1.safe_inv()
187            &&& TagFmt.consistent(self.0)
188        }
189
190        proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
191            asn1_fmt::<Content, true>(self.0, self.1).lemma_parse_non_malleable(buf1, buf2);
192        }
193    }
194
195    impl<
196        Content: SpecCombinator + EquivSerializers,
197        const DER: bool,
198    > EquivSerializersGeneral for ASN1Fmt<Content, DER> {
199        open spec fn equiv_general_inv(&self) -> bool {
200            self.1.equiv_inv()
201        }
202
203        proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
204            asn1_fmt::<Content, DER>(self.0, self.1).lemma_serialize_equiv(v, obuf);
205        }
206    }
207
208    impl<Content: SpecCombinator + EquivSerializers, const DER: bool> EquivSerializers for ASN1Fmt<
209        Content,
210        DER,
211    > {
212        open spec fn equiv_inv(&self) -> bool {
213            self.1.equiv_inv()
214        }
215
216        proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
217            asn1_fmt::<Content, DER>(self.0, self.1).lemma_serialize_equiv_on_empty(v);
218        }
219    }
220
221}
222
223impl<'i, Content, const DER: bool> Parser<&'i [u8]> for ASN1Fmt<Content, DER> where
224    Content: SpecCombinator + Parser<&'i [u8]>,
225 {
226    type PT = Content::PT;
227
228    fn min_byte_len(&self) -> usize {
229        // Every TLV carries at least one identifier octet and one length octet
230        // before its content. This is what lets `SET OF` and `SEQUENCE OF`
231        // size their result.
232        2usize.saturating_add(self.1.min_byte_len())
233    }
234
235    open spec fn exec_inv(&self) -> bool {
236        self.1.exec_inv()
237    }
238
239    fn parse(&self, ibuf: &&'i [u8]) -> PResult<Self::PT> {
240        broadcast use crate::core::spec::SafeParser::lemma_parse_safe;
241        broadcast use crate::core::spec::SoundParser::lemma_parse_sound_value;
242        broadcast use super::tag::lemma_const_tag_fmt_exec_inv;
243
244        let _ = ibuf.len();
245
246        let (n1, _tag_val) = Const(TagFmt, self.0).parse(ibuf)?;
247        let rest = ibuf.skip(n1);
248        let (n2, len) = LengthFmt::<DER>.parse(&rest)?;
249        let rest = rest.skip(n2);
250        let (n3, val) = ExactLen(len, &self.1).parse(&rest)?;
251        Ok((n1 + n2 + n3, val))
252    }
253}
254
255impl<Output: OutputBuf, Content, T, const DER: bool> Serializer<Output, T> for ASN1Fmt<
256    Content,
257    DER,
258> where T: DeepView + ?Sized, Content: SpecCombinator + Serializer<Output, T> + ByteLen<T> {
259    #[verifier::prophetic]
260    open spec fn exec_inv(&self) -> bool {
261        &&& <_ as Serializer<Output, T>>::exec_inv(&self.1)
262        &&& <_ as ByteLen<T>>::exec_inv(&self.1)
263    }
264
265    fn serialize_into(&self, v: &T, obuf: &mut Output) {
266        broadcast use crate::core::exec::output::outbuf_lemmas;
267
268        let ghost vv = v.deep_view();
269        assert(self.consistent(vv) == (self.1.byte_len(vv) as usize as nat == self.1.byte_len(vv)));
270        assert(self.1.byte_len(vv) <= usize::MAX);
271        let len = self.1.length(v);
272
273        Const(TagFmt, self.0).serialize_into(&self.0, obuf);
274        LengthFmt::<DER>.serialize_into(&len, obuf);
275        self.1.serialize_into(v, obuf);
276    }
277}
278
279impl<Content, T, const DER: bool> Prepare<T> for ASN1Fmt<Content, DER> where
280    T: DeepView + ?Sized,
281    Content: SpecCombinator + Prepare<T>,
282 {
283    open spec fn exec_inv(&self) -> bool {
284        self.1.exec_inv()
285    }
286
287    fn prepare(&self, v: &T) -> Result<usize, PreSerializeError> {
288        broadcast use super::tag::lemma_const_tag_fmt_exec_inv;
289
290        let n1 = Const(TagFmt, self.0).prepare(&self.0)?;
291        let n3 = self.1.prepare(v)?;
292        let n2 = LengthFmt::<DER>.prepare(&n3)?;
293        let _total_len = n1.checked_add(n2).ok_or(
294            PreSerializeError::length_too_large(),
295        )?.checked_add(n3).ok_or(PreSerializeError::length_too_large())?;
296        Ok(n1 + n2 + n3)
297    }
298}
299
300impl<Content, T, const DER: bool> ByteLen<T> for ASN1Fmt<Content, DER> where
301    T: DeepView + ?Sized,
302    Content: SpecCombinator + ByteLen<T>,
303 {
304    open spec fn exec_inv(&self) -> bool {
305        self.1.exec_inv()
306    }
307
308    fn length(&self, v: &T) -> usize {
309        let n1 = Const(TagFmt, self.0).length(&self.0);
310        let n3 = self.1.length(v);
311        let n2 = LengthFmt::<DER>.length(&n3);
312        n1 + n2 + n3
313    }
314}
315
316} // verus!
317/*
318*
319some test functions
320*/
321verus! {
322
323#[cfg(feature = "alloc")]
324fn test_exec_asn1_fmt(buf: &&[u8]) -> PResult<bool> {
325    use super::BoolFmt;
326    use super::{BER, DER};
327
328    let asn_bool = ASN1Fmt::<_, DER>(TagFmt::BOOLEAN, BoolFmt::<DER>);
329    let (_n, v) = asn_bool.parse(buf)?;
330    if let Ok(len) = asn_bool.prepare(&v) {
331        let mut obuf = vec![0; len];
332        asn_bool.serialize(&v, &mut obuf);
333
334        proof {
335            asn_bool.theorem_parse_serialize_roundtrip(buf@);
336            assert(obuf@ == buf@[0.._n]);
337        }
338    }
339    Err(ParseError::custom("Test function"))
340}
341
342} // verus!
343#[cfg(test)]
344mod tests {
345    use super::*;
346    use crate::asn1::bitstring::BitString;
347    use crate::asn1::tag::{Class, TagNumber};
348    use crate::asn1::{ASN1Fmt, BitStringFmt, BoolFmt, Tag};
349    use crate::asn1::{BER, DER};
350    use crate::core::exec::{ByteLen, Parser, Prepare, SerializerExt};
351
352    #[test]
353    fn test_asn1_bool_der_and_ber() {
354        // DER BoolFmt (canonical: TRUE must be 0xFF)
355        let der_bool = ASN1Fmt::<_, DER>(TagFmt::BOOLEAN, BoolFmt::<DER>);
356
357        // Parse valid true
358        let input_true = [0x01, 0x01, 0xFF];
359        let (n, val) = der_bool.parse(&&input_true[..]).unwrap();
360        assert_eq!(n, 3);
361        assert_eq!(val, true);
362
363        // Parse valid false
364        let input_false = [0x01, 0x01, 0x00];
365        let (n, val) = der_bool.parse(&&input_false[..]).unwrap();
366        assert_eq!(n, 3);
367        assert_eq!(val, false);
368
369        // Parse invalid/non-canonical true (0x01) under DER -> should fail
370        let input_noncanonical = [0x01, 0x01, 0x01];
371        assert!(der_bool.parse(&&input_noncanonical[..]).is_err());
372
373        // BER BoolFmt (permits any non-zero byte for true)
374        let ber_bool = ASN1Fmt::<_, BER>(TagFmt::BOOLEAN, BoolFmt::<BER>);
375        let (n, val) = ber_bool.parse(&&input_noncanonical[..]).unwrap();
376        assert_eq!(n, 3);
377        assert_eq!(val, true);
378
379        // Serialize and check DER roundtrip
380        let mut out = vec![0; der_bool.prepare(&true).unwrap()];
381        der_bool.serialize(&true, &mut out);
382        assert_eq!(out, input_true);
383        assert_eq!(der_bool.prepare(&true), Ok(3));
384        assert_eq!(der_bool.length(&true), 3);
385    }
386
387    #[test]
388    fn test_asn1_bitstring_der_and_ber() {
389        // DER BitString (requires trailing unused bits to be zero)
390        let der_bitstring = ASN1Fmt::<_, DER>(TagFmt::BIT_STRING, BitStringFmt::<DER>);
391
392        // Valid BIT STRING: 4 unused bits, last byte 0xA0 (0b1010_0000)
393        let input_valid = [0x03, 0x02, 0x04, 0xA0];
394        let (n, bs) = der_bitstring.parse(&&input_valid[..]).unwrap();
395        assert_eq!(n, 4);
396        assert_eq!(bs.unused(), 4);
397        assert_eq!(bs.bits(), &[0xA0]);
398
399        // Invalid BIT STRING under DER: 4 unused bits, but last byte is 0xA1 (0b1010_0001) - final bit is 1, not 0
400        let input_invalid = [0x03, 0x02, 0x04, 0xA1];
401        assert!(der_bitstring.parse(&&input_invalid[..]).is_err());
402
403        // Under BER, non-zero trailing bits are permitted
404        let ber_bitstring = ASN1Fmt::<_, BER>(TagFmt::BIT_STRING, BitStringFmt::<BER>);
405        let (n, bs) = ber_bitstring.parse(&&input_invalid[..]).unwrap();
406        assert_eq!(n, 4);
407        assert_eq!(bs.unused(), 4);
408        assert_eq!(bs.bits(), &[0xA1]);
409
410        // Roundtrip serialization for DER BitString
411        let valid_bs = BitString::new(4, &[0xA0]);
412        let mut out = vec![0; der_bitstring.prepare(&valid_bs).unwrap()];
413        der_bitstring.serialize(&valid_bs, &mut out);
414        assert_eq!(out, input_valid);
415        assert_eq!(der_bitstring.prepare(&valid_bs), Ok(4));
416        assert_eq!(der_bitstring.length(&valid_bs), 4);
417    }
418}
vest_lib/asn1/tlv.rs

vest_lib/asn1/
tlv.rs
