Struct BitStringFmt 

pub struct BitStringFmt<const DER: bool = true>;

ASN.1 BIT STRING contents format.

When DER = true (the default), only the canonical DER form is accepted, which requires the trailing unused bits to be zero.

When DER = false, the parser allows any value for the trailing unused 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 ByteLen<BitStringOwned> for BitStringFmt<false>

Available on crate feature alloc only.

exec fn length(&self, v: &BitStringOwned) -> usize

fn exec_inv(&self) -> bool

impl<const DER: bool> Clone for BitStringFmt<DER>

fn clone(&self) -> BitStringFmt<DER>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<const DER: bool> Consistency for BitStringFmt<DER>

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

type Val = BitStringSpec

The type of values whose consistency is being checked.

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 DerState for BitStringFmt<true>

type State = PairDerState<bool, BytesDerState>

impl<const DER: bool> EquivSerializers for BitStringFmt<DER>

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

fn equiv_inv(&self) -> bool

impl<const DER: bool> GoodSerializer for BitStringFmt<DER>

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

fn serialize_inv(&self) -> bool

impl<const DER: bool> NonMalleable for BitStringFmt<DER>

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

fn nonmal_inv(&self) -> bool

impl<'i, const DER: bool> Parser<&'i [u8]> for BitStringFmt<DER>

exec fn parse(&self, ibuf: &&'i [u8]) -> PResult<Self::PT>

type PT = BitString<'i, DER>

Executable value returned by this parser.

fn exec_inv(&self) -> 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 Prepare<BitStringOwned> for BitStringFmt<false>

Available on crate feature alloc only.

exec fn prepare(&self, v: &BitStringOwned) -> Result<usize, PreSerializeError>

fn exec_inv(&self) -> bool

impl<const DER: bool> Productive for BitStringFmt<DER>

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

fn productive_inv(&self) -> bool

impl<const DER: bool> SPRoundTripDps for BitStringFmt<DER>

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

fn unambiguous(&self) -> bool

impl<const DER: bool> SafeParser for BitStringFmt<DER>

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

fn safe_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

impl<Output: OutputBuf> Serializer<Output, BitStringOwned> for BitStringFmt<false>

Available on crate feature alloc only.

exec fn serialize_into(&self, v: &BitStringOwned, obuf: &mut Output)

fn exec_inv(&self) -> bool

impl<const DER: bool> SoundParser for BitStringFmt<DER>

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

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

fn sound_inv(&self) -> bool

impl<const DER: bool> SpecByteLen for BitStringFmt<DER>

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

type T = BitStringSpec

The type of values whose byte length is being computed.

impl<const DER: bool> SpecParser for BitStringFmt<DER>

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

type PVal = BitStringSpec

The type of parsed values.

impl<const DER: bool> SpecSerializer for BitStringFmt<DER>

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

type SVal = BitStringSpec

The type of values to be serialized.

impl<const DER: bool> SpecSerializerDps for BitStringFmt<DER>

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

type SValue = BitStringSpec

The type of values to be serialized.

impl<const DER: bool> Copy for BitStringFmt<DER>