Struct UniversalStringFmt 

pub struct UniversalStringFmt;

ASN.1 UniversalString format.

Trait Implementations

impl BerDecoderOwned for UniversalStringFmt

Available on crate feature alloc only.

exec fn decode_owned(&self, bytes: Vec<u8>) -> Result<Self::Owned, ParseError>

type Owned = String

impl ByteLen<String> for UniversalStringFmt

Available on crate feature alloc only.

exec fn length(&self, value: &UniversalString) -> usize

fn exec_inv(&self) -> bool

impl Clone for UniversalStringFmt

fn clone(&self) -> UniversalStringFmt

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Consistency for UniversalStringFmt

open spec fn consistent(&self, value: Self::Val) -> bool

{ universalstring_fmt().consistent(value) }

type Val = Seq<char>

The type of values whose consistency is being checked.

impl DerOrd<String> for UniversalStringFmt

Available on crate feature alloc only.

proof fn lemma_der_serialize_len(&self, value: Seq<char>)

open spec fn der_remaining( &self, value: Seq<char>, state: UniversalStringDerState, ) -> Seq<u8>

{ self.spec_serialize(value).skip(universal_string_der_position(state) as int) }

open spec fn der_state_valid( &self, value: Seq<char>, state: UniversalStringDerState, ) -> bool

{
    &&& state.char_index <= value.len()
    &&& state.octet_index < 4
    &&& state.char_index == value.len() ==> state.octet_index == 0

}

exec fn der_start(&self, value: &UniversalString) -> state : UniversalStringDerState

exec fn der_next( &self, value: &UniversalString, state: &mut UniversalStringDerState, ) -> next : Option<u8>

fn der_leq(&self, left: &T, right: &T) -> bool

impl DerState for UniversalStringFmt

Available on crate feature alloc only.

type State = UniversalStringDerState

impl EquivSerializers for UniversalStringFmt

proof fn lemma_serialize_equiv_on_empty(&self, value: Self::SVal)

fn equiv_inv(&self) -> bool

impl GoodSerializer for UniversalStringFmt

proof fn lemma_serialize_len(&self, value: Self::SVal)

fn serialize_inv(&self) -> bool

impl NonMalleable for UniversalStringFmt

proof fn lemma_parse_non_malleable(&self, buf1: Seq<u8>, buf2: Seq<u8>)

fn nonmal_inv(&self) -> bool

impl<'i> Parser<&'i [u8]> for UniversalStringFmt

Available on crate feature alloc only.

exec fn parse(&self, ibuf: &&'i [u8]) -> PResult<Self::PT>

type PT = String

Executable value returned by this parser.

fn exec_inv(&self) -> bool

impl Prepare<String> for UniversalStringFmt

Available on crate feature alloc only.

exec fn prepare(&self, value: &UniversalString) -> Result<usize, PreSerializeError>

fn exec_inv(&self) -> bool

impl Productive for UniversalStringFmt

open spec fn productive_inv(&self) -> bool

{ false }

proof fn lemma_productive(&self, _input: Seq<u8>)

impl SPRoundTripDps for UniversalStringFmt

proof fn theorem_serialize_dps_parse_roundtrip(&self, value: Self::T, obuf: Seq<u8>)

fn unambiguous(&self) -> bool

impl SafeParser for UniversalStringFmt

proof fn lemma_parse_safe(&self, ibuf: Seq<u8>)

fn safe_inv(&self) -> bool

impl<Output: OutputBuf> Serializer<Output, String> for UniversalStringFmt

Available on crate feature alloc only.

exec fn serialize_into(&self, value: &UniversalString, obuf: &mut Output)

fn exec_inv(&self) -> bool

impl SoundParser for UniversalStringFmt

proof fn lemma_parse_sound_consumption(&self, ibuf: Seq<u8>)

proof fn lemma_parse_sound_value(&self, ibuf: Seq<u8>)

fn sound_inv(&self) -> bool

impl SpecByteLen for UniversalStringFmt

open spec fn byte_len(&self, value: Self::T) -> nat

{ universalstring_fmt().byte_len(value) }

type T = Seq<char>

The type of values whose byte length is being computed.

impl SpecParser for UniversalStringFmt

open spec fn spec_parse(&self, ibuf: Seq<u8>) -> Option<(int, Self::PVal)>

{ universalstring_fmt().spec_parse(ibuf) }

type PVal = Seq<char>

The type of parsed values.

impl SpecSerializer for UniversalStringFmt

open spec fn spec_serialize(&self, value: Self::SVal) -> Seq<u8>

{ universalstring_fmt().spec_serialize(value) }

type SVal = Seq<char>

The type of values to be serialized.

impl SpecSerializerDps for UniversalStringFmt

open spec fn spec_serialize_dps(&self, value: Self::SValue, obuf: Seq<u8>) -> Seq<u8>

{ universalstring_fmt().spec_serialize_dps(value, obuf) }

type SValue = Seq<char>

The type of values to be serialized.

impl Copy for UniversalStringFmt