Project Structure

Organizing Sector9 projects: file extensions, module layout, and test organization.

File Extensions

Sector9 uses two file extensions for source code:

Extension	Description
.sr9	Canonical Sector9 source file (preferred)
.mo	Legacy Motoko extension (still supported)

Both extensions feed the same parser and verifier. New projects should use .sr9; .mo remains a legacy-compatible suffix. Import resolution prefers .sr9 when both suffixes are present.

Modules vs Actors

Sector9 distinguishes between modules (stateless logic) and actors (stateful entry points):

Module Files

Modules contain reusable logic, types, and helper functions. They should keep runtime state out unless that state is intentionally owned by an actor or another verified root:

math.sr9

// math.sr9 - Reusable stateless logic.

module {
  public func double(n : Nat) : Nat
    ensures result == n * 2;
  {
    n * 2
  };
}

Actor Files

Actors are persistent entry points with mutable state:

counter.sr9

// counter.sr9 - Actor using a local module.

import Math "./math";

persistent actor Counter {
  var count : Nat = 0;

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

  public func doubled() : async Nat
    reads count
    ensures result == count * 2;
  {
    Math.double(count)
  };
}

When to use which:

• Use modules for reusable logic, types, and pure functions
• Use actors for stateful services with public entry points

Import Syntax

Sector9 supports local and system imports:

// Local imports (relative path, no extension)
import Math "./math";
import Types "./types";

// Selective imports
import { double; triple } "./math";

// Core library imports
import Debug "mo:core/Debug";
import Nat "mo:core/Nat";

Imports must appear at the top of the file before any definitions.

Recommended Layout

A typical Sector9 project follows this structure:

my-project/
├── src/
│   ├── main.sr9          # Main actor (entry point)
│   ├── types.sr9         # Shared type definitions
│   ├── lib/
│   │   ├── math.sr9      # Math utilities
│   │   └── utils.sr9     # General helpers
│   └── modules/
│       ├── pool.sr9      # Business logic module
│       └── logs.sr9      # Logging module
├── test/
│   ├── math_sat.sr9      # Tests that should verify
│   ├── math_unsat.sr9    # Tests that should fail
│   └── ok/               # Golden output files
└── dfx.json              # Project configuration

Test File Naming

In this repository, verifier tests encode their expected outcome in the filename suffix:

Suffix	Meaning	Example
_sat	Verification succeeds	increment_sat.sr9
_unsat	Verification fails (intentional)	overflow_unsat.sr9
_assert_unsat	An assert fails	bounds_assert_unsat.sr9
_ensures_unsat	A postcondition fails	contract_ensures_unsat.sr9
_reject	Type-check rejection	invalid_syntax_reject.sr9

These suffixes allow repo test runners to automatically validate expected outcomes. Application projects can use the same convention, but it is not required by the compiler.

Golden Files

Repo test directories include an ok/ subdirectory containing expected outputs:

test/
├── increment_sat.sr9
├── increment_unsat.sr9
└── ok/
    ├── increment_sat.vpr           # Generated Viper code
    ├── increment_sat.vpr.stderr    # Translation diagnostics
    ├── increment_sat.silicon       # Verification result (JSON)
    └── increment_sat.silicon.ret   # Exit code

Golden files serve as compiler regression tests. When verifier behavior intentionally changes in this repository, maintainers run ./update_goldens.sh test/path/file.sr9 to accept new outputs.

Multi-File Projects

Larger projects separate concerns across files:

types.sr9

// types.sr9 - Shared type definitions.

module {
  public type Balance = Nat;
  public type TransferResult = { remaining : Balance };
}

pool.sr9

// pool.sr9 - Business logic over shared types.

import T "./types";

module {
  public func transfer(from : T.Balance, amount : Nat) : T.TransferResult
    requires amount <= from;
    ensures result.remaining == from - amount;
  {
    { remaining = from - amount }
  };
}

main.sr9

// main.sr9 - Actor state delegates arithmetic to modules.

import T "./types";
import Pool "./pool";

persistent actor TokenService {
  var balance : T.Balance = 0;

  public func withdraw(amount : Nat) : async Nat
    modifies balance
    entry_requires amount <= balance;
    requires amount <= balance;
    ensures balance == old(balance) - amount;
    ensures result == balance;
  {
    let next = Pool.transfer(balance, amount);
    balance := next.remaining;
    balance
  };
}

This pattern enables:

• Separation of concerns: Logic vs. state vs. types
• Code reuse: Multiple actors can import the same modules
• Independent verification: Standalone modules can be verified as runtime-capable roots, while imported callers reason from their written contracts

Interface and Implementation Separation

For complex modules, separate interface definitions from implementations:

// pool_interface.sr9 - Types only
module {
  public type Pool = { reserveX : Nat; reserveY : Nat };
  public type SwapResult = { amountOut : Nat; newPool : Pool };
}

// pool_impl.sr9 - Implementation
import I "./pool_interface";

module {
  public func swap(pool : I.Pool, amountIn : Nat) : I.SwapResult
    requires amountIn > 0;
    ensures result.amountOut > 0;
  {
    // Implementation
  };
}

Version Patterns

When evolving data structures, use versioned modules:

// memory_v1.sr9
module {
  public type State = { count : Nat };
}

// memory_v2.sr9
module {
  public type State = { count : Nat; lastUpdate : Nat };

  public func migrate(old : V1.State) : State {
    { count = old.count; lastUpdate = 0 }
  };
}

This allows smooth upgrades while maintaining verification contracts.

Summary

• Use .sr9 extension for new files (.mo still works for compatibility)
• Modules contain stateless logic; actors contain stateful entry points
• Imports use relative paths without file extensions
• Repo test suffixes (_sat, _unsat, _reject) encode expected outcomes
• Golden files in repo ok/ directories provide compiler regression testing
• Separate interfaces from implementations for complex modules, and write contracts on exported APIs that callers should rely on