Fixed-Width Numbers

Nat8-Nat64 and Int8-Int64 for when you need specific bit widths and bounded arithmetic.

Overview

Fixed-width numeric types provide precise control over integer representation. Unlike unbounded Nat and Int, these types have both lower and upper bounds that the verifier automatically tracks. This enables reasoning about overflow, bit operations, and memory layout.

fixed-basic.sr9

// Fixed-width types for precise control over bit widths
persistent actor {
  var byte : Nat8 = 42;
  var word : Nat16 = 1000;
  var dword : Nat32 = 100000;
  var qword : Nat64 = 10000000000;

  var signed8 : Int8 = -50;
  var signed32 : Int32 = -1000000;

  // Explicit type annotations for literals
  public func literals() : async () {
    let a : Nat8 = 255;
    let b : Nat16 = 65535;
    let c : Int8 = -128;
    let d : Int32 = 2_147_483_647;  // Underscores for readability
  };
}

Type Ranges

Unsigned Types (Nat8-Nat64)

Type	Bits	Minimum	Maximum
Nat8	8	0	255
Nat16	16	0	65,535
Nat32	32	0	4,294,967,295
Nat64	64	0	18,446,744,073,709,551,615

Signed Types (Int8-Int64)

Type	Bits	Minimum	Maximum
Int8	8	-128	127
Int16	16	-32,768	32,767
Int32	32	-2,147,483,648	2,147,483,647
Int64	64	-9,223,372,036,854,775,808	9,223,372,036,854,775,807

Automatic Bounds

The verifier automatically injects bounds for all fixed-width types. When you read a Nat8 parameter or field, the verifier knows it satisfies 0 <= x <= 255. You can use this knowledge in assertions and contracts without stating it explicitly.

fixed-bounds.sr9

// The verifier automatically tracks fixed-width bounds
persistent actor {
  public func checkNat8Bounds(x : Nat8) : async () {
    // These assertions always pass - automatic bounds
    assert x >= 0;
    assert x <= 255;
  };

  public func checkNat32Bounds(x : Nat32) : async () {
    assert x >= 0;
    assert x <= 4294967295;
  };

  public func checkInt8Bounds(x : Int8) : async () {
    // Signed types have both negative and positive bounds
    assert x >= -128;
    assert x <= 127;
  };

  public func checkInt64Bounds(x : Int64) : async () {
    assert x >= -9223372036854775808;
    assert x <= 9223372036854775807;
  };
}

This automatic tracking extends to:

• Function parameters - bounds assumed on entry
• Actor fields - bounds hold after reading
• Return values - bounds ensured automatically
• Record fields - bounds apply to nested fixed-width values

Overflow and Underflow

Unlike unbounded types, fixed-width arithmetic can overflow (exceed the maximum) or underflow (go below the minimum). By default, Sector9 uses checked mode: arithmetic that might overflow fails verification.

With Guard

fixed-overflow-guard.sr9

// Guards prevent overflow in fixed-width arithmetic
persistent actor {
  // Safe increment: guard prevents overflow
  public func safeInc(x : Nat8) : async Nat8
    entry_requires x < 255;
    requires x < 255;
    ensures result == x + (1 : Nat8);
  {
    x + (1 : Nat8)
  };

  // Safe addition: combined value stays in bounds
  public func safeAdd(a : Nat16, b : Nat16) : async Nat16
    entry_requires a + b <= 65535;
    requires a + b <= 65535;
    ensures result == a + b;
  {
    a + b
  };

  // Safe signed increment: guard both bounds
  public func safeIncSigned(x : Int8) : async Int8
    entry_requires x < 127;
    requires x < 127;
    ensures result == x + (1 : Int8);
  {
    x + (1 : Int8)
  };

  // Safe signed decrement: guard lower bound
  public func safeDecSigned(x : Int8) : async Int8
    entry_requires x > -128;
    requires x > -128;
    ensures result == x - (1 : Int8);
  {
    x - (1 : Int8)
  };
}

Missing Guard

fixed-overflow-missing_unsat.sr9

// Missing overflow guards cause verification failure
persistent actor {
  // FAILS: No guard prevents x from being 255
  public func unsafeInc(x : Nat8) : async Nat8
    ensures result == x + (1 : Nat8);
  {
    x + (1 : Nat8)  // Overflow possible when x == 255
  };
}

The verifier rejects the "missing guard" version because x could be 255, making x + 1 overflow the Nat8 range.

Guard Patterns

For unsigned types, guard against the upper bound:

requires x < 255           // Nat8 increment
requires a + b <= 65535    // Nat16 addition

For signed types, guard against both bounds:

requires x < 127           // Int8 increment (overflow)
requires x > -128          // Int8 decrement (underflow)
requires a + b >= -32768   // Int16 addition lower bound
requires a + b <= 32767    // Int16 addition upper bound

Saturating Arithmetic

When you want values to clamp at boundaries instead of requiring guards, implement saturating operations:

fixed-saturation.sr9

// Saturating arithmetic: clamp at boundaries instead of overflow
persistent actor {
  // Increment with saturation at max value
  public func saturatingInc(x : Nat8) : async Nat8
    ensures result >= x;
    ensures result <= 255;
  {
    if (x < 255) { x + (1 : Nat8) } else { 255 : Nat8 }
  };

  // Decrement with saturation at min value
  public func saturatingDecSigned(x : Int8) : async Int8
    ensures result <= x;
    ensures result >= -128;
  {
    if (x > -128) { x - (1 : Int8) } else { -128 : Int8 }
  };

  // Safe subtraction for unsigned: clamp at zero
  public func saturatingSub(a : Nat8, b : Nat8) : async Nat8
    ensures result <= a;
  {
    if (b <= a) { a - b } else { 0 : Nat8 }
  };
}

This pattern is common for counters, accumulators, and any value that should stay within bounds without failing.

Type Conversions

Widening (Safe)

Converting from a smaller type to a larger type is always safe. Nat8 fits in Nat32, and Int16 fits in Int64.

Narrowing (Requires Proof)

Converting from a larger type to a smaller type requires proving the value fits and using the target module conversion, such as Nat8.fromNat(x). The verifier needs to know the source value is within the target type's range.

fixed-conversion.sr9

// Type conversions between fixed-width types
import Nat8 "mo:core/Nat8";
import Nat32 "mo:core/Nat32";
import Int32 "mo:core/Int32";

persistent actor {
  // Widening to unbounded Nat is always safe.
  public func widenToNat(x : Nat8) : async Nat {
    Nat8.toNatSpec(x)
  };

  // Narrowing: requires a bounds proof.
  public func narrowFromNat(x : Nat) : async Nat8
    entry_requires x <= 255;
    requires x <= 255;
  {
    Nat8.fromNat(x)
  };

  // Nat to Nat32 also needs the target bound.
  public func natToNat32(x : Nat) : async Nat32
    entry_requires x <= 4_294_967_295;
    requires x <= 4_294_967_295;
  {
    Nat32.fromNat(x)
  };

  // Signed to unsigned requires a non-negative value.
  public func signedToUnsigned(x : Int32) : async Nat32
    entry_requires x >= 0;
    requires x >= 0;
  {
    Int32.toNat32(x)
  };
}

Signed/Unsigned Conversions

Converting from signed to unsigned requires an explicit conversion and a non-negative proof. Converting from unsigned to signed requires proving the value fits in the signed target range; for example, not every Nat8 fits in Int8 because Nat8 can reach 255 while Int8 stops at 127. See Int.toNat for the unbounded signed-to-natural case.

Explicit Type Annotations

Numeric literals need type annotations when the target type is not inferrable. Use parentheses and a type suffix:

let a : Nat8 = 42;              // Type from binding
let b = (42 : Nat8);            // Explicit annotation on literal
let c = x + (1 : Nat8);         // Annotation in expression
let d : Nat32 = 1_000_000;      // Underscores for readability

Verification Mode

Verified builds require checked integer mode. In --verify and ordinary Viper verification workflows, --int-mode bitvec and --int-mode unchecked are rejected. Treat fixed-width arithmetic as a proof obligation: if an operation could overflow or underflow, add a guard or use a wider intermediate type.

sector9 --verify file.sr9                 # checked mode
sector9 --verify --int-mode checked file.sr9

If you intentionally need wrapping arithmetic, isolate that behavior behind a small trusted or runtime-only surface and document the trust boundary. Do not expect the verified lane to prove bitvector wraparound properties today.

Bitwise Operations

Fixed-width types support bitwise operations:

let a : Nat8 = 0b1010_1010;
let b : Nat8 = 0b0000_1111;

let and_result = a & b;    // 0b0000_1010
let or_result = a | b;     // 0b1010_1111
let xor_result = a ^ b;    // 0b1010_0101
let not_result = ^a;       // 0b0101_0101 (bitwise NOT)

The bitwise NOT operation (^) for unsigned types computes MAX - x (flipping all bits). For signed types, it computes -x - 1 (two's complement).

Common Patterns

Byte Buffer Index

var buffer : [var Nat8] = [var 0, 0, 0, 0];
var index : Nat8 = 0;

public func write(value : Nat8) : async ()
  entry_requires index < 4;
  requires index < 4;
  modifies buffer, index
{
  buffer[index] := value;
  index += 1;
}

Counter with Maximum

var count : Nat32 = 0;

public func increment() : async Nat32
  entry_requires count < 4294967295;
  requires count < 4294967295;
  modifies count
  ensures result == old(count) + 1;
{
  count += 1;
  count
}

Safe Percentage Calculation

public func percentage(value : Nat8, total : Nat8) : async Nat8
  entry_requires total > 0;
  entry_requires value <= total;
  requires total > 0;
  requires value <= total;
  ensures result <= 100;
{
  // Widening prevents overflow in multiplication
  let wide_value : Nat32 = value;
  let wide_total : Nat32 = total;
  let pct : Nat32 = (wide_value * 100) / wide_total;

  // Narrowing is safe because percentage <= 100
  let result : Nat8 = pct;
  result
}

When to Use Fixed-Width Types

Use fixed-width types when:

• You need specific memory layout (e.g., protocol buffers, binary formats)
• You're interfacing with external systems expecting specific sizes
• You want to reason about overflow explicitly
• You're performing bitwise operations

Use unbounded types (Nat, Int) when:

• Values could grow arbitrarily large
• You want simpler verification without overflow guards
• Mathematical correctness is more important than memory efficiency

Summary

• Fixed-width types (Nat8-Nat64, Int8-Int64) have specific bit widths and bounded ranges
• The verifier automatically tracks both lower and upper bounds
• Verified code uses checked mode and requires preconditions to prevent overflow
• Saturating patterns clamp values at boundaries instead of failing
• Type conversions may require explicit conversion functions and proofs when narrowing or changing signedness
• --verify rejects bitvec and unchecked integer modes
• Prefer unbounded types unless you specifically need fixed-width semantics