Invariants and Await

Actor invariants must hold at every suspending boundary, modeling the possibility that other messages executed while the actor was suspended.

For the full await soundness model and related restrictions, see Verified Restrictions and Soundness Notes.

The Release-Assume Model

When the verifier encounters a suspending await, it models the boundary as three steps:

1. Prove the invariant holds before the await
2. Release the invariant (other actors may run)
3. Assume the invariant holds when execution resumes

This reflects the Internet Computer's execution model: while your actor awaits a response, other messages may enter your actor through public methods and modify actor state. Sector9 uses the public methods' write effects to decide which fields may be changed, then keeps only the facts justified by actor invariants, frames for untouched fields, and local values that cannot alias actor state. See the interference model for the precise rule.

Invariants Are Available Before Await

Before reaching an await, you can rely on actor invariants in your code:

async-inv-before-await.sr9

// Invariant available before await
persistent actor {
  var counter : Int = 0;
  invariant counter >= 0;

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

  public func run() : async () modifies counter {
    assert counter >= 0;  // Invariant available here
    try { await bump(); } catch (_) {};
  };
}

The assert counter >= 0 succeeds because the invariant is established at method entry and preserved until the await.

Invariants Are Re-Assumed After Await

After an await completes, the verifier assumes the invariant holds again:

async-inv-after-await.sr9

// Invariant re-assumed after await
persistent actor {
  var counter : Int = 0;
  invariant counter >= 0;

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

  public func run() : async () modifies counter {
    try { await bump(); } catch (_) {};
    assert counter >= 0;  // Invariant holds after await
  };
}

The assertion after the awaited bump() succeeds because the verifier assumes counter >= 0 when execution resumes. The actual value of counter may have changed (it could be 1, 5, or 100), but the invariant property is guaranteed.

Invariant Violations at Await Boundaries

The verifier checks that invariants hold at two key points around await:

Before Await

Violating the invariant before an await fails verification:

async-inv-violation-before_unsat.sr9

// Invariant violation before await fails verification
persistent actor {
  var counter : Int = 0;
  invariant counter >= 0;

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

  public func run() : async () modifies counter {
    counter := -1;  // Violates invariant
    try { await bump(); } catch (_) {};  // ERROR: invariant must hold before await
  };
}

Setting counter := -1 violates the invariant. The verifier cannot proceed to the await because it cannot prove the invariant holds.

After Await (At Method Exit)

Violations after await but before method exit are also caught:

async-inv-violation-after_unsat.sr9

// Invariant violation after await but before exit fails verification
persistent actor {
  var counter : Int = 10;
  invariant counter >= 0;

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

  public func violateAfterAwait() : async () modifies counter {
    try { await noop(); } catch (_) {};
    counter := -100;  // ERROR: invariant violated at method exit
  };
}

Even though the invariant holds after the awaited noop(), setting counter := -100 violates it before the method returns.

What Changes Across Await

Without invariants, the verifier cannot assume anything about shared state after an await:

async-shared-stale_unsat.sr9

// Without invariants, shared state is not stable across await
persistent actor {
  var counter : Int = 0;

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

  public func run() : async () modifies counter {
    let before = counter;
    try { await bump(); } catch (_) {};
    assert counter == before;  // ERROR: counter may have changed
  };
}

This fails because counter is in the modifies clause of a public method. Between the snapshot let before = counter and resumption after the awaited bump(), another message could have called a public method that writes counter.

The Invariant Is Your Only Guarantee

After await, exact field values are known only for fields that the interference analysis can prove no public method may write. For fields that can be written during suspension, only invariant properties survive. If your invariant says counter >= 0, you know counter >= 0 but not the exact value. If you need to track exact values, use local snapshots, stronger invariants, or ghost state.

Fresh Locals Are Preserved

Objects allocated locally that do not escape to actor fields remain stable across await:

async-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 run() : async () modifies counter {
    let local : [var Int] = [var 5, 6];  // Fresh allocation
    try { await bump(); } catch (_) {};
    assert local[0] == 5;  // Valid: fresh local not affected
    assert local[1] == 6;
  };
}

The local array [var 5, 6] is freshly allocated and does not alias any actor state. The verifier's escape analysis determines it cannot be modified by other actors, so its values remain stable.

What Counts as Fresh

A local is preserved across await if it:

• Is allocated within the current method
• Does not escape to actor fields or return values
• Is not an alias to actor state

Aliases to actor fields are rejected at await boundaries because the local reference would cross into a suspension where the underlying actor state may be modified. See Local vs Shared State.

Loop Invariants with Await

Loop invariants over local variables work correctly even when the loop body contains await:

async-loop-invariant.sr9

// Loop invariants work with await in the body
persistent actor {
  var counter : Int = 0;

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

  public func run(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;
      try { await bump(); } catch (_) {};
      i += 1;
    };
  };
}

The loop invariant i >= 0 and i <= n is over local variable i, which is not affected by await. The verifier checks the same obligations described in loop invariant annotation:

1. The invariant holds on loop entry
2. If the invariant holds at the start of an iteration, it holds at the end
3. The invariant holds after the loop terminates

Multiple Awaits

Each suspending await is a potential interference point. For sequential awaits:

public func multiStep() : async () modifies counter {
  try { await step1(); } catch (_) {};  // Invariant checked before, assumed after
  doWork();
  try { await step2(); } catch (_) {};  // Invariant checked before, assumed after
  try { await step3(); } catch (_) {};  // Invariant checked before, assumed after
}

The invariant is verified before each await and assumed after each await. Between awaits, normal verification applies.

await* follows the same rule only when the called async* computation may actually suspend. If the async* call chain contains no suspending await, Sector9 treats it like a local call and does not add an extra interference boundary.

Common Mistakes

Assuming Exact Values After Await

// WRONG: Exact value not preserved
public func bad() : async () modifies counter {
  let snapshot = counter;
  try { await pause(); } catch (_) {};
  assert counter == snapshot;  // Fails
}

Invariant Too Strict for Operations

// WRONG: Cannot temporarily violate invariant before await
persistent actor {
  var flag : Bool = true;
  invariant flag;

  public func process() : async () modifies flag {
    flag := false;    // Violates invariant
    try { await doWork(); } catch (_) {};  // Error here
    flag := true;
  }
}

If you need to temporarily break an invariant, restructure your code so the invariant holds at all await points.

See Also

• Actor Invariants - Declaring actor invariants
• Invariant Preservation - How invariants are checked
• Interference Model - What can change during await
• Local vs Shared State - Which variables are stable across await

Summary

• Actor invariants must hold before each await (verifier proves this)
• Actor invariants are assumed to hold after each await resumes
• The release-assume model reflects potential interference from other messages while suspended
• Fields written by possible public interference lose exact value facts; untouched fields can still frame
• Fresh local allocations are preserved across await
• Loop invariants over locals work correctly with await in the body