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#[verifier::external_body]
139#[inline(always)]
140pub const exec fn layout_for_val_is_valid<V: ?Sized>(val: Tracked<&V>)
141    ensures
142        valid_layout(spec_size_of_val::<V>(val@) as usize, spec_align_of_val::<V>(val@) as usize),
143        spec_size_of_val::<V>(val@) as usize as nat == spec_size_of_val::<V>(val@),
144        spec_align_of_val::<V>(val@) as usize as nat == spec_align_of_val::<V>(val@),
145        spec_align_of_val::<V>(val@) != 0,
146        spec_size_of_val::<V>(val@) % spec_align_of_val::<V>(val@) == 0,
147    opens_invariants none
148    no_unwind
149{
150}
151
152/// Size of primitives ([Reference](https://doc.rust-lang.org/reference/type-layout.html#r-layout.primitive)).
153///
154/// Note that alignment may be platform specific; if you need to use alignment, use
155/// [Verus's global directive](https://verus-lang.github.io/verus/guide/reference-global.html).
156pub broadcast axiom fn layout_of_primitives()
157    ensures
158        #![trigger size_of::<bool>()]
159        #![trigger size_of::<char>()]
160        #![trigger size_of::<u8>()]
161        #![trigger size_of::<i8>()]
162        #![trigger size_of::<u16>()]
163        #![trigger size_of::<i16>()]
164        #![trigger size_of::<u32>()]
165        #![trigger size_of::<i32>()]
166        #![trigger size_of::<u64>()]
167        #![trigger size_of::<i64>()]
168        #![trigger size_of::<usize>()]
169        #![trigger size_of::<isize>()]
170        size_of::<bool>() == 1,
171        size_of::<char>() == 4,
172        size_of::<u8>() == size_of::<i8>() == 1,
173        size_of::<u16>() == size_of::<i16>() == 2,
174        size_of::<u32>() == size_of::<i32>() == 4,
175        size_of::<u64>() == size_of::<i64>() == 8,
176        size_of::<u128>() == size_of::<i128>() == 16,
177        size_of::<usize>() == size_of::<isize>(),
178        size_of::<usize>() * 8 == usize::BITS,
179;
180
181/// Size and alignment of the unit tuple ([Reference](https://doc.rust-lang.org/reference/type-layout.html#r-layout.tuple.unit)).
182pub broadcast axiom fn layout_of_unit_tuple()
183    ensures
184        #![trigger size_of::<()>()]
185        #![trigger align_of::<()>()]
186        size_of::<()>() == 0,
187        align_of::<()>() == 1,
188;
189
190/// 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)).
191pub broadcast axiom fn layout_of_references_and_pointers<T: ?Sized>()
192    ensures
193        #![trigger size_of::<*mut T>()]
194        #![trigger size_of::<*const T>()]
195        #![trigger size_of::<&T>()]
196        #![trigger align_of::<*mut T>()]
197        #![trigger align_of::<*const T>()]
198        #![trigger align_of::<&T>()]
199        size_of::<*mut T>() == size_of::<*const T>() == size_of::<&T>(),
200        align_of::<*mut T>() == align_of::<*const T>() == align_of::<&T>(),
201;
202
203/// Pointers to sized types have the same size and alignment as `usize`
204/// ([Reference](https://doc.rust-lang.org/reference/type-layout.html#r-layout.pointer.intro)).
205pub broadcast axiom fn layout_of_references_and_pointers_for_sized_types<T: Sized>()
206    ensures
207        #![trigger size_of::<*mut T>()]
208        #![trigger align_of::<*mut T>()]
209        size_of::<*mut T>() == size_of::<usize>(),
210        align_of::<*mut T>() == align_of::<usize>(),
211;
212
213/// Pointers to unsized types have at least the size and alignment as pointers to sized types
214/// ([Reference](https://doc.rust-lang.org/reference/type-layout.html#r-layout.pointer.unsized)).
215pub broadcast axiom fn layout_of_references_and_pointers_for_unsized_types<T: ?Sized>()
216    ensures
217        #![trigger size_of::<*mut T>()]
218        #![trigger align_of::<*mut T>()]
219        size_of::<*mut T>() >= size_of::<usize>(),
220        align_of::<*mut T>() >= align_of::<usize>(),
221;
222
223/// Slices have the same layout as the underlying type.
224/// ([Reference](https://doc.rust-lang.org/reference/type-layout.html#slice-layout)).
225pub broadcast axiom fn layout_of_slices<T>(x: &[T])
226    ensures
227        #![trigger spec_size_of_val::<[T]>(x)]
228        #![trigger spec_align_of_val::<[T]>(x)]
229        spec_align_of_val::<[T]>(x) == align_of::<T>(),
230        spec_size_of_val::<[T]>(x) == x@.len() * size_of::<T>(),
231;
232
233/// `str` has the same layout as `[u8]`, which has the same layout as `u8`.
234/// ([Reference](https://doc.rust-lang.org/reference/type-layout.html#str-layout)).
235pub broadcast axiom fn layout_of_str(x: &str)
236    ensures
237        #![trigger spec_align_of_val::<str>(x)]
238        #![trigger spec_size_of_val::<str>(x)]
239        // todo - how to specify spec_size_of_val::<str>(x) in terms of the byte representation of x?
240        spec_align_of_val::<str>(x) == align_of::<u8>(),
241;
242
243/// The size is a multiple of alignment and alignment is always a power of 2
244/// ([reference](https://doc.rust-lang.org/reference/type-layout.html#r-layout.properties.size)).
245pub broadcast axiom fn align_properties<T>()
246    ensures
247        #![trigger align_of::<T>()]
248        size_of::<T>() % align_of::<T>() == 0,
249        is_pow2(align_of::<T>() as int),
250;
251
252/// The alignment is at least 1
253/// ([reference](https://doc.rust-lang.org/reference/type-layout.html#r-layout.properties.size)).
254pub broadcast proof fn align_nonzero<T>()
255    ensures
256        #![trigger align_of::<T>()]
257        align_of::<T>() > 0,
258{
259    broadcast use crate::vstd::arithmetic::power::lemma_pow_positive, align_properties;
260    broadcast use crate::vstd::arithmetic::power2::is_pow2_equiv;
261
262}
263
264/// The alignment of `u8` is 1, per [type layout rules](https://doc.rust-lang.org/reference/type-layout.html).
265/// Note: This is not part of the alignment broadcast group due to proof time-out,
266/// so it must be imported directly as needed.
267pub broadcast proof fn align_of_u8()
268    ensures
269        #![trigger size_of::<u8>()]
270        align_of::<u8>() == 1,
271{
272    broadcast use {
273        layout_of_primitives,
274        align_properties,
275        align_nonzero,
276        crate::vstd::arithmetic::div_mod::lemma_mod_is_zero,
277    };
278
279}
280
281/// The size of a usize will always be a power of 2,
282/// since Verus assumes 32 or 64-bit architecture.
283pub proof fn usize_size_pow2()
284    ensures
285        is_pow2(size_of::<usize>() as int),
286{
287    broadcast use super::group_vstd_default;
288
289    reveal(is_pow2);
290
291    assert(is_pow2(4)) by (compute);
292    assert(is_pow2(8)) by (compute);
293}
294
295/// Relates the unsigned integer max values to their sizes and bits.
296pub proof fn unsigned_int_max_values()
297    ensures
298        (usize::MAX as nat) == pow2(usize::BITS as nat) - 1,
299        (usize::MAX as nat) == pow(256, size_of::<usize>()) - 1,
300        (u8::MAX as nat) == pow2(u8::BITS as nat) - 1,
301        (u8::MAX as nat) == pow(256, size_of::<u8>()) - 1,
302        (u16::MAX as nat) == pow2(u16::BITS as nat) - 1,
303        (u16::MAX as nat) == pow(256, size_of::<u16>()) - 1,
304        (u32::MAX as nat) == pow2(u32::BITS as nat) - 1,
305        (u32::MAX as nat) == pow(256, size_of::<u32>()) - 1,
306        (u64::MAX as nat) == pow2(u64::BITS as nat) - 1,
307        (u64::MAX as nat) == pow(256, size_of::<u64>()) - 1,
308        (u128::MAX as nat) == pow2(u128::BITS as nat) - 1,
309        (u128::MAX as nat) == pow(256, size_of::<u128>()) - 1,
310{
311    broadcast use layout_of_primitives;
312
313    reveal(pow);
314    assert(0x100 == pow2(8)) by (compute);
315    assert(0x1_0000 == pow2(16)) by (compute);
316    assert(0x1_0000_0000 == pow2(32)) by (compute);
317    assert(0x1_0000_0000_0000_0000 == pow2(64)) by (compute);
318    assert(0x1_0000_0000_0000_0000_0000_0000_0000_0000 == pow2(128)) by (compute);
319    assert(pow(256, 1) == pow2(8)) by (compute);
320    assert(pow(256, 2) == pow2(16)) by (compute);
321    assert(pow(256, 4) == pow2(32)) by (compute);
322    assert(pow(256, 8) == pow2(64)) by (compute);
323    assert(pow(256, 16) == pow2(128)) by (compute);
324}
325
326/// Relates the signed integer min and max values to their sizes and bits.
327pub proof fn signed_int_min_max_values()
328    ensures
329        (isize::MAX as nat) == pow2((isize::BITS - 1) as nat) - 1,
330        abs(isize::MIN as int) == pow2((isize::BITS - 1) as nat),
331        (isize::MAX as nat) * 2 == pow(256, size_of::<isize>()) - 2,
332        abs(isize::MIN as int) * 2 == pow(256, size_of::<isize>()),
333        (i8::MAX as nat) == pow2((i8::BITS - 1) as nat) - 1,
334        abs(i8::MIN as int) == pow2((i8::BITS - 1) as nat),
335        (i8::MAX as nat) * 2 == pow(256, size_of::<i8>()) - 2,
336        abs(i8::MIN as int) * 2 == pow(256, size_of::<i8>()),
337        (i16::MAX as nat) == pow2((i16::BITS - 1) as nat) - 1,
338        abs(i16::MIN as int) == pow2((i16::BITS - 1) as nat),
339        (i16::MAX as nat) * 2 == pow(256, size_of::<i16>()) - 2,
340        abs(i16::MIN as int) * 2 == pow(256, size_of::<i16>()),
341        (i32::MAX as nat) == pow2((i32::BITS - 1) as nat) - 1,
342        abs(i32::MIN as int) == pow2((i32::BITS - 1) as nat),
343        (i32::MAX as nat) * 2 == pow(256, size_of::<i32>()) - 2,
344        abs(i32::MIN as int) * 2 == pow(256, size_of::<i32>()),
345        (i64::MAX as nat) == pow2((i64::BITS - 1) as nat) - 1,
346        abs(i64::MIN as int) == pow2((i64::BITS - 1) as nat),
347        (i64::MAX as nat) * 2 == pow(256, size_of::<i64>()) - 2,
348        abs(i64::MIN as int) * 2 == pow(256, size_of::<i64>()),
349        (i128::MAX as nat) == pow2((i128::BITS - 1) as nat) - 1,
350        abs(i128::MIN as int) == pow2((i128::BITS - 1) as nat),
351        (i128::MAX as nat) * 2 == pow(256, size_of::<i128>()) - 2,
352        abs(i128::MIN as int) * 2 == pow(256, size_of::<i128>()),
353{
354    broadcast use layout_of_primitives;
355
356    reveal(pow);
357    assert(0x80 == pow2(7)) by (compute);
358    assert(0x8_000 == pow2(15)) by (compute);
359    assert(0x80_000_000 == pow2(31)) by (compute);
360    assert(0x8_000_000_000_000_000 == pow2(63)) by (compute);
361    assert(0x80_000_000_000_000_000_000_000_000_000_000 == pow2(127)) by (compute);
362    assert(pow(256, 1) == pow2(7) * 2) by (compute);
363    assert(pow(256, 2) == pow2(15) * 2) by (compute);
364    assert(pow(256, 4) == pow2(31) * 2) by (compute);
365    assert(pow(256, 8) == pow2(63) * 2) by (compute);
366    assert(pow(256, 16) == pow2(127) * 2) by (compute);
367}
368
369pub broadcast group group_align_properties {
370    align_properties,
371    align_nonzero,
372}
373
374/// [`MaybeUninit<T>`](core::mem::MaybeUninit) has the same size and aligment as `T`
375/// ([Reference](https://doc.rust-lang.org/stable/std/mem/union.MaybeUninit.html#layout-1)).
376pub broadcast axiom fn layout_of_maybe_uninit<T: Sized>()
377    ensures
378        #![trigger size_of::<MaybeUninit<T>>()]
379        #![trigger align_of::<MaybeUninit<T>>()]
380        size_of::<MaybeUninit<T>>() == size_of::<T>(),
381        align_of::<MaybeUninit<T>>() == align_of::<T>(),
382;
383
384pub broadcast group group_layout_axioms {
385    layout_of_primitives,
386    layout_of_unit_tuple,
387    layout_of_references_and_pointers,
388    layout_of_references_and_pointers_for_sized_types,
389    layout_of_references_and_pointers_for_unsized_types,
390    layout_of_slices,
391    layout_of_str,
392    layout_of_maybe_uninit,
393    group_align_properties,
394}
395
396} // verus!
vstd/layout.rs

vstd/
layout.rs
