Interference Model

The verifier models await interference by asking which public methods could have executed while your actor was suspended, then havocing the actor fields those methods may write.

What Is Interference

When your actor awaits an async call, execution suspends. During this suspension, the Internet Computer may process other messages to your actor. This includes:

• Calls from external actors
• Callbacks from previous async calls
• Reentrancy from the call you just made

The verifier cannot know which calls occurred, in what order, or how many times. It models this uncertainty as interference: any public method may have been called while the current method was suspended.

Conservative Approximation

The interference model is intentionally conservative about scheduling and precise about effects. At each suspending await boundary, the verifier assumes:

1. All public methods may execute - Any public function in your actor could have been called
2. Multiple times - The same method could run repeatedly
3. In any order - No assumptions about call sequence
4. By any caller - No restrictions on who called
5. With declared write effects - The fields in those methods' modifies clauses may change

This means fields that public methods may write are havoced (made unknown) at await boundaries, subject to your actor invariant guarantees. Fields no public method can write keep stronger frame facts.

interf-all-writes.sr9

// All public method writes can happen during interference
persistent actor {
  var balance : Int = 0;
  var nonce : Nat = 0;
  invariant balance >= 0;

  public func deposit(amount : Nat) : async () modifies balance {
    balance += amount;
  };

  public func incrementNonce() : async () modifies nonce {
    nonce += 1;
  };

  public func withdraw(_amount : Nat) : async () modifies balance, nonce {
    let _oldBalance = balance;
    try { await pause(); } catch (_) {};
    // After await: only invariant (balance >= 0) guaranteed
    // balance could be oldBalance, or higher from deposits
    // nonce could be any value (incrementNonce may have run)
    assert balance >= 0;  // Invariant holds
  };

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

After the awaited pause(), the verifier knows only the invariant facts about publicly writable fields. The exact balance and nonce are unknown because deposit() and incrementNonce() could have been called.

No Message Ordering Guarantees

The verifier does not assume messages are processed in any particular order. Even if you make sequential async calls, other messages may interleave:

interf-no-order_unsat.sr9

// The verifier does not assume message ordering
persistent actor {
  var step : Nat = 0;

  public func setStep1() : async () modifies step {
    step := 1;
  };

  public func setStep2() : async () modifies step {
    step := 2;
  };

  public func run() : async () modifies step {
    try { await setStep1(); } catch (_) {};
    try { await setStep2(); } catch (_) {};
    // WRONG: Cannot assume step == 2
    // Other calls may have interleaved
    assert step == 2;  // ERROR: step could be 1 or any value
  };
}

This fails because between the awaited setStep1() and setStep2() calls, other calls could have modified step. The verifier cannot prove step == 2 at the assertion.

Reentrancy Modeling

Reentrancy occurs when code you call (directly or transitively) makes a callback to your actor. The verifier models reentrancy conservatively:

interf-reentrancy.sr9

// Reentrancy during await can call any public method
persistent actor {
  var locked : Bool = false;
  var counter : Nat = 0;
  invariant counter <= 100;

  public func increment() : async ()
    modifies counter
    entry_requires counter < 100;
    requires counter < 100;
  {
    counter += 1;
  };

  public func longOperation() : async ()
    modifies locked, counter
    entry_requires not locked;
    requires not locked;
  {
    locked := true;
    try { await externalCall(); } catch (_) {};
    // During await: increment() could be called many times
    // But invariant ensures counter <= 100
    assert counter <= 100;  // Guaranteed by invariant
    locked := false;
  };

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

During the awaited externalCall(), the external canister could call back to increment() multiple times. The verifier assumes this could happen, but the invariant counter <= 100 still holds because increment() has matching entry_requires/requires guards for counter < 100.

The Havoc Mechanism

Internally, the verifier implements interference via an exhale-inhale pattern:

1. Before await: Prove invariant holds, then release (exhale) permissions
2. At await: State is unknown (havoced)
3. After await: Regain (inhale) permissions, assume invariant holds

interf-havoc-effect.sr9

// Demonstrating the exhale-inhale havoc pattern
persistent actor {
  var value : Int = 10;
  invariant value > 0;

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

  public func process() : async Int modifies value {
    let _before = value;
    assert value > 0;       // Invariant available

    try { await externalCall(); } catch (_) {};
    // At await:
    // 1. Verifier proves invariant (value > 0)
    // 2. Permission released (exhale)
    // 3. After resume: permission regained (inhale)
    // 4. Invariant assumed (value > 0)
    // BUT: exact value is unknown (could be 1, 100, etc.)

    assert value > 0;       // Still holds
    // assert value == before;  // Would FAIL
    value
  };
}

The key insight: only invariant properties survive across await. Exact values are lost to the havoc.

Effect-Based Filtering

Not all state is havoced. The verifier's escape analysis identifies:

• Shared state: Actor fields and anything that aliases them
• Local state: Fresh allocations that don't escape

Only shared state is subject to interference. Fresh local allocations remain stable. See Local vs Shared State for details.

What the Model Does NOT Capture

The conservative model is sound but imprecise. It does NOT capture:

Actual Runtime Behavior	Verifier Assumption
FIFO message ordering	No ordering
One message at a time	Other messages may run during suspension
Caller restrictions	Any caller
Rate limits	Unbounded calls

This means the verifier may reject programs that would actually be safe under a stronger application-level protocol. Strengthen your invariants, narrow public write effects, or re-check conditions after await to help the verifier understand what properties are preserved.

Invariants as Interference Contracts

Your invariant is effectively a contract with the interference model. It says: "No matter what public methods execute, this property will hold."

interf-conservative.sr9

// Conservative model: any effect in modifies clause may occur
persistent actor {
  var a : Int = 0;
  var b : Int = 0;
  var c : Int = 0;
  invariant a + b + c == 0;  // Sum always zero

  public func adjustA(delta : Int) : async ()
    modifies a, b
  {
    a += delta;
    b -= delta;  // Maintain invariant
  };

  public func adjustB(delta : Int) : async ()
    modifies b, c
  {
    b += delta;
    c -= delta;  // Maintain invariant
  };

  public func observe() : async Int modifies a, b, c {
    try { await pause(); } catch (_) {};
    // After await: a, b, c could have any values
    // BUT: invariant a + b + c == 0 still holds
    assert a + b + c == 0;
    a + b + c
  };

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

The invariant a + b + c == 0 constrains all interference. Even though adjustA and adjustB can run during the await in observe, they maintain the sum invariant.

Common Patterns

Use Invariants for Cross-Await Properties

persistent actor {
  var balance : Int = 0;
  invariant balance >= 0;

  public func safeWithdraw(amount : Nat) : async Bool
    modifies balance
    entry_requires amount <= balance;
    requires amount <= balance;
  {
    try { await checkPermissions(); } catch (_) {};
    // Cannot assume balance >= amount anymore
    // But we know balance >= 0
    if (balance >= amount) {
      balance -= amount;
      true
    } else {
      false
    }
  };
}

Capture Values Before Await for Later Use

If you need pre-await values, store primitive or immutable values in locals before the await:

public func log() : async () reads counter {
  let snapshot = counter;
  try { await externalLog(snapshot); } catch (_) {};
  // snapshot is a copied local value, unaffected by interference
  // Can still use snapshot here
}

Re-check Conditions After Await

Never assume conditions still hold after await:

// WRONG
public func wrong() : async () modifies flag
  entry_requires flag;
  requires flag;
{
  try { await doWork(); } catch (_) {};
  assert flag;  // May fail - flag could have changed
}

// RIGHT
public func right() : async () modifies flag
  entry_requires flag;
  requires flag;
{
  try { await doWork(); } catch (_) {};
  if (flag) {
    // Proceed only if condition still holds
  };
}

See Also

• Invariants and Await - How invariants interact with await
• Local vs Shared State - What remains stable across await
• Frame Conditions Across Await - Weaker frame guarantees in async
• Async Star - When await* does or does not create an extra boundary

Summary

• The interference model assumes any public method could execute during await
• No assumptions about message ordering or call frequency
• Reentrancy is modeled conservatively
• Publicly writable shared fields are havoced at await boundaries
• Only invariant properties are guaranteed after await
• Fresh local allocations are not subject to interference
• Use invariants to specify what properties survive interference