Frame Conditions Across Await

Frame conditions that guarantee unchanged fields are weaker at suspending await boundaries, but Sector9 keeps them precise for fields no public method can write.

What Are Frame Conditions

In synchronous methods, frame conditions guarantee that fields not in the modifies clause remain unchanged. If a method declares modifies x, the verifier automatically adds ensures y == old(y) for every field y not in the modifies clause.

This guarantee weakens when a suspending await occurs. Interference allows other public methods to execute while your actor is suspended. Fields those methods may modify lose exact value facts; fields no public method can write can still be framed.

Sync vs Async Frames

Sync (Strong Frames)

In sync methods, frames are strong. If secondary is not in modifies, it cannot change:

public func syncIncrement() : ()
  modifies primary
  ensures primary == old(primary) + 1;
  ensures secondary == old(secondary);  // Automatic frame
{
  primary += 1;
};

Async (Weak Frames)

In async methods with await, frames are weak for fields that another public method may modify. Even though secondary is only in reads for this method, another public method may write it:

public func asyncIncrement() : async ()
  modifies primary
  reads secondary
  // Cannot add: ensures secondary == old(secondary)
{
  primary += 1;
  try { await pause(); } catch (_) {};
  // secondary might have changed during await
};

Why Frames Weaken

At each await point, the verifier models interference: any public method could execute. If another public method has modifies secondary, then secondary could change during your await.

frame-weak-after-await_unsat.sr9

// Frame conditions weaken after await
// Expected Outcome: UNSAT (verification fails)
// Without an invariant, cannot guarantee read-only fields stay unchanged

persistent actor {
  var counter : Int = 0;
  var limit : Int = 100;

  // This method could be called during await
  public func setLimit(n : Int) : async ()
    modifies limit
  {
    limit := n;
  };

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

  // Trying to prove limit unchanged across await
  public func checkLimitAfterAwait() : async Bool
    reads limit
    modifies counter
    ensures limit == old(limit);  // FAILS: cannot prove this
  {
    counter += 1;
    try { await pause(); } catch (_) {};
    // During await, setLimit could have been called
    // limit might now be different from old(limit)
    counter < limit
  };
}

The method setLimit could be called during the awaited pause(). Even though checkLimitAfterAwait only reads limit, it cannot prove limit == old(limit) because the interference model allows setLimit to modify it.

The Frame Hierarchy

Understanding when frame guarantees apply:

Scenario	Frame Guarantee
Sync method, field not in modifies	Strong: field unchanged
Async method, no await, field not in modifies	Strong: field unchanged
Await, field has no public writers	Stronger selective frame may preserve exact value
Async method with await, field in invariant	Preserved via invariant
Async method with await, field publicly writable and not protected	Weak: field may change

The key insight: frames are strong until an await occurs. After await, exact facts survive only for fields outside the possible public write set; publicly writable fields need invariant properties or local snapshots.

Using Invariants to Preserve Frames

When you need a field to remain unchanged across await, pin it with an invariant:

frame-invariant-preserves.sr9

// Invariants preserve frame-like guarantees across await
// The invariant pins the field value, making it stable

persistent actor {
  var counter : Int = 0;
  var max_value : Int = 1000;

  // Invariant pins max_value to a specific value
  invariant max_value == 1000;

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

  // With the invariant, we can prove max_value stays unchanged
  public func process() : async ()
    modifies counter
    reads max_value
    ensures max_value == old(max_value);  // Succeeds due to invariant
  {
    let before = max_value;
    try { await bump(); } catch (_) {};
    // After await: invariant guarantees max_value == 1000
    assert max_value == before;  // Verified
    assert max_value == 1000;    // Verified
  };
}

The invariant max_value == 1000 ensures this property holds before and after every await. The verifier can then prove max_value == old(max_value) because the invariant pins the exact value even if a public method could write the field.

Invariant Patterns for Frames

Different invariant patterns provide different frame-like guarantees:

// Exact value: strongest frame guarantee
invariant config == 42;
// After await: config == 42

// Range bound: partial frame guarantee
invariant limit >= 100 and limit <= 200;
// After await: limit in [100, 200], but exact value unknown

// Relationship: relative frame guarantee
invariant total == a + b + c;
// After await: sum preserved, individual values may vary

The old() Expression Across Await

The old() expression refers to method entry state, not the state before each await. This is intentional: there are no per-await snapshots.

frame-old-method-entry.sr9

// old() refers to method entry, not pre-await state
// This is NOT per-await snapshot semantics

persistent actor {
  var x : Nat = 0;

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

  // Demonstrating old() semantics in async methods
  public func demonstrateOld(n : Nat) : async Nat
    modifies x
    entry_requires n > 0;
    requires n > 0;
    // old(x) refers to value at method ENTRY
    ensures result == old(x) + n;
  {
    let entry = x;        // Runtime snapshot of the entry value
    x += n;               // x changed from entry
    try { await tick(); } catch (_) {};
    // old(x) still refers to method entry, not pre-await
    assert old(x) == entry;  // old(x) still names method entry
    entry + n             // Return the value derived from method entry
  };
}

Even after the awaited tick(), old(x) still refers to the value of x at method entry.

No Per-Await Snapshots

A common misconception is that old() resets after each await. It does not:

frame-old-not-per-await_unsat.sr9

// old() does NOT create per-await snapshots
// Expected Outcome: UNSAT (verification fails)
// Demonstrates that old(x) always refers to method entry

persistent actor {
  var x : Nat = 1;

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

  // This incorrectly assumes old(x) resets after await
  public func badAssumption(n : Nat) : async Nat
    modifies x
    entry_requires n > 0;
    requires n > 0;
    ensures old(x) == x;  // FAILS: x changed before await
  {
    x += n;          // x is now old(x) + n
    try { await tick(); } catch (_) {};
    // old(x) still refers to method entry
    // x is entry + n, not equal to old(x)
    x
  };
}

The postcondition old(x) == x fails because x changed before the await. The old(x) still refers to the entry value, not a snapshot taken just before the awaited tick().

Why No Per-Await Snapshots

Per-await snapshots would require tracking state at each suspension point, significantly complicating the verification model. The current design is simpler and more predictable: old() always means method entry. Use a local variable when you need the value immediately before a particular await.

The Local Snapshot Pattern

To preserve values across await, capture them in local primitive variables:

frame-local-snapshot.sr9

// Using local snapshots to preserve values across await
// The snapshot pattern: capture primitives before await

persistent actor {
  var balance : Int = 0;
  var transactions : Int = 0;

  invariant balance >= 0;

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

  // Public method that could be called during await
  public func deposit(amount : Nat) : async ()
    modifies balance, transactions
    entry_requires amount > 0;
    requires amount > 0;
  {
    balance += amount;
    transactions += 1;
  };

  // Snapshot pattern: capture values before await
  public func reportAndProcess(amount : Nat) : async Int
    modifies balance, transactions
    entry_requires amount > 0;
    requires amount > 0;
    ensures result >= 0;
  {
    // Capture current values in local primitives
    let balanceSnapshot = balance;
    let _txSnapshot = transactions;

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

    // After await, snapshots are still valid
    // (they are local primitives, not references)
    assert balanceSnapshot >= 0;  // Verified

    // But balance and transactions may have changed
    // due to deposit() calls during await

    balance += amount;
    transactions += 1;
    balance
  };
}

Local primitives are copied by value, not by reference. The balanceSnapshot variable holds an Int value that cannot be affected by interference. This is fundamentally different from old(), which refers to heap state that may have changed.

When Snapshots Work

Local snapshots work for:

Type	Works	Reason
Int, Nat, Bool	Yes	Primitives are copied
Text, Char	Yes	Immutable
Immutable records	Yes	No var fields to modify
Mutable references	No	Still points to shared state

Comparing Preservation Techniques

Technique	What It Preserves	When to Use
Invariants	Properties that must hold	Protecting important constraints
Local snapshots	Primitive values	Capturing pre-await state
Fresh allocations	Local objects	Objects that don't escape
old()	Entry state reference	Postconditions comparing to entry

Choose based on what you need to preserve:

• Exact values needed after await: Use local snapshots
• Properties needed after await: Use invariants
• Comparing to method entry: Use old() in postconditions

Async Methods Without Await

If an async method contains no await, frame conditions remain strong:

public func noAwait() : async ()
  modifies x
  reads y
  ensures y == old(y);  // Valid: no await
{
  x += 1;
  // No await here, so y cannot change
};

The verifier only applies interference at actual await points. Methods declared async but without suspending await statements get sync-like frame guarantees. The same idea applies to await*: if the async* callee cannot suspend, it is treated like a local call rather than a commit boundary.

Common Mistakes

Assuming Read-Only Fields Stay Unchanged

// WRONG: y could change during await
public func bad() : async ()
  reads y
  modifies x
  ensures y == old(y);  // Fails
{
  x += 1;
  try { await pause(); } catch (_) {};
};

Fix by adding an invariant or using a local snapshot.

Confusing old() with Pre-Await State

// WRONG: old(x) is method entry, not pre-await
public func wrong(n : Nat) : async Nat
  modifies x
  ensures old(x) == x;  // Fails if x changed before await
{
  x += n;
  try { await tick(); } catch (_) {};
  x
};

Use local variables to capture pre-await state if needed.

Over-Relying on modifies for Frame Guarantees

// WRONG: modifies only affects THIS method
public func caller() : async ()
  modifies a
  reads b
  ensures b == old(b);  // Fails
{
  try { await callee(); } catch (_) {};  // callee or other methods might modify b
};

The modifies clause specifies what this method changes, not what other methods can change.

Debugging Frame Issues

When frame conditions fail across await:

1. Check for interference - Is there a public method that modifies the field?
2. Add an invariant - If the field should never change, add invariant field == value
3. Use local snapshots - If you need the pre-await value, capture it
4. Check await points - Remove awaits temporarily to isolate the issue
5. Review the interference model - Remember that any public method with a matching write effect could execute

See Also

• The modifies Clause - Declaring modification footprints
• Frame Conditions - Frame conditions in sync code
• Invariants and Await - How invariants interact with await
• Interference Model - What can change during await
• Local vs Shared State - Which variables are stable across await
• Async Star - Why non-suspending await* does not add a frame break

Summary

• Frame conditions are strong in sync methods and async methods without await
• Frame conditions weaken at await boundaries for publicly writable fields
• Invariants restore frame-like guarantees by constraining what interference can do
• Selective havoc preserves exact facts for fields no public method can write
• old() refers to method entry, not pre-await state (no per-await snapshots)
• Local snapshots preserve primitive values across await by copying
• Choose between invariants, snapshots, and fresh allocations based on your needs
• Async methods without await get strong frame guarantees