The reads Clause

The reads clause declares which actor fields a function observes without modifying.

Overview

When a function reads actor state without modifying it, you declare which fields it accesses using reads. This serves two purposes:

1. Read permission: The verifier grants read access to declared fields
2. Framing guarantee: Fields in reads but not in modifies are guaranteed unchanged and can be referenced after calls

Without a reads clause, reading a field that isn't in modifies causes a translation error.

Syntax

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

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

For multiple fields, separate them with commas. The reads clause can appear before or after modifies:

public func mixed() : async () reads x modifies y {
  // reads x, writes y
}

Basic Usage

reads-basic.sr9

persistent actor {
  var balance : Nat = 100;
  var owner : Text = "alice";

  // Read-only access to balance
  public func getBalance() : async Nat
    reads balance
    ensures result == balance;
  {
    balance
  };

  // Read-only access to owner
  public func getOwner() : async Text
    reads owner
    ensures result == owner;
  {
    owner
  };

  // Read multiple fields
  public func describe() : async (Text, Nat)
    reads owner, balance
    ensures result.0 == owner;
    ensures result.1 == balance;
  {
    (owner, balance)
  };
}

Key points:

• Each function lists the fields it reads
• The verifier checks that actual reads stay within the declared set
• Postconditions can reference the declared fields

Framing: Read-Only Fields Are Unchanged

The most powerful feature of reads is automatic framing. When you declare reads y without modifies y, the verifier guarantees that y remains unchanged.

reads-framing.sr9

persistent actor {
  var x : Int = 0;
  var y : Int = 10;
  var z : Int = 100;

  // Writes x, only reads y
  private func copyYtoX() : () reads y modifies x {
    x := y;
  };

  // Caller proves y is unchanged
  public func test() : async () reads y modifies x {
    let y0 = y;
    copyYtoX();
    assert y == y0;  // Verified: y is framed because it's in reads, not modifies
    assert x == y0;  // x now equals original y
  };

  // Multiple read-only fields are all framed
  private func updateX(_val : Int) : () reads y, z modifies x {
    x := y + z;
  };

  public func testMultiple() : async () reads y, z modifies x {
    let y0 = y;
    let z0 = z;
    updateX(0);
    assert y == y0;  // y framed
    assert z == z0;  // z framed
  };
}

This works because:

1. copyYtoX declares reads y but only modifies x
2. The verifier automatically generates a frame condition: y == old(y)
3. Callers can assert that y is unchanged after the call

Missing Reads: A Common Error

If you read a field (directly or through a called function) without declaring it, the verifier rejects the program:

reads-missing_unsat.sr9

persistent actor {
  var config : Int = 42;
  var state : Int = 0;

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

  // ERROR: Missing reads config
  // The caller doesn't declare reads config, but calls needsConfig which requires it
  public func broken() : async Int {
    needsConfig()  // Error: reads clause missing fields: config
  };
}

The error message tells you exactly which field is missing:

reads clause missing fields: fld$config

The fix is to add the missing field to your reads clause:

public func fixed() : async Int reads config {
  needsConfig()
}

Transitive Effects Through Calls

When function A calls function B, the effects compose. If B declares reads x, then A must also declare reads x (or have x in its modifies clause):

reads-transitive.sr9

persistent actor {
  var config : Int = 100;
  var state : Int = 0;

  // Direct read
  private func getConfig() : Int reads config
    ensures result == config;
  {
    config
  };

  // Transitive read through getConfig
  private func getConfigViaCall() : Int reads config
    ensures result == config;
  {
    getConfig()
  };

  // Uses config transitively, writes state
  private func updateFromConfig() : () reads config modifies state
    ensures state == config;
  {
    state := getConfigViaCall();
  };

  // Top-level method must declare all transitive reads
  public func apply() : async () reads config modifies state {
    let c0 = config;
    updateFromConfig();
    assert config == c0;  // config framed (only read)
    assert state == c0;   // state updated
  };
}

The verifier computes effect summaries across the call graph and validates that each function's reads clause covers all transitively read fields that are not already covered by modifies.

Reads vs Modifies

The key distinction between reads and modifies:

Aspect	reads	modifies
Permission	Read-only (shared)	Read-write (exclusive)
Field changes	Guaranteed unchanged	May change
Framing	Automatic field == old(field)	No automatic frame

A field in modifies implicitly grants read permission. You don't need to list a field in both:

// Correct: x in modifies implies read permission
public func increment() : async () modifies x {
  x := x + 1;  // Reading and writing x
}

Reads with Postconditions

You can write postconditions that reference read-only fields. The verifier knows these fields haven't changed:

public func getScaled(factor : Int) : async Int
  reads base
  ensures result == base * factor;
{
  base * factor
}

For read-only fields, you can explicitly state the frame condition, though it's automatic:

public func readOnly() : async Int
  reads x
  ensures x == old(x);  // Automatic, but explicit is fine
  ensures result == x;
{
  x
}

Reads with Arrays

Array fields work the same as scalar fields. Declaring reads data grants read access to all array elements:

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

  public func sum() : async Int
    reads data
    entry_requires data.size() > 0;
    requires data.size() > 0;
  {
    var total = 0;
    for (i in data.keys()) {
      total += data[i];
    };
    total
  };

  public func testFraming() : async () reads data modifies other {
    let d0 = data[0];
    other := 42;
    assert data[0] == d0;  // data is framed
  };
}

Common Mistakes

Forgetting Transitive Reads

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

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.

Assuming Modifies Implies Reads-Only

If a field is in modifies, it may change. Don't assume it stays the same:

private func maybeChange() : () modifies x {
  if (someCondition) { x := x + 1 };
}

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

The verifier respects the declared modifies, not the implementation.

Reading Undeclared Fields in Contracts

Fields referenced in postconditions must be in reads or modifies:

// ERROR: reads clause missing fields: limit
public func check(val : Int) : async Bool
  ensures result == (val <= limit);  // limit not declared
{
  val <= limit
}

Fix by adding reads limit.

Summary

• reads declares which fields a function observes without modifying
• Fields in reads but not modifies are automatically framed as unchanged
• All field accesses must be declared; missing declarations cause errors
• Effects compose through function calls; callers must declare callee reads
• modifies implies read permission; you don't need both for the same field

Related Topics

• modifies for write permissions and may-change effects
• Frame conditions for how read-only fields stay stable
• Effect inference for transitive reads through helper calls
• Actor invariants for facts that remain available across await