verdict_parser/asn1/
explicit.rs

1use super::*;
2use vstd::prelude::*;
3
4verus! {
5
6/// Explicit tagging wrapps the inner combinator in a new TLV tuple
7/// Equivalent to ImplicitTag(tag, LengthWrapped(inner))
8#[derive(Debug, View)]
9pub struct ExplicitTag<T>(pub TagValue, pub T);
10
11impl<T> ASN1Tagged for ExplicitTag<T> {
12    open spec fn spec_tag(&self) -> TagValue {
13        self.0
14    }
15
16    #[inline(always)]
17    fn tag(&self) -> TagValue {
18        self.0.clone()
19    }
20}
21
22impl<T: View> ViewWithASN1Tagged for ExplicitTag<T> {
23    proof fn lemma_view_preserves_tag(&self) {}
24}
25
26impl<T: SpecCombinator> SpecCombinator for ExplicitTag<T> {
27    type SpecResult = T::SpecResult;
28
29    closed spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()> {
30        LengthWrapped(self.1).spec_parse(s)
31    }
32
33    proof fn spec_parse_wf(&self, s: Seq<u8>) {
34        LengthWrapped(self.1).spec_parse_wf(s)
35    }
36
37    closed spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()> {
38        LengthWrapped(self.1).spec_serialize(v)
39    }
40}
41
42impl<T: SecureSpecCombinator> SecureSpecCombinator for ExplicitTag<T> {
43    open spec fn is_prefix_secure() -> bool {
44        true
45    }
46
47    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult) {
48        LengthWrapped(self.1).theorem_serialize_parse_roundtrip(v)
49    }
50
51    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
52        LengthWrapped(self.1).theorem_parse_serialize_roundtrip(buf)
53    }
54
55    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
56        LengthWrapped(self.1).lemma_prefix_secure(s1, s2)
57    }
58}
59
60impl<T: Combinator> Combinator for ExplicitTag<T> where
61    <T as View>::V: SecureSpecCombinator<SpecResult = <<T as Combinator>::Owned as View>::V>,
62    for<'a> T::Result<'a>: PolyfillClone,
63{
64    type Result<'a> = T::Result<'a>;
65    type Owned = T::Owned;
66
67    closed spec fn spec_length(&self) -> Option<usize> {
68        None
69    }
70
71    fn length(&self) -> Option<usize> {
72        None
73    }
74
75    open spec fn parse_requires(&self) -> bool {
76        self.1.parse_requires()
77    }
78
79    #[inline(always)]
80    fn parse<'a>(&self, s: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) {
81        LengthWrapped(&self.1).parse(s)
82    }
83
84    open spec fn serialize_requires(&self) -> bool {
85        self.1.serialize_requires()
86    }
87
88    #[inline(always)]
89    fn serialize(&self, v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> (res: Result<usize, SerializeError>) {
90        LengthWrapped(&self.1).serialize(v, data, pos)
91    }
92}
93
94}
verdict_parser/asn1/explicit.rs

verdict_parser/asn1/
explicit.rs
