vest_lib 0.2.2

Verified parser and serializer combinators in Verus
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81

//! Alternative formats and their ambiguity conditions.
//!
//! [`Choice`] uses a structural sum and requires disjoint parse domains for
//! round trips. [`Alt`] is defined over a single value type and is malleable by default.
/// Executable trait implementations for this combinator.
pub mod exec;
/// Correctness proofs for this combinator.
pub mod proof;
/// Specification trait implementations for this combinator.
pub mod spec;

use vstd::prelude::*;

pub use spec::Sum;

verus! {

/// Ordered choice combinator consuming/producing a sum type.
///
/// Parsing semantics: tries `A` first, wrapping success in [`Sum::Inl`]; on failure, tries `B`,
/// wrapping success in [`Sum::Inr`].
///
/// ## Consistency
///
/// If a value `a` is consistent with `A`, then `Sum::Inl(a)` is consistent with `Choice(A, B)`.
/// If a value `b` is consistent with `B`, then `Sum::Inr(b)` is consistent with `Choice(A, B)`.
///
/// ## Unambiguity
///
/// Requires `disjoint_domains(A, B)`.
#[derive(Copy)]
pub struct Choice<A, B>(pub A, pub B);

impl<A: Clone, B: Clone> Clone for Choice<A, B> {
    fn clone(&self) -> (cloned: Self)
        ensures
            call_ensures(A::clone, (&self.0,), cloned.0),
            call_ensures(B::clone, (&self.1,), cloned.1),
    {
        Choice(self.0.clone(), self.1.clone())
    }
}

/// Ordered alternative combinator.
///
/// Parsing semantics: like [`Choice`], but both branches consume/produce the same type.
/// The result is returned directly without a [`Sum`] wrapper.
///
/// Serialization semantics: if only one branch is consistent with a value, that
/// branch is used. If both branches are consistent, serialization is
/// intentionally underspecified and may use either branch.
///
/// ## Consistency
///
/// A value `v` is consistent with `Alt(A, B)` iff it is consistent with `A` OR `B`.
///
/// ## Unambiguity
///
/// Requires `disjoint_domains(A, B)`.
///
/// ## Malleability
///
/// This combinator introduces malleability by default.
/// Non-malleability can be recovered if `A` is disjoint from `B` (see `disjoint_values`).
#[derive(Copy)]
pub struct Alt<A, B, const NONDETERMINISTIC: bool = false>(pub A, pub B);

impl<A: Clone, B: Clone, const NONDETERMINISTIC: bool> Clone for Alt<A, B, NONDETERMINISTIC> {
    fn clone(&self) -> (cloned: Self)
        ensures
            call_ensures(A::clone, (&self.0,), cloned.0),
            call_ensures(B::clone, (&self.1,), cloned.1),
    {
        Alt(self.0.clone(), self.1.clone())
    }
}

/// Dispatch combinator that selects one of `N` branches based on a "tag" value.
pub struct Dispatch<T, C, const N: usize>(pub T, pub [(T, C); N]);

} // verus!