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

//! Formats that consume the remaining input.
//!
//! [`Tail`] borrows all remaining bytes. [`Eof`] accepts only an empty input
//! and is used to make complete-consumption requirements explicit.
/// 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! {

/// Tail combinator: denotes the "tail" of the format, useful for under-specification.
///
/// Parsing semantics: consumes and return all remaining bytes (even if the input is empty).
///
/// ## Note
///
/// The DPS serialization replaces (not prepends to) the output buffer,
/// so `Tail` should only appear at the end of a format (and the trait system enforces this).
#[derive(Clone, Copy)]
pub struct Tail;

/// End-of-file combinator: denotes the "EOF".
///
/// Parsing semantics: succeeds only if the input is empty, producing `()`.
///
/// Implements [`AdmitsUniqueVal`](crate::core::spec::AdmitsUniqueVal).
///
/// ## Note
///
/// The DPS serialization always replaces the output buffer with the empty sequence, so `Eof`
/// should only appear at the end of a format (and the trait system enforces this).
#[derive(Clone, Copy)]
pub struct Eof;

/// Sequential composition of formats `A` and `B`, where the direction of parsing is reversed compared to [`super::Pair`].
///
/// Parsing semantics: parses `B` from the back, consumes the tail part of the input, then parses `A`.
#[derive(Copy)]
pub struct PairRev<A, B>(pub B, pub A);

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

/// Sugar for `Optional(C, Eof)`.
#[derive(Copy)]
pub struct OptionalEnd<C>(pub C);

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

/// Sugar for `Repeat(C, Eof)`.
#[derive(Copy)]
pub struct RepeatTillEnd<C>(pub C);

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

} // verus!