vest_lib/combinators/preceded/
spec.rs

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

vest_lib/combinators/preceded/
spec.rs
