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    open spec fn exec_inv(&self) -> bool {
45        self.inner.exec_inv()
46    }
47
48    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
49        match self.inner.parse(ibuf) {
50            Ok((n, v)) => {
51                let mapped = self.mapper.0.map(v);
52                assert(self.spec_parse(ibuf@) == Some((n as int, mapped.deep_view())));
53                Ok((n, mapped))
54            },
55            Err(err) => Err(err),
56        }
57    }
58}
59
60impl<Output: OutputBuf, Inner, M, MRev, T> Serializer<Output, T> for super::Mapped<
61    Inner,
62    BiMap<M, MRev>,
63> where
64    T: DeepView,
65    M: SpecMap<Input = MRev::Output, Output = T::V>,
66    MRev: SpecMap<Input = T::V> + for <'x>Map<&'x T>,
67    Inner: for <'x>Serializer<Output, <MRev as Map<&'x T>>::O>,
68 {
69    #[verifier::prophetic]
70    open spec fn exec_inv(&self) -> bool {
71        self.inner.exec_inv()
72    }
73
74    fn serialize_into(&self, v: &T, obuf: &mut Output) {
75        let inner_v = self.mapper.1.map(v);
76        proof {
77            assert(self.spec_serialize(v.deep_view()) == self.inner.spec_serialize(
78                inner_v.deep_view(),
79            ));
80        }
81        self.inner.serialize_into(&inner_v, obuf);
82    }
83}
84
85impl<Inner, M, MRev, T> Prepare<T> for super::Mapped<Inner, BiMap<M, MRev>> where
86    T: DeepView,
87    M: SpecMap<Input = MRev::Output, Output = T::V>,
88    MRev: SpecMap<Input = T::V> + for <'x>Map<&'x T>,
89    Inner: for <'x>Prepare<<MRev as Map<&'x T>>::O>,
90 {
91    open spec fn exec_inv(&self) -> bool {
92        self.inner.exec_inv()
93    }
94
95    fn prepare(&self, v: &T) -> Result<usize, PreSerializeError> {
96        let inner_v = self.mapper.1.map(v);
97        self.inner.prepare(&inner_v)
98    }
99}
100
101impl<Inner, M, MRev, T> ByteLen<T> for super::Mapped<Inner, BiMap<M, MRev>> where
102    T: DeepView,
103    M: SpecMap<Input = MRev::Output, Output = T::V>,
104    MRev: SpecMap<Input = T::V> + for <'x>Map<&'x T>,
105    Inner: for <'x>ByteLen<<MRev as Map<&'x T>>::O>,
106 {
107    open spec fn exec_inv(&self) -> bool {
108        self.inner.exec_inv()
109    }
110
111    fn length(&self, v: &T) -> usize {
112        let inner_v = self.mapper.1.map(v);
113        self.inner.length(&inner_v)
114    }
115}
116
117} // verus!
vest_lib/combinators/mapped/exec.rs

vest_lib/combinators/mapped/
exec.rs
