Frequently Asked Questions

Common questions and answers about Sector9 verification.

General Questions

What does "verification failed" mean?

When Sector9 reports a verification failure, it means the verifier found a modeled execution path where your specification does not hold. This is different from a test failure: verification checks symbolic inputs, not just sampled test cases.

A failure indicates one of:

• A bug in your code that violates the specification
• A specification that is too strong for the implementation
• A missing precondition, invariant, or loop invariant

Use --counterexample to see concrete values that trigger the failure when the Silicon/Viper server JAR is available in your environment.

Why does verification take so long?

Verification time depends on:

• Quantifiers: Universal (forall) and existential (exists) quantifiers require SMT solver instantiation. Keep triggers small and well-scoped.
• Large old() expressions: Snapshots of heap structures add overhead. Minimize old() over complex data.
• Nested loops: Each loop requires an invariant; deeply nested loops compound proof complexity.

Tips for faster verification:

• Use --cores N for parallel verification
• Break large functions into smaller ones with clear contracts
• Use named helper predicates instead of inline complex expressions

What is the difference between assert and runtime:assert?

Construct	Verification	Runtime
assert P	Proof obligation	Erased (no effect)
runtime:assert P	Proof obligation	Traps if P is false
trap P	Proves not P	Traps if P is true

Use assert for verification-only checks. Use runtime:assert when you want both verification and runtime enforcement. Use trap for conditions that should be unreachable under the current specification.

Can I verify partial programs?

Yes. Use trusted functions to stub unverified code:

public trusted func externalCall() : async Nat
  requires true;
  ensures result >= 0;
{ 0 }  // Body not verified, but contract is assumed

The verifier assumes trusted contracts hold without proof. Keep your trusted base minimal.

---

Ghost State Questions

Where can I use ghost variables?

Ghost variables can be mentioned in verifier-only contracts and invariants. Runtime code cannot read or write them; updates belong in ghost { } blocks:

ghost var counter : Nat = 0;

public func increment() : async () modifies counter {
  // counter := 1;  // ERROR M0314: outside ghost block
  ghost { counter := counter + 1; };  // Correct
}

Actor and module ghost fields can appear in verifier-only contracts such as requires, ensures, and modifies. Local ghost variables cannot appear in contracts because they are out of scope, and ghost state cannot appear in entry_requires because those guards run at runtime.

Can ghost blocks modify runtime state?

No. Ghost blocks are erased at runtime, so allowing runtime state modification would be unsound. The following are rejected:

• Actor field assignment: ghost { balance := 0; } (rejected)
• Array element assignment: ghost { arr[0] := 1; } (rejected)
• Mutable record field assignment: ghost { cell.x := 1; } (rejected)

Ghost blocks can read runtime state for assertions:

ghost { assert balance >= 0; };  // Reading balance is fine

What goes in ghost blocks vs contracts?

Purpose	Use
Caller-visible requirements	requires clause
Caller-visible guarantees	ensures clause
Internal verification state	ghost var + ghost { }
Intermediate proof steps	assert inside function body

Ghost state is for tracking internal invariants that callers do not see. Contracts describe the public interface.

---

Spec Collection Questions

Do updates consume collections?

No. Spec collections (Map, Set, Seq, Multiset) are persistent values. Updates return new values and do not consume the old version, so aliasing is allowed:

ghost {
  let m0 = Map.empty<Nat, Int>();
  let m1 = Map.update(m0, 1, 10);
  let m2 = Map.update(m0, 2, 20);  // ok: m0 still valid
  assert Map.card(m0) == 0;
}

Update operations return new collections; read operations (get, contains, card, domain, len) are pure queries.

What types can I store in collections?

Collections require spec-immutable element types:

Allowed:

• Primitives: Nat, Int, Bool, Text, etc.
• Immutable records: Records without var fields
• Tuples of immutable types
• Options: ?T where T is immutable
• Nested collections: Map<Nat, Set<Nat>>
• Opaque/token handles by identity: Map<Nat, Asset.Handle> records the handle, not a payload snapshot

Rejected (error M0242):

• Records with var fields
• Arrays (both [T] and [var T])
• Functions
• Actors and modules
• Async types

---

Async/Await Questions

What happens to state across await?

At each await point, the verifier models potential interference from other messages. In verification mode, it also rejects locals that may reference actor state across an await (you must drop or copy them first).

1. Before await: Actor invariant must hold
2. During await: Any public method could execute (any number of times, any order)
3. After await: Actor invariant is re-assumed, but exact values may have changed

public func run() : async () modifies counter {
  let before = counter;
  try { await pause(); } catch (_) {};
  // assert counter == before;  // FAILS: counter may have changed
  assert counter >= 0;           // Valid if invariant guarantees this
}

How do I preserve values across await?

Use the snapshot pattern with primitive values:

public func run() : async Int modifies counter {
  let snapshot = counter;  // Primitive value copied
  try { await bump(); } catch (_) {};
  snapshot  // Preserved across await
}

This works for primitives (Int, Nat, Bool, Text) and immutable records. It does NOT work for mutable references or arrays - those remain aliased and subject to interference.

Why does my local variable change across await?

Check if your "local" actually aliases actor state:

// WRONG: alias to actor field
let cell_ref = actorCell;
try { await pause(); } catch (_) {};
assert cell_ref.x == old_value;  // FAILS: aliased state havoced

// RIGHT: fresh allocation
let fresh : Cell = { var x = 1 };
try { await pause(); } catch (_) {};
assert fresh.x == 1;  // Valid: fresh locals preserved

The verifier performs escape analysis. If a value escapes to actor fields or comes from external sources, it is subject to interference, and verification now rejects keeping those references across an await.

Why does the verifier require try/catch around await?

Awaiting an async call can fail with a runtime Error. In verification mode, every await must be enclosed in a try with a catch-all handler so the error path is explicitly handled. Use:

try { await risky() } catch (_) { /* return fallback */ }

await? is not supported in Sector9.

How are async* and await* different from async and await?

async* creates a repeatable computation and await* executes it by passing control into the callee. It does not force a new interleaving point by itself. If the callee never reaches a real suspending await, the call remains atomic. If it may suspend, await* must be inside a catch-all try/catch, and the verifier applies the same await-interference model.

What does old() refer to across await?

old() always refers to method entry, not the most recent await. There are no per-await snapshots:

public func run() : async () modifies counter
  ensures counter >= old(counter)  // old = value at method entry
{
  counter += 10;
  try { await pause(); } catch (_) {};  // Interference may change counter
  counter += 5;      // old(counter) still = entry value
}

---

Pure Function Questions

What restrictions apply to pure functions?

Pure functions must be side-effect free:

Allowed	Not Allowed
Parameters	State access (actor/module fields)
Pure/trusted calls with known summaries	Mutation of any kind
Immutable expressions	assert, trap, runtime:assert
Non-recursive logic	Recursion (even mutual)

// Valid pure function
pure func square(n : Int) : Int { n * n };

// Invalid: recursive
pure func fact(n : Nat) : Nat {
  if (n == 0) { 1 } else { n * fact(n - 1) }  // Rejected
};

// Invalid: state access
pure func getCounter() : Nat { counter };  // Rejected

Why can't pure functions be recursive?

The verifier inlines local pure function bodies at call sites. Recursive definitions would cause infinite inlining. If you need recursion, use a method or lemma with contracts, or isolate a trusted proof helper.

Why can't pure functions use old()?

Pure functions have no state, so there is no "prior state" to capture. The old() expression only makes sense in postconditions of stateful methods.

---

Contract Questions

Why can't I use old() in requires?

The requires clause is checked at method entry - there is no prior state yet. Use old() only in ensures:

// WRONG
public func increment() : async ()
  requires old(counter) >= 0;  // Rejected: old() in requires

// RIGHT
public func increment() : async ()
  entry_requires counter >= 0;
  requires counter >= 0;
  ensures counter == old(counter) + 1;

Why doesn't my division verify?

Division by zero is undefined and must be explicitly guarded, even in specifications:

// WRONG
public func divide(x : Nat, y : Nat) : async Nat
  ensures result == x / y;  // y could be 0

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

This applies to both code and specifications.

Why do I need reads and modifies?

These clauses declare your function's footprint:

• modifies x grants write permission to field x
• reads x grants read permission to field x

Missing declarations cause permission errors:

var a : Int = 0;
var b : Int = 0;

private func helper() : Int reads a, b {
  a + b
};

// WRONG: missing reads b
public func caller() : async Int reads a {
  helper()  // Error: no permission to read b
};

// RIGHT
public func caller() : async Int reads a, b {
  helper()
};

---

Array and Loop Questions

Why does my array access fail even with a size check?

Preconditions alone may not establish array permissions. Add an invariant:

var arr : [var Nat] = [var 1, 2, 3];
// Without invariant: verifier cannot prove size is stable
invariant arr.size() == 3;

public func getFirst() : async Nat
  entry_requires arr.size() >= 1;
  requires arr.size() >= 1;
  ensures result == arr[0];

What loop iteration patterns are supported?

for-in accepts any iterator object whose next() method is () -> ?T with a type contract. Arrays get a special-case arr.values() lowering with built-in invariants, but other iterators are also supported:

// Supported (array-specialized invariants)
for (x in arr.values()) { ... }

// Supported (iterator contracts; add your own invariants)
for (k in arr.keys()) { ... }
for (c in text.chars()) { ... }

For indices with strong bounds guarantees, you can still use while loops with explicit index management.

How do I find the right loop invariant?

Loop invariants must be:

1. True on entry: Holds before the first iteration
2. Preserved: If true before an iteration, true after
3. Useful: Combined with loop exit condition, proves what you need

Common patterns:

• Bounds: loop:invariant i >= 0 and i <= n
• Partial results: loop:invariant sum == expected_sum_for_indices_0_to_i
• Ghost state: loop:invariant ghost_count == i

Add intermediate assertions inside the loop to debug invariant failures.

---

Quantifier Questions

How do triggers work?

Triggers guide the SMT solver on when to instantiate quantified formulas. Use forallWith for explicit triggers:

assert forallWith<Nat>(
  pure func (k : Nat) : Bool = Set.contains(k, s) ==> k >= 0,
  [pure func (k : Nat) : Bool = Set.contains(k, s)]  // Trigger: call-like
);

Without good triggers, the solver may:

• Fail to instantiate (verification fails unexpectedly)
• Over-instantiate (verification times out)

When should I use forall vs forallWith?

Use forall when trigger inference works (simple cases):

assert forall<Nat>(pure func (n : Nat) : Bool = n + 1 > n);

Use forallWith when you need explicit control:

assert forallWith<Nat>(
  pure func (k : Nat) : Bool = Map.contains(k, m) ==> Map.get(m, k) >= 0,
  [pure func (k : Nat) : Bool = Map.contains(k, m)]
);

---

Error Resolution Quick Reference

Error	Cause	Fix
M0242	Mutable type in collection	Use immutable element types
M0243	Disabled historical collection-linearity check	Current spec collections are persistent values
M0244	Disabled historical collection-linearity check	Bind update results when you need the new value
M0311	==> outside a verification context	Use in contracts, verification assertions, ghost blocks, pure functions, or lemmas
M0313	old() outside an allowed context	Use in ensures clauses, verification assertions, or ghost blocks
M0314	Ghost var in runtime code	Wrap in ghost { } block
M0316	Local ghost var in contract	Use parameters, result, or actor/module fields in contracts
Division failure	Missing non-zero guard	Add requires divisor != 0; exported actor methods usually need matching entry_requires
Permission failure	Missing reads/modifies	Add required footprint clauses
Invariant failure	Invariant not maintained	Ensure invariant holds at all public boundaries and await points
Counterexample unavailable	Missing VIPER_SERVER / Silicon JAR	Build the verifier bundle or use --check and --viper for frontend/translation debugging

Summary

• Verification checks symbolic inputs, not just sampled test cases
• Ghost state is erased at runtime; use for verification-only tracking
• Spec collections are persistent values - updates return new values and aliasing is allowed
• await havoces shared state; only invariants survive
• await* is atomic unless the async* callee may actually suspend
• Pure functions cannot access state, recurse, or use assertions
• old() refers to method entry, not per-await snapshots
• Always guard division with non-zero preconditions
• Declare reads and modifies for all accessed fields