Function bmp_string_der_position 

pub open spec fn bmp_string_der_position(state: BmpStringDerState) -> nat

{ state.char_index as nat * 2 + if state.second_octet { 1nat } else { 0nat } }