vest/regular/
tail.rs

1use crate::properties::*;
2use vstd::prelude::*;
3
4verus! {
5
6/// Combinator that returns the rest of the input bytes from the current position.
7pub struct Tail;
8
9impl View for Tail {
10    type V = Tail;
11
12    open spec fn view(&self) -> Self::V {
13        Tail
14    }
15}
16
17impl SpecCombinator for Tail {
18    type SpecResult = Seq<u8>;
19
20    open spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()> {
21        if s.len() <= usize::MAX {
22            Ok((s.len() as usize, s))
23        } else {
24            Err(())
25        }
26    }
27
28    open spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()> {
29        if v.len() <= usize::MAX {
30            Ok(v)
31        } else {
32            Err(())
33        }
34    }
35
36    proof fn spec_parse_wf(&self, s: Seq<u8>) {
37    }
38}
39
40impl SecureSpecCombinator for Tail {
41    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult) {
42    }
43
44    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
45        assert(buf.subrange(0, buf.len() as int) == buf);
46    }
47
48    open spec fn is_prefix_secure() -> bool {
49        false
50    }
51
52    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
53    }
54}
55
56impl Combinator for Tail {
57    type Result<'a> = &'a [u8];
58
59    type Owned = Vec<u8>;
60
61    open spec fn spec_length(&self) -> Option<usize> {
62        None
63    }
64
65    fn length(&self) -> Option<usize> {
66        None
67    }
68
69    fn parse<'a>(&self, s: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) {
70        if s.len() <= usize::MAX {
71            Ok(((s.len()), s))
72        } else {
73            Err(ParseError::SizeOverflow)
74        }
75    }
76
77    fn serialize(&self, v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> (res: Result<
78        usize,
79        SerializeError,
80    >) {
81        if pos <= data.len() {
82            if v.len() <= data.len() - pos {
83                set_range(data, pos, v);
84                assert(data@.subrange(pos as int, pos + v@.len() as int) == self@.spec_serialize(
85                    v@,
86                ).unwrap());
87                Ok(v.len())
88            } else {
89                Err(SerializeError::InsufficientBuffer)
90            }
91        } else {
92            Err(SerializeError::InsufficientBuffer)
93        }
94    }
95}
96
97} // verus!
vest/regular/tail.rs

vest/regular/
tail.rs
