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.take(N as int)))
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<Len: AsLen> SpecParser for super::Varied<Len> {
136    type PVal = Seq<u8>;
137
138    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
139        if ibuf.len() < self.0.as_nat() {
140            None
141        } else {
142            Some((self.0.as_nat() as int, ibuf.take(self.0.as_nat() as int)))
143        }
144    }
145}
146
147impl<Len: AsLen> Consistency for super::Varied<Len> {
148    type Val = Seq<u8>;
149
150    open spec fn consistent(&self, v: Self::Val) -> bool {
151        v.len() == self.0.as_nat()
152    }
153}
154
155impl<Len: AsLen> SafeParser for super::Varied<Len> {
156    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
157    }
158}
159
160impl<Len: AsLen> SoundParser for super::Varied<Len> {
161    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
162    }
163
164    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
165    }
166}
167
168impl<Len: AsLen> SpecSerializerDps for super::Varied<Len> {
169    type SValue = Seq<u8>;
170
171    open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
172        v + obuf
173    }
174}
175
176impl<Len: AsLen> SpecSerializer for super::Varied<Len> {
177    type SVal = Seq<u8>;
178
179    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
180        v
181    }
182}
183
184impl<Len: AsLen> NonTailFmt for super::Varied<Len> {
185    proof fn lemma_serialize_dps_prepend(&self, v: Seq<u8>, obuf: Seq<u8>) {
186        assert(self.spec_serialize_dps(v, obuf) == v + obuf);
187    }
188
189    proof fn lemma_serialize_dps_len(&self, v: Seq<u8>, obuf: Seq<u8>) {
190        assert(self.spec_serialize_dps(v, obuf).len() - obuf.len() == v.len());
191    }
192}
193
194impl<Len: AsLen> GoodSerializer for super::Varied<Len> {
195    proof fn lemma_serialize_len(&self, v: Self::SVal) {
196        assert(self.spec_serialize(v).len() == v.len());
197    }
198}
199
200impl<Len: AsLen> SpecByteLen for super::Varied<Len> {
201    type T = Seq<u8>;
202
203    open spec fn byte_len(&self, v: Self::T) -> nat {
204        v.len()
205    }
206}
207
208impl<Len: AsLen> MinMaxByteLen for super::Varied<Len> {
209    open spec fn min(&self) -> nat {
210        self.0.as_nat()
211    }
212
213    open spec fn max(&self) -> nat {
214        self.0.as_nat()
215    }
216
217    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
218    }
219}
220
221impl<Len: AsLen> super::Varied<Len> {
222    pub open spec fn byte_len(v: <Self as SpecByteLen>::T) -> nat {
223        v.len()
224    }
225}
226
227impl<Len: AsLen> BytesCombinator for super::Varied<Len> {
228    proof fn lemma_byte_len_is_buf_len(&self, s: Seq<u8>) {
229    }
230}
231
232impl<Len: AsLen> ValueByteLen for super::Varied<Len> {
233    open spec fn value_byte_len(v: Self::T) -> nat {
234        v.len()
235    }
236
237    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
238    }
239}
240
241impl<Inner: SpecParser, Len: AsLen> SpecParser for super::ExactLen<Inner, Len> {
242    type PVal = Inner::PVal;
243
244    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
245        super::AndThen(super::Varied(self.0), self.1).spec_parse(ibuf)
246    }
247}
248
249impl<Inner: Consistency + SpecByteLen<T = Inner::Val>, Len: AsLen> Consistency for super::ExactLen<
250    Inner,
251    Len,
252> {
253    type Val = Inner::Val;
254
255    open spec fn consistent(&self, v: Self::Val) -> bool {
256        &&& self.1.consistent(v)
257        &&& self.0.as_nat() == self.1.byte_len(v)
258    }
259}
260
261impl<Inner: SafeParser, Len: AsLen> SafeParser for super::ExactLen<Inner, Len> {
262    open spec fn safe_inv(&self) -> bool {
263        super::AndThen(super::Varied(self.0), self.1).safe_inv()
264    }
265
266    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
267        super::AndThen(super::Varied(self.0), self.1).lemma_parse_safe(ibuf);
268    }
269}
270
271impl<Inner: SoundParser, Len: AsLen> SoundParser for super::ExactLen<Inner, Len> {
272    open spec fn sound_inv(&self) -> bool {
273        super::AndThen(super::Varied(self.0), self.1).sound_inv()
274    }
275
276    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
277        super::AndThen(super::Varied(self.0), self.1).lemma_parse_sound_consumption(ibuf);
278    }
279
280    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
281        super::AndThen(super::Varied(self.0), self.1).lemma_parse_sound_value(ibuf);
282    }
283}
284
285impl<Inner: SpecSerializerDps, Len: AsLen> SpecSerializerDps for super::ExactLen<Inner, Len> {
286    type SValue = Inner::SValue;
287
288    open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
289        super::AndThen(super::Varied(self.0), self.1).spec_serialize_dps(v, obuf)
290    }
291}
292
293impl<Inner: SpecSerializer, Len: AsLen> SpecSerializer for super::ExactLen<Inner, Len> {
294    type SVal = Inner::SVal;
295
296    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
297        super::AndThen(super::Varied(self.0), self.1).spec_serialize(v)
298    }
299}
300
301impl<Inner, Len> NonTailFmt for super::ExactLen<Inner, Len> where
302    Inner: GoodSerializer + EquivSerializers,
303    Len: AsLen,
304 {
305    open spec fn serialize_dps_inv(&self) -> bool {
306        super::AndThen(super::Varied(self.0), self.1).serialize_dps_inv()
307    }
308
309    proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>) {
310        super::AndThen(super::Varied(self.0), self.1).lemma_serialize_dps_prepend(v, obuf);
311    }
312
313    proof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>) {
314        super::AndThen(super::Varied(self.0), self.1).lemma_serialize_dps_len(v, obuf);
315    }
316}
317
318impl<Inner: GoodSerializer, Len: AsLen> GoodSerializer for super::ExactLen<Inner, Len> {
319    open spec fn serialize_inv(&self) -> bool {
320        super::AndThen(super::Varied(self.0), self.1).serialize_inv()
321    }
322
323    proof fn lemma_serialize_len(&self, v: Self::SVal) {
324        super::AndThen(super::Varied(self.0), self.1).lemma_serialize_len(v);
325    }
326}
327
328impl<Inner: SpecByteLen, Len: AsLen> SpecByteLen for super::ExactLen<Inner, Len> {
329    type T = Inner::T;
330
331    open spec fn byte_len(&self, v: Self::T) -> nat {
332        super::AndThen(super::Varied(self.0), self.1).byte_len(v)
333    }
334}
335
336impl<Inner, Len> MinMaxByteLen for super::ExactLen<Inner, Len> where
337    Inner: SpecByteLen + Consistency<Val = Inner::T>,
338    Len: AsLen,
339 {
340    open spec fn min(&self) -> nat {
341        self.0.as_nat()
342    }
343
344    open spec fn max(&self) -> nat {
345        self.0.as_nat()
346    }
347
348    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
349        assert(self.0.as_nat() == self.1.byte_len(v));
350    }
351}
352
353impl<Inner: SpecByteLen, Len: AsLen> super::ExactLen<Inner, Len> {
354    pub open spec fn byte_len(inner: Inner, v: <Self as SpecByteLen>::T) -> nat {
355        inner.byte_len(v)
356    }
357}
358
359impl<Inner: ValueByteLen, Len: AsLen> ValueByteLen for super::ExactLen<Inner, Len> {
360    open spec fn value_byte_len(v: Self::T) -> nat {
361        Inner::value_byte_len(v)
362    }
363
364    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
365        self.1.lemma_value_len_matches_byte_len(v);
366    }
367}
368
369impl<A, Then> SpecParser for super::AndThen<A, Then> where
370    A: SpecParser<PVal = Seq<u8>>,
371    Then: SpecParser,
372 {
373    type PVal = Then::PVal;
374
375    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
376        match self.0.spec_parse(ibuf) {
377            None => None,
378            Some((len_a, chunk)) => match self.1.spec_parse(chunk) {
379                Some((len_b, v)) if len_a == len_b => Some((len_a, v)),
380                _ => None,
381            },
382        }
383    }
384}
385
386impl<A, Then> Consistency for super::AndThen<A, Then> where
387    A: BytesCombinator + Consistency<Val = Seq<u8>>,
388    Then: Consistency + SpecByteLen<T = Then::Val>,
389 {
390    type Val = Then::Val;
391
392    open spec fn consistent(&self, v: Self::Val) -> bool {
393        &&& self.1.consistent(v)
394        &&& exists|chunk: Seq<u8>|
395            self.0.consistent(chunk) && self.0.byte_len(chunk) == self.1.byte_len(v)
396    }
397}
398
399pub broadcast proof fn lemma_tail_and_then_consistent<Then>(then: Then, v: Then::Val) where
400    Then: Consistency + SpecByteLen<T = Then::Val>,
401
402    ensures
403        #[trigger] super::AndThen(Tail, then).consistent(v) == then.consistent(v),
404{
405    if then.consistent(v) {
406        let chunk = Seq::new(then.byte_len(v), |_i| 0u8);
407        assert(Tail.consistent(chunk));
408        assert(Tail.byte_len(chunk) == then.byte_len(v));
409        assert(super::AndThen(Tail, then).0.consistent(chunk));
410    } else {
411    }
412}
413
414pub broadcast group tail_and_then_lemmas {
415    lemma_tail_and_then_consistent,
416}
417
418impl<A, Then> SafeParser for super::AndThen<A, Then> where
419    A: BytesCombinator + SafeParser<PVal = Seq<u8>>,
420    Then: SafeParser,
421 {
422    open spec fn safe_inv(&self) -> bool {
423        self.0.safe_inv()
424    }
425
426    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
427        self.0.lemma_parse_safe(ibuf);
428    }
429}
430
431impl<A, Then> SoundParser for super::AndThen<A, Then> where
432    A: BytesCombinator + SoundParser,
433    Then: SoundParser,
434 {
435    open spec fn sound_inv(&self) -> bool {
436        self.0.sound_inv() && self.1.sound_inv()
437    }
438
439    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
440        match self.0.spec_parse(ibuf) {
441            None => {},
442            Some((len_a, chunk)) => match self.1.spec_parse(chunk) {
443                Some((len_b, v)) if len_a == len_b => {
444                    self.1.lemma_parse_sound_consumption(chunk);
445                    assert(self.byte_len(v) == self.1.byte_len(v));
446                },
447                _ => {},
448            },
449        }
450    }
451
452    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
453        match self.0.spec_parse(ibuf) {
454            None => {},
455            Some((len_a, chunk)) => match self.1.spec_parse(chunk) {
456                Some((len_b, v)) if len_a == len_b => {
457                    self.0.lemma_parse_sound_value(ibuf);
458                    self.0.lemma_parse_sound_consumption(ibuf);
459                    self.1.lemma_parse_sound_consumption(chunk);
460                    self.1.lemma_parse_sound_value(chunk);
461                    assert(self.0.consistent(chunk));
462                },
463                _ => {},
464            },
465        }
466    }
467}
468
469impl<A, Then> SpecSerializerDps for super::AndThen<A, Then> where
470    A: SpecSerializerDps<SValue = Seq<u8>>,
471    Then: SpecSerializerDps,
472 {
473    type SValue = Then::SValue;
474
475    open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
476        self.0.spec_serialize_dps(self.1.spec_serialize_dps(v, seq![]), obuf)
477    }
478}
479
480impl<A, Then> SpecSerializer for super::AndThen<A, Then> where
481    A: SpecSerializer<SVal = Seq<u8>>,
482    Then: SpecSerializer,
483 {
484    type SVal = Then::SVal;
485
486    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
487        let inner_bytes = self.1.spec_serialize(v);
488        self.0.spec_serialize(inner_bytes)
489    }
490}
491
492impl<A, Then> NonTailFmt for super::AndThen<A, Then> where
493    A: BytesCombinator + NonTailFmt,
494    Then: GoodSerializer + EquivSerializers,
495 {
496    open spec fn serialize_dps_inv(&self) -> bool {
497        &&& self.0.serialize_dps_inv()
498        &&& self.1.serialize_inv()
499        &&& self.1.equiv_inv()
500    }
501
502    proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>) {
503        self.0.lemma_serialize_dps_prepend(self.1.spec_serialize_dps(v, seq![]), obuf);
504    }
505
506    proof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>) {
507        self.1.lemma_serialize_equiv_on_empty(v);
508        self.1.lemma_serialize_len(v);
509        let inner_bytes = self.1.spec_serialize_dps(v, seq![]);
510        self.0.lemma_serialize_dps_len(inner_bytes, obuf);
511        self.0.lemma_byte_len_is_buf_len(inner_bytes);
512    }
513}
514
515impl<A, Then> GoodSerializer for super::AndThen<A, Then> where
516    A: BytesCombinator + GoodSerializer,
517    Then: GoodSerializer,
518 {
519    open spec fn serialize_inv(&self) -> bool {
520        &&& self.0.serialize_inv()
521        &&& self.1.serialize_inv()
522    }
523
524    proof fn lemma_serialize_len(&self, v: Self::SVal) {
525        let inner_bytes = self.1.spec_serialize(v);
526        self.1.lemma_serialize_len(v);
527        self.0.lemma_serialize_len(inner_bytes);
528        self.0.lemma_byte_len_is_buf_len(inner_bytes);
529    }
530}
531
532impl<A, Then: SpecByteLen> SpecByteLen for super::AndThen<A, Then> {
533    type T = Then::T;
534
535    open spec fn byte_len(&self, v: Self::T) -> nat {
536        self.1.byte_len(v)
537    }
538}
539
540impl<A, Then> MinMaxByteLen for super::AndThen<A, Then> where
541    A: BytesCombinator + Consistency<Val = Seq<u8>>,
542    Then: MinMaxByteLen,
543 {
544    open spec fn min(&self) -> nat {
545        self.1.min()
546    }
547
548    open spec fn max(&self) -> nat {
549        self.1.max()
550    }
551
552    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
553        self.1.lemma_min_max_byte_len(v);
554    }
555}
556
557impl<A, Then> ValueByteLen for super::AndThen<A, Then> where
558    A: BytesCombinator + Consistency<Val = Seq<u8>>,
559    Then: ValueByteLen,
560 {
561    open spec fn value_byte_len(v: Self::T) -> nat {
562        Then::value_byte_len(v)
563    }
564
565    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
566        self.1.lemma_value_len_matches_byte_len(v);
567    }
568}
569
570// pub open spec fn fill_array_rec<const N: usize>(base: [u8; N], s: Seq<u8>, i: nat) -> [u8; N]
571//     recommends
572//         s.len() == N,
573//         i <= N,
574//     decreases i,
575// {
576//     if i == 0 {
577//         base
578//     } else {
579//         let idx = (i - 1) as int;
580//         // base[idx] = s[idx];
581//         fill_array_rec(spec_array_update(base, idx, s[idx]), s, idx as nat)
582//     }
583// }
584// pub open spec fn array_from_seq<const N: usize>(s: Seq<u8>) -> [u8; N]
585//     recommends s.len() == N
586// {
587//     let base = vstd::array::spec_array_fill_for_copy_type::<u8, N>(0);
588//     fill_array_rec(base, s, N as nat)
589// }
590// proof fn lemma_fill_array_rec<const N: usize>(base: [u8; N], s: Seq<u8>, i: nat)
591//     requires
592//         s.len() == N,
593//         i <= N,
594//     ensures
595//         ({
596//             let res = fill_array_rec(base, s, i);
597//             forall|k: int| #![auto] 0 <= k < i ==> res[k] == s[k]
598//         }),
599//         ({
600//             let res = fill_array_rec(base, s, i);
601//             forall|k: int| #![auto] i <= k < N ==> res[k] == base[k]
602//         }),
603//     decreases i,
604// {
605//     if i == 0 {
606//     } else {
607//         let idx = (i - 1) as int;
608//         let new_base = spec_array_update(base, idx, s[idx]);
609//         lemma_fill_array_rec(new_base, s, idx as nat);
610//         let res = fill_array_rec(base, s, i);
611//         // Help Verus with array length
612//         // assert(res.len() == N);
613//         // assert(0 <= idx < N);
614//         assert(res[idx] == new_base[idx]);
615//         assert(new_base[idx] == s[idx]);
616//         assert(res[idx] == s[idx]);
617//     }
618// }
619// proof fn lemma_array_from_seq<const N: usize>(s: Seq<u8>)
620//     requires s.len() == N,
621//     ensures
622//         array_from_seq::<N>(s)@ == s,
623// {
624//     let base = spec_array_fill_for_copy_type::<u8, N>(0);
625//     lemma_fill_array_rec(base, s, N as nat);
626//     assert(array_from_seq::<N>(s)@ =~= s);
627// }
628} // verus!
vest_lib/combinators/bytes/spec.rs

vest_lib/combinators/bytes/
spec.rs
