vest_lib/combinators/bytes/
spec.rs

1//! Specifications for fixed- and variable-length bytes.
2use crate::combinators::length::AsLen;
3use crate::core::{proof::*, spec::*};
4use vstd::prelude::*;
5
6use super::Varied;
7use crate::combinators::Tail;
8
9verus! {
10
11pub uninterp spec fn array_from_seq<const N: usize, T>(s: Seq<T>) -> [T; N]
12    recommends
13        s.len() == N,
14;
15
16pub broadcast axiom fn axiom_array_from_seq<const N: usize, T>(s: Seq<T>)
17    requires
18        s.len() == N,
19    ensures
20        (#[trigger] array_from_seq::<N, T>(s))@ == s,
21;
22
23pub broadcast proof fn lemma_array_from_seq_roundtrip<const N: usize, T>(a: [T; N])
24    ensures
25        #[trigger] array_from_seq::<N, T>(a@) == a,
26{
27    broadcast use axiom_array_from_seq;
28
29}
30
31impl<const N: usize> SpecParser for super::Fixed<N> {
32    type PVal = Seq<u8>;
33
34    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
35        if ibuf.len() < N as int {
36            None
37        } else {
38            Some((N as int, ibuf[0..N]))
39        }
40    }
41}
42
43impl<const N: usize> Consistency for super::Fixed<N> {
44    type Val = Seq<u8>;
45
46    open spec fn consistent(&self, v: Self::Val) -> bool {
47        v.len() == N
48    }
49}
50
51impl<const N: usize> SafeParser for super::Fixed<N> {
52    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
53    }
54}
55
56impl<const N: usize> SoundParser for super::Fixed<N> {
57    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
58    }
59
60    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
61    }
62}
63
64impl<const N: usize> SpecSerializerDps for super::Fixed<N> {
65    type SValue = Seq<u8>;
66
67    open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
68        v + obuf
69    }
70}
71
72impl<const N: usize> SpecSerializer for super::Fixed<N> {
73    type SVal = Seq<u8>;
74
75    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
76        v
77    }
78}
79
80impl<const N: usize> NonTailFmt for super::Fixed<N> {
81    proof fn lemma_serialize_dps_prepend(&self, v: Seq<u8>, obuf: Seq<u8>) {
82        assert(self.spec_serialize_dps(v, obuf) == v + obuf);
83    }
84
85    proof fn lemma_serialize_dps_len(&self, v: Seq<u8>, obuf: Seq<u8>) {
86        assert(self.spec_serialize_dps(v, obuf).len() - obuf.len() == v.len());
87    }
88}
89
90impl<const N: usize> GoodSerializer for super::Fixed<N> {
91    proof fn lemma_serialize_len(&self, v: Self::SVal) {
92        assert(self.spec_serialize(v).len() == v.len());
93    }
94}
95
96impl<const N: usize> SpecByteLen for super::Fixed<N> {
97    type T = Seq<u8>;
98
99    open spec fn byte_len(&self, v: Self::T) -> nat {
100        v.len()
101    }
102}
103
104impl<const N: usize> MinMaxByteLen for super::Fixed<N> {
105    open spec fn min(&self) -> nat {
106        N as nat
107    }
108
109    open spec fn max(&self) -> nat {
110        N as nat
111    }
112
113    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
114    }
115}
116
117impl<const N: usize> StaticByteLen for super::Fixed<N> {
118    open spec fn static_byte_len() -> nat {
119        N as nat
120    }
121
122    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
123    }
124}
125
126impl<const N: usize> ValueByteLen for super::Fixed<N> {
127    open spec fn value_byte_len(_v: Self::T) -> nat {
128        N as nat
129    }
130
131    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
132    }
133}
134
135impl<const N: usize> BytesCombinator for super::Fixed<N> {
136    proof fn lemma_byte_len_is_buf_len(&self, buf: Seq<u8>) {
137    }
138}
139
140impl<Len: AsLen> SpecParser for super::Varied<Len> {
141    type PVal = Seq<u8>;
142
143    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
144        if ibuf.len() < self.0.as_nat() {
145            None
146        } else {
147            Some((self.0.as_nat() as int, ibuf[0..self.0.as_nat()]))
148        }
149    }
150}
151
152impl<Len: AsLen> Consistency for super::Varied<Len> {
153    type Val = Seq<u8>;
154
155    open spec fn consistent(&self, v: Self::Val) -> bool {
156        v.len() == self.0.as_nat()
157    }
158}
159
160impl<Len: AsLen> SafeParser for super::Varied<Len> {
161    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
162    }
163}
164
165impl<Len: AsLen> SoundParser for super::Varied<Len> {
166    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
167    }
168
169    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
170    }
171}
172
173impl<Len: AsLen> SpecSerializerDps for super::Varied<Len> {
174    type SValue = Seq<u8>;
175
176    open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
177        v + obuf
178    }
179}
180
181impl<Len: AsLen> SpecSerializer for super::Varied<Len> {
182    type SVal = Seq<u8>;
183
184    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
185        v
186    }
187}
188
189impl<Len: AsLen> NonTailFmt for super::Varied<Len> {
190    proof fn lemma_serialize_dps_prepend(&self, v: Seq<u8>, obuf: Seq<u8>) {
191        assert(self.spec_serialize_dps(v, obuf) == v + obuf);
192    }
193
194    proof fn lemma_serialize_dps_len(&self, v: Seq<u8>, obuf: Seq<u8>) {
195        assert(self.spec_serialize_dps(v, obuf).len() - obuf.len() == v.len());
196    }
197}
198
199impl<Len: AsLen> GoodSerializer for super::Varied<Len> {
200    proof fn lemma_serialize_len(&self, v: Self::SVal) {
201        assert(self.spec_serialize(v).len() == v.len());
202    }
203}
204
205impl<Len: AsLen> SpecByteLen for super::Varied<Len> {
206    type T = Seq<u8>;
207
208    open spec fn byte_len(&self, v: Self::T) -> nat {
209        v.len()
210    }
211}
212
213impl<Len: AsLen> MinMaxByteLen for super::Varied<Len> {
214    open spec fn min(&self) -> nat {
215        self.0.as_nat()
216    }
217
218    open spec fn max(&self) -> nat {
219        self.0.as_nat()
220    }
221
222    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
223    }
224}
225
226impl<Len: AsLen> super::Varied<Len> {
227    pub open spec fn byte_len(v: <Self as SpecByteLen>::T) -> nat {
228        v.len()
229    }
230}
231
232impl<Len: AsLen> BytesCombinator for super::Varied<Len> {
233    proof fn lemma_byte_len_is_buf_len(&self, s: Seq<u8>) {
234    }
235}
236
237impl<Len: AsLen> ValueByteLen for super::Varied<Len> {
238    open spec fn value_byte_len(v: Self::T) -> nat {
239        v.len()
240    }
241
242    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
243    }
244}
245
246impl<Inner: SpecParser, Len: AsLen> SpecParser for super::ExactLen<Inner, Len> {
247    type PVal = Inner::PVal;
248
249    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
250        super::AndThen(super::Varied(self.0), self.1).spec_parse(ibuf)
251    }
252}
253
254impl<Inner: Consistency + SpecByteLen<T = Inner::Val>, Len: AsLen> Consistency for super::ExactLen<
255    Inner,
256    Len,
257> {
258    type Val = Inner::Val;
259
260    open spec fn consistent(&self, v: Self::Val) -> bool {
261        &&& self.1.consistent(v)
262        &&& self.0.as_nat() == self.1.byte_len(v)
263    }
264}
265
266impl<Inner: SafeParser, Len: AsLen> SafeParser for super::ExactLen<Inner, Len> {
267    open spec fn safe_inv(&self) -> bool {
268        super::AndThen(super::Varied(self.0), self.1).safe_inv()
269    }
270
271    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
272        super::AndThen(super::Varied(self.0), self.1).lemma_parse_safe(ibuf);
273    }
274}
275
276impl<Inner: SoundParser, Len: AsLen> SoundParser for super::ExactLen<Inner, Len> {
277    open spec fn sound_inv(&self) -> bool {
278        super::AndThen(super::Varied(self.0), self.1).sound_inv()
279    }
280
281    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
282        super::AndThen(super::Varied(self.0), self.1).lemma_parse_sound_consumption(ibuf);
283    }
284
285    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
286        super::AndThen(super::Varied(self.0), self.1).lemma_parse_sound_value(ibuf);
287    }
288}
289
290impl<Inner: SpecSerializerDps, Len: AsLen> SpecSerializerDps for super::ExactLen<Inner, Len> {
291    type SValue = Inner::SValue;
292
293    open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
294        super::AndThen(super::Varied(self.0), self.1).spec_serialize_dps(v, obuf)
295    }
296}
297
298impl<Inner: SpecSerializer, Len: AsLen> SpecSerializer for super::ExactLen<Inner, Len> {
299    type SVal = Inner::SVal;
300
301    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
302        super::AndThen(super::Varied(self.0), self.1).spec_serialize(v)
303    }
304}
305
306impl<Inner, Len> NonTailFmt for super::ExactLen<Inner, Len> where
307    Inner: GoodSerializer + EquivSerializers,
308    Len: AsLen,
309 {
310    open spec fn serialize_dps_inv(&self) -> bool {
311        super::AndThen(super::Varied(self.0), self.1).serialize_dps_inv()
312    }
313
314    proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>) {
315        super::AndThen(super::Varied(self.0), self.1).lemma_serialize_dps_prepend(v, obuf);
316    }
317
318    proof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>) {
319        super::AndThen(super::Varied(self.0), self.1).lemma_serialize_dps_len(v, obuf);
320    }
321}
322
323impl<Inner: GoodSerializer, Len: AsLen> GoodSerializer for super::ExactLen<Inner, Len> {
324    open spec fn serialize_inv(&self) -> bool {
325        super::AndThen(super::Varied(self.0), self.1).serialize_inv()
326    }
327
328    proof fn lemma_serialize_len(&self, v: Self::SVal) {
329        super::AndThen(super::Varied(self.0), self.1).lemma_serialize_len(v);
330    }
331}
332
333impl<Inner: SpecByteLen, Len: AsLen> SpecByteLen for super::ExactLen<Inner, Len> {
334    type T = Inner::T;
335
336    open spec fn byte_len(&self, v: Self::T) -> nat {
337        super::AndThen(super::Varied(self.0), self.1).byte_len(v)
338    }
339}
340
341impl<Inner, Len> MinMaxByteLen for super::ExactLen<Inner, Len> where
342    Inner: SpecByteLen + Consistency<Val = Inner::T>,
343    Len: AsLen,
344 {
345    open spec fn min(&self) -> nat {
346        self.0.as_nat()
347    }
348
349    open spec fn max(&self) -> nat {
350        self.0.as_nat()
351    }
352
353    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
354        assert(self.0.as_nat() == self.1.byte_len(v));
355    }
356}
357
358impl<Inner: SpecByteLen, Len: AsLen> super::ExactLen<Inner, Len> {
359    pub open spec fn byte_len(inner: Inner, v: <Self as SpecByteLen>::T) -> nat {
360        inner.byte_len(v)
361    }
362}
363
364impl<Inner: ValueByteLen, Len: AsLen> ValueByteLen for super::ExactLen<Inner, Len> {
365    open spec fn value_byte_len(v: Self::T) -> nat {
366        Inner::value_byte_len(v)
367    }
368
369    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
370        self.1.lemma_value_len_matches_byte_len(v);
371    }
372}
373
374impl<Inner: StaticByteLen, Len: AsLen> StaticByteLen for super::ExactLen<Inner, Len> {
375    open spec fn static_byte_len() -> nat {
376        Inner::static_byte_len()
377    }
378
379    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
380        self.1.lemma_static_len_matches_byte_len(v);
381    }
382}
383
384impl<A, Then> SpecParser for super::AndThen<A, Then> where
385    A: SpecParser<PVal = Seq<u8>>,
386    Then: SpecParser,
387 {
388    type PVal = Then::PVal;
389
390    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
391        match self.0.spec_parse(ibuf) {
392            None => None,
393            Some((len_a, chunk)) => match self.1.spec_parse(chunk) {
394                Some((len_b, v)) if len_a == len_b => Some((len_a, v)),
395                _ => None,
396            },
397        }
398    }
399}
400
401impl<A, Then> Consistency for super::AndThen<A, Then> where
402    A: BytesCombinator + Consistency<Val = Seq<u8>>,
403    Then: Consistency + SpecByteLen<T = Then::Val>,
404 {
405    type Val = Then::Val;
406
407    open spec fn consistent(&self, v: Self::Val) -> bool {
408        &&& self.1.consistent(v)
409        &&& exists|chunk: Seq<u8>|
410            self.0.consistent(chunk) && self.0.byte_len(chunk) == self.1.byte_len(v)
411    }
412}
413
414pub broadcast proof fn lemma_tail_and_then_consistent<Then>(then: Then, v: Then::Val) where
415    Then: Consistency + SpecByteLen<T = Then::Val>,
416
417    ensures
418        #[trigger] super::AndThen(Tail, then).consistent(v) == then.consistent(v),
419{
420    if then.consistent(v) {
421        let chunk = Seq::new(then.byte_len(v), |_i| 0u8);
422        assert(Tail.consistent(chunk));
423        assert(Tail.byte_len(chunk) == then.byte_len(v));
424        assert(super::AndThen(Tail, then).0.consistent(chunk));
425    } else {
426    }
427}
428
429pub broadcast group tail_and_then_lemmas {
430    lemma_tail_and_then_consistent,
431}
432
433impl<A, Then> SafeParser for super::AndThen<A, Then> where
434    A: BytesCombinator + SafeParser<PVal = Seq<u8>>,
435    Then: SafeParser,
436 {
437    open spec fn safe_inv(&self) -> bool {
438        self.0.safe_inv()
439    }
440
441    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
442        self.0.lemma_parse_safe(ibuf);
443    }
444}
445
446impl<A, Then> SoundParser for super::AndThen<A, Then> where
447    A: BytesCombinator + SoundParser,
448    Then: SoundParser,
449 {
450    open spec fn sound_inv(&self) -> bool {
451        self.0.sound_inv() && self.1.sound_inv()
452    }
453
454    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
455        match self.0.spec_parse(ibuf) {
456            None => {},
457            Some((len_a, chunk)) => match self.1.spec_parse(chunk) {
458                Some((len_b, v)) if len_a == len_b => {
459                    self.1.lemma_parse_sound_consumption(chunk);
460                    assert(self.byte_len(v) == self.1.byte_len(v));
461                },
462                _ => {},
463            },
464        }
465    }
466
467    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
468        match self.0.spec_parse(ibuf) {
469            None => {},
470            Some((len_a, chunk)) => match self.1.spec_parse(chunk) {
471                Some((len_b, v)) if len_a == len_b => {
472                    self.0.lemma_parse_sound_value(ibuf);
473                    self.0.lemma_parse_sound_consumption(ibuf);
474                    self.1.lemma_parse_sound_consumption(chunk);
475                    self.1.lemma_parse_sound_value(chunk);
476                    assert(self.0.consistent(chunk));
477                },
478                _ => {},
479            },
480        }
481    }
482}
483
484impl<A, Then> SpecSerializerDps for super::AndThen<A, Then> where
485    A: SpecSerializerDps<SValue = Seq<u8>>,
486    Then: SpecSerializerDps,
487 {
488    type SValue = Then::SValue;
489
490    open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
491        self.0.spec_serialize_dps(self.1.spec_serialize_dps(v, seq![]), obuf)
492    }
493}
494
495impl<A, Then> SpecSerializer for super::AndThen<A, Then> where
496    A: SpecSerializer<SVal = Seq<u8>>,
497    Then: SpecSerializer,
498 {
499    type SVal = Then::SVal;
500
501    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
502        let inner_bytes = self.1.spec_serialize(v);
503        self.0.spec_serialize(inner_bytes)
504    }
505}
506
507impl<A, Then> NonTailFmt for super::AndThen<A, Then> where
508    A: BytesCombinator + NonTailFmt,
509    Then: GoodSerializer + EquivSerializers,
510 {
511    open spec fn serialize_dps_inv(&self) -> bool {
512        &&& self.0.serialize_dps_inv()
513        &&& self.1.serialize_inv()
514        &&& self.1.equiv_inv()
515    }
516
517    proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>) {
518        self.0.lemma_serialize_dps_prepend(self.1.spec_serialize_dps(v, seq![]), obuf);
519    }
520
521    proof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>) {
522        self.1.lemma_serialize_equiv_on_empty(v);
523        self.1.lemma_serialize_len(v);
524        let inner_bytes = self.1.spec_serialize_dps(v, seq![]);
525        self.0.lemma_serialize_dps_len(inner_bytes, obuf);
526        self.0.lemma_byte_len_is_buf_len(inner_bytes);
527    }
528}
529
530impl<A, Then> GoodSerializer for super::AndThen<A, Then> where
531    A: BytesCombinator + GoodSerializer,
532    Then: GoodSerializer,
533 {
534    open spec fn serialize_inv(&self) -> bool {
535        &&& self.0.serialize_inv()
536        &&& self.1.serialize_inv()
537    }
538
539    proof fn lemma_serialize_len(&self, v: Self::SVal) {
540        let inner_bytes = self.1.spec_serialize(v);
541        self.1.lemma_serialize_len(v);
542        self.0.lemma_serialize_len(inner_bytes);
543        self.0.lemma_byte_len_is_buf_len(inner_bytes);
544    }
545}
546
547impl<A, Then: SpecByteLen> SpecByteLen for super::AndThen<A, Then> {
548    type T = Then::T;
549
550    open spec fn byte_len(&self, v: Self::T) -> nat {
551        self.1.byte_len(v)
552    }
553}
554
555impl<A, Then> MinMaxByteLen for super::AndThen<A, Then> where
556    A: BytesCombinator + Consistency<Val = Seq<u8>>,
557    Then: MinMaxByteLen,
558 {
559    open spec fn min(&self) -> nat {
560        self.1.min()
561    }
562
563    open spec fn max(&self) -> nat {
564        self.1.max()
565    }
566
567    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
568        self.1.lemma_min_max_byte_len(v);
569    }
570}
571
572impl<A, Then> ValueByteLen for super::AndThen<A, Then> where
573    A: BytesCombinator + Consistency<Val = Seq<u8>>,
574    Then: ValueByteLen,
575 {
576    open spec fn value_byte_len(v: Self::T) -> nat {
577        Then::value_byte_len(v)
578    }
579
580    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
581        self.1.lemma_value_len_matches_byte_len(v);
582    }
583}
584
585impl<A, Then> StaticByteLen for super::AndThen<A, Then> where
586    A: BytesCombinator + StaticByteLen,
587    Then: Consistency + SpecByteLen<T = Then::Val>,
588 {
589    open spec fn static_byte_len() -> nat {
590        A::static_byte_len()
591    }
592
593    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
594        let chunk = choose|chunk: Seq<u8>|
595            self.0.consistent(chunk) && self.0.byte_len(chunk) == self.1.byte_len(v);
596        self.0.lemma_static_len_matches_byte_len(chunk);
597    }
598}
599
600// pub open spec fn fill_array_rec<const N: usize>(base: [u8; N], s: Seq<u8>, i: nat) -> [u8; N]
601//     recommends
602//         s.len() == N,
603//         i <= N,
604//     decreases i,
605// {
606//     if i == 0 {
607//         base
608//     } else {
609//         let idx = (i - 1) as int;
610//         // base[idx] = s[idx];
611//         fill_array_rec(spec_array_update(base, idx, s[idx]), s, idx as nat)
612//     }
613// }
614// pub open spec fn array_from_seq<const N: usize>(s: Seq<u8>) -> [u8; N]
615//     recommends s.len() == N
616// {
617//     let base = vstd::array::spec_array_fill_for_copy_type::<u8, N>(0);
618//     fill_array_rec(base, s, N as nat)
619// }
620// proof fn lemma_fill_array_rec<const N: usize>(base: [u8; N], s: Seq<u8>, i: nat)
621//     requires
622//         s.len() == N,
623//         i <= N,
624//     ensures
625//         ({
626//             let res = fill_array_rec(base, s, i);
627//             forall|k: int| #![auto] 0 <= k < i ==> res[k] == s[k]
628//         }),
629//         ({
630//             let res = fill_array_rec(base, s, i);
631//             forall|k: int| #![auto] i <= k < N ==> res[k] == base[k]
632//         }),
633//     decreases i,
634// {
635//     if i == 0 {
636//     } else {
637//         let idx = (i - 1) as int;
638//         let new_base = spec_array_update(base, idx, s[idx]);
639//         lemma_fill_array_rec(new_base, s, idx as nat);
640//         let res = fill_array_rec(base, s, i);
641//         // Help Verus with array length
642//         // assert(res.len() == N);
643//         // assert(0 <= idx < N);
644//         assert(res[idx] == new_base[idx]);
645//         assert(new_base[idx] == s[idx]);
646//         assert(res[idx] == s[idx]);
647//     }
648// }
649// proof fn lemma_array_from_seq<const N: usize>(s: Seq<u8>)
650//     requires s.len() == N,
651//     ensures
652//         array_from_seq::<N>(s)@ == s,
653// {
654//     let base = spec_array_fill_for_copy_type::<u8, N>(0);
655//     lemma_fill_array_rec(base, s, N as nat);
656//     assert(array_from_seq::<N>(s)@ =~= s);
657// }
658} // verus!
vest_lib/combinators/bytes/spec.rs

vest_lib/combinators/bytes/
spec.rs
