Function bmp_code_unit 

pub open spec fn bmp_code_unit(bytes: Seq<u8>, i: int) -> u32

recommends

0 <= 2 * i,

2 * i + 1 < bytes.len(),

{ u16_be_from_bytes([bytes[2 * i], bytes[2 * i + 1]]) as u32 }