vest_lib/combinators/implicit/
proof.rs

1//! Correctness proofs for dependent formats that omit their header value.
2use crate::core::{proof::*, spec::*};
3use vstd::prelude::*;
4
5verus! {
6
7impl<Head, Tail> SPRoundTripDps for super::Implicit<Head, Tail> where
8    Head: SPRoundTripDps + NonTailFmt,
9    Tail: super::DepCombinator<Key = Head::T>,
10    Tail::Body: SPRoundTripDps<T = Tail::Val>,
11 {
12    open spec fn unambiguous(&self) -> bool {
13        &&& self.0.serialize_dps_inv()
14        &&& self.0.unambiguous()
15        &&& forall|key: Head::T| #[trigger] self.1.apply(key).unambiguous()
16    }
17
18    proof fn theorem_serialize_dps_parse_roundtrip(&self, value: Self::T, obuf: Seq<u8>) {
19        let key = self.1.recover(value);
20        let next = self.1.apply(key);
21        let next_buf = next.spec_serialize_dps(value, obuf);
22        let serialized = self.0.spec_serialize_dps(key, next_buf);
23        assert(self.0.consistent(key) && next.consistent(value));
24        next.theorem_serialize_dps_parse_roundtrip(value, obuf);
25        self.0.theorem_serialize_dps_parse_roundtrip(key, next_buf);
26        self.0.lemma_serialize_dps_prepend(key, next_buf);
27        self.0.lemma_serialize_dps_len(key, next_buf);
28        if let Some((n0, _)) = self.0.spec_parse(serialized) {
29            assert(n0 == serialized.len() - next_buf.len());
30            assert(serialized.skip(n0) == next_buf);
31        }
32    }
33}
34
35impl<Head, Tail> NonMalleable for super::Implicit<Head, Tail> where
36    Head: SoundParser + NonMalleable,
37    Tail: super::DepCombinator<Key = Head::T>,
38    Tail::Body: SoundParser<T = Tail::Val> + NonMalleable,
39 {
40    open spec fn nonmal_inv(&self) -> bool {
41        &&& self.0.nonmal_inv()
42        &&& self.0.sound_inv()
43        &&& forall|key: Head::PVal| #[trigger] self.1.apply(key).nonmal_inv()
44        &&& forall|key: Head::PVal| #[trigger] self.1.apply(key).sound_inv()
45        &&& self.1.recover_inv()
46    }
47
48    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
49        if let Some((n1, v1)) = self.spec_parse(buf1) {
50            if let Some((n2, v2)) = self.spec_parse(buf2) {
51                if v1 == v2 {
52                    assert(self.nonmal_inv());
53                    let (n1a, k1) = self.0.spec_parse(buf1)->0;
54                    let (n2a, k2) = self.0.spec_parse(buf2)->0;
55                    let body1 = self.1.apply(k1);
56                    let body2 = self.1.apply(k2);
57                    let (n1b, v) = body1.spec_parse(buf1.skip(n1a))->0;
58                    let (n2b, v) = body2.spec_parse(buf2.skip(n2a))->0;
59                    self.0.lemma_parse_sound_value(buf1);
60                    self.0.lemma_parse_sound_value(buf2);
61                    body1.lemma_parse_sound_value(buf1.skip(n1a));
62                    body2.lemma_parse_sound_value(buf2.skip(n2a));
63                    self.1.lemma_recover_consistent(k1, v);
64                    self.1.lemma_recover_consistent(k2, v);
65                    assert(k1 == k2 && body1 == body2);
66                    let body = body1;
67                    self.0.lemma_parse_safe(buf1);
68                    self.0.lemma_parse_safe(buf2);
69                    body.lemma_parse_safe(buf1.skip(n1a));
70                    body.lemma_parse_safe(buf2.skip(n2a));
71                    self.0.lemma_parse_non_malleable(buf1, buf2);
72                    body.lemma_parse_non_malleable(buf1.skip(n1a), buf2.skip(n2a));
73                    assert(n1 == n1a + n1b && n2 == n2a + n2b);
74                    assert(buf1.take(n1) == buf2.take(n2)) by {
75                        assert(buf1.take(n1) == buf1.take(n1a) + buf1.skip(n1a).take(n1b));
76                        assert(buf2.take(n2) == buf2.take(n2a) + buf2.skip(n2a).take(n2b));
77                    }
78                }
79            }
80        }
81    }
82}
83
84impl<Head, Tail> NoLookAhead for super::Implicit<Head, Tail> where
85    Head: NoLookAhead,
86    Tail: super::DepCombinator<Key = Head::PVal>,
87    Tail::Body: NoLookAhead<PVal = Tail::Val>,
88 {
89    open spec fn no_lookahead_inv(&self) -> bool {
90        &&& self.0.no_lookahead_inv()
91        &&& forall|key: Head::PVal| #[trigger] self.1.apply(key).no_lookahead_inv()
92    }
93
94    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
95        broadcast use vstd::seq_lib::group_seq_properties;
96
97        use crate::combinators::tuple::proof::lemma_take_skip;
98
99        if let Some((n, v)) = self.spec_parse(i1) {
100            if 0 <= n <= i2.len() {
101                if i2.take(n) == i1.take(n) {
102                    if let Some((n1, key)) = self.0.spec_parse(i1) {
103                        let body = self.1.apply(key);
104                        if let Some((n2, _v2)) = body.spec_parse(i1.skip(n1)) {
105                            self.lemma_parse_safe(i1);
106                            self.0.lemma_parse_safe(i1);
107                            body.lemma_parse_safe(i1.skip(n1));
108                            assert(i2.take(n1) == i1.take(n1));
109                            self.0.lemma_no_lookahead(i1, i2);
110                            assert(i2.skip(n1).take(n2) == i1.skip(n1).take(n2)) by {
111                                lemma_take_skip(i1, n1, n2);
112                                lemma_take_skip(i2, n1, n2);
113                            };
114                            body.lemma_no_lookahead(i1.skip(n1), i2.skip(n1));
115                            assert(self.spec_parse(i2) == Some((n, v)));
116                        }
117                    }
118                }
119            }
120        }
121    }
122}
123
124impl<Head, Tail> Productive for super::Implicit<Head, Tail> where
125    Head: Productive,
126    Tail: super::DepCombinator<Key = Head::PVal>,
127    Tail::Body: Productive<PVal = Tail::Val>,
128 {
129    open spec fn productive_inv(&self) -> bool {
130        ||| self.0.productive_inv()
131        ||| forall|key: Head::PVal| #[trigger] self.1.apply(key).productive_inv()
132    }
133
134    proof fn lemma_productive(&self, s: Seq<u8>) {
135        if let Some((n, v)) = self.spec_parse(s) {
136            let (n1, key) = self.0.spec_parse(s)->0;
137            let next = self.1.apply(key);
138            let (n2, _val) = next.spec_parse(s.skip(n1))->0;
139            self.0.lemma_parse_safe(s);
140            next.lemma_parse_safe(s.skip(n1));
141            if self.0.productive_inv() {
142                self.0.lemma_productive(s);
143            } else {
144                next.lemma_productive(s.skip(n1));
145            }
146        }
147    }
148}
149
150impl<Head, Tail> EquivSerializersGeneral for super::Implicit<Head, Tail> where
151    Head: EquivSerializersGeneral,
152    Tail: super::DepCombinator<Key = Head::SVal>,
153    Tail::Body: EquivSerializersGeneral<SVal = Tail::Val>,
154 {
155    open spec fn equiv_general_inv(&self) -> bool {
156        &&& self.0.equiv_general_inv()
157        &&& forall|key: Head::SVal| #[trigger] self.1.apply(key).equiv_general_inv()
158    }
159
160    proof fn lemma_serialize_equiv(&self, value: Self::SVal, obuf: Seq<u8>) {
161        let key = self.1.recover(value);
162        let next = self.1.apply(key);
163        let obuf1 = next.spec_serialize_dps(value, obuf);
164        next.lemma_serialize_equiv(value, obuf);
165        self.0.lemma_serialize_equiv(key, obuf1);
166    }
167}
168
169impl<Head, Tail> EquivSerializers for super::Implicit<Head, Tail> where
170    Head: EquivSerializersGeneral,
171    Tail: super::DepCombinator<Key = Head::SVal>,
172    Tail::Body: EquivSerializers<SVal = Tail::Val>,
173 {
174    open spec fn equiv_inv(&self) -> bool {
175        &&& self.0.equiv_general_inv()
176        &&& forall|key: Head::SVal| #[trigger] self.1.apply(key).equiv_inv()
177    }
178
179    proof fn lemma_serialize_equiv_on_empty(&self, value: Self::SVal) {
180        let key = self.1.recover(value);
181        let next = self.1.apply(key);
182        let empty = Seq::empty();
183        let obuf = next.spec_serialize_dps(value, empty);
184        next.lemma_serialize_equiv_on_empty(value);
185        self.0.lemma_serialize_equiv(key, obuf);
186    }
187}
188
189} // verus!
vest_lib/combinators/implicit/proof.rs

vest_lib/combinators/implicit/
proof.rs
