Struct BoolFmt 

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

ASN.1 BOOLEAN format.

When DER = true (the default), this is the canonical DER form: FALSE = 0x00, TRUE = 0xFF.

When DER = false, this is the more permissive BER form: FALSE = 0x00, TRUE = any non-zero byte.

Trait Implementations

impl<const DER: bool> ByteLen<bool> for BoolFmt<DER>

exec fn length(&self, _v: &bool) -> usize

fn exec_inv(&self) -> bool

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

fn clone(&self) -> BoolFmt<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 BoolFmt<DER>

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

{ bool_fmt::<DER>().consistent(v) }

type Val = bool

The type of values whose consistency is being checked.

impl DerOrd<bool> for BoolFmt<true>

proof fn lemma_der_serialize_len(&self, value: bool)

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

{ if state { Seq::empty() } else { self.spec_serialize(value) } }

open spec fn der_state_valid(&self, _value: bool, _state: bool) -> bool

{ true }

exec fn der_start(&self, b: &bool) -> state : bool

exec fn der_next(&self, b: &bool, state: &mut bool) -> next : Option<u8>

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

impl DerState for BoolFmt<true>

type State = bool

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

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

fn equiv_inv(&self) -> bool

impl<const DER: bool> EquivSerializersGeneral for BoolFmt<DER>

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

fn equiv_general_inv(&self) -> bool

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

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

fn serialize_inv(&self) -> bool

impl<const DER: bool> MinMaxByteLen for BoolFmt<DER>

open spec fn min(&self) -> nat

{ BOOL_BYTE_LEN as nat }

open spec fn max(&self) -> nat

{ BOOL_BYTE_LEN as nat }

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

impl<const DER: bool> NoLookAhead for BoolFmt<DER>

proof fn lemma_no_lookahead(&self, i1: Seq<u8>, i2: Seq<u8>)

fn no_lookahead_inv(&self) -> bool

fn corollary_non_extensible(&self, i1: Seq<u8>, i2: Seq<u8>)

impl NonMalleable for BoolFmt<true>

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

fn nonmal_inv(&self) -> bool

impl<const DER: bool> NonTailFmt for BoolFmt<DER>

proof fn lemma_serialize_dps_prepend(&self, v: bool, obuf: Seq<u8>)

proof fn lemma_serialize_dps_len(&self, v: bool, obuf: Seq<u8>)

fn serialize_dps_inv(&self) -> bool

impl<const DER: bool> Parser<&[u8]> for BoolFmt<DER>

exec fn parse(&self, ibuf: &&[u8]) -> PResult<bool>

type PT = bool

Executable value returned by this parser.

fn exec_inv(&self) -> bool

impl<const DER: bool> Prepare<bool> for BoolFmt<DER>

exec fn prepare(&self, _v: &bool) -> Result<usize, PreSerializeError>

fn exec_inv(&self) -> bool

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

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

fn productive_inv(&self) -> bool

impl<const DER: bool> SPRoundTripDps for BoolFmt<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 BoolFmt<DER>

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

fn safe_inv(&self) -> bool

impl<Output: OutputBuf, const DER: bool> Serializer<Output, bool> for BoolFmt<DER>

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

fn exec_inv(&self) -> bool

impl<const DER: bool> SoundParser for BoolFmt<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 BoolFmt<DER>

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

{ BOOL_BYTE_LEN as nat }

type T = bool

The type of values whose byte length is being computed.

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

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

{ bool_fmt::<DER>().spec_parse(ibuf) }

type PVal = bool

The type of parsed values.

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

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

{ bool_fmt::<DER>().spec_serialize(v) }

type SVal = bool

The type of values to be serialized.

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

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

{ bool_fmt::<DER>().spec_serialize_dps(v, obuf) }

type SValue = bool

The type of values to be serialized.

impl<const DER: bool> StaticByteLen for BoolFmt<DER>

open spec fn static_byte_len() -> nat

{ BOOL_BYTE_LEN as nat }

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

impl<const DER: bool> ValueByteLen for BoolFmt<DER>

open spec fn value_byte_len(_v: Self::T) -> nat

{ BOOL_BYTE_LEN as nat }

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

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