Trait vstd::std_specs::range::StepSpec

source ·

pub trait StepSpecwhere
    Self: Sized,{
    // Required methods
    fn spec_is_lt(self, other: Self) -> bool;
    fn spec_steps_between(self, end: Self) -> Option<usize>;
    fn spec_steps_between_int(self, end: Self) -> int;
    fn spec_forward_checked(self, count: usize) -> Option<Self>;
    fn spec_forward_checked_int(self, count: int) -> Option<Self>;
    fn spec_backward_checked(self, count: usize) -> Option<Self>;
    fn spec_backward_checked_int(self, count: int) -> Option<Self>;
}

Required Methods§

source

spec fn spec_backward_checked_int(self, count: int) -> Option<Self>

Object Safety§

This trait is not object safe.

Implementations on Foreign Types§

source §

impl StepSpec for i8

source §

open spec fn spec_is_lt(self, other: Self) -> bool

{ self < other }

source §

open spec fn spec_steps_between(self, end: Self) -> Option<usize>

{
    let n = end - self;
    if usize::MIN <= n <= usize::MAX { Some(n as usize) } else { None }
}

source §

open spec fn spec_steps_between_int(self, end: Self) -> int

{ end - self }

source §

open spec fn spec_forward_checked(self, count: usize) -> Option<Self>

{ self.spec_forward_checked_int(count as int) }

source §

open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>

{ if self + count <= i8::MAX { Some((self + count) as i8) } else { None } }

source §

open spec fn spec_backward_checked(self, count: usize) -> Option<Self>

{ self.spec_backward_checked_int(count as int) }

source §

open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>

{ if self - count >= i8::MIN { Some((self - count) as i8) } else { None } }

source §

impl StepSpec for i16

source §

open spec fn spec_is_lt(self, other: Self) -> bool

{ self < other }

source §

open spec fn spec_steps_between(self, end: Self) -> Option<usize>

{
    let n = end - self;
    if usize::MIN <= n <= usize::MAX { Some(n as usize) } else { None }
}

source §

open spec fn spec_steps_between_int(self, end: Self) -> int

{ end - self }

source §

open spec fn spec_forward_checked(self, count: usize) -> Option<Self>

{ self.spec_forward_checked_int(count as int) }

source §

open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>

{ if self + count <= i16::MAX { Some((self + count) as i16) } else { None } }

source §

open spec fn spec_backward_checked(self, count: usize) -> Option<Self>

{ self.spec_backward_checked_int(count as int) }

source §

open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>

{ if self - count >= i16::MIN { Some((self - count) as i16) } else { None } }

source §

impl StepSpec for i32

source §

open spec fn spec_is_lt(self, other: Self) -> bool

{ self < other }

source §

open spec fn spec_steps_between(self, end: Self) -> Option<usize>

{
    let n = end - self;
    if usize::MIN <= n <= usize::MAX { Some(n as usize) } else { None }
}

source §

open spec fn spec_steps_between_int(self, end: Self) -> int

{ end - self }

source §

open spec fn spec_forward_checked(self, count: usize) -> Option<Self>

{ self.spec_forward_checked_int(count as int) }

source §

open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>

{ if self + count <= i32::MAX { Some((self + count) as i32) } else { None } }

source §

open spec fn spec_backward_checked(self, count: usize) -> Option<Self>

{ self.spec_backward_checked_int(count as int) }

source §

open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>

{ if self - count >= i32::MIN { Some((self - count) as i32) } else { None } }

source §

impl StepSpec for i64

source §

open spec fn spec_is_lt(self, other: Self) -> bool

{ self < other }

source §

open spec fn spec_steps_between(self, end: Self) -> Option<usize>

{
    let n = end - self;
    if usize::MIN <= n <= usize::MAX { Some(n as usize) } else { None }
}

source §

open spec fn spec_steps_between_int(self, end: Self) -> int

{ end - self }

source §

open spec fn spec_forward_checked(self, count: usize) -> Option<Self>

{ self.spec_forward_checked_int(count as int) }

source §

open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>

{ if self + count <= i64::MAX { Some((self + count) as i64) } else { None } }

source §

open spec fn spec_backward_checked(self, count: usize) -> Option<Self>

{ self.spec_backward_checked_int(count as int) }

source §

open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>

{ if self - count >= i64::MIN { Some((self - count) as i64) } else { None } }

source §

impl StepSpec for i128

source §

open spec fn spec_is_lt(self, other: Self) -> bool

{ self < other }

source §

open spec fn spec_steps_between(self, end: Self) -> Option<usize>

{
    let n = end - self;
    if usize::MIN <= n <= usize::MAX { Some(n as usize) } else { None }
}

source §

open spec fn spec_steps_between_int(self, end: Self) -> int

{ end - self }

source §

open spec fn spec_forward_checked(self, count: usize) -> Option<Self>

{ self.spec_forward_checked_int(count as int) }

source §

open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>

{ if self + count <= i128::MAX { Some((self + count) as i128) } else { None } }

source §

open spec fn spec_backward_checked(self, count: usize) -> Option<Self>

{ self.spec_backward_checked_int(count as int) }

source §

open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>

{ if self - count >= i128::MIN { Some((self - count) as i128) } else { None } }

source §

impl StepSpec for isize

source §

open spec fn spec_is_lt(self, other: Self) -> bool

{ self < other }

source §

open spec fn spec_steps_between(self, end: Self) -> Option<usize>

{
    let n = end - self;
    if usize::MIN <= n <= usize::MAX { Some(n as usize) } else { None }
}

source §

open spec fn spec_steps_between_int(self, end: Self) -> int

{ end - self }

source §

open spec fn spec_forward_checked(self, count: usize) -> Option<Self>

{ self.spec_forward_checked_int(count as int) }

source §

open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>

{ if self + count <= isize::MAX { Some((self + count) as isize) } else { None } }

source §

open spec fn spec_backward_checked(self, count: usize) -> Option<Self>

{ self.spec_backward_checked_int(count as int) }

source §

open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>

{ if self - count >= isize::MIN { Some((self - count) as isize) } else { None } }

source §

impl StepSpec for u8

source §

open spec fn spec_is_lt(self, other: Self) -> bool

{ self < other }

source §

open spec fn spec_steps_between(self, end: Self) -> Option<usize>

{
    let n = end - self;
    if usize::MIN <= n <= usize::MAX { Some(n as usize) } else { None }
}

source §

open spec fn spec_steps_between_int(self, end: Self) -> int

{ end - self }

source §

open spec fn spec_forward_checked(self, count: usize) -> Option<Self>

{ self.spec_forward_checked_int(count as int) }

source §

open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>

{ if self + count <= u8::MAX { Some((self + count) as u8) } else { None } }

source §

open spec fn spec_backward_checked(self, count: usize) -> Option<Self>

{ self.spec_backward_checked_int(count as int) }

source §

open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>

{ if self - count >= u8::MIN { Some((self - count) as u8) } else { None } }

source §

impl StepSpec for u16

source §

open spec fn spec_is_lt(self, other: Self) -> bool

{ self < other }

source §

open spec fn spec_steps_between(self, end: Self) -> Option<usize>

{
    let n = end - self;
    if usize::MIN <= n <= usize::MAX { Some(n as usize) } else { None }
}

source §

open spec fn spec_steps_between_int(self, end: Self) -> int

{ end - self }

source §

open spec fn spec_forward_checked(self, count: usize) -> Option<Self>

{ self.spec_forward_checked_int(count as int) }

source §

open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>

{ if self + count <= u16::MAX { Some((self + count) as u16) } else { None } }

source §

open spec fn spec_backward_checked(self, count: usize) -> Option<Self>

{ self.spec_backward_checked_int(count as int) }

source §

open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>

{ if self - count >= u16::MIN { Some((self - count) as u16) } else { None } }

source §

impl StepSpec for u32

source §

open spec fn spec_is_lt(self, other: Self) -> bool

{ self < other }

source §

open spec fn spec_steps_between(self, end: Self) -> Option<usize>

{
    let n = end - self;
    if usize::MIN <= n <= usize::MAX { Some(n as usize) } else { None }
}

source §

open spec fn spec_steps_between_int(self, end: Self) -> int

{ end - self }

source §

open spec fn spec_forward_checked(self, count: usize) -> Option<Self>

{ self.spec_forward_checked_int(count as int) }

source §

open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>

{ if self + count <= u32::MAX { Some((self + count) as u32) } else { None } }

source §

open spec fn spec_backward_checked(self, count: usize) -> Option<Self>

{ self.spec_backward_checked_int(count as int) }

source §

open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>

{ if self - count >= u32::MIN { Some((self - count) as u32) } else { None } }

source §

impl StepSpec for u64

source §

open spec fn spec_is_lt(self, other: Self) -> bool

{ self < other }

source §

open spec fn spec_steps_between(self, end: Self) -> Option<usize>

{
    let n = end - self;
    if usize::MIN <= n <= usize::MAX { Some(n as usize) } else { None }
}

source §

open spec fn spec_steps_between_int(self, end: Self) -> int

{ end - self }

source §

open spec fn spec_forward_checked(self, count: usize) -> Option<Self>

{ self.spec_forward_checked_int(count as int) }

source §

open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>

{ if self + count <= u64::MAX { Some((self + count) as u64) } else { None } }

source §

open spec fn spec_backward_checked(self, count: usize) -> Option<Self>

{ self.spec_backward_checked_int(count as int) }

source §

open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>

{ if self - count >= u64::MIN { Some((self - count) as u64) } else { None } }

source §

impl StepSpec for u128

source §

open spec fn spec_is_lt(self, other: Self) -> bool

{ self < other }

source §

open spec fn spec_steps_between(self, end: Self) -> Option<usize>

{
    let n = end - self;
    if usize::MIN <= n <= usize::MAX { Some(n as usize) } else { None }
}

source §

open spec fn spec_steps_between_int(self, end: Self) -> int

{ end - self }

source §

open spec fn spec_forward_checked(self, count: usize) -> Option<Self>

{ self.spec_forward_checked_int(count as int) }

source §

open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>

{ if self + count <= u128::MAX { Some((self + count) as u128) } else { None } }

source §

open spec fn spec_backward_checked(self, count: usize) -> Option<Self>

{ self.spec_backward_checked_int(count as int) }

source §

open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>

{ if self - count >= u128::MIN { Some((self - count) as u128) } else { None } }

source §

impl StepSpec for usize

source §

open spec fn spec_is_lt(self, other: Self) -> bool

{ self < other }

source §

open spec fn spec_steps_between(self, end: Self) -> Option<usize>

{
    let n = end - self;
    if usize::MIN <= n <= usize::MAX { Some(n as usize) } else { None }
}

source §

open spec fn spec_steps_between_int(self, end: Self) -> int

{ end - self }

source §

open spec fn spec_forward_checked(self, count: usize) -> Option<Self>

{ self.spec_forward_checked_int(count as int) }

source §

open spec fn spec_forward_checked_int(self, count: int) -> Option<Self>

{ if self + count <= usize::MAX { Some((self + count) as usize) } else { None } }

source §

open spec fn spec_backward_checked(self, count: usize) -> Option<Self>

{ self.spec_backward_checked_int(count as int) }

source §

open spec fn spec_backward_checked_int(self, count: int) -> Option<Self>

{ if self - count >= usize::MIN { Some((self - count) as usize) } else { None } }