pub uninterp spec fn pod_bytes<T: Pod>(val: T) -> Seq<u8>Expand description
Spec function: the byte representation of a Pod value.
This is uninterpreted — the actual byte mapping depends on T’s layout
(endianness, padding, etc.) which we don’t model. Callers use this to
relate writes and reads of the same value through memory.