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    open spec fn exec_inv(&self) -> bool {
19        self.1.exec_inv()
20    }
21
22    fn parse(&self, ibuf: &I) -> (r: PResult<Self::PT>) {
23        match self.1.parse(ibuf) {
24            Ok((n, v)) => Ok((n, v)),
25            Err(err) => Err(err.push_format(self.0)),
26        }
27    }
28}
29
30impl<Output: OutputBuf, T, Inner> Serializer<Output, T> for super::Named<Inner> where
31    T: DeepView,
32    Inner: Serializer<Output, T>,
33 {
34    #[verifier::prophetic]
35    open spec fn exec_inv(&self) -> bool {
36        self.1.exec_inv()
37    }
38
39    fn serialize_into(&self, v: &T, obuf: &mut Output) {
40        self.1.serialize_into(v, obuf);
41    }
42}
43
44impl<T, Inner> ByteLen<T> for super::Named<Inner> where T: DeepView, Inner: ByteLen<T> {
45    open spec fn exec_inv(&self) -> bool {
46        self.1.exec_inv()
47    }
48
49    fn length(&self, v: &T) -> (len: usize) {
50        self.1.length(v)
51    }
52}
53
54impl<T, Inner> Prepare<T> for super::Named<Inner> where T: DeepView, Inner: Prepare<T> {
55    open spec fn exec_inv(&self) -> bool {
56        self.1.exec_inv()
57    }
58
59    fn prepare(&self, v: &T) -> (checked: Result<usize, PreSerializeError>) {
60        match self.1.prepare(v) {
61            Err(err) => Err(err.push_format(self.0)),
62            otherwise => otherwise,
63        }
64    }
65}
66
67} // verus!
vest_lib/combinators/named/exec.rs

vest_lib/combinators/named/
exec.rs
