vest_lib/combinators/terminated/
spec.rs

1//! Specification for sequential formats discarding their suffix.
2use crate::{
3    combinators::{mapped::spec::*, Mapped, Pair, Refined},
4    core::{proof::*, spec::*},
5};
6use vstd::prelude::*;
7
8verus! {
9
10pub open spec fn terminated<FmtA, FmtB, A, B, const CHECK: bool>(
11    a: FmtA,
12    b: FmtB,
13    b_val: B,
14) -> Mapped<Refined<Pair<FmtA, FmtB>, PredFnSpec<(A, B)>>, BiMapper<(A, B), A>> {
15    Mapped {
16        inner: Refined(
17            Pair(a, b),
18            |pair: (A, B)|
19                if CHECK {
20                    pair.1 == b_val
21                } else {
22                    true
23                },
24        ),
25        mapper: BiMap(|pair: (A, B)| pair.0, |a| (a, b_val)),
26    }
27}
28
29impl<A, B, const CHECK: bool> SpecParser for super::Terminated<A, B, B::PVal, CHECK> where
30    A: SpecParser,
31    B: SpecParser,
32 {
33    type PVal = A::PVal;
34
35    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
36        let fmt = terminated::<_, _, _, _, CHECK>(self.a, self.b, self.b_val);
37        fmt.spec_parse(ibuf)
38    }
39}
40
41impl<A, B, const CHECK: bool> SpecSerializerDps for super::Terminated<A, B, B::SValue, CHECK> where
42    A: SpecSerializerDps,
43    B: SpecSerializerDps,
44 {
45    type SValue = A::SValue;
46
47    open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
48        let fmt = terminated::<_, _, _, _, CHECK>(self.a, self.b, self.b_val);
49        fmt.spec_serialize_dps(v, obuf)
50    }
51}
52
53impl<A, B, const CHECK: bool> SpecSerializer for super::Terminated<A, B, B::SVal, CHECK> where
54    A: SpecSerializer,
55    B: SpecSerializer,
56 {
57    type SVal = A::SVal;
58
59    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
60        let fmt = terminated::<_, _, _, _, CHECK>(self.a, self.b, self.b_val);
61        fmt.spec_serialize(v)
62    }
63}
64
65impl<A, B, const CHECK: bool> Consistency for super::Terminated<A, B, B::Val, CHECK> where
66    A: Consistency,
67    B: Consistency,
68 {
69    type Val = A::Val;
70
71    open spec fn consistent(&self, v: Self::Val) -> bool {
72        let fmt = terminated::<_, _, _, _, CHECK>(self.a, self.b, self.b_val);
73        fmt.consistent(v)
74    }
75}
76
77impl<A, B, const CHECK: bool> SafeParser for super::Terminated<A, B, B::PVal, CHECK> where
78    A: SafeParser,
79    B: SafeParser,
80 {
81    open spec fn safe_inv(&self) -> bool {
82        let fmt = terminated::<_, _, _, _, CHECK>(self.a, self.b, self.b_val);
83        fmt.safe_inv()
84    }
85
86    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
87        let fmt = terminated::<_, _, _, _, CHECK>(self.a, self.b, self.b_val);
88        fmt.lemma_parse_safe(ibuf);
89    }
90}
91
92impl<A, B> SoundParser for super::Terminated<A, B, B::PVal, true> where
93    A: SoundParser,
94    B: SoundParser,
95 {
96    open spec fn sound_inv(&self) -> bool {
97        Pair(self.a, self.b).sound_inv()
98    }
99
100    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
101        let fmt = terminated::<_, _, _, _, true>(self.a, self.b, self.b_val);
102        fmt.lemma_parse_sound_consumption(ibuf);
103    }
104
105    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
106        let fmt = terminated::<_, _, _, _, true>(self.a, self.b, self.b_val);
107        fmt.lemma_parse_sound_value(ibuf);
108    }
109}
110
111impl<A, B> SoundParser for super::Terminated<A, B, B::PVal, false> where
112    A: SoundParser,
113    B: SoundParser + AdmitsUniqueVal,
114 {
115    open spec fn sound_inv(&self) -> bool {
116        &&& Pair(self.a, self.b).sound_inv()
117        &&& self.b.consistent(self.b_val)
118    }
119
120    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
121        let pair = Pair(self.a, self.b);
122        pair.lemma_parse_sound_consumption(ibuf);
123        pair.lemma_parse_sound_value(ibuf);
124        if let Some((n, va)) = self.spec_parse(ibuf) {
125            let (_m, p) = pair.spec_parse(ibuf)->0;
126            self.b.lemma_unique_consistent_val(self.b_val, p.1);
127        }
128    }
129
130    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
131        let pair = Pair(self.a, self.b);
132        pair.lemma_parse_sound_value(ibuf);
133    }
134}
135
136impl<A, B, const CHECK: bool> NonTailFmt for super::Terminated<A, B, B::SValue, CHECK> where
137    A: NonTailFmt,
138    B: NonTailFmt,
139 {
140    open spec fn serialize_dps_inv(&self) -> bool {
141        let fmt = terminated::<_, _, _, _, CHECK>(self.a, self.b, self.b_val);
142        fmt.serialize_dps_inv()
143    }
144
145    proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>) {
146        let fmt = terminated::<_, _, _, _, CHECK>(self.a, self.b, self.b_val);
147        fmt.lemma_serialize_dps_prepend(v, obuf);
148    }
149
150    proof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>) {
151        let fmt = terminated::<_, _, _, _, CHECK>(self.a, self.b, self.b_val);
152        fmt.lemma_serialize_dps_len(v, obuf);
153    }
154}
155
156impl<A, B, const CHECK: bool> GoodSerializer for super::Terminated<A, B, B::SVal, CHECK> where
157    A: GoodSerializer,
158    B: GoodSerializer,
159 {
160    open spec fn serialize_inv(&self) -> bool {
161        let fmt = terminated::<_, _, _, _, CHECK>(self.a, self.b, self.b_val);
162        fmt.serialize_inv()
163    }
164
165    proof fn lemma_serialize_len(&self, v: Self::SVal) {
166        let fmt = terminated::<_, _, _, _, CHECK>(self.a, self.b, self.b_val);
167        fmt.lemma_serialize_len(v);
168    }
169}
170
171impl<A, B, const CHECK: bool> SpecByteLen for super::Terminated<A, B, B::T, CHECK> where
172    A: SpecByteLen,
173    B: SpecByteLen,
174 {
175    type T = A::T;
176
177    open spec fn byte_len(&self, v: Self::T) -> nat {
178        let fmt = terminated::<_, _, _, _, CHECK>(self.a, self.b, self.b_val);
179        fmt.byte_len(v)
180    }
181}
182
183impl<A, B, const CHECK: bool> MinMaxByteLen for super::Terminated<A, B, B::T, CHECK> where
184    A: MinMaxByteLen,
185    B: MinMaxByteLen,
186 {
187    open spec fn min(&self) -> nat {
188        terminated::<_, _, _, _, CHECK>(self.a, self.b, self.b_val).min()
189    }
190
191    open spec fn max(&self) -> nat {
192        terminated::<_, _, _, _, CHECK>(self.a, self.b, self.b_val).max()
193    }
194
195    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
196        terminated::<_, _, _, _, CHECK>(self.a, self.b, self.b_val).lemma_min_max_byte_len(v);
197    }
198}
199
200impl<A, B, const CHECK: bool> StaticByteLen for super::Terminated<A, B, B::T, CHECK> where
201    A: StaticByteLen,
202    B: StaticByteLen,
203 {
204    open spec fn static_byte_len() -> nat {
205        <Pair<A, B> as StaticByteLen>::static_byte_len()
206    }
207
208    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
209        let fmt = terminated::<_, _, _, _, CHECK>(self.a, self.b, self.b_val);
210        fmt.lemma_static_len_matches_byte_len(v);
211    }
212}
213
214impl<A, B, const CHECK: bool> ValueByteLen for super::Terminated<A, B, B::T, CHECK> where
215    A: ValueByteLen,
216    B: StaticByteLen,
217 {
218    open spec fn value_byte_len(v: Self::T) -> nat {
219        A::value_byte_len(v) + B::static_byte_len()
220    }
221
222    proof fn lemma_value_len_matches_byte_len(&self, v: Self::T) {
223        assert(self.byte_len(v) == Pair(self.a, self.b).byte_len((v, self.b_val)));
224        self.a.lemma_value_len_matches_byte_len(v);
225        self.b.lemma_static_len_matches_byte_len(self.b_val);
226    }
227}
228
229} // verus!
vest_lib/combinators/terminated/spec.rs

vest_lib/combinators/terminated/
spec.rs
