Skip to main content

Actor Declarations

Actors are the canister-facing services in Sector9. They encapsulate stable canister state, expose shared public methods, and define the boundaries where actor invariants, entry guards, and async interleaving matter.

Basic Syntax​

The core syntax for declaring an actor uses the persistent actor keywords:

persistent actor {
  // fields and methods
}

The persistent keyword makes upgrade persistence explicit. In a persistent actor, ordinary actor fields default to stable storage and survive upgrades when their types are stable; use transient for caches or derived state that should reset. Upgrade compatibility is covered in state persistence.

Anonymous vs Named Actors​

Actors can be declared with or without a name.

Anonymous Actor​

An anonymous actor has no identifier:

actor-basic.sr9
// Basic persistent actor with state and a method
persistent actor {
  var count : Nat = 0;

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

Named Actor​

A named actor includes an identifier after the keywords:

actor-named.sr9
// Named persistent actor
persistent actor Counter {
  var count : Nat = 0;

  invariant count <= 1_000_000;

  public func get() : async Nat
    reads count
    ensures result == count;
  {
    count
  };

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

Names are optional but useful for documentation and debugging. The name appears in error messages and generated artifacts.

Actor Structure​

An actor body contains:

ComponentPurposeExample
FieldsMutable state with varvar count : Nat = 0
InvariantsMethod-boundary properties over stateinvariant count >= 0
Public functionsShared entry points callable externallypublic func get() : async Nat
Private functionsInternal helpersfunc helper() : Nat

Complete Example​

actor-with-invariant.sr9
// Actor with invariant ensuring balance never goes negative
persistent actor Bank {
  var balance : Int = 0;

  invariant balance >= 0;

  public func deposit(amount : Nat) : async ()
    modifies balance
    ensures balance == old(balance) + amount;
  {
    balance += amount;
  };

  public func withdraw(amount : Nat) : async Bool
    modifies balance
    ensures result == (old(balance) >= amount);
    ensures result ==> balance == old(balance) - amount;
    ensures (not result) ==> balance == old(balance);
  {
    if (balance >= amount) {
      balance -= amount;
      true
    } else {
      false
    }
  };
}

Actors vs Modules​

Actors and modules serve different purposes:

AspectModuleActor
StateStatelessMutable state with var
FunctionsSynchronous local functionsShared methods return async T; private helpers can be synchronous
PersistenceNo canister storageOrdinary fields persist across calls and upgrades; transient fields reset on upgrade
VerificationLibrary/type checking and contractsFull contract verification
Use caseLibraries, helpersServices, canisters

Use modules for stateless logic and actors for stateful services:

actor-with-module.sr9
// Actor using a helper module
module Math {
  public func double(n : Nat) : Nat { n * 2 };
};

persistent actor Calculator {
  var storedResult : Nat = 0;

  public func doubleAndStore(n : Nat) : async Nat
    modifies storedResult
    ensures storedResult == n * 2;
  {
    storedResult := Math.double(n);
    storedResult
  };
}

The persistent Keyword​

Sector9 currently defaults to requiring the persistent keyword for stateful actors. This makes persistence explicit and prevents accidental data loss during upgrades.

persistent actor {
  var data : Nat = 0;
  // ...
}

Verification and $Self​

When Sector9 verifies an actor, it models the actor instance as $Self. This appears in:

  • Invariants: The verifier checks that $Inv($Self) holds at method boundaries
  • Permissions: Field access requires acc($Self.field, ...) permissions
  • Error messages: References like $Self.count indicate actor field access

You write contracts using field names directly. The $Self notation appears only in verifier output and error messages.

For public exported methods, use entry_requires for runtime entry guards and matching requires clauses for proof facts. In verification mode, a public actor method with nontrivial logical requires and no entry_requires is rejected.

Common Mistakes​

Non-Shared Constructor Parameters​

Actor classes cannot accept non-serializable parameters:

// Error M0034: shared constructor has non-shared parameter type
actor class Counter(initial : [var Int]) { }

Fix by using shared types (no var, no functions):

actor class Counter(initial : [Int]) { }

Public Fields Must Be Functions​

Actors expose functionality through functions, not direct field access:

// Error M0125: public actor field needs to be a manifest function
persistent actor {
  public let value = 42;  // Wrong
}

Fix by using a function:

persistent actor {
  let value = 42;
  public func getValue() : async Nat { value };  // Correct
}

Await Outside Async Context​

The await keyword only works inside async functions:

// Error M0038: misplaced await
persistent actor {
  let x = try { await someAsyncCall() } catch (_) { 0 };  // Wrong - in actor body
}

Fix by placing await inside an async function:

persistent actor {
  public func init() : async () {
    let x = try { await someAsyncCall() } catch (_) { 0 };  // Correct
  };
}

Summary​

  • Use persistent actor { } to declare canister actors with upgrade-persistent state
  • Named actors (persistent actor Name { }) improve debugging
  • Actors contain fields, invariants, and public/private functions
  • The persistent keyword is required for stateful actors
  • Modules handle stateless logic; actors handle stateful services
  • Public actor members must be shared functions returning async types