verdict_parser/common/
unreachable.rs

1use super::*;
2use vstd::prelude::*;
3
4verus! {
5
6/// Similar to Fail, but without error message
7#[derive(View)]
8pub struct Unreachable;
9
10impl SpecCombinator for Unreachable {
11    type SpecResult = ();
12
13    open spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()> {
14        Err(())
15    }
16
17    open spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()> {
18        Err(())
19    }
20
21    proof fn spec_parse_wf(&self, s: Seq<u8>) {
22    }
23}
24
25impl SecureSpecCombinator for Unreachable {
26    open spec fn is_prefix_secure() -> bool {
27        true
28    }
29
30    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
31    }
32
33    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult) {
34    }
35
36    proof fn theorem_parse_serialize_roundtrip(&self, s: Seq<u8>) {
37    }
38}
39
40impl Combinator for Unreachable {
41    type Result<'a> = ();
42
43    type Owned = ();
44
45    open spec fn spec_length(&self) -> Option<usize> {
46        Some(0)
47    }
48
49    fn length(&self) -> Option<usize> {
50        Some(0)
51    }
52
53    #[inline(always)]
54    fn parse<'a>(&self, _s: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) {
55        Err(ParseError::Other("Unreachable".to_string()))
56    }
57
58    #[inline(always)]
59    fn serialize(&self, _v: Self::Result<'_>, _data: &mut Vec<u8>, _pos: usize) -> (res: Result<
60        usize,
61        SerializeError,
62    >) {
63        Err(SerializeError::Other("Unreachable".to_string()))
64    }
65}
66
67// Unreachable is disjoint from any other combinator
68impl<T> DisjointFrom<T> for Unreachable where T: SpecCombinator {
69    open spec fn disjoint_from(&self, c: &T) -> bool {
70        true
71    }
72
73    proof fn parse_disjoint_on(&self, c: &T, buf: Seq<u8>) {
74    }
75}
76
77} // verus!
verdict_parser/common/unreachable.rs

verdict_parser/common/
unreachable.rs
