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 lt_log_total(self, other: Self)

logic

ensures

self < other || self == other || other < self

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

The comparison operation.

impl PartialEq for PeanoInt

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

ghost

ensures

result == (*self == *other)

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

Inequality operator !=.

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 PartialOrdLogic for PeanoInt

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

logic(open, inline)

self.0 < o.0

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

logic(open, inline)

self.0 <= o.0

fn irreflexive(self)

logic

ensures

!(self < self)

fn transitive(x: Self, y: Self, z: Self)

logic

requires

x < y

requires

y < z

ensures

x < z

fn le_lt_log(self, other: Self)

logic

ensures

(self <= other) == (self < other || self == other)

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

The logical > operation.

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

The logical >= operation.

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

logic(open, sealed)

impl View for PeanoInt

fn view(self) -> u64

logic(open, inline)

self.0

type ViewTy = u64