At-Most-Once Delivery

The Internet Computer guarantees that messages are delivered at most once: a message may succeed once, reject before running, or run and fail, but the system will not duplicate it. This is the foundation of message semantics on the IC and the reason Sector9 code should treat every await as a possible failure point.

The At-Most-Once Guarantee

When you call an async function on another actor (or your own), the IC guarantees:

Outcome	What Happens
Success	Message delivered exactly once, response returned
Failure	Message rejects before execution or execution fails, caller receives error
Never	Message delivered multiple times

This means a message either succeeds once or reports failure once. The IC does not retry failed messages automatically. If execution traps after a commit point, earlier committed effects can remain; delivery and rollback are separate concepts.

delivery-at-most-once.sr9
// Messages are delivered at most once - they may fail but never duplicate.
// This actor demonstrates the at-most-once guarantee.

persistent actor {
  var processedCount : Nat = 0;
  invariant processedCount >= 0;

  // Each message increments exactly once or not at all
  public func processMessage() : async ()
    modifies processedCount
    ensures processedCount == old(processedCount) + 1;
  {
    processedCount += 1;
  };

  // If this message traps, the caller sees an error
  // but the message is NOT retried automatically
  public func riskyProcess(value : Nat) : async ()
    modifies processedCount
    entry_requires value > 0 and value <= 1000;
    requires value > 0;
    requires value <= 1000;
  {
    processedCount += 1;
    // If this guard were violated, changes would revert and the message
    // would not be redelivered. Verified code proves it cannot fire.
    trap value > 1000;
  };
}

If processMessage fails (due to trap, timeout, or network issues), the caller receives an error. The message is not retried. The caller must decide whether to retry.

Why At-Most-Once Matters

At-most-once delivery has important implications for actor design:

No Automatic Retry

Failed messages are not retried by the IC. If a call fails:

The caller receives an error (e.g., #call_error)
Uncommitted state changes in the callee are rolled back
The caller must implement retry logic if needed

delivery-no-retry.sr9
// The IC does NOT automatically retry failed messages.
// Callers must implement retry logic if needed.

persistent actor {
  var counter : Int = 0;
  var lastCaller : ?Principal = null;
  invariant counter >= 0;

  // If this call fails, counter is NOT incremented
  // The caller decides whether to retry
  public func increment() : async Int
    modifies counter
    ensures result == old(counter) + 1;
  {
    counter += 1;
    counter
  };

  // Caller-side retry pattern (conceptual)
  // Note: Actual retry logic would be in the calling canister
  public func incrementWithRetry(_maxRetries : Nat) : async ?Int
    modifies counter
  {
    // In real code, this would call another canister
    // and retry on failure up to maxRetries times
    ?counter
  };

  // Track the last successful caller for idempotency
  public shared({caller}) func recordedIncrement() : async Bool
    modifies counter, lastCaller
  {
    // Idempotency check: same caller means duplicate attempt
    switch (lastCaller) {
      case (?prev) {
        if (prev == caller) {
          return false;  // Already processed
        };
      };
      case null {};
    };

    counter += 1;
    lastCaller := ?caller;
    true
  };
}

No Duplicate Processing

You never need to guard against the same message being processed twice by the system. However, if your application retries, you may need idempotency checks to prevent duplicate application-level effects.

Failure is Always Possible

Any async call may fail. Design your actors to handle this:

Check return values from async calls
Use try/catch for error handling
Consider partial failure in multi-step operations

Designing for Failure

Idempotent Operations

Idempotent operations produce the same result whether called once or multiple times. They are safe for caller-side retry:

// Idempotent: setting to a specific value
public func setBalance(newBalance : Int) : async ()
  modifies balance
  entry_requires newBalance >= 0;
  requires newBalance >= 0;
{
  balance := newBalance;  // Same result if called twice with same value
};

Non-Idempotent Operations

Non-idempotent operations (like incrementing) require careful handling:

// Non-idempotent: incrementing changes state each time
public func increment() : async ()
  modifies counter
{
  counter += 1;  // Calling twice = +2, not idempotent
};

If the caller needs to retry non-idempotent operations, consider:

Request IDs to detect duplicates
Nonces that prevent replay
Two-phase commit patterns

Two-Phase Commit Pattern

For operations involving external calls, use a two-phase commit to handle partial failure:

delivery-failure-handling.sr9
// Designing for message failure: callers must handle the possibility
// that any async call may fail.

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

  private func externalTransfer(_to : Principal, _amount : Int) : async Bool {
    // Simulates external call that may fail
    true
  };

  // Pattern: Idempotent operations are safe for retry
  public func setBalance(newBalance : Int) : async ()
    modifies balance
    entry_requires newBalance >= 0;
    requires newBalance >= 0;
    ensures balance == newBalance;
  {
    balance := newBalance;
  };

  // Pattern: Non-idempotent operations need careful handling
  public func withdraw(amount : Int) : async Bool
    modifies balance
    entry_requires amount >= 0;
    requires amount >= 0;
  {
    if (balance < amount) {
      return false;
    };
    balance -= amount;
    true
  };

  // Pattern: Two-phase commit for external calls
  public func safeTransfer(to : Principal, amount : Int) : async Bool
    modifies balance, pendingTransfers
    entry_requires amount >= 0;
    requires amount >= 0;
  {
    if (balance < amount) {
      return false;
    };

    // Phase 1: Reserve funds
    balance -= amount;
    pendingTransfers += 1;

    // Phase 2: External call (may fail)
    let success = try { await externalTransfer(to, amount) } catch (_) { false };

    // Phase 3: Finalize or rollback
    pendingTransfers -= 1;
    if (not success) {
      balance += amount;  // Rollback on failure
    };
    success
  };
}

The pattern:

Reserve - Make local changes optimistically
Execute - Perform external call (may fail)
Finalize - Confirm or rollback based on result

Verification Model

Sector9 uses a conservative interference model that aligns with at-most-once semantics. At each await boundary, the verifier assumes:

Assumption	Rationale
Any public method may execute	Messages from any caller may arrive
Multiple times	Methods can be called repeatedly
In any order	No FIFO guarantees in verification
By any principal	No caller restrictions assumed

delivery-conservative-model.sr9
// Sector9 uses a conservative interference model at await boundaries.
// This means the verifier assumes ANY public method could execute.

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

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

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

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

  // During await, the verifier assumes:
  // - deposit() could be called (balance increases)
  // - incrementNonce() could be called (nonce changes)
  // - Any combination, any order, any number of times
  public func readAfterPause() : async Int
    modifies balance, nonce  // Needed because we await and model interference
  {
    let _beforeBalance = balance;
    let _beforeNonce = nonce;

    try { await pause(); } catch (_) {};  // <-- Interference point

    // After await:
    // - balance >= 0 (invariant guaranteed)
    // - Exact balance value unknown (could have changed)
    // - nonce value unknown (could have changed)
    assert balance >= 0;  // This succeeds (invariant)

    balance
  };
}

This conservative model is sound: if Sector9 verifies your code, it works under all possible message orderings, including edge cases the IC may not actually produce.

What the IC Actually Guarantees

At runtime, the IC provides stronger guarantees than the verifier assumes:

IC Behavior	Verifier Assumption
FIFO message ordering per sender	No ordering assumed
One message at a time	Arbitrary interleaving
Specific caller for each message	Any caller possible

Sector9 deliberately under-approximates these guarantees. This means:

The verifier may reject programs that are safe at runtime
Verified programs are correct under any possible scheduling

Invariants as Delivery Contracts

Actor invariants are your contract with the interference model. They specify what properties hold despite arbitrary message delivery:

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

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

  public func observe() : async Int
    reads balance
  {
    try { await pause(); } catch (_) {};
    // balance >= 0 guaranteed by invariant
    // even though deposit() could have run
    balance
  };
}

Message Failure Modes

Messages can fail in several ways:

Failure Mode	Cause	Effect
Trap	Runtime error in callee	State rolled back, error returned
Timeout	Call took too long	Error returned to caller
Canister stopped	Target canister is stopped	Error returned
Queue full	Message queue exhausted	`#call_error` returned
Cycles exhausted	Insufficient cycles	Canister stops

All these failures produce an error for the caller. Some fail before the callee runs; others run and then roll back the current uncommitted segment. If the callee already crossed a commit point, earlier committed effects remain.

Error Handling

Use try/catch to handle message failures:

public func safeCall() : async Bool {
  try {
    await riskyOperation();
    true
  } catch (e) {
    // Message failed - decide what to do
    false
  }
}

The catch block executes if the async call fails. Callee postconditions are available on the success path only; the catch path is still verified as ordinary code and must provide its own safe fallback behavior.

Relationship to Commit Points

At-most-once delivery interacts with commit points:

Before commit point: If message handling traps, all changes revert
After commit point: Prior changes are permanent, later changes revert

This means a single message can have partial effects if it contains multiple commit points. See Trap Behavior for details.

Best Practices

1. Validate Before Committing

Check preconditions before reaching a commit point:

public func transfer(amount : Int) : async Bool
  modifies balance
  entry_requires amount >= 0;
  requires amount >= 0;
{
  if (balance < amount) {
    return false;  // Reject early, no state changes
  };
  balance -= amount;
  true
}

2. Use Invariants for Safety Properties

Invariants guarantee properties across message deliveries:

invariant balance >= 0;  // True after any sequence of messages

3. Consider Idempotency for Retryable Operations

If callers may retry, design for idempotency or use request tracking.

4. Handle All Async Failures

Never assume an async call succeeds. Always handle potential failures.

Summary

Messages are delivered at most once: they succeed once or fail completely
The IC does not automatically retry failed messages
Callers must handle failures and decide whether to retry
Sector9 uses a conservative model assuming arbitrary message interleaving
Actor invariants are the contract for properties that survive message delivery
Design for failure: validate early, use two-phase commit, handle errors

The At-Most-Once Guarantee​

Why At-Most-Once Matters​

No Automatic Retry​

No Duplicate Processing​

Failure is Always Possible​

Designing for Failure​

Idempotent Operations​

Non-Idempotent Operations​

Two-Phase Commit Pattern​

Verification Model​

What the IC Actually Guarantees​

Invariants as Delivery Contracts​

Message Failure Modes​

Error Handling​

Relationship to Commit Points​

Best Practices​

1. Validate Before Committing​

2. Use Invariants for Safety Properties​

3. Consider Idempotency for Retryable Operations​

4. Handle All Async Failures​

Summary​

See Also​