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    /// A lower bound on the number of bytes one successful parse consumes.
52    ///
53    /// This is a capacity hint for repetition formats.
54    ///
55    /// Formats whose minimum is statically known should override it;
56    /// the DSL compiler emits an override for every named format it generates.
57    fn min_byte_len(&self) -> usize {
58        0
59    }
60}
61
62impl<Spec, Exec> SpecParser for (Spec, Exec) where Spec: SpecParser {
63    type PVal = Spec::PVal;
64
65    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
66        self.0.spec_parse(ibuf)
67    }
68}
69
70impl<Spec, Exec> SafeParser for (Spec, Exec) where Spec: SafeParser {
71    open spec fn safe_inv(&self) -> bool {
72        self.0.safe_inv()
73    }
74
75    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
76        self.0.lemma_parse_safe(ibuf);
77    }
78}
79
80impl<Spec, Exec> Productive for (Spec, Exec) where Spec: Productive {
81    open spec fn productive_inv(&self) -> bool {
82        self.0.productive_inv()
83    }
84
85    proof fn lemma_productive(&self, input: Seq<u8>) {
86        self.0.lemma_productive(input);
87    }
88}
89
90impl<I, T, Spec, Exec> Parser<I> for (Spec, Exec) where
91    I: View<V = Seq<u8>>,
92    T: DeepView<V = Spec::PVal>,
93    Spec: SpecParser,
94    Exec: Fn(&I) -> PResult<T>,
95 {
96    type PT = T;
97
98    open spec fn exec_inv(&self) -> bool {
99        &&& forall|i: &I| call_requires(self.1, (i,))
100        &&& forall|i: &I, r: PResult<T>|
101            #![auto]
102            call_ensures(self.1, (i,), r) ==> parse_matches_spec(r, self.spec_parse(i@))
103    }
104
105    fn parse(&self, ibuf: &I) -> (r: PResult<T>) {
106        (self.1)(ibuf)
107    }
108}
109
110impl<P: SpecParser> SpecParser for &P {
111    type PVal = P::PVal;
112
113    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
114        (*self).spec_parse(ibuf)
115    }
116}
117
118impl<P: SafeParser> SafeParser for &P {
119    open spec fn safe_inv(&self) -> bool {
120        (*self).safe_inv()
121    }
122
123    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
124        (*self).lemma_parse_safe(ibuf);
125    }
126}
127
128impl<P: Productive> Productive for &P {
129    open spec fn productive_inv(&self) -> bool {
130        (*self).productive_inv()
131    }
132
133    proof fn lemma_productive(&self, s: Seq<u8>) {
134        (*self).lemma_productive(s);
135    }
136}
137
138impl<I, P> Parser<I> for &P where I: View<V = Seq<u8>>, P: Parser<I> {
139    type PT = P::PT;
140
141    open spec fn exec_inv(&self) -> bool {
142        (*self).exec_inv()
143    }
144
145    fn parse(&self, ibuf: &I) -> (r: PResult<Self::PT>) {
146        (*self).parse(ibuf)
147    }
148}
149
150pub proof fn lemma_ref_safe_productive_inv<P>(parser: &P) where P: Productive
151    requires
152        parser.safe_inv(),
153        parser.productive_inv(),
154    ensures
155        <&P as SafeParser>::safe_inv(&parser),
156        <&P as Productive>::productive_inv(&parser),
157{
158}
159
160} // verus!
vest_lib/core/exec/parser.rs

vest_lib/core/exec/
parser.rs
