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

vest_lib/combinators/opt/
exec.rs
