vest_lib 0.2.2

Verified parser and serializer combinators in Verus
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121

//! Executable mapper interfaces and mapped-format implementations.
use super::spec::{BiMap, SpecMap};
use crate::core::exec::fns::Map;
use crate::core::exec::output::*;
use crate::core::spec::SoundParser;
use crate::core::{
    exec::{
        fns::Pred,
        input::InputSlice,
        parser::{PResult, Parser},
        serializer::{ByteLen, PreSerializeError, Prepare, Serializer},
        ParseError,
    },
    spec::{SpecParser, SpecSerializer},
};
use core::marker::PhantomData;
use vstd::prelude::*;
use OutputBuf;

verus! {

// impl<I, A, M> Parser<I> for super::Mapped<A, M> where
//     I: View<V = Seq<u8>>,
//     A: Parser<I>,
//     M: Mapper<I, PIn = A::O, In = A::PVal>,
//  {
//     type O = M::POut;
//     open spec fn exec_inv(&self) -> bool {
//         self.inner.exec_inv()
//     }
//     fn parse(&self, ibuf: &I) -> PResult<Self::O> {
//         let (n, v) = self.inner.parse(ibuf)?;
//         Ok((n, M::map(v)))
//     }
// }
impl<I, Inner, M, MRev> Parser<I> for super::Mapped<Inner, BiMap<M, MRev>> where
    I: View<V = Seq<u8>>,
    Inner: Parser<I>,
    M: Map<Inner::PT, Input = Inner::PVal>,
    MRev: SpecMap<Input = M::Output, Output = M::Input>,
 {
    type PT = M::O;

    fn min_byte_len(&self) -> usize {
        self.inner.min_byte_len()
    }

    open spec fn exec_inv(&self) -> bool {
        self.inner.exec_inv()
    }

    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
        match self.inner.parse(ibuf) {
            Ok((n, v)) => {
                let mapped = self.mapper.0.map(v);
                assert(self.spec_parse(ibuf@) == Some((n as int, mapped.deep_view())));
                Ok((n, mapped))
            },
            Err(err) => Err(err),
        }
    }
}

impl<Output: OutputBuf, Inner, M, MRev, T> Serializer<Output, T> for super::Mapped<
    Inner,
    BiMap<M, MRev>,
> where
    T: DeepView,
    M: SpecMap<Input = MRev::Output, Output = T::V>,
    MRev: SpecMap<Input = T::V> + for <'x>Map<&'x T>,
    Inner: for <'x>Serializer<Output, <MRev as Map<&'x T>>::O>,
 {
    #[verifier::prophetic]
    open spec fn exec_inv(&self) -> bool {
        self.inner.exec_inv()
    }

    fn serialize_into(&self, v: &T, obuf: &mut Output) {
        let inner_v = self.mapper.1.map(v);
        proof {
            assert(self.spec_serialize(v.deep_view()) == self.inner.spec_serialize(
                inner_v.deep_view(),
            ));
        }
        self.inner.serialize_into(&inner_v, obuf);
    }
}

impl<Inner, M, MRev, T> Prepare<T> for super::Mapped<Inner, BiMap<M, MRev>> where
    T: DeepView,
    M: SpecMap<Input = MRev::Output, Output = T::V>,
    MRev: SpecMap<Input = T::V> + for <'x>Map<&'x T>,
    Inner: for <'x>Prepare<<MRev as Map<&'x T>>::O>,
 {
    open spec fn exec_inv(&self) -> bool {
        self.inner.exec_inv()
    }

    fn prepare(&self, v: &T) -> Result<usize, PreSerializeError> {
        let inner_v = self.mapper.1.map(v);
        self.inner.prepare(&inner_v)
    }
}

impl<Inner, M, MRev, T> ByteLen<T> for super::Mapped<Inner, BiMap<M, MRev>> where
    T: DeepView,
    M: SpecMap<Input = MRev::Output, Output = T::V>,
    MRev: SpecMap<Input = T::V> + for <'x>Map<&'x T>,
    Inner: for <'x>ByteLen<<MRev as Map<&'x T>>::O>,
 {
    open spec fn exec_inv(&self) -> bool {
        self.inner.exec_inv()
    }

    fn length(&self, v: &T) -> usize {
        let inner_v = self.mapper.1.map(v);
        self.inner.length(&inner_v)
    }
}

} // verus!