vest_lib/combinators/named/
mod.rs

1//! Name-carrying wrapper for runtime error reporting.
2//!
3//! [`Named`] preserves the child's format semantics and attaches a static name
4//! while parse or preparation errors propagate outward.
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/// Transparent wrapper around `Inner` that annotates runtime parse errors with a static format
18/// name.
19///
20/// The semantic format is unchanged: parsing, consistency, serialization, and all proof
21/// obligations are delegated to `Inner`.
22#[derive(Copy)]
23pub struct Named<Inner>(pub &'static str, pub Inner);
24
25impl<Inner: Clone> Clone for Named<Inner> {
26    fn clone(&self) -> (cloned: Self)
27        ensures
28            call_ensures(Inner::clone, (&self.1,), cloned.1),
29    {
30        Named(self.0, self.1.clone())
31    }
32}
33
34impl<Inner: LeafNonMalleable> LeafNonMalleable for Named<Inner> {
35    proof fn nonmal_leaf_inv(&self) {
36        self.1.nonmal_leaf_inv();
37    }
38}
39
40} // verus!
vest_lib/combinators/named/mod.rs

vest_lib/combinators/named/
mod.rs
