Skip to main content

Test Levels

Sector9 organizes verification tests into numbered levels that progress from simple to complex, helping developers understand what verification features are being tested and at what difficulty.

Level System Overview​

Tests in test/viper/ include 23 numbered directories (level1 through level24, with level14 absent). Each level introduces more sophisticated verification concepts, while many newer regression and product tests live in feature directories such as async2, entry_requires, core_*, restrict_*, and bug*.

Level RangeComplexityFocus
1-3FoundationalBasic contracts, modules, invariants
4-7IntermediateLoops, pure functions, control flow
8-13AdvancedPermissions, aliasing, effects
15-24ExpertQuantifiers, collections, protocols

Level Details​

Level 1: Basic Contracts and Arithmetic​

The simplest tests covering fundamental verification concepts.

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

Features tested:

Example files:

  • arithmetic_add_sat.mo - Addition postcondition
  • requires_basic_sat.mo - Simple precondition
  • old_expression_sat.mo - Value snapshots

Level 2: Modules and Actors​

Module system and actor composition.

Features tested:

  • Module imports and exports
  • Actor definitions with contracts
  • Parametric modules (functors)
  • Cross-module verification

Example files:

  • module_and_actor_sat.mo - Module-actor interaction
  • functor_module_sat.mo - Modules as parameters
  • import_chain_actor_sat.mo - Deep import chains

Level 3: Actor Invariants​

State invariants that must hold between method calls.

persistent actor Counter {
  var count : Nat = 0;
  invariant count >= 0;

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

Features tested:

  • Actor-level invariant declarations
  • Invariant preservation across methods
  • Ghost variables at actor scope
  • Recursive data structures

Level 4: Loop Control Flow​

Loop structures with breaks and continues.

Features tested:

Level 5: Higher-Order Functions​

Functions as values and module-level functions.

Features tested:

  • Conditional function assignment
  • Module function references
  • Higher-order patterns
  • Record spread operations

Level 6-7: Framing and Pure Functions​

Heap framing and side-effect-free functions.

Features tested:

Level 8-9: Bounds and Mutable Records​

Fixed-width integer reasoning and mutable record permissions.

Features tested:

Level 10-11: Ghost State and Effects​

Specification-only state and effect inference.

Features tested:

Level 12-13: Escape Analysis​

Tracking which values may alias across operations.

Features tested:

  • Fresh allocation detection
  • Escape through fields
  • Frame inference
  • Variant pattern matching

Level 15-16: Quantifiers​

Universal and existential quantification.

persistent actor ArrayAll {
  public func allPositive(arr : [Int]) : async Bool
    ensures result == forall(func (i : Nat) : Bool {
      i >= arr.size() or arr[i] > 0
    });
  {
    // implementation
  };
}

Features tested:

  • forall over arrays
  • exists with maps
  • Quantified invariants
  • Trigger patterns

Level 17-18: Collections and Async​

Specification collections and async/await verification.

Features tested:

Level 19-20: Protocol Patterns​

Complete protocol implementations.

Features tested:

  • AMM (Automated Market Maker) logic
  • Conservation invariants
  • Factory patterns
  • Nested async loops

Level 21-24: Advanced Features​

Edge cases and specialized verification.

Features tested:

  • Counterexample extraction
  • Lemmas with quantifiers
  • Iterator patterns
  • Complex array operations

Category Directories​

Beyond numbered levels, tests are also organized by feature category. The directory set changes as regressions are added; run find test/viper -maxdepth 1 -type d -printf '%f\n' | sort for the current list.

Directory PatternPurpose
bugs*, bugzcl, bugsfoundRegression tests for fixed issues
async, async2async/await semantics and interference
core_*, core_lemma_*Core library modules and trusted arithmetic lemmas
entry_requires, contractsRuntime entry guards and logical contracts
quantifiers, map, collections, puremapQuantifiers and specification collections
restrict_*, gapsVerified-subset restrictions and known unsupported patterns
performanceTimeout and stress tests

Choosing a Level for New Tests​

When adding tests, place them at the appropriate level:

  1. Start at the lowest level that includes all required features
  2. Check existing tests at that level for similar patterns
  3. Create a test family with _sat, _unsat, and _reject variants

For example, a test using forall over an array belongs in level16, not level1, even if the logic is simple.

Running Tests by Level​

Run all tests at a specific level through the shared test runner from that test directory:

cd test/viper/level1
../../run.sh -v *.mo

Run the default Viper suite from the repository root:

./test-viper.sh

Run the slow Viper lane when the feature needs stress coverage:

./test-viper.sh --slow

For expected outcomes and suffixes, see test naming conventions. For accepted output updates, see golden files.

Summary​

  • Tests are organized into 23 levels (1-24, excluding 14) with increasing complexity
  • Level 1-3: Basic contracts, modules, invariants
  • Level 4-7: Loops, pure functions, control flow
  • Level 8-13: Permissions, aliasing, effect tracking
  • Level 15-24: Quantifiers, collections, full protocols
  • Category directories group tests by feature (bugs, quantifiers, async, etc.)
  • Place new tests at the lowest level that includes all required features