vest_lib/combinators/marker/
exec.rs

1//! Executable implementations for empty and uninhabitable formats.
2use crate::core::exec::output::*;
3use crate::core::exec::ComplianceErrorKind;
4use crate::core::exec::{
5    parser::{PResult, Parser},
6    serializer::{ByteLen, PreSerializeError, Prepare, Serializer},
7    ParseError, ParseErrorKind,
8};
9use crate::Never;
10use vstd::prelude::*;
11use OutputBuf;
12
13verus! {
14
15/// An uninhabited type that implements DeepView.
16#[derive(Copy, Clone, Debug, PartialEq, Eq)]
17#[verifier::external_body]
18pub struct ExecNever;
19
20impl DeepView for ExecNever {
21    type V = Never;
22
23    open spec fn deep_view(&self) -> Self::V {
24        *self
25    }
26}
27
28impl<I: View<V = Seq<u8>>> Parser<I> for super::Empty {
29    type PT = ();
30
31    fn min_byte_len(&self) -> usize {
32        0
33    }
34
35    fn parse(&self, _ibuf: &I) -> PResult<Self::PT> {
36        Ok((0, ()))
37    }
38}
39
40impl<Output: OutputBuf> Serializer<Output, ()> for super::Empty {
41    fn serialize_into(&self, _v: &(), _obuf: &mut Output) {
42        broadcast use crate::core::exec::output::outbuf_lemmas;
43
44    }
45}
46
47impl ByteLen<()> for super::Empty {
48    fn length(&self, _v: &()) -> (len: usize) {
49        0
50    }
51}
52
53impl Prepare<()> for super::Empty {
54    fn prepare(&self, _v: &()) -> (checked: Result<usize, PreSerializeError>) {
55        Ok(0)
56    }
57}
58
59impl<I: View<V = Seq<u8>>> Parser<I> for super::Void {
60    type PT = ExecNever;
61
62    fn min_byte_len(&self) -> usize {
63        0
64    }
65
66    fn parse(&self, _ibuf: &I) -> (r: PResult<Self::PT>) {
67        Err(ParseError::new(ParseErrorKind::Custom(self.0)))
68    }
69}
70
71impl<Output: OutputBuf> Serializer<Output, ExecNever> for super::Void {
72    fn serialize_into(&self, _v: &ExecNever, _obuf: &mut Output) {
73        broadcast use crate::core::exec::output::outbuf_lemmas;
74
75    }
76}
77
78impl ByteLen<ExecNever> for super::Void {
79    fn length(&self, _v: &ExecNever) -> (len: usize) {
80        0
81    }
82}
83
84impl Prepare<ExecNever> for super::Void {
85    fn prepare(&self, _v: &ExecNever) -> (checked: Result<usize, PreSerializeError>) {
86        Err(PreSerializeError::not_compliant(ComplianceErrorKind::Custom(self.0)))
87    }
88}
89
90} // verus!
vest_lib/combinators/marker/exec.rs

vest_lib/combinators/marker/
exec.rs
