Struct ImplicitlyTaggedFmt 

pub struct ImplicitlyTaggedFmt<F>(pub Tag, pub F);

Const-constructible ASN.1 IMPLICIT tagging wrapper.

Tuple Fields

0: Tag

1: F

Trait Implementations

impl<F, T> ByteLen<T> for ImplicitlyTaggedFmt<F>

where T: DeepView + ?Sized, F: Retaggable + ByteLen<T>,

open spec fn exec_inv(&self) -> bool

{ <F as ByteLen<T>>::exec_inv(&self.1.spec_retagged(self.0)) }

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

impl<F: Clone> Clone for ImplicitlyTaggedFmt<F>

exec fn clone(&self) -> cloned : Self

ensures

cloned.0 == self.0,

call_ensures(F::clone, (&self.1,), cloned.1),

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

Performs copy-assignment from source.

impl<F> Consistency for ImplicitlyTaggedFmt<F>

where F: Retaggable + Consistency,

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

{ self.1.spec_retagged(self.0).consistent(value) }

type Val = <F as Consistency>::Val

The type of values whose consistency is being checked.

impl<F, T> DerOrd<T> for ImplicitlyTaggedFmt<F>

where T: DeepView + ?Sized, F: Retaggable + DerOrd<T>,

proof fn lemma_der_serialize_len(&self, value: T::V)

open spec fn der_remaining(&self, value: T::V, state: <F as DerState>::State) -> Seq<u8>

{ self.1.spec_retagged(self.0).der_remaining(value, state) }

open spec fn der_state_valid(&self, value: T::V, state: <F as DerState>::State) -> bool

{ self.1.spec_retagged(self.0).der_state_valid(value, state) }

exec fn der_start(&self, v: &T) -> state : <F as DerState>::State

exec fn der_next(&self, v: &T, state: &mut <F as DerState>::State) -> next : Option<u8>

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

impl<F> DerState for ImplicitlyTaggedFmt<F>

where F: Retaggable + DerState,

type State = <F as DerState>::State

impl<F> EquivSerializers for ImplicitlyTaggedFmt<F>

where F: Retaggable + EquivSerializers,

open spec fn equiv_inv(&self) -> bool

{ self.1.spec_retagged(self.0).equiv_inv() }

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

impl<F> EquivSerializersGeneral for ImplicitlyTaggedFmt<F>

where F: Retaggable + EquivSerializersGeneral,

open spec fn equiv_general_inv(&self) -> bool

{ self.1.spec_retagged(self.0).equiv_general_inv() }

proof fn lemma_serialize_equiv(&self, value: Self::SVal, obuf: Seq<u8>)

impl<F> GoodSerializer for ImplicitlyTaggedFmt<F>

where F: Retaggable + GoodSerializer,

open spec fn serialize_inv(&self) -> bool

{ self.1.spec_retagged(self.0).serialize_inv() }

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

impl<Format> HasAsn1Start for ImplicitlyTaggedFmt<Format>

where Format: Retaggable + HasAsn1Start,

IMPLICIT tagging delegates parsing and its start domain to the concretely retagged format.

open spec fn asn1_start(&self) -> Asn1StartDomain

{ self.1.spec_retagged(self.0).asn1_start() }

proof fn lemma_parse_implies_asn1_start(&self, input: Seq<u8>)

impl<F> NoLookAhead for ImplicitlyTaggedFmt<F>

where F: Retaggable + NoLookAhead,

open spec fn no_lookahead_inv(&self) -> bool

{ self.1.spec_retagged(self.0).no_lookahead_inv() }

proof fn lemma_no_lookahead(&self, ibuf1: Seq<u8>, ibuf2: Seq<u8>)

fn corollary_non_extensible(&self, i1: Seq<u8>, i2: Seq<u8>)

impl<F> NonMalleable for ImplicitlyTaggedFmt<F>

where F: Retaggable + NonMalleable,

open spec fn nonmal_inv(&self) -> bool

{ self.1.spec_retagged(self.0).nonmal_inv() }

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

impl<F> NonTailFmt for ImplicitlyTaggedFmt<F>

where F: Retaggable + NonTailFmt,

open spec fn serialize_dps_inv(&self) -> bool

{ self.1.spec_retagged(self.0).serialize_dps_inv() }

proof fn lemma_serialize_dps_prepend(&self, value: Self::SValue, obuf: Seq<u8>)

proof fn lemma_serialize_dps_len(&self, value: Self::SValue, obuf: Seq<u8>)

impl<Input, F> Parser<Input> for ImplicitlyTaggedFmt<F>

where Input: InputBuf, F: Retaggable + Parser<Input>,

open spec fn exec_inv(&self) -> bool

{ <F as Parser<Input>>::exec_inv(&self.1.spec_retagged(self.0)) }

exec fn parse(&self, ibuf: &Input) -> PResult<Self::PT>

type PT = <F as Parser<Input>>::PT

Executable value returned by this parser.

impl<F, T> Prepare<T> for ImplicitlyTaggedFmt<F>

where T: DeepView + ?Sized, F: Retaggable + Prepare<T>,

open spec fn exec_inv(&self) -> bool

{ <F as Prepare<T>>::exec_inv(&self.1.spec_retagged(self.0)) }

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

impl<F> Productive for ImplicitlyTaggedFmt<F>

where F: Retaggable + Productive,

open spec fn productive_inv(&self) -> bool

{ self.1.spec_retagged(self.0).productive_inv() }

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

impl<F: Retaggable> Retaggable for ImplicitlyTaggedFmt<F>

Allows IMPLICIT tagging to compose/chain through an existing IMPLICIT-tag wrapper.

The newer tag replaces the stored outer tag and the underlying format is retained; when used, the underlying Retaggable implementation selects the correct primitive/constructed form.

open spec fn spec_retagged(&self, tag: Tag) -> Self

{ Self(tag, self.1) }

exec fn retagged(&self, tag: Tag) -> Self

impl<F> SPRoundTripDps for ImplicitlyTaggedFmt<F>

where F: Retaggable + SPRoundTripDps,

open spec fn unambiguous(&self) -> bool

{ self.1.spec_retagged(self.0).unambiguous() }

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

impl<F> SafeParser for ImplicitlyTaggedFmt<F>

where F: Retaggable + SafeParser,

open spec fn safe_inv(&self) -> bool

{ self.1.spec_retagged(self.0).safe_inv() }

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

impl<Output, F, T> Serializer<Output, T> for ImplicitlyTaggedFmt<F>

where Output: OutputBuf, T: DeepView + ?Sized, F: Retaggable + Serializer<Output, T>,

open spec fn exec_inv(&self) -> bool

{ <F as Serializer<Output, T>>::exec_inv(&self.1.spec_retagged(self.0)) }

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

impl<F> SoundParser for ImplicitlyTaggedFmt<F>

where F: Retaggable + SoundParser,

open spec fn sound_inv(&self) -> bool

{ self.1.spec_retagged(self.0).sound_inv() }

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

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

impl<F> SpecByteLen for ImplicitlyTaggedFmt<F>

where F: Retaggable + SpecByteLen,

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

{ self.1.spec_retagged(self.0).byte_len(value) }

type T = <F as SpecByteLen>::T

The type of values whose byte length is being computed.

impl<F> SpecParser for ImplicitlyTaggedFmt<F>

where F: Retaggable + SpecParser,

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

{ self.1.spec_retagged(self.0).spec_parse(ibuf) }

type PVal = <F as SpecParser>::PVal

The type of parsed values.

impl<F> SpecSerializer for ImplicitlyTaggedFmt<F>

where F: Retaggable + SpecSerializer,

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

{ self.1.spec_retagged(self.0).spec_serialize(value) }

type SVal = <F as SpecSerializer>::SVal

The type of values to be serialized.

impl<F> SpecSerializerDps for ImplicitlyTaggedFmt<F>

where F: Retaggable + SpecSerializerDps,

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

{ self.1.spec_retagged(self.0).spec_serialize_dps(value, obuf) }

type SValue = <F as SpecSerializerDps>::SValue

The type of values to be serialized.

impl<F: Copy> Copy for ImplicitlyTaggedFmt<F>