vstd/
layout.rs

Help
1#![allow(unused_imports)]
2
3use super::prelude::*;
4
5verus! {
6
7// TODO add some means for Verus to calculate the size & alignment of types
8// TODO use a definition from a math library, once we have one.
9pub open spec fn is_power_2(n: int) -> bool
10    decreases n,
11{
12    if n <= 0 {
13        false
14    } else if n == 1 {
15        true
16    } else {
17        n % 2 == 0 && is_power_2(n / 2)
18    }
19}
20
21/// Matches the conditions here: <https://doc.rust-lang.org/stable/std/alloc/struct.Layout.html>
22pub open spec fn valid_layout(size: usize, align: usize) -> bool {
23    is_power_2(align as int) && size <= isize::MAX as int - (isize::MAX as int % align as int)
24}
25
26#[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>")]
27pub uninterp spec fn is_sized<V: ?Sized>() -> bool;
28
29pub uninterp spec fn size_of<V>() -> nat;
30
31pub uninterp spec fn align_of<V>() -> nat;
32
33// Naturally, the size of any executable type is going to fit into a `usize`.
34// What I'm not sure of is whether it will be possible to "reason about" arbitrarily
35// big types _in ghost code_ without tripping one of rustc's checks.
36//
37// I think it could go like this:
38//   - Have some polymorphic code that constructs a giant tuple and proves false
39//   - Make sure the code doesn't get monomorphized by rustc
40//   - To export the 'false' fact from the polymorphic code without monomorphizing,
41//     use broadcast_forall.
42//
43// Therefore, we are NOT creating an axiom that `size_of` fits in usize.
44// However, we still give the guarantee that if you call `core::mem::size_of`
45// at runtime, then the resulting usize is correct.
46#[verifier::inline]
47pub open spec fn size_of_as_usize<V>() -> usize
48    recommends
49        size_of::<V>() as usize as int == size_of::<V>(),
50{
51    size_of::<V>() as usize
52}
53
54#[verifier::inline]
55pub open spec fn align_of_as_usize<V>() -> usize
56    recommends
57        align_of::<V>() as usize as int == align_of::<V>(),
58{
59    align_of::<V>() as usize
60}
61
62#[verifier::when_used_as_spec(size_of_as_usize)]
63pub assume_specification<V>[ core::mem::size_of::<V> ]() -> (u: usize)
64    ensures
65        u as nat == size_of::<V>(),
66    opens_invariants none
67    no_unwind
68;
69
70#[verifier::when_used_as_spec(align_of_as_usize)]
71pub assume_specification<V>[ core::mem::align_of::<V> ]() -> (u: usize)
72    ensures
73        u as nat == align_of::<V>(),
74    opens_invariants none
75    no_unwind
76;
77
78/// Lemma to learn that the (size, alignment) of a type is a valid "layout".
79/// See [`valid_layout`] for the exact conditions.
80///
81/// Also exports that size is a multiple of alignment ([Reference](https://doc.rust-lang.org/reference/type-layout.html#r-layout.properties.size)).
82///
83/// Note that, unusually for a lemma, this is an `exec`-mode function. (This is necessary to
84/// ensure that the types are really compilable, as ghost code can reason about "virtual" types
85/// that exceed these bounds.) Despite being `exec`-mode, it is a no-op.
86#[verifier::external_body]
87#[inline(always)]
88pub exec fn layout_for_type_is_valid<V>()
89    ensures
90        valid_layout(size_of::<V>() as usize, align_of::<V>() as usize),
91        size_of::<V>() as usize as nat == size_of::<V>(),
92        align_of::<V>() as usize as nat == align_of::<V>(),
93        align_of::<V>() != 0,
94        size_of::<V>() % align_of::<V>() == 0,
95    opens_invariants none
96    no_unwind
97{
98}
99
100/// Size of primitives ([Reference](https://doc.rust-lang.org/reference/type-layout.html#r-layout.primitive)).
101///
102/// Note that alignment may be platform specific; if you need to use alignment, use
103/// [Verus's global directive](https://verus-lang.github.io/verus/guide/reference-global.html).
104pub broadcast axiom fn layout_of_primitives()
105    ensures
106        #![trigger size_of::<bool>()]
107        #![trigger size_of::<char>()]
108        #![trigger size_of::<u8>()]
109        #![trigger size_of::<i8>()]
110        #![trigger size_of::<u16>()]
111        #![trigger size_of::<i16>()]
112        #![trigger size_of::<u32>()]
113        #![trigger size_of::<i32>()]
114        #![trigger size_of::<u64>()]
115        #![trigger size_of::<i64>()]
116        #![trigger size_of::<usize>()]
117        #![trigger size_of::<isize>()]
118        size_of::<bool>() == 1,
119        size_of::<char>() == 4,
120        size_of::<u8>() == size_of::<i8>() == 1,
121        size_of::<u16>() == size_of::<i16>() == 2,
122        size_of::<u32>() == size_of::<i32>() == 4,
123        size_of::<u64>() == size_of::<i64>() == 8,
124        size_of::<u128>() == size_of::<i128>() == 16,
125        size_of::<usize>() == size_of::<isize>(),
126        size_of::<usize>() * 8 == usize::BITS,
127;
128
129/// Size and alignment of the unit tuple ([Reference](https://doc.rust-lang.org/reference/type-layout.html#r-layout.tuple.unit)).
130pub broadcast axiom fn layout_of_unit_tuple()
131    ensures
132        #![trigger size_of::<()>()]
133        #![trigger align_of::<()>()]
134        size_of::<()>() == 0,
135        align_of::<()>() == 1,
136;
137
138/// 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)).
139pub broadcast axiom fn layout_of_references_and_pointers<T: ?Sized>()
140    ensures
141        #![trigger size_of::<*mut T>()]
142        #![trigger size_of::<*const T>()]
143        #![trigger size_of::<&T>()]
144        #![trigger align_of::<*mut T>()]
145        #![trigger align_of::<*const T>()]
146        #![trigger align_of::<&T>()]
147        size_of::<*mut T>() == size_of::<*const T>() == size_of::<&T>(),
148        align_of::<*mut T>() == align_of::<*const T>() == align_of::<&T>(),
149;
150
151/// Pointers to sized types have the same size and alignment as usize
152/// ([Reference](https://doc.rust-lang.org/reference/type-layout.html#r-layout.pointer.intro)).
153pub broadcast axiom fn layout_of_references_and_pointers_for_sized_types<T: Sized>()
154    ensures
155        #![trigger size_of::<*mut T>()]
156        #![trigger align_of::<*mut T>()]
157        size_of::<*mut T>() == size_of::<usize>(),
158        align_of::<*mut T>() == align_of::<usize>(),
159;
160
161pub broadcast group group_layout_axioms {
162    layout_of_primitives,
163    layout_of_unit_tuple,
164    layout_of_references_and_pointers,
165    layout_of_references_and_pointers_for_sized_types,
166}
167
168} // verus!
vstd/layout.rs

vstd/
layout.rs
