Function from_bytes_spec 

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

{ decode_pod::<T>(bytes[0..core::mem::size_of::<T>()]) }

The value decoded from the first size_of::<T>() input bytes.