Cross-Canister Scheduling

Sector9's Viper lane does not model cross-canister message ordering or FIFO guarantees. The verifier uses a conservative interference model that assumes any interleaving can occur at await boundaries.

What This Means

The Internet Computer has specific message scheduling semantics:

• FIFO ordering: Messages to a canister are processed in order
• One-at-a-time: Only one message executes at a time per canister
• Callback ordering: Callbacks execute in a predictable order

Sector9 does not model these guarantees. Instead, it uses a conservative approximation:

Actual IC Behavior	Verifier Assumption
FIFO message ordering	No ordering assumed
One message at a time	Arbitrary interleaving
Caller restrictions	Any caller possible
Rate limits	Unbounded calls

This means the verifier may reject programs that are safe at runtime. The tradeoff is conservative local reasoning: if Sector9 verifies a property, that property holds under the verifier's over-approximation of possible schedules, including schedules the IC does not produce.

The Interference Model

When your actor awaits an async call, execution suspends. During this suspension, the verifier assumes:

1. Any public method in your actor could execute
2. Methods could run multiple times
3. Called by any principal
4. In any order

This is called the "Release-Assume" model:

1. Prove the actor invariant holds before the await
2. Release state (other actors may run)
3. Assume the invariant holds when execution resumes

What You CAN Verify

Invariant properties are preserved across await boundaries:

scheduling-invariant-preserved.sr9

// What CAN be verified: invariants preserved across await
persistent actor {
  var counter : Int = 0;

  invariant counter >= 0;

  private func increment() : async () modifies counter {
    counter += 1;
  };

  public func safeIncrement() : async () modifies counter {
    try {
      await increment();
    } catch (_) {};
    // Invariant counter >= 0 is assumed here
    assert counter >= 0;
  };
}

After the await, you can assume counter >= 0 because:

• The invariant was proven before the await
• Any methods that ran during the await also maintained the invariant
• The invariant is assumed when execution resumes

What You CANNOT Verify

Exact values or ordering-dependent properties fail verification:

scheduling-exact-value_unsat.sr9

// What CANNOT be verified: exact values after await
persistent actor {
  var counter : Int = 0;

  invariant counter >= 0;

  private func increment() : async () modifies counter {
    counter += 1;
  };

  public func checkExact() : async () modifies counter {
    let before = counter;
    try {
      await increment();
    } catch (_) {};
    // FAILS: other actors could have changed counter
    assert counter == before + 1;
  };
}

The assertion fails because:

• During the await, deposit, withdraw, or increment could have run
• The verifier does not know the IC processes messages in order
• counter could be any value satisfying the invariant

Understanding Conservative Interference

The conservative model is illustrated by this example:

scheduling-interference-model.sr9

// The conservative interference model
persistent actor {
  var balance : Int = 100;

  invariant balance >= 0;

  // Any public method could run during await
  public func deposit(amount : Int) : async ()
    modifies balance
    entry_requires amount >= 0;
    requires amount >= 0;
  {
    balance += amount;
  };

  public func withdraw(amount : Int) : async ()
    modifies balance
    entry_requires amount >= 0;
    entry_requires amount <= balance;
    requires amount >= 0;
    requires amount <= balance;
  {
    // Safe: invariant guarantees balance >= 0
    balance -= amount;
  };

  public func transfer(amount : Int) : async ()
    modifies balance
    entry_requires amount >= 0;
    entry_requires amount <= balance;
    requires amount >= 0;
    requires amount <= balance;
  {
    let _before = balance;
    balance -= amount;
    try {
      await deposit(0);  // Any method could run here
    } catch (_) {
      ()
    };
    // Cannot assume balance == before - amount
    // Only know: balance >= 0 (from invariant)
    assert balance >= 0;
  };
}

In transfer:

• Before the await, we subtract amount from balance
• During the await, any public method could run (deposit, withdraw, transfer)
• After the await, we only know balance >= 0 (the invariant)

The verifier cannot prove balance == before - amount because it does not model that:

• No other messages arrived during the await
• Messages are processed in FIFO order
• Only one message runs at a time

Why This Limitation Exists

Cross-canister scheduling involves:

• Message queues: Multiple canisters sending messages
• Ingress throttling: Rate limits on external calls
• Callback chains: Complex ordering of responses
• Failure modes: Rejected messages, timeout, traps

Modeling these semantics requires a different verification lane. Sector9's Viper backend focuses on local correctness: each method preserves contracts and invariants between await boundaries under conservative interference. The active TLA+ backend is the protocol-level lane for interleavings, failure schedules, scoped liveness, and cross-canister temporal claims.

Workarounds

Strengthen Invariants

Express ordering-independent properties as invariants:

scheduling-strengthen-invariant.sr9

// Workaround: strengthen invariants for specific properties
persistent actor {
  var balance : Int = 100;
  var minBalance : Int = 0;

  // Stronger invariant captures the property we need
  invariant balance >= minBalance;
  invariant minBalance >= 0;

  public func deposit(amount : Int) : async ()
    reads minBalance
    modifies balance
    entry_requires amount >= 0;
    requires amount >= 0;
  {
    balance += amount;
  };

  public func setMinimum(min : Int) : async ()
    reads balance
    modifies minBalance
    entry_requires min >= 0;
    entry_requires min <= balance;
    requires min >= 0;
    requires min <= balance;
  {
    minBalance := min;
  };

  public func safeTransfer(amount : Int) : async ()
    reads minBalance
    modifies balance
    entry_requires amount >= 0;
    entry_requires amount <= balance - minBalance;
    requires amount >= 0;
    requires amount <= balance - minBalance;
  {
    balance -= amount;
    try {
      await deposit(0);
    } catch (_) {
      ()
    };
    // Now we can prove balance >= minBalance
    assert balance >= minBalance;
  };
}

Instead of tracking exact values, the invariant balance >= minBalance captures the property you need regardless of interleaving.

Use Fresh Local State

Fresh allocations that do not escape to actor fields remain stable. Every await in verified code is still wrapped in try/catch; the point here is that the local object itself is not reachable by other actor methods:

scheduling-fresh-local.sr9

// Fresh local allocations remain stable across await
persistent actor {
  private func tick() : async () { () };

  public func freshLocalStable() : async Int {
    // Fresh allocation in current method
    let local = { var x = 42 };
    try {
      await tick();
    } catch (_) {};
    // local.x is preserved - it cannot be accessed by other actors
    assert local.x == 42;
    local.x
  };
}

Local objects created in the current method cannot be accessed by other actors, so they are not subject to interference.

Design for Commutativity

Structure operations so the result is independent of execution order:

• Deposits commute: Order does not affect final balance
• Counters commute: Increments can happen in any order
• Sets commute: Add/remove operations are order-independent

When operations commute, the conservative model does not over-approximate.

Accept the Approximation

For properties that truly depend on IC scheduling:

• Keep the Viper proof in recorded-observation form
• Add or update a *.protocol.sr9 root for the TLA+ property
• Mark only the narrow local surface as trusted when there is no verified implementation path
• Test runtime behavior with PIC scenarios when the property has an executable runtime surface

What Is Modeled

For clarity, here is what Sector9 does model about async execution:

Aspect	Modeled	Notes
Atomicity between awaits	Yes	Code between awaits runs without interleaving
Invariant preservation	Yes	Invariants proven before await, assumed after
Fresh allocation stability	Yes	Local objects that do not escape remain stable
Reentrancy-sensitive invariants	Yes	Conservative: any method could be called
Shared state invalidation	Yes	Actor fields are havoced at await

And what is not modeled:

Aspect	Modeled	Notes
FIFO message ordering	No	Conservative approximation
Callback ordering	No	No assumptions about response order
Cross-canister scheduling	No	Out of scope for Viper backend
Rate limits	No	Unbounded calls assumed
Failure recovery	No	See Runtime Traps

Practical Guidance

Situation	Recommendation
Proving exact values after await	Strengthen invariants or accept approximation
Ordering-dependent logic	Design for commutativity or move the claim to the protocol lane
Cross-canister protocols	Use TLA+ protocol roots for cross-canister temporal claims
Complex async patterns	Use fresh locals for intermediate state
Performance testing	Test at runtime, outside verification scope

Protocol-Level Lane

Protocol-level verification is not a Viper feature. Use the TLA+ backend for claims that cross await boundaries or depend on multiple canisters:

• *.protocol.sr9 roots define protocol catalogs and properties
• --verify --tla verifies trusted local companions first, then runs TLC
• PIR fail-closed checks reject missing or ambiguous method/action linkage
• TLA+ owns scoped liveness, async request/response/rollback structure, and protocol-visible interleavings

SimPy remains a future simulation backend for economic and timing behavior.

These tools complement Viper's local correctness proofs with protocol-level analysis.

Summary

• Cross-canister scheduling and FIFO ordering are not modeled
• The verifier uses conservative interference: any interleaving at await boundaries
• Invariant properties are preserved and can be proven
• Exact values after await cannot be verified
• Workarounds: strengthen invariants, use fresh locals, design for commutativity
• Use TLA+ protocol roots for cross-await and cross-canister claims