Viper Output (--viper)

Emit Viper code for manual inspection, debugging, or understanding how Sector9 translates contracts and permissions.

The --viper flag runs the translation pipeline and outputs the intermediate Viper representation to stdout without invoking the SMT solver. This is the same Viper program shape that --verify sends to Silicon.

Basic Usage

sector9 --viper file.sr9

Output goes to stdout. Redirect to a file for inspection:

sector9 --viper file.sr9 > output.vpr

When to Use --viper

Use --viper when you need to:

1. Debug verification failures - Understand how your contracts are encoded
2. Inspect quantifier triggers - See what triggers were inferred or applied
3. Learn the translation - Study how Sector9 constructs map to Viper primitives
4. Test Viper edits directly - Modify generated code and test hypotheses
5. Diagnose permission issues - See how reads/modifies become acc(...) permissions

Example

Given this Sector9 source:

persistent actor ArithmeticAdd {
  public func add(a : Int, b : Int) : async Int
    ensures result == a + b;
  {
    a + b
  };
}

Running sector9 --viper add.sr9 produces Viper code including:

method add($Self: Ref, a: Int, b: Int) returns ($Res: Int)
     requires $Inv($Self)
     ensures ($Inv($Self) && ($Res == (a + b)))
     {
       $Res := (a + b);
       goto $Ret;
       label $Ret;
       $expire_borrows(2);
     }

Key observations:

• result becomes $Res in the postcondition
• The actor invariant $Inv($Self) is required and ensured
• The async method becomes a synchronous Viper method
• Control flow uses labels and gotos

Output Structure

The generated .vpr file has these sections:

1. Prelude Import

import "/tmp/sector9/sector9/prelude.vpr"

The prelude contains array encoding, method tokens, numeric bounds helpers, and definitions shared across verification programs.

2. Per-File Definitions

Type-specific field declarations and array initialization methods:

field $array$int: Int
field $array$nat: Int

method $Array_init$nat($n: Int) returns ($arr: Array)
  requires $n >= 0
  ensures $size($arr) == $n
  ensures $array_acc($arr, $array$nat, write)
  ensures $nat_array_bounds($arr)

3. Imported Modules

Methods and functions from imported modules:

/* --- Imported Modules --- */
method $alloc_actor() returns ($r: Ref)
     ensures (($r != null) && true)

4. Spec Functions

Pure functions translated as Viper functions (prefixed with $spec$):

/* --- Spec Functions --- */
function $spec$Math$square(p$x: Int): Int
{
  (p$x * p$x)
}

5. Async Infrastructure

Future payload domains encoding async return values:

/* --- Async Infrastructure --- */
domain $FuturePayload {
  function $Consumed(): $FuturePayload
  function $F_add($F_add$0: Int, ...): $FuturePayload
  // Discriminators, destructors, and axioms
}

6. Actor

Methods, fields, invariants, and predicates:

/* --- Actor --- */
field fld$count: Int

method increment($Self: Ref)
     requires $Inv($Self)
     ensures $Inv($Self)
     { ... }

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

--viper vs --verify

Aspect	--viper	--verify
Translation	Yes	Yes
SMT solving	No	Yes
Output	Viper code to stdout	Verification result
Speed	Fast	Slower (depends on proof)
Use case	Debugging, learning	Pre-deployment validation

Related Flags

With --verify

When using --verify, you can save the intermediate Viper:

# Save Viper while verifying
sector9 --verify --verify-vpr-out output.vpr file.sr9

# Keep Viper files even on success (normally deleted)
sector9 --verify --viper-keep-vpr file.sr9

Integer Modes

The --int-mode flag affects the current Viper verification encoding. Use checked; the Viper lane rejects bitvec and unchecked today.

# Checked fixed-width arithmetic encoding (the verified lane)
sector9 --viper --int-mode checked file.sr9

Other Useful Flags

# Suppress warnings in output
sector9 --viper --hide-warnings file.sr9

# Ensure deterministic output (for diffing)
sector9 --viper --deterministic file.sr9

Debugging Workflow

When verification fails with --verify, use --viper to investigate:

# 1. Verification fails
sector9 --package core ./core/src --verify my_actor.sr9
# Error: Postcondition might not hold

# 2. Generate Viper to inspect
sector9 --package core ./core/src --viper my_actor.sr9 > debug.vpr

# 3. Examine the encoding
# - Check how your contract was translated
# - Look for permission issues (acc(...))
# - Inspect quantifier triggers

# 4. Optionally test Viper edits directly
./scripts/verify-vpr.sh debug.vpr

scripts/verify-vpr.sh runs raw Silicon with one verifier worker by default. Use VERIFY_VPR_PARALLEL_VERIFIERS=N only when you are deliberately comparing Silicon worker counts; for repeatable generated-VPR baselines, keep the default and parallelize multiple files outside the helper.

What to Look For in Viper Output

Contracts

• requires becomes method preconditions
• ensures becomes method postconditions
• result becomes $Res in postconditions
• old(...) becomes a snapshot expression captured at method entry or at the relevant labeled point

Fields and Permissions

• modifies x generates acc(($Self).fld$x, write) permission
• reads x generates acc(($Self).fld$x, wildcard) permission
• Actor invariants become $Inv($Self) predicates
• Mutable records introduce generated Owned$MutRec$... predicates; see mutable record ownership.

Quantifiers

forall i: Int :: {arr[i]} 0 <= i && i < len ==> arr[i] >= 0
           ^^^^^^^^^^^^^
           This is the trigger

Triggers guide SMT solver instantiation. Missing or bad triggers cause performance issues.

Collections

• Map<K, V> becomes Map[K, V]
• Set<T> becomes Set[T]
• Seq<T> becomes Seq[T]

Operations lower into Viper collection operations such as map lookup, set membership, sequence length, and multiset cardinality. Use the emitted .vpr to inspect the exact encoding for a proof.

Exit Codes

Code	Meaning
0	Translation succeeded, Viper emitted
1	Translation failed (type errors, unsupported features)
2	Invalid arguments

Troubleshooting

Output is empty or minimal

Run --check first for source, import, and type errors. Translation only runs on well-formed programs.

"Unsupported" errors

Some inherited or advanced Sector9 constructs are not yet supported for verification. Check the current limitations documentation.

Determinism issues

If the same file produces different Viper output on different runs, use --deterministic:

sector9 --viper --deterministic file.sr9 > a.vpr
sector9 --viper --deterministic file.sr9 > b.vpr
diff a.vpr b.vpr  # Should be identical

Summary

• --viper outputs the Viper intermediate representation without verifying
• Useful for debugging verification failures and understanding the translation
• Combine with --verify-vpr-out to save Viper during verification
• The output shows how contracts, fields, and collections are encoded
• Use this to diagnose permission issues, quantifier triggers, and encoding problems