Enum Integer 

pub enum Integer<'a> {
    Small {
        v: i64,
    },
    Big {
        raw: BigInt<'a>,
    },
}

Variants

Small

Fields

v: i64

Big

Fields

raw: BigInt<'a>

Implementations

impl<'a> Integer<'a>

pub fn arrow_raw(self) -> BigInt<'a>

pub fn arrow_v(self) -> i64

pub fn arrow_Small_v(self) -> i64

pub fn arrow_Big_raw(self) -> BigInt<'a>

impl<'a> Integer<'a>

pub const exec fn from_i64(v: i64) -> Self

Constructs the exact ASN.1 INTEGER value represented by an i64.

pub exec fn as_i64(&self) -> value : Option<i64>

ensures

value matches Some(v) ==> self.deep_view() == v as int,

Returns the value as an i64 when it is represented by the small variant.

pub exec fn in_i64_range<const HAS_MIN: bool, const MIN: i64, const HAS_MAX: bool, const MAX: i64>( &self, ) -> ok : bool

ensures

ok
    == ({
        &&& HAS_MIN ==> MIN as int <= self.deep_view()
        &&& HAS_MAX ==> self.deep_view() <= MAX as int

    }),

Tests an inclusive interval whose endpoints are representable as i64.

Trait Implementations

impl<'i> ByteLen<Integer<'i>> for EnumeratedFmt

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

fn exec_inv(&self) -> bool

impl<'i> ByteLen<Integer<'i>> for IntegerFmt

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

fn exec_inv(&self) -> bool

impl<'a> Clone for Integer<'a>

fn clone(&self) -> Integer<'a>

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl<'a> DeepView for Integer<'a>

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

type V = int

impl<'a> DerOrd<Integer<'a>> for EnumeratedFmt

proof fn lemma_der_serialize_len(&self, value: int)

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

{ IntegerFmt.der_remaining(value, state) }

open spec fn der_state_valid(&self, value: int, state: IntegerDerState) -> bool

{ IntegerFmt.der_state_valid(value, state) }

exec fn der_start(&self, i: &Integer<'a>) -> state : IntegerDerState

exec fn der_next(&self, i: &Integer<'a>, state: &mut IntegerDerState) -> next : Option<u8>

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

impl<'a> DerOrd<Integer<'a>> for IntegerFmt

proof fn lemma_der_serialize_len(&self, value: int)

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

{ self.spec_serialize(value).skip(state.pos as int) }

open spec fn der_state_valid(&self, value: int, state: IntegerDerState) -> bool

{
    &&& state.pos <= state.len
    &&& state.len == self.spec_serialize(value).len()
    &&& state.small == (i64::MIN as int <= value <= i64::MAX as int)
    &&& state.small
        ==> {
            &&& state.len <= 9
            &&& state.bytes@.take(state.len as int) == self.spec_serialize(value)

        }

}

exec fn der_start(&self, i: &Integer<'a>) -> state : IntegerDerState

exec fn der_next(&self, i: &Integer<'a>, state: &mut IntegerDerState) -> next : Option<u8>

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

impl<'a, const HAS_MIN: bool, const MIN: i64, const HAS_MAX: bool, const MAX: i64> Pred<Integer<'a>> for IntegerRange<HAS_MIN, MIN, HAS_MAX, MAX>

exec fn test(&self, value: &Integer<'a>) -> ok : bool

impl<'i> Prepare<Integer<'i>> for EnumeratedFmt

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

fn exec_inv(&self) -> bool

impl<'i> Prepare<Integer<'i>> for IntegerFmt

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

fn exec_inv(&self) -> bool

impl<'i, Output: OutputBuf> Serializer<Output, Integer<'i>> for EnumeratedFmt

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

fn exec_inv(&self) -> bool

impl<'i, Output: OutputBuf> Serializer<Output, Integer<'i>> for IntegerFmt

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

fn exec_inv(&self) -> bool

impl<'a> Copy for Integer<'a>