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
16impl<const N: usize, I: InputBuf> Parser<I> for super::Fixed<N> {
17    type PT = I;
18
19    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
20        if ibuf.len() < N {
21            Err(ParseError::unexpected_eof())
22        } else {
23            Ok((N, ibuf.take(N)))
24        }
25    }
26}
27
28impl<Output: OutputBuf, const N: usize> Serializer<Output, [u8]> for super::Fixed<N> {
29    fn serialize_into(&self, v: &[u8], obuf: &mut Output) {
30        obuf.write_bytes(v);
31    }
32}
33
34impl<'i, Output: OutputBuf, const N: usize> Serializer<Output, &'i [u8]> for super::Fixed<N> {
35    fn serialize_into(&self, v: &&'i [u8], obuf: &mut Output) {
36        obuf.write_bytes(*v);
37    }
38}
39
40impl<Output: OutputBuf, const N: usize> Serializer<Output, [u8; N]> for super::Fixed<N> {
41    fn serialize_into(&self, v: &[u8; N], obuf: &mut Output) {
42        obuf.write_bytes(v);
43    }
44}
45
46// impl<Output: OutputBuf, const N: usize> Serializer<Output, [u8; N]> for super::Fixed<N> {
47//     fn ex_serialize(&self, v: &[u8; N], obuf: &mut Output) {
48//         obuf.write_bytes(v);
49//     }
50// }
51impl<const N: usize> ByteLen<[u8]> for super::Fixed<N> {
52    fn length(&self, v: &[u8]) -> (len: usize) {
53        v.len()
54    }
55}
56
57impl<'i, const N: usize> ByteLen<&'i [u8]> for super::Fixed<N> {
58    fn length(&self, v: &&'i [u8]) -> (len: usize) {
59        v.len()
60    }
61}
62
63impl<const N: usize> Prepare<[u8]> for super::Fixed<N> {
64    fn prepare(&self, v: &[u8]) -> (checked: Result<usize, PreSerializeError>) {
65        if v.len() == N {
66            Ok(N)
67        } else {
68            Err(PreSerializeError::not_compliant(ComplianceErrorKind::LengthInconsistent))
69        }
70    }
71}
72
73impl<'i, const N: usize> Prepare<&'i [u8]> for super::Fixed<N> {
74    fn prepare(&self, v: &&'i [u8]) -> (checked: Result<usize, PreSerializeError>) {
75        if v.len() == N {
76            Ok(N)
77        } else {
78            Err(PreSerializeError::not_compliant(ComplianceErrorKind::LengthInconsistent))
79        }
80    }
81}
82
83impl<Len: AsLen, I: InputBuf> Parser<I> for super::Varied<Len> {
84    type PT = I;
85
86    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
87        let len = self.0.get();
88        if ibuf.len() < len {
89            Err(ParseError::unexpected_eof())
90        } else {
91            Ok((len, ibuf.take(len)))
92        }
93    }
94}
95
96impl<Output: OutputBuf, Len: AsLen> Serializer<Output, [u8]> for super::Varied<Len> {
97    fn serialize_into(&self, v: &[u8], obuf: &mut Output) {
98        obuf.write_bytes(v);
99    }
100}
101
102impl<'i, Output: OutputBuf, Len: AsLen> Serializer<Output, &'i [u8]> for super::Varied<Len> {
103    fn serialize_into(&self, v: &&'i [u8], obuf: &mut Output) {
104        obuf.write_bytes(*v);
105    }
106}
107
108impl<Len: AsLen> ByteLen<[u8]> for super::Varied<Len> {
109    fn length(&self, v: &[u8]) -> (len: usize) {
110        v.len()
111    }
112}
113
114impl<'i, Len: AsLen> ByteLen<&'i [u8]> for super::Varied<Len> {
115    fn length(&self, v: &&'i [u8]) -> (len: usize) {
116        v.len()
117    }
118}
119
120impl<Len: AsLen> Prepare<[u8]> for super::Varied<Len> {
121    fn prepare(&self, v: &[u8]) -> (checked: Result<usize, PreSerializeError>) {
122        if v.len() == self.0.get() {
123            Ok(v.len())
124        } else {
125            Err(PreSerializeError::not_compliant(ComplianceErrorKind::LengthInconsistent))
126        }
127    }
128}
129
130impl<'i, Len: AsLen> Prepare<&'i [u8]> for super::Varied<Len> {
131    fn prepare(&self, v: &&'i [u8]) -> (checked: Result<usize, PreSerializeError>) {
132        if v.len() == self.0.get() {
133            Ok(v.len())
134        } else {
135            Err(PreSerializeError::not_compliant(ComplianceErrorKind::LengthInconsistent))
136        }
137    }
138}
139
140impl<I, Len, Inner> Parser<I> for super::ExactLen<Inner, Len> where
141    I: InputBuf,
142    Len: AsLen,
143    Inner: Parser<I>,
144 {
145    type PT = Inner::PT;
146
147    open spec fn exec_inv(&self) -> bool {
148        self.1.exec_inv()
149    }
150
151    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
152        super::AndThen(super::Varied(self.0), &self.1).parse(ibuf)
153    }
154}
155
156impl<I: InputBuf, A, Then> Parser<I> for super::AndThen<A, Then> where
157    A: Parser<I, PT = I, PVal = Seq<u8>>,
158    Then: Parser<I>,
159 {
160    type PT = Then::PT;
161
162    open spec fn exec_inv(&self) -> bool {
163        &&& self.0.exec_inv()
164        &&& self.1.exec_inv()
165    }
166
167    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
168        assert(self.exec_inv());
169
170        let (len_a, chunk) = self.0.parse(ibuf)?;
171        proof {
172            chunk.deep_view_eq_view();
173        }
174        let (len_b, v) = self.1.parse(&chunk)?;
175        if len_b == len_a {
176            Ok((len_b, v))
177        } else {
178            Err(ParseError::length_mismatch())
179        }
180    }
181}
182
183impl<Output: OutputBuf, Len, Inner, T> Serializer<Output, T> for super::ExactLen<Inner, Len> where
184    Len: AsLen,
185    T: DeepView + ?Sized,
186    Inner: Serializer<Output, T> + SpecByteLen<T = T::V>,
187 {
188    #[verifier::prophetic]
189    open spec fn exec_inv(&self) -> bool {
190        self.1.exec_inv()
191    }
192
193    fn serialize_into(&self, v: &T, obuf: &mut Output) {
194        self.1.serialize_into(v, obuf);
195    }
196}
197
198impl<Output: OutputBuf, Then, T> Serializer<Output, T> for super::AndThen<Tail, Then> where
199    T: DeepView + ?Sized,
200    Then: Serializer<Output, T>,
201 {
202    #[verifier::prophetic]
203    open spec fn exec_inv(&self) -> bool {
204        self.1.exec_inv()
205    }
206
207    fn serialize_into(&self, v: &T, obuf: &mut Output) {
208        self.1.serialize_into(v, obuf);
209    }
210}
211
212impl<Len, Inner, InnerST> ByteLen<InnerST> for super::ExactLen<Inner, Len> where
213    Len: AsLen,
214    InnerST: DeepView + ?Sized,
215    Inner: ByteLen<InnerST>,
216 {
217    open spec fn exec_inv(&self) -> bool {
218        self.1.exec_inv()
219    }
220
221    fn length(&self, v: &InnerST) -> (len: usize) {
222        self.1.length(v)
223    }
224}
225
226impl<Len, Inner, InnerST> Prepare<InnerST> for super::ExactLen<Inner, Len> where
227    Len: AsLen,
228    InnerST: DeepView + ?Sized,
229    Inner: Prepare<InnerST>,
230 {
231    open spec fn exec_inv(&self) -> bool {
232        self.1.exec_inv()
233    }
234
235    fn prepare(&self, v: &InnerST) -> (checked: Result<usize, PreSerializeError>) {
236        let len = self.1.prepare(v)?;
237        if len == self.0.get() {
238            Ok(len)
239        } else {
240            Err(PreSerializeError::not_compliant(ComplianceErrorKind::LengthInconsistent))
241        }
242    }
243}
244
245impl<Then, T> Prepare<T> for super::AndThen<Tail, Then> where
246    T: DeepView + ?Sized,
247    Then: Prepare<T>,
248 {
249    open spec fn exec_inv(&self) -> bool {
250        self.1.exec_inv()
251    }
252
253    fn prepare(&self, v: &T) -> (checked: Result<usize, PreSerializeError>) {
254        let len = self.1.prepare(v)?;
255        proof {
256            let chunk = Seq::new(len as nat, |_i| 0u8);
257            assert(self.0.consistent(chunk));
258        }
259        Ok(len)
260    }
261}
262
263impl<A, Then, ThenST> ByteLen<ThenST> for super::AndThen<A, Then> where
264    ThenST: DeepView + ?Sized,
265    Then: ByteLen<ThenST>,
266 {
267    open spec fn exec_inv(&self) -> bool {
268        self.1.exec_inv()
269    }
270
271    fn length(&self, v: &ThenST) -> (len: usize) {
272        self.1.length(v)
273    }
274}
275
276} // verus!
vest_lib/combinators/bytes/exec.rs

vest_lib/combinators/bytes/
exec.rs
