vest_lib/combinators/
reference.rs

1//! Adapter for serializing a value through a shared reference.
2//!
3//! `Ref<F>` has exactly the same specification and parsing behavior as `F`,
4//! but its executable serializer, preparation, and length APIs accept `&T`
5//! whenever `F` accepts `T`. This is useful for nominal-value mappers which
6//! reverse-map a struct into a tuple of references to its fields.
7use crate::core::exec::output::OutputBuf;
8use crate::core::exec::{
9    parser::{PResult, Parser},
10    serializer::{ByteLen, PreSerializeError, Prepare, Serializer},
11};
12use crate::core::{proof::*, spec::*};
13use vstd::prelude::*;
14
15verus! {
16
17#[derive(Copy)]
18pub struct Ref<Inner>(pub Inner);
19
20impl<Inner: Clone> Clone for Ref<Inner> {
21    fn clone(&self) -> (cloned: Self)
22        ensures
23            call_ensures(Inner::clone, (&self.0,), cloned.0),
24    {
25        Ref(self.0.clone())
26    }
27}
28
29impl<Inner: SpecParser> SpecParser for Ref<Inner> {
30    type PVal = Inner::PVal;
31
32    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
33        self.0.spec_parse(ibuf)
34    }
35}
36
37impl<Inner: Consistency> Consistency for Ref<Inner> {
38    type Val = Inner::Val;
39
40    open spec fn consistent(&self, v: Self::Val) -> bool {
41        self.0.consistent(v)
42    }
43}
44
45impl<Inner: SpecSerializerDps> SpecSerializerDps for Ref<Inner> {
46    type SValue = Inner::SValue;
47
48    open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
49        self.0.spec_serialize_dps(v, obuf)
50    }
51}
52
53impl<Inner: SpecSerializer> SpecSerializer for Ref<Inner> {
54    type SVal = Inner::SVal;
55
56    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
57        self.0.spec_serialize(v)
58    }
59}
60
61impl<Inner: SpecByteLen> SpecByteLen for Ref<Inner> {
62    type T = Inner::T;
63
64    open spec fn byte_len(&self, v: Self::T) -> nat {
65        self.0.byte_len(v)
66    }
67}
68
69impl<Inner: StaticByteLen> StaticByteLen for Ref<Inner> {
70    open spec fn static_byte_len() -> nat {
71        Inner::static_byte_len()
72    }
73
74    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
75        self.0.lemma_static_len_matches_byte_len(v);
76    }
77}
78
79impl<Inner: ValueByteLen> ValueByteLen for Ref<Inner> {
80    open spec fn value_byte_len(v: Self::T) -> nat {
81        Inner::value_byte_len(v)
82    }
83
84    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
85        self.0.lemma_value_len_matches_byte_len(v);
86    }
87}
88
89impl<Inner: MinMaxByteLen> MinMaxByteLen for Ref<Inner> {
90    open spec fn min(&self) -> nat {
91        self.0.min()
92    }
93
94    open spec fn max(&self) -> nat {
95        self.0.max()
96    }
97
98    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
99        self.0.lemma_min_max_byte_len(v);
100    }
101}
102
103impl<Inner: SafeParser> SafeParser for Ref<Inner> {
104    open spec fn safe_inv(&self) -> bool {
105        self.0.safe_inv()
106    }
107
108    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
109        self.0.lemma_parse_safe(ibuf);
110    }
111}
112
113impl<Inner: Productive> Productive for Ref<Inner> {
114    open spec fn productive_inv(&self) -> bool {
115        self.0.productive_inv()
116    }
117
118    proof fn lemma_productive(&self, ibuf: Seq<u8>) {
119        self.0.lemma_productive(ibuf);
120    }
121}
122
123impl<Inner: SoundParser> SoundParser for Ref<Inner> {
124    open spec fn sound_inv(&self) -> bool {
125        self.0.sound_inv()
126    }
127
128    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
129        self.0.lemma_parse_sound_consumption(ibuf);
130    }
131
132    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
133        self.0.lemma_parse_sound_value(ibuf);
134    }
135}
136
137impl<Inner: NonTailFmt> NonTailFmt for Ref<Inner> {
138    open spec fn serialize_dps_inv(&self) -> bool {
139        self.0.serialize_dps_inv()
140    }
141
142    proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>) {
143        self.0.lemma_serialize_dps_prepend(v, obuf);
144    }
145
146    proof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>) {
147        self.0.lemma_serialize_dps_len(v, obuf);
148    }
149}
150
151impl<Inner: GoodSerializer> GoodSerializer for Ref<Inner> {
152    open spec fn serialize_inv(&self) -> bool {
153        self.0.serialize_inv()
154    }
155
156    proof fn lemma_serialize_len(&self, v: Self::SVal) {
157        self.0.lemma_serialize_len(v);
158    }
159}
160
161impl<Inner: SPRoundTripDps> SPRoundTripDps for Ref<Inner> {
162    open spec fn unambiguous(&self) -> bool {
163        self.0.unambiguous()
164    }
165
166    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
167        self.0.theorem_serialize_dps_parse_roundtrip(v, obuf);
168    }
169}
170
171impl<Inner: NonMalleable> NonMalleable for Ref<Inner> {
172    open spec fn nonmal_inv(&self) -> bool {
173        self.0.nonmal_inv()
174    }
175
176    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
177        self.0.lemma_parse_non_malleable(buf1, buf2);
178    }
179}
180
181impl<Inner: NoLookAhead> NoLookAhead for Ref<Inner> {
182    open spec fn no_lookahead_inv(&self) -> bool {
183        self.0.no_lookahead_inv()
184    }
185
186    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
187        self.0.lemma_no_lookahead(i1, i2);
188    }
189}
190
191impl<Inner: EquivSerializersGeneral> EquivSerializersGeneral for Ref<Inner> {
192    open spec fn equiv_general_inv(&self) -> bool {
193        self.0.equiv_general_inv()
194    }
195
196    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
197        self.0.lemma_serialize_equiv(v, obuf);
198    }
199}
200
201impl<Inner: EquivSerializers> EquivSerializers for Ref<Inner> {
202    open spec fn equiv_inv(&self) -> bool {
203        self.0.equiv_inv()
204    }
205
206    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
207        self.0.lemma_serialize_equiv_on_empty(v);
208    }
209}
210
211impl<I, Inner> Parser<I> for Ref<Inner> where I: View<V = Seq<u8>>, Inner: Parser<I> {
212    type PT = Inner::PT;
213
214    fn min_byte_len(&self) -> usize {
215        self.0.min_byte_len()
216    }
217
218    open spec fn exec_inv(&self) -> bool {
219        self.0.exec_inv()
220    }
221
222    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
223        self.0.parse(ibuf)
224    }
225}
226
227impl<Output, Inner, T> Serializer<Output, &T> for Ref<Inner> where
228    Output: OutputBuf,
229    T: DeepView + ?Sized,
230    Inner: Serializer<Output, T>,
231 {
232    #[verifier::prophetic]
233    open spec fn exec_inv(&self) -> bool {
234        self.0.exec_inv()
235    }
236
237    fn serialize_into(&self, v: &&T, obuf: &mut Output) {
238        self.0.serialize_into(*v, obuf);
239    }
240}
241
242impl<Inner, T> Prepare<&T> for Ref<Inner> where T: DeepView + ?Sized, Inner: Prepare<T> {
243    open spec fn exec_inv(&self) -> bool {
244        self.0.exec_inv()
245    }
246
247    fn prepare(&self, v: &&T) -> Result<usize, PreSerializeError> {
248        self.0.prepare(*v)
249    }
250}
251
252impl<Inner, T> ByteLen<&T> for Ref<Inner> where T: DeepView + ?Sized, Inner: ByteLen<T> {
253    open spec fn exec_inv(&self) -> bool {
254        self.0.exec_inv()
255    }
256
257    fn length(&self, v: &&T) -> usize {
258        self.0.length(*v)
259    }
260}
261
262} // verus!
vest_lib/combinators/reference.rs

vest_lib/combinators/
reference.rs
