pub broadcast proof fn axiom_pod_bytes_injective<T: Pod>(v1: T, v2: T)Expand description
ensures
#[trigger] pod_bytes(v1) == #[trigger] pod_bytes(v2) ==> v1 == v2,Axiom: pod_bytes is injective — equal byte sequences come from equal values.
T: Pod has a well-defined byte layout (no padding for repr(C) primitives),
so the byte sequence uniquely determines the value.