Int

Reference for mo:core/Int in the core library.

Int is the unbounded signed arithmetic surface. Basic arithmetic helpers have contracts that mirror the operators, while division and remainder require a non-zero divisor. Use the Spec helpers and axiom modules when a proof needs more algebra than the local contract exposes.

Import

mo:core/Int

Status

• Runtime module

Public API

Types

• Int

Modules

• Spec

Functions

abs(x : Int) : Nat

Returns the absolute value.

Contract

ensures result == Prim.abs(x);

Use when: code or specifications need this operation with the documented contract.

toText(x : Int) : Text

Converts between the module type and the target representation.

Use when: crossing between this module's value and another representation.

fromText(text : Text) : ?Int

Converts between the module type and the target representation.

Use when: crossing between this module's value and another representation.

toNat(int : Int) : Nat

Converts between the module type and the target representation.

Contract

requires int >= 0;
ensures result == Prim.abs(int);

Use when: crossing between this module's value and another representation.

fromNat(nat : Nat) : Int

Converts between the module type and the target representation.

Contract

ensures result == (nat : Int);

Use when: crossing between this module's value and another representation.

min(x : Int, y : Int) : Int

Returns the selected bound according to the module's ordering.

Contract

ensures result == (if (x < y) { x } else { y });

Use when: code or specifications need this operation with the documented contract.

max(x : Int, y : Int) : Int

Returns the selected bound according to the module's ordering.

Contract

ensures result == (if (x < y) { y } else { x });

Use when: code or specifications need this operation with the documented contract.

equal(x : Int, y : Int) : Bool

Compares the supplied values and relates the result to the underlying order.

Contract

ensures result == (x == y);

Use when: code or contracts need an explicit comparison helper instead of an operator.

notEqual(x : Int, y : Int) : Bool

Compares the supplied values and relates the result to the underlying order.

Contract

ensures result == (x != y);

Use when: code or contracts need an explicit comparison helper instead of an operator.

less(x : Int, y : Int) : Bool

Compares the supplied values and relates the result to the underlying order.

Contract

ensures result == (x < y);

Use when: code or contracts need an explicit comparison helper instead of an operator.

lessOrEqual(x : Int, y : Int) : Bool

Compares the supplied values and relates the result to the underlying order.

Contract

ensures result == (x <= y);

Use when: code or contracts need an explicit comparison helper instead of an operator.

greater(x : Int, y : Int) : Bool

Compares the supplied values and relates the result to the underlying order.

Contract

ensures result == (x > y);

Use when: code or contracts need an explicit comparison helper instead of an operator.

greaterOrEqual(x : Int, y : Int) : Bool

Compares the supplied values and relates the result to the underlying order.

Contract

ensures result == (x >= y);

Use when: code or contracts need an explicit comparison helper instead of an operator.

compare(x : Int, y : Int) : Types.Order

Compares the supplied values and relates the result to the underlying order.

Contract

ensures result == #less ==> x < y;
ensures result == #equal ==> x == y;
ensures result == #greater ==> x > y;
ensures x < y ==> result == #less;
ensures x == y ==> result == #equal;
ensures x > y ==> result == #greater;

Use when: code or contracts need an explicit comparison helper instead of an operator.

neg(x : Int) : Int

Returns the arithmetic negation.

Contract

ensures result == -x;

Use when: code or specifications need this operation with the documented contract.

add(x : Int, y : Int) : Int

Returns the sum of the two operands.

Contract

ensures result == x + y;

Use when: the postcondition must relate the updated value to the previous one.

sub(x : Int, y : Int) : Int

Returns the left operand minus the right operand.

Contract

ensures result == x - y;

Use when: code or specifications need this operation with the documented contract.

mul(x : Int, y : Int) : Int

Returns the product of the two operands.

Contract

ensures result == x * y;

Use when: code or specifications need this operation with the documented contract.

div(x : Int, y : Int) : Int

Returns the integer quotient, subject to the divisor precondition.

Contract

requires y != 0;
ensures result == x / y;

Use when: code or specifications need this operation with the documented contract.

rem(x : Int, y : Int) : Int

Returns the integer remainder, subject to the divisor precondition.

Contract

requires y != 0;
ensures result == x % y;

Use when: code or specifications need this operation with the documented contract.

pow(x : Int, y : Int) : Int

Returns the left operand raised to the supplied exponent.

Contract

ensures result == x ** y;

Use when: code or specifications need this operation with the documented contract.

range(fromInclusive : Int, toExclusive : Int) : Iter.Iter<Int>

Creates an iterator over the requested numeric range or domain.

Contract

ensures Iter.Spec.forall<Int>(pure func (k : Int) : Bool =
Iter.Spec.contains<Int>(result, k) ==> (k >= fromInclusive and k < toExclusive));
ensures Iter.Spec.forall<Int>(pure func (k : Int) : Bool =
(k >= fromInclusive and k < toExclusive) ==> Iter.Spec.contains<Int>(result, k));

Use when: iteration boundaries should be explicit in code and examples.

rangeBy(fromInclusive : Int, toExclusive : Int, step : Int) : Iter.Iter<Int>

Creates an iterator over the requested numeric range or domain.

Contract

ensures (step == 0 or (step > 0 and fromInclusive >= toExclusive) or (step < 0 and fromInclusive <= toExclusive)) ==>
Iter.Spec.forall<Int>(pure func (k : Int) : Bool = not Iter.Spec.contains<Int>(result, k));
ensures (step > 0 and fromInclusive < toExclusive) ==> Iter.Spec.contains<Int>(result, fromInclusive);
ensures (step < 0 and fromInclusive > toExclusive) ==> Iter.Spec.contains<Int>(result, fromInclusive);
ensures (step > 0 and fromInclusive < toExclusive) ==>
Iter.Spec.forall<Int>(pure func (k : Int) : Bool =
Iter.Spec.contains<Int>(result, k) ==> (k >= fromInclusive and k < toExclusive));
ensures (step < 0 and fromInclusive > toExclusive) ==>
Iter.Spec.forall<Int>(pure func (k : Int) : Bool =
Iter.Spec.contains<Int>(result, k) ==> (k <= fromInclusive and k > toExclusive));

Use when: iteration boundaries should be explicit in code and examples.

rangeInclusive(from : Int, to : Int) : Iter.Iter<Int>

Creates an iterator over the requested numeric range or domain.

Contract

ensures (from > to) ==> Iter.Spec.forall<Int>(pure func (k : Int) : Bool = not Iter.Spec.contains<Int>(result, k));
ensures (from <= to) ==> Iter.Spec.contains<Int>(result, from);
ensures Iter.Spec.forall<Int>(pure func (k : Int) : Bool =
Iter.Spec.contains<Int>(result, k) ==> (k >= from and k <= to));
ensures Iter.Spec.forall<Int>(pure func (k : Int) : Bool =
(k >= from and k <= to) ==> Iter.Spec.contains<Int>(result, k));

Use when: iteration boundaries should be explicit in code and examples.

rangeByInclusive(from : Int, to : Int, step : Int) : Iter.Iter<Int>

Creates an iterator over the requested numeric range or domain.

Contract

ensures (from == to) ==> Iter.Spec.contains<Int>(result, from);
ensures (from == to) ==> Iter.Spec.forall<Int>(pure func (k : Int) : Bool = Iter.Spec.contains<Int>(result, k) ==> k == from);
ensures (from != to and (step == 0 or (step > 0 and from > to) or (step < 0 and from < to))) ==>
Iter.Spec.forall<Int>(pure func (k : Int) : Bool = not Iter.Spec.contains<Int>(result, k));
ensures (from != to and step > 0 and from <= to) ==> Iter.Spec.contains<Int>(result, from);
ensures (from != to and step < 0 and from >= to) ==> Iter.Spec.contains<Int>(result, from);
ensures (step > 0 and from <= to) ==>
Iter.Spec.forall<Int>(pure func (k : Int) : Bool =
Iter.Spec.contains<Int>(result, k) ==> (k >= from and k <= to));
ensures (step < 0 and from >= to) ==>
Iter.Spec.forall<Int>(pure func (k : Int) : Bool =
Iter.Spec.contains<Int>(result, k) ==> (k <= from and k >= to));

Use when: iteration boundaries should be explicit in code and examples.

Spec Module

Spec Functions

toText(x : Int) : Text

Provides a ghost/spec-only abstraction for contracts and proofs.

Use when: Use in contracts, ghost code, or lemmas when the runtime value needs an abstract proof model.

fromText(text : Text) : ?Int

Provides a ghost/spec-only abstraction for contracts and proofs.

Use when: Use in contracts, ghost code, or lemmas when the runtime value needs an abstract proof model.

Spec Lemmas

roundtrip(x : Int) : ()

Establishes fromText(toText(x)) == ?x in the current proof context.

Contract

ensures fromText(toText(x)) == ?x;

Use when: a proof needs this fact explicitly and the solver has not derived it automatically.

Summary

• Runtime module under mo:core/Int.
• Exposes 25 public functions.
• Includes 2 spec helpers in Spec.
• Includes 1 trusted spec lemmas in Spec.