vest_lib/combinators/choice/
mod.rs

1//! Alternative formats and their ambiguity conditions.
2//!
3//! [`Choice`] uses a structural sum and requires disjoint parse domains for
4//! round trips. [`Alt`] is defined over a single value type and is malleable by default.
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
14pub use spec::Sum;
15
16verus! {
17
18/// Ordered choice combinator consuming/producing a sum type.
19///
20/// Parsing semantics: tries `A` first, wrapping success in [`Sum::Inl`]; on failure, tries `B`,
21/// wrapping success in [`Sum::Inr`].
22///
23/// ## Consistency
24///
25/// If a value `a` is consistent with `A`, then `Sum::Inl(a)` is consistent with `Choice(A, B)`.
26/// If a value `b` is consistent with `B`, then `Sum::Inr(b)` is consistent with `Choice(A, B)`.
27///
28/// ## Unambiguity
29///
30/// Requires `disjoint_domains(A, B)`.
31#[derive(Copy)]
32pub struct Choice<A, B>(pub A, pub B);
33
34impl<A: Clone, B: Clone> Clone for Choice<A, B> {
35    fn clone(&self) -> (cloned: Self)
36        ensures
37            call_ensures(A::clone, (&self.0,), cloned.0),
38            call_ensures(B::clone, (&self.1,), cloned.1),
39    {
40        Choice(self.0.clone(), self.1.clone())
41    }
42}
43
44/// Ordered alternative combinator.
45///
46/// Parsing semantics: like [`Choice`], but both branches consume/produce the same type.
47/// The result is returned directly without a [`Sum`] wrapper.
48///
49/// Serialization semantics: if only one branch is consistent with a value, that
50/// branch is used. If both branches are consistent, serialization is
51/// intentionally underspecified and may use either branch.
52///
53/// ## Consistency
54///
55/// A value `v` is consistent with `Alt(A, B)` iff it is consistent with `A` OR `B`.
56///
57/// ## Unambiguity
58///
59/// Requires `disjoint_domains(A, B)`.
60///
61/// ## Malleability
62///
63/// This combinator introduces malleability by default.
64/// Non-malleability can be recovered if `A` is disjoint from `B` (see `disjoint_values`).
65#[derive(Copy)]
66pub struct Alt<A, B, const NONDETERMINISTIC: bool = false>(pub A, pub B);
67
68impl<A: Clone, B: Clone, const NONDETERMINISTIC: bool> Clone for Alt<A, B, NONDETERMINISTIC> {
69    fn clone(&self) -> (cloned: Self)
70        ensures
71            call_ensures(A::clone, (&self.0,), cloned.0),
72            call_ensures(B::clone, (&self.1,), cloned.1),
73    {
74        Alt(self.0.clone(), self.1.clone())
75    }
76}
77
78/// Dispatch combinator that selects one of `N` branches based on a "tag" value.
79pub struct Dispatch<T, C, const N: usize>(pub T, pub [(T, C); N]);
80
81} // verus!
vest_lib/combinators/choice/mod.rs

vest_lib/combinators/choice/
mod.rs
