Skip to main content

NumExt

creusot_std::std::num

Trait NumExt 

Source 
pub trait NumExt {
    // Required methods
    fn leading_zeros_logic(self) -> u32;
    fn trailing_zeros_logic(self) -> u32;
    fn leading_ones_logic(self) -> u32;
    fn trailing_ones_logic(self) -> u32;
}

Required Methods§

Source

fn leading_zeros_logic(self) -> u32

logic ⚠

Source

fn trailing_zeros_logic(self) -> u32

logic ⚠

Source

fn leading_ones_logic(self) -> u32

logic ⚠

Source

fn trailing_ones_logic(self) -> u32

logic ⚠

Implementations on Foreign Types§

Source§

impl NumExt for u8

Source§

fn leading_zeros_logic(self) -> u32

logic(opaque) ⚠

ensures 

result <= $type::BITS

ensures

(result != $type::BITS) == (self >> ($type::BITS - result - 1u32) == $one)

ensures 

(result == $type::BITS) == (self == $zero)

Source§

fn trailing_zeros_logic(self) -> u32

logic(opaque) ⚠

ensures 

result <= $type::BITS

ensures

(result != $type::BITS) == (self << ($type::BITS - result - 1u32) == $one << ($type::BITS - 1u32))

ensures 

(result == $type::BITS) == (self == $zero)

Source§

fn leading_ones_logic(self) -> u32

logic(opaque) ⚠

ensures 

result <= $type::BITS

ensures

(result != $type::BITS) == (!self >> ($type::BITS - result - 1u32) == $zero)

ensures 

(result == $type::BITS) == (self == $type::MAX)

Source§

fn trailing_ones_logic(self) -> u32

logic(opaque) ⚠

ensures 

result <= $type::BITS

ensures

(result == $type::BITS) == (!self << ($type::BITS - result - 1u32) == $one << ($type::BITS - 1u32))

ensures 

(result == $type::BITS) == (self == $type::MAX)

Source§

impl NumExt for u16

Source§

fn leading_zeros_logic(self) -> u32

logic(opaque) ⚠

ensures 

result <= $type::BITS

ensures

(result != $type::BITS) == (self >> ($type::BITS - result - 1u32) == $one)

ensures 

(result == $type::BITS) == (self == $zero)

Source§

fn trailing_zeros_logic(self) -> u32

logic(opaque) ⚠

ensures 

result <= $type::BITS

ensures

(result != $type::BITS) == (self << ($type::BITS - result - 1u32) == $one << ($type::BITS - 1u32))

ensures 

(result == $type::BITS) == (self == $zero)

Source§

fn leading_ones_logic(self) -> u32

logic(opaque) ⚠

ensures 

result <= $type::BITS

ensures

(result != $type::BITS) == (!self >> ($type::BITS - result - 1u32) == $zero)

ensures 

(result == $type::BITS) == (self == $type::MAX)

Source§

fn trailing_ones_logic(self) -> u32

logic(opaque) ⚠

ensures 

result <= $type::BITS

ensures

(result == $type::BITS) == (!self << ($type::BITS - result - 1u32) == $one << ($type::BITS - 1u32))

ensures 

(result == $type::BITS) == (self == $type::MAX)

Source§

impl NumExt for u32

Source§

fn leading_zeros_logic(self) -> u32

logic(opaque) ⚠

ensures 

result <= $type::BITS

ensures

(result != $type::BITS) == (self >> ($type::BITS - result - 1u32) == $one)

ensures 

(result == $type::BITS) == (self == $zero)

Source§

fn trailing_zeros_logic(self) -> u32

logic(opaque) ⚠

ensures 

result <= $type::BITS

ensures

(result != $type::BITS) == (self << ($type::BITS - result - 1u32) == $one << ($type::BITS - 1u32))

ensures 

(result == $type::BITS) == (self == $zero)

Source§

fn leading_ones_logic(self) -> u32

logic(opaque) ⚠

ensures 

result <= $type::BITS

ensures

(result != $type::BITS) == (!self >> ($type::BITS - result - 1u32) == $zero)

ensures 

(result == $type::BITS) == (self == $type::MAX)

Source§

fn trailing_ones_logic(self) -> u32

logic(opaque) ⚠

ensures 

result <= $type::BITS

ensures

(result == $type::BITS) == (!self << ($type::BITS - result - 1u32) == $one << ($type::BITS - 1u32))

ensures 

(result == $type::BITS) == (self == $type::MAX)

Source§

impl NumExt for u64

Source§

fn leading_zeros_logic(self) -> u32

logic(opaque) ⚠

ensures 

result <= $type::BITS

ensures

(result != $type::BITS) == (self >> ($type::BITS - result - 1u32) == $one)

ensures 

(result == $type::BITS) == (self == $zero)

Source§

fn trailing_zeros_logic(self) -> u32

logic(opaque) ⚠

ensures 

result <= $type::BITS

ensures

(result != $type::BITS) == (self << ($type::BITS - result - 1u32) == $one << ($type::BITS - 1u32))

ensures 

(result == $type::BITS) == (self == $zero)

Source§

fn leading_ones_logic(self) -> u32

logic(opaque) ⚠

ensures 

result <= $type::BITS

ensures

(result != $type::BITS) == (!self >> ($type::BITS - result - 1u32) == $zero)

ensures 

(result == $type::BITS) == (self == $type::MAX)

Source§

fn trailing_ones_logic(self) -> u32

logic(opaque) ⚠

ensures 

result <= $type::BITS

ensures

(result == $type::BITS) == (!self << ($type::BITS - result - 1u32) == $one << ($type::BITS - 1u32))

ensures 

(result == $type::BITS) == (self == $type::MAX)

Source§

impl NumExt for u128

Source§

fn leading_zeros_logic(self) -> u32

logic(opaque) ⚠

ensures 

result <= $type::BITS

ensures

(result != $type::BITS) == (self >> ($type::BITS - result - 1u32) == $one)

ensures 

(result == $type::BITS) == (self == $zero)

Source§

fn trailing_zeros_logic(self) -> u32

logic(opaque) ⚠

ensures 

result <= $type::BITS

ensures

(result != $type::BITS) == (self << ($type::BITS - result - 1u32) == $one << ($type::BITS - 1u32))

ensures 

(result == $type::BITS) == (self == $zero)

Source§

fn leading_ones_logic(self) -> u32

logic(opaque) ⚠

ensures 

result <= $type::BITS

ensures

(result != $type::BITS) == (!self >> ($type::BITS - result - 1u32) == $zero)

ensures 

(result == $type::BITS) == (self == $type::MAX)

Source§

fn trailing_ones_logic(self) -> u32

logic(opaque) ⚠

ensures 

result <= $type::BITS

ensures

(result == $type::BITS) == (!self << ($type::BITS - result - 1u32) == $one << ($type::BITS - 1u32))

ensures 

(result == $type::BITS) == (self == $type::MAX)

Source§

impl NumExt for usize

Source§

fn leading_zeros_logic(self) -> u32

logic(opaque) ⚠

ensures 

result <= $type::BITS

ensures

(result != $type::BITS) == (self >> ($type::BITS - result - 1u32) == $one)

ensures 

(result == $type::BITS) == (self == $zero)

Source§

fn trailing_zeros_logic(self) -> u32

logic(opaque) ⚠

ensures 

result <= $type::BITS

ensures

(result != $type::BITS) == (self << ($type::BITS - result - 1u32) == $one << ($type::BITS - 1u32))

ensures 

(result == $type::BITS) == (self == $zero)

Source§

fn leading_ones_logic(self) -> u32

logic(opaque) ⚠

ensures 

result <= $type::BITS

ensures

(result != $type::BITS) == (!self >> ($type::BITS - result - 1u32) == $zero)

ensures 

(result == $type::BITS) == (self == $type::MAX)

Source§

fn trailing_ones_logic(self) -> u32

logic(opaque) ⚠

ensures 

result <= $type::BITS

ensures

(result == $type::BITS) == (!self << ($type::BITS - result - 1u32) == $one << ($type::BITS - 1u32))

ensures 

(result == $type::BITS) == (self == $type::MAX)

Implementors§