vest_lib/combinators/tuple/
proof.rs

1//! Correctness and ambiguity proofs for sequential composition.
2use crate::combinators::mapped::spec::SpecMap;
3use crate::core::{proof::*, spec::*};
4use vstd::prelude::*;
5
6verus! {
7
8impl<A: SPRoundTripDps + NonTailFmt, B: SPRoundTripDps> SPRoundTripDps for super::Pair<A, B> {
9    open spec fn unambiguous(&self) -> bool {
10        &&& self.0.serialize_dps_inv()
11        &&& self.0.unambiguous()
12        &&& self.1.unambiguous()
13    }
14
15    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
16        let serialized1 = self.1.spec_serialize_dps(v.1, obuf);
17        let serialized0 = self.0.spec_serialize_dps(v.0, serialized1);
18        assert(self.unambiguous());
19        self.1.theorem_serialize_dps_parse_roundtrip(v.1, obuf);
20        self.0.theorem_serialize_dps_parse_roundtrip(v.0, serialized1);
21        self.0.lemma_serialize_dps_prepend(v.0, serialized1);
22        self.0.lemma_serialize_dps_len(v.0, serialized1);
23        if let Some((n0, v0)) = self.0.spec_parse(serialized0) {
24            assert(n0 == serialized0.len() - serialized1.len());
25            assert(serialized0.skip(n0) == serialized1);
26        }
27    }
28}
29
30// impl<A: PSRoundTrip + GoodSerializerDps + EquivSerializersGeneral, B: PSRoundTrip> PSRoundTrip for (
31//     A,
32//     B,
33// ) {
34// }
35impl<A: NonMalleable, B: NonMalleable> NonMalleable for super::Pair<A, B> {
36    open spec fn nonmal_inv(&self) -> bool {
37        &&& self.0.nonmal_inv()
38        &&& self.1.nonmal_inv()
39        &&& self.0.safe_inv()
40        &&& self.1.safe_inv()
41    }
42
43    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
44        if let Some((n1, v1)) = self.spec_parse(buf1) {
45            if let Some((n2, v2)) = self.spec_parse(buf2) {
46                if v1 == v2 {
47                    let (n1a, a1) = self.0.spec_parse(buf1)->0;
48                    let (n2a, a2) = self.0.spec_parse(buf2)->0;
49                    let (n1b, b1) = self.1.spec_parse(buf1.skip(n1a))->0;
50                    let (n2b, b2) = self.1.spec_parse(buf2.skip(n2a))->0;
51                    assert(self.nonmal_inv());
52                    self.0.lemma_parse_safe(buf1);
53                    self.0.lemma_parse_safe(buf2);
54                    self.1.lemma_parse_safe(buf1.skip(n1a));
55                    self.1.lemma_parse_safe(buf2.skip(n2a));
56                    self.0.lemma_parse_non_malleable(buf1, buf2);
57                    self.1.lemma_parse_non_malleable(buf1.skip(n1a), buf2.skip(n2a));
58                    assert(n1 == n1a + n1b && n2 == n2a + n2b);
59                    assert(buf1.take(n1) == buf2.take(n2)) by {
60                        assert(buf1.take(n1) == buf1.take(n1a) + buf1.skip(n1a).take(n1b));
61                        assert(buf2.take(n2) == buf2.take(n2a) + buf2.skip(n2a).take(n2b));
62                    }
63                }
64            }
65        }
66    }
67}
68
69pub(crate) proof fn lemma_take_skip<T>(s: Seq<T>, n1: int, n2: int)
70    requires
71        0 <= n1,
72        0 <= n2,
73        n1 + n2 <= s.len(),
74    ensures
75        s.take(n1 + n2).skip(n1) == s.skip(n1).take(n2),
76{
77}
78
79impl<A: NoLookAhead, B: NoLookAhead> NoLookAhead for super::Pair<A, B> {
80    open spec fn no_lookahead_inv(&self) -> bool {
81        &&& self.0.no_lookahead_inv()
82        &&& self.1.no_lookahead_inv()
83    }
84
85    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
86        broadcast use vstd::seq_lib::group_seq_properties;
87
88        if let Some((n, v)) = self.spec_parse(i1) {
89            if 0 <= n <= i2.len() {
90                if i2.take(n) == i1.take(n) {
91                    if let Some((n1, v1)) = self.0.spec_parse(i1) {
92                        if let Some((n2, v2)) = self.1.spec_parse(i1.skip(n1)) {
93                            assert(self.no_lookahead_inv());
94                            self.lemma_parse_safe(i1);
95                            self.0.lemma_parse_safe(i1);
96                            self.1.lemma_parse_safe(i1.skip(n1));
97                            assert(i2.take(n1) == i1.take(n1));
98                            self.0.lemma_no_lookahead(i1, i2);
99                            assert(i2.skip(n1).take(n2) == i1.skip(n1).take(n2)) by {
100                                lemma_take_skip(i1, n1, n2);
101                                lemma_take_skip(i2, n1, n2);
102                            };
103                            self.1.lemma_no_lookahead(i1.skip(n1), i2.skip(n1));
104                        }
105                    }
106                }
107            }
108        }
109    }
110}
111
112impl<A: Productive, B: Productive> Productive for super::Pair<A, B> {
113    open spec fn productive_inv(&self) -> bool {
114        ||| self.0.productive_inv()
115        ||| self.1.productive_inv()
116    }
117
118    proof fn lemma_productive(&self, s: Seq<u8>) {
119        if let Some((n, _v)) = self.spec_parse(s) {
120            let (n1, _v1) = self.0.spec_parse(s)->0;
121            let (n2, _v2) = self.1.spec_parse(s.skip(n1))->0;
122            self.0.lemma_parse_safe(s);
123            self.1.lemma_parse_safe(s.skip(n1));
124            if self.0.productive_inv() {
125                self.0.lemma_productive(s);
126            } else {
127                self.1.lemma_productive(s.skip(n1));
128            }
129        }
130    }
131}
132
133impl<A, B> EquivSerializersGeneral for super::Pair<A, B> where
134    A: EquivSerializersGeneral,
135    B: EquivSerializersGeneral,
136 {
137    open spec fn equiv_general_inv(&self) -> bool {
138        &&& self.0.equiv_general_inv()
139        &&& self.1.equiv_general_inv()
140    }
141
142    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
143        let obuf1 = self.1.spec_serialize_dps(v.1, obuf);
144        assert(self.equiv_general_inv());
145
146        self.1.lemma_serialize_equiv(v.1, obuf);
147        self.0.lemma_serialize_equiv(v.0, obuf1);
148
149        // From self.1.lemma_serialize_equiv:
150        // self.1.spec_serialize_dps(v.1, obuf) == self.1.spec_serialize(v.1) + obuf
151        // So: obuf1 == self.1.spec_serialize(v.1) + obuf
152
153        // From self.0.lemma_serialize_equiv:
154        // self.0.spec_serialize_dps(v.0, obuf1) == self.0.spec_serialize(v.0) + obuf1
155
156        // Therefore:
157        // spec_serialize_dps(v, obuf) = self.0.spec_serialize_dps(v.0, obuf1)
158        //                              = self.0.spec_serialize(v.0) + obuf1
159        //                              = self.0.spec_serialize(v.0) + self.1.spec_serialize(v.1) + obuf
160        //                              = spec_serialize(v) + obuf
161    }
162}
163
164impl<A, B> EquivSerializers for super::Pair<A, B> where
165    A: EquivSerializersGeneral,
166    B: EquivSerializers,
167 {
168    open spec fn equiv_inv(&self) -> bool {
169        &&& self.0.equiv_general_inv()
170        &&& self.1.equiv_inv()
171    }
172
173    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
174        let empty = Seq::empty();
175        let obuf = self.1.spec_serialize_dps(v.1, empty);
176        assert(self.equiv_inv());
177        self.1.lemma_serialize_equiv_on_empty(v.1);
178        self.0.lemma_serialize_equiv(v.0, obuf);
179    }
180}
181
182impl<A, B> SPRoundTripDps for super::Bind<A, B> where
183    A: SPRoundTripDps + NonTailFmt,
184    B: SpecMap<Input = A::T>,
185    B::Output: SPRoundTripDps,
186 {
187    open spec fn unambiguous(&self) -> bool {
188        &&& self.0.serialize_dps_inv()
189        &&& self.0.unambiguous()
190        &&& forall|key: A::T| #[trigger] self.1.spec_map(key).unambiguous()
191    }
192
193    proof fn theorem_serialize_dps_parse_roundtrip(&self, value: Self::T, obuf: Seq<u8>) {
194        let (key, val) = value;
195        let next = self.1.spec_map(key);
196        let next_buf = next.spec_serialize_dps(val, obuf);
197        let serialized = self.0.spec_serialize_dps(key, next_buf);
198        assert(self.unambiguous());
199        next.theorem_serialize_dps_parse_roundtrip(val, obuf);
200        self.0.theorem_serialize_dps_parse_roundtrip(key, next_buf);
201        self.0.lemma_serialize_dps_prepend(key, next_buf);
202        self.0.lemma_serialize_dps_len(key, next_buf);
203        if let Some((n0, _)) = self.0.spec_parse(serialized) {
204            assert(n0 == serialized.len() - next_buf.len());
205            assert(serialized.skip(n0) == next_buf);
206        }
207    }
208}
209
210impl<A, B> NoLookAhead for super::Bind<A, B> where
211    A: NoLookAhead,
212    B: SpecMap<Input = A::PVal>,
213    B::Output: NoLookAhead,
214 {
215    open spec fn no_lookahead_inv(&self) -> bool {
216        &&& self.0.no_lookahead_inv()
217        &&& forall|key: A::PVal| #[trigger] self.1.spec_map(key).no_lookahead_inv()
218    }
219
220    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
221        broadcast use vstd::seq_lib::group_seq_properties;
222
223        use crate::combinators::tuple::proof::lemma_take_skip;
224
225        if let Some((n, v)) = self.spec_parse(i1) {
226            if 0 <= n <= i2.len() {
227                if i2.take(n) == i1.take(n) {
228                    if let Some((n1, key)) = self.0.spec_parse(i1) {
229                        let next = self.1.spec_map(key);
230                        if let Some((n2, _val)) = next.spec_parse(i1.skip(n1)) {
231                            assert(self.no_lookahead_inv());
232                            self.lemma_parse_safe(i1);
233                            self.0.lemma_parse_safe(i1);
234                            next.lemma_parse_safe(i1.skip(n1));
235                            assert(i2.take(n1) == i1.take(n1));
236                            self.0.lemma_no_lookahead(i1, i2);
237                            assert(i2.skip(n1).take(n2) == i1.skip(n1).take(n2)) by {
238                                lemma_take_skip(i1, n1, n2);
239                                lemma_take_skip(i2, n1, n2);
240                            };
241                            next.lemma_no_lookahead(i1.skip(n1), i2.skip(n1));
242                            assert(self.spec_parse(i2) == Some((n, v)));
243                        }
244                    }
245                }
246            }
247        }
248    }
249}
250
251impl<A, B> NonMalleable for super::Bind<A, B> where
252    A: NonMalleable,
253    B: SpecMap<Input = A::PVal>,
254    B::Output: NonMalleable,
255 {
256    open spec fn nonmal_inv(&self) -> bool {
257        &&& self.0.nonmal_inv()
258        &&& self.0.safe_inv()
259        &&& forall|key: A::PVal| #[trigger] self.1.spec_map(key).nonmal_inv()
260        &&& forall|key: A::PVal| #[trigger] self.1.spec_map(key).safe_inv()
261    }
262
263    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
264        if let Some((n1, v1)) = self.spec_parse(buf1) {
265            if let Some((n2, v2)) = self.spec_parse(buf2) {
266                if v1 == v2 {
267                    assert(self.nonmal_inv());
268                    let (n1a, key1) = self.0.spec_parse(buf1)->0;
269                    let (n2a, key2) = self.0.spec_parse(buf2)->0;
270                    let next1 = self.1.spec_map(key1);
271                    let next2 = self.1.spec_map(key2);
272                    let (n1b, _val) = next1.spec_parse(buf1.skip(n1a))->0;
273                    let (n2b, _val) = next2.spec_parse(buf2.skip(n2a))->0;
274                    assert(key1 == key2 && next1 == next2);
275                    let next = next1;
276                    self.0.lemma_parse_safe(buf1);
277                    self.0.lemma_parse_safe(buf2);
278                    next.lemma_parse_safe(buf1.skip(n1a));
279                    next.lemma_parse_safe(buf2.skip(n2a));
280                    self.0.lemma_parse_non_malleable(buf1, buf2);
281                    next.lemma_parse_non_malleable(buf1.skip(n1a), buf2.skip(n2a));
282                    assert(n1 == n1a + n1b && n2 == n2a + n2b);
283                    assert(buf1.take(n1) == buf2.take(n2)) by {
284                        assert(buf1.take(n1) == buf1.take(n1a) + buf1.skip(n1a).take(n1b));
285                        assert(buf2.take(n2) == buf2.take(n2a) + buf2.skip(n2a).take(n2b));
286                    }
287                }
288            }
289        }
290    }
291}
292
293impl<A, B> Productive for super::Bind<A, B> where
294    A: Productive,
295    B: SpecMap<Input = A::PVal>,
296    B::Output: Productive,
297 {
298    open spec fn productive_inv(&self) -> bool {
299        ||| self.0.productive_inv()
300        ||| forall|key: A::PVal| #[trigger] self.1.spec_map(key).productive_inv()
301    }
302
303    proof fn lemma_productive(&self, s: Seq<u8>) {
304        if let Some((n, v)) = self.spec_parse(s) {
305            let (n1, key) = self.0.spec_parse(s)->0;
306            let next = self.1.spec_map(key);
307            let (n2, _val) = next.spec_parse(s.skip(n1))->0;
308            self.0.lemma_parse_safe(s);
309            next.lemma_parse_safe(s.skip(n1));
310            if self.0.productive_inv() {
311                self.0.lemma_productive(s);
312            } else {
313                next.lemma_productive(s.skip(n1));
314            }
315        }
316    }
317}
318
319impl<A, B> EquivSerializersGeneral for super::Bind<A, B> where
320    A: EquivSerializersGeneral,
321    B: SpecMap<Input = A::SVal>,
322    B::Output: EquivSerializersGeneral,
323 {
324    open spec fn equiv_general_inv(&self) -> bool {
325        &&& self.0.equiv_general_inv()
326        &&& forall|key: A::SVal| #[trigger] self.1.spec_map(key).equiv_general_inv()
327    }
328
329    proof fn lemma_serialize_equiv(&self, value: Self::SVal, obuf: Seq<u8>) {
330        let (key, val) = value;
331        let next = self.1.spec_map(key);
332        let obuf1 = next.spec_serialize_dps(val, obuf);
333        assert(self.equiv_general_inv());
334        next.lemma_serialize_equiv(val, obuf);
335        self.0.lemma_serialize_equiv(key, obuf1);
336    }
337}
338
339impl<A, B> EquivSerializers for super::Bind<A, B> where
340    A: EquivSerializersGeneral,
341    B: SpecMap<Input = A::SVal>,
342    B::Output: EquivSerializers,
343 {
344    open spec fn equiv_inv(&self) -> bool {
345        &&& self.0.equiv_general_inv()
346        &&& forall|key: A::SVal| #[trigger] self.1.spec_map(key).equiv_inv()
347    }
348
349    proof fn lemma_serialize_equiv_on_empty(&self, value: Self::SVal) {
350        let (key, val) = value;
351        let next = self.1.spec_map(key);
352        let empty = Seq::empty();
353        let obuf = next.spec_serialize_dps(val, empty);
354        assert(self.equiv_inv());
355        next.lemma_serialize_equiv_on_empty(val);
356        self.0.lemma_serialize_equiv(key, obuf);
357    }
358}
359
360} // verus!
vest_lib/combinators/tuple/proof.rs

vest_lib/combinators/tuple/
proof.rs
