vest_lib/regular/
end.rs

1use crate::properties::*;
2use vstd::prelude::*;
3
4verus! {
5
6/// Combinator that succeeds only at the end of the input buffer and consumes nothing
7pub struct End;
8
9impl View for End {
10    type V = Self;
11
12    open spec fn view(&self) -> Self::V {
13        *self
14    }
15}
16
17impl SpecCombinator for End {
18    type Type = ();
19
20    open spec fn spec_parse(&self, s: Seq<u8>) -> Option<(int, Self::Type)> {
21        if s.len() == 0 {
22            Some((0, ()))
23        } else {
24            None
25        }
26    }
27
28    open spec fn spec_serialize(&self, v: Self::Type) -> Seq<u8> {
29        Seq::empty()
30    }
31}
32
33impl SecureSpecCombinator for End {
34    open spec fn is_prefix_secure() -> bool {
35        false
36    }
37
38    open spec fn is_productive(&self) -> bool {
39        false
40    }
41
42    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
43    }
44
45    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::Type) {
46    }
47
48    proof fn theorem_parse_serialize_roundtrip(&self, s: Seq<u8>) {
49    }
50
51    proof fn lemma_parse_length(&self, s: Seq<u8>) {
52    }
53
54    proof fn lemma_parse_productive(&self, s: Seq<u8>) {
55    }
56}
57
58impl<'x, I: VestInput, O: VestOutput<I>> Combinator<'x, I, O> for End {
59    type Type = ();
60
61    type SType = ();
62
63    fn length(&self, _v: Self::SType) -> usize {
64        0
65    }
66
67    fn parse(&self, s: I) -> (res: Result<(usize, Self::Type), ParseError>) {
68        if s.len() == 0 {
69            Ok((0, ()))
70        } else {
71            Err(ParseError::NotEof)
72        }
73    }
74
75    fn serialize(&self, _v: Self::SType, _data: &mut O, _pos: usize) -> (res: Result<
76        usize,
77        SerializeError,
78    >) {
79        assert(seq_splice(_data@, _pos, Seq::<u8>::empty()) == _data@);
80        Ok(0)
81    }
82}
83
84} // verus!
vest_lib/regular/end.rs

vest_lib/regular/
end.rs
