Mutable Record Types

Records with var fields are mutable records. They use reference semantics, so the verifier tracks access with permissions and generated ownership predicates.

What Makes a Record Mutable

A record is mutable if it has at least one var field. Compare:

// Immutable record: no var fields
type Point = { x : Int; y : Int };

// Mutable record: has var fields
type Cell = { var x : Int };

This distinction changes both runtime behavior and the verification encoding:

Aspect	Immutable Record	Mutable Record
Semantics	Value	Reference
Updates	Replace entire value	Modify individual fields
Viper encoding	ADT (algebraic data type)	Heap reference with ownership
Permission tracking	Implicit	Generated Owned$MutRec$... predicates

Declaring and Using Mutable Records

Use var before the field name to make it mutable:

mutrec-basic.sr9

// Basic mutable record definition and field access
persistent actor {
  // A mutable record: has at least one var field
  type Cell = { var x : Int };

  // Create a mutable record
  var cell : Cell = { var x = 0 };

  // Read a field
  private func getValue() : Int
    reads cell
    ensures result == cell.x;
  {
    cell.x
  };

  // Write a field
  private func setValue(v : Int) : ()
    modifies cell
    ensures cell.x == v;
  {
    cell.x := v;
  };

  public func demo(v : Int) : async Int
    modifies cell
    ensures cell.x == v;
    ensures result == v;
  {
    setValue(v);
    getValue()
  };
}

Key points:

• type Cell = { var x : Int } defines a mutable record type
• { var x = 0 } creates a mutable record instance
• Field access uses dot notation: cell.x
• Field assignment uses := operator: cell.x := v

Mutable vs Immutable Records

The key difference is how you update them:

mutrec-vs-immutable.sr9

// Comparison: mutable vs immutable records
persistent actor {
  // Immutable record: no var fields, value semantics
  type Point = { x : Int; y : Int };

  // Mutable record: has var fields, reference semantics
  type Cell = { var x : Int; var y : Int };

  var point : Point = { x = 0; y = 0 };
  var cell : Cell = { var x = 0; var y = 0 };

  // Immutable records: replace the entire value
  private func movePoint(dx : Int, dy : Int) : ()
    modifies point
    ensures point.x == old(point.x) + dx;
    ensures point.y == old(point.y) + dy;
  {
    point := { x = point.x + dx; y = point.y + dy };
  };

  // Mutable records: update individual fields
  private func moveCell(dx : Int, dy : Int) : ()
    modifies cell
    ensures cell.x == old(cell.x) + dx;
    ensures cell.y == old(cell.y) + dy;
  {
    cell.x := cell.x + dx;
    cell.y := cell.y + dy;
  };

  public func moveBoth(dx : Int, dy : Int) : async ()
    modifies point, cell
    ensures point.x == old(point.x) + dx;
    ensures point.y == old(point.y) + dy;
    ensures cell.x == old(cell.x) + dx;
    ensures cell.y == old(cell.y) + dy;
  {
    movePoint(dx, dy);
    moveCell(dx, dy);
  };
}

For immutable records, you must create a new record with updated values. For mutable records, you update fields in place.

This affects verification: mutable records require the verifier to track which code has permission to access each field. Immutable records are values; mutable records are heap objects.

Mutable Records as Parameters

When you pass a mutable record to a function, the function receives a reference to the original:

mutrec-parameter.sr9

// Mutable records as function parameters
persistent actor {
  type Cell = { var x : Int };

  // Functions can take mutable records by reference
  private func increment(c : Cell) : ()
    ensures c.x == old(c.x) + 1;
  {
    c.x := c.x + 1;
  };

  // Multiple parameters
  private func swap(c1 : Cell, c2 : Cell) : ()
    ensures c1.x == old(c2.x);
    ensures c2.x == old(c1.x);
  {
    let tmp = c1.x;
    c1.x := c2.x;
    c2.x := tmp;
  };

  // Using the functions
  var a : Cell = { var x = 10 };
  var b : Cell = { var x = 20 };

  public func run() : async () modifies a, b {
    increment(a);
    assert a.x == 11;
    swap(a, b);
    assert a.x == 20;
    assert b.x == 11;
  };
}

Modifications through the parameter affect the original record. This is pass-by-reference semantics, so contracts should say whether the callee reads or changes the fields it receives. Actor fields still use the ordinary reads and modifies clauses.

Multiple Fields

Mutable records can have any number of var fields. Contracts can specify which fields change:

mutrec-multifield.sr9

// Mutable records with multiple fields
persistent actor {
  type Counter = {
    var value : Int;
    var limit : Int;
  };

  var counter : Counter = { var value = 0; var limit = 100 };

  // Update specific fields
  private func increment() : ()
    modifies counter
    requires counter.value < counter.limit;
    ensures counter.value == old(counter.value) + 1;
    ensures counter.limit == old(counter.limit);
  {
    counter.value := counter.value + 1;
  };

  // Reset value but preserve limit
  private func reset() : ()
    modifies counter
    ensures counter.value == 0;
    ensures counter.limit == old(counter.limit);
  {
    counter.value := 0;
  };

  // Set new limit
  private func setLimit(newLimit : Int) : ()
    modifies counter
    requires newLimit >= 0;
    ensures counter.limit == newLimit;
    ensures counter.value == old(counter.value);
  {
    counter.limit := newLimit;
  };

  public func demo(newLimit : Int) : async ()
    modifies counter
    entry_requires newLimit > 0;
    requires newLimit > 0;
    ensures counter.value == 0;
    ensures counter.limit == newLimit;
  {
    reset();
    setLimit(newLimit);
    increment();
    reset();
  };
}

Notice how each function specifies exactly which fields change and which stay the same. The verifier tracks permissions per field.

How the Verifier Handles Mutable Records

Under the hood, the verifier uses ownership predicates to track permissions. For a type like { var x : Int; var y : Int }:

1. The verifier generates an Owned$MutRec$HASH predicate
2. This predicate bundles permissions for all fields
3. Field access opens the predicate to expose the field permissions
4. After access, the predicate is closed again

This is inserted by the verifier, not written in Sector9, but it explains error messages that mention Owned$MutRec. See Ownership Predicates for details.

Restrictions

Cannot Pattern-Match Mutable Fields

Pattern matching on var fields is rejected. A mutable field is a heap location, not a value field that can safely be destructured by a pattern:

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

Instead, access fields directly:

let value = cell.x;  // Correct: direct field access

Cannot Use in Spec Collections

Mutable records cannot be keys or 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)

Spec collections require spec-immutable elements because:

• membership and map keys must be stable
• mutable elements would let equality change after insertion
• aliases to collection elements would create unsound proof scenarios

Mutable Arrays Affect Spec-Immutability

A record containing a mutable array ([var T]) is not spec-immutable even if no fields are declared var:

// This is rejected by spec collections because data is mutable
type Container = { data : [var Int] };

Such types cannot be used in spec collections. They may still be usable in ordinary verified code when they fit the current owned/local mutable-data lane.

Mixed Mutability

A record can have both mutable and immutable fields:

type Account = {
  id : Nat;           // immutable: identity never changes
  var balance : Int;  // mutable: balance can change
};

The record is still a mutable record because it has at least one var field.

Common Patterns

Mutable Cell Pattern

Use a mutable record when you need pass-by-reference semantics:

type Ref<T> = { var value : T };

private func modify(r : Ref<Int>) : ()
  ensures r.value == old(r.value) + 1;
{
  r.value := r.value + 1;
};

State Object Pattern

Group related mutable state into a record:

type TokenState = {
  var supply : Nat;
  var paused : Bool;
};

var state : TokenState = { var supply = 0; var paused = false };

private func mint(amount : Nat) : ()
  modifies state
  requires not state.paused;
  ensures state.supply == old(state.supply) + amount;
{
  state.supply := state.supply + amount;
};

Summary

• A record is mutable if it has at least one var field
• Mutable records use reference semantics: updates modify in place
• Passing a mutable record to a function gives the function access to the original
• The verifier tracks permissions using ownership predicates (invisible to you)
• Mutable records cannot be pattern-matched or used in spec collections
• Records containing mutable arrays are not spec-immutable

Related Topics

• Ownership predicates for the verifier mechanism
• Aliasing restrictions for self-aliased calls and disjointness
• Spec collection restrictions for immutable element requirements