Reading Error Messages

Understanding what the verifier is telling you.

Sector9 produces two categories of errors: type/translation errors that occur before verification, and verification failures that occur when the verifier cannot prove a property. This page explains how to read both.

The Two Error Categories

Type and Translation Errors

These errors prevent verification from running. They include type mismatches, syntax errors, unsupported constructs, and translation failures.

Format:

file.sr9:line:column: category error [CODE], message

Example:

counter.sr9:5:12: type error [M0057], unbound variable balanse

Common categories:

• type error - Type mismatch, undefined variable, constraint violation
• syntax error - Invalid syntax or misplaced construct
• viper error - Unsupported construct that cannot be translated

Use sector9 --explain M0057 to request a longer explanation for an error code when one is available. Some codes currently only print the short diagnostic, so the source span and message remain the most important evidence.

Verification Failures

These errors indicate the verifier found a possible execution path where your specification does not hold. The program is syntactically correct, but the verifier cannot prove the property you specified.

Format:

✗ verification failed (N issues)

------------------------------
[1] Obligation might not hold
  Detailed message about what failed.
  method: function_name
  at: file.sr9:line:column
  snippet:
      relevant source code
  hint:
    - Suggestion for fixing

Understanding Obligation Types

Each verification failure reports an obligation - a property the verifier tried to prove. The obligation type tells you what kind of specification failed.

Postcondition Failures

[1] Postcondition might not hold
  Assertion result >= 0 might not hold.
  method: withdraw

What it means: The function body does not establish the ensures clause.

Common causes:

• Missing case in implementation (e.g., negative result possible)
• Postcondition is stronger than what the code guarantees
• Missing intermediate assertions to guide the proof

Fix strategies:

• Check that all code paths establish the postcondition
• Add assert statements to verify intermediate values
• Weaken the postcondition if it is too strong

Precondition Failures

[1] Precondition might not hold
  Precondition n > 0 might not hold at this call site.
  method: divide
  at: math.sr9:15:12

What it means: The caller does not establish the callee's requires clause.

Common causes:

• Calling a function without satisfying its requirements
• Caller's preconditions are weaker than what the callee needs
• Missing guard before the call

Fix strategies:

• Add a precondition to the caller that implies the callee's requirement
• Add a guard (if (n > 0) { ... }) before the call
• Strengthen the caller's requires clause

Assert Failures

[1] Assert might not hold
  Assertion x >= 0 might not hold.
  at: counter.sr9:25:4

What it means: The static assert statement cannot be proven true at that point.

Common causes:

• Insufficient preconditions to establish the assertion
• Missing loop invariant in a preceding loop
• State changed by an intervening operation

Fix strategies:

• Add preconditions that imply the assertion
• Add intermediate assertions to track value changes
• Check that loop invariants capture necessary properties

Invariant Failures

[1] Invariant might not hold
  Folding $Inv($Self) might fail.
  Assertion self.balance >= 0 might not hold.

What it means: An actor invariant is not maintained at a public boundary.

Common causes:

• Method modifies state but breaks the invariant
• Initialization does not establish the invariant
• State changed across await violates the invariant

Fix strategies:

• Ensure all methods restore the invariant before returning
• Check that __init__ establishes the invariant
• Verify invariants hold before and after each await

Loop Invariant Failures

[1] Loop invariant might not hold
  Loop invariant sum >= 0 might not hold.
  at: loop.sr9:12:8

What it means: Either the loop:invariant is not established on loop entry, or the loop body does not preserve it.

Common causes:

• Invariant not true before the first iteration
• Loop body breaks the invariant
• Invariant too weak to prove the postcondition

Fix strategies:

• Check that the invariant holds before the loop starts
• Ensure each iteration preserves the invariant
• Strengthen the invariant to include all necessary properties

Permission Failures

[1] Insufficient permission
  There might be insufficient permission to access self.balance.

What it means: The function accesses a field not listed in its reads or modifies clause.

Common causes:

• Missing reads clause for a field that is read
• Missing modifies clause for a field that is written
• Calling a helper that needs permissions not granted to the caller

Fix strategies:

• Add reads field_name to the function signature
• Add modifies field_name if the field is also written
• Ensure transitive permissions through the call chain

Reading the Failure Details

Each failure includes contextual information:

Location (at:)

at: counter.sr9:8:4

Points to the source location where the failure occurred. For precondition failures, this is the call site. For postcondition failures, this is often the ensures clause.

Method Name (method:)

method: increment

The function or method containing the failure. For actor invariants, this may be __init__ or a public method.

Snippet (snippet:)

snippet:
    ensures result == x + 1;

The relevant source code. For complex failures, this helps identify which specification or statement failed.

Label (label:)

label: safety_check

If you named an assertion with a label, it appears here. Named assertions help identify failures in code with multiple assertions.

Hints (hint:)

hint:
  - Strengthen the implementation or weaken the ensures.
  - Check that all code paths establish the postcondition.

Actionable suggestions for resolving the failure. These are generated from the mapped obligation and source context when available, with text fallback only for presentation. A precondition failure inside an ensures, invariant, or loop:invariant may name the helper whose requires clause was not proven. For arithmetic, a Nat subtraction lower-bound hint is emitted only when the failing obligation is actually a Nat subtraction or generated Nat.sub obligation.

Interpreting Common Error Patterns

Division by Zero

[1] Assert might not hold
  Division might fail due to possible zero divisor.

Division and modulo require explicit non-zero guards. Put caller-controlled guards in both entry_requires and requires on exported methods:

// Add precondition
public func divide(x : Nat, y : Nat) : async Nat
  entry_requires y != 0;
  requires y != 0;
  ensures result == x / y;

Nat Subtraction Underflow

[1] Assert might not hold
  Nat subtraction might require the left side to be at least the right side.

Natural number subtraction is partial. Guard x - y with a fact such as x >= y, or use a branch that handles the x < y case before subtracting:

public func debit(balance : Nat, amount : Nat) : async Nat
  entry_requires amount <= balance;
  requires amount <= balance;
  ensures result == balance - amount;
{
  balance - amount
}

Missing Footprint

[1] Insufficient permission to access balance
  footprint_missing:
    reads: ["balance"]

The footprint_missing field (in JSON output) identifies exactly which clauses are missing:

// Add the missing reads
public func getBalance() : async Nat reads balance {
  balance
}

State Across Await

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

State may change during await due to interference:

// Wrong: counter may be modified by other calls during await
public func run() : async () modifies counter
  ensures counter == old(counter) + 1;
{
  counter += 1;
  try { await pause(); } catch (_) {};  // Interference point
}

// Right: only guarantee invariant properties
public func run() : async () modifies counter
  ensures counter >= 0;  // If backed by an actor invariant
{
  counter += 1;
  try { await pause(); } catch (_) {};
}

Pure Function Restrictions

counter.sr9:4:33: type error [M0240], pure functions may not write state
counter.sr9:5:5: type error [M0317], pure function cannot access `counter`

Pure functions cannot access actor state or perform side effects:

// Wrong
pure func helper() : Nat { counter }

// Right: pass state as parameter
pure func helper(c : Nat) : Nat { c + 1 }

Using Counterexamples

Add --counterexample to ask the backend for concrete values that violate the specification:

sector9 --verify --counterexample file.sr9

Counterexample extraction needs the Viper server backend. If viperserver.jar is missing, use JSON or TOON without --counterexample first, or set VIPER_SERVER=/absolute/path/to/viperserver.jar.

Output:

Counterexample summary
  result = -5
  amount = 100
  balance = 50

This shows that when amount = 100 and balance = 50, the result is -5, violating a postcondition like result >= 0.

Counterexamples transform abstract failures into concrete test cases you can reason about.

Quick Diagnosis Guide

Symptom	Likely Cause	First Step
Postcondition fails	Implementation does not match spec	Add assert before return
Precondition fails at call	Caller does not establish requirement	Add guard or caller precondition
Invariant fails	State mutation breaks invariant	Check all modifying code paths
Permission error	Missing reads or modifies	Check footprint declarations
Division error	Missing non-zero guard	Add entry_requires divisor != 0 and requires divisor != 0 on exported methods
Type error M0240	Pure function accesses state	Pass state as parameter
Type error M0317	Pure function reads field	Make function non-pure or pass value

When to Use JSON Output

For complex failures or scripted analysis, use --json:

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

JSON output includes:

• failure_id - Stable hash for correlating failures across runs
• obligation_kind - Machine-readable obligation type
• fix_hints - Array of suggested fixes
• footprint_missing - Exact missing reads/modifies clauses
• counterexample - Structured counterexample data

See JSON Output for the complete schema.

Summary

• Type errors (M0xxx codes) prevent verification from running
• Verification failures indicate the verifier cannot prove a specification
• Each failure reports an obligation type: postcondition, precondition, assert, invariant, or permission
• The at:, snippet:, and hint: fields help locate and fix the issue
• Use --counterexample to see concrete failing values
• Common patterns include division guards, missing footprints, and pure function restrictions
• Use --json for programmatic analysis of failures