vstd_extra/external/
bitvec.rs

1//! Verus specifications for the third-party `bitvec` crate, trusted as TCB from
2//! inspection of the `bitvec-1.0.1` source (`store.rs`, `order.rs`,
3//! `vec/{api,ops}.rs`, `slice/{api,ops}.rs`) and centralized here rather than beside
4//! an OSTD caller. `id-alloc` is currently the only consumer (`BitVec<u8, Lsb0>`).
5//!
6//! Contracts are admitted only for trusted primitive storage (`u8`, `u32`, `usize`,
7//! `u64` on 64-bit, with `Lsb0`). `BitStore` alone is insufficient: `Cell`, atomic,
8//! or alias-safe storage can mutate through a shared reference, and implementing the
9//! external traits grants no model guarantees. Contracts are therefore guarded by an
10//! uninterpreted model predicate assumed only for those instances; primitive storage
11//! has `Mem = Self` and `Unalias = Self` (its internal `Access`/`Alias` types are not
12//! admitted).
13//!
14//! The model is a `Seq<bool>`; the views below equate every executed `bitvec`
15//! operation to a `Seq` operation, so all reasoning in `id-alloc` stays at the
16//! `Seq<bool>` level.
17use crate::seq_extra::is_first_zero;
18use bitvec::{
19    order::{BitOrder, Lsb0},
20    slice::{BitSlice, BitSliceIndex},
21    store::BitStore,
22    vec::BitVec,
23};
24use core::ops::{Deref, DerefMut, Index, Range};
25use vstd::{prelude::*, std_specs::core::IndexSpec};
26
27macro_rules! bitvec_model_axiom {
28    ($name:ident, $t:ty) => {
29        ::vstd::prelude::verus! {
30            pub broadcast axiom fn $name()
31                ensures
32                    #[trigger] obeys_bitvec_model::<$t, Lsb0>(),
33            ;
34        }
35};
36}
37
38// Keep instances separate so pruning an unused type does not remove the others.
39bitvec_model_axiom!(axiom_u8_bitvec_model, u8);
40bitvec_model_axiom!(axiom_u32_bitvec_model, u32);
41bitvec_model_axiom!(axiom_usize_bitvec_model, usize);
42#[cfg(target_pointer_width = "64")]
43bitvec_model_axiom!(axiom_u64_bitvec_model, u64);
44
45verus! {
46
47/// Verus declaration for bitvec's default `Lsb0` bit order (a zero-sized marker).
48#[verifier::external_type_specification]
49#[verifier::external_body]
50pub struct ExLsb0(Lsb0);
51
52/// Type-level declaration only; this does not assume any `BitStore` semantics.
53#[verifier::external_trait_specification]
54pub trait ExBitStore: 'static + core::fmt::Debug {
55    type ExternalTraitSpecificationFor: bitvec::store::BitStore;
56}
57
58/// Type-level declaration only; this does not assume any `BitOrder` semantics.
59#[verifier::external_trait_specification]
60pub trait ExBitOrder: 'static {
61    type ExternalTraitSpecificationFor: bitvec::order::BitOrder;
62}
63
64/// Verus declaration for bitvec's `BitSliceIndex` trait. Only the associated types
65/// are surfaced; `id-alloc` uses the `Range<usize>` instance, whose `Immut` is a
66/// `&BitSlice`.
67#[verifier::external_trait_specification]
68pub trait ExBitSliceIndex<'a, T: BitStore, O: BitOrder> {
69    type ExternalTraitSpecificationFor: BitSliceIndex<'a, T, O>;
70
71    type Immut;
72
73    type Mut;
74}
75
76/// Opaque external wrapper for the owned bitmap type.
77#[verifier::external_type_specification]
78#[verifier::external_body]
79#[verifier::reject_recursive_types(T)]
80#[verifier::reject_recursive_types(O)]
81pub struct ExBitVec<T: BitStore, O: BitOrder>(BitVec<T, O>);
82
83/// Opaque external wrapper for the borrowed bit-slice type.
84#[verifier::external_type_specification]
85#[verifier::external_body]
86#[verifier::reject_recursive_types(T)]
87#[verifier::reject_recursive_types(O)]
88pub struct ExBitSlice<T: BitStore, O: BitOrder>(BitSlice<T, O>);
89
90/// The full bitmap, modelled as a sequence of booleans.
91pub uninterp spec fn bitvec_view<T: BitStore, O: BitOrder>(b: &BitVec<T, O>) -> Seq<bool>;
92
93/// The content of a borrowed bit-slice, modelled as a sequence of booleans.
94pub uninterp spec fn bitslice_view<T: BitStore, O: BitOrder>(b: &BitSlice<T, O>) -> Seq<bool>;
95
96/// Whether storage and order support the immutable sequence model. Only the
97/// concrete instances in `group_bitvec_models` are trusted below.
98pub uninterp spec fn obeys_bitvec_model<T: BitStore, O: BitOrder>() -> bool;
99
100/// The only index and `get` specializations covered by this bridge.
101pub uninterp spec fn obeys_bitslice_index_model<T: BitStore, O: BitOrder, Idx>() -> bool where
102    BitSlice<T, O>: Index<Idx>,
103;
104
105pub uninterp spec fn obeys_bitslice_get_model<'a, T: BitStore, O: BitOrder, I>() -> bool where
106    I: BitSliceIndex<'a, T, O>,
107;
108
109pub broadcast axiom fn axiom_usize_bitslice_index_model<T: BitStore, O: BitOrder>()
110    requires
111        obeys_bitvec_model::<T, O>(),
112    ensures
113        #[trigger] obeys_bitslice_index_model::<T, O, usize>(),
114;
115
116pub broadcast axiom fn axiom_range_bitslice_get_model<'a, T: BitStore, O: BitOrder>()
117    requires
118        obeys_bitvec_model::<T, O>(),
119    ensures
120        #[trigger] obeys_bitslice_get_model::<'a, T, O, Range<usize>>(),
121;
122
123pub broadcast group group_bitvec_models {
124    axiom_u8_bitvec_model,
125    axiom_u32_bitvec_model,
126    axiom_usize_bitvec_model,
127    axiom_usize_bitslice_index_model,
128    axiom_range_bitslice_get_model,
129    #[cfg(target_pointer_width = "64")]
130    axiom_u64_bitvec_model,
131}
132
133/// Derefs to a `BitSlice` over exactly the `BitVec`'s own bits.
134pub assume_specification<'a, T: BitStore, O: BitOrder>[ <BitVec<T, O> as Deref>::deref ](
135    bv: &'a BitVec<T, O>,
136) -> (ret: &'a <BitVec<T, O> as Deref>::Target)
137    ensures
138        obeys_bitvec_model::<T, O>() ==> bitslice_view(ret) == bitvec_view(bv),
139;
140
141/// A `BitVec` derefs mutably to a `BitSlice` over exactly its own bits; a mutation
142/// performed through the returned borrow is reflected in the `BitVec`'s final view.
143pub assume_specification<'a, T: BitStore, O: BitOrder>[ <BitVec<T, O> as DerefMut>::deref_mut ](
144    bv: &'a mut BitVec<T, O>,
145) -> (ret: &'a mut <BitVec<T, O> as Deref>::Target)
146    ensures
147        obeys_bitvec_model::<T, O>() ==> {
148            &&& bitslice_view(ret) == bitvec_view(old(bv))
149            &&& bitvec_view(final(bv)) == bitslice_view(final(ret))
150        },
151;
152
153/// Constructs an empty `BitVec` (length 0). The capacity hint is not modelled.
154/// Panics if `capacity` exceeds `BitSlice::<T, O>::MAX_BITS` (= `usize::MAX >> 3`);
155/// callers must keep `capacity` within that bound.
156pub assume_specification<T: BitStore, O: BitOrder>[ BitVec::<T, O>::with_capacity ](
157    capacity: usize,
158) -> (ret: BitVec<T, O>)
159    requires
160        obeys_bitvec_model::<T, O>(),
161        capacity <= usize::MAX / 8,
162    ensures
163        bitvec_view(&ret).len() == 0,
164;
165
166/// Resizes the `BitVec` to `new_len`, filling new positions with `value` and
167/// preserving existing bits up to the shorter length. Panics if `new_len` exceeds
168/// `BitSlice::<T, O>::MAX_BITS` (= `usize::MAX >> 3`).
169pub assume_specification<T: BitStore, O: BitOrder>[ BitVec::<T, O>::resize ](
170    bv: &mut BitVec<T, O>,
171    new_len: usize,
172    value: bool,
173)
174    requires
175        obeys_bitvec_model::<T, O>(),
176        new_len <= usize::MAX / 8,
177    ensures
178        bitvec_view(final(bv)).len() == new_len,
179        forall|i: int|
180            #![trigger bitvec_view(final(bv))[i]]
181            0 <= i < new_len ==> bitvec_view(final(bv))[i] == (if i < bitvec_view(old(bv)).len() {
182                bitvec_view(old(bv))[i]
183            } else {
184                value
185            }),
186;
187
188/// The number of bits.
189pub assume_specification<T: BitStore, O: BitOrder>[ BitVec::<T, O>::len ](
190    bv: &BitVec<T, O>,
191) -> usize
192    requires
193        obeys_bitvec_model::<T, O>(),
194    returns
195        bitvec_view(bv).len() as usize,
196;
197
198/// Reads a single bit (panics if `idx` is out of bounds); the `usize` result is
199/// related to the model by [`axiom_bitvec_index_usize`].
200pub uninterp spec fn bitvec_index_value<'a, T: BitStore, O: BitOrder, Idx>(
201    bv: &'a BitVec<T, O>,
202    idx: Idx,
203) -> &'a <BitVec<T, O> as Index<Idx>>::Output where BitSlice<T, O>: Index<Idx>;
204
205pub assume_specification<'a, T: BitStore, O: BitOrder, Idx>[ <BitVec<T, O> as Index<Idx>>::index ](
206    bv: &'a BitVec<T, O>,
207    idx: Idx,
208) -> (ret: &'a <BitVec<T, O> as Index<Idx>>::Output) where BitSlice<T, O>: Index<Idx>
209    ensures
210        obeys_bitvec_model::<T, O>() && obeys_bitslice_index_model::<T, O, Idx>() ==> ret
211            == bitvec_index_value(bv, idx),
212;
213
214/// The indexed `usize` bit equals the model value.
215pub broadcast axiom fn axiom_bitvec_index_usize<T: BitStore, O: BitOrder>(
216    bv: &BitVec<T, O>,
217    idx: usize,
218)
219    requires
220        obeys_bitvec_model::<T, O>(),
221    ensures
222        #![trigger bitvec_index_value(bv, idx)]
223        *bitvec_index_value(bv, idx) == bitvec_view(bv)[idx as int],
224;
225
226/// `BitVec`'s `Index` precondition (`index_req`): the index must be in `[0, len)`,
227/// the condition under which `BitVec::index` does not panic.
228pub broadcast axiom fn axiom_bitvec_index_req<T: BitStore, O: BitOrder>(bv: &BitVec<T, O>, i: usize)
229    requires
230        obeys_bitvec_model::<T, O>(),
231    ensures
232        #![trigger <BitVec<T, O> as IndexSpec<usize>>::index_req(bv, &i)]
233        <BitVec<T, O> as IndexSpec<usize>>::index_req(bv, &i) == (i < bitvec_view(bv).len()),
234;
235
236/// Bit length is bounded by `BitSlice::<T, O>::MAX_BITS` (= `usize::MAX >> 3`).
237pub broadcast axiom fn axiom_bitvec_len_bound<T: BitStore, O: BitOrder>(bv: &BitVec<T, O>)
238    requires
239        obeys_bitvec_model::<T, O>(),
240    ensures
241        #![trigger bitvec_view(bv)]
242        bitvec_view(bv).len() <= (usize::MAX as int) / 8,
243;
244
245/// Writes a single bit. Panics if `index` is out of bounds.
246pub assume_specification<T: BitStore, O: BitOrder>[ BitSlice::<T, O>::set ](
247    bv: &mut BitSlice<T, O>,
248    index: usize,
249    value: bool,
250)
251    requires
252        obeys_bitvec_model::<T, O>(),
253        index < bitslice_view(bv).len(),
254    ensures
255        bitslice_view(final(bv)) == bitslice_view(old(bv)).update(index as int, value),
256;
257
258/// Borrows a part of the bit-slice (`get` is generic over `I`); the `Range<usize>`
259/// result is related to a sub-range by [`axiom_bitslice_get_range`].
260pub uninterp spec fn bitslice_get_value<'a, T: BitStore, O: BitOrder, I: BitSliceIndex<'a, T, O>>(
261    bv: &BitSlice<T, O>,
262    idx: I,
263) -> Option<<I as BitSliceIndex<'a, T, O>>::Immut>;
264
265pub assume_specification<'a, T: BitStore, O: BitOrder, I: BitSliceIndex<'a, T, O>>[ BitSlice::<
266    T,
267    O,
268>::get ](bv: &'a BitSlice<T, O>, idx: I) -> Option<<I as BitSliceIndex<'a, T, O>>::Immut>
269    requires
270        obeys_bitvec_model::<T, O>(),
271        obeys_bitslice_get_model::<'a, T, O, I>(),
272    returns
273        bitslice_get_value(bv, idx),
274;
275
276/// For a `Range<usize>`, `get` returns `Some` of a bit-slice equal to the
277/// sub-range `bitslice_view(bv)[start..end]` when
278/// `0 <= start <= end <= bitslice_view(bv).len()`, and `None` otherwise.
279pub broadcast axiom fn axiom_bitslice_get_range<'a, T: BitStore, O: BitOrder>(
280    bv: &BitSlice<T, O>,
281    range: Range<usize>,
282)
283    requires
284        obeys_bitvec_model::<T, O>(),
285    ensures
286        #![trigger bitslice_get_value(bv, range)]
287        match bitslice_get_value(bv, range) {
288            Some(s) => {
289                &&& 0 <= range.start <= range.end <= bitslice_view(bv).len()
290                &&& bitslice_view(s) == bitslice_view(bv)[range.start..range.end]
291            },
292            None => !(0 <= range.start <= range.end <= bitslice_view(bv).len()),
293        },
294;
295
296/// The first index holding a `0` bit, counted from the start of the slice.
297pub assume_specification<T: BitStore, O: BitOrder>[ BitSlice::<T, O>::first_zero ](
298    bv: &BitSlice<T, O>,
299) -> (ret: Option<usize>)
300    requires
301        obeys_bitvec_model::<T, O>(),
302    ensures
303        match ret {
304            Some(j) => {
305                &&& is_first_zero(bitslice_view(bv), j as int)
306                &&& j < bitslice_view(bv).len()
307            },
308            None => forall|i: int|
309                #![trigger bitslice_view(bv)[i]]
310                0 <= i < bitslice_view(bv).len() ==> bitslice_view(bv)[i],
311        },
312;
313
314} // verus!
vstd_extra/external/bitvec.rs

vstd_extra/external/
bitvec.rs
