Struct Integer16Fmt 

pub struct Integer16Fmt;

ASN.1 INTEGER contents specialized to the i16 representation.

Values in the i8 range use one octet; all other values use two big-endian octets. Redundant two-octet encodings are rejected.

Trait Implementations

impl ByteLen<i16> for Integer16Fmt

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

fn exec_inv(&self) -> bool

impl Clone for Integer16Fmt

fn clone(&self) -> Integer16Fmt

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Consistency for Integer16Fmt

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

{ true }

type Val = i16

The type of values whose consistency is being checked.

impl DerOrd<i16> for Integer16Fmt

proof fn lemma_der_serialize_len(&self, value: i16)

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

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

open spec fn der_state_valid(&self, value: i16, state: Integer16DerState) -> bool

{
    &&& state.pos <= state.len <= 2
    &&& state.len == self.spec_serialize(value).len()
    &&& state.bytes@.take(state.len as int) == self.spec_serialize(value)

}

exec fn der_start(&self, i: &i16) -> state : Integer16DerState

exec fn der_next(&self, i: &i16, state: &mut Integer16DerState) -> next : Option<u8>

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

impl DerState for Integer16Fmt

type State = Integer16DerState

impl EquivSerializers for Integer16Fmt

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

fn equiv_inv(&self) -> bool

impl GoodSerializer for Integer16Fmt

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

fn serialize_inv(&self) -> bool

impl NonMalleable for Integer16Fmt

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

fn nonmal_inv(&self) -> bool

impl<'i> Parser<&'i [u8]> for Integer16Fmt

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

type PT = i16

Executable value returned by this parser.

fn exec_inv(&self) -> bool

impl Prepare<i16> for Integer16Fmt

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

fn exec_inv(&self) -> bool

impl Productive for Integer16Fmt

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

fn productive_inv(&self) -> bool

impl SPRoundTripDps for Integer16Fmt

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

fn unambiguous(&self) -> bool

impl SafeParser for Integer16Fmt

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

fn safe_inv(&self) -> bool

impl<Output: OutputBuf> Serializer<Output, i16> for Integer16Fmt

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

fn exec_inv(&self) -> bool

impl SoundParser for Integer16Fmt

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 SpecByteLen for Integer16Fmt

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

{ if fits_i8(v) { I8.byte_len(v as i8) } else { I16Be.byte_len(v) } }

type T = i16

The type of values whose byte length is being computed.

impl SpecParser for Integer16Fmt

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

{
    if ibuf.len() == 1 {
        let (_, v) = I8.spec_parse(ibuf)->0;
        Some((1, v as i16))
    } else if ibuf.len() == 2 {
        match I16Be.spec_parse(ibuf) {
            Some((_, v)) if !fits_i8(v) => Some((2, v)),
            _ => None,
        }
    } else {
        None
    }
}

type PVal = i16

The type of parsed values.

impl SpecSerializer for Integer16Fmt

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

{ if fits_i8(v) { I8.spec_serialize(v as i8) } else { I16Be.spec_serialize(v) } }

type SVal = i16

The type of values to be serialized.

impl SpecSerializerDps for Integer16Fmt

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

{ if fits_i8(v) { I8.spec_serialize(v as i8) } else { I16Be.spec_serialize(v) } }

type SValue = i16

The type of values to be serialized.

impl Copy for Integer16Fmt