Termination (decreases)

Sector9 verifies partial correctness only: it proves properties hold if programs terminate, but does not prove termination itself.

For the full list of verifier limitations and soundness rules, see Verified Restrictions and Soundness Notes.

What This Means

Sector9 proves that your code is correct assuming it terminates. This is called partial correctness:

• Verified: If a loop finishes, the postcondition holds
• Verified: If a recursive function returns, the result satisfies ensures
• Not verified: Whether the loop or recursion actually terminates

This is a fundamental design choice, not a bug. Many verification systems start with partial correctness because termination proofs require additional infrastructure.

The decreases Clause

The decreases clause would specify a termination measure - a value that decreases on each recursive call or loop iteration. Sector9 parses this syntax but rejects it during verification:

termination-decreases_unsat.sr9

// Decreases clauses are rejected in verification mode
persistent actor {
  public func countdown(x : Nat) : async Nat
    decreases x;  // ERROR: M0335 - decreases clauses not supported
  {
    if (x == 0) { 0 }
    else { await countdown(x - 1) }
  };
}

This produces error M0335:

type error [M0335], decreases clauses are not yet supported for verification

Why decreases Is Unsupported

The underlying Viper/Silicon verification backend has limitations with termination checking:

1. Silicon's termination checking does not work well with algebraic data types (ADTs)
2. The termination plugin (viper.silicon.plugins.Termination) is not available in the current build
3. Without the plugin, decreases clauses cause verification failures

Loops and Partial Correctness

Loop invariants verify that properties hold if the loop terminates:

termination-loop-partial.sr9

// Loops verify partial correctness - IF they terminate, invariants hold
persistent actor {
  var counter : Nat = 0;

  public func sumTo(n : Nat) : async Nat
    modifies counter
    ensures 2 * result == n * (n + 1);
  {
    var i : Nat = 0;
    var acc : Nat = 0;

    while (i < n) {
      loop:invariant i >= 0 and i <= n;
      loop:invariant 2 * acc == i * (i + 1);
      acc += i + 1;
      i += 1;
    };

    acc
  };
}

The verifier proves:

• The invariant holds on loop entry
• Each iteration preserves the invariant
• When i < n becomes false, the postcondition follows

It does not prove that i eventually reaches n. For bounded loops with incrementing counters, termination is obvious to humans but not formally verified.

Recursive Functions

Pure functions cannot be directly recursive in verified code because the verifier would need recursive axioms and termination reasoning for their contracts.

// ERROR: recursive pure functions not supported
pure func factorial(n : Nat) : Nat {
  if (n == 0) { 1 }
  else { n * factorial(n - 1) }
}

Workaround: Trusted Pure Functions

Mark recursive pure functions as trusted to bypass the recursion restriction:

termination-trusted-recursive.sr9

// Workaround: mark recursive pure functions as trusted
module {
  public pure trusted func factorial(n : Nat) : Nat
    requires n >= 0;
    ensures result >= 1;
  {
    if (n == 0) { 1 }
    else { n * factorial(n - 1) }
  };
}

The verifier treats trusted functions as a specification boundary: callers may use the contract, while the trusted body is not proved. This expands your trusted base, so use it sparingly.

Workaround: Lemmas with Closed Forms

When a closed-form solution exists, use a non-recursive pure function with a lemma:

module {
  pure func triangular(n : Nat) : Nat {
    n * (n + 1) / 2
  }

  public lemma triangularStep(i : Nat) : ()
    ensures triangular(i) + (i + 1) == triangular(i + 1);
  { }
}

The pure function is verified (not assumed). The lemma establishes the inductive property.

Workaround: Convert to Loops

Replace recursion with iteration when possible:

public func factorial(n : Nat) : async Nat
  ensures result >= 1;
{
  var acc : Nat = 1;
  var i : Nat = 1;

  while (i <= n) {
    loop:invariant acc >= 1;
    loop:invariant i >= 1;
    acc := acc * i;
    i := i + 1;
  };

  acc
}

Loops with bounded counters are easier to reason about and verify.

Recursive Data Types

Functions over recursive data types (lists, trees) face similar limitations. Base cases verify, but recursive traversals may not unfold correctly:

Works (Base Case)

type List = { #nil; #cons : (Int, List) };

pure func isEmpty(l : List) : Bool {
  switch (l) {
    case (#nil) { true };
    case (#cons(_, _)) { false };
  }
}

Limited (Recursion)

type List = { #nil; #cons : (Int, List) };

// Recursive call limits verification depth
pure func length(l : List) : Nat {
  switch (l) {
    case (#nil) { 0 };
    case (#cons(_, tail)) { 1 + length(tail) };  // Limited unfolding
  }
}

Practical Guidance

Situation	Recommendation
Bounded loop with incrementing counter	Use loop invariants; termination is implicit
Recursive mathematical function	Use closed-form pure function + lemma if possible
Recursive data traversal	Mark as trusted pure or limit to base cases
Complex recursion pattern	Convert to loop with explicit state

Soundness Note

Partial correctness is sound only relative to Sector9's verifier model, the trusted base, and the assumption that the checked execution path terminates. The limitation is that it cannot prove termination:

• If Sector9 verifies your code, the contracts are proven for executions that reach them under that model
• Non-terminating code vacuously satisfies all postconditions (they never run)
• Test for termination through runtime testing and code review

Summary

• Sector9 provides partial correctness - properties are verified assuming termination
• The decreases clause is parsed but rejected (error M0335)
• Pure recursive functions must be marked trusted, replaced with lemmas, or converted to loops
• Loop invariants verify correctness but not termination
• Termination support requires Viper's termination plugin, not currently available