Understanding the Pipeline

This guide explains how Sector9 transforms Sector9 source code into verified programs, walking through each stage of the verification pipeline.

Pipeline Overview

Sector9 verification proceeds through four main stages:

Sector9 Source (.sr9, legacy .mo accepted)
       ↓
   [Lowering]
       ↓
MVIR (Sector9 Verification IR)
       ↓
   [MVIR Passes]
       ↓
   Viper Code (.vpr)
       ↓
   [Silicon SMT]
       ↓
Verification Result

Each stage has a specific role:

Stage	Purpose
Lowering	Translate the Sector9 AST to MVIR semantic representation
MVIR Passes	Run 20+ analysis and transformation passes
Viper Generation	Encode MVIR as Viper verification conditions
SMT Solving	Prove or disprove the verification conditions

Stage 1: Lowering (Sector9 to MVIR)

The lowering stage translates Sector9 source code into MVIR (Sector9 Verification Intermediate Representation), a semantic IR designed for verification. The frontend still accepts legacy .mo files, but new verifier examples should use .sr9 unless they intentionally test legacy compatibility.

What Happens

1. Import Resolution - External modules are resolved and translated
2. Contract Collection - requires, ensures, and invariant clauses are extracted
3. Alias Planning - Array and option borrowing strategies are computed
4. Expression Lowering - Sector9 expressions become MVIR expressions
5. Statement Lowering - Control flow is normalized for verification
6. Type Translation - Sector9 types map to verification-friendly encodings

Key Files

The lowering implementation spans several files in src/viper/:

File	Purpose
lower.ml	Main orchestration and entry points
lower_exp.ml	Expression translation
lower_stmt.ml	Statement translation
lower_types.ml	Type translation
contracts.ml	Trusted-contract checks and contract utilities
lower_helpers_async.ml	Async and await* helper lowering
mvir_place.ml	Place and footprint representation

Example Transformation

Given this Sector9 code:

persistent actor Counter {
  var count : Nat = 0;

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

The lowering stage produces MVIR that captures:

• The count field as a heap location
• The modifies count footprint as a permission requirement
• The ensures clause with old(count) as a snapshot reference
• The assignment as a heap write operation

Stage 2: MVIR Passes

The MVIR pipeline runs 20+ transformation passes that prepare the code for Viper encoding. Each pass performs a specific analysis or rewrite.

Pass Execution Order

Passes run in a fixed order with dependencies between them:

1.  Caller ID              - Materialize caller identity requirements when used
2.  Trap Contracts         - Convert `trap` / `runtime:assert` to obligations
3.  Backend Requirements   - Derive Viper prelude requirements
4.  Mutable Record Post    - Fix mutable record postconditions
5.  Mutable Record Alias   - Handle aliasing constraints
6.  Hoist Allocations      - Lift allocations to statement level
7.  Field Distinctness     - Mark field projections as distinct
8.  Wellformedness Check   - Validate MVIR structure
9.  Location Normalization - Canonicalize location expressions
10. Division Guards        - Insert non-zero guards for division
11. Value Post-Processing  - Fix value-based postconditions
12. Contract Access        - Analyze contract field accesses
13. Inline Indices         - Inline index expressions
14. XSeq Freeze Projection - Stabilize projected sequence views
15. Escape Analysis        - Infer reference escapes
16. Effects Analysis       - Infer reads/writes summaries
17. Freeze Indices         - Snapshot index values for `old()`
18. Annotate Calls         - Mark call sites with effects
19. Annotate Await         - Attach await havoc metadata
20. Alias Guard            - Check cross-await alias safety
21. Await Rewriting        - Materialize async interference barriers
22. Init Const Invariants  - Add initialization invariants
23. Array Size Post        - Add array-size preservation posts
24. Actor Invariants       - Strengthen actor invariants
25. Loop Permissions       - Constrain loop permissions
26. Permission Markers     - Insert permission state markers
27. Fold/Unfold Insertion  - Add predicate fold/unfold operations
28. Spec Rewrite           - Resolve specialized spec calls
29. Final Validation       - Check post-pipeline wellformedness

Key Analyses

Three passes perform particularly important analyses:

Escape Analysis (mvir_escape.ml): Determines whether references escape method boundaries. This affects what can be invalidated across await points.

Effects Analysis (mvir_effects.ml): Infers which heap locations each method reads and writes. This validates reads/modifies clauses and drives frame condition generation.

Permission Fold/Unfold (mvir_perm_fold_unfold.ml): Inserts operations to track ownership predicates for mutable records. Uses fixpoint iteration on the control flow graph.

Await Locals (mvir_await_locals.ml) and Await Rewriting (mvir_await.ml): Reject unsafe references that cross suspension points and materialize the interference model described in Await Expressions.

Debugging MVIR Passes

Use --mvir-stage for the two broad snapshots and --dump-pass for a specific pipeline pass:

# MVIR before the pass pipeline
XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --mvir --mvir-stage lowered file.sr9

# MVIR after all passes
XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --mvir --mvir-stage passes file.sr9

# Stop after a specific pass
XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --mvir --dump-pass escape file.sr9

Current dump pass names include backend_reqs, mutrec_post, mutrec_alias, hoist_allocs, field_distinct, wf, locn, contract_div_guard, value_post, contract_access, inline_indices, xseq_freeze_proj, escape, effects, semantic_framing, locn2, freeze_indices, annotate_calls, annotate_await, alias_guard, await, init_const_invariants, array_size_post, actor_invariants, perm_markers, and perm_fold_unfold. The final spec_rewrite and post-pipeline validation run after dumpable passes.

Stage 3: Viper Generation

After MVIR passes complete, the code is encoded as Viper verification conditions.

Viper AST Structure

The generated Viper program contains:

Item	Purpose
Domains	ADT encodings for records, variants, arrays
Fields	Actor state fields
Predicates	Ownership predicates for mutable records
Functions	Pure function translations
Methods	Actor methods with pre/postconditions
Axioms	Type distinctness and collection axioms

Example Output

The increment method above generates Viper like:

method increment($Self: Ref)
  requires $Inv($Self)
  requires acc($Self.count, write)
  ensures $Inv($Self)
  ensures acc($Self.count, write)
  ensures $Self.count == old($Self.count) + 1
{
  $Self.count := $Self.count + 1
  label $Ret
}

predicate $Inv($Self: Ref) {
  true
}

Viewing Generated Viper

Generate Viper code without running verification:

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

Save Viper code during verification:

XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --verify --verify-vpr-out output.vpr file.sr9

Stage 4: SMT Solving (Silicon)

The final stage sends the Viper code to Silicon, which translates it to SMT queries and invokes Z3.

What Happens

1. Sector9 writes the Viper code to a temporary .vpr file
2. Silicon is invoked as a Java process
3. Silicon translates Viper to SMT-LIB format
4. Z3 attempts to prove each verification condition
5. Results are parsed and mapped back to source locations

Silicon Invocation

Sector9 runs Silicon with:

java -Xmx2048m -Xss16m -cp viperserver.jar \
  viper.silicon.SiliconRunner \
  --numberOfParallelVerifiers N \
  --z3Exe /path/to/z3 \
  output.vpr

Key flags:

Flag	Purpose
--numberOfParallelVerifiers	Parallel verification threads
--counterexample mapped	Enable model extraction
--enableMoreCompleteExhale	More precise permission reasoning

Configuration Options

Control SMT behavior with CLI flags:

# Set verification timeout
XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --verify --verify-timeout-ms 60000 file.sr9

# Control parallelism
XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --verify --cores 4 file.sr9

# Enable counterexamples
XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --verify --counterexample file.sr9

Environment variables:

Variable	Purpose
VIPER_SERVER	Override Silicon JAR location
SILICON_FLAGS	Additional Silicon arguments
S9_VIPER_TIMING=1	Print translator/lowering timing counters
S9_VIPER_DISABLE_TRANSITIVE_SLICE=1	Debug-only escape hatch to disable default transitive VPR item slicing while isolating slicer regressions
XDG_CACHE_HOME	Cache directory for prelude files

Prelude and Infrastructure

Sector9 generates a prelude file containing foundational Viper definitions:

Core Domains

Array Domain: Models arrays as indexed heaps with size and distinctness axioms.

Method Token Domain: Tracks method call permissions for async verification.

Collection Domains: Encodes Map, Set, Seq, and Multiset operations.

Prelude Location

The prelude is written to a cached location and imported by generated Viper files:

import "/path/to/sector9-prelude.vpr"

View the prelude with:

find "${XDG_CACHE_HOME:-/tmp/sector9}" -name '*prelude*.vpr' -print

Data Flow Example

Tracing a simple increment through the pipeline:

public func inc(n : Nat) : async Nat
  ensures result == n + 1;
{
  n + 1
}

After Lowering (MVIR):

MethodI("inc", [("n", NatT)], [("$Res", NatT)],
  pres = [],
  posts = [EqCmpE(Result, AddE(LocalVar "n", IntLitE 1))],
  body = Some([ReturnS(AddE(LocalVar "n", IntLitE 1))]))

After MVIR Passes: Effects analysis adds empty read/write sets. No await barriers needed.

After Viper Generation:

method inc($Self: Ref, n: Int) returns ($Res: Int)
  requires $Inv($Self)
  ensures $Inv($Self)
  ensures $Res == n + 1
{
  $Res := n + 1
  goto $Ret
  label $Ret
}

SMT Result: Z3 proves the postcondition holds for all inputs.

Extending the Pipeline

When adding new verification features:

1. Parser/Typing - Add syntax support in mo_frontend/
2. Lowering - Translate to MVIR in lower_exp.ml or lower_stmt.ml
3. MVIR Passes - Add analysis or transformation passes if needed
4. Viper Encoding - Extend mvir_to_viper.ml for new MVIR constructs
5. Tests - Add _sat, _unsat, and _reject tests

See Adding New Tests for test creation guidelines.

Troubleshooting

Viewing Intermediate Outputs

# See MVIR after specific pass
XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --mvir --dump-pass effects file.sr9

# Keep generated Viper files
XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --verify --viper-keep-vpr file.sr9

# Verbose Silicon output
XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --verify --viper-trace file.sr9

Common Issues

Translation fails: Check --check output for type errors. Use --viper to see where translation stops.

Verification timeout: Try --verify-timeout-ms 300000 for complex proofs. Add intermediate assertions to help the solver.

Permission errors: Review reads/modifies clauses. Use --mvir --dump-pass perm_fold_unfold to see permission insertion.

Summary

• Sector9 verification has four stages: Lowering, MVIR Passes, Viper Generation, and SMT Solving
• The MVIR pipeline runs 20+ passes for effect analysis, permission tracking, and code normalization
• Use --mvir --mvir-stage and --mvir --dump-pass to inspect intermediate representations
• Use --viper and --verify-vpr-out to examine generated Viper code
• The prelude provides foundational Viper domains for arrays, tokens, and collections