Struct Named 

pub struct Named<Inner>(pub &'static str, pub Inner);

Transparent wrapper around Inner that annotates runtime parse errors with a static format name.

The semantic format is unchanged: parsing, consistency, serialization, and all proof obligations are delegated to Inner.

Tuple Fields

0: &'static str

1: Inner

Trait Implementations

impl<Inner: AdmitsUniqueVal> AdmitsUniqueVal for Named<Inner>

proof fn lemma_unique_consistent_val(&self, v1: Self::Val, v2: Self::Val)

impl<T, Inner> ByteLen<T> for Named<Inner>

where T: DeepView, Inner: ByteLen<T>,

open spec fn exec_inv(&self) -> bool

{ self.1.exec_inv() }

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

impl<Inner: BytesCombinator> BytesCombinator for Named<Inner>

proof fn lemma_byte_len_is_buf_len(&self, buf: Seq<u8>)

impl<Inner: Clone> Clone for Named<Inner>

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

ensures

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

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

Performs copy-assignment from source.

impl<Inner: Consistency> Consistency for Named<Inner>

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

{ self.1.consistent(v) }

type Val = <Inner as Consistency>::Val

The type of values whose consistency is being checked.

impl<Inner: EquivSerializers> EquivSerializers for Named<Inner>

open spec fn equiv_inv(&self) -> bool

{ self.1.equiv_inv() }

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

impl<Inner: EquivSerializersGeneral> EquivSerializersGeneral for Named<Inner>

open spec fn equiv_general_inv(&self) -> bool

{ self.1.equiv_general_inv() }

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

impl<Inner: GoodSerializer> GoodSerializer for Named<Inner>

open spec fn serialize_inv(&self) -> bool

{ self.1.serialize_inv() }

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

impl<Inner: HasAsn1Start> HasAsn1Start for Named<Inner>

Diagnostic naming does not change the accepted byte domain.

open spec fn asn1_start(&self) -> Asn1StartDomain

{ self.1.asn1_start() }

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

impl<Inner: LeafNonMalleable> LeafNonMalleable for Named<Inner>

proof fn nonmal_leaf_inv(&self)

impl<Inner: MinMaxByteLen> MinMaxByteLen for Named<Inner>

open spec fn min(&self) -> nat

{ self.1.min() }

open spec fn max(&self) -> nat

{ self.1.max() }

proof fn lemma_min_max_byte_len(&self, v: Self::T)

impl<Inner: NoLookAhead> NoLookAhead for Named<Inner>

open spec fn no_lookahead_inv(&self) -> bool

{ self.1.no_lookahead_inv() }

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

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

impl<Inner: NonMalleable> NonMalleable for Named<Inner>

open spec fn nonmal_inv(&self) -> bool

{ self.1.nonmal_inv() }

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

impl<Inner: NonTailFmt> NonTailFmt for Named<Inner>

open spec fn serialize_dps_inv(&self) -> bool

{ self.1.serialize_dps_inv() }

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

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

impl<I, Inner> Parser<I> for Named<Inner>

where I: View<V = Seq<u8>>, Inner: Parser<I>,

open spec fn exec_inv(&self) -> bool

{ self.1.exec_inv() }

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

type PT = <Inner as Parser<I>>::PT

Executable value returned by this parser.

impl<T, Inner> Prepare<T> for Named<Inner>

where T: DeepView, Inner: Prepare<T>,

open spec fn exec_inv(&self) -> bool

{ self.1.exec_inv() }

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

impl<Inner: Productive> Productive for Named<Inner>

open spec fn productive_inv(&self) -> bool

{ self.1.productive_inv() }

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

impl<Inner: SPRoundTripDps> SPRoundTripDps for Named<Inner>

open spec fn unambiguous(&self) -> bool

{ self.1.unambiguous() }

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

impl<Inner: SafeParser> SafeParser for Named<Inner>

open spec fn safe_inv(&self) -> bool

{ self.1.safe_inv() }

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

impl<Output: OutputBuf, T, Inner> Serializer<Output, T> for Named<Inner>

where T: DeepView, Inner: Serializer<Output, T>,

open spec fn exec_inv(&self) -> bool

{ self.1.exec_inv() }

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

impl<Inner: SoundParser> SoundParser for Named<Inner>

open spec fn sound_inv(&self) -> bool

{ self.1.sound_inv() }

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

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

impl<Inner: SpecByteLen> SpecByteLen for Named<Inner>

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

{ self.1.byte_len(v) }

type T = <Inner as SpecByteLen>::T

The type of values whose byte length is being computed.

impl<Inner: SpecParser> SpecParser for Named<Inner>

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

{ self.1.spec_parse(ibuf) }

type PVal = <Inner as SpecParser>::PVal

The type of parsed values.

impl<Inner: SpecSerializer> SpecSerializer for Named<Inner>

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

{ self.1.spec_serialize(v) }

type SVal = <Inner as SpecSerializer>::SVal

The type of values to be serialized.

impl<Inner: SpecSerializerDps> SpecSerializerDps for Named<Inner>

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

{ self.1.spec_serialize_dps(v, obuf) }

type SValue = <Inner as SpecSerializerDps>::SValue

The type of values to be serialized.

impl<Inner: StaticByteLen> StaticByteLen for Named<Inner>

open spec fn static_byte_len() -> nat

{ Inner::static_byte_len() }

proof fn lemma_static_len_matches_byte_len(&self, v: Self::T)

impl<Inner: ValueByteLen> ValueByteLen for Named<Inner>

open spec fn value_byte_len(v: Self::T) -> nat

{ Inner::value_byte_len(v) }

proof fn lemma_value_len_matches_byte_len(&self, v: Self::T)

impl<Inner: Copy> Copy for Named<Inner>