vest_lib/
properties.rs

1pub use crate::buf_traits::*;
2pub use crate::errors::*;
3use alloc::boxed::Box;
4
5use vstd::prelude::*;
6use vstd::*;
7
8verus! {
9
10/// The parse result of a combinator.
11pub type PResult<T, E> = Result<(usize, T), E>;
12
13/// The serialize result of a combinator.
14pub type SResult<T, E> = Result<T, E>;
15
16/// Specification for parser and serializer [`Combinator`]s. All Vest combinators must implement this
17/// trait.
18pub trait SpecCombinator {
19    /// The view of [`Combinator::Result`].
20    type Type;
21
22    /// Well-formedness of the format [`Self::type`] (e.g., refinements on the type).
23    open spec fn wf(&self, v: Self::Type) -> bool {
24        true
25    }
26
27    /// Pre-conditions for parsing and serialization.
28    ///
29    /// ## Examples
30    ///
31    /// - Sequencing combinators require that the first combinator is prefix-secure.
32    /// - Repetition combinators require that the inner combinator is prefix-secure.
33    /// - [`crate::regular::repetition::Repeat`] combinator requires that the
34    ///   inner combinator is productive.
35    /// - [`crate::regular::variant::Choice`] combinator requires that `Snd` is [`crate::regular::disjoint::DisjointFrom`] `Fst`.
36    open spec fn requires(&self) -> bool {
37        true
38    }
39
40    /// The specification of [`Combinator::parse`].
41    spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, Self::Type)>;
42
43    /// The specification of [`Combinator::serialize`].
44    spec fn spec_serialize(&self, v: Self::Type) -> Seq<u8>;
45}
46
47/// Theorems and lemmas that must be proven for a combinator to be considered correct and secure.
48pub trait SecureSpecCombinator: SpecCombinator {
49    /// One of the top-level roundtrip properties
50    /// It reads "if we serialize a (well-formed) value, then parsing the serialized bytes should
51    /// give us the same value back."
52    /// If we somehow get a different value, it means that different high-level values can
53    /// correspond to the same low-level representation, or put differently, the same byte
54    /// sequences can be parsed into different values.
55    ///
56    /// This property can be understood as
57    /// 1. injectivity of serialization: different values should serialize to different byte
58    ///    sequences
59    /// 2. surjectivity of parsing: every valid high-level value should associate with at least one
60    ///    low-level representation.
61    /// 3. correctness of parsing: given a correct serializer that produces some byte sequence from
62    ///   a value, the corresponding parser should be able to parse the byte sequence back to the
63    ///   same value (can lead to format-confusion attacks if not satisfied).
64    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type)
65        requires
66            self.requires(),
67        ensures
68            self.wf(v) ==> self.spec_parse(self.spec_serialize(v)) == Some(
69                (self.spec_serialize(v).len() as int, v),
70            ),
71    ;
72
73    /// Followed from `theorem_serialize_parse_roundtrip`
74    proof fn corollary_parse_surjective(&self, v: Self::Type)
75        requires
76            self.requires(),
77            self.wf(v),
78        ensures
79            exists|b: Seq<u8>| #[trigger] self.spec_parse(b) matches Some((_, v_)) && v_ == v,
80    {
81        self.theorem_serialize_parse_roundtrip(v);
82    }
83
84    /// Followed from `theorem_serialize_parse_roundtrip`
85    proof fn corollary_serialize_injective(&self, v1: Self::Type, v2: Self::Type)
86        requires
87            self.requires(),
88        ensures
89            self.wf(v1) && self.wf(v2) ==> self.spec_serialize(v1) == self.spec_serialize(v2) ==> v1
90                == v2,
91    {
92        self.theorem_serialize_parse_roundtrip(v1);
93        self.theorem_serialize_parse_roundtrip(v2);
94    }
95
96    /// Followed from `theorem_serialize_parse_roundtrip`
97    proof fn corollary_serialize_injective_contraposition(&self, v1: Self::Type, v2: Self::Type)
98        requires
99            self.requires(),
100        ensures
101            self.wf(v1) && self.wf(v2) ==> v1 != v2 ==> self.spec_serialize(v1)
102                != self.spec_serialize(v2),
103    {
104        self.theorem_serialize_parse_roundtrip(v1);
105        self.theorem_serialize_parse_roundtrip(v2);
106    }
107
108    /// One of the top-level roundtrip properties
109    /// It reads "if we successfully parse a byte sequence, then serializing the parsed value should
110    /// give us the same byte sequence back."
111    /// If we somehow get a different byte sequence, it means that different low-level representations
112    /// can correspond to the same high-level value, or put differently, the same value can be
113    /// serialized into different byte sequences.
114    ///
115    /// This property can be understood as
116    /// 1. injectivity of parsing: different byte sequences should parse to different values (can
117    ///    lead to parser mallability attacks if not satisfied)
118    /// 2. correctness of serialization: given a correct parser that produces some value from a byte
119    ///   sequence, the corresponding serializer should be able to serialize the value back to the same
120    ///   byte sequence (up to the number of bytes consumed).
121    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>)
122        requires
123            self.requires(),
124        ensures
125            self.spec_parse(buf) matches Some((n, v)) ==> {
126                &&& self.wf(v)
127                &&& self.spec_serialize(v) == buf.take(n)
128            },
129    ;
130
131    /// Followed from `theorem_parse_serialize_roundtrip`
132    proof fn corollary_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>)
133        requires
134            self.requires(),
135        ensures
136            self.spec_parse(buf1) matches Some((n1, v1)) ==> self.spec_parse(buf2) matches Some(
137                (n2, v2),
138            ) ==> v1 == v2 ==> buf1.take(n1) == buf2.take(n2),
139    {
140        self.theorem_parse_serialize_roundtrip(buf1);
141        self.theorem_parse_serialize_roundtrip(buf2);
142    }
143
144    /// Like an associated constant, denotes whether the combinator is prefix-secure.
145    spec fn is_prefix_secure() -> bool;
146
147    /// This prefix-secure lemma is used in the proof of the roundtrip properties for sequencing
148    /// and repeating combinators.
149    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>)
150        requires
151            self.requires(),
152        ensures
153            Self::is_prefix_secure() ==> self.spec_parse(s1) is Some ==> self.spec_parse(s1 + s2)
154                == self.spec_parse(s1),
155    ;
156
157    /// The parser-length lemma is used in the proof of the roundtrip properties and the prefix-secure
158    /// lemma
159    proof fn lemma_parse_length(&self, s: Seq<u8>)
160        requires
161            self.requires(),
162        ensures
163            self.spec_parse(s) matches Some((n, _)) ==> 0 <= n <= s.len(),
164    ;
165
166    /// Like an associated constant, denotes whether the combinator is productive
167    spec fn is_productive(&self) -> bool;
168
169    /// This lemma is used in the proof of the roundtrip properties for optional and unbounded
170    /// repeating combinators.
171    proof fn lemma_parse_productive(&self, s: Seq<u8>)
172        requires
173            self.requires(),
174        ensures
175            self.is_productive() ==> (self.spec_parse(s) matches Some((n, _)) ==> n > 0),
176    ;
177
178    /// This lemma is used in the proof of the roundtrip properties for optional and unbounded
179    /// repeating combinators.
180    proof fn lemma_serialize_productive(&self, v: Self::Type)
181        requires
182            self.requires(),
183            self.wf(v),
184        ensures
185            self.is_productive() ==> self.spec_serialize(v).len() > 0,
186    {
187        self.theorem_serialize_parse_roundtrip(v);
188        self.lemma_parse_productive(self.spec_serialize(v));
189    }
190}
191
192/// Implementation for parser and serializer combinators. A combinator's view must be a
193/// [`SecureSpecCombinator`].
194pub trait Combinator<'x, I, O>: View where
195    I: VestInput,
196    O: VestOutput<I>,
197    Self::V: SecureSpecCombinator<Type = <Self::Type as View>::V>,
198 {
199    /// The result type of parsing
200    type Type: View;
201
202    /// The input type of serialization, often a reference to [`Self::Type`].
203    /// For "structural" formats though (e.g., [`crate::regular::sequence::Pair`] and [`crate::regular::variant::Choice`]),
204    /// this is the tuple/sum of the corresponding [`Combinator::SType`] types.
205    type SType: View<V = <Self::Type as View>::V>;
206
207    /// The length of the output buffer.
208    /// This can be used to optimize serialization by pre-allocating the buffer.
209    fn length(&self, v: Self::SType) -> (len: usize)
210        requires
211            self@.requires(),
212            self.ex_requires(),
213            self@.wf(v@),
214            self@.spec_serialize(v@).len() <= usize::MAX,
215        ensures
216            len == self@.spec_serialize(v@).len(),
217    ;
218
219    /// Additional pre-conditions for parsing and serialization
220    ///
221    /// e.g., [`crate::regular::sequence::Pair`] combinator requires that the
222    ///   [`crate::regular::sequence::Continuation`] is well-formed w.r.t. the
223    ///   `spec_fn` closure.
224    open spec fn ex_requires(&self) -> bool {
225        true
226    }
227
228    /// The parsing function.
229    /// To enable "zero-copy" parsing, implementations of `parse` should not
230    /// consume/deepcopy the input buffer `I`, but rather return a slice of the
231    /// input buffer for `Self::Type` whenever possible.
232    /// See [`crate::buf_traits::VestInput`] and [`crate::buf_traits::VestPublicInput`] for
233    /// more details.
234    ///
235    /// ## Pre-conditions
236    ///
237    /// - [`SpecCombinator::requires`]
238    /// - [`Combinator::ex_requires`]
239    ///
240    /// ## Post-conditions
241    /// Essentially, the implementation of `parse` is functionally correct with respect to the
242    /// specification `spec_parse` on both success and failure cases.
243    fn parse(&self, s: I) -> (res: PResult<Self::Type, ParseError>)
244        requires
245            self@.requires(),
246            self.ex_requires(),
247            s@.len() <= usize::MAX,
248        ensures
249            res matches Ok((n, v)) ==> self@.spec_parse(s@) == Some((n as int, v@)),
250            self@.spec_parse(s@) matches Some((n, v)) ==> res matches Ok((m, u)) && m == n && v
251                == u@,
252            res is Err ==> self@.spec_parse(s@) is None,
253            self@.spec_parse(s@) is None ==> res is Err,
254    ;
255
256    /// The serialization function.
257    /// The intended use of `serialize` is to serialize a value `v` into the
258    /// buffer `buf` at the position `pos` "in-place" (i.e., without
259    /// allocating a new buffer or extending the buffer).
260    ///
261    /// ## Pre-conditions
262    ///
263    /// - [`SpecCombinator::requires`]
264    /// - [`Combinator::ex_requires`]
265    /// - [`SpecCombinator::wf`]
266    /// - `pos` is less than or equal to the length of the buffer, whose length
267    ///   is less than or equal to `usize::MAX`.
268    ///
269    /// ## Post-conditions
270    /// `serialize` ensures that it is functionally correct with respect to the
271    /// specification `spec_serialize` when it returns `Ok`. This is because
272    /// `serialize` being a partial function can fail (e.g.,
273    /// insufficient buffer space), while `spec_serialize` is a
274    /// total function (with infinite buffer size) and will never fail.
275    fn serialize(&self, v: Self::SType, buf: &mut O, pos: usize) -> (res: SResult<
276        usize,
277        SerializeError,
278    >)
279        requires
280            self@.requires(),
281            self.ex_requires(),
282            self@.wf(v@),
283            pos <= old(buf)@.len() <= usize::MAX,
284        ensures
285            res matches Ok(n) ==> {
286                &&& buf@.len() == old(buf)@.len()
287                &&& pos <= usize::MAX - n && pos + n <= buf@.len()
288                &&& n == self@.spec_serialize(v@).len()
289                &&& buf@ == seq_splice(old(buf)@, pos, self@.spec_serialize(v@))
290            },
291    ;
292}
293
294impl<C: SpecCombinator> SpecCombinator for &C {
295    type Type = C::Type;
296
297    open spec fn wf(&self, v: Self::Type) -> bool {
298        (*self).wf(v)
299    }
300
301    open spec fn requires(&self) -> bool {
302        (*self).requires()
303    }
304
305    open spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, Self::Type)> {
306        (*self).spec_parse(s)
307    }
308
309    open spec fn spec_serialize(&self, v: Self::Type) -> Seq<u8> {
310        (*self).spec_serialize(v)
311    }
312}
313
314impl<C: SecureSpecCombinator> SecureSpecCombinator for &C {
315    open spec fn is_prefix_secure() -> bool {
316        C::is_prefix_secure()
317    }
318
319    open spec fn is_productive(&self) -> bool {
320        (*self).is_productive()
321    }
322
323    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type) {
324        (*self).theorem_serialize_parse_roundtrip(v)
325    }
326
327    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
328        (*self).theorem_parse_serialize_roundtrip(buf)
329    }
330
331    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
332        (*self).lemma_prefix_secure(s1, s2)
333    }
334
335    proof fn lemma_parse_length(&self, s: Seq<u8>) {
336        (*self).lemma_parse_length(s)
337    }
338
339    proof fn lemma_parse_productive(&self, s: Seq<u8>) {
340        (*self).lemma_parse_productive(s)
341    }
342}
343
344impl<'x, I, O, C: Combinator<'x, I, O>> Combinator<'x, I, O> for &C where
345    I: VestInput,
346    O: VestOutput<I>,
347    C::V: SecureSpecCombinator<Type = <C::Type as View>::V>,
348 {
349    type Type = C::Type;
350
351    type SType = C::SType;
352
353    fn length(&self, v: Self::SType) -> usize {
354        assert(self.ex_requires());
355        (*self).length(v)
356    }
357
358    open spec fn ex_requires(&self) -> bool {
359        (*self).ex_requires()
360    }
361
362    fn parse(&self, s: I) -> (res: Result<(usize, Self::Type), ParseError>) {
363        (*self).parse(s)
364    }
365
366    fn serialize(&self, v: Self::SType, data: &mut O, pos: usize) -> (res: Result<
367        usize,
368        SerializeError,
369    >) {
370        (*self).serialize(v, data, pos)
371    }
372}
373
374impl<C: SpecCombinator> SpecCombinator for Box<C> {
375    type Type = C::Type;
376
377    open spec fn wf(&self, v: Self::Type) -> bool {
378        (**self).wf(v)
379    }
380
381    open spec fn requires(&self) -> bool {
382        (**self).requires()
383    }
384
385    open spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, Self::Type)> {
386        (**self).spec_parse(s)
387    }
388
389    open spec fn spec_serialize(&self, v: Self::Type) -> Seq<u8> {
390        (**self).spec_serialize(v)
391    }
392}
393
394impl<C: SecureSpecCombinator> SecureSpecCombinator for Box<C> {
395    open spec fn is_prefix_secure() -> bool {
396        C::is_prefix_secure()
397    }
398
399    open spec fn is_productive(&self) -> bool {
400        (**self).is_productive()
401    }
402
403    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type) {
404        (**self).theorem_serialize_parse_roundtrip(v)
405    }
406
407    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
408        (**self).theorem_parse_serialize_roundtrip(buf)
409    }
410
411    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
412        (**self).lemma_prefix_secure(s1, s2)
413    }
414
415    proof fn lemma_parse_length(&self, s: Seq<u8>) {
416        (**self).lemma_parse_length(s)
417    }
418
419    proof fn lemma_parse_productive(&self, s: Seq<u8>) {
420        (**self).lemma_parse_productive(s)
421    }
422}
423
424impl<'x, I, O, C: Combinator<'x, I, O>> Combinator<'x, I, O> for Box<C> where
425    I: VestInput,
426    O: VestOutput<I>,
427    C::V: SecureSpecCombinator<Type = <C::Type as View>::V>,
428 {
429    type Type = C::Type;
430
431    type SType = C::SType;
432
433    fn length(&self, v: Self::SType) -> usize {
434        (**self).length(v)
435    }
436
437    open spec fn ex_requires(&self) -> bool {
438        (**self).ex_requires()
439    }
440
441    fn parse(&self, s: I) -> (res: Result<(usize, Self::Type), ParseError>) {
442        (**self).parse(s)
443    }
444
445    fn serialize(&self, v: Self::SType, data: &mut O, pos: usize) -> (res: Result<
446        usize,
447        SerializeError,
448    >) {
449        (**self).serialize(v, data, pos)
450    }
451}
452
453// The following is an attempt to support `Fn`s as combinators.
454// I started implementing it because Verus doesn't support existential types (impl Trait) yet,
455// which is required to be able to put `Depend` combinator in the function's return type,
456// but more generally, I think it's probably also good to have a way in our framework to define
457// combinators as a group of (parsing and serializing) functions.
458//
459// Overall this is doable, but it's a bit tricky to implement because of the current limitations of Verus:
460// - Verus doesn't have general support for struct invariants yet, which means we have to add
461// pre-conditions to the security properties (i.e. the struct containing a pair of parsing and
462// serializing functions must be "well-formed" in some sense).
463// - Verus doesn't have general support for `&mut` types yet, which means for serialization we
464// cannot freely pass around the `&mut Vec<u8>`
465//
466// In theory, we could factor out all the lifetime parameters in `Combinator` trait and use generic
467// type parameters instead for both parsing and serialization, but that would require another
468// entire-codebase refactoring, which I think is not worth it at this point.
469//
470// #[verifier::reject_recursive_types(Type)]
471// pub struct SpecCombinatorFn<Type, const Prefix: u8> {
472//     pub parse: spec_fn(Seq<u8>) -> PResult<Type, ()>,
473//     pub serialize: spec_fn(Type) -> SResult<Seq<u8>, ()>,
474// }
475//
476// impl<Type, const Prefix: u8> SpecCombinatorFn<Type, Prefix> {
477//     pub open spec fn new(
478//         parse: spec_fn(Seq<u8>) -> PResult<Type, ()>,
479//         serialize: spec_fn(Type) -> SResult<Seq<u8>, ()>,
480//     ) -> (o: Self)
481//         recommends
482//             forall|v| Self::theorem_serialize_parse_roundtrip(parse, serialize, v),
483//             forall|buf| Self::theorem_parse_serialize_roundtrip(parse, serialize, buf),
484//             forall|s1, s2| Self::lemma_prefix_secure(parse, s1, s2),
485//     {
486//         Self { parse, serialize }
487//     }
488//
489//     pub open spec fn theorem_serialize_parse_roundtrip(
490//         parse: spec_fn(Seq<u8>) -> PResult<Type, ()>,
491//         serialize: spec_fn(Type) -> SResult<Seq<u8>, ()>,
492//         v: Type,
493//     ) -> bool {
494//         serialize(v) matches Ok(b) ==> parse(b) == Ok::<_, ()>((b.len() as usize, v))
495//     }
496//
497//     pub open spec fn theorem_parse_serialize_roundtrip(
498//         parse: spec_fn(Seq<u8>) -> Result<(usize, Type), ()>,
499//         serialize: spec_fn(Type) -> Result<Seq<u8>, ()>,
500//         buf: Seq<u8>,
501//     ) -> bool {
502//         buf.len() <= usize::MAX ==> ( parse(buf) matches Ok((n, v)) ==> serialize(v) == Ok::<
503//         _,
504//         (),
505//         >(buf.take(n as int)) )
506//     }
507//
508//     pub open spec fn lemma_prefix_secure(
509//         parse: spec_fn(Seq<u8>) -> Result<(usize, Type), ()>,
510//         s1: Seq<u8>,
511//         s2: Seq<u8>,
512//     ) -> bool {
513//         s1.len() + s2.len() <= usize::MAX && (Prefix == 1) ==>
514//         parse(s1) is Ok ==> parse(s1 + s2) == parse(s1)
515//     }
516// }
517//
518//
519// impl<Type, const Prefix: u8> SpecCombinator for SpecCombinatorFn<Type, Prefix> {
520//     type Type = Type;
521//
522//     open spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::Type), ()> {
523//         if let Ok((n, v)) = (self.parse)(s) {
524//             if n <= s.len() {
525//                 Ok((n, v))
526//             } else {
527//                 Err(())
528//             }
529//         } else {
530//             Err(())
531//         }
532//     }
533//
534//     open spec fn spec_serialize(&self, v: Self::Type) -> Result<Seq<u8>, ()> {
535//         (self.serialize)(v)
536//     }
537//
538//     proof fn spec_parse_wf(&self, s: Seq<u8>) {
539//     }
540// }
541//
542// impl<Type, const Prefix: u8> SecureSpecCombinator for SpecCombinatorFn<Type, Prefix> {
543//     open spec fn is_prefix_secure() -> bool {
544//         Prefix == 1
545//     }
546//
547//     proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type) {
548//         assume(Self::theorem_serialize_parse_roundtrip(self.parse, self.serialize, v));
549//     }
550//
551//     proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
552//         assume(Self::theorem_parse_serialize_roundtrip(self.parse, self.serialize, buf));
553//     }
554//
555//     proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
556//         assume(Self::lemma_prefix_secure(self.parse, s1, s2));
557//     }
558// }
559//
560// pub struct CombinatorFn<I, O, R, P, S, const Prefix: u8> where
561//     I: VestInput,
562//     O: VestOutput<I>,
563//     R: View,
564//     P: Continuation<I, Output = PResult<R, ParseError>>,
565//     S: for<'a> Continuation<(R, &'a mut O, usize), Output = SResult<usize, SerializeError>>,
566// {
567//     pub parse: P,
568//     pub serialize: S,
569//     pub spec_parse: Ghost<spec_fn(Seq<u8>) -> PResult<R::V, ()>>,
570//     pub spec_serialize: Ghost<spec_fn(R::V) -> SResult<Seq<u8>, ()>>,
571//     phantom: std::marker::PhantomData<(I, O)>,
572// }
573//
574// impl<'a, 'b, R, P, S, const Prefix: u8> View for CombinatorFn<'a, 'b, R, P, S, Prefix> where
575//     R: View,
576//     P: Fn(&'a [u8]) -> Result<(usize, R), ()>,
577//     S: Fn(R, &'b mut Vec<u8>, usize) -> Result<usize, ()>,
578// {
579//     type V = SpecCombinatorFn<R::V, Prefix>;
580//
581//     open spec fn view(&self) -> Self::V {
582//         let Ghost(parse) = self.spec_parse;
583//         let Ghost(serialize) = self.spec_serialize;
584//         SpecCombinatorFn {
585//             parse,
586//             serialize,
587//         }
588//     }
589// }
590//
591// impl<'a, 'b, R, P, S, const Prefix: u8> Combinator for CombinatorFn<'a, 'b, R, P, S, Prefix> where
592//     R: View,
593//     P: Fn(&'a [u8]) -> Result<(usize, R), ()>,
594//     S: Fn(R, &'b mut Vec<u8>, usize) -> Result<usize, ()>,
595//     Self::V: SecureSpecCombinator<Type = R::V>,
596//  {
597//     type Result<'c> = R;
598//
599//     type Owned = R;
600//
601//     open spec fn spec_length(&self) -> Option<usize> {
602//         None
603//     }
604//
605//     fn length(&self) -> Option<usize> {
606//         None
607//     }
608//
609//     fn exec_is_prefix_secure() -> bool {
610//         Prefix == 1
611//     }
612//
613//     fn parse<'c>(&self, s: &'c [u8]) -> Result<(usize, Self::Result<'c>), ()> where 'c: 'a {
614//         (self.parse)(s)
615//     }
616//
617//     fn serialize(&self, v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> Result<usize, ()> {
618//         (self.serialize)(v, data, pos)
619//     }
620// }
621} // verus!
622// ///////// Separating the parsing and serializing functions
623// ///////// Unsuccesful due to conflicting trait impls and Verus limitations (&mut support)
624// // pub trait Parser<I, O>
625// // where
626// //     I: VestInput,
627// // {
628// //     type Type;
629// //
630// //     fn parse_fn(&self, s: I) -> PResult<Self::Type, ParseError>;
631// // }
632// //
633// // pub trait Serializer<I, O>
634// // where
635// //     I: VestInput,
636// //     O: VestOutput<I>,
637// // {
638// //     type Type;
639// //
640// //     fn serialize_fn(
641// //         &self,
642// //         v: Self::Type,
643// //         data: &mut O,
644// //         pos: usize,
645// //     ) -> SResult<usize, SerializeError>;
646// // }
647// //
648// // impl<I, O, Type, F> Parser<I, O> for F
649// // where
650// //     I: VestInput,
651// //     F: Fn(I) -> PResult<Type, ParseError>,
652// // {
653// //     type Type = Type;
654// //
655// //     fn parse_fn(&self, s: I) -> PResult<Self::Type, ParseError> {
656// //         self(s)
657// //     }
658// // }
659// //
660// // impl<I, O, Fst, Snd> Parser<I, O> for (Fst, Snd)
661// // where
662// //     I: VestInput,
663// //     O: VestOutput<I>,
664// //     Fst: Combinator<I, O>,
665// //     Snd: Combinator<I, O>,
666// //     Fst::V: SecureSpecCombinator<Type = <Fst::Type as View>::V>,
667// //     Snd::V: SecureSpecCombinator<Type = <Snd::Type as View>::V>,
668// // {
669// //     type Type = (Fst::Type, Snd::Type);
670// //
671// //     fn parse_fn(&self, s: I) -> PResult<Self::Type, ParseError> {
672// //         (&self.0, &self.1).parse(s)
673// //     }
674// // }
675// //
676// // impl<I: VestPublicInput, O: VestPublicOutput<I>> Parser<I, O> for crate::regular::uints::U8 {
677// //     type Type = u8;
678// //
679// //     fn parse_fn(&self, s: I) -> PResult<Self::Type, ParseError> {
680// //         <_ as Combinator<I, O>>::parse(self, s)
681// //     }
682// // }
683// //
684// // fn parse_pair_of_u8<I, O>(s: I) -> PResult<(u8, u8), ParseError>
685// // where
686// //     I: VestPublicInput,
687// //     O: VestPublicOutput<I>,
688// // {
689// //     <_ as Parser<I, O>>::parse_fn(&(crate::regular::uints::U8, crate::regular::uints::U8), s)
690// // }
691// //
692// // fn test<I, O, P: Parser<I, O>>(p: P, s: I) -> PResult<P::Type, ParseError>
693// // where
694// //     I: VestPublicInput,
695// // {
696// //     p.parse_fn(s)
697// // }
698// //
699// // fn test2() {
700// //     let s = Vec::new();
701// //     let r = test::<_, Vec<u8>, _>(parse_pair_of_u8::<&[u8], Vec<u8>>, s.as_slice());
702// // }
703// // fn parse_pair<I, O, Fst, Snd>(
704// //     fst: Fst,
705// //     snd: Snd,
706// //     s: I,
707// // ) -> PResult<(Fst::Type, Snd::Type), ParseError>
708// // where
709// //     I: VestInput,
710// //     O: VestOutput<I>,
711// //     Fst: Parser<I, O>,
712// //     Snd: Parser<I, O>,
713// // {
714// //     // (fst, snd).parse(s)
715// // }
716// // impl<I, O, C: Combinator<I, O>> Parser<I, O> for C
717// // where
718// //     I: VestInput,
719// //     O: VestOutput<I>,
720// //     C::V: SecureSpecCombinator<Type = <C::Type as View>::V>,
721// // {
722// //     type Type = C::Type;
723// //
724// //     fn parse_fn(&self, s: I) -> PResult<Self::Type, ParseError> {
725// //         self.parse(s)
726// //     }
727// // }
728// // impl<I, O, C: Combinator<I, O>> Serializer<I, O> for C
729// // where
730// //     I: VestInput,
731// //     O: VestOutput<I>,
732// //     C::V: SecureSpecCombinator<Type = <C::Type as View>::V>,
733// // {
734// //     type Type = C::Type;
735// //
736// //     fn serialize_fn(
737// //         &self,
738// //         v: Self::Type,
739// //         data: &mut O,
740// //         pos: usize,
741// //     ) -> SResult<usize, SerializeError> {
742// //         self.serialize(v, data, pos)
743// //     }
744// // }
745// // fn parse_pair<I, O, Fst, Snd>(
746// //     fst: &Fst,
747// //     snd: &Snd,
748// //     s: I,
749// // ) -> PResult<(Fst::Type, Snd::Type), ParseError>
750// // where
751// //     I: VestInput,
752// //     O: VestOutput<I>,
753// //     Fst: Parser<I, Type = Fst::Type>,
754// //     Snd: Parser<I, Type = Snd::Type>,
755// // {
756// //     let (n, v1) = fst.parse(s.clone())?;
757// //     let s_ = s.subrange(n, s.len());
758// //     let (m, v2) = snd.parse(s_)?;
759// //     if let Some(nm) = n.checked_add(m) {
760// //         Ok((nm, (v1, v2)))
761// //     } else {
762// //         Err(ParseError::SizeOverflow)
763// //     }
764// // }
765// ///////// "Lazy" combinators (`dyn` not supported by Verus yet) to support recursive formats
766// // impl<C: View> View for dyn crate::regular::depend::Continuation<(), Output = C> {
767// //     type V = C::V;
768// //
769// //     // spec fn view(&self) -> Self::V;
770// // }
771// // impl<I, O, C: Combinator<I, O>> Combinator<I, O>
772// //     for Box<dyn crate::regular::depend::Continuation<(), Output = C>>
773// // where
774// //     I: VestInput,
775// //     O: VestOutput<I>,
776// //     C::V: SecureSpecCombinator<Type = <C::Type as View>::V>,
777// // {
778// //     type Type = Box<C::Type>;
779// //
780// //     fn length(&self) -> Option<usize> {
781// //         None
782// //     }
783// //
784// //     fn parse(&self, s: I) -> Result<(usize, Self::Type), ParseError> {
785// //         match self.apply(()).parse(s) {
786// //             Ok((n, v)) => Ok((n, Box::new(v))),
787// //             Err(e) => Err(e),
788// //         }
789// //     }
790// //
791// //     fn serialize(&self, v: Self::Type, data: &mut O, pos: usize) -> Result<usize, SerializeError> {
792// //         self.apply(()).serialize(*v, data, pos)
793// //     }
794// // }
795// //////// The following works, but currently we cannot verify it due to Verus limitations
796// // pub const INSTR_BASE: u8 = 0;
797// // pub const AUXBLOCK_BEGIN: u8 = 1;
798// // pub const AUXBLOCK_END: u8 = 11;
799// //
800// // #[derive(Debug)]
801// // struct InstrFmt(Either<u8, Box<AuxBlockFmt>>);
802// // #[derive(Debug)]
803// // struct AuxBlockFmt((u8, (RepeatResult<Box<InstrFmt>>, u8)));
804// //
805// // impl vstd::view::View for InstrFmt {
806// //     type V = Self;
807// // }
808// // impl vstd::view::View for AuxBlockFmt {
809// //     type V = Self;
810// // }
811// //
812// // struct InstrCom(
813// //     pub OrdChoice<Refined<U8, TagPred<u8>>, Box<dyn Continuation<(), Output = AuxBlockCom>>>,
814// // );
815// // struct AuxBlockCom(
816// //     pub  (
817// //         Refined<U8, TagPred<u8>>,
818// //         (
819// //             Star<Box<dyn Continuation<(), Output = InstrCom>>>,
820// //             Refined<U8, TagPred<u8>>,
821// //         ),
822// //     ),
823// // );
824// // impl vstd::view::View for InstrCom {
825// //     type V = Self;
826// // }
827// // impl vstd::view::View for AuxBlockCom {
828// //     type V = Self;
829// // }
830// // impl SpecCombinator for InstrCom {
831// //     type Type = InstrFmt;
832// // }
833// // impl SecureSpecCombinator for InstrCom {}
834// // impl SpecCombinator for AuxBlockCom {
835// //     type Type = AuxBlockFmt;
836// // }
837// // impl SecureSpecCombinator for AuxBlockCom {}
838// //
839// // impl DisjointFrom<Refined<U8, TagPred<u8>>> for AuxBlockCom {}
840// //
841// // impl<'a> Combinator<&'a [u8], Vec<u8>> for InstrCom {
842// //     type Type = InstrFmt;
843// //     fn length(&self) -> Option<usize> {
844// //         <_ as Combinator<&[u8], Vec<u8>>>::length(&self.0)
845// //     }
846// //     fn parse(&self, s: &'a [u8]) -> Result<(usize, Self::Type), ParseError> {
847// //         match <_ as Combinator<&[u8], Vec<u8>>>::parse(&self.0, s) {
848// //             Ok((n, Either::Left(v))) => Ok((n, InstrFmt(Either::Left(v)))),
849// //             Ok((n, Either::Right(v))) => Ok((n, InstrFmt(Either::Right(v)))),
850// //             Err(e) => Err(e),
851// //         }
852// //     }
853// //     fn serialize(
854// //         &self,
855// //         v: Self::Type,
856// //         data: &mut Vec<u8>,
857// //         pos: usize,
858// //     ) -> Result<usize, SerializeError> {
859// //         <_ as Combinator<&[u8], Vec<u8>>>::serialize(&self.0, v.0, data, pos)
860// //     }
861// // }
862// //
863// // impl<'a> Combinator<&'a [u8], Vec<u8>> for AuxBlockCom {
864// //     type Type = AuxBlockFmt;
865// //     fn length(&self) -> Option<usize> {
866// //         <_ as Combinator<&[u8], Vec<u8>>>::length(&self.0)
867// //     }
868// //     fn parse(&self, s: &'a [u8]) -> Result<(usize, Self::Type), ParseError> {
869// //         match <_ as Combinator<&[u8], Vec<u8>>>::parse(&self.0, s) {
870// //             Ok((n, (a, (b, c)))) => Ok((n, AuxBlockFmt((a, (b, c))))),
871// //             Err(e) => Err(e),
872// //         }
873// //     }
874// //     fn serialize(
875// //         &self,
876// //         v: Self::Type,
877// //         data: &mut Vec<u8>,
878// //         pos: usize,
879// //     ) -> Result<usize, SerializeError> {
880// //         <_ as Combinator<&[u8], Vec<u8>>>::serialize(&self.0, v.0, data, pos)
881// //     }
882// // }
883// //
884// // struct AuxBlockCont;
885// // struct InstrCont;
886// //
887// // impl Continuation<()> for AuxBlockCont {
888// //     type Output = AuxBlockCom;
889// //
890// //     fn apply(&self, i: ()) -> Self::Output {
891// //         AuxBlockCom((
892// //             Refined {
893// //                 inner: U8,
894// //                 predicate: TagPred(AUXBLOCK_BEGIN),
895// //             },
896// //             (
897// //                 Star(Box::new(InstrCont)),
898// //                 Refined {
899// //                     inner: U8,
900// //                     predicate: TagPred(AUXBLOCK_END),
901// //                 },
902// //             ),
903// //         ))
904// //     }
905// // }
906// //
907// // impl Continuation<()> for InstrCont {
908// //     type Output = InstrCom;
909// //
910// //     fn apply(&self, i: ()) -> Self::Output {
911// //         InstrCom(OrdChoice(
912// //             Refined {
913// //                 inner: U8,
914// //                 predicate: TagPred(INSTR_BASE),
915// //             },
916// //             Box::new(AuxBlockCont),
917// //         ))
918// //     }
919// // }
920// //
921// // fn test() {
922// //     // let buf = vec![0x00];
923// //     let buf = vec![0x01, 0, 0, 0x01, 0, 0, 0, 0x0B, 0, 0x0B];
924// //     let aux_block = AuxBlockCont.apply(());
925// //     let instr = InstrCont.apply(());
926// //     let (consumed, parsed) = instr.parse(&buf).unwrap_or_else(|e| {
927// //         panic!("Failed to parse: {}", e);
928// //     });
929// //     println!("consumed: {}", consumed);
930// //     println!("parsed: {:?}", parsed);
931// // }
932//
933// // Monomorphized approach to lazy combinators
934// // Would work if Verus fix https://github.com/verus-lang/verus/issues/1487
935// // use crate::regular::choice::Either;
936// // use crate::regular::choice::OrdChoice;
937// // use crate::regular::depend::Continuation;
938// // use crate::regular::disjoint::DisjointFrom;
939// // use crate::regular::refined::Refined;
940// // use crate::regular::repeat::RepeatResult;
941// // use crate::regular::star::Star;
942// // use crate::regular::tag::TagPred;
943// // use crate::regular::uints::U8;
944// // use crate::regular::map::Iso;
945// // use crate::regular::map::Mapped;
946// // use crate::regular::map::SpecIso;
947// //
948// // verus! {
949// //
950// // trait LazyCombinator {
951// //     type Comb: View;
952// //
953// //     spec fn spec_thunk(&self) -> Option<<Self::Comb as View>::V>;
954// //
955// //     fn thunk(&self) -> (o: Option<Self::Comb>) ensures o matches Some(c) ==> c@ == self.spec_thunk().unwrap();
956// // }
957// //
958// // struct LazyInstrCom(usize);
959// // struct LazyAuxBlockCom(usize);
960// //
961// // impl View for LazyInstrCom {
962// //     type V = Self;
963// //
964// //     open spec fn view(&self) -> Self::V {
965// //         *self
966// //     }
967// // }
968// //
969// // impl View for LazyAuxBlockCom {
970// //     type V = Self;
971// //
972// //     open spec fn view(&self) -> Self::V {
973// //         *self
974// //     }
975// // }
976// //
977// // impl LazyCombinator for LazyInstrCom {
978// //     type Comb = InstrCom;
979// //
980// //     closed spec fn spec_thunk(&self) -> Option<<InstrCom as View>::V> {
981// //         match self.0 {
982// //             0usize => None,
983// //             _ => Some(
984// //                 SpecInstrCom(
985// //                     Mapped {
986// //                         inner: OrdChoice(
987// //                             Refined { inner: U8, predicate: TagPred(INSTR_BASE) },
988// //                             LazyAuxBlockCom((self.0 - 1) as usize),
989// //                         ),
990// //                         mapper: InstrIso,
991// //                     },
992// //                 )
993// //             )
994// //         }
995// //     }
996// //
997// //     fn thunk(&self) -> Option<InstrCom> {
998// //         match self.0 {
999// //             0 => None,
1000// //             _ => Some(
1001// //                 InstrCom(
1002// //                     Mapped {
1003// //                         inner: OrdChoice(
1004// //                             Refined { inner: U8, predicate: TagPred(INSTR_BASE) },
1005// //                             LazyAuxBlockCom(self.0 - 1),
1006// //                         ),
1007// //                         mapper: InstrIso,
1008// //                     },
1009// //                 )
1010// //             )
1011// //         }
1012// //     }
1013// // }
1014// //
1015// // impl LazyCombinator for LazyAuxBlockCom {
1016// //     type Comb = AuxBlockCom;
1017// //
1018// //     closed spec fn spec_thunk(&self) -> Option<<AuxBlockCom as View>::V> {
1019// //         match self.0 {
1020// //             0usize => None,
1021// //             _ => Some(
1022// //                 SpecAuxBlockCom(
1023// //                     Mapped {
1024// //                         inner: (
1025// //                             Refined { inner: U8, predicate: TagPred(AUXBLOCK_BEGIN) },
1026// //                             (
1027// //                                 Star(LazyInstrCom((self.0 - 1) as usize)),
1028// //                                 Refined { inner: U8, predicate: TagPred(AUXBLOCK_END) },
1029// //                             ),
1030// //                         ),
1031// //                         mapper: AuxBlockIso,
1032// //                     },
1033// //                 )
1034// //             )
1035// //         }
1036// //     }
1037// //
1038// //     fn thunk(&self) -> Option<AuxBlockCom> {
1039// //         match self.0 {
1040// //             0 => None,
1041// //             _ => Some(
1042// //                 AuxBlockCom(
1043// //                     Mapped {
1044// //                         inner: (
1045// //                             Refined { inner: U8, predicate: TagPred(AUXBLOCK_BEGIN) },
1046// //                             (
1047// //                                 Star(LazyInstrCom(self.0 - 1)),
1048// //                                 Refined { inner: U8, predicate: TagPred(AUXBLOCK_END) },
1049// //                             ),
1050// //                         ),
1051// //                         mapper: AuxBlockIso,
1052// //                     },
1053// //                 )
1054// //             )
1055// //         }
1056// //     }
1057// // }
1058// //
1059// // impl SpecCombinator for LazyInstrCom {
1060// //     type Type = SpecInstrFmt;
1061// //
1062// //     closed spec fn spec_parse(&self, s: Seq<u8>) -> PResult<Self::Type, ()> {
1063// //         match self.spec_thunk() {
1064// //             Some(c) => c.spec_parse(s),
1065// //             None => Err(()),
1066// //         }
1067// //         // Self::spec_thunk().spec_parse(s)
1068// //     }
1069// //
1070// //     closed spec fn spec_serialize(&self, v: Self::Type) -> SResult<Seq<u8>, ()> {
1071// //         match self.spec_thunk() {
1072// //             Some(c) => c.spec_serialize(v),
1073// //             None => Err(()),
1074// //         }
1075// //         // Self::spec_thunk().spec_serialize(v)
1076// //     }
1077// // }
1078// //
1079// // impl SecureSpecCombinator for LazyInstrCom {
1080// //     closed spec fn is_prefix_secure() -> bool {
1081// //         <<Self as LazyCombinator>::Comb as View>::V::is_prefix_secure()
1082// //     }
1083// //
1084// //     closed spec fn is_productive(&self) -> bool {
1085// //         match self.spec_thunk() {
1086// //             Some(c) => c.is_productive(),
1087// //             None => false,
1088// //         }
1089// //     }
1090// //
1091// //     proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type) {
1092// //         match self.spec_thunk() {
1093// //             Some(c) => c.theorem_serialize_parse_roundtrip(v),
1094// //             None => {}
1095// //         }
1096// //     }
1097// //
1098// //     proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
1099// //         match self.spec_thunk() {
1100// //             Some(c) => c.theorem_parse_serialize_roundtrip(buf),
1101// //             None => {}
1102// //         }
1103// //     }
1104// //
1105// //     proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
1106// //         match self.spec_thunk() {
1107// //             Some(c) => c.lemma_prefix_secure(s1, s2),
1108// //             None => {}
1109// //         }
1110// //     }
1111// //
1112// //     proof fn lemma_parse_length(&self, s: Seq<u8>) {
1113// //         match self.spec_thunk() {
1114// //             Some(c) => c.lemma_parse_length(s),
1115// //             None => {}
1116// //         }
1117// //     }
1118// //
1119// //     proof fn lemma_parse_productive(&self, s: Seq<u8>) {
1120// //         match self.spec_thunk() {
1121// //             Some(c) => c.lemma_parse_productive(s),
1122// //             None => {}
1123// //         }
1124// //     }
1125// // }
1126// //
1127// // impl SpecCombinator for LazyAuxBlockCom {
1128// //     type Type = SpecAuxBlockFmt;
1129// //
1130// //     closed spec fn spec_parse(&self, s: Seq<u8>) -> PResult<Self::Type, ()> {
1131// //         match self.spec_thunk() {
1132// //             Some(c) => c.spec_parse(s),
1133// //             None => Err(()),
1134// //         }
1135// //     }
1136// //
1137// //     closed spec fn spec_serialize(&self, v: Self::Type) -> SResult<Seq<u8>, ()> {
1138// //         match self.spec_thunk() {
1139// //             Some(c) => c.spec_serialize(v),
1140// //             None => Err(()),
1141// //         }
1142// //     }
1143// // }
1144// //
1145// // impl SecureSpecCombinator for LazyAuxBlockCom {
1146// //     closed spec fn is_prefix_secure() -> bool {
1147// //         <<Self as LazyCombinator>::Comb as View>::V::is_prefix_secure()
1148// //     }
1149// //
1150// //     closed spec fn is_productive(&self) -> bool {
1151// //         match self.spec_thunk() {
1152// //             Some(c) => c.is_productive(),
1153// //             None => false,
1154// //         }
1155// //     }
1156// //
1157// //     proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type) {
1158// //         match self.spec_thunk() {
1159// //             Some(c) => c.theorem_serialize_parse_roundtrip(v),
1160// //             None => {}
1161// //         }
1162// //     }
1163// //
1164// //     proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
1165// //         match self.spec_thunk() {
1166// //             Some(c) => c.theorem_parse_serialize_roundtrip(buf),
1167// //             None => {}
1168// //         }
1169// //     }
1170// //
1171// //     proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
1172// //         match self.spec_thunk() {
1173// //             Some(c) => c.lemma_prefix_secure(s1, s2),
1174// //             None => {}
1175// //         }
1176// //     }
1177// //
1178// //     proof fn lemma_parse_length(&self, s: Seq<u8>) {
1179// //         match self.spec_thunk() {
1180// //             Some(c) => c.lemma_parse_length(s),
1181// //             None => {}
1182// //         }
1183// //     }
1184// //
1185// //     proof fn lemma_parse_productive(&self, s: Seq<u8>) {
1186// //         match self.spec_thunk() {
1187// //             Some(c) => c.lemma_parse_productive(s),
1188// //             None => {}
1189// //         }
1190// //     }
1191// // }
1192// //
1193// // impl DisjointFrom<Refined<U8, TagPred<u8>>> for LazyAuxBlockCom {
1194// //     closed spec fn disjoint_from(&self, other: &Refined<U8, TagPred<u8>>) -> bool {
1195// //         match self.spec_thunk() {
1196// //             Some(c) => c.0.inner.0.disjoint_from(other),
1197// //             None => false,
1198// //         }
1199// //         // Self::spec_thunk().0.inner.0.disjoint_from(other)
1200// //         // (self.0)().0.inner.0.disjoint_from(other)
1201// //     }
1202// //
1203// //     proof fn parse_disjoint_on(&self, other: &Refined<U8, TagPred<u8>>, buf: Seq<u8>) {
1204// //         match self.spec_thunk() {
1205// //             Some(c) => c.0.inner.0.parse_disjoint_on(other, buf),
1206// //             None => {}
1207// //         }
1208// //         // Self::spec_thunk().0.inner.0.parse_disjoint_on(other, buf)
1209// //         // (self.0)().0.inner.0.parse_disjoint_on(other, buf)
1210// //     }
1211// // }
1212// //
1213// // impl<'a> Combinator<&'a [u8], Vec<u8>> for LazyInstrCom
1214// // {
1215// //     type Type = Box<InstrFmt>;
1216// //
1217// //     closed spec fn spec_length(&self) -> Option<usize> {
1218// //         None
1219// //     }
1220// //
1221// //     fn length(&self) -> Option<usize> {
1222// //         None
1223// //     }
1224// //
1225// //     closed spec fn parse_requires(&self) -> bool {
1226// //         forall |c: <Self as LazyCombinator>::Comb| c.parse_requires()
1227// //     }
1228// //
1229// //     fn parse(&self, s: &[u8]) -> PResult<Self::Type, ParseError> {
1230// //         match self.thunk() {
1231// //             Some(c) => match c.parse(s) {
1232// //                 Ok((n, v)) => Ok((n, Box::new(v))),
1233// //                 Err(e) => Err(e),
1234// //             },
1235// //             None => Err(ParseError::Other("Ran out of fuels".to_string())),
1236// //         }
1237// //     }
1238// //
1239// //     closed spec fn serialize_requires(&self) -> bool {
1240// //         forall |c: <Self as LazyCombinator>::Comb| c.serialize_requires()
1241// //     }
1242// //
1243// //     fn serialize(&self, v: Self::Type, data: &mut Vec<u8>, pos: usize) -> SResult<usize, SerializeError> {
1244// //         match self.thunk() {
1245// //             Some(c) => c.serialize(*v, data, pos),
1246// //             None => Err(SerializeError::Other("Ran out of fuels".to_string())),
1247// //         }
1248// //     }
1249// // }
1250// //
1251// // impl<'a> Combinator<&'a [u8], Vec<u8>> for LazyAuxBlockCom
1252// // {
1253// //     type Type = Box<AuxBlockFmt>;
1254// //
1255// //     closed spec fn spec_length(&self) -> Option<usize> {
1256// //         None
1257// //     }
1258// //
1259// //     fn length(&self) -> Option<usize> {
1260// //         None
1261// //     }
1262// //
1263// //     closed spec fn parse_requires(&self) -> bool {
1264// //         forall |c: <Self as LazyCombinator>::Comb| c.parse_requires()
1265// //     }
1266// //
1267// //     fn parse(&self, s: &[u8]) -> PResult<Self::Type, ParseError> {
1268// //         match self.thunk() {
1269// //             Some(c) => match c.parse(s) {
1270// //                 Ok((n, v)) => Ok((n, Box::new(v))),
1271// //                 Err(e) => Err(e),
1272// //             },
1273// //             None => Err(ParseError::Other("Ran out of fuels".to_string())),
1274// //         }
1275// //     }
1276// //
1277// //     closed spec fn serialize_requires(&self) -> bool {
1278// //         forall |c: <Self as LazyCombinator>::Comb| c.serialize_requires()
1279// //     }
1280// //
1281// //     fn serialize(&self, v: Self::Type, data: &mut Vec<u8>, pos: usize) -> SResult<usize, SerializeError> {
1282// //         match self.thunk() {
1283// //             Some(c) => c.serialize(*v, data, pos),
1284// //             None => Err(SerializeError::Other("Ran out of fuels".to_string())),
1285// //         }
1286// //     }
1287// // }
1288// //
1289// //
1290// // // impl<T: SpecCombinator> SpecCombinator for spec_fn() -> T {
1291// // //     type Type = T::Type;
1292// // //
1293// // //     open spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::Type), ()> {
1294// // //         self().spec_parse(s)
1295// // //     }
1296// // //
1297// // //     open spec fn spec_serialize(&self, v: Self::Type) -> Result<Seq<u8>, ()> {
1298// // //         self().spec_serialize(v)
1299// // //     }
1300// // // }
1301// // //
1302// // // impl<T: SecureSpecCombinator> SecureSpecCombinator for spec_fn() -> T {
1303// // //     open spec fn is_prefix_secure() -> bool {
1304// // //         T::is_prefix_secure()
1305// // //     }
1306// // //
1307// // //     open spec fn is_productive(&self) -> bool {
1308// // //         self().is_productive()
1309// // //     }
1310// // //
1311// // //     proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type) {
1312// // //         self().theorem_serialize_parse_roundtrip(v)
1313// // //     }
1314// // //
1315// // //     proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
1316// // //         self().theorem_parse_serialize_roundtrip(buf)
1317// // //     }
1318// // //
1319// // //     proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
1320// // //         self().lemma_prefix_secure(s1, s2)
1321// // //     }
1322// // //
1323// // //     proof fn lemma_parse_length(&self, s: Seq<u8>) {
1324// // //         self().lemma_parse_length(s)
1325// // //     }
1326// // //
1327// // //     proof fn lemma_parse_productive(&self, s: Seq<u8>) {
1328// // //         self().lemma_parse_productive(s)
1329// // //     }
1330// // // }
1331// //
1332// //
1333// // pub const INSTR_BASE: u8 = 0;
1334// //
1335// // pub const AUXBLOCK_BEGIN: u8 = 1;
1336// //
1337// // pub const AUXBLOCK_END: u8 = 11;
1338// //
1339// // ghost enum SpecInstrFmt {
1340// //     Base(u8),
1341// //     Block(SpecAuxBlockFmt),
1342// // }
1343// //
1344// // type SpecInstrFmtAlias = Either<u8, SpecAuxBlockFmt>;
1345// //
1346// // ghost struct SpecAuxBlockFmt {
1347// //     begin: u8,
1348// //     instrs: Seq<SpecInstrFmt>,
1349// //     end: u8,
1350// // }
1351// //
1352// // type SpecAuxBlockFmtAlias = (u8, (Seq<SpecInstrFmt>, u8));
1353// //
1354// // #[derive(Debug)]
1355// // enum InstrFmt {
1356// //     Base(u8),
1357// //     Block(Box<AuxBlockFmt>),
1358// // }
1359// //
1360// // type InstrFmtAlias = Either<u8, Box<AuxBlockFmt>>;
1361// //
1362// // #[derive(Debug)]
1363// // struct AuxBlockFmt {
1364// //     begin: u8,
1365// //     instrs: RepeatResult<Box<InstrFmt>>,
1366// //     end: u8,
1367// // }
1368// //
1369// // type AuxBlockFmtAlias = (u8, (RepeatResult<Box<InstrFmt>>, u8));
1370// //
1371// // impl View for InstrFmt {
1372// //     type V = SpecInstrFmt;
1373// //
1374// //     closed spec fn view(&self) -> Self::V {
1375// //         match self {
1376// //             InstrFmt::Base(v) => SpecInstrFmt::Base(*v),
1377// //             InstrFmt::Block(v) => SpecInstrFmt::Block(v@),
1378// //         }
1379// //     }
1380// // }
1381// //
1382// // impl View for AuxBlockFmt {
1383// //     type V = SpecAuxBlockFmt;
1384// //
1385// //     closed spec fn view(&self) -> Self::V {
1386// //         SpecAuxBlockFmt { begin: self.begin, instrs: self.instrs.view(), end: self.end }
1387// //     }
1388// // }
1389// //
1390// // impl SpecFrom<SpecInstrFmtAlias> for SpecInstrFmt {
1391// //     closed spec fn spec_from(v: SpecInstrFmtAlias) -> Self {
1392// //         match v {
1393// //             Either::Left(v) => SpecInstrFmt::Base(v),
1394// //             Either::Right(v) => SpecInstrFmt::Block(v),
1395// //         }
1396// //     }
1397// // }
1398// //
1399// // impl SpecFrom<SpecInstrFmt> for SpecInstrFmtAlias {
1400// //     closed spec fn spec_from(v: SpecInstrFmt) -> Self {
1401// //         match v {
1402// //             SpecInstrFmt::Base(v) => Either::Left(v),
1403// //             SpecInstrFmt::Block(v) => Either::Right(v),
1404// //         }
1405// //     }
1406// // }
1407// //
1408// // impl SpecFrom<SpecAuxBlockFmtAlias> for SpecAuxBlockFmt {
1409// //     closed spec fn spec_from(v: SpecAuxBlockFmtAlias) -> Self {
1410// //         let (begin, (instrs, end)) = v;
1411// //         SpecAuxBlockFmt { begin, instrs, end }
1412// //     }
1413// // }
1414// //
1415// // impl SpecFrom<SpecAuxBlockFmt> for SpecAuxBlockFmtAlias {
1416// //     closed spec fn spec_from(v: SpecAuxBlockFmt) -> Self {
1417// //         (v.begin, (v.instrs, v.end))
1418// //     }
1419// // }
1420// //
1421// // impl From<InstrFmtAlias> for InstrFmt {
1422// //     fn ex_from(v: InstrFmtAlias) -> Self {
1423// //         match v {
1424// //             Either::Left(v) => InstrFmt::Base(v),
1425// //             Either::Right(v) => InstrFmt::Block(v),
1426// //         }
1427// //     }
1428// // }
1429// //
1430// // impl From<InstrFmt> for InstrFmtAlias {
1431// //     fn ex_from(v: InstrFmt) -> Self {
1432// //         match v {
1433// //             InstrFmt::Base(v) => Either::Left(v),
1434// //             InstrFmt::Block(v) => Either::Right(v),
1435// //         }
1436// //     }
1437// // }
1438// //
1439// // impl From<AuxBlockFmtAlias> for AuxBlockFmt {
1440// //     fn ex_from(v: AuxBlockFmtAlias) -> Self {
1441// //         let (begin, (instrs, end)) = v;
1442// //         AuxBlockFmt { begin, instrs, end }
1443// //     }
1444// // }
1445// //
1446// // impl From<AuxBlockFmt> for AuxBlockFmtAlias {
1447// //     fn ex_from(v: AuxBlockFmt) -> Self {
1448// //         (v.begin, (v.instrs, v.end))
1449// //     }
1450// // }
1451// //
1452// // struct InstrIso;
1453// //
1454// // impl View for InstrIso {
1455// //     type V = Self;
1456// //
1457// //     closed spec fn view(&self) -> Self::V {
1458// //         InstrIso
1459// //     }
1460// // }
1461// //
1462// // impl SpecIso for InstrIso {
1463// //     type Src = SpecInstrFmtAlias;
1464// //
1465// //     type Dst = SpecInstrFmt;
1466// //
1467// //     proof fn spec_iso(s: Self::Src) {
1468// //     }
1469// //
1470// //     proof fn spec_iso_rev(s: Self::Dst) {
1471// //     }
1472// // }
1473// //
1474// // impl Iso for InstrIso {
1475// //     type Src = InstrFmtAlias;
1476// //
1477// //     type Dst = InstrFmt;
1478// // }
1479// //
1480// // struct AuxBlockIso;
1481// //
1482// // impl View for AuxBlockIso {
1483// //     type V = Self;
1484// //
1485// //     closed spec fn view(&self) -> Self::V {
1486// //         AuxBlockIso
1487// //     }
1488// // }
1489// //
1490// // impl SpecIso for AuxBlockIso {
1491// //     type Src = SpecAuxBlockFmtAlias;
1492// //
1493// //     type Dst = SpecAuxBlockFmt;
1494// //
1495// //     proof fn spec_iso(s: Self::Src) {
1496// //     }
1497// //
1498// //     proof fn spec_iso_rev(s: Self::Dst) {
1499// //     }
1500// // }
1501// //
1502// // impl Iso for AuxBlockIso {
1503// //     type Src = AuxBlockFmtAlias;
1504// //
1505// //     type Dst = AuxBlockFmt;
1506// // }
1507// //
1508// // struct InstrCom(pub Mapped<OrdChoice<Refined<U8, TagPred<u8>>, LazyAuxBlockCom>, InstrIso>);
1509// //
1510// // struct AuxBlockCom(
1511// //     pub Mapped<
1512// //         (Refined<U8, TagPred<u8>>, (Star<LazyInstrCom>, Refined<U8, TagPred<u8>>)),
1513// //         AuxBlockIso,
1514// //     >,
1515// // );
1516// //
1517// // struct SpecInstrCom(pub SpecInstrComInner);
1518// //
1519// // struct SpecAuxBlockCom(pub SpecAuxBlockComInner);
1520// //
1521// // type SpecInstrComInner = Mapped<
1522// //     OrdChoice<Refined<U8, TagPred<u8>>, LazyAuxBlockCom>,
1523// //     InstrIso,
1524// // >;
1525// //
1526// // type SpecAuxBlockComInner = Mapped<
1527// //     (Refined<U8, TagPred<u8>>, (Star<LazyInstrCom>, Refined<U8, TagPred<u8>>)),
1528// //     AuxBlockIso,
1529// // >;
1530// //
1531// // impl View for InstrCom {
1532// //     type V = SpecInstrCom;
1533// //
1534// //     closed spec fn view(&self) -> Self::V {
1535// //         SpecInstrCom(self.0@)
1536// //     }
1537// // }
1538// //
1539// // impl View for AuxBlockCom {
1540// //     type V = SpecAuxBlockCom;
1541// //
1542// //     closed spec fn view(&self) -> Self::V {
1543// //         SpecAuxBlockCom(self.0@)
1544// //     }
1545// // }
1546// //
1547// // impl SpecCombinator for SpecInstrCom {
1548// //     type Type = SpecInstrFmt;
1549// //
1550// //     closed spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::Type), ()> {
1551// //         self.0.spec_parse(s)
1552// //     }
1553// //
1554// //     closed spec fn spec_serialize(&self, v: Self::Type) -> Result<Seq<u8>, ()> {
1555// //         self.0.spec_serialize(v)
1556// //     }
1557// // }
1558// //
1559// // impl SecureSpecCombinator for SpecInstrCom {
1560// //     open spec fn is_prefix_secure() -> bool {
1561// //         SpecInstrComInner::is_prefix_secure()
1562// //     }
1563// //
1564// //     open spec fn is_productive(&self) -> bool {
1565// //         self.0.is_productive()
1566// //     }
1567// //
1568// //     proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type) {
1569// //         // self.0.theorem_serialize_parse_roundtrip(v.0)
1570// //         self.0.theorem_serialize_parse_roundtrip(v)
1571// //     }
1572// //
1573// //     proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
1574// //         self.0.theorem_parse_serialize_roundtrip(buf)
1575// //     }
1576// //
1577// //     proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
1578// //         self.0.lemma_prefix_secure(s1, s2)
1579// //     }
1580// //
1581// //     proof fn lemma_parse_length(&self, s: Seq<u8>) {
1582// //         self.0.lemma_parse_length(s)
1583// //     }
1584// //
1585// //     proof fn lemma_parse_productive(&self, s: Seq<u8>) {
1586// //         self.0.lemma_parse_productive(s)
1587// //     }
1588// // }
1589// //
1590// // impl SpecCombinator for SpecAuxBlockCom {
1591// //     type Type = SpecAuxBlockFmt;
1592// //
1593// //     closed spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::Type), ()> {
1594// //         self.0.spec_parse(s)
1595// //     }
1596// //
1597// //     closed spec fn spec_serialize(&self, v: Self::Type) -> Result<Seq<u8>, ()> {
1598// //         self.0.spec_serialize(v)
1599// //     }
1600// // }
1601// //
1602// // impl SecureSpecCombinator for SpecAuxBlockCom {
1603// //     open spec fn is_prefix_secure() -> bool {
1604// //         SpecAuxBlockComInner::is_prefix_secure()
1605// //     }
1606// //
1607// //     open spec fn is_productive(&self) -> bool {
1608// //         self.0.is_productive()
1609// //     }
1610// //
1611// //     proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type) {
1612// //         self.0.theorem_serialize_parse_roundtrip(v)
1613// //
1614// //     }
1615// //
1616// //     proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
1617// //         self.0.theorem_parse_serialize_roundtrip(buf)
1618// //     }
1619// //
1620// //     proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
1621// //         self.0.lemma_prefix_secure(s1, s2)
1622// //     }
1623// //
1624// //     proof fn lemma_parse_length(&self, s: Seq<u8>) {
1625// //         self.0.lemma_parse_length(s)
1626// //     }
1627// //
1628// //     proof fn lemma_parse_productive(&self, s: Seq<u8>) {
1629// //         self.0.lemma_parse_productive(s)
1630// //     }
1631// // }
1632// //
1633// // // impl DisjointFrom<Refined<U8, TagPred<u8>>> for SpecAuxBlockCont {
1634// // //     closed spec fn disjoint_from(&self, other: &Refined<U8, TagPred<u8>>) -> bool {
1635// // //         (self.0)().0.inner.0.disjoint_from(other)
1636// // //     }
1637// // //
1638// // //     proof fn parse_disjoint_on(&self, other: &Refined<U8, TagPred<u8>>, buf: Seq<u8>) {
1639// // //         (self.0)().0.inner.0.parse_disjoint_on(other, buf)
1640// // //     }
1641// // // }
1642// //
1643// // // impl DisjointFrom<Refined<U8, TagPred<u8>>> for SpecInstrCom {}
1644// // impl<'a> Combinator<&'a [u8], Vec<u8>> for InstrCom {
1645// //     type Type = InstrFmt;
1646// //
1647// //     open spec fn spec_length(&self) -> Option<usize> {
1648// //         None
1649// //     }
1650// //
1651// //     fn length(&self) -> Option<usize> {
1652// //         None
1653// //     }
1654// //
1655// //     fn parse(&self, s: &'a [u8]) -> Result<(usize, Self::Type), ParseError> {
1656// //         <_ as Combinator<&[u8], Vec<u8>>>::parse(
1657// //             &self.0,
1658// //             s,
1659// //         )
1660// //     }
1661// //
1662// //     fn serialize(&self, v: Self::Type, data: &mut Vec<u8>, pos: usize) -> Result<
1663// //         usize,
1664// //         SerializeError,
1665// //     > {
1666// //         <_ as Combinator<&[u8], Vec<u8>>>::serialize(&self.0, v, data, pos)
1667// //     }
1668// // }
1669// //
1670// // impl<'a> Combinator<&'a [u8], Vec<u8>> for AuxBlockCom {
1671// //     type Type = AuxBlockFmt;
1672// //
1673// //     open spec fn spec_length(&self) -> Option<usize> {
1674// //         None
1675// //     }
1676// //
1677// //     fn length(&self) -> Option<usize> {
1678// //         None
1679// //     }
1680// //
1681// //     fn parse(&self, s: &'a [u8]) -> Result<(usize, Self::Type), ParseError> {
1682// //         <_ as Combinator<&[u8], Vec<u8>>>::parse(
1683// //             &self.0,
1684// //             s,
1685// //         )
1686// //     }
1687// //
1688// //     fn serialize(&self, v: Self::Type, data: &mut Vec<u8>, pos: usize) -> Result<
1689// //         usize,
1690// //         SerializeError,
1691// //     > {
1692// //         <_ as Combinator<&[u8], Vec<u8>>>::serialize(&self.0, v, data, pos)
1693// //     }
1694// // }
1695// //
1696// // } // verus!
vest_lib/properties.rs

vest_lib/
properties.rs
