Skip to main content

Counterexample Analysis

Using --counterexample to find the failing case.

When verification fails with an abstract "might not hold" message, counterexamples can provide concrete values that trigger the failure. This page explains how to analyze backend models when the Viper server can produce them.

Getting Counterexamples​

Add --counterexample (or --models) to your verification command:

sector9 --verify --counterexample file.sr9

Counterexample extraction requires the Viper server backend. If this environment cannot locate viperserver.jar, the command exits before producing models. You can still use JSON Output or TOON Format without models to inspect the failing obligation.

This produces output like:

------------------------------
[1] Postcondition might not hold
  Assertion result == a + b + 1 might not hold.
  method: add

Counterexample summary
  return: a=0, b=0, result=0

The counterexample shows that a=0, b=0 produces result=0, but the postcondition expects result=1.

The Analysis Workflow​

Counterexample analysis follows a three-step process. Use the obligation from Reading Error Messages first, then use the model to decide whether the specification or implementation is wrong.

Step 1: Identify the Failing Inputs​

Look at the counterexample bindings and identify which values are relevant to the failure:

Counterexample summary
  return: amount=100, self.balance=50

Here amount=100 and self.balance=50 are the inputs that cause the failure.

Step 2: Trace the Execution​

Mentally execute the function with those specific values:

public func withdraw(amount : Nat) : async Nat
  reads balance
  modifies balance
  ensures result == amount;  // What happens when amount=100, balance=50?
{
  balance := balance - amount;  // 50 - 100 = underflow
  amount
}

Step 3: Determine the Fix​

Ask: Are these inputs valid or invalid?

  • Valid inputs exposing a bug: Fix the implementation
  • Invalid inputs: Add a precondition to rule them out

For the withdrawal example, amount=100 when balance=50 is an invalid scenario. Add an exported runtime guard plus the matching logical precondition:

public func withdraw(amount : Nat) : async Nat
  entry_requires amount <= balance;
  requires amount <= balance;  // Rule out invalid inputs
  reads balance
  modifies balance
  ensures result == amount;

Analyzing Postcondition Failures​

Postcondition failures are the most common case for counterexample analysis.

Example: Off-by-One Error​

persistent actor Counter {
  var count : Nat = 0;

  public func increment() : async Nat
    modifies count
    ensures count == old(count) + 2;  // Bug: claiming +2 when doing +1
  {
    count += 1;
    count
  };
}

Running with --counterexample:

[1] Postcondition might not hold
  Assertion count == old(count) + 2 might not hold.

Counterexample summary
  return: self.count=1

Analysis: When old(count)=0, incrementing by 1 gives count=1, not count=2. The postcondition is wrong.

Fix: Change + 2 to + 1 in the postcondition.

Example: Missing Case​

public func abs(x : Int) : async Int
  ensures result >= 0;
  ensures x >= 0 ==> result == x;
{
  x  // Bug: doesn't handle negative case
};

Counterexample:

Counterexample summary
  return: x=-1, result=-1

Analysis: When x=-1, the function returns -1, violating result >= 0.

Fix: Add the negative case:

public func abs(x : Int) : async Int
  ensures result >= 0;
{
  if (x >= 0) { x } else { -x }
};

Analyzing Precondition Failures​

When a precondition fails at a call site, the counterexample shows the caller's state.

public func safeDivide(a : Nat, b : Nat) : async Nat
  entry_requires b != 0;
  requires b != 0;
{
  a / b
};

public func compute(x : Nat) : async Nat {
  try { await safeDivide(10, x) } catch (_) { 0 }  // Error: x might be 0
};

Counterexample:

[1] Precondition might not hold
  Precondition b != 0 might not hold at this call site.

Counterexample summary
  entry: x=0

Analysis: The caller can receive x=0, which violates the callee's requirement.

Fix: Add a guard or precondition to the caller:

public func compute(x : Nat) : async Nat
  entry_requires x != 0;
  requires x != 0;
{
  try { await safeDivide(10, x) } catch (_) { 0 }
};

Analyzing Invariant Failures​

Actor invariants must hold at public boundaries. Counterexamples show the state when the invariant breaks.

persistent actor Bank {
  var deposits : Nat = 0;
  var withdrawals : Nat = 0;

  invariant deposits >= withdrawals;

  public func withdraw(amount : Nat) : async ()
    modifies withdrawals
  {
    withdrawals += amount;  // Can break invariant
  };
}

Counterexample:

[1] Invariant might not hold
  Assertion deposits >= withdrawals might not hold.

Counterexample summary
  return: amount=100, self.deposits=50, self.withdrawals=150

Analysis: Starting with deposits=50, withdrawals=50, withdrawing 100 makes withdrawals=150, breaking the invariant.

Fix: Add a precondition:

public func withdraw(amount : Nat) : async ()
  entry_requires withdrawals + amount <= deposits;
  requires withdrawals + amount <= deposits;
  modifies withdrawals

Analyzing Loop Invariant Failures​

Loop invariant failures show the state at a specific iteration.

public func sum(arr : [Nat]) : async Nat {
  var total : Nat = 0;
  var i : Nat = 0;
  while (i < arr.size())
    loop:invariant total >= 0;  // Too weak
    loop:invariant i <= arr.size();
  {
    total += arr[i];
    i += 1;
  };
  total
};

If verification fails because the invariant is too weak to prove the postcondition, you need to strengthen it:

loop:invariant forall<Nat>(pure func (j : Nat) : Bool =
  j < i ==> arr[j] <= total);

Interpreting Counterexample Values​

Numeric Values​

Integers appear as decimal strings:

a=0, b=-5, result=100

Reference Values​

Heap objects appear as solver-internal representations:

self=Null($Ref!val!0)       # Null reference
self=Ref ($Ref!val!0) {...} # Non-null reference

These indicate whether references are equal or distinct. The specific syntax is not meant for direct interpretation.

Field Values​

Actor fields appear with the self. prefix:

self.balance=100, self.count=5

Internal Variables​

By default, compiler-generated variables like $Res (result) and $Self are hidden. Use --show-internal to see them:

sector9 --verify --counterexample --show-internal file.sr9

When Counterexamples Are Not Available​

Counterexamples may be missing or incomplete in some cases:

SMT Solver Limitations​

Complex constraints or timeouts can prevent the solver from producing a model:

[1] Postcondition might not hold
  ...
  (no counterexample available)

Workaround: Simplify the specification, add intermediate assertions, or increase the verification timeout.

Symbolic Values​

Some values may appear as symbolic expressions rather than concrete numbers:

x=f(...)

Workaround: Add intermediate assertions to constrain the search space.

Permission Failures​

Permission errors (missing reads/modifies) don't produce counterexamples because the contract is malformed before the solver runs.

Debugging Workflow Example​

Consider this complete debugging session:

persistent actor TokenVault {
  var supply : Nat = 1000;
  var locked : Nat = 0;

  public func lock(amount : Nat) : async ()
    modifies supply
    modifies locked
    ensures supply + locked == 1000;  // Conservation law
  {
    supply -= amount;
    locked += amount;
  };
}

Step 1: Run with counterexample

$ sector9 --verify --counterexample vault.sr9

Output:

[1] Postcondition might not hold
  Assertion supply + locked == 1000 might not hold.

Counterexample summary
  return: amount=1001, self.supply=..., self.locked=...

Step 2: Analyze

When amount=1001 and supply=1000, the subtraction supply -= amount would underflow (or in Nat semantics, trap). The postcondition cannot hold because the operation itself is invalid.

Step 3: Fix

Add entry_requires and requires to rule out invalid exported calls:

public func lock(amount : Nat) : async ()
  entry_requires amount <= supply;
  requires amount <= supply;  // Cannot lock more than available
  modifies supply
  modifies locked
  ensures supply + locked == 1000;

Using JSON for Programmatic Analysis​

For CI/CD or scripted analysis, use --json with --counterexample:

sector9 --verify --json --counterexample file.sr9 | jq '.failures[0].counterexample'

Extract specific bindings:

# Get all variable values
jq '.failures[0].counterexample.models[].bindings[] | "\(.name)=\(.value)"'

# Get only local variables
jq '.failures[0].counterexample.models[].bindings[] | select(.kind == "local")'

See JSON Output and Counterexamples (--counterexample) for the complete schema.

Summary​

  • Run sector9 --verify --counterexample file.sr9 to get concrete failing values
  • Follow the three-step workflow: identify inputs, trace execution, determine fix
  • Valid failing inputs indicate implementation bugs; invalid inputs need preconditions
  • Counterexamples may be available for postconditions, preconditions, invariants, and assertions
  • Use --show-internal to see compiler-generated variables
  • Counterexamples may be unavailable for complex constraints or permission errors
  • Use --json for programmatic analysis in CI/CD pipelines