ostd_pod/
lib.rs

1//! This crate defines a marker trait for plain old data (POD).
2#![no_std]
3
4use vstd::prelude::*;
5
6use core::mem::MaybeUninit;
7
8verus! {
9
10/// A marker trait for plain old data (POD).
11///
12/// A POD type `T:Pod` supports converting to and from arbitrary
13/// `mem::size_of::<T>()` bytes _safely_.
14/// For example, simple primitive types like `u8` and `i16`
15/// are POD types. But perhaps surprisingly, `bool` is not POD
16/// because Rust compiler makes implicit assumption that
17/// a byte of `bool` has a value of either `0` or `1`.
18/// Interpreting a byte of value `3` has a `bool` value has
19/// undefined behavior.
20///
21/// # Safety
22///
23/// Marking a non-POD type as POD may cause undefined behaviors.
24pub unsafe trait Pod: Copy + Sized {
25    /// Creates a new instance of Pod type that is filled with zeroes.
26    #[verifier::external_body]
27    fn new_zeroed() -> Self {
28        // SAFETY. An all-zero value of `T: Pod` is always valid.
29        unsafe { core::mem::zeroed() }
30    }
31
32    /// Creates a new instance of Pod type with uninitialized content.
33    #[verifier::external_body]
34    fn new_uninit() -> Self {
35        // SAFETY. A value of `T: Pod` can have arbitrary bits.
36        #[allow(clippy::uninit_assumed_init)]
37        unsafe { MaybeUninit::uninit().assume_init() }
38    }
39
40    /// Creates a new instance from the given bytes.
41    #[verus_spec(
42        requires
43            bytes@.len() >= core::mem::size_of::<Self>(),
44        returns
45            from_bytes_spec::<Self>(bytes@),
46    )]
47    fn from_bytes(bytes: &[u8]) -> Self {
48        let mut new_self = Self::new_uninit();
49        let copy_len = new_self.as_bytes().len();
50        new_self.as_bytes_mut().copy_from_slice(&bytes[..copy_len]);
51        proof {
52            assert(new_self == decode_pod::<Self>(bytes@[0..core::mem::size_of::<Self>()]));
53        }
54        new_self
55    }
56
57    /// As a slice of bytes.
58    #[verifier::external_body]
59    #[verus_spec(r =>
60        ensures
61            r.len() == core::mem::size_of::<Self>(),
62            r@ == pod_bytes(*self),
63    )]
64    fn as_bytes(&self) -> &[u8] {
65        let ptr = self as *const Self as *const u8;
66        let len = core::mem::size_of::<Self>();
67        unsafe { core::slice::from_raw_parts(ptr, len) }
68    }
69
70    /// As a mutable slice of bytes.
71    #[verifier::external_body]
72    #[verus_spec(r =>
73        ensures
74            r.len() == core::mem::size_of::<Self>(),
75            final(r)@ == pod_bytes(*final(self)),
76            *final(self) == decode_pod::<Self>(final(r)@),
77    )]
78    fn as_bytes_mut(&mut self) -> &mut [u8] {
79        let ptr = self as *mut Self as *mut u8;
80        let len = core::mem::size_of::<Self>();
81        unsafe { core::slice::from_raw_parts_mut(ptr, len) }
82    }
83}
84
85/// The value decoded from the first `size_of::<T>()` input bytes.
86pub open spec fn from_bytes_spec<T>(bytes: Seq<u8>) -> T {
87    decode_pod::<T>(bytes[0..core::mem::size_of::<T>()])
88}
89
90/// Spec function: the byte representation of a [`Pod`] value.
91///
92/// This is uninterpreted — the actual byte mapping depends on `T`'s layout
93/// (endianness, padding, etc.) which we don't model. Callers use this to
94/// relate writes and reads of the same value through memory.
95pub uninterp spec fn pod_bytes<T>(val: T) -> Seq<u8>;
96
97/// The Pod value whose byte representation equals `bytes` (when one exists).
98///
99/// Defined via `choose`; if no Pod value maps to `bytes`, the result is
100/// arbitrary. Callers should obtain the relevant existence fact from a checked
101/// byte conversion before relying on the returned value.
102pub open spec fn decode_pod<T>(bytes: Seq<u8>) -> T {
103    choose|val: T| pod_bytes::<T>(val) == bytes
104}
105
106macro_rules! impl_pod_for {
107    ($($pod_ty:ty),*) => {
108        $(unsafe impl Pod for $pod_ty {})*
109    };
110}
111
112// impl Pod for primitive types
113impl_pod_for!(u8, u16, u32, u64, u128, i8, i16, i32, i64, i128, isize, usize);
114
115// impl Pod for array
116unsafe impl<T: Pod, const N: usize> Pod for [T; N] {
117
118}
119
120} // verus!
121#[cfg(feature = "derive")]
122pub use ostd_pod_derive::*;
ostd_pod/lib.rs

ostd_pod/
lib.rs
