Struct DefaultedFmt 

pub struct DefaultedFmt<Field, Default, Rest, const DER: bool = true>(pub Field, pub Default, pub Rest);

ASN.1 DEFAULT component with continuation.

The semantic value always contains the component value. On parsing, absence is replaced by default. On serialization, a value equal to default is omitted. DER additionally rejects an explicitly encoded default value.

Tuple Fields

0: Field

1: Default

2: Rest

Trait Implementations

impl<Field, Default, Rest, R, const DER: bool> ByteLen<(Default, R)> for DefaultedFmt<Field, Default, Rest, DER>

where Field: SpecByteLen<T = Default> + ByteLen<Default>, Rest: SpecByteLen<T = R::V> + ByteLen<R>, Default: DeepView<V = Default> + PartialEq + Structural + Copy, R: DeepView,

open spec fn exec_inv(&self) -> bool

{
    &&& self.0.exec_inv()
    &&& self.2.exec_inv()
    &&& forall |v: Default| v.deep_view() == v

}

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

impl<Field: Clone, Default: Clone, Rest: Clone, const DER: bool> Clone for DefaultedFmt<Field, Default, Rest, DER>

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

ensures

call_ensures(Field::clone, (&self.0,), cloned.0),

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

call_ensures(Rest::clone, (&self.2,), cloned.2),

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

Performs copy-assignment from source.

impl<Field, Rest, const DER: bool> Consistency for DefaultedFmt<Field, Field::Val, Rest, DER>

where Field: SpecByteLen + Consistency<Val = Field::T>, Rest: SpecByteLen + Consistency<Val = Rest::T>,

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

{ defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).consistent(v) }

type Val = (<Field as Consistency>::Val, <Rest as Consistency>::Val)

The type of values whose consistency is being checked.

impl<Field, Default, Rest, R> DerOrd<(Default, R)> for DefaultedFmt<Field, Default, Rest, true>

where Default: DeepViewIdentity + PartialEq + Structural, R: DeepView, Field: DerOrd<Default>, Rest: DerOrd<R>,

proof fn lemma_der_serialize_len(&self, value: (Default, R::V))

open spec fn der_remaining( &self, value: (Default, R::V), state: PairDerState<OptDerState<Field::State>, Rest::State>, ) -> Seq<u8>

{
    if state.in_left {
        (match (&value.0, &state.left) {
            (field, OptDerState::Some(inner)) if *field != self.1 => {
                self.0.der_remaining(*field, *inner)
            }
            (field, OptDerState::None) if *field == self.1 => Seq::empty(),
            _ => Seq::empty(),
        }) + self.2.der_remaining(value.1, state.right)
    } else {
        self.2.der_remaining(value.1, state.right)
    }
}

open spec fn der_state_valid( &self, value: (Default, R::V), state: PairDerState<OptDerState<Field::State>, Rest::State>, ) -> bool

{
    &&& match (&value.0, &state.left) {
        (field, OptDerState::Some(inner)) if *field != self.1 => {
            self.0.der_state_valid(*field, *inner)
        }
        (field, OptDerState::None) if *field == self.1 => true,
        _ => false,
    }
    &&& self.2.der_state_valid(value.1, state.right)
    &&& !state.in_left
        ==> {
            match (&value.0, &state.left) {
                (field, OptDerState::Some(inner)) if *field != self.1 => {
                    self.0.der_remaining(*field, *inner).len() == 0
                }
                (field, OptDerState::None) if *field == self.1 => true,
                _ => false,
            }
        }

}

exec fn der_start( &self, v: &(Default, R), ) -> state : PairDerState<OptDerState<Field::State>, Rest::State>

exec fn der_next( &self, v: &(Default, R), state: &mut PairDerState<OptDerState<Field::State>, Rest::State>, ) -> next : Option<u8>

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

impl<Field: DerState, Rest: DerState, Default> DerState for DefaultedFmt<Field, Default, Rest, true>

type State = PairDerState<OptDerState<<Field as DerState>::State>, <Rest as DerState>::State>

impl<Field, Rest, const DER: bool> EquivSerializers for DefaultedFmt<Field, Field::SVal, Rest, DER>

where Field: SpecByteLen + EquivSerializersGeneral<SVal = Field::T>, Rest: SpecByteLen + EquivSerializers<SVal = Rest::T>,

open spec fn equiv_inv(&self) -> bool

{ defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).equiv_inv() }

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

impl<Field, Rest, const DER: bool> EquivSerializersGeneral for DefaultedFmt<Field, Field::SVal, Rest, DER>

where Field: SpecByteLen + EquivSerializersGeneral<SVal = Field::T>, Rest: SpecByteLen + EquivSerializersGeneral<SVal = Rest::T>,

open spec fn equiv_general_inv(&self) -> bool

{ defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).equiv_general_inv() }

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

impl<Field, Rest, const DER: bool> GoodSerializer for DefaultedFmt<Field, Field::SVal, Rest, DER>

where Field: GoodSerializer, Rest: GoodSerializer,

open spec fn serialize_inv(&self) -> bool

{ defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).serialize_inv() }

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

impl<Field, Rest, const DER: bool> HasAsn1Start for DefaultedFmt<Field, Field::PVal, Rest, DER>

where Field: SpecByteLen + HasAsn1Start<PVal = Field::T>, Rest: SpecByteLen + HasAsn1Start<PVal = Rest::T>,

ASN.1 DEFAULT has the same possible starts as OPTIONAL: the field or its continuation.

open spec fn asn1_start(&self) -> Asn1StartDomain

{ asn1_start_union(self.0.asn1_start(), self.2.asn1_start()) }

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

impl<Field, Rest, const DER: bool> NoLookAhead for DefaultedFmt<Field, Field::PVal, Rest, DER>

where Field: SpecByteLen + NoLookAhead<PVal = Field::T>, Rest: SpecByteLen + NoLookAhead<PVal = Rest::T>,

open spec fn no_lookahead_inv(&self) -> bool

{ defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).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<Field, Rest, const DER: bool> NonMalleable for DefaultedFmt<Field, Field::PVal, Rest, DER>

where Field: SoundParser + NonMalleable, Rest: SoundParser + NonMalleable,

open spec fn nonmal_inv(&self) -> bool

{ defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).nonmal_inv() }

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

impl<Field, Rest, const DER: bool> NonTailFmt for DefaultedFmt<Field, Field::SValue, Rest, DER>

where Field: NonTailFmt, Rest: NonTailFmt,

open spec fn serialize_dps_inv(&self) -> bool

{ defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).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, Field, Rest, const DER: bool> Parser<I> for DefaultedFmt<Field, Field::T, Rest, DER>

where I: InputBuf, Field: Parser<I, PT = Field::T> + SafeParser<PVal = Field::T> + SpecByteLen, Rest: Parser<I> + SafeParser<PVal = Rest::T> + SpecByteLen, Field::T: DeepView<V = Field::T> + PartialEq + Structural + Copy,

open spec fn exec_inv(&self) -> bool

{
    &&& self.0.exec_inv()
    &&& self.0.safe_inv()
    &&& self.2.exec_inv()
    &&& self.2.safe_inv()
    &&& forall |v: Field::T| v.deep_view() == v
    &&& vstd::laws_eq::obeys_concrete_eq::<Field::T>()

}

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

type PT = (<Field as Parser<I>>::PT, <Rest as Parser<I>>::PT)

Executable value returned by this parser.

impl<Field, Default, Rest, R, const DER: bool> Prepare<(Default, R)> for DefaultedFmt<Field, Default, Rest, DER>

where Field: SpecByteLen<T = Default> + Prepare<Default>, Rest: SpecByteLen<T = R::V> + Prepare<R>, Default: DeepView<V = Default> + PartialEq + Structural + Copy, R: DeepView,

open spec fn exec_inv(&self) -> bool

{
    &&& self.0.exec_inv()
    &&& self.2.exec_inv()
    &&& forall |v: Default| v.deep_view() == v

}

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

impl<Field, Rest, const DER: bool> Productive for DefaultedFmt<Field, Field::PVal, Rest, DER>

where Field: SpecByteLen + Productive<PVal = Field::T>, Rest: SpecByteLen + Productive<PVal = Rest::T>,

open spec fn productive_inv(&self) -> bool

{ defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).productive_inv() }

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

impl<Field, Rest, const DER: bool> SPRoundTripDps for DefaultedFmt<Field, Field::T, Rest, DER>

where Field: SPRoundTripDps + NonTailFmt, Rest: SPRoundTripDps,

open spec fn unambiguous(&self) -> bool

{ defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).unambiguous() }

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

impl<Field, Rest, const DER: bool> SafeParser for DefaultedFmt<Field, Field::PVal, Rest, DER>

where Field: SpecByteLen + SafeParser<PVal = Field::T>, Rest: SpecByteLen + SafeParser<PVal = Rest::T>,

open spec fn safe_inv(&self) -> bool

{ defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).safe_inv() }

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

impl<Output: OutputBuf, Field, Default, Rest, R, const DER: bool> Serializer<Output, (Default, R)> for DefaultedFmt<Field, Default, Rest, DER>

where Field: SpecByteLen<T = Default> + Serializer<Output, Default>, Rest: SpecByteLen<T = R::V> + Serializer<Output, R>, Default: DeepView<V = Default> + PartialEq + Structural + Copy, R: DeepView,

open spec fn exec_inv(&self) -> bool

{
    &&& self.0.exec_inv()
    &&& self.2.exec_inv()
    &&& forall |v: Default| v.deep_view() == v

}

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

impl<Field, Rest, const DER: bool> SoundParser for DefaultedFmt<Field, Field::PVal, Rest, DER>

where Field: SoundParser, Rest: SoundParser,

open spec fn sound_inv(&self) -> bool

{ defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).sound_inv() }

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

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

impl<Field, Rest, const DER: bool> SpecByteLen for DefaultedFmt<Field, Field::T, Rest, DER>

where Field: SpecByteLen, Rest: SpecByteLen,

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

{ defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).byte_len(v) }

type T = (<Field as SpecByteLen>::T, <Rest as SpecByteLen>::T)

The type of values whose byte length is being computed.

impl<Field, Rest, const DER: bool> SpecParser for DefaultedFmt<Field, Field::PVal, Rest, DER>

where Field: SpecByteLen + SpecParser<PVal = Field::T>, Rest: SpecByteLen + SpecParser<PVal = Rest::T>,

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

{ defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).spec_parse(ibuf) }

type PVal = (<Field as SpecParser>::PVal, <Rest as SpecParser>::PVal)

The type of parsed values.

impl<Field, Rest, const DER: bool> SpecSerializer for DefaultedFmt<Field, Field::SVal, Rest, DER>

where Field: SpecByteLen + SpecSerializer<SVal = Field::T>, Rest: SpecByteLen + SpecSerializer<SVal = Rest::T>,

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

{ defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).spec_serialize(v) }

type SVal = (<Field as SpecSerializer>::SVal, <Rest as SpecSerializer>::SVal)

The type of values to be serialized.

impl<Field, Rest, const DER: bool> SpecSerializerDps for DefaultedFmt<Field, Field::SValue, Rest, DER>

where Field: SpecByteLen + SpecSerializerDps<SValue = Field::T>, Rest: SpecByteLen + SpecSerializerDps<SValue = Rest::T>,

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

{ defaulted_fmt::<Field, Rest, DER>(self.0, self.1, self.2).spec_serialize_dps(v, obuf) }

type SValue = (<Field as SpecSerializerDps>::SValue, <Rest as SpecSerializerDps>::SValue)

The type of values to be serialized.

impl<Field: Copy, Default: Copy, Rest: Copy, const DER: bool> Copy for DefaultedFmt<Field, Default, Rest, DER>