Struct BitStringSpec 

pub struct BitStringSpec {
    pub unused: u8,
    pub bits: Seq<u8>,
}

Fields

unused: u8

bits: Seq<u8>

Implementations

impl BitStringSpec

pub open spec fn wf<const DER: bool>(&self) -> bool

{
    &&& self.unused <= 7
    &&& (self.bits.len() == 0 ==> self.unused == 0)
    &&& (DER
        ==> (self.bits.len() > 0 ==> self.bits.last().trailing_zeros() >= self.unused))

}