vest_lib/combinators/opt/
spec.rs

1//! Specifications for optional formats.
2use crate::{
3    combinators::Pair,
4    core::{proof::*, spec::*},
5};
6use vstd::prelude::*;
7
8verus! {
9
10impl<A> SpecParser for super::Opt<A> where A: SpecParser {
11    type PVal = Option<A::PVal>;
12
13    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
14        match self.0.spec_parse(ibuf) {
15            Some((n, v)) => Some((n, Some(v))),
16            None => Some((0, None)),
17        }
18    }
19}
20
21impl<A> Consistency for super::Opt<A> where A: Consistency {
22    type Val = Option<A::Val>;
23
24    open spec fn consistent(&self, v: Self::Val) -> bool {
25        match v {
26            None => true,
27            Some(vv) => self.0.consistent(vv),
28        }
29    }
30}
31
32impl<A> SafeParser for super::Opt<A> where A: SafeParser {
33    open spec fn safe_inv(&self) -> bool {
34        self.0.safe_inv()
35    }
36
37    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
38        assert(self.safe_inv());
39        self.0.lemma_parse_safe(ibuf);
40    }
41}
42
43impl<A> SoundParser for super::Opt<A> where A: SoundParser {
44    open spec fn sound_inv(&self) -> bool {
45        self.0.sound_inv()
46    }
47
48    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
49        match self.0.spec_parse(ibuf) {
50            Some((n, vv)) => {
51                assert(self.sound_inv());
52                self.0.lemma_parse_sound_consumption(ibuf);
53            },
54            None => {},
55        }
56    }
57
58    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
59        assert(self.sound_inv());
60        self.0.lemma_parse_sound_value(ibuf);
61    }
62}
63
64impl<A> SpecSerializerDps for super::Opt<A> where A: SpecSerializerDps {
65    type SValue = Option<A::SValue>;
66
67    open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
68        match v {
69            None => obuf,
70            Some(vv) => self.0.spec_serialize_dps(vv, obuf),
71        }
72    }
73}
74
75impl<A> SpecSerializer for super::Opt<A> where A: SpecSerializer {
76    type SVal = Option<A::SVal>;
77
78    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
79        match v {
80            None => Seq::empty(),
81            Some(vv) => self.0.spec_serialize(vv),
82        }
83    }
84}
85
86impl<A> NonTailFmt for super::Opt<A> where A: NonTailFmt {
87    open spec fn serialize_dps_inv(&self) -> bool {
88        self.0.serialize_dps_inv()
89    }
90
91    proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>) {
92        match v {
93            None => {
94                assert(self.spec_serialize_dps(v, obuf) == Seq::empty() + obuf);
95            },
96            Some(vv) => {
97                self.0.lemma_serialize_dps_prepend(vv, obuf);
98            },
99        }
100    }
101
102    proof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>) {
103        match v {
104            None => {},
105            Some(vv) => {
106                self.0.lemma_serialize_dps_len(vv, obuf);
107            },
108        }
109    }
110}
111
112impl<A: GoodSerializer> GoodSerializer for super::Opt<A> {
113    open spec fn serialize_inv(&self) -> bool {
114        self.0.serialize_inv()
115    }
116
117    proof fn lemma_serialize_len(&self, v: Self::SVal) {
118        match v {
119            None => {},
120            Some(vv) => {
121                self.0.lemma_serialize_len(vv);
122            },
123        }
124    }
125}
126
127impl<Inner: SpecByteLen> SpecByteLen for super::Opt<Inner> {
128    type T = Option<Inner::T>;
129
130    open spec fn byte_len(&self, v: Self::T) -> nat {
131        match v {
132            None => 0,
133            Some(vv) => self.0.byte_len(vv),
134        }
135    }
136}
137
138impl<Inner: MinMaxByteLen> MinMaxByteLen for super::Opt<Inner> {
139    open spec fn min(&self) -> nat {
140        0
141    }
142
143    open spec fn max(&self) -> nat {
144        self.0.max()
145    }
146
147    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
148        match v {
149            None => (),
150            Some(vv) => self.0.lemma_min_max_byte_len(vv),
151        }
152    }
153}
154
155impl<Inner: ValueByteLen> ValueByteLen for super::Opt<Inner> {
156    open spec fn value_byte_len(v: Self::T) -> nat {
157        match v {
158            None => 0,
159            Some(vv) => Inner::value_byte_len(vv),
160        }
161    }
162
163    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
164        match v {
165            None => (),
166            Some(vv) => self.0.lemma_value_len_matches_byte_len(vv),
167        }
168    }
169}
170
171impl<A: SpecParser, B: SpecParser> SpecParser for super::Optional<A, B> {
172    type PVal = (Option<A::PVal>, B::PVal);
173
174    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
175        Pair(super::Opt(self.0), self.1).spec_parse(ibuf)
176    }
177}
178
179impl<A, B> Consistency for super::Optional<A, B> where A: Consistency, B: Consistency {
180    type Val = (Option<A::Val>, B::Val);
181
182    open spec fn consistent(&self, v: Self::Val) -> bool {
183        Pair(super::Opt(self.0), self.1).consistent(v)
184    }
185}
186
187impl<A, B> SafeParser for super::Optional<A, B> where A: SafeParser, B: SafeParser {
188    open spec fn safe_inv(&self) -> bool {
189        &&& self.0.safe_inv()
190        &&& self.1.safe_inv()
191    }
192
193    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
194        Pair(super::Opt(self.0), self.1).lemma_parse_safe(ibuf)
195    }
196}
197
198impl<A, B> SoundParser for super::Optional<A, B> where A: SoundParser, B: SoundParser {
199    open spec fn sound_inv(&self) -> bool {
200        &&& self.0.sound_inv()
201        &&& self.1.sound_inv()
202    }
203
204    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
205        Pair(super::Opt(self.0), self.1).lemma_parse_sound_consumption(ibuf)
206    }
207
208    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
209        Pair(super::Opt(self.0), self.1).lemma_parse_sound_value(ibuf)
210    }
211}
212
213impl<A: SpecSerializerDps, B: SpecSerializerDps> SpecSerializerDps for super::Optional<A, B> {
214    type SValue = (Option<A::SValue>, B::SValue);
215
216    open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
217        Pair(super::Opt(self.0), self.1).spec_serialize_dps(v, obuf)
218    }
219}
220
221impl<A: NonTailFmt, B: NonTailFmt> NonTailFmt for super::Optional<A, B> {
222    open spec fn serialize_dps_inv(&self) -> bool {
223        &&& self.0.serialize_dps_inv()
224        &&& self.1.serialize_dps_inv()
225    }
226
227    proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>) {
228        Pair(super::Opt(self.0), self.1).lemma_serialize_dps_prepend(v, obuf)
229    }
230
231    proof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>) {
232        Pair(super::Opt(self.0), self.1).lemma_serialize_dps_len(v, obuf);
233    }
234}
235
236impl<A: GoodSerializer, B: GoodSerializer> GoodSerializer for super::Optional<A, B> {
237    open spec fn serialize_inv(&self) -> bool {
238        &&& self.0.serialize_inv()
239        &&& self.1.serialize_inv()
240    }
241
242    proof fn lemma_serialize_len(&self, v: Self::SVal) {
243        Pair(super::Opt(self.0), self.1).lemma_serialize_len(v);
244    }
245}
246
247impl<A: SpecByteLen, B: SpecByteLen> SpecByteLen for super::Optional<A, B> {
248    type T = (Option<A::T>, B::T);
249
250    open spec fn byte_len(&self, v: Self::T) -> nat {
251        Pair(super::Opt(self.0), self.1).byte_len(v)
252    }
253}
254
255impl<A: MinMaxByteLen, B: MinMaxByteLen> MinMaxByteLen for super::Optional<A, B> {
256    open spec fn min(&self) -> nat {
257        Pair(super::Opt(self.0), self.1).min()
258    }
259
260    open spec fn max(&self) -> nat {
261        Pair(super::Opt(self.0), self.1).max()
262    }
263
264    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
265        Pair(super::Opt(self.0), self.1).lemma_min_max_byte_len(v);
266    }
267}
268
269impl<A: ValueByteLen, B: ValueByteLen> ValueByteLen for super::Optional<A, B> {
270    open spec fn value_byte_len(v: Self::T) -> nat {
271        <Pair<super::Opt<A>, B> as ValueByteLen>::value_byte_len(v)
272    }
273
274    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
275        Pair(super::Opt(self.0), self.1).lemma_value_len_matches_byte_len(v);
276    }
277}
278
279impl<A: SpecSerializer, B: SpecSerializer> SpecSerializer for super::Optional<A, B> {
280    type SVal = (Option<A::SVal>, B::SVal);
281
282    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
283        Pair(super::Opt(self.0), self.1).spec_serialize(v)
284    }
285}
286
287} // verus!
vest_lib/combinators/opt/spec.rs

vest_lib/combinators/opt/
spec.rs
