Function u32_be_to_bytes 

pub open spec fn u32_be_to_bytes(o: u32) -> [u8; 4]

{
    [
        ((o >> 24) & 0xff) as u8,
        ((o >> 16) & 0xff) as u8,
        ((o >> 8) & 0xff) as u8,
        (o & 0xff) as u8,
    ]
}