vest/regular/cond.rs
1use crate::properties::*;
2use vstd::prelude::*;
3
4verus! {
5
6/// Combinator that checks if `cond` is true and then delegates to the `inner` combinator.
7pub struct Cond<Inner> {
8 /// The condition to check before parsing or serializing.
9 pub cond: bool,
10 /// The combinator to delegate to if `cond` is true.
11 pub inner: Inner,
12}
13
14impl<Inner: View> View for Cond<Inner> {
15 type V = Cond<Inner::V>;
16
17 open spec fn view(&self) -> Self::V {
18 Cond { cond: self.cond, inner: self.inner@ }
19 }
20}
21
22impl<Inner: SpecCombinator> SpecCombinator for Cond<Inner> {
23 type SpecResult = Inner::SpecResult;
24
25 open spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()> {
26 if self.cond {
27 self.inner.spec_parse(s)
28 } else {
29 Err(())
30 }
31 }
32
33 proof fn spec_parse_wf(&self, s: Seq<u8>) {
34 if self.cond {
35 self.inner.spec_parse_wf(s);
36 }
37 }
38
39 open spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()> {
40 if self.cond {
41 self.inner.spec_serialize(v)
42 } else {
43 Err(())
44 }
45 }
46}
47
48impl<Inner: SecureSpecCombinator> SecureSpecCombinator for Cond<Inner> {
49 proof fn theorem_serialize_parse_roundtrip(&self, v: Self::SpecResult) {
50 if self.cond {
51 self.inner.theorem_serialize_parse_roundtrip(v);
52 }
53 }
54
55 proof fn theorem_parse_serialize_roundtrip(&self, buf: Seq<u8>) {
56 if self.cond {
57 self.inner.theorem_parse_serialize_roundtrip(buf);
58 }
59 }
60
61 open spec fn is_prefix_secure() -> bool {
62 Inner::is_prefix_secure()
63 }
64
65 proof fn lemma_prefix_secure(&self, s1: Seq<u8>, s2: Seq<u8>) {
66 if self.cond {
67 self.inner.lemma_prefix_secure(s1, s2);
68 }
69 }
70}
71
72impl<Inner: Combinator> Combinator for Cond<Inner> where
73 Inner::V: SecureSpecCombinator<SpecResult = <Inner::Owned as View>::V>,
74 {
75 type Result<'a> = Inner::Result<'a>;
76
77 type Owned = Inner::Owned;
78
79 open spec fn spec_length(&self) -> Option<usize> {
80 if self.cond@ {
81 self.inner.spec_length()
82 } else {
83 None
84 }
85 }
86
87 fn length(&self) -> Option<usize> {
88 if self.cond {
89 self.inner.length()
90 } else {
91 None
92 }
93 }
94
95 open spec fn parse_requires(&self) -> bool {
96 self.inner.parse_requires()
97 }
98
99 fn parse<'a>(&self, s: &'a [u8]) -> Result<(usize, Self::Result<'a>), ParseError> {
100 if self.cond {
101 self.inner.parse(s)
102 } else {
103 Err(ParseError::CondFailed)
104 }
105 }
106
107 open spec fn serialize_requires(&self) -> bool {
108 self.inner.serialize_requires()
109 }
110
111 fn serialize(&self, v: Self::Result<'_>, data: &mut Vec<u8>, pos: usize) -> Result<
112 usize,
113 SerializeError,
114 > {
115 if self.cond {
116 self.inner.serialize(v, data, pos)
117 } else {
118 Err(SerializeError::CondFailed)
119 }
120 }
121}
122
123// #[cfg(test)]
124// mod test {
125// #![allow(unused_imports)]
126
127
128// use crate::properties::*;
129// use crate::regular::and_then::*;
130// use crate::regular::bytes::*;
131// use crate::regular::bytes_n::*;
132// use crate::regular::choice::*;
133// use crate::regular::cond::*;
134// use crate::regular::depend::*;
135// use crate::regular::map::*;
136// use crate::regular::refined::*;
137// use crate::regular::tail::*;
138// use crate::regular::uints::*;
139// use crate::regular::tag::*;
140// use crate::utils::*;
141// use vstd::prelude::*;
142
143// verus! {
144
145// pub type SpecContentType = u8;
146
147// pub type ContentType = u8;
148
149// pub type ContentTypeOwned = u8;
150
151// pub type SpecContent0 = Seq<u8>;
152
153// pub type Content0<'a> = &'a [u8];
154
155// pub type Content0Owned = Vec<u8>;
156
157// pub enum SpecMsgCF4 {
158// C0(SpecContent0),
159// C1(u16),
160// C2(u32),
161// Unrecognized(Seq<u8>),
162// }
163
164// pub type SpecMsgCF4Inner = Either<SpecContent0, Either<u16, Either<u32, Seq<u8>>>>;
165
166// impl SpecFrom<SpecMsgCF4> for SpecMsgCF4Inner {
167// open spec fn spec_from(m: SpecMsgCF4) -> SpecMsgCF4Inner {
168// match m {
169// SpecMsgCF4::C0(m) => Either::Left(m),
170// SpecMsgCF4::C1(m) => Either::Right(Either::Left(m)),
171// SpecMsgCF4::C2(m) => Either::Right(Either::Right(Either::Left(m))),
172// SpecMsgCF4::Unrecognized(m) => Either::Right(Either::Right(Either::Right(m))),
173// }
174// }
175// }
176
177// impl SpecFrom<SpecMsgCF4Inner> for SpecMsgCF4 {
178// open spec fn spec_from(m: SpecMsgCF4Inner) -> SpecMsgCF4 {
179// match m {
180// Either::Left(m) => SpecMsgCF4::C0(m),
181// Either::Right(Either::Left(m)) => SpecMsgCF4::C1(m),
182// Either::Right(Either::Right(Either::Left(m))) => SpecMsgCF4::C2(m),
183// Either::Right(Either::Right(Either::Right(m))) => SpecMsgCF4::Unrecognized(m),
184// }
185// }
186// }
187
188// pub enum MsgCF4<'a> {
189// C0(Content0<'a>),
190// C1(u16),
191// C2(u32),
192// Unrecognized(&'a [u8]),
193// }
194
195// pub type MsgCF4Inner<'a> = Either<Content0<'a>, Either<u16, Either<u32, &'a [u8]>>>;
196
197// impl View for MsgCF4<'_> {
198// type V = SpecMsgCF4;
199
200// open spec fn view(&self) -> Self::V {
201// match self {
202// MsgCF4::C0(m) => SpecMsgCF4::C0(m@),
203// MsgCF4::C1(m) => SpecMsgCF4::C1(m@),
204// MsgCF4::C2(m) => SpecMsgCF4::C2(m@),
205// MsgCF4::Unrecognized(m) => SpecMsgCF4::Unrecognized(m@),
206// }
207// }
208// }
209
210// impl<'a> From<MsgCF4<'a>> for MsgCF4Inner<'a> {
211// fn ex_from(m: MsgCF4<'a>) -> MsgCF4Inner<'a> {
212// match m {
213// MsgCF4::C0(m) => Either::Left(m),
214// MsgCF4::C1(m) => Either::Right(Either::Left(m)),
215// MsgCF4::C2(m) => Either::Right(Either::Right(Either::Left(m))),
216// MsgCF4::Unrecognized(m) => Either::Right(Either::Right(Either::Right(m))),
217// }
218// }
219// }
220
221// impl<'a> From<MsgCF4Inner<'a>> for MsgCF4<'a> {
222// fn ex_from(m: MsgCF4Inner<'a>) -> MsgCF4<'a> {
223// match m {
224// Either::Left(m) => MsgCF4::C0(m),
225// Either::Right(Either::Left(m)) => MsgCF4::C1(m),
226// Either::Right(Either::Right(Either::Left(m))) => MsgCF4::C2(m),
227// Either::Right(Either::Right(Either::Right(m))) => MsgCF4::Unrecognized(m),
228// }
229// }
230// }
231
232// pub struct MsgCF4Mapper;
233
234// impl View for MsgCF4Mapper {
235// type V = Self;
236
237// open spec fn view(&self) -> Self::V {
238// *self
239// }
240// }
241
242// impl SpecIso for MsgCF4Mapper {
243// type Src = SpecMsgCF4Inner;
244
245// type Dst = SpecMsgCF4;
246
247// proof fn spec_iso(s: Self::Src) {
248// }
249
250// proof fn spec_iso_rev(s: Self::Dst) {
251// }
252// }
253
254// impl Iso for MsgCF4Mapper {
255// type Src<'a> = MsgCF4Inner<'a>;
256
257// type Dst<'a> = MsgCF4<'a>;
258
259// type SrcOwned = MsgCF4OwnedInner;
260
261// type DstOwned = MsgCF4Owned;
262// }
263
264// pub enum MsgCF4Owned {
265// C0(Content0Owned),
266// C1(u16),
267// C2(u32),
268// Unrecognized(Vec<u8>),
269// }
270
271// pub type MsgCF4OwnedInner = Either<Content0Owned, Either<u16, Either<u32, Vec<u8>>>>;
272
273// impl View for MsgCF4Owned {
274// type V = SpecMsgCF4;
275
276// open spec fn view(&self) -> Self::V {
277// match self {
278// MsgCF4Owned::C0(m) => SpecMsgCF4::C0(m@),
279// MsgCF4Owned::C1(m) => SpecMsgCF4::C1(m@),
280// MsgCF4Owned::C2(m) => SpecMsgCF4::C2(m@),
281// MsgCF4Owned::Unrecognized(m) => SpecMsgCF4::Unrecognized(m@),
282// }
283// }
284// }
285
286// impl From<MsgCF4Owned> for MsgCF4OwnedInner {
287// fn ex_from(m: MsgCF4Owned) -> MsgCF4OwnedInner {
288// match m {
289// MsgCF4Owned::C0(m) => Either::Left(m),
290// MsgCF4Owned::C1(m) => Either::Right(Either::Left(m)),
291// MsgCF4Owned::C2(m) => Either::Right(Either::Right(Either::Left(m))),
292// MsgCF4Owned::Unrecognized(m) => Either::Right(Either::Right(Either::Right(m))),
293// }
294// }
295// }
296
297// impl From<MsgCF4OwnedInner> for MsgCF4Owned {
298// fn ex_from(m: MsgCF4OwnedInner) -> MsgCF4Owned {
299// match m {
300// Either::Left(m) => MsgCF4Owned::C0(m),
301// Either::Right(Either::Left(m)) => MsgCF4Owned::C1(m),
302// Either::Right(Either::Right(Either::Left(m))) => MsgCF4Owned::C2(m),
303// Either::Right(Either::Right(Either::Right(m))) => MsgCF4Owned::Unrecognized(m),
304// }
305// }
306// }
307
308// pub struct SpecMsgC {
309// pub f2: SpecContentType,
310// pub f3: u8,
311// pub f4: SpecMsgCF4,
312// }
313
314// pub type SpecMsgCInner = ((SpecContentType, u8), SpecMsgCF4);
315
316// impl SpecFrom<SpecMsgC> for SpecMsgCInner {
317// open spec fn spec_from(m: SpecMsgC) -> SpecMsgCInner {
318// ((m.f2, m.f3), m.f4)
319// }
320// }
321
322// impl SpecFrom<SpecMsgCInner> for SpecMsgC {
323// open spec fn spec_from(m: SpecMsgCInner) -> SpecMsgC {
324// let ((f2, f3), f4) = m;
325// SpecMsgC { f2, f3, f4 }
326// }
327// }
328
329// pub struct MsgC<'a> {
330// pub f2: ContentType,
331// pub f3: u8,
332// pub f4: MsgCF4<'a>,
333// }
334
335// pub type MsgCInner<'a> = ((ContentType, u8), MsgCF4<'a>);
336
337// impl View for MsgC<'_> {
338// type V = SpecMsgC;
339
340// open spec fn view(&self) -> Self::V {
341// SpecMsgC { f2: self.f2@, f3: self.f3@, f4: self.f4@ }
342// }
343// }
344
345// impl<'a> From<MsgC<'a>> for MsgCInner<'a> {
346// fn ex_from(m: MsgC<'a>) -> MsgCInner<'a> {
347// ((m.f2, m.f3), m.f4)
348// }
349// }
350
351// impl<'a> From<MsgCInner<'a>> for MsgC<'a> {
352// fn ex_from(m: MsgCInner<'a>) -> MsgC<'a> {
353// let ((f2, f3), f4) = m;
354// MsgC { f2, f3, f4 }
355// }
356// }
357
358// pub struct MsgCMapper;
359
360// impl View for MsgCMapper {
361// type V = Self;
362
363// open spec fn view(&self) -> Self::V {
364// *self
365// }
366// }
367
368// impl SpecIso for MsgCMapper {
369// type Src = SpecMsgCInner;
370
371// type Dst = SpecMsgC;
372
373// proof fn spec_iso(s: Self::Src) {
374// }
375
376// proof fn spec_iso_rev(s: Self::Dst) {
377// }
378// }
379
380// impl Iso for MsgCMapper {
381// type Src<'a> = MsgCInner<'a>;
382
383// type Dst<'a> = MsgC<'a>;
384
385// type SrcOwned = MsgCOwnedInner;
386
387// type DstOwned = MsgCOwned;
388// }
389
390// pub struct MsgCOwned {
391// pub f2: ContentTypeOwned,
392// pub f3: u8,
393// pub f4: MsgCF4Owned,
394// }
395
396// pub type MsgCOwnedInner = ((ContentTypeOwned, u8), MsgCF4Owned);
397
398// impl View for MsgCOwned {
399// type V = SpecMsgC;
400
401// open spec fn view(&self) -> Self::V {
402// SpecMsgC { f2: self.f2@, f3: self.f3@, f4: self.f4@ }
403// }
404// }
405
406// impl From<MsgCOwned> for MsgCOwnedInner {
407// fn ex_from(m: MsgCOwned) -> MsgCOwnedInner {
408// ((m.f2, m.f3), m.f4)
409// }
410// }
411
412// impl From<MsgCOwnedInner> for MsgCOwned {
413// fn ex_from(m: MsgCOwnedInner) -> MsgCOwned {
414// let ((f2, f3), f4) = m;
415// MsgCOwned { f2, f3, f4 }
416// }
417// }
418
419// pub struct SpecMsgD {
420// pub f1: Seq<u8>,
421// pub f2: u16,
422// }
423
424// pub type SpecMsgDInner = (Seq<u8>, u16);
425
426// impl SpecFrom<SpecMsgD> for SpecMsgDInner {
427// open spec fn spec_from(m: SpecMsgD) -> SpecMsgDInner {
428// (m.f1, m.f2)
429// }
430// }
431
432// impl SpecFrom<SpecMsgDInner> for SpecMsgD {
433// open spec fn spec_from(m: SpecMsgDInner) -> SpecMsgD {
434// let (f1, f2) = m;
435// SpecMsgD { f1, f2 }
436// }
437// }
438
439// pub struct MsgD<'a> {
440// pub f1: &'a [u8],
441// pub f2: u16,
442// }
443
444// pub type MsgDInner<'a> = (&'a [u8], u16);
445
446// impl View for MsgD<'_> {
447// type V = SpecMsgD;
448
449// open spec fn view(&self) -> Self::V {
450// SpecMsgD { f1: self.f1@, f2: self.f2@ }
451// }
452// }
453
454// impl<'a> From<MsgD<'a>> for MsgDInner<'a> {
455// fn ex_from(m: MsgD<'a>) -> MsgDInner<'a> {
456// (m.f1, m.f2)
457// }
458// }
459
460// impl<'a> From<MsgDInner<'a>> for MsgD<'a> {
461// fn ex_from(m: MsgDInner<'a>) -> MsgD<'a> {
462// let (f1, f2) = m;
463// MsgD { f1, f2 }
464// }
465// }
466
467// pub struct MsgDMapper;
468
469// impl View for MsgDMapper {
470// type V = Self;
471
472// open spec fn view(&self) -> Self::V {
473// *self
474// }
475// }
476
477// impl SpecIso for MsgDMapper {
478// type Src = SpecMsgDInner;
479
480// type Dst = SpecMsgD;
481
482// proof fn spec_iso(s: Self::Src) {
483// }
484
485// proof fn spec_iso_rev(s: Self::Dst) {
486// }
487// }
488
489// impl Iso for MsgDMapper {
490// type Src<'a> = MsgDInner<'a>;
491
492// type Dst<'a> = MsgD<'a>;
493
494// type SrcOwned = MsgDOwnedInner;
495
496// type DstOwned = MsgDOwned;
497// }
498
499// pub struct MsgDOwned {
500// pub f1: Vec<u8>,
501// pub f2: u16,
502// }
503
504// pub type MsgDOwnedInner = (Vec<u8>, u16);
505
506// impl View for MsgDOwned {
507// type V = SpecMsgD;
508
509// open spec fn view(&self) -> Self::V {
510// SpecMsgD { f1: self.f1@, f2: self.f2@ }
511// }
512// }
513
514// impl From<MsgDOwned> for MsgDOwnedInner {
515// fn ex_from(m: MsgDOwned) -> MsgDOwnedInner {
516// (m.f1, m.f2)
517// }
518// }
519
520// impl From<MsgDOwnedInner> for MsgDOwned {
521// fn ex_from(m: MsgDOwnedInner) -> MsgDOwned {
522// let (f1, f2) = m;
523// MsgDOwned { f1, f2 }
524// }
525// }
526
527// pub struct SpecMsgB {
528// pub f1: SpecMsgD,
529// }
530
531// pub type SpecMsgBInner = SpecMsgD;
532
533// impl SpecFrom<SpecMsgB> for SpecMsgBInner {
534// open spec fn spec_from(m: SpecMsgB) -> SpecMsgBInner {
535// m.f1
536// }
537// }
538
539// impl SpecFrom<SpecMsgBInner> for SpecMsgB {
540// open spec fn spec_from(m: SpecMsgBInner) -> SpecMsgB {
541// let f1 = m;
542// SpecMsgB { f1 }
543// }
544// }
545
546// pub struct MsgB<'a> {
547// pub f1: MsgD<'a>,
548// }
549
550// pub type MsgBInner<'a> = MsgD<'a>;
551
552// impl View for MsgB<'_> {
553// type V = SpecMsgB;
554
555// open spec fn view(&self) -> Self::V {
556// SpecMsgB { f1: self.f1@ }
557// }
558// }
559
560// impl<'a> From<MsgB<'a>> for MsgBInner<'a> {
561// fn ex_from(m: MsgB<'a>) -> MsgBInner<'a> {
562// m.f1
563// }
564// }
565
566// impl<'a> From<MsgBInner<'a>> for MsgB<'a> {
567// fn ex_from(m: MsgBInner<'a>) -> MsgB<'a> {
568// let f1 = m;
569// MsgB { f1 }
570// }
571// }
572
573// pub struct MsgBMapper;
574
575// impl View for MsgBMapper {
576// type V = Self;
577
578// open spec fn view(&self) -> Self::V {
579// *self
580// }
581// }
582
583// impl SpecIso for MsgBMapper {
584// type Src = SpecMsgBInner;
585
586// type Dst = SpecMsgB;
587
588// proof fn spec_iso(s: Self::Src) {
589// }
590
591// proof fn spec_iso_rev(s: Self::Dst) {
592// }
593// }
594
595// impl Iso for MsgBMapper {
596// type Src<'a> = MsgBInner<'a>;
597
598// type Dst<'a> = MsgB<'a>;
599
600// type SrcOwned = MsgBOwnedInner;
601
602// type DstOwned = MsgBOwned;
603// }
604
605// pub struct MsgBOwned {
606// pub f1: MsgDOwned,
607// }
608
609// pub type MsgBOwnedInner = MsgDOwned;
610
611// impl View for MsgBOwned {
612// type V = SpecMsgB;
613
614// open spec fn view(&self) -> Self::V {
615// SpecMsgB { f1: self.f1@ }
616// }
617// }
618
619// impl From<MsgBOwned> for MsgBOwnedInner {
620// fn ex_from(m: MsgBOwned) -> MsgBOwnedInner {
621// m.f1
622// }
623// }
624
625// impl From<MsgBOwnedInner> for MsgBOwned {
626// fn ex_from(m: MsgBOwnedInner) -> MsgBOwned {
627// let f1 = m;
628// MsgBOwned { f1 }
629// }
630// }
631
632// pub struct SpecMsgA {
633// pub f1: SpecMsgB,
634// pub f2: Seq<u8>,
635// }
636
637// pub type SpecMsgAInner = (SpecMsgB, Seq<u8>);
638
639// impl SpecFrom<SpecMsgA> for SpecMsgAInner {
640// open spec fn spec_from(m: SpecMsgA) -> SpecMsgAInner {
641// (m.f1, m.f2)
642// }
643// }
644
645// impl SpecFrom<SpecMsgAInner> for SpecMsgA {
646// open spec fn spec_from(m: SpecMsgAInner) -> SpecMsgA {
647// let (f1, f2) = m;
648// SpecMsgA { f1, f2 }
649// }
650// }
651
652// pub struct MsgA<'a> {
653// pub f1: MsgB<'a>,
654// pub f2: &'a [u8],
655// }
656
657// pub type MsgAInner<'a> = (MsgB<'a>, &'a [u8]);
658
659// impl View for MsgA<'_> {
660// type V = SpecMsgA;
661
662// open spec fn view(&self) -> Self::V {
663// SpecMsgA { f1: self.f1@, f2: self.f2@ }
664// }
665// }
666
667// impl<'a> From<MsgA<'a>> for MsgAInner<'a> {
668// fn ex_from(m: MsgA<'a>) -> MsgAInner<'a> {
669// (m.f1, m.f2)
670// }
671// }
672
673// impl<'a> From<MsgAInner<'a>> for MsgA<'a> {
674// fn ex_from(m: MsgAInner<'a>) -> MsgA<'a> {
675// let (f1, f2) = m;
676// MsgA { f1, f2 }
677// }
678// }
679
680// pub struct MsgAMapper;
681
682// impl View for MsgAMapper {
683// type V = Self;
684
685// open spec fn view(&self) -> Self::V {
686// *self
687// }
688// }
689
690// impl SpecIso for MsgAMapper {
691// type Src = SpecMsgAInner;
692
693// type Dst = SpecMsgA;
694
695// proof fn spec_iso(s: Self::Src) {
696// }
697
698// proof fn spec_iso_rev(s: Self::Dst) {
699// }
700// }
701
702// impl Iso for MsgAMapper {
703// type Src<'a> = MsgAInner<'a>;
704
705// type Dst<'a> = MsgA<'a>;
706
707// type SrcOwned = MsgAOwnedInner;
708
709// type DstOwned = MsgAOwned;
710// }
711
712// pub struct MsgAOwned {
713// pub f1: MsgBOwned,
714// pub f2: Vec<u8>,
715// }
716
717// pub type MsgAOwnedInner = (MsgBOwned, Vec<u8>);
718
719// impl View for MsgAOwned {
720// type V = SpecMsgA;
721
722// open spec fn view(&self) -> Self::V {
723// SpecMsgA { f1: self.f1@, f2: self.f2@ }
724// }
725// }
726
727// impl From<MsgAOwned> for MsgAOwnedInner {
728// fn ex_from(m: MsgAOwned) -> MsgAOwnedInner {
729// (m.f1, m.f2)
730// }
731// }
732
733// impl From<MsgAOwnedInner> for MsgAOwned {
734// fn ex_from(m: MsgAOwnedInner) -> MsgAOwned {
735// let (f1, f2) = m;
736// MsgAOwned { f1, f2 }
737// }
738// }
739
740// pub type ContentTypeCombinator = U8;
741
742// pub type Content0Combinator = Bytes;
743
744// pub type MsgCF4Combinator = AndThen<
745// Bytes,
746// Mapped<
747// OrdChoice<Cond<Content0Combinator>, OrdChoice<Cond<U16>, OrdChoice<Cond<U32>, Cond<Tail>>>>,
748// MsgCF4Mapper,
749// >,
750// >;
751
752// pub type MsgCCombinator = Mapped<
753// SpecDepend<(ContentTypeCombinator, U8), MsgCF4Combinator>,
754// MsgCMapper,
755// >;
756
757// pub spec const SPEC_MSGD_F1: Seq<u8> = seq![1; 4];
758
759// pub exec const MSGD_F1: [u8; 4]
760// ensures
761// MSGD_F1@ == SPEC_MSGD_F1,
762// {
763// let arr: [u8; 4] = [1;4];
764// assert(arr@ == SPEC_MSGD_F1);
765// arr
766// }
767
768// pub struct BytesPredicate16235736133663645624;
769
770// impl View for BytesPredicate16235736133663645624 {
771// type V = Self;
772
773// open spec fn view(&self) -> Self::V {
774// *self
775// }
776// }
777
778// impl SpecPred for BytesPredicate16235736133663645624 {
779// type Input = Seq<u8>;
780
781// open spec fn spec_apply(&self, i: &Self::Input) -> bool {
782// i == &SPEC_MSGD_F1
783// }
784// }
785
786// impl Pred for BytesPredicate16235736133663645624 {
787// type Input<'a> = &'a [u8];
788
789// type InputOwned = Vec<u8>;
790
791// fn apply(&self, i: &Self::Input<'_>) -> bool {
792// compare_slice(i, MSGD_F1.as_slice())
793// }
794// }
795
796// pub const MSGD_F2: u16 = 4660;
797
798// pub type MsgDCombinator = Mapped<
799// (Refined<BytesN<4>, BytesPredicate16235736133663645624>, Refined<U16, TagPred<u16>>),
800// MsgDMapper,
801// >;
802
803// pub type MsgBCombinator = Mapped<MsgDCombinator, MsgBMapper>;
804
805// pub type MsgACombinator = Mapped<(MsgBCombinator, Tail), MsgAMapper>;
806
807// pub open spec fn spec_content_type() -> ContentTypeCombinator {
808// U8
809// }
810
811// pub fn content_type() -> (o: ContentTypeCombinator)
812// ensures
813// o@ == spec_content_type(),
814// {
815// U8
816// }
817
818// pub open spec fn spec_content_0(num: u8) -> Content0Combinator {
819// Bytes(num as usize)
820// }
821
822// pub fn content_0<'a>(num: u8) -> (o: Content0Combinator)
823// ensures
824// o@ == spec_content_0(num@),
825// {
826// Bytes(num as usize)
827// }
828
829// pub open spec fn spec_msg_c_f4(f3: u8, f2: SpecContentType) -> MsgCF4Combinator {
830// AndThen(
831// Bytes(f3 as usize),
832// Mapped {
833// inner: OrdChoice(
834// Cond { cond: f2 == 0, inner: spec_content_0(f3) },
835// OrdChoice(
836// Cond { cond: f2 == 1, inner: U16 },
837// OrdChoice(
838// Cond { cond: f2 == 2, inner: U32 },
839// Cond { cond: !(f2 == 0 || f2 == 1 || f2 == 2), inner: Tail },
840// ),
841// ),
842// ),
843// mapper: MsgCF4Mapper,
844// },
845// )
846// }
847
848// pub fn msg_c_f4<'a>(f3: u8, f2: ContentType) -> (o: MsgCF4Combinator)
849// ensures
850// o@ == spec_msg_c_f4(f3@, f2@),
851// {
852// AndThen(
853// Bytes(f3 as usize),
854// Mapped {
855// inner: OrdChoice(
856// Cond { cond: f2 == 0, inner: content_0(f3) },
857// OrdChoice(
858// Cond { cond: f2 == 1, inner: U16 },
859// OrdChoice(
860// Cond { cond: f2 == 2, inner: U32 },
861// Cond { cond: !(f2 == 0 || f2 == 1 || f2 == 2), inner: Tail },
862// ),
863// ),
864// ),
865// mapper: MsgCF4Mapper,
866// },
867// )
868// }
869
870// pub open spec fn spec_msg_d() -> MsgDCombinator {
871// Mapped {
872// inner: (
873// Refined { inner: BytesN::<4>, predicate: BytesPredicate16235736133663645624 },
874// Refined { inner: U16, predicate: TagPred(MSGD_F2) },
875// ),
876// mapper: MsgDMapper,
877// }
878// }
879
880// pub fn msg_d() -> (o: MsgDCombinator)
881// ensures
882// o@ == spec_msg_d(),
883// {
884// Mapped {
885// inner: (
886// Refined { inner: BytesN::<4>, predicate: BytesPredicate16235736133663645624 },
887// Refined { inner: U16, predicate: TagPred(MSGD_F2) },
888// ),
889// mapper: MsgDMapper,
890// }
891// }
892
893// pub open spec fn spec_msg_b() -> MsgBCombinator {
894// Mapped { inner: spec_msg_d(), mapper: MsgBMapper }
895// }
896
897// pub fn msg_b() -> (o: MsgBCombinator)
898// ensures
899// o@ == spec_msg_b(),
900// {
901// Mapped { inner: msg_d(), mapper: MsgBMapper }
902// }
903
904// pub open spec fn spec_msg_a() -> MsgACombinator {
905// Mapped { inner: (spec_msg_b(), Tail), mapper: MsgAMapper }
906// }
907
908// pub fn msg_a() -> (o: MsgACombinator)
909// ensures
910// o@ == spec_msg_a(),
911// {
912// Mapped { inner: (msg_b(), Tail), mapper: MsgAMapper }
913// }
914
915// pub open spec fn parse_spec_content_type(i: Seq<u8>) -> Result<(usize, SpecContentType), ()> {
916// spec_content_type().spec_parse(i)
917// }
918
919// pub open spec fn serialize_spec_content_type(msg: SpecContentType) -> Result<Seq<u8>, ()> {
920// spec_content_type().spec_serialize(msg)
921// }
922
923// pub fn parse_content_type(i: &[u8]) -> (o: Result<(usize, ContentType), ParseError>)
924// ensures
925// o matches Ok(r) ==> parse_spec_content_type(i@) matches Ok(r_) && r@ == r_,
926// {
927// content_type().parse(i)
928// }
929
930// pub fn serialize_content_type(msg: ContentType, data: &mut Vec<u8>, pos: usize) -> (o: Result<
931// usize,
932// SerializeError,
933// >)
934// ensures
935// o matches Ok(n) ==> {
936// &&& serialize_spec_content_type(msg@) matches Ok(buf)
937// &&& n == buf.len() && data@ == seq_splice(old(data)@, pos, buf)
938// },
939// {
940// content_type().serialize(msg, data, pos)
941// }
942
943// pub open spec fn parse_spec_content_0(i: Seq<u8>, num: u8) -> Result<(usize, SpecContent0), ()> {
944// spec_content_0(num).spec_parse(i)
945// }
946
947// pub open spec fn serialize_spec_content_0(msg: SpecContent0, num: u8) -> Result<Seq<u8>, ()> {
948// spec_content_0(num).spec_serialize(msg)
949// }
950
951// pub fn parse_content_0(i: &[u8], num: u8) -> (o: Result<(usize, Content0<'_>), ParseError>)
952// ensures
953// o matches Ok(r) ==> parse_spec_content_0(i@, num@) matches Ok(r_) && r@ == r_,
954// {
955// content_0(num).parse(i)
956// }
957
958// pub fn serialize_content_0(msg: Content0<'_>, data: &mut Vec<u8>, pos: usize, num: u8) -> (o:
959// Result<usize, SerializeError>)
960// ensures
961// o matches Ok(n) ==> {
962// &&& serialize_spec_content_0(msg@, num@) matches Ok(buf)
963// &&& n == buf.len() && data@ == seq_splice(old(data)@, pos, buf)
964// },
965// {
966// content_0(num).serialize(msg, data, pos)
967// }
968
969// pub open spec fn parse_spec_msg_c_f4(i: Seq<u8>, f3: u8, f2: SpecContentType) -> Result<
970// (usize, SpecMsgCF4),
971// (),
972// > {
973// spec_msg_c_f4(f3, f2).spec_parse(i)
974// }
975
976// pub open spec fn serialize_spec_msg_c_f4(msg: SpecMsgCF4, f3: u8, f2: SpecContentType) -> Result<
977// Seq<u8>,
978// (),
979// > {
980// spec_msg_c_f4(f3, f2).spec_serialize(msg)
981// }
982
983// pub fn parse_msg_c_f4(i: &[u8], f3: u8, f2: ContentType) -> (o: Result<
984// (usize, MsgCF4<'_>),
985// ParseError,
986// >)
987// ensures
988// o matches Ok(r) ==> parse_spec_msg_c_f4(i@, f3@, f2@) matches Ok(r_) && r@ == r_,
989// {
990// msg_c_f4(f3, f2).parse(i)
991// }
992
993// pub fn serialize_msg_c_f4(
994// msg: MsgCF4<'_>,
995// data: &mut Vec<u8>,
996// pos: usize,
997// f3: u8,
998// f2: ContentType,
999// ) -> (o: Result<usize, SerializeError>)
1000// ensures
1001// o matches Ok(n) ==> {
1002// &&& serialize_spec_msg_c_f4(msg@, f3@, f2@) matches Ok(buf)
1003// &&& n == buf.len() && data@ == seq_splice(old(data)@, pos, buf)
1004// },
1005// {
1006// msg_c_f4(f3, f2).serialize(msg, data, pos)
1007// }
1008
1009// pub open spec fn parse_spec_msg_c(i: Seq<u8>) -> Result<(usize, SpecMsgC), ()> {
1010// let fst = (spec_content_type(), U8);
1011// let snd = |deps|
1012// {
1013// let (f2, f3) = deps;
1014// spec_msg_c_f4(f3, f2)
1015// };
1016// Mapped { inner: SpecDepend { fst, snd }, mapper: MsgCMapper }.spec_parse(i)
1017// }
1018
1019// pub open spec fn serialize_spec_msg_c(msg: SpecMsgC) -> Result<Seq<u8>, ()> {
1020// let fst = (spec_content_type(), U8);
1021// let snd = |deps|
1022// {
1023// let (f2, f3) = deps;
1024// spec_msg_c_f4(f3, f2)
1025// };
1026// Mapped { inner: SpecDepend { fst, snd }, mapper: MsgCMapper }.spec_serialize(msg)
1027// }
1028
1029// pub fn parse_msg_c(i: &[u8]) -> (o: Result<(usize, MsgC<'_>), ParseError>)
1030// ensures
1031// o matches Ok(r) ==> parse_spec_msg_c(i@) matches Ok(r_) && r@ == r_,
1032// {
1033// let ghost spec_snd = |deps|
1034// {
1035// let (f2, f3) = deps;
1036// spec_msg_c_f4(f3, f2)
1037// };
1038// let fst = (content_type(), U8);
1039// let snd = |deps: (ContentType, u8)| -> (o: MsgCF4Combinator)
1040// ensures
1041// o@ == spec_snd(deps@),
1042// {
1043// let (f2, f3) = deps;
1044// msg_c_f4(f3, f2)
1045// };
1046// Mapped { inner: Depend { fst, snd, spec_snd: Ghost(spec_snd) }, mapper: MsgCMapper }.parse(i)
1047// }
1048
1049// pub fn serialize_msg_c(msg: MsgC<'_>, data: &mut Vec<u8>, pos: usize) -> (o: Result<
1050// usize,
1051// SerializeError,
1052// >)
1053// ensures
1054// o matches Ok(n) ==> {
1055// &&& serialize_spec_msg_c(msg@) matches Ok(buf)
1056// &&& n == buf.len() && data@ == seq_splice(old(data)@, pos, buf)
1057// },
1058// {
1059// let ghost spec_snd = |deps|
1060// {
1061// let (f2, f3) = deps;
1062// spec_msg_c_f4(f3, f2)
1063// };
1064// let fst = (content_type(), U8);
1065// let snd = |deps: (ContentType, u8)| -> (o: MsgCF4Combinator)
1066// ensures
1067// o@ == spec_snd(deps@),
1068// {
1069// let (f2, f3) = deps;
1070// msg_c_f4(f3, f2)
1071// };
1072// Mapped { inner: Depend { fst, snd, spec_snd: Ghost(spec_snd) }, mapper: MsgCMapper }.serialize(
1073// msg,
1074// data,
1075// pos,
1076// )
1077// }
1078
1079// pub open spec fn parse_spec_msg_d(i: Seq<u8>) -> Result<(usize, SpecMsgD), ()> {
1080// spec_msg_d().spec_parse(i)
1081// }
1082
1083// pub open spec fn serialize_spec_msg_d(msg: SpecMsgD) -> Result<Seq<u8>, ()> {
1084// spec_msg_d().spec_serialize(msg)
1085// }
1086
1087// pub fn parse_msg_d(i: &[u8]) -> (o: Result<(usize, MsgD<'_>), ParseError>)
1088// ensures
1089// o matches Ok(r) ==> parse_spec_msg_d(i@) matches Ok(r_) && r@ == r_,
1090// {
1091// msg_d().parse(i)
1092// }
1093
1094// pub fn serialize_msg_d(msg: MsgD<'_>, data: &mut Vec<u8>, pos: usize) -> (o: Result<
1095// usize,
1096// SerializeError,
1097// >)
1098// ensures
1099// o matches Ok(n) ==> {
1100// &&& serialize_spec_msg_d(msg@) matches Ok(buf)
1101// &&& n == buf.len() && data@ == seq_splice(old(data)@, pos, buf)
1102// },
1103// {
1104// msg_d().serialize(msg, data, pos)
1105// }
1106
1107// pub open spec fn parse_spec_msg_b(i: Seq<u8>) -> Result<(usize, SpecMsgB), ()> {
1108// spec_msg_b().spec_parse(i)
1109// }
1110
1111// pub open spec fn serialize_spec_msg_b(msg: SpecMsgB) -> Result<Seq<u8>, ()> {
1112// spec_msg_b().spec_serialize(msg)
1113// }
1114
1115// pub fn parse_msg_b(i: &[u8]) -> (o: Result<(usize, MsgB<'_>), ParseError>)
1116// ensures
1117// o matches Ok(r) ==> parse_spec_msg_b(i@) matches Ok(r_) && r@ == r_,
1118// {
1119// msg_b().parse(i)
1120// }
1121
1122// pub fn serialize_msg_b(msg: MsgB<'_>, data: &mut Vec<u8>, pos: usize) -> (o: Result<
1123// usize,
1124// SerializeError,
1125// >)
1126// ensures
1127// o matches Ok(n) ==> {
1128// &&& serialize_spec_msg_b(msg@) matches Ok(buf)
1129// &&& n == buf.len() && data@ == seq_splice(old(data)@, pos, buf)
1130// },
1131// {
1132// msg_b().serialize(msg, data, pos)
1133// }
1134
1135// pub open spec fn parse_spec_msg_a(i: Seq<u8>) -> Result<(usize, SpecMsgA), ()> {
1136// spec_msg_a().spec_parse(i)
1137// }
1138
1139// pub open spec fn serialize_spec_msg_a(msg: SpecMsgA) -> Result<Seq<u8>, ()> {
1140// spec_msg_a().spec_serialize(msg)
1141// }
1142
1143// pub fn parse_msg_a(i: &[u8]) -> (o: Result<(usize, MsgA<'_>), ParseError>)
1144// ensures
1145// o matches Ok(r) ==> parse_spec_msg_a(i@) matches Ok(r_) && r@ == r_,
1146// {
1147// msg_a().parse(i)
1148// }
1149
1150// pub fn serialize_msg_a(msg: MsgA<'_>, data: &mut Vec<u8>, pos: usize) -> (o: Result<
1151// usize,
1152// SerializeError,
1153// >)
1154// ensures
1155// o matches Ok(n) ==> {
1156// &&& serialize_spec_msg_a(msg@) matches Ok(buf)
1157// &&& n == buf.len() && data@ == seq_splice(old(data)@, pos, buf)
1158// },
1159// {
1160// msg_a().serialize(msg, data, pos)
1161// }
1162
1163
1164
1165
1166// } // verus!
1167// // use crate::regular::{
1168// // choice::{OrdChoice, Either},
1169// // bytes_n::BytesN,
1170// // depend::{Depend, SpecDepend},
1171// // bytes::Bytes,
1172// // uints::{U8, U64},
1173// // and_then::AndThen,
1174// // };
1175// // use super::*;
1176// //
1177// // spec fn spec_ord_conds(val: u8) -> OrdChoice<Cond<u8, u8, BytesN<2>>, Cond<u8, u8, BytesN<3>>> {
1178// // OrdChoice(
1179// // Cond { lhs: val, rhs: 0, inner: BytesN::<2> },
1180// // Cond { lhs: val, rhs: 1, inner: BytesN::<3> },
1181// // )
1182// // }
1183// //
1184// // fn ord_conds(val: u8) -> (o: OrdChoice<Cond<u8, u8, BytesN<2>>, Cond<u8, u8, BytesN<3>>>)
1185// // ensures
1186// // o@ == spec_ord_conds(val@),
1187// // {
1188// // OrdChoice::new(
1189// // Cond { lhs: val, rhs: 0, inner: BytesN::<2> },
1190// // Cond { lhs: val, rhs: 1, inner: BytesN::<3> },
1191// // )
1192// // }
1193// //
1194// // spec fn spec_parse_tlv(input: Seq<u8>) -> Result<
1195// // (usize, ((u8, u8), Either<Seq<u8>, u64>)),
1196// // (),
1197// // > {
1198// // SpecDepend {
1199// // fst: (U8, U8),
1200// // snd: |deps: (u8, u8)|
1201// // {
1202// // let (tag, len) = deps;
1203// // Bytes(len as usize).spec_and_then(
1204// // OrdChoice(
1205// // Cond { lhs: tag, rhs: 0, inner: BytesN::<2> },
1206// // Cond { lhs: tag, rhs: 1, inner: U64 },
1207// // ),
1208// // )
1209// // },
1210// // }.spec_parse(input)
1211// // }
1212// //
1213// // fn parse_tlv(input: &[u8]) -> (res: Result<(usize, ((u8, u8), Either<&[u8], u64>)), ()>)
1214// // ensures
1215// // res is Ok ==> res.unwrap()@ == spec_parse_tlv(input@).unwrap(),
1216// // {
1217// // let ghost spec_snd = |deps: (u8, u8)|
1218// // {
1219// // let (tag, len) = deps;
1220// // Bytes(len as usize).spec_and_then(
1221// // OrdChoice(
1222// // Cond { lhs: tag, rhs: 0, inner: BytesN::<2> },
1223// // Cond { lhs: tag, rhs: 1, inner: U64 },
1224// // ),
1225// // )
1226// // };
1227// // Depend {
1228// // fst: (U8, U8),
1229// // snd: (|deps: (u8, u8)| -> (o: AndThen<
1230// // Bytes,
1231// // OrdChoice<Cond<u8, u8, BytesN<2>>, Cond<u8, u8, U64>>,
1232// // >)
1233// // ensures
1234// // o@ == spec_snd(deps@),
1235// // {
1236// // let (tag, len) = deps;
1237// // Bytes(len as usize).and_then(
1238// // OrdChoice::new(
1239// // Cond { lhs: tag, rhs: 0, inner: BytesN::<2> },
1240// // Cond { lhs: tag, rhs: 1, inner: U64 },
1241// // ),
1242// // )
1243// // }),
1244// // spec_snd: Ghost(spec_snd),
1245// // }.parse(input)
1246// // }
1247// //
1248
1249
1250// }
1251
1252} // verus!