vest_lib/combinators/tail/
proof.rs

1//! Correctness proofs for tail-position formats.
2use crate::combinators::Pair;
3use crate::{
4    combinators::{Optional, Repeat},
5    core::{proof::*, spec::*},
6};
7use vstd::prelude::*;
8
9verus! {
10
11impl SPRoundTripDps for super::Tail {
12    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
13    }
14}
15
16// impl PSRoundTrip for super::Tail {
17//     proof fn theorem_parse_serialize_roundtrip(&self, ibuf: Seq<u8>) {
18//     }
19// }
20impl NonMalleable for super::Tail {
21    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
22    }
23}
24
25impl Productive for super::Tail {
26    open spec fn productive_inv(&self) -> bool {
27        false
28    }
29
30    proof fn lemma_productive(&self, s: Seq<u8>) {
31    }
32}
33
34impl EquivSerializers for super::Tail {
35    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
36    }
37}
38
39impl SPRoundTripDps for super::Eof {
40    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
41    }
42}
43
44// impl PSRoundTrip for super::Eof {
45//     proof fn theorem_parse_serialize_roundtrip(&self, ibuf: Seq<u8>) {
46//     }
47// }
48impl NonMalleable for super::Eof {
49    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
50    }
51}
52
53impl Productive for super::Eof {
54    open spec fn productive_inv(&self) -> bool {
55        false
56    }
57
58    proof fn lemma_productive(&self, s: Seq<u8>) {
59    }
60}
61
62impl EquivSerializers for super::Eof {
63    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
64    }
65}
66
67impl<A, B> SPRoundTripDps for super::PairRev<A, B> where
68    A: SPRoundTripDps + NonTailFmt + NoLookAhead,
69    B: StaticByteLen + EquivSerializers + GoodSerializer + SPRoundTrip,
70 {
71    open spec fn unambiguous(&self) -> bool {
72        &&& self.0.serialize_inv()
73        &&& self.0.equiv_inv()
74        &&& self.0.sp_roundtrip_inv()
75        &&& self.1.unambiguous()
76        &&& self.1.serialize_dps_inv()
77        &&& self.1.safe_inv()
78        &&& self.1.no_lookahead_inv()
79    }
80
81    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
82        broadcast use vstd::seq_lib::group_seq_properties;
83
84        let serialized1 = self.0.spec_serialize_dps(v.1, seq![]);
85        let serialized0 = self.1.spec_serialize_dps(v.0, serialized1);
86        let n1 = self.1.byte_len(v.0) as int;
87        let n2 = self.0.byte_len(v.1) as int;
88
89        self.0.lemma_serialize_equiv_on_empty(v.1);
90        self.0.lemma_serialize_len(v.1);
91        self.0.theorem_serialize_parse_roundtrip(v.1);
92        self.0.lemma_static_len_matches_byte_len(v.1);
93
94        self.1.theorem_serialize_dps_parse_roundtrip(v.0, serialized1);
95        self.1.lemma_serialize_dps_prepend(v.0, serialized1);
96        self.1.lemma_serialize_dps_len(v.0, serialized1);
97        assert(serialized0.take(n1).take(n1) == serialized0.take(n1));
98        self.1.lemma_no_lookahead(serialized0, serialized0.take(n1));
99        assert(self.1.spec_parse(serialized0.take(n1)) == Some((n1, v.0)));
100
101        assert(self.0.spec_parse(serialized0.skip(n1)) == Some((n2, v.1)));
102        assert(self.spec_parse(serialized0) == Some((n1 + n2, v)));
103    }
104}
105
106impl<A, B> NonMalleable for super::PairRev<A, B> where
107    A: NonMalleable,
108    B: StaticByteLen + NonMalleable<PVal = B::T>,
109 {
110    open spec fn nonmal_inv(&self) -> bool {
111        &&& self.0.nonmal_inv()
112        &&& self.1.nonmal_inv()
113        &&& self.0.safe_inv()
114        &&& self.1.safe_inv()
115    }
116
117    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
118        if let Some((n1, v1)) = self.spec_parse(buf1) {
119            if let Some((n2, v2)) = self.spec_parse(buf2) {
120                if v1 == v2 {
121                    let prefix1 = buf1.len() - B::static_byte_len();
122                    let prefix2 = buf2.len() - B::static_byte_len();
123                    self.1.lemma_parse_non_malleable(buf1.take(prefix1), buf2.take(prefix2));
124                    self.0.lemma_parse_non_malleable(buf1.skip(prefix1), buf2.skip(prefix2));
125
126                    let (n1b, b1) = self.0.spec_parse(buf1.skip(prefix1))->0;
127                    let (n2b, b2) = self.0.spec_parse(buf2.skip(prefix2))->0;
128                    let (n1a, a1) = self.1.spec_parse(buf1.take(prefix1))->0;
129                    let (n2a, a2) = self.1.spec_parse(buf2.take(prefix2))->0;
130                    assert(prefix1 == n1a && prefix2 == n2a);
131                    assert(n1 == buf1.len() && n2 == buf2.len());
132
133                    self.0.lemma_parse_safe(buf1.skip(prefix1));
134                    self.0.lemma_parse_safe(buf2.skip(prefix2));
135                    self.1.lemma_parse_safe(buf1.take(prefix1));
136                    self.1.lemma_parse_safe(buf2.take(prefix2));
137
138                    assert(buf1.take(n1) == buf2.take(n2)) by {
139                        assert(buf1.take(n1) == buf1.take(n1a) + buf1.skip(n1a).take(n1b));
140                        assert(buf2.take(n2) == buf2.take(n2a) + buf2.skip(n2a).take(n2b));
141                        assert(buf1.take(prefix1).take(n1a) == buf1.take(n1a));
142                        assert(buf2.take(prefix2).take(n2a) == buf2.take(n2a));
143                    }
144                }
145            }
146        }
147    }
148}
149
150impl<A: Productive, B: StaticByteLen + SafeParser<PVal = B::T>> Productive for super::PairRev<
151    A,
152    B,
153> {
154    open spec fn productive_inv(&self) -> bool {
155        B::static_byte_len() > 0 || (self.1.productive_inv() && self.1.safe_inv())
156    }
157
158    proof fn lemma_productive(&self, s: Seq<u8>) {
159        if let Some((n, _v)) = self.spec_parse(s) {
160            let prefix = s.len() - B::static_byte_len();
161            let (n1, _a) = self.1.spec_parse(s.take(prefix))->0;
162            let (n2, _b) = self.0.spec_parse(s.skip(prefix))->0;
163            assert(n == n1 + n2);
164            if B::static_byte_len() > 0 {
165                assert(n2 == B::static_byte_len());
166                assert(n2 > 0);
167            } else {
168                self.1.lemma_productive(s.take(prefix));
169                assert(n1 > 0);
170            }
171            assert(n > 0);
172        }
173    }
174}
175
176impl<A, B> EquivSerializers for super::PairRev<A, B> where
177    A: EquivSerializersGeneral,
178    B: EquivSerializers,
179 {
180    open spec fn equiv_inv(&self) -> bool {
181        Pair(self.1, self.0).equiv_inv()
182    }
183
184    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
185        Pair(self.1, self.0).lemma_serialize_equiv_on_empty((v.0, v.1));
186    }
187}
188
189impl<C: SPRoundTripDps + NonTailFmt + Productive> SPRoundTripDps for super::OptionalEnd<C> {
190    open spec fn unambiguous(&self) -> bool {
191        &&& self.0.serialize_dps_inv()
192        &&& self.0.unambiguous()
193        &&& self.0.safe_inv()
194        &&& self.0.productive_inv()
195    }
196
197    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
198        broadcast use crate::combinators::disjoint::lemma_disjoint_eof;
199
200        Optional(self.0, super::Eof).theorem_serialize_dps_parse_roundtrip((v, ()), obuf);
201    }
202}
203
204impl<C: NonMalleable + SafeParser> NonMalleable for super::OptionalEnd<C> {
205    open spec fn nonmal_inv(&self) -> bool {
206        Optional(self.0, super::Eof).nonmal_inv()
207    }
208
209    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
210        Optional(self.0, super::Eof).lemma_parse_non_malleable(buf1, buf2);
211    }
212}
213
214impl<C: SafeParser> Productive for super::OptionalEnd<C> {
215    open spec fn productive_inv(&self) -> bool {
216        false
217    }
218
219    proof fn lemma_productive(&self, s: Seq<u8>) {
220    }
221}
222
223impl<C: EquivSerializersGeneral> EquivSerializers for super::OptionalEnd<C> {
224    open spec fn equiv_inv(&self) -> bool {
225        self.0.equiv_general_inv()
226    }
227
228    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
229        Optional(self.0, super::Eof).lemma_serialize_equiv_on_empty((v, ()));
230    }
231}
232
233impl<C: SPRoundTripDps + NonTailFmt + Productive> SPRoundTripDps for super::RepeatTillEnd<C> {
234    open spec fn unambiguous(&self) -> bool {
235        &&& self.0.serialize_dps_inv()
236        &&& self.0.unambiguous()
237        &&& self.0.safe_inv()
238        &&& self.0.productive_inv()
239    }
240
241    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
242        broadcast use crate::combinators::disjoint::lemma_disjoint_eof;
243
244        Repeat(self.0, super::Eof).theorem_serialize_dps_parse_roundtrip((v, ()), obuf);
245    }
246}
247
248impl<C: NonMalleable + SafeParser> NonMalleable for super::RepeatTillEnd<C> {
249    open spec fn nonmal_inv(&self) -> bool {
250        Repeat(self.0, super::Eof).nonmal_inv()
251    }
252
253    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
254        Repeat(self.0, super::Eof).lemma_parse_non_malleable(buf1, buf2);
255    }
256}
257
258impl<C: SafeParser> Productive for super::RepeatTillEnd<C> {
259    open spec fn productive_inv(&self) -> bool {
260        false
261    }
262
263    proof fn lemma_productive(&self, s: Seq<u8>) {
264    }
265}
266
267impl<C: EquivSerializersGeneral> EquivSerializers for super::RepeatTillEnd<C> {
268    open spec fn equiv_inv(&self) -> bool {
269        self.0.equiv_general_inv()
270    }
271
272    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
273        Repeat(self.0, super::Eof).lemma_serialize_equiv_on_empty((v, ()));
274    }
275}
276
277} // verus!
vest_lib/combinators/tail/proof.rs

vest_lib/combinators/tail/
proof.rs
