verdict_parser/common/
cached.rs

1use super::*;
2use std::ops::Deref;
3use vstd::prelude::*;
4
5verus! {
6
7/// Same behavior as T, but also returns the slice
8/// consumed by T in the exec version
9#[derive(View)]
10pub struct Cached<T>(pub T);
11
12pub struct CachedValue<'a, C: Combinator> where
13    C::V: SecureSpecCombinator<SpecResult = <C::Owned as View>::V>,
14{
15    inner: C::Result<'a>,
16    combinator: Ghost<C>,
17    serialized: &'a [u8],
18}
19
20/// View of CachedValue discards the serialization
21impl<'a, C: Combinator> View for CachedValue<'a, C> where
22    C::V: SecureSpecCombinator<SpecResult = <C::Owned as View>::V>,
23    for<'b> C::Result<'b>: View,
24{
25    type V = <C::Result<'a> as View>::V;
26
27    closed spec fn view(&self) -> Self::V {
28        self.inner@
29    }
30}
31
32impl<'a, C: Combinator> PolyfillClone for CachedValue<'a, C> where
33    C::V: SecureSpecCombinator<SpecResult = <C::Owned as View>::V>,
34    C::Result<'a>: PolyfillClone,
35{
36    #[inline(always)]
37    fn clone(&self) -> Self {
38        proof {
39            use_type_invariant(self);
40        }
41        CachedValue {
42            inner: self.inner.clone(),
43            combinator: self.combinator,
44            serialized: self.serialized,
45        }
46    }
47}
48
49impl<'a, C: Combinator> CachedValue<'a, C> where
50    C::V: SecureSpecCombinator<SpecResult = <C::Owned as View>::V>,
51{
52    #[verifier::type_invariant]
53    closed spec fn inv(self) -> bool {
54        let res = self.combinator@@.spec_serialize(self.inner@);
55        &&& res.is_ok()
56        &&& self.serialized@ =~= res.unwrap()
57    }
58
59    #[inline(always)]
60    pub fn get(&self) -> (res: &C::Result<'a>)
61        ensures res@ == self@
62    {
63        &self.inner
64    }
65
66    /// Since we can't expose any of self's fields, we can't check if
67    /// the combinator expected by the user is the same as self.combinator
68    ///
69    /// But the type of self.combinator is exposed to the user, and
70    /// if there is a unique constructor for that type, then we can
71    /// deduce that the serialized result would be the same.
72    #[inline(always)]
73    pub fn serialize(&self) -> (res: &[u8])
74        requires forall |c1: C, c2: C| c1.view() == c2.view()
75        ensures forall |c: C| (#[trigger] c.view()).spec_serialize(self@) matches Ok(r) && r == res@
76    {
77        proof {
78            use_type_invariant(self);
79        }
80        self.serialized
81    }
82}
83
84impl<T: SpecCombinator> SpecCombinator for Cached<T> {
85    type SpecResult = T::SpecResult;
86
87    open spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()> {
88        self.0.spec_parse(s)
89    }
90
91    open spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()> {
92        self.0.spec_serialize(v)
93    }
94
95    proof fn spec_parse_wf(&self, s: Seq<u8>) {
96        self.0.spec_parse_wf(s)
97    }
98}
99
100impl<T: SecureSpecCombinator> SecureSpecCombinator for Cached<T> {
101    open spec fn is_prefix_secure() -> bool {
102        T::is_prefix_secure()
103    }
104
105    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
106        self.0.lemma_prefix_secure(s1, s2)
107    }
108
109    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult) {
110        self.0.theorem_serialize_parse_roundtrip(v)
111    }
112
113    proof fn theorem_parse_serialize_roundtrip(&self, s: Seq<u8>) {
114        self.0.theorem_parse_serialize_roundtrip(s)
115    }
116}
117
118impl<T: Combinator> Combinator for Cached<T> where
119    T::V: SecureSpecCombinator<SpecResult = <T::Owned as View>::V>,
120{
121    type Result<'a> = CachedValue<'a, T>;
122    type Owned = T::Owned;
123
124    open spec fn spec_length(&self) -> Option<usize> {
125        self.0.spec_length()
126    }
127
128    fn length(&self) -> Option<usize> {
129        self.0.length()
130    }
131
132    open spec fn parse_requires(&self) -> bool {
133        self.0.parse_requires()
134    }
135
136    #[inline(always)]
137    fn parse<'a>(&self, s: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>)
138    {
139        let (n, x) = self.0.parse(s)?;
140        proof {
141            assert(s.len() <= usize::MAX);
142            self@.theorem_parse_serialize_roundtrip(s@);
143        }
144        Ok((n, CachedValue { inner: x, combinator: Ghost(self.0), serialized: slice_take(s, n) }))
145    }
146
147    open spec fn serialize_requires(&self) -> bool {
148        self.0.serialize_requires()
149    }
150
151    #[inline(always)]
152    fn serialize(&self, v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> (res: Result<
153        usize,
154        SerializeError,
155    >) {
156        self.0.serialize(v.inner, data, pos)
157    }
158}
159
160}
161
162impl<'a, C: Combinator> std::fmt::Debug for CachedValue<'a, C>
163where
164    C::V: SecureSpecCombinator<SpecResult = <C::Owned as View>::V>,
165    C::Result<'a>: std::fmt::Debug,
166{
167    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
168        self.inner.fmt(f)
169    }
170}
verdict_parser/common/cached.rs

verdict_parser/common/
cached.rs
