Struct Bits 

pub struct Bits<Repr: SpecByteLen, Tuple, Nominal> {
    pub repr: Repr,
    pub unpack: FnSpec<(Repr::T,), Tuple>,
    pub pack: FnSpec<(Tuple,), Repr::T>,
    pub refinement: PredFnSpec<Tuple>,
    pub ctor: FnSpec<(Tuple,), Nominal>,
    pub dtor: FnSpec<(Nominal,), Tuple>,
    pub consistent: PredFnSpec<Nominal>,
}

Packs a tuple of logical bitfield values into one fixed-width integer representation.

Generated Vest bitfield formats use the functions stored here to unpack the wire integer, validate the structural tuple, construct the public nominal value, and perform the inverse operation during serialization.

Fields

repr: Repr

Integer format that reads and writes the complete bitfield word.

unpack: FnSpec<(Repr::T,), Tuple>

Splits the representation into its structural field tuple.

pack: FnSpec<(Tuple,), Repr::T>

Packs the structural field tuple into the representation.

refinement: PredFnSpec<Tuple>

Predicate enforcing field widths and reserved-bit constraints.

ctor: FnSpec<(Tuple,), Nominal>

Constructs the public nominal value from structural fields.

dtor: FnSpec<(Nominal,), Tuple>

Projects a public nominal value back to structural fields.

consistent: PredFnSpec<Nominal>

Additional consistency predicate for nominal values.

Trait Implementations

impl<Repr, Tuple, Nominal> Consistency for Bits<Repr, Tuple, Nominal>

where Repr: SpecByteLen + Consistency<Val = Repr::T>,

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

{
    let fmt = bits(
        self.repr,
        self.unpack,
        self.pack,
        self.refinement,
        self.ctor,
        self.dtor,
    );
    &&& fmt.consistent(v)
    &&& (self.consistent)(v)

}

type Val = Nominal

The type of values whose consistency is being checked.

impl<Repr, Tuple, Nominal> EquivSerializers for Bits<Repr, Tuple, Nominal>

where Repr: SpecByteLen + EquivSerializers<SVal = Repr::T>,

open spec fn equiv_inv(&self) -> bool

{
    let fmt = bits(
        self.repr,
        self.unpack,
        self.pack,
        self.refinement,
        self.ctor,
        self.dtor,
    );
    fmt.equiv_inv()
}

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

impl<Repr, Tuple, Nominal> EquivSerializersGeneral for Bits<Repr, Tuple, Nominal>

where Repr: SpecByteLen + EquivSerializersGeneral<SVal = Repr::T>,

open spec fn equiv_general_inv(&self) -> bool

{
    let fmt = bits(
        self.repr,
        self.unpack,
        self.pack,
        self.refinement,
        self.ctor,
        self.dtor,
    );
    fmt.equiv_general_inv()
}

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

impl<Repr, Tuple, Nominal> GoodSerializer for Bits<Repr, Tuple, Nominal>

where Repr: GoodSerializer,

open spec fn serialize_inv(&self) -> bool

{
    let fmt = bits(
        self.repr,
        self.unpack,
        self.pack,
        self.refinement,
        self.ctor,
        self.dtor,
    );
    fmt.serialize_inv()
}

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

impl<Repr, Tuple, Nominal> MinMaxByteLen for Bits<Repr, Tuple, Nominal>

where Repr: MinMaxByteLen,

open spec fn min(&self) -> nat

{
    let fmt = bits(
        self.repr,
        self.unpack,
        self.pack,
        self.refinement,
        self.ctor,
        self.dtor,
    );
    fmt.min()
}

open spec fn max(&self) -> nat

{
    let fmt = bits(
        self.repr,
        self.unpack,
        self.pack,
        self.refinement,
        self.ctor,
        self.dtor,
    );
    fmt.max()
}

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

impl<Repr, Tuple, Nominal> NoLookAhead for Bits<Repr, Tuple, Nominal>

where Repr: SpecByteLen + NoLookAhead<PVal = Repr::T>,

open spec fn no_lookahead_inv(&self) -> bool

{
    let fmt = bits(
        self.repr,
        self.unpack,
        self.pack,
        self.refinement,
        self.ctor,
        self.dtor,
    );
    fmt.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<Repr, Tuple, Nominal> NonMalleable for Bits<Repr, Tuple, Nominal>

where Repr: SpecByteLen + SoundParser + NonMalleable<PVal = Repr::T>,

open spec fn nonmal_inv(&self) -> bool

{
    let fmt = bits(
        self.repr,
        self.unpack,
        self.pack,
        self.refinement,
        self.ctor,
        self.dtor,
    );
    fmt.nonmal_inv()
}

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

impl<Repr, Tuple, Nominal> NonTailFmt for Bits<Repr, Tuple, Nominal>

where Repr: NonTailFmt,

open spec fn serialize_dps_inv(&self) -> bool

{
    let fmt = bits(
        self.repr,
        self.unpack,
        self.pack,
        self.refinement,
        self.ctor,
        self.dtor,
    );
    fmt.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<Repr, Tuple, Nominal> Productive for Bits<Repr, Tuple, Nominal>

where Repr: SpecByteLen + Productive<PVal = Repr::T>,

open spec fn productive_inv(&self) -> bool

{
    let fmt = bits(
        self.repr,
        self.unpack,
        self.pack,
        self.refinement,
        self.ctor,
        self.dtor,
    );
    fmt.productive_inv()
}

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

impl<Repr, Tuple, Nominal> SPRoundTripDps for Bits<Repr, Tuple, Nominal>

where Repr: SPRoundTripDps,

open spec fn unambiguous(&self) -> bool

{
    &&& self.repr.unambiguous()
    &&& forall |unpacked: Tuple| {
        (#[trigger] (self.consistent)((self.ctor)(unpacked))
            && (self.refinement)(unpacked))
            ==> (self.unpack)((self.pack)(unpacked)) == unpacked
    }
    &&& forall |t: Nominal| {
        #[trigger] (self.consistent)(t) ==> (self.ctor)((self.dtor)(t)) == t
    }

}

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

impl<Repr, Tuple, Nominal> SafeParser for Bits<Repr, Tuple, Nominal>

where Repr: SpecByteLen + SafeParser<PVal = Repr::T>,

open spec fn safe_inv(&self) -> bool

{
    let fmt = bits(
        self.repr,
        self.unpack,
        self.pack,
        self.refinement,
        self.ctor,
        self.dtor,
    );
    fmt.safe_inv()
}

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

impl<Repr, Tuple, Nominal> SoundParser for Bits<Repr, Tuple, Nominal>

where Repr: SoundParser,

open spec fn sound_inv(&self) -> bool

{
    let fmt = bits(
        self.repr,
        self.unpack,
        self.pack,
        self.refinement,
        self.ctor,
        self.dtor,
    );
    &&& fmt.sound_inv()
    &&& forall |ibuf| (
        #[trigger]
        fmt.spec_parse(ibuf) matches Some((_, v)) ==> (self.consistent)(v)
    )

}

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

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

impl<Repr, Tuple, Nominal> SpecByteLen for Bits<Repr, Tuple, Nominal>

where Repr: SpecByteLen,

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

{
    let fmt = bits(
        self.repr,
        self.unpack,
        self.pack,
        self.refinement,
        self.ctor,
        self.dtor,
    );
    fmt.byte_len(v)
}

type T = Nominal

The type of values whose byte length is being computed.

impl<Repr, Tuple, Nominal> SpecParser for Bits<Repr, Tuple, Nominal>

where Repr: SpecByteLen + SpecParser<PVal = Repr::T>,

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

{
    let fmt = bits(
        self.repr,
        self.unpack,
        self.pack,
        self.refinement,
        self.ctor,
        self.dtor,
    );
    fmt.spec_parse(ibuf)
}

type PVal = Nominal

The type of parsed values.

impl<Repr, Tuple, Nominal> SpecSerializer for Bits<Repr, Tuple, Nominal>

where Repr: SpecByteLen + SpecSerializer<SVal = Repr::T>,

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

{
    let fmt = bits(
        self.repr,
        self.unpack,
        self.pack,
        self.refinement,
        self.ctor,
        self.dtor,
    );
    fmt.spec_serialize(v)
}

type SVal = Nominal

The type of values to be serialized.

impl<Repr, Tuple, Nominal> SpecSerializerDps for Bits<Repr, Tuple, Nominal>

where Repr: SpecByteLen + SpecSerializerDps<SValue = Repr::T>,

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

{
    let fmt = bits(
        self.repr,
        self.unpack,
        self.pack,
        self.refinement,
        self.ctor,
        self.dtor,
    );
    fmt.spec_serialize_dps(v, obuf)
}

type SValue = Nominal

The type of values to be serialized.

impl<Repr, Tuple, Nominal> StaticByteLen for Bits<Repr, Tuple, Nominal>

where Repr: StaticByteLen,

open spec fn static_byte_len() -> nat

{ Repr::static_byte_len() }

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