verdict_parser/asn1/
len_wrapped.rs

1use super::*;
2use vstd::prelude::*;
3
4verus! {
5
6/// Wrap the inner combinator in a Length-Buffer pair
7#[derive(Debug)]
8pub struct LengthWrapped<T>(pub T);
9
10impl<T: View> View for LengthWrapped<T> {
11    type V = LengthWrapped<T::V>;
12
13    open spec fn view(&self) -> Self::V {
14        LengthWrapped(self.0@)
15    }
16}
17
18impl<T: SpecCombinator> SpecCombinator for LengthWrapped<T> {
19    type SpecResult = T::SpecResult;
20
21    closed spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()> {
22        match new_spec_length_wrapped_inner(self.0).spec_parse(s) {
23            Ok((len, (_, v))) => Ok((len, v)),
24            Err(..) => Err(()),
25        }
26    }
27
28    proof fn spec_parse_wf(&self, s: Seq<u8>) {
29        new_spec_length_wrapped_inner(self.0).spec_parse_wf(s)
30    }
31
32    closed spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()> {
33        match self.0.spec_serialize(v) {
34            // Need to compute the inner serialized length first
35            Ok(buf) => new_spec_length_wrapped_inner(self.0).spec_serialize((buf.len() as LengthValue, v)),
36            Err(..) => Err(()),
37        }
38    }
39}
40
41impl<T: SecureSpecCombinator> SecureSpecCombinator for LengthWrapped<T> {
42    open spec fn is_prefix_secure() -> bool {
43        true
44    }
45
46    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult) {
47        if let Ok(buf) = self.0.spec_serialize(v) {
48            new_spec_length_wrapped_inner(self.0).theorem_serialize_parse_roundtrip((buf.len() as LengthValue, v))
49        }
50    }
51
52    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
53        new_spec_length_wrapped_inner(self.0).theorem_parse_serialize_roundtrip(buf)
54    }
55
56    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
57        new_spec_length_wrapped_inner(self.0).lemma_prefix_secure(s1, s2)
58    }
59}
60
61impl<T: Combinator> Combinator for LengthWrapped<T> where
62    <T as View>::V: SecureSpecCombinator<SpecResult = <<T as Combinator>::Owned as View>::V>,
63    for<'a> T::Result<'a>: PolyfillClone,
64{
65    type Result<'a> = T::Result<'a>;
66    type Owned = T::Owned;
67
68    closed spec fn spec_length(&self) -> Option<usize> {
69        None
70    }
71
72    fn length(&self) -> Option<usize> {
73        None
74    }
75
76    open spec fn parse_requires(&self) -> bool {
77        self.0.parse_requires()
78    }
79
80    #[inline(always)]
81    fn parse<'a>(&self, s: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) {
82        let (len, (_, v)) = new_length_wrapped_inner(&self.0).parse(s)?;
83        Ok((len, v))
84    }
85
86    open spec fn serialize_requires(&self) -> bool {
87        self.0.serialize_requires()
88    }
89
90    #[inline(always)]
91    fn serialize(&self, v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> (res: Result<usize, SerializeError>) {
92        // TODO: can we avoid serializing twice?
93        let len = self.0.serialize(v.clone(), data, pos)?;
94        let final_len = new_length_wrapped_inner(&self.0).serialize((len as LengthValue, v), data, pos)?;
95
96        if pos < data.len() && final_len < data.len() - pos {
97            assert(data@ =~= seq_splice(old(data)@, pos, self@.spec_serialize(v@).unwrap()));
98            return Ok(final_len);
99        }
100
101        Err(SerializeError::InsufficientBuffer)
102    }
103}
104
105/// The function |i| AndThen<Bytes, T>
106pub struct LengthWrappedCont<'a, T>(pub &'a T);
107
108impl<'b, T: Combinator> Continuation for LengthWrappedCont<'b, T> where
109    <T as View>::V: SecureSpecCombinator<SpecResult = <<T as Combinator>::Owned as View>::V>,
110{
111    type Input<'a> = LengthValue;
112    type Output = AndThen<Bytes, &'b T>;
113
114    #[inline(always)]
115    fn apply<'a>(&self, i: Self::Input<'a>) -> (o: Self::Output) {
116        AndThen(Bytes(i as usize), &self.0)
117    }
118
119    closed spec fn requires<'a>(&self, i: Self::Input<'a>) -> bool {
120        true
121    }
122
123    closed spec fn ensures<'a>(&self, i: Self::Input<'a>, o: Self::Output) -> bool {
124        &&& self.0.parse_requires() ==> o.parse_requires()
125        &&& self.0.serialize_requires() ==> o.serialize_requires()
126        &&& o@ == AndThen(Bytes(i as usize), self.0@)
127    }
128}
129
130#[allow(dead_code)]
131type SpecLengthWrappedInner<T> = SpecDepend<Length, AndThen<Bytes, T>>;
132type LengthWrappedInner<'a, T> = Depend<Length, AndThen<Bytes, &'a T>, LengthWrappedCont<'a, T>>;
133
134/// SpecDepend version of new_length_wrapped_inner
135closed spec fn new_spec_length_wrapped_inner<T: SpecCombinator>(inner: T) -> SpecLengthWrappedInner<T> {
136    SpecDepend {
137        fst: Length,
138        snd: |l| {
139            AndThen(Bytes(l as usize), inner)
140        },
141    }
142}
143
144/// Spec version of new_length_wrapped_inner
145closed spec fn new_length_wrapped_inner_spec<'a, T: Combinator>(inner: &'a T) -> LengthWrappedInner<'a, T> where
146    <T as View>::V: SecureSpecCombinator<SpecResult = <<T as Combinator>::Owned as View>::V>,
147{
148    Depend {
149        fst: Length,
150        snd: LengthWrappedCont(inner),
151        spec_snd: Ghost(|l| {
152            AndThen(Bytes(l as usize), inner@)
153        }),
154    }
155}
156
157#[inline(always)]
158fn new_length_wrapped_inner<'a, T: Combinator>(inner: &'a T) -> (res: LengthWrappedInner<'a, T>) where
159    <T as View>::V: SecureSpecCombinator<SpecResult = <<T as Combinator>::Owned as View>::V>,
160
161    ensures
162        res == new_length_wrapped_inner_spec(inner),
163        res@ == new_spec_length_wrapped_inner(inner@),
164{
165    Depend {
166        fst: Length,
167        snd: LengthWrappedCont(inner),
168        spec_snd: Ghost(|l| {
169            AndThen(Bytes(l as usize), inner@)
170        }),
171    }
172}
173
174}
verdict_parser/asn1/len_wrapped.rs

verdict_parser/asn1/
len_wrapped.rs
