vest_lib/combinators/marker/
mod.rs

1//! Marker combinators for empty and impossible wire languages.
2//!
3//! [`Empty`] accepts the empty prefix and produces `()`. [`Void`] accepts
4//! nothing and is useful for eliminating impossible choice branches.
5/// Executable trait implementations for this combinator.
6pub mod exec;
7/// Correctness proofs for this combinator.
8pub mod proof;
9/// Specification trait implementations for this combinator.
10pub mod spec;
11
12use crate::core::proof::LeafNonMalleable;
13use vstd::prelude::*;
14
15verus! {
16
17/// Marker combinator that denotes the "empty" format.
18///
19/// Parsing semantics: always succeeds without consuming any input, returning `()`.
20///
21/// Serialization semantics: produces an empty byte sequence.
22#[derive(Clone, Copy)]
23pub struct Empty;
24
25/// Marker combinator that denotes the "void" format.
26///
27/// Parsing semantics: always fails.
28///
29/// ## Consistency
30///
31/// No value is consistent with `Void`.
32#[derive(Clone, Copy)]
33pub struct Void(pub &'static str);
34
35impl LeafNonMalleable for Empty {
36    proof fn nonmal_leaf_inv(&self) {
37    }
38}
39
40impl LeafNonMalleable for Void {
41    proof fn nonmal_leaf_inv(&self) {
42    }
43}
44
45} // verus!
vest_lib/combinators/marker/mod.rs

vest_lib/combinators/marker/
mod.rs
