vest_lib/combinators/implicit/
spec.rs

1//! Specification for dependent formats that omit their header value.
2use super::*;
3use crate::combinators::bytes::ExactLen;
4use crate::combinators::length::AsLen;
5use crate::combinators::tuple::Pair;
6use crate::combinators::{Choice, Cond, Sum, Varied, Void};
7use crate::core::spec::*;
8use crate::Never;
9use vstd::prelude::*;
10
11verus! {
12
13impl<Head, Tail> SpecParser for Implicit<Head, Tail> where
14    Head: SpecParser,
15    Tail: DepCombinator<Key = Head::PVal>,
16    Tail::Body: SpecParser<PVal = Tail::Val>,
17 {
18    type PVal = Tail::Val;
19
20    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
21        match self.0.spec_parse(ibuf) {
22            Some((n1, key)) => {
23                let body = self.1.apply(key);
24                match body.spec_parse(ibuf.skip(n1)) {
25                    Some((n2, value)) => Some((n1 + n2, value)),
26                    None => None,
27                }
28            },
29            None => None,
30        }
31    }
32}
33
34impl<Head, Tail> Consistency for Implicit<Head, Tail> where
35    Head: Consistency,
36    Tail: DepCombinator<Key = Head::Val>,
37 {
38    type Val = Tail::Val;
39
40    open spec fn consistent(&self, value: Self::Val) -> bool {
41        let key = self.1.recover(value);
42        self.0.consistent(key) && self.1.apply(key).consistent(value)
43    }
44}
45
46impl<Head, Tail> SafeParser for Implicit<Head, Tail> where
47    Head: SafeParser,
48    Tail: DepCombinator<Key = Head::PVal>,
49    Tail::Body: SafeParser<PVal = Tail::Val>,
50 {
51    open spec fn safe_inv(&self) -> bool {
52        &&& self.0.safe_inv()
53        &&& forall|key: Head::PVal| #[trigger] self.1.apply(key).safe_inv()
54    }
55
56    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
57        self.0.lemma_parse_safe(ibuf);
58        if let Some((n1, key)) = self.0.spec_parse(ibuf) {
59            let body = self.1.apply(key);
60            body.lemma_parse_safe(ibuf.skip(n1));
61        }
62    }
63}
64
65impl<Head, Tail> SoundParser for Implicit<Head, Tail> where
66    Head: SoundParser,
67    Tail: DepCombinator<Key = Head::PVal>,
68    Tail::Body: SoundParser<T = Tail::Val>,
69 {
70    open spec fn sound_inv(&self) -> bool {
71        &&& self.0.sound_inv()
72        &&& forall|key: Head::PVal| #[trigger] self.1.apply(key).sound_inv()
73        &&& self.1.recover_inv()
74    }
75
76    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
77        self.0.lemma_parse_sound_consumption(ibuf);
78        if let Some((n1, key)) = self.0.spec_parse(ibuf) {
79            let body = self.1.apply(key);
80            body.lemma_parse_sound_consumption(ibuf.skip(n1));
81            body.lemma_parse_sound_value(ibuf.skip(n1));
82            if let Some((n2, value)) = body.spec_parse(ibuf.skip(n1)) {
83                self.1.lemma_recover_consistent(key, value);
84                assert(self.1.recover(value) == key);
85                assert(self.byte_len(value) == self.0.byte_len(key) + body.byte_len(value));
86            }
87        }
88    }
89
90    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
91        self.0.lemma_parse_sound_value(ibuf);
92        if let Some((n1, key)) = self.0.spec_parse(ibuf) {
93            let body = self.1.apply(key);
94            body.lemma_parse_sound_value(ibuf.skip(n1));
95            if let Some((_n2, value)) = body.spec_parse(ibuf.skip(n1)) {
96                self.1.lemma_recover_consistent(key, value);
97                assert(self.1.recover(value) == key);
98                assert(self.consistent(value));
99            }
100        }
101    }
102}
103
104impl<Head, Tail> SpecSerializerDps for Implicit<Head, Tail> where
105    Head: SpecSerializerDps,
106    Tail: DepCombinator<Key = Head::SValue>,
107    Tail::Body: SpecSerializerDps<SValue = Tail::Val>,
108 {
109    type SValue = Tail::Val;
110
111    open spec fn spec_serialize_dps(&self, value: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
112        let key = self.1.recover(value);
113        let body = self.1.apply(key);
114        self.0.spec_serialize_dps(key, body.spec_serialize_dps(value, obuf))
115    }
116}
117
118impl<Head, Tail> SpecSerializer for Implicit<Head, Tail> where
119    Head: SpecSerializer,
120    Tail: DepCombinator<Key = Head::SVal>,
121    Tail::Body: SpecSerializer<SVal = Tail::Val>,
122 {
123    type SVal = Tail::Val;
124
125    open spec fn spec_serialize(&self, value: Self::SVal) -> Seq<u8> {
126        let key = self.1.recover(value);
127        let body = self.1.apply(key);
128        self.0.spec_serialize(key) + body.spec_serialize(value)
129    }
130}
131
132impl<Head, Tail> NonTailFmt for Implicit<Head, Tail> where
133    Head: NonTailFmt,
134    Tail: DepCombinator<Key = Head::SValue>,
135    Tail::Body: NonTailFmt<T = Tail::Val>,
136 {
137    open spec fn serialize_dps_inv(&self) -> bool {
138        &&& self.0.serialize_dps_inv()
139        &&& forall|key: Head::SValue| #[trigger] self.1.apply(key).serialize_dps_inv()
140    }
141
142    proof fn lemma_serialize_dps_prepend(&self, value: Self::SValue, obuf: Seq<u8>) {
143        let key = self.1.recover(value);
144        let body = self.1.apply(key);
145        let body_buf = body.spec_serialize_dps(value, obuf);
146
147        body.lemma_serialize_dps_prepend(value, obuf);
148        self.0.lemma_serialize_dps_prepend(key, body_buf);
149
150        let witness_body = choose|w: Seq<u8>| body.spec_serialize_dps(value, obuf) == w + obuf;
151        let witness_prefix = choose|w: Seq<u8>|
152            self.0.spec_serialize_dps(key, body_buf) == w + body_buf;
153        assert(self.spec_serialize_dps(value, obuf) == witness_prefix + witness_body + obuf);
154    }
155
156    proof fn lemma_serialize_dps_len(&self, value: Self::SValue, obuf: Seq<u8>) {
157        let key = self.1.recover(value);
158        let body = self.1.apply(key);
159        let body_buf = body.spec_serialize_dps(value, obuf);
160        body.lemma_serialize_dps_len(value, obuf);
161        self.0.lemma_serialize_dps_len(key, body_buf);
162    }
163}
164
165impl<Head, Tail> GoodSerializer for Implicit<Head, Tail> where
166    Head: GoodSerializer,
167    Tail: DepCombinator<Key = Head::SVal>,
168    Tail::Body: GoodSerializer<T = Tail::Val>,
169 {
170    open spec fn serialize_inv(&self) -> bool {
171        &&& self.0.serialize_inv()
172        &&& forall|key: Head::SVal| #[trigger] self.1.apply(key).serialize_inv()
173    }
174
175    proof fn lemma_serialize_len(&self, value: Self::SVal) {
176        let key = self.1.recover(value);
177        let body = self.1.apply(key);
178        self.0.lemma_serialize_len(key);
179        body.lemma_serialize_len(value);
180    }
181}
182
183impl<Head, Tail> SpecByteLen for Implicit<Head, Tail> where
184    Head: SpecByteLen,
185    Tail: DepCombinator<Key = Head::T>,
186    Tail::Body: SpecByteLen<T = Tail::Val>,
187 {
188    type T = Tail::Val;
189
190    open spec fn byte_len(&self, value: Self::T) -> nat {
191        let key = self.1.recover(value);
192        let body = self.1.apply(key);
193        self.0.byte_len(key) + body.byte_len(value)
194    }
195}
196
197impl<Head, Tail> StaticByteLen for Implicit<Head, Tail> where
198    Head: StaticByteLen,
199    Tail: DepCombinator<Key = Head::T>,
200    Tail::Body: StaticByteLen<T = Tail::Val>,
201 {
202    open spec fn static_byte_len() -> nat {
203        Head::static_byte_len() + Tail::Body::static_byte_len()
204    }
205
206    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
207        let key = self.1.recover(v);
208        let body = self.1.apply(key);
209        self.0.lemma_static_len_matches_byte_len(key);
210        body.lemma_static_len_matches_byte_len(v);
211    }
212}
213
214impl<Head, Tail> ValueByteLen for Implicit<Head, Tail> where
215    Head: StaticByteLen,
216    Tail: DepCombinator<Key = Head::T>,
217    Tail::Body: ValueByteLen<T = Tail::Val>,
218 {
219    open spec fn value_byte_len(value: Self::T) -> nat {
220        Head::static_byte_len() + Tail::Body::value_byte_len(value)
221    }
222
223    proof fn lemma_value_len_matches_byte_len(&self, value: Self::T) {
224        let key = self.1.recover(value);
225        let next = self.1.apply(key);
226        self.0.lemma_static_len_matches_byte_len(key);
227        next.lemma_value_len_matches_byte_len(value);
228    }
229}
230
231// ----To enable compositions like `Implicit(T1, Implicit(T2, ...))`---
232// NOTE: The above is not true... but I will keep it here for fun
233impl<Head, Nested> DepCombinator for Implicit<Head, Nested> where
234    Head: Consistency,
235    Nested: DepCombinator<Key = Head::Val>,
236 {
237    type Key = Head::Val;
238
239    type Val = Nested::Val;
240
241    type Body = Nested::Body;
242
243    open spec fn apply(&self, key: Self::Key) -> Self::Body {
244        self.1.apply(key)
245    }
246
247    open spec fn recover(&self, value: Self::Val) -> Self::Key {
248        self.1.recover(value)
249    }
250
251    open spec fn recover_inv(&self) -> bool {
252        self.1.recover_inv()
253    }
254
255    proof fn lemma_recover_consistent(&self, key: Self::Key, value: Self::Val) {
256        self.1.lemma_recover_consistent(key, value);
257    }
258}
259
260impl<Key, Val, Body> DepCombinator for KVFormat<Key, Val, Body> where Body: Consistency<Val = Val> {
261    type Key = Key;
262
263    type Val = Val;
264
265    type Body = Body;
266
267    open spec fn apply(&self, key: Self::Key) -> Self::Body {
268        (self.0)(key)
269    }
270
271    open spec fn recover(&self, value: Self::Val) -> Self::Key {
272        (self.1)(value)
273    }
274
275    open spec fn recover_inv(&self) -> bool {
276        forall|key: Key, value: Val| #[trigger]
277            (self.0)(key).consistent(value) ==> (self.1)(value) == key
278    }
279
280    proof fn lemma_recover_consistent(&self, key: Self::Key, value: Self::Val) {
281        if self.apply(key).consistent(value) {
282            assert(self.recover(value) == key);
283        }
284    }
285}
286
287// Enabling patterns like `Implicit(U8, VariedU8())`, `Implicit(U16, VariedU16())`,
288// and arbitrary user length types implementing `AsLen`.
289impl<Len: AsLen> DepCombinator for VariedLen<Len> {
290    type Key = Len;
291
292    type Val = Seq<u8>;
293
294    type Body = Varied<Len>;
295
296    open spec fn apply(&self, key: Self::Key) -> Self::Body {
297        Varied(key)
298    }
299
300    open spec fn recover(&self, value: Self::Val) -> Self::Key {
301        Len::as_self(value.len())
302    }
303
304    proof fn lemma_recover_consistent(&self, key: Self::Key, value: Self::Val) {
305        if self.apply(key).consistent(value) {
306            Len::lemma_lossless_casting(key);
307            assert(value.len() == key.as_nat());
308        }
309    }
310}
311
312// Similar to `VariedLen`, but with the body being an arbitrary combinator instead of just `Varied`.
313impl<Len, Then> DepCombinator for NBytesOf<Len, Then> where
314    Len: AsLen,
315    Then: SpecByteLen + Consistency<Val = Then::T>,
316 {
317    type Key = Len;
318
319    type Val = Then::Val;
320
321    type Body = ExactLen<Then, Len>;
322
323    open spec fn apply(&self, key: Self::Key) -> Self::Body {
324        ExactLen(key, self.1)
325    }
326
327    open spec fn recover(&self, value: Self::Val) -> Self::Key {
328        Len::as_self(self.1.byte_len(value))
329    }
330
331    proof fn lemma_recover_consistent(&self, key: Self::Key, value: Self::Val) {
332        if self.apply(key).consistent(value) {
333            Len::lemma_lossless_casting(key);
334        }
335    }
336}
337
338// Enabling Patterns like `Implicit(Pair(H1, H2), Pair(T1, T2))`.
339// e.g.,
340// ```
341// fmt = {
342//   @l1: u8,
343//   @l2: u16,
344//   payload1: [u8; @l1],
345//   payload2: [u8; @l2],
346// }
347impl<D1: DepCombinator, D2: DepCombinator> DepCombinator for Pair<D1, D2> {
348    type Key = (D1::Key, D2::Key);
349
350    type Val = (D1::Val, D2::Val);
351
352    type Body = Pair<D1::Body, D2::Body>;
353
354    open spec fn apply(&self, key: Self::Key) -> Self::Body {
355        Pair(self.0.apply(key.0), self.1.apply(key.1))
356    }
357
358    open spec fn recover(&self, value: Self::Val) -> Self::Key {
359        (self.0.recover(value.0), self.1.recover(value.1))
360    }
361
362    open spec fn recover_inv(&self) -> bool {
363        self.0.recover_inv() && self.1.recover_inv()
364    }
365
366    proof fn lemma_recover_consistent(&self, key: Self::Key, value: Self::Val) {
367        self.0.lemma_recover_consistent(key.0, value.0);
368        self.1.lemma_recover_consistent(key.1, value.1);
369    }
370}
371
372impl<Tag, C, Rest> DepCombinator for TVOr<Tag, C, Rest> where
373    C: Consistency,
374    Rest: DepCombinator<Key = Tag>,
375 {
376    type Key = Tag;
377
378    type Val = Sum<C::Val, Rest::Val>;
379
380    type Body = Choice<Cond<C>, Rest::Body>;
381
382    open spec fn apply(&self, key: Self::Key) -> Self::Body {
383        Choice(Cond(key == self.0, self.1), self.2.apply(key))
384    }
385
386    open spec fn recover(&self, value: Self::Val) -> Self::Key {
387        match value {
388            Sum::Inl(_) => self.0,
389            Sum::Inr(vr) => self.2.recover(vr),
390        }
391    }
392
393    open spec fn recover_inv(&self) -> bool {
394        self.2.recover_inv()
395    }
396
397    proof fn lemma_recover_consistent(&self, key: Self::Key, value: Self::Val) {
398        if self.apply(key).consistent(value) {
399            match value {
400                Sum::Inl(vl) => {
401                    assert(self.recover(value) == key);
402                },
403                Sum::Inr(vr) => {
404                    self.2.lemma_recover_consistent(key, vr);
405                },
406            }
407        }
408    }
409}
410
411impl<Tag> DepCombinator for VoidTag<Tag> {
412    type Key = Tag;
413
414    type Val = Never;
415
416    type Body = Void;
417
418    open spec fn apply(&self, _key: Self::Key) -> Self::Body {
419        Void("Impossible")
420    }
421
422    open spec fn recover(&self, value: Self::Val) -> Self::Key {
423        use vstd::pervasive::arbitrary;
424        arbitrary::<Tag>()
425    }
426
427    proof fn lemma_recover_consistent(&self, _key: Self::Key, value: Self::Val) {
428    }
429}
430
431impl<Tag, Left, Right> DepCombinator for TagValNode<Tag, Left, Right> where
432    Left: DepCombinator<Key = Tag>,
433    Right: DepCombinator<Key = Tag>,
434 {
435    type Key = Tag;
436
437    type Val = Sum<Left::Val, Right::Val>;
438
439    type Body = Choice<Left::Body, Right::Body>;
440
441    open spec fn apply(&self, key: Self::Key) -> Self::Body {
442        Choice(self.0.apply(key), self.1.apply(key))
443    }
444
445    open spec fn recover(&self, value: Self::Val) -> Self::Key {
446        match value {
447            Sum::Inl(vl) => self.0.recover(vl),
448            Sum::Inr(vr) => self.1.recover(vr),
449        }
450    }
451
452    open spec fn recover_inv(&self) -> bool {
453        self.0.recover_inv() && self.1.recover_inv()
454    }
455
456    proof fn lemma_recover_consistent(&self, key: Self::Key, value: Self::Val) {
457        match value {
458            Sum::Inl(vl) => {
459                self.0.lemma_recover_consistent(key, vl);
460            },
461            Sum::Inr(vr) => {
462                self.1.lemma_recover_consistent(key, vr);
463            },
464        }
465    }
466}
467
468impl<Tag, C: Consistency> DepCombinator for TVLeaf<Tag, C> {
469    type Key = Tag;
470
471    type Val = C::Val;
472
473    type Body = Cond<C>;
474
475    open spec fn apply(&self, key: Self::Key) -> Self::Body {
476        Cond(key == self.0, self.1)
477    }
478
479    open spec fn recover(&self, _value: Self::Val) -> Self::Key {
480        self.0
481    }
482
483    proof fn lemma_recover_consistent(&self, key: Self::Key, value: Self::Val) {
484    }
485}
486
487impl<Tag, Len, V> DepCombinator for TLVal<Tag, Len, V> where
488    Len: AsLen,
489    V: DepCombinator<Key = Tag>,
490    V::Body: SpecByteLen<T = V::Val>,
491 {
492    type Key = (Tag, Len);
493
494    type Val = V::Val;
495
496    type Body = ExactLen<V::Body, Len>;
497
498    open spec fn apply(&self, key: Self::Key) -> Self::Body {
499        let (tag, len) = key;
500        ExactLen(len, self.0.apply(tag))
501    }
502
503    open spec fn recover(&self, value: Self::Val) -> Self::Key {
504        let tag = self.0.recover(value);
505        let body = self.0.apply(tag);
506        (tag, Len::as_self(body.byte_len(value)))
507    }
508
509    open spec fn recover_inv(&self) -> bool {
510        self.0.recover_inv()
511    }
512
513    proof fn lemma_recover_consistent(&self, key: Self::Key, value: Self::Val) {
514        if self.apply(key).consistent(value) {
515            self.0.lemma_recover_consistent(key.0, value);
516            Len::lemma_lossless_casting(key.1);
517            let body = self.0.apply(key.0);
518            assert(body.byte_len(value) == key.1.as_nat());
519        }
520    }
521}
522
523} // verus!
vest_lib/combinators/implicit/spec.rs

vest_lib/combinators/implicit/
spec.rs
