Struct Int 

pub struct Int;

An unbounded, mathematical integer.

This type cannot be only be constructed in logical or ghost code.

Integers in pearlite

Note that in pearlite, all integer literals are of type Int:

let x = 1i32;
//             ↓ need to use the view operator to convert `i32` to `Int`
proof_assert!(x@ == 1);

You can use the usual operators on integers: +, -, *, / and %.

Note that those operators are not available in ghost code.

Implementations

impl Int

pub fn pow(self, p: Int) -> Int

Compute self^p.

Example

proof_assert!(3.pow(4) == 729);

logic

pub fn pow2(self) -> Int

Compute 2^p.

Example

proof_assert!(pow2(4) == 16);

logic

pub fn max(self, x: Int) -> Int

Compute the maximum of self and x.

Example

proof_assert!(10.max(2) == 10);

logic

pub fn min(self, x: Int) -> Int

Compute the minimum of self and x.

Example

proof_assert!(10.max(2) == 2);

logic

pub fn div_euclid(self, d: Int) -> Int

Compute the euclidean division of self by d.

Example

proof_assert!(10.div_euclid(3) == 3);

logic

pub fn rem_euclid(self, d: Int) -> Int

Compute the remainder of the euclidean division of self by d.

Example

 proof_assert!(10.rem_euclid(3) == 1);

logic

pub fn abs_diff(self, other: Int) -> Int

Compute the absolute difference of self and x.

Example

proof_assert!(10.abs_diff(3) == 7);
proof_assert!(3.abs_diff(10) == 7);
proof_assert!((-5).abs_diff(5) == 10);

logic(open)

if self < other { other - self } else { self - other }

impl Int

pub fn new(value: i128) -> Ghost<Self>

Create a new Int value

The result is wrapped in a Ghost, so that it can only be access inside a ghost! block.

You should not have to use this method directly: instead, use the int suffix inside of a ghost block:

let x: Ghost<Int> = ghost!(1int);
ghost! {
    let y: Int = 2int;
};

terminates

ghost

ensures

*result == value@

pub fn incr_ghost(&mut self)

terminates

ghost

ensures

^self == *self + 1

pub fn decr_ghost(&mut self)

terminates

ghost

ensures

^self == *self - 1

Trait Implementations

impl Add for Int

fn add(self, other: Int) -> Self

terminates

ghost

ensures

result == self + other

type Output = Int

The resulting type after applying the + operator.

impl AddLogic for Int

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

logic

type Output = Int

impl Clone for Int

fn clone(&self) -> Self

terminates

ghost

ensures

result == *self

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

Performs copy-assignment from source.

impl DeepModel for Int

fn deep_model(self) -> Self::DeepModelTy

logic(open, inline)

self

type DeepModelTy = Int

impl Div for Int

fn div(self, other: Int) -> Self

terminates

ghost

ensures

result == self / other

type Output = Int

The resulting type after applying the / operator.

impl DivLogic for Int

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

logic

type Output = Int

impl<T> Index<Int> for Seq<T>

fn index(&self, index: Int) -> &Self::Output

terminates

ghost

requires

0 <= index && index < self.len()

ensures

*result == self[index]

type Output = T

The returned type after indexing.

impl<T> IndexLogic<Int> for [T]

fn index_logic(self, ix: Int) -> Self::Item

logic(open, inline)

self@[ix]

type Item = T

impl<T, const N: usize> IndexLogic<Int> for [T; N]

fn index_logic(self, ix: Int) -> Self::Item

logic(open, inline)

self@[ix]

type Item = T

impl<T> IndexLogic<Int> for Seq<T>

fn index_logic(self, _: Int) -> Self::Item

logic

type Item = T

impl<T, A: Allocator> IndexLogic<Int> for Vec<T, A>

Available on crate feature nightly only.

fn index_logic(self, ix: Int) -> Self::Item

logic(open, inline)

self@[ix]

type Item = T

impl<T, A: Allocator> IndexLogic<Int> for VecDeque<T, A>

Available on crate feature nightly only.

fn index_logic(self, ix: Int) -> Self::Item

logic(open, inline)

self@[ix]

type Item = T

impl<T> IndexMut<Int> for Seq<T>

fn index_mut(&mut self, index: Int) -> &mut Self::Output

terminates

ghost

requires

0 <= index && index < self.len()

ensures

(*self).len() == (^self).len()

ensures

*result == (*self)[index] && ^result == (^self)[index]

ensures

forall<i> i != index ==> (*self).get(i) == (^self).get(i)

impl LocalUpdate<Int> for Int

fn premise(self, _: Int, _: Int) -> bool

logic(open, inline)

true

fn update(self, from_auth: Int, from_frag: Int) -> (Int, Int)

logic(open, inline)

from_auth + self, from_frag + self

fn frame_preserving(self, from_auth: Int, from_frag: Int, frame: Option<Int>)

logic

requires

self.premise(from_auth, from_frag)

requires

Some(from_frag).op(frame) == Some(Some(from_auth))

ensures

let (to_auth, to_frag) = LocalUpdate::update(self, from_auth, from_frag);
Some(to_frag).op(frame) == Some(Some(to_auth))

impl Mul for Int

fn mul(self, other: Int) -> Self

terminates

ghost

ensures

result == self * other

type Output = Int

The resulting type after applying the * operator.

impl MulLogic for Int

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

logic

type Output = Int

impl Neg for Int

fn neg(self) -> Self

terminates

ghost

ensures

result == -self

type Output = Int

The resulting type after applying the - operator.

impl NegLogic for Int

fn neg(self) -> Self

logic

type Output = Int

impl OrdLogic for Int

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

logic(open)

/* Macro-generated */

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

logic

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

logic

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

logic

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

logic

fn cmp_le_log(x: Self, y: Self)

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

ensures

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

fn cmp_lt_log(x: Self, y: Self)

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

ensures

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

fn cmp_ge_log(x: Self, y: Self)

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

ensures

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

fn cmp_gt_log(x: Self, y: Self)

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

ensures

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

fn refl(x: Self)

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

ensures

x.cmp_log(x) == 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) == Ordering::Less

ensures

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

fn antisym2(x: Self, y: Self)

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

requires

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

ensures

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

fn eq_cmp(x: Self, y: Self)

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

ensures

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

impl PartialEq for Int

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

terminates

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 Int

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

terminates

ghost

ensures

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

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

terminates

ghost

ensures

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

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

terminates

ghost

ensures

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

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

terminates

ghost

ensures

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

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

terminates

ghost

ensures

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

impl Plain for Int

fn into_ghost(snap: Snapshot<Self>) -> Ghost<Self>

ensures

*result == *snap

terminates

ghost

impl RA for Int

fn op(self, other: Self) -> Option<Int>

logic(open, inline)

Some(self + other)

fn factor(self, factor: Self) -> Option<Self>

logic(open, inline)

Some(self - factor)

ensures

match result {
    Some(c) => factor.op(c) == Some(self),
    None => false,
}

fn commutative(a: Self, b: Self)

logic(law)

ensures

a.op(b) == b.op(a)

fn associative(a: Self, b: Self, c: Self)

logic

ensures

a.op(b).and_then_logic(|ab: Self| ab.op(c)) == b.op(c).and_then_logic(|bc| a.op(bc))

fn core(self) -> Option<Self>

logic(open, inline)

Some(0)

fn core_idemp(self)

logic

ensures

let c = self.core().unwrap_logic();
c.op(c) == Some(c)

ensures

self.core().unwrap_logic().op(self) == Some(self)

fn core_is_maximal_idemp(self, i: Self)

logic

requires

i.op(i) == Some(i)

requires

i.op(self) == Some(self)

ensures

match self.core() {
    Some(c) => i.incl(c),
    None => false,
}

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

logic(open, inline)

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

Inclusion of RA.

fn incl_op(self, other: Self, comb: Self)

logic(law)

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

logic(open, sealed)

fn incl_eq_op(a: Self, b: Self, x: Self) -> bool

logic(open, sealed)

fn update(self, x: Self) -> bool

Ensures that we can go from self to x without making composition with the frame invalid.

fn update_nondet(self, s: Set<Self>) -> bool

This is used in Resource::update_nondet.

fn associative_none(a: Self, b: Self, c: Self, bc: Self)

Specialized version of Self::associative, in the case where a.op(b) == None.

fn associative_some(a: Self, b: Self, c: Self, ab: Self, bc: Self)

Specialized version of Self::associative, in the case where a.op(b) and b.op(c) are both valid.

fn incl_transitive(a: Self, b: Self, c: Self)

RA::incl is transitive.

impl Rem for Int

fn rem(self, other: Int) -> Self

terminates

ghost

ensures

result == self % other

type Output = Int

The resulting type after applying the % operator.

impl RemLogic for Int

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

logic

type Output = Int

impl Sub for Int

fn sub(self, other: Int) -> Self

terminates

ghost

ensures

result == self - other

type Output = Int

The resulting type after applying the - operator.

impl SubLogic for Int

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

logic

type Output = Int

impl UnitRA for Int

fn unit() -> Self

logic(open, inline)

0

ensures

forall<x: Self> #[trigger(x.op(result))] x.op(result) == Some(x)

fn core_total(self) -> Self

logic(open, inline)

0

ensures

self.core() == Some(result)

fn core_total_idemp(self)

logic

ensures

self.core_total().op(self.core_total()) == Some(self.core_total())

ensures

self.core_total().op(self) == Some(self)

fn incl_refl()

In unitary RAs, the inclusion relation is reflexive

fn unit_core()

The unit is its own core

impl WellFounded for Int

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

logic(open, inline)

self >= 0 && self > other

fn no_infinite_decreasing_sequence(s: Mapping<Int, Self>) -> Int

logic(opaque)

ensures

result >= 0

ensures

!Self::well_founded_relation(s[result], s[result + 1])

impl Copy for Int