vest_lib/combinators/bytes/
mod.rs

1//! Fixed- and value-dependent byte sequence combinators.
2//!
3//! Use [`Fixed`] for a compile-time length, [`Varied`] for a runtime length,
4//! and [`ExactLen`] to confine another format to a bounded byte region.
5/// Executable trait implementations for this combinator.
6pub mod exec;
7/// Correctness proofs for this combinator.
8pub mod proof;
9/// Specification trait implementations for this combinator.
10pub mod spec;
11
12use crate::core::proof::LeafNonMalleable;
13use vstd::prelude::*;
14
15use super::AsLen;
16
17verus! {
18
19/// Parses/serializes exactly `N` bytes as `Seq<u8>`.
20#[derive(Clone, Copy)]
21pub struct Fixed<const N: usize>;
22
23/// Parses/serializes a variable-length byte sequence `Seq<u8>`.
24///
25/// The length is determined by `self.0`, which must implement [`super::length::AsLen`] and
26/// defaults to `u8`.
27///
28/// ## Consistency
29///
30/// A byte sequence is consistent w.r.t `Varied` iff its length equals `self.0`.
31#[derive(Copy)]
32pub struct Varied<Len = u8>(pub Len);
33
34impl<Len: Clone> Clone for Varied<Len> {
35    fn clone(&self) -> (cloned: Self)
36        ensures
37            call_ensures(Len::clone, (&self.0,), cloned.0),
38    {
39        Varied(self.0.clone())
40    }
41}
42
43/// Wraps an inner combinator, constraining it to consume/produce exactly `self.0` bytes.
44///
45/// Implemented as `AndThen(Varied(self.0), self.1)`.
46///
47/// ## Consistency
48///
49/// A value of type `Inner::Val` is consistent w.r.t `ExactLen` iff it is consistent w.r.t `Inner` and
50/// its byte length given by `Inner` equals `self.0`.
51#[derive(Copy)]
52pub struct ExactLen<Inner, Len = u8>(pub Len, pub Inner);
53
54impl<Inner: Clone, Len: Clone> Clone for ExactLen<Inner, Len> {
55    fn clone(&self) -> (cloned: Self)
56        ensures
57            call_ensures(Len::clone, (&self.0,), cloned.0),
58            call_ensures(Inner::clone, (&self.1,), cloned.1),
59    {
60        ExactLen(self.0.clone(), self.1.clone())
61    }
62}
63
64/// Run a [bytes combinator](crate::core::spec::BytesCombinator) `A` and then
65/// re-interpret the *entire* bytes consumed/produced by `A` with another combinator `B`.
66///
67/// ## Consistency
68///
69/// A value of type `B::Val` is consistent w.r.t `AndThen<A, B>` iff there exists a value of type
70/// `A::Val` that is consistent w.r.t `A` and whose byte length equals the byte length of the `B::Val` value w.r.t `B`.
71/// Prefer [`ExactLen`] over `AndThen` to avoid the existential reasoning in the consistency condition.
72#[derive(Copy)]
73pub struct AndThen<A, B>(pub A, pub B);
74
75impl<A: Clone, B: Clone> Clone for AndThen<A, B> {
76    fn clone(&self) -> (cloned: Self)
77        ensures
78            call_ensures(A::clone, (&self.0,), cloned.0),
79            call_ensures(B::clone, (&self.1,), cloned.1),
80    {
81        AndThen(self.0.clone(), self.1.clone())
82    }
83}
84
85impl<const N: usize> LeafNonMalleable for Fixed<N> {
86    proof fn nonmal_leaf_inv(&self) {
87    }
88}
89
90impl<Len: AsLen> LeafNonMalleable for Varied<Len> {
91    proof fn nonmal_leaf_inv(&self) {
92    }
93}
94
95} // verus!
vest_lib/combinators/bytes/mod.rs

vest_lib/combinators/bytes/
mod.rs
