vest_lib 0.2.2

Verified parser and serializer combinators in Verus
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90

//! Executable implementations for empty and uninhabitable formats.
use crate::core::exec::output::*;
use crate::core::exec::ComplianceErrorKind;
use crate::core::exec::{
    parser::{PResult, Parser},
    serializer::{ByteLen, PreSerializeError, Prepare, Serializer},
    ParseError, ParseErrorKind,
};
use crate::Never;
use vstd::prelude::*;
use OutputBuf;

verus! {

/// An uninhabited type that implements DeepView.
#[derive(Copy, Clone, Debug, PartialEq, Eq)]
#[verifier::external_body]
pub struct ExecNever;

impl DeepView for ExecNever {
    type V = Never;

    open spec fn deep_view(&self) -> Self::V {
        *self
    }
}

impl<I: View<V = Seq<u8>>> Parser<I> for super::Empty {
    type PT = ();

    fn min_byte_len(&self) -> usize {
        0
    }

    fn parse(&self, _ibuf: &I) -> PResult<Self::PT> {
        Ok((0, ()))
    }
}

impl<Output: OutputBuf> Serializer<Output, ()> for super::Empty {
    fn serialize_into(&self, _v: &(), _obuf: &mut Output) {
        broadcast use crate::core::exec::output::outbuf_lemmas;

    }
}

impl ByteLen<()> for super::Empty {
    fn length(&self, _v: &()) -> (len: usize) {
        0
    }
}

impl Prepare<()> for super::Empty {
    fn prepare(&self, _v: &()) -> (checked: Result<usize, PreSerializeError>) {
        Ok(0)
    }
}

impl<I: View<V = Seq<u8>>> Parser<I> for super::Void {
    type PT = ExecNever;

    fn min_byte_len(&self) -> usize {
        0
    }

    fn parse(&self, _ibuf: &I) -> (r: PResult<Self::PT>) {
        Err(ParseError::new(ParseErrorKind::Custom(self.0)))
    }
}

impl<Output: OutputBuf> Serializer<Output, ExecNever> for super::Void {
    fn serialize_into(&self, _v: &ExecNever, _obuf: &mut Output) {
        broadcast use crate::core::exec::output::outbuf_lemmas;

    }
}

impl ByteLen<ExecNever> for super::Void {
    fn length(&self, _v: &ExecNever) -> (len: usize) {
        0
    }
}

impl Prepare<ExecNever> for super::Void {
    fn prepare(&self, _v: &ExecNever) -> (checked: Result<usize, PreSerializeError>) {
        Err(PreSerializeError::not_compliant(ComplianceErrorKind::Custom(self.0)))
    }
}

} // verus!