Skip to main content

Adding New Tests

This guide walks through creating verification tests for Sector9, from writing the test file to integrating with the test suite.

Quick Start​

To add a new verification test:

  1. Create a .mo or .sr9 file in an appropriate test/viper/ directory with the expected suffix
  2. Run ./update_goldens.sh test/viper/<dir>/your_test.mo to generate golden files
  3. Run ./test-viper.sh to verify the test passes against suffix expectations and goldens

Test File Location​

Tests are organized by complexity level and feature area:

test/viper/
├── level1/          # Basic: arithmetic, arrays, simple contracts
├── level2/          # Actors, modules, imports
├── level3/          # Actor invariants and recursive data shapes
├── level4/          # Loop control-flow coverage
├── level5/          # Higher-order functions, type aliases
├── level8/          # Fixed-width numerics
├── level16/         # Quantifiers
├── level18/         # Collections, await semantics
├── quantifiers/     # forall, exists, triggers
├── async/           # Async/await verification
├── bugs/            # Regression tests
└── ...

Choose a directory that matches your test's complexity. When in doubt, use the lowest level that includes the features you need.

Naming Your Test​

The filename suffix determines the expected outcome:

SuffixMeaning
_satVerification must succeed
_unsatVerification must fail
_rejectTranslation to Viper must fail
_nopermMust fail with permission error

See Test Naming Conventions for details.

Writing the Test File​

Minimal Structure​

A verification test requires a persistent actor with contracts:

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

Include a header documenting the test purpose:

// ============================================================================
// Sector9 Verification Test
// ============================================================================
//
// Test Name: [Descriptive name]
// Level: [level1, level2, etc.]
// Expected Outcome: [SAT, UNSAT, REJECT]
//
// Purpose:
//   [What this test verifies]
//
// Why This Should [Verify/Fail]:
//   [Brief explanation]
//
// ============================================================================

persistent actor {
  // ... test code
}

Test Configuration​

Control test behavior with inline directives:

// viper-test: verify --cores 1             # Override verification flags for this file
// viper-test: viper --deterministic        # Override Viper generation flags
// viper-test: slow-threshold 60            # Mark as slow only after 60s
// viper-test: serial                       # Avoid parallel suite scheduling

The test runner always performs both translation and verification for normal tests. Inline directives add target-specific flags; they should not include --verify, --viper, --json, --toon, or output-path flags because the runner owns those.

Generating Golden Files​

Golden files capture expected outputs for regression detection.

First-Time Setup​

Generate golden files for a new test:

./update_goldens.sh test/viper/level1/my_new_test_sat.mo

This creates files in test/viper/level1/ok/:

FileContent
my_new_test_sat.vprGenerated Viper code
my_new_test_sat.vpr.stderrTranslator diagnostics
my_new_test_sat.siliconVerification result (JSON)
my_new_test_sat.silicon.retReturn code

Batch Update​

Update all golden files after intentional changes:

./update_goldens.sh

Verify Against Goldens​

Check that outputs match expected values:

./test-viper.sh

Complete Example: SAT Test​

Create test/viper/level1/bounded_increment_sat.mo:

// ============================================================================
// Sector9 Verification Test
// ============================================================================
//
// Test Name: Bounded increment
// Level: level1
// Expected Outcome: SAT
//
// Purpose:
//   Verify increment with upper bound precondition.
//
// Why This Should Verify:
//   Precondition ensures no overflow; postcondition matches implementation.
//
// ============================================================================

persistent actor BoundedIncrement {
  public func inc(n : Nat) : async Nat
    entry_requires n < 1000;
    requires n < 1000;
    ensures result == n + 1;
    ensures result <= 1000;
  {
    n + 1
  };
}

Generate golden files:

./update_goldens.sh test/viper/level1/bounded_increment_sat.mo

Verify:

cd test/viper/level1 && ../../run.sh -v bounded_increment_sat.mo

Complete Example: UNSAT Test​

Create test/viper/level1/bounded_increment_unsat.mo:

// ============================================================================
// Sector9 Verification Test
// ============================================================================
//
// Test Name: Bounded increment (wrong bound)
// Level: level1
// Expected Outcome: UNSAT
//
// Purpose:
//   Demonstrate postcondition failure with wrong bound.
//
// Why This Should Fail:
//   Claims result < 1000, but n=999 produces result=1000.
//
// ============================================================================

persistent actor BoundedIncrementUnsat {
  public func inc(n : Nat) : async Nat
    entry_requires n < 1000;
    requires n < 1000;
    ensures result == n + 1;
    ensures result < 1000;  // Wrong: fails when n = 999
  {
    n + 1
  };
}

Complete Example: REJECT Test​

Create test/viper/level3/pure_old_reject.mo:

// ============================================================================
// Sector9 Verification Test
// ============================================================================
//
// Test Name: Pure function with old (rejected)
// Level: level3
// Expected Outcome: REJECT
//
// Purpose:
//   Verify that old() is rejected in pure function contracts.
//
// Why This Should Be Rejected:
//   Pure functions cannot use old() - they have no state context.
//
// ============================================================================

module {
  var state : Nat = 0;

  public pure func bad(x : Nat) : Nat
    ensures result == old(state);  // Error: old() not allowed in pure
  {
    x
  };
}

Running Individual Tests​

Verification Only​

XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --verify test/viper/level1/my_test_sat.mo

Generate Viper Code​

XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --viper test/viper/level1/my_test_sat.mo > output.vpr

With Counterexamples​

XDG_CACHE_HOME=/tmp/sector9 ./bin/sector9 --verify --counterexample test/viper/level1/my_test_unsat.mo

Counterexample output requires the Silicon/Viper server JAR to be available. If the local VIPER_SERVER path is missing, plain --check and --viper can still help narrow frontend and translation issues.

Test Report​

After running ./test-viper.sh, check test/viper_test.txt for results:

=== level1 ===
✅ [m] bounded_increment_sat.mo - verified OK
✅ [m] bounded_increment_unsat.mo - postcondition might not hold...

Columns:

  • Semantic status: ✅ pass, ❌ fail
  • Golden status: [m] match, [!] mismatch, [ ] missing
  • Filename and outcome summary

Troubleshooting​

Test fails unexpectedly​

  1. Check the suffix matches your intent (_sat vs _unsat)
  2. Run with --counterexample to see failing inputs
  3. Add intermediate assert statements to locate the issue

Golden files out of date​

./update_goldens.sh test/viper/<dir>/your_test.mo

Permission errors​

Ensure reads/modifies clauses cover all accessed fields. See Permission Errors.

Test times out​

Default timeout is 120 seconds. For complex tests:

VERIFY_TIMEOUT_MS=300000 ./test-viper.sh

Best Practices​

  1. One concept per test - Test a single verification feature
  2. Include both SAT and UNSAT variants - Prove both success and failure detection
  3. Use descriptive names - array_bounds_check_sat.mo not test1.mo
  4. Document the test - Headers explain purpose and expected behavior
  5. Keep tests minimal - Smallest code that exercises the feature
  6. Use appropriate level - Match test complexity to directory

Summary​

  • Place tests in the appropriate test/viper/ directory with an expected-outcome suffix
  • Use ./update_goldens.sh to generate expected outputs
  • Run ./test-viper.sh to verify all tests pass
  • Include header comments documenting test purpose
  • Create both _sat and _unsat variants for thorough coverage