Function u16_be_from_bytes 

pub open spec fn u16_be_from_bytes(i: [u8; 2]) -> u16

{ (i[0] as u16) << 8 | (i[1] as u16) }