Struct Const 

pub struct Const<Inner, Value>(pub Inner, pub Value);

Constant-value combinator: matches a specific constant value.

Parsing semantics: parses with inner and succeeds only if the result equals the expected value. The matched constant value itself is returned.

Implements AdmitsUniqueVal.

Tuple Fields

0: Inner

1: Value

Trait Implementations

impl<const N: usize> AdmitsUniqueVal for Const<Fixed<N>, [u8; N]>

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

impl<Inner> AdmitsUniqueVal for Const<Inner, Inner::Val>

where Inner: Consistency,

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

impl<const N: usize> ByteLen<[u8; N]> for Const<Fixed<N>, [u8; N]>

open spec fn exec_inv(&self) -> bool

{ true }

exec fn length(&self, _v: &[u8; N]) -> len : usize

impl<Inner, V, T> ByteLen<T> for Const<Inner, V>

where T: DeepView<V = V>, Inner: SpecByteLen<T = V> + ByteLen<T>,

open spec fn exec_inv(&self) -> bool

{ self.0.exec_inv() }

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

impl<Inner: Clone, Value: Clone> Clone for Const<Inner, Value>

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

ensures

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

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

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

Performs copy-assignment from source.

impl<const N: usize> Consistency for Const<Fixed<N>, [u8; N]>

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

{
    &&& self.0.consistent(v)
    &&& v == self.1@

}

type Val = Seq<u8>

The type of values whose consistency is being checked.

impl<Inner> Consistency for Const<Inner, Inner::Val>

where Inner: Consistency,

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

{
    &&& self.0.consistent(v)
    &&& v == self.1

}

type Val = <Inner as Consistency>::Val

The type of values whose consistency is being checked.

impl<const N: usize> EquivSerializers for Const<Fixed<N>, [u8; N]>

open spec fn equiv_inv(&self) -> bool

{ self.0.equiv_inv() }

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

impl<Inner> EquivSerializers for Const<Inner, Inner::SVal>

where Inner: EquivSerializers,

open spec fn equiv_inv(&self) -> bool

{ self.0.equiv_inv() }

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

impl<const N: usize> EquivSerializersGeneral for Const<Fixed<N>, [u8; N]>

open spec fn equiv_general_inv(&self) -> bool

{ self.0.equiv_general_inv() }

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

impl<Inner> EquivSerializersGeneral for Const<Inner, Inner::SVal>

where Inner: EquivSerializersGeneral,

open spec fn equiv_general_inv(&self) -> bool

{ self.0.equiv_general_inv() }

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

impl<const N: usize> GoodSerializer for Const<Fixed<N>, [u8; N]>

open spec fn serialize_inv(&self) -> bool

{ self.0.serialize_inv() }

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

impl<Inner> GoodSerializer for Const<Inner, Inner::SVal>

where Inner: GoodSerializer,

open spec fn serialize_inv(&self) -> bool

{ self.0.serialize_inv() }

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

impl HasAsn1Start for Const<TagFmt, Tag>

A constant ASN.1 tag has the exact start domain of its required tag value.

open spec fn asn1_start(&self) -> Asn1StartDomain

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

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

impl<const N: usize> MinMaxByteLen for Const<Fixed<N>, [u8; N]>

open spec fn min(&self) -> nat

{ self.0.min() }

open spec fn max(&self) -> nat

{ self.0.max() }

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

impl<Inner> MinMaxByteLen for Const<Inner, Inner::T>

where Inner: MinMaxByteLen,

open spec fn min(&self) -> nat

{ self.0.min() }

open spec fn max(&self) -> nat

{ self.0.max() }

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

impl<const N: usize> NoLookAhead for Const<Fixed<N>, [u8; N]>

open spec fn no_lookahead_inv(&self) -> bool

{ self.0.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: NoLookAhead> NoLookAhead for Const<Inner, Inner::PVal>

open spec fn no_lookahead_inv(&self) -> bool

{ self.0.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<const N: usize> NonMalleable for Const<Fixed<N>, [u8; N]>

open spec fn nonmal_inv(&self) -> bool

{ self.0.nonmal_inv() }

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

impl<Inner: NonMalleable> NonMalleable for Const<Inner, Inner::PVal>

open spec fn nonmal_inv(&self) -> bool

{ self.0.nonmal_inv() }

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

impl<const N: usize> NonTailFmt for Const<Fixed<N>, [u8; N]>

open spec fn serialize_dps_inv(&self) -> bool

{ self.0.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<Inner> NonTailFmt for Const<Inner, Inner::SValue>

where Inner: NonTailFmt,

open spec fn serialize_dps_inv(&self) -> bool

{ self.0.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<const N: usize> Parser<&[u8]> for Const<Fixed<N>, [u8; N]>

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

type PT = [u8; N]

Executable value returned by this parser.

fn exec_inv(&self) -> bool

impl<I, Inner, T> Parser<I> for Const<Inner, T>

where I: InputBuf, Inner: Parser<I, PT = T, PVal = T>, T: DeepView<V = T> + PartialEq + Structural,

open spec fn exec_inv(&self) -> bool

{
    &&& self.0.exec_inv()
    &&& forall |v: Inner::PVal| v.deep_view() == v

}

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

type PT = <Inner as SpecParser>::PVal

Executable value returned by this parser.

impl<const N: usize> Prepare<[u8; N]> for Const<Fixed<N>, [u8; N]>

exec fn prepare(&self, v: &[u8; N]) -> checked : Result<usize, PreSerializeError>

fn exec_inv(&self) -> bool

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

where T: DeepView<V = T> + PartialEq + Structural, Inner: Prepare<T>,

open spec fn exec_inv(&self) -> bool

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

}

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

impl<const N: usize> Productive for Const<Fixed<N>, [u8; N]>

open spec fn productive_inv(&self) -> bool

{ self.0.productive_inv() }

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

impl<Inner: Productive> Productive for Const<Inner, Inner::PVal>

open spec fn productive_inv(&self) -> bool

{ self.0.productive_inv() }

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

impl<const N: usize> SPRoundTripDps for Const<Fixed<N>, [u8; N]>

open spec fn unambiguous(&self) -> bool

{ self.0.unambiguous() }

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

impl<Inner: SPRoundTripDps> SPRoundTripDps for Const<Inner, Inner::PVal>

open spec fn unambiguous(&self) -> bool

{ self.0.unambiguous() }

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

impl<const N: usize> SafeParser for Const<Fixed<N>, [u8; N]>

open spec fn safe_inv(&self) -> bool

{ self.0.safe_inv() }

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

impl<Inner> SafeParser for Const<Inner, Inner::PVal>

where Inner: SafeParser,

open spec fn safe_inv(&self) -> bool

{ self.0.safe_inv() }

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

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

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

open spec fn exec_inv(&self) -> bool

{ self.0.exec_inv() }

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

impl<const N: usize> SoundParser for Const<Fixed<N>, [u8; N]>

open spec fn sound_inv(&self) -> bool

{ 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<Inner> SoundParser for Const<Inner, Inner::PVal>

where Inner: SoundParser,

open spec fn sound_inv(&self) -> bool

{ 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<const N: usize> SpecByteLen for Const<Fixed<N>, [u8; N]>

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

{ self.0.byte_len(v) }

type T = Seq<u8>

The type of values whose byte length is being computed.

impl<Inner> SpecByteLen for Const<Inner, Inner::T>

where Inner: SpecByteLen,

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

{ self.0.byte_len(v) }

type T = <Inner as SpecByteLen>::T

The type of values whose byte length is being computed.

impl<const N: usize> SpecParser for Const<Fixed<N>, [u8; N]>

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

{
    match self.0.spec_parse(ibuf) {
        Some((n, v)) if v == self.1@ => Some((n, v)),
        _ => None,
    }
}

type PVal = Seq<u8>

The type of parsed values.

impl<Inner> SpecParser for Const<Inner, Inner::PVal>

where Inner: SpecParser,

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

{
    match self.0.spec_parse(ibuf) {
        Some((n, v)) if v == self.1 => Some((n, v)),
        _ => None,
    }
}

type PVal = <Inner as SpecParser>::PVal

The type of parsed values.

impl<const N: usize> SpecSerializer for Const<Fixed<N>, [u8; N]>

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

{ self.0.spec_serialize(v) }

type SVal = Seq<u8>

The type of values to be serialized.

impl<Inner> SpecSerializer for Const<Inner, Inner::SVal>

where Inner: SpecSerializer,

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

{ self.0.spec_serialize(v) }

type SVal = <Inner as SpecSerializer>::SVal

The type of values to be serialized.

impl<const N: usize> SpecSerializerDps for Const<Fixed<N>, [u8; N]>

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

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

type SValue = Seq<u8>

The type of values to be serialized.

impl<Inner> SpecSerializerDps for Const<Inner, Inner::SValue>

where Inner: SpecSerializerDps,

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

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

type SValue = <Inner as SpecSerializerDps>::SValue

The type of values to be serialized.

impl<const N: usize> StaticByteLen for Const<Fixed<N>, [u8; N]>

open spec fn static_byte_len() -> nat

{ Fixed::<N>::static_byte_len() }

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

impl<Inner> StaticByteLen for Const<Inner, Inner::T>

where Inner: StaticByteLen,

open spec fn static_byte_len() -> nat

{ Inner::static_byte_len() }

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

impl<const N: usize> ValueByteLen for Const<Fixed<N>, [u8; N]>

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

{ Fixed::<N>::value_byte_len(v) }

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

impl<Inner> ValueByteLen for Const<Inner, Inner::T>

where Inner: ValueByteLen,

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, Value: Copy> Copy for Const<Inner, Value>