vest_lib/combinators/mapped/
proof.rs

1//! Correctness proofs for total and partial semantic mappings.
2use super::spec::*;
3use crate::core::{proof::*, spec::*};
4use vstd::prelude::*;
5
6verus! {
7
8impl<Inner, M> SPRoundTripDps for super::Mapped<Inner, M> where
9    Inner: SPRoundTripDps,
10    M: LossyMapper<In = Inner::T>,
11 {
12    open spec fn unambiguous(&self) -> bool {
13        self.inner.unambiguous()
14    }
15
16    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
17        let inner_v = self.mapper.spec_map_rev(v);
18        self.inner.theorem_serialize_dps_parse_roundtrip(inner_v, obuf);
19        assert(self.mapper.wf_out(v));
20        self.mapper.lemma_sound_mapper(v);
21    }
22}
23
24impl<Inner, M> NonMalleable for super::Mapped<Inner, M> where
25    Inner: SoundParser + NonMalleable,
26    M: LosslessMapper<In = Inner::PVal>,
27 {
28    open spec fn nonmal_inv(&self) -> bool {
29        &&& self.inner.nonmal_inv()
30        &&& self.inner.sound_inv()
31        &&& forall|v: Inner::T| #![auto] self.inner.consistent(v) ==> self.mapper.wf_in(v)
32    }
33
34    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
35        if let Some((n1, v1)) = self.spec_parse(buf1) {
36            if let Some((n2, v2)) = self.spec_parse(buf2) {
37                if v1 == v2 {
38                    let (i_n1, i_v1) = self.inner.spec_parse(buf1)->0;
39                    let (i_n2, i_v2) = self.inner.spec_parse(buf2)->0;
40                    self.inner.lemma_parse_sound_value(buf1);
41                    self.inner.lemma_parse_sound_value(buf2);
42                    assert(self.mapper.wf_in(i_v1));
43                    assert(self.mapper.wf_in(i_v2));
44                    self.mapper.lemma_lossless_mapper(i_v1);
45                    self.mapper.lemma_lossless_mapper(i_v2);
46                    self.inner.lemma_parse_non_malleable(buf1, buf2);
47                }
48            }
49        }
50    }
51}
52
53impl<Inner, M> NoLookAhead for super::Mapped<Inner, M> where
54    Inner: NoLookAhead,
55    M: SpecMapper<In = Inner::PVal>,
56 {
57    open spec fn no_lookahead_inv(&self) -> bool {
58        self.inner.no_lookahead_inv()
59    }
60
61    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
62        if let Some((n, v)) = self.spec_parse(i1) {
63            if 0 <= n <= i2.len() {
64                if i2.take(n) == i1.take(n) {
65                    assert(self.safe_inv());
66                    assert(self.no_lookahead_inv());
67                    self.inner.lemma_no_lookahead(i1, i2);
68                }
69            }
70        }
71    }
72}
73
74impl<Inner, M> Productive for super::Mapped<Inner, M> where
75    Inner: Productive,
76    M: SpecMapper<In = Inner::PVal>,
77 {
78    open spec fn productive_inv(&self) -> bool {
79        self.inner.productive_inv()
80    }
81
82    proof fn lemma_productive(&self, s: Seq<u8>) {
83        self.inner.lemma_productive(s);
84    }
85}
86
87impl<Inner, M> EquivSerializersGeneral for super::Mapped<Inner, M> where
88    Inner: EquivSerializersGeneral,
89    M: SpecMapper<In = Inner::SVal>,
90 {
91    open spec fn equiv_general_inv(&self) -> bool {
92        self.inner.equiv_general_inv()
93    }
94
95    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
96        let inner_v = self.mapper.spec_map_rev(v);
97        self.inner.lemma_serialize_equiv(inner_v, obuf);
98    }
99}
100
101impl<Inner, M> EquivSerializers for super::Mapped<Inner, M> where
102    Inner: EquivSerializers,
103    M: SpecMapper<In = Inner::SVal>,
104 {
105    open spec fn equiv_inv(&self) -> bool {
106        self.inner.equiv_inv()
107    }
108
109    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
110        let inner_v = self.mapper.spec_map_rev(v);
111        self.inner.lemma_serialize_equiv_on_empty(inner_v);
112    }
113}
114
115/*
116 * Support for plain spec closures as mappers
117 */
118
119impl<Inner: SPRoundTripDps, Out> SPRoundTripDps for super::Mapped<
120    Inner,
121    FnSpecMapper<Inner::T, Out>,
122> {
123    open spec fn unambiguous(&self) -> bool {
124        &&& self.inner.unambiguous()
125        &&& forall|o: Out| #[trigger]
126            self.consistent(o) ==> (self.mapper.0)((self.mapper.1)(o)) == o
127    }
128
129    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
130        let inner_v = self.mapper.1(v);
131        self.inner.theorem_serialize_dps_parse_roundtrip(inner_v, obuf);
132    }
133}
134
135impl<Inner, Out> NonMalleable for super::Mapped<Inner, FnSpecMapper<Inner::PVal, Out>> where
136    Inner: SoundParser + NonMalleable,
137 {
138    open spec fn nonmal_inv(&self) -> bool {
139        &&& self.inner.nonmal_inv()
140        &&& self.inner.sound_inv()
141        &&& forall|v: Inner::PVal| #[trigger]
142            self.inner.consistent(v) ==> (self.mapper.1)((self.mapper.0)(v)) == v
143    }
144
145    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
146        if let Some((n1, v1)) = self.spec_parse(buf1) {
147            if let Some((n2, v2)) = self.spec_parse(buf2) {
148                if v1 == v2 {
149                    let (i_n1, i_v1) = self.inner.spec_parse(buf1)->0;
150                    let (i_n2, i_v2) = self.inner.spec_parse(buf2)->0;
151                    self.inner.lemma_parse_sound_value(buf1);
152                    self.inner.lemma_parse_sound_value(buf2);
153                    self.inner.lemma_parse_non_malleable(buf1, buf2);
154                }
155            }
156        }
157    }
158}
159
160/*
161 * Support for [`BiMap`] that can be used for both spec mappers and exec mappers.
162 */
163
164impl<Inner, M, MRev> SPRoundTripDps for super::Mapped<Inner, BiMap<M, MRev>> where
165    Inner: SPRoundTripDps,
166    M: SpecMap<Input = Inner::T>,
167    MRev: SpecMap<Input = M::Output, Output = M::Input>,
168 {
169    open spec fn unambiguous(&self) -> bool {
170        &&& self.inner.unambiguous()
171        &&& forall|o: M::Output| #![auto] self.consistent(o) ==> self.mapper.sound(o)
172    }
173
174    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
175        assert(self.unambiguous());
176        assert(self.mapper.sound(v));
177        let inner_v = self.mapper.1.spec_map(v);
178        self.inner.theorem_serialize_dps_parse_roundtrip(inner_v, obuf);
179    }
180}
181
182impl<Inner, M, MRev> NonMalleable for super::Mapped<Inner, BiMap<M, MRev>> where
183    Inner: SoundParser + NonMalleable,
184    M: SpecMap<Input = Inner::PVal>,
185    MRev: SpecMap<Input = M::Output, Output = M::Input>,
186 {
187    open spec fn nonmal_inv(&self) -> bool {
188        &&& self.inner.nonmal_inv()
189        &&& self.inner.sound_inv()
190        &&& forall|i: Inner::T| #![auto] self.inner.consistent(i) ==> self.mapper.lossless(i)
191    }
192
193    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
194        if let Some((n1, v1)) = self.spec_parse(buf1) {
195            if let Some((n2, v2)) = self.spec_parse(buf2) {
196                if v1 == v2 {
197                    let (i_n1, i_v1) = self.inner.spec_parse(buf1)->0;
198                    let (i_n2, i_v2) = self.inner.spec_parse(buf2)->0;
199                    self.inner.lemma_parse_sound_value(buf1);
200                    self.inner.lemma_parse_sound_value(buf2);
201                    self.inner.lemma_parse_non_malleable(buf1, buf2);
202                }
203            }
204        }
205    }
206}
207
208impl<Inner, M, MRev> NoLookAhead for super::Mapped<Inner, BiMap<M, MRev>> where
209    Inner: NoLookAhead,
210    M: SpecMap<Input = Inner::PVal>,
211    MRev: SpecMap<Input = M::Output, Output = M::Input>,
212 {
213    open spec fn no_lookahead_inv(&self) -> bool {
214        self.inner.no_lookahead_inv()
215    }
216
217    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
218        if let Some((n, v)) = self.spec_parse(i1) {
219            if 0 <= n <= i2.len() {
220                if i2.take(n) == i1.take(n) {
221                    assert(self.safe_inv());
222                    assert(self.no_lookahead_inv());
223                    self.inner.lemma_no_lookahead(i1, i2);
224                }
225            }
226        }
227    }
228}
229
230impl<Inner, M, MRev> Productive for super::Mapped<Inner, BiMap<M, MRev>> where
231    Inner: Productive,
232    M: SpecMap<Input = Inner::PVal>,
233    MRev: SpecMap<Input = M::Output, Output = M::Input>,
234 {
235    open spec fn productive_inv(&self) -> bool {
236        self.inner.productive_inv()
237    }
238
239    proof fn lemma_productive(&self, s: Seq<u8>) {
240        self.inner.lemma_productive(s);
241    }
242}
243
244impl<Inner, M, MRev> EquivSerializersGeneral for super::Mapped<Inner, BiMap<M, MRev>> where
245    Inner: EquivSerializersGeneral,
246    M: SpecMap<Input = Inner::SVal>,
247    MRev: SpecMap<Input = M::Output, Output = M::Input>,
248 {
249    open spec fn equiv_general_inv(&self) -> bool {
250        self.inner.equiv_general_inv()
251    }
252
253    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
254        let inner_v = self.mapper.1.spec_map(v);
255        self.inner.lemma_serialize_equiv(inner_v, obuf);
256    }
257}
258
259impl<Inner, M, MRev> EquivSerializers for super::Mapped<Inner, BiMap<M, MRev>> where
260    Inner: EquivSerializers,
261    M: SpecMap<Input = Inner::SVal>,
262    MRev: SpecMap<Input = M::Output, Output = M::Input>,
263 {
264    open spec fn equiv_inv(&self) -> bool {
265        self.inner.equiv_inv()
266    }
267
268    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
269        let inner_v = self.mapper.1.spec_map(v);
270        self.inner.lemma_serialize_equiv_on_empty(inner_v);
271    }
272}
273
274impl<Inner, M> SPRoundTripDps for super::TryMap<Inner, M> where
275    Inner: SPRoundTripDps,
276    M: LossyMapper<In = Inner::T>,
277 {
278    open spec fn unambiguous(&self) -> bool {
279        self.inner().unambiguous()
280    }
281
282    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
283        self.inner().theorem_serialize_dps_parse_roundtrip(v, obuf);
284    }
285}
286
287impl<Inner, M> NonMalleable for super::TryMap<Inner, M> where
288    Inner: SoundParser + NonMalleable,
289    M: LosslessMapper<In = Inner::PVal>,
290 {
291    open spec fn nonmal_inv(&self) -> bool {
292        self.inner().nonmal_inv()
293    }
294
295    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
296        self.inner().lemma_parse_non_malleable(buf1, buf2);
297    }
298}
299
300impl<Inner, M> NoLookAhead for super::TryMap<Inner, M> where
301    Inner: NoLookAhead,
302    M: LossyMapper<In = Inner::PVal>,
303 {
304    open spec fn no_lookahead_inv(&self) -> bool {
305        self.inner().no_lookahead_inv()
306    }
307
308    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
309        assert(self.no_lookahead_inv());
310        self.inner().lemma_no_lookahead(i1, i2);
311    }
312}
313
314impl<Inner, M> Productive for super::TryMap<Inner, M> where
315    Inner: Productive,
316    M: SpecMapper<In = Inner::PVal>,
317 {
318    open spec fn productive_inv(&self) -> bool {
319        self.inner().productive_inv()
320    }
321
322    proof fn lemma_productive(&self, s: Seq<u8>) {
323        self.inner().lemma_productive(s);
324    }
325}
326
327impl<Inner, M> EquivSerializersGeneral for super::TryMap<Inner, M> where
328    Inner: EquivSerializersGeneral,
329    M: SpecMapper<In = Inner::SVal>,
330 {
331    open spec fn equiv_general_inv(&self) -> bool {
332        self.inner().equiv_general_inv()
333    }
334
335    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
336        self.inner().lemma_serialize_equiv(v, obuf);
337    }
338}
339
340impl<Inner, M> EquivSerializers for super::TryMap<Inner, M> where
341    Inner: EquivSerializers,
342    M: SpecMapper<In = Inner::SVal>,
343 {
344    open spec fn equiv_inv(&self) -> bool {
345        self.inner().equiv_inv()
346    }
347
348    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
349        self.inner().lemma_serialize_equiv_on_empty(v);
350    }
351}
352
353} // verus!
vest_lib/combinators/mapped/proof.rs

vest_lib/combinators/mapped/
proof.rs
