vest/regular/
fail.rs

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

vest/regular/
fail.rs
