pub open spec fn u24_be_to_bytes(o: u32) -> [u8; 3]
{ [((o >> 16) & 0xff) as u8, ((o >> 8) & 0xff) as u8, (o & 0xff) as u8] }