Struct ASN1Fmt 

pub struct ASN1Fmt<Content, const DER: bool = true>(pub Tag, pub Content);

Tuple Fields

0: Tag

1: Content

Trait Implementations

impl<Content, T, const DER: bool> ByteLen<T> for ASN1Fmt<Content, DER>

where T: DeepView + ?Sized, Content: SpecCombinator + ByteLen<T>,

open spec fn exec_inv(&self) -> bool

{ self.1.exec_inv() }

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

impl<Content: Clone, const DER: bool> Clone for ASN1Fmt<Content, DER>

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

ensures

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

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

Performs copy-assignment from source.

impl<Content: SpecCombinator, const DER: bool> Consistency for ASN1Fmt<Content, DER>

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

{ asn1_fmt::<Content, DER>(self.0, self.1).consistent(v) }

type Val = <Content as SpecParser>::PVal

The type of values whose consistency is being checked.

impl<Content, T> DerOrd<T> for ASN1Fmt<Content, true>

where T: DeepView + ?Sized, Content: SpecCombinator<T = T::V> + DerOrd<T>,

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

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

{
    match state.phase {
        0 => {
            TagFmt.der_remaining(self.0, state.tag)
                + LengthFmt::<true>.der_remaining(state.content_len, state.length)
                + self.1.der_remaining(value, state.content)
        }
        1 => {
            LengthFmt::<true>.der_remaining(state.content_len, state.length)
                + self.1.der_remaining(value, state.content)
        }
        _ => self.1.der_remaining(value, state.content),
    }
}

open spec fn der_state_valid( &self, value: T::V, state: TlvDerState<Content::State>, ) -> bool

{
    &&& TagFmt.der_state_valid(self.0, state.tag)
    &&& LengthFmt::<true>.der_state_valid(state.content_len, state.length)
    &&& self.1.der_state_valid(value, state.content)
    &&& state.content_len as nat == self.1.byte_len(value)
    &&& state.phase <= 2
    &&& state.phase >= 1 ==> TagFmt.der_remaining(self.0, state.tag).len() == 0
    &&& state.phase >= 2
        ==> LengthFmt::<true>.der_remaining(state.content_len, state.length).len() == 0

}

exec fn der_start(&self, v: &T) -> state : TlvDerState<Content::State>

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

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

impl<Content: DerState> DerState for ASN1Fmt<Content, true>

type State = TlvDerState<<Content as DerState>::State>

impl<Content: SpecCombinator + EquivSerializers, const DER: bool> EquivSerializers for ASN1Fmt<Content, DER>

open spec fn equiv_inv(&self) -> bool

{ self.1.equiv_inv() }

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

impl<Content: SpecCombinator + EquivSerializers, const DER: bool> EquivSerializersGeneral for ASN1Fmt<Content, DER>

open spec fn equiv_general_inv(&self) -> bool

{ self.1.equiv_inv() }

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

impl<Content: SpecCombinator + GoodSerializer, const DER: bool> GoodSerializer for ASN1Fmt<Content, DER>

open spec fn serialize_inv(&self) -> bool

{ self.1.serialize_inv() }

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

impl<Content: SpecCombinator, const DER: bool> HasAsn1Start for ASN1Fmt<Content, DER>

Ordinary definite-length TLVs have one exact outer tag.

open spec fn asn1_start(&self) -> Asn1StartDomain

{
    asn1_start_exact_uint(
        self.0.class,
        self.0.constructed,
        tag_num_to_uint(self.0.number),
    )
}

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

impl<Content: SpecCombinator + SafeParser, const DER: bool> NoLookAhead for ASN1Fmt<Content, DER>

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

fn no_lookahead_inv(&self) -> bool

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

impl<Content: SpecCombinator + SoundParser + NonMalleable> NonMalleable for ASN1Fmt<Content, true>

open spec fn nonmal_inv(&self) -> bool

{
    &&& self.1.nonmal_inv()
    &&& self.1.sound_inv()
    &&& self.1.safe_inv()
    &&& TagFmt.consistent(self.0)

}

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

impl<Content: SpecCombinator + GoodSerializer + EquivSerializers, const DER: bool> NonTailFmt for ASN1Fmt<Content, DER>

open spec fn serialize_dps_inv(&self) -> bool

{
    &&& self.1.serialize_inv()
    &&& self.1.equiv_inv()

}

proof fn lemma_serialize_dps_prepend(&self, v: Content::PVal, obuf: Seq<u8>)

proof fn lemma_serialize_dps_len(&self, v: Content::PVal, obuf: Seq<u8>)

impl<'i, Content, const DER: bool> Parser<&'i [u8]> for ASN1Fmt<Content, DER>

where Content: SpecCombinator + Parser<&'i [u8]>,

open spec fn exec_inv(&self) -> bool

{ self.1.exec_inv() }

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

type PT = <Content as Parser<&'i [u8]>>::PT

Executable value returned by this parser.

impl<Content, T, const DER: bool> Prepare<T> for ASN1Fmt<Content, DER>

where T: DeepView + ?Sized, Content: SpecCombinator + Prepare<T>,

open spec fn exec_inv(&self) -> bool

{ self.1.exec_inv() }

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

impl<Content: SpecCombinator + Productive, const DER: bool> Productive for ASN1Fmt<Content, DER>

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

fn productive_inv(&self) -> bool

impl<C: Copy, const DER: bool> Retaggable for ASN1Fmt<C, DER>

Supports IMPLICIT tagging of an ordinary ASN.1 TLV.

Retagging replaces the tag class and number, preserves the base format’s primitive/constructed form, and leaves its content format unchanged.

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

{
    ASN1Fmt(
        Tag {
            class: tag.class,
            constructed: self.0.constructed,
            number: tag.number,
        },
        self.1,
    )
}

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

impl<Content: SpecCombinator + EquivSerializers + GoodSerializer + SPRoundTrip, const DER: bool> SPRoundTripDps for ASN1Fmt<Content, DER>

open spec fn unambiguous(&self) -> bool

{
    &&& self.1.serialize_inv()
    &&& self.1.equiv_inv()
    &&& self.1.sp_roundtrip_inv()

}

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

impl<Content: SpecCombinator + SafeParser, const DER: bool> SafeParser for ASN1Fmt<Content, DER>

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

fn safe_inv(&self) -> bool

impl<Output: OutputBuf, Content, T, const DER: bool> Serializer<Output, T> for ASN1Fmt<Content, DER>

where T: DeepView + ?Sized, Content: SpecCombinator + Serializer<Output, T> + ByteLen<T>,

open spec fn exec_inv(&self) -> bool

{
    &&& <_ as Serializer<Output, T>>::exec_inv(&self.1)
    &&& <_ as ByteLen<T>>::exec_inv(&self.1)

}

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

impl<Content: SpecCombinator + SoundParser> SoundParser for ASN1Fmt<Content, true>

open spec fn sound_inv(&self) -> bool

{
    &&& self.1.sound_inv()
    &&& TagFmt.consistent(self.0)

}

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

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

impl<Content: SpecCombinator, const DER: bool> SpecByteLen for ASN1Fmt<Content, DER>

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

{ asn1_fmt::<Content, DER>(self.0, self.1).byte_len(v) }

type T = <Content as SpecParser>::PVal

The type of values whose byte length is being computed.

impl<Content: SpecCombinator, const DER: bool> SpecParser for ASN1Fmt<Content, DER>

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

{ asn1_fmt::<Content, DER>(self.0, self.1).spec_parse(ibuf) }

type PVal = <Content as SpecParser>::PVal

The type of parsed values.

impl<Content: SpecCombinator, const DER: bool> SpecSerializer for ASN1Fmt<Content, DER>

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

{ asn1_fmt::<Content, DER>(self.0, self.1).spec_serialize(v) }

type SVal = <Content as SpecParser>::PVal

The type of values to be serialized.

impl<Content: SpecCombinator, const DER: bool> SpecSerializerDps for ASN1Fmt<Content, DER>

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

{ asn1_fmt::<Content, DER>(self.0, self.1).spec_serialize_dps(v, obuf) }

type SValue = <Content as SpecParser>::PVal

The type of values to be serialized.

impl<Content: Copy, const DER: bool> Copy for ASN1Fmt<Content, DER>