Await Expressions

The await expression suspends execution until an async operation completes, then returns its result. Understanding await is essential for verification because each suspending await is an interference point where other actors may execute and where earlier state changes have committed.

What is Await?

When you call an async function, you get a future - a placeholder for a value that will be available later. The await expression suspends the current method until that future resolves, then extracts the result value.

let future : async Nat = someAsyncFunc();
let value : Nat = try { await future } catch (_) { 0 };  // Suspends until future resolves

During the suspension, other actors, and even your own public methods through reentrancy, may execute. This is the key challenge for verification: the world can change while you wait. Sector9 therefore treats an await as both a commit point and an interference point.

Basic Syntax

The await expression has the form await expr where expr has type async T:

await-basic.sr9

// Basic await expression
persistent actor {
  var counter : Int = 0;
  invariant counter >= 0;

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

  // Await suspends until bump() completes
  public func increment() : async Int
    modifies counter
    ensures result >= 0;
  {
    try { await bump(); } catch (_) {};
    counter
  };
}

Key points:

• await can only appear inside async functions
• The await suspends until the async operation completes
• After await, execution continues with the result value
• Contracts are checked modularly at each await point

Multiple Awaits

A method can contain multiple await expressions. Each await is a separate suspension point:

await-multiple.sr9

// Multiple sequential awaits
persistent actor {
  var a : Int = 0;
  var b : Int = 0;
  invariant a >= 0 and b >= 0;

  private func incA() : async ()
    modifies a
    ensures a == old(a) + 1;
  {
    a += 1;
  };

  private func incB() : async ()
    modifies b
    ensures b == old(b) + 1;
  {
    b += 1;
  };

  // Each await is a separate suspension point
  public func incrementBoth() : async Int
    modifies a, b
    ensures result >= 0;
  {
    try { await incA(); } catch (_) {};
    try { await incB(); } catch (_) {};
    a + b
  };
}

The verifier treats each await independently:

1. Check preconditions and prove invariant before first await
2. Assume invariant holds after first await
3. Check preconditions and prove invariant before second await
4. Assume invariant holds after second await
5. Prove postconditions at method exit

Await Variants

Sector9 supports two await keywords for different async types:

Keyword	Type	Behavior
await	async T	Suspends until future resolves, returns T
await*	async* T	Continues through a computation; suspends only if that computation reaches a real await

// Regular await
let value : Nat = try { await someFunc() } catch (_) { 0 };

// Computation await
private func localStep(n : Nat) : async* Nat {
  n + 1
};

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

Use await for async T. Use await* for async* T. Composite queries are one common source of async* values, but await* is not limited to composite queries and does not by itself decide whether execution goes through consensus. await? is not supported by Sector9 verification; use try/catch around awaits that can fail.

When the awaited expression is a shared call to a proof-enabled sr9 boundary, the async control-flow rules still apply. The call may additionally carry proof wrappers and token wire conversions, but the caller must still handle failure and reason about post-await state through invariants, frames, or rechecks.

Verification Mode Restrictions

Verification enforces a stricter subset around await:

• Every await and every await* that may reach a real suspension must be enclosed in a try with a catch-all handler.
• Direct let x = await f()-style value binding is rejected; use let x = try { await f() } catch (_) { fallback } so both success and failure paths are explicit.
• await inside a catch must itself be wrapped in an inner catch-all; finally blocks cannot contain await.
• Futures must be awaited; fire-and-forget async values are rejected.

The catch path is part of the proof, not an afterthought. If the success path uses a callee postcondition, the catch path must still leave the actor in a state strong enough to satisfy invariants and the enclosing method's postconditions.

Invariants and Await

Actor invariants are critical for reasoning about state after await. The verifier uses a release-assume model:

await-with-invariant.sr9

// Invariant preservation across await
persistent actor {
  var counter : Int = 0;
  invariant counter >= 0;

  private func bump() : async () modifies counter {
    counter += 1;
  };

  public func safeIncrement() : async () modifies counter {
    // Invariant available here (assumed at entry)
    assert counter >= 0;

    try { await bump(); } catch (_) {};  // Invariant released, then re-assumed

    // Invariant available here (assumed after await)
    assert counter >= 0;
  };
}

The invariant lifecycle at each await:

1. Prove - Before await, prove the invariant holds
2. Release - Permissions to shared state are released
3. Assume - After await resumes, assume the invariant holds

This reflects reality: while you await, other methods may modify state, but they must preserve the invariant.

Local vs Shared State Across Await

The verifier distinguishes between fresh local state and shared state:

Fresh Locals Are Preserved

Local variables that don't escape to actor fields remain stable across await:

await-local-preserved.sr9

// Fresh locals are preserved across await
persistent actor {
  var counter : Int = 0;

  private func bump() : async () modifies counter {
    counter += 1;
  };

  public func localSnapshot() : async Int
    modifies counter
  {
    let snapshot = counter;  // Local copy of primitive
    try { await bump(); } catch (_) {};
    // snapshot is unchanged - it's a fresh local
    snapshot
  };
}

The snapshot variable is a fresh local primitive. It cannot be modified by other actors because they have no reference to it.

Shared State Is Invalidated

Actor fields and aliases to them become unknown after await:

await-shared-stale_unsat.sr9

// Shared state is invalidated at await (verification fails)
persistent actor {
  var counter : Int = 0;
  invariant counter >= 0;

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

  public func badAssumption() : async () modifies counter {
    let before = counter;
    try { await bump(); } catch (_) {};
    // ERROR: cannot assume counter == before
    // Counter was modified during the await
    assert counter == before;
  };
}

This verification fails because counter is shared state. During the await, any public method could have modified it. Only invariants can guarantee properties about shared state after await.

The old() Expression and Await

A common point of confusion: old(x) refers to method entry state, not pre-await state.

await-old-method-entry.sr9

// old() refers to method entry, not pre-await state
persistent actor {
  var x : Int = 0;

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

  public func demonstrateOld(n : Int) : async Int
    modifies x
    entry_requires n > 0;
    requires n > 0;
    ensures result == old(x);  // old(x) is method entry value
  {
    let entry = x;  // Capture entry value
    x += n;         // Modify x
    try { await tick(); } catch (_) {};  // old(x) still refers to entry, not here
    entry           // Return the entry value
  };
}

There are no per-await snapshots. If you need the pre-await value, capture it in a local variable before the await.

// Capture pre-await value manually
let preAwaitValue = counter;
try { await someOperation(); } catch (_) {};
// Use preAwaitValue, not old(counter)

Await in Loops

Await can appear inside loops. Each iteration's await is a suspension point:

await-in-loop.sr9

// Await inside a loop with loop invariant
persistent actor {
  var counter : Int = 0;
  invariant counter >= 0;

  private func bump() : async () modifies counter {
    counter += 1;
  };

  public func incrementN(n : Int) : async ()
    modifies counter
    entry_requires n >= 0;
    requires n >= 0;
  {
    var i = 0;
    while (i < n) {
      loop:invariant i >= 0 and i <= n;
      loop:invariant counter >= 0;
      try { await bump(); } catch (_) {};
      i += 1;
    };
  };
}

Loop invariants must account for the await:

• Before each iteration's await, prove the loop invariant
• After the await, assume the loop invariant (and actor invariant) hold
• The loop invariant should include bounds on loop variables and any properties needed about shared state

Where Await Cannot Appear

Await is restricted to certain contexts:

Not in Query Functions

Ordinary query functions cannot await:

await-in-query_reject.sr9

// Await is not allowed in query functions (type error)
persistent actor {
  var counter : Int = 0;

  private func fetch() : async Int reads counter {
    counter
  };

  // ERROR: queries cannot await
  public query func badQuery() : async Int {
    await fetch()  // M0037: misplaced await
  };
}

Error M0037: misplaced await; a query cannot contain an await

Not in Pure or Lemma Functions

Pure functions must be side-effect free and deterministic:

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

Not Outside Async Context

Await requires an enclosing async function or expression:

// Error M0038: misplaced await
func syncFunc() : Nat {
  await someAsync()  // Cannot await in sync function
};

Scope Restrictions

The future being awaited must come from the current scope or an enclosing scope. This prevents deadlocks:

// Error M0087: ill-scoped await
do {
  let a : async () = async { await b; };  // b not in scope
  let b : async () = async { await a; };  // circular reference
};

The type system prevents circular dependencies that could cause deadlocks.

Common Mistakes

Assuming State After Await

Wrong

public func wrong() : async () modifies counter {
  let before = counter;
  try { await someOperation(); } catch (_) {};
  assert counter == before;  // Fails: counter may have changed
};

Correct

persistent actor {
  var counter : Int = 0;
  invariant counter >= 0;

  public func correct() : async () modifies counter {
    try { await someOperation(); } catch (_) {};
    assert counter >= 0;  // Works: guaranteed by invariant
  };
}

Only properties guaranteed by invariants are known after await.

Confusing old() with Pre-Await

Wrong

public func wrong(n : Int) : async Int
  modifies x
  ensures old(x) == x;  // Expects old to mean "before await"
{
  x += n;
  try { await tick(); } catch (_) {};
  x  // old(x) is still the method entry value!
};

Correct

public func correct(n : Int) : async Int
  modifies x
  ensures result == old(x) + n;  // old(x) is method entry
{
  x += n;
  try { await tick(); } catch (_) {};
  old(x) + n  // Compute from entry value
};

Remember: old() always refers to method entry, never to intermediate points.

Weakened Frame Conditions

In synchronous methods, fields not in modifies are guaranteed unchanged. In async methods with await, this guarantee weakens:

persistent actor {
  var a : Int = 0;
  var b : Int = 0;  // Not in modifies

  public func updateA() : async ()
    modifies a
    ensures b == old(b);  // May fail without invariant!
  {
    try { await someOperation(); } catch (_) {};
    a += 1;
  };
}

Without an invariant pinning b, other methods could modify it during the await. Add an invariant if you need frame guarantees across await.

Interference Model

The verifier uses a conservative interference model. At each suspending await:

1. All public methods may execute - Any public function could be called
2. Multiple times - The same method could run repeatedly
3. In any order - No assumptions about call sequence
4. By any caller - No restrictions on who called

This means shared state is havoced (made unknown) at await boundaries, except for invariant guarantees. A non-suspending await* is treated like a local call and does not create this boundary.

The model is intentionally conservative. It does not try to predict the exact IC schedule; it asks whether your method remains correct for every public interleaving allowed by its own contracts, frames, and invariants.

Summary

• await expr suspends execution until the async operation completes
• Two variants: await for futures and await* for computations
• Each await is an interference point where other actors may execute
• Each suspending await is also a commit point for earlier state changes
• await* is an interference point only when the computation may reach a real await; non-suspending computations are treated like local calls
• Invariants are proven before and assumed after each await
• Fresh locals (not escaping to actor state) are preserved across await
• Shared state (actor fields and aliases) is invalidated at await
• old() refers to method entry, not pre-await state
• Await cannot appear in queries, pure functions, lemmas, or sync functions
• Use invariants to guarantee properties about shared state after await

Related Topics

• Atomicity between awaits for interleaving boundaries
• Commit points for what survives traps
• Old expressions for method-entry snapshots
• Async star for async* computations