Skip to main content

Overflow Checking Mode

Verified Sector9 code uses checked fixed-width integer arithmetic. Potential overflow and underflow are proof obligations.

Current Verified Mode​

ModeFlagBehaviorUse Case
Checked--int-mode checkedOverflow fails verificationStrict safety proofs (default)
Bitvec--int-mode bitvecRejected by --verifyNot a verified lane today
Unchecked--int-mode uncheckedRejected by --verifyNot a verified lane today

The default is checked, and it is the only integer mode accepted by --verify.

Checked Mode (Default)​

In checked mode, fixed-width arithmetic operations generate proof obligations that the result stays within the type's bounds. If overflow could occur, verification fails.

overflow-checked-safe.sr9
// In checked mode, fixed-width arithmetic requires safe bounds.
// This verifies because x < 255 prevents overflow.
persistent actor {
  public func inc(x : Nat8) : async Nat8
    entry_requires x < 255;
    requires x < 255;
    ensures result == x + (1 : Nat8);
  {
    x + (1 : Nat8)
  }
}

The requires x < 255 precondition ensures that x + 1 cannot exceed the Nat8 maximum of 255.

Without this guard, verification fails:

overflow-checked-fails_unsat.sr9
// In checked mode, wraparound is forbidden.
// This fails verification: 255 + 1 cannot equal 0.
persistent actor {
  public func wrap() : async Nat8 {
    let x : Nat8 = 255;
    let y : Nat8 = x + (1 : Nat8);
    assert y == 0;  // Fails: wraparound not allowed
    y
  }
}

This fails because checked mode forbids wraparound. The assertion y == 0 cannot be proven since 255 + 1 does not wrap to 0.

Signed Types in Checked Mode​

Signed types require guards for both underflow and overflow:

overflow-signed-checked.sr9
// Signed types also require overflow protection in checked mode.
persistent actor {
  public func add_safe(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
  };
}

For Int8, valid results must be in the range -128 to 127.

Rejected Modes​

--verify --int-mode bitvec and --verify --int-mode unchecked fail before Viper runs. If you need wrapping behavior, use the explicit wrapping helpers from the core fixed-width modules or expose a small trusted surface with contracts that say exactly which wraparound fact callers may rely on.

Automatic Type Bounds​

In checked mode, Sector9 automatically tracks bounds for fixed-width types. 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;
  }
}

Fixed-Width Type Bounds​

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

Unbounded Types​

Unbounded Nat and Int have no upper bounds:

overflow-unbounded.sr9
// Unbounded Nat and Int have no upper bound, only Nat >= 0.
persistent actor {
  public func big_numbers(n : Nat, _i : Int) : async () {
    // Nat is always non-negative
    assert n >= 0;

    // No upper bound on Nat - this is valid
    let big : Nat = 99999999999999999999;
    assert big > 0;

    // Int has no bounds at all
    let neg : Int = -99999999999999999999;
    assert neg < 0;
  };
}
  • Nat: Only has a lower bound of 0
  • Int: Has no bounds at all

These types do not overflow upward in Sector9 verification. They model mathematical integers for addition and multiplication. Nat subtraction is still partial: the verifier must prove the result is non-negative, so x - y needs a fact such as x >= y.

Spec vs Runtime Behavior​

In checked mode, fixed-width operators are only connected to their mathematical result when the verifier can prove the result is in range. If the proof is missing, callers cannot use the expected arithmetic fact, and verification fails on the surrounding postcondition, assertion, or bounds obligation.

Practical Guidance​

Use checked arithmetic in verified code. When a proof is difficult, prefer:

  • a wider intermediate type
  • a tighter precondition
  • a small helper lemma for arithmetic facts
  • unbounded Nat or Int when fixed-width representation is not essential
  • an explicit x >= y guard before Nat subtraction

Summary​

  • Verification accepts checked integer mode only
  • Checked mode requires proving that fixed-width arithmetic stays in bounds
  • bitvec and unchecked are rejected by --verify
  • Fixed-width types have automatic bounds that the verifier tracks
  • Unbounded Nat and Int do not have upper overflow; Nat subtraction still needs a non-negative result proof
  • Omit --int-mode or pass --int-mode checked for verification