Skip to main content

Aliasing Restrictions

Mutable records use reference semantics, so multiple variables can point to the same object. This page explains what aliasing patterns are supported, how the verifier handles aliased parameters, and what patterns are rejected.

What Aliasing Means​

Two variables alias when they reference the same mutable record:

let c1 : Cell = { var x = 0 };
let c2 = c1;  // c2 aliases c1
c2.x := 99;
assert c1.x == 99;  // Both see the update

Aliasing is sound but requires the verifier to handle it correctly. The core challenge: when two parameters might alias, updates through one affect the other.

Conditional Postconditions​

When a function takes multiple mutable record parameters of the same type, the verifier handles the ownership requirements conditionally. If two parameters may be the same object, the generated permissions and postconditions have to account for both aliased and distinct cases:

alias-self-call.sr9
// Aliased parameters: calling with the same object twice
persistent actor {
  type Cell = { var x : Int };
  var cell : Cell = { var x = 0 };

  // Postconditions handle both aliased and distinct cases
  private func increment_both(c1 : Cell, c2 : Cell) : ()
    ensures c1 == c2 ==> c1.x == old(c1.x) + 2;
    ensures c1 != c2 ==> c1.x == old(c1.x) + 1;
    ensures c1 != c2 ==> c2.x == old(c2.x) + 1;
  {
    c1.x := c1.x + 1;
    c2.x := c2.x + 1;
  };

  // Call with same object - verifies correctly
  public func test_aliased() : async ()
    modifies cell
    ensures cell.x == old(cell.x) + 2;
  {
    increment_both(cell, cell);
  };
}

The function increment_both has two postcondition forms:

  • c1 == c2 ==> ... — what happens if both parameters point to the same object
  • c1 != c2 ==> ... — what happens if they point to different objects

This pattern handles self-aliased calls like increment_both(cell, cell) correctly.

Explicit Disjointness​

When aliasing is not intended, require distinct parameters explicitly:

alias-disjoint-precondition.sr9
// Requiring distinct parameters with explicit precondition
persistent actor {
  type Cell = { var x : Int };

  // Function requires parameters to be distinct
  private func swap(c1 : Cell, c2 : Cell) : ()
    requires c1 != c2;
    ensures c1.x == old(c2.x);
    ensures c2.x == old(c1.x);
  {
    let tmp = c1.x;
    c1.x := c2.x;
    c2.x := tmp;
  };

  public func test_swap() : async () {
    let a : Cell = { var x = 10 };
    let b : Cell = { var x = 20 };
    swap(a, b);  // Fresh allocations are always distinct
    assert a.x == 20;
    assert b.x == 10;
  };
}

The requires c1 != c2 precondition tells callers they cannot pass the same object twice. With this precondition, the verifier can use the simpler disjoint-ownership path. See requires for caller obligations.

Fresh Allocations Are Distinct​

Freshly allocated records are guaranteed to not alias any existing reference:

alias-fresh-disjoint.sr9
// Fresh allocations are guaranteed distinct
persistent actor {
  type Cell = { var x : Int };
  var existing : Cell = { var x = 42 };

  public func test_fresh_distinct() : async () modifies existing {
    let fresh : Cell = { var x = 0 };
    // Fresh allocations do not alias existing references
    let ex0 = existing.x;
    fresh.x := 99;
    assert existing.x == ex0;  // existing unchanged by fresh.x update
    assert fresh.x == 99;
  };
}

The verifier knows that each { var ... } expression creates a new, unique object. This guarantees:

  • Fresh allocations are distinct from each other
  • Fresh allocations are distinct from actor fields
  • Updates to one do not affect the other

How the Verifier Handles Aliasing​

The verifier uses partition-based alias reasoning:

  1. Group parameters by their mutable record type
  2. Generate all partitions of these parameters (aliased vs. distinct combinations)
  3. Compute effects for each partition based on which updates share targets
  4. Emit guarded facts that are valid for that partition

For a function with two Cell parameters, the verifier considers:

  • Both same object: c1 == c2
  • Both distinct: c1 != c2

For three parameters, it considers all groupings: all same, all distinct, pairs matching, etc.

Example: How Partitions Work​

Consider:

private func update(c1 : Cell, c2 : Cell) : ()
{
  c1.x := c1.x + 1;
  c2.x := c2.x + 10;
};

The verifier generates:

ConditionEffect on c1.xEffect on c2.x
c1 == c2old(c1.x) + 11(same as c1)
c1 != c2old(c1.x) + 1old(c2.x) + 10

When aliased, both updates apply to the same object sequentially. When distinct, each object receives its own update.

Aliasing and Await​

For aliasing behavior across await boundaries, see Local vs Shared State. The key points:

  • Fresh allocations that don't escape remain stable across await
  • Aliases to actor fields may not remain live across await; copy primitive data first or re-read through actor state after the await
  • Escaping a fresh allocation to an actor field makes it shared

Restrictions​

Cannot Pattern-Match Mutable Fields​

Pattern matching on var fields is rejected because mutable fields are heap locations, not destructurable value fields:

mutrec-pattern-match_reject.sr9
// Cannot pattern-match mutable record fields
persistent actor {
  type Cell = { var x : Int };

  public func bad() : async () {
    let cell : Cell = { var x = 10 };
    // ERROR: cannot pattern match mutable field x
    let { x } = cell;
  };
}

The error is:

type error [M0120], cannot pattern match mutable field x

Access mutable fields directly instead:

let value = cell.x;  // Direct field access

Cannot Use in Spec Collections​

Mutable records cannot be elements of spec collections such as Set, Seq, Map, or Multiset:

mutrec-in-collection_reject.sr9
// Mutable records cannot be used in spec collections
persistent actor {
  type Cell = { var x : Int };

  public func bad() : async () {
    ghost {
      // ERROR: Set element type must be immutable
      let s : Set<Cell> = Set.empty();
    };
  };
}

The error is:

type error [M0242], Set element type must be immutable (field x is mutable; no var fields or mutable arrays)

This restriction exists because:

  • Set membership must be stable (mutable elements break equality)
  • Aliasing to collection elements creates unsound proof scenarios
  • Collection operations (insert, remove, contains) assume immutable identity

Arrays of Mutable Records​

Arrays of mutable records have a supported local lane, including cases where a mutable record owns a mutable array of mutable records:

type Cell = { var value : Nat };
type Box = { var items : [var Cell] };

let b : Box = { var items = [var { var value = 0 }] };

The limits are around unbounded aliasing and escape, not the existence of the array itself. Keep mutable-record arrays owned locally, add loop invariants when iterating, and avoid storing aliases in actor fields across awaits. When the shape becomes hard to prove, use a spec collection for the proof model and a runtime array for implementation state.

Aliasing Patterns​

Supported: Self-Aliased Calls​

Calling a function with the same object for multiple parameters:

add_to_both(cell, cell);  // Same object twice

Works when postconditions handle the c1 == c2 case.

Supported: Known-Distinct Calls​

Calling with objects guaranteed distinct:

let a : Cell = { var x = 0 };
let b : Cell = { var x = 0 };
swap(a, b);  // Fresh allocations are distinct

Supported: Explicit Preconditions​

Requiring disjointness when needed:

requires c1 != c2;  // Caller must prove distinct

Unsupported: Unbounded Aliasing​

The verifier cannot track aliasing across:

  • Arbitrary collections of mutable records
  • Recursive data structures with mutable nodes
  • Callbacks with captured mutable references

For these patterns, expose a smaller verified interface, add explicit disjointness preconditions, or use ghost modeling. If you need a proof-only boundary while developing a larger proof, prefer abstract declarations; reserve trusted declarations for assumptions you are intentionally accepting.

Common Mistakes​

Missing Conditional Postcondition​

// WRONG: assumes parameters are distinct
private func add(c1 : Cell, c2 : Cell) : ()
  ensures c1.x == old(c1.x) + 1;
  ensures c2.x == old(c2.x) + 1;  // Fails if c1 == c2
{
  c1.x := c1.x + 1;
  c2.x := c2.x + 1;
};

Fix: add guarded postconditions for the aliased case or require disjointness with requires c1 != c2.

Assuming Fresh After Escape​

// WRONG: Fresh escapes to field
let fresh : Cell = { var x = 0 };
actorField := fresh;  // fresh now aliases actor state
try { await pause(); } catch (_) {};
assert fresh.x == 0;  // Rejected/fails: fresh is now shared

Fix: do not keep or rely on mutable references after storing them in actor fields across an await; copy primitive fields first or re-read through actor state after the await.

See Also​

Summary​

  • Multiple variables can alias the same mutable record
  • The verifier uses conditional postconditions to handle both aliased and distinct cases
  • Fresh allocations are guaranteed distinct from each other and existing references
  • Use requires c1 != c2 to require disjointness when aliasing is not intended
  • Pattern matching on mutable fields is rejected
  • Mutable records cannot be spec collection elements
  • Aliasing behavior changes at await boundaries based on escape analysis