Effect Inference

The verifier automatically computes which fields each function reads and writes by analyzing the call graph.

Overview

When you write modifies and reads clauses, the verifier checks that your declarations match reality. It does this by:

1. Analyzing each function body to find direct field accesses
2. Following function calls to collect transitive effects
3. Iterating to a fixpoint until all effects stabilize

This automatic analysis means you do not need to manually trace through call chains to discover every effect from scratch. You still declare the intended reads and modifies footprint; the verifier computes the actual footprint and reports mismatches.

How Effect Inference Works

The verifier performs effect inference in three phases:

Phase 1: Local Analysis

For each function, the verifier scans the body and records:

• Writes: Field assignments (x := ...) and array element writes
• Reads: Field accesses in expressions and contracts
• Callsites: Which functions are called and with what arguments

Phase 2: Transitive Propagation

The verifier iterates over the call graph:

1. Start with each function's local effects
2. For each call, union the callee's effects into the caller
3. Repeat until no changes occur (fixpoint)

After this phase, each function has a complete effect summary including all transitive effects from nested calls.

Phase 3: Validation

The verifier compares inferred effects against your declarations:

• If inferred writes exceed declared modifies, the program is rejected
• If inferred reads exceed declared reads, the program is rejected
• If declarations cover all inferred effects, verification proceeds

Basic Example

inference-basic.sr9

// Effect inference: verifier computes effects through calls
// No explicit effect annotations needed on intermediate calls

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

  // Helper writes to x - effect inferred from code
  private func writeX() : () modifies x {
    x := x + 1;
  };

  // Caller must declare x because writeX modifies it
  // The verifier computes this automatically
  public func caller() : async () reads y modifies x {
    let y0 = y;
    writeX();
    assert y == y0;  // y framed: not in any modifies
  };
}

Key points:

• writeX() modifies x directly
• caller() calls writeX(), so the verifier infers that caller transitively modifies x
• The modifies x declaration on caller is required because of this transitive effect
• Field y is not in any modifies set, so it remains framed

Effect Propagation Through Call Chains

Effects propagate through arbitrarily deep call chains:

inference-chain.sr9

// Effect inference through call chains
// Effects propagate transitively from deepest call to top

persistent actor {
  var data : Int = 0;
  var config : Int = 100;
  var flag : Bool = false;

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

  // Middle level: transitively modifies data
  private func level2() : () modifies data {
    level3();
  };

  // Top helper: transitively modifies data
  private func level1() : () modifies data {
    level2();
  };

  // Public entry: must include all transitive effects
  // The verifier computes that level1 -> level2 -> level3 -> modifies data
  public func run() : async () reads config, flag modifies data {
    let c0 = config;
    let f0 = flag;
    level1();
    assert config == c0;  // Verified: config framed through chain
    assert flag == f0;    // Verified: flag framed through chain
  };
}

The verifier traces the call path:

• run() calls level1()
• level1() calls level2()
• level2() calls level3()
• level3() modifies data

Therefore, all four functions must declare modifies data. Fields config and flag are only read, so they remain framed through the entire chain.

Read Effect Inference

Read effects are inferred the same way as write effects:

inference-reads.sr9

// Effect inference for reads through function calls
// Read effects propagate transitively like write effects

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

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

  // Transitively reads config via getConfig
  private func computeValue() : Int reads config
    ensures result == config * 2;
  {
    getConfig() * 2
  };

  // Must declare reads config because computeValue reads it transitively
  public func apply() : async () reads config modifies state
    ensures state == config * 2;
  {
    state := computeValue();
  };
}

The verifier determines:

• getConfig() reads config directly
• computeValue() reads config transitively (via getConfig)
• apply() reads config transitively (via computeValue)

Each function must declare reads config because the transitive analysis requires it.

Missing Effect Declarations

When your declarations do not cover all inferred effects, the verifier rejects the program:

inference-missing_unsat.sr9

// Effect inference: error when caller missing required effects
// The verifier detects transitive effects and reports missing ones

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

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

  // ERROR: modifies clause missing fields: a
  // The verifier knows modifiesA writes to a, so caller must declare it
  public func badCaller() : async () {
    modifiesA();
  };
}

The error message identifies the missing field:

modifies clause missing fields: a

The fix is to add the missing declaration:

public func badCaller() : async () modifies a {
  modifiesA();
}

Conservative May-Write Effects

Effect inference is conservative. If a callee declares modifies x, callers must treat x as possibly changed even when the callee only writes under a branch:

private func maybeWrite(flag : Bool) : () modifies x {
  if (flag) {
    x += 1;
  };
};

public func caller(flag : Bool) : async () modifies x {
  let before = x;
  maybeWrite(flag);
  // The footprint alone is not enough to prove this.
  if (not flag) {
    // assert x == before;  // Needs a callee postcondition.
  };
}

The field footprint is still modifies x. The verifier does not silently narrow the footprint based on the particular argument value at one call site. Use postconditions when callers need branch-specific facts about what changed.

Modifies Implies Read Permission

Declaring modifies x automatically grants read permission for x. You do not need to also declare reads x:

public func swap() : async () modifies x, y {
  let temp = x;  // Read of x allowed by modifies x
  x := y;        // Read of y allowed by modifies y
  y := temp;
};

The verifier treats modifies as a superset of reads for permission purposes.

Effect Inference and Pure Functions

Pure functions have no effects by design. They cannot:

• Read or write actor fields
• Call non-pure functions
• Use await

Because pure functions have empty effect summaries, they do not contribute to transitive effects:

pure func double(n : Int) : Int { n * 2 };

public func compute() : async () modifies result {
  result := double(result);  // double has no transitive effects
};

Effect Inference Across Await

Effect inference works normally within atomic sections between awaits. At await boundaries, the verifier uses public method effect summaries to determine which fields may be modified by re-entrant calls.

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

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

  public func run() : async () reads config modifies counter {
    let c0 = config;
    try { await inc(); } catch (_) {};
    // Cannot assert config == c0 without invariant
    // Reentrancy allows config to change
  };
}

The verifier collects public/exported modifies declarations across the actor to build an interference set. Any field that an interleavable public method may modify can change during a suspending await.

Common Mistakes

Forgetting Transitive Effects

The most common error is declaring local effects but forgetting effects from called functions:

private func helper() : () modifies a, b {
  a := 1;
  b := 2;
};

// ERROR: modifies clause missing fields: a, b
public func caller() : async () {
  helper();
}

Always check what your callees modify and include those fields.

Assuming Effect Inference Is Optional

Effect inference is not optional. The verifier always performs it and always validates your declarations. You cannot skip modifies and reads clauses and hope for the best.

Confusing Inference with Declaration

Effect inference computes what effects actually occur. It does not add effects you did not declare. If you forget modifies x, the verifier reports an error rather than silently adding it.

How the Algorithm Works (Technical)

The verifier uses fixpoint iteration:

1. Initialize each function's effect summary with local effects
2. For each function, iterate through callsites
3. Look up callee summary and normalize generated names for imports/generic specializations
4. Union callee effects into caller summary
5. If any summary changed, repeat from step 2
6. When no changes occur, compare summaries against declarations

This algorithm handles:

• Mutually recursive functions (via fixpoint)
• Arbitrarily deep call chains (via iteration)

Summary

• Effect inference automatically computes reads and writes for each function
• Effects propagate transitively through the call graph via fixpoint iteration
• Your declarations must cover all inferred effects or the program is rejected
• Effect inference is conservative: declared modifies fields are may-write fields
• Pure functions have no effects and do not contribute to transitive effects
• Missing declarations produce clear error messages identifying the missing fields

Related Topics

• modifies for write declarations
• reads for read declarations
• Frame conditions for caller-visible unchanged fields
• Await semantics for why public effects matter across suspension