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

vest_lib/combinators/tuple/
spec.rs
