Viper Encoding Reference

This reference documents how Sector9 language constructs are translated to Viper for formal verification. Sector9 is derived from Motoko, so many inherited constructs look familiar, but the verified source language is Sector9. Understanding this encoding helps when debugging verification failures or interpreting Viper output.

Translation Pipeline Overview

Sector9 translates Sector9 source to Viper through a multi-stage pipeline:

Sector9 AST → MVIR (Verification IR) → Viper AST → Silicon Backend

The key stages are:

Lowering: The Sector9 AST is lowered to MVIR, extracting contracts and computing effects
MVIR Pipeline: 20+ analysis passes refine the IR (escape analysis, effects, permissions)
Encoding: MVIR is encoded as Viper syntax
Verification: Silicon (the Viper backend) checks the Viper program

You can inspect the generated Viper code using --viper:

XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --viper myfile.sr9 > output.vpr

Type Encoding

Primitive Types

Sector9 numeric types map to Viper's unbounded Int. Type-specific bounds are enforced through contracts.

Sector9 Type	Viper Type	Notes
`Bool`	`Bool`	Native boolean
`Nat`	`Int`	Non-negative enforced via `>= 0`
`Int`	`Int`	Unbounded integer
`Nat8`..`Nat64`	`Int`	Bounds enforced via axioms
`Int8`..`Int64`	`Int`	Bounds enforced via axioms
`Text`	`Int`	Uninterpreted (opaque)
`Char`	`Int`	Uninterpreted
`Blob`	`Int`	Uninterpreted
`Principal`	`Int`	Uninterpreted
`Float`	`Float`	Uninterpreted (opaque domain)

For fixed-width types, constants like $max_nat8 and $min_int64 are available in contracts.

Composite Types

Arrays become Viper's Array type with element access via location functions:

// Sector9
arr[i]

// Viper encoding
($loc(arr, i)).$array$nat

The $loc function returns a heap reference, and $array$nat is the typed field for array elements.

Tuples map to Viper tuple types with projection functions:

// Sector9
let (x, y) = pair;

// Viper encoding
$tuple_prj_2_0(pair)  // First element
$tuple_prj_2_1(pair)  // Second element

Options become Viper's Option[T] with standard Some/None constructors.

Records (immutable) become Viper ADT domains:

// Sector9
type Point = { x: Nat; y: Nat };

// Viper encoding
domain anonRecord$abc123 {
  function $anonRecord$abc123$x(r: anonRecord$abc123): Int
  function $anonRecord$abc123$y(r: anonRecord$abc123): Int
  // Constructor and accessor axioms
}

Mutable records are encoded as heap references with ownership predicates:

// Sector9
type Token = { id: Nat; var owner: Text };

// Viper encoding
field MutRec$hash$id: Int
field MutRec$hash$owner: Int

predicate Owned$MutRec$hash(r: Ref) {
  acc(r.MutRec$hash$id) && acc(r.MutRec$hash$owner)
}

Variants become ADT domains with discriminant functions:

// Sector9
type Status = { #ok : Nat; #error : Text };

// Viper encoding
domain anonVariant$def456 {
  function $anonVariant$def456$ok(v: Int): anonVariant$def456
  function $anonVariant$def456$error(v: Int): anonVariant$def456
  function $tag$anonVariant$def456(v: anonVariant$def456): Int

  axiom { forall x: Int :: $tag$...$ok(x) == 0 }
  axiom { forall x: Int :: $tag$...$error(x) == 1 }
}

Pattern matching compiles to tag-based conditionals.

Spec Collections

Spec collections map directly to Viper's built-in collection types:

Sector9 Type	Viper Type
`Seq<T>`	`Seq[T]`
`Set<T>`	`Set[T]`
`Map<K, V>`	`Map[K, V]`
`Multiset<T>`	`Multiset[T]`

Element types must be spec-immutable (no var fields or mutable arrays). Opaque/token handles are allowed by identity; the collection stores the handle, not a snapshot of the owner payload. Core-library snapshot bridges such as BMap.entries, MBMap.entries, and BSeq.toArray / BSeq.toList / BSeq.freeze preserve that identity-only boundary for handle elements.

Contract Encoding

Requires and Ensures

Contracts translate directly to Viper preconditions and postconditions:

// Sector9
public func add(x: Nat, y: Nat): Nat
  requires x + y <= 1000;
  ensures result == x + y;
{ x + y }

// Viper encoding
method add($Self: Ref, x: Int, y: Int) returns ($Res: Int)
  requires $Inv($Self) && (x >= 0) && (y >= 0) && (x + y <= 1000)
  ensures $Inv($Self) && ($Res >= 0) && ($Res == x + y)

Key encoding details:

result becomes $Res (the return variable)
Nat types gain >= 0 constraints
Actor invariant $Inv($Self) is injected automatically

Assertions

The three assertion types have different encodings:

Sector9	Viper Encoding	Semantics
`assert E`	`assert E`	Verification obligation
`runtime:assert E`	`assert E` + runtime trap	Checked at both levels
`trap E`	`assert !E`	Trap when E is true

Old Expressions

The old() expression captures values at method entry:

// Sector9
ensures balance == old(balance) + amount

// Viper encoding
ensures ($Self).fld$balance == old(($Self).fld$balance) + amount

When actor invariants are present, old() is wrapped with unfolding to ensure permission:

ensures ($Self).fld$balance ==
        old(unfolding $Inv($Self) in ($Self).fld$balance) + amount

Quantifiers

Quantifiers translate with explicit triggers for SMT instantiation:

// Sector9
assert forall<Nat>(pure func (i : Nat) : Bool = (i < n) ==> (arr[i] >= 0))

// Viper encoding
assert (forall i: Int :: {($loc(arr, i)).$array$nat}
         (i >= 0) ==> ((i < n) ==> (($loc(arr, i)).$array$nat >= 0)))

The {...} syntax specifies triggers that guide quantifier instantiation.

Actor Encoding

Actor Structure

Actors become Viper methods operating on a $Self: Ref parameter:

// Sector9
persistent actor Counter {
  var count: Nat = 0;

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

// Viper encoding
field fld$count: Int

predicate $Inv($Self: Ref) {
  acc(($Self).fld$count, write) && ($Self).fld$count >= 0
}

method __init__($Self: Ref)
  requires acc(($Self).fld$count, write)
  ensures $Inv($Self)
{
  ($Self).fld$count := 0;
  fold $Inv($Self);
}

method increment($Self: Ref)
  requires $Inv($Self)
  ensures $Inv($Self)
  ensures unfolding $Inv($Self) in
          ($Self).fld$count == old(unfolding $Inv($Self) in ($Self).fld$count) + 1
{
  unfold $Inv($Self);
  ($Self).fld$count := ($Self).fld$count + 1;
  fold $Inv($Self);
}

Field Access

Actor fields are prefixed with fld$ and accessed through $Self:

Sector9	Viper
`count` (read)	`($Self).fld$count`
`count := x`	`($Self).fld$count := x`

Actor Invariants

Actor-level invariant declarations become Viper predicates:

// Sector9
invariant balance >= 0;

// Viper encoding
predicate $Inv($Self: Ref) {
  acc(($Self).fld$balance, write) && ($Self).fld$balance >= 0
}

The invariant is:

Required at method entry (requires $Inv($Self))
Ensured at method exit (ensures $Inv($Self))
Unfolded to access fields, refolded before returns

Async and Await Encoding

Async Methods

Async methods are encoded as synchronous Viper methods. Futures are modeled through a domain:

domain $FuturePayload {
  function $Consumed(): $FuturePayload
  function $F_increment(): $FuturePayload
  function $F_getCount(): $FuturePayload
  // Exhaustiveness and exclusivity axioms
}

Await Boundaries

At await points, the verifier models potential interference from concurrent execution:

Actor invariant is unfolded
Shared state locations are havoc'd (assigned unknown values)
Actor invariant is re-assumed
Verification continues with weaker knowledge about state

// Before await
unfold $Inv($Self);
// Havoc shared state
havoc ($Self).fld$count;  // May have changed
// After await
inhale $Inv($Self);  // Assume invariant still holds

Local variables that don't escape are preserved across await.

Permission Model

Read vs Write Permissions

Sector9 uses Viper's permission model with two levels:

Permission	Viper Syntax	Meaning
Write	`acc(field, write)`	Exclusive access
Read	`acc(field, wildcard)`	Shared read access

Footprint Clauses

The reads and modifies clauses control permissions:

// Sector9
public func transfer(amount: Nat)
  reads balance
  modifies balance

// Viper encoding
method transfer($Self: Ref, amount: Int)
  requires acc(($Self).fld$balance, write)  // From modifies
  ensures acc(($Self).fld$balance, write)

Frame Conditions

Fields not in modifies generate frame postconditions:

// Sector9
modifies x  // y is not modified

// Viper encoding
ensures ($Self).fld$y == old(($Self).fld$y)  // y unchanged

Loop Encoding

Loop Invariants

Loop invariants translate with permission tracking:

// Sector9
while (i < n) {
  loop:invariant i >= 0 and i <= n;
  loop:invariant sum == old(sum) + i;
  // body
}

// Viper encoding
while (i < n)
  invariant acc(($Self).fld$sum, write)
  invariant (i >= 0) && (i <= n)
  invariant ($Self).fld$sum == old(($Self).fld$sum) + i
{
  // body
}

Ghost State Encoding

Ghost Variables

Ghost variables exist only in verification:

// Sector9
ghost var history: Seq<Nat> = Seq.empty<Nat>();

// Viper encoding
field fld$history: Seq[Int]
// Treated identically to runtime fields in Viper
// But erased from compiled output

Ghost Blocks

Ghost blocks update ghost state:

// Sector9
ghost {
  history := Seq.append(history, amount);
}

// Viper encoding
($Self).fld$history := Seq_append(($Self).fld$history, Seq_singleton(amount));

Common Encoding Patterns

Natural Number Bounds

Nat types gain non-negativity constraints:

requires (n >= 0)  // Nat parameter
ensures ($Res >= 0)  // Nat result

Array Bounds

Array access includes bounds axioms:

requires $array_acc(arr, $array$nat, write)
requires $nat_array_bounds(arr)  // All elements >= 0
requires i >= 0 && i < $size(arr)

Option Handling

Option operations use pattern matching:

// Checking Some
is_some(opt)

// Extracting value (after Some check)
get_some(opt)

Inspecting Generated Viper

To debug verification failures:

Generate Viper: XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --viper file.sr9 > file.vpr
Look for the failing method
Check preconditions are sufficient
Verify loop invariants are inductive
Ensure permissions are available for heap access

The test directory contains many examples of Sector9 source files and their Viper encodings:

test/viper/level1/ - Basic contracts and arithmetic
test/viper/level3/ - Actor invariants
test/viper/level7/ - Loops with invariants
test/viper/quantifiers/ - Quantified assertions

Each .mo file has a corresponding ok/*.vpr file showing the generated Viper.

Summary

Types: Primitives become Int/Bool, composites become ADT domains or heap references
Contracts: requires/ensures map directly; result becomes $Res
Actors: Become methods with $Self: Ref and $Inv predicate for invariants
Async: Await boundaries havoc shared state; local variables preserved
Permissions: reads/modifies control heap access permissions
Loops: Invariants must include permissions and be inductive
Ghost: Encoded identically but erased from runtime

Translation Pipeline Overview​

Type Encoding​

Primitive Types​

Composite Types​

Spec Collections​

Contract Encoding​

Requires and Ensures​

Assertions​

Old Expressions​

Quantifiers​

Actor Encoding​

Actor Structure​

Field Access​

Actor Invariants​

Async and Await Encoding​

Async Methods​

Await Boundaries​

Permission Model​

Read vs Write Permissions​

Footprint Clauses​

Frame Conditions​

Loop Encoding​

Loop Invariants​

Ghost State Encoding​

Ghost Variables​

Ghost Blocks​

Common Encoding Patterns​

Natural Number Bounds​

Array Bounds​

Option Handling​

Inspecting Generated Viper​

Summary​