Local vs Shared State

The verifier's escape analysis classifies variables into local (preserved) and shared (invalidated) categories at await boundaries.

Three Ownership Categories

The verifier performs escape analysis to classify every variable into one of three categories:

Category	Description	Across Await
Actor-rooted	Actor fields and anything reachable from them	Invalidated (havoced)
Fresh allocation	Objects allocated in the current method that don't escape	Preserved (stable)
Unknown/external	Values from external calls or unknown sources	Invalidated (havoced)

Only fresh, non-escaping allocations remain stable across await. Actor-rooted references are not allowed to remain live across a suspending await, and unknown references are treated conservatively. Everything that can be reached by another message is subject to interference.

alias-three-categories.sr9

// Three ownership categories at await boundaries
persistent actor {
  type Cell = { var x : Int };
  var actorField : Cell = { var x = 0 };  // Category 1: Actor-rooted (shared)

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

  public func demonstrate() : async () modifies actorField {
    let fresh : Cell = { var x = 1 };     // Category 2: Fresh allocation (local)
    let _fieldSnapshot = actorField.x;    // Primitive snapshot of actor state

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

    // After await:
    assert fresh.x == 1;   // Fresh locals are preserved
    // Primitive snapshots remain available; actorField.x itself is unknown.
    // A live alias to actorField would be rejected across await.
    // actorField.x is unknown, only invariant properties hold
  };
}

Fresh Locals Are Preserved

When you allocate an object locally and it does not escape to actor fields or public returns, the verifier knows it cannot be modified by other actors:

alias-fresh-local.sr9

// Fresh local allocations remain stable 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 x : Int } = { var x = 42 };  // Fresh allocation
    try { await bump(); } catch (_) {};
    assert local.x == 42;  // Fresh local is preserved
  };
}

The local record { var x = 42 } is freshly allocated. The verifier's escape analysis determines no other actor can reach it, so local.x remains 42 after the await.

Arrays Work the Same Way

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 is freshly allocated and does not alias any actor state. Its elements are preserved across await.

Aliases to Actor State Are Invalidated

When a local variable aliases actor state, it becomes shared. The verifier cannot preserve exact values for shared state across await:

alias-to-field_unsat.sr9

// Aliases to actor fields are invalidated across await
persistent actor {
  type Cell = { var x : Int };
  var cell : Cell = { var x = 0 };

  private func bump() : async () modifies cell {
    cell.x += 1;
  };

  public func run() : async () modifies cell {
    let cellAlias = cell;  // Alias to actor field
    let before = cellAlias.x;
    try { await bump(); } catch (_) {};
    assert cellAlias.x == before;  // ERROR: alias invalidated
  };
}

The variable alias points to the same object as cell (an actor field). During the await, bump() could execute, modifying cell.x. In current verification mode this shape is rejected at the await boundary if the alias remains live; if the proof reaches a later assertion, the exact field fact is not available.

Verification Restriction: No Actor-State References Across Await

In verification mode, locals that may reference actor state at an await boundary are rejected, not just invalidated. The verifier reports:

await may not cross references to actor state; drop or copy before await (live: ...)

Avoid keeping references to actor fields across await or suspending await*. Instead:

• Copy primitive values into local snapshots
• Move the await earlier or later so the alias doesn't cross it
• Refactor to use immutable data or ghost state

Escaping Fresh Allocations

A fresh allocation becomes shared if it escapes to an actor field:

alias-escape-to-field_unsat.sr9

// Fresh locals become shared when stored in actor fields
persistent actor {
  type Cell = { var x : Int };
  var stored : Cell = { var x = 0 };

  private func bump() : async () modifies stored {
    stored.x += 1;
  };

  public func run() : async () modifies stored {
    let fresh : Cell = { var x = 10 };
    stored := fresh;  // Fresh local now escapes to actor field
    let before = fresh.x;
    try { await bump(); } catch (_) {};
    assert fresh.x == before;  // ERROR: fresh escaped, now shared
  };
}

Even though fresh starts as a local allocation, storing it in stored makes it reachable from actor state. After that point, the verifier treats fresh as shared.

How Escape Analysis Works

The verifier uses a flow-insensitive, allocation-site points-to analysis:

1. Track allocation sites - Each { var ... } or [var ...] gets a unique identity
2. Build constraints - Variable assignments, field stores, and function calls create aliasing relationships
3. Identify escape roots - Actor fields ($Self), public return values, and unknown calls are escape roots
4. Compute reachability - Objects transitively reachable from escape roots are marked as escaping
5. Classify variables - Variables pointing to escaping objects are shared; others are local

Conservative by Design

The analysis is flow-insensitive: it considers all possible executions, not the actual control flow. This is sound (never misses aliasing) but may be imprecise (may over-approximate sharing).

public func example() : async () modifies field {
  let obj : { var x : Int } = { var x = 0 };
  if (condition) {
    field := obj;  // obj escapes in one branch
  };
  try { await pause(); } catch (_) {};
  // obj is treated as shared even if condition is false
}

The Snapshot Pattern

To preserve shared state values across await, capture them in primitive locals before the await:

alias-snapshot-pattern.sr9

// Capture shared values into locals before await
persistent actor {
  var counter : Int = 0;
  invariant counter >= 0;

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

  public func run() : async Int
    modifies counter
    ensures result >= 0;
  {
    let snapshot = counter;  // Capture value, not alias
    try { await bump(); } catch (_) {};
    // snapshot is a primitive, not affected by interference
    // counter may have changed, but snapshot is stable
    snapshot
  };
}

The variable snapshot holds an Int value, not a reference. Primitive values are copied, not aliased, so snapshot is unaffected by changes to counter.

When Snapshots Work

Snapshots work best for:

• Primitive types: Int, Nat, Bool, Text, Char
• Immutable records: Records without var fields
• Immutable arrays: [T] values that do not carry mutable actor-state references

Snapshots do not work for mutable references:

let snapshot = cell;  // Copies the reference, not the value
// snapshot and cell point to the same object

Relationship to Permissions

Escape analysis interacts with the permission model:

Classification	Permission at Await	After Await
Local	Write permission retained	Full access
Shared and publicly writable	Permissions released	Invariant properties and re-acquired permissions
Shared but not publicly writable	Permissions retained through the frame model	Exact field facts may be preserved

For publicly writable shared state, permissions are released before await and re-acquired after, but exact values are lost. For local state, permissions are never released. For fields no public method can write, the selective havoc model can preserve exact facts. The permission side of this model is covered in read/write permissions.

Opaque/token handles follow this same local-versus-shared split. A freshly allocated local handle can cross an await and later be passed to its owner module's API. A handle recovered from actor-owned state, including nested carriers such as records, options, variants, arrays, BMap, MBMap, or BSeq, is treated as actor-state reachable and cannot be kept live across the await boundary.

Common Mistakes

Assuming Local After Store

// WRONG: obj escapes to field
let obj : { var x : Int } = { var x = 1 };
actorField := obj;
try { await pause(); } catch (_) {};
assert obj.x == 1;  // Fails: obj is now shared

Aliasing Through Parameters

private func helper(cell : { var x : Int }) : () {
  // cell could alias actor state
  // Cannot assume cell.x is preserved after calls
};

Nested Aliasing

type Outer = { var inner : { var x : Int } };
var wrapper : Outer = { var inner = { var x = 0 } };

let alias = wrapper.inner;  // Aliases nested actor state
try { await pause(); } catch (_) {};
// alias.x is invalidated

Debugging Aliasing Issues

When verification fails due to aliasing:

1. Check the assignment chain - Trace where the variable was assigned
2. Look for stores to fields - Any store to an actor field marks the value as shared
3. Consider transitivity - If a = b and b is shared, a is shared
4. Use the snapshot pattern - Copy primitive values before await
5. Check public modifiers - A field with no public writers has stronger frame behavior than a field in a public modifies clause

Verification Error Pattern

Aliasing issues often appear as explicit await-safety errors:

await may not cross references to actor state; drop or copy before await (live: ...)

This means a live local may reference actor state at an await boundary. Drop the reference before the await or copy primitive/immutable data into a snapshot.

See Also

• Invariants and Await - How invariants interact with await
• Interference Model - What can change during await
• Frame Conditions Across Await - Weaker frame guarantees in async
• Ghost Variables - Verification-only state for tracking
• Footprints - How public write effects drive await havoc

Summary

• The verifier classifies variables as local (preserved) or shared (invalidated) across await
• Fresh allocations that don't escape remain stable across await
• Aliases to actor fields must not remain live across suspending awaits
• Escaping to actor fields or public returns makes a local become shared
• Use the snapshot pattern to capture primitive values before await
• Escape analysis is conservative: when in doubt, values are treated as shared