Update Functions

Update functions are public actor methods that execute through consensus. Use them for durable state changes, security-sensitive checks, and calls that may affect other canisters. They are the usual boundary for entry guards, actor invariants, and async interleaving.

Read an update method header as two interfaces at once. The deployed interface decides which external messages may enter through entry_requires. The proof interface decides what verified callers may assume through requires, ensures, reads, modifies, and invariants. Keeping those two roles separate is what prevents public methods from smuggling unverified caller assumptions into proofs.

Declaration Syntax

Update functions are declared with public func inside an actor:

public func methodName(params) : async ReturnType
  modifies field1, field2
  entry_requires runtime_precondition;
  requires precondition;
  ensures postcondition;
{
  // body
}

The async return type is required for public actor functions. The verifier treats any public func inside an actor as an update function unless it has the query modifier.

Basic Example

A simple counter with a verified increment operation:

update-basic.sr9

// Basic update function with postcondition
persistent actor Counter {
  var count : Nat = 0;

  // Update function: modifies state, goes through consensus
  public func increment() : async Nat
    modifies count
    ensures result == old(count) + 1;
    ensures count == result;
  {
    count += 1;
    count
  };
}

The verifier proves that:

1. count increases by exactly 1
2. The returned value equals the new count
3. The actor invariant (if any) is preserved

Contracts on Update Functions

Update functions support full contract specifications:

• entry_requires - Runtime entry guards for exported methods
• requires - Logical preconditions the verifier assumes after the entry guard
• ensures - Postconditions guaranteed after execution
• modifies - Fields the function may change
• reads - Fields the function reads (for framing)

update-with-requires.sr9

// Update function with precondition and postcondition
persistent actor Wallet {
  var balance : Nat = 0;

  invariant balance <= 1_000_000;

  // Precondition ensures caller provides valid input
  public func deposit(amount : Nat) : async ()
    modifies balance
    entry_requires amount > 0 and balance + amount <= 1_000_000;
    requires amount > 0;
    requires balance + amount <= 1_000_000;
    ensures balance == old(balance) + amount;
  {
    balance += amount;
  };

  // Precondition prevents underflow
  public func withdraw(amount : Nat) : async ()
    modifies balance
    entry_requires amount <= balance;
    requires amount <= balance;
    ensures balance == old(balance) - amount;
  {
    balance -= amount;
  };
}

The guards and preconditions protect against:

• Invalid inputs (amount > 0)
• Invariant violations (balance + amount <= 1_000_000)
• Underflow (amount <= balance)

For public actor methods, nontrivial requires clauses need matching entry_requires guards. The runtime guard rejects invalid external calls before the method body runs; the logical precondition is the proof fact used by the verifier. Use entry_requires true only when invariants and trusted entry state justify the logical precondition without caller input. If the fact depends on a message argument, caller identity, current balance, authorization role, or any other external-entry condition, put it in entry_requires.

The modifies Clause

The modifies clause declares which actor fields an update function may change. This is essential for verification:

public func setBalance(newBalance : Nat) : async ()
  modifies balance
  ensures balance == newBalance;
{
  balance := newBalance;
};

Rules:

• List all fields the function writes to
• Fields not in modifies are framed (proven unchanged)
• Missing a field in modifies causes a permission error

Framing with reads and modifies

When a function reads a field but does not modify it, list it in reads. The verifier then proves that field remains unchanged:

update-multiple-fields.sr9

// Update function modifying multiple fields
persistent actor Position {
  var x : Int = 0;
  var y : Int = 0;

  // Modifies both coordinates
  public func move(dx : Int, dy : Int) : async ()
    modifies x, y
    ensures x == old(x) + dx;
    ensures y == old(y) + dy;
  {
    x += dx;
    y += dy;
  };

  // Modifies only x, y is framed (unchanged)
  public func moveX(dx : Int) : async ()
    reads y
    modifies x
    ensures x == old(x) + dx;
    ensures y == old(y);  // Framing: y unchanged
  {
    x += dx;
  };

  // Swap coordinates
  public func swap() : async ()
    modifies x, y
    ensures x == old(y);
    ensures y == old(x);
  {
    let temp = x;
    x := y;
    y := temp;
  };
}

In moveX, the reads y clause means:

• The function can read y
• The function cannot modify y
• The verifier can frame y across the function body

Calling Private Functions

Update functions can call private helper functions. The verifier uses the helper's contracts to reason about the public function:

update-calling-private.sr9

// Update function calling private helpers
persistent actor BoundedCounter {
  var count : Nat = 0;
  let MAX : Nat = 100;

  invariant count <= MAX;

  // Private helper with its own contract
  private func doIncrement() : Nat
    reads MAX
    modifies count
    requires count < MAX;
    ensures result == old(count) + 1;
    ensures count == result;
  {
    count += 1;
    count
  };

  // Public update function uses the helper
  public func increment() : async Nat
    reads MAX
    modifies count
    entry_requires count < MAX;
    requires count < MAX;
    ensures result == old(count) + 1;
  {
    doIncrement()
  };

  public func addN(n : Nat) : async Nat
    reads MAX
    modifies count
    entry_requires count + n <= MAX;
    requires count + n <= MAX;
    ensures count == old(count) + n;
    ensures result == count;
  {
    var i = 0;
    while (i < n) {
      loop:invariant i >= 0 and i <= n;
      loop:invariant count == old(count) + i;
      loop:invariant count + (n - i) <= MAX;
      ignore doIncrement();
      i += 1;
    };
    count
  };
}

When increment calls doIncrement:

1. The verifier checks that increment satisfies doIncrement's precondition (count < MAX)
2. The verifier assumes doIncrement's postcondition holds after the call

This modular approach keeps proofs tractable for complex functions.

The same modular discipline applies to imported actors and shared interfaces: the caller should rely on the callee's declared contract surface, not on an unstated expectation about its implementation. For proof-enabled cross-canister boundaries, use sr9 shared methods and the digital asset proof flow.

Actor Invariants

Update functions automatically interact with actor invariants:

Point	Behavior
Entry	Invariant is assumed to hold
Exit	Invariant must be proven to hold

persistent actor {
  var balance : Nat = 0;

  invariant balance <= 1_000_000;

  // Invariant is assumed at entry, proven at exit
  public func deposit(amount : Nat) : async ()
    modifies balance
    entry_requires balance + amount <= 1_000_000;
    requires balance + amount <= 1_000_000;
  {
    balance += amount;
    // Verifier proves: balance <= 1_000_000
  };
}

The entry guard rejects calls that would break the invariant; the matching logical precondition lets the verifier prove the invariant is preserved. For richer state relationships, keep the invariant in one place and use helper contracts to prove each transition locally.

Return Types

Update functions must return an async type:

// Returns a value
public func getValue() : async Nat { ... }

// Returns unit
public func doSomething() : async () { ... }

The async type indicates that:

• The call goes through consensus
• The caller must await the result
• State changes commit at message/await boundaries; code between await points is atomic

See await and interleaving for the proof rules around suspension.

Shared Type Restrictions

Update function parameters and return types must be shared types. Shared types can be serialized across the network:

Allowed:

• Primitives: Nat, Int, Bool, Text, Float, Principal, Blob
• Containers: ?T, [T], tuples, records, variants (if element types are shared)
• Actor references whose interface contains only shared functions

Not allowed:

• Functions (cannot serialize closures)
• Mutable arrays ([var T] in parameters)
• Modules
• Non-shared async types

// Error M0031: shared function has non-shared parameter type
public func bad(f : Nat -> Nat) : async () { };

// Correct: use only shared types
public func good(n : Nat) : async Nat { n + 1 };

Common Mistakes

Missing modifies Clause

Forgetting to declare modified fields causes a permission error:

Wrong

// Error: Missing modifies clause
persistent actor {
  var counter : Nat = 0;

  // Error: modifies field without declaring it
  public func increment() : async ()
    // Missing: modifies counter
    ensures counter == old(counter) + 1;
  {
    counter += 1;  // Permission error: no modifies counter
  };
}

Correct

persistent actor {
var counter : Nat = 0;

public func increment() : async ()
  modifies counter  // Declare the modified field
  ensures counter == old(counter) + 1;
{
  counter += 1;
};
}

Missing async Return Type

Public actor functions must return async types:

// Error M0035: shared function must have return type '()' or 'async <typ>'
persistent actor {
  public func bad() : Nat { 42 };
}

// Correct
persistent actor {
  public func good() : async Nat { 42 };
}

Non-Shared Parameter Types

Parameters must be serializable:

// Error M0031: shared function has non-shared parameter type
persistent actor {
  public func bad(callback : Nat -> Nat) : async Nat {
    callback(42)
  };
}

Functions cannot be passed to update functions because they cannot be serialized across the network.

Use reads for fields you inspect without changing, and modifies for fields you assign or pass to mutating helpers.

Calling Update Functions from Queries

Query functions cannot call update functions:

// Error M0188: cannot call a shared function from a query function
persistent actor {
  var count : Nat = 0;

  public func increment() : async () modifies count {
    count += 1;
  };

  public query func badQuery() : async Nat reads count {
    await increment();  // Error: queries cannot call updates
    count
  };
}

Use a regular update function for durable state changes.

Update vs Query Functions

Aspect	Update Function	Query Function
Declaration	public func	public query func
State modification	Durable (modifies)	Non-consensus; prefer read-only, declare modifies if written
Consensus	Yes (slower)	No (faster)
Invariant checking	At entry and exit	At entry and exit

Use query functions for read-only operations to improve performance. See Query Functions for details.

Verification Across Await

When an update function contains await, the verifier models potential interference from other calls:

persistent actor {
  var balance : Nat = 0;

  invariant balance >= 0;

  public func transfer(amount : Nat) : async ()
    modifies balance
    entry_requires amount <= balance;
    requires amount <= balance;
  {
    balance -= amount;
    try { await someOtherCall(); } catch (_) {};
    // After await: balance may have changed!
    // Only the invariant (balance >= 0) is guaranteed
  };
}

Before each suspending await, the method must re-establish actor invariants. After the await resumes, exact actor-field values should be treated as stale unless they are protected by invariants, fresh local snapshots, or precise frame reasoning. See Await Expressions and Async Frames for the detailed rules.

After an await:

• Actor invariants are re-assumed
• Local variables that don't escape remain stable
• Field values may have changed (other calls could have executed)

See Async Verification for detailed coverage.

Summary

• Update functions are public func methods that can modify actor state
• Declare modified fields with modifies and read-only fields with reads
• Use entry_requires for runtime guards on exported methods and matching requires clauses for proof facts
• Use ensures to specify postconditions the function guarantees
• Actor invariants are automatically checked at method boundaries
• Parameters and return types must be shared (serializable) types
• Update functions go through consensus, making them slower than queries
• Use private helper functions with contracts for modular verification

Related Topics

• Entry requires for exported runtime guards
• Modifies clauses for write permissions
• Commit points for when update changes become permanent
• Caller identity for access control