vest_lib/combinators/opt/
exec.rs

1//! Executable implementations for optional formats.
2use crate::core::exec::output::*;
3use crate::core::{
4    exec::{
5        input::InputBuf,
6        parser::{PResult, Parser},
7        serializer::{ByteLen, PreSerializeError, Prepare, Serializer},
8    },
9    spec::{SafeParser, SpecParser},
10};
11use vstd::prelude::*;
12use OutputBuf;
13
14verus! {
15
16impl<I, A> Parser<I> for super::Opt<A> where I: View<V = Seq<u8>>, A: Parser<I> {
17    type PT = Option<A::PT>;
18
19    open spec fn exec_inv(&self) -> bool {
20        self.0.exec_inv()
21    }
22
23    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
24        match self.0.parse(ibuf) {
25            Ok((n, v)) => Ok((n, Some(v))),
26            Err(_) => {
27                let none = None;
28                assert(self.spec_parse(ibuf@) == Some((0int, none.deep_view())));
29                Ok((0, none))
30            },
31        }
32    }
33}
34
35impl<Output: OutputBuf, A, T> Serializer<Output, Option<T>> for super::Opt<A> where
36    T: DeepView,
37    A: Serializer<Output, T>,
38 {
39    #[verifier::prophetic]
40    open spec fn exec_inv(&self) -> bool {
41        self.0.exec_inv()
42    }
43
44    fn serialize_into(&self, v: &Option<T>, obuf: &mut Output) {
45        broadcast use crate::core::exec::output::outbuf_lemmas;
46
47        match v {
48            Some(vv) => self.0.serialize_into(vv, obuf),
49            None => {},
50        }
51    }
52}
53
54impl<A, T> ByteLen<Option<T>> for super::Opt<A> where T: DeepView, A: ByteLen<T> {
55    open spec fn exec_inv(&self) -> bool {
56        self.0.exec_inv()
57    }
58
59    fn length(&self, v: &Option<T>) -> (len: usize) {
60        match v {
61            Some(vv) => self.0.length(vv),
62            None => 0,
63        }
64    }
65}
66
67impl<A, T> Prepare<Option<T>> for super::Opt<A> where T: DeepView, A: Prepare<T> {
68    open spec fn exec_inv(&self) -> bool {
69        self.0.exec_inv()
70    }
71
72    fn prepare(&self, v: &Option<T>) -> (checked: Result<usize, PreSerializeError>) {
73        match v {
74            Some(vv) => self.0.prepare(vv),
75            None => Ok(0),
76        }
77    }
78}
79
80impl<I, A, B> Parser<I> for super::Optional<A, B> where
81    I: InputBuf,
82    A: Parser<I> + SafeParser,
83    B: Parser<I> + SafeParser,
84 {
85    type PT = (Option<A::PT>, B::PT);
86
87    open spec fn exec_inv(&self) -> bool {
88        &&& self.0.exec_inv()
89        &&& self.0.safe_inv()
90        &&& self.1.exec_inv()
91        &&& self.1.safe_inv()
92    }
93
94    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
95        crate::combinators::Pair(super::Opt(&self.0), &self.1).parse(ibuf)
96    }
97}
98
99impl<Output: OutputBuf, A, B, TA, TB> Serializer<Output, (Option<TA>, TB)> for super::Optional<
100    A,
101    B,
102> where TA: DeepView, TB: DeepView, A: Serializer<Output, TA>, B: Serializer<Output, TB> {
103    #[verifier::prophetic]
104    open spec fn exec_inv(&self) -> bool {
105        &&& self.0.exec_inv()
106        &&& self.1.exec_inv()
107    }
108
109    fn serialize_into(&self, v: &(Option<TA>, TB), obuf: &mut Output) {
110        crate::combinators::Pair(super::Opt(&self.0), &self.1).serialize_into(v, obuf);
111    }
112}
113
114impl<A, B, TA, TB> ByteLen<(Option<TA>, TB)> for super::Optional<A, B> where
115    TA: DeepView,
116    TB: DeepView,
117    A: ByteLen<TA>,
118    B: ByteLen<TB>,
119 {
120    open spec fn exec_inv(&self) -> bool {
121        &&& self.0.exec_inv()
122        &&& self.1.exec_inv()
123    }
124
125    fn length(&self, v: &(Option<TA>, TB)) -> (len: usize) {
126        crate::combinators::Pair(super::Opt(&self.0), &self.1).length(v)
127    }
128}
129
130impl<A, B, TA, TB> Prepare<(Option<TA>, TB)> for super::Optional<A, B> where
131    TA: DeepView,
132    TB: DeepView,
133    A: Prepare<TA>,
134    B: Prepare<TB>,
135 {
136    open spec fn exec_inv(&self) -> bool {
137        &&& self.0.exec_inv()
138        &&& self.1.exec_inv()
139    }
140
141    fn prepare(&self, v: &(Option<TA>, TB)) -> Result<usize, PreSerializeError> {
142        crate::combinators::Pair(super::Opt(&self.0), &self.1).prepare(v)
143    }
144}
145
146} // verus!
vest_lib/combinators/opt/exec.rs

vest_lib/combinators/opt/
exec.rs
