Trait AsLen 

pub trait AsLen: Sized + Copy {
    // Required methods
    spec fn as_nat(self) -> nat;
    exec fn get(self) -> len : usize;
    spec fn as_self(n: nat) -> Self;
    proof fn lemma_lossless_casting(v: Self);
}

Types that can serve as format length (or count) fields.

The spec-facing conversion is to nat, which is the natural domain for lengths in proofs. The exec-facing conversion is to usize, which is the natural domain for runtime indexing.

Required Methods

spec fn as_nat(self) -> nat

The mathematical length represented by this value.

exec fn get(self) -> len : usize

ensures

len as nat == self.as_nat(),

The runtime length represented by this value.

spec fn as_self(n: nat) -> Self

Construct from a nat.

proof fn lemma_lossless_casting(v: Self)

ensures

Self::as_self(v.as_nat()) == v,

as_self(v.as_nat()) == v.

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementations on Foreign Types

impl AsLen for u8

open spec fn as_nat(self) -> nat

{ self as nat }

exec fn get(self) -> len : usize

open spec fn as_self(n: nat) -> Self

{ n as u8 }

proof fn lemma_lossless_casting(v: Self)

impl AsLen for u16

open spec fn as_nat(self) -> nat

{ self as nat }

exec fn get(self) -> len : usize

open spec fn as_self(n: nat) -> Self

{ n as u16 }

proof fn lemma_lossless_casting(v: Self)

impl AsLen for u32

open spec fn as_nat(self) -> nat

{ self as nat }

exec fn get(self) -> len : usize

open spec fn as_self(n: nat) -> Self

{ n as u32 }

proof fn lemma_lossless_casting(v: Self)

impl AsLen for u64

open spec fn as_nat(self) -> nat

{ self as nat }

exec fn get(self) -> len : usize

open spec fn as_self(n: nat) -> Self

{ n as u64 }

proof fn lemma_lossless_casting(v: Self)

impl AsLen for usize

open spec fn as_nat(self) -> nat

{ self as nat }

exec fn get(self) -> len : usize

open spec fn as_self(n: nat) -> Self

{ n as usize }

proof fn lemma_lossless_casting(v: Self)

impl<T: AsLen> AsLen for &T

open spec fn as_nat(self) -> nat

{ (*self).as_nat() }

exec fn get(self) -> len : usize

open spec fn as_self(n: nat) -> Self

{ &T::as_self(n) }

proof fn lemma_lossless_casting(v: Self)

Implementors