Async Functions

Async functions return futures that represent eventual values. All public actor methods must return async types, and private functions can also be async when they need to call or compose asynchronous work.

For verification, the important question is not just "does this return a future?" It is "where can execution suspend and let other messages interleave?" Ordinary await always creates a suspension point. await* creates one only when the continued async* computation may reach a real await.

What is an Async Function?

An async function is a function whose return type is async T for some type T. Calling it produces a future - a placeholder for a value that will be available later. The caller uses await to suspend execution until the future resolves.

// Async function signature
func name(params) : async ReturnType

Async functions enable:

• Non-blocking calls between actors
• Concurrent processing of independent operations
• Composition of asynchronous workflows
• Explicit proof boundaries around suspension and interleaving

Basic Syntax

Declare an async function by specifying async before the return type:

async-basic.sr9

// Basic async function declaration
persistent actor {
  var counter : Int = 0;
  invariant counter >= 0;

  // Private async function
  private func bump() : async ()
    modifies counter
    ensures counter == old(counter) + 1;
  {
    counter += 1;
  };

  // Public async function that awaits another
  public func increment() : async Int
    modifies counter
    ensures result >= 0;
  {
    try { await bump(); } catch (_) {};
    counter
  };
}

Key points:

• Private async functions use private func name() : async T
• Public async functions use public func name() : async T
• The caller observes the result by awaiting the future
• Contracts (modifies, ensures, requires) work the same as synchronous functions, with extra proof obligations around suspending awaits

Async Functions with Return Values

Async functions can return values. The value is delivered when the future completes:

async-return-value.sr9

// Async function returning a value
persistent actor {
  var balance : Nat = 100;

  // Async function with return value and contract
  public func withdraw(amount : Nat) : async Nat
    modifies balance
    entry_requires amount <= balance;
    requires amount <= balance;
    ensures result == old(balance) - amount;
    ensures balance == result;
  {
    balance -= amount;
    balance
  };

  // Async function returning result of computation
  public func getDoubled() : async Nat
    reads balance
    ensures result == balance * 2;
  {
    balance * 2
  };
}

The result keyword in postconditions refers to the returned value, just like in synchronous functions.

Private Async Helpers

Private async functions serve as helpers that can be composed:

async-private-helper.sr9

// Private async helper functions
persistent actor {
  var counter : Int = 0;
  invariant counter >= 0;

  // Private async helper with its own contract
  private func doIncrement() : async ()
    modifies counter
    ensures counter == old(counter) + 1;
  {
    counter += 1;
  };

  // Public function using the helper
  public func incrementTwice() : async Int
    modifies counter
    ensures result >= 0;
  {
    try { await doIncrement(); } catch (_) {};
    try { await doIncrement(); } catch (_) {};
    counter
  };
}

The verifier reasons modularly:

1. Before incrementTwice awaits doIncrement(), it checks that doIncrement's preconditions are satisfied
2. Verified awaits are wrapped in try/catch; the helper's postconditions are available on the success path, while the catch path must provide its own safe fallback
3. This repeats for each await in sequence

Two Async Sorts: async and async*

Sector9 has two kinds of async types:

Sort	Keyword	Await	Use Case
Future	async T	await	Normal async operations
Computation	async* T	await*	Composable async control flow

Regular futures (async T) are used for most async operations. They represent a single pending result from an async call.

await? is not supported by Sector9 verification. Use try/catch around await when you need to handle failures in verified code.

Computations (async* T) package a piece of async control flow so another function can continue through it with await*. They are useful when you want helper functions to preserve the caller's atomic slice unless the helper actually reaches a real suspension point.

async* is not a "skip consensus" marker. Consensus is determined by the enclosing shared call and by whether you are in an update, query, or composite query context. In an update flow, code reached through await* still participates in the update execution; if it reaches an ordinary await, that await is the suspension/commit/interference boundary.

// Regular async function
public func update() : async Nat { 42 };

// Computation helper: no extra await boundary if the helper never awaits
private func computeLocal(n : Nat) : async* Nat {
  n + 1
};

public func run(n : Nat) : async Nat {
  await* computeLocal(n)
};

Composite queries are one place where await* appears, because composite query calls use computation-style async results, but async* itself is the computation/continuation form. See Async Star for details.

The migration trap is assuming async* means "not consensus" or "query-only." It does not. It is a control-flow form. In an update method, code reached through await* is still part of the update execution; it simply avoids adding an extra proof break when the helper does not actually suspend.

Invariants and Async Functions

Actor invariants interact with async functions at specific points:

async-invariant.sr9

// Async functions with invariant preservation
persistent actor {
  var balance : Nat = 0;
  invariant balance <= 1_000_000;

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

  // Invariant must hold before and after await
  public func deposit(amount : Nat) : async ()
    modifies balance
    entry_requires balance + amount <= 1_000_000;
    requires balance + amount <= 1_000_000;
  {
    balance += amount;
    // Invariant proven here: balance <= 1_000_000

    try { await pause(); } catch (_) {};
    // Invariant assumed to hold after await

    assert balance <= 1_000_000;
  };
}

The invariant lifecycle:

1. Method entry - invariant is assumed to hold
2. Before await - invariant must be proven to hold (release)
3. After await - invariant is assumed to hold again (assume)
4. Method exit - invariant must be proven to hold

This "release-assume" model accounts for potential interference during the await. See Invariants and Await for more details.

Use invariants for facts that must survive arbitrary interleavings. Use local snapshots for facts you only need to remember as values. Do not rely on exact actor-field equality after a suspending await unless an invariant or frame rule justifies it; the interference model intentionally treats public state as potentially changed.

Shared Type Requirements

Async types must contain only shared types - types that can be serialized across the network:

Shared types:

• Primitives: Nat, Int, Bool, Text, Float, Principal, Blob
• Containers of shared types: ?T, [T], tuples, records, variants
• Actor references whose interface contains only shared functions
• Other async types: async T (when T is shared)

Not shared:

• Functions (closures cannot be serialized)
• Mutable arrays in async results
• Modules
• Generic types not bounded by shared

Common Patterns

Implicit Async Body

Public actor methods return async values, but the method body is written as the value to produce. Sector9 inherits Motoko's implicit async-body wrapping:

async-implicit-body.sr9

// Public actor method bodies are implicitly wrapped as async results.
persistent actor {
  var count : Nat = 0;

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

Verification contracts still apply normally; if the body reads or writes actor fields, declare the corresponding reads or modifies clauses.

Non-Shared Content in Async

Async types must contain only shared content:

async-non-shared_reject.sr9

// Error: async type must have shared content
persistent actor {
  // Error M0033: async type has non-shared content type
  var pendingCallbacks : [async (Nat -> Nat)] = [];
  // Functions cannot be stored in async types
}

Functions cannot be stored in async types because they cannot be serialized.

Mismatched Await Keywords

Using the wrong await keyword for the async sort:

// Error M0088: cannot await* a regular async
let fut : async Nat = someFunc();
try { await* fut } catch (_) { 0 };  // Wrong: use await instead

// Error M0088: cannot await a computation
let comp : async* Nat = someQuery();
try { await comp } catch (_) { 0 };  // Wrong: use await* instead

Use await for async T and await* for async* T.

Async Functions vs Synchronous Functions

Aspect	Sync Function	Async Function
Return type	T	async T
Calling	Direct: f()	Await: await f()
State after call	Unchanged unless the call mutates it	Shared actor state may have changed after a suspending await
Invariant check	At entry/exit	At entry/exit + around awaits
Execution	Immediate	Produces a future; observation of the result requires await

Async functions introduce complexity because:

• Other calls may execute while awaiting (interference)
• Actor invariants are the primary mechanism for reasoning about post-await state
• The old() expression captures method entry state, not pre-await state

Pure Functions Cannot Be Async

Pure functions are restricted from using await:

// Error M0240: pure or lemma functions may not await
pure func bad() : Nat {
  await someAsync();  // Not allowed
  42
};

Pure functions must be side-effect free and cannot suspend execution. If you need async behavior, remove the pure modifier.

Summary

• Async functions return async T and represent eventual values (futures)
• All public actor methods must have async return types
• Private async functions can serve as helpers with their own contracts
• Actor invariants are proven before and assumed after each await
• Two async sorts exist: async T (use await) and async* T (use await*)
• await* only creates an interference boundary when the computation may reach a real await
• async* is a computation form, not a consensus bypass
• Async types must contain only shared (serializable) content
• Pure and lemma functions cannot use await
• The verifier reasons modularly using contracts at each await point

Related Topics

• Await expressions for suspension syntax and restrictions
• Commit points for rollback and permanence
• Async verification for the release-assume model
• Composite queries for query-specific await*