vest_lib/combinators/tuple/
spec.rs

1//! Specifications for sequential composition.
2use crate::combinators::mapped::spec::*;
3use crate::core::{proof::*, spec::*};
4use vstd::prelude::*;
5
6verus! {
7
8impl<A, B> SpecParser for super::Pair<A, B> where A: SpecParser, B: SpecParser {
9    type PVal = (A::PVal, B::PVal);
10
11    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
12        match self.0.spec_parse(ibuf) {
13            Some((n1, v1)) => match self.1.spec_parse(ibuf[n1..]) {
14                Some((n2, v2)) => Some((n1 + n2, (v1, v2))),
15                None => None,
16            },
17            None => None,
18        }
19    }
20}
21
22impl<A, B> Consistency for super::Pair<A, B> where A: Consistency, B: Consistency {
23    type Val = (A::Val, B::Val);
24
25    open spec fn consistent(&self, v: Self::Val) -> bool {
26        self.0.consistent(v.0) && self.1.consistent(v.1)
27    }
28}
29
30impl<A, B> SafeParser for super::Pair<A, B> where A: SafeParser, B: SafeParser {
31    open spec fn safe_inv(&self) -> bool {
32        &&& self.0.safe_inv()
33        &&& self.1.safe_inv()
34    }
35
36    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
37        assert(self.safe_inv());
38        self.0.lemma_parse_safe(ibuf);
39        if let Some((n1, v1)) = self.0.spec_parse(ibuf) {
40            self.1.lemma_parse_safe(ibuf[n1..]);
41        }
42    }
43}
44
45impl<A, B> SoundParser for super::Pair<A, B> where A: SoundParser, B: SoundParser {
46    open spec fn sound_inv(&self) -> bool {
47        &&& self.0.sound_inv()
48        &&& self.1.sound_inv()
49    }
50
51    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
52        assert(self.sound_inv());
53        self.0.lemma_parse_sound_consumption(ibuf);
54        if let Some((n1, v1)) = self.0.spec_parse(ibuf) {
55            self.1.lemma_parse_sound_consumption(ibuf[n1..]);
56        }
57    }
58
59    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
60        assert(self.sound_inv());
61        self.0.lemma_parse_sound_value(ibuf);
62        if let Some((n1, v1)) = self.0.spec_parse(ibuf) {
63            self.1.lemma_parse_sound_value(ibuf[n1..]);
64        }
65    }
66}
67
68impl<A, B> SpecSerializerDps for super::Pair<A, B> where
69    A: SpecSerializerDps,
70    B: SpecSerializerDps,
71 {
72    type SValue = (A::SValue, B::SValue);
73
74    open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
75        self.0.spec_serialize_dps(v.0, self.1.spec_serialize_dps(v.1, obuf))
76    }
77}
78
79impl<A, B> SpecSerializer for super::Pair<A, B> where A: SpecSerializer, B: SpecSerializer {
80    type SVal = (A::SVal, B::SVal);
81
82    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
83        self.0.spec_serialize(v.0) + self.1.spec_serialize(v.1)
84    }
85}
86
87impl<A, B> NonTailFmt for super::Pair<A, B> where A: NonTailFmt, B: NonTailFmt {
88    open spec fn serialize_dps_inv(&self) -> bool {
89        &&& self.0.serialize_dps_inv()
90        &&& self.1.serialize_dps_inv()
91    }
92
93    proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>) {
94        let serialized1 = self.1.spec_serialize_dps(v.1, obuf);
95        let serialized0 = self.0.spec_serialize_dps(v.0, serialized1);
96        assert(self.serialize_dps_inv());
97        self.1.lemma_serialize_dps_prepend(v.1, obuf);
98        self.0.lemma_serialize_dps_prepend(v.0, serialized1);
99        let witness1 = choose|wit1: Seq<u8>| self.1.spec_serialize_dps(v.1, obuf) == wit1 + obuf;
100        let witness0 = choose|wit0: Seq<u8>|
101            self.0.spec_serialize_dps(v.0, serialized1) == wit0 + serialized1;
102        assert(serialized0 == witness0 + witness1 + obuf);
103    }
104
105    proof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>) {
106        assert(self.serialize_dps_inv());
107        self.1.lemma_serialize_dps_len(v.1, obuf);
108        let serialized1 = self.1.spec_serialize_dps(v.1, obuf);
109        self.0.lemma_serialize_dps_len(v.0, serialized1);
110    }
111}
112
113impl<A, B> GoodSerializer for super::Pair<A, B> where A: GoodSerializer, B: GoodSerializer {
114    open spec fn serialize_inv(&self) -> bool {
115        &&& self.0.serialize_inv()
116        &&& self.1.serialize_inv()
117    }
118
119    proof fn lemma_serialize_len(&self, v: Self::SVal) {
120        assert(self.serialize_inv());
121        self.1.lemma_serialize_len(v.1);
122        self.0.lemma_serialize_len(v.0);
123    }
124}
125
126impl<A: SpecByteLen, B: SpecByteLen> SpecByteLen for super::Pair<A, B> {
127    type T = (A::T, B::T);
128
129    open spec fn byte_len(&self, v: Self::T) -> nat {
130        self.0.byte_len(v.0) + self.1.byte_len(v.1)
131    }
132}
133
134impl<A: MinMaxByteLen, B: MinMaxByteLen> MinMaxByteLen for super::Pair<A, B> {
135    open spec fn max(&self) -> nat {
136        self.0.max() + self.1.max()
137    }
138
139    open spec fn min(&self) -> nat {
140        self.0.min() + self.1.min()
141    }
142
143    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
144        self.0.lemma_min_max_byte_len(v.0);
145        self.1.lemma_min_max_byte_len(v.1);
146    }
147}
148
149impl<A: ValueByteLen, B: ValueByteLen> ValueByteLen for super::Pair<A, B> {
150    open spec fn value_byte_len(v: Self::T) -> nat {
151        A::value_byte_len(v.0) + B::value_byte_len(v.1)
152    }
153
154    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
155        self.0.lemma_value_len_matches_byte_len(v.0);
156        self.1.lemma_value_len_matches_byte_len(v.1);
157    }
158}
159
160impl<A: StaticByteLen, B: StaticByteLen> StaticByteLen for super::Pair<A, B> {
161    open spec fn static_byte_len() -> nat {
162        A::static_byte_len() + B::static_byte_len()
163    }
164
165    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
166        self.0.lemma_static_len_matches_byte_len(v.0);
167        self.1.lemma_static_len_matches_byte_len(v.1);
168    }
169}
170
171impl<A, B> SpecParser for super::Bind<A, B> where
172    A: SpecParser,
173    B: SpecMap<Input = A::PVal>,
174    B::Output: SpecParser,
175 {
176    type PVal = (A::PVal, <B::Output as SpecParser>::PVal);
177
178    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
179        match self.0.spec_parse(ibuf) {
180            Some((n1, key)) => {
181                let next = self.1.spec_map(key);
182                match next.spec_parse(ibuf[n1..]) {
183                    Some((n2, val)) => Some((n1 + n2, (key, val))),
184                    None => None,
185                }
186            },
187            None => None,
188        }
189    }
190}
191
192impl<A, B> Consistency for super::Bind<A, B> where
193    A: Consistency,
194    B: SpecMap<Input = A::Val>,
195    B::Output: Consistency,
196 {
197    type Val = (A::Val, <B::Output as Consistency>::Val);
198
199    open spec fn consistent(&self, value: Self::Val) -> bool {
200        let (key, val) = value;
201        self.0.consistent(key) && self.1.spec_map(key).consistent(val)
202    }
203}
204
205impl<A, B> SafeParser for super::Bind<A, B> where
206    A: SafeParser,
207    B: SpecMap<Input = A::PVal>,
208    B::Output: SafeParser,
209 {
210    open spec fn safe_inv(&self) -> bool {
211        &&& self.0.safe_inv()
212        &&& forall|key: A::PVal| #[trigger] self.1.spec_map(key).safe_inv()
213    }
214
215    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
216        assert(self.safe_inv());
217        self.0.lemma_parse_safe(ibuf);
218        if let Some((n1, key)) = self.0.spec_parse(ibuf) {
219            let next = self.1.spec_map(key);
220            next.lemma_parse_safe(ibuf[n1..]);
221        }
222    }
223}
224
225impl<A, B> SoundParser for super::Bind<A, B> where
226    A: SoundParser,
227    B: SpecMap<Input = A::PVal>,
228    B::Output: SoundParser,
229 {
230    open spec fn sound_inv(&self) -> bool {
231        &&& self.0.sound_inv()
232        &&& forall|key: A::PVal| #[trigger] self.1.spec_map(key).sound_inv()
233    }
234
235    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
236        self.0.lemma_parse_sound_consumption(ibuf);
237        self.0.lemma_parse_sound_value(ibuf);
238        if let Some((n1, key)) = self.0.spec_parse(ibuf) {
239            let next = self.1.spec_map(key);
240            next.lemma_parse_sound_consumption(ibuf[n1..]);
241            next.lemma_parse_sound_value(ibuf[n1..]);
242            if let Some((_n2, val)) = next.spec_parse(ibuf[n1..]) {
243                assert(self.byte_len((key, val)) == self.0.byte_len(key) + next.byte_len(val));
244            }
245        }
246    }
247
248    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
249        self.0.lemma_parse_sound_value(ibuf);
250        if let Some((n1, key)) = self.0.spec_parse(ibuf) {
251            let next = self.1.spec_map(key);
252            next.lemma_parse_sound_value(ibuf[n1..]);
253            if let Some((_n2, val)) = next.spec_parse(ibuf[n1..]) {
254                assert(self.consistent((key, val)));
255            }
256        }
257    }
258}
259
260impl<A, B> SpecSerializerDps for super::Bind<A, B> where
261    A: SpecSerializerDps,
262    B: SpecMap<Input = A::SValue>,
263    B::Output: SpecSerializerDps,
264 {
265    type SValue = (A::SValue, <B::Output as SpecSerializerDps>::SValue);
266
267    open spec fn spec_serialize_dps(&self, value: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
268        let (key, val) = value;
269        let next = self.1.spec_map(key);
270        self.0.spec_serialize_dps(key, next.spec_serialize_dps(val, obuf))
271    }
272}
273
274impl<A, B> SpecSerializer for super::Bind<A, B> where
275    A: SpecSerializer,
276    B: SpecMap<Input = A::SVal>,
277    B::Output: SpecSerializer,
278 {
279    type SVal = (A::SVal, <B::Output as SpecSerializer>::SVal);
280
281    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
282        let (key, val) = v;
283        let next = self.1.spec_map(key);
284        self.0.spec_serialize(key) + next.spec_serialize(val)
285    }
286}
287
288impl<A, B> NonTailFmt for super::Bind<A, B> where
289    A: NonTailFmt,
290    B: SpecMap<Input = A::SValue>,
291    B::Output: NonTailFmt,
292 {
293    open spec fn serialize_dps_inv(&self) -> bool {
294        &&& self.0.serialize_dps_inv()
295        &&& forall|key: A::SValue| #[trigger] self.1.spec_map(key).serialize_dps_inv()
296    }
297
298    proof fn lemma_serialize_dps_prepend(&self, value: Self::SValue, obuf: Seq<u8>) {
299        let (key, val) = value;
300        let next = self.1.spec_map(key);
301        let next_buf = next.spec_serialize_dps(val, obuf);
302
303        assert(self.serialize_dps_inv());
304        next.lemma_serialize_dps_prepend(val, obuf);
305        self.0.lemma_serialize_dps_prepend(key, next_buf);
306
307        let witness_next = choose|w: Seq<u8>| next.spec_serialize_dps(val, obuf) == w + obuf;
308        let witness_prefix = choose|w: Seq<u8>|
309            self.0.spec_serialize_dps(key, next_buf) == w + next_buf;
310        assert(self.spec_serialize_dps(value, obuf) == witness_prefix + witness_next + obuf);
311    }
312
313    proof fn lemma_serialize_dps_len(&self, value: Self::SValue, obuf: Seq<u8>) {
314        let (key, val) = value;
315        let next = self.1.spec_map(key);
316        let next_buf = next.spec_serialize_dps(val, obuf);
317        assert(self.serialize_dps_inv());
318        next.lemma_serialize_dps_len(val, obuf);
319        self.0.lemma_serialize_dps_len(key, next_buf);
320    }
321}
322
323impl<A, B> GoodSerializer for super::Bind<A, B> where
324    A: GoodSerializer,
325    B: SpecMap<Input = A::SVal>,
326    B::Output: GoodSerializer,
327 {
328    open spec fn serialize_inv(&self) -> bool {
329        &&& self.0.serialize_inv()
330        &&& forall|key: A::SVal| #[trigger] self.1.spec_map(key).serialize_inv()
331    }
332
333    proof fn lemma_serialize_len(&self, value: Self::SVal) {
334        let (key, val) = value;
335        let next = self.1.spec_map(key);
336        assert(self.serialize_inv());
337        self.0.lemma_serialize_len(key);
338        next.lemma_serialize_len(val);
339    }
340}
341
342impl<A, B> SpecByteLen for super::Bind<A, B> where
343    A: SpecByteLen,
344    B: SpecMap<Input = A::T>,
345    B::Output: SpecByteLen,
346 {
347    type T = (A::T, <B::Output as SpecByteLen>::T);
348
349    open spec fn byte_len(&self, value: Self::T) -> nat {
350        let (key, val) = value;
351        let next = self.1.spec_map(key);
352        self.0.byte_len(key) + next.byte_len(val)
353    }
354}
355
356impl<A, B> ValueByteLen for super::Bind<A, B> where
357    A: ValueByteLen,
358    B: SpecMap<Input = A::T>,
359    B::Output: ValueByteLen,
360 {
361    open spec fn value_byte_len(value: Self::T) -> nat {
362        A::value_byte_len(value.0) + <B::Output as ValueByteLen>::value_byte_len(value.1)
363    }
364
365    proof fn lemma_value_len_matches_byte_len(&self, value: Self::T) {
366        let (key, val) = value;
367        let next = self.1.spec_map(key);
368        self.0.lemma_value_len_matches_byte_len(key);
369        next.lemma_value_len_matches_byte_len(val);
370    }
371}
372
373impl<A, B> StaticByteLen for super::Bind<A, B> where
374    A: StaticByteLen,
375    B: SpecMap<Input = A::T>,
376    B::Output: StaticByteLen,
377 {
378    open spec fn static_byte_len() -> nat {
379        A::static_byte_len() + <B::Output as StaticByteLen>::static_byte_len()
380    }
381
382    proof fn lemma_static_len_matches_byte_len(&self, value: Self::T) {
383        let (key, val) = value;
384        let next = self.1.spec_map(key);
385        self.0.lemma_static_len_matches_byte_len(key);
386        next.lemma_static_len_matches_byte_len(val);
387    }
388}
389
390} // verus!
vest_lib/combinators/tuple/spec.rs

vest_lib/combinators/tuple/
spec.rs
