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    open spec fn exec_inv(&self) -> bool {
229        self.1.exec_inv()
230    }
231
232    fn parse(&self, ibuf: &&'i [u8]) -> PResult<Self::PT> {
233        broadcast use crate::core::spec::SafeParser::lemma_parse_safe;
234        broadcast use crate::core::spec::SoundParser::lemma_parse_sound_value;
235        broadcast use super::tag::lemma_const_tag_fmt_exec_inv;
236
237        let _ = ibuf.len();
238
239        let (n1, _tag_val) = Const(TagFmt, self.0).parse(ibuf)?;
240        let rest = ibuf.skip(n1);
241        let (n2, len) = LengthFmt::<DER>.parse(&rest)?;
242        let rest = rest.skip(n2);
243        let (n3, val) = ExactLen(len, &self.1).parse(&rest)?;
244        Ok((n1 + n2 + n3, val))
245    }
246}
247
248impl<Output: OutputBuf, Content, T, const DER: bool> Serializer<Output, T> for ASN1Fmt<
249    Content,
250    DER,
251> where T: DeepView + ?Sized, Content: SpecCombinator + Serializer<Output, T> + ByteLen<T> {
252    #[verifier::prophetic]
253    open spec fn exec_inv(&self) -> bool {
254        &&& <_ as Serializer<Output, T>>::exec_inv(&self.1)
255        &&& <_ as ByteLen<T>>::exec_inv(&self.1)
256    }
257
258    fn serialize_into(&self, v: &T, obuf: &mut Output) {
259        broadcast use crate::core::exec::output::outbuf_lemmas;
260
261        let ghost vv = v.deep_view();
262        assert(self.consistent(vv) == (self.1.byte_len(vv) as usize as nat == self.1.byte_len(vv)));
263        assert(self.1.byte_len(vv) <= usize::MAX);
264        let len = self.1.length(v);
265
266        Const(TagFmt, self.0).serialize_into(&self.0, obuf);
267        LengthFmt::<DER>.serialize_into(&len, obuf);
268        self.1.serialize_into(v, obuf);
269    }
270}
271
272impl<Content, T, const DER: bool> Prepare<T> for ASN1Fmt<Content, DER> where
273    T: DeepView + ?Sized,
274    Content: SpecCombinator + Prepare<T>,
275 {
276    open spec fn exec_inv(&self) -> bool {
277        self.1.exec_inv()
278    }
279
280    fn prepare(&self, v: &T) -> Result<usize, PreSerializeError> {
281        broadcast use super::tag::lemma_const_tag_fmt_exec_inv;
282
283        let n1 = Const(TagFmt, self.0).prepare(&self.0)?;
284        let n3 = self.1.prepare(v)?;
285        let n2 = LengthFmt::<DER>.prepare(&n3)?;
286        let _total_len = n1.checked_add(n2).ok_or(
287            PreSerializeError::length_too_large(),
288        )?.checked_add(n3).ok_or(PreSerializeError::length_too_large())?;
289        Ok(n1 + n2 + n3)
290    }
291}
292
293impl<Content, T, const DER: bool> ByteLen<T> for ASN1Fmt<Content, DER> where
294    T: DeepView + ?Sized,
295    Content: SpecCombinator + ByteLen<T>,
296 {
297    open spec fn exec_inv(&self) -> bool {
298        self.1.exec_inv()
299    }
300
301    fn length(&self, v: &T) -> usize {
302        let n1 = Const(TagFmt, self.0).length(&self.0);
303        let n3 = self.1.length(v);
304        let n2 = LengthFmt::<DER>.length(&n3);
305        n1 + n2 + n3
306    }
307}
308
309} // verus!
310/*
311*
312some test functions
313*/
314verus! {
315
316#[cfg(feature = "alloc")]
317fn test_exec_asn1_fmt(buf: &&[u8]) -> PResult<bool> {
318    use super::BoolFmt;
319    use super::{BER, DER};
320
321    let asn_bool = ASN1Fmt::<_, DER>(TagFmt::BOOLEAN, BoolFmt::<DER>);
322    let (_n, v) = asn_bool.parse(buf)?;
323    if let Ok(len) = asn_bool.prepare(&v) {
324        let mut obuf = vec![0; len];
325        asn_bool.serialize(&v, &mut obuf);
326
327        proof {
328            asn_bool.theorem_parse_serialize_roundtrip(buf@);
329            assert(obuf@ == buf@.take(_n as int));
330        }
331    }
332    Err(ParseError::custom("Test function"))
333}
334
335} // verus!
336#[cfg(test)]
337mod tests {
338    use super::*;
339    use crate::asn1::bitstring::BitString;
340    use crate::asn1::tag::{Class, TagNumber};
341    use crate::asn1::{ASN1Fmt, BitStringFmt, BoolFmt, Tag};
342    use crate::asn1::{BER, DER};
343    use crate::core::exec::{ByteLen, Parser, Prepare, SerializerExt};
344
345    #[test]
346    fn test_asn1_bool_der_and_ber() {
347        // DER BoolFmt (canonical: TRUE must be 0xFF)
348        let der_bool = ASN1Fmt::<_, DER>(TagFmt::BOOLEAN, BoolFmt::<DER>);
349
350        // Parse valid true
351        let input_true = [0x01, 0x01, 0xFF];
352        let (n, val) = der_bool.parse(&&input_true[..]).unwrap();
353        assert_eq!(n, 3);
354        assert_eq!(val, true);
355
356        // Parse valid false
357        let input_false = [0x01, 0x01, 0x00];
358        let (n, val) = der_bool.parse(&&input_false[..]).unwrap();
359        assert_eq!(n, 3);
360        assert_eq!(val, false);
361
362        // Parse invalid/non-canonical true (0x01) under DER -> should fail
363        let input_noncanonical = [0x01, 0x01, 0x01];
364        assert!(der_bool.parse(&&input_noncanonical[..]).is_err());
365
366        // BER BoolFmt (permits any non-zero byte for true)
367        let ber_bool = ASN1Fmt::<_, BER>(TagFmt::BOOLEAN, BoolFmt::<BER>);
368        let (n, val) = ber_bool.parse(&&input_noncanonical[..]).unwrap();
369        assert_eq!(n, 3);
370        assert_eq!(val, true);
371
372        // Serialize and check DER roundtrip
373        let mut out = vec![0; der_bool.prepare(&true).unwrap()];
374        der_bool.serialize(&true, &mut out);
375        assert_eq!(out, input_true);
376        assert_eq!(der_bool.prepare(&true), Ok(3));
377        assert_eq!(der_bool.length(&true), 3);
378    }
379
380    #[test]
381    fn test_asn1_bitstring_der_and_ber() {
382        // DER BitString (requires trailing unused bits to be zero)
383        let der_bitstring = ASN1Fmt::<_, DER>(TagFmt::BIT_STRING, BitStringFmt::<DER>);
384
385        // Valid BIT STRING: 4 unused bits, last byte 0xA0 (0b1010_0000)
386        let input_valid = [0x03, 0x02, 0x04, 0xA0];
387        let (n, bs) = der_bitstring.parse(&&input_valid[..]).unwrap();
388        assert_eq!(n, 4);
389        assert_eq!(bs.unused(), 4);
390        assert_eq!(bs.bits(), &[0xA0]);
391
392        // Invalid BIT STRING under DER: 4 unused bits, but last byte is 0xA1 (0b1010_0001) - final bit is 1, not 0
393        let input_invalid = [0x03, 0x02, 0x04, 0xA1];
394        assert!(der_bitstring.parse(&&input_invalid[..]).is_err());
395
396        // Under BER, non-zero trailing bits are permitted
397        let ber_bitstring = ASN1Fmt::<_, BER>(TagFmt::BIT_STRING, BitStringFmt::<BER>);
398        let (n, bs) = ber_bitstring.parse(&&input_invalid[..]).unwrap();
399        assert_eq!(n, 4);
400        assert_eq!(bs.unused(), 4);
401        assert_eq!(bs.bits(), &[0xA1]);
402
403        // Roundtrip serialization for DER BitString
404        let valid_bs = BitString::new(4, &[0xA0]);
405        let mut out = vec![0; der_bitstring.prepare(&valid_bs).unwrap()];
406        der_bitstring.serialize(&valid_bs, &mut out);
407        assert_eq!(out, input_valid);
408        assert_eq!(der_bitstring.prepare(&valid_bs), Ok(4));
409        assert_eq!(der_bitstring.length(&valid_bs), 4);
410    }
411}
vest_lib/asn1/tlv.rs

vest_lib/asn1/
tlv.rs
