vest_lib/combinators/bits/
spec.rs

1//! Specification interfaces for byte-aligned bitfield formats.
2use crate::combinators::{mapped::spec::*, Mapped, Pair, Refined};
3use crate::core::{proof::*, spec::*};
4use vstd::prelude::*;
5
6verus! {
7
8pub open spec fn bits<Repr: SpecByteLen, Tuple, Nominal>(
9    repr: Repr,
10    unpack: spec_fn(Repr::T) -> Tuple,
11    pack: spec_fn(Tuple) -> Repr::T,
12    refinement: PredFnSpec<Tuple>,
13    ctor: spec_fn(Tuple) -> Nominal,
14    dtor: spec_fn(Nominal) -> Tuple,
15) -> Mapped<
16    Refined<Mapped<Repr, BiMapper<Repr::T, Tuple>>, PredFnSpec<Tuple>>,
17    BiMapper<Tuple, Nominal>,
18> {
19    Mapped {
20        inner: Refined(Mapped { inner: repr, mapper: BiMap(unpack, pack) }, refinement),
21        mapper: BiMap(ctor, dtor),
22    }
23}
24
25impl<Repr, Tuple, Nominal> SpecParser for super::Bits<Repr, Tuple, Nominal> where
26    Repr: SpecByteLen + SpecParser<PVal = Repr::T>,
27 {
28    type PVal = Nominal;
29
30    open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)> {
31        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
32        fmt.spec_parse(ibuf)
33    }
34}
35
36impl<Repr, Tuple, Nominal> SpecSerializerDps for super::Bits<Repr, Tuple, Nominal> where
37    Repr: SpecByteLen + SpecSerializerDps<SValue = Repr::T>,
38 {
39    type SValue = Nominal;
40
41    open spec fn spec_serialize_dps(&self, v: Self::SValue, obuf: Seq<u8>) -> Seq<u8> {
42        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
43        fmt.spec_serialize_dps(v, obuf)
44    }
45}
46
47impl<Repr, Tuple, Nominal> SpecSerializer for super::Bits<Repr, Tuple, Nominal> where
48    Repr: SpecByteLen + SpecSerializer<SVal = Repr::T>,
49 {
50    type SVal = Nominal;
51
52    open spec fn spec_serialize(&self, v: Self::SVal) -> Seq<u8> {
53        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
54        fmt.spec_serialize(v)
55    }
56}
57
58impl<Repr, Tuple, Nominal> Consistency for super::Bits<Repr, Tuple, Nominal> where
59    Repr: SpecByteLen + Consistency<Val = Repr::T>,
60 {
61    type Val = Nominal;
62
63    open spec fn consistent(&self, v: Self::Val) -> bool {
64        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
65        &&& fmt.consistent(v)
66        &&& (self.consistent)(v)
67    }
68}
69
70impl<Repr, Tuple, Nominal> SpecByteLen for super::Bits<Repr, Tuple, Nominal> where
71    Repr: SpecByteLen,
72 {
73    type T = Nominal;
74
75    open spec fn byte_len(&self, v: Self::T) -> nat {
76        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
77        fmt.byte_len(v)
78    }
79}
80
81impl<Repr, Tuple, Nominal> SafeParser for super::Bits<Repr, Tuple, Nominal> where
82    Repr: SpecByteLen + SafeParser<PVal = Repr::T>,
83 {
84    open spec fn safe_inv(&self) -> bool {
85        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
86        fmt.safe_inv()
87    }
88
89    proof fn lemma_parse_safe(&self, ibuf: Seq<u8>) {
90        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
91        assert(self.safe_inv() == fmt.safe_inv());
92        fmt.lemma_parse_safe(ibuf);
93    }
94}
95
96impl<Repr, Tuple, Nominal> SoundParser for super::Bits<Repr, Tuple, Nominal> where
97    Repr: SoundParser,
98 {
99    open spec fn sound_inv(&self) -> bool {
100        // &&& forall|ibuf| #[trigger]
101        //     fmt.spec_parse(ibuf) matches Some((_, v)) ==> (self.consistent)(v)
102        // &&& self.repr.sound_inv()
103        // &&& forall|packed: Repr::T| #[trigger]
104        //     self.repr.consistent(packed) ==> (self.pack)((self.unpack)(packed)) == packed
105        // &&& forall|t: Tuple| #[trigger]
106        //     ((self.refinement)(t)) && self.repr.consistent((self.pack)(t)) ==> (self.dtor)(
107        //         (self.ctor)(t),
108        //     ) == t
109        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
110        &&& fmt.sound_inv()
111        &&& forall|ibuf| #[trigger]
112            fmt.spec_parse(ibuf) matches Some((_, v)) ==> (self.consistent)(v)
113    }
114
115    proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>) {
116        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
117        fmt.lemma_parse_sound_consumption(ibuf);
118    }
119
120    proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>) {
121        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
122        fmt.lemma_parse_sound_value(ibuf);
123    }
124}
125
126impl<Repr, Tuple, Nominal> NonTailFmt for super::Bits<Repr, Tuple, Nominal> where Repr: NonTailFmt {
127    open spec fn serialize_dps_inv(&self) -> bool {
128        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
129        fmt.serialize_dps_inv()
130    }
131
132    proof fn lemma_serialize_dps_prepend(&self, v: Self::SValue, obuf: Seq<u8>) {
133        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
134        fmt.lemma_serialize_dps_prepend(v, obuf);
135    }
136
137    proof fn lemma_serialize_dps_len(&self, v: Self::SValue, obuf: Seq<u8>) {
138        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
139        fmt.lemma_serialize_dps_len(v, obuf);
140    }
141}
142
143impl<Repr, Tuple, Nominal> GoodSerializer for super::Bits<Repr, Tuple, Nominal> where
144    Repr: GoodSerializer,
145 {
146    open spec fn serialize_inv(&self) -> bool {
147        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
148        fmt.serialize_inv()
149    }
150
151    proof fn lemma_serialize_len(&self, v: Self::SVal) {
152        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
153        fmt.lemma_serialize_len(v);
154    }
155}
156
157impl<Repr, Tuple, Nominal> MinMaxByteLen for super::Bits<Repr, Tuple, Nominal> where
158    Repr: MinMaxByteLen,
159 {
160    open spec fn min(&self) -> nat {
161        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
162        fmt.min()
163    }
164
165    open spec fn max(&self) -> nat {
166        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
167        fmt.max()
168    }
169
170    proof fn lemma_min_max_byte_len(&self, v: Self::T) {
171        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
172        fmt.lemma_min_max_byte_len(v);
173    }
174}
175
176impl<Repr, Tuple, Nominal> StaticByteLen for super::Bits<Repr, Tuple, Nominal> where
177    Repr: StaticByteLen,
178 {
179    open spec fn static_byte_len() -> nat {
180        Repr::static_byte_len()
181    }
182
183    proof fn lemma_static_len_matches_byte_len(&self, v: Self::T) {
184        let fmt = bits(self.repr, self.unpack, self.pack, self.refinement, self.ctor, self.dtor);
185        fmt.lemma_static_len_matches_byte_len(v);
186    }
187}
188
189} // verus!
vest_lib/combinators/bits/spec.rs

vest_lib/combinators/bits/
spec.rs
