Function size_of_usize 

pub open spec fn size_of_usize() -> nat

{ if usize::BITS == 32 { 4 } else { 8 } }

Number of bytes in usize.