vest_lib/combinators/tail/
spec.rs

1//! Specifications for tail-position formats.
2use crate::combinators::Pair;
3use crate::{
4    combinators::marker::spec::ZERO_BYTE_LEN,
5    combinators::{Optional, Repeat},
6    core::{proof::*, spec::*},
7};
8use vstd::prelude::*;
9
10verus! {
11
12impl SpecParser for super::Tail {
13    type PVal = Seq<u8>;
14
15    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
16        Some((ibuf.len() as int, ibuf))
17    }
18}
19
20impl Consistency for super::Tail {
21    type Val = Seq<u8>;
22
23    open spec fn consistent(&self, _v: Self::Val) -> bool {
24        true
25    }
26}
27
28impl SafeParser for super::Tail {
29    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
30    }
31}
32
33impl SoundParser for super::Tail {
34    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
35    }
36
37    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
38    }
39}
40
41impl SpecSerializerDps for super::Tail {
42    type SValue = Seq<u8>;
43
44    open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
45        v
46    }
47}
48
49impl SpecSerializer for super::Tail {
50    type SVal = Seq<u8>;
51
52    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
53        v
54    }
55}
56
57impl SpecByteLen for super::Tail {
58    type T = Seq<u8>;
59
60    open spec fn byte_len(&self, v: Self::T) -> nat {
61        v.len()
62    }
63}
64
65impl BytesCombinator for super::Tail {
66    proof fn lemma_byte_len_is_buf_len(&self, s: Seq<u8>) {
67    }
68}
69
70impl ValueByteLen for super::Tail {
71    open spec fn value_byte_len(v: Self::T) -> nat {
72        v.len()
73    }
74
75    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
76    }
77}
78
79impl GoodSerializer for super::Tail {
80    proof fn lemma_serialize_len(&self, v: Self::SVal) {
81    }
82}
83
84impl SpecParser for super::Eof {
85    type PVal = ();
86
87    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
88        if ibuf.len() == 0 {
89            Some((0, ()))
90        } else {
91            None
92        }
93    }
94}
95
96impl Consistency for super::Eof {
97    type Val = ();
98
99    open spec fn consistent(&self, _v: Self::Val) -> bool {
100        true
101    }
102}
103
104impl AdmitsUniqueVal for super::Eof {
105    proof fn lemma_unique_consistent_val(&self, v1: Self::Val, v2: Self::Val) {
106    }
107}
108
109impl SafeParser for super::Eof {
110    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
111    }
112}
113
114impl SoundParser for super::Eof {
115    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
116    }
117
118    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
119    }
120}
121
122impl SpecSerializerDps for super::Eof {
123    type SValue = ();
124
125    open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
126        Seq::empty()
127    }
128}
129
130impl SpecSerializer for super::Eof {
131    type SVal = ();
132
133    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
134        Seq::empty()
135    }
136}
137
138impl SpecByteLen for super::Eof {
139    type T = ();
140
141    open spec fn byte_len(&self, _v: Self::T) -> nat {
142        ZERO_BYTE_LEN as nat
143    }
144}
145
146impl MinMaxByteLen for super::Eof {
147    open spec fn min(&self) -> nat {
148        ZERO_BYTE_LEN as nat
149    }
150
151    open spec fn max(&self) -> nat {
152        ZERO_BYTE_LEN as nat
153    }
154
155    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
156    }
157}
158
159impl StaticByteLen for super::Eof {
160    open spec fn static_byte_len() -> nat {
161        ZERO_BYTE_LEN as nat
162    }
163
164    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
165    }
166}
167
168impl ValueByteLen for super::Eof {
169    open spec fn value_byte_len(_v: Self::T) -> nat {
170        ZERO_BYTE_LEN as nat
171    }
172
173    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
174    }
175}
176
177impl GoodSerializer for super::Eof {
178    proof fn lemma_serialize_len(&self, v: Self::SVal) {
179    }
180}
181
182impl<C: SpecParser> SpecParser for super::OptionalEnd<C> {
183    type PVal = Option<C::PVal>;
184
185    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
186        match Optional(self.0, super::Eof).spec_parse(ibuf) {
187            Some((n, (v, _))) => Some((n, v)),
188            None => None,
189        }
190    }
191}
192
193// /// Parsing semantics: parses `B` from the back, consumes the tail of the input, then parses `A`.
194// pub struct PairRev<A, B>(pub B, pub A);
195impl<A, B> SpecParser for super::PairRev<A, B> where
196    A: SpecParser,
197    B: StaticByteLen + SpecParser<PVal = B::T>,
198 {
199    type PVal = (A::PVal, B::PVal);
200
201    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
202        if ibuf.len() < B::static_byte_len() {
203            None
204        } else {
205            let prefix = ibuf.len() - B::static_byte_len();
206            match self.1.spec_parse(ibuf.take(prefix)) {
207                Some((n1, v1)) if n1 == prefix => {
208                    match self.0.spec_parse(ibuf.skip(prefix)) {
209                        Some((n2, v2)) if n2 == B::static_byte_len() => Some((n1 + n2, (v1, v2))),
210                        _ => None,
211                    }
212                },
213                _ => None,
214            }
215        }
216    }
217}
218
219impl<A, B> Consistency for super::PairRev<A, B> where A: Consistency, B: Consistency {
220    type Val = (A::Val, B::Val);
221
222    open spec fn consistent(&self, v: Self::Val) -> bool {
223        Pair(self.1, self.0).consistent((v.0, v.1))
224    }
225}
226
227impl<A, B> SafeParser for super::PairRev<A, B> where
228    A: SafeParser,
229    B: StaticByteLen + SafeParser<PVal = B::T>,
230 {
231    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
232    }
233}
234
235impl<A, B> SoundParser for super::PairRev<A, B> where
236    A: SoundParser,
237    B: StaticByteLen + SoundParser,
238 {
239    open spec fn sound_inv(&self) -> bool {
240        &&& self.0.sound_inv()
241        &&& self.1.sound_inv()
242    }
243
244    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
245        if ibuf.len() >= B::static_byte_len() {
246            let prefix = ibuf.len() - B::static_byte_len();
247            self.0.lemma_parse_sound_consumption(ibuf.skip(prefix));
248            self.1.lemma_parse_sound_consumption(ibuf.take(prefix));
249        }
250    }
251
252    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
253        if ibuf.len() >= B::static_byte_len() {
254            let prefix = ibuf.len() - B::static_byte_len();
255            self.0.lemma_parse_sound_value(ibuf.skip(prefix));
256            self.1.lemma_parse_sound_value(ibuf.take(prefix));
257        }
258    }
259}
260
261impl<A, B> SpecSerializerDps for super::PairRev<A, B> where
262    A: SpecSerializerDps,
263    B: SpecSerializerDps,
264 {
265    type SValue = (A::SValue, B::SValue);
266
267    open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
268        self.1.spec_serialize_dps(v.0, self.0.spec_serialize_dps(v.1, seq![]))
269    }
270}
271
272impl<A, B> SpecSerializer for super::PairRev<A, B> where A: SpecSerializer, B: SpecSerializer {
273    type SVal = (A::SVal, B::SVal);
274
275    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
276        Pair(self.1, self.0).spec_serialize((v.0, v.1))
277    }
278}
279
280impl<A, B> GoodSerializer for super::PairRev<A, B> where A: GoodSerializer, B: GoodSerializer {
281    open spec fn serialize_inv(&self) -> bool {
282        Pair(self.1, self.0).serialize_inv()
283    }
284
285    proof fn lemma_serialize_len(&self, v: Self::SVal) {
286        Pair(self.1, self.0).lemma_serialize_len((v.0, v.1));
287    }
288}
289
290impl<A, B> SpecByteLen for super::PairRev<A, B> where A: SpecByteLen, B: SpecByteLen {
291    type T = (A::T, B::T);
292
293    open spec fn byte_len(&self, v: Self::T) -> nat {
294        self.1.byte_len(v.0) + self.0.byte_len(v.1)
295    }
296}
297
298impl<A: MinMaxByteLen, B: MinMaxByteLen> MinMaxByteLen for super::PairRev<A, B> {
299    open spec fn min(&self) -> nat {
300        self.1.min() + self.0.min()
301    }
302
303    open spec fn max(&self) -> nat {
304        self.1.max() + self.0.max()
305    }
306
307    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
308        self.1.lemma_min_max_byte_len(v.0);
309        self.0.lemma_min_max_byte_len(v.1);
310    }
311}
312
313impl<A, B> ValueByteLen for super::PairRev<A, B> where A: ValueByteLen, B: ValueByteLen {
314    open spec fn value_byte_len(v: Self::T) -> nat {
315        A::value_byte_len(v.0) + B::value_byte_len(v.1)
316    }
317
318    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
319        self.1.lemma_value_len_matches_byte_len(v.0);
320        self.0.lemma_value_len_matches_byte_len(v.1);
321    }
322}
323
324impl<A, B> StaticByteLen for super::PairRev<A, B> where A: StaticByteLen, B: StaticByteLen {
325    open spec fn static_byte_len() -> nat {
326        A::static_byte_len() + B::static_byte_len()
327    }
328
329    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
330        self.1.lemma_static_len_matches_byte_len(v.0);
331        self.0.lemma_static_len_matches_byte_len(v.1);
332    }
333}
334
335impl<C> Consistency for super::OptionalEnd<C> where C: Consistency {
336    type Val = Option<C::Val>;
337
338    open spec fn consistent(&self, v: Self::Val) -> bool {
339        Optional(self.0, super::Eof).consistent((v, ()))
340    }
341}
342
343impl<C> SafeParser for super::OptionalEnd<C> where C: SafeParser {
344    open spec fn safe_inv(&self) -> bool {
345        self.0.safe_inv()
346    }
347
348    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
349        Optional(self.0, super::Eof).lemma_parse_safe(ibuf)
350    }
351}
352
353impl<C> SoundParser for super::OptionalEnd<C> where C: SoundParser {
354    open spec fn sound_inv(&self) -> bool {
355        self.0.sound_inv()
356    }
357
358    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
359        Optional(self.0, super::Eof).lemma_parse_sound_consumption(ibuf)
360    }
361
362    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
363        Optional(self.0, super::Eof).lemma_parse_sound_value(ibuf)
364    }
365}
366
367impl<C: SpecSerializerDps> SpecSerializerDps for super::OptionalEnd<C> {
368    type SValue = Option<C::SValue>;
369
370    open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
371        Optional(self.0, super::Eof).spec_serialize_dps((v, ()), obuf)
372    }
373}
374
375impl<C: SpecSerializer> SpecSerializer for super::OptionalEnd<C> {
376    type SVal = Option<C::SVal>;
377
378    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
379        Optional(self.0, super::Eof).spec_serialize((v, ()))
380    }
381}
382
383impl<C: GoodSerializer> GoodSerializer for super::OptionalEnd<C> {
384    open spec fn serialize_inv(&self) -> bool {
385        self.0.serialize_inv()
386    }
387
388    proof fn lemma_serialize_len(&self, v: Self::SVal) {
389        Optional(self.0, super::Eof).lemma_serialize_len((v, ()));
390    }
391}
392
393impl<C: SpecByteLen> SpecByteLen for super::OptionalEnd<C> {
394    type T = Option<C::T>;
395
396    open spec fn byte_len(&self, v: Self::T) -> nat {
397        Optional(self.0, super::Eof).byte_len((v, ()))
398    }
399}
400
401impl<C: MinMaxByteLen> MinMaxByteLen for super::OptionalEnd<C> {
402    open spec fn min(&self) -> nat {
403        Optional(self.0, super::Eof).min()
404    }
405
406    open spec fn max(&self) -> nat {
407        Optional(self.0, super::Eof).max()
408    }
409
410    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
411        Optional(self.0, super::Eof).lemma_min_max_byte_len((v, ()));
412    }
413}
414
415impl<C: ValueByteLen> ValueByteLen for super::OptionalEnd<C> {
416    open spec fn value_byte_len(v: Self::T) -> nat {
417        <Optional<C, super::Eof> as ValueByteLen>::value_byte_len((v, ()))
418    }
419
420    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
421        Optional(self.0, super::Eof).lemma_value_len_matches_byte_len((v, ()));
422    }
423}
424
425impl<C: SpecParser> SpecParser for super::RepeatTillEnd<C> {
426    type PVal = Seq<C::PVal>;
427
428    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
429        match Repeat(self.0, super::Eof).spec_parse(ibuf) {
430            Some((n, (vs, _))) => Some((n, vs)),
431            None => None,
432        }
433    }
434}
435
436impl<C> Consistency for super::RepeatTillEnd<C> where C: Consistency {
437    type Val = Seq<C::Val>;
438
439    open spec fn consistent(&self, v: Self::Val) -> bool {
440        Repeat(self.0, super::Eof).consistent((v, ()))
441    }
442}
443
444impl<C> SafeParser for super::RepeatTillEnd<C> where C: SafeParser {
445    open spec fn safe_inv(&self) -> bool {
446        self.0.safe_inv()
447    }
448
449    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
450        Repeat(self.0, super::Eof).lemma_parse_safe(ibuf)
451    }
452}
453
454impl<C> SoundParser for super::RepeatTillEnd<C> where C: SoundParser {
455    open spec fn sound_inv(&self) -> bool {
456        self.0.sound_inv()
457    }
458
459    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
460        Repeat(self.0, super::Eof).lemma_parse_sound_consumption(ibuf)
461    }
462
463    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
464        Repeat(self.0, super::Eof).lemma_parse_sound_value(ibuf)
465    }
466}
467
468impl<C: SpecSerializerDps> SpecSerializerDps for super::RepeatTillEnd<C> {
469    type SValue = Seq<C::SValue>;
470
471    open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
472        Repeat(self.0, super::Eof).spec_serialize_dps((v, ()), obuf)
473    }
474}
475
476impl<C: SpecSerializer> SpecSerializer for super::RepeatTillEnd<C> {
477    type SVal = Seq<C::SVal>;
478
479    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
480        Repeat(self.0, super::Eof).spec_serialize((v, ()))
481    }
482}
483
484impl<C: GoodSerializer> GoodSerializer for super::RepeatTillEnd<C> {
485    open spec fn serialize_inv(&self) -> bool {
486        self.0.serialize_inv()
487    }
488
489    proof fn lemma_serialize_len(&self, v: Self::SVal) {
490        Repeat(self.0, super::Eof).lemma_serialize_len((v, ()));
491    }
492}
493
494impl<C: SpecByteLen> SpecByteLen for super::RepeatTillEnd<C> {
495    type T = Seq<C::T>;
496
497    open spec fn byte_len(&self, v: Self::T) -> nat {
498        Repeat(self.0, super::Eof).byte_len((v, ()))
499    }
500}
501
502impl<C: ValueByteLen> ValueByteLen for super::RepeatTillEnd<C> {
503    open spec fn value_byte_len(v: Self::T) -> nat {
504        <Repeat<C, super::Eof> as ValueByteLen>::value_byte_len((v, ()))
505    }
506
507    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
508        Repeat(self.0, super::Eof).lemma_value_len_matches_byte_len((v, ()));
509    }
510}
511
512} // verus!
vest_lib/combinators/tail/spec.rs

vest_lib/combinators/tail/
spec.rs
