vest_lib/combinators/bytes/
proof.rs

1//! Correctness proofs for fixed- and variable-length bytes.
2use crate::combinators::length::AsLen;
3use crate::combinators::Tail;
4use crate::core::{proof::*, spec::*};
5use vstd::prelude::*;
6
7use super::Varied;
8
9verus! {
10
11impl<const N: usize> SPRoundTripDps for super::Fixed<N> {
12    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
13    }
14}
15
16impl<const N: usize> NonMalleable for super::Fixed<N> {
17    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
18    }
19}
20
21impl<const N: usize> NoLookAhead for super::Fixed<N> {
22    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
23    }
24}
25
26impl<const N: usize> Productive for super::Fixed<N> {
27    open spec fn productive_inv(&self) -> bool {
28        N > 0
29    }
30
31    proof fn lemma_productive(&self, s: Seq<u8>) {
32    }
33}
34
35impl<const N: usize> EquivSerializersGeneral for super::Fixed<N> {
36    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
37    }
38}
39
40impl<const N: usize> EquivSerializers for super::Fixed<N> {
41    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
42    }
43}
44
45impl<Len: AsLen> SPRoundTripDps for super::Varied<Len> {
46    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
47    }
48}
49
50impl<Len: AsLen> NonMalleable for super::Varied<Len> {
51    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
52    }
53}
54
55impl<Len: AsLen> NoLookAhead for super::Varied<Len> {
56    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
57    }
58}
59
60impl<Len: AsLen> Productive for super::Varied<Len> {
61    open spec fn productive_inv(&self) -> bool {
62        self.0.as_nat() > 0
63    }
64
65    proof fn lemma_productive(&self, s: Seq<u8>) {
66    }
67}
68
69impl<Len: AsLen> EquivSerializersGeneral for super::Varied<Len> {
70    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
71    }
72}
73
74impl<Len: AsLen> EquivSerializers for super::Varied<Len> {
75    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
76    }
77}
78
79impl<Inner, Len> SPRoundTripDps for super::ExactLen<Inner, Len> where
80    Inner: EquivSerializers + GoodSerializer + SPRoundTrip,
81    Len: AsLen,
82 {
83    open spec fn unambiguous(&self) -> bool {
84        &&& self.1.serialize_inv()
85        &&& self.1.equiv_inv()
86        &&& self.1.sp_roundtrip_inv()
87    }
88
89    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
90        let inner_bytes = self.1.spec_serialize_dps(v, seq![]);
91        self.1.lemma_serialize_equiv_on_empty(v);
92        self.1.lemma_serialize_len(v);
93        self.1.theorem_serialize_parse_roundtrip(v);
94        super::Varied(self.0).theorem_serialize_dps_parse_roundtrip(inner_bytes, obuf);
95    }
96}
97
98impl<Inner: NonMalleable, Len: AsLen> NonMalleable for super::ExactLen<Inner, Len> {
99    open spec fn nonmal_inv(&self) -> bool {
100        super::AndThen(super::Varied(self.0), self.1).nonmal_inv()
101    }
102
103    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
104        super::AndThen(super::Varied(self.0), self.1).lemma_parse_non_malleable(buf1, buf2);
105    }
106}
107
108impl<Inner, Len> Productive for super::ExactLen<Inner, Len> where Inner: SafeParser, Len: AsLen {
109    open spec fn productive_inv(&self) -> bool {
110        super::AndThen(super::Varied(self.0), self.1).productive_inv()
111    }
112
113    proof fn lemma_productive(&self, s: Seq<u8>) {
114        super::AndThen(super::Varied(self.0), self.1).lemma_productive(s);
115    }
116}
117
118// [`ExactLen`] can make "look-ahead" parsers (e.g., [`Tail`] and [`Eof`]) non-look-ahead
119// (s.t. they can no longer "predict" the future)
120// because it always consumes the same number of bytes when it succeeds
121impl<Inner: SafeParser, Len: AsLen> NoLookAhead for super::ExactLen<Inner, Len> {
122    open spec fn no_lookahead_inv(&self) -> bool {
123        super::AndThen(super::Varied(self.0), self.1).no_lookahead_inv()
124    }
125
126    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
127        super::AndThen(super::Varied(self.0), self.1).lemma_no_lookahead(i1, i2);
128    }
129}
130
131////// [`ExactLen`] can make "context-sensitive" serializers (e.g., [`Tail`] and [`Eof`]) "context-free",
132// [`ExactLen`] can make "position-sensitive" serializers (e.g., [`Tail`] and [`Eof`]) "position-insensitive"
133// (s.t. they can no longer "change" the past)
134// because it "boxes" the inner serializer from the outside context `obuf`
135impl<Inner: EquivSerializers, Len: AsLen> EquivSerializersGeneral for super::ExactLen<Inner, Len> {
136    open spec fn equiv_general_inv(&self) -> bool {
137        super::AndThen(super::Varied(self.0), self.1).equiv_general_inv()
138    }
139
140    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
141        super::AndThen(super::Varied(self.0), self.1).lemma_serialize_equiv(v, obuf);
142    }
143}
144
145impl<Inner: EquivSerializers, Len: AsLen> EquivSerializers for super::ExactLen<Inner, Len> {
146    open spec fn equiv_inv(&self) -> bool {
147        super::AndThen(super::Varied(self.0), self.1).equiv_inv()
148    }
149
150    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
151        super::AndThen(super::Varied(self.0), self.1).lemma_serialize_equiv_on_empty(v);
152    }
153}
154
155impl<Len, Then> SPRoundTripDps for super::AndThen<Varied<Len>, Then> where
156    Then: EquivSerializers + GoodSerializer + SPRoundTrip,
157    Len: AsLen,
158 {
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        let inner_bytes = self.1.spec_serialize_dps(v, seq![]);
167        self.1.lemma_serialize_equiv_on_empty(v);
168        self.1.lemma_serialize_len(v);
169        self.1.theorem_serialize_parse_roundtrip(v);
170        self.0.theorem_serialize_dps_parse_roundtrip(inner_bytes, obuf);
171    }
172}
173
174impl<Then> SPRoundTripDps for super::AndThen<Tail, Then> where
175    Then: EquivSerializers + GoodSerializer + SPRoundTrip,
176 {
177    open spec fn unambiguous(&self) -> bool {
178        &&& self.1.serialize_inv()
179        &&& self.1.equiv_inv()
180        &&& self.1.sp_roundtrip_inv()
181    }
182
183    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
184        let inner_bytes = self.1.spec_serialize_dps(v, seq![]);
185        self.1.lemma_serialize_equiv_on_empty(v);
186        self.1.lemma_serialize_len(v);
187        self.1.theorem_serialize_parse_roundtrip(v);
188        self.0.theorem_serialize_dps_parse_roundtrip(inner_bytes, obuf);
189    }
190}
191
192impl<A, Then> NonMalleable for super::AndThen<A, Then> where
193    A: BytesCombinator + SoundParser + NonMalleable,
194    Then: NonMalleable,
195 {
196    open spec fn nonmal_inv(&self) -> bool {
197        &&& self.0.nonmal_inv()
198        &&& self.0.sound_inv()
199        &&& self.1.nonmal_inv()
200        &&& self.1.safe_inv()
201    }
202
203    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
204        if let Some((n1, v1)) = self.spec_parse(buf1) {
205            if let Some((n2, v2)) = self.spec_parse(buf2) {
206                if v1 == v2 {
207                    let (n1a, chunk1) = self.0.spec_parse(buf1)->0;
208                    let (n2a, chunk2) = self.0.spec_parse(buf2)->0;
209                    let (n1b, v1b) = self.1.spec_parse(chunk1)->0;
210                    let (n2b, v2b) = self.1.spec_parse(chunk2)->0;
211                    self.0.lemma_parse_sound_consumption(buf1);
212                    self.0.lemma_parse_sound_consumption(buf2);
213                    self.0.lemma_byte_len_is_buf_len(chunk1);
214                    self.0.lemma_byte_len_is_buf_len(chunk2);
215                    self.0.lemma_parse_non_malleable(buf1, buf2);
216                    self.1.lemma_parse_non_malleable(chunk1, chunk2);
217                    assert(n1 == n1a && n2 == n2a);
218                    assert(chunk1.take(n1a) == chunk2.take(n2a));
219                    assert(chunk1.take(n1a) == chunk1);
220                    assert(chunk2.take(n2a) == chunk2);
221                    assert(chunk1 == chunk2);
222                    assert(buf1.take(n1a) == buf2.take(n2a));
223                }
224            }
225        }
226    }
227}
228
229impl<A, Then> NoLookAhead for super::AndThen<A, Then> where
230    A: BytesCombinator + NoLookAhead<PVal = Seq<u8>>,
231    Then: SafeParser,
232 {
233    open spec fn no_lookahead_inv(&self) -> bool {
234        self.0.no_lookahead_inv()
235    }
236
237    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
238        if let Some((n, v)) = self.spec_parse(i1) {
239            if 0 <= n <= i2.len() {
240                if i2.take(n) == i1.take(n) {
241                    self.0.lemma_no_lookahead(i1, i2);
242                }
243            }
244        }
245    }
246}
247
248impl<A, Then> Productive for super::AndThen<A, Then> where
249    A: BytesCombinator + Productive<PVal = Seq<u8>>,
250    Then: SafeParser,
251 {
252    open spec fn productive_inv(&self) -> bool {
253        self.0.productive_inv()
254    }
255
256    proof fn lemma_productive(&self, s: Seq<u8>) {
257        self.0.lemma_productive(s);
258    }
259}
260
261impl<A, Then> EquivSerializersGeneral for super::AndThen<A, Then> where
262    A: EquivSerializersGeneral<SVal = Seq<u8>, SValue = Seq<u8>>,
263    Then: EquivSerializers,
264 {
265    open spec fn equiv_general_inv(&self) -> bool {
266        &&& self.0.equiv_general_inv()
267        &&& self.1.equiv_inv()
268    }
269
270    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
271        let inner_bytes = self.1.spec_serialize(v);
272        self.0.lemma_serialize_equiv(inner_bytes, obuf);
273        self.1.lemma_serialize_equiv_on_empty(v);
274    }
275}
276
277impl<A, Then> EquivSerializers for super::AndThen<A, Then> where
278    A: EquivSerializers<SVal = Seq<u8>, SValue = Seq<u8>>,
279    Then: EquivSerializers,
280 {
281    open spec fn equiv_inv(&self) -> bool {
282        &&& self.0.equiv_inv()
283        &&& self.1.equiv_inv()
284    }
285
286    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
287        self.1.lemma_serialize_equiv_on_empty(v);
288        self.0.lemma_serialize_equiv_on_empty(self.1.spec_serialize(v));
289    }
290}
291
292} // verus!
vest_lib/combinators/bytes/proof.rs

vest_lib/combinators/bytes/
proof.rs
