Skip to main content

Bounds Proofs

Proving that fixed-width integer values stay within their valid ranges during arithmetic operations.

Automatic Type Bounds​

In checked mode (the default), Sector9 automatically tracks bounds for all fixed-width integer types. When you read a Nat8 value, the verifier knows it satisfies 0 <= x <= 255. You can assert these bounds directly:

overflow-bounds-automatic.sr9
// Fixed-width types have automatic bounds that can be asserted.
persistent actor {
  public func check_bounds(n8 : Nat8, n16 : Nat16, i8 : Int8) : async () {
    // Nat8: 0 to 255
    assert n8 >= 0;
    assert n8 <= 255;

    // Nat16: 0 to 65535
    assert n16 >= 0;
    assert n16 <= 65535;

    // Int8: -128 to 127
    assert i8 >= -128;
    assert i8 <= 127;
  }
}

These assertions verify because the verifier injects bounds constraints based on the type. This happens automatically for:

  • Parameters: Function parameters have their type bounds assumed
  • Fields: Actor and record fields have bounds when read
  • Return values: Results have bounds ensured automatically

Fixed-Width Type Bounds Reference​

TypeMinimumMaximum
Nat80255
Nat16065,535
Nat3204,294,967,295
Nat64018,446,744,073,709,551,615
Int8-128127
Int16-32,76832,767
Int32-2,147,483,6482,147,483,647
Int64-9,223,372,036,854,775,8089,223,372,036,854,775,807
Nat0(unbounded)
Int(unbounded)(unbounded)

Unbounded Nat has only a lower bound. Unbounded Int has no bounds at all. Nat still cannot go below zero, so subtraction on Nat creates an underflow proof obligation even though Nat has no upper overflow.

Proving Arithmetic Stays in Bounds​

In checked mode, arithmetic operations generate proof obligations that results stay within bounds. If the verifier cannot prove an operation is safe, verification fails.

Precondition Guards​

The most common pattern is a precondition that rules out overflow:

bounds-increment-guard.sr9
// Increment requires a bounds guard to prevent overflow.
persistent actor {
  var counter : Nat8 = 0;

  public func increment() : async Nat8
    modifies counter
    entry_requires counter < 255;
    requires counter < 255;
    ensures result == old(counter) + (1 : Nat8);
  {
    counter := counter + (1 : Nat8);
    counter
  }
}

The requires counter < 255 precondition ensures counter + 1 stays within Nat8 bounds. Public actor methods should pair that logical fact with entry_requires when external callers control the input. Without this guard, verification fails.

What Happens Without a Guard​

bounds-missing-guard_unsat.sr9
// Missing bounds guard causes verification failure.
persistent actor {
  var counter : Nat8 = 0;

  // FAILS: No guard prevents overflow when counter == 255
  public func increment() : async Nat8
    modifies counter
    ensures result == old(counter) + (1 : Nat8);
  {
    counter := counter + (1 : Nat8);  // May overflow
    counter
  }
}

This fails because when counter == 255, the addition 255 + 1 would exceed the Nat8 maximum. The verifier detects this potential overflow.

Bounds Through Control Flow​

Conditional logic can establish bounds without requiring preconditions:

bounds-conditional.sr9
// Conditional logic can establish bounds without preconditions.
persistent actor {
  public func safe_add(x : Nat8, y : Nat8) : async Nat8
    ensures result >= x;
  {
    // Check if addition would overflow
    if (x > 255 - y) {
      255 : Nat8  // Cap at maximum
    } else {
      x + y
    }
  }
}

The if (x > 255 - y) check ensures the else-branch only executes when x + y is safe. The verifier tracks this path constraint.

Postcondition Bounds​

You can specify bounds on return values using ensures:

bounds-postcondition.sr9
// Postconditions can state bounds on return values.
persistent actor {
  public func clamp(x : Nat8, low : Nat8, high : Nat8) : async Nat8
    entry_requires low <= high;
    requires low <= high;
    ensures result >= low;
    ensures result <= high;
  {
    if (x < low) {
      low
    } else if (x > high) {
      high
    } else {
      x
    }
  };
}

The postconditions ensures result >= low and ensures result <= high document and verify the output range.

Bounds in Loop Invariants​

Loop invariants often need to maintain bounds through iterations:

bounds-loop-invariant.sr9
// Loop invariants maintain bounds through iterations.
persistent actor {
  public func count_up(limit : Nat8) : async Nat8
    entry_requires limit < 255;
    requires limit < 255;
    ensures result == limit + (1 : Nat8);
  {
    var i : Nat8 = 0;
    while (i <= limit) {
      loop:invariant i <= limit + (1 : Nat8);
      i := i + (1 : Nat8);
    };
    i
  };
}

The loop:invariant i <= limit + (1 : Nat8) maintains that i stays within valid Nat8 range throughout the loop. The requires limit < 255 ensures the invariant's upper bound (limit + 1) is itself a valid Nat8.

Common Bounds Proof Patterns​

Increment with Saturation​

public func saturating_inc(x : Nat8) : async Nat8 {
  if (x < 255) { x + (1 : Nat8) } else { 255 : Nat8 }
}

Safe Subtraction for Unsigned​

public func safe_sub(x : Nat8, y : Nat8) : async Nat8
  entry_requires y <= x;
  requires y <= x;
{
  x - y
}

For unbounded Nat, the same shape is needed for underflow:

public func nat_sub(x : Nat, y : Nat) : async Nat
  entry_requires y <= x;
  requires y <= x;
{
  x - y
}

Range Validation​

public func validate_range(x : Nat) : async Nat8
  entry_requires x <= 255;
  requires x <= 255;
{
  let bounded : Nat8 = x;
  bounded
}

Two-Operand Bounds​

public func safe_multiply(x : Nat8, y : Nat8) : async Nat16 {
  // Widen first so the multiplication is checked against Nat16 bounds.
  let result : Nat16 = Nat16.fromNat8(x) * Nat16.fromNat8(y);
  result
}

Verification Integer Mode​

Verified code uses checked integer mode:

ModeBounds Behavior
checked (default)Overflow generates proof obligations that must be satisfied
bitvecRejected by --verify
uncheckedRejected by --verify

In checked mode, you must prove that 255 + 1 for Nat8 cannot occur unless the expression is guarded or widened first. See Overflow Checking Mode for details.

Common Mistakes​

Guarding the Wrong Direction for Signed Types​

// WRONG for decrement: this guards the upper bound, not underflow
public func dec(x : Int8) : async Int8
  entry_requires x < 127;
  requires x < 127;
{
  x - (1 : Int8)
}

// CORRECT: Guards lower bound for subtraction
public func dec(x : Int8) : async Int8
  entry_requires x > -128;
  requires x > -128;
{
  x - (1 : Int8)
}

For signed types, guard the direction the operation can fail in: addition can overflow positive, subtraction can underflow negative, and mixed expressions may need both.

Assuming Bounds After Arithmetic​

// WRONG: Bounds don't survive arithmetic without proof
public func double(x : Nat8) : async Nat8 {
  let y = x + x;  // May overflow
  assert y <= 255;  // Fails: y could be 510
  y
}

// CORRECT: Guard before arithmetic
public func double(x : Nat8) : async Nat8
  entry_requires x <= 127;
  requires x <= 127;  // Ensures x + x <= 254
{
  x + x
}

Mixing Bounded and Unbounded Types​

// WRONG: Nat has no upper bound
public func to_nat8(x : Nat) : async Nat8 {
  let bounded : Nat8 = x;  // May fail: x could exceed 255
  bounded
}

// CORRECT: Require bounds
public func to_nat8(x : Nat) : async Nat8
  entry_requires x <= 255;
  requires x <= 255;
{
  let bounded : Nat8 = x;
  bounded
}

Summary​

  • Fixed-width types have automatic bounds that the verifier tracks
  • In checked mode, arithmetic generates proof obligations that results stay in bounds
  • Use requires preconditions to rule out overflow at the call site
  • Conditional logic can establish bounds through control flow
  • Loop invariants must maintain bounds through iterations
  • Signed types need guards for both overflow and underflow
  • Unbounded Nat has only a lower bound and still needs underflow guards for subtraction; Int has no bounds
  • --verify accepts checked mode only; bitvec and unchecked are rejected