Actor Fields

Actor fields store canister state across method calls. In a persistent actor, ordinary fields also participate in upgrade persistence, while transient fields reset on upgrade. Mutable fields are the main heap roots the verifier tracks with reads, modifies, permissions, and actor invariants.

Declaring Fields

Fields are declared inside the actor body using var for mutable state or let for constants:

persistent actor {
  var counter : Nat = 0;      // Mutable field
  let maxValue : Nat = 1000;  // Immutable constant
}

Every field requires:

• A type annotation (: Nat)
• An initializer (= 0)

Mutable Fields with var

Mutable fields hold state that changes over time. They form the core of actor functionality:

persistent actor {
  var balance : Int = 0;
  var active : Bool = true;

  public func deposit(amount : Nat) : async ()
    modifies balance
    ensures balance == old(balance) + amount;
  {
    balance += amount;
  };
}

When you modify a field, you must declare it in the modifies clause. This tells the verifier which fields may change.

Immutable Fields with let

Use let for configuration values that never change:

field-immutable.sr9

// Immutable fields with let
persistent actor Config {
  // Immutable configuration
  let maxBalance : Nat = 1000;
  let minWithdraw : Nat = 10;

  var balance : Nat = 0;

  public func deposit(amount : Nat) : async Bool
    modifies balance
    reads maxBalance
    entry_requires amount > 0;
    requires amount > 0;
    ensures result == (old(balance) + amount <= maxBalance);
    ensures result ==> balance == old(balance) + amount;
    ensures (not result) ==> balance == old(balance);
  {
    if (balance + amount <= maxBalance) {
      balance += amount;
      true
    } else {
      false
    }
  };
}

Immutable fields:

• Cannot appear in modifies clauses
• Remain constant across all method calls
• Provide automatic framing. Spec-immutable actor let fields are treated as implicit reads, while mutable or heap-like fields still need explicit footprints when accessed through methods.

Field Types

Actor fields support many types:

Type Category	Examples	Notes
Numbers	Nat, Int, Nat64, Int32	Unbounded and fixed-width
Text	Text, Char	Unicode strings and characters
Boolean	Bool	true or false
Records	{ x : Int; y : Int }	Named field collections
Tuples	(Int, Bool)	Positional collections
Arrays	[var Int], [Int]	Mutable or immutable
Variants	{ #ok : T; #err : E }	Tagged unions
Options	?Nat	Nullable values

field-types.sr9

// Actor fields with different types
persistent actor FieldTypes {
  // Primitive types
  var counter : Nat = 0;
  var balance : Int = 100;
  var active : Bool = true;
  var name : Text = "Account";

  // Composite types
  var position : { x : Int; y : Int } = { x = 0; y = 0 };
  var data : [var Int] = [var 1, 2, 3];

  public func getCounter() : async Nat
    reads counter
    ensures result == counter;
  {
    counter
  };

  public func getPosition() : async { x : Int; y : Int }
    reads position
    ensures result == position;
  {
    position
  };
}

Record Fields

Records group related values together:

field-record.sr9

// Record field with multiple properties
persistent actor Point2D {
  var point : { x : Int; y : Int } = { x = 0; y = 0 };

  public func move(dx : Int, dy : Int) : async ()
    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 };
  };

  public func getX() : async Int
    reads point
    ensures result == point.x;
  {
    point.x
  };

  public func getY() : async Int
    reads point
    ensures result == point.y;
  {
    point.y
  };
}

Record updates require replacing the entire record. You cannot update a single field in place unless the record itself has mutable (var) fields.

Array Fields

Mutable arrays store indexed collections:

field-array.sr9

// Mutable array field
persistent actor ArrayStorage {
  var items : [var Int] = [var 0, 0, 0];

  public func get(index : Nat) : async Int
    reads items
    entry_requires index < items.size();
    requires index < items.size();
    ensures result == items[index];
  {
    items[index]
  };

  public func set(index : Nat, value : Int) : async ()
    modifies items
    entry_requires index < items.size();
    requires index < items.size();
    ensures items[index] == value;
  {
    items[index] := value;
  };

  public func getSize() : async Nat
    reads items
    ensures result == items.size();
  {
    items.size()
  };
}

Key points:

• Use [var T] for mutable arrays (elements can be updated)
• Use [T] for immutable arrays (read-only after creation)
• Array bounds must be verified explicitly with requires index < arr.size(); exported methods should pair that logical precondition with entry_requires
• Deep-mutable actor fields such as nested arrays remain a restricted verification surface; prefer flat fields or spec-collection models for proofs

Ghost Fields

Ghost fields exist only for verification and are erased from runtime code:

field-ghost.sr9

// Ghost field for verification-only tracking
persistent actor DepositTracker {
  var balance : Nat = 0;
  ghost var totalDeposited : Nat = 0;

  invariant balance <= totalDeposited;

  public func deposit(amount : Nat) : async ()
    modifies balance, totalDeposited
    entry_requires amount > 0;
    requires amount > 0;
    ensures balance == old(balance) + amount;
  {
    balance += amount;
    ghost { totalDeposited += amount; };
  };

  public func withdraw(amount : Nat) : async Bool
    modifies balance
    entry_requires amount > 0;
    requires amount > 0;
    ensures result == (old(balance) >= amount);
    ensures result ==> balance == old(balance) - amount;
    ensures (not result) ==> balance == old(balance);
  {
    if (balance >= amount) {
      balance -= amount;
      true
    } else {
      false
    }
  };
}

Ghost fields:

• Declared with ghost var
• Updated inside ghost { } blocks
• Cannot be read or written in runtime code
• Useful for tracking abstract properties (totals, histories, permissions)

See Ghost Variables for details.

Field Permissions

The verifier tracks which fields each method reads and writes:

Clause	Permission	Effect
modifies x	Write	Can read and modify x
reads x	Read	Can only read x
(neither)	None	Cannot access mutable actor field x

A field in modifies implicitly grants read permission. You do not need both clauses for the same field.

public func transfer(amount : Nat) : async ()
  reads maxBalance      // Read-only access
  modifies balance      // Read and write access
  entry_requires balance + amount <= maxBalance;
  requires balance + amount <= maxBalance;
{
  balance += amount;
};

Missing permissions cause translation errors:

// Error: modifies clause missing fields: counter
public func bad() : async () {
  counter += 1;  // Writes without declaring modifies
};

See Footprints for complete coverage.

Multiple Fields

Actors commonly have multiple related fields. The verifier tracks each independently:

field-multiple.sr9

// Multiple fields with conservation invariant
persistent actor TokenVault {
  var available : Nat = 100;
  var locked : Nat = 0;

  invariant available + locked == 100;

  public func lock(amount : Nat) : async Bool
    modifies available, locked
    ensures result == (old(available) >= amount);
    ensures result ==> available == old(available) - amount;
    ensures result ==> locked == old(locked) + amount;
    ensures (not result) ==> available == old(available);
    ensures (not result) ==> locked == old(locked);
  {
    if (available >= amount) {
      available -= amount;
      locked += amount;
      true
    } else {
      false
    }
  };

  public func unlock(amount : Nat) : async Bool
    modifies available, locked
    ensures result == (old(locked) >= amount);
    ensures result ==> available == old(available) + amount;
    ensures result ==> locked == old(locked) - amount;
    ensures (not result) ==> available == old(available);
    ensures (not result) ==> locked == old(locked);
  {
    if (locked >= amount) {
      locked -= amount;
      available += amount;
      true
    } else {
      false
    }
  };
}

The invariant available + locked == 100 relates both fields. The verifier ensures this relationship holds after every public method.

Field Initialization

Field initializers run when the actor is created. The verifier checks that initial values satisfy all invariants:

persistent actor {
  var balance : Int = 100;
  var limit : Int = 50;

  invariant balance >= limit;  // Holds: 100 >= 50
}

If initialization violates an invariant, verification fails:

persistent actor {
  var balance : Int = 0;
  var limit : Int = 50;

  invariant balance >= limit;  // Fails: 0 < 50
}

The $Self Reference

When reading verifier output, you may see references like $Self.balance. This internal notation represents the actor instance:

• $Self is the current actor
• $Self.balance is the balance field on that actor
• acc($Self.balance, write) means write permission to the field

You write code using field names directly. The $Self notation appears only in error messages and generated Viper code.

Transient Fields

Some fields need to stay available across method calls but do not need to survive upgrades. Mark them with transient:

persistent actor {
  var balance : Nat = 0;               // Stable in a persistent actor
  transient var cache : [Nat] = [];    // Reset on upgrade
}

Transient fields:

• Reset to their initial value after upgrade
• Useful for caches, temporary state, or derived data
• Still follow the same verification rules as persistent fields
• Still persist for ordinary message execution; transient only changes upgrade behavior

Common Mistakes

Accessing Fields Without Permission

Every field access requires a reads or modifies declaration:

Wrong

public func check() : async Bool {
  balance > 0  // Error: missing reads clause
};

Correct

public func check() : async Bool
  reads balance
{
  balance > 0
};

Modifying Without Declaration

Writes require modifies:

Wrong

public func reset() : async () {
  counter := 0;  // Error: missing modifies clause
};

Correct

public func reset() : async ()
  modifies counter
{
  counter := 0;
};

Mutable State in Modules

Modules cannot have mutable fields. Only actors support persistent state:

// Error M0014: non-static expression in module
module {
  var counter : Nat = 0;  // Wrong - modules are stateless
}

Use actors for mutable state, modules for stateless logic.

Ghost Blocks Mutating Runtime Fields

Ghost code cannot modify runtime fields:

// Error: ghost block mutating non-ghost field 'balance'
public func bad() : async () modifies balance {
  ghost { balance := 0; };  // Wrong - unsound
};

Ghost blocks can only update ghost variables.

Summary

• Fields store actor state using var (mutable) or let (immutable)
• In persistent actors, ordinary fields are stable across upgrades and transient fields reset
• Every field needs a type annotation and initializer
• Declare modifies for writes, reads for read-only access
• Use ghost var for verification-only state
• Field initializers must satisfy all invariants
• Modules cannot have mutable fields; use actors for state
• $Self.field notation appears only in verifier output

Related Topics

• Modifies clauses and reads clauses for actor field permissions
• Ghost variables for proof-only state
• Stable variables for upgrade-persistent fields
• Arrays for array permissions and bounds
• Actor invariants for relationships over fields