Framing and Permissions

How reads and modifies clauses translate into verification permissions that enable automatic framing.

Overview

The previous sections explained Read vs Write permissions and permission errors. This page connects the dots: how your reads and modifies declarations become permissions, and how those permissions automatically generate frame conditions.

The key insight is that framing is a consequence of permissions. In non-suspending code, when a function lacks write permission to a field, the verifier knows that field cannot change. This implicit guarantee is the frame condition.

From Footprints to Permissions

When you declare reads and modifies clauses, the verifier translates them into permissions:

Declaration	Permission Granted	What You Can Do
Not declared	None	Cannot access
reads field	Read (shared)	Observe only
modifies field	Write (exclusive)	Read and write

The verifier generates access permissions for each declared field. Fields not mentioned receive no permission, meaning they cannot be accessed at all.

framing-permission-basics.sr9

// Footprints translate to permissions that enable framing
persistent actor FramingPermissionBasics {
  var balance : Int = 100;
  var limit : Int = 1000;
  var owner : Text = "alice";

  // modifies balance -> Write permission for balance
  // reads limit -> Read permission for limit
  // owner -> No permission (cannot access)
  private func deposit(amount : Int) : ()
    reads limit
    modifies balance
    requires amount >= 0;
    requires balance + amount <= limit;
    ensures balance == old(balance) + amount;
    // Automatic: limit == old(limit) (read-only framed)
  {
    balance := balance + amount;
  };

  public func test() : async ()
    reads limit, owner
    modifies balance
  {
    let limit0 = limit;
    let owner0 = owner;
    deposit(50);
    // Read-only fields are automatically framed
    assert limit == limit0;
    assert owner == owner0;
    assert balance == 150;
  };
}

In this example:

• modifies balance grants write permission to balance
• reads limit grants read permission to limit
• owner has no declaration in deposit, so deposit cannot access it

The Permission-Framing Connection

The verifier automatically generates frame conditions based on permissions:

Field's Permission	Framing Guarantee
None	Cannot access directly
Read only	field == old(field) in non-suspending code
Write	No guarantee (may change)

framing-permission-table.sr9

// Demonstrating the permission table:
// | Clause         | Permission | Framing Guarantee        |
// |----------------|------------|--------------------------|
// | Not declared   | None       | Cannot access            |
// | reads only     | Read       | field == old(field)      |
// | modifies       | Write      | No guarantee (may change)|
persistent actor PermissionTable {
  var readonly : Int = 10;   // Will use reads
  var writable : Int = 20;   // Will use modifies
  var _hidden : Int = 30;    // Will not declare

  private func operation() : ()
    reads readonly
    modifies writable
    ensures writable == old(writable) + readonly;
    // Auto-framed: readonly == old(readonly)
  {
    writable := writable + readonly;
    // Cannot access hidden: no permission declared
  };

  public func run() : async ()
    reads readonly
    modifies writable
  {
    let ro = readonly;
    operation();
    assert readonly == ro;   // Framed (read-only)
    assert writable == 30;   // Changed (write permission)
  };
}

This is why framing works: if a function only has read permission for a field and no suspending boundary intervenes, it cannot modify that field. The verifier encodes this as an automatic postcondition field == old(field).

Write Subsumes Read

Write permission includes read permission. When you declare modifies field, you can both read and write that field without adding it to reads:

framing-write-subsumes-read.sr9

// Write permission subsumes read: modifies grants both read and write
persistent actor WriteSubsumesRead {
  var counter : Int = 0;

  // modifies counter grants both read and write
  private func incrementAndReturn() : Int
    modifies counter
    ensures result == old(counter);
    ensures counter == old(counter) + 1;
  {
    let before = counter;  // Reading (allowed by modifies)
    counter := counter + 1; // Writing (allowed by modifies)
    before
  };

  // Only reads counter - cannot write
  private func peek() : Int
    reads counter
    ensures result == counter;
  {
    counter  // Reading (allowed by reads)
    // counter := 0  // Would fail: reads does not grant write
  };

  public func test() : async Int
    modifies counter
  {
    let v1 = peek();           // Uses read from caller's modifies
    let v2 = incrementAndReturn(); // Uses write from caller's modifies
    assert v1 == v2;
    v1
  };
}

The permission hierarchy is:

Write (exclusive)
  │
  └── Read (shared)

This means:

• A function with modifies x can call helpers that only reads x
• The caller's write permission satisfies the callee's read requirement

Semantic Framing

The verifier performs semantic framing from effect summaries: it analyzes what each function actually reads and writes and shrinks the permission bundle accordingly. This means:

1. Fields truly untouched by a callee do not need to be handed to that callee
2. Read-only accesses get read permission (framed)
3. Only actual writes get write permission (not framed)

framing-semantic-shrinking.sr9

// Semantic framing: verifier shrinks permissions based on actual effects
persistent actor SemanticShrinking {
  var a : Int = 1;
  var b : Int = 2;
  var c : Int = 3;

  // Writes only a, reads b, does not touch c
  private func updateA() : ()
    reads b
    modifies a
    ensures a == old(a) + b;
  {
    a := a + b;
  };

  // Even though we have modifies for a, the verifier knows:
  // - b is framed (read-only permission)
  // - c is framed (no permission given to updateA)
  public func test() : async ()
    reads b, c
    modifies a
  {
    let b0 = b;
    let c0 = c;
    updateA();
    assert b == b0;  // b is framed (read-only)
    assert c == c0;  // c is framed (not in any clause)
    assert a == 1 + b;
  };
}

The verifier computes an effect summary for each function. Fields not in the write set are automatically framed at call sites that have enough permission to mention them. This is more precise than a raw caller-side permission bundle: the verifier tracks what the callee actually reads and writes.

Transitive Permission Propagation

Permissions propagate through call chains. If function A calls function B, and B needs permission for a field, A must also declare that permission:

framing-transitive-permissions.sr9

// Permissions propagate transitively through call chains
persistent actor TransitivePermissions {
  var x : Int = 10;
  var y : Int = 20;
  var z : Int = 30;

  // Deepest level: only modifies x
  private func level3() : () modifies x {
    x := x + 1;
  };

  // Middle level: must declare modifies x
  private func level2() : () modifies x {
    level3();
  };

  // Top level: must also declare modifies x
  private func level1() : () modifies x {
    level2();
  };

  // Caller can rely on framing for y and z through entire chain
  public func run() : async ()
    reads y, z
    modifies x
  {
    let y0 = y;
    let z0 = z;
    level1();
    // y and z are framed through all three levels
    assert y == y0;
    assert z == z0;
    assert x == 11;
  };
}

The verifier computes effects transitively:

• level3 writes x
• level2 calls level3, so it also writes x
• level1 calls level2, so it also writes x
• run calls level1, so it must declare modifies x

Frame conditions also propagate: since no function in the chain touches y or z, they remain framed at every level.

No Permission Means No Access

If you do not declare permission for a field, the verifier prevents access to it entirely. This is stronger than framing: you cannot even observe the field's value.

framing-no-permission-unsat_unsat.sr9

// Demonstration: without permission, cannot access a field
// This example should FAIL verification (expected _unsat behavior)
persistent actor NoPermissionAccess {
  var secret : Int = 42;
  var public_val : Int = 0;

  // Only has permission for public_val
  private func tryAccess() : ()
    modifies public_val
    ensures public_val == 1;
  {
    public_val := 1;
    // Cannot reference secret in ensures: no permission
  };

  public func test() : async ()
    modifies public_val
  {
    tryAccess();
    // This assertion cannot be proven: we have no reads for secret
    // The verifier does not know what secret contains
    assert secret == 42;  // FAILS: no permission to read secret
  };
}

This is rejected because test has no reads secret declaration. The verifier prevents the field access before it reaches a meaningful assertion proof.

Permissions and Mutable Records

For mutable records (records with var fields), the verifier uses ownership predicates that bundle permissions for all fields. When you access a record:

1. The verifier unfolds the ownership predicate to get individual field permissions
2. You access the fields you need
3. The verifier folds the predicate back when done

This is invisible in your code but explains some permission error messages that mention "Owned" predicates.

type Cell = { var x : Int; var y : Int };

private func updateX(c : Cell) : ()
  modifies c.x
{
  c.x := c.x + 1;
  // c.y is framed: only x is in modifies
}

Permissions Across Await

Permissions have special behavior at await points:

1. Before await: Permissions to actor fields are held
2. At await: Write permissions to publicly writable shared state are released
3. After await: Permissions are reacquired, but field values may have changed unless preserved by selective havoc, invariants, or snapshots

This is because other messages can execute during the await. The verifier cannot assume framing across await boundaries for actor fields that public methods may write.

public func run() : async () modifies counter {
  let before = counter;
  try { await pause(); } catch (_) {};
  // Cannot assert counter == before: it may have changed
}

To preserve values across await, use actor invariants, local snapshots, or keep the field outside the possible public write set.

The Viper Encoding

Under the hood, Sector9 translates permissions to Viper's access predicates:

Sector9	Viper Encoding
reads field	acc($Self.field, wildcard)
modifies field	acc($Self.field, write)
No declaration	No access predicate

The verifier injects a $Perm predicate that bundles all actor field permissions. Semantic framing shrinks this bundle based on effect analysis, removing permissions for untouched fields.

Common Patterns

Pattern 1: Read-Only Helper with Framing

private func sum() : Int reads a, b {
  a + b  // Framing: a == old(a), b == old(b)
};

public func useSumTwice() : async Int reads a, b {
  let first = sum();
  let second = sum();
  assert first == second;  // Verified: a and b are framed
  first
}

Pattern 2: Writer with Framed Observers

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

public func test() : async () reads y modifies x {
  let y0 = y;
  incrementX();
  assert y == y0;  // Verified: incrementX has no permission for y
}

Pattern 3: Transitive Framing Through Layers

private func innerWrite() : () modifies data { data := 1; };
private func middle() : () modifies data { innerWrite(); };

public func outer() : async () reads config modifies data {
  let c = config;
  middle();
  assert config == c;  // config framed through entire chain
}

Debugging Permission Issues

When you encounter permission-related framing failures:

1. Check declarations: Ensure all accessed fields have reads or modifies
2. Check transitivity: If calling helpers, add their required permissions
3. Check the error location: Permission errors point to the exact access
4. Check for await: Framing weakens across await for fields public methods can write
5. Check for escaping: Locals that escape to actor state lose permission guarantees

See Permission Errors for detailed error handling.

Summary

• reads and modifies clauses translate to read and write permissions
• Framing is automatic in non-suspending code: fields without write permission are guaranteed unchanged
• Write permission subsumes read permission
• Permissions propagate transitively through call chains
• Semantic framing shrinks permissions based on actual effects
• Fields without any declaration cannot be accessed
• Permissions behave specially across await boundaries, where public write effects drive selective havoc

Related Topics

• Frame conditions for the basic unchanged-field rule
• Read/write permissions for permission levels
• Mutable record ownership for record-field permission bundles
• Async frame conditions for selective frame preservation after await