Arrays

Arrays are indexed runtime collections with a fixed size at creation time. Sector9 supports both mutable arrays [var T] that allow element updates and immutable arrays [T] that cannot change after creation. For proof-only sequence models, use Seq instead.

Creating Arrays

Use square brackets to create array literals:

array-basic.sr9

// Basic array creation and access
persistent actor {
  // Immutable array - cannot change elements after creation
  let immutableArr : [Nat] = [1, 2, 3, 4, 5];

  // Mutable array - can update elements
  var mutableArr : [var Nat] = [var 10, 20, 30];
  invariant mutableArr.size() == 3;

  // Empty arrays
  let emptyImmutable : [Nat] = [];
  var emptyMutable : [var Nat] = [var];

  public func basics() : async Nat
    reads immutableArr, mutableArr
  {
    // Read from immutable array
    let first = immutableArr[0];  // 1
    let second = immutableArr[1]; // 2

    // Read from mutable array
    let mFirst = mutableArr[0];   // 10

    // Get array size
    let size = immutableArr.size(); // 5

    assert size == 5;

    first + mFirst // returns 11
  };
}

Key points:

• [T] is an immutable array of elements of type T
• [var T] is a mutable array where elements can be updated
• Literal syntax: [1, 2, 3] for immutable, [var 1, 2, 3] for mutable
• Empty arrays: [] for immutable, [var] for mutable
• All elements must have compatible types
• Use arr[i] to read element at index i (index type is Nat)
• Use arr.size() to get the array length

Mutability

Array mutability determines whether elements can be updated after creation:

array-mutation.sr9

// Updating mutable array elements
persistent actor {
  var data : [var Nat] = [var 1, 2, 3];

  public func updateElement(i : Nat, value : Nat) : async ()
    modifies data
    entry_requires i < data.size();
    requires i < data.size();
    ensures data[i] == value;
  {
    // Update using assignment
    data[i] := value;
  };

  public func swap(i : Nat, j : Nat) : async ()
    modifies data
    entry_requires i < data.size() and j < data.size();
    requires i < data.size();
    requires j < data.size();
    ensures data[i] == old(data[j]);
    ensures data[j] == old(data[i]);
  {
    let temp = data[i];
    data[i] := data[j];
    data[j] := temp;
  };
}

Mutability rules:

• arr[i] := value updates element at index i (mutable arrays only)
• Immutable arrays cannot be updated after creation
• modifies arr grants permission to update any element
• old(arr[i]) captures the element value at method entry

The mutability of an array is part of its type:

• A mutable array [var Nat] cannot be assigned to an immutable [Nat]
• The binding mutability (let vs var) is separate from array element mutability

Bounds Checking

Array access requires proving the index is within bounds. The verifier tracks array sizes and requires explicit bounds checks:

array-bounds.sr9

// Array bounds checking in verification
persistent actor {
  var data : [var Nat] = [var 10, 20, 30];
  invariant data.size() == 3;

  // Correct: bounds check in precondition
  public func safeGet(i : Nat) : async Nat
    reads data
    entry_requires i < data.size();
    requires i < data.size();
    ensures result == data[i];
  {
    data[i]
  };

  // Using size in contracts
  public func getFirst() : async Nat
    reads data
    entry_requires data.size() > 0;
    requires data.size() > 0;
    ensures result == data[0];
  {
    data[0]
  };

  // Size preservation after updates
  public func setFirst(value : Nat) : async ()
    modifies data
    ensures data.size() == old(data.size());
    ensures data[0] == value;
  {
    data[0] := value;
  };
}

Bounds patterns:

• requires i < data.size() - precondition guards array access
• invariant data.size() == N - fixed-size invariant for actor arrays
• ensures data.size() == old(data.size()) - size preserved after update
• Without a bounds guard, verification fails with a permission error because the verifier cannot prove the indexed heap location exists

Iterating with for-in

Use for-in loops with .values() to iterate over array elements:

array-iteration.sr9

// Iterating over arrays with for-in loops
persistent actor {
  var data : [var Nat] = [var 1, 2, 3, 4, 5];
  invariant data.size() == 5;

  // Sum all elements using for-in
  public func sum() : async Nat
    reads data
    ensures result >= 0;
  {
    var total : Nat = 0;
    for (x in data.values()) {
      loop:invariant total >= 0;
      total += x;
    };
    total
  };

  // Count elements matching a condition
  public func countPositive() : async Nat
    reads data
  {
    var count : Nat = 0;
    for (x in data.values()) {
      loop:invariant count <= data.size();
      if (x > 0) {
        count += 1;
      };
    };
    count
  };
}

Loop rules:

• Use arr.values() to iterate over elements
• Add loop:invariant to specify properties preserved across iterations
• The loop variable receives each element value in order

Quantifiers and Arrays

Use forall and exists to express properties over array indices:

array-quantifier.sr9

// Using quantifiers with arrays
persistent actor {
  var data : [var Nat] = [var 1, 2, 3, 4, 5];
  invariant data.size() == 5;
  // All elements are positive
  invariant forall<Nat>(pure func (i : Nat) : Bool =
    (i < data.size()) ==> (data[i] >= 1)
  );

  // Assert all elements satisfy a property
  public func allPositive() : async Bool
    reads data
  {
    let n = data.size();
    assert forall<Nat>(pure func (i : Nat) : Bool =
      (i < n) ==> (data[i] >= 1)
    );
    true
  };

  // Check if any element matches
  public func hasValue(target : Nat) : async Bool
    reads data
  {
    var found = false;
    for (x in data.values()) {
      if (x == target) {
        found := true;
      };
    };
    found
  };
}

Quantifier patterns:

• forall<Nat>(pure func (i : Nat) : Bool = (i < n) ==> property(arr[i])) - all indices
• exists<Nat>(pure func (i : Nat) : Bool = (i < n) and arr[i] == target) - some index
• Always guard with i < arr.size() using implication (==>) for forall or conjunction (and) for exists
• The quantified function must be pure

Footprints

Declare array access in function footprints:

public func readAll() : async Nat
  reads data           // Read permission for all elements
{ ... };

public func updateAll() : async ()
  modifies data        // Write permission for all elements
{ ... };

public func copyTo(dest : [var Nat]) : async ()
  reads data           // Read source
  modifies dest        // Write destination
{ ... };

Footprint rules:

• reads arr grants read access to all elements of arr
• modifies arr grants read and write access to all elements
• Footprints apply to the entire array, not individual indices
• Frame conditions: unlisted fields remain unchanged across calls

Verification Behavior

The verifier models arrays with indexed heap locations:

Motoko	Viper Translation
arr[i] read	$loc(arr, i).$array$T
arr[i] := v write	$loc(arr, i).$array$T := v
arr.size()	$size(arr)
modifies arr	$array_acc(arr, write)

Arrays generate bounds predicates for numeric element types (Nat, Int, fixed-width types). The verifier automatically assumes elements satisfy type bounds (for example, Nat elements are non-negative and fixed-width elements stay inside their checked ranges). See numeric bounds for the same proof shape outside arrays.

Verification Failure Example

Missing bounds checks cause verification failures:

array-missing-bounds_unsat.sr9

// Verification failure: missing bounds check
persistent actor {
  var data : [var Nat] = [var 10, 20, 30];
  invariant data.size() == 3;

  // ERROR: No bounds check - verification fails
  public func unsafeGet(i : Nat) : async Nat
    reads data
    // Missing: requires i < data.size()
    ensures result == data[i];
  {
    data[i] // Verification fails: cannot prove i < size
  };
}

Without requires i < data.size(), the verifier cannot prove the access is safe. The error appears as "insufficient permission to access" because unbounded indices may exceed the array size.

Restrictions

For-In Loop Iterators

arr.values() is special-cased in verification and automatically introduces array permissions and index bounds. Other iterator forms (like arr.keys() or arr.vals()) are supported if the iterator's next() method has a type contract, but they do not introduce array-specific invariants. Add your own invariants or use a while loop when you need bounds facts.

// Recommended: values() gives array-aware invariants
for (x in arr.values()) { ... }

// Supported: iterator form, but you must add your own bounds reasoning
for (k in arr.keys()) { ... }

To iterate with indices and explicit bounds, use a while loop:

var i : Nat = 0;
while (i < arr.size()) {
  loop:invariant i <= arr.size();
  let x = arr[i];
  // use x and i
  i += 1;
};

Pure and Spec Restrictions

Named pure functions cannot close over actor arrays or index mutable arrays from hidden state:

var data : [var Nat] = [var 1, 2, 3];

// ERROR M0317: pure function cannot index arrays
pure func getFirst() : Nat { data[0] };

Pure functions can use their parameters and call other pure functions. For quantified array properties, use a guarded anonymous pure predicate such as i < arr.size() ==> arr[i] >= 0; the verifier supplies the array permission from the surrounding contract or assertion.

Nested Arrays

Nested mutable arrays have limited support:

// Supported: nested immutable arrays
let matrix : [[Nat]] = [[1, 2], [3, 4]];

// Limited: nested mutable arrays may have aliasing issues
var grid : [var [var Nat]] = [var [var 1, 2], [var 3, 4]];

For complex multi-dimensional data, consider flattening:

var flat : [var Nat] = [var 0, 0, 0, 0]; // 2x2 matrix
let cols = 2;

pure func index(row : Nat, col : Nat) : Nat { row * cols + col };

public func set(row : Nat, col : Nat, v : Nat) : async ()
  modifies flat
  entry_requires index(row, col) < flat.size();
  requires index(row, col) < flat.size();
{
  flat[index(row, col)] := v;
};

Mutable Record Arrays

Arrays of mutable records are no longer a blanket unsupported case. Current verification support covers the owned/fresh lanes used by the core library and the ownership tests, including local mutable-record arrays and some opaque handle payloads. Deeply nested or escaping shapes still need explicit ownership and aliasing proofs, and some shapes remain outside the supported verifier lane.

type Cell = { var value : Nat };

// Supported in the fresh local lane.
var cells : [var Cell] = [var { var value = 0 }];
cells[0].value := 1;

When this gets hard to verify, prefer a flattened representation or keep the mutable records behind a small module API with explicit contracts.

Spec Collection Restrictions

Mutable arrays cannot be elements of spec collections (Seq, Set, Map, Multiset):

// ERROR: mutable arrays cannot be Seq elements
let s : Seq<[var Nat]> = Seq.empty();

Spec collections require immutable element types for equality stability.

Array vs Seq

Feature	Array ([T], [var T])	Seq (Seq<T>)
Purpose	Runtime data storage	Verification reasoning
Mutability	Mutable with [var T]	Always immutable
Index type	Nat	Int
Location	Heap-allocated	Ghost state only
Footprints	reads/modifies required	No footprints needed
Operations	Index, update, iterate	Concat, slice, contains

Use arrays for runtime data. Use Seq in ghost blocks and contracts for reasoning about sequences.

Error Codes

Code	Meaning
M0317	Pure function cannot index arrays
M0242	Mutable array in spec collection element

Summary

• [T] is immutable; [var T] is mutable
• Create with literals: [1, 2, 3] or [var 1, 2, 3]
• Access elements with arr[i] where i : Nat
• Get length with arr.size()
• Update mutable arrays with arr[i] := value
• Declare footprints: reads arr or modifies arr
• Always guard access with bounds checks: requires i < arr.size()
• Use for (x in arr.values()) to iterate
• Use forall<Nat>(...) with i < size ==> guard for array properties
• Named pure functions cannot close over actor arrays; guarded anonymous pure predicates are the usual way to write quantified array facts
• Nested mutable arrays and mutable record arrays have limited support