Nat32

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

Nat32 is an unsigned 32-bit surface used by hashing, counters, and bit-level APIs. Checked operations require range facts; wrap operations intentionally discard overflow.

Import

mo:core/Nat32

Status

• Runtime module

Public API

Types

• Nat32

Values

• maxValue

Functions

toNatSpec(x : Nat32) : Nat

Converts between the module type and the target representation.

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

toNat(x : Nat32) : Nat

Converts between the module type and the target representation.

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

fromNat(n : Nat) : Nat32

Converts between the module type and the target representation.

Contract

requires n <= 4_294_967_295;

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

fromNat16(x : Nat16) : Nat32

Converts between the module type and the target representation.

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

toNat16(x : Nat32) : Nat16

Converts between the module type and the target representation.

Contract

requires x <= (65_535 : Nat32);

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

fromNat64(x : Nat64) : Nat32

Converts between the module type and the target representation.

Contract

requires x <= (4_294_967_295 : Nat64);

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

toNat64(x : Nat32) : Nat64

Converts between the module type and the target representation.

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

fromIntWrap(x : Int) : Nat32

Converts between the module type and the target representation.

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

toText(x : Nat32) : Text

Converts between the module type and the target representation.

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

min(x : Nat32, y : Nat32) : Nat32

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

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

Returns the sum of the two operands.

Contract

requires x + y <= (4_294_967_295 : Nat32);
ensures result == x + y;

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

sub(x : Nat32, y : Nat32) : Nat32

Returns the left operand minus the right operand.

Contract

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

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

mul(x : Nat32, y : Nat32) : Nat32

Returns the product of the two operands.

Contract

requires x * y <= (4_294_967_295 : Nat32);
ensures result == x * y;

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

div(x : Nat32, y : Nat32) : Nat32

Returns the integer quotient, subject to the divisor precondition.

Contract

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

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

rem(x : Nat32, y : Nat32) : Nat32

Returns the integer remainder, subject to the divisor precondition.

Contract

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

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

pow(x : Nat32, y : Nat32) : Nat32

Returns the left operand raised to the supplied exponent.

Contract

requires y <= (1 : Nat32) or Nat.pow(toNatSpec(x), toNatSpec(y)) <= 4_294_967_295;
ensures toNatSpec(result) == Nat.pow(toNatSpec(x), toNatSpec(y));
ensures y == 0 ==> result == 1;
ensures y == 1 ==> result == x;

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

bitnot(x : Nat32) : Nat32

Performs the corresponding bit-level operation.

Contract

ensures result + x == maxValue;

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

bitand(x : Nat32, y : Nat32) : Nat32

Performs the corresponding bit-level operation.

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

bitor(x : Nat32, y : Nat32) : Nat32

Performs the corresponding bit-level operation.

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

bitxor(x : Nat32, y : Nat32) : Nat32

Performs the corresponding bit-level operation.

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

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

Performs the corresponding bit-level operation.

Contract

ensures y == 0 ==> result == x;

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

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

Performs the corresponding bit-level operation.

Contract

ensures y == 0 ==> result == x;

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

bitrotLeft(x : Nat32, y : Nat32) : Nat32

Performs the corresponding bit-level operation.

Contract

ensures y == 0 ==> result == x;

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

bitrotRight(x : Nat32, y : Nat32) : Nat32

Performs the corresponding bit-level operation.

Contract

ensures y == 0 ==> result == x;

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

bittest(x : Nat32, p : Nat) : Bool

Performs the corresponding bit-level operation.

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

bitset(x : Nat32, p : Nat) : Nat32

Performs the corresponding bit-level operation.

Contract

ensures p >= 32 ==> result == x;

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

bitclear(x : Nat32, p : Nat) : Nat32

Performs the corresponding bit-level operation.

Contract

ensures p >= 32 ==> result == x;

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

bitflip(x : Nat32, p : Nat) : Nat32

Performs the corresponding bit-level operation.

Contract

ensures p >= 32 ==> result == x;

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

bitcountNonZero(x : Nat32) : Nat32

Performs the corresponding bit-level operation.

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

bitcountLeadingZero(x : Nat32) : Nat32

Performs the corresponding bit-level operation.

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

bitcountTrailingZero(x : Nat32) : Nat32

Performs the corresponding bit-level operation.

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

explode(x : Nat32) : (Nat8, Nat8, Nat8, Nat8)

Breaks the fixed-width integer into its byte components.

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

addWrap(x : Nat32, y : Nat32) : Nat32

Returns wrapping addition for the fixed-width type.

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

subWrap(x : Nat32, y : Nat32) : Nat32

Returns wrapping subtraction for the fixed-width type.

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

mulWrap(x : Nat32, y : Nat32) : Nat32

Returns wrapping multiplication for the fixed-width type.

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

powWrap(x : Nat32, y : Nat32) : Nat32

Returns wrapping exponentiation for the fixed-width type.

Contract

ensures toNatSpec(result) == Nat.pow(toNatSpec(x), toNatSpec(y)) % 4_294_967_296;
ensures y == 0 ==> result == 1;
ensures y == 1 ==> result == x;

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

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

Creates an iterator over the requested numeric range or domain.

Contract

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

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

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

Creates an iterator over the requested numeric range or domain.

Contract

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

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

allValues() : Iter.Iter<Nat32>

Creates an iterator over the requested numeric range or domain.

Contract

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

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

Summary

• Runtime module under mo:core/Nat32.
• Exposes 47 public functions.