vest_lib/core/exec/
input.rs

1//! Input abstractions for executable parsers.
2use vstd::{prelude::*, slice::slice_subrange};
3
4verus! {
5
6/// A byte input whose ordinary and deep views denote the same byte sequence.
7pub trait InputSlice: View<V = Seq<u8>> + DeepView<V = Seq<u8>> {
8    /// Proves that the two logical views of this input agree.
9    proof fn deep_view_eq_view(&self)
10        ensures
11            self.deep_view() == self@,
12    ;
13}
14
15/// Trait for types that can be used as input for Vest parsers, roughly corresponding to byte
16/// buffers.
17pub trait InputBuf: InputSlice + Sized {
18    /// The length of the buffer.
19    fn len(&self) -> (len: usize)
20        ensures
21            len == self@.len(),
22    ;
23
24    /// A slice-like view of the range `[i, j)` of the buffer.
25    fn subrange(&self, i: usize, j: usize) -> (sliced: Self)
26        requires
27            0 <= i as int <= j as int <= self@.len(),
28        ensures
29            sliced@ == self@.subrange(i as int, j as int),
30            sliced.deep_view() == sliced@,
31    ;
32
33    /// A view of the first `n` bytes of the buffer.
34    fn take(&self, n: usize) -> (taken: Self)
35        requires
36            n as int <= self@.len(),
37        ensures
38            taken@ == self@.take(n as int),
39            taken.deep_view() == taken@,
40    {
41        self.subrange(0, n)
42    }
43
44    /// A view of the buffer with the first `n` bytes skipped.
45    fn skip(&self, n: usize) -> (skipped: Self)
46        requires
47            n as int <= self@.len(),
48        ensures
49            skipped@ == self@.skip(n as int),
50            skipped.deep_view() == skipped@,
51    {
52        self.subrange(n, self.len())
53    }
54}
55
56impl<'input> InputSlice for &'input [u8] {
57    proof fn deep_view_eq_view(&self) {
58        assert(self.deep_view() == self@);
59    }
60}
61
62impl<'input> InputBuf for &'input [u8] {
63    fn len(&self) -> (len: usize) {
64        <[u8]>::len(self)
65    }
66
67    fn subrange(&self, i: usize, j: usize) -> &'input [u8] {
68        let sliced = slice_subrange(self, i, j);
69        proof {
70            sliced.deep_view_eq_view();
71        }
72        sliced
73    }
74}
75
76} // verus!
vest_lib/core/exec/input.rs

vest_lib/core/exec/
input.rs
