vest_lib/combinators/mapped/
mod.rs

1//! Semantic type transformations over structural combinator values.
2//!
3//! [`Mapped`] carries full round trips when its mapper is lossless and sound;
4//! [`TryMap`] also admits a fallible executable conversion.
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 vstd::prelude::*;
13
14verus! {
15
16/// `Mapped { inner, mapper }` transforms the inner combinator's value type.
17///
18/// Lossless mappers preserve all format properties including parser soundness and non-malleability, while lossy mappers may introduce malleability.
19#[derive(Copy)]
20pub struct Mapped<Inner, M> {
21    /// The inner combinator whose values are being transformed.
22    pub inner: Inner,
23    /// The mapping between the inner and outer value types.
24    pub mapper: M,
25}
26
27impl<Inner: Clone, M: Clone> Clone for Mapped<Inner, M> {
28    fn clone(&self) -> (cloned: Self)
29        ensures
30            call_ensures(Inner::clone, (&self.inner,), cloned.inner),
31            call_ensures(M::clone, (&self.mapper,), cloned.mapper),
32    {
33        Mapped { inner: self.inner.clone(), mapper: self.mapper.clone() }
34    }
35}
36
37/// `TryMap { inner, mapper }` is the derived combinator
38/// `Mapped { inner: Refined(inner, |v| mapper.wf_in(v)), mapper }`.
39///
40/// Parsing fails when the parsed inner value does not satisfy `mapper.wf_in`.
41/// Serialization maps values back with `mapper.spec_map_rev`, and consistency
42/// requires both `mapper.wf_out(v)` and that the reverse-mapped inner value is
43/// consistent and satisfies `mapper.wf_in`.
44#[derive(Copy)]
45pub struct TryMap<Inner, M> {
46    /// The inner combinator whose values are being transformed.
47    pub inner: Inner,
48    /// The mapping between the inner and outer value types.
49    pub mapper: M,
50}
51
52impl<Inner: Clone, M: Clone> Clone for TryMap<Inner, M> {
53    fn clone(&self) -> (cloned: Self)
54        ensures
55            call_ensures(Inner::clone, (&self.inner,), cloned.inner),
56            call_ensures(M::clone, (&self.mapper,), cloned.mapper),
57    {
58        TryMap { inner: self.inner.clone(), mapper: self.mapper.clone() }
59    }
60}
61
62} // verus!
vest_lib/combinators/mapped/mod.rs

vest_lib/combinators/mapped/
mod.rs
