vest_lib/
prelude.rs

1//! This module re-exports the most commonly used items from Vest.
2//!
3//! `use vest_lib::prelude::*;` would include the Verus prelude, Vest's executable,
4//! specification and proof traits, as well as its format combinators.
5//!
6//! In addition, some basic length and bytes-view broadcast lemmas are enabled automatically when
7//! `vest_lib` is imported.
8pub use crate::combinators::*;
9pub use crate::core::exec::{
10    ByteLen, InputBuf, InputSlice, OutputBuf, OutputSlice, PResult, ParseError, ParseErrorKind,
11    Parser, PreSerializeError, Prepare, Serializer, SerializerExt,
12};
13pub use crate::core::{proof::*, spec::*};
14pub use vstd::prelude::*;
15
16#[cfg(verus_keep_ghost)]
17pub use crate::combinators::star::spec::lemma_star_static_byte_len;
18#[cfg(feature = "alloc")]
19use alloc::vec::Vec;
20
21verus! {
22
23/// Byte slices have the same shallow and deep views.
24pub broadcast proof fn lemma_byte_slice_view(bytes: &[u8])
25    ensures
26        #[trigger] bytes.deep_view() == bytes@,
27{
28    assert(bytes.deep_view() =~= bytes@);
29}
30
31/// Fixed byte arrays have the same shallow and deep views.
32pub broadcast proof fn lemma_byte_array_view<const N: usize>(bytes: &[u8; N])
33    ensures
34        #[trigger] bytes.deep_view() == bytes@,
35{
36    assert(bytes.deep_view() =~= bytes@);
37}
38
39/// Identity-view elements give a vector the same shallow and deep views.
40#[cfg(feature = "alloc")]
41pub broadcast proof fn lemma_identity_vec_view<T: DeepView<V = T>>(values: &Vec<T>)
42    requires
43        forall|item: T| #[trigger] item.deep_view() == item,
44    ensures
45        #[trigger] values.deep_view() == values@,
46{
47    assert(values.deep_view() =~= values@);
48}
49
50#[cfg_attr(verus_keep_ghost, verifier::broadcast_use_by_default_when_this_crate_is_imported)]
51pub broadcast group basic_lemmas {
52    StaticByteLen::lemma_static_len_matches_byte_len,
53    GoodSerializer::lemma_serialize_len,
54    lemma_star_static_byte_len,
55    lemma_byte_slice_view,
56    lemma_byte_array_view,
57    #[cfg(feature = "alloc")]
58    lemma_identity_vec_view,
59}
60
61/// Opt-in parser facts: consumed bounds, consistent values, and exact byte lengths.
62pub broadcast group parser_lemmas {
63    SafeParser::lemma_parse_safe,
64    SoundParser::lemma_parse_sound_consumption,
65    SoundParser::lemma_parse_sound_value,
66}
67
68} // verus!
vest_lib/prelude.rs

vest_lib/
prelude.rs
