vest_lib/combinators/bytes/
exec.rs

1//! Executable implementations for fixed- and variable-length bytes.
2use crate::combinators::{AsLen, Tail};
3use crate::core::exec::input::{InputBuf, InputSlice};
4use crate::core::exec::output::*;
5use crate::core::exec::{
6    parser::{PResult, Parser},
7    serializer::{ByteLen, ComplianceErrorKind, PreSerializeError, Prepare, Serializer},
8    ParseError,
9};
10use crate::core::spec::{Consistency, SpecByteLen, SpecParser};
11use vstd::prelude::*;
12use OutputBuf;
13
14verus! {
15
16/// Opaque view of `core`'s slice-to-array conversion error.
17#[verifier::external_type_specification]
18#[verifier::external_body]
19pub struct ExTryFromSliceError(core::array::TryFromSliceError);
20
21/// Specification for `core`'s borrowing slice-to-array conversion.
22pub assume_specification<'a, T, const N: usize>[ <&'a [T; N] as TryFrom<&'a [T]>>::try_from ](
23    slice: &'a [T],
24) -> (res: Result<&'a [T; N], core::array::TryFromSliceError>)
25    ensures
26        slice@.len() == N ==> res is Ok && res->Ok_0@ == slice@,
27        slice@.len() != N ==> res is Err,
28;
29
30impl<const N: usize, I: InputBuf> Parser<I> for super::Fixed<N> {
31    type PT = I;
32
33    fn min_byte_len(&self) -> usize {
34        N
35    }
36
37    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
38        if ibuf.len() < N {
39            Err(ParseError::unexpected_eof())
40        } else {
41            Ok((N, ibuf.take(N)))
42        }
43    }
44}
45
46impl<Output: OutputBuf, const N: usize> Serializer<Output, [u8]> for super::Fixed<N> {
47    #[inline(always)]
48    fn serialize_into(&self, v: &[u8], obuf: &mut Output) {
49        // `consistent(v)` fixes the length to `N`, but only at the proof level.
50        // We recover the array type from the slice to help with compiler optimizations.
51        let fixed = <&[u8; N]>::try_from(v).unwrap();
52        obuf.write_array(fixed);
53    }
54}
55
56impl<'i, Output: OutputBuf, const N: usize> Serializer<Output, &'i [u8]> for super::Fixed<N> {
57    #[inline(always)]
58    fn serialize_into(&self, v: &&'i [u8], obuf: &mut Output) {
59        let fixed = <&[u8; N]>::try_from(*v).unwrap();
60        obuf.write_array(fixed);
61    }
62}
63
64impl<Output: OutputBuf, const N: usize> Serializer<Output, [u8; N]> for super::Fixed<N> {
65    #[inline(always)]
66    fn serialize_into(&self, v: &[u8; N], obuf: &mut Output) {
67        obuf.write_array(v);
68    }
69}
70
71// impl<Output: OutputBuf, const N: usize> Serializer<Output, [u8; N]> for super::Fixed<N> {
72//     fn ex_serialize(&self, v: &[u8; N], obuf: &mut Output) {
73//         obuf.write_bytes(v);
74//     }
75// }
76impl<const N: usize> ByteLen<[u8]> for super::Fixed<N> {
77    fn length(&self, v: &[u8]) -> (len: usize) {
78        v.len()
79    }
80}
81
82impl<'i, const N: usize> ByteLen<&'i [u8]> for super::Fixed<N> {
83    fn length(&self, v: &&'i [u8]) -> (len: usize) {
84        v.len()
85    }
86}
87
88impl<const N: usize> Prepare<[u8]> for super::Fixed<N> {
89    fn prepare(&self, v: &[u8]) -> (checked: Result<usize, PreSerializeError>) {
90        if v.len() == N {
91            Ok(N)
92        } else {
93            Err(PreSerializeError::not_compliant(ComplianceErrorKind::LengthInconsistent))
94        }
95    }
96}
97
98impl<'i, const N: usize> Prepare<&'i [u8]> for super::Fixed<N> {
99    fn prepare(&self, v: &&'i [u8]) -> (checked: Result<usize, PreSerializeError>) {
100        if v.len() == N {
101            Ok(N)
102        } else {
103            Err(PreSerializeError::not_compliant(ComplianceErrorKind::LengthInconsistent))
104        }
105    }
106}
107
108impl<Len: AsLen, I: InputBuf> Parser<I> for super::Varied<Len> {
109    type PT = I;
110
111    fn min_byte_len(&self) -> usize {
112        self.0.get()
113    }
114
115    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
116        let len = self.0.get();
117        if ibuf.len() < len {
118            Err(ParseError::unexpected_eof())
119        } else {
120            Ok((len, ibuf.take(len)))
121        }
122    }
123}
124
125impl<Output: OutputBuf, Len: AsLen> Serializer<Output, [u8]> for super::Varied<Len> {
126    fn serialize_into(&self, v: &[u8], obuf: &mut Output) {
127        obuf.write_bytes(v);
128    }
129}
130
131impl<'i, Output: OutputBuf, Len: AsLen> Serializer<Output, &'i [u8]> for super::Varied<Len> {
132    fn serialize_into(&self, v: &&'i [u8], obuf: &mut Output) {
133        obuf.write_bytes(*v);
134    }
135}
136
137impl<Len: AsLen> ByteLen<[u8]> for super::Varied<Len> {
138    fn length(&self, v: &[u8]) -> (len: usize) {
139        v.len()
140    }
141}
142
143impl<'i, Len: AsLen> ByteLen<&'i [u8]> for super::Varied<Len> {
144    fn length(&self, v: &&'i [u8]) -> (len: usize) {
145        v.len()
146    }
147}
148
149impl<Len: AsLen> Prepare<[u8]> for super::Varied<Len> {
150    fn prepare(&self, v: &[u8]) -> (checked: Result<usize, PreSerializeError>) {
151        if v.len() == self.0.get() {
152            Ok(v.len())
153        } else {
154            Err(PreSerializeError::not_compliant(ComplianceErrorKind::LengthInconsistent))
155        }
156    }
157}
158
159impl<'i, Len: AsLen> Prepare<&'i [u8]> for super::Varied<Len> {
160    fn prepare(&self, v: &&'i [u8]) -> (checked: Result<usize, PreSerializeError>) {
161        if v.len() == self.0.get() {
162            Ok(v.len())
163        } else {
164            Err(PreSerializeError::not_compliant(ComplianceErrorKind::LengthInconsistent))
165        }
166    }
167}
168
169impl<I, Len, Inner> Parser<I> for super::ExactLen<Inner, Len> where
170    I: InputBuf,
171    Len: AsLen,
172    Inner: Parser<I>,
173 {
174    type PT = Inner::PT;
175
176    fn min_byte_len(&self) -> usize {
177        self.0.get()
178    }
179
180    open spec fn exec_inv(&self) -> bool {
181        self.1.exec_inv()
182    }
183
184    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
185        super::AndThen(super::Varied(self.0), &self.1).parse(ibuf)
186    }
187}
188
189impl<I: InputBuf, A, Then> Parser<I> for super::AndThen<A, Then> where
190    A: Parser<I, PT = I, PVal = Seq<u8>>,
191    Then: Parser<I>,
192 {
193    type PT = Then::PT;
194
195    fn min_byte_len(&self) -> usize {
196        self.0.min_byte_len()
197    }
198
199    open spec fn exec_inv(&self) -> bool {
200        &&& self.0.exec_inv()
201        &&& self.1.exec_inv()
202    }
203
204    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
205        assert(self.exec_inv());
206
207        let (len_a, chunk) = self.0.parse(ibuf)?;
208        proof {
209            chunk.deep_view_eq_view();
210        }
211        let (len_b, v) = self.1.parse(&chunk)?;
212        if len_b == len_a {
213            Ok((len_b, v))
214        } else {
215            Err(ParseError::length_mismatch())
216        }
217    }
218}
219
220impl<Output: OutputBuf, Len, Inner, T> Serializer<Output, T> for super::ExactLen<Inner, Len> where
221    Len: AsLen,
222    T: DeepView + ?Sized,
223    Inner: Serializer<Output, T> + SpecByteLen<T = T::V>,
224 {
225    #[verifier::prophetic]
226    open spec fn exec_inv(&self) -> bool {
227        self.1.exec_inv()
228    }
229
230    fn serialize_into(&self, v: &T, obuf: &mut Output) {
231        self.1.serialize_into(v, obuf);
232    }
233}
234
235impl<Output: OutputBuf, Then, T> Serializer<Output, T> for super::AndThen<Tail, Then> where
236    T: DeepView + ?Sized,
237    Then: Serializer<Output, T>,
238 {
239    #[verifier::prophetic]
240    open spec fn exec_inv(&self) -> bool {
241        self.1.exec_inv()
242    }
243
244    fn serialize_into(&self, v: &T, obuf: &mut Output) {
245        self.1.serialize_into(v, obuf);
246    }
247}
248
249impl<Len, Inner, InnerST> ByteLen<InnerST> for super::ExactLen<Inner, Len> where
250    Len: AsLen,
251    InnerST: DeepView + ?Sized,
252    Inner: ByteLen<InnerST>,
253 {
254    open spec fn exec_inv(&self) -> bool {
255        self.1.exec_inv()
256    }
257
258    fn length(&self, v: &InnerST) -> (len: usize) {
259        self.1.length(v)
260    }
261}
262
263impl<Len, Inner, InnerST> Prepare<InnerST> for super::ExactLen<Inner, Len> where
264    Len: AsLen,
265    InnerST: DeepView + ?Sized,
266    Inner: Prepare<InnerST>,
267 {
268    open spec fn exec_inv(&self) -> bool {
269        self.1.exec_inv()
270    }
271
272    fn prepare(&self, v: &InnerST) -> (checked: Result<usize, PreSerializeError>) {
273        let len = self.1.prepare(v)?;
274        if len == self.0.get() {
275            Ok(len)
276        } else {
277            Err(PreSerializeError::not_compliant(ComplianceErrorKind::LengthInconsistent))
278        }
279    }
280}
281
282impl<Then, T> Prepare<T> for super::AndThen<Tail, Then> where
283    T: DeepView + ?Sized,
284    Then: Prepare<T>,
285 {
286    open spec fn exec_inv(&self) -> bool {
287        self.1.exec_inv()
288    }
289
290    fn prepare(&self, v: &T) -> (checked: Result<usize, PreSerializeError>) {
291        let len = self.1.prepare(v)?;
292        proof {
293            let chunk = Seq::new(len as nat, |_i| 0u8);
294            assert(self.0.consistent(chunk));
295        }
296        Ok(len)
297    }
298}
299
300impl<A, Then, ThenST> ByteLen<ThenST> for super::AndThen<A, Then> where
301    ThenST: DeepView + ?Sized,
302    Then: ByteLen<ThenST>,
303 {
304    open spec fn exec_inv(&self) -> bool {
305        self.1.exec_inv()
306    }
307
308    fn length(&self, v: &ThenST) -> (len: usize) {
309        self.1.length(v)
310    }
311}
312
313} // verus!
vest_lib/combinators/bytes/exec.rs

vest_lib/combinators/bytes/
exec.rs
