Struct EnumeratedFmt 

pub struct EnumeratedFmt;

ASN.1 ENUMERATED contents format.

Trait Implementations

impl<'i> ByteLen<Integer<'i>> for EnumeratedFmt

exec fn length(&self, v: &Enumerated<'i>) -> usize

fn exec_inv(&self) -> bool

impl Clone for EnumeratedFmt

fn clone(&self) -> EnumeratedFmt

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Consistency for EnumeratedFmt

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

{ IntegerFmt.consistent(v) }

type Val = int

The type of values whose consistency is being checked.

impl<'a> DerOrd<Integer<'a>> for EnumeratedFmt

proof fn lemma_der_serialize_len(&self, value: int)

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

{ IntegerFmt.der_remaining(value, state) }

open spec fn der_state_valid(&self, value: int, state: IntegerDerState) -> bool

{ IntegerFmt.der_state_valid(value, state) }

exec fn der_start(&self, i: &Integer<'a>) -> state : IntegerDerState

exec fn der_next(&self, i: &Integer<'a>, state: &mut IntegerDerState) -> next : Option<u8>

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

impl DerState for EnumeratedFmt

type State = IntegerDerState

impl EquivSerializers for EnumeratedFmt

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

fn equiv_inv(&self) -> bool

impl GoodSerializer for EnumeratedFmt

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

fn serialize_inv(&self) -> bool

impl NonMalleable for EnumeratedFmt

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

fn nonmal_inv(&self) -> bool

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

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

type PT = Integer<'i>

Executable value returned by this parser.

fn exec_inv(&self) -> bool

impl<'i> Prepare<Integer<'i>> for EnumeratedFmt

exec fn prepare(&self, v: &Enumerated<'i>) -> Result<usize, PreSerializeError>

fn exec_inv(&self) -> bool

impl Productive for EnumeratedFmt

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

fn productive_inv(&self) -> bool

impl SPRoundTripDps for EnumeratedFmt

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

fn unambiguous(&self) -> bool

impl SafeParser for EnumeratedFmt

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

fn safe_inv(&self) -> bool

impl<'i, Output: OutputBuf> Serializer<Output, Integer<'i>> for EnumeratedFmt

exec fn serialize_into(&self, v: &Enumerated<'i>, obuf: &mut Output)

fn exec_inv(&self) -> bool

impl SoundParser for EnumeratedFmt

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 EnumeratedFmt

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

{ IntegerFmt.byte_len(v) }

type T = int

The type of values whose byte length is being computed.

impl SpecParser for EnumeratedFmt

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

{ IntegerFmt.spec_parse(ibuf) }

type PVal = int

The type of parsed values.

impl SpecSerializer for EnumeratedFmt

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

{ IntegerFmt.spec_serialize(v) }

type SVal = int

The type of values to be serialized.

impl SpecSerializerDps for EnumeratedFmt

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

{ IntegerFmt.spec_serialize_dps(v, obuf) }

type SValue = int

The type of values to be serialized.

impl Copy for EnumeratedFmt