Function universal_code_point 

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

recommends

0 <= 4 * i,

4 * i + 3 < bytes.len(),

{
    u32_be_from_bytes([
        bytes[4 * i],
        bytes[4 * i + 1],
        bytes[4 * i + 2],
        bytes[4 * i + 3],
    ])
}