vstd/
layout.rs

1#![allow(unused_imports)]
2
3use super::arithmetic::power::*;
4use super::arithmetic::power2::*;
5use super::bits::*;
6use super::math::*;
7use super::prelude::*;
8use core::mem::MaybeUninit;
9
10verus! {
11
12/// Matches the conditions here: <https://doc.rust-lang.org/stable/std/alloc/struct.Layout.html>
13pub open spec fn valid_layout(size: usize, align: usize) -> bool {
14    is_pow2(align as int) && size <= isize::MAX as int - (isize::MAX as int % align as int)
15}
16
17#[cfg_attr(not(verus_verify_core), deprecated = "is_sized is now defunct; lemmas that require V to be sized should now use the trait bound `V: Sized` instead of is_sized<V>")]
18pub uninterp spec fn is_sized<V: ?Sized>() -> bool;
19
20pub uninterp spec fn size_of<V>() -> nat;
21
22pub uninterp spec fn align_of<V>() -> nat;
23
24// compiler wants &V instead of V -- complains about V not being Sized
25/// Spec for `size_of_val`: <https://doc.rust-lang.org/std/mem/fn.size_of_val.html>.
26pub uninterp spec fn spec_size_of_val<V: ?Sized>(val: &V) -> nat;
27
28/// Spec for `align_of_val`: <https://doc.rust-lang.org/std/mem/fn.align_of_val.html>.
29pub uninterp spec fn spec_align_of_val<V: ?Sized>(val: &V) -> nat;
30
31// Naturally, the size of any executable type is going to fit into a `usize`.
32// What I'm not sure of is whether it will be possible to "reason about" arbitrarily
33// big types _in ghost code_ without tripping one of rustc's checks.
34//
35// I think it could go like this:
36//   - Have some polymorphic code that constructs a giant tuple and proves false
37//   - Make sure the code doesn't get monomorphized by rustc
38//   - To export the 'false' fact from the polymorphic code without monomorphizing,
39//     use broadcast_forall.
40//
41// Therefore, we are NOT creating an axiom that `size_of` fits in usize.
42// However, we still give the guarantee that if you call `core::mem::size_of`
43// at runtime, then the resulting usize is correct.
44#[verifier::inline]
45pub open spec fn size_of_as_usize<V>() -> usize
46    recommends
47        size_of::<V>() as usize as int == size_of::<V>(),
48{
49    size_of::<V>() as usize
50}
51
52#[verifier::inline]
53pub open spec fn align_of_as_usize<V>() -> usize
54    recommends
55        align_of::<V>() as usize as int == align_of::<V>(),
56{
57    align_of::<V>() as usize
58}
59
60#[verifier::inline]
61pub open spec fn size_of_val_as_usize<V: ?Sized>(val: &V) -> usize
62    recommends
63        spec_size_of_val::<V>(val) as usize as int == spec_size_of_val::<V>(val),
64{
65    spec_size_of_val::<V>(val) as usize
66}
67
68#[verifier::inline]
69pub open spec fn align_of_val_as_usize<V: ?Sized>(val: &V) -> usize
70    recommends
71        spec_align_of_val::<V>(val) as usize as int == spec_align_of_val::<V>(val),
72{
73    spec_align_of_val::<V>(val) as usize
74}
75
76#[verifier::when_used_as_spec(size_of_as_usize)]
77pub assume_specification<V>[ core::mem::size_of::<V> ]() -> (u: usize)
78    ensures
79        u as nat == size_of::<V>(),
80    opens_invariants none
81    no_unwind
82;
83
84#[verifier::when_used_as_spec(align_of_as_usize)]
85pub assume_specification<V>[ core::mem::align_of::<V> ]() -> (u: usize)
86    ensures
87        u as nat == align_of::<V>(),
88    opens_invariants none
89    no_unwind
90;
91
92#[verifier::when_used_as_spec(size_of_val_as_usize)]
93pub assume_specification<V: ?Sized>[ core::mem::size_of_val::<V> ](val: &V) -> (u: usize)
94    ensures
95        u as nat == spec_size_of_val::<V>(val),
96    opens_invariants none
97    no_unwind
98;
99
100#[verifier::when_used_as_spec(align_of_val_as_usize)]
101pub assume_specification<V: ?Sized>[ core::mem::align_of_val::<V> ](val: &V) -> (u: usize)
102    ensures
103        u as nat == spec_align_of_val::<V>(val),
104    opens_invariants none
105    no_unwind
106;
107
108/// Lemma to learn that the (size, alignment) of a type is a valid "layout".
109/// See [`valid_layout`] for the exact conditions.
110///
111/// Also exports that size is a multiple of alignment ([Reference](https://doc.rust-lang.org/reference/type-layout.html#r-layout.properties.size)).
112///
113/// Note that, unusually for a lemma, this is an `exec`-mode function. (This is necessary to
114/// ensure that the types are really compilable, as ghost code can reason about "virtual" types
115/// that exceed these bounds.) Despite being `exec`-mode, it is a no-op.
116#[verifier::external_body]
117#[inline(always)]
118pub const exec fn layout_for_type_is_valid<V>()
119    ensures
120        valid_layout(size_of::<V>() as usize, align_of::<V>() as usize),
121        size_of::<V>() as usize as nat == size_of::<V>(),
122        align_of::<V>() as usize as nat == align_of::<V>(),
123        align_of::<V>() != 0,
124        size_of::<V>() % align_of::<V>() == 0,
125    opens_invariants none
126    no_unwind
127{
128}
129
130/// Lemma to learn that the (size, alignment) of a (possibly not Sized) value is a valid "layout".
131/// See [`valid_layout`] for the exact conditions.
132///
133/// Also exports that size is a multiple of alignment ([Reference](https://doc.rust-lang.org/reference/type-layout.html#r-layout.properties.size)).
134///
135/// Note that, unusually for a lemma, this is an `exec`-mode function. (This is necessary to
136/// ensure that the types are really compilable, as ghost code can reason about "virtual" types
137/// that exceed these bounds.) Despite being `exec`-mode, it is a no-op.
138#[allow(unused_variables)]
139#[verifier::external_body]
140#[inline(always)]
141pub const exec fn layout_for_val_is_valid<V: ?Sized>(val: Tracked<&V>)
142    ensures
143        valid_layout(spec_size_of_val::<V>(val@) as usize, spec_align_of_val::<V>(val@) as usize),
144        spec_size_of_val::<V>(val@) as usize as nat == spec_size_of_val::<V>(val@),
145        spec_align_of_val::<V>(val@) as usize as nat == spec_align_of_val::<V>(val@),
146        spec_align_of_val::<V>(val@) != 0,
147        spec_size_of_val::<V>(val@) % spec_align_of_val::<V>(val@) == 0,
148    opens_invariants none
149    no_unwind
150{
151}
152
153/// Size of primitives ([Reference](https://doc.rust-lang.org/reference/type-layout.html#r-layout.primitive)).
154///
155/// Note that alignment may be platform specific; if you need to use alignment, use
156/// [Verus's global directive](https://verus-lang.github.io/verus/guide/reference-global.html).
157pub broadcast axiom fn layout_of_primitives()
158    ensures
159        #![trigger size_of::<bool>()]
160        #![trigger size_of::<char>()]
161        #![trigger size_of::<u8>()]
162        #![trigger size_of::<i8>()]
163        #![trigger size_of::<u16>()]
164        #![trigger size_of::<i16>()]
165        #![trigger size_of::<u32>()]
166        #![trigger size_of::<i32>()]
167        #![trigger size_of::<u64>()]
168        #![trigger size_of::<i64>()]
169        #![trigger size_of::<usize>()]
170        #![trigger size_of::<isize>()]
171        size_of::<bool>() == 1,
172        size_of::<char>() == 4,
173        size_of::<u8>() == size_of::<i8>() == 1,
174        size_of::<u16>() == size_of::<i16>() == 2,
175        size_of::<u32>() == size_of::<i32>() == 4,
176        size_of::<u64>() == size_of::<i64>() == 8,
177        size_of::<u128>() == size_of::<i128>() == 16,
178        size_of::<usize>() == size_of::<isize>(),
179        size_of::<usize>() * 8 == usize::BITS,
180;
181
182/// Size and alignment of the unit tuple ([Reference](https://doc.rust-lang.org/reference/type-layout.html#r-layout.tuple.unit)).
183pub broadcast axiom fn layout_of_unit_tuple()
184    ensures
185        #![trigger size_of::<()>()]
186        #![trigger align_of::<()>()]
187        size_of::<()>() == 0,
188        align_of::<()>() == 1,
189;
190
191/// Pointers and references have the same layout. Mutability of the pointer or reference does not change the layout ([Reference](https://doc.rust-lang.org/reference/type-layout.html#r-layout.pointer.intro)).
192pub broadcast axiom fn layout_of_references_and_pointers<T: ?Sized>()
193    ensures
194        #![trigger size_of::<*mut T>()]
195        #![trigger size_of::<*const T>()]
196        #![trigger size_of::<&T>()]
197        #![trigger align_of::<*mut T>()]
198        #![trigger align_of::<*const T>()]
199        #![trigger align_of::<&T>()]
200        size_of::<*mut T>() == size_of::<*const T>() == size_of::<&T>(),
201        align_of::<*mut T>() == align_of::<*const T>() == align_of::<&T>(),
202;
203
204/// Pointers to sized types have the same size and alignment as `usize`
205/// ([Reference](https://doc.rust-lang.org/reference/type-layout.html#r-layout.pointer.intro)).
206pub broadcast axiom fn layout_of_references_and_pointers_for_sized_types<T: Sized>()
207    ensures
208        #![trigger size_of::<*mut T>()]
209        #![trigger align_of::<*mut T>()]
210        size_of::<*mut T>() == size_of::<usize>(),
211        align_of::<*mut T>() == align_of::<usize>(),
212;
213
214/// Pointers to unsized types have at least the size and alignment as pointers to sized types
215/// ([Reference](https://doc.rust-lang.org/reference/type-layout.html#r-layout.pointer.unsized)).
216pub broadcast axiom fn layout_of_references_and_pointers_for_unsized_types<T: ?Sized>()
217    ensures
218        #![trigger size_of::<*mut T>()]
219        #![trigger align_of::<*mut T>()]
220        size_of::<*mut T>() >= size_of::<usize>(),
221        align_of::<*mut T>() >= align_of::<usize>(),
222;
223
224/// Slices have the same layout as the underlying type.
225/// ([Reference](https://doc.rust-lang.org/reference/type-layout.html#slice-layout)).
226pub broadcast axiom fn layout_of_slices<T>(x: &[T])
227    ensures
228        #![trigger spec_size_of_val::<[T]>(x)]
229        #![trigger spec_align_of_val::<[T]>(x)]
230        spec_align_of_val::<[T]>(x) == align_of::<T>(),
231        spec_size_of_val::<[T]>(x) == x@.len() * size_of::<T>(),
232;
233
234/// `str` has the same layout as `[u8]`, which has the same layout as `u8`.
235/// ([Reference](https://doc.rust-lang.org/reference/type-layout.html#str-layout)).
236pub broadcast axiom fn layout_of_str(x: &str)
237    ensures
238        #![trigger spec_align_of_val::<str>(x)]
239        #![trigger spec_size_of_val::<str>(x)]
240        // todo - how to specify spec_size_of_val::<str>(x) in terms of the byte representation of x?
241        spec_align_of_val::<str>(x) == align_of::<u8>(),
242;
243
244/// The size is a multiple of alignment and alignment is always a power of 2
245/// ([reference](https://doc.rust-lang.org/reference/type-layout.html#r-layout.properties.size)).
246pub broadcast axiom fn align_properties<T>()
247    ensures
248        #![trigger align_of::<T>()]
249        size_of::<T>() % align_of::<T>() == 0,
250        is_pow2(align_of::<T>() as int),
251;
252
253/// The alignment is at least 1
254/// ([reference](https://doc.rust-lang.org/reference/type-layout.html#r-layout.properties.size)).
255pub broadcast proof fn align_nonzero<T>()
256    ensures
257        #![trigger align_of::<T>()]
258        align_of::<T>() > 0,
259{
260    broadcast use crate::vstd::arithmetic::power::lemma_pow_positive, align_properties;
261    broadcast use crate::vstd::arithmetic::power2::is_pow2_equiv;
262
263}
264
265/// The alignment of `u8` is 1, per [type layout rules](https://doc.rust-lang.org/reference/type-layout.html).
266/// Note: This is not part of the alignment broadcast group due to proof time-out,
267/// so it must be imported directly as needed.
268pub broadcast proof fn align_of_u8()
269    ensures
270        #![trigger align_of::<u8>()]
271        align_of::<u8>() == 1,
272{
273    broadcast use {
274        layout_of_primitives,
275        align_properties,
276        align_nonzero,
277        crate::vstd::arithmetic::div_mod::lemma_mod_is_zero,
278    };
279
280}
281
282/// The size of a usize will always be a power of 2,
283/// since Verus assumes 32 or 64-bit architecture.
284pub proof fn usize_size_pow2()
285    ensures
286        is_pow2(size_of::<usize>() as int),
287{
288    broadcast use super::group_vstd_default;
289
290    reveal(is_pow2);
291
292    assert(is_pow2(4)) by (compute);
293    assert(is_pow2(8)) by (compute);
294}
295
296/// Relates the unsigned integer max values to their sizes and bits.
297pub proof fn unsigned_int_max_values()
298    ensures
299        (usize::MAX as nat) == pow2(usize::BITS as nat) - 1,
300        (usize::MAX as nat) == pow(256, size_of::<usize>()) - 1,
301        (u8::MAX as nat) == pow2(u8::BITS as nat) - 1,
302        (u8::MAX as nat) == pow(256, size_of::<u8>()) - 1,
303        (u16::MAX as nat) == pow2(u16::BITS as nat) - 1,
304        (u16::MAX as nat) == pow(256, size_of::<u16>()) - 1,
305        (u32::MAX as nat) == pow2(u32::BITS as nat) - 1,
306        (u32::MAX as nat) == pow(256, size_of::<u32>()) - 1,
307        (u64::MAX as nat) == pow2(u64::BITS as nat) - 1,
308        (u64::MAX as nat) == pow(256, size_of::<u64>()) - 1,
309        (u128::MAX as nat) == pow2(u128::BITS as nat) - 1,
310        (u128::MAX as nat) == pow(256, size_of::<u128>()) - 1,
311{
312    broadcast use layout_of_primitives;
313
314    reveal(pow);
315    assert(0x100 == pow2(8)) by (compute);
316    assert(0x1_0000 == pow2(16)) by (compute);
317    assert(0x1_0000_0000 == pow2(32)) by (compute);
318    assert(0x1_0000_0000_0000_0000 == pow2(64)) by (compute);
319    assert(0x1_0000_0000_0000_0000_0000_0000_0000_0000 == pow2(128)) by (compute);
320    assert(pow(256, 1) == pow2(8)) by (compute);
321    assert(pow(256, 2) == pow2(16)) by (compute);
322    assert(pow(256, 4) == pow2(32)) by (compute);
323    assert(pow(256, 8) == pow2(64)) by (compute);
324    assert(pow(256, 16) == pow2(128)) by (compute);
325}
326
327/// Relates the signed integer min and max values to their sizes and bits.
328pub proof fn signed_int_min_max_values()
329    ensures
330        (isize::MAX as nat) == pow2((isize::BITS - 1) as nat) - 1,
331        abs(isize::MIN as int) == pow2((isize::BITS - 1) as nat),
332        (isize::MAX as nat) * 2 == pow(256, size_of::<isize>()) - 2,
333        abs(isize::MIN as int) * 2 == pow(256, size_of::<isize>()),
334        (i8::MAX as nat) == pow2((i8::BITS - 1) as nat) - 1,
335        abs(i8::MIN as int) == pow2((i8::BITS - 1) as nat),
336        (i8::MAX as nat) * 2 == pow(256, size_of::<i8>()) - 2,
337        abs(i8::MIN as int) * 2 == pow(256, size_of::<i8>()),
338        (i16::MAX as nat) == pow2((i16::BITS - 1) as nat) - 1,
339        abs(i16::MIN as int) == pow2((i16::BITS - 1) as nat),
340        (i16::MAX as nat) * 2 == pow(256, size_of::<i16>()) - 2,
341        abs(i16::MIN as int) * 2 == pow(256, size_of::<i16>()),
342        (i32::MAX as nat) == pow2((i32::BITS - 1) as nat) - 1,
343        abs(i32::MIN as int) == pow2((i32::BITS - 1) as nat),
344        (i32::MAX as nat) * 2 == pow(256, size_of::<i32>()) - 2,
345        abs(i32::MIN as int) * 2 == pow(256, size_of::<i32>()),
346        (i64::MAX as nat) == pow2((i64::BITS - 1) as nat) - 1,
347        abs(i64::MIN as int) == pow2((i64::BITS - 1) as nat),
348        (i64::MAX as nat) * 2 == pow(256, size_of::<i64>()) - 2,
349        abs(i64::MIN as int) * 2 == pow(256, size_of::<i64>()),
350        (i128::MAX as nat) == pow2((i128::BITS - 1) as nat) - 1,
351        abs(i128::MIN as int) == pow2((i128::BITS - 1) as nat),
352        (i128::MAX as nat) * 2 == pow(256, size_of::<i128>()) - 2,
353        abs(i128::MIN as int) * 2 == pow(256, size_of::<i128>()),
354{
355    broadcast use layout_of_primitives;
356
357    reveal(pow);
358    assert(0x80 == pow2(7)) by (compute);
359    assert(0x8_000 == pow2(15)) by (compute);
360    assert(0x80_000_000 == pow2(31)) by (compute);
361    assert(0x8_000_000_000_000_000 == pow2(63)) by (compute);
362    assert(0x80_000_000_000_000_000_000_000_000_000_000 == pow2(127)) by (compute);
363    assert(pow(256, 1) == pow2(7) * 2) by (compute);
364    assert(pow(256, 2) == pow2(15) * 2) by (compute);
365    assert(pow(256, 4) == pow2(31) * 2) by (compute);
366    assert(pow(256, 8) == pow2(63) * 2) by (compute);
367    assert(pow(256, 16) == pow2(127) * 2) by (compute);
368}
369
370pub broadcast group group_align_properties {
371    align_properties,
372    align_nonzero,
373}
374
375/// [`MaybeUninit<T>`](core::mem::MaybeUninit) has the same size and aligment as `T`
376/// ([Reference](https://doc.rust-lang.org/stable/std/mem/union.MaybeUninit.html#layout-1)).
377pub broadcast axiom fn layout_of_maybe_uninit<T: Sized>()
378    ensures
379        #![trigger size_of::<MaybeUninit<T>>()]
380        #![trigger align_of::<MaybeUninit<T>>()]
381        size_of::<MaybeUninit<T>>() == size_of::<T>(),
382        align_of::<MaybeUninit<T>>() == align_of::<T>(),
383;
384
385pub broadcast group group_layout_axioms {
386    layout_of_primitives,
387    layout_of_unit_tuple,
388    layout_of_references_and_pointers,
389    layout_of_references_and_pointers_for_sized_types,
390    layout_of_references_and_pointers_for_unsized_types,
391    layout_of_slices,
392    layout_of_str,
393    layout_of_maybe_uninit,
394    group_align_properties,
395}
396
397} // verus!
vstd/layout.rs

vstd/
layout.rs
