Function universal_string_der_position 

pub open spec fn universal_string_der_position(state: UniversalStringDerState) -> nat

{ state.char_index as nat * 4 + state.octet_index as nat }