EndianNat

vstd::endian

Struct EndianNat 

Source 
pub struct EndianNat<B: Base> {
    pub endian: Endian,
    pub digits: Seq<int>,
    pub phantom: PhantomData<B>,
}
Expand description

Provides either little-endian or big-endian interpretation of a sequence of numbers with a given base. This interpretation may have any number of leading zeros. With little-endian, the first digit is the least significant position; the last digit is the most significant position. With big-endian, the last digit of a sequence is the least significant position; the first digit is the most significant position.

Fields§

§endian: Endian§digits: Seq<int>§phantom: PhantomData<B>

Implementations§

Source§

impl<B: Base> EndianNat<B>

Source

pub open spec fn in_bounds(s: Seq<int>) -> bool

{ forall |i| 0 <= i < s.len() ==> 0 <= #[trigger] s[i] < B::base() }

True when all numbers in s are valid digits in the given base.

Source

pub open spec fn wf(self) -> bool

{ Self::in_bounds(self.digits) }

True when all of self.digits are valid digits in the given base.

Source

pub open spec fn new(endian: Endian, digits: Seq<int>) -> Self

recommends
Self::in_bounds(digits),
{
    EndianNat {
        endian,
        digits,
        phantom: PhantomData,
    }
}

Creates a new EndianNat with the given digits and endianness.

Source

pub open spec fn new_default(digits: Seq<int>) -> Self

recommends
Self::in_bounds(digits),
{
    EndianNat {
        endian: endianness(),
        digits,
        phantom: PhantomData,
    }
}

Creates a new EndianNat with the given digits and the default endianness (endianness()).

Source

pub open spec fn len(self) -> nat

{ self.digits.len() }

Number of digits in this EndianNat.

Source

pub open spec fn index(self, i: int) -> int

recommends
0 <= i < self.digits.len(),
{ self.digits[i] }

The ith digit in this EndianNat.

Source

pub open spec fn first(self) -> nat

recommends
self.digits.len() > 0,
{ self.digits.first() as nat }

The first digit in this EndianNat. Ignores endianness.

Source

pub open spec fn last(self) -> nat

recommends
self.digits.len() > 0,
{ self.digits.last() as nat }

The last digit in this EndianNat. Ignores endianness.

Source

pub open spec fn least(self) -> nat

recommends
self.digits.len() > 0,
{
    match self.endian {
        Endian::Little => self.first(),
        Endian::Big => self.last(),
    }
}

The least significant digit in this EndianNat.

Source

pub open spec fn most(self) -> nat

recommends
self.digits.len() > 0,
{
    match self.endian {
        Endian::Little => self.last(),
        Endian::Big => self.first(),
    }
}

The most significant digit in this EndianNat.

Source

pub open spec fn skip(self, n: nat) -> Self

recommends
0 <= n <= self.digits.len(),
{
    EndianNat {
        endian: self.endian,
        digits: self.digits.skip(n as int),
        phantom: self.phantom,
    }
}

Constructs an EndianNat by skipping the first n digits of the original EndianNat. Ignores endianness.

Source

pub open spec fn take(self, n: nat) -> Self

recommends
0 <= n <= self.digits.len(),
{
    EndianNat {
        endian: self.endian,
        digits: self.digits.take(n as int),
        phantom: self.phantom,
    }
}

Constructs an EndianNat by taking only the first n digits of the original EndianNat. Ignores endianness.

Source

pub open spec fn skip_least(self, n: nat) -> Self

recommends
0 <= n <= self.digits.len(),
{
    match self.endian {
        Endian::Little => self.skip(n),
        Endian::Big => self.take((self.len() - n) as nat),
    }
}

Constructs an EndianNat by skipping the least significant n digits of the original EndianNat.

Source

pub open spec fn skip_most(self, n: nat) -> Self

recommends
0 <= n <= self.digits.len(),
{
    match self.endian {
        Endian::Little => self.take((self.len() - n) as nat),
        Endian::Big => self.skip(n),
    }
}

Constructs an EndianNat by skipping the most significant n digits of the original EndianNat.

Source

pub open spec fn take_least(self, n: nat) -> Self

recommends
0 <= n <= self.digits.len(),
{
    match self.endian {
        Endian::Little => self.take(n),
        Endian::Big => self.skip((self.len() - n) as nat),
    }
}

Constructs an EndianNat by taking only the least significant n digits of the original EndianNat.

Source

pub open spec fn take_most(self, n: nat) -> Self

recommends
0 <= n <= self.digits.len(),
{
    match self.endian {
        Endian::Little => self.skip((self.len() - n) as nat),
        Endian::Big => self.take(n),
    }
}

Constructs an EndianNat by taking only the most significant n digits of the original EndianNat.

Source

pub open spec fn drop_first(self) -> Self

recommends
self.len() > 0,
{
    EndianNat {
        endian: self.endian,
        digits: self.digits.drop_first(),
        phantom: self.phantom,
    }
}

Constructs an EndianNat by dropping the first digit of the original EndianNat. Ignores endianness.

Source

pub open spec fn drop_last(self) -> Self

recommends
self.len() > 0,
{
    EndianNat {
        endian: self.endian,
        digits: self.digits.drop_last(),
        phantom: self.phantom,
    }
}

Constructs an EndianNat by dropping the last digit of the original EndianNat. Ignores endianness.

Source

pub open spec fn drop_least(self) -> Self

recommends
self.len() > 0,
{
    match self.endian {
        Endian::Little => self.drop_first(),
        Endian::Big => self.drop_last(),
    }
}

Constructs an EndianNat by dropping the least significant digit of the original EndianNat.

Source

pub open spec fn drop_most(self) -> Self

recommends
self.len() > 0,
{
    match self.endian {
        Endian::Little => self.drop_last(),
        Endian::Big => self.drop_first(),
    }
}

Constructs an EndianNat by dropping the most significant digits of the original EndianNat.

Source

pub open spec fn append(self, other: Self) -> Self

recommends
self.endian == other.endian,
{ EndianNat::new(self.endian, self.digits + other.digits) }

Constructs an EndianNat by appending the digits of other to the end of the digits of self. Ignores endianness.

Source

pub open spec fn append_least(self, other: Self) -> Self

recommends
self.endian == other.endian,
{
    match self.endian {
        Endian::Little => other.append(self),
        Endian::Big => self.append(other),
    }
}

Constructs an EndianNat by appending the digits of other to the digits of self in the least significant position (i.e., other becomes the least significant bits).

Source

pub open spec fn append_most(self, other: Self) -> Self

recommends
self.endian == other.endian,
{
    match self.endian {
        Endian::Little => self.append(other),
        Endian::Big => other.append(self),
    }
}

Constructs an EndianNat by appending the digits of other to the digits of self in the most significant position (i.e., other becomes the most significant bits).

Source

pub open spec fn push_first(self, n: int) -> Self

recommends
n < B::base(),
{
    EndianNat {
        endian: self.endian,
        digits: seq![n].add(self.digits),
        phantom: self.phantom,
    }
}

Constructs an EndianNat by appending n to the front of the digits of self. Ignores endianness.

Source

pub open spec fn push_last(self, n: int) -> Self

recommends
n < B::base(),
{
    EndianNat {
        endian: self.endian,
        digits: self.digits.push(n),
        phantom: self.phantom,
    }
}

Constructs an EndianNat by appending n to the end of the digits of self. Ignores endianness.

Source

pub open spec fn push_least(self, n: int) -> Self

recommends
n < B::base(),
{
    match self.endian {
        Endian::Little => self.push_first(n),
        Endian::Big => self.push_last(n),
    }
}

Constructs an EndianNat by appending n to the least significant position in the digits of self.

Source

pub open spec fn push_most(self, n: int) -> Self

recommends
n < B::base(),
{
    match self.endian {
        Endian::Little => self.push_last(n),
        Endian::Big => self.push_first(n),
    }
}

Constructs an EndianNat by appending n to the most significant position in the digits of self.

Source

pub open spec fn to_nat(self) -> nat

{
    if self.len() == 0 {
        0
    } else {
        self.drop_least().to_nat() * B::base() + self.least()
    }
}

Converts an EndianNat to the natural number that it represents, processing the digits from least significant to most significant, hiding the details of endianness.

Source

pub broadcast proof fn to_nat_properties(self)

requires
self.wf(),
ensures
#[trigger] self.to_nat() < base_upper_bound_excl::<B>(self.len()),
Source

pub proof fn to_nat_append_least(endian: Self, other: Self)

requires
endian.wf(),
other.wf(),
endian.endian == other.endian,
ensures
endian.append_least(other).to_nat()
    == (endian.to_nat() * base_upper_bound_excl::<B>(other.len())) + other.to_nat(),
Source

pub open spec fn from_nat(n: nat, len: nat) -> Self

recommends
n < base_upper_bound_excl::<B>(len),
{
    if len == 0 {
        EndianNat {
            digits: Seq::empty(),
            endian: endianness(),
            phantom: PhantomData,
        }
    } else {
        let least = (n % B::base()) as int;
        let rest = n / B::base();
        let rest_endian = Self::from_nat(rest, (len - 1) as nat);
        rest_endian.push_least(least)
    }
}

Converts a natural number to an EndianNat representation with the specified number of digits (len) and default endianness (endianness()). n should be less than the maximum number that can be represented in len digits in this base.

Source

pub broadcast proof fn from_nat_properties(n: nat, len: nat)

requires
n < base_upper_bound_excl::<B>(len),
ensures
Self::from_nat(n, len).len() == len,
Self::from_nat(n, len).endian == endianness(),
Self::from_nat(n, len).wf(),
Source

pub broadcast proof fn from_nat_to_nat(n: nat, len: nat)

requires
n < base_upper_bound_excl::<B>(len),
ensures
#[trigger] Self::from_nat(n, len).to_nat() == n,

Ensures that performing from_nat and then to_nat results in the original value, provided that the value can be encoded in the given base in the given number of digits.

Source

pub broadcast proof fn to_nat_from_nat(endian_nat: Self)

requires
endian_nat.wf(),
endian_nat.endian == endianness(),
ensures
#[trigger] Self::from_nat(endian_nat.to_nat(), endian_nat.len()) == endian_nat,

Ensures that performing to_nat and then from_nat results in the original EndianNat.

Source

pub broadcast proof fn to_nat_injective(n1: Self, n2: Self)

requires
n1.wf(),
n2.wf(),
n1.endian == endianness(),
n2.endian == endianness(),
n1.len() == n2.len(),
#[trigger] n1.to_nat() == #[trigger] n2.to_nat(),
ensures
n1 == n2,
Source

pub broadcast proof fn from_nat_injective(n1: nat, len1: nat, n2: nat, len2: nat)

requires
n1 < base_upper_bound_excl::<B>(len1),
n2 < base_upper_bound_excl::<B>(len2),
#[trigger] Self::from_nat(n1, len1) == #[trigger] Self::from_nat(n2, len2),
ensures
n1 == n2,
Source

pub open spec fn to_nat_most(self) -> nat

{
    if self.len() == 0 {
        0
    } else {
        (self.drop_most().to_nat_most()
            + self.most() * pow(B::base() as int, (self.len() - 1) as nat)) as nat
    }
}

Converts an EndianNat to the natural number that it represents, processing the digits from most significant to least significant, hiding the details of endianness.

Source

pub broadcast proof fn to_nat_eq_to_nat_most(self)

requires
self.wf(),
ensures
#[trigger] self.to_nat() == #[trigger] self.to_nat_most(),

Ensures that to_nat and to_nat_most agree.

Source§

impl<B: Base> EndianNat<B>

Source

pub open spec fn exp<BIG>() -> nat
where BIG: BasePow2, B: CompatibleSmallerBaseFor<BIG>,

{ BIG::bits() / B::bits() }

B::base() to the power of exp() is BIG::base(). In other words, exp() is the number of digits in base B that correspond to a single digit in base BIG.

Source

pub broadcast proof fn exp_properties<BIG>()
where BIG: BasePow2, B: CompatibleSmallerBaseFor<BIG>,

ensures
base_upper_bound_excl::<B>(Self::exp()) == BIG::base(),
Self::exp() > 0,
Source

pub open spec fn from_big<BIG>(n: EndianNat<BIG>) -> Self
where BIG: BasePow2, B: CompatibleSmallerBaseFor<BIG>,

{
    if n.len() == 0 {
        EndianNat::new(n.endian, Seq::empty())
    } else {
        Self::from_big(n.drop_least())
            .append_least(EndianNat::from_nat(n.least(), Self::exp()))
    }
}

Converts an EndianNat representation in the “big” base BIG to an EndianNat representation in the “small” base B. The result represents the same non-negative number as the original.

Source

pub broadcast proof fn from_big_properties<BIG>(n: EndianNat<BIG>)
where BIG: BasePow2, B: CompatibleSmallerBaseFor<BIG>,

requires
n.wf(),
n.endian == endianness(),
ensures
Self::from_big(n).wf(),
Self::from_big(n).endian == endianness(),
Self::from_big(n).len() == n.len() * Self::exp(),
Self::from_big(n).to_nat() == n.to_nat(),
Source

pub open spec fn to_big<BIG>(n: EndianNat<B>) -> EndianNat<BIG>
where BIG: BasePow2, B: CompatibleSmallerBaseFor<BIG>,

recommends
n.len() % Self::exp() == 0,
{
    if n.len() == 0 {
        EndianNat::new(n.endian, Seq::empty())
    } else {
        Self::to_big(n.skip_least(Self::exp()))
            .append_least(
                EndianNat::new(n.endian, seq![n.take_least(Self::exp()).to_nat() as int]),
            )
    }
}

Converts an EndianNat representation in the “small” base B to an EndianNat representation in the “big” base BIG. The result represents the same non-negative number as the original.

Source

pub broadcast proof fn to_big_properties<BIG>(n: EndianNat<B>)
where BIG: BasePow2, B: CompatibleSmallerBaseFor<BIG>,

requires
n.wf(),
n.endian == endianness(),
n.len() % Self::exp() == 0,
ensures
Self::to_big(n).wf(),
Self::to_big(n).endian == endianness(),
Self::to_big(n).len() == n.len() / Self::exp(),
Self::to_big(n).to_nat() == n.to_nat(),
Source

pub broadcast proof fn to_big_from_big<BIG>(n: EndianNat<B>)
where BIG: BasePow2, B: CompatibleSmallerBaseFor<BIG>,

requires
n.wf(),
n.endian == endianness(),
n.len() % Self::exp() == 0,
ensures
#[trigger] Self::from_big(Self::to_big(n)) == n,

Ensures that performing to_big and then from_big results in the original EndianNat<B>.

Source

pub broadcast proof fn from_big_to_big<BIG>(n: EndianNat<BIG>)
where BIG: BasePow2, B: CompatibleSmallerBaseFor<BIG>,

requires
n.wf(),
n.endian == endianness(),
ensures
#[trigger] Self::to_big(Self::from_big(n)) == n,

Ensures that performing from_big and then to_big results in the original EndianNat<BIG>.

Source

pub broadcast proof fn to_big_injective<BIG>(n1: EndianNat<B>, n2: EndianNat<B>)
where BIG: BasePow2, B: CompatibleSmallerBaseFor<BIG>,

requires
n1.wf(),
n2.wf(),
n1.endian == endianness(),
n2.endian == endianness(),
n1.len() % Self::exp() == 0,
n2.len() % Self::exp() == 0,
#[trigger] Self::to_big(n1) == #[trigger] Self::to_big(n2),
ensures
n1 == n2,
Source

pub broadcast proof fn from_big_injective<BIG>(n1: EndianNat<BIG>, n2: EndianNat<BIG>)
where BIG: BasePow2, B: CompatibleSmallerBaseFor<BIG>,

requires
n1.wf(),
n2.wf(),
n1.endian == endianness(),
n2.endian == endianness(),
#[trigger] Self::from_big(n1) == #[trigger] Self::from_big(n2),
ensures
n1 == n2,
Source

pub proof fn to_big_single<BIG>(x: EndianNat<B>)
where BIG: BasePow2, B: CompatibleSmallerBaseFor<BIG>,

requires
x.len() == Self::exp(),
x.len() > 0,
ensures
Self::to_big(x).len() == 1,
Self::to_big(x).index(0) == x.to_nat() as int,

Auto Trait Implementations§

§

impl<B> Freeze for EndianNat<B>

§

impl<B> RefUnwindSafe for EndianNat<B>
where B: RefUnwindSafe,

§

impl<B> Send for EndianNat<B>
where B: Send,

§

impl<B> Sync for EndianNat<B>
where B: Sync,

§

impl<B> Unpin for EndianNat<B>
where B: Unpin,

§

impl<B> UnwindSafe for EndianNat<B>
where B: UnwindSafe,

Blanket Implementations§

Source§

impl<T> Any for T
where T: 'static + ?Sized,

Source§

fn type_id(&self) -> TypeId

Gets the TypeId of self. Read more
Source§

impl<T> Borrow<T> for T
where T: ?Sized,

Source§

fn borrow(&self) -> &T

Immutably borrows from an owned value. Read more
Source§

impl<T> BorrowMut<T> for T
where T: ?Sized,

Source§

fn borrow_mut(&mut self) -> &mut T

Mutably borrows from an owned value. Read more
Source§

impl<T> From<T> for T

Source§

fn from(t: T) -> T

Returns the argument unchanged.

Source§

impl<T, VERUS_SPEC__A> FromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: From<T>,

Source§

exec fn obeys_from_spec() -> bool

Source§

exec fn from_spec(v: T) -> VERUS_SPEC__A

Source§

impl<T, U> Into<U> for T
where U: From<T>,

Source§

fn into(self) -> U

Calls U::from(self).

That is, this conversion is whatever the implementation of From<T> for U chooses to do.

Source§

impl<T, VERUS_SPEC__A> IntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: Into<T>,

Source§

exec fn obeys_into_spec() -> bool

Source§

exec fn into_spec(self) -> T

Source§

impl<T, U> IntoSpecImpl<U> for T
where U: From<T>,

Source§

open spec fn obeys_into_spec() -> bool

{ <U as FromSpec<Self>>::obeys_from_spec() }
Source§

open spec fn into_spec(self) -> U

{ U::from_spec(self) }
Source§

impl<T, U> TryFrom<U> for T
where U: Into<T>,

Source§

type Error = Infallible

The type returned in the event of a conversion error.
Source§

fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>

Performs the conversion.
Source§

impl<T, VERUS_SPEC__A> TryFromSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryFrom<T>,

Source§

exec fn obeys_try_from_spec() -> bool

Source§

exec fn try_from_spec( v: T, ) -> Result<VERUS_SPEC__A, <VERUS_SPEC__A as TryFrom<T>>::Error>

Source§

impl<T, U> TryInto<U> for T
where U: TryFrom<T>,

Source§

type Error = <U as TryFrom<T>>::Error

The type returned in the event of a conversion error.
Source§

fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>

Performs the conversion.
Source§

impl<T, VERUS_SPEC__A> TryIntoSpec<T> for VERUS_SPEC__A
where VERUS_SPEC__A: TryInto<T>,

Source§

exec fn obeys_try_into_spec() -> bool

Source§

exec fn try_into_spec(self) -> Result<T, <VERUS_SPEC__A as TryInto<T>>::Error>

Source§

impl<T, U> TryIntoSpecImpl<U> for T
where U: TryFrom<T>,

Source§

open spec fn obeys_try_into_spec() -> bool

{ <U as TryFromSpec<Self>>::obeys_try_from_spec() }
Source§

open spec fn try_into_spec(self) -> Result<U, <U as TryFrom<T>>::Error>

{ <U as TryFromSpec<Self>>::try_from_spec(self) }