Natural Numbers (Nat)

Unbounded non-negative integers - the default numeric type for safe arithmetic in Sector9.

Overview

Nat represents mathematical natural numbers: 0, 1, 2, 3, and so on with no upper limit. The verifier automatically knows that every Nat value satisfies n >= 0, which enables reasoning about non-negativity without explicit assertions.

nat-basic.sr9

// Basic Nat declarations and operations
persistent actor {
  var counter : Nat = 0;

  public func increment() : async Nat
    modifies counter
    ensures result == old(counter) + 1;
  {
    counter += 1;
    counter
  };

  public func add(a : Nat, b : Nat) : async Nat
    ensures result == a + b;
  {
    a + b
  };
}

Automatic Bounds

The verifier automatically tracks that Nat values are non-negative. You can rely on this in your contracts without stating it explicitly.

nat-bounds.sr9

// Nat bounds are automatically verified
persistent actor {
  var value : Nat = 100;

  // The verifier automatically knows Nat values are >= 0
  public func checkNonNegative() : async ()
    modifies value
  {
    let v = value;
    assert v >= 0;  // Always provable for Nat
  };

  // Parameters inherit Nat bounds
  public func processNat(x : Nat) : async Nat
    ensures result >= 0;  // Automatic for Nat return type
  {
    x + 1
  };
}

For plain Nat, only the lower bound (>= 0) is enforced. There is no upper bound - Nat can represent arbitrarily large values.

Subtraction and Underflow

Subtraction on Nat requires care. The result must remain non-negative, so you need preconditions that prevent underflow.

Correct

nat-subtraction.sr9

// Safe Nat subtraction requires preconditions
persistent actor {
  var balance : Nat = 100;

  // Subtraction requires guard to prevent underflow
  public func withdraw(amount : Nat) : async Nat
    modifies balance
    entry_requires amount <= balance;
    requires amount <= balance;  // Prevents underflow
    ensures result == old(balance) - amount;
  {
    balance -= amount;
    balance
  };

  // Safe decrement pattern
  public func decrement() : async Nat
    modifies balance
    entry_requires balance > 0;
    requires balance > 0;
    ensures balance == old(balance) - 1;
  {
    balance -= 1;
    balance
  };
}

Wrong

nat-subtraction-missing_unsat.sr9

// UNSAT: Missing underflow guard
persistent actor {
  var balance : Nat = 100;

  // This fails verification - amount could exceed balance
  public func withdraw(amount : Nat) : async Nat
    modifies balance
    ensures result == old(balance) - amount;
  {
    balance -= amount;  // Verification failure: potential underflow
    balance
  };
}

The verifier rejects the "wrong" version because amount could exceed balance, causing the subtraction to produce a negative result - impossible for Nat. See preconditions for how to make this obligation explicit.

Fixed-Width Variants

Sector9 inherits fixed-width unsigned integer types with both lower and upper bounds:

Type	Minimum	Maximum
Nat8	0	255
Nat16	0	65,535
Nat32	0	4,294,967,295
Nat64	0	18,446,744,073,709,551,615
Nat	0	(unbounded)

The verifier automatically tracks both bounds for fixed-width types.

nat-fixed-width.sr9

// Fixed-width Nat types have both lower and upper bounds
persistent actor {
  var small : Nat8 = 0;
  var medium : Nat16 = 0;
  var large : Nat32 = 0;
  var huge : Nat64 = 0;

  // Nat8: 0 to 255
  public func incrementSmall() : async Nat8
    modifies small
    entry_requires small < 255;
    requires small < 255;  // Prevents overflow
    ensures result == old(small) + (1 : Nat8);
  {
    small += 1;
    small
  };

  // Verifier automatically knows bounds
  public func checkBounds() : async ()
    modifies small, medium, large, huge
  {
    assert small >= 0;
    assert small <= 255;

    assert medium >= 0;
    assert medium <= 65535;

    assert large >= 0;
    assert large <= 4294967295;

    assert huge >= 0;
    assert huge <= 18446744073709551615;
  };
}

Fixed-width types require overflow guards when incrementing near their maximum value. See Fixed-Width Numbers for the detailed checked-mode rules.

Relationship to Int

Nat is a subtype of Int. This means:

• Nat values can be used where Int is expected - implicit upcasting works automatically
• Int values require an explicit conversion plus proof of non-negativity - prove x >= 0, then use a conversion such as Int.toNat(x)

nat-to-int.sr9

// Nat is a subtype of Int - can be used where Int is expected
import Int "mo:core/Int";

persistent actor {
  // Nat can be passed to Int parameters
  public func processInt(x : Int) : async Int
    ensures result == x * 2;
  {
    x * 2
  };

  public func doubleNat(n : Nat) : async Int {
    // Nat value used where Int is expected - works automatically
    try { await processInt(n) } catch (_) { 0 }
  };

  // Int cannot be used where Nat is expected without verification
  public func absolute(x : Int) : async Nat
    entry_requires x >= 0;  // Runtime guard for exported callers
    requires x >= 0;        // Must prove non-negativity
    ensures result == x;
  {
    // Safe: we proved x >= 0
    let n : Nat = Int.toNat(x);
    n
  };
}

When the verifier combines Nat and Int in an expression, the result type is Int (the common supertype).

Division Safety

Division and modulo operations on Nat require non-zero divisor guards:

public func divide(x : Nat, y : Nat) : async Nat
  entry_requires y != 0;  // or: entry_requires y > 0
  requires y != 0;        // or: requires y > 0
  ensures result == x / y;
{
  x / y
}

The guard must appear before any division in your contract. This is rejected:

public func bad(a : Nat, b : Nat) : async Nat
  requires a / b > 0  // Division before guard
  requires b != 0     // Too late
{ a / b }

Common Patterns

Decrement with Guard

public func decrement(n : Nat) : async Nat
  entry_requires n > 0;
  requires n > 0;
  ensures result == n - 1;
{
  n - 1
}

Bounded Counter

var counter : Nat = 0;

public func increment() : async Nat
  entry_requires counter < 1000;
  requires counter < 1000;  // Establish upper bound for reasoning
  modifies counter
  ensures counter == old(counter) + 1;
{
  counter += 1;
  counter
}

Transfer with Balance Check

public func transfer(from : Nat, to : Nat, amount : Nat) : async (Nat, Nat)
  entry_requires amount <= from;
  requires amount <= from;
  ensures result.0 == from - amount;
  ensures result.1 == to + amount;
{
  (from - amount, to + amount)
}

Summary

• Nat represents unbounded non-negative integers (0, 1, 2, ...)
• The verifier automatically knows Nat values satisfy >= 0
• Subtraction requires preconditions to prevent underflow
• Fixed-width variants (Nat8, Nat16, Nat32, Nat64) have both lower and upper bounds
• Nat is a subtype of Int - Nat values can be used where Int is expected
• Division requires explicit non-zero guards in contracts