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 parse(&self, _ibuf: &I) -> PResult<Self::PT> {
32        Ok((0, ()))
33    }
34}
35
36impl<Output: OutputBuf> Serializer<Output, ()> for super::Empty {
37    fn serialize_into(&self, _v: &(), _obuf: &mut Output) {
38        broadcast use crate::core::exec::output::outbuf_lemmas;
39
40    }
41}
42
43impl ByteLen<()> for super::Empty {
44    fn length(&self, _v: &()) -> (len: usize) {
45        0
46    }
47}
48
49impl Prepare<()> for super::Empty {
50    fn prepare(&self, _v: &()) -> (checked: Result<usize, PreSerializeError>) {
51        Ok(0)
52    }
53}
54
55impl<I: View<V = Seq<u8>>> Parser<I> for super::Void {
56    type PT = ExecNever;
57
58    fn parse(&self, _ibuf: &I) -> (r: PResult<Self::PT>) {
59        Err(ParseError::new(ParseErrorKind::Custom(self.0)))
60    }
61}
62
63impl<Output: OutputBuf> Serializer<Output, ExecNever> for super::Void {
64    fn serialize_into(&self, _v: &ExecNever, _obuf: &mut Output) {
65        broadcast use crate::core::exec::output::outbuf_lemmas;
66
67    }
68}
69
70impl ByteLen<ExecNever> for super::Void {
71    fn length(&self, _v: &ExecNever) -> (len: usize) {
72        0
73    }
74}
75
76impl Prepare<ExecNever> for super::Void {
77    fn prepare(&self, _v: &ExecNever) -> (checked: Result<usize, PreSerializeError>) {
78        Err(PreSerializeError::not_compliant(ComplianceErrorKind::Custom(self.0)))
79    }
80}
81
82} // verus!
vest_lib/combinators/marker/exec.rs

vest_lib/combinators/marker/
exec.rs
