Skip to main content

Numeric Modules

Numeric types expose verification-friendly operations with explicit contracts and range helpers.

Nat (mo:core/Nat)​

Natural numbers (unbounded, non-negative).

See Nat for the full API, including spec helpers.

Int (mo:core/Int)​

Signed integers (unbounded).

See Int for the full API, including spec helpers.

Example: Nat and Int​

nat-int.sr9
import Nat "mo:core/Nat";
import Int "mo:core/Int";

module {
  public func absSum(x : Int.Int, y : Int.Int) : Nat.Nat
    requires true;
    ensures true;
  {
    Nat.add(Int.abs(x), Int.abs(y))
  };
}

Fixed-Width Ints (mo:core/Int8, Int16, Int32)​

Fixed-width signed integers with wrap and bit-level operations.

See Int8, Int16, and Int32 for full APIs and spec helpers.

Fixed-Width Nats (mo:core/Nat8, Nat16, Nat32)​

Fixed-width unsigned integers with wrap and bit-level operations.

See Nat8, Nat16, and Nat32 for full APIs and spec helpers.

Division and Power Helpers​

Nat.div, Nat.rem, Int.div, and Int.rem are trusted wrappers with contracts. Callers still need explicit non-zero guards before using division or modulo in code or specifications. See entry requirements for the public-method guard pattern.

Float (mo:core/Float)​

Floating-point operations are provided as trusted wrappers. Use them for runtime math and formatting, but avoid relying on them for deep SMT arithmetic proofs.

See Float for the full API.

Summary​

  • Nat and Int provide unbounded arithmetic with explicit contracts.
  • Fixed-width integer modules include bitwise operations, wrapping arithmetic, and range helpers for the currently shipped 8/16/32-bit modules.
  • Float is available via trusted wrappers for runtime math and formatting.