Integers (Int)

Unbounded signed integers - the type for arithmetic that may involve negative values.

Overview

Int represents mathematical integers: ..., -2, -1, 0, 1, 2, ... with no upper or lower limit. Unlike Nat, Int values can be negative, and the verifier makes no automatic assumptions about their bounds.

int-basic.sr9

// Basic Int declarations and operations
persistent actor {
  var balance : Int = 0;

  public func adjust(delta : Int) : async Int
    modifies balance
    ensures result == old(balance) + delta;
  {
    balance += delta;
    balance
  };

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

  public func subtract(a : Int, b : Int) : async Int
    ensures result == a - b;
  {
    a - b
  };
}

Negative Values

Int allows negative values without any preconditions. This is the key difference from Nat, which requires subtraction guards to prevent underflow.

int-negative.sr9

// Int supports negative values - no lower bound
persistent actor {
  var temperature : Int = 20;

  // Can go negative without preconditions
  public func cool(degrees : Int) : async Int
    modifies temperature
    entry_requires degrees > 0;
    requires degrees > 0;
    ensures temperature == old(temperature) - degrees;
    ensures result == temperature;
  {
    temperature -= degrees;
    temperature
  };

  // Absolute value shows negative handling
  public func abs(x : Int) : async Int
    ensures result >= 0;
    ensures x >= 0 ==> result == x;
    ensures x < 0 ==> result == -x;
  {
    if (x < 0) { -x } else { x }
  };

  // Sign function
  public func sign(x : Int) : async Int
    ensures x > 0 ==> result == 1;
    ensures x < 0 ==> result == -1;
    ensures x == 0 ==> result == 0;
  {
    if (x > 0) { 1 } else if (x < 0) { -1 } else { 0 }
  };
}

Because Int has no lower bound, subtraction never fails - the result can go arbitrarily negative. This makes Int easier to work with when dealing with deltas, differences, or signed quantities.

Fixed-Width Variants

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

Type	Minimum	Maximum
Int8	-128	127
Int16	-32,768	32,767
Int32	-2,147,483,648	2,147,483,647
Int64	-9,223,372,036,854,775,808	9,223,372,036,854,775,807
Int	(unbounded)	(unbounded)

For fixed-width types, you must guard both overflow (positive direction) and underflow (negative direction).

int-fixed-width.sr9

// Fixed-width signed integers have both upper and lower bounds
persistent actor {
  // Int8 ranges from -128 to 127
  public func addInt8(a : Int8, b : Int8) : async Int8
    entry_requires a + b >= -128;
    entry_requires a + b <= 127;
    requires a + b >= -128;
    requires a + b <= 127;
    ensures result == a + b;
  {
    a + b
  };

  // Safe increment for Int32
  public func incInt32(x : Int32) : async Int32
    entry_requires x < 2_147_483_647;  // Guard against overflow
    requires x < 2_147_483_647;
    ensures result == x + (1 : Int32);
  {
    x + (1 : Int32)
  };

  // Safe decrement for Int32
  public func decInt32(x : Int32) : async Int32
    entry_requires x > -2_147_483_648;  // Guard against underflow
    requires x > -2_147_483_648;
    ensures result == x - (1 : Int32);
  {
    x - (1 : Int32)
  };
}

The verifier tracks both bounds automatically for fixed-width types, but you must provide preconditions that ensure operations stay within range.

Relationship to Nat

Nat is a subtype of Int. This creates an asymmetric relationship:

• Nat to Int: Works automatically. Every Nat value is a valid Int.
• Int to Nat: Requires an explicit conversion and proof. You must prove x >= 0 before calling a conversion such as Int.toNat(x).

// Nat automatically works where Int is expected
import Int "mo:core/Int";

public func processInt(x : Int) : async Int { x * 2 };

public func example(n : Nat) : async Int {
  try { await processInt(n) } catch (_) { 0 }  // OK: Nat → Int is automatic
};

// Int requires proof to become Nat
public func toNat(x : Int) : async Nat
  entry_requires x >= 0;  // Runtime guard for exported callers
  requires x >= 0;        // Must prove non-negativity
{
  Int.toNat(x)  // Safe: verifier knows x >= 0
};

When combining Nat and Int in expressions, the result type is Int (the common supertype).

Division Safety

Division and modulo operations require non-zero divisor guards, just like with Nat. Use entry_requires for exported runtime guards and requires for verifier facts.

int-division.sr9

// Division with Int requires non-zero guards
persistent actor {
  public func divide(a : Int, b : Int) : async Int
    entry_requires b != 0;
    requires b != 0;
    ensures result == a / b;
  {
    a / b
  };

  public func modulo(a : Int, b : Int) : async Int
    entry_requires b != 0;
    requires b != 0;
    ensures result == a % b;
  {
    a % b
  };

  // Both positive and negative divisors work
  public func divideByNegative(a : Int) : async Int
    ensures result == a / -2;
  {
    a / -2
  };
}

Valid guards for Int division:

Pattern	Meaning
d != 0	d is not zero
d > 0	d is positive (implies non-zero)
d < 0	d is negative (implies non-zero)

The guard must appear before any division in your contract. This applies to both the dividend and divisor positions.

Common Patterns

Absolute Value

public func abs(x : Int) : async Int
  ensures result >= 0
  ensures result == x or result == -x
{
  if (x < 0) { -x } else { x }
}

Clamp to Range

int-clamp.sr9

// Clamp value to range - common Int pattern
persistent actor {
  public func clamp(x : Int, lo : Int, hi : Int) : async Int
    entry_requires lo <= hi;
    requires lo <= hi;
    ensures result >= lo;
    ensures result <= hi;
    ensures x < lo ==> result == lo;
    ensures x > hi ==> result == hi;
    ensures lo <= x and x <= hi ==> result == x;
  {
    if (x < lo) {
      lo
    } else if (x > hi) {
      hi
    } else {
      x
    }
  };

  public func minMax(a : Int, b : Int) : async { min : Int; max : Int }
    ensures result.min <= result.max;
    ensures result.min == a or result.min == b;
    ensures result.max == a or result.max == b;
  {
    if (a <= b) {
      { min = a; max = b }
    } else {
      { min = b; max = a }
    }
  };
}

Difference with Sign

public func difference(a : Int, b : Int) : async { diff : Int; positive : Bool }
  ensures result.diff == a - b or result.diff == b - a
  ensures result.positive ==> result.diff >= 0
{
  if (a >= b) {
    { diff = a - b; positive = true }
  } else {
    { diff = b - a; positive = true }
  }
}

Bounded Increment

var counter : Int = 0;

public func boundedIncrement(max : Int) : async Int
  modifies counter
  entry_requires max > 0;
  requires max > 0;
  ensures counter <= max;
  ensures counter >= old(counter) or counter == max;
{
  if (counter < max) {
    counter += 1;
  };
  counter
}

When to Use Int vs Nat

Use Nat when...	Use Int when...
Values are never negative	Values can be negative
Counting items or sizes	Differences or deltas
Array indices	Temperature, coordinates
Token amounts	Balance adjustments
IDs and keys	Comparison results

Nat provides automatic non-negativity guarantees, so prefer it when values are inherently non-negative. Use Int when you need the full range of signed arithmetic.

Verification Notes

• No automatic bounds: Unlike Nat, the verifier assumes nothing about Int values. You must state any bounds explicitly in preconditions or invariants.
• Subtraction is safe: Int subtraction never underflows, so no guards are needed.
• Division guards required: Both Nat and Int require explicit non-zero guards for division and modulo.
• Fixed-width types need both bounds: For Int8, Int16, Int32, Int64, guard against both overflow and underflow. See Fixed-Width Numbers.

Summary

• Int represents unbounded signed integers (..., -2, -1, 0, 1, 2, ...)
• No automatic bounds - the verifier makes no assumptions about Int values
• Subtraction is always safe (no underflow) unlike Nat
• Nat is a subtype of Int - Nat values work where Int is expected
• Fixed-width variants (Int8, Int16, Int32, Int64) have both upper and lower bounds
• Division requires explicit non-zero guards in contracts