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        self.inner.lemma_parse_sound_consumption(ibuf);
119        self.inner.lemma_parse_sound_value(ibuf);
120        if let Some((_n, inner_v)) = self.inner.spec_parse(ibuf) {
121            assert(self.mapper.wf_in(inner_v));
122            self.mapper.lemma_lossless_mapper(inner_v);
123        }
124    }
125
126    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
127        self.inner.lemma_parse_sound_value(ibuf);
128        if let Some((_n, inner_v)) = self.inner.spec_parse(ibuf) {
129            assert(self.mapper.wf_in(inner_v));
130            self.mapper.lemma_mapper_wf_in_out(inner_v);
131            self.mapper.lemma_lossless_mapper(inner_v);
132            assert(self.consistent(self.mapper.spec_map(inner_v)));
133        }
134    }
135}
136
137impl<Inner, M> Consistency for super::Mapped<Inner, M> where
138    Inner: Consistency,
139    M: SpecMapper<In = Inner::Val>,
140 {
141    type Val = M::Out;
142
143    open spec fn consistent(&self, v: Self::Val) -> bool {
144        &&& self.mapper.wf_out(v)
145        &&& self.inner.consistent(self.mapper.spec_map_rev(v))
146    }
147}
148
149impl<Inner, M> SpecSerializerDps for super::Mapped<Inner, M> where
150    Inner: SpecSerializerDps,
151    M: SpecMapper<In = Inner::SValue>,
152 {
153    type SValue = M::Out;
154
155    open spec fn spec_serialize_dps(&self, v: M::Out, obuf: Seq<u8>) -> Seq<u8> {
156        self.inner.spec_serialize_dps(self.mapper.spec_map_rev(v), obuf)
157    }
158}
159
160impl<Inner, M> NonTailFmt for super::Mapped<Inner, M> where
161    Inner: NonTailFmt,
162    M: SpecMapper<In = Inner::SValue>,
163 {
164    open spec fn serialize_dps_inv(&self) -> bool {
165        self.inner.serialize_dps_inv()
166    }
167
168    proof fn lemma_serialize_dps_prepend(&self, v: M::Out, obuf: Seq<u8>) {
169        assert(self.serialize_dps_inv());
170        self.inner.lemma_serialize_dps_prepend(self.mapper.spec_map_rev(v), obuf);
171    }
172
173    proof fn lemma_serialize_dps_len(&self, v: M::Out, obuf: Seq<u8>) {
174        assert(self.serialize_dps_inv());
175        self.inner.lemma_serialize_dps_len(self.mapper.spec_map_rev(v), obuf);
176    }
177}
178
179impl<Inner, M> GoodSerializer for super::Mapped<Inner, M> where
180    Inner: GoodSerializer,
181    M: SpecMapper<In = Inner::SVal>,
182 {
183    open spec fn serialize_inv(&self) -> bool {
184        self.inner.serialize_inv()
185    }
186
187    proof fn lemma_serialize_len(&self, v: M::Out) {
188        assert(self.serialize_inv());
189        self.inner.lemma_serialize_len(self.mapper.spec_map_rev(v));
190    }
191}
192
193impl<Inner, M> SpecByteLen for super::Mapped<Inner, M> where
194    Inner: SpecByteLen,
195    M: SpecMapper<In = Inner::T>,
196 {
197    type T = M::Out;
198
199    open spec fn byte_len(&self, v: Self::T) -> nat {
200        self.inner.byte_len(self.mapper.spec_map_rev(v))
201    }
202}
203
204impl<Inner, M> MinMaxByteLen for super::Mapped<Inner, M> where
205    Inner: MinMaxByteLen,
206    M: SpecMapper<In = Inner::T>,
207 {
208    open spec fn min(&self) -> nat {
209        self.inner.min()
210    }
211
212    open spec fn max(&self) -> nat {
213        self.inner.max()
214    }
215
216    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
217        self.inner.lemma_min_max_byte_len(self.mapper.spec_map_rev(v));
218    }
219}
220
221impl<Inner, M> StaticByteLen for super::Mapped<Inner, M> where
222    Inner: StaticByteLen,
223    M: SpecMapper<In = Inner::T>,
224 {
225    open spec fn static_byte_len() -> nat {
226        Inner::static_byte_len()
227    }
228
229    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
230        self.inner.lemma_static_len_matches_byte_len(self.mapper.spec_map_rev(v));
231    }
232}
233
234impl<Inner, M> SpecSerializer for super::Mapped<Inner, M> where
235    Inner: SpecSerializer,
236    M: SpecMapper<In = Inner::SVal>,
237 {
238    type SVal = M::Out;
239
240    open spec fn spec_serialize(&self, v: M::Out) -> Seq<u8> {
241        self.inner.spec_serialize(self.mapper.spec_map_rev(v))
242    }
243}
244
245/*
246 * Support for plain spec closures as mappers
247 */
248
249pub type FnSpecMapper<In, Out> = (spec_fn(In) -> Out, spec_fn(Out) -> In);
250
251impl<In, Out> SpecMapper for FnSpecMapper<In, Out> {
252    type In = In;
253
254    type Out = Out;
255
256    open spec fn spec_map(&self, i: Self::In) -> Self::Out {
257        (self.0)(i)
258    }
259
260    open spec fn spec_map_rev(&self, o: Self::Out) -> Self::In {
261        (self.1)(o)
262    }
263}
264
265impl<Inner: SpecParser, Out> SpecParser for super::Mapped<Inner, spec_fn(Inner::PVal) -> Out> {
266    type PVal = Out;
267
268    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Out)> {
269        match self.inner.spec_parse(ibuf) {
270            Some((n, v)) => Some((n, (self.mapper)(v))),
271            None => None,
272        }
273    }
274}
275
276impl<Inner: SafeParser, Out> SafeParser for super::Mapped<Inner, spec_fn(Inner::PVal) -> Out> {
277    open spec fn safe_inv(&self) -> bool {
278        self.inner.safe_inv()
279    }
280
281    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
282        self.inner.lemma_parse_safe(ibuf);
283    }
284}
285
286impl<Inner: Productive, Out> Productive for super::Mapped<Inner, spec_fn(Inner::PVal) -> Out> {
287    open spec fn productive_inv(&self) -> bool {
288        self.inner.productive_inv()
289    }
290
291    proof fn lemma_productive(&self, s: Seq<u8>) {
292        self.inner.lemma_productive(s);
293    }
294}
295
296impl<Inner: SoundParser, Out> SoundParser for super::Mapped<Inner, FnSpecMapper<Inner::PVal, Out>> {
297    open spec fn sound_inv(&self) -> bool {
298        &&& self.inner.sound_inv()
299        &&& forall|v: Inner::T| #[trigger]
300            self.inner.consistent(v) ==> (self.mapper.1)((self.mapper.0)(v)) == v
301    }
302
303    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
304        self.inner.lemma_parse_sound_consumption(ibuf);
305        self.inner.lemma_parse_sound_value(ibuf);
306    }
307
308    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
309        self.inner.lemma_parse_sound_value(ibuf);
310    }
311}
312
313impl<Inner: SpecSerializerDps, Out> SpecSerializerDps for super::Mapped<
314    Inner,
315    spec_fn(Out) -> Inner::SValue,
316> {
317    type SValue = Out;
318
319    open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
320        self.inner.spec_serialize_dps((self.mapper)(v), obuf)
321    }
322}
323
324impl<Inner: SpecSerializer, Out> SpecSerializer for super::Mapped<
325    Inner,
326    spec_fn(Out) -> Inner::SVal,
327> {
328    type SVal = Out;
329
330    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
331        self.inner.spec_serialize((self.mapper)(v))
332    }
333}
334
335/*
336 * Support for [`BiMap`] that can be used for both spec mappers and exec mappers.
337 */
338
339pub trait SpecMap {
340    type Input;
341
342    type Output;
343
344    spec fn spec_map(&self, i: Self::Input) -> Self::Output;
345}
346
347impl<I, O> SpecMap for spec_fn(I) -> O {
348    type Input = I;
349
350    type Output = O;
351
352    open spec fn spec_map(&self, i: Self::Input) -> Self::Output {
353        (self)(i)
354    }
355}
356
357#[derive(Copy)]
358pub struct BiMap<M, MRev>(pub M, pub MRev);
359
360impl<M: Clone, MRev: Clone> Clone for BiMap<M, MRev> {
361    fn clone(&self) -> (cloned: Self)
362        ensures
363            call_ensures(M::clone, (&self.0,), cloned.0),
364            call_ensures(MRev::clone, (&self.1,), cloned.1),
365    {
366        BiMap(self.0.clone(), self.1.clone())
367    }
368}
369
370pub type BiMapper<In, Out> = BiMap<spec_fn(In) -> Out, spec_fn(Out) -> In>;
371
372impl<M, MRev> BiMap<M, MRev> where M: SpecMap, MRev: SpecMap<Input = M::Output, Output = M::Input> {
373    pub open spec fn sound(&self, o: M::Output) -> bool {
374        let BiMap(m, mrev) = *self;
375        m.spec_map(mrev.spec_map(o)) == o
376    }
377
378    pub open spec fn lossless(&self, i: M::Input) -> bool {
379        let BiMap(m, mrev) = *self;
380        mrev.spec_map(m.spec_map(i)) == i
381    }
382}
383
384impl<Inner, M, MRev> SpecParser for super::Mapped<Inner, BiMap<M, MRev>> where
385    Inner: SpecParser,
386    M: SpecMap<Input = Inner::PVal>,
387    MRev: SpecMap<Input = M::Output, Output = M::Input>,
388 {
389    type PVal = M::Output;
390
391    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, M::Output)> {
392        match self.inner.spec_parse(ibuf) {
393            Some((n, v)) => Some((n, self.mapper.0.spec_map(v))),
394            None => None,
395        }
396    }
397}
398
399impl<Inner, M, MRev> SpecSerializerDps for super::Mapped<Inner, BiMap<M, MRev>> where
400    Inner: SpecSerializerDps,
401    M: SpecMap<Input = Inner::SValue>,
402    MRev: SpecMap<Input = M::Output, Output = M::Input>,
403 {
404    type SValue = M::Output;
405
406    open spec fn spec_serialize_dps(&self, v: M::Output, obuf: Seq<u8>) -> Seq<u8> {
407        self.inner.spec_serialize_dps(self.mapper.1.spec_map(v), obuf)
408    }
409}
410
411impl<Inner, M, MRev> SpecSerializer for super::Mapped<Inner, BiMap<M, MRev>> where
412    Inner: SpecSerializer,
413    M: SpecMap<Input = Inner::SVal>,
414    MRev: SpecMap<Input = M::Output, Output = M::Input>,
415 {
416    type SVal = M::Output;
417
418    open spec fn spec_serialize(&self, v: M::Output) -> Seq<u8> {
419        self.inner.spec_serialize(self.mapper.1.spec_map(v))
420    }
421}
422
423impl<Inner, M, MRev> Consistency for super::Mapped<Inner, BiMap<M, MRev>> where
424    Inner: Consistency,
425    M: SpecMap<Input = Inner::Val>,
426    MRev: SpecMap<Input = M::Output, Output = M::Input>,
427 {
428    type Val = M::Output;
429
430    open spec fn consistent(&self, v: Self::Val) -> bool {
431        self.inner.consistent(self.mapper.1.spec_map(v))
432    }
433}
434
435impl<Inner, M, MRev> SpecByteLen for super::Mapped<Inner, BiMap<M, MRev>> where
436    Inner: SpecByteLen,
437    M: SpecMap<Input = Inner::T>,
438    MRev: SpecMap<Input = M::Output, Output = M::Input>,
439 {
440    type T = M::Output;
441
442    open spec fn byte_len(&self, v: Self::T) -> nat {
443        self.inner.byte_len(self.mapper.1.spec_map(v))
444    }
445}
446
447impl<Inner, M, MRev> SafeParser for super::Mapped<Inner, BiMap<M, MRev>> where
448    Inner: SafeParser,
449    M: SpecMap<Input = Inner::PVal>,
450    MRev: SpecMap<Input = M::Output, Output = M::Input>,
451 {
452    open spec fn safe_inv(&self) -> bool {
453        self.inner.safe_inv()
454    }
455
456    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
457        self.inner.lemma_parse_safe(ibuf);
458    }
459}
460
461impl<Inner, M, MRev> SoundParser for super::Mapped<Inner, BiMap<M, MRev>> where
462    Inner: SoundParser,
463    M: SpecMap<Input = Inner::PVal>,
464    MRev: SpecMap<Input = M::Output, Output = M::Input>,
465 {
466    #[verifier::inline]
467    open spec fn sound_inv(&self) -> bool {
468        &&& self.inner.sound_inv()
469        &&& forall|i: Inner::T| #[trigger] self.inner.consistent(i) ==> self.mapper.lossless(i)
470    }
471
472    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
473        self.inner.lemma_parse_sound_consumption(ibuf);
474        self.inner.lemma_parse_sound_value(ibuf);
475    }
476
477    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
478        self.inner.lemma_parse_sound_value(ibuf);
479    }
480}
481
482impl<Inner, M, MRev> NonTailFmt for super::Mapped<Inner, BiMap<M, MRev>> where
483    Inner: NonTailFmt,
484    M: SpecMap<Input = Inner::SValue>,
485    MRev: SpecMap<Input = M::Output, Output = M::Input>,
486 {
487    open spec fn serialize_dps_inv(&self) -> bool {
488        self.inner.serialize_dps_inv()
489    }
490
491    proof fn lemma_serialize_dps_prepend(&self, v: M::Output, obuf: Seq<u8>) {
492        self.inner.lemma_serialize_dps_prepend(self.mapper.1.spec_map(v), obuf);
493    }
494
495    proof fn lemma_serialize_dps_len(&self, v: M::Output, obuf: Seq<u8>) {
496        self.inner.lemma_serialize_dps_len(self.mapper.1.spec_map(v), obuf);
497    }
498}
499
500impl<Inner, M, MRev> GoodSerializer for super::Mapped<Inner, BiMap<M, MRev>> where
501    Inner: GoodSerializer,
502    M: SpecMap<Input = Inner::SVal>,
503    MRev: SpecMap<Input = M::Output, Output = M::Input>,
504 {
505    open spec fn serialize_inv(&self) -> bool {
506        self.inner.serialize_inv()
507    }
508
509    proof fn lemma_serialize_len(&self, v: M::Output) {
510        self.inner.lemma_serialize_len(self.mapper.1.spec_map(v));
511    }
512}
513
514impl<Inner, M, MRev> MinMaxByteLen for super::Mapped<Inner, BiMap<M, MRev>> where
515    Inner: MinMaxByteLen,
516    M: SpecMap<Input = Inner::T>,
517    MRev: SpecMap<Input = M::Output, Output = M::Input>,
518 {
519    open spec fn min(&self) -> nat {
520        self.inner.min()
521    }
522
523    open spec fn max(&self) -> nat {
524        self.inner.max()
525    }
526
527    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
528        self.inner.lemma_min_max_byte_len(self.mapper.1.spec_map(v));
529    }
530}
531
532impl<Inner, M, MRev> StaticByteLen for super::Mapped<Inner, BiMap<M, MRev>> where
533    Inner: StaticByteLen,
534    M: SpecMap<Input = Inner::T>,
535    MRev: SpecMap<Input = M::Output, Output = M::Input>,
536 {
537    open spec fn static_byte_len() -> nat {
538        Inner::static_byte_len()
539    }
540
541    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
542        self.inner.lemma_static_len_matches_byte_len(self.mapper.1.spec_map(v));
543    }
544}
545
546pub type TryMapPred<In> = PredFnSpec<In>;
547
548pub type TryMapInner<Inner, M> = super::Mapped<
549    Refined<Inner, TryMapPred<<M as SpecMapper>::In>>,
550    M,
551>;
552
553impl<Inner, M: SpecMapper> super::TryMap<Inner, M> {
554    pub open spec fn inner(&self) -> TryMapInner<Inner, M> {
555        super::Mapped {
556            inner: Refined(self.inner, |v: M::In| self.mapper.wf_in(v)),
557            mapper: self.mapper,
558        }
559    }
560}
561
562impl<Inner, M> SpecParser for super::TryMap<Inner, M> where
563    Inner: SpecParser,
564    M: SpecMapper<In = Inner::PVal>,
565 {
566    type PVal = M::Out;
567
568    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, M::Out)> {
569        self.inner().spec_parse(ibuf)
570    }
571}
572
573impl<Inner, M> SafeParser for super::TryMap<Inner, M> where
574    Inner: SafeParser,
575    M: SpecMapper<In = Inner::PVal>,
576 {
577    open spec fn safe_inv(&self) -> bool {
578        self.inner().safe_inv()
579    }
580
581    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
582        self.inner().lemma_parse_safe(ibuf);
583    }
584}
585
586impl<Inner, M> SoundParser for super::TryMap<Inner, M> where
587    Inner: SoundParser,
588    M: LosslessMapper<In = Inner::PVal>,
589 {
590    open spec fn sound_inv(&self) -> bool {
591        self.inner().sound_inv()
592    }
593
594    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
595        self.inner().lemma_parse_sound_consumption(ibuf);
596    }
597
598    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
599        self.inner().lemma_parse_sound_value(ibuf);
600    }
601}
602
603impl<Inner, M> Consistency for super::TryMap<Inner, M> where
604    Inner: Consistency,
605    M: SpecMapper<In = Inner::Val>,
606 {
607    type Val = M::Out;
608
609    open spec fn consistent(&self, v: Self::Val) -> bool {
610        self.inner().consistent(v)
611    }
612}
613
614impl<Inner, M> SpecSerializerDps for super::TryMap<Inner, M> where
615    Inner: SpecSerializerDps,
616    M: SpecMapper<In = Inner::SValue>,
617 {
618    type SValue = M::Out;
619
620    open spec fn spec_serialize_dps(&self, v: M::Out, obuf: Seq<u8>) -> Seq<u8> {
621        self.inner().spec_serialize_dps(v, obuf)
622    }
623}
624
625impl<Inner, M> NonTailFmt for super::TryMap<Inner, M> where
626    Inner: NonTailFmt,
627    M: SpecMapper<In = Inner::SValue>,
628 {
629    open spec fn serialize_dps_inv(&self) -> bool {
630        self.inner().serialize_dps_inv()
631    }
632
633    proof fn lemma_serialize_dps_prepend(&self, v: M::Out, obuf: Seq<u8>) {
634        self.inner().lemma_serialize_dps_prepend(v, obuf);
635    }
636
637    proof fn lemma_serialize_dps_len(&self, v: M::Out, obuf: Seq<u8>) {
638        self.inner().lemma_serialize_dps_len(v, obuf);
639    }
640}
641
642impl<Inner, M> GoodSerializer for super::TryMap<Inner, M> where
643    Inner: GoodSerializer,
644    M: SpecMapper<In = Inner::SVal>,
645 {
646    open spec fn serialize_inv(&self) -> bool {
647        self.inner().serialize_inv()
648    }
649
650    proof fn lemma_serialize_len(&self, v: M::Out) {
651        self.inner().lemma_serialize_len(v);
652    }
653}
654
655impl<Inner, M> SpecByteLen for super::TryMap<Inner, M> where
656    Inner: SpecByteLen,
657    M: SpecMapper<In = Inner::T>,
658 {
659    type T = M::Out;
660
661    open spec fn byte_len(&self, v: Self::T) -> nat {
662        self.inner().byte_len(v)
663    }
664}
665
666impl<Inner, M> MinMaxByteLen for super::TryMap<Inner, M> where
667    Inner: MinMaxByteLen,
668    M: SpecMapper<In = Inner::T>,
669 {
670    open spec fn min(&self) -> nat {
671        self.inner().min()
672    }
673
674    open spec fn max(&self) -> nat {
675        self.inner().max()
676    }
677
678    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
679        self.inner().lemma_min_max_byte_len(v);
680    }
681}
682
683impl<Inner, M> StaticByteLen for super::TryMap<Inner, M> where
684    Inner: StaticByteLen,
685    M: SpecMapper<In = Inner::T>,
686 {
687    open spec fn static_byte_len() -> nat {
688        TryMapInner::<Inner, M>::static_byte_len()
689    }
690
691    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
692        self.inner().lemma_static_len_matches_byte_len(v);
693    }
694}
695
696impl<Inner, M> SpecSerializer for super::TryMap<Inner, M> where
697    Inner: SpecSerializer,
698    M: SpecMapper<In = Inner::SVal>,
699 {
700    type SVal = M::Out;
701
702    open spec fn spec_serialize(&self, v: M::Out) -> Seq<u8> {
703        self.inner().spec_serialize(v)
704    }
705}
706
707} // verus!
vest_lib/combinators/mapped/spec.rs

vest_lib/combinators/mapped/
spec.rs
