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: SafeParser> SafeParser for Ref<Inner> {
70    open spec fn safe_inv(&self) -> bool {
71        self.0.safe_inv()
72    }
73
74    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
75        self.0.lemma_parse_safe(ibuf);
76    }
77}
78
79impl<Inner: Productive> Productive for Ref<Inner> {
80    open spec fn productive_inv(&self) -> bool {
81        self.0.productive_inv()
82    }
83
84    proof fn lemma_productive(&self, ibuf: Seq<u8>) {
85        self.0.lemma_productive(ibuf);
86    }
87}
88
89impl<Inner: SoundParser> SoundParser for Ref<Inner> {
90    open spec fn sound_inv(&self) -> bool {
91        self.0.sound_inv()
92    }
93
94    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
95        self.0.lemma_parse_sound_consumption(ibuf);
96    }
97
98    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
99        self.0.lemma_parse_sound_value(ibuf);
100    }
101}
102
103impl<Inner: NonTailFmt> NonTailFmt for Ref<Inner> {
104    open spec fn serialize_dps_inv(&self) -> bool {
105        self.0.serialize_dps_inv()
106    }
107
108    proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>) {
109        self.0.lemma_serialize_dps_prepend(v, obuf);
110    }
111
112    proof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>) {
113        self.0.lemma_serialize_dps_len(v, obuf);
114    }
115}
116
117impl<Inner: GoodSerializer> GoodSerializer for Ref<Inner> {
118    open spec fn serialize_inv(&self) -> bool {
119        self.0.serialize_inv()
120    }
121
122    proof fn lemma_serialize_len(&self, v: Self::SVal) {
123        self.0.lemma_serialize_len(v);
124    }
125}
126
127impl<Inner: SPRoundTripDps> SPRoundTripDps for Ref<Inner> {
128    open spec fn unambiguous(&self) -> bool {
129        self.0.unambiguous()
130    }
131
132    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
133        self.0.theorem_serialize_dps_parse_roundtrip(v, obuf);
134    }
135}
136
137impl<Inner: NonMalleable> NonMalleable for Ref<Inner> {
138    open spec fn nonmal_inv(&self) -> bool {
139        self.0.nonmal_inv()
140    }
141
142    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
143        self.0.lemma_parse_non_malleable(buf1, buf2);
144    }
145}
146
147impl<Inner: NoLookAhead> NoLookAhead for Ref<Inner> {
148    open spec fn no_lookahead_inv(&self) -> bool {
149        self.0.no_lookahead_inv()
150    }
151
152    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
153        self.0.lemma_no_lookahead(i1, i2);
154    }
155}
156
157impl<Inner: EquivSerializersGeneral> EquivSerializersGeneral for Ref<Inner> {
158    open spec fn equiv_general_inv(&self) -> bool {
159        self.0.equiv_general_inv()
160    }
161
162    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
163        self.0.lemma_serialize_equiv(v, obuf);
164    }
165}
166
167impl<Inner: EquivSerializers> EquivSerializers for Ref<Inner> {
168    open spec fn equiv_inv(&self) -> bool {
169        self.0.equiv_inv()
170    }
171
172    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
173        self.0.lemma_serialize_equiv_on_empty(v);
174    }
175}
176
177impl<I, Inner> Parser<I> for Ref<Inner> where I: View<V = Seq<u8>>, Inner: Parser<I> {
178    type PT = Inner::PT;
179
180    open spec fn exec_inv(&self) -> bool {
181        self.0.exec_inv()
182    }
183
184    fn parse(&self, ibuf: &I) -> PResult<Self::PT> {
185        self.0.parse(ibuf)
186    }
187}
188
189impl<Output, Inner, T> Serializer<Output, &T> for Ref<Inner> where
190    Output: OutputBuf,
191    T: DeepView + ?Sized,
192    Inner: Serializer<Output, T>,
193 {
194    #[verifier::prophetic]
195    open spec fn exec_inv(&self) -> bool {
196        self.0.exec_inv()
197    }
198
199    fn serialize_into(&self, v: &&T, obuf: &mut Output) {
200        self.0.serialize_into(*v, obuf);
201    }
202}
203
204impl<Inner, T> Prepare<&T> for Ref<Inner> where T: DeepView + ?Sized, Inner: Prepare<T> {
205    open spec fn exec_inv(&self) -> bool {
206        self.0.exec_inv()
207    }
208
209    fn prepare(&self, v: &&T) -> Result<usize, PreSerializeError> {
210        self.0.prepare(*v)
211    }
212}
213
214impl<Inner, T> ByteLen<&T> for Ref<Inner> where T: DeepView + ?Sized, Inner: ByteLen<T> {
215    open spec fn exec_inv(&self) -> bool {
216        self.0.exec_inv()
217    }
218
219    fn length(&self, v: &&T) -> usize {
220        self.0.length(*v)
221    }
222}
223
224} // verus!
vest_lib/combinators/reference.rs

vest_lib/combinators/
reference.rs
