Struct PeanoInt 

#[non_exhaustive]
#[repr(transparent)]
pub struct PeanoInt(pub u64);

A peano integer wrapping a 64-bits integer.

See the module explanation.

Tuple Fields (Non-exhaustive)

Non-exhaustive structs could have additional fields added in future. Therefore, non-exhaustive structs cannot be constructed in external crates using the traditional Struct { .. } syntax; cannot be matched against without a wildcard ..; and struct update syntax will not work.

0: u64

Implementations

impl PeanoInt

pub fn new() -> Self

Create a new peano integer with value 0.

ghost

ensures

result.0 == 0u64

pub fn incr(self) -> Self

Increase the integer by one.

This method guarantees that increments cannot get optimized together, e.g. that

let mut x = PeanoInt::new();
for _ in 0..1_000_000 {
    x.incr();
}

Does not get optimized down to a single addition.

Since the backing integer is 64 bits long, no program could ever actually reach the point where the integer overflows.

terminates

ensures

result.0@ == self.0@ + 1

pub fn to_u64(self) -> u64

Get the underlying integer.

ghost

ensures

result == self.0

pub fn to_i64(self) -> i64

Get the underlying integer.

ghost

ensures

result@ == self.0@

pub fn to_u128(self) -> u128

Get the underlying integer.

ghost

ensures

result@ == self.0@

pub fn to_i128(self) -> i128

Get the underlying integer.

ghost

ensures

result@ == self.0@

Trait Implementations

impl Clone for PeanoInt

fn clone(&self) -> Self

ensures

pub u64

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Copy for PeanoInt

impl DeepModel for PeanoInt

fn deep_model(self) -> u64

logic(open, inline)

self.0

type DeepModelTy = u64

impl Default for PeanoInt

fn default() -> Self

ensures

Default

impl Eq for PeanoInt

impl From<PeanoInt> for u64

fn from(val: PeanoInt) -> Self

ghost

ensures

result == val.0

impl From<PeanoInt> for i64

fn from(val: PeanoInt) -> Self

ghost

ensures

result@ == val.0@

impl From<PeanoInt> for u128

fn from(val: PeanoInt) -> Self

ghost

ensures

result@ == val.0@

impl From<PeanoInt> for i128

fn from(val: PeanoInt) -> Self

ghost

ensures

result@ == val.0@

impl Ord for PeanoInt

fn cmp(&self, other: &Self) -> Ordering

ghost

ensures

result == (*self).cmp_log(*other)

fn max(self, other: Self) -> Self

where Self: Sized,

Compares and returns the maximum of two values.

fn min(self, other: Self) -> Self

where Self: Sized,

Compares and returns the minimum of two values.

fn clamp(self, min: Self, max: Self) -> Self

where Self: Sized,

Restrict a value to a certain interval.

impl OrdLogic for PeanoInt

fn cmp_log(self, o: Self) -> Ordering

logic(open, inline)

self.0.cmp_log(o.0)

fn le_log(self, o: Self) -> bool

logic(open, inline)

self.0.le_log(o.0)

fn lt_log(self, o: Self) -> bool

logic(open, inline)

self.0.lt_log(o.0)

fn ge_log(self, o: Self) -> bool

logic(open, inline)

self.0.ge_log(o.0)

fn gt_log(self, o: Self) -> bool

logic(open, inline)

self.0.gt_log(o.0)

fn cmp_le_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.le_log(y) == (x.cmp_log(y) != core::cmp::Ordering::Greater)

fn cmp_lt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.lt_log(y) == (x.cmp_log(y) == core::cmp::Ordering::Less)

fn cmp_ge_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.ge_log(y) == (x.cmp_log(y) != core::cmp::Ordering::Less)

fn cmp_gt_log(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

x.gt_log(y) == (x.cmp_log(y) == core::cmp::Ordering::Greater)

fn refl(x: Self)

logic(open(pub(self)), law)

ensures

x.cmp_log(x) == core::cmp::Ordering::Equal

fn trans(x: Self, y: Self, z: Self, o: Ordering)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == o

requires

y.cmp_log(z) == o

ensures

x.cmp_log(z) == o

fn antisym1(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == core::cmp::Ordering::Less

ensures

y.cmp_log(x) == core::cmp::Ordering::Greater

fn antisym2(x: Self, y: Self)

logic(open(pub(self)), law)

requires

x.cmp_log(y) == core::cmp::Ordering::Greater

ensures

y.cmp_log(x) == core::cmp::Ordering::Less

fn eq_cmp(x: Self, y: Self)

logic(open(pub(self)), law)

ensures

(x == y) == (x.cmp_log(y) == core::cmp::Ordering::Equal)

impl PartialEq for PeanoInt

fn eq(&self, other: &Self) -> bool

ghost

ensures

result == (*self == *other)

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl PartialOrd for PeanoInt

fn partial_cmp(&self, other: &Self) -> Option<Ordering>

ghost

ensures

result == Some((*self).cmp_log(*other))

fn lt(&self, other: &Self) -> bool

ghost

ensures

result == (self@ < other@)

fn le(&self, other: &Self) -> bool

ghost

ensures

result == (self@ <= other@)

fn gt(&self, other: &Self) -> bool

ghost

ensures

result == (self@ > other@)

fn ge(&self, other: &Self) -> bool

ghost

ensures

result == (self@ >= other@)

impl View for PeanoInt

fn view(self) -> u64

logic(open, inline)

self.0

type ViewTy = u64