vest_lib/combinators/choice/
exec.rs

1//! Executable implementations for ordered alternatives.
2use crate::core::exec::output::*;
3use crate::core::{
4    exec::{
5        parser::{PResult, Parser},
6        serializer::{ByteLen, ComplianceErrorKind, PreSerializeError, Prepare, Serializer},
7        ParseErrorKind,
8    },
9    spec::{Consistency, SpecByteLen, SpecParser, SpecSerializer},
10};
11use vstd::prelude::*;
12use OutputBuf;
13
14verus! {
15
16impl<A: View, B: View> View for super::Sum<A, B> {
17    type V = super::Sum<A::V, B::V>;
18
19    open spec fn view(&self) -> Self::V {
20        match self {
21            super::Sum::Inl(a) => super::Sum::Inl(a@),
22            super::Sum::Inr(b) => super::Sum::Inr(b@),
23        }
24    }
25}
26
27impl<A: DeepView, B: DeepView> DeepView for super::Sum<A, B> {
28    type V = super::Sum<A::V, B::V>;
29
30    open spec fn deep_view(&self) -> Self::V {
31        match self {
32            super::Sum::Inl(a) => super::Sum::Inl(a.deep_view()),
33            super::Sum::Inr(b) => super::Sum::Inr(b.deep_view()),
34        }
35    }
36}
37
38impl<I, A, B> Parser<I> for super::Choice<A, B> where
39    I: View<V = Seq<u8>>,
40    A: Parser<I>,
41    B: Parser<I>,
42 {
43    type PT = super::Sum<A::PT, B::PT>;
44
45    fn min_byte_len(&self) -> usize {
46        let a = self.0.min_byte_len();
47        let b = self.1.min_byte_len();
48        if a < b {
49            a
50        } else {
51            b
52        }
53    }
54
55    open spec fn exec_inv(&self) -> bool {
56        &&& self.0.exec_inv()
57        &&& self.1.exec_inv()
58    }
59
60    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
61        match self.0.parse(ibuf) {
62            Ok((n, v)) => Ok((n, super::Sum::Inl(v))),
63            Err(first_err) => {
64                match self.1.parse(ibuf) {
65                    Ok((n, v)) => {
66                        let inr_v = super::Sum::Inr(v);
67                        assert(self.spec_parse(ibuf@) == Some((n as int, inr_v.deep_view())));
68                        Ok((n, inr_v))
69                    },
70                    Err(second_err) => {
71                        match first_err.kind {
72                            ParseErrorKind::RecursionLimitExceeded => Err(first_err),
73                            _ => Err(second_err),
74                        }
75                    },
76                }
77            },
78        }
79    }
80}
81
82impl<Output: OutputBuf, A, B, TA, TB> Serializer<Output, super::Sum<TA, TB>> for super::Choice<
83    A,
84    B,
85> where TA: DeepView, TB: DeepView, A: Serializer<Output, TA>, B: Serializer<Output, TB> {
86    #[verifier::prophetic]
87    open spec fn exec_inv(&self) -> bool {
88        &&& self.0.exec_inv()
89        &&& self.1.exec_inv()
90    }
91
92    fn serialize_into(&self, v: &super::Sum<TA, TB>, obuf: &mut Output) {
93        match v {
94            super::Sum::Inl(va) => self.0.serialize_into(va, obuf),
95            super::Sum::Inr(vb) => self.1.serialize_into(vb, obuf),
96        }
97    }
98}
99
100impl<A, B, TA, TB> ByteLen<super::Sum<TA, TB>> for super::Choice<A, B> where
101    TA: DeepView,
102    TB: DeepView,
103    A: ByteLen<TA>,
104    B: ByteLen<TB>,
105 {
106    open spec fn exec_inv(&self) -> bool {
107        &&& self.0.exec_inv()
108        &&& self.1.exec_inv()
109    }
110
111    fn length(&self, v: &super::Sum<TA, TB>) -> (len: usize) {
112        match v {
113            super::Sum::Inl(va) => self.0.length(va),
114            super::Sum::Inr(vb) => self.1.length(vb),
115        }
116    }
117}
118
119impl<A, B, TA, TB> Prepare<super::Sum<TA, TB>> for super::Choice<A, B> where
120    TA: DeepView,
121    TB: DeepView,
122    A: Prepare<TA>,
123    B: Prepare<TB>,
124 {
125    open spec fn exec_inv(&self) -> bool {
126        &&& self.0.exec_inv()
127        &&& self.1.exec_inv()
128    }
129
130    fn prepare(&self, v: &super::Sum<TA, TB>) -> (checked: Result<usize, PreSerializeError>) {
131        match v {
132            super::Sum::Inl(va) => self.0.prepare(va),
133            super::Sum::Inr(vb) => self.1.prepare(vb),
134        }
135    }
136}
137
138impl<const NONDETERMINISTIC: bool, I, A, B> Parser<I> for super::Alt<A, B, NONDETERMINISTIC> where
139    I: View<V = Seq<u8>>,
140    A: Parser<I>,
141    B: Parser<I, PVal = A::PVal, PT = A::PT>,
142 {
143    type PT = A::PT;
144
145    fn min_byte_len(&self) -> usize {
146        let a = self.0.min_byte_len();
147        let b = self.1.min_byte_len();
148        if a < b {
149            a
150        } else {
151            b
152        }
153    }
154
155    open spec fn exec_inv(&self) -> bool {
156        &&& self.0.exec_inv()
157        &&& self.1.exec_inv()
158    }
159
160    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
161        match self.0.parse(ibuf) {
162            Ok(r) => Ok(r),
163            Err(_) => self.1.parse(ibuf),
164        }
165    }
166}
167
168impl<I, A, B> Parser<I> for super::Sum<A, B> where
169    I: View<V = Seq<u8>>,
170    A: Parser<I>,
171    B: Parser<I>,
172 {
173    type PT = super::Sum<A::PT, B::PT>;
174
175    fn min_byte_len(&self) -> usize {
176        // The branch is already chosen here.
177        match self {
178            super::Sum::Inl(a) => a.min_byte_len(),
179            super::Sum::Inr(b) => b.min_byte_len(),
180        }
181    }
182
183    open spec fn exec_inv(&self) -> bool {
184        match self {
185            super::Sum::Inl(a) => a.exec_inv(),
186            super::Sum::Inr(b) => b.exec_inv(),
187        }
188    }
189
190    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
191        match self {
192            super::Sum::Inl(a) => {
193                let (n, v) = a.parse(ibuf)?;
194                Ok((n, super::Sum::Inl(v)))
195            },
196            super::Sum::Inr(b) => {
197                let (n, v) = b.parse(ibuf)?;
198                Ok((n, super::Sum::Inr(v)))
199            },
200        }
201    }
202}
203
204impl<Output: OutputBuf, A, B, TA, TB> Serializer<Output, super::Sum<TA, TB>> for super::Sum<
205    A,
206    B,
207> where TA: DeepView, TB: DeepView, A: Serializer<Output, TA>, B: Serializer<Output, TB> {
208    #[verifier::prophetic]
209    open spec fn exec_inv(&self) -> bool {
210        match self {
211            super::Sum::Inl(a) => a.exec_inv(),
212            super::Sum::Inr(b) => b.exec_inv(),
213        }
214    }
215
216    fn serialize_into(&self, v: &super::Sum<TA, TB>, obuf: &mut Output) {
217        match (self, v) {
218            (super::Sum::Inl(a), super::Sum::Inl(va)) => a.serialize_into(va, obuf),
219            (super::Sum::Inr(b), super::Sum::Inr(vb)) => b.serialize_into(vb, obuf),
220            _ => (),
221        }
222    }
223}
224
225impl<A, B, TA, TB> ByteLen<super::Sum<TA, TB>> for super::Sum<A, B> where
226    TA: DeepView,
227    TB: DeepView,
228    A: ByteLen<TA>,
229    B: ByteLen<TB>,
230 {
231    open spec fn exec_inv(&self) -> bool {
232        match self {
233            super::Sum::Inl(a) => a.exec_inv(),
234            super::Sum::Inr(b) => b.exec_inv(),
235        }
236    }
237
238    fn length(&self, v: &super::Sum<TA, TB>) -> (len: usize) {
239        match (self, v) {
240            (super::Sum::Inl(a), super::Sum::Inl(va)) => a.length(va),
241            (super::Sum::Inr(b), super::Sum::Inr(vb)) => b.length(vb),
242            _ => 0,
243        }
244    }
245}
246
247impl<A, B, TA, TB> Prepare<super::Sum<TA, TB>> for super::Sum<A, B> where
248    TA: DeepView,
249    TB: DeepView,
250    A: Prepare<TA>,
251    B: Prepare<TB>,
252 {
253    open spec fn exec_inv(&self) -> bool {
254        match self {
255            super::Sum::Inl(a) => a.exec_inv(),
256            super::Sum::Inr(b) => b.exec_inv(),
257        }
258    }
259
260    fn prepare(&self, v: &super::Sum<TA, TB>) -> (checked: Result<usize, PreSerializeError>) {
261        match (self, v) {
262            (super::Sum::Inl(a), super::Sum::Inl(va)) => a.prepare(va),
263            (super::Sum::Inr(b), super::Sum::Inr(vb)) => b.prepare(vb),
264            _ => Err(PreSerializeError::not_compliant(ComplianceErrorKind::InvalidChoice)),
265        }
266    }
267}
268
269} // verus!
vest_lib/combinators/choice/exec.rs

vest_lib/combinators/choice/
exec.rs
