Struct Dispatch 

pub struct Dispatch<T, C, const N: usize>(pub T, pub [(T, C); N]);

Dispatch combinator that selects one of N branches based on a “tag” value.

Tuple Fields

0: T

1: [(T, C); N]

Implementations

impl<T, C, const N: usize> Dispatch<T, C, N>

pub open spec fn has_active_branch(&self) -> bool

{ branch_exists(self.0, self.1@) }

pub open spec fn active_branch(&self) -> C

recommends

self.has_active_branch(),

{ self.1[tag_position(self.0, self.1@) as int].1 }

pub proof fn lemma_active_branch_is(&self, idx: nat)

requires

idx < self.1@.len(),

self.1[idx as int].0 == self.0,

unique_branch_match(self.0, self.1@),

ensures

self.has_active_branch(),

self.active_branch() == self.1[idx as int].1,

Trait Implementations

impl<T, C: Consistency, const N: usize> Consistency for Dispatch<T, C, N>

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

{
    &&& self.has_active_branch()
    &&& self.active_branch().consistent(v)

}

type Val = <C as Consistency>::Val

The type of values whose consistency is being checked.

impl<T, C: EquivSerializers, const N: usize> EquivSerializers for Dispatch<T, C, N>

open spec fn equiv_inv(&self) -> bool

{ self.active_branch().equiv_inv() }

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

impl<T, C, const N: usize> EquivSerializersGeneral for Dispatch<T, C, N>

where C: EquivSerializersGeneral,

open spec fn equiv_general_inv(&self) -> bool

{ self.active_branch().equiv_general_inv() }

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

impl<T, C: GoodSerializer, const N: usize> GoodSerializer for Dispatch<T, C, N>

open spec fn serialize_inv(&self) -> bool

{ self.active_branch().serialize_inv() }

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

impl<T, C: MinMaxByteLen, const N: usize> MinMaxByteLen for Dispatch<T, C, N>

open spec fn min(&self) -> nat

{ if self.has_active_branch() { self.active_branch().min() } else { 0 } }

open spec fn max(&self) -> nat

{ if self.has_active_branch() { self.active_branch().max() } else { 0 } }

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

impl<T, C: NoLookAhead, const N: usize> NoLookAhead for Dispatch<T, C, N>

open spec fn no_lookahead_inv(&self) -> bool

{ self.active_branch().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<T, C: NonMalleable, const N: usize> NonMalleable for Dispatch<T, C, N>

open spec fn nonmal_inv(&self) -> bool

{ self.active_branch().nonmal_inv() }

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

impl<T, C: NonTailFmt, const N: usize> NonTailFmt for Dispatch<T, C, N>

open spec fn serialize_dps_inv(&self) -> bool

{ self.active_branch().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<T, C: Productive, const N: usize> Productive for Dispatch<T, C, N>

open spec fn productive_inv(&self) -> bool

{ self.active_branch().productive_inv() }

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

impl<T, C, const N: usize> SPRoundTripDps for Dispatch<T, C, N>

where C: SPRoundTripDps,

open spec fn unambiguous(&self) -> bool

{ self.active_branch().unambiguous() }

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

impl<T, C: SafeParser, const N: usize> SafeParser for Dispatch<T, C, N>

open spec fn safe_inv(&self) -> bool

{ self.active_branch().safe_inv() }

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

impl<T, C: SoundParser, const N: usize> SoundParser for Dispatch<T, C, N>

open spec fn sound_inv(&self) -> bool

{ self.active_branch().sound_inv() }

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

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

impl<T, C: SpecByteLen, const N: usize> SpecByteLen for Dispatch<T, C, N>

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

{ self.active_branch().byte_len(v) }

type T = <C as SpecByteLen>::T

The type of values whose byte length is being computed.

impl<T, C: SpecParser, const N: usize> SpecParser for Dispatch<T, C, N>

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

{ if self.has_active_branch() { self.active_branch().spec_parse(ibuf) } else { None } }

type PVal = <C as SpecParser>::PVal

The type of parsed values.

impl<T, C: SpecSerializer, const N: usize> SpecSerializer for Dispatch<T, C, N>

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

{ self.active_branch().spec_serialize(v) }

type SVal = <C as SpecSerializer>::SVal

The type of values to be serialized.

impl<T, C: SpecSerializerDps, const N: usize> SpecSerializerDps for Dispatch<T, C, N>

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

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

type SValue = <C as SpecSerializerDps>::SValue

The type of values to be serialized.

impl<T, C: StaticByteLen, const N: usize> StaticByteLen for Dispatch<T, C, N>

open spec fn static_byte_len() -> nat

{ C::static_byte_len() }

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

impl<T, C: ValueByteLen, const N: usize> ValueByteLen for Dispatch<T, C, N>

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

{ C::value_byte_len(v) }

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