pub broadcast proof fn axiom_pod_bytes_len<T: Pod>(val: T)Expand description
ensures
#[trigger] pod_bytes(val).len() == core::mem::size_of::<T>(),Axiom: the byte representation of a T: Pod value has length size_of::<T>().