vest_lib/combinators/mapped/
exec.rs

1//! Executable mapper interfaces and mapped-format implementations.
2use super::spec::{BiMap, SpecMap};
3use crate::core::exec::fns::Map;
4use crate::core::exec::output::*;
5use crate::core::spec::SoundParser;
6use crate::core::{
7    exec::{
8        fns::Pred,
9        input::InputSlice,
10        parser::{PResult, Parser},
11        serializer::{ByteLen, PreSerializeError, Prepare, Serializer},
12        ParseError,
13    },
14    spec::{SpecParser, SpecSerializer},
15};
16use core::marker::PhantomData;
17use vstd::prelude::*;
18use OutputBuf;
19
20verus! {
21
22// impl<I, A, M> Parser<I> for super::Mapped<A, M> where
23//     I: View<V = Seq<u8>>,
24//     A: Parser<I>,
25//     M: Mapper<I, PIn = A::O, In = A::PVal>,
26//  {
27//     type O = M::POut;
28//     open spec fn exec_inv(&self) -> bool {
29//         self.inner.exec_inv()
30//     }
31//     fn parse(&self, ibuf: &I) -> PResult<Self::O> {
32//         let (n, v) = self.inner.parse(ibuf)?;
33//         Ok((n, M::map(v)))
34//     }
35// }
36impl<I, Inner, M, MRev> Parser<I> for super::Mapped<Inner, BiMap<M, MRev>> where
37    I: View<V = Seq<u8>>,
38    Inner: Parser<I>,
39    M: Map<Inner::PT, Input = Inner::PVal>,
40    MRev: SpecMap<Input = M::Output, Output = M::Input>,
41 {
42    type PT = M::O;
43
44    fn min_byte_len(&self) -> usize {
45        self.inner.min_byte_len()
46    }
47
48    open spec fn exec_inv(&self) -> bool {
49        self.inner.exec_inv()
50    }
51
52    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
53        match self.inner.parse(ibuf) {
54            Ok((n, v)) => {
55                let mapped = self.mapper.0.map(v);
56                assert(self.spec_parse(ibuf@) == Some((n as int, mapped.deep_view())));
57                Ok((n, mapped))
58            },
59            Err(err) => Err(err),
60        }
61    }
62}
63
64impl<Output: OutputBuf, Inner, M, MRev, T> Serializer<Output, T> for super::Mapped<
65    Inner,
66    BiMap<M, MRev>,
67> where
68    T: DeepView,
69    M: SpecMap<Input = MRev::Output, Output = T::V>,
70    MRev: SpecMap<Input = T::V> + for <'x>Map<&'x T>,
71    Inner: for <'x>Serializer<Output, <MRev as Map<&'x T>>::O>,
72 {
73    #[verifier::prophetic]
74    open spec fn exec_inv(&self) -> bool {
75        self.inner.exec_inv()
76    }
77
78    fn serialize_into(&self, v: &T, obuf: &mut Output) {
79        let inner_v = self.mapper.1.map(v);
80        proof {
81            assert(self.spec_serialize(v.deep_view()) == self.inner.spec_serialize(
82                inner_v.deep_view(),
83            ));
84        }
85        self.inner.serialize_into(&inner_v, obuf);
86    }
87}
88
89impl<Inner, M, MRev, T> Prepare<T> for super::Mapped<Inner, BiMap<M, MRev>> where
90    T: DeepView,
91    M: SpecMap<Input = MRev::Output, Output = T::V>,
92    MRev: SpecMap<Input = T::V> + for <'x>Map<&'x T>,
93    Inner: for <'x>Prepare<<MRev as Map<&'x T>>::O>,
94 {
95    open spec fn exec_inv(&self) -> bool {
96        self.inner.exec_inv()
97    }
98
99    fn prepare(&self, v: &T) -> Result<usize, PreSerializeError> {
100        let inner_v = self.mapper.1.map(v);
101        self.inner.prepare(&inner_v)
102    }
103}
104
105impl<Inner, M, MRev, T> ByteLen<T> for super::Mapped<Inner, BiMap<M, MRev>> where
106    T: DeepView,
107    M: SpecMap<Input = MRev::Output, Output = T::V>,
108    MRev: SpecMap<Input = T::V> + for <'x>Map<&'x T>,
109    Inner: for <'x>ByteLen<<MRev as Map<&'x T>>::O>,
110 {
111    open spec fn exec_inv(&self) -> bool {
112        self.inner.exec_inv()
113    }
114
115    fn length(&self, v: &T) -> usize {
116        let inner_v = self.mapper.1.map(v);
117        self.inner.length(&inner_v)
118    }
119}
120
121} // verus!
vest_lib/combinators/mapped/exec.rs

vest_lib/combinators/mapped/
exec.rs
