Function continuation_byte 

pub open spec fn continuation_byte() -> ContinuationByte

{
    Mapped {
        inner: Refined(U8, |b: u8| b >= CONTINUATION_BIT),
        mapper: LowBitsMask,
    }
}

Check that high bit is set, and map to the corresponding low 7 bits.