Struct BitString 

pub struct BitString<'a, const DER: bool = true> { /* private fields */ }

The ASN.1 BIT STRING.

Represented as: (number_of_unused_bits_in_final_octet, payload_octets).

Implementations

impl<'a, const DER: bool> BitString<'a, DER>

pub exec fn new(unused: u8, bits: &'a [u8]) -> bs : Self

requires

unused <= 7,

bits.len() == 0 ==> unused == 0,

DER ==> (bits.len() > 0 ==> bits@.last().trailing_zeros() >= unused),

ensures

(bs.deep_view()
    == BitStringSpec {
        unused,
        bits: bits.deep_view(),
    }),

pub exec fn unused(&self) -> unused : u8

ensures

unused == self.deep_view().unused,

self.deep_view().wf::<DER>(),

pub exec fn bits(&self) -> bits : &'a [u8]

ensures

bits.deep_view() == self.deep_view().bits,

Trait Implementations

impl<'i, const DER: bool> ByteLen<BitString<'i, DER>> for BitStringFmt<DER>

exec fn length(&self, v: &BitString<'i, DER>) -> usize

fn exec_inv(&self) -> bool

impl<'a, const DER: bool> DeepView for BitString<'a, DER>

closed spec fn deep_view(&self) -> Self::V

type V = BitStringSpec

impl<'a> DerOrd<BitString<'a>> for BitStringFmt<true>

proof fn lemma_der_serialize_len(&self, value: BitStringSpec)

open spec fn der_remaining( &self, value: BitStringSpec, state: PairDerState<bool, BytesDerState>, ) -> Seq<u8>

{
    <Pair<
        U8,
        Tail,
    > as DerOrd<
        (u8, &'a [u8]),
    >>::der_remaining(&Pair(U8, Tail), (value.unused, value.bits), state)
}

open spec fn der_state_valid( &self, value: BitStringSpec, state: PairDerState<bool, BytesDerState>, ) -> bool

{
    <Pair<
        U8,
        Tail,
    > as DerOrd<
        (u8, &'a [u8]),
    >>::der_state_valid(&Pair(U8, Tail), (value.unused, value.bits), state)
}

exec fn der_start( &self, b: &BitString<'a, true>, ) -> state : PairDerState<bool, BytesDerState>

exec fn der_next( &self, b: &BitString<'a, true>, state: &mut PairDerState<bool, BytesDerState>, ) -> next : Option<u8>

fn der_leq(&self, left: &T, right: &T) -> bool

impl<'i, const DER: bool> Prepare<BitString<'i, DER>> for BitStringFmt<DER>

exec fn prepare(&self, v: &BitString<'i, DER>) -> Result<usize, PreSerializeError>

fn exec_inv(&self) -> bool

impl<'i, Output: OutputBuf, const DER: bool> Serializer<Output, BitString<'i, DER>> for BitStringFmt<DER>

exec fn serialize_into(&self, v: &BitString<'i, DER>, obuf: &mut Output)

fn exec_inv(&self) -> bool