Struct BerAnyFmt 

pub struct BerAnyFmt<const LIMIT: usize>;

BER ANY/open type with bounded nesting for indefinite-length constructed values.

Parsing accepts definite values and recursively framed indefinite constructed values. Serialization is normalized to a definite-length encoding.

Trait Implementations

impl<const LIMIT: usize> ByteLen<AnyOwned> for BerAnyFmt<LIMIT>

Available on crate feature alloc only.

exec fn length(&self, value: &AnyOwned) -> usize

fn exec_inv(&self) -> bool

impl<const LIMIT: usize> Clone for BerAnyFmt<LIMIT>

fn clone(&self) -> BerAnyFmt<LIMIT>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<const LIMIT: usize> Consistency for BerAnyFmt<LIMIT>

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

{ AnyFmt::<BER>.consistent(value) }

type Val = AnySpec

The type of values whose consistency is being checked.

impl<const LIMIT: usize> EquivSerializers for BerAnyFmt<LIMIT>

proof fn lemma_serialize_equiv_on_empty(&self, value: AnySpec)

fn equiv_inv(&self) -> bool

impl<const LIMIT: usize> EquivSerializersGeneral for BerAnyFmt<LIMIT>

proof fn lemma_serialize_equiv(&self, value: AnySpec, obuf: Seq<u8>)

fn equiv_general_inv(&self) -> bool

impl<const LIMIT: usize> GoodSerializer for BerAnyFmt<LIMIT>

proof fn lemma_serialize_len(&self, value: AnySpec)

fn serialize_inv(&self) -> bool

impl<const LIMIT: usize> HasAsn1Start for BerAnyFmt<LIMIT>

Recursive BER ANY accepts every complete tag except EOC.

open spec fn asn1_start(&self) -> Asn1StartDomain

{ asn1_start_any_non_eoc() }

proof fn lemma_parse_implies_asn1_start(&self, input: Seq<u8>)

impl<const LIMIT: usize> NonTailFmt for BerAnyFmt<LIMIT>

proof fn lemma_serialize_dps_prepend(&self, value: AnySpec, obuf: Seq<u8>)

proof fn lemma_serialize_dps_len(&self, value: AnySpec, obuf: Seq<u8>)

fn serialize_dps_inv(&self) -> bool

impl<'i, const LIMIT: usize> Parser<&'i [u8]> for BerAnyFmt<LIMIT>

Available on crate feature alloc only.

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

type PT = AnyOwned

Executable value returned by this parser.

fn exec_inv(&self) -> bool

impl<const LIMIT: usize> Prepare<AnyOwned> for BerAnyFmt<LIMIT>

Available on crate feature alloc only.

exec fn prepare(&self, value: &AnyOwned) -> Result<usize, PreSerializeError>

fn exec_inv(&self) -> bool

impl<const LIMIT: usize> Productive for BerAnyFmt<LIMIT>

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

fn productive_inv(&self) -> bool

impl<const LIMIT: usize> SPRoundTripDps for BerAnyFmt<LIMIT>

proof fn theorem_serialize_dps_parse_roundtrip(&self, value: AnySpec, obuf: Seq<u8>)

fn unambiguous(&self) -> bool

impl<const LIMIT: usize> SafeParser for BerAnyFmt<LIMIT>

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

fn safe_inv(&self) -> bool

impl<Output: OutputBuf, const LIMIT: usize> Serializer<Output, AnyOwned> for BerAnyFmt<LIMIT>

Available on crate feature alloc only.

exec fn serialize_into(&self, value: &AnyOwned, obuf: &mut Output)

fn exec_inv(&self) -> bool

impl<const LIMIT: usize> SpecByteLen for BerAnyFmt<LIMIT>

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

{ AnyFmt::<BER>.byte_len(value) }

type T = AnySpec

The type of values whose byte length is being computed.

impl<const LIMIT: usize> SpecParser for BerAnyFmt<LIMIT>

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

{ ber_any_parse::<LIMIT>(input) }

type PVal = AnySpec

The type of parsed values.

impl<const LIMIT: usize> SpecSerializer for BerAnyFmt<LIMIT>

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

{ AnyFmt::<BER>.spec_serialize(value) }

type SVal = AnySpec

The type of values to be serialized.

impl<const LIMIT: usize> SpecSerializerDps for BerAnyFmt<LIMIT>

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

{ AnyFmt::<BER>.spec_serialize_dps(value, obuf) }

type SValue = AnySpec

The type of values to be serialized.

impl<const LIMIT: usize> Copy for BerAnyFmt<LIMIT>