Skip to main content

Frame Conditions

Frame conditions guarantee that fields outside a function's modifies footprint are not written by that function. Callers can use the guarantee for fields they can mention through their own reads or modifies permissions.

Overview​

When you declare modifies x, you are telling the verifier two things:

  1. The function may change x
  2. The function does NOT change any other fields

The second guarantee is a frame condition. For every field not in modifies and available in the relevant permission context, the verifier can use the frame fact:

field == old(field)

This lets callers reason about what stays the same without you writing explicit postconditions for every unchanged field.

How Frame Conditions Work​

The verifier generates frame postconditions automatically:

frame-basic.sr9
// Frame conditions: unlisted fields are guaranteed unchanged
// The verifier automatically adds postcondition: field == old(field)

persistent actor {
  var counter : Int = 0;
  var limit : Int = 100;

  // Only modifies counter - limit is automatically framed
  private func increment() : ()
    modifies counter
    requires counter < limit;
    ensures counter == old(counter) + 1;
  {
    counter += 1;
  };

  // Caller can prove limit is unchanged after calling increment
  public func checkLimit() : async Bool
    reads limit
    modifies counter
  {
    let limitBefore = limit;
    increment();
    assert limit == limitBefore;  // Verified: limit is framed
    counter < limit
  };
}

When increment() declares modifies counter:

  • The verifier allows writes to counter
  • The verifier generates limit == old(limit) as an implicit postcondition
  • Callers can assert limit is unchanged after calling increment()

You usually do not write the frame condition explicitly. It is automatic for read-only fields you have permission to mention.

Frame Conditions Through Call Chains​

Frame guarantees propagate transitively. When function A calls function B, and B only modifies field x, then A's callers know all fields except x are unchanged through the entire call chain.

frame-transitive.sr9
// Transitive frame conditions through call chains
// Frame guarantees propagate through multiple levels of calls

persistent actor {
  var a : Int = 0;
  var b : Int = 0;
  var c : Int = 0;

  // Deepest call: modifies only a
  private func updateA() : () modifies a {
    a := a + 1;
  };

  // Middle call: transitively modifies only a
  private func middle() : () modifies a {
    updateA();
  };

  // Top call: transitively modifies only a
  // Fields b and c remain framed through entire chain
  public func top() : async () reads b, c modifies a {
    let b0 = b;
    let c0 = c;
    middle();
    assert b == b0;  // Verified: b is framed through all calls
    assert c == c0;  // Verified: c is framed through all calls
  };
}

The verifier computes effect summaries across the call graph. Each level of the call chain must declare modifies a because the deep call writes to a. Fields b and c remain framed through all three levels.

What Triggers a Frame Condition​

A field gets a frame condition when:

Field locationResult
Not in modifies, not in readsNot written by the callee, but no permission to mention it in this function
In reads onlyFrame condition: field == old(field)
In modifiesMay change, no frame guarantee

Fields in reads but not in modifies are automatically framed. The previous pages on modifies and reads explain this in detail.

Modifies Does NOT Mean Unchanged​

A critical distinction: being in modifies means the field may change, not that it will change. But callers cannot assume it stays the same.

frame-modifies-not-guarantee_unsat.sr9
// Being in modifies does NOT guarantee unchanged
// This example fails verification

persistent actor {
  var y : Int = 0;

  // Claims modifies y - even if body does nothing
  private func claimsModifiesY() : () modifies y {
    ()  // Empty body, but y could change per the contract
  };

  // WRONG: Cannot assume y is unchanged after call that declares modifies y
  public func wrongAssumption() : async () modifies y {
    let y0 = y;
    claimsModifiesY();
    assert y == y0;  // FAILS: y is in modifies, so might have changed
  };
}

This fails verification. Even though claimsModifiesY does nothing, the declaration modifies y means the verifier cannot prove y == y0 after the call. The verifier respects the declared contract, not the implementation.

Frame Conditions and Arrays​

For array fields, declaring modifies arr grants permission to modify any element. All other fields remain framed:

persistent actor {
  var data : [var Int] = [var 0, 0, 0];
  var config : Int = 42;

  private func updateFirst() : () modifies data {
    data[0] := 100;
  };

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

The frame condition applies at the field level. You cannot selectively frame individual array indices through modifies alone.

Frame Conditions Across Await​

Frame conditions work differently across await boundaries. Because other code can execute during the await (re-entrancy), the verifier cannot guarantee fields are unchanged.

persistent actor {
  var counter : Int = 0;

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

  // This FAILS verification without an invariant
  public func run() : async () reads counter
    ensures counter == old(counter);  // Cannot prove this!
  {
    try { await pause(); } catch (_) {};
  };
}

To preserve field values across await, use one of:

  1. Actor invariants: Pin the value with invariant field == value
  2. Local snapshots: Capture the value in a local variable before await

See Invariants and Await for details.

Explicit Frame Postconditions​

You can write frame conditions explicitly, though it is rarely needed:

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

This is useful when you want to document the guarantee clearly or when the automatic frame condition is not inferred.

Common Mistakes​

Assuming Modifies Means Unchanged​

If a function declares modifies x, you cannot assume x is unchanged after the call, even if the function does nothing to x in practice. The verifier uses the declared contract.

Forgetting Transitive Effects​

When your function calls another that modifies a field, you must include that field in your own modifies clause. Otherwise, the verifier rejects the program:

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

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

Relying on Framing Across Await​

Ordinary call-frame facts do not preserve actor fields across suspending await points. Use invariants or local variables to preserve values through suspension.

Summary​

  • Frame conditions guarantee fields outside modifies are not written by that function
  • The verifier generates these postconditions automatically
  • Frame guarantees propagate through transitive call chains
  • Fields in modifies may or may not change; no frame guarantee
  • Frame conditions require special handling across await boundaries