Orthogonal Persistence

Actor state automatically persists across committed update calls, and stable fields persist across upgrades, without explicit save/load code.

For verification, persistence has to be separated from knowledge. A field may persist at runtime, but after a suspending await the verifier cannot assume its exact old value unless an invariant, frame condition, or local snapshot justifies that fact.

What is Orthogonal Persistence?

Orthogonal persistence means that an actor's state is automatically preserved without requiring explicit database operations, serialization code, or manual save/load logic. The term "orthogonal" indicates that persistence is independent of other program concerns.

When you declare a field in a persistent actor, that field's value survives:

Every update method call that reaches a commit point
Canister upgrades when the field has a stable type
System restarts and replica changes on the Internet Computer

This eliminates an entire class of bugs related to forgetting to save state or incorrectly deserializing it.

Basic Example

persistence-basic.sr9
// Basic orthogonal persistence - state survives across method calls
persistent actor {
  var counter : Nat = 0;

  invariant counter >= 0;

  // Each call increments the counter; the value persists between calls
  public func increment() : async Nat
    modifies counter
    ensures counter == old(counter) + 1;
    ensures result == counter;
  {
    counter += 1;
    counter
  };

  // Query the current value - reads persistent state
  public query func get() : async Nat
    reads counter
    ensures result == counter;
  {
    counter
  };
}

Each call to increment() increases the counter. The next call sees the incremented value because state persists automatically. No database writes or explicit saving are required.

No Manual Serialization

Traditional systems require explicit save/load operations:

// Traditional approach (pseudocode - NOT Sector9)
func updateCounter() {
  counter := database.read("counter");
  counter += 1;
  database.write("counter", counter);
}

With orthogonal persistence, you simply declare and use the field:

persistence-no-manual.sr9
// Traditional databases vs Orthogonal persistence comparison
//
// Traditional approach (pseudocode - NOT valid Sector9):
//   func save() { database.write("counter", counter); }
//   func load() { counter := database.read("counter"); }
//
// With orthogonal persistence: just declare the field

persistent actor {
  // Automatically persisted - no save() or load() needed
  var counter : Nat = 0;
  var history : [Nat] = [];
  var lastUpdated : Nat = 0;

  // All these fields persist across:
  // - Every method call
  // - Canister upgrades (if stable)
  // - System restarts

  public func update(value : Nat) : async ()
    modifies counter, lastUpdated
    ensures counter == value;
  {
    counter := value;
    lastUpdated := lastUpdated + 1;
  };
}

All three fields (counter, history, lastUpdated) persist automatically. The runtime handles all serialization and storage internally.

How Persistence Works

The Internet Computer provides orthogonal persistence through its execution model:

Event	State Behavior
Method call completes	All field changes persist
Query call	Normally read-only; query-execution-local writes require `modifies` but should not be treated as durable update state
`await` expression	State commits before suspension (see commit points)
Suspending `await*`	Commits only if the continued computation may reach a real `await`
Trap before commit	All tentative changes roll back
Canister upgrade	Stable fields preserved; transient fields reset

The key insight is that actor memory is the source of truth. There is no separate database layer to synchronize.

Do not read this as "every write is immediately final." Sector9 follows the IC commit model: changes before a commit point survive later traps, while changes since the last commit roll back if the current message traps. The detailed rules are in Commit Points.

Persistence and Verification

Sector9 verifies properties about persistent state using contracts and invariants:

persistence-invariant-protects.sr9
// Actor invariants protect persistent state across async boundaries
persistent actor {
  var balance : Nat = 100;

  // This invariant is guaranteed at all public method boundaries
  // and is re-assumed after every await
  invariant balance >= 10;

  public func withdraw(amount : Nat) : async Bool
    modifies balance
    entry_requires amount + 10 <= balance;  // Ensures balance stays >= 10
    requires amount + 10 <= balance;
    ensures result == true;
    ensures balance == old(balance) - amount;
  {
    balance -= amount;
    true
  };

  public func asyncOperation() : async ()
    modifies balance
    ensures balance >= 10;
  {
    // Before await: prove invariant holds
    let _snapshot = balance;

    try { await otherCanister(); } catch (_) {};

    // After await: invariant re-assumed (balance >= 10)
    // But exact value is unknown (could be 10 or 1000)
    assert balance >= 10;
  };

  private func otherCanister() : async () {};
}

Key verification guarantees:

Invariants express properties that hold at all public method boundaries
old() expressions capture field values at method entry
modifies clauses declare which fields a method may change
ensures clauses specify relationships between old and new values

State Across Await Points

When a method contains await, state behavior becomes more nuanced:

persistence-across-await.sr9
// Demonstrating state persistence across await points
persistent actor {
  var total : Nat = 0;

  invariant total >= 0;

  // Helper that performs async work
  private func process(n : Nat) : async Nat
    reads total
    ensures result == n * 2;
  {
    n * 2
  };

  public func accumulate(value : Nat) : async Nat
    modifies total
    ensures result >= 0;
  {
    // State change before await - tentative until commit
    let _before = total;

    // Await is a commit point; state before this persists
    let processed = try { await process(value) } catch (_) { 0 };

    // After await: invariant holds but exact value may differ
    // (other methods could have run during await)
    total += processed;
    total
  };
}

At each suspending boundary (await, or await* whose computation may reach a real await):

Commit: State changes before the await become permanent
Interference: Other methods may execute while awaiting
Resume: Only the actor invariant is guaranteed; exact values may differ

This is why postconditions across suspending await points are often weaker (using >= rather than exact equality). A non-suspending await* stays in the current atomic slice and does not introduce this interference.

Stable fields do not avoid this rule. Stability is about upgrade persistence; await interference is about other messages running before the current method resumes. If you need a fact about stable state after await, express it as an actor invariant or re-check it after the await.

Comparison with Databases

Aspect	Traditional Database	Orthogonal Persistence
State location	External storage	Actor memory
Save operations	Explicit writes	Automatic
Load operations	Explicit reads	Automatic
Consistency	Manual transaction logic	Guaranteed by runtime
Failure handling	Rollback code needed	Automatic rollback on trap
Upgrade migration	Schema migration scripts	Type-compatible upgrades

When State Persists

State changes become permanent at commit points:

await expressions
await* expressions whose async* computation may suspend
return statements (explicit or implicit)
Method exit

Before a commit point, a trap causes all changes to roll back. After a commit point, prior changes survive even if a later trap occurs.

See Commit Points for details.

Persistent vs Non-Persistent Actors

The persistent keyword controls default field behavior:

// All fields default to stable (persist across upgrades)
persistent actor {
  var counter : Nat = 0;          // Implicitly stable
  transient var cache : Nat = 0;  // Explicitly transient
}

// Legacy mode only: fields default to transient
actor {
  stable var counter : Nat = 0;   // Explicitly stable
  var cache : Nat = 0;            // Implicitly transient
}

Using persistent actor is the standard form for production code. Current Sector9 defaults require it for stateful actors; legacy actor defaults are relevant only when compiling in legacy mode. The explicit transient keyword marks fields that should reset on upgrade.

Summary

Orthogonal persistence automatically preserves actor state without explicit save/load code
Committed state survives later method calls and compatible upgrades
persistent actor makes all fields stable by default
Stable does not mean unchanged across await; use invariants or rechecks for post-await facts
Actor invariants express properties that persist across all operations
Commit points determine when changes become permanent
Non-suspending await* does not create an extra commit/interference point
Traps before commit cause rollback; traps after commit do not affect prior commits

Stable variables for upgrade-persistent fields
Upgrade compatibility for safe schema changes
Commit points for when changes become permanent
Actor invariants for persistent state properties

What is Orthogonal Persistence?​

Basic Example​

No Manual Serialization​

How Persistence Works​

Persistence and Verification​

State Across Await Points​

Comparison with Databases​

When State Persists​

Persistent vs Non-Persistent Actors​

Summary​

Related Topics​