Struct Alt 

pub struct Alt<A, B, const NONDETERMINISTIC: bool = false>(pub A, pub B);

Ordered alternative combinator.

Parsing semantics: like Choice, but both branches consume/produce the same type. The result is returned directly without a Sum wrapper.

Serialization semantics: if only one branch is consistent with a value, that branch is used. If both branches are consistent, serialization is intentionally underspecified and may use either branch.

Consistency

A value v is consistent with Alt(A, B) iff it is consistent with A OR B.

Unambiguity

Requires disjoint_domains(A, B).

Malleability

This combinator introduces malleability by default. Non-malleability can be recovered if A is disjoint from B (see disjoint_values).

Tuple Fields

0: A

1: B

Implementations

impl<const NONDETERMINISTIC: bool, A, B> Alt<A, B, NONDETERMINISTIC>

where A: Consistency, B: Consistency<Val = A::Val>,

pub open spec fn choose_left(&self, v: A::Val) -> bool

{
    if NONDETERMINISTIC {
        arbitrary_or_left(self.0.consistent(v), self.1.consistent(v))
    } else {
        self.0.consistent(v)
    }
}

For non-deterministic Alt: If exactly one branch accepts v, this returns that branch. If both accept v, the choice is unspecified.

For deterministic Alt, this returns true iff the left branch accepts v.

Trait Implementations

impl<A: Clone, B: Clone, const NONDETERMINISTIC: bool> Clone for Alt<A, B, NONDETERMINISTIC>

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

ensures

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

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

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

Performs copy-assignment from source.

impl<const NONDETERMINISTIC: bool, A: Consistency, B: Consistency<Val = A::Val>> Consistency for Alt<A, B, NONDETERMINISTIC>

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

{ self.0.consistent(v) || self.1.consistent(v) }

type Val = <A as Consistency>::Val

The type of values whose consistency is being checked.

impl<const NONDETERMINISTIC: bool, A, B> EquivSerializers for Alt<A, B, NONDETERMINISTIC>

where A: EquivSerializers + Consistency<Val = A::SVal>, B: EquivSerializers<SVal = A::SVal> + Consistency<Val = B::SVal>,

open spec fn equiv_inv(&self) -> bool

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

}

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

impl<const NONDETERMINISTIC: bool, A, B> EquivSerializersGeneral for Alt<A, B, NONDETERMINISTIC>

where A: EquivSerializersGeneral + Consistency<Val = A::SVal>, B: EquivSerializersGeneral<SVal = A::SVal> + Consistency<Val = B::SVal>,

open spec fn equiv_general_inv(&self) -> bool

{
    &&& self.0.equiv_general_inv()
    &&& self.1.equiv_general_inv()

}

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

impl<const NONDETERMINISTIC: bool, A, B> GoodSerializer for Alt<A, B, NONDETERMINISTIC>

where A: GoodSerializer + Consistency<Val = A::SVal>, B: GoodSerializer<T = A::T> + Consistency<Val = B::SVal>,

open spec fn serialize_inv(&self) -> bool

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

}

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

impl<const NONDETERMINISTIC: bool, Left: HasAsn1Start, Right: HasAsn1Start<PVal = Left::PVal>> HasAsn1Start for Alt<Left, Right, NONDETERMINISTIC>

Ordered alternatives have the same accepted start union as structural choices.

open spec fn asn1_start(&self) -> Asn1StartDomain

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

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

impl<const NONDETERMINISTIC: bool, A, B> MinMaxByteLen for Alt<A, B, NONDETERMINISTIC>

where A: MinMaxByteLen, B: MinMaxByteLen<T = A::T>,

open spec fn min(&self) -> nat

{ if self.0.min() <= self.1.min() { self.0.min() } else { self.1.min() } }

open spec fn max(&self) -> nat

{ if self.0.max() <= self.1.max() { self.1.max() } else { self.0.max() } }

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

impl<const NONDETERMINISTIC: bool, A, B> NoLookAhead for Alt<A, B, NONDETERMINISTIC>

where A: NoLookAhead, B: NoLookAhead<PVal = A::PVal>,

open spec fn no_lookahead_inv(&self) -> bool

{
    &&& self.0.no_lookahead_inv()
    &&& self.1.no_lookahead_inv()
    &&& disjoint_domains(self.0, self.1)

}

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 NONDETERMINISTIC: bool, A, B> NonMalleable for Alt<A, B, NONDETERMINISTIC>

where A: SoundParser + NonMalleable, B: SoundParser<T = A::T> + NonMalleable,

open spec fn nonmal_inv(&self) -> bool

{
    &&& self.0.sound_inv()
    &&& self.1.sound_inv()
    &&& self.0.nonmal_inv()
    &&& self.1.nonmal_inv()
    &&& disjoint_values(self.0, self.1)

}

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

impl<const NONDETERMINISTIC: bool, A, B> NonTailFmt for Alt<A, B, NONDETERMINISTIC>

where A: NonTailFmt + Consistency<Val = A::SValue>, B: NonTailFmt<T = A::T> + Consistency<Val = B::SValue>,

open spec fn serialize_dps_inv(&self) -> bool

{
    &&& self.0.serialize_dps_inv()
    &&& 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<const NONDETERMINISTIC: bool, I, A, B> Parser<I> for Alt<A, B, NONDETERMINISTIC>

where I: View<V = Seq<u8>>, A: Parser<I>, B: Parser<I, PVal = A::PVal, PT = A::PT>,

open spec fn exec_inv(&self) -> bool

{
    &&& self.0.exec_inv()
    &&& self.1.exec_inv()

}

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

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

Executable value returned by this parser.

impl<const NONDETERMINISTIC: bool, A, B> Productive for Alt<A, B, NONDETERMINISTIC>

where A: Productive, B: Productive<PVal = A::PVal>,

open spec fn productive_inv(&self) -> bool

{
    &&& self.0.productive_inv()
    &&& self.1.productive_inv()

}

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

impl<const NONDETERMINISTIC: bool, A: SPRoundTripDps, B: SPRoundTripDps<T = A::T>> SPRoundTripDps for Alt<A, B, NONDETERMINISTIC>

open spec fn unambiguous(&self) -> bool

{
    &&& self.0.unambiguous()
    &&& self.1.unambiguous()
    &&& disjoint_domains(self.0, self.1)

}

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

impl<const NONDETERMINISTIC: bool, A, B> SafeParser for Alt<A, B, NONDETERMINISTIC>

where A: SafeParser, B: SafeParser<PVal = A::PVal>,

open spec fn safe_inv(&self) -> bool

{
    &&& self.0.safe_inv()
    &&& self.1.safe_inv()

}

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

impl<const NONDETERMINISTIC: bool, A, B> SoundParser for Alt<A, B, NONDETERMINISTIC>

where A: SoundParser, B: SoundParser<T = A::T>,

open spec fn sound_inv(&self) -> bool

{
    &&& self.0.sound_inv()
    &&& self.1.sound_inv()
    &&& disjoint_values(self.0, self.1)

}

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

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

impl<const NONDETERMINISTIC: bool, A, B> SpecByteLen for Alt<A, B, NONDETERMINISTIC>

where A: SpecByteLen + Consistency<Val = A::T>, B: SpecByteLen<T = A::T> + Consistency<Val = B::T>,

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

{ if self.choose_left(v) { self.0.byte_len(v) } else { self.1.byte_len(v) } }

type T = <A as SpecByteLen>::T

The type of values whose byte length is being computed.

impl<const NONDETERMINISTIC: bool, A: SpecParser, B: SpecParser<PVal = A::PVal>> SpecParser for Alt<A, B, NONDETERMINISTIC>

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

{
    if let None = self.0.spec_parse(ibuf) {
        self.1.spec_parse(ibuf)
    } else {
        self.0.spec_parse(ibuf)
    }
}

type PVal = <A as SpecParser>::PVal

The type of parsed values.

impl<const NONDETERMINISTIC: bool, A, B> SpecSerializer for Alt<A, B, NONDETERMINISTIC>

where A: SpecSerializer + Consistency<Val = A::SVal>, B: SpecSerializer<SVal = A::SVal> + Consistency<Val = B::SVal>,

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

{ if self.choose_left(v) { self.0.spec_serialize(v) } else { self.1.spec_serialize(v) } }

type SVal = <A as SpecSerializer>::SVal

The type of values to be serialized.

impl<const NONDETERMINISTIC: bool, A, B> SpecSerializerDps for Alt<A, B, NONDETERMINISTIC>

where A: SpecSerializerDps + Consistency<Val = A::SValue>, B: SpecSerializerDps<SValue = A::SValue> + Consistency<Val = B::SValue>,

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

{
    if self.choose_left(v) {
        self.0.spec_serialize_dps(v, obuf)
    } else {
        self.1.spec_serialize_dps(v, obuf)
    }
}

type SValue = <A as SpecSerializerDps>::SValue

The type of values to be serialized.

impl<A: Copy, B: Copy, const NONDETERMINISTIC: bool> Copy for Alt<A, B, NONDETERMINISTIC>