#![allow(unused_imports)] use super::arithmetic::power::*; use super::arithmetic::power2::*; use super::bits::*; use super::math::*; use super::prelude::*; use core::mem::MaybeUninit; verus! { /// Matches the conditions here: pub open spec fn valid_layout(size: usize, align: usize) -> bool { is_pow2(align as int) && size <= isize::MAX as int - (isize::MAX as int % align as int) } #[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")] pub uninterp spec fn is_sized() -> bool; pub uninterp spec fn size_of() -> nat; pub uninterp spec fn align_of() -> nat; // compiler wants &V instead of V -- complains about V not being Sized /// Spec for `size_of_val`: . pub uninterp spec fn spec_size_of_val(val: &V) -> nat; /// Spec for `align_of_val`: . pub uninterp spec fn spec_align_of_val(val: &V) -> nat; // Naturally, the size of any executable type is going to fit into a `usize`. // What I'm not sure of is whether it will be possible to "reason about" arbitrarily // big types _in ghost code_ without tripping one of rustc's checks. // // I think it could go like this: // - Have some polymorphic code that constructs a giant tuple and proves false // - Make sure the code doesn't get monomorphized by rustc // - To export the 'false' fact from the polymorphic code without monomorphizing, // use broadcast_forall. // // Therefore, we are NOT creating an axiom that `size_of` fits in usize. // However, we still give the guarantee that if you call `core::mem::size_of` // at runtime, then the resulting usize is correct. #[verifier::inline] pub open spec fn size_of_as_usize() -> usize recommends size_of::() as usize as int == size_of::(), { size_of::() as usize } #[verifier::inline] pub open spec fn align_of_as_usize() -> usize recommends align_of::() as usize as int == align_of::(), { align_of::() as usize } #[verifier::inline] pub open spec fn size_of_val_as_usize(val: &V) -> usize recommends spec_size_of_val::(val) as usize as int == spec_size_of_val::(val), { spec_size_of_val::(val) as usize } #[verifier::inline] pub open spec fn align_of_val_as_usize(val: &V) -> usize recommends spec_align_of_val::(val) as usize as int == spec_align_of_val::(val), { spec_align_of_val::(val) as usize } #[verifier::when_used_as_spec(size_of_as_usize)] pub assume_specification[ core::mem::size_of:: ]() -> (u: usize) ensures u as nat == size_of::(), opens_invariants none no_unwind ; #[verifier::when_used_as_spec(align_of_as_usize)] pub assume_specification[ core::mem::align_of:: ]() -> (u: usize) ensures u as nat == align_of::(), opens_invariants none no_unwind ; #[verifier::when_used_as_spec(size_of_val_as_usize)] pub assume_specification[ core::mem::size_of_val:: ](val: &V) -> (u: usize) ensures u as nat == spec_size_of_val::(val), opens_invariants none no_unwind ; #[verifier::when_used_as_spec(align_of_val_as_usize)] pub assume_specification[ core::mem::align_of_val:: ](val: &V) -> (u: usize) ensures u as nat == spec_align_of_val::(val), opens_invariants none no_unwind ; /// Lemma to learn that the (size, alignment) of a type is a valid "layout". /// See [`valid_layout`] for the exact conditions. /// /// Also exports that size is a multiple of alignment ([Reference](https://doc.rust-lang.org/reference/type-layout.html#r-layout.properties.size)). /// /// Note that, unusually for a lemma, this is an `exec`-mode function. (This is necessary to /// ensure that the types are really compilable, as ghost code can reason about "virtual" types /// that exceed these bounds.) Despite being `exec`-mode, it is a no-op. #[verifier::external_body] #[inline(always)] pub const exec fn layout_for_type_is_valid() ensures valid_layout(size_of::() as usize, align_of::() as usize), size_of::() as usize as nat == size_of::(), align_of::() as usize as nat == align_of::(), align_of::() != 0, size_of::() % align_of::() == 0, opens_invariants none no_unwind { } /// Lemma to learn that the (size, alignment) of a (possibly not Sized) value is a valid "layout". /// See [`valid_layout`] for the exact conditions. /// /// Also exports that size is a multiple of alignment ([Reference](https://doc.rust-lang.org/reference/type-layout.html#r-layout.properties.size)). /// /// Note that, unusually for a lemma, this is an `exec`-mode function. (This is necessary to /// ensure that the types are really compilable, as ghost code can reason about "virtual" types /// that exceed these bounds.) Despite being `exec`-mode, it is a no-op. #[allow(unused_variables)] #[verifier::external_body] #[inline(always)] pub const exec fn layout_for_val_is_valid(val: Tracked<&V>) ensures valid_layout(spec_size_of_val::(val@) as usize, spec_align_of_val::(val@) as usize), spec_size_of_val::(val@) as usize as nat == spec_size_of_val::(val@), spec_align_of_val::(val@) as usize as nat == spec_align_of_val::(val@), spec_align_of_val::(val@) != 0, spec_size_of_val::(val@) % spec_align_of_val::(val@) == 0, opens_invariants none no_unwind { } /// Size of primitives ([Reference](https://doc.rust-lang.org/reference/type-layout.html#r-layout.primitive)). /// /// Note that alignment may be platform specific; if you need to use alignment, use /// [Verus's global directive](https://verus-lang.github.io/verus/guide/reference-global.html). pub broadcast axiom fn layout_of_primitives() ensures #![trigger size_of::()] #![trigger size_of::()] #![trigger size_of::()] #![trigger size_of::()] #![trigger size_of::()] #![trigger size_of::()] #![trigger size_of::()] #![trigger size_of::()] #![trigger size_of::()] #![trigger size_of::()] #![trigger size_of::()] #![trigger size_of::()] size_of::() == 1, size_of::() == 4, size_of::() == size_of::() == 1, size_of::() == size_of::() == 2, size_of::() == size_of::() == 4, size_of::() == size_of::() == 8, size_of::() == size_of::() == 16, size_of::() == size_of::(), size_of::() * 8 == usize::BITS, ; /// Size and alignment of the unit tuple ([Reference](https://doc.rust-lang.org/reference/type-layout.html#r-layout.tuple.unit)). pub broadcast axiom fn layout_of_unit_tuple() ensures #![trigger size_of::<()>()] #![trigger align_of::<()>()] size_of::<()>() == 0, align_of::<()>() == 1, ; /// 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)). pub broadcast axiom fn layout_of_references_and_pointers() ensures #![trigger size_of::<*mut T>()] #![trigger size_of::<*const T>()] #![trigger size_of::<&T>()] #![trigger align_of::<*mut T>()] #![trigger align_of::<*const T>()] #![trigger align_of::<&T>()] size_of::<*mut T>() == size_of::<*const T>() == size_of::<&T>(), align_of::<*mut T>() == align_of::<*const T>() == align_of::<&T>(), ; /// Pointers to sized types have the same size and alignment as `usize` /// ([Reference](https://doc.rust-lang.org/reference/type-layout.html#r-layout.pointer.intro)). pub broadcast axiom fn layout_of_references_and_pointers_for_sized_types() ensures #![trigger size_of::<*mut T>()] #![trigger align_of::<*mut T>()] size_of::<*mut T>() == size_of::(), align_of::<*mut T>() == align_of::(), ; /// Pointers to unsized types have at least the size and alignment as pointers to sized types /// ([Reference](https://doc.rust-lang.org/reference/type-layout.html#r-layout.pointer.unsized)). pub broadcast axiom fn layout_of_references_and_pointers_for_unsized_types() ensures #![trigger size_of::<*mut T>()] #![trigger align_of::<*mut T>()] size_of::<*mut T>() >= size_of::(), align_of::<*mut T>() >= align_of::(), ; /// Slices have the same layout as the underlying type. /// ([Reference](https://doc.rust-lang.org/reference/type-layout.html#slice-layout)). pub broadcast axiom fn layout_of_slices(x: &[T]) ensures #![trigger spec_size_of_val::<[T]>(x)] #![trigger spec_align_of_val::<[T]>(x)] spec_align_of_val::<[T]>(x) == align_of::(), spec_size_of_val::<[T]>(x) == x@.len() * size_of::(), ; /// `str` has the same layout as `[u8]`, which has the same layout as `u8`. /// ([Reference](https://doc.rust-lang.org/reference/type-layout.html#str-layout)). pub broadcast axiom fn layout_of_str(x: &str) ensures #![trigger spec_align_of_val::(x)] #![trigger spec_size_of_val::(x)] // todo - how to specify spec_size_of_val::(x) in terms of the byte representation of x? spec_align_of_val::(x) == align_of::(), ; /// The size is a multiple of alignment and alignment is always a power of 2 /// ([reference](https://doc.rust-lang.org/reference/type-layout.html#r-layout.properties.size)). pub broadcast axiom fn align_properties() ensures #![trigger align_of::()] size_of::() % align_of::() == 0, is_pow2(align_of::() as int), ; /// The alignment is at least 1 /// ([reference](https://doc.rust-lang.org/reference/type-layout.html#r-layout.properties.size)). pub broadcast proof fn align_nonzero() ensures #![trigger align_of::()] align_of::() > 0, { broadcast use crate::vstd::arithmetic::power::lemma_pow_positive, align_properties; broadcast use crate::vstd::arithmetic::power2::is_pow2_equiv; } /// The alignment of `u8` is 1, per [type layout rules](https://doc.rust-lang.org/reference/type-layout.html). /// Note: This is not part of the alignment broadcast group due to proof time-out, /// so it must be imported directly as needed. pub broadcast proof fn align_of_u8() ensures #![trigger align_of::()] align_of::() == 1, { broadcast use { layout_of_primitives, align_properties, align_nonzero, crate::vstd::arithmetic::div_mod::lemma_mod_is_zero, }; } /// The size of a usize will always be a power of 2, /// since Verus assumes 32 or 64-bit architecture. pub proof fn usize_size_pow2() ensures is_pow2(size_of::() as int), { broadcast use super::group_vstd_default; reveal(is_pow2); assert(is_pow2(4)) by (compute); assert(is_pow2(8)) by (compute); } /// Relates the unsigned integer max values to their sizes and bits. pub proof fn unsigned_int_max_values() ensures (usize::MAX as nat) == pow2(usize::BITS as nat) - 1, (usize::MAX as nat) == pow(256, size_of::()) - 1, (u8::MAX as nat) == pow2(u8::BITS as nat) - 1, (u8::MAX as nat) == pow(256, size_of::()) - 1, (u16::MAX as nat) == pow2(u16::BITS as nat) - 1, (u16::MAX as nat) == pow(256, size_of::()) - 1, (u32::MAX as nat) == pow2(u32::BITS as nat) - 1, (u32::MAX as nat) == pow(256, size_of::()) - 1, (u64::MAX as nat) == pow2(u64::BITS as nat) - 1, (u64::MAX as nat) == pow(256, size_of::()) - 1, (u128::MAX as nat) == pow2(u128::BITS as nat) - 1, (u128::MAX as nat) == pow(256, size_of::()) - 1, { broadcast use layout_of_primitives; lemma_unsigned_int_max_is_pow2_minus_1(); reveal(pow); assert(pow(256, 1) == pow2(8)) by (compute); assert(pow(256, 2) == pow2(16)) by (compute); assert(pow(256, 4) == pow2(32)) by (compute); assert(pow(256, 8) == pow2(64)) by (compute); assert(pow(256, 16) == pow2(128)) by (compute); } /// Relates the signed integer min and max values to their sizes and bits. pub proof fn signed_int_min_max_values() ensures (isize::MAX as nat) == pow2((isize::BITS - 1) as nat) - 1, abs(isize::MIN as int) == pow2((isize::BITS - 1) as nat), (isize::MAX as nat) * 2 == pow(256, size_of::()) - 2, abs(isize::MIN as int) * 2 == pow(256, size_of::()), (i8::MAX as nat) == pow2((i8::BITS - 1) as nat) - 1, abs(i8::MIN as int) == pow2((i8::BITS - 1) as nat), (i8::MAX as nat) * 2 == pow(256, size_of::()) - 2, abs(i8::MIN as int) * 2 == pow(256, size_of::()), (i16::MAX as nat) == pow2((i16::BITS - 1) as nat) - 1, abs(i16::MIN as int) == pow2((i16::BITS - 1) as nat), (i16::MAX as nat) * 2 == pow(256, size_of::()) - 2, abs(i16::MIN as int) * 2 == pow(256, size_of::()), (i32::MAX as nat) == pow2((i32::BITS - 1) as nat) - 1, abs(i32::MIN as int) == pow2((i32::BITS - 1) as nat), (i32::MAX as nat) * 2 == pow(256, size_of::()) - 2, abs(i32::MIN as int) * 2 == pow(256, size_of::()), (i64::MAX as nat) == pow2((i64::BITS - 1) as nat) - 1, abs(i64::MIN as int) == pow2((i64::BITS - 1) as nat), (i64::MAX as nat) * 2 == pow(256, size_of::()) - 2, abs(i64::MIN as int) * 2 == pow(256, size_of::()), (i128::MAX as nat) == pow2((i128::BITS - 1) as nat) - 1, abs(i128::MIN as int) == pow2((i128::BITS - 1) as nat), (i128::MAX as nat) * 2 == pow(256, size_of::()) - 2, abs(i128::MIN as int) * 2 == pow(256, size_of::()), { broadcast use layout_of_primitives; reveal(pow); assert(0x80 == pow2(7)) by (compute); assert(0x8_000 == pow2(15)) by (compute); assert(0x80_000_000 == pow2(31)) by (compute); assert(0x8_000_000_000_000_000 == pow2(63)) by (compute); assert(0x80_000_000_000_000_000_000_000_000_000_000 == pow2(127)) by (compute); assert(pow(256, 1) == pow2(7) * 2) by (compute); assert(pow(256, 2) == pow2(15) * 2) by (compute); assert(pow(256, 4) == pow2(31) * 2) by (compute); assert(pow(256, 8) == pow2(63) * 2) by (compute); assert(pow(256, 16) == pow2(127) * 2) by (compute); } pub broadcast group group_align_properties { align_properties, align_nonzero, } /// [`MaybeUninit`](core::mem::MaybeUninit) has the same size and aligment as `T` /// ([Reference](https://doc.rust-lang.org/stable/std/mem/union.MaybeUninit.html#layout-1)). pub broadcast axiom fn layout_of_maybe_uninit() ensures #![trigger size_of::>()] #![trigger align_of::>()] size_of::>() == size_of::(), align_of::>() == align_of::(), ; pub broadcast group group_layout_axioms { layout_of_primitives, layout_of_unit_tuple, layout_of_references_and_pointers, layout_of_references_and_pointers_for_sized_types, layout_of_references_and_pointers_for_unsized_types, layout_of_slices, layout_of_str, layout_of_maybe_uninit, group_align_properties, } } // verus!