vest_lib/regular/
fail.rs

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

vest_lib/regular/
fail.rs
