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#[cfg(verus_only)]
28use vstd::std_specs::cmp::PartialEqIs;
29
30verus! {
31
32pub assume_specification<T: core::cmp::PartialEq<U>, U>[ <[T] as PartialEq<[U]>>::eq ](
33    x: &[T],
34    y: &[U],
35) -> (res: bool)
36    ensures
37        res == (x@.len() == y@.len() && forall|i: int|
38            #![auto]
39            0 <= i < x@.len() ==> x@[i].is_eq(&y@[i])),
40;
41
42#[inline(always)]
43pub fn bytes_eq(a: &[u8], b: &[u8]) -> (r: bool)
44    ensures
45        r == (a@ == b@),
46        r == (a.deep_view() == b.deep_view()),
47{
48    let res = *a == *b;
49    assert(a@ == a.deep_view());
50    assert(b@ == b.deep_view());
51    assert(res ==> (a.deep_view() == b.deep_view()));
52    res
53}
54
55} // verus!
vest_lib/core/exec/mod.rs

vest_lib/core/exec/
mod.rs
