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
82
83
84
85
86
87
88

//! Repetition into vectors/sequences.
//!
//! [`Star`] stops when its child no longer matches;
//! [`RepeatTillEnd`](crate::combinators::RepeatTillEnd) requires a
//! bounded region to be exhausted. Their child must be productive so every
//! successful iteration consumes input.
/// 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! {

/// Kleene star combinator: greedy zero-or-more repetition, consuming/producing `Seq<A::PVal>`.
///
/// Parsing semantics: always succeeds (may return an empty sequence). Stops when `A` fails or
/// consumes zero bytes.
///
/// ## Consistency
///
/// A sequence `s` is consistent with `Star<A>` iff every element of `s` is consistent with `A`.
///
/// ## Note
///
/// This combinator is mostly used *internally* to specify [`Repeat<A, B>`], which is
/// able to disambiguate `A` and `B` and hence more compositional.
#[derive(Copy)]
pub struct Star<A>(pub A);

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

/// Zero-or-more `A` followed by terminator `B`: sugar for `Pair(Star<A>, B)`.
///
/// ## Unambiguity
///
/// Requires `disjoint_domains(A, B)`.
#[derive(Copy)]
pub struct Repeat<A, B>(pub A, pub B);

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

/// Exactly `N` repetitions of combinator `C` (`N` is a runtime value).
#[derive(Copy)]
pub struct RepeatN<C, N = u8>(pub N, pub C);

impl<C: Clone, N: Clone> Clone for RepeatN<C, N> {
    fn clone(&self) -> (cloned: Self)
        ensures
            call_ensures(N::clone, (&self.0,), cloned.0),
            call_ensures(C::clone, (&self.1,), cloned.1),
    {
        RepeatN(self.0.clone(), self.1.clone())
    }
}

/// Exactly `N` repetitions of combinator `C` (`N` is a compile-time constant).
#[derive(Copy)]
pub struct Array<const N: usize, C>(pub C);

impl<const N: usize, C: Clone> Clone for Array<N, C> {
    fn clone(&self) -> (cloned: Self)
        ensures
            call_ensures(C::clone, (&self.0,), cloned.0),
    {
        Array(self.0.clone())
    }
}

} // verus!