verdict_parser/asn1/
implicit.rs

1use super::*;
2use vstd::prelude::*;
3
4verus! {
5
6/// Implicit tagging replaces the tag value in the ASN1Tagged trait,
7/// but otherwise parses/serializes exactly the same way as the inner combinator
8#[derive(Debug, View)]
9pub struct ImplicitTag<T>(pub TagValue, pub T);
10
11impl<T> ASN1Tagged for ImplicitTag<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 ImplicitTag<T> {
23    proof fn lemma_view_preserves_tag(&self) {}
24}
25
26impl<T: SpecCombinator> SpecCombinator for ImplicitTag<T> {
27    type SpecResult = T::SpecResult;
28
29    closed spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()> {
30        self.1.spec_parse(s)
31    }
32
33    proof fn spec_parse_wf(&self, s: Seq<u8>) {
34        self.1.spec_parse_wf(s)
35    }
36
37    closed spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()> {
38        self.1.spec_serialize(v)
39    }
40}
41
42impl<T: SecureSpecCombinator> SecureSpecCombinator for ImplicitTag<T> {
43    open spec fn is_prefix_secure() -> bool {
44        T::is_prefix_secure()
45    }
46
47    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult) {
48        self.1.theorem_serialize_parse_roundtrip(v)
49    }
50
51    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
52        self.1.theorem_parse_serialize_roundtrip(buf)
53    }
54
55    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
56        self.1.lemma_prefix_secure(s1, s2)
57    }
58}
59
60impl<T: ASN1Tagged + Combinator> Combinator for ImplicitTag<T> where
61    <T as View>::V: SecureSpecCombinator<SpecResult = <<T as Combinator>::Owned as View>::V>,
62    <T as View>::V: ASN1Tagged,
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        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        self.1.serialize(v, data, pos)
91    }
92}
93
94}
verdict_parser/asn1/implicit.rs

verdict_parser/asn1/
implicit.rs
