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

//! Optional values selected by whether a child parser matches.
//!
//! [`Optional`] maps absence to `None`; its unambiguity and non-malleability
//! depend on the optional child being distinguishable from what follows.
/// 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::*;

verus! {

/// Optional combinator: denotes an optional field.
///
/// Parsing semantics: tries `A`, returning `Some(a)` on success; on failure, returns `None` without consuming input.
///
/// Serialization semantics: if the value is `Some(a)`, serializes `a` with `A`; if the value is `None`, produces no output.
///
/// ## Consistency
///
/// A value `v` is consistent with `Opt<A>` iff either `v` is consistent with `A` or `v` is `None`.
///
/// ## Note
///
/// This combinator is mostly used *internally* to specify [`Optional<A, B>`], which is
/// able to disambiguate `A` and `B` and hence more compositional.
#[derive(Copy)]
pub struct Opt<A>(pub A);

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

/// Optional field with an arbitrary continuation, defined as `Pair(Opt<A>, B)`.
///
/// ## Unambiguity
///
/// Requires `disjoint_domains(A, B)`.
#[derive(Copy)]
pub struct Optional<A, B>(pub A, pub B);

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

} // verus!