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

vest_lib/combinators/mapped/
proof.rs
