Deep Aliasing

Sector9 supports basic aliasing for mutable records and arrays, but deep aliasing patterns are out of scope. This page explains what is not supported and how to work around these limitations.

What Deep Aliasing Means

Shallow aliasing is when two variables reference the same mutable object directly:

let c1 : Cell = { var x = 0 };
let c2 = c1;  // c2 aliases c1

Deep aliasing involves chains of references, nested mutable structures, or aliasing within collections:

// Deep chain: outer.middle.inner may alias other.middle.inner
// Nested arrays: matrix[i] may alias matrix[j]
// Collection aliasing: elements within a set may alias external references

The verifier handles shallow aliasing through conditional postconditions. Deep aliasing requires ownership tracking that compounds exponentially with nesting depth.

Unsupported Patterns

Deep Mutable Chains

Mutable records nested inside other mutable records create aliasing chains the verifier cannot fully track. The snippet below is intentionally descriptive: the problem is not the type declaration alone, but using deeply nested mutable identity as shared verified state.

aliasing-deep-chain_reject.sr9

// Deep aliasing through field chains is out of scope
module {
  type Inner = { var value : Int };
  type Middle = { var inner : Inner };
  type Outer = { var middle : Middle };

  // The verifier cannot track aliasing through
  // deep field chains like outer.middle.inner
  // This limitation exists because:
  // - Ownership predicates would need to unfold recursively
  // - Aliasing relationships at each level compound complexity
}

The limitation exists because:

• Ownership predicates would need recursive unfolding at each level
• Aliasing relationships at each level compound the complexity
• The verifier uses finite unfolding depth to ensure termination

Keep Mutable Fields Shallow

Verified code is most predictable when mutable fields contain shallow payloads. The verifier has targeted support for direct mutable records and arrays, plus fresh local deep-mutable values that do not escape. Nested mutable payloads in actor or module fields remain restricted, especially when they are hidden inside other containers.

// Avoid: nested mutable identity hidden inside an actor field
type Wrapper = { var inner : { var x : Int } };

Nested Mutable Arrays

Arrays of arrays with mutable elements are not supported as shared verified state. The snippet is descriptive because the restriction is about the escaped actor/module state shape, not a standalone comment-only module:

aliasing-nested-array_reject.sr9

// Nested mutable arrays are out of scope
module {
  // This pattern is unsupported:
  // var matrix : [var [var Int]] = [var [var 1, 2], [var 3, 4]];
  //
  // The verifier cannot express ownership predicates for:
  // - Arbitrary-length outer array
  // - Arbitrary-length inner arrays at each index
  // - Aliasing between inner arrays (matrix[0] == matrix[1]?)
  //
  // Use alternative patterns:
  // - Flattened 1D array with computed indices
  // - Fixed-size record with named fields
  // - Ghost modeling for verification
}

The verifier cannot express ownership for:

• Arbitrary-length outer arrays
• Arbitrary-length inner arrays at each index
• Potential aliasing between inner arrays (matrix[0] == matrix[1]?)

Mutable Elements in Spec Collections

Mutable records and arrays cannot be elements of Set, Seq, Map, or Multiset:

aliasing-collection-reject.sr9

// Mutable records and arrays cannot be spec collection elements
module {
  type Cell = { var x : Int };

  // These are rejected (M0242):
  // let s : Set<Cell> = Set.empty();
  // let m : Map<Nat, Cell> = Map.empty();
  // let seq : Seq<[var Int]> = Seq.empty();

  // Reason: Spec collections require immutable elements.
  // Mutable content would create:
  // - Aliasing to collection contents
  // - Identity instability (mutable elements break equality)
  // - Unsound proof scenarios when modifying elements
}

This restriction (error M0242) exists because spec collections require spec-immutable key, value, and element types:

• Spec collections are immutable ghost state
• Mutable elements break identity stability
• Aliasing to collection contents creates unsound proofs

Escape Analysis Limitations

The verifier uses flow-insensitive escape analysis. This is sound but may be imprecise:

aliasing-escape-limit.sr9

// Flow-insensitive escape analysis may over-approximate
persistent actor {
  type Cell = { var x : Int };
  var stored : Cell = { var x = 0 };

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

  public func example(condition : Bool) : async ()
    modifies stored
  {
    let fresh : Cell = { var x = 10 };

    if (condition) {
      stored := fresh;  // Fresh escapes in one branch
    };

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

    // Fresh is treated as shared even if condition is false.
    // The escape analysis is flow-insensitive: it considers
    // all possible executions, not actual control flow.
    // This is sound but may be imprecise.

    // To preserve freshness, ensure no escape path exists:
    // let separate : Cell = { var x = 20 };
    // try { await pause(); } catch (_) {};
    // assert separate.x == 20;  // This works
  };
}

Flow-insensitive means the analysis considers all possible execution paths, not the actual control flow. A fresh allocation that escapes in any branch is treated as shared in all branches.

Three Ownership Categories

The escape analysis classifies objects into three categories:

Category	Description	Across Await
Actor-rooted	Actor fields and reachable objects	Invalidated
Fresh allocation	Objects created in current method	Preserved if no escape
Unknown/external	Values from external calls	Invalidated

Only fresh allocations that never escape remain stable across await boundaries.

Workarounds

Flatten Nested Structures

Instead of nested mutable arrays, use a flat array with computed indices:

aliasing-workaround-flat.sr9

// Workaround: flatten nested structures
persistent actor {
  // Instead of nested mutable arrays:
  // var matrix : [var [var Int]] = ...;

  // Use a flat array with computed indices:
  var flat : [var Int] = [var 0, 0, 0, 0];  // 2x2 matrix
  invariant flat.size() == 4;

  pure func index(row : Nat, col : Nat) : Nat {
    row * 2 + col
  };

  public func get(row : Nat, col : Nat) : async Int
    reads flat
    entry_requires row < 2 and col < 2;
    requires row < 2 and col < 2;
  {
    flat[index(row, col)]
  };

  public func set(row : Nat, col : Nat, value : Int) : async ()
    modifies flat
    entry_requires row < 2 and col < 2;
    requires row < 2 and col < 2;
  {
    flat[index(row, col)] := value;
  };
}

The flat representation eliminates nested aliasing concerns while providing equivalent functionality.

Use Ghost State for Verification

Model complex structures with ghost state that mirrors runtime behavior:

aliasing-workaround-ghost.sr9

// Workaround: use ghost state for verification
persistent actor {
  // Runtime: mutable data structure
  var data : [var Int] = [var 0, 0, 0];

  // Ghost: verification model
  ghost var model : Seq<Int> =
    Seq.concat(Seq.concat(Seq.singleton(0), Seq.singleton(0)), Seq.singleton(0));

  invariant data.size() == 3;
  invariant Seq.len(model) == data.size();

  public func update(i : Nat, value : Int) : async ()
    modifies data, model
    entry_requires i < 3;
    requires i < 3;
    ensures Seq.get(model, i) == value;
  {
    data[i] := value;
    ghost {
      model := Seq.update(model, i, value);
    };
  };

  public func sum() : async Int
    reads data, model
    ensures result == Seq.get(model, 0) + Seq.get(model, 1) + Seq.get(model, 2);
  {
    data[0] + data[1] + data[2]
  };
}

The ghost Seq tracks the logical state while the runtime array holds actual data. Invariants connect them.

Use Fixed-Size Records

Replace variable-length nested structures with fixed-size records:

// Instead of: var matrix : [var [var Int]]
// Use named fields for known dimensions:
type Matrix2x2 = {
  var a00 : Int; var a01 : Int;
  var a10 : Int; var a11 : Int;
};

Named fields have explicit ownership that the verifier can track.

Mark Complex Code as Trusted

When deep aliasing is unavoidable, mark functions as trusted:

public trusted func processComplexStructure(data : ComplexType) : ()
  ensures someProperty(data);
{
  // Body not verified, but contract is assumed
  ...
};

This expands your trusted base, so use sparingly and document assumptions.

What Is Supported

For contrast, these aliasing patterns are supported:

Pattern	Description	Support
Shallow mutable record aliasing	let c2 = c1 where c1 : Cell	Conditional postconditions
Self-aliased calls	f(cell, cell)	Partition inference
Explicit disjointness	requires c1 != c2	Direct precondition
Fresh allocation disjointness	New objects are distinct	Automatic
Single-level array elements	arr[i] for flat arrays	Indexed heap model
Actor field aliasing at await	Invalidation model	Escape analysis

If the verifier cannot prove disjointness (for example, two parameters might alias), it rejects the call. Add an explicit requires a != b or refactor to use fresh allocations.

See Mutable Records Aliasing and Local vs Shared State for details on supported patterns.

Why This Limitation Exists

The core challenge is ownership tracking. The verifier uses ownership predicates (like Owned$Cell$...) to track permission to access mutable state. These predicates must be:

1. Folded and unfolded - accessing a field requires unfolding, then refolding
2. Exclusive - only one owner can have write permission
3. Finite - the verifier must terminate

Deep aliasing requires tracking ownership at multiple levels simultaneously. For a chain like a.b.c.d, the verifier would need to unfold permissions at each level, track potential aliasing at each level, and refold in the correct order. The combinatorial explosion makes this intractable for arbitrary depth.

Practical Guidance

Situation	Recommendation
Direct mutable records and arrays	Supported when ownership is explicit and shallow
Fresh local deep-mutable values	Supported only if they do not escape
Deeply nested actor/module state	Flatten or use ghost modeling
Arrays of mutable records	Use primitive arrays with reconstruction
Mutable records in collections	Use ghost Map/Set of immutable keys
Complex graph structures	Mark as trusted or model abstractly

Summary

• Deep aliasing in persistent actor/module state is restricted
• The verifier uses flow-insensitive escape analysis, which is sound but may over-approximate
• Mutable elements cannot appear in spec collections (error M0242)
• Workarounds: flatten structures, use ghost state, use fixed-size records, or mark as trusted
• Shallow aliasing for mutable records is fully supported with conditional postconditions