From Dafny/Viper/Other

Mapping verification concepts from Dafny, Viper, and other formal verification systems to Sector9.

If you have experience with Dafny, Viper, or similar verification tools, this guide helps you apply that knowledge to Sector9. The core concepts transfer directly, but syntax and some restrictions differ.

Quick Comparison

Concept	Dafny	Viper	Sector9
Preconditions	requires	requires	requires
Postconditions	ensures	ensures	ensures
Return value	result or func name	result	result
Loop invariants	invariant (outside)	invariant (inside)	loop:invariant (inside)
Ghost variables	ghost var	N/A	ghost var
Pure functions	function	function	pure func
Lemmas	lemma	N/A	lemma
Collections	map<K,V>, set<T>, seq<T>	built-in domains	Map<K,V>, Set<T>, Seq<T>
Universal	forall x :: ...	forall x: T :: ...	forall<T>(pure func (x : T) : Bool = ...)
Existential	exists x :: ...	exists x: T :: ...	exists<T>(pure func (x : T) : Bool = ...)
Frame clauses	modifies, reads	acc() permissions	modifies, reads
Backend	Boogie	Z3 directly	Viper (Silicon)

Contracts: requires and ensures

Contract syntax is nearly identical to Dafny. Place contracts between the function signature and body:

public func divide(a : Int, b : Int) : async Int
  entry_requires b != 0;
  requires b != 0;
  ensures result == a / b;
{
  a / b
};

Key differences from Dafny:

• Contracts appear between signature and body (like Dafny)
• Multiple contracts are AND-ed together (same as Dafny)
• Use result keyword for return value (same as Dafny)

Key differences from Viper:

• Sector9 uses requires/ensures keywords (same as Viper methods)
• No explicit acc() permissions needed for simple field access
• Sector9's modifies/reads clauses abstract over Viper's permission system

For exported actor methods, nontrivial logical requires clauses also need runtime-facing entry_requires guards. Module helpers and private helpers do not use entry_requires.

Loop Invariants

Sector9 places loop invariants inside the loop body using loop:invariant:

public func sum(n : Nat) : async Nat
  ensures result == n * (n + 1) / 2;
{
  var i : Nat = 0;
  var acc : Nat = 0;
  while (i < n) {
    loop:invariant i <= n;
    loop:invariant acc == i * (i + 1) / 2;
    i += 1;
    acc += i;
  };
  acc
};

Dafny syntax places invariants outside:

while i < n
  invariant i <= n
  invariant acc == i * (i + 1) / 2
{
  // body
}

Sector9 syntax places them inside with a prefix:

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

Both express the same inductive reasoning. Sector9's placement is closer to Viper's internal specification style.

Ghost State

Ghost variables work similarly to Dafny but require explicit ghost { } blocks for mutations:

import Runtime "mo:core/Runtime";

persistent actor {
  var balance : Nat = 0;
  ghost var totalDeposits : Nat = 0;

  invariant balance <= totalDeposits;

  public func deposit(amount : Nat) : async ()
    modifies balance, totalDeposits
  {
    balance += amount;
    ghost { totalDeposits := totalDeposits + amount; };
  };
};

Key differences from Dafny:

• Mutations must be wrapped in ghost { } blocks
• Ghost fields must appear in modifies clauses
• Ghost fields may appear in verifier-only contracts, but not in runtime entry_requires guards

Ghost blocks cannot:

• Modify runtime state (balance, arrays, mutable records)
• Appear in pure functions
• Read runtime variables that aren't already in scope

Pure Functions

Sector9's pure func is more restrictive than Dafny's function:

pure func max(a : Int, b : Int) : Int
  ensures result >= a;
  ensures result >= b;
{
  if (a >= b) { a } else { b }
};

Restrictions compared to Dafny:

Capability	Dafny function	Sector9 pure func
Recursion	Allowed	Not allowed
State access	Immutable state allowed	No state access
Array indexing	Allowed	Allowed in supported spec contexts, but mutable array state still needs permissions
Assertions	Not allowed	Not allowed
Use in specs	Yes	Yes

Workaround for recursion: Use trusted pure to make the contract an assumption, or use a lemma/method with an explicit contract:

public pure trusted func factorial(n : Nat) : Nat
  ensures result >= 1;
{
  if (n == 0) { 1 } else { n * factorial(n - 1) }
};

The body is assumed correct but not verified. This expands the trusted base, so keep the contract small and test callers with _sat and _unsat cases.

Quantifiers

Sector9 uses function literal syntax for quantifiers instead of Dafny's :: notation:

Universal quantification:

// Dafny:  forall i: nat :: i < arr.Length ==> arr[i] > 0
// Sector9:
assert forall<Nat>(pure func (i : Nat) : Bool =
  (i < arr.size()) ==> (arr[i] > 0));

Existential quantification:

// Dafny:  exists n: nat :: n == target
// Sector9:
assert exists<Nat>(pure func (n : Nat) : Bool = n == target);

Explicit triggers use forallWith:

// Dafny:  forall i :: {arr[i]} i < n ==> arr[i] > 0
// Sector9:
assert forallWith<Nat>(
  pure func (i : Nat) : Bool = (i < n) ==> (arr[i] > 0),
  [pure func (i : Nat) : Bool = arr[i]]
);

Multiple triggers:

assert forallWith<Nat>(
  pure func (i : Nat) : Bool = (i < a.size() and i < b.size()) ==> (a[i] == b[i]),
  [
    pure func (i : Nat) : Bool = a[i],
    pure func (i : Nat) : Bool = b[i]
  ]
);

Spec Collections

Sector9 has direct equivalents to Dafny's built-in collection types:

Map

// Dafny: var m: map<nat, int> := map[]; m := m[1 := 100];
// Sector9:
let m0 : Map<Nat, Int> = Map.empty();
let m1 = Map.update(m0, 1, 100);
assert Map.get(m1, 1) == 100;
assert Map.contains(1, m1);

Set

// Dafny: var s: set<nat> := {42}; assert 42 in s;
// Sector9:
let s = Set.singleton<Nat>(42);
assert Set.contains(42, s);
assert Set.card(s) == 1;

Seq

// Dafny: var s: seq<nat> := [1, 2, 3]; assert s[0] == 1;
// Sector9:
let s = Seq.concat(Seq.singleton<Nat>(1),
        Seq.concat(Seq.singleton<Nat>(2), Seq.singleton<Nat>(3)));
assert Seq.get(s, 0) == 1;
assert Seq.len(s) == 3;

Multiset

// Dafny: var m: multiset<nat> := multiset{1, 1, 2};
// Sector9:
let m = Multiset.union(Multiset.singleton<Nat>(1),
        Multiset.union(Multiset.singleton<Nat>(1), Multiset.singleton<Nat>(2)));
assert Multiset.count(m, 1) == 2;

Key difference: Persistent semantics

Sector9 collections are persistent values. Updates return new values and do not consume inputs:

let m1 = Map.update(m0, 1, 10);
let m2 = Map.update(m0, 2, 20);  // ok: m0 still valid

Read-only operations (get, contains, card, domain) remain pure queries.

Frame Conditions (modifies/reads)

Sector9 uses explicit modifies and reads clauses like Dafny:

persistent actor {
  var balance : Int = 0;
  var owner : Text = "alice";

  public func deposit(amount : Int) : async ()
    modifies balance
    reads owner
    ensures balance == old(balance) + amount;
    ensures owner == old(owner);  // Auto-generated frame condition
  {
    balance += amount;
  };
};

How it maps to Viper:

• modifies grants write permission (Viper: acc(field, write))
• reads grants read permission (Viper: acc(field, wildcard))
• Unlisted fields get automatic frame conditions (proven unchanged)

Key differences from Viper:

• No manual acc() predicates needed
• No fractional permissions - just Read/Write
• No explicit fold/unfold for simple cases

old() Expressions

The old() expression works the same as Dafny - it captures values at method entry:

public func increment() : async ()
  modifies counter
  ensures counter == old(counter) + 1;
{
  counter += 1;
};

Restrictions (same as Dafny):

• Only in ensures clauses, assert statements, and ghost blocks
• Not in requires (no prior state at entry)
• Not in actor invariants (must always hold)

Additional Sector9 restriction:

• Not in pure function contracts (pure functions have no state)

Lemmas

Lemmas work similarly to Dafny - they establish facts for the verifier:

public lemma addCommutes(a : Int, b : Int) : ()
  ensures a + b == b + a;
{
};

public func useCommutes(x : Int, y : Int) : async Int
  ensures result == y + x;
{
  addCommutes(x, y);  // Invoke lemma
  x + y
};

Lemmas can encode recursive proof structure (unlike plain pure func), but they still need contracts strong enough for callers to use.

Trusted Code

Sector9's trusted modifier is similar to using assume in Dafny proofs:

public trusted func externalCall(x : Nat) : Nat
  requires x > 0;
  ensures result > x;
{
  // Body assumed correct, not verified
  x + 1
};

• Contracts are checked at call sites
• Body is not verified (developer claims correctness)
• Use sparingly - expands the trusted base

Use abstract instead when you need a bodyless verifier placeholder rather than an unchecked implementation. abstract and trusted are deliberately separate: abstract functions have no body, while trusted functions are implementation assumptions.

Actor-Specific Features

Sector9 has features for IC actor verification that don't exist in Dafny/Viper:

Actor Invariants

Express properties that hold across all public method calls:

persistent actor {
  var balance : Nat = 0;
  invariant balance >= 0;

  public func withdraw(amount : Nat) : async Bool
    modifies balance
  {
    if (balance >= amount) {
      balance -= amount;
      true
    } else {
      false
    }
  };
};

Invariants are checked at method entry, method exit, and before each await. After an await, Viper assumes the invariant is restored but does not preserve exact actor-field values unless your contracts and frames justify them.

Await Boundaries

Await points model interference from concurrent actors:

public func transfer(amount : Nat) : async ()
  modifies balance
{
  let pre = balance;
  try {
    await otherActor.notify();
  } catch (_) {
    // verified code uses catch-all handlers for awaits
  };
  // After await: balance may have changed
  // Only invariants are guaranteed
  assert balance >= 0;  // Verified via invariant
};

Between awaits, execution is atomic. At await boundaries, shared state can change (any public method may execute).

Principal and Caller

Access control verification using IC principals:

persistent actor {
  var owner : ?Principal = null;

  public shared({caller}) func claimOwnership() : async ()
    modifies owner
    entry_requires owner == null;
    requires owner == null;
    ensures owner == ?caller;
  {
    owner := ?caller;
  };

  public shared({caller}) func adminOnly() : async ()
    reads owner
    entry_requires owner == ?caller;
    requires owner == ?caller;
  {
    // Only owner can call
  };
};

Key Restrictions

No Termination Checking

decreases clauses are not supported:

// REJECTED
public func countdown(n : Nat) : async Nat
  decreases n;  // Error M0335
{
  if (n == 0) { 0 } else { try { await countdown(n - 1) } catch (_) { 0 } }
};

Sector9 proves partial correctness only. Programs are verified assuming they terminate.

No Recursive Pure Functions

Pure functions cannot recurse:

// REJECTED
pure func factorial(n : Nat) : Nat {
  if (n == 0) { 1 } else { n * factorial(n - 1) }  // Error
};

Use lemmas for recursive proofs, or trusted pure for unverified recursion.

Division Guards Required

Division and modulo require explicit non-zero guards:

// WRONG: guard comes after division
public func bad(a : Nat, b : Nat) : async Nat
  requires a / b > 0;  // Error: b may be zero
  requires b != 0;
{ a / b };

// CORRECT: guard first
public func good(a : Nat, b : Nat) : async Nat
  entry_requires b != 0;
  requires b != 0;
  requires a / b > 0;
{ a / b };

Immutable Collection Elements

Spec collections only accept immutable element types:

// REJECTED: mutable record as key
type Key = { var id : Int };
let m : Map<Key, Int> = Map.empty();  // Error

// CORRECT: immutable record
type Key = { id : Int };
let m : Map<Key, Int> = Map.empty();

Not allowed: var fields, mutable arrays, functions, actors.

Concept Mapping Summary

Dafny/Viper Concept	Sector9 Equivalent	Notes
requires P	requires P;	Identical
ensures Q	ensures Q;	Identical
invariant I (loop)	loop:invariant I;	Inside loop body
ghost var x	ghost var x	Use ghost { } for mutations
function f()	pure func f()	More restrictive
lemma L()	public lemma L()	Similar
assume P	trusted func	Body not verified
forall x :: P	forall<T>(pure func (x : T) : Bool = P)	Function literal syntax
exists x :: P	exists<T>(pure func (x : T) : Bool = P)	Function literal syntax
map<K,V>	Map<K, V>	Persistent proof-only value semantics
set<T>	Set<T>	Persistent proof-only value semantics
seq<T>	Seq<T>	Persistent proof-only value semantics
multiset<T>	Multiset<T>	Persistent proof-only value semantics
modifies s	modifies field	Per-field
reads s	reads field	Per-field
old(e)	old(e)	Identical
decreases e	Not supported	No termination proofs
acc(x.f, p)	modifies/reads	Abstracted

Verification Workflow

1. Type check: XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --check file.sr9
2. Verify: XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --verify file.sr9
3. Debug: XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --verify --counterexample file.sr9
4. Inspect Viper: XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --viper file.sr9

Summary

• Contract syntax (requires, ensures, old) is nearly identical to Dafny
• Loop invariants go inside loops with loop:invariant prefix
• Ghost mutations require explicit ghost { } blocks
• Pure functions are more restricted than Dafny's function
• Quantifiers use function literal syntax instead of forall x :: ...
• Collections are persistent values (updates return new values)
• No termination checking (decreases rejected)
• Actor invariants and await boundaries are Sector9-specific