vest_lib/core/exec/
parser.rs

1//! Executable parser traits.
2use crate::core::proof::Productive;
3use crate::core::spec::{SafeParser, SpecParser};
4use vstd::prelude::*;
5
6use super::ParseError;
7
8verus! {
9
10/// Result returned by an executable parser.
11///
12/// On success, the `usize` is the number of input bytes consumed and `O` is the
13/// parsed value. A parser may leave a suffix of its input unconsumed.
14pub type PResult<O> = Result<(usize, O), ParseError>;
15
16/// Relates an executable parse result to its pure [`SpecParser`] result.
17pub open spec fn parse_matches_spec<O: DeepView>(
18    r: PResult<O>,
19    spec_parse: Option<(int, O::V)>,
20) -> bool {
21    &&& r is Ok <==> spec_parse is Some
22    &&& r is Err <==> spec_parse is None
23    &&& r matches Ok((n, v)) ==> spec_parse == Some((n as int, v.deep_view()))
24}
25
26/// An executable parser proved equivalent to a pure [`SpecParser`].
27///
28/// `Input` is normally `&[u8]`. Successful parsing returns both the consumed
29/// byte count and a value whose deep view is exactly the value returned by
30/// `SpecParser::spec_parse`.
31pub trait Parser<Input: View<V = Seq<u8>>>: SpecParser {
32    /// Executable value returned by this parser.
33    type PT: DeepView<V = Self::PVal>;
34
35    /// Extra invariant required by this parser's executable implementation.
36    ///
37    /// Most formats leave this as `true`; functional and recursive
38    /// parser callbacks use it to connect executable code to their specifications.
39    open spec fn exec_inv(&self) -> bool {
40        true
41    }
42
43    /// Parses a prefix of `ibuf`.
44    fn parse(&self, ibuf: &Input) -> (r: PResult<Self::PT>)
45        requires
46            self.exec_inv(),
47        ensures
48            parse_matches_spec(r, self.spec_parse(ibuf@)),
49    ;
50}
51
52impl<Spec, Exec> SpecParser for (Spec, Exec) where Spec: SpecParser {
53    type PVal = Spec::PVal;
54
55    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
56        self.0.spec_parse(ibuf)
57    }
58}
59
60impl<Spec, Exec> SafeParser for (Spec, Exec) where Spec: SafeParser {
61    open spec fn safe_inv(&self) -> bool {
62        self.0.safe_inv()
63    }
64
65    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
66        self.0.lemma_parse_safe(ibuf);
67    }
68}
69
70impl<Spec, Exec> Productive for (Spec, Exec) where Spec: Productive {
71    open spec fn productive_inv(&self) -> bool {
72        self.0.productive_inv()
73    }
74
75    proof fn lemma_productive(&self, input: Seq<u8>) {
76        self.0.lemma_productive(input);
77    }
78}
79
80impl<I, T, Spec, Exec> Parser<I> for (Spec, Exec) where
81    I: View<V = Seq<u8>>,
82    T: DeepView<V = Spec::PVal>,
83    Spec: SpecParser,
84    Exec: Fn(&I) -> PResult<T>,
85 {
86    type PT = T;
87
88    open spec fn exec_inv(&self) -> bool {
89        &&& forall|i: &I| call_requires(self.1, (i,))
90        &&& forall|i: &I, r: PResult<T>|
91            #![auto]
92            call_ensures(self.1, (i,), r) ==> parse_matches_spec(r, self.spec_parse(i@))
93    }
94
95    fn parse(&self, ibuf: &I) -> (r: PResult<T>) {
96        (self.1)(ibuf)
97    }
98}
99
100impl<P: SpecParser> SpecParser for &P {
101    type PVal = P::PVal;
102
103    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
104        (*self).spec_parse(ibuf)
105    }
106}
107
108impl<P: SafeParser> SafeParser for &P {
109    open spec fn safe_inv(&self) -> bool {
110        (*self).safe_inv()
111    }
112
113    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
114        (*self).lemma_parse_safe(ibuf);
115    }
116}
117
118impl<P: Productive> Productive for &P {
119    open spec fn productive_inv(&self) -> bool {
120        (*self).productive_inv()
121    }
122
123    proof fn lemma_productive(&self, s: Seq<u8>) {
124        (*self).lemma_productive(s);
125    }
126}
127
128impl<I, P> Parser<I> for &P where I: View<V = Seq<u8>>, P: Parser<I> {
129    type PT = P::PT;
130
131    open spec fn exec_inv(&self) -> bool {
132        (*self).exec_inv()
133    }
134
135    fn parse(&self, ibuf: &I) -> (r: PResult<Self::PT>) {
136        (*self).parse(ibuf)
137    }
138}
139
140pub proof fn lemma_ref_safe_productive_inv<P>(parser: &P) where P: Productive
141    requires
142        parser.safe_inv(),
143        parser.productive_inv(),
144    ensures
145        <&P as SafeParser>::safe_inv(&parser),
146        <&P as Productive>::productive_inv(&parser),
147{
148}
149
150} // verus!
vest_lib/core/exec/parser.rs

vest_lib/core/exec/
parser.rs
