Struct PeanoInt

pub struct PeanoInt(/* private fields */);

A peano integer wrapping a 64-bits integer.

See the module explanation.

Implementations

impl PeanoInt

pub fn new() -> Self

Create a new peano integer with value 0.

pure

ensures

result@ == 0

pub fn incr(&mut 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.

ensures

(^self)@ == (*self)@ + 1

pub fn to_u64(self) -> u64

Get the underlying integer.

pure

ensures

result@ == self@

pub fn to_i64(self) -> i64

Get the underlying integer.

pure

ensures

result@ == self@

pub fn to_u128(self) -> u128

Get the underlying integer.

pure

ensures

result@ == self@

pub fn to_i128(self) -> i128

Get the underlying integer.

pure

ensures

result@ == self@

Trait Implementations

impl Clone for PeanoInt

fn clone(&self) -> Self

ensures

Clone

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

Performs copy-assignment from source.

impl Default for PeanoInt

fn default() -> Self

ensures

Default

impl Default for PeanoInt

fn is_default(self) -> bool

logic(prophetic)

Default

impl From<PeanoInt> for i128

fn from(val: PeanoInt) -> Self

ensures

result@ == val@

impl From<PeanoInt> for i64

fn from(val: PeanoInt) -> Self

ensures

result@ == val@

impl From<PeanoInt> for u128

fn from(val: PeanoInt) -> Self

ensures

result@ == val@

impl From<PeanoInt> for u64

fn from(val: PeanoInt) -> Self

ensures

result@ == val@

impl View for PeanoInt

fn view(self) -> Int

logic

self.0.view()

type ViewTy = Int

impl Copy for PeanoInt