Read vs Write Permissions

The verifier uses a read/write permission model to track access to actor fields and mutable heap locations.

Overview

Sector9 tracks permissions to ensure sound verification of heap access. Every actor-field access requires an appropriate footprint clause:

Permission	Grants	Source Clause
Read	Shared observation	reads
Write	Exclusive modification	modifies

Write permission is strictly stronger than read permission. If you have write permission to a location, you automatically have read permission.

Why Permissions Matter

Permissions enable the verifier to reason about:

1. Isolation: Functions cannot modify state they do not have permission for
2. Framing: fields without write permission are guaranteed unchanged within the current non-suspending step
3. Soundness: await interference cannot be mistaken for stable state

Without permission tracking, the verifier could not distinguish between fields that might change and fields guaranteed to stay the same.

The Permission Hierarchy

Sector9 uses a simple two-level hierarchy:

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

Read permission allows observation but not modification. Multiple functions can hold read permission to the same location simultaneously.

Write permission allows both reading and writing. Write permission is exclusive in the proof state: the verifier treats it as authority to update the location, so callers cannot infer that the location was preserved unless the callee promises that explicitly with an ensures clause.

perm-read-write.sr9

// Permission hierarchy: reads grants shared read, modifies grants exclusive write
persistent actor PermissionHierarchy {
  var balance : Int = 100;
  var limit : Int = 500;

  // Read permission (shared): multiple functions can read simultaneously
  public func getBalance() : async Int
    reads balance
    ensures result == balance;
  {
    balance
  };

  // Write permission (exclusive): only one function can modify at a time
  public func deposit(amount : Int) : async ()
    modifies balance
    entry_requires amount >= 0;
    requires amount >= 0;
    ensures balance == old(balance) + amount;
  {
    balance := balance + amount;
  };

  // Write implies read: modifies grants both read and write access
  public func doubleBalance() : async ()
    modifies balance
    ensures balance == old(balance) * 2;
  {
    balance := balance * 2;  // Reading and writing with same permission
  };

  // Combining permissions: read some, modify others
  public func adjustBalance(delta : Int) : async ()
    reads limit
    modifies balance
    entry_requires balance + delta <= limit;
    requires balance + delta <= limit;
    ensures balance == old(balance) + delta;
  {
    balance := balance + delta;
  };
}

Key points:

• reads balance grants shared read permission
• modifies balance grants exclusive write permission (which includes read)
• You can combine permissions: reads limit modifies balance

Write Implies Read

When you declare modifies field, you automatically get read permission for that field. You do not need to declare both:

// Correct: modifies grants read permission implicitly
public func doubleValue() : async () modifies x {
  x := x * 2;  // Reading and writing x with same permission
}

This is why the permission ordering is Read ≤ Write. Write permission subsumes read permission.

perm-hierarchy.sr9

// Permission ordering: Read ≤ Write (Write is stronger than Read)
persistent actor PermissionOrdering {
  var counter : Int = 0;

  // Read permission: sufficient for observation
  private func observe() : Int
    reads counter
    ensures result == counter;
  {
    counter
  };

  // Write permission: sufficient for both reading and writing
  private func increment() : ()
    modifies counter
    ensures counter == old(counter) + 1;
  {
    counter := counter + 1;
  };

  // Callers combine permissions transitively
  public func observeAndIncrement() : async Int
    modifies counter
    ensures result == old(counter);
    ensures counter == old(counter) + 1;
  {
    let before = observe();  // Uses read from modifies
    increment();             // Uses write from modifies
    before
  };
}

In observeAndIncrement, the modifies counter declaration provides enough permission for both:

• Calling observe() which requires read permission
• Calling increment() which requires write permission

Write Permission Is Exclusive

When a function declares modifies field, it has exclusive access to that field. This means:

1. The function may change the field
2. Callers cannot assume the field is unchanged
3. The proof treats the field as under this function's update authority until a call or await boundary transfers control

perm-exclusive_unsat.sr9

// Write permission is exclusive: callee may modify, caller cannot assume unchanged
persistent actor ExclusiveWrite {
  var value : Int = 0;

  private func mayModify() : ()
    modifies value
    // No postcondition about value - it may change
  {
    value := value + 1;
  };

  public func test() : async ()
    modifies value
  {
    let before = value;
    mayModify();
    // FAILS: mayModify has write permission, so value may have changed
    assert value == before;
  };
}

This verification fails because mayModify has write permission to value. Even though we saved the value before the call, the callee is free to change it. The verifier reasons from the function's declared contract, not from wishful assumptions at the call site.

To fix this, you would need mayModify to provide a postcondition guaranteeing the value is unchanged, or not include value in its modifies clause.

Read Permission Enables Framing

The power of the permission model is framing: fields with only read permission are guaranteed unchanged during a non-suspending method body or helper call.

perm-framing.sr9

// Framing: read-only fields are guaranteed unchanged
persistent actor PermissionFraming {
  var x : Int = 10;
  var y : Int = 20;

  // Only has write permission for x, read permission for y
  private func updateX(newVal : Int) : ()
    reads y
    modifies x
    ensures x == newVal;
    // y == old(y) is automatic from reads-only
  {
    x := newVal;
  };

  public func test() : async ()
    reads y
    modifies x
  {
    let y0 = y;
    updateX(42);
    // y is unchanged because updateX only has read permission for y
    assert y == y0;
    assert x == 42;
  };
}

Here updateX has:

• Write permission for x (via modifies x)
• Read permission for y (via reads y)

Since y is read-only and there is no suspending boundary in the relevant step, the verifier automatically knows y == old(y) after the call. The caller can assert y == y0 without an explicit postcondition.

This is the key difference:

Clause	Permission	Framing
reads field	Read (shared)	Automatic: field == old(field)
modifies field	Write (exclusive)	None: field may change

Missing Permissions

If you access a field without declaring permission, the verifier rejects the program:

perm-missing_reject.sr9

// Missing permission: reading without declaration causes rejection
persistent actor MissingPermission {
  var secret : Int = 42;

  // ERROR: reads clause missing fields: secret
  public func leak() : async Int {
    secret  // No permission to read secret
  };
}

The error message tells you exactly which field is missing:

reads clause missing fields: secret; add `reads secret` (or `modifies secret` for written fields)

The fix is to declare the access:

public func leak() : async Int reads secret {
  secret
}

Permissions and Contracts

Permissions affect where fields can appear:

Context	Required Permission
Function body read	reads or modifies
Function body write	modifies
requires clause	reads or modifies
ensures clause	reads or modifies
invariant	Automatically satisfied for actor fields

Postconditions can reference any field you have permission for:

public func transfer(amount : Int) : async ()
  reads limit
  modifies balance
  entry_requires amount <= limit;
  requires amount <= limit;
  ensures balance == old(balance) - amount;
{
  balance := balance - amount;
}

Permissions and Async

Permissions interact specially with await:

1. Before await: The verifier checks that actor invariants hold
2. At await: Permissions to publicly writable shared state are released
3. After await: Permissions are reacquired, but values may have changed unless the field is protected by an invariant or outside the possible public write set

This is because other messages may execute during the await. See Invariants and Await and Await Frames for details.

For local variables that do not alias actor state, permissions are retained across await.

Viper Encoding

Under the hood, permissions map to Viper access predicates:

Sector9	Viper
Read permission	acc(field, wildcard)
Write permission	acc(field, write)

The verifier automatically inserts fold and unfold operations to manage permissions for mutable records and predicates.

Common Mistakes

Assuming Modifies Means Unchanged

If a function declares modifies x but happens to not change it, callers still cannot assume x is unchanged:

private func noop() : () modifies x {
  ()  // Does nothing, but modifies x is declared
};

public func bad() : async () modifies x {
  let x0 = x;
  noop();
  assert x == x0;  // FAILS: x might have changed
}

The fix is either:

• Remove x from noop's modifies clause if it truly never changes
• Add a postcondition ensures x == old(x) to noop

Forgetting Transitive Permissions

If function A calls function B that reads or modifies a field, A must also declare that permission:

private func helper() : Int reads config { config };

// ERROR: reads clause missing fields: config
public func caller() : async Int {
  helper()
}

Fix by adding reads config to caller.

Confusing Declaration with Obligation

modifies x means "may modify x", not "must modify x". A field in the modifies set might remain unchanged. Similarly, reads x means "may read x", not "will read x".

Summary

• Sector9 uses two permission levels: Read (shared observation) and Write (exclusive update authority)
• Write permission subsumes read permission: modifies grants both
• Read-only fields (reads without modifies) are automatically framed as unchanged in non-suspending code
• All field accesses require explicit permission declarations
• Permissions are tracked symbolically and validated by the verifier
• The verifier respects declared contracts, not implementation behavior

Related Topics

• Permission errors for diagnosing missing reads and modifies
• Framing and permissions for automatic unchanged-field reasoning
• Await frames for the weaker frame model after suspension
• Footprints for the source-level reads and modifies syntax