Test Naming Conventions

Test file names encode the expected verification outcome, enabling automatic pass/fail detection.

Primary Suffixes

Sector9 verification tests use filename suffixes to indicate what outcome the test runner should expect:

Suffix	Expected Outcome	When to Use
_sat	Verification succeeds	Contracts are satisfied by the implementation
_unsat	Verification fails	Contracts cannot be satisfied (intentional failure)
_reject	Type-check rejection	Code violates language rules before verification
_noperm	Permission error	Missing reads/modifies causes framing failure

How It Works

The test runner (test-viper.sh) extracts the suffix from the filename and compares the actual verification result against the expected outcome:

# From test-viper.sh
if [[ "$base_noext" == *_sat ]]; then
    expect_sat=1
elif [[ "$base_noext" == *_unsat ]]; then
    expect_unsat=1
elif [[ "$base_noext" == *_noperm ]]; then
    expect_noperm=1
elif [[ "$base_noext" == *_reject ]] || [[ "$base_noext" == *reject ]]; then
    expect_reject=1
fi

The runner also accepts legacy names that end in reject, but new tests should use the explicit _reject suffix so the expected outcome is obvious in menus, diffs, and golden output.

Suffix Details

_sat - Verification Succeeds

Use this suffix when the implementation correctly satisfies all contracts. The verifier should find no counterexamples.

// requires_basic_sat.mo
persistent actor {
  public func inc(n : Nat) : async Nat
    entry_requires n <= 1000;
    requires n <= 1000;
    ensures result == n + 1;
  {
    n + 1  // Correct: matches postcondition
  };
}

_unsat - Verification Fails

Use this suffix when the implementation intentionally violates a contract. The verifier should report a verification failure.

// requires_basic_unsat.mo
persistent actor {
  public func inc(n : Nat) : async Nat
    entry_requires n <= 1000;
    requires n <= 1000;
    ensures result == n + 2;  // Wrong: off by one
  {
    n + 1  // Returns n+1, but claims n+2
  };
}

_reject - Type-Check Rejection

Use this suffix when the code violates language rules and should be rejected before verification begins. This includes syntax errors, type errors, and invalid use of verification constructs.

// pure_assert_reject.mo
module {
  public pure func bad(x : Nat) : Nat {
    assert x > 0;  // Error: assert not allowed in pure functions
    x
  };
}

_noperm - Permission Error

Use this suffix when code lacks the necessary reads or modifies clauses. The verifier rejects the code due to missing heap permissions.

// variable_index_noperm.mo
persistent actor {
  var arr : [var Nat] = [var 1, 2, 3];

  public func getAt(i : Nat) : async Nat {
    arr[i]  // Error: no bounds check, permission violation
  };
}

Compound Suffixes

For more precise failure classification, combine a failure type with the base suffix:

Compound Suffix	Meaning
_assert_unsat	An assert statement fails verification
_ensures_unsat	A postcondition (ensures) fails verification

These compound suffixes help identify exactly which part of the specification fails.

Naming Pattern

Test files follow this structure:

[descriptive_name]_[compound?]_[outcome].mo

Examples:

• loop_invariant_sat.mo - Loop invariant verified successfully
• array_bounds_unsat.mo - Array bounds check fails
• pure_old_reject.mo - Invalid use of old() in pure function
• nat64_bounds_ensures_unsat.mo - Nat64 postcondition fails

Test File Headers

Each test file includes a header documenting its purpose:

// ============================================================================
// Sector9 Verification Test
// ============================================================================
//
// Test Name: Basic requires/ensures
// Level: level1
// Expected Outcome: SAT
//
// Purpose:
//   Verify basic precondition and postcondition combination.
//
// Why This Should Verify:
//   Simple arithmetic identity under the given precondition.
//
// ============================================================================

Distribution

The distribution changes as new coverage is added. To compute the current counts from the repository:

find test/viper -maxdepth 2 -type f \( -name '*.mo' -o -name '*.sr9' \) \
  | sed 's#.*/##' \
  | awk '
    /_sat\.(mo|sr9)$/ {sat++}
    /_unsat\.(mo|sr9)$/ {unsat++}
    /_reject\.(mo|sr9)$/ {reject++}
    /_noperm\.(mo|sr9)$/ {noperm++}
    END {print "sat=" sat, "unsat=" unsat, "reject=" reject, "noperm=" noperm}
  '

At the time this page was audited, test/viper contained 1701 _sat tests, 963 _unsat tests, 348 _reject tests, and 11 _noperm tests.

This distribution gives the suite broad coverage of both passing and failing cases. Re-run the command above when you need current numbers for a report or release note.

To inspect one test directly, use the verifier command from the repository root:

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

For batch runs and accepted golden updates, see golden files and verification flags.

Summary

• Use _sat for tests that should verify successfully
• Use _unsat for tests with intentional contract violations
• Use _reject for tests with language/type errors
• Use _noperm for tests with missing permissions
• Use compound suffixes (_assert_unsat, _ensures_unsat) for precise failure location
• The test runner automatically validates outcomes based on filename suffixes