vest/regular/
map.rs

1#![allow(rustdoc::broken_intra_doc_links)]
2use crate::properties::*;
3use vstd::prelude::*;
4
5verus! {
6
7/// Spec version of [`Iso`].
8/// It mandates that the isomorphism is bijective.
9pub trait SpecIso {
10    /// The source type of the isomorphism.
11    type Src: SpecFrom<Self::Dst>;
12
13    /// The destination type of the isomorphism.
14    type Dst: SpecFrom<Self::Src>;
15
16    /// One direction of the isomorphism.
17    proof fn spec_iso(s: Self::Src)
18        ensures
19        Self::Src::spec_from(Self::Dst::spec_from(s)) == s,
20    ;
21
22    /// The other direction of the isomorphism.
23    proof fn spec_iso_rev(s: Self::Dst)
24        ensures
25            Self::Dst::spec_from(Self::Src::spec_from(s)) == s,
26    ;
27}
28
29/// Similar fix to <https://github.com/secure-foundations/vest/issues/16>
30pub trait SpecIsoFn: SpecIso {
31    /// Applies the isomorphism to the source type.
32    spec fn spec_apply(s: Self::Src) -> Self::Dst;
33
34    /// Applies the reverse isomorphism to the destination type.
35    spec fn spec_rev_apply(s: Self::Dst) -> Self::Src;
36}
37
38impl<T: SpecIso> SpecIsoFn for T {
39    /// Applies the isomorphism to the source type.
40    open spec fn spec_apply(s: Self::Src) -> Self::Dst {
41        Self::Dst::spec_from(s)
42    }
43
44    /// Applies the reverse isomorphism to the destination type.
45    open spec fn spec_rev_apply(s: Self::Dst) -> Self::Src {
46        Self::Src::spec_from(s)
47    }
48}
49
50/// All isomorphisms to be used in [`Mapped`] combinator must implement this trait.
51/// [`Self::apply`] and [`Self::rev_apply`] must be inverses of each other.
52/// See [`SpecIso::spec_iso`] and [`SpecIso::spec_iso_rev`] for more details.
53pub trait Iso: View where
54    Self::V: SpecIso<Src = <Self::SrcOwned as View>::V, Dst = <Self::DstOwned as View>::V>,
55    <Self::SrcOwned as View>::V: SpecFrom<<Self::DstOwned as View>::V>,
56    <Self::DstOwned as View>::V: SpecFrom<<Self::SrcOwned as View>::V>,
57 {
58    /// The source type of the isomorphism.
59    type Src<'a>: View<V = <Self::SrcOwned as View>::V> + From<Self::Dst<'a>>;
60
61    /// The destination type of the isomorphism.
62    type Dst<'a>: View<V = <Self::DstOwned as View>::V> + From<Self::Src<'a>>;
63
64    /// The owned version of the source type.
65    type SrcOwned: View + From<Self::DstOwned>;
66
67    /// The owned version of the destination type.
68    type DstOwned: View + From<Self::SrcOwned>;
69
70    /// Applies the isomorphism to the source type.
71    fn apply(s: Self::Src<'_>) -> (res: Self::Dst<'_>)
72        ensures
73            res@ == Self::V::spec_apply(s@),
74    {
75        Self::Dst::ex_from(s)
76    }
77
78    /// Applies the reverse isomorphism to the destination type.
79    fn rev_apply(s: Self::Dst<'_>) -> (res: Self::Src<'_>)
80        ensures
81            res@ == Self::V::spec_rev_apply(s@),
82    {
83        Self::Src::ex_from(s)
84    }
85}
86
87/// Combinator that maps the result of an `inner` combinator with an isomorphism that implements
88/// [`Iso`].
89pub struct Mapped<Inner, M> {
90    /// The inner combinator.
91    pub inner: Inner,
92    /// The isomorphism.
93    pub mapper: M,
94}
95
96impl<Inner: View, M: View> View for Mapped<Inner, M> {
97    type V = Mapped<Inner::V, M::V>;
98
99    open spec fn view(&self) -> Self::V {
100        Mapped { inner: self.inner@, mapper: self.mapper@ }
101    }
102}
103
104impl<Inner, M> SpecCombinator for Mapped<Inner, M> where
105    Inner: SpecCombinator,
106    M: SpecIso<Src = Inner::SpecResult>,
107    Inner::SpecResult: SpecFrom<M::Dst>,
108    M::Dst: SpecFrom<Inner::SpecResult>,
109 {
110    type SpecResult = M::Dst;
111
112    open spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()> {
113        match self.inner.spec_parse(s) {
114            Err(e) => Err(e),
115            Ok((n, v)) => Ok((n, M::spec_apply(v))),
116        }
117    }
118
119    proof fn spec_parse_wf(&self, s: Seq<u8>) {
120        self.inner.spec_parse_wf(s);
121        if let Ok((n, v)) = self.inner.spec_parse(s) {
122            M::spec_iso(v);
123        }
124    }
125
126    open spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()> {
127        self.inner.spec_serialize(M::spec_rev_apply(v))
128    }
129}
130
131impl<Inner, M> SecureSpecCombinator for Mapped<Inner, M> where
132    Inner: SecureSpecCombinator,
133    M: SpecIso<Src = Inner::SpecResult>,
134    Inner::SpecResult: SpecFrom<M::Dst>,
135    M::Dst: SpecFrom<Inner::SpecResult>,
136 {
137    open spec fn is_prefix_secure() -> bool {
138        Inner::is_prefix_secure()
139    }
140
141    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult) {
142        if let Ok(buf) = self.inner.spec_serialize(M::spec_rev_apply(v)) {
143            M::spec_iso_rev(v);
144            self.inner.theorem_serialize_parse_roundtrip(M::spec_rev_apply(v))
145        }
146    }
147
148    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
149        self.inner.spec_parse_wf(buf);
150        self.inner.theorem_parse_serialize_roundtrip(buf);
151        if let Ok((n, v)) = self.inner.spec_parse(buf) {
152            M::spec_iso(v)
153        }
154    }
155
156    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
157        self.inner.lemma_prefix_secure(s1, s2);
158        if let Ok((n, v)) = self.inner.spec_parse(s1) {
159            self.inner.spec_parse_wf(s1);
160            M::spec_iso(v)
161        }
162    }
163}
164
165impl<Inner, M> Combinator for Mapped<
166    Inner,
167    M,
168> where
169    Inner: Combinator,
170    Inner::V: SecureSpecCombinator<SpecResult = <Inner::Owned as View>::V>,
171    for <'a> M: Iso<Src<'a> = Inner::Result<'a>, SrcOwned = Inner::Owned>,
172    for <'a>Inner::Result<'a>: From<M::Dst<'a>> + View,
173    for <'a>M::Dst<'a>: From<Inner::Result<'a>> + View,
174    M::V: SpecIso<Src = <Inner::Owned as View>::V, Dst = <M::DstOwned as View>::V>,
175    <Inner::Owned as View>::V: SpecFrom<<M::DstOwned as View>::V>,
176    <M::DstOwned as View>::V: SpecFrom<<Inner::Owned as View>::V>,
177 {
178    type Result<'a> = M::Dst<'a>;
179
180    type Owned = M::DstOwned;
181
182    open spec fn spec_length(&self) -> Option<usize> {
183        self.inner.spec_length()
184    }
185
186    fn length(&self) -> Option<usize> {
187        self.inner.length()
188    }
189
190    open spec fn parse_requires(&self) -> bool {
191        self.inner.parse_requires()
192    }
193
194    fn parse<'a>(&self, s: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) {
195        match self.inner.parse(s) {
196            Err(e) => Err(e),
197            Ok((n, v)) => {
198                proof {
199                    M::V::spec_iso(v@);
200                }
201                Ok((n, M::apply(v)))
202            },
203        }
204    }
205
206    open spec fn serialize_requires(&self) -> bool {
207        self.inner.serialize_requires()
208    }
209
210    fn serialize(&self, v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> (res: Result<
211        usize,
212        SerializeError,
213    >) {
214        self.inner.serialize(M::rev_apply(v), data, pos)
215    }
216}
217
218/// Spec version of [`TryFromInto`].
219pub trait SpecTryFromInto {
220    /// The source type
221    type Src: SpecTryFrom<Self::Dst>;
222
223    /// The destination type
224    type Dst: SpecTryFrom<Self::Src>;
225
226    /// One direction of the isomorphism when the conversion is successful.
227    proof fn spec_iso(s: Self::Src)
228        ensures
229            Self::Dst::spec_try_from(s) matches Ok(v) ==> {
230                &&& Self::Src::spec_try_from(v) is Ok
231                &&& Self::Src::spec_try_from(v) matches Ok(s_) && s == s_
232            },
233    ;
234
235    /// The other direction of the isomorphism when the conversion is successful.
236    proof fn spec_iso_rev(s: Self::Dst)
237        ensures
238            Self::Src::spec_try_from(s) matches Ok(v) ==> {
239                &&& Self::Dst::spec_try_from(v) is Ok
240                &&& Self::Dst::spec_try_from(v) matches Ok(s_) && s == s_
241            },
242    ;
243}
244
245/// Similar fix to <https://github.com/secure-foundations/vest/issues/16>
246pub trait SpecTryFromIntoFn: SpecTryFromInto {
247    /// Applies the faillible conversion to the source type.
248    spec fn spec_apply(s: Self::Src) -> Result<
249        Self::Dst,
250        <Self::Dst as SpecTryFrom<Self::Src>>::Error,
251    >;
252
253    /// Applies the reverse faillible conversion to the destination type.
254    spec fn spec_rev_apply(s: Self::Dst) -> Result<
255        Self::Src,
256        <Self::Src as SpecTryFrom<Self::Dst>>::Error,
257    >;
258}
259
260impl<T: SpecTryFromInto> SpecTryFromIntoFn for T {
261    /// Applies the faillible conversion to the source type.
262    open spec fn spec_apply(s: Self::Src) -> Result<
263        Self::Dst,
264        <Self::Dst as SpecTryFrom<Self::Src>>::Error,
265    > {
266        Self::Dst::spec_try_from(s)
267    }
268
269    /// Applies the reverse faillible conversion to the destination type.
270    open spec fn spec_rev_apply(s: Self::Dst) -> Result<
271        Self::Src,
272        <Self::Src as SpecTryFrom<Self::Dst>>::Error,
273    > {
274        Self::Src::spec_try_from(s)
275    }
276}
277
278/// Faillible version of [`Iso`].
279pub trait TryFromInto: View where
280    Self::V: SpecTryFromInto<Src = <Self::SrcOwned as View>::V, Dst = <Self::DstOwned as View>::V>,
281    <Self::SrcOwned as View>::V: SpecTryFrom<<Self::DstOwned as View>::V>,
282    <Self::DstOwned as View>::V: SpecTryFrom<<Self::SrcOwned as View>::V>,
283 {
284    /// The source type
285    type Src<'a>: View<V = <Self::SrcOwned as View>::V> + TryFrom<Self::Dst<'a>>;
286
287    /// The destination type
288    type Dst<'a>: View<V = <Self::DstOwned as View>::V> + TryFrom<Self::Src<'a>>;
289
290    /// The owned version of the source type.
291    type SrcOwned: View + TryFrom<Self::DstOwned>;
292
293    /// The owned version of the destination type.
294    type DstOwned: View + TryFrom<Self::SrcOwned>;
295
296    /// Applies the faillible conversion to the source type.
297    fn apply(s: Self::Src<'_>) -> (res: Result<
298        Self::Dst<'_>,
299        <Self::Dst<'_> as TryFrom<Self::Src<'_>>>::Error,
300    >)
301        ensures
302            res matches Ok(v) ==> {
303                &&& Self::V::spec_apply(s@) is Ok
304                &&& Self::V::spec_apply(s@) matches Ok(v_) && v@ == v_
305            },
306            res matches Err(e) ==> Self::V::spec_apply(s@) is Err,
307    {
308        Self::Dst::ex_try_from(s)
309    }
310
311    /// Applies the reverse faillible conversion to the destination type.
312    fn rev_apply(s: Self::Dst<'_>) -> (res: Result<
313        Self::Src<'_>,
314        <Self::Src<'_> as TryFrom<Self::Dst<'_>>>::Error,
315    >)
316        ensures
317            res matches Ok(v) ==> {
318                &&& Self::V::spec_rev_apply(s@) is Ok
319                &&& Self::V::spec_rev_apply(s@) matches Ok(v_) && v@ == v_
320            },
321            res matches Err(e) ==> Self::V::spec_rev_apply(s@) is Err,
322    {
323        Self::Src::ex_try_from(s)
324    }
325}
326
327/// Combinator that maps the result of an `inner` combinator with a faillible conversion
328/// that implements [`TryFromInto`].
329pub struct TryMap<Inner, M> {
330    /// The inner combinator.
331    pub inner: Inner,
332    /// The faillible conversion.
333    pub mapper: M,
334}
335
336impl<Inner: View, M: View> View for TryMap<Inner, M> {
337    type V = TryMap<Inner::V, M::V>;
338
339    open spec fn view(&self) -> Self::V {
340        TryMap { inner: self.inner@, mapper: self.mapper@ }
341    }
342}
343
344impl<Inner, M> SpecCombinator for TryMap<Inner, M> where
345    Inner: SpecCombinator,
346    M: SpecTryFromInto<Src = Inner::SpecResult>,
347    Inner::SpecResult: SpecTryFrom<M::Dst>,
348    M::Dst: SpecTryFrom<Inner::SpecResult>,
349 {
350    type SpecResult = M::Dst;
351
352    open spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()> {
353        match self.inner.spec_parse(s) {
354            Err(e) => Err(e),
355            Ok((n, v)) => match M::spec_apply(v) {
356                Ok(v) => Ok((n, v)),
357                Err(_) => Err(()),
358            },
359        }
360    }
361
362    proof fn spec_parse_wf(&self, s: Seq<u8>) {
363        self.inner.spec_parse_wf(s);
364        if let Ok((n, v)) = self.inner.spec_parse(s) {
365            M::spec_iso(v);
366        }
367    }
368
369    open spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()> {
370        match M::spec_rev_apply(v) {
371            Ok(v) => self.inner.spec_serialize(v),
372            Err(_) => Err(()),
373        }
374    }
375}
376
377impl<Inner, M> SecureSpecCombinator for TryMap<Inner, M> where
378    Inner: SecureSpecCombinator,
379    M: SpecTryFromInto<Src = Inner::SpecResult>,
380    Inner::SpecResult: SpecTryFrom<M::Dst>,
381    M::Dst: SpecTryFrom<Inner::SpecResult>,
382 {
383    open spec fn is_prefix_secure() -> bool {
384        Inner::is_prefix_secure()
385    }
386
387    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult) {
388        if let Ok(v_) = M::spec_rev_apply(v) {
389            M::spec_iso_rev(v);
390            self.inner.theorem_serialize_parse_roundtrip(v_);
391        }
392    }
393
394    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
395        self.inner.spec_parse_wf(buf);
396        self.inner.theorem_parse_serialize_roundtrip(buf);
397        if let Ok((n, v)) = self.inner.spec_parse(buf) {
398            M::spec_iso(v)
399        }
400    }
401
402    proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
403        self.inner.lemma_prefix_secure(s1, s2);
404        if let Ok((n, v)) = self.inner.spec_parse(s1) {
405            self.inner.spec_parse_wf(s1);
406            M::spec_iso(v)
407        }
408    }
409}
410
411impl<Inner, M> Combinator for TryMap<
412    Inner,
413    M,
414> where
415    Inner: Combinator,
416    Inner::V: SecureSpecCombinator<SpecResult = <Inner::Owned as View>::V>,
417    for <'a> M: TryFromInto<Src<'a> = Inner::Result<'a>, SrcOwned = Inner::Owned>,
418    for <'a>Inner::Result<'a>: TryFrom<M::Dst<'a>> + View,
419    for <'a>M::Dst<'a>: TryFrom<Inner::Result<'a>> + View,
420    M::V: SpecTryFromInto<Src = <Inner::Owned as View>::V, Dst = <M::DstOwned as View>::V>,
421    <Inner::Owned as View>::V: SpecTryFrom<<M::DstOwned as View>::V>,
422    <M::DstOwned as View>::V: SpecTryFrom<<Inner::Owned as View>::V>,
423 {
424    type Result<'a> = M::Dst<'a>;
425
426    type Owned = M::DstOwned;
427
428    open spec fn spec_length(&self) -> Option<usize> {
429        self.inner.spec_length()
430    }
431
432    fn length(&self) -> Option<usize> {
433        self.inner.length()
434    }
435
436    open spec fn parse_requires(&self) -> bool {
437        self.inner.parse_requires()
438    }
439
440    fn parse<'a>(&self, s: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) {
441        match self.inner.parse(s) {
442            Err(e) => Err(e),
443            Ok((n, v)) => match M::apply(v) {
444                Ok(v) => Ok((n, v)),
445                Err(_) => Err(ParseError::TryMapFailed),
446            },
447        }
448    }
449
450    open spec fn serialize_requires(&self) -> bool {
451        self.inner.serialize_requires()
452    }
453
454    fn serialize(&self, v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> (res: Result<
455        usize,
456        SerializeError,
457    >) {
458        match M::rev_apply(v) {
459            Ok(v) => self.inner.serialize(v, data, pos),
460            Err(_) => Err(SerializeError::TryMapFailed),
461        }
462    }
463}
464
465#[cfg(test)]
466#[allow(unused)]
467mod test {
468    use super::*;
469    use super::super::uints::*;
470
471    verus! {
472
473// exhaustive enum
474
475#[derive(Structural, Copy, Clone, PartialEq, Eq)]
476pub enum FieldLess {
477    A = 0,
478    B = 1,
479    C = 2,
480}
481
482pub type FieldLessInner = u8;
483
484impl View for FieldLess {
485    type V = Self;
486
487    open spec fn view(&self) -> Self::V {
488        *self
489    }
490}
491
492impl Compare<FieldLess> for FieldLess {
493    fn compare(&self, other: &FieldLess) -> bool {
494        *self == *other
495    }
496}
497impl SpecTryFrom<FieldLessInner> for FieldLess {
498    type Error = ();
499
500    open spec fn spec_try_from(v: FieldLessInner) -> Result<FieldLess, ()> {
501        match v {
502            0u8 => Ok(FieldLess::A),
503            1u8 => Ok(FieldLess::B),
504            2u8 => Ok(FieldLess::C),
505            _ => Err(()),
506        }
507    }
508}
509
510impl SpecTryFrom<FieldLess> for FieldLessInner {
511    type Error = ();
512
513    open spec fn spec_try_from(v: FieldLess) -> Result<FieldLessInner, ()> {
514        match v {
515            FieldLess::A => Ok(0u8),
516            FieldLess::B => Ok(1u8),
517            FieldLess::C => Ok(2u8),
518        }
519    }
520}
521
522impl TryFrom<FieldLessInner> for FieldLess {
523    type Error = ();
524
525    fn ex_try_from(v: FieldLessInner) -> Result<FieldLess, ()> {
526        match v {
527            0u8 => Ok(FieldLess::A),
528            1u8 => Ok(FieldLess::B),
529            2u8 => Ok(FieldLess::C),
530            _ => Err(()),
531        }
532    }
533}
534
535impl TryFrom<FieldLess> for FieldLessInner {
536    type Error = ();
537
538    fn ex_try_from(v: FieldLess) -> Result<FieldLessInner, ()> {
539        match v {
540            FieldLess::A => Ok(0u8),
541            FieldLess::B => Ok(1u8),
542            FieldLess::C => Ok(2u8),
543        }
544    }
545}
546
547struct FieldLessMapper;
548
549impl View for FieldLessMapper {
550    type V = Self;
551
552    open spec fn view(&self) -> Self::V {
553        *self
554    }
555}
556
557impl SpecTryFromInto for FieldLessMapper {
558    type Src = FieldLessInner;
559    type Dst = FieldLess;
560
561    proof fn spec_iso(s: Self::Src) {}
562
563    proof fn spec_iso_rev(s: Self::Dst) {}
564}
565
566impl TryFromInto for FieldLessMapper {
567    type Src<'a> = FieldLessInner;
568    type Dst<'a> = FieldLess;
569
570    type SrcOwned = FieldLessInner;
571    type DstOwned = FieldLess;
572}
573
574type FieldLessCombinator = TryMap<U8, FieldLessMapper>;
575
576spec fn spec_field_less() -> FieldLessCombinator {
577    TryMap { inner: U8, mapper: FieldLessMapper }
578}
579
580fn field_less() -> (o: FieldLessCombinator)
581    ensures o@ == spec_field_less(),
582{
583    TryMap { inner: U8, mapper: FieldLessMapper }
584}
585
586spec fn parse_spec_field_less(i: Seq<u8>) -> Result<(usize, FieldLess), ()> {
587    spec_field_less().spec_parse(i)
588}
589
590spec fn serialize_spec_field_less(msg: FieldLess) -> Result<Seq<u8>, ()> {
591    spec_field_less().spec_serialize(msg)
592}
593
594fn parse_field_less(i: &[u8]) -> (o: Result<(usize, FieldLess), ParseError>)
595    ensures
596        o matches Ok(r) ==> parse_spec_field_less(i@) matches Ok(r_) && r@ == r_,
597{
598    field_less().parse(i)
599}
600
601fn serialize_field_less(msg: FieldLess, data: &mut Vec<u8>, pos: usize) -> (o: Result<usize, SerializeError>)
602    ensures
603        o matches Ok(n) ==> {
604            &&& serialize_spec_field_less(msg@) matches Ok(buf)
605            &&& n == buf.len() && data@ == seq_splice(old(data)@, pos, buf)
606        },
607{
608    field_less().serialize(msg, data, pos)
609}
610
611// non-exhaustive enum
612// NOTE: It turns out that the following encoding creates an anbiguous format, e.g. both
613// `NonExhaustive::X` and `NonExhaustive::Unknown(0)` would be serialized to `0x00`, which could
614// lead to format confusion attacks (though it's not immediately clear how). Interestingly,
615// [rustls](https://github.com/rustls/rustls/blob/main/rustls/src/msgs/macros.rs#L68) uses a
616// similar encoding for all its enums.
617//
618// For security, we should just use primitive uint combinators for non-exhaustive enums.
619
620// #[non_exhaustive]
621// #[repr(u8)]
622// pub enum NonExhaustive {
623//     X = 0,
624//     Y = 1,
625//     Z = 2,
626//     Unknown(u8),
627// }
628//
629// pub type NonExhaustiveInner = u8;
630//
631// impl View for NonExhaustive {
632//     type V = Self;
633//
634//     open spec fn view(&self) -> Self::V {
635//         *self
636//     }
637// }
638//
639// impl SpecFrom<NonExhaustiveInner> for NonExhaustive {
640//     open spec fn spec_from(v: NonExhaustiveInner) -> NonExhaustive {
641//         match v {
642//             0u8 => NonExhaustive::X,
643//             1u8 => NonExhaustive::Y,
644//             2u8 => NonExhaustive::Z,
645//             _ => NonExhaustive::Unknown(v),
646//         }
647//     }
648// }
649//
650// impl SpecFrom<NonExhaustive> for NonExhaustiveInner {
651//     open spec fn spec_from(v: NonExhaustive) -> NonExhaustiveInner {
652//         match v {
653//             NonExhaustive::X => 0u8,
654//             NonExhaustive::Y => 1u8,
655//             NonExhaustive::Z => 2u8,
656//             NonExhaustive::Unknown(v) => v,
657//         }
658//     }
659// }
660//
661// impl From<NonExhaustiveInner> for NonExhaustive {
662//     fn ex_from(v: NonExhaustiveInner) -> NonExhaustive {
663//         match v {
664//             0u8 => NonExhaustive::X,
665//             1u8 => NonExhaustive::Y,
666//             2u8 => NonExhaustive::Z,
667//             _ => NonExhaustive::Unknown(v),
668//         }
669//     }
670// }
671//
672// impl From<NonExhaustive> for NonExhaustiveInner {
673//     fn ex_from(v: NonExhaustive) -> NonExhaustiveInner {
674//         match v {
675//             NonExhaustive::X => 0u8,
676//             NonExhaustive::Y => 1u8,
677//             NonExhaustive::Z => 2u8,
678//             NonExhaustive::Unknown(v) => v,
679//         }
680//     }
681// }
682//
683// struct NonExhaustiveMapper;
684//
685// impl View for NonExhaustiveMapper {
686//     type V = Self;
687//
688//     open spec fn view(&self) -> Self::V {
689//         *self
690//     }
691// }
692//
693// impl SpecIso for NonExhaustiveMapper {
694//     type Src = NonExhaustiveInner;
695//     type Dst = NonExhaustive;
696//
697//     proof fn spec_iso(s: Self::Src) {
698//     }
699//
700//     proof fn spec_iso_rev(s: Self::Dst) {
701//         // would fail because of the ambiguity in the encoding
702//     }
703// }
704//
705// impl Iso for NonExhaustiveMapper {
706//     type Src<'a> = NonExhaustiveInner;
707//     type Dst<'a> = NonExhaustive;
708//
709//     type SrcOwned = NonExhaustiveInner;
710//     type DstOwned = NonExhaustive;
711// }
712
713
714
715
716}
717
718}
719
720} // verus!
vest/regular/map.rs

vest/regular/
map.rs
