Counterexamples (--counterexample)

Concrete failing values that show why verification failed.

When verification fails, the verifier can sometimes produce a counterexample: a specific set of input values that violates the contract. This transforms an abstract "might not hold" message into a concrete debugging scenario with actual values.

When to Use

Use --counterexample (or the alias --models) when:

• A postcondition failure message is unclear
• You need to understand which inputs violate a contract
• You want to reproduce a verification failure with concrete values
• You are debugging complex arithmetic or state-based contracts

Basic Usage

Add --counterexample to any verification command:

sector9 --package core ./core/src --verify --counterexample file.sr9

The alias --models works identically:

sector9 --package core ./core/src --verify --models file.sr9

Counterexamples work with all output formats:

sector9 --package core ./core/src --verify --counterexample file.sr9           # Human-readable
sector9 --package core ./core/src --verify --json --counterexample file.sr9    # JSON output
sector9 --package core ./core/src --verify --toon --counterexample file.sr9    # TOON output

Counterexample extraction uses the Viper server path. If viperserver.jar is not discoverable, the command exits before verification and asks you to set VIPER_SERVER=/absolute/path/to/viperserver.jar or rebuild the toolchain.

What Counterexamples Show

A counterexample provides concrete values for variables at the point of failure. Consider this buggy function:

public func add(a : Int, b : Int) : async Int
  ensures result == a + b + 1;  // Bug: off by one
{
  a + b
};

Without --counterexample:

✗ verification failed (1 issue)

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

With --counterexample:

✗ verification failed (1 issue)

------------------------------
[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 reveals that when a=0 and b=0, the function returns 0, but the postcondition expects 1.

Counterexample Structure

Counterexamples contain one or more models, each representing program state at a specific point:

Model Labels

Label	Meaning
entry	State when function is called (precondition context)
return	State when function returns (postcondition context)
Named labels	State at specific assertion points

Binding Types

Each variable binding has a kind:

Kind	Description	Examples
local	Function parameters and local variables	x, amount, result
field	Actor or object fields	self.balance, self.count
internal	Compiler-generated variables	$Res, $Self

By default, internal bindings are hidden unless they appear in the error message. Use --show-internal to include all internal bindings.

State and Heap Counterexamples

Counterexamples work for both pure arithmetic and stateful code.

Arithmetic Example

public func abs(x : Int) : async Int
  ensures result >= 0;
  ensures x >= 0 ==> result == x;  // Bug: missing negative case
{
  x  // Returns x unchanged
};

Counterexample:

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

The verifier found that x=-1 produces result=-1, violating result >= 0.

State Update Example

persistent actor Bank {
  var balance : Nat = 0;

  public func deposit(amount : Nat) : async ()
    modifies balance
    ensures balance == old(balance) + amount + 1;  // Bug: off by one
  {
    balance := balance + amount;
  };
}

Counterexample:

Counterexample summary
  return: amount=0, self=...

When amount=0, the balance increases by 0, not by 1 as the postcondition requires.

JSON Counterexample Format

With --json, counterexamples appear in a structured format:

{
  "counterexample": {
    "models": [
      {
        "label": "return",
        "bindings": [
          {
            "name": "a",
            "value": "0",
            "kind": "local",
            "scope": "local"
          },
          {
            "name": "b",
            "value": "0",
            "kind": "local",
            "scope": "local"
          },
          {
            "name": "$Res",
            "value": "0",
            "kind": "internal",
            "scope": "internal"
          }
        ]
      }
    ]
  }
}

Extract counterexample values with jq:

# Get all binding names and values
sector9 --package core ./core/src --verify --json --counterexample file.sr9 | \
  jq '.failures[0].counterexample.models[].bindings[] | "\(.name)=\(.value)"'

# Get only local bindings
sector9 --package core ./core/src --verify --json --counterexample file.sr9 | \
  jq '.failures[0].counterexample.models[].bindings[] | select(.kind == "local")'

Interpreting Counterexample Values

Numeric Values

Integer values appear as decimal strings:

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

Reference Values

Object references appear as solver-internal representations:

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

These internal representations indicate the solver's model for heap objects. The specific syntax is not meant for direct interpretation; what matters is whether values are distinct or equal.

Field Values

Actor fields are shown with the self. prefix:

self.balance=100, self.count=5

Limitations

Counterexamples have some limitations to be aware of:

Not Always Available

The SMT solver may not produce a model for every failure. Complex constraints or timeouts can result in missing counterexamples.

Symbolic Values

Some values may appear as symbolic expressions rather than concrete numbers when the solver cannot determine a specific value.

Heap Abstraction

Heap state (mutable records, arrays) may appear as abstract references rather than fully expanded values.

Backend Requirement

Counterexample extraction requires the Viper server/Silicon backend with model support. If the backend is missing or lacks counterexample support, an error appears before models are printed:

sector9 verify: could not locate viperserver.jar

Related Flags

Flag	Effect
--counterexample	Include counterexample models in output
--models	Alias for --counterexample
--show-internal	Include internal bindings (e.g., $Res, $Self)

For machine-readable model data, combine this with JSON Output or TOON Format.

Debugging Workflow

A typical workflow when a verification failure occurs:

1. Run with --counterexample to get concrete values
2. Identify which inputs cause the failure
3. Check if those inputs are expected (valid inputs that expose a bug) or unexpected (missing precondition)
4. Fix the implementation or strengthen the contract accordingly

Example:

# Step 1: Get counterexample
$ sector9 --package core ./core/src --verify --counterexample transfer.sr9
...
Counterexample summary
  return: amount=100, self.balance=50

# Step 2: Interpret
# The failure shows amount=100 when balance=50
# This means transferring more than available triggers the failure

# Step 3: Fix - add a precondition
# requires amount <= balance;

Summary

• Use --counterexample to request concrete failing values
• --models is an alias for --counterexample
• Counterexamples show variable values at entry and return points
• Bindings are classified as local, field, or internal
• Use with --json for programmatic processing
• Not all failures produce counterexamples because models depend on the backend and the failing obligation shape
• Use --show-internal to see compiler-generated variables