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

//! Input abstractions for executable parsers.
use vstd::{prelude::*, slice::slice_subrange};

verus! {

/// A byte input whose ordinary and deep views denote the same byte sequence.
pub trait InputSlice: View<V = Seq<u8>> + DeepView<V = Seq<u8>> {
    /// Proves that the two logical views of this input agree.
    proof fn deep_view_eq_view(&self)
        ensures
            self.deep_view() == self@,
    ;
}

/// Trait for types that can be used as input for Vest parsers, roughly corresponding to byte
/// buffers.
pub trait InputBuf: InputSlice + Sized {
    /// The length of the buffer.
    fn len(&self) -> (len: usize)
        ensures
            len == self@.len(),
    ;

    /// A slice-like view of the range `[i, j)` of the buffer.
    fn subrange(&self, i: usize, j: usize) -> (sliced: Self)
        requires
            0 <= i as int <= j as int <= self@.len(),
        ensures
            sliced@ == self@[i..j],
            sliced.deep_view() == sliced@,
    ;

    /// A view of the first `n` bytes of the buffer.
    fn take(&self, n: usize) -> (taken: Self)
        requires
            n as int <= self@.len(),
        ensures
            taken@ == self@[0..n],
            taken.deep_view() == taken@,
    {
        self.subrange(0, n)
    }

    /// A view of the buffer with the first `n` bytes skipped.
    fn skip(&self, n: usize) -> (skipped: Self)
        requires
            n as int <= self@.len(),
        ensures
            skipped@ == self@[n..],
            skipped.deep_view() == skipped@,
    {
        self.subrange(n, self.len())
    }
}

impl<'input> InputSlice for &'input [u8] {
    proof fn deep_view_eq_view(&self) {
        assert(self.deep_view() == self@);
    }
}

impl<'input> InputBuf for &'input [u8] {
    fn len(&self) -> (len: usize) {
        <[u8]>::len(self)
    }

    fn subrange(&self, i: usize, j: usize) -> &'input [u8] {
        let sliced = slice_subrange(self, i, j);
        proof {
            sliced.deep_view_eq_view();
        }
        sliced
    }
}

} // verus!