Function decode_pod 

pub open spec fn decode_pod<T>(bytes: Seq<u8>) -> T

{ choose |val: T| pod_bytes::<T>(val) == bytes }

The Pod value whose byte representation equals bytes (when one exists).

Defined via choose; if no Pod value maps to bytes, the result is arbitrary. Callers should obtain the relevant existence fact from a checked byte conversion before relying on the returned value.