vest/regular/
depend.rs

1use crate::properties::*;
2use vstd::prelude::*;
3use vstd::slice::slice_subrange;
4
5verus! {
6
7/// Spec version of [`Depend`].
8pub struct SpecDepend<Fst, Snd> where Fst: SecureSpecCombinator, Snd: SpecCombinator {
9    /// combinators that contain dependencies
10    pub fst: Fst,
11    /// closure that captures dependencies and maps them to the dependent combinators
12    pub snd: spec_fn(Fst::SpecResult) -> Snd,
13}
14
15impl<Fst, Snd> SpecCombinator for SpecDepend<Fst, Snd> where
16    Fst: SecureSpecCombinator,
17    Snd: SpecCombinator,
18 {
19    type SpecResult = (Fst::SpecResult, Snd::SpecResult);
20
21    open spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()> {
22        if Fst::is_prefix_secure() {
23            if let Ok((n, v1)) = self.fst.spec_parse(s) {
24                let snd = (self.snd)(v1);
25                if let Ok((m, v2)) = snd.spec_parse(s.subrange(n as int, s.len() as int)) {
26                    if n <= usize::MAX - m {
27                        Ok(((n + m) as usize, (v1, v2)))
28                    } else {
29                        Err(())
30                    }
31                } else {
32                    Err(())
33                }
34            } else {
35                Err(())
36            }
37        } else {
38            Err(())
39        }
40    }
41
42    proof fn spec_parse_wf(&self, s: Seq<u8>) {
43        if let Ok((n, v1)) = self.fst.spec_parse(s) {
44            let snd = (self.snd)(v1);
45            if let Ok((m, v2)) = snd.spec_parse(s.subrange(n as int, s.len() as int)) {
46                self.fst.spec_parse_wf(s);
47                snd.spec_parse_wf(s.subrange(n as int, s.len() as int));
48            }
49        }
50    }
51
52    open spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()> {
53        if Fst::is_prefix_secure() {
54            if let Ok(buf1) = self.fst.spec_serialize(v.0) {
55                let snd = (self.snd)(v.0);
56                if let Ok(buf2) = snd.spec_serialize(v.1) {
57                    if buf1.len() + buf2.len() <= usize::MAX {
58                        Ok(buf1.add(buf2))
59                    } else {
60                        Err(())
61                    }
62                } else {
63                    Err(())
64                }
65            } else {
66                Err(())
67            }
68        } else {
69            Err(())
70        }
71    }
72}
73
74impl<Fst, Snd> SecureSpecCombinator for SpecDepend<Fst, Snd> where
75    Fst: SecureSpecCombinator,
76    Snd: SecureSpecCombinator,
77 {
78    proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult) {
79        if let Ok((buf)) = self.spec_serialize(v) {
80            let buf0 = self.fst.spec_serialize(v.0).unwrap();
81            let buf1 = (self.snd)(v.0).spec_serialize(v.1).unwrap();
82            self.fst.theorem_serialize_parse_roundtrip(v.0);
83            self.fst.lemma_prefix_secure(buf0, buf1);
84            (self.snd)(v.0).theorem_serialize_parse_roundtrip(v.1);
85            assert(buf0.add(buf1).subrange(buf0.len() as int, buf.len() as int) == buf1);
86        }
87    }
88
89    proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
90        if let Ok((nm, (v0, v1))) = self.spec_parse(buf) {
91            let (n, v0_) = self.fst.spec_parse(buf).unwrap();
92            self.fst.spec_parse_wf(buf);
93            let buf0 = buf.subrange(0, n as int);
94            let buf1 = buf.subrange(n as int, buf.len() as int);
95            assert(buf == buf0.add(buf1));
96            self.fst.theorem_parse_serialize_roundtrip(buf);
97            let (m, v1_) = (self.snd)(v0).spec_parse(buf1).unwrap();
98            (self.snd)(v0).theorem_parse_serialize_roundtrip(buf1);
99            (self.snd)(v0).spec_parse_wf(buf1);
100            let buf2 = self.spec_serialize((v0, v1)).unwrap();
101            assert(buf2 == buf.subrange(0, nm as int));
102        } else {
103        }
104    }
105
106    open spec fn is_prefix_secure() -> bool {
107        Fst::is_prefix_secure() && Snd::is_prefix_secure()
108    }
109
110    proof fn lemma_prefix_secure(&self, buf: Seq<u8>, s2: Seq<u8>) {
111        if Fst::is_prefix_secure() && Snd::is_prefix_secure() {
112            if let Ok((nm, (v0, v1))) = self.spec_parse(buf) {
113                let (n, _) = self.fst.spec_parse(buf).unwrap();
114                self.fst.spec_parse_wf(buf);
115                let buf0 = buf.subrange(0, n as int);
116                let buf1 = buf.subrange(n as int, buf.len() as int);
117                self.fst.lemma_prefix_secure(buf0, buf1);
118                self.fst.lemma_prefix_secure(buf0, buf1.add(s2));
119                self.fst.lemma_prefix_secure(buf, s2);
120                let snd = (self.snd)(v0);
121                let (m, v1_) = snd.spec_parse(buf1).unwrap();
122                assert(buf.add(s2).subrange(0, n as int) == buf0);
123                assert(buf.add(s2).subrange(n as int, buf.add(s2).len() as int) == buf1.add(s2));
124                snd.lemma_prefix_secure(buf1, s2);
125            } else {
126            }
127        } else {
128        }
129    }
130}
131
132/// Combinator that sequentially applies two combinators, where the second combinator depends on
133/// the result of the first one.
134pub struct Depend<Fst, Snd, F> where
135    Fst: Combinator,
136    Snd: Combinator,
137    Fst::V: SecureSpecCombinator<SpecResult = <Fst::Owned as View>::V>,
138    Snd::V: SecureSpecCombinator<SpecResult = <Snd::Owned as View>::V>,
139    F: for <'a>Fn(Fst::Result<'a>) -> Snd,
140 {
141    /// combinators that contain dependencies
142    pub fst: Fst,
143    /// closure that captures dependencies and maps them to the dependent combinators
144    pub snd: F,
145    /// spec closure for well-formedness
146    pub spec_snd: Ghost<spec_fn(<Fst::Owned as View>::V) -> Snd::V>,
147}
148
149impl<Fst, Snd, F> Depend<Fst, Snd, F> where
150    Fst: Combinator,
151    Snd: Combinator,
152    Fst::V: SecureSpecCombinator<SpecResult = <Fst::Owned as View>::V>,
153    Snd::V: SecureSpecCombinator<SpecResult = <Snd::Owned as View>::V>,
154    F: for <'a>Fn(Fst::Result<'a>) -> Snd,
155 {
156    /// well-formed [`DepPair`] should have its clousre [`snd`] well-formed w.r.t. [`spec_snd`]
157    pub open spec fn wf(&self) -> bool {
158        let Ghost(spec_snd_dep) = self.spec_snd;
159        &&& forall|i| #[trigger] (self.snd).requires((i,))
160        &&& forall|i, snd| (self.snd).ensures((i,), snd) ==> spec_snd_dep(i@) == snd@
161    }
162}
163
164impl<Fst, Snd, F> View for Depend<Fst, Snd, F> where
165    Fst: Combinator,
166    Snd: Combinator,
167    Fst::V: SecureSpecCombinator<SpecResult = <Fst::Owned as View>::V>,
168    Snd::V: SecureSpecCombinator<SpecResult = <Snd::Owned as View>::V>,
169    F: for <'a>Fn(Fst::Result<'a>) -> Snd,
170 {
171    type V = SpecDepend<Fst::V, Snd::V>;
172
173    open spec fn view(&self) -> Self::V {
174        let Ghost(spec_snd) = self.spec_snd;
175        SpecDepend { fst: self.fst@, snd: spec_snd }
176    }
177}
178
179impl<Fst, Snd, F> Combinator for Depend<Fst, Snd, F> where
180    Fst: Combinator,
181    Snd: Combinator,
182    Fst::V: SecureSpecCombinator<SpecResult = <Fst::Owned as View>::V>,
183    Snd::V: SecureSpecCombinator<SpecResult = <Snd::Owned as View>::V>,
184    F: for <'a>Fn(Fst::Result<'a>) -> Snd,
185    for <'a>Fst::Result<'a>: Copy,
186 {
187    type Result<'a> = (Fst::Result<'a>, Snd::Result<'a>);
188
189    type Owned = (Fst::Owned, Snd::Owned);
190
191    open spec fn spec_length(&self) -> Option<usize> {
192        None
193    }
194
195    fn length(&self) -> Option<usize> {
196        None
197    }
198
199    open spec fn parse_requires(&self) -> bool {
200        &&& self.wf()
201        &&& self.fst.parse_requires()
202        &&& Fst::V::is_prefix_secure()
203        &&& forall|i, snd| (self.snd).ensures((i,), snd) ==> snd.parse_requires()
204    }
205
206    fn parse<'a>(&self, s: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) {
207            let (n, v1) = self.fst.parse(s)?;
208            let s_ = slice_subrange(s, n, s.len());
209            let snd = (self.snd)(v1);
210            let (m, v2) = snd.parse(s_)?;
211            if n <= usize::MAX - m {
212                Ok(((n + m), (v1, v2)))
213            } else {
214                Err(ParseError::SizeOverflow)
215            }
216    }
217
218    open spec fn serialize_requires(&self) -> bool {
219        &&& self.wf()
220        &&& self.fst.serialize_requires()
221        &&& Fst::V::is_prefix_secure()
222        &&& forall|i, snd| (self.snd).ensures((i,), snd) ==> snd.serialize_requires()
223    }
224
225    fn serialize(&self, v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> (res: Result<
226        usize,
227        SerializeError,
228    >) {
229            let n = self.fst.serialize(v.0, data, pos)?;
230            if n <= usize::MAX - pos && n + pos <= data.len() {
231                let snd = (self.snd)(v.0);
232                let m = snd.serialize(v.1, data, pos + n)?;
233                if m <= usize::MAX - n {
234                    assert(data@.subrange(pos as int, pos + n + m as int) == self@.spec_serialize(
235                        v@,
236                    ).unwrap());
237                    assert(data@ == seq_splice(old(data)@, pos, self@.spec_serialize(v@).unwrap()));
238                    Ok(n + m)
239                } else {
240                    Err(SerializeError::SizeOverflow)
241                }
242            } else {
243                Err(SerializeError::InsufficientBuffer)
244            }
245    }
246}
247
248#[cfg(test)]
249#[allow(unused)]
250mod test {
251    use crate::properties::*;
252    use crate::regular::{
253        and_then::AndThen,
254        bytes::Bytes,
255        bytes_n::BytesN,
256        choice::*,
257        cond::Cond,
258        depend::{Depend, SpecDepend},
259        map::*,
260        tail::Tail,
261        uints::{U16, U32, U8},
262    };
263    use vstd::prelude::*;
264
265    /// somewhat more complex TLV example
266    /// should be generated from the following vest code:
267    /// ```vest
268    /// msg1 = {
269    ///   a: u8,
270    ///   b: u16,
271    ///   c: [u8; 3],
272    ///   data: Tail,
273    /// }
274    ///
275    /// msg2 = {
276    ///   a: u8,
277    ///   b: u16,
278    ///   c: u32,
279    /// }
280    ///
281    /// msg3 = {
282    ///   data: [u8; 6],
283    /// }
284    ///
285    /// msg_type = enum {
286    ///   Msg1 = 1,
287    ///   Msg2 = 2,
288    ///   Msg3 = 3,
289    /// }
290    ///
291    /// tlv = {
292    ///   @tag: msg_type,
293    ///   @len: u8,
294    ///   content: [u8; @len] >>= choose(@tag) {
295    ///     Msg1 => msg1,
296    ///     Msg2 => msg2,
297    ///     Msg3 => msg3,
298    ///   },
299    ///   rest: Tail,
300    /// }
301    /// ```
302    /// Message type 1
303    pub struct SpecMsg1 {
304        pub a: u8,
305        pub b: u16,
306        pub c: Seq<u8>,
307        pub d: Seq<u8>,
308    }
309
310    pub type SpecMsg1Inner = (((u8, u16), Seq<u8>), Seq<u8>);
311
312    pub struct Msg1<'a> {
313        pub a: u8,
314        pub b: u16,
315        pub c: &'a [u8],
316        pub d: &'a [u8],
317    }
318
319    pub struct Msg1Owned {
320        pub a: u8,
321        pub b: u16,
322        pub c: Vec<u8>,
323        pub d: Vec<u8>,
324    }
325
326    pub type Msg1Inner<'a> = (((u8, u16), &'a [u8]), &'a [u8]);
327
328    pub type Msg1InnerOwned = (((u8, u16), Vec<u8>), Vec<u8>);
329
330    impl View for Msg1<'_> {
331        type V = SpecMsg1;
332
333        open spec fn view(&self) -> Self::V {
334            SpecMsg1 { a: self.a, b: self.b, c: self.c@, d: self.d@ }
335        }
336    }
337
338    impl View for Msg1Owned {
339        type V = SpecMsg1;
340
341        open spec fn view(&self) -> Self::V {
342            SpecMsg1 { a: self.a, b: self.b, c: self.c@, d: self.d@ }
343        }
344    }
345
346    impl SpecFrom<SpecMsg1> for SpecMsg1Inner {
347        open spec fn spec_from(t: SpecMsg1) -> SpecMsg1Inner {
348            (((t.a, t.b), t.c), t.d)
349        }
350    }
351
352    impl SpecFrom<SpecMsg1Inner> for SpecMsg1 {
353        open spec fn spec_from(e: SpecMsg1Inner) -> SpecMsg1 {
354            let (((a, b), c), d) = e;
355            SpecMsg1 { a, b, c, d }
356        }
357    }
358
359    impl<'a> From<Msg1<'a>> for Msg1Inner<'a> {
360        fn ex_from(e: Msg1) -> (res: Msg1Inner) {
361            (((e.a, e.b), e.c), e.d)
362        }
363    }
364
365    impl<'a> From<Msg1Inner<'a>> for Msg1<'a> {
366        fn ex_from(e: Msg1Inner) -> (res: Msg1) {
367            let (((a, b), c), d) = e;
368            Msg1 { a, b, c, d }
369        }
370    }
371
372    impl From<Msg1Owned> for Msg1InnerOwned {
373        fn ex_from(e: Msg1Owned) -> (res: Msg1InnerOwned) {
374            (((e.a, e.b), e.c), e.d)
375        }
376    }
377
378    impl From<Msg1InnerOwned> for Msg1Owned {
379        fn ex_from(e: Msg1InnerOwned) -> (res: Msg1Owned) {
380            let (((a, b), c), d) = e;
381            Msg1Owned { a, b, c, d }
382        }
383    }
384
385    pub struct Msg1Mapper;
386
387    impl View for Msg1Mapper {
388        type V = Self;
389
390        open spec fn view(&self) -> Self::V {
391            *self
392        }
393    }
394
395    impl SpecIso for Msg1Mapper {
396        type Src = SpecMsg1Inner;
397
398        type Dst = SpecMsg1;
399
400        proof fn spec_iso(s: SpecMsg1Inner) {
401        }
402
403        proof fn spec_iso_rev(s: SpecMsg1) {
404        }
405    }
406
407    impl Iso for Msg1Mapper {
408        type Src<'a> = Msg1Inner<'a>;
409
410        type Dst<'a> = Msg1<'a>;
411
412        type SrcOwned = Msg1InnerOwned;
413
414        type DstOwned = Msg1Owned;
415    }
416
417    /// Message type 2
418    pub struct Msg2 {
419        pub a: u8,
420        pub b: u16,
421        pub c: u32,
422    }
423
424    pub type Msg2Inner = ((u8, u16), u32);
425
426    impl View for Msg2 {
427        type V = Msg2;
428
429        open spec fn view(&self) -> Self::V {
430            *self
431        }
432    }
433
434    impl SpecFrom<Msg2> for Msg2Inner {
435        open spec fn spec_from(t: Msg2) -> Msg2Inner {
436            ((t.a, t.b), t.c)
437        }
438    }
439
440    impl From<Msg2> for Msg2Inner {
441        fn ex_from(e: Msg2) -> (res: Msg2Inner) {
442            ((e.a, e.b), e.c)
443        }
444    }
445
446    impl SpecFrom<Msg2Inner> for Msg2 {
447        open spec fn spec_from(e: Msg2Inner) -> Msg2 {
448            let ((a, b), c) = e;
449            Msg2 { a, b, c }
450        }
451    }
452
453    impl From<Msg2Inner> for Msg2 {
454        fn ex_from(e: Msg2Inner) -> (res: Msg2) {
455            let ((a, b), c) = e;
456            Msg2 { a, b, c }
457        }
458    }
459
460    pub struct Msg2Mapper;
461
462    impl View for Msg2Mapper {
463        type V = Self;
464
465        open spec fn view(&self) -> Self::V {
466            *self
467        }
468    }
469
470    impl SpecIso for Msg2Mapper {
471        type Src = Msg2Inner;
472
473        type Dst = Msg2;
474
475        proof fn spec_iso(s: Msg2Inner) {
476        }
477
478        proof fn spec_iso_rev(s: Msg2) {
479        }
480    }
481
482    impl Iso for Msg2Mapper {
483        type Src<'a> = Msg2Inner;
484
485        type Dst<'a> = Msg2;
486
487        type SrcOwned = Msg2Inner;
488
489        type DstOwned = Msg2;
490    }
491
492    /// Message type 3
493    pub struct SpecMsg3 {
494        pub a: Seq<u8>,
495    }
496
497    pub type SpecMsg3Inner = Seq<u8>;
498
499    pub struct Msg3<'a> {
500        pub a: &'a [u8],
501    }
502
503    pub struct Msg3Owned {
504        pub a: Vec<u8>,
505    }
506
507    pub type Msg3Inner<'a> = &'a [u8];
508
509    pub type Msg3InnerOwned = Vec<u8>;
510
511    impl View for Msg3<'_> {
512        type V = SpecMsg3;
513
514        open spec fn view(&self) -> Self::V {
515            SpecMsg3 { a: self.a@ }
516        }
517    }
518
519    impl View for Msg3Owned {
520        type V = SpecMsg3;
521
522        open spec fn view(&self) -> Self::V {
523            SpecMsg3 { a: self.a@ }
524        }
525    }
526
527    impl SpecFrom<SpecMsg3> for SpecMsg3Inner {
528        open spec fn spec_from(e: SpecMsg3) -> SpecMsg3Inner {
529            e.a
530        }
531    }
532
533    impl SpecFrom<SpecMsg3Inner> for SpecMsg3 {
534        open spec fn spec_from(e: SpecMsg3Inner) -> SpecMsg3 {
535            SpecMsg3 { a: e }
536        }
537    }
538
539    impl<'a> From<Msg3<'a>> for Msg3Inner<'a> {
540        fn ex_from(e: Msg3) -> (res: Msg3Inner) {
541            e.a
542        }
543    }
544
545    impl<'a> From<Msg3Inner<'a>> for Msg3<'a> {
546        fn ex_from(e: Msg3Inner) -> (res: Msg3) {
547            Msg3 { a: e }
548        }
549    }
550
551    impl From<Msg3Owned> for Msg3InnerOwned {
552        fn ex_from(e: Msg3Owned) -> (res: Msg3InnerOwned) {
553            e.a
554        }
555    }
556
557    impl From<Msg3InnerOwned> for Msg3Owned {
558        fn ex_from(e: Msg3InnerOwned) -> (res: Msg3Owned) {
559            Msg3Owned { a: e }
560        }
561    }
562
563    pub struct Msg3Mapper;
564
565    impl View for Msg3Mapper {
566        type V = Self;
567
568        open spec fn view(&self) -> Self::V {
569            *self
570        }
571    }
572
573    impl SpecIso for Msg3Mapper {
574        type Src = SpecMsg3Inner;
575
576        type Dst = SpecMsg3;
577
578        proof fn spec_iso(s: SpecMsg3Inner) {
579        }
580
581        proof fn spec_iso_rev(s: SpecMsg3) {
582        }
583    }
584
585    impl Iso for Msg3Mapper {
586        type Src<'a> = Msg3Inner<'a>;
587
588        type Dst<'a> = Msg3<'a>;
589
590        type SrcOwned = Msg3InnerOwned;
591
592        type DstOwned = Msg3Owned;
593    }
594
595    /// Message type tlv content
596    pub enum SpecTlvContent {
597        M1(SpecMsg1),
598        M2(Msg2),
599        M3(SpecMsg3),
600    }
601
602    pub type SpecTlvContentInner = ord_choice_result!(SpecMsg1, Msg2, SpecMsg3);
603
604    pub enum TlvContent<'a> {
605        M1(Msg1<'a>),
606        M2(Msg2),
607        M3(Msg3<'a>),
608    }
609
610    pub enum TlvContentOwned {
611        M1(Msg1Owned),
612        M2(Msg2),
613        M3(Msg3Owned),
614    }
615
616    pub type TlvContentInner<'a> = ord_choice_result!(Msg1<'a>, Msg2, Msg3<'a>);
617    pub type TlvContentOwnedInner = ord_choice_result!(Msg1Owned, Msg2, Msg3Owned);
618
619    impl View for TlvContent<'_> {
620        type V = SpecTlvContent;
621
622        open spec fn view(&self) -> Self::V {
623            match self {
624                TlvContent::M1(m) => SpecTlvContent::M1(m@),
625                TlvContent::M2(m) => SpecTlvContent::M2(m@),
626                TlvContent::M3(m) => SpecTlvContent::M3(m@),
627            }
628        }
629    }
630
631    impl View for TlvContentOwned {
632        type V = SpecTlvContent;
633
634        open spec fn view(&self) -> Self::V {
635            match self {
636                TlvContentOwned::M1(m) => SpecTlvContent::M1(m@),
637                TlvContentOwned::M2(m) => SpecTlvContent::M2(m@),
638                TlvContentOwned::M3(m) => SpecTlvContent::M3(m@),
639            }
640        }
641    }
642
643    impl SpecFrom<SpecTlvContent> for SpecTlvContentInner {
644        open spec fn spec_from(e: SpecTlvContent) -> SpecTlvContentInner {
645            match e {
646                SpecTlvContent::M1(m) => inj_ord_choice_result!(m, *, *),
647                SpecTlvContent::M2(m) => inj_ord_choice_result!(*, m, *),
648                SpecTlvContent::M3(m) => inj_ord_choice_result!(*, *, m),
649            }
650        }
651    }
652
653    impl SpecFrom<SpecTlvContentInner> for SpecTlvContent {
654        open spec fn spec_from(e: SpecTlvContentInner) -> SpecTlvContent {
655            match e {
656                inj_ord_choice_pat!(m, *, *) => SpecTlvContent::M1(m),
657                inj_ord_choice_pat!(*, m, *) => SpecTlvContent::M2(m),
658                inj_ord_choice_pat!(*, *, m) => SpecTlvContent::M3(m),
659            }
660        }
661    }
662
663    impl<'a> From<TlvContent<'a>> for TlvContentInner<'a> {
664        fn ex_from(e: TlvContent) -> (res: TlvContentInner) {
665            match e {
666                TlvContent::M1(m) => inj_ord_choice_result!(m, *, *),
667                TlvContent::M2(m) => inj_ord_choice_result!(*, m, *),
668                TlvContent::M3(m) => inj_ord_choice_result!(*, *, m),
669            }
670        }
671    }
672
673    impl<'a> From<TlvContentInner<'a>> for TlvContent<'a> {
674        fn ex_from(e: TlvContentInner) -> (res: TlvContent) {
675            match e {
676                inj_ord_choice_pat!(m, *, *) => TlvContent::M1(m),
677                inj_ord_choice_pat!(*, m, *) => TlvContent::M2(m),
678                inj_ord_choice_pat!(*, *, m) => TlvContent::M3(m),
679            }
680        }
681    }
682
683    impl From<TlvContentOwned> for TlvContentOwnedInner {
684        fn ex_from(e: TlvContentOwned) -> (res: TlvContentOwnedInner) {
685            match e {
686                TlvContentOwned::M1(m) => inj_ord_choice_result!(m, *, *),
687                TlvContentOwned::M2(m) => inj_ord_choice_result!(*, m, *),
688                TlvContentOwned::M3(m) => inj_ord_choice_result!(*, *, m),
689            }
690        }
691    }
692
693    impl From<TlvContentOwnedInner> for TlvContentOwned {
694        fn ex_from(e: TlvContentOwnedInner) -> (res: TlvContentOwned) {
695            match e {
696                inj_ord_choice_pat!(m, *, *) => TlvContentOwned::M1(m),
697                inj_ord_choice_pat!(*, m, *) => TlvContentOwned::M2(m),
698                inj_ord_choice_pat!(*, *, m) => TlvContentOwned::M3(m),
699            }
700        }
701    }
702
703    pub struct TlvContentMapper;
704
705    impl View for TlvContentMapper {
706        type V = Self;
707
708        open spec fn view(&self) -> Self::V {
709            *self
710        }
711    }
712
713    impl SpecIso for TlvContentMapper {
714        type Src = SpecTlvContentInner;
715
716        type Dst = SpecTlvContent;
717
718        proof fn spec_iso(s: SpecTlvContentInner) {
719        }
720
721        proof fn spec_iso_rev(s: SpecTlvContent) {
722        }
723    }
724
725    impl Iso for TlvContentMapper {
726        type Src<'a> = TlvContentInner<'a>;
727
728        type Dst<'a> = TlvContent<'a>;
729
730        type SrcOwned = TlvContentOwnedInner;
731
732        type DstOwned = TlvContentOwned;
733    }
734
735    /// TLV
736    pub struct SpecTlv {
737        pub tag: u8,
738        pub len: u8,
739        pub content: SpecTlvContent,
740        pub rest: Seq<u8>,
741    }
742
743    pub type SpecTlvInner = ((u8, u8), (SpecTlvContent, Seq<u8>));
744
745    pub struct Tlv<'a> {
746        pub tag: u8,
747        pub len: u8,
748        pub content: TlvContent<'a>,
749        pub rest: &'a [u8],
750    }
751
752    pub type TlvInner<'a> = ((u8, u8), (TlvContent<'a>, &'a [u8]));
753
754    pub struct TlvOwned {
755        pub tag: u8,
756        pub len: u8,
757        pub content: TlvContentOwned,
758        pub rest: Vec<u8>,
759    }
760
761    pub type TlvInnerOwned = ((u8, u8), (TlvContentOwned, Vec<u8>));
762
763    impl View for Tlv<'_> {
764        type V = SpecTlv;
765
766        open spec fn view(&self) -> Self::V {
767            SpecTlv { tag: self.tag, len: self.len, content: self.content@, rest: self.rest@ }
768        }
769    }
770
771    impl View for TlvOwned {
772        type V = SpecTlv;
773
774        open spec fn view(&self) -> Self::V {
775            SpecTlv { tag: self.tag, len: self.len, content: self.content@, rest: self.rest@ }
776        }
777    }
778
779    impl SpecFrom<SpecTlv> for SpecTlvInner {
780        open spec fn spec_from(e: SpecTlv) -> SpecTlvInner {
781            ((e.tag, e.len), (e.content, e.rest))
782        }
783    }
784
785    impl SpecFrom<SpecTlvInner> for SpecTlv {
786        open spec fn spec_from(e: SpecTlvInner) -> SpecTlv {
787            let ((tag, len), (content, rest)) = e;
788            SpecTlv { tag, len, content, rest }
789        }
790    }
791
792    impl<'a> From<Tlv<'a>> for TlvInner<'a> {
793        fn ex_from(e: Tlv) -> (res: TlvInner) {
794            ((e.tag, e.len), (e.content, e.rest))
795        }
796    }
797
798    impl<'a> From<TlvInner<'a>> for Tlv<'a> {
799        fn ex_from(e: TlvInner) -> (res: Tlv) {
800            let ((tag, len), (content, rest)) = e;
801            Tlv { tag, len, content, rest }
802        }
803    }
804
805    impl From<TlvOwned> for TlvInnerOwned {
806        fn ex_from(e: TlvOwned) -> (res: TlvInnerOwned) {
807            ((e.tag, e.len), (e.content, e.rest))
808        }
809    }
810
811    impl From<TlvInnerOwned> for TlvOwned {
812        fn ex_from(e: TlvInnerOwned) -> (res: TlvOwned) {
813            let ((tag, len), (content, rest)) = e;
814            TlvOwned { tag, len, content, rest }
815        }
816    }
817
818    pub struct TlvMapper;
819
820    impl View for TlvMapper {
821        type V = Self;
822
823        open spec fn view(&self) -> Self::V {
824            *self
825        }
826    }
827
828    impl SpecIso for TlvMapper {
829        type Src = SpecTlvInner;
830
831        type Dst = SpecTlv;
832
833        proof fn spec_iso(s: SpecTlvInner) {
834        }
835
836        proof fn spec_iso_rev(s: SpecTlv) {
837        }
838    }
839
840    impl Iso for TlvMapper {
841        type Src<'a> = TlvInner<'a>;
842
843        type Dst<'a> = Tlv<'a>;
844
845        type SrcOwned = TlvInnerOwned;
846
847        type DstOwned = TlvOwned;
848    }
849
850    type Msg1Combinator = Mapped<(((U8, U16), Bytes), Tail), Msg1Mapper>;
851
852    type Msg2Combinator = Mapped<((U8, U16), U32), Msg2Mapper>;
853
854    type Msg3Combinator = Mapped<BytesN<6>, Msg3Mapper>;
855
856    type TlvContentCombinator = AndThen<
857        Bytes,
858        Mapped<
859            ord_choice_type!(Cond<Msg1Combinator>, Cond<Msg2Combinator>, Cond<Msg3Combinator>),
860            TlvContentMapper,
861        >,
862    >;
863
864    type TlvCombinator = Mapped<SpecDepend<(U8, U8), (TlvContentCombinator, Tail)>, TlvMapper>;
865
866    // type TlvCombinator = Mapped<Depend<(U8, U8), (TlvContentCombinator, Tail), impl Fn((u8, u8)) -> (TlvContentCombinator, Tail)>, TlvMapper>;
867    pub open spec fn spec_msg1() -> Msg1Combinator {
868        Mapped { inner: (((U8, U16), Bytes(3)), Tail), mapper: Msg1Mapper }
869    }
870
871    pub open spec fn spec_msg2() -> Msg2Combinator {
872        Mapped { inner: ((U8, U16), U32), mapper: Msg2Mapper }
873    }
874
875    pub open spec fn spec_msg3() -> Msg3Combinator {
876        Mapped { inner: BytesN::<6>, mapper: Msg3Mapper }
877    }
878
879    pub open spec fn spec_tlv_content(tag: u8, len: u8) -> TlvContentCombinator {
880        AndThen(
881            Bytes(len as usize),
882            Mapped {
883                inner: ord_choice!(
884                    Cond { cond: tag == 1, inner: spec_msg1() },
885                    Cond { cond: tag == 2, inner: spec_msg2() },
886                    Cond { cond: tag == 3, inner: spec_msg3() },
887                ),
888                mapper: TlvContentMapper,
889            },
890        )
891    }
892
893    pub open spec fn spec_tlv() -> TlvCombinator {
894        let fst = (U8, U8);
895        let snd = |deps|
896            {
897                let (tag, len) = deps;
898                (spec_tlv_content(tag, len), Tail)
899            };
900        Mapped { inner: SpecDepend { fst, snd }, mapper: TlvMapper }
901    }
902
903    pub fn msg1() -> (o: Msg1Combinator)
904        ensures
905            o@ == spec_msg1(),
906    {
907        Mapped { inner: (((U8, U16), Bytes(3)), Tail), mapper: Msg1Mapper }
908    }
909
910    pub fn msg2() -> (o: Msg2Combinator)
911        ensures
912            o@ == spec_msg2(),
913    {
914        Mapped { inner: ((U8, U16), U32), mapper: Msg2Mapper }
915    }
916
917    pub fn msg3() -> (o: Msg3Combinator)
918        ensures
919            o@ == spec_msg3(),
920    {
921        Mapped { inner: BytesN::<6>, mapper: Msg3Mapper }
922    }
923
924    fn tlv_content(tag: u8, len: u8) -> (o: TlvContentCombinator)
925        ensures
926            o@ == spec_tlv_content(tag@, len@),
927    {
928        AndThen(
929            Bytes(len as usize),
930            Mapped {
931                inner: ord_choice!(
932                    Cond { cond: tag == 1, inner: msg1() },
933                    Cond { cond: tag == 2, inner: msg2() },
934                    Cond { cond: tag == 3, inner: msg3() },
935                ),
936                mapper: TlvContentMapper,
937            },
938        )
939    }
940
941    pub open spec fn spec_msg1_parse(i: Seq<u8>) -> Result<(usize, SpecMsg1), ()> {
942        spec_msg1().spec_parse(i)
943    }
944
945    pub open spec fn spec_msg1_serialize(msg: SpecMsg1) -> Result<Seq<u8>, ()> {
946        spec_msg1().spec_serialize(msg)
947    }
948
949    pub open spec fn spec_msg2_parse(i: Seq<u8>) -> Result<(usize, Msg2), ()> {
950        spec_msg2().spec_parse(i)
951    }
952
953    pub open spec fn spec_msg2_serialize(msg: Msg2) -> Result<Seq<u8>, ()> {
954        spec_msg2().spec_serialize(msg)
955    }
956
957    pub open spec fn spec_msg3_parse(i: Seq<u8>) -> Result<(usize, SpecMsg3), ()> {
958        spec_msg3().spec_parse(i)
959    }
960
961    pub open spec fn spec_msg3_serialize(msg: SpecMsg3) -> Result<Seq<u8>, ()> {
962        spec_msg3().spec_serialize(msg)
963    }
964
965    pub open spec fn spec_tlv_content_parse(i: Seq<u8>, tag: u8, len: u8) -> Result<
966        (usize, SpecTlvContent),
967        (),
968    > {
969        spec_tlv_content(tag, len).spec_parse(i)
970    }
971
972    pub open spec fn spec_tlv_content_serialize(msg: SpecTlvContent, tag: u8, len: u8) -> Result<
973        Seq<u8>,
974        (),
975    > {
976        spec_tlv_content(tag, len).spec_serialize(msg)
977    }
978
979    pub open spec fn spec_tlv_parse(i: Seq<u8>) -> Result<(usize, SpecTlv), ()> {
980        spec_tlv().spec_parse(i)
981    }
982
983    pub open spec fn spec_tlv_serialize(msg: SpecTlv) -> Result<Seq<u8>, ()> {
984        spec_tlv().spec_serialize(msg)
985    }
986
987    pub fn msg1_parse(i: &[u8]) -> (o: Result<(usize, Msg1<'_>), ParseError>)
988        ensures
989            o matches Ok(r) ==> spec_msg1_parse(i@) matches Ok(r_) && r@ == r_,
990    {
991        msg1().parse(i)
992    }
993
994    pub fn msg1_serialize(msg: Msg1<'_>, data: &mut Vec<u8>, pos: usize) -> (o: Result<usize, SerializeError>)
995        ensures
996            o matches Ok(n) ==> {
997                &&& spec_msg1_serialize(msg@) matches Ok(buf)
998                &&& n == buf.len() && data@ == seq_splice(old(data)@, pos, buf)
999            },
1000    {
1001        msg1().serialize(msg, data, pos)
1002    }
1003
1004    pub fn msg2_parse(i: &[u8]) -> (o: Result<(usize, Msg2), ParseError>)
1005        ensures
1006            o matches Ok(r) ==> spec_msg2_parse(i@) matches Ok(r_) && r@ == r_,
1007    {
1008        msg2().parse(i)
1009    }
1010
1011    pub fn msg2_serialize(msg: Msg2, data: &mut Vec<u8>, pos: usize) -> (o: Result<usize, SerializeError>)
1012        ensures
1013            o matches Ok(n) ==> {
1014                &&& spec_msg2_serialize(msg@) matches Ok(buf)
1015                &&& n == buf.len() && data@ == seq_splice(old(data)@, pos, buf)
1016            },
1017    {
1018        msg2().serialize(msg, data, pos)
1019    }
1020
1021    pub fn msg3_parse(i: &[u8]) -> (o: Result<(usize, Msg3<'_>), ParseError>)
1022        ensures
1023            o matches Ok(r) ==> spec_msg3_parse(i@) matches Ok(r_) && r@ == r_,
1024    {
1025        msg3().parse(i)
1026    }
1027
1028    pub fn msg3_serialize(msg: Msg3<'_>, data: &mut Vec<u8>, pos: usize) -> (o: Result<usize, SerializeError>)
1029        ensures
1030            o matches Ok(n) ==> {
1031                &&& spec_msg3_serialize(msg@) matches Ok(buf)
1032                &&& n == buf.len() && data@ == seq_splice(old(data)@, pos, buf)
1033            },
1034    {
1035        msg3().serialize(msg, data, pos)
1036    }
1037
1038    fn tlv_content_parse(i: &[u8], tag: u8, len: u8) -> (o: Result<(usize, TlvContent<'_>), ParseError>)
1039        ensures
1040            o matches Ok(r) ==> spec_tlv_content_parse(i@, tag@, len@) matches Ok(r_) && r@ == r_,
1041    {
1042        tlv_content(tag, len).parse(i)
1043    }
1044
1045    fn tlv_content_serialize(
1046        msg: TlvContent<'_>,
1047        data: &mut Vec<u8>,
1048        pos: usize,
1049        tag: u8,
1050        len: u8,
1051    ) -> (o: Result<usize, SerializeError>)
1052        ensures
1053            o matches Ok(n) ==> {
1054                &&& spec_tlv_content_serialize(msg@, tag@, len@) matches Ok(buf)
1055                &&& n == buf.len() && data@ == seq_splice(old(data)@, pos, buf)
1056            },
1057    {
1058        tlv_content(tag, len).serialize(msg, data, pos)
1059    }
1060
1061    pub fn tlv_parse(i: &[u8]) -> (o: Result<(usize, Tlv<'_>), ParseError>)
1062        ensures
1063            o matches Ok(r) ==> spec_tlv_parse(i@) matches Ok(r_) && r@ == r_,
1064    {
1065        let ghost spec_snd = |deps|
1066            {
1067                let (tag, len) = deps;
1068                (spec_tlv_content(tag, len), Tail)
1069            };
1070        let fst = (U8, U8);
1071        let snd = |deps: (u8, u8)| -> (o: (TlvContentCombinator, Tail))
1072            ensures
1073                o@ == spec_snd(deps@),
1074            {
1075                let (tag, len) = deps;
1076                (tlv_content(tag, len), Tail)
1077            };
1078        Mapped { inner: Depend { fst, snd, spec_snd: Ghost(spec_snd) }, mapper: TlvMapper }.parse(i)
1079    }
1080
1081    pub fn tlv_serialize(msg: Tlv<'_>, data: &mut Vec<u8>, pos: usize) -> (o: Result<usize, SerializeError>)
1082        ensures
1083            o matches Ok(n) ==> {
1084                &&& spec_tlv_serialize(msg@) matches Ok(buf)
1085                &&& n == buf.len() && data@ == seq_splice(old(data)@, pos, buf)
1086            },
1087    {
1088        let ghost spec_snd = |deps|
1089            {
1090                let (tag, len) = deps;
1091                (spec_tlv_content(tag, len), Tail)
1092            };
1093        let fst = (U8, U8);
1094        let snd = |deps: (u8, u8)| -> (o: (TlvContentCombinator, Tail))
1095            ensures
1096                o@ == spec_snd(deps@),
1097            {
1098                let (tag, len) = deps;
1099                (tlv_content(tag, len), Tail)
1100            };
1101        Mapped {
1102            inner: Depend { fst, snd, spec_snd: Ghost(spec_snd) },
1103            mapper: TlvMapper,
1104        }.serialize(msg, data, pos)
1105    }
1106
1107    // use crate::regular::{uints::{U8, U16, U32, U64}, bytes::Bytes, and_then::AndThen, tag::Tag};
1108    // use super::*;
1109    //
1110    // spec fn spec_dep(input: Seq<u8>) -> Result<(usize, ((u8, (u16, u32)), ((), Seq<u8>))), ()> {
1111    //     let msg = SpecDepend {
1112    //         fst: (U8, (U16, U32)),
1113    //         snd: |deps|
1114    //             {
1115    //                 let (a, (_b, c)): (u8, (u16, u32)) = deps;
1116    //                 (Bytes(a as usize).spec_and_then(Tag::spec_new(U64, 99999)), Bytes(c as usize))
1117    //             },
1118    //     };
1119    //     msg.spec_parse(input)
1120    // }
1121    //
1122    // fn dep(input: &[u8]) -> (o: Result<(usize, ((u8, (u16, u32)), ((), &[u8]))), ()>)
1123    //     ensures
1124    //         o is Ok ==> o.unwrap()@ == spec_dep(input@).unwrap(),
1125    // {
1126    //     let ghost spec_snd = |deps|
1127    //         {
1128    //             let (a, (_b, c)): (u8, (u16, u32)) = deps;
1129    //             (Bytes(a as usize).spec_and_then(Tag::spec_new(U64, 99999)), Bytes(c as usize))
1130    //         };
1131    //     let msg = Depend {
1132    //         fst: (U8, (U16, U32)),
1133    //         snd: (|deps| -> (o: (AndThen<Bytes, Tag<U64, u64>>, Bytes))
1134    //             ensures
1135    //                 o@ == spec_snd(deps@),
1136    //             {
1137    //                 let (a, (_b, c)): (u8, (u16, u32)) = deps;
1138    //                 (Bytes(a as usize).and_then(Tag::new(U64, 99999)), Bytes(c as usize))
1139    //             }),
1140    //         spec_snd: Ghost(spec_snd),
1141    //     };
1142    //     msg.parse(input)
1143    // }
1144
1145}
1146
1147} // verus!
vest/regular/depend.rs

vest/regular/
depend.rs
