vest_lib/combinators/mapped/
spec.rs

1//! Mapper traits for type transformations used by [`super::Mapped`].
2use crate::{
3    combinators::refined::Refined,
4    core::{proof::*, spec::*},
5};
6use vstd::prelude::*;
7
8verus! {
9
10/// A bidirectional mapping between two types (forward for parsing, reverse for
11/// serialization). For roundtrip guarantees, implement and prove
12/// [`LossyMapper`] or [`LosslessMapper`] as appropriate.
13pub trait SpecMapper {
14    /// The input type.
15    type In;
16
17    /// The output type.
18    type Out;
19
20    /// Forward mapping (used during parsing).
21    spec fn spec_map(&self, i: Self::In) -> Self::Out;
22
23    /// Reverse mapping (used during serialization).
24    spec fn spec_map_rev(&self, o: Self::Out) -> Self::In;
25
26    /// Optional refinement predicates on the input type.
27    ///
28    /// This is the precondition for [`LosslessMapper::lemma_lossless_mapper`].
29    open spec fn wf_in(&self, i: Self::In) -> bool {
30        true
31    }
32
33    /// Optional refinement predicates on the output type.
34    ///
35    /// This is the precondition for [`LossyMapper::lemma_sound_mapper`].
36    open spec fn wf_out(&self, o: Self::Out) -> bool {
37        true
38    }
39}
40
41/// A [`SpecMapper`] that can be lossy (i.e., malleable).
42pub trait LossyMapper: SpecMapper {
43    /// A sound mapper should satisfy `spec_map(spec_map_rev(o)) == o` for all well-formed `o`.
44    /// That is, once `Self::Out` values are mapped to `Self::In`, `spec_map` should map them back to the original `Self::Out` values.
45    proof fn lemma_sound_mapper(&self, o: Self::Out)
46        requires
47            self.wf_out(o),
48        ensures
49            self.spec_map(self.spec_map_rev(o)) == o,
50    ;
51
52    proof fn lemma_mapper_wf_out_in(&self, o: Self::Out)
53        requires
54            self.wf_out(o),
55        ensures
56            self.wf_in(self.spec_map_rev(o)),
57    ;
58}
59
60/// A [`SpecMapper`] that is lossless (i.e., non-malleable).
61pub trait LosslessMapper: LossyMapper {
62    /// A lossless mapper should satisfy `spec_map_rev(spec_map(i)) == i` for all well-formed `i`.
63    /// That is, `spec_map` should be injective on well-formed `Self::In` values, and `spec_map_rev` should be its inverse.
64    proof fn lemma_lossless_mapper(&self, i: Self::In)
65        requires
66            self.wf_in(i),
67        ensures
68            self.spec_map_rev(self.spec_map(i)) == i,
69    ;
70
71    /// For well-formed `i`, `spec_map(i)` should also be well-formed.
72    proof fn lemma_mapper_wf_in_out(&self, i: Self::In)
73        requires
74            self.wf_in(i),
75        ensures
76            self.wf_out(self.spec_map(i)),
77    ;
78}
79
80impl<Inner, M> SpecParser for super::Mapped<Inner, M> where
81    Inner: SpecParser,
82    M: SpecMapper<In = Inner::PVal>,
83 {
84    type PVal = M::Out;
85
86    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, M::Out)> {
87        match self.inner.spec_parse(ibuf) {
88            Some((n, v)) => Some((n, self.mapper.spec_map(v))),
89            None => None,
90        }
91    }
92}
93
94impl<Inner, M> SafeParser for super::Mapped<Inner, M> where
95    Inner: SafeParser,
96    M: SpecMapper<In = Inner::PVal>,
97 {
98    open spec fn safe_inv(&self) -> bool {
99        self.inner.safe_inv()
100    }
101
102    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
103        assert(self.safe_inv());
104        self.inner.lemma_parse_safe(ibuf);
105    }
106}
107
108impl<Inner, M> SoundParser for super::Mapped<Inner, M> where
109    Inner: SoundParser,
110    M: LosslessMapper<In = Inner::PVal>,
111 {
112    open spec fn sound_inv(&self) -> bool {
113        &&& self.inner.sound_inv()
114        &&& forall|v: Inner::T| #![auto] self.inner.consistent(v) ==> self.mapper.wf_in(v)
115    }
116
117    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
118        assert(self.sound_inv());
119        self.inner.lemma_parse_sound_consumption(ibuf);
120        self.inner.lemma_parse_sound_value(ibuf);
121        if let Some((_n, inner_v)) = self.inner.spec_parse(ibuf) {
122            assert(self.mapper.wf_in(inner_v));
123            self.mapper.lemma_lossless_mapper(inner_v);
124        }
125    }
126
127    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
128        assert(self.sound_inv());
129        self.inner.lemma_parse_sound_value(ibuf);
130        if let Some((_n, inner_v)) = self.inner.spec_parse(ibuf) {
131            assert(self.mapper.wf_in(inner_v));
132            self.mapper.lemma_mapper_wf_in_out(inner_v);
133            self.mapper.lemma_lossless_mapper(inner_v);
134            assert(self.consistent(self.mapper.spec_map(inner_v)));
135        }
136    }
137}
138
139impl<Inner, M> Consistency for super::Mapped<Inner, M> where
140    Inner: Consistency,
141    M: SpecMapper<In = Inner::Val>,
142 {
143    type Val = M::Out;
144
145    open spec fn consistent(&self, v: Self::Val) -> bool {
146        &&& self.mapper.wf_out(v)
147        &&& self.inner.consistent(self.mapper.spec_map_rev(v))
148    }
149}
150
151impl<Inner, M> SpecSerializerDps for super::Mapped<Inner, M> where
152    Inner: SpecSerializerDps,
153    M: SpecMapper<In = Inner::SValue>,
154 {
155    type SValue = M::Out;
156
157    open spec fn spec_serialize_dps(&self, v: M::Out, obuf: Seq<u8>) -> Seq<u8> {
158        self.inner.spec_serialize_dps(self.mapper.spec_map_rev(v), obuf)
159    }
160}
161
162impl<Inner, M> NonTailFmt for super::Mapped<Inner, M> where
163    Inner: NonTailFmt,
164    M: SpecMapper<In = Inner::SValue>,
165 {
166    open spec fn serialize_dps_inv(&self) -> bool {
167        self.inner.serialize_dps_inv()
168    }
169
170    proof fn lemma_serialize_dps_prepend(&self, v: M::Out, obuf: Seq<u8>) {
171        assert(self.serialize_dps_inv());
172        self.inner.lemma_serialize_dps_prepend(self.mapper.spec_map_rev(v), obuf);
173    }
174
175    proof fn lemma_serialize_dps_len(&self, v: M::Out, obuf: Seq<u8>) {
176        assert(self.serialize_dps_inv());
177        self.inner.lemma_serialize_dps_len(self.mapper.spec_map_rev(v), obuf);
178    }
179}
180
181impl<Inner, M> GoodSerializer for super::Mapped<Inner, M> where
182    Inner: GoodSerializer,
183    M: SpecMapper<In = Inner::SVal>,
184 {
185    open spec fn serialize_inv(&self) -> bool {
186        self.inner.serialize_inv()
187    }
188
189    proof fn lemma_serialize_len(&self, v: M::Out) {
190        assert(self.serialize_inv());
191        self.inner.lemma_serialize_len(self.mapper.spec_map_rev(v));
192    }
193}
194
195impl<Inner, M> SpecByteLen for super::Mapped<Inner, M> where
196    Inner: SpecByteLen,
197    M: SpecMapper<In = Inner::T>,
198 {
199    type T = M::Out;
200
201    open spec fn byte_len(&self, v: Self::T) -> nat {
202        self.inner.byte_len(self.mapper.spec_map_rev(v))
203    }
204}
205
206impl<Inner, M> MinMaxByteLen for super::Mapped<Inner, M> where
207    Inner: MinMaxByteLen,
208    M: SpecMapper<In = Inner::T>,
209 {
210    open spec fn min(&self) -> nat {
211        self.inner.min()
212    }
213
214    open spec fn max(&self) -> nat {
215        self.inner.max()
216    }
217
218    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
219        self.inner.lemma_min_max_byte_len(self.mapper.spec_map_rev(v));
220    }
221}
222
223impl<Inner, M> StaticByteLen for super::Mapped<Inner, M> where
224    Inner: StaticByteLen,
225    M: SpecMapper<In = Inner::T>,
226 {
227    open spec fn static_byte_len() -> nat {
228        Inner::static_byte_len()
229    }
230
231    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
232        self.inner.lemma_static_len_matches_byte_len(self.mapper.spec_map_rev(v));
233    }
234}
235
236impl<Inner, M> SpecSerializer for super::Mapped<Inner, M> where
237    Inner: SpecSerializer,
238    M: SpecMapper<In = Inner::SVal>,
239 {
240    type SVal = M::Out;
241
242    open spec fn spec_serialize(&self, v: M::Out) -> Seq<u8> {
243        self.inner.spec_serialize(self.mapper.spec_map_rev(v))
244    }
245}
246
247/*
248 * Support for plain spec closures as mappers
249 */
250
251pub type FnSpecMapper<In, Out> = (spec_fn(In) -> Out, spec_fn(Out) -> In);
252
253impl<In, Out> SpecMapper for FnSpecMapper<In, Out> {
254    type In = In;
255
256    type Out = Out;
257
258    open spec fn spec_map(&self, i: Self::In) -> Self::Out {
259        (self.0)(i)
260    }
261
262    open spec fn spec_map_rev(&self, o: Self::Out) -> Self::In {
263        (self.1)(o)
264    }
265}
266
267impl<Inner: SpecParser, Out> SpecParser for super::Mapped<Inner, spec_fn(Inner::PVal) -> Out> {
268    type PVal = Out;
269
270    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Out)> {
271        match self.inner.spec_parse(ibuf) {
272            Some((n, v)) => Some((n, (self.mapper)(v))),
273            None => None,
274        }
275    }
276}
277
278impl<Inner: SafeParser, Out> SafeParser for super::Mapped<Inner, spec_fn(Inner::PVal) -> Out> {
279    open spec fn safe_inv(&self) -> bool {
280        self.inner.safe_inv()
281    }
282
283    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
284        self.inner.lemma_parse_safe(ibuf);
285    }
286}
287
288impl<Inner: Productive, Out> Productive for super::Mapped<Inner, spec_fn(Inner::PVal) -> Out> {
289    open spec fn productive_inv(&self) -> bool {
290        self.inner.productive_inv()
291    }
292
293    proof fn lemma_productive(&self, s: Seq<u8>) {
294        self.inner.lemma_productive(s);
295    }
296}
297
298impl<Inner: SoundParser, Out> SoundParser for super::Mapped<Inner, FnSpecMapper<Inner::PVal, Out>> {
299    open spec fn sound_inv(&self) -> bool {
300        &&& self.inner.sound_inv()
301        &&& forall|v: Inner::T| #[trigger]
302            self.inner.consistent(v) ==> (self.mapper.1)((self.mapper.0)(v)) == v
303    }
304
305    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
306        self.inner.lemma_parse_sound_consumption(ibuf);
307        self.inner.lemma_parse_sound_value(ibuf);
308    }
309
310    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
311        self.inner.lemma_parse_sound_value(ibuf);
312    }
313}
314
315impl<Inner: SpecSerializerDps, Out> SpecSerializerDps for super::Mapped<
316    Inner,
317    spec_fn(Out) -> Inner::SValue,
318> {
319    type SValue = Out;
320
321    open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
322        self.inner.spec_serialize_dps((self.mapper)(v), obuf)
323    }
324}
325
326impl<Inner: SpecSerializer, Out> SpecSerializer for super::Mapped<
327    Inner,
328    spec_fn(Out) -> Inner::SVal,
329> {
330    type SVal = Out;
331
332    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
333        self.inner.spec_serialize((self.mapper)(v))
334    }
335}
336
337/*
338 * Support for [`BiMap`] that can be used for both spec mappers and exec mappers.
339 */
340
341pub trait SpecMap {
342    type Input;
343
344    type Output;
345
346    spec fn spec_map(&self, i: Self::Input) -> Self::Output;
347}
348
349impl<I, O> SpecMap for spec_fn(I) -> O {
350    type Input = I;
351
352    type Output = O;
353
354    open spec fn spec_map(&self, i: Self::Input) -> Self::Output {
355        (self)(i)
356    }
357}
358
359#[derive(Copy)]
360pub struct BiMap<M, MRev>(pub M, pub MRev);
361
362impl<M: Clone, MRev: Clone> Clone for BiMap<M, MRev> {
363    fn clone(&self) -> (cloned: Self)
364        ensures
365            call_ensures(M::clone, (&self.0,), cloned.0),
366            call_ensures(MRev::clone, (&self.1,), cloned.1),
367    {
368        BiMap(self.0.clone(), self.1.clone())
369    }
370}
371
372pub type BiMapper<In, Out> = BiMap<spec_fn(In) -> Out, spec_fn(Out) -> In>;
373
374impl<M, MRev> BiMap<M, MRev> where M: SpecMap, MRev: SpecMap<Input = M::Output, Output = M::Input> {
375    pub open spec fn sound(&self, o: M::Output) -> bool {
376        let BiMap(m, mrev) = *self;
377        m.spec_map(mrev.spec_map(o)) == o
378    }
379
380    pub open spec fn lossless(&self, i: M::Input) -> bool {
381        let BiMap(m, mrev) = *self;
382        mrev.spec_map(m.spec_map(i)) == i
383    }
384}
385
386impl<Inner, M, MRev> SpecParser for super::Mapped<Inner, BiMap<M, MRev>> where
387    Inner: SpecParser,
388    M: SpecMap<Input = Inner::PVal>,
389    MRev: SpecMap<Input = M::Output, Output = M::Input>,
390 {
391    type PVal = M::Output;
392
393    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, M::Output)> {
394        match self.inner.spec_parse(ibuf) {
395            Some((n, v)) => Some((n, self.mapper.0.spec_map(v))),
396            None => None,
397        }
398    }
399}
400
401impl<Inner, M, MRev> SpecSerializerDps for super::Mapped<Inner, BiMap<M, MRev>> where
402    Inner: SpecSerializerDps,
403    M: SpecMap<Input = Inner::SValue>,
404    MRev: SpecMap<Input = M::Output, Output = M::Input>,
405 {
406    type SValue = M::Output;
407
408    open spec fn spec_serialize_dps(&self, v: M::Output, obuf: Seq<u8>) -> Seq<u8> {
409        self.inner.spec_serialize_dps(self.mapper.1.spec_map(v), obuf)
410    }
411}
412
413impl<Inner, M, MRev> SpecSerializer for super::Mapped<Inner, BiMap<M, MRev>> where
414    Inner: SpecSerializer,
415    M: SpecMap<Input = Inner::SVal>,
416    MRev: SpecMap<Input = M::Output, Output = M::Input>,
417 {
418    type SVal = M::Output;
419
420    open spec fn spec_serialize(&self, v: M::Output) -> Seq<u8> {
421        self.inner.spec_serialize(self.mapper.1.spec_map(v))
422    }
423}
424
425impl<Inner, M, MRev> Consistency for super::Mapped<Inner, BiMap<M, MRev>> where
426    Inner: Consistency,
427    M: SpecMap<Input = Inner::Val>,
428    MRev: SpecMap<Input = M::Output, Output = M::Input>,
429 {
430    type Val = M::Output;
431
432    open spec fn consistent(&self, v: Self::Val) -> bool {
433        self.inner.consistent(self.mapper.1.spec_map(v))
434    }
435}
436
437impl<Inner, M, MRev> SpecByteLen for super::Mapped<Inner, BiMap<M, MRev>> where
438    Inner: SpecByteLen,
439    M: SpecMap<Input = Inner::T>,
440    MRev: SpecMap<Input = M::Output, Output = M::Input>,
441 {
442    type T = M::Output;
443
444    open spec fn byte_len(&self, v: Self::T) -> nat {
445        self.inner.byte_len(self.mapper.1.spec_map(v))
446    }
447}
448
449impl<Inner, M, MRev> SafeParser for super::Mapped<Inner, BiMap<M, MRev>> where
450    Inner: SafeParser,
451    M: SpecMap<Input = Inner::PVal>,
452    MRev: SpecMap<Input = M::Output, Output = M::Input>,
453 {
454    open spec fn safe_inv(&self) -> bool {
455        self.inner.safe_inv()
456    }
457
458    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
459        self.inner.lemma_parse_safe(ibuf);
460    }
461}
462
463impl<Inner, M, MRev> SoundParser for super::Mapped<Inner, BiMap<M, MRev>> where
464    Inner: SoundParser,
465    M: SpecMap<Input = Inner::PVal>,
466    MRev: SpecMap<Input = M::Output, Output = M::Input>,
467 {
468    #[verifier::inline]
469    open spec fn sound_inv(&self) -> bool {
470        &&& self.inner.sound_inv()
471        &&& forall|i: Inner::T| #[trigger] self.inner.consistent(i) ==> self.mapper.lossless(i)
472    }
473
474    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
475        self.inner.lemma_parse_sound_consumption(ibuf);
476        self.inner.lemma_parse_sound_value(ibuf);
477    }
478
479    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
480        self.inner.lemma_parse_sound_value(ibuf);
481    }
482}
483
484impl<Inner, M, MRev> NonTailFmt for super::Mapped<Inner, BiMap<M, MRev>> where
485    Inner: NonTailFmt,
486    M: SpecMap<Input = Inner::SValue>,
487    MRev: SpecMap<Input = M::Output, Output = M::Input>,
488 {
489    open spec fn serialize_dps_inv(&self) -> bool {
490        self.inner.serialize_dps_inv()
491    }
492
493    proof fn lemma_serialize_dps_prepend(&self, v: M::Output, obuf: Seq<u8>) {
494        self.inner.lemma_serialize_dps_prepend(self.mapper.1.spec_map(v), obuf);
495    }
496
497    proof fn lemma_serialize_dps_len(&self, v: M::Output, obuf: Seq<u8>) {
498        self.inner.lemma_serialize_dps_len(self.mapper.1.spec_map(v), obuf);
499    }
500}
501
502impl<Inner, M, MRev> GoodSerializer for super::Mapped<Inner, BiMap<M, MRev>> where
503    Inner: GoodSerializer,
504    M: SpecMap<Input = Inner::SVal>,
505    MRev: SpecMap<Input = M::Output, Output = M::Input>,
506 {
507    open spec fn serialize_inv(&self) -> bool {
508        self.inner.serialize_inv()
509    }
510
511    proof fn lemma_serialize_len(&self, v: M::Output) {
512        self.inner.lemma_serialize_len(self.mapper.1.spec_map(v));
513    }
514}
515
516impl<Inner, M, MRev> MinMaxByteLen for super::Mapped<Inner, BiMap<M, MRev>> where
517    Inner: MinMaxByteLen,
518    M: SpecMap<Input = Inner::T>,
519    MRev: SpecMap<Input = M::Output, Output = M::Input>,
520 {
521    open spec fn min(&self) -> nat {
522        self.inner.min()
523    }
524
525    open spec fn max(&self) -> nat {
526        self.inner.max()
527    }
528
529    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
530        self.inner.lemma_min_max_byte_len(self.mapper.1.spec_map(v));
531    }
532}
533
534impl<Inner, M, MRev> StaticByteLen for super::Mapped<Inner, BiMap<M, MRev>> where
535    Inner: StaticByteLen,
536    M: SpecMap<Input = Inner::T>,
537    MRev: SpecMap<Input = M::Output, Output = M::Input>,
538 {
539    open spec fn static_byte_len() -> nat {
540        Inner::static_byte_len()
541    }
542
543    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
544        self.inner.lemma_static_len_matches_byte_len(self.mapper.1.spec_map(v));
545    }
546}
547
548pub type TryMapPred<In> = PredFnSpec<In>;
549
550pub type TryMapInner<Inner, M> = super::Mapped<
551    Refined<Inner, TryMapPred<<M as SpecMapper>::In>>,
552    M,
553>;
554
555impl<Inner, M: SpecMapper> super::TryMap<Inner, M> {
556    pub open spec fn inner(&self) -> TryMapInner<Inner, M> {
557        super::Mapped {
558            inner: Refined(self.inner, |v: M::In| self.mapper.wf_in(v)),
559            mapper: self.mapper,
560        }
561    }
562}
563
564impl<Inner, M> SpecParser for super::TryMap<Inner, M> where
565    Inner: SpecParser,
566    M: SpecMapper<In = Inner::PVal>,
567 {
568    type PVal = M::Out;
569
570    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, M::Out)> {
571        self.inner().spec_parse(ibuf)
572    }
573}
574
575impl<Inner, M> SafeParser for super::TryMap<Inner, M> where
576    Inner: SafeParser,
577    M: SpecMapper<In = Inner::PVal>,
578 {
579    open spec fn safe_inv(&self) -> bool {
580        self.inner().safe_inv()
581    }
582
583    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
584        self.inner().lemma_parse_safe(ibuf);
585    }
586}
587
588impl<Inner, M> SoundParser for super::TryMap<Inner, M> where
589    Inner: SoundParser,
590    M: LosslessMapper<In = Inner::PVal>,
591 {
592    open spec fn sound_inv(&self) -> bool {
593        self.inner().sound_inv()
594    }
595
596    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
597        self.inner().lemma_parse_sound_consumption(ibuf);
598    }
599
600    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
601        self.inner().lemma_parse_sound_value(ibuf);
602    }
603}
604
605impl<Inner, M> Consistency for super::TryMap<Inner, M> where
606    Inner: Consistency,
607    M: SpecMapper<In = Inner::Val>,
608 {
609    type Val = M::Out;
610
611    open spec fn consistent(&self, v: Self::Val) -> bool {
612        self.inner().consistent(v)
613    }
614}
615
616impl<Inner, M> SpecSerializerDps for super::TryMap<Inner, M> where
617    Inner: SpecSerializerDps,
618    M: SpecMapper<In = Inner::SValue>,
619 {
620    type SValue = M::Out;
621
622    open spec fn spec_serialize_dps(&self, v: M::Out, obuf: Seq<u8>) -> Seq<u8> {
623        self.inner().spec_serialize_dps(v, obuf)
624    }
625}
626
627impl<Inner, M> NonTailFmt for super::TryMap<Inner, M> where
628    Inner: NonTailFmt,
629    M: SpecMapper<In = Inner::SValue>,
630 {
631    open spec fn serialize_dps_inv(&self) -> bool {
632        self.inner().serialize_dps_inv()
633    }
634
635    proof fn lemma_serialize_dps_prepend(&self, v: M::Out, obuf: Seq<u8>) {
636        self.inner().lemma_serialize_dps_prepend(v, obuf);
637    }
638
639    proof fn lemma_serialize_dps_len(&self, v: M::Out, obuf: Seq<u8>) {
640        self.inner().lemma_serialize_dps_len(v, obuf);
641    }
642}
643
644impl<Inner, M> GoodSerializer for super::TryMap<Inner, M> where
645    Inner: GoodSerializer,
646    M: SpecMapper<In = Inner::SVal>,
647 {
648    open spec fn serialize_inv(&self) -> bool {
649        self.inner().serialize_inv()
650    }
651
652    proof fn lemma_serialize_len(&self, v: M::Out) {
653        self.inner().lemma_serialize_len(v);
654    }
655}
656
657impl<Inner, M> SpecByteLen for super::TryMap<Inner, M> where
658    Inner: SpecByteLen,
659    M: SpecMapper<In = Inner::T>,
660 {
661    type T = M::Out;
662
663    open spec fn byte_len(&self, v: Self::T) -> nat {
664        self.inner().byte_len(v)
665    }
666}
667
668impl<Inner, M> MinMaxByteLen for super::TryMap<Inner, M> where
669    Inner: MinMaxByteLen,
670    M: SpecMapper<In = Inner::T>,
671 {
672    open spec fn min(&self) -> nat {
673        self.inner().min()
674    }
675
676    open spec fn max(&self) -> nat {
677        self.inner().max()
678    }
679
680    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
681        self.inner().lemma_min_max_byte_len(v);
682    }
683}
684
685impl<Inner, M> StaticByteLen for super::TryMap<Inner, M> where
686    Inner: StaticByteLen,
687    M: SpecMapper<In = Inner::T>,
688 {
689    open spec fn static_byte_len() -> nat {
690        TryMapInner::<Inner, M>::static_byte_len()
691    }
692
693    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
694        self.inner().lemma_static_len_matches_byte_len(v);
695    }
696}
697
698impl<Inner, M> SpecSerializer for super::TryMap<Inner, M> where
699    Inner: SpecSerializer,
700    M: SpecMapper<In = Inner::SVal>,
701 {
702    type SVal = M::Out;
703
704    open spec fn spec_serialize(&self, v: M::Out) -> Seq<u8> {
705        self.inner().spec_serialize(v)
706    }
707}
708
709} // verus!
vest_lib/combinators/mapped/spec.rs

vest_lib/combinators/mapped/
spec.rs
