verdict_parser/common/
end.rs

1use super::*;
2use vstd::prelude::*;
3
4verus! {
5
6/// A combinator that only matches the end of the buffer
7#[derive(Debug, View)]
8pub struct End;
9
10#[derive(Debug, View, PolyfillClone, Eq, PartialEq)]
11pub struct EndValue;
12
13impl SpecCombinator for End {
14    type SpecResult = EndValue;
15
16    open spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()> {
17        if s.len() == 0 {
18            Ok((0, EndValue))
19        } else {
20            Err(())
21        }
22    }
23
24    open spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()> {
25        Ok(seq![])
26    }
27
28    proof fn spec_parse_wf(&self, s: Seq<u8>) {}
29}
30
31impl SecureSpecCombinator for End {
32    open spec fn is_prefix_secure() -> bool {
33        false
34    }
35
36    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult) {}
37
38    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
39        let empty: Seq<u8> = seq![];
40        assert(buf.subrange(0, 0) == empty);
41    }
42
43    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {}
44}
45
46impl Combinator for End {
47    type Result<'a> = EndValue;
48    type Owned = EndValue;
49
50    closed spec fn spec_length(&self) -> Option<usize> {
51        Some(0)
52    }
53
54    fn length(&self) -> Option<usize> {
55        Some(0)
56    }
57
58    #[inline(always)]
59    fn parse<'a>(&self, s: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) {
60        if s.len() == 0 {
61            Ok((0, EndValue))
62        } else {
63            Err(ParseError::Other("Expecting end of the buffer".to_string()))
64        }
65    }
66
67    #[inline(always)]
68    fn serialize(&self, _v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> (res: Result<usize, SerializeError>) {
69        if pos <= data.len() {
70            let ghost empty: Seq<u8> = seq![];
71            assert(data@ =~= seq_splice(old(data)@, pos, empty));
72            Ok(0)
73        } else {
74            Err(SerializeError::InsufficientBuffer)
75        }
76    }
77}
78
79}
verdict_parser/common/end.rs

verdict_parser/common/
end.rs
