vest_lib/asn1/
any.rs

1//! ASN.1 ANY / open-type values.
2//!
3//! An ANY value is one complete, self-delimiting TLV. The semantic representation
4//! retains the decoded tag and opaque contents bytes.
5use crate::combinators::{
6    bytes::ExactLen, mapped::spec::FnSpecMapper, Bind, Mapped, Pair, Refined, Tail,
7};
8use crate::core::exec::input::InputBuf;
9use crate::core::exec::output::OutputBuf;
10use crate::core::exec::{
11    parser::{PResult, Parser},
12    serializer::{ByteLen, PreSerializeError, Prepare, Serializer},
13    ParseError,
14};
15use crate::core::{proof::*, spec::*};
16#[cfg(feature = "alloc")]
17use alloc::vec::Vec;
18use vstd::prelude::*;
19
20use super::{AnyFmt, LengthFmt, Tag, TagFmt};
21
22verus! {
23
24pub type AnyWireFmt<const DER: bool> = Pair<
25    TagFmt,
26    Bind<LengthFmt<DER>, spec_fn(usize) -> ExactLen<Tail, usize>>,
27>;
28
29pub type AnyInnerFmt<const DER: bool> = Refined<
30    Mapped<AnyWireFmt<DER>, FnSpecMapper<(Tag, (usize, Seq<u8>)), AnySpec>>,
31    PredFnSpec<AnySpec>,
32>;
33
34/// Semantic representation of an open type.
35#[verifier::ext_equal]
36pub struct AnySpec {
37    pub tag: Tag,
38    pub content: Seq<u8>,
39}
40
41pub open spec fn any_fmt<const DER: bool>() -> AnyInnerFmt<DER> {
42    Refined(
43        Mapped {
44            inner: Pair(TagFmt, Bind(LengthFmt::<DER>, |len: usize| ExactLen(len, Tail))),
45            mapper: (
46                |v: (Tag, (usize, Seq<u8>))| AnySpec { tag: v.0, content: v.1.1 },
47                |v: AnySpec| (v.tag, (v.content.len() as usize, v.content)),
48            ),
49        },
50        |v: AnySpec| v.tag != TagFmt::EOC,
51    )
52}
53
54proof fn lemma_any_mapped_sound_nonmal_inv()
55    ensures
56        any_fmt::<true>().0.sound_inv(),
57        any_fmt::<true>().0.nonmal_inv(),
58{
59    let mapped = any_fmt::<true>().0;
60    assert forall|v: (Tag, (usize, Seq<u8>))| #[trigger] mapped.inner.consistent(v) implies (
61    mapped.mapper.1)((mapped.mapper.0)(v)) == v by {
62        let (_tag, (len, content)) = v;
63        assert(len as nat == content.len());
64        assert(content.len() <= usize::MAX);
65    }
66}
67
68proof fn lemma_any_mapped_unambiguous<const DER: bool>()
69    ensures
70        any_fmt::<DER>().0.unambiguous(),
71{
72    let mapped = any_fmt::<DER>().0;
73    assert forall|v: AnySpec| #[trigger] mapped.consistent(v) implies (mapped.mapper.0)(
74        (mapped.mapper.1)(v),
75    ) == v by {}
76}
77
78mod derived_specs {
79    use super::*;
80
81    impl<const DER: bool> SpecParser for AnyFmt<DER> {
82        type PVal = AnySpec;
83
84        open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
85            any_fmt::<DER>().spec_parse(ibuf)
86        }
87    }
88
89    impl<const DER: bool> Consistency for AnyFmt<DER> {
90        type Val = AnySpec;
91
92        open spec fn consistent(&self, v: Self::Val) -> bool {
93            any_fmt::<DER>().consistent(v)
94        }
95    }
96
97    impl<const DER: bool> SpecSerializerDps for AnyFmt<DER> {
98        type SValue = AnySpec;
99
100        open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
101            any_fmt::<DER>().spec_serialize_dps(v, obuf)
102        }
103    }
104
105    impl<const DER: bool> SpecSerializer for AnyFmt<DER> {
106        type SVal = AnySpec;
107
108        open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
109            any_fmt::<DER>().spec_serialize(v)
110        }
111    }
112
113    impl<const DER: bool> SpecByteLen for AnyFmt<DER> {
114        type T = AnySpec;
115
116        open spec fn byte_len(&self, v: Self::T) -> nat {
117            any_fmt::<DER>().byte_len(v)
118        }
119    }
120
121}
122
123mod derived_proofs {
124    use super::*;
125
126    impl<const DER: bool> SafeParser for AnyFmt<DER> {
127        proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
128            any_fmt::<DER>().lemma_parse_safe(ibuf);
129        }
130    }
131
132    impl<const DER: bool> Productive for AnyFmt<DER> {
133        proof fn lemma_productive(&self, ibuf: Seq<u8>) {
134            any_fmt::<DER>().lemma_productive(ibuf);
135        }
136    }
137
138    impl SoundParser for AnyFmt<true> {
139        proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
140            lemma_any_mapped_sound_nonmal_inv();
141            any_fmt::<true>().lemma_parse_sound_consumption(ibuf);
142        }
143
144        proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
145            lemma_any_mapped_sound_nonmal_inv();
146            any_fmt::<true>().lemma_parse_sound_value(ibuf);
147        }
148    }
149
150    impl<const DER: bool> NonTailFmt for AnyFmt<DER> {
151        proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>) {
152            any_fmt::<DER>().lemma_serialize_dps_prepend(v, obuf);
153        }
154
155        proof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>) {
156            any_fmt::<DER>().lemma_serialize_dps_len(v, obuf);
157        }
158    }
159
160    impl<const DER: bool> GoodSerializer for AnyFmt<DER> {
161        proof fn lemma_serialize_len(&self, v: Self::SVal) {
162            any_fmt::<DER>().lemma_serialize_len(v);
163        }
164    }
165
166    impl<const DER: bool> SPRoundTripDps for AnyFmt<DER> {
167        proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
168            lemma_any_mapped_unambiguous::<DER>();
169            any_fmt::<DER>().theorem_serialize_dps_parse_roundtrip(v, obuf);
170        }
171    }
172
173    impl NonMalleable for AnyFmt<true> {
174        proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
175            lemma_any_mapped_sound_nonmal_inv();
176            any_fmt::<true>().lemma_parse_non_malleable(buf1, buf2);
177        }
178    }
179
180    impl<const DER: bool> EquivSerializersGeneral for AnyFmt<DER> {
181        proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
182            any_fmt::<DER>().lemma_serialize_equiv(v, obuf);
183        }
184    }
185
186    impl<const DER: bool> EquivSerializers for AnyFmt<DER> {
187        proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
188            any_fmt::<DER>().lemma_serialize_equiv_on_empty(v);
189        }
190    }
191
192}
193
194/// Borrowed executable open-type value.
195pub struct Any<'a> {
196    tag: Tag,
197    content: &'a [u8],
198}
199
200impl<'a> DeepView for Any<'a> {
201    type V = AnySpec;
202
203    closed spec fn deep_view(&self) -> Self::V {
204        AnySpec { tag: self.tag, content: self.content.deep_view() }
205    }
206}
207
208impl<'a> Any<'a> {
209    pub fn new(tag: Tag, content: &'a [u8]) -> (value: Self)
210        ensures
211            value.deep_view() == (AnySpec { tag, content: content.deep_view() }),
212    {
213        Self { tag, content }
214    }
215
216    pub fn tag(&self) -> (tag: Tag)
217        ensures
218            tag == self.deep_view().tag,
219    {
220        self.tag
221    }
222
223    pub fn content(&self) -> (content: &'a [u8])
224        ensures
225            content.deep_view() == self.deep_view().content,
226    {
227        self.content
228    }
229}
230
231/// Owned executable open-type value.
232///
233/// This is the representation used by the recursive BER ANY parser: an indefinite-length
234/// constructed value has no single borrowed content slice once its terminating EOC is removed.
235#[cfg(feature = "alloc")]
236pub struct AnyOwned {
237    tag: Tag,
238    content: Vec<u8>,
239}
240
241#[cfg(feature = "alloc")]
242impl DeepView for AnyOwned {
243    type V = AnySpec;
244
245    closed spec fn deep_view(&self) -> Self::V {
246        AnySpec { tag: self.tag, content: self.content.deep_view() }
247    }
248}
249
250#[cfg(feature = "alloc")]
251impl AnyOwned {
252    pub fn new(tag: Tag, content: Vec<u8>) -> (value: Self)
253        ensures
254            value.deep_view() == (AnySpec { tag, content: content.deep_view() }),
255    {
256        Self { tag, content }
257    }
258
259    pub fn tag(&self) -> (tag: Tag)
260        ensures
261            tag == self.deep_view().tag,
262    {
263        self.tag
264    }
265
266    pub fn content(&self) -> (content: &[u8])
267        ensures
268            content.deep_view() == self.deep_view().content,
269    {
270        self.content.as_slice()
271    }
272
273    pub fn into_content(self) -> (content: Vec<u8>)
274        ensures
275            content.deep_view() == self.deep_view().content,
276    {
277        self.content
278    }
279}
280
281impl<'a, const DER: bool> Parser<&'a [u8]> for AnyFmt<DER> {
282    type PT = Any<'a>;
283
284    fn parse(&self, ibuf: &&'a [u8]) -> PResult<Self::PT> {
285        broadcast use crate::core::spec::SafeParser::lemma_parse_safe;
286        broadcast use crate::core::spec::SoundParser::lemma_parse_sound_value;
287
288        let _ = ibuf.len();
289        let (n1, tag) = TagFmt.parse(ibuf)?;
290        if tag == TagFmt::EOC {
291            return Err(ParseError::invalid_tag());
292        }
293        let rest = ibuf.skip(n1);
294        let (n2, len) = LengthFmt::<DER>.parse(&rest)?;
295        let rest = rest.skip(n2);
296        let (n3, content) = ExactLen(len, Tail).parse(&rest)?;
297        Ok((n1 + n2 + n3, Any { tag, content }))
298    }
299}
300
301impl<'a, Output: OutputBuf, const DER: bool> Serializer<Output, Any<'a>> for AnyFmt<DER> {
302    fn serialize_into(&self, v: &Any<'a>, obuf: &mut Output) {
303        broadcast use crate::core::exec::output::outbuf_lemmas;
304
305        let len = v.content.len();
306        TagFmt.serialize_into(&v.tag, obuf);
307        LengthFmt::<DER>.serialize_into(&len, obuf);
308        Tail.serialize_into(&v.content, obuf);
309    }
310}
311
312impl<'a, const DER: bool> Prepare<Any<'a>> for AnyFmt<DER> {
313    fn prepare(&self, v: &Any<'a>) -> Result<usize, PreSerializeError> {
314        if v.tag == TagFmt::EOC {
315            return Err(PreSerializeError::custom("EOC is not an open-type value"));
316        }
317        let n1 = TagFmt.prepare(&v.tag)?;
318        let content_len = Tail.prepare(&v.content)?;
319        let n2 = LengthFmt::<DER>.prepare(&content_len)?;
320        let header = n1.checked_add(n2).ok_or(PreSerializeError::length_too_large())?;
321        let total = header.checked_add(content_len).ok_or(PreSerializeError::length_too_large())?;
322        Ok(total)
323    }
324}
325
326impl<'a, const DER: bool> ByteLen<Any<'a>> for AnyFmt<DER> {
327    fn length(&self, v: &Any<'a>) -> usize {
328        let n1 = TagFmt.length(&v.tag);
329        let content_len = Tail.length(&v.content);
330        let n2 = LengthFmt::<DER>.length(&content_len);
331        n1 + n2 + content_len
332    }
333}
334
335#[cfg(feature = "alloc")]
336impl<Output: OutputBuf, const DER: bool> Serializer<Output, AnyOwned> for AnyFmt<DER> {
337    fn serialize_into(&self, v: &AnyOwned, obuf: &mut Output) {
338        broadcast use crate::core::exec::output::outbuf_lemmas;
339
340        let len = v.content.len();
341        TagFmt.serialize_into(&v.tag, obuf);
342        LengthFmt::<DER>.serialize_into(&len, obuf);
343        Tail.serialize_into(v.content.as_slice(), obuf);
344    }
345}
346
347#[cfg(feature = "alloc")]
348impl<const DER: bool> Prepare<AnyOwned> for AnyFmt<DER> {
349    fn prepare(&self, v: &AnyOwned) -> Result<usize, PreSerializeError> {
350        if v.tag == TagFmt::EOC {
351            return Err(PreSerializeError::custom("EOC is not an open-type value"));
352        }
353        let n1 = TagFmt.prepare(&v.tag)?;
354        let content_len = Tail.prepare(v.content.as_slice())?;
355        let n2 = LengthFmt::<DER>.prepare(&content_len)?;
356        let header = n1.checked_add(n2).ok_or(PreSerializeError::length_too_large())?;
357        let total = header.checked_add(content_len).ok_or(PreSerializeError::length_too_large())?;
358        Ok(total)
359    }
360}
361
362#[cfg(feature = "alloc")]
363impl<const DER: bool> ByteLen<AnyOwned> for AnyFmt<DER> {
364    fn length(&self, v: &AnyOwned) -> usize {
365        let n1 = TagFmt.length(&v.tag);
366        let content_len = Tail.length(v.content.as_slice());
367        let n2 = LengthFmt::<DER>.length(&content_len);
368        n1 + n2 + content_len
369    }
370}
371
372} // verus!
373#[cfg(test)]
374mod tests {
375    use crate::asn1::TagFmt;
376    use crate::core::exec::{Parser, Prepare, SerializerExt};
377
378    #[test]
379    fn any_roundtrips_one_complete_tlv() {
380        let input = [0x30, 0x03, 0x02, 0x01, 0x05, 0xff];
381        let (n, value) = super::super::der::ANY.parse(&&input[..]).unwrap();
382        assert_eq!(n, 5);
383        assert_eq!(value.tag(), TagFmt::SEQUENCE);
384        assert_eq!(value.content(), &[0x02, 0x01, 0x05]);
385
386        let mut output = vec![0; super::super::der::ANY.prepare(&value).unwrap()];
387        super::super::der::ANY.serialize(&value, &mut output);
388        assert_eq!(output, &input[..5]);
389    }
390
391    #[test]
392    fn any_rejects_eoc_as_a_value() {
393        assert!(super::super::der::ANY.parse(&&[0x00, 0x00][..]).is_err());
394    }
395}
vest_lib/asn1/any.rs

vest_lib/asn1/
any.rs
