vest_lib/regular/
success.rs

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

vest_lib/regular/
success.rs
