Skip to main content

The modifies Clause

The modifies clause declares which actor fields a function may change.

Overview​

When a function modifies actor state, you must declare which fields it changes using modifies. This serves two purposes:

  1. Write permission: The verifier grants write access only to declared fields
  2. Framing guarantee: Fields outside modifies are not written by the function; callers can use that guarantee for fields they have permission to mention

Without a modifies clause, the verifier assumes the function writes nothing and will reject any field assignment.

Syntax​

The modifies clause appears in the function header, after the return type:

public func methodName() : async ReturnType
  modifies field1, field2
{
  // body
}

For multiple fields, separate them with commas. Private functions use the same syntax without async:

private func helper() : () modifies field1 {
  // body
}

Basic Usage​

modifies-basic.sr9
// Basic modifies clause usage
// Demonstrates field-level write permissions

persistent actor {
  var balance : Int = 0;
  var owner : Text = "alice";

  // Declares that this function may modify balance
  public func deposit(amount : Int) : async ()
    modifies balance
    entry_requires amount >= 0;
    requires amount >= 0;
    ensures balance == old(balance) + amount;
  {
    balance += amount;
  };

  // Multiple fields can be modified
  public func transfer(newOwner : Text, amount : Int) : async ()
    modifies balance, owner
    entry_requires amount >= 0;
    requires amount >= 0;
    ensures balance == old(balance) - amount;
    ensures owner == newOwner;
  {
    balance -= amount;
    owner := newOwner;
  };
}

Key points:

  • Each function lists the fields it may write
  • The verifier checks that actual writes stay within the declared set
  • old(balance) refers to the value at function entry

Framing: Unlisted Fields Are Unchanged​

The most powerful feature of modifies is automatic framing. When you declare modifies y, the verifier knows that all other fields remain unchanged.

modifies-framing.sr9
// Modifies and framing
// Fields NOT in modifies are guaranteed unchanged

persistent actor {
  var x : Int = 0;
  var y : Int = 0;

  // Only modifies y - x is automatically framed
  private func updateY(newVal : Int) : () modifies y {
    y := newVal;
  };

  // Caller can rely on x being unchanged
  public func test() : async () reads x modifies y {
    let x0 = x;
    updateY(42);
    assert x == x0;  // Verified: x is framed
  };
}

This works because:

  1. updateY declares modifies y
  2. The caller reads x before calling updateY
  3. Since x is not in the modifies set, the verifier preserves x == x0

Missing Modifies: A Common Error​

If you modify a field without declaring it, the verifier rejects the program:

modifies-missing_unsat.sr9
// Missing modifies clause
// This file demonstrates a verification error

persistent actor {
  var counter : Nat = 0;

  // ERROR: modifies clause missing fields: counter
  public func inc() : async () {
    counter += 1;  // Writes to counter without declaring it
  };
}

The error message tells you exactly which field is missing:

modifies clause missing fields: counter

The fix is to add the declaration:

public func inc() : async () modifies counter {
  counter += 1;
}

Modifies Does Not Require Change​

A field in modifies may be changed, but it does not have to be. This is safe and common:

private func maybeUpdate(flag : Bool) : () modifies x {
  if (flag) {
    x := x + 1;
  };
  // x unchanged if flag is false - still valid
}

However, this means callers cannot assume a field is unchanged just because the function did nothing in practice. The verifier treats modifies x as "x might change".

Interaction with Postconditions​

When you declare modifies, you can write postconditions that describe the new value:

public func increment() : async ()
  modifies counter
  ensures counter == old(counter) + 1;
{
  counter += 1;
}

For fields not in modifies but available through reads, the verifier automatically adds frame conditions. You can also write them explicitly:

public func updateX(newVal : Int) : async ()
  modifies x
  reads y
  ensures x == newVal;
  ensures y == old(y);  // Automatic, but explicit is fine
{
  x := newVal;
}

Transitive Effects Through Calls​

When function A calls function B, the effects compose. If B declares modifies x, then A must also declare modifies x (or a superset):

private func helper() : () modifies x {
  x := x + 1;
};

// Must include x in modifies because helper modifies x
public func caller() : async () modifies x {
  helper();
}

The verifier computes effect summaries across the call graph and validates that each function's modifies clause covers all transitively written fields.

Modifies with Arrays​

Array fields work the same as scalar fields:

persistent actor {
  var data : [var Int] = [var 1, 2, 3];
  var other : Int = 0;

  private func updateFirst() : () modifies data
    requires data.size() > 0;
    ensures data.size() == old(data.size());
  {
    data[0] := 100;
  };

  public func test() : async () reads other modifies data {
    let o0 = other;
    updateFirst();
    assert other == o0;  // other is framed
  };
}

When you declare modifies data, you get permission to modify any element of the array.

Common Mistakes​

Assuming a Modified Field Is Unchanged​

If a called function declares modifies x, you cannot assume x is unchanged after the call, even if the function happens to do nothing:

private func doesNothing() : () modifies y {
  ()  // Empty body, but modifies y is declared
};

public func bad() : async () modifies y {
  let y0 = y;
  doesNothing();
  assert y == y0;  // FAILS: y might have changed
}

The verifier respects the declared contract, not the implementation.

Forgetting Transitive Modifies​

If your function calls another that modifies a field, you must include that field:

private func inner() : () modifies a { a := 1; };

// ERROR: modifies clause missing fields: a
public func outer() : async () {
  inner();
}

Fix by adding modifies a to outer.

Summary​

  • modifies declares which fields a function may change
  • Fields not in modifies are automatically framed as unchanged
  • All modifications must be declared; missing declarations cause errors
  • Effects compose through function calls
  • A field in modifies may or may not actually change; callers cannot assume either