ostd_pod/
lib.rs

1//! This crate defines a marker trait for plain old data (POD).
2#![no_std]
3
4use vstd::prelude::*;
5use vstd_extra::array_ptr::{self, ArrayPtr, PointsToArray};
6
7use core::mem::MaybeUninit;
8
9verus! {
10
11/// A marker trait for plain old data (POD).
12///
13/// A POD type `T:Pod` supports converting to and from arbitrary
14/// `mem::size_of::<T>()` bytes _safely_.
15/// For example, simple primitive types like `u8` and `i16`
16/// are POD types. But perhaps surprisingly, `bool` is not POD
17/// because Rust compiler makes implicit assumption that
18/// a byte of `bool` has a value of either `0` or `1`.
19/// Interpreting a byte of value `3` has a `bool` value has
20/// undefined behavior.
21///
22/// # Safety
23///
24/// Marking a non-POD type as POD may cause undefined behaviors.
25pub unsafe trait Pod: Copy + Sized {
26    /// Creates a new instance of Pod type that is filled with zeroes.
27    #[verifier::external_body]
28    fn new_zeroed() -> Self {
29        // SAFETY. An all-zero value of `T: Pod` is always valid.
30        unsafe { core::mem::zeroed() }
31    }
32
33    /// Creates a new instance of Pod type with uninitialized content.
34    #[verifier::external_body]
35    fn new_uninit() -> Self {
36        // SAFETY. A value of `T: Pod` can have arbitrary bits.
37        #[allow(clippy::uninit_assumed_init)]
38        unsafe { MaybeUninit::uninit().assume_init() }
39    }
40
41    /// As an immutable slice of bytes.
42    #[verifier::external_body]
43    fn as_bytes(&self) -> (r: &[u8])
44        ensures
45            r.len() == core::mem::size_of::<Self>(),
46    {
47        let ptr = self as *const Self as *const u8;
48        let len = core::mem::size_of::<Self>();
49
50        unsafe { core::slice::from_raw_parts(ptr, len) }
51    }
52
53    /// As a mutable slice of bytes.
54    #[verifier::external_body]
55    fn as_bytes_mut(&mut self) -> (r: &mut [u8])
56        ensures
57            r.len() == core::mem::size_of::<Self>(),
58    {
59        let ptr = self as *mut Self as *mut u8;
60        let len = core::mem::size_of::<Self>();
61
62        unsafe { core::slice::from_raw_parts_mut(ptr, len) }
63    }
64
65    /// As a slice of bytes via an [`ArrayPtr`] (with a tracked permission).
66    ///
67    /// This is the verus-flavored variant; the raw `&[u8]` view is [`Self::as_bytes`].
68    #[verifier::external_body]
69    fn as_array_ptr_bytes<const N: usize>(&self) -> (slice: (
70        ArrayPtr<u8, N>,
71        Tracked<&array_ptr::PointsTo<u8, N>>,
72    ))
73        ensures
74            slice.1@.value().len() == core::mem::size_of::<Self>(),
75            slice.1@.wf(),
76            slice.0.addr() == slice.1@.addr(),
77    {
78        let ptr = self as *const Self as *const u8;
79
80        (ArrayPtr::from_addr(ptr as usize), Tracked::assume_new())
81    }
82}
83
84/// Spec function: the byte representation of a [`Pod`] value.
85///
86/// This is uninterpreted — the actual byte mapping depends on `T`'s layout
87/// (endianness, padding, etc.) which we don't model. Callers use this to
88/// relate writes and reads of the same value through memory.
89pub uninterp spec fn pod_bytes<T: Pod>(val: T) -> Seq<u8>;
90
91/// Axiom: the byte representation of a `T: Pod` value has length `size_of::<T>()`.
92pub broadcast axiom fn axiom_pod_bytes_len<T: Pod>(val: T)
93    ensures
94        #[trigger] pod_bytes(val).len() == core::mem::size_of::<T>(),
95;
96
97/// Axiom: [`pod_bytes`] is injective — equal byte sequences come from equal values.
98///
99/// `T: Pod` has a well-defined byte layout (no padding for `repr(C)` primitives),
100/// so the byte sequence uniquely determines the value.
101pub broadcast axiom fn axiom_pod_bytes_injective<T: Pod>(v1: T, v2: T)
102    ensures
103        #[trigger] pod_bytes(v1) == #[trigger] pod_bytes(v2) ==> v1 == v2,
104;
105
106/// The Pod value whose byte representation equals `bytes` (when one exists).
107///
108/// Defined via `choose` over the injective [`pod_bytes`]; if no Pod value
109/// maps to `bytes`, the result is arbitrary. Callers should establish
110/// existence before relying on the returned value.
111pub open spec fn decode_pod<T: Pod>(bytes: Seq<u8>) -> T {
112    choose|v: T| pod_bytes::<T>(v) == bytes
113}
114
115/// Round-trip: `decode_pod(pod_bytes(v)) == v` by injectivity.
116pub broadcast proof fn lemma_decode_pod_inverse<T: Pod>(v: T)
117    ensures
118        #[trigger] decode_pod::<T>(pod_bytes::<T>(v)) == v,
119{
120    let bytes = pod_bytes::<T>(v);
121    let chosen: T = choose|w: T| pod_bytes::<T>(w) == bytes;
122    assert(pod_bytes::<T>(chosen) == bytes);
123    broadcast use axiom_pod_bytes_injective;
124
125}
126
127macro_rules! impl_pod_for {
128    ($($pod_ty:ty),*) => {
129        $(unsafe impl Pod for $pod_ty {})*
130    };
131}
132
133// impl Pod for primitive types
134impl_pod_for!(u8, u16, u32, u64, u128, i8, i16, i32, i64, i128, isize, usize);
135
136// impl Pod for array
137unsafe impl<T: Pod, const N: usize> Pod for [T; N] {
138
139}
140
141} // verus!
ostd_pod/lib.rs

ostd_pod/
lib.rs
