Struct Any 

pub struct Any<'a> { /* private fields */ }

Borrowed executable open-type value.

Implementations

impl<'a> Any<'a>

pub exec fn new(tag: Tag, content: &'a [u8]) -> value : Self

ensures

value.deep_view()
    == (AnySpec {
        tag,
        content: content.deep_view(),
    }),

pub exec fn tag(&self) -> tag : Tag

ensures

tag == self.deep_view().tag,

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

ensures

content.deep_view() == self.deep_view().content,

Trait Implementations

impl<'a, const DER: bool> ByteLen<Any<'a>> for AnyFmt<DER>

exec fn length(&self, v: &Any<'a>) -> usize

fn exec_inv(&self) -> bool

impl<'a> DeepView for Any<'a>

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

type V = AnySpec

impl<'a> DerOrd<Any<'a>> for AnyFmt<true>

proof fn lemma_der_serialize_len(&self, value: AnySpec)

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

{
    <AnyDerInnerFmt as DerOrd<
        (Tag, (usize, &'a [u8])),
    >>::der_remaining(
        &Pair(TagFmt, Pair(LengthFmt::<true>, Tail)),
        (value.tag, (value.content.len() as usize, value.content)),
        state,
    )
}

open spec fn der_state_valid(&self, value: AnySpec, state: AnyDerState) -> bool

{
    <AnyDerInnerFmt as DerOrd<
        (Tag, (usize, &'a [u8])),
    >>::der_state_valid(
        &Pair(TagFmt, Pair(LengthFmt::<true>, Tail)),
        (value.tag, (value.content.len() as usize, value.content)),
        state,
    )
}

exec fn der_start(&self, a: &Any<'a>) -> state : AnyDerState

exec fn der_next(&self, a: &Any<'a>, state: &mut AnyDerState) -> next : Option<u8>

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

impl<'a, const DER: bool> Prepare<Any<'a>> for AnyFmt<DER>

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

fn exec_inv(&self) -> bool

impl<'a, Output: OutputBuf, const DER: bool> Serializer<Output, Any<'a>> for AnyFmt<DER>

exec fn serialize_into(&self, v: &Any<'a>, obuf: &mut Output)

fn exec_inv(&self) -> bool