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    open spec fn exec_inv(&self) -> bool {
46        &&& self.0.exec_inv()
47        &&& self.1.exec_inv()
48    }
49
50    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
51        match self.0.parse(ibuf) {
52            Ok((n, v)) => Ok((n, super::Sum::Inl(v))),
53            Err(first_err) => {
54                match self.1.parse(ibuf) {
55                    Ok((n, v)) => {
56                        let inr_v = super::Sum::Inr(v);
57                        assert(self.spec_parse(ibuf@) == Some((n as int, inr_v.deep_view())));
58                        Ok((n, inr_v))
59                    },
60                    Err(second_err) => {
61                        match first_err.kind {
62                            ParseErrorKind::RecursionLimitExceeded => Err(first_err),
63                            _ => Err(second_err),
64                        }
65                    },
66                }
67            },
68        }
69    }
70}
71
72impl<Output: OutputBuf, A, B, TA, TB> Serializer<Output, super::Sum<TA, TB>> for super::Choice<
73    A,
74    B,
75> where TA: DeepView, TB: DeepView, A: Serializer<Output, TA>, B: Serializer<Output, TB> {
76    #[verifier::prophetic]
77    open spec fn exec_inv(&self) -> bool {
78        &&& self.0.exec_inv()
79        &&& self.1.exec_inv()
80    }
81
82    fn serialize_into(&self, v: &super::Sum<TA, TB>, obuf: &mut Output) {
83        match v {
84            super::Sum::Inl(va) => self.0.serialize_into(va, obuf),
85            super::Sum::Inr(vb) => self.1.serialize_into(vb, obuf),
86        }
87    }
88}
89
90impl<A, B, TA, TB> ByteLen<super::Sum<TA, TB>> for super::Choice<A, B> where
91    TA: DeepView,
92    TB: DeepView,
93    A: ByteLen<TA>,
94    B: ByteLen<TB>,
95 {
96    open spec fn exec_inv(&self) -> bool {
97        &&& self.0.exec_inv()
98        &&& self.1.exec_inv()
99    }
100
101    fn length(&self, v: &super::Sum<TA, TB>) -> (len: usize) {
102        match v {
103            super::Sum::Inl(va) => self.0.length(va),
104            super::Sum::Inr(vb) => self.1.length(vb),
105        }
106    }
107}
108
109impl<A, B, TA, TB> Prepare<super::Sum<TA, TB>> for super::Choice<A, B> where
110    TA: DeepView,
111    TB: DeepView,
112    A: Prepare<TA>,
113    B: Prepare<TB>,
114 {
115    open spec fn exec_inv(&self) -> bool {
116        &&& self.0.exec_inv()
117        &&& self.1.exec_inv()
118    }
119
120    fn prepare(&self, v: &super::Sum<TA, TB>) -> (checked: Result<usize, PreSerializeError>) {
121        match v {
122            super::Sum::Inl(va) => self.0.prepare(va),
123            super::Sum::Inr(vb) => self.1.prepare(vb),
124        }
125    }
126}
127
128impl<const NONDETERMINISTIC: bool, I, A, B> Parser<I> for super::Alt<A, B, NONDETERMINISTIC> where
129    I: View<V = Seq<u8>>,
130    A: Parser<I>,
131    B: Parser<I, PVal = A::PVal, PT = A::PT>,
132 {
133    type PT = A::PT;
134
135    open spec fn exec_inv(&self) -> bool {
136        &&& self.0.exec_inv()
137        &&& self.1.exec_inv()
138    }
139
140    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
141        match self.0.parse(ibuf) {
142            Ok(r) => Ok(r),
143            Err(_) => self.1.parse(ibuf),
144        }
145    }
146}
147
148impl<I, A, B> Parser<I> for super::Sum<A, B> where
149    I: View<V = Seq<u8>>,
150    A: Parser<I>,
151    B: Parser<I>,
152 {
153    type PT = super::Sum<A::PT, B::PT>;
154
155    open spec fn exec_inv(&self) -> bool {
156        match self {
157            super::Sum::Inl(a) => a.exec_inv(),
158            super::Sum::Inr(b) => b.exec_inv(),
159        }
160    }
161
162    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
163        match self {
164            super::Sum::Inl(a) => {
165                let (n, v) = a.parse(ibuf)?;
166                Ok((n, super::Sum::Inl(v)))
167            },
168            super::Sum::Inr(b) => {
169                let (n, v) = b.parse(ibuf)?;
170                Ok((n, super::Sum::Inr(v)))
171            },
172        }
173    }
174}
175
176impl<Output: OutputBuf, A, B, TA, TB> Serializer<Output, super::Sum<TA, TB>> for super::Sum<
177    A,
178    B,
179> where TA: DeepView, TB: DeepView, A: Serializer<Output, TA>, B: Serializer<Output, TB> {
180    #[verifier::prophetic]
181    open spec fn exec_inv(&self) -> bool {
182        match self {
183            super::Sum::Inl(a) => a.exec_inv(),
184            super::Sum::Inr(b) => b.exec_inv(),
185        }
186    }
187
188    fn serialize_into(&self, v: &super::Sum<TA, TB>, obuf: &mut Output) {
189        match (self, v) {
190            (super::Sum::Inl(a), super::Sum::Inl(va)) => a.serialize_into(va, obuf),
191            (super::Sum::Inr(b), super::Sum::Inr(vb)) => b.serialize_into(vb, obuf),
192            _ => (),
193        }
194    }
195}
196
197impl<A, B, TA, TB> ByteLen<super::Sum<TA, TB>> for super::Sum<A, B> where
198    TA: DeepView,
199    TB: DeepView,
200    A: ByteLen<TA>,
201    B: ByteLen<TB>,
202 {
203    open spec fn exec_inv(&self) -> bool {
204        match self {
205            super::Sum::Inl(a) => a.exec_inv(),
206            super::Sum::Inr(b) => b.exec_inv(),
207        }
208    }
209
210    fn length(&self, v: &super::Sum<TA, TB>) -> (len: usize) {
211        match (self, v) {
212            (super::Sum::Inl(a), super::Sum::Inl(va)) => a.length(va),
213            (super::Sum::Inr(b), super::Sum::Inr(vb)) => b.length(vb),
214            _ => 0,
215        }
216    }
217}
218
219impl<A, B, TA, TB> Prepare<super::Sum<TA, TB>> for super::Sum<A, B> where
220    TA: DeepView,
221    TB: DeepView,
222    A: Prepare<TA>,
223    B: Prepare<TB>,
224 {
225    open spec fn exec_inv(&self) -> bool {
226        match self {
227            super::Sum::Inl(a) => a.exec_inv(),
228            super::Sum::Inr(b) => b.exec_inv(),
229        }
230    }
231
232    fn prepare(&self, v: &super::Sum<TA, TB>) -> (checked: Result<usize, PreSerializeError>) {
233        match (self, v) {
234            (super::Sum::Inl(a), super::Sum::Inl(va)) => a.prepare(va),
235            (super::Sum::Inr(b), super::Sum::Inr(vb)) => b.prepare(vb),
236            _ => Err(PreSerializeError::not_compliant(ComplianceErrorKind::InvalidChoice)),
237        }
238    }
239}
240
241} // verus!
vest_lib/combinators/choice/exec.rs

vest_lib/combinators/choice/
exec.rs
