vest_lib/core/exec/
bridge_lemmas.rs

1//! Bridges executable invariants through common combinator wrappers.
2use crate::combinators::bytes::{AndThen, ExactLen};
3use crate::combinators::mapped::spec::{BiMap, SpecMap};
4use crate::combinators::named::Named;
5use crate::combinators::reference::Ref;
6use crate::combinators::tail::{RepeatTillEnd, Tail};
7use crate::combinators::AsLen;
8use crate::combinators::Optional;
9use crate::combinators::OptionalEnd;
10use crate::combinators::{
11    Alt, Array, Bind, Choice, Cond, Const, Mapped, Opt, Pair, Preceded, PrefixTagged, Refined,
12    Repeat, RepeatN, Star, SuffixTagged, Sum, Terminated,
13};
14use crate::core::exec::fns::{FnByteLen, FnPrepare, FnSerializer, Map, MapRef, Pred};
15use crate::core::exec::input::InputBuf;
16use crate::core::exec::{ByteLen, OutputBuf, Parser, Prepare, Serializer};
17use crate::core::proof::Productive;
18use crate::core::spec::{
19    BytesCombinator, Consistency, SafeParser, SpecByteLen, SpecParser, SpecPred, SpecSerializer,
20    SpecSerializerDps,
21};
22#[cfg(feature = "alloc")]
23use alloc::vec::Vec;
24use vstd::prelude::*;
25
26verus! {
27
28// ----------------------------------------------------
29// Executable function adapters
30// ----------------------------------------------------
31
32/// Exposes the semantic specification bundled into an [`FnSerializer`] without requiring callers
33/// to unfold the adapter's individual trait implementations.
34pub proof fn lemma_fn_serializer_specs<Output, T, Spec, Exec>(
35    serializer: &FnSerializer<Output, T, Spec, Exec>,
36    value: T::V,
37) where
38    Output: OutputBuf,
39    T: DeepView + ?Sized,
40    Spec: SpecByteLen<T = T::V> + SpecSerializer<SVal = T::V> + Consistency<Val = T::V>,
41    Exec: Fn(&T, &mut Output),
42
43    ensures
44        serializer.consistent(value) == serializer.spec_fn@.consistent(value),
45        serializer.byte_len(value) == serializer.spec_fn@.byte_len(value),
46        serializer.spec_serialize(value) == serializer.spec_fn@.spec_serialize(value),
47{
48}
49
50/// Connects an executable serializer callback, through the Rust reference adapter, directly to
51/// its bundled ghost serializer.
52pub proof fn lemma_ref_fn_serializer_congruence<Output, T, Spec, Exec>(
53    serializer: &FnSerializer<Output, T, Spec, Exec>,
54) where
55    Output: OutputBuf,
56    T: DeepView + ?Sized,
57    Spec: SpecByteLen<T = T::V> + SpecSerializer<SVal = T::V> + Consistency<Val = T::V>,
58    Exec: Fn(&T, &mut Output),
59
60    ensures
61        crate::combinators::congruence::serializer_congruent(serializer, serializer.spec_fn@),
62{
63    use crate::combinators::congruence::*;
64
65    assert forall|value: T::V| #[trigger]
66        serializer.consistent(value) == serializer.spec_fn@.consistent(value) by {
67        lemma_fn_serializer_specs(serializer, value);
68    }
69    assert forall|value: T::V| #[trigger]
70        serializer.byte_len(value) == serializer.spec_fn@.byte_len(value) by {
71        lemma_fn_serializer_specs(serializer, value);
72    }
73    assert forall|value: T::V| #[trigger]
74        serializer.spec_serialize(value) == serializer.spec_fn@.spec_serialize(value) by {
75        lemma_fn_serializer_specs(serializer, value);
76    }
77    lemma_prepare_congruent_intro(serializer, serializer.spec_fn@);
78    lemma_serializer_congruent_intro(serializer, serializer.spec_fn@);
79}
80
81/// Exposes the consistency and byte-length specification bundled into an [`FnPrepare`].
82pub proof fn lemma_fn_prepare_specs<T, Spec, Exec>(
83    prepare: &FnPrepare<T, Spec, Exec>,
84    value: T::V,
85) where
86    T: DeepView + ?Sized,
87    Spec: SpecByteLen<T = T::V> + Consistency<Val = T::V>,
88    Exec: Fn(&T) -> Result<usize, crate::core::exec::PreSerializeError>,
89
90    ensures
91        prepare.consistent(value) == prepare.spec_fn@.consistent(value),
92        prepare.byte_len(value) == prepare.spec_fn@.byte_len(value),
93{
94}
95
96/// Connects an executable preparation callback, through the Rust reference adapter, directly to
97/// its bundled ghost preparation specification.
98pub proof fn lemma_ref_fn_prepare_congruence<T, Spec, Exec>(
99    prepare: &FnPrepare<T, Spec, Exec>,
100) where
101    T: DeepView + ?Sized,
102    Spec: SpecByteLen<T = T::V> + Consistency<Val = T::V>,
103    Exec: Fn(&T) -> Result<usize, crate::core::exec::PreSerializeError>,
104
105    ensures
106        crate::combinators::congruence::prepare_congruent(prepare, prepare.spec_fn@),
107{
108    use crate::combinators::congruence::*;
109
110    assert forall|value: T::V| #[trigger]
111        prepare.consistent(value) == prepare.spec_fn@.consistent(value) by {
112        lemma_fn_prepare_specs(prepare, value);
113    }
114    assert forall|value: T::V| #[trigger]
115        prepare.byte_len(value) == prepare.spec_fn@.byte_len(value) by {
116        lemma_fn_prepare_specs(prepare, value);
117    }
118    lemma_prepare_congruent_intro(prepare, prepare.spec_fn@);
119}
120
121/// Exposes the byte-length and consistency specification bundled into an [`FnByteLen`].
122pub proof fn lemma_fn_byte_len_specs<T, Spec, Exec>(
123    length: &FnByteLen<T, Spec, Exec>,
124    value: T::V,
125) where
126    T: DeepView + ?Sized,
127    Spec: SpecByteLen<T = T::V> + Consistency<Val = T::V>,
128    Exec: Fn(&T) -> usize,
129
130    ensures
131        length.consistent(value) == length.spec_fn@.consistent(value),
132        length.byte_len(value) == length.spec_fn@.byte_len(value),
133{
134}
135
136/// Relates a referenced executable byte-length callback to its bundled ghost specification.
137pub proof fn lemma_ref_fn_byte_len_congruence<T, Spec, Exec>(
138    length: &FnByteLen<T, Spec, Exec>,
139) where
140    T: DeepView + ?Sized,
141    Spec: SpecByteLen<T = T::V> + Consistency<Val = T::V>,
142    Exec: Fn(&T) -> usize,
143
144    ensures
145        crate::combinators::congruence::prepare_congruent(length, length.spec_fn@),
146{
147    use crate::combinators::congruence::*;
148
149    assert forall|value: T::V| #[trigger]
150        length.consistent(value) == length.spec_fn@.consistent(value) by {
151        lemma_fn_byte_len_specs(length, value);
152    }
153    assert forall|value: T::V| #[trigger]
154        length.byte_len(value) == length.spec_fn@.byte_len(value) by {
155        lemma_fn_byte_len_specs(length, value);
156    }
157    lemma_prepare_congruent_intro(length, length.spec_fn@);
158}
159
160// ----------------------------------------------------
161// ExactLen
162// ----------------------------------------------------
163pub proof fn lemma_exact_len_parser_exec_inv<I, Len, Inner>(fmt: &ExactLen<Inner, Len>) where
164    I: InputBuf,
165    Len: AsLen,
166    Inner: Parser<I> + SafeParser,
167
168    ensures
169        fmt.1.exec_inv() && fmt.1.safe_inv() ==> fmt.exec_inv() && fmt.safe_inv(),
170{
171}
172
173pub proof fn lemma_exact_len_serializer_exec_inv<Output, Inner, Len, T>(
174    fmt: &ExactLen<Inner, Len>,
175) where
176    Output: OutputBuf,
177    Len: AsLen,
178    Inner: Serializer<Output, T> + SpecByteLen<T = T::V>,
179    T: DeepView + ?Sized,
180
181    ensures
182        fmt.1.exec_inv() ==> fmt.exec_inv(),
183{
184}
185
186pub proof fn lemma_exact_len_prepare_exec_inv<Inner, Len, T>(fmt: &ExactLen<Inner, Len>) where
187    Len: AsLen,
188    Inner: Prepare<T>,
189    T: DeepView + ?Sized,
190
191    ensures
192        fmt.1.exec_inv() ==> fmt.exec_inv(),
193{
194}
195
196// ----------------------------------------------------
197// AndThen
198// ----------------------------------------------------
199pub proof fn lemma_and_then_parser_exec_inv<I, TailType, Then>(fmt: &AndThen<TailType, Then>) where
200    I: InputBuf,
201    TailType: Parser<I, PT = I, PVal = Seq<u8>>,
202    Then: Parser<I>,
203
204    ensures
205        fmt.0.exec_inv() && fmt.1.exec_inv() ==> fmt.exec_inv(),
206{
207}
208
209pub proof fn lemma_and_then_serializer_exec_inv<Output, Then, T>(fmt: &AndThen<Tail, Then>) where
210    Output: OutputBuf,
211    Then: Serializer<Output, T>,
212    T: DeepView + ?Sized,
213
214    ensures
215        fmt.1.exec_inv() ==> fmt.exec_inv(),
216{
217}
218
219pub proof fn lemma_and_then_prepare_exec_inv<Then, T>(fmt: &AndThen<Tail, Then>) where
220    Then: Prepare<T>,
221    T: DeepView + ?Sized,
222
223    ensures
224        fmt.1.exec_inv() ==> fmt.exec_inv(),
225{
226}
227
228// ----------------------------------------------------
229// Mapped
230// ----------------------------------------------------
231pub proof fn lemma_mapped_parser_exec_inv<I, Inner, M, MRev>(
232    fmt: &Mapped<Inner, BiMap<M, MRev>>,
233) where
234    I: View<V = Seq<u8>>,
235    Inner: Parser<I>,
236    M: Map<Inner::PT, Input = Inner::PVal>,
237    MRev: SpecMap<Input = M::Output, Output = M::Input>,
238
239    ensures
240        fmt.inner.exec_inv() ==> fmt.exec_inv(),
241{
242}
243
244pub proof fn lemma_mapped_serializer_exec_inv<Output, Inner, M, MRev, T, InnerT>(
245    fmt: &Mapped<Inner, BiMap<M, MRev>>,
246) where
247    Output: OutputBuf,
248    Inner: Serializer<Output, InnerT>,
249    T: DeepView,
250    InnerT: DeepView,
251    M: SpecMap<Input = Inner::T, Output = T::V>,
252    MRev: for <'x>Map<&'x T, O = InnerT, Input = T::V, Output = Inner::T>,
253
254    ensures
255        fmt.inner.exec_inv() ==> fmt.exec_inv(),
256{
257}
258
259pub proof fn lemma_mapped_prepare_exec_inv<Inner, M, MRev, T, InnerT>(
260    fmt: &Mapped<Inner, BiMap<M, MRev>>,
261) where
262    Inner: Prepare<InnerT>,
263    T: DeepView,
264    InnerT: DeepView,
265    M: SpecMap<Input = Inner::T, Output = T::V>,
266    MRev: for <'x>Map<&'x T, O = InnerT, Input = T::V, Output = Inner::T>,
267
268    ensures
269        fmt.inner.exec_inv() ==> fmt.exec_inv(),
270{
271}
272
273// ----------------------------------------------------
274// Refined
275// ----------------------------------------------------
276pub proof fn lemma_refined_parser_exec_inv<I, A, PredFn>(fmt: &Refined<A, PredFn>) where
277    I: View<V = Seq<u8>>,
278    A: Parser<I>,
279    PredFn: Pred<A::PT>,
280
281    ensures
282        fmt.0.exec_inv() ==> fmt.exec_inv(),
283{
284}
285
286pub proof fn lemma_refined_serializer_exec_inv<Output, A, PredFn, T>(
287    fmt: &Refined<A, PredFn>,
288) where Output: OutputBuf, A: Serializer<Output, T>, PredFn: SpecPred<T::V>, T: DeepView
289    ensures
290        fmt.0.exec_inv() ==> fmt.exec_inv(),
291{
292}
293
294pub proof fn lemma_refined_prepare_exec_inv<A, PredFn, T>(fmt: &Refined<A, PredFn>) where
295    A: Prepare<T>,
296    PredFn: Pred<T>,
297    T: DeepView,
298
299    ensures
300        fmt.0.exec_inv() ==> fmt.exec_inv(),
301{
302}
303
304// ----------------------------------------------------
305// Const
306// ----------------------------------------------------
307pub proof fn lemma_const_parser_exec_inv<I, Inner, T>(fmt: &Const<Inner, T>) where
308    I: InputBuf,
309    Inner: Parser<I, PT = T, PVal = T> + Prepare<T>,
310    T: DeepView<V = T> + PartialEq + Structural,
311
312    ensures
313        (Parser::<I>::exec_inv(&fmt.0) && (forall|v: T| v.deep_view() == v)) ==> Parser::<
314            I,
315        >::exec_inv(fmt),
316{
317}
318
319pub proof fn lemma_const_serializer_exec_inv<Output, Inner, T>(fmt: &Const<Inner, T>) where
320    Output: OutputBuf,
321    Inner: Serializer<Output, T>,
322    T: DeepView<V = T>,
323
324    ensures
325        fmt.0.exec_inv() ==> fmt.exec_inv(),
326{
327}
328
329pub proof fn lemma_const_prepare_exec_inv<Inner, T>(fmt: &Const<Inner, T>) where
330    Inner: Prepare<T>,
331    T: DeepView<V = T> + PartialEq + Structural,
332
333    ensures
334        (fmt.0.exec_inv() && (forall|v: T| v.deep_view() == v)) ==> fmt.exec_inv(),
335{
336}
337
338// ----------------------------------------------------
339// Repeat
340// ----------------------------------------------------
341#[cfg(feature = "alloc")]
342pub proof fn lemma_repeat_parser_exec_inv<I, A, B>(fmt: &Repeat<A, B>) where
343    I: InputBuf,
344    A: Parser<I> + SafeParser + Productive + Copy,
345    B: Parser<I> + SafeParser + Copy,
346
347    ensures
348        (fmt.0.exec_inv() && fmt.0.safe_inv() && fmt.0.productive_inv() && fmt.1.exec_inv()
349            && fmt.1.safe_inv()) ==> (fmt.exec_inv() && fmt.safe_inv()),
350{
351}
352
353// ----------------------------------------------------
354// RepeatTillEnd
355// ----------------------------------------------------
356#[cfg(feature = "alloc")]
357pub proof fn lemma_repeat_till_end_parser_exec_inv<I, A>(fmt: &RepeatTillEnd<A>) where
358    I: InputBuf,
359    A: Parser<I> + SafeParser + Productive + Copy,
360
361    ensures
362        (fmt.0.exec_inv() && fmt.0.safe_inv() && fmt.0.productive_inv()) ==> (fmt.exec_inv()
363            && fmt.safe_inv()),
364{
365}
366
367// ----------------------------------------------------
368// Cond
369// ----------------------------------------------------
370pub proof fn lemma_cond_parser_exec_inv<I, Inner>(fmt: &Cond<Inner>) where
371    I: View<V = Seq<u8>>,
372    Inner: Parser<I>,
373
374    ensures
375        fmt.1.exec_inv() ==> fmt.exec_inv(),
376{
377}
378
379pub proof fn lemma_cond_serializer_exec_inv<Output, Inner, T>(fmt: &Cond<Inner>) where
380    Output: OutputBuf,
381    Inner: Serializer<Output, T>,
382    T: DeepView,
383
384    ensures
385        fmt.1.exec_inv() ==> fmt.exec_inv(),
386{
387}
388
389pub proof fn lemma_cond_prepare_exec_inv<Inner, T>(fmt: &Cond<Inner>) where
390    Inner: Prepare<T>,
391    T: DeepView,
392
393    ensures
394        fmt.1.exec_inv() ==> fmt.exec_inv(),
395{
396}
397
398// ----------------------------------------------------
399// Choice
400// ----------------------------------------------------
401pub proof fn lemma_choice_parser_exec_inv<I, A, B>(fmt: &Choice<A, B>) where
402    I: View<V = Seq<u8>>,
403    A: Parser<I>,
404    B: Parser<I>,
405
406    ensures
407        (fmt.0.exec_inv() && fmt.1.exec_inv()) ==> fmt.exec_inv(),
408{
409}
410
411pub proof fn lemma_choice_serializer_exec_inv<Output, A, B, TA, TB>(fmt: &Choice<A, B>) where
412    Output: OutputBuf,
413    TA: DeepView,
414    TB: DeepView,
415    A: Serializer<Output, TA>,
416    B: Serializer<Output, TB>,
417
418    ensures
419        (fmt.0.exec_inv() && fmt.1.exec_inv()) ==> fmt.exec_inv(),
420{
421}
422
423pub proof fn lemma_choice_prepare_exec_inv<A, B, TA, TB>(fmt: &Choice<A, B>) where
424    TA: DeepView,
425    TB: DeepView,
426    A: Prepare<TA>,
427    B: Prepare<TB>,
428
429    ensures
430        (fmt.0.exec_inv() && fmt.1.exec_inv()) ==> fmt.exec_inv(),
431{
432}
433
434// ----------------------------------------------------
435// Alt
436// ----------------------------------------------------
437pub proof fn lemma_alt_parser_exec_inv<const NONDETERMINISTIC: bool, I, A, B>(
438    fmt: &Alt<A, B, NONDETERMINISTIC>,
439) where I: View<V = Seq<u8>>, A: Parser<I>, B: Parser<I, PVal = A::PVal, PT = A::PT>
440    ensures
441        (fmt.0.exec_inv() && fmt.1.exec_inv()) ==> fmt.exec_inv(),
442{
443}
444
445// ----------------------------------------------------
446// Sum
447// ----------------------------------------------------
448pub proof fn lemma_sum_inl_parser_exec_inv<I, A, B>(a: A) where
449    I: View<V = Seq<u8>>,
450    A: Parser<I>,
451    B: Parser<I>,
452
453    ensures
454        a.exec_inv() ==> (&Sum::<A, B>::Inl(a)).exec_inv(),
455{
456}
457
458pub proof fn lemma_sum_inr_parser_exec_inv<I, A, B>(b: B) where
459    I: View<V = Seq<u8>>,
460    A: Parser<I>,
461    B: Parser<I>,
462
463    ensures
464        b.exec_inv() ==> (&Sum::<A, B>::Inr(b)).exec_inv(),
465{
466}
467
468pub proof fn lemma_sum_inl_serializer_exec_inv<Output, A, B, TA, TB>(a: A) where
469    Output: OutputBuf,
470    TA: DeepView,
471    TB: DeepView,
472    A: Serializer<Output, TA>,
473    B: Serializer<Output, TB>,
474
475    ensures
476        a.exec_inv() ==> (&Sum::<A, B>::Inl(a)).exec_inv(),
477{
478}
479
480pub proof fn lemma_sum_inr_serializer_exec_inv<Output, A, B, TA, TB>(b: B) where
481    Output: OutputBuf,
482    TA: DeepView,
483    TB: DeepView,
484    A: Serializer<Output, TA>,
485    B: Serializer<Output, TB>,
486
487    ensures
488        b.exec_inv() ==> (&Sum::<A, B>::Inr(b)).exec_inv(),
489{
490}
491
492pub proof fn lemma_sum_inl_prepare_exec_inv<A, B, TA, TB>(a: A) where
493    TA: DeepView,
494    TB: DeepView,
495    A: Prepare<TA>,
496    B: Prepare<TB>,
497
498    ensures
499        a.exec_inv() ==> (&Sum::<A, B>::Inl(a)).exec_inv(),
500{
501}
502
503pub proof fn lemma_sum_inr_prepare_exec_inv<A, B, TA, TB>(b: B) where
504    TA: DeepView,
505    TB: DeepView,
506    A: Prepare<TA>,
507    B: Prepare<TB>,
508
509    ensures
510        b.exec_inv() ==> (&Sum::<A, B>::Inr(b)).exec_inv(),
511{
512}
513
514// ----------------------------------------------------
515// Opt
516// ----------------------------------------------------
517pub proof fn lemma_opt_parser_exec_inv<I, A>(fmt: &Opt<A>) where I: View<V = Seq<u8>>, A: Parser<I>
518    ensures
519        fmt.0.exec_inv() ==> fmt.exec_inv(),
520{
521}
522
523pub proof fn lemma_opt_serializer_exec_inv<Output, A, T>(fmt: &Opt<A>) where
524    Output: OutputBuf,
525    A: Serializer<Output, T>,
526    T: DeepView,
527
528    ensures
529        fmt.0.exec_inv() ==> fmt.exec_inv(),
530{
531}
532
533pub proof fn lemma_opt_prepare_exec_inv<A, T>(fmt: &Opt<A>) where A: Prepare<T>, T: DeepView
534    ensures
535        fmt.0.exec_inv() ==> fmt.exec_inv(),
536{
537}
538
539// ----------------------------------------------------
540// Optional
541// ----------------------------------------------------
542pub proof fn lemma_optional_parser_exec_inv<I, A, B>(fmt: &Optional<A, B>) where
543    I: InputBuf,
544    A: Parser<I> + SafeParser,
545    B: Parser<I> + SafeParser,
546
547    ensures
548        (fmt.0.exec_inv() && fmt.0.safe_inv() && fmt.1.exec_inv() && fmt.1.safe_inv())
549            ==> fmt.exec_inv(),
550{
551}
552
553pub proof fn lemma_optional_serializer_exec_inv<Output, A, B, TA, TB>(fmt: &Optional<A, B>) where
554    Output: OutputBuf,
555    TA: DeepView,
556    TB: DeepView,
557    A: Serializer<Output, TA>,
558    B: Serializer<Output, TB>,
559
560    ensures
561        (fmt.0.exec_inv() && fmt.1.exec_inv()) ==> fmt.exec_inv(),
562{
563}
564
565pub proof fn lemma_optional_prepare_exec_inv<A, B, TA, TB>(fmt: &Optional<A, B>) where
566    TA: DeepView,
567    TB: DeepView,
568    A: Prepare<TA>,
569    B: Prepare<TB>,
570
571    ensures
572        (fmt.0.exec_inv() && fmt.1.exec_inv()) ==> fmt.exec_inv(),
573{
574}
575
576// ----------------------------------------------------
577// OptionalEnd
578// ----------------------------------------------------
579pub proof fn lemma_optional_end_parser_exec_inv<I, A>(fmt: &OptionalEnd<A>) where
580    I: InputBuf,
581    A: Parser<I> + SafeParser,
582
583    ensures
584        (fmt.0.exec_inv() && fmt.0.safe_inv()) ==> fmt.exec_inv(),
585{
586}
587
588pub proof fn lemma_optional_end_serializer_exec_inv<Output, A, T>(fmt: &OptionalEnd<A>) where
589    Output: OutputBuf,
590    A: Serializer<Output, T>,
591    T: DeepView,
592
593    ensures
594        fmt.0.exec_inv() ==> fmt.exec_inv(),
595{
596}
597
598pub proof fn lemma_optional_end_prepare_exec_inv<A, T>(fmt: &OptionalEnd<A>) where
599    A: Prepare<T>,
600    T: DeepView,
601
602    ensures
603        fmt.0.exec_inv() ==> fmt.exec_inv(),
604{
605}
606
607// ----------------------------------------------------
608// Preceded
609// ----------------------------------------------------
610pub proof fn lemma_preceded_parser_exec_inv<I, A, B, AVal>(fmt: &Preceded<A, AVal, B, false>) where
611    I: InputBuf,
612    A: Parser<I, PT = AVal> + SafeParser<PVal = AVal>,
613    B: Parser<I> + SafeParser,
614    AVal: DeepView<V = AVal>,
615
616    ensures
617        (fmt.a.exec_inv() && fmt.a.safe_inv() && fmt.b.exec_inv() && fmt.b.safe_inv())
618            ==> fmt.exec_inv(),
619{
620}
621
622pub proof fn lemma_preceded_checked_parser_exec_inv<I, A, B, AVal>(
623    fmt: &Preceded<A, AVal, B, true>,
624) where
625    I: InputBuf,
626    A: Parser<I, PT = AVal> + SafeParser<PVal = AVal>,
627    B: Parser<I> + SafeParser,
628    AVal: DeepView<V = AVal> + PartialEq + Structural,
629
630    ensures
631        (fmt.a.exec_inv() && fmt.a.safe_inv() && fmt.b.exec_inv() && fmt.b.safe_inv() && (forall|
632            v: AVal,
633        |
634            v.deep_view() == v)) ==> fmt.exec_inv(),
635{
636}
637
638pub proof fn lemma_preceded_serializer_exec_inv<Output, A, B, AVal, T, const CHECK: bool>(
639    fmt: &Preceded<A, AVal, B, CHECK>,
640) where
641    Output: OutputBuf,
642    A: Serializer<Output, AVal>,
643    B: Serializer<Output, T>,
644    AVal: DeepView<V = AVal>,
645    T: DeepView,
646
647    ensures
648        (fmt.a.exec_inv() && fmt.b.exec_inv() && (forall|v: AVal| v.deep_view() == v))
649            ==> fmt.exec_inv(),
650{
651}
652
653pub proof fn lemma_preceded_prepare_exec_inv<A, B, AVal, T, const CHECK: bool>(
654    fmt: &Preceded<A, AVal, B, CHECK>,
655) where A: Prepare<AVal>, B: Prepare<T>, AVal: DeepView<V = AVal>, T: DeepView
656    ensures
657        (fmt.a.exec_inv() && fmt.b.exec_inv() && (forall|v: AVal| v.deep_view() == v))
658            ==> fmt.exec_inv(),
659{
660}
661
662// ----------------------------------------------------
663// Terminated
664// ----------------------------------------------------
665pub proof fn lemma_terminated_parser_exec_inv<I, A, B, BVal>(
666    fmt: &Terminated<A, B, BVal, false>,
667) where
668    I: InputBuf,
669    A: Parser<I> + SafeParser,
670    B: Parser<I, PT = BVal> + SafeParser<PVal = BVal>,
671    BVal: DeepView<V = BVal>,
672
673    ensures
674        (fmt.a.exec_inv() && fmt.a.safe_inv() && fmt.b.exec_inv() && fmt.b.safe_inv())
675            ==> fmt.exec_inv(),
676{
677}
678
679pub proof fn lemma_terminated_checked_parser_exec_inv<I, A, B, BVal>(
680    fmt: &Terminated<A, B, BVal, true>,
681) where
682    I: InputBuf,
683    A: Parser<I> + SafeParser,
684    B: Parser<I, PT = BVal> + SafeParser<PVal = BVal>,
685    BVal: DeepView<V = BVal> + PartialEq + Structural,
686
687    ensures
688        (fmt.a.exec_inv() && fmt.a.safe_inv() && fmt.b.exec_inv() && fmt.b.safe_inv() && (forall|
689            v: BVal,
690        |
691            v.deep_view() == v)) ==> fmt.exec_inv(),
692{
693}
694
695pub proof fn lemma_terminated_serializer_exec_inv<Output, A, B, BVal, T, const CHECK: bool>(
696    fmt: &Terminated<A, B, BVal, CHECK>,
697) where
698    Output: OutputBuf,
699    A: Serializer<Output, T>,
700    B: Serializer<Output, BVal>,
701    BVal: DeepView<V = BVal>,
702    T: DeepView,
703
704    ensures
705        (fmt.a.exec_inv() && fmt.b.exec_inv() && (forall|v: BVal| v.deep_view() == v))
706            ==> fmt.exec_inv(),
707{
708}
709
710pub proof fn lemma_terminated_prepare_exec_inv<A, B, BVal, T, const CHECK: bool>(
711    fmt: &Terminated<A, B, BVal, CHECK>,
712) where A: Prepare<T>, B: Prepare<BVal>, BVal: DeepView<V = BVal>, T: DeepView
713    ensures
714        (fmt.a.exec_inv() && fmt.b.exec_inv() && (forall|v: BVal| v.deep_view() == v))
715            ==> fmt.exec_inv(),
716{
717}
718
719// ----------------------------------------------------
720// PrefixTagged / SuffixTagged
721// ----------------------------------------------------
722pub proof fn lemma_prefix_tagged_parser_exec_inv<I, Tg, TagVal, Of>(
723    fmt: &PrefixTagged<Tg, TagVal, Of>,
724) where
725    I: InputBuf,
726    Tg: SpecByteLen<T = TagVal> + Parser<I, PT = TagVal, PVal = TagVal> + SafeParser,
727    TagVal: DeepView<V = TagVal> + PartialEq + Structural + Copy,
728    Of: Parser<I> + SafeParser,
729
730    ensures
731        (fmt.0.exec_inv() && fmt.0.safe_inv() && fmt.2.exec_inv() && fmt.2.safe_inv() && (forall|
732            v: TagVal,
733        |
734            v.deep_view() == v)) ==> fmt.exec_inv(),
735{
736}
737
738pub proof fn lemma_prefix_tagged_serializer_exec_inv<Output, Tg, TagVal, Of, T>(
739    fmt: &PrefixTagged<Tg, TagVal, Of>,
740) where
741    Output: OutputBuf,
742    Tg: SpecByteLen<T = TagVal> + Serializer<Output, TagVal>,
743    TagVal: DeepView<V = TagVal> + PartialEq + Structural + Copy,
744    Of: Serializer<Output, T>,
745    T: DeepView,
746
747    ensures
748        (fmt.0.exec_inv() && fmt.2.exec_inv() && (forall|v: TagVal| v.deep_view() == v))
749            ==> fmt.exec_inv(),
750{
751}
752
753pub proof fn lemma_prefix_tagged_prepare_exec_inv<Tg, TagVal, Of, T>(
754    fmt: &PrefixTagged<Tg, TagVal, Of>,
755) where
756    Tg: SpecByteLen<T = TagVal> + Prepare<TagVal>,
757    TagVal: DeepView<V = TagVal> + PartialEq + Structural + Copy,
758    Of: Prepare<T>,
759    T: DeepView,
760
761    ensures
762        (fmt.0.exec_inv() && fmt.2.exec_inv() && (forall|v: TagVal| v.deep_view() == v))
763            ==> fmt.exec_inv(),
764{
765}
766
767pub proof fn lemma_suffix_tagged_parser_exec_inv<I, Of, Tg, TagVal>(
768    fmt: &SuffixTagged<Of, Tg, TagVal>,
769) where
770    I: InputBuf,
771    Tg: SpecByteLen<T = TagVal> + Parser<I, PT = TagVal, PVal = TagVal> + SafeParser,
772    TagVal: DeepView<V = TagVal> + PartialEq + Structural + Copy,
773    Of: Parser<I> + SafeParser,
774
775    ensures
776        (fmt.0.exec_inv() && fmt.0.safe_inv() && fmt.1.exec_inv() && fmt.1.safe_inv() && (forall|
777            v: TagVal,
778        |
779            v.deep_view() == v)) ==> fmt.exec_inv(),
780{
781}
782
783pub proof fn lemma_suffix_tagged_serializer_exec_inv<Output, Of, Tg, TagVal, T>(
784    fmt: &SuffixTagged<Of, Tg, TagVal>,
785) where
786    Output: OutputBuf,
787    Tg: SpecByteLen<T = TagVal> + Serializer<Output, TagVal>,
788    TagVal: DeepView<V = TagVal> + PartialEq + Structural + Copy,
789    Of: Serializer<Output, T>,
790    T: DeepView,
791
792    ensures
793        (fmt.0.exec_inv() && fmt.1.exec_inv() && (forall|v: TagVal| v.deep_view() == v))
794            ==> fmt.exec_inv(),
795{
796}
797
798pub proof fn lemma_suffix_tagged_prepare_exec_inv<Of, Tg, TagVal, T>(
799    fmt: &SuffixTagged<Of, Tg, TagVal>,
800) where
801    Tg: SpecByteLen<T = TagVal> + Prepare<TagVal>,
802    TagVal: DeepView<V = TagVal> + PartialEq + Structural + Copy,
803    Of: Prepare<T>,
804    T: DeepView,
805
806    ensures
807        (fmt.0.exec_inv() && fmt.1.exec_inv() && (forall|v: TagVal| v.deep_view() == v))
808            ==> fmt.exec_inv(),
809{
810}
811
812// ----------------------------------------------------
813// Pair
814// ----------------------------------------------------
815pub proof fn lemma_pair_parser_exec_inv<I, A, B>(fmt: &Pair<A, B>) where
816    I: InputBuf,
817    A: Parser<I> + SafeParser,
818    B: Parser<I> + SafeParser,
819
820    ensures
821        (fmt.0.exec_inv() && fmt.0.safe_inv() && fmt.1.exec_inv() && fmt.1.safe_inv())
822            ==> fmt.exec_inv(),
823{
824}
825
826pub proof fn lemma_pair_serializer_exec_inv<Output, A, B, TA, TB>(fmt: &Pair<A, B>) where
827    Output: OutputBuf,
828    TA: DeepView,
829    TB: DeepView,
830    A: Serializer<Output, TA>,
831    B: Serializer<Output, TB>,
832
833    ensures
834        (fmt.0.exec_inv() && fmt.1.exec_inv()) ==> fmt.exec_inv(),
835{
836}
837
838pub proof fn lemma_pair_prepare_exec_inv<A, B, TA, TB>(fmt: &Pair<A, B>) where
839    TA: DeepView,
840    TB: DeepView,
841    A: Prepare<TA>,
842    B: Prepare<TB>,
843
844    ensures
845        (fmt.0.exec_inv() && fmt.1.exec_inv()) ==> fmt.exec_inv(),
846{
847}
848
849// ----------------------------------------------------
850// Bind
851// ----------------------------------------------------
852pub proof fn lemma_bind_parser_exec_inv<I, A, B>(fmt: &Bind<A, B>) where
853    I: InputBuf,
854    A: Parser<I> + SafeParser,
855    B: MapRef<A::PT, Input = A::PVal>,
856    B::O: Parser<I> + SafeParser,
857
858    ensures
859        (fmt.0.exec_inv() && fmt.0.safe_inv() && (forall|pb: B::O| #[trigger]
860            pb.exec_inv() && pb.safe_inv())) ==> (#[trigger] fmt.exec_inv() && fmt.safe_inv()),
861{
862    if fmt.0.exec_inv() && fmt.0.safe_inv() && (forall|pb: B::O| #[trigger]
863        pb.exec_inv() && pb.safe_inv()) {
864        assert(Parser::<I>::exec_inv(fmt));
865        assert forall|key: A::PVal| #[trigger] fmt.1.spec_map(key).safe_inv() by {
866            let pb = fmt.1.spec_map(key);
867            assert(pb.exec_inv());
868            assert(pb.exec_inv());
869        };
870        assert(fmt.safe_inv());
871    }
872}
873
874pub proof fn lemma_bind_serializer_exec_inv<Output, A, B, TA, TB>(fmt: &Bind<A, B>) where
875    Output: OutputBuf,
876    TA: DeepView,
877    TB: DeepView,
878    A: Serializer<Output, TA>,
879    B::O: Serializer<Output, TB>,
880    B: MapRef<TA, Input = TA::V>,
881
882    ensures
883        (fmt.0.exec_inv() && (forall|pb: B::O| pb.exec_inv())) ==> fmt.exec_inv(),
884{
885}
886
887pub proof fn lemma_bind_prepare_exec_inv<A, B, TA, TB>(fmt: &Bind<A, B>) where
888    TA: DeepView,
889    TB: DeepView,
890    A: Prepare<TA>,
891    B::O: Prepare<TB>,
892    B: MapRef<TA, Input = TA::V>,
893
894    ensures
895        (fmt.0.exec_inv() && (forall|pb: B::O| pb.exec_inv())) ==> fmt.exec_inv(),
896{
897}
898
899// ----------------------------------------------------
900// Rust shared references
901// ----------------------------------------------------
902pub proof fn lemma_ref_parser_exec_inv<I, P>(parser: &P) where I: View<V = Seq<u8>>, P: Parser<I>
903    ensures
904        parser.exec_inv() ==> (&parser).exec_inv(),
905{
906}
907
908pub proof fn lemma_ref_serializer_exec_inv<Output, S, T>(serializer: &S) where
909    Output: OutputBuf,
910    S: Serializer<Output, T>,
911    T: DeepView + ?Sized,
912
913    ensures
914        serializer.exec_inv() ==> (&serializer).exec_inv(),
915{
916}
917
918pub proof fn lemma_ref_prepare_exec_inv<S, T>(serializer: &S) where
919    S: Prepare<T>,
920    T: DeepView + ?Sized,
921
922    ensures
923        serializer.exec_inv() ==> (&serializer).exec_inv(),
924{
925}
926
927pub proof fn lemma_ref_byte_len_exec_inv<S, T>(length: &S) where
928    S: ByteLen<T>,
929    T: DeepView + ?Sized,
930
931    ensures
932        length.exec_inv() ==> ByteLen::<T>::exec_inv(&length),
933{
934}
935
936pub proof fn lemma_pair_byte_len_exec_inv<A, B, TA, TB>(fmt: &Pair<A, B>) where
937    A: ByteLen<TA>,
938    B: ByteLen<TB>,
939    TA: DeepView,
940    TB: DeepView,
941
942    ensures
943        (ByteLen::<TA>::exec_inv(&fmt.0) && ByteLen::<TB>::exec_inv(&fmt.1)) ==>
944            ByteLen::<(TA, TB)>::exec_inv(fmt),
945{
946}
947
948pub proof fn lemma_repeat_n_byte_len_exec_inv<Inner, N, T>(fmt: &RepeatN<Inner, N>) where
949    Inner: ByteLen<T>,
950    N: AsLen,
951    T: DeepView,
952
953    ensures
954        ByteLen::<T>::exec_inv(&fmt.1) ==> ByteLen::<[T]>::exec_inv(fmt),
955{
956}
957
958// ----------------------------------------------------
959// Ref
960// ----------------------------------------------------
961pub proof fn lemma_reference_parser_exec_inv<I, Inner>(fmt: &Ref<Inner>) where
962    I: View<V = Seq<u8>>,
963    Inner: Parser<I>,
964
965    ensures
966        fmt.0.exec_inv() ==> fmt.exec_inv(),
967{
968}
969
970pub proof fn lemma_reference_serializer_exec_inv<Output, Inner, T>(fmt: &Ref<Inner>) where
971    Output: OutputBuf,
972    Inner: Serializer<Output, T>,
973    T: DeepView + ?Sized,
974
975    ensures
976        fmt.0.exec_inv() ==> fmt.exec_inv(),
977{
978}
979
980pub proof fn lemma_reference_prepare_exec_inv<Inner, T>(fmt: &Ref<Inner>) where
981    Inner: Prepare<T>,
982    T: DeepView + ?Sized,
983
984    ensures
985        fmt.0.exec_inv() ==> fmt.exec_inv(),
986{
987}
988
989// ----------------------------------------------------
990// Named
991// ----------------------------------------------------
992pub proof fn lemma_named_parser_exec_inv<I, Inner>(fmt: &Named<Inner>) where
993    I: View<V = Seq<u8>>,
994    Inner: Parser<I>,
995
996    ensures
997        fmt.1.exec_inv() ==> fmt.exec_inv(),
998{
999}
1000
1001pub proof fn lemma_named_serializer_exec_inv<Output, Inner, T>(fmt: &Named<Inner>) where
1002    Output: OutputBuf,
1003    Inner: Serializer<Output, T>,
1004    T: DeepView,
1005
1006    ensures
1007        fmt.1.exec_inv() ==> fmt.exec_inv(),
1008{
1009}
1010
1011pub proof fn lemma_named_prepare_exec_inv<Inner, T>(fmt: &Named<Inner>) where
1012    Inner: Prepare<T>,
1013    T: DeepView,
1014
1015    ensures
1016        fmt.1.exec_inv() ==> fmt.exec_inv(),
1017{
1018}
1019
1020// ----------------------------------------------------
1021// Star
1022// ----------------------------------------------------
1023#[cfg(feature = "alloc")]
1024pub proof fn lemma_star_parser_exec_inv<I, Inner>(fmt: &Star<Inner>) where
1025    I: InputBuf,
1026    Inner: Parser<I> + SafeParser + Productive + Copy,
1027
1028    ensures
1029        (fmt.0.exec_inv() && fmt.0.safe_inv() && fmt.0.productive_inv()) ==> (fmt.exec_inv()
1030            && fmt.safe_inv()),
1031{
1032}
1033
1034pub proof fn lemma_star_serializer_exec_inv<Output, Inner, T>(fmt: &Star<Inner>) where
1035    Output: OutputBuf,
1036    Inner: Serializer<Output, T>,
1037    T: DeepView,
1038
1039    ensures
1040        fmt.0.exec_inv() ==> fmt.exec_inv(),
1041{
1042}
1043
1044pub proof fn lemma_star_prepare_exec_inv<Inner, T>(fmt: &Star<Inner>) where
1045    Inner: Prepare<T>,
1046    T: DeepView,
1047
1048    ensures
1049        fmt.0.exec_inv() ==> fmt.exec_inv(),
1050{
1051}
1052
1053pub proof fn lemma_repeat_serializer_exec_inv<Output, A, B, TA, TB>(fmt: &Repeat<A, B>) where
1054    Output: OutputBuf,
1055    A: Serializer<Output, TA> + Copy,
1056    B: Serializer<Output, TB>,
1057    TA: DeepView,
1058    TB: DeepView,
1059
1060    ensures
1061        (fmt.0.exec_inv() && fmt.1.exec_inv()) ==> fmt.exec_inv(),
1062{
1063}
1064
1065pub proof fn lemma_repeat_prepare_exec_inv<A, B, TA, TB>(fmt: &Repeat<A, B>) where
1066    A: Prepare<TA> + Copy,
1067    B: Prepare<TB>,
1068    TA: DeepView,
1069    TB: DeepView,
1070
1071    ensures
1072        (fmt.0.exec_inv() && fmt.1.exec_inv()) ==> fmt.exec_inv(),
1073{
1074}
1075
1076pub proof fn lemma_repeat_till_end_slice_serializer_exec_inv<Output, A, T>(
1077    fmt: &RepeatTillEnd<A>,
1078) where Output: OutputBuf, A: Serializer<Output, T> + Copy, T: DeepView
1079    ensures
1080        fmt.0.exec_inv() ==> Serializer::<Output, &[T]>::exec_inv(fmt),
1081{
1082}
1083
1084pub proof fn lemma_repeat_till_end_slice_prepare_exec_inv<A, T>(fmt: &RepeatTillEnd<A>) where
1085    A: Prepare<T> + Copy,
1086    T: DeepView,
1087
1088    ensures
1089        fmt.0.exec_inv() ==> Prepare::<&[T]>::exec_inv(fmt),
1090{
1091}
1092
1093#[cfg(feature = "alloc")]
1094pub proof fn lemma_repeat_till_end_vec_serializer_exec_inv<Output, A, T>(
1095    fmt: &RepeatTillEnd<A>,
1096) where Output: OutputBuf, A: Serializer<Output, T> + Copy, T: DeepView
1097    ensures
1098        fmt.0.exec_inv() ==> Serializer::<Output, Vec<T>>::exec_inv(fmt),
1099{
1100}
1101
1102#[cfg(feature = "alloc")]
1103pub proof fn lemma_repeat_till_end_vec_prepare_exec_inv<A, T>(fmt: &RepeatTillEnd<A>) where
1104    A: Prepare<T> + Copy,
1105    T: DeepView,
1106
1107    ensures
1108        fmt.0.exec_inv() ==> Prepare::<Vec<T>>::exec_inv(fmt),
1109{
1110}
1111
1112// ----------------------------------------------------
1113// RepeatN
1114// ----------------------------------------------------
1115#[cfg(feature = "alloc")]
1116pub proof fn lemma_repeat_n_parser_exec_inv<I, Inner, N>(fmt: &RepeatN<Inner, N>) where
1117    I: InputBuf,
1118    Inner: Parser<I> + SafeParser,
1119    N: AsLen,
1120
1121    ensures
1122        (fmt.1.exec_inv() && fmt.1.safe_inv()) ==> (fmt.exec_inv()),
1123{
1124}
1125
1126pub proof fn lemma_repeat_n_serializer_exec_inv<Output, Inner, N, T>(fmt: &RepeatN<Inner, N>) where
1127    Output: OutputBuf,
1128    Inner: Serializer<Output, T>,
1129    N: AsLen,
1130    T: DeepView,
1131
1132    ensures
1133        fmt.1.exec_inv() ==> fmt.exec_inv(),
1134{
1135}
1136
1137pub proof fn lemma_repeat_n_prepare_exec_inv<Inner, N, T>(fmt: &RepeatN<Inner, N>) where
1138    Inner: Prepare<T>,
1139    N: AsLen,
1140    T: DeepView,
1141
1142    ensures
1143        fmt.1.exec_inv() ==> fmt.exec_inv(),
1144{
1145}
1146
1147// ----------------------------------------------------
1148// Array
1149// ----------------------------------------------------
1150pub proof fn lemma_array_parser_exec_inv<I, Inner, const N: usize>(fmt: &Array<N, Inner>) where
1151    I: InputBuf,
1152    Inner: Parser<I> + SafeParser,
1153
1154    ensures
1155        (fmt.0.exec_inv() && fmt.0.safe_inv()) ==> fmt.exec_inv(),
1156{
1157}
1158
1159pub proof fn lemma_array_serializer_exec_inv<Output, Inner, T, const N: usize>(
1160    fmt: &Array<N, Inner>,
1161) where Output: OutputBuf, Inner: Serializer<Output, T>, T: DeepView
1162    ensures
1163        fmt.0.exec_inv() ==> fmt.exec_inv(),
1164{
1165}
1166
1167pub proof fn lemma_array_prepare_exec_inv<Inner, T, const N: usize>(fmt: &Array<N, Inner>) where
1168    Inner: Prepare<T>,
1169    T: DeepView,
1170
1171    ensures
1172        fmt.0.exec_inv() ==> fmt.exec_inv(),
1173{
1174}
1175
1176} // verus!
vest_lib/core/exec/bridge_lemmas.rs

vest_lib/core/exec/
bridge_lemmas.rs
