vest_lib/combinators/opt/
proof.rs

1//! Correctness and ambiguity proofs for optional formats.
2use crate::{
3    combinators::Pair,
4    core::{proof::*, spec::*},
5};
6use vstd::prelude::*;
7
8verus! {
9
10impl<A: SPRoundTripDps> super::Opt<A> {
11    proof fn lemma_serialize_parse_roundtrip(&self, v: Option<A::T>, obuf: Seq<u8>)
12        requires
13            self.0.unambiguous(),
14            parser_fails_on(self.0, obuf),
15        ensures
16            self.consistent(v) ==> {
17                let ibuf = self.spec_serialize_dps(v, obuf);
18                let n = self.byte_len(v) as int;
19                self.spec_parse(ibuf) == Some((n, v))
20            },
21    {
22        match v {
23            None => {},
24            Some(vv) => {
25                if self.consistent(Some(vv)) {
26                    self.0.theorem_serialize_dps_parse_roundtrip(vv, obuf);
27                }
28            },
29        }
30    }
31}
32
33impl<A: NoLookAhead> super::Opt<A> {
34    proof fn lemma_opt_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>)
35        requires
36            self.0.safe_inv(),
37            self.0.no_lookahead_inv(),
38            parser_fails_on(self.0, i1) ==> parser_fails_on(self.0, i2),
39        ensures
40            self.spec_parse(i1) matches Some((n, v)) ==> 0 <= n <= i2.len() ==> i2.take(n)
41                == i1.take(n) ==> self.spec_parse(i2) == Some((n, v)),
42    {
43        if let Some((n, v)) = self.spec_parse(i1) {
44            if 0 <= n <= i2.len() {
45                if i2.take(n) == i1.take(n) {
46                    if let Some((n0, v0)) = self.0.spec_parse(i1) {
47                        self.0.lemma_no_lookahead(i1, i2);
48                    } else {
49                        assert(self.0.spec_parse(i2) is None);
50                    }
51                }
52            }
53        }
54    }
55}
56
57impl<A: NonMalleable> NonMalleable for super::Opt<A> {
58    open spec fn nonmal_inv(&self) -> bool {
59        self.0.nonmal_inv()
60    }
61
62    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
63        self.0.lemma_parse_non_malleable(buf1, buf2);
64    }
65}
66
67impl<A: SafeParser> Productive for super::Opt<A> {
68    open spec fn productive_inv(&self) -> bool {
69        false
70    }
71
72    proof fn lemma_productive(&self, s: Seq<u8>) {
73    }
74}
75
76impl<A> EquivSerializersGeneral for super::Opt<A> where A: EquivSerializersGeneral {
77    open spec fn equiv_general_inv(&self) -> bool {
78        self.0.equiv_general_inv()
79    }
80
81    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
82        match v {
83            None => {},
84            Some(vv) => {
85                self.0.lemma_serialize_equiv(vv, obuf);
86            },
87        }
88    }
89}
90
91impl<A> EquivSerializers for super::Opt<A> where A: EquivSerializers {
92    open spec fn equiv_inv(&self) -> bool {
93        self.0.equiv_inv()
94    }
95
96    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
97        match v {
98            None => {},
99            Some(vv) => {
100                self.0.lemma_serialize_equiv_on_empty(vv);
101            },
102        }
103    }
104}
105
106impl<A: SPRoundTripDps + NonTailFmt, B: SPRoundTripDps> SPRoundTripDps for super::Optional<A, B> {
107    open spec fn unambiguous(&self) -> bool {
108        &&& self.0.serialize_dps_inv()
109        &&& self.0.unambiguous()
110        &&& self.1.unambiguous()
111        &&& disjoint_domains(self.0, self.1)
112    }
113
114    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
115        let opt = super::Opt(self.0);
116        let serialized1 = self.1.spec_serialize_dps(v.1, obuf);
117        self.1.theorem_serialize_dps_parse_roundtrip(v.1, obuf);
118        assert(parser_fails_on(self.0, serialized1)) by {
119            reveal(disjoint_domains);
120            assert(self.1.spec_parse(serialized1) is Some);
121        }
122        let serialized0 = opt.spec_serialize_dps(v.0, serialized1);
123        opt.lemma_serialize_parse_roundtrip(v.0, serialized1);
124        let n0 = serialized0.len() - serialized1.len();
125        opt.lemma_serialize_dps_prepend(v.0, serialized1);
126        opt.lemma_serialize_dps_len(v.0, serialized1);
127        assert(serialized0.skip(n0) == serialized1);
128    }
129}
130
131// impl<
132//     A: PSRoundTrip + GoodSerializerDps + EquivSerializersGeneral,
133//     B: PSRoundTrip,
134// > PSRoundTrip for super::Optional<A, B> {
135// }
136impl<A: NonMalleable, B: NonMalleable> NonMalleable for super::Optional<A, B> {
137    open spec fn nonmal_inv(&self) -> bool {
138        Pair(super::Opt(self.0), self.1).nonmal_inv()
139    }
140
141    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
142        Pair(super::Opt(self.0), self.1).lemma_parse_non_malleable(buf1, buf2);
143    }
144}
145
146impl<A: NoLookAhead, B: NoLookAhead> NoLookAhead for super::Optional<A, B> {
147    open spec fn no_lookahead_inv(&self) -> bool {
148        &&& self.0.no_lookahead_inv()
149        &&& self.1.no_lookahead_inv()
150        &&& disjoint_domains(self.0, self.1)
151    }
152
153    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
154        reveal(disjoint_domains);
155        broadcast use vstd::seq_lib::group_seq_properties;
156
157        use crate::combinators::tuple::proof::lemma_take_skip;
158
159        let opt = super::Opt(self.0);
160        if let Some((n, v)) = self.spec_parse(i1) {
161            if 0 <= n <= i2.len() {
162                if i2.take(n) == i1.take(n) {
163                    assert(self.safe_inv());
164                    if let Some((n0, a)) = self.0.spec_parse(i1) {
165                        if let Some((n1, b)) = self.1.spec_parse(i1.skip(n0)) {
166                            assert(opt.safe_inv());
167                            assert(self.1.safe_inv());
168                            opt.lemma_parse_safe(i1);
169                            self.1.lemma_parse_safe(i1.skip(n0));
170                            assert(i2.take(n0) == i1.take(n0));
171                            opt.lemma_opt_no_lookahead(i1, i2);
172                            assert(i2.skip(n0).take(n1) == i1.skip(n0).take(n1)) by {
173                                lemma_take_skip(i1, n0, n1);
174                                lemma_take_skip(i2, n0, n1);
175                            };
176                            self.1.lemma_no_lookahead(i1.skip(n0), i2.skip(n0));
177                        }
178                    } else if let Some((n1, b)) = self.1.spec_parse(i1) {
179                        assert(disjoint_domains(self.0, self.1));
180                        assert(self.1.safe_inv());
181                        self.1.lemma_no_lookahead(i1, i2);
182                    }
183                }
184            }
185        }
186    }
187}
188
189impl<A: Productive, B: Productive> Productive for super::Optional<A, B> {
190    open spec fn productive_inv(&self) -> bool {
191        self.1.productive_inv()
192    }
193
194    proof fn lemma_productive(&self, s: Seq<u8>) {
195        if let Some((n, _v)) = self.spec_parse(s) {
196            let (n1, _v1) = super::Opt(self.0).spec_parse(s)->0;
197            let (n2, _v2) = self.1.spec_parse(s.skip(n1))->0;
198            super::Opt(self.0).lemma_parse_safe(s);
199            self.1.lemma_productive(s.skip(n1));
200        }
201    }
202}
203
204impl<
205    A: EquivSerializersGeneral,
206    B: EquivSerializersGeneral,
207> EquivSerializersGeneral for super::Optional<A, B> {
208    open spec fn equiv_general_inv(&self) -> bool {
209        &&& self.0.equiv_general_inv()
210        &&& self.1.equiv_general_inv()
211    }
212
213    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
214        Pair(super::Opt(self.0), self.1).lemma_serialize_equiv(v, obuf);
215    }
216}
217
218impl<A: EquivSerializersGeneral, B: EquivSerializers> EquivSerializers for super::Optional<A, B> {
219    open spec fn equiv_inv(&self) -> bool {
220        &&& self.0.equiv_general_inv()
221        &&& self.1.equiv_inv()
222    }
223
224    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
225        Pair(super::Opt(self.0), self.1).lemma_serialize_equiv_on_empty(v);
226    }
227}
228
229} // verus!
vest_lib/combinators/opt/proof.rs

vest_lib/combinators/opt/
proof.rs
