Skip to main content

Nat

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

Nat is the unbounded non-negative arithmetic surface. Subtraction, division, and remainder still need explicit guards (x >= y, y > 0) before the operation can be used in verified code or specifications.

Import​

mo:core/Nat

Status​

  • Runtime module

Public API​

Types​

  • Nat

Modules​

  • Spec

Functions​

toText(n : Nat) : Text​

Converts between the module type and the target representation.

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

fromText(text : Text) : ?Nat​

Converts between the module type and the target representation.

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

fromInt(i : Int) : Nat​

Converts between the module type and the target representation.

Contract

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

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

toInt(n : Nat) : Int​

Converts between the module type and the target representation.

Contract

ensures result == (n : Int);

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

min(x : Nat, y : Nat) : Nat​

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 : Nat, y : Nat) : Nat​

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 : Nat, y : Nat) : 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 : Nat, y : Nat) : 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 : Nat, y : Nat) : 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 : Nat, y : Nat) : 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 : Nat, y : Nat) : 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 : Nat, y : Nat) : 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 : Nat, y : Nat) : 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.

add(x : Nat, y : Nat) : Nat​

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 : Nat, y : Nat) : Nat​

Returns the left operand minus the right operand.

Contract

requires x >= y;
ensures result + y == x;

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

mul(x : Nat, y : Nat) : Nat​

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 : Nat, y : Nat) : Nat​

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 : Nat, y : Nat) : Nat​

Returns the integer remainder, subject to the divisor precondition.

Contract

requires y > 0;
ensures result == x % y;
ensures result < y;

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

pow(x : Nat, y : Nat) : Nat​

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.

bitshiftLeft(x : Nat, y : Nat32) : Nat​

Performs the corresponding bit-level operation.

Contract

ensures result == Prim.shiftLeft(x, y);

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

bitshiftRight(x : Nat, y : Nat32) : Nat​

Performs the corresponding bit-level operation.

Contract

ensures result == Prim.shiftRight(x, y);

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

range(fromInclusive : Nat, toExclusive : Nat) : Iter.Iter<Nat>​

Creates an iterator over the requested numeric range or domain.

Contract

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

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

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

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<Nat>(pure func (k : Nat) : Bool = not Iter.Spec.contains<Nat>(result, k));
ensures (step > 0 and fromInclusive < toExclusive) ==> Iter.Spec.contains<Nat>(result, fromInclusive);
ensures (step < 0 and fromInclusive > toExclusive) ==> Iter.Spec.contains<Nat>(result, fromInclusive);
ensures (step > 0 and fromInclusive < toExclusive) ==>
Iter.Spec.forall<Nat>(pure func (k : Nat) : Bool =
Iter.Spec.contains<Nat>(result, k) ==> (k >= fromInclusive and k < toExclusive));
ensures (step < 0 and fromInclusive > toExclusive) ==>
Iter.Spec.forall<Nat>(pure func (k : Nat) : Bool =
Iter.Spec.contains<Nat>(result, k) ==> (k <= fromInclusive and k > toExclusive));

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

rangeInclusive(from : Nat, to : Nat) : Iter.Iter<Nat>​

Creates an iterator over the requested numeric range or domain.

Contract

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

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

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

Creates an iterator over the requested numeric range or domain.

Contract

ensures (from == to) ==> Iter.Spec.contains<Nat>(result, from);
ensures (from == to) ==> Iter.Spec.forall<Nat>(pure func (k : Nat) : Bool = Iter.Spec.contains<Nat>(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<Nat>(pure func (k : Nat) : Bool = not Iter.Spec.contains<Nat>(result, k));
ensures (from != to and step > 0 and from <= to) ==> Iter.Spec.contains<Nat>(result, from);
ensures (from != to and step < 0 and from >= to) ==> Iter.Spec.contains<Nat>(result, from);
ensures (step > 0 and from <= to) ==>
Iter.Spec.forall<Nat>(pure func (k : Nat) : Bool =
Iter.Spec.contains<Nat>(result, k) ==> (k >= from and k <= to));
ensures (step < 0 and from >= to) ==>
Iter.Spec.forall<Nat>(pure func (k : Nat) : Bool =
Iter.Spec.contains<Nat>(result, k) ==> (k <= from and k >= to));

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

allValues() : Iter.Iter<Nat>​

Creates an iterator over the requested numeric range or domain.

Contract

ensures Iter.Spec.forall<Nat>(pure func (k : Nat) : Bool = Iter.Spec.contains<Nat>(result, k));

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

Spec Module​

Spec Functions​

toText(n : Nat) : 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) : ?Nat​

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(n : Nat) : ()​

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

Contract

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

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

Summary​

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