vest_lib/combinators/opt/
mod.rs

1//! Optional values selected by whether a child parser matches.
2//!
3//! [`Optional`] maps absence to `None`; its unambiguity and non-malleability
4//! depend on the optional child being distinguishable from what follows.
5/// Executable trait implementations for this combinator.
6pub mod exec;
7/// Correctness proofs for this combinator.
8pub mod proof;
9/// Specification trait implementations for this combinator.
10pub mod spec;
11
12use vstd::prelude::*;
13
14verus! {
15
16/// Optional combinator: denotes an optional field.
17///
18/// Parsing semantics: tries `A`, returning `Some(a)` on success; on failure, returns `None` without consuming input.
19///
20/// Serialization semantics: if the value is `Some(a)`, serializes `a` with `A`; if the value is `None`, produces no output.
21///
22/// ## Consistency
23///
24/// A value `v` is consistent with `Opt<A>` iff either `v` is consistent with `A` or `v` is `None`.
25///
26/// ## Note
27///
28/// This combinator is mostly used *internally* to specify [`Optional<A, B>`], which is
29/// able to disambiguate `A` and `B` and hence more compositional.
30#[derive(Copy)]
31pub struct Opt<A>(pub A);
32
33impl<A: Clone> Clone for Opt<A> {
34    fn clone(&self) -> (cloned: Self)
35        ensures
36            call_ensures(A::clone, (&self.0,), cloned.0),
37    {
38        Opt(self.0.clone())
39    }
40}
41
42/// Optional field with an arbitrary continuation, defined as `Pair(Opt<A>, B)`.
43///
44/// ## Unambiguity
45///
46/// Requires `disjoint_domains(A, B)`.
47#[derive(Copy)]
48pub struct Optional<A, B>(pub A, pub B);
49
50impl<A: Clone, B: Clone> Clone for Optional<A, B> {
51    fn clone(&self) -> (cloned: Self)
52        ensures
53            call_ensures(A::clone, (&self.0,), cloned.0),
54            call_ensures(B::clone, (&self.1,), cloned.1),
55    {
56        Optional(self.0.clone(), self.1.clone())
57    }
58}
59
60} // verus!
vest_lib/combinators/opt/mod.rs

vest_lib/combinators/opt/
mod.rs
