vest_lib/combinators/refined/
proof.rs

1//! Correctness proofs for predicates, refinements, and constants.
2use super::spec::*;
3use crate::combinators::Fixed;
4use crate::core::{proof::*, spec::*};
5use vstd::prelude::*;
6
7verus! {
8
9impl<A, Pred> SPRoundTripDps for super::Refined<A, Pred> where
10    A: SPRoundTripDps,
11    Pred: SpecPred<A::PVal>,
12 {
13    open spec fn unambiguous(&self) -> bool {
14        self.0.unambiguous()
15    }
16
17    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
18        self.0.theorem_serialize_dps_parse_roundtrip(v, obuf)
19    }
20}
21
22// impl<A: PSRoundTrip, Pred: SpecPred<A::PVal>> PSRoundTrip for super::Refined<A, Pred> {
23//     proof fn theorem_parse_serialize_roundtrip(&self, ibuf: Seq<u8>) {
24//         self.0.theorem_parse_serialize_roundtrip(ibuf);
25//     }
26// }
27impl<A: NonMalleable, Pred: SpecPred<A::PVal>> NonMalleable for super::Refined<A, Pred> {
28    open spec fn nonmal_inv(&self) -> bool {
29        self.0.nonmal_inv()
30    }
31
32    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
33        self.0.lemma_parse_non_malleable(buf1, buf2);
34    }
35}
36
37impl<A: NoLookAhead, Pred: SpecPred<A::PVal>> NoLookAhead for super::Refined<A, Pred> {
38    open spec fn no_lookahead_inv(&self) -> bool {
39        self.0.no_lookahead_inv()
40    }
41
42    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
43        if let Some((n, v)) = self.spec_parse(i1) {
44            if 0 <= n <= i2.len() {
45                if i2.take(n) == i1.take(n) {
46                    assert(self.no_lookahead_inv());
47                    self.0.lemma_no_lookahead(i1, i2);
48                    assert(self.0.spec_parse(i2) == Some((n, v)));
49                    assert(self.spec_parse(i2) == Some((n, v)));
50                }
51            }
52        }
53    }
54}
55
56impl<A: Productive, Pred: SpecPred<A::PVal>> Productive for super::Refined<A, Pred> {
57    open spec fn productive_inv(&self) -> bool {
58        self.0.productive_inv()
59    }
60
61    proof fn lemma_productive(&self, s: Seq<u8>) {
62        self.0.lemma_productive(s);
63    }
64}
65
66impl<A, Pred> EquivSerializersGeneral for super::Refined<A, Pred> where
67    A: EquivSerializersGeneral,
68    Pred: SpecPred<A::SVal>,
69 {
70    open spec fn equiv_general_inv(&self) -> bool {
71        self.0.equiv_general_inv()
72    }
73
74    proof fn lemma_serialize_equiv(&self, v: Self::SValue, obuf: Seq<u8>) {
75        self.0.lemma_serialize_equiv(v, obuf);
76    }
77}
78
79impl<A, Pred> EquivSerializers for super::Refined<A, Pred> where
80    A: EquivSerializers,
81    Pred: SpecPred<A::SVal>,
82 {
83    open spec fn equiv_inv(&self) -> bool {
84        self.0.equiv_inv()
85    }
86
87    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SValue) {
88        self.0.lemma_serialize_equiv_on_empty(v);
89    }
90}
91
92impl<Inner: SPRoundTripDps> SPRoundTripDps for super::Const<Inner, Inner::PVal> {
93    open spec fn unambiguous(&self) -> bool {
94        self.0.unambiguous()
95    }
96
97    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::SValue, obuf: Seq<u8>) {
98        assert(v == self.1);
99        self.0.theorem_serialize_dps_parse_roundtrip(v, obuf);
100    }
101}
102
103// impl<Inner: PSRoundTrip> PSRoundTrip for super::Const<Inner, Inner::PVal> {
104//     proof fn theorem_parse_serialize_roundtrip(&self, ibuf: Seq<u8>) {
105//         self.0.theorem_parse_serialize_roundtrip(ibuf);
106//     }
107// }
108impl<Inner: NonMalleable> NonMalleable for super::Const<Inner, Inner::PVal> {
109    open spec fn nonmal_inv(&self) -> bool {
110        self.0.nonmal_inv()
111    }
112
113    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
114        self.0.lemma_parse_non_malleable(buf1, buf2);
115    }
116}
117
118impl<Inner: NoLookAhead> NoLookAhead for super::Const<Inner, Inner::PVal> {
119    open spec fn no_lookahead_inv(&self) -> bool {
120        self.0.no_lookahead_inv()
121    }
122
123    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
124        if let Some((n, v)) = self.spec_parse(i1) {
125            if 0 <= n <= i2.len() {
126                if i2.take(n) == i1.take(n) {
127                    self.0.lemma_no_lookahead(i1, i2);
128                }
129            }
130        }
131    }
132}
133
134impl<Inner: Productive> Productive for super::Const<Inner, Inner::PVal> {
135    open spec fn productive_inv(&self) -> bool {
136        self.0.productive_inv()
137    }
138
139    proof fn lemma_productive(&self, s: Seq<u8>) {
140        self.0.lemma_productive(s);
141    }
142}
143
144impl<Inner> EquivSerializersGeneral for super::Const<Inner, Inner::SVal> where
145    Inner: EquivSerializersGeneral,
146 {
147    open spec fn equiv_general_inv(&self) -> bool {
148        self.0.equiv_general_inv()
149    }
150
151    proof fn lemma_serialize_equiv(&self, v: Self::SValue, obuf: Seq<u8>) {
152        self.0.lemma_serialize_equiv(v, obuf);
153    }
154}
155
156impl<Inner> EquivSerializers for super::Const<Inner, Inner::SVal> where Inner: EquivSerializers {
157    open spec fn equiv_inv(&self) -> bool {
158        self.0.equiv_inv()
159    }
160
161    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SValue) {
162        self.0.lemma_serialize_equiv_on_empty(v);
163    }
164}
165
166impl<const N: usize> SPRoundTripDps for super::Const<Fixed::<N>, [u8; N]> {
167    open spec fn unambiguous(&self) -> bool {
168        self.0.unambiguous()
169    }
170
171    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::SValue, obuf: Seq<u8>) {
172        self.0.theorem_serialize_dps_parse_roundtrip(v, obuf);
173    }
174}
175
176impl<const N: usize> NonMalleable for super::Const<Fixed::<N>, [u8; N]> {
177    open spec fn nonmal_inv(&self) -> bool {
178        self.0.nonmal_inv()
179    }
180
181    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
182        self.0.lemma_parse_non_malleable(buf1, buf2);
183    }
184}
185
186impl<const N: usize> NoLookAhead for super::Const<Fixed::<N>, [u8; N]> {
187    open spec fn no_lookahead_inv(&self) -> bool {
188        self.0.no_lookahead_inv()
189    }
190
191    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
192        if let Some((n, v)) = self.spec_parse(i1) {
193            if 0 <= n <= i2.len() {
194                if i2.take(n) == i1.take(n) {
195                    self.0.lemma_no_lookahead(i1, i2);
196                }
197            }
198        }
199    }
200}
201
202impl<const N: usize> Productive for super::Const<Fixed::<N>, [u8; N]> {
203    open spec fn productive_inv(&self) -> bool {
204        self.0.productive_inv()
205    }
206
207    proof fn lemma_productive(&self, s: Seq<u8>) {
208        self.0.lemma_productive(s);
209    }
210}
211
212impl<const N: usize> EquivSerializersGeneral for super::Const<Fixed::<N>, [u8; N]> {
213    open spec fn equiv_general_inv(&self) -> bool {
214        self.0.equiv_general_inv()
215    }
216
217    proof fn lemma_serialize_equiv(&self, v: Self::SValue, obuf: Seq<u8>) {
218        self.0.lemma_serialize_equiv(v, obuf);
219    }
220}
221
222impl<const N: usize> EquivSerializers for super::Const<Fixed::<N>, [u8; N]> {
223    open spec fn equiv_inv(&self) -> bool {
224        self.0.equiv_inv()
225    }
226
227    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SValue) {
228        self.0.lemma_serialize_equiv_on_empty(v);
229    }
230}
231
232impl<Tg, Of> SPRoundTripDps for super::PrefixTagged<Tg, Tg::T, Of> where
233    Tg: SpecByteLen + SPRoundTripDps + NonTailFmt,
234    Of: SPRoundTripDps,
235 {
236    open spec fn unambiguous(&self) -> bool {
237        with_prefix_tag(self.0, self.1, self.2).unambiguous()
238    }
239
240    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
241        with_prefix_tag(self.0, self.1, self.2).theorem_serialize_dps_parse_roundtrip(v, obuf);
242    }
243}
244
245impl<Tg, Of> NonMalleable for super::PrefixTagged<Tg, Tg::T, Of> where
246    Tg: SpecByteLen + SoundParser + NonMalleable,
247    Of: SoundParser + NonMalleable,
248 {
249    open spec fn nonmal_inv(&self) -> bool {
250        with_prefix_tag(self.0, self.1, self.2).nonmal_inv()
251    }
252
253    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
254        with_prefix_tag(self.0, self.1, self.2).lemma_parse_non_malleable(buf1, buf2);
255    }
256}
257
258impl<Tg, Of> NoLookAhead for super::PrefixTagged<Tg, Tg::T, Of> where
259    Tg: SpecByteLen + NoLookAhead<PVal = Tg::T>,
260    Of: NoLookAhead,
261 {
262    open spec fn no_lookahead_inv(&self) -> bool {
263        with_prefix_tag(self.0, self.1, self.2).no_lookahead_inv()
264    }
265
266    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
267        with_prefix_tag(self.0, self.1, self.2).lemma_no_lookahead(i1, i2);
268    }
269}
270
271impl<Tg, Of> Productive for super::PrefixTagged<Tg, Tg::T, Of> where
272    Tg: SpecByteLen + Productive<PVal = Tg::T>,
273    Of: Productive,
274 {
275    open spec fn productive_inv(&self) -> bool {
276        with_prefix_tag(self.0, self.1, self.2).productive_inv()
277    }
278
279    proof fn lemma_productive(&self, s: Seq<u8>) {
280        with_prefix_tag(self.0, self.1, self.2).lemma_productive(s);
281    }
282}
283
284impl<Tg, Of> EquivSerializersGeneral for super::PrefixTagged<Tg, Tg::T, Of> where
285    Tg: SpecByteLen + EquivSerializersGeneral<SVal = Tg::T, SValue = Tg::T> + Consistency<
286        Val = Tg::T,
287    >,
288    Of: EquivSerializersGeneral,
289 {
290    open spec fn equiv_general_inv(&self) -> bool {
291        with_prefix_tag(self.0, self.1, self.2).equiv_general_inv()
292    }
293
294    proof fn lemma_serialize_equiv(&self, v: Self::SValue, obuf: Seq<u8>) {
295        with_prefix_tag(self.0, self.1, self.2).lemma_serialize_equiv(v, obuf);
296    }
297}
298
299impl<Tg, Of> EquivSerializers for super::PrefixTagged<Tg, Tg::T, Of> where
300    Tg: SpecByteLen + EquivSerializersGeneral<SVal = Tg::T, SValue = Tg::T> + Consistency<
301        Val = Tg::T,
302    >,
303    Of: EquivSerializers,
304 {
305    open spec fn equiv_inv(&self) -> bool {
306        with_prefix_tag(self.0, self.1, self.2).equiv_inv()
307    }
308
309    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SValue) {
310        with_prefix_tag(self.0, self.1, self.2).lemma_serialize_equiv_on_empty(v);
311    }
312}
313
314impl<Of, Tg> SPRoundTripDps for super::SuffixTagged<Of, Tg, Tg::T> where
315    Tg: SpecByteLen + SPRoundTripDps,
316    Of: SPRoundTripDps + NonTailFmt,
317 {
318    open spec fn unambiguous(&self) -> bool {
319        with_suffix_tag(self.1, self.2, self.0).unambiguous()
320    }
321
322    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
323        with_suffix_tag(self.1, self.2, self.0).theorem_serialize_dps_parse_roundtrip(v, obuf);
324    }
325}
326
327impl<Of, Tg> NonMalleable for super::SuffixTagged<Of, Tg, Tg::T> where
328    Tg: SpecByteLen + SoundParser + NonMalleable,
329    Of: SoundParser + NonMalleable,
330 {
331    open spec fn nonmal_inv(&self) -> bool {
332        with_suffix_tag(self.1, self.2, self.0).nonmal_inv()
333    }
334
335    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
336        with_suffix_tag(self.1, self.2, self.0).lemma_parse_non_malleable(buf1, buf2);
337    }
338}
339
340impl<Of, Tg> NoLookAhead for super::SuffixTagged<Of, Tg, Tg::T> where
341    Tg: SpecByteLen + NoLookAhead<PVal = Tg::T>,
342    Of: NoLookAhead,
343 {
344    open spec fn no_lookahead_inv(&self) -> bool {
345        with_suffix_tag(self.1, self.2, self.0).no_lookahead_inv()
346    }
347
348    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
349        with_suffix_tag(self.1, self.2, self.0).lemma_no_lookahead(i1, i2);
350    }
351}
352
353impl<Of, Tg> Productive for super::SuffixTagged<Of, Tg, Tg::T> where
354    Tg: SpecByteLen + Productive<PVal = Tg::T>,
355    Of: Productive,
356 {
357    open spec fn productive_inv(&self) -> bool {
358        with_suffix_tag(self.1, self.2, self.0).productive_inv()
359    }
360
361    proof fn lemma_productive(&self, s: Seq<u8>) {
362        with_suffix_tag(self.1, self.2, self.0).lemma_productive(s);
363    }
364}
365
366impl<Of, Tg> EquivSerializersGeneral for super::SuffixTagged<Of, Tg, Tg::T> where
367    Tg: SpecByteLen + EquivSerializersGeneral<SVal = Tg::T, SValue = Tg::T> + Consistency<
368        Val = Tg::T,
369    >,
370    Of: EquivSerializersGeneral,
371 {
372    open spec fn equiv_general_inv(&self) -> bool {
373        with_suffix_tag(self.1, self.2, self.0).equiv_general_inv()
374    }
375
376    proof fn lemma_serialize_equiv(&self, v: Self::SValue, obuf: Seq<u8>) {
377        with_suffix_tag(self.1, self.2, self.0).lemma_serialize_equiv(v, obuf);
378    }
379}
380
381impl<Of, Tg> EquivSerializers for super::SuffixTagged<Of, Tg, Tg::T> where
382    Tg: SpecByteLen + EquivSerializers<SVal = Tg::T, SValue = Tg::T> + Consistency<Val = Tg::T>,
383    Of: EquivSerializersGeneral,
384 {
385    open spec fn equiv_inv(&self) -> bool {
386        with_suffix_tag(self.1, self.2, self.0).equiv_inv()
387    }
388
389    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SValue) {
390        with_suffix_tag(self.1, self.2, self.0).lemma_serialize_equiv_on_empty(v);
391    }
392}
393
394} // verus!
vest_lib/combinators/refined/proof.rs

vest_lib/combinators/refined/
proof.rs
