Skip to main content

Division Safety

Division and modulo operations in contracts require explicit non-zero guards.

The Problem​

Division by zero is undefined. When division appears in method contracts (requires, ensures, assertions lowered as contract obligations, or invariants), the verifier must prove the divisor is never zero. Without proof, the Viper translation rejects the program before SMT verification.

// REJECTED - divisor y could be zero
public func divide(x : Nat, y : Nat) : async Nat
  ensures result == x / y;
{ x / y }

Error message:

division/modulo by possibly zero denominator in contract; add requires d != 0 or d > 0

Basic Non-Zero Guards​

Add a requires clause to guarantee the divisor is non-zero:

division-basic.sr9
// Basic division with non-zero guard
persistent actor {
  public func divide(a : Int, b : Int) : async Int
    entry_requires b != 0;
    requires b != 0;
    ensures result == a / b;
  {
    a / b
  };

  // Alternative: use positive guard
  public func dividePositive(a : Int, b : Int) : async Int
    entry_requires b > 0;
    requires b > 0;
    ensures result == a / b;
  {
    a / b
  };
}

The verifier recognizes these guard patterns:

PatternMeaning
d != 0d is not zero
d > 0d is positive (implies non-zero)
d < 0d is negative (implies non-zero)
d >= 1d is at least 1 (implies non-zero for Nat)

Guard Placement​

When using division in preconditions, place the non-zero guard before the division. Current verification collects logical preconditions before checking contract divisions, so requires order is not semantically significant to the proof. entry_requires clauses are executable runtime checks, though, so guard order matters there: do not evaluate a / b before checking b != 0.

division-guard-order.sr9
// Correct: guard appears before division
persistent actor {
  public func divideWithCheck(a : Nat, b : Nat) : async Nat
    entry_requires b != 0;
    entry_requires a / b > 0;
    requires b != 0;
    requires a / b > 0;
    ensures result == a / b;
  {
    a / b
  };
}

Best practice: place non-zero guards in separate requires clauses before any division. For exported actor methods, mirror caller-provided non-zero assumptions with entry_requires so external calls are checked at the runtime boundary, and put the executable entry_requires guard before any entry_requires expression that divides.

Modulo Operations​

Modulo (%) follows the same rules as division. Both require non-zero guards:

division-modulo.sr9
// Division and modulo together
persistent actor {
  public func divMod(a : Nat, b : Nat) : async (Nat, Nat)
    entry_requires b != 0;
    requires b != 0;
    ensures result.0 == a / b;
    ensures result.1 == a % b;
    ensures a == result.0 * b + result.1;
  {
    (a / b, a % b)
  };

  // Modulo bounds
  public func modBound(a : Nat, b : Nat) : async Nat
    entry_requires b != 0;
    requires b != 0;
    ensures result == a % b;
    ensures result < b;
  {
    a % b
  };
}

Nested and Computed Divisors​

When the divisor is a computed expression, you must guard the entire expression:

division-nested.sr9
// Nested and computed divisors
persistent actor {
  // Computed divisor: guard the expression
  public func divBySum(a : Nat, b : Nat, c : Nat) : async Nat
    entry_requires b + c != 0;
    requires b + c != 0;
    ensures result == a / (b + c);
  {
    a / (b + c)
  };

  // Nested division: guard each level
  public func divNested(a : Nat, b : Nat, c : Nat) : async Nat
    entry_requires b != 0;
    entry_requires c != 0;
    entry_requires b / c != 0;
    requires b != 0;
    requires c != 0;
    requires b / c != 0;
    ensures result == a / (b / c);
  {
    a / (b / c)
  };
}

For nested divisions like a / (b / c), guard each divisor separately, then guard the computed result.

Runtime Protection​

Use runtime:assert for defense-in-depth. This both proves and enforces at runtime:

division-runtime.sr9
// Defense-in-depth with runtime:assert
persistent actor {
  public func safeDivide(a : Int, b : Int) : async Int
    entry_requires b != 0;
    requires b != 0;
    ensures result == a / b;
  {
    runtime:assert b != 0;
    a / b
  };
}

The requires clause is for callers. The runtime:assert provides a safety net if the precondition is violated.

Division in Pure Functions​

Pure functions can perform division but cannot use assert, runtime:assert, or trap. Use requires clauses only:

division-pure.sr9
// Pure function with division
module {
  // Pure helper for division
  public pure func half(n : Nat) : Nat
    requires n >= 2;
    ensures result == n / 2;
  {
    n / 2
  };

  // Use in contracts
  public pure func isEven(n : Nat) : Bool {
    n % 2 == 0
  };
}

Division in Loop Invariants​

Division in loop invariants requires guards that hold throughout the loop:

division-loop.sr9
// Division in loop invariant
persistent actor {
  public func sumDivided(n : Nat, d : Nat) : async Nat
    entry_requires d != 0;
    requires d != 0;
    ensures result == n / d;
  {
    var i : Nat = 0;
    var acc : Nat = 0;

    while (i < n) {
      loop:invariant i <= n;
      loop:invariant d != 0;
      loop:invariant acc == i / d or i < d;
      i += 1;
      if (i % d == 0) {
        acc += 1;
      };
    };

    n / d
  };
}

The invariant d != 0 is trivially preserved since d is not modified.

Literal Divisors​

Non-zero literal divisors are always allowed without guards:

public func percent(x : Nat) : async Nat
  ensures result == x / 100;
{ x / 100 }

The verifier recognizes that 100 is non-zero.

Common Mistakes​

Missing Guard​

// REJECTED
public func bad(a : Nat, b : Nat) : async Nat
  ensures result == a / b;
{ a / b }

Fix: add entry_requires b != 0; requires b != 0; for exported actor methods, or just requires b != 0; for private/module helpers.

Guard Hidden After Division​

// Logical requires are accepted today, but this is unsafe entry_requires order.
public func bad(a : Nat, b : Nat) : async Nat
  entry_requires a / b > 0;
  entry_requires b != 0;
  requires a / b > 0;
  requires b != 0;
{ a / b }

Fix: move entry_requires b != 0 and requires b != 0 before the division.

Unguarded Computed Divisor​

// REJECTED - (b - c) could be zero
public func bad(a : Nat, b : Nat, c : Nat) : async Nat
  entry_requires b >= c;
  requires b >= c;
  ensures result == a / (b - c);
{ a / (b - c) }

Fix: add entry_requires (b - c) != 0; requires (b - c) != 0; or use the stronger b > c, which implies b - c > 0 for Nat.

Summary​

  • Division and modulo in contracts require explicit non-zero guards
  • Use requires d != 0 or requires d > 0 for any divisor used in contracts
  • Put executable entry_requires guards before any entry guard that divides
  • Computed divisors need explicit guards on the full expression
  • Literal non-zero divisors are automatically allowed
  • Pure functions must use requires clauses, not assertions
  • Use runtime:assert for defense-in-depth protection