Loops

Loops let you execute code repeatedly. Sector9 supports while, infinite loop with labeled exits, and for-in iteration over contracted iterators. In verified code, loop invariants are the bridge between each iteration and the final postcondition.

While Loops

The while loop executes its body repeatedly as long as the condition is true:

while (condition) {
  // body
};

The condition must be of type Bool. The loop body must be of type () (unit). The entire while expression returns ().

loop-while-basic.sr9

// Basic while loop with condition and body
module {
  public func countdown(n : Nat) : Nat
    ensures result == 0;
  {
    var i : Nat = n;
    while (i > 0) {
      loop:invariant i <= n;
      i -= 1;
    };
    i
  };

  public func sumTo(n : Nat) : Nat
    ensures 2 * result == n * (n + 1);
  {
    var i : Nat = 0;
    var acc : Nat = 0;
    while (i < n) {
      loop:invariant i <= n;
      loop:invariant 2 * acc == i * (i + 1);
      acc += i + 1;
      i += 1;
    };
    acc
  };
}

The first function counts down from n to zero. The second computes the sum 1 + 2 + ... + n using a while loop with an accumulator.

For-In Loops

The for-in loop iterates over an iterator. The most common iterator is an array's .values():

for (element in array.values()) {
  // body using element
};

The loop variable binds to each element in turn. The body executes once per element and must be of type ().

You can also iterate any object that exposes a next() method with a type contract:

type Iter<T> = {
  next : () -> ?T contract { requires true; ensures true; };
};

func consume(it : Iter<Nat>) : () {
  for (x in it) { let _ = x; };
};

loop-for-basic.sr9

// For-in loop over array.values()
persistent actor {
  public func sumArray(arr : [Nat]) : async Nat
    ensures result >= 0;
  {
    var total : Nat = 0;
    for (x in arr.values()) {
      loop:invariant total >= 0;
      total += x;
    };
    total
  };

  public func countPositive(arr : [Int]) : async Nat
    ensures result >= 0;
  {
    var count : Nat = 0;
    for (x in arr.values()) {
      loop:invariant count >= 0;
      if (x > 0) {
        count += 1;
      };
    };
    count
  };
}

Supported Iterators

Verification supports:

Pattern	Support	Notes
arr.values()	Supported	Special-case with array index/permission invariants
arr.vals() / arr.keys()	Supported	Uses iterator contracts; add your own invariants
blob.values() / blob.keys()	Supported	Iterator contracts are available, contents still opaque
text.chars()	Supported	Iterator contracts are available, contents still opaque
Custom iterators	Supported if next() is contracted	next() must be () -> ?T with a type contract

The verifier relies on the iterator's next() contract. If next() is missing or uncontracted, the loop is rejected. For array-heavy loops, combine these iterator facts with reads and modifies so permissions are explicit.

Infinite Loops

The loop construct creates an infinite loop that must be exited with break:

label name loop {
  // body
  if (exit_condition) {
    break name;
  };
};

Without a break, the loop runs forever (the expression has type Non - non-terminating). With a labeled break, the loop exits and continues after the loop.

loop-infinite.sr9

// Infinite loop with labeled break
persistent actor {
  public func findFirst(target : Int) : async Int
    entry_requires target >= 0 and target <= 100;
    requires target >= 0 and target <= 100;
    ensures result == target or result == -1;
  {
    var i : Int = 0;
    var found : Int = -1;

    label search loop {
      loop:invariant i >= 0;
      loop:invariant found == -1 or found == target;
      if (i > 100) {
        break search;
      };
      if (i == target) {
        found := i;
        break search;
      };
      i += 1;
    };

    found
  };
}

The label search creates a named exit point. The break search statement exits the loop immediately.

Labeled Break

Loops can have labels. The break statement exits the labeled loop:

label name while (condition) {
  // ...
  if (should_exit) {
    break name;
  };
  // ...
};

Break is useful for early exit when you find what you're looking for:

loop-break.sr9

// Labeled break exits the named loop
persistent actor {
  public func findInArray(arr : [Int], target : Int) : async Int
    ensures result == -1 or result >= 0;
  {
    var found : Int = -1;
    var idx : Int = 0;

    label search for (x in arr.values()) {
      loop:invariant found == -1 or found >= 0;
      loop:invariant idx >= 0;
      if (x == target) {
        found := idx;
        break search;
      };
      idx += 1;
    };

    found
  };

  public func sumUntil(arr : [Int], limit : Int) : async Int
    requires limit >= 0;
    ensures result >= 0;
  {
    var sum : Int = 0;

    label iter for (x in arr.values()) {
      loop:invariant sum >= 0;
      if (sum + x > limit) {
        break iter;
      };
      sum += x;
    };

    sum
  };
}

Nested Break

With nested loops, you can break to an outer loop by using its label:

label outer while (i < n) {
  label inner while (j < m) {
    if (found) {
      break outer;  // Exit both loops
    };
    j += 1;
  };
  i += 1;
};

Labeled Continue

The continue statement skips to the next iteration of the labeled loop:

label name while (condition) {
  // ...
  if (should_skip) {
    continue name;
  };
  // rest of body skipped
};

loop-continue.sr9

// Labeled continue skips to next iteration
persistent actor {
  public func sumEvens(n : Int) : async Int
    entry_requires n >= 0;
    requires n >= 0;
    ensures result >= 0;
  {
    var sum : Int = 0;
    var i : Int = 0;

    label iter while (i < n) {
      loop:invariant i >= 0 and i <= n;
      loop:invariant sum >= 0;
      i += 1;
      if (i % 2 != 0) {
        continue iter;
      };
      sum += i;
    };

    sum
  };

  public func skipNegatives(arr : [Int]) : async Int
    ensures result >= 0;
  {
    var sum : Int = 0;

    label process for (x in arr.values()) {
      loop:invariant sum >= 0;
      if (x < 0) {
        continue process;
      };
      sum += x;
    };

    sum
  };
}

The first function sums only even numbers by skipping odd ones with continue. The second skips negative values.

Continue with Nested Loops

Like break, continue can target an outer loop:

label outer for (x in arr1.values()) {
  label inner for (y in arr2.values()) {
    if (condition) {
      continue outer;  // Skip to next x
    };
  };
};

Nested Loops

Each level of nesting can have its own loop invariants. The inner loop's invariant often references the outer loop's state:

loop-nested.sr9

// Nested loops with inner invariant referencing outer state
persistent actor {
  public func sumGrid(rows : Nat, cols : Nat) : async Nat
    entry_requires rows <= 5 and cols <= 5;
    requires rows <= 5 and cols <= 5;
    ensures result == rows * cols;
  {
    var total : Nat = 0;
    var r : Nat = 0;

    while (r < rows) {
      loop:invariant r <= rows;
      loop:invariant total == r * cols;

      var c : Nat = 0;
      while (c < cols) {
        loop:invariant c <= cols;
        loop:invariant total == r * cols + c;
        total += 1;
        c += 1;
      };

      r += 1;
    };

    total
  };
}

The inner invariant total == r * cols + c relates the running total to both the outer loop's progress (r * cols completed rows) and the inner loop's progress (c columns in the current row).

Loop Invariants

All loop forms support the loop:invariant annotation for verification. Place invariants at the start of the loop body:

while (condition) {
  loop:invariant property1;
  loop:invariant property2;
  // body
};

The verifier checks that:

1. The invariant holds before the loop starts
2. Each iteration preserves the invariant
3. The invariant plus the exit condition implies the postcondition

See Loop Invariants for detailed coverage.

Common Invariant Patterns

Bounds tracking:

loop:invariant i >= 0 and i <= n;

Accumulator relationship:

loop:invariant 2 * sum == i * (i + 1);

Field modification tracking:

loop:invariant counter == old(counter) + i;

Automatic Invariants

Sector9 automatically adds some low-level invariants:

• Nat bounds: Variables of type Nat get >= 0 invariants
• Array permissions: Arrays indexed in the loop get permission invariants
• Array size stability: Indexed arrays have their size captured and preserved
• For-loop index bounds: The synthesized index variable stays in bounds

These help with bounds and permissions, but they do not encode your algorithm. You still write the business invariant that connects the loop counter, accumulator, collection model, or actor state to the postcondition.

Return in Loops

The return statement exits the entire function, not just the loop:

public func find(arr : [Int], target : Int) : async Int {
  for (x in arr.values()) {
    if (x == target) {
      return x;  // Exits the function immediately
    };
  };
  -1
};

Restrictions

No Allocation in Conditions

Array literals and object literals cannot appear in while conditions or loop invariants:

// Rejected
while (([] : [Nat]).size() == 0) { ... }

// Use a variable instead
let arr : [Nat] = [];
while (arr.size() == 0) { ... }

For-In Pattern Restrictions

The loop variable pattern must be a simple identifier. Complex patterns are not supported:

// Supported
for (x in arr.values()) { ... }

// Not supported
for (0 in arr.values()) { ... }      // Literal patterns rejected
for (?x in optArr.values()) { ... }  // Option patterns rejected

Termination Not Verified

Sector9 proves partial correctness only. It does not verify that loops terminate. The decreases clause is parsed but rejected in verification mode. See the termination limitation for the broader verifier boundary.

This means the verifier proves: "If the loop terminates, the postcondition holds." It does not prove that the loop actually terminates.

Common Mistakes

Missing Loop Label

Using break or continue requires a label:

// Wrong - no label to break to
while (condition) {
  break;  // Error: needs a label
};

// Correct
label done while (condition) {
  break done;
};

Invariant Not Preserved

The loop body must maintain the invariant:

// Fails verification
while (i < n) {
  loop:invariant counter == old(counter);  // Claims counter unchanged
  counter += 1;  // But we modify it here
  i += 1;
};

The invariant claims counter is unchanged, but the body modifies it.

Missing Bounds Invariant

Forgetting to bound loop variables is a common error:

// May have issues
while (i < n) {
  loop:invariant sum == i * (i + 1) / 2;  // Missing: i >= 0 and i <= n
  // ...
};

Always include bounds invariants for loop counters.

Summary

• while (condition) { body } loops while condition is true
• for (x in arr.values()) { body } iterates over array elements
• for (x in it) { body } iterates any iterator with a contracted next()
• loop { body } creates an infinite loop requiring break to exit
• Labels enable break name and continue name for early exit and skip
• Nested loops can break/continue to outer labels
• All loops support loop:invariant for verification
• Iterators must expose next : () -> ?T with a type contract
• Termination is not verified (partial correctness only)

Related Topics

• Loop invariants for inductive proofs over iteration
• Arrays for array permissions and stable sizes
• Spec collections for sequence/map/set models used in loop summaries