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

//! Marker combinators for empty and impossible wire languages.
//!
//! [`Empty`] accepts the empty prefix and produces `()`. [`Void`] accepts
//! nothing and is useful for eliminating impossible choice branches.
/// Executable trait implementations for this combinator.
pub mod exec;
/// Correctness proofs for this combinator.
pub mod proof;
/// Specification trait implementations for this combinator.
pub mod spec;

use crate::core::proof::LeafNonMalleable;
use vstd::prelude::*;

verus! {

/// Marker combinator that denotes the "empty" format.
///
/// Parsing semantics: always succeeds without consuming any input, returning `()`.
///
/// Serialization semantics: produces an empty byte sequence.
#[derive(Clone, Copy)]
pub struct Empty;

/// Marker combinator that denotes the "void" format.
///
/// Parsing semantics: always fails.
///
/// ## Consistency
///
/// No value is consistent with `Void`.
#[derive(Clone, Copy)]
pub struct Void(pub &'static str);

impl LeafNonMalleable for Empty {
    proof fn nonmal_leaf_inv(&self) {
    }
}

impl LeafNonMalleable for Void {
    proof fn nonmal_leaf_inv(&self) {
    }
}

} // verus!