vest/regular/
builder.rs

1use crate::properties::*;
2use vstd::prelude::*;
3
4verus! {
5
6/// An abstraction over a suspended computation involving a sequence of bytes.
7pub trait Builder {
8    /// The value of the computation.
9    spec fn value(&self) -> Seq<u8>;
10
11    /// Ensures that the value of the computation is well-formed.
12    proof fn value_wf(&self)
13        ensures
14            self.value().len() <= usize::MAX,
15    ;
16
17    /// The length of the bytes value.
18    fn length(&self) -> (res: usize)
19        ensures
20            res == self.value().len(),
21    ;
22
23    /// Serializes the value of the computation into a mutable byte vector.
24    fn into_mut_vec(&self, data: &mut Vec<u8>, pos: usize)
25        requires
26            0 <= pos + self.value().len() <= old(data)@.len() <= usize::MAX,
27        ensures
28            data@.len() == old(data)@.len(),
29            seq_splice(old(data)@, pos, self.value()) == data@,
30    ;
31
32    /// Serializes the value of the computation into a byte vector.
33    fn into_vec(&self) -> (res: Vec<u8>)
34        ensures
35            res@ == self.value(),
36    {
37        let mut res = init_vec_u8(self.length());
38        self.into_mut_vec(&mut res, 0);
39        assert(res@ == seq_splice(res@, 0, self.value()));
40        assert(seq_splice(res@, 0, self.value()) == self.value());
41        res
42    }
43}
44
45/// Combinator that encapsulates a suspended computation for efficient serialization.
46pub struct BuilderCombinator<T>(pub T);
47
48impl<T> View for BuilderCombinator<T> {
49    type V = BuilderCombinator<T>;
50
51    open spec fn view(&self) -> Self::V {
52        *self
53    }
54}
55
56impl<T: Builder> SpecCombinator for BuilderCombinator<T> {
57    type SpecResult = ();
58
59    open spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, ()), ()> {
60        if s == self.0.value() {
61            Ok((s.len() as usize, ()))
62        } else {
63            Err(())
64        }
65    }
66
67    proof fn spec_parse_wf(&self, s: Seq<u8>) {
68    }
69
70    open spec fn spec_serialize(&self, v: ()) -> Result<Seq<u8>, ()> {
71        Ok(self.0.value())
72    }
73}
74
75impl<T: Builder> SecureSpecCombinator for BuilderCombinator<T> {
76    open spec fn is_prefix_secure() -> bool {
77        false
78    }
79
80    proof fn theorem_serialize_parse_roundtrip(&self, v: ()) {
81        self.0.value_wf()
82    }
83
84    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
85        self.0.value_wf();
86        assert(buf.subrange(0, buf.len() as int) == buf);
87    }
88
89    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
90    }
91}
92
93impl<T> Combinator for BuilderCombinator<T> where T: Builder + View, T::V: Builder {
94    type Result<'a> = ();
95
96    type Owned = ();
97
98    open spec fn spec_length(&self) -> Option<usize> {
99        None
100    }
101
102    fn length(&self) -> Option<usize> {
103        None
104    }
105
106    fn parse(&self, s: &[u8]) -> (res: Result<(usize, ()), ParseError>) {
107        let v = self.0.into_vec();
108        proof {
109            self.0.value_wf();
110        }
111        if compare_slice(s, v.as_slice()) {
112            Ok((s.len(), ()))
113        } else {
114            Err(ParseError::BuilderError)
115        }
116    }
117
118    fn serialize(&self, _v: (), data: &mut Vec<u8>, pos: usize) -> (res: Result<
119        usize,
120        SerializeError,
121    >) {
122        if self.0.length() <= data.len() && pos <= data.len() - self.0.length() {
123            self.0.into_mut_vec(data, pos);
124            assert(pos + self.0.value().len() <= data@.len());
125            assert(data@ == seq_splice(old(data)@, pos, self.spec_serialize(()).unwrap()));
126            assert(data@.subrange(pos as int, pos + self.0.value().len() as int) == self.0.value());
127            Ok(self.0.length())
128        } else {
129            Err(SerializeError::InsufficientBuffer)
130        }
131    }
132}
133
134} // verus!
vest/regular/builder.rs

vest/regular/
builder.rs
