vest_lib/core/exec/
mod.rs

1//! Executable parsing, validation, length calculation, and serialization.
2//!
3//! Application code normally uses the following trait methods:
4//!
5//! - [`Parser::parse`] consumes an input prefix and produces a structured value;
6//! - [`Prepare::prepare`] validates a value against the format specification and computes its exact wire length;
7//! - [`SerializerExt::serialize`] writes into an exactly sized slice without allocation.
8//!
9//! [`InputBuf`] and [`OutputBuf`] let combinators share implementations across different buffer types.
10pub mod bridge_lemmas;
11pub mod error;
12pub mod fns;
13pub mod input;
14pub mod output;
15pub mod parser;
16pub mod serializer;
17
18pub use error::{ParseError, ParseErrorKind};
19pub use input::{InputBuf, InputSlice};
20pub use output::{OutputBuf, OutputSlice};
21pub use parser::{PResult, Parser};
22pub use serializer::{
23    ByteLen, ComplianceErrorKind, PreSerializeError, Prepare, Serializer, SerializerExt,
24};
25
26use vstd::prelude::*;
27
28verus! {
29
30#[inline(always)]
31pub fn bytes_eq(a: &[u8], b: &[u8]) -> (r: bool)
32    ensures
33        r == (a@ == b@),
34        r == (a.deep_view() == b.deep_view()),
35{
36    let res = *a == *b;
37    assert(a@ == a.deep_view());
38    assert(b@ == b.deep_view());
39    assert(res ==> (a.deep_view() == b.deep_view()));
40    res
41}
42
43} // verus!
vest_lib/core/exec/mod.rs

vest_lib/core/exec/
mod.rs
