AlignExt

align_ext

Trait AlignExt 

Source 
pub trait AlignExt {
    // Required methods
    exec fn align_up(self, power_of_two: Self) -> ret : Self;
    exec fn align_down(self, power_of_two: Self) -> ret : Self;
}
Expand description

An extension trait for Rust integer types, including u8, u16, u32, u64, and usize, to provide methods to make integers aligned to a power of two.

Required Methods§

Source

fn align_up(self, power_of_two: Self) -> Self

Returns to the smallest number that is greater than or equal to self and is a multiple of the given power of two.

The method panics if power_of_two is not a power of two or is smaller than 2 or the calculation overflows because self is too large.

§Examples
use crate::align_ext::AlignExt;
assert_eq!(12usize.align_up(2), 12);
assert_eq!(12usize.align_up(4), 12);
assert_eq!(12usize.align_up(8), 16);
assert_eq!(12usize.align_up(16), 16);
Source

fn align_down(self, power_of_two: Self) -> Self

Returns to the greatest number that is smaller than or equal to self and is a multiple of the given power of two.

The method panics if power_of_two is not a power of two or is smaller than 2 or the calculation overflows because self is too large. In release mode,

§Examples
use crate::align_ext::AlignExt;
assert_eq!(12usize.align_down(2), 12);
assert_eq!(12usize.align_down(4), 12);
assert_eq!(12usize.align_down(8), 8);
assert_eq!(12usize.align_down(16), 0);

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§

Source§

impl AlignExt for u8

§Verified Properties

§Safety

The implementation is written in safe Rust and there is no undefined behavior.

§Functional correctness

The implementation meets the specification given in the trait AlignExt.

Source§

exec fn align_up(self, align: Self) -> ret : Self

requires
exists |e: nat| pow2(e) == align,
align >= 2,
self + (align - 1) <= u8::MAX,
ensures
ret >= self,
ret % align == 0,
ret == nat_align_up(self as nat, align as nat),
forall |n: nat| !(n >= self && #[trigger] (n % align as nat) == 0) || (ret <= n),
§Preconditions
  • align is a power of two.
  • align >= 2.
  • self + (align - 1) does not overflow.
§Postconditions
  • The function will not panic.
  • The return value is the smallest number that is greater than or equal to self and is a multiple of align.
Source§

exec fn align_down(self, align: Self) -> ret : Self

requires
exists |e: nat| pow2(e) == align,
align >= 2,
ensures
ret <= self,
ret % align == 0,
ret == nat_align_down(self as nat, align as nat),
forall |n: nat| !(n <= self && #[trigger] (n % align as nat) == 0) || (ret >= n),
§Preconditions
  • align is a power of two.
  • align >= 2.
§Postconditions
  • The function will not panic.
  • The return value is the greatest number that is smaller than or equal to self and is a multiple of align.
Source§

impl AlignExt for u16

§Verified Properties

§Safety

The implementation is written in safe Rust and there is no undefined behavior.

§Functional correctness

The implementation meets the specification given in the trait AlignExt.

Source§

exec fn align_up(self, align: Self) -> ret : Self

requires
exists |e: nat| pow2(e) == align,
align >= 2,
self + (align - 1) <= u16::MAX,
ensures
ret >= self,
ret % align == 0,
ret == nat_align_up(self as nat, align as nat),
forall |n: nat| !(n >= self && #[trigger] (n % align as nat) == 0) || (ret <= n),
§Preconditions
  • align is a power of two.
  • align >= 2.
  • self + (align - 1) does not overflow.
§Postconditions
  • The function will not panic.
  • The return value is the smallest number that is greater than or equal to self and is a multiple of align.
Source§

exec fn align_down(self, align: Self) -> ret : Self

requires
exists |e: nat| pow2(e) == align,
align >= 2,
ensures
ret <= self,
ret % align == 0,
ret == nat_align_down(self as nat, align as nat),
forall |n: nat| !(n <= self && #[trigger] (n % align as nat) == 0) || (ret >= n),
§Preconditions
  • align is a power of two.
  • align >= 2.
§Postconditions
  • The function will not panic.
  • The return value is the greatest number that is smaller than or equal to self and is a multiple of align.
Source§

impl AlignExt for u32

§Verified Properties

§Safety

The implementation is written in safe Rust and there is no undefined behavior.

§Functional correctness

The implementation meets the specification given in the trait AlignExt.

Source§

exec fn align_up(self, align: Self) -> ret : Self

requires
exists |e: nat| pow2(e) == align,
align >= 2,
self + (align - 1) <= u32::MAX,
ensures
ret >= self,
ret % align == 0,
ret == nat_align_up(self as nat, align as nat),
forall |n: nat| !(n >= self && #[trigger] (n % align as nat) == 0) || (ret <= n),
§Preconditions
  • align is a power of two.
  • align >= 2.
  • self + (align - 1) does not overflow.
§Postconditions
  • The function will not panic.
  • The return value is the smallest number that is greater than or equal to self and is a multiple of align.
Source§

exec fn align_down(self, align: Self) -> ret : Self

requires
exists |e: nat| pow2(e) == align,
align >= 2,
ensures
ret <= self,
ret % align == 0,
ret == nat_align_down(self as nat, align as nat),
forall |n: nat| !(n <= self && #[trigger] (n % align as nat) == 0) || (ret >= n),
§Preconditions
  • align is a power of two.
  • align >= 2.
§Postconditions
  • The function will not panic.
  • The return value is the greatest number that is smaller than or equal to self and is a multiple of align.
Source§

impl AlignExt for u64

§Verified Properties

§Safety

The implementation is written in safe Rust and there is no undefined behavior.

§Functional correctness

The implementation meets the specification given in the trait AlignExt.

Source§

exec fn align_up(self, align: Self) -> ret : Self

requires
exists |e: nat| pow2(e) == align,
align >= 2,
self + (align - 1) <= u64::MAX,
ensures
ret >= self,
ret % align == 0,
ret == nat_align_up(self as nat, align as nat),
forall |n: nat| !(n >= self && #[trigger] (n % align as nat) == 0) || (ret <= n),
§Preconditions
  • align is a power of two.
  • align >= 2.
  • self + (align - 1) does not overflow.
§Postconditions
  • The function will not panic.
  • The return value is the smallest number that is greater than or equal to self and is a multiple of align.
Source§

exec fn align_down(self, align: Self) -> ret : Self

requires
exists |e: nat| pow2(e) == align,
align >= 2,
ensures
ret <= self,
ret % align == 0,
ret == nat_align_down(self as nat, align as nat),
forall |n: nat| !(n <= self && #[trigger] (n % align as nat) == 0) || (ret >= n),
§Preconditions
  • align is a power of two.
  • align >= 2.
§Postconditions
  • The function will not panic.
  • The return value is the greatest number that is smaller than or equal to self and is a multiple of align.
Source§

impl AlignExt for usize

§Verified Properties

§Safety

The implementation is written in safe Rust and there is no undefined behavior.

§Functional correctness

The implementation meets the specification given in the trait AlignExt.

Source§

exec fn align_up(self, align: Self) -> ret : Self

requires
exists |e: nat| pow2(e) == align,
align >= 2,
self + (align - 1) <= usize::MAX,
ensures
ret >= self,
ret % align == 0,
ret == nat_align_up(self as nat, align as nat),
forall |n: nat| !(n >= self && #[trigger] (n % align as nat) == 0) || (ret <= n),
§Preconditions
  • align is a power of two.
  • align >= 2.
  • self + (align - 1) does not overflow.
§Postconditions
  • The function will not panic.
  • The return value is the smallest number that is greater than or equal to self and is a multiple of align.
Source§

exec fn align_down(self, align: Self) -> ret : Self

requires
exists |e: nat| pow2(e) == align,
align >= 2,
ensures
ret <= self,
ret % align == 0,
ret == nat_align_down(self as nat, align as nat),
forall |n: nat| !(n <= self && #[trigger] (n % align as nat) == 0) || (ret >= n),
§Preconditions
  • align is a power of two.
  • align >= 2.
§Postconditions
  • The function will not panic.
  • The return value is the greatest number that is smaller than or equal to self and is a multiple of align.

Implementors§