vest_lib/combinators/named/
exec.rs

1//! Executable error-context propagation for named formats.
2use crate::core::exec::output::*;
3use crate::core::{
4    exec::{
5        parser::{PResult, Parser},
6        serializer::{ByteLen, PreSerializeError, Prepare, Serializer},
7    },
8    spec::SpecSerializer,
9};
10use vstd::prelude::*;
11use OutputBuf;
12
13verus! {
14
15impl<I, Inner> Parser<I> for super::Named<Inner> where I: View<V = Seq<u8>>, Inner: Parser<I> {
16    type PT = Inner::PT;
17
18    fn min_byte_len(&self) -> usize {
19        self.1.min_byte_len()
20    }
21
22    open spec fn exec_inv(&self) -> bool {
23        self.1.exec_inv()
24    }
25
26    fn parse(&self, ibuf: &I) -> (r: PResult<Self::PT>) {
27        match self.1.parse(ibuf) {
28            Ok((n, v)) => Ok((n, v)),
29            Err(err) => Err(err.push_format(self.0)),
30        }
31    }
32}
33
34impl<Output: OutputBuf, T, Inner> Serializer<Output, T> for super::Named<Inner> where
35    T: DeepView,
36    Inner: Serializer<Output, T>,
37 {
38    #[verifier::prophetic]
39    open spec fn exec_inv(&self) -> bool {
40        self.1.exec_inv()
41    }
42
43    fn serialize_into(&self, v: &T, obuf: &mut Output) {
44        self.1.serialize_into(v, obuf);
45    }
46}
47
48impl<T, Inner> ByteLen<T> for super::Named<Inner> where T: DeepView, Inner: ByteLen<T> {
49    open spec fn exec_inv(&self) -> bool {
50        self.1.exec_inv()
51    }
52
53    fn length(&self, v: &T) -> (len: usize) {
54        self.1.length(v)
55    }
56}
57
58impl<T, Inner> Prepare<T> for super::Named<Inner> where T: DeepView, Inner: Prepare<T> {
59    open spec fn exec_inv(&self) -> bool {
60        self.1.exec_inv()
61    }
62
63    fn prepare(&self, v: &T) -> (checked: Result<usize, PreSerializeError>) {
64        match self.1.prepare(v) {
65            Err(err) => Err(err.push_format(self.0)),
66            otherwise => otherwise,
67        }
68    }
69}
70
71} // verus!
vest_lib/combinators/named/exec.rs

vest_lib/combinators/named/
exec.rs
