Type Alias ParserSpecs 

pub type ParserSpecs<SpecP, Cnstcy, Blen> = (SpecP, Cnstcy, Blen);

Bundled triple of parser, consistency, and byte-length spec functions.

Trait Implementations

impl<SpecP, Cnstcy, Blen> Consistency for ParserSpecs<SpecP, Cnstcy, Blen>

where Blen: SpecByteLen, SpecP: SpecParser<PVal = Blen::T>, Cnstcy: Consistency<Val = Blen::T>,

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

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

type Val = <Blen as SpecByteLen>::T

The type of values whose consistency is being checked.

impl<SpecP, Cnstcy, Blen> NonMalleable for ParserSpecs<SpecP, Cnstcy, Blen>

where Blen: SpecByteLen, SpecP: SpecParser<PVal = Blen::T>, Cnstcy: Consistency<Val = Blen::T>,

open spec fn nonmal_inv(&self) -> bool

{
    let (p, _, _) = *self;
    let p_fn = |ibuf| p.spec_parse(ibuf);
    non_malleable_parser(p_fn)
}

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

impl<SpecP, Cnstcy, Blen> SpecByteLen for ParserSpecs<SpecP, Cnstcy, Blen>

where Blen: SpecByteLen, SpecP: SpecParser<PVal = Blen::T>, Cnstcy: Consistency<Val = Blen::T>,

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

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

type T = <Blen as SpecByteLen>::T

The type of values whose byte length is being computed.

impl<SpecP, Cnstcy, Blen> SpecParser for ParserSpecs<SpecP, Cnstcy, Blen>

where Blen: SpecByteLen, SpecP: SpecParser<PVal = Blen::T>, Cnstcy: Consistency<Val = Blen::T>,

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

{ (self.0).spec_parse(ibuf) }

type PVal = <Blen as SpecByteLen>::T

The type of parsed values.