vest_lib/combinators/terminated/
proof.rs

1//! Correctness proofs for sequential formats discarding their suffix.
2use super::spec::*;
3use crate::{
4    combinators::Pair,
5    core::{proof::*, spec::*},
6};
7use vstd::prelude::*;
8
9verus! {
10
11impl<A, B, const CHECK: bool> SPRoundTripDps for super::Terminated<A, B, B::SValue, CHECK> where
12    A: SPRoundTripDps + NonTailFmt,
13    B: SPRoundTripDps,
14 {
15    open spec fn unambiguous(&self) -> bool {
16        Pair(self.a, self.b).unambiguous()
17    }
18
19    proof fn theorem_serialize_dps_parse_roundtrip(&self, v: Self::T, obuf: Seq<u8>) {
20        let fmt = terminated::<_, _, _, _, CHECK>(self.a, self.b, self.b_val);
21        fmt.theorem_serialize_dps_parse_roundtrip(v, obuf);
22    }
23}
24
25impl<A, B> NonMalleable for super::Terminated<A, B, B::PVal, true> where
26    A: SoundParser + NonMalleable,
27    B: SoundParser + NonMalleable,
28 {
29    open spec fn nonmal_inv(&self) -> bool {
30        &&& Pair(self.a, self.b).sound_inv()
31        &&& Pair(self.a, self.b).nonmal_inv()
32    }
33
34    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
35        let fmt = terminated::<_, _, _, _, true>(self.a, self.b, self.b_val);
36        fmt.lemma_parse_non_malleable(buf1, buf2);
37    }
38}
39
40impl<A, B> NonMalleable for super::Terminated<A, B, B::PVal, false> where
41    A: SoundParser + NonMalleable,
42    B: SoundParser + NonMalleable + AdmitsUniqueVal,
43 {
44    open spec fn nonmal_inv(&self) -> bool {
45        &&& Pair(self.a, self.b).sound_inv()
46        &&& Pair(self.a, self.b).nonmal_inv()
47    }
48
49    proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>) {
50        let pair = Pair(self.a, self.b);
51        if let Some((n1, v1)) = self.spec_parse(buf1) {
52            if let Some((n2, v2)) = self.spec_parse(buf2) {
53                if v1 == v2 {
54                    let (_m1, p1) = pair.spec_parse(buf1)->0;
55                    let (_m2, p2) = pair.spec_parse(buf2)->0;
56                    pair.lemma_parse_sound_value(buf1);
57                    pair.lemma_parse_sound_value(buf2);
58                    self.b.lemma_unique_consistent_val(p1.1, p2.1);
59                    pair.lemma_parse_non_malleable(buf1, buf2);
60                }
61            }
62        }
63    }
64}
65
66impl<A, B, const CHECK: bool> NoLookAhead for super::Terminated<A, B, B::PVal, CHECK> where
67    A: NoLookAhead,
68    B: NoLookAhead,
69 {
70    open spec fn no_lookahead_inv(&self) -> bool {
71        let fmt = terminated::<_, _, _, _, CHECK>(self.a, self.b, self.b_val);
72        fmt.no_lookahead_inv()
73    }
74
75    proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>) {
76        let fmt = terminated::<_, _, _, _, CHECK>(self.a, self.b, self.b_val);
77        fmt.lemma_no_lookahead(i1, i2);
78    }
79}
80
81impl<A, B> Productive for super::Terminated<A, B, B::PVal, true> where
82    A: Productive,
83    B: Productive,
84 {
85    open spec fn productive_inv(&self) -> bool {
86        terminated::<_, _, _, _, true>(self.a, self.b, self.b_val).productive_inv()
87    }
88
89    proof fn lemma_productive(&self, s: Seq<u8>) {
90        terminated::<_, _, _, _, true>(self.a, self.b, self.b_val).lemma_productive(s);
91    }
92}
93
94impl<A, B> Productive for super::Terminated<A, B, B::PVal, false> where
95    A: Productive,
96    B: Productive,
97 {
98    open spec fn productive_inv(&self) -> bool {
99        terminated::<_, _, _, _, false>(self.a, self.b, self.b_val).productive_inv()
100    }
101
102    proof fn lemma_productive(&self, s: Seq<u8>) {
103        terminated::<_, _, _, _, false>(self.a, self.b, self.b_val).lemma_productive(s);
104    }
105}
106
107impl<A, B, const CHECK: bool> EquivSerializersGeneral for super::Terminated<
108    A,
109    B,
110    B::SValue,
111    CHECK,
112> where A: EquivSerializersGeneral, B: EquivSerializersGeneral + Consistency<Val = B::SVal> {
113    open spec fn equiv_general_inv(&self) -> bool {
114        let fmt = terminated::<_, _, _, _, CHECK>(self.a, self.b, self.b_val);
115        fmt.equiv_general_inv()
116    }
117
118    proof fn lemma_serialize_equiv(&self, v: Self::SVal, obuf: Seq<u8>) {
119        let fmt = terminated::<_, _, _, _, CHECK>(self.a, self.b, self.b_val);
120        fmt.lemma_serialize_equiv(v, obuf);
121    }
122}
123
124impl<A, B, const CHECK: bool> EquivSerializers for super::Terminated<A, B, B::SValue, CHECK> where
125    A: EquivSerializersGeneral,
126    B: EquivSerializers + Consistency<Val = B::SVal>,
127 {
128    open spec fn equiv_inv(&self) -> bool {
129        let fmt = terminated::<_, _, _, _, CHECK>(self.a, self.b, self.b_val);
130        fmt.equiv_inv()
131    }
132
133    proof fn lemma_serialize_equiv_on_empty(&self, v: Self::SVal) {
134        let fmt = terminated::<_, _, _, _, CHECK>(self.a, self.b, self.b_val);
135        fmt.lemma_serialize_equiv_on_empty(v);
136    }
137}
138
139} // verus!
vest_lib/combinators/terminated/proof.rs

vest_lib/combinators/terminated/
proof.rs
