Ghost Patterns

Common idioms for using ghost state effectively in verification. These patterns combine ghost variables, ghost blocks, and ghost modules to solve recurring verification problems.

The Shadow Pattern

The shadow pattern maintains a ghost variable that mirrors runtime state. This creates a parallel ghost model that invariants can reference.

ghost-pattern-shadow.sr9

// Shadow pattern: ghost variable mirrors runtime state

persistent actor {
  var counter : Nat = 0;
  ghost var shadow : Nat = 0;

  invariant counter == shadow;

  public func increment() : async () modifies counter, shadow
    ensures counter == old(counter) + 1;
  {
    counter := counter + 1;
    ghost { shadow := shadow + 1; };
  };

  public func add(n : Nat) : async () modifies counter, shadow
    entry_requires n <= 100;
    requires n <= 100;
    ensures counter == old(counter) + n;
  {
    counter := counter + n;
    ghost { shadow := shadow + n; };
  };

  public func reset() : async () modifies counter, shadow
    ensures counter == 0;
  {
    counter := 0;
    ghost { shadow := 0; };
  };
}

When to use:

• The runtime state has complex internal structure you want to abstract
• You need to express invariants about a value's history
• Multiple operations must maintain the same relationship to ghost state

The invariant counter == shadow proves that runtime and ghost stay synchronized. Every operation updates both in lockstep.

The Conservation Pattern

Track what goes in and what comes out. Conservation invariants prove that resources are neither created nor destroyed.

ghost-block-basic.sr9

// Basic ghost block usage

persistent actor {
  var balance : Nat = 0;
  ghost var totalDeposits : Nat = 0;
  ghost var totalWithdrawals : Nat = 0;

  // Conservation invariant
  invariant balance + totalWithdrawals == totalDeposits;

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

  public func withdraw(amount : Nat) : async () modifies balance, totalWithdrawals
    reads totalDeposits
    entry_requires amount <= balance;
    requires amount <= balance;
    ensures balance == old(balance) - amount;
  {
    balance -= amount;
    ghost { totalWithdrawals := totalWithdrawals + amount; };
  };
}

The invariant balance + totalWithdrawals == totalDeposits captures the conservation law without relying on potentially trapping Nat subtraction. Every deposited unit is either still held or has been withdrawn.

Key elements:

• Separate ghost variables for inflows and outflows
• Invariant expresses the conservation equation
• Ghost blocks update the appropriate ghost variable with each operation

The History Pattern

Track cumulative information about all operations performed.

ghost-pattern-history.sr9

// History pattern: ghost variables track cumulative changes

persistent actor {
  var balance : Nat = 100;
  ghost var totalCredits : Nat = 100;
  ghost var totalDebits : Nat = 0;
  ghost var transactionCount : Nat = 0;

  invariant balance == totalCredits - totalDebits;
  invariant totalCredits >= totalDebits;

  public func credit(amount : Nat) : async () modifies balance, totalCredits, transactionCount
    requires amount > 0;
    requires amount <= 1000;
    ensures balance == old(balance) + amount;
    ensures transactionCount == old(transactionCount) + 1;
  {
    balance := balance + amount;
    ghost {
      totalCredits := totalCredits + amount;
      transactionCount := transactionCount + 1;
    };
  };

  public func debit(amount : Nat) : async () modifies balance, totalDebits, transactionCount
    requires amount > 0;
    requires amount <= balance;
    ensures balance == old(balance) - amount;
    ensures transactionCount == old(transactionCount) + 1;
  {
    balance := balance - amount;
    ghost {
      totalDebits := totalDebits + amount;
      transactionCount := transactionCount + 1;
    };
  };
}

This example tracks total credits, total debits, and transaction count. The conservation invariant ensures balance correctness while the transaction count proves audit completeness.

When to use:

• Proving properties about operation sequences
• Audit requirements (counting operations)
• Monotonicity proofs (values only increase)

The Loop Synchronization Pattern

Use ghost variables to track loop progress and prove loop postconditions.

ghost-block-loop.sr9

// Ghost blocks in loops

persistent actor {
  ghost var iterations : Nat = 0;

  public func countUp(n : Nat) : async Nat modifies iterations
    entry_requires n <= 100;
    requires n <= 100;
    ensures result == n;
    ensures iterations == n;
  {
    var i : Nat = 0;
    ghost { iterations := 0; };

    while (i < n) {
      loop:invariant i <= n;
      loop:invariant iterations == i;

      i += 1;
      ghost { iterations := iterations + 1; };
    };

    i
  };
}

The ghost variable iterations tracks loop progress. The loop:invariant ties it to the loop counter i, and the postcondition ensures iterations == n proves the loop executed exactly n times.

Pattern elements:

1. Initialize ghost variable before the loop
2. Add loop:invariant relating ghost to loop state
3. Update ghost inside the loop body
4. Use postcondition to assert final ghost value

The Abstract Model Pattern

Ghost state in modules provides an abstract specification that clients reason about through contracts.

ghost-module-token.sr9

// A module with ghost state for tracking abstract balance
module {
  public class Token() {
    // Runtime field - the actual balance
    var balance : Nat = 0;

    // Ghost field - abstract model for verification
    ghost var abstract_balance : Nat = 0;

    public func deposit(amount : Nat) : ()
      modifies balance, abstract_balance
      ensures abstract_balance == old(abstract_balance) + amount;
    {
      balance += amount;
      ghost { abstract_balance := abstract_balance + amount };
    };

    public func get_balance() : Nat
      reads abstract_balance
      ensures result == abstract_balance;
    {
      var r : Nat = 0;
      ghost { r := abstract_balance };
      r
    };
  };
}

The ghost field abstract_balance is the specification. Clients reason through the method contracts (ensures abstract_balance == old(abstract_balance) + amount), not by reading the field directly. This decouples verification from implementation details.

Key insight: Ghost fields are private to the module. Clients reason through reads and modifies clauses, not direct ghost field access.

The Composition Pattern

Layer ghost state across module boundaries for multi-level verification.

ghost-module-wallet.sr9

// Composing ghost state across modules
import Inner "./ghost-module-token";

module {
  public class Wallet() {
    // Runtime fields
    var name : Text = "";
    var token : Inner.Token = Inner.Token();

    // Ghost field for tracking cumulative deposits
    ghost var total_deposited : Nat = 0;

    public func set_name(n : Text) : ()
      modifies name
    {
      name := n;
    };

    public func add_funds(amount : Nat) : ()
      modifies token, total_deposited
      ensures total_deposited == old(total_deposited) + amount;
    {
      token.deposit(amount);
      ghost { total_deposited := total_deposited + amount };
    };

    public func check_total() : Nat
      reads total_deposited
      ensures result == total_deposited;
    {
      var r : Nat = 0;
      ghost { r := total_deposited };
      r
    };
  };
}

The Wallet module has its own ghost field total_deposited that tracks cumulative deposits. It uses the Token module's interface but maintains independent ghost state for higher-level properties.

Pattern structure:

1. Inner module has its own ghost fields and contracts
2. Outer module declares additional ghost fields for aggregate properties
3. Outer module's ghost blocks update only its own ghost fields
4. Contracts at each level specify their respective ghost state

The Proof Step Pattern

Use ghost blocks with assertions to break complex proofs into steps.

ghost-block-multi.sr9

// Multiple statements in ghost blocks

persistent actor {
  var value : Nat = 0;
  ghost var history : Nat = 0;
  ghost var updateCount : Nat = 0;

  invariant updateCount >= 0;

  public func setValue(n : Nat) : async () modifies value, history, updateCount
    entry_requires n <= 1000;
    requires n <= 1000;
    ensures value == n;
    ensures updateCount == old(updateCount) + 1;
  {
    value := n;

    // Single ghost block with multiple statements
    ghost {
      history := value;
      updateCount += 1;
      assert history == n;
    };
  };
}

The ghost block contains assert history == n, which creates an intermediate proof obligation. This helps the verifier by making implicit reasoning steps explicit.

When to use:

• The verifier times out on a complex proof
• You want to document your reasoning
• Debugging a failing verification

Pattern Combinations

Real code often combines patterns. A token system might use:

persistent actor {
  var supply : Nat = 0;

  // History pattern: proof-only event counters
  ghost var mintEvents : Nat = 0;
  ghost var burnEvents : Nat = 0;

  invariant mintEvents >= burnEvents;

  public func mint(amount : Nat) : async ()
    modifies supply, mintEvents
    entry_requires amount > 0;
    requires amount > 0;
    ensures supply == old(supply) + amount;
  {
    supply += amount;
    ghost {
      mintEvents := mintEvents + 1;
    };
  };
}

This combines:

• Runtime state: supply is the value exposed to callers
• History: mintEvents and burnEvents track operation counts
• Ghost updates: mintEvents changes only inside ghost { }

Anti-Patterns

Unsynchronized Ghost Updates

// WRONG: Ghost and runtime can desync
public func bad() : async ()
  modifies counter, shadow
{
  counter += 1;
  // Missing: ghost { shadow := shadow + 1; };
}

Every runtime mutation needs a corresponding ghost update. Missing updates break invariants.

Ghost State in Contracts

// WRONG: Local ghost variables cannot appear in contracts
public func bad(n : Nat) : async Nat {
  ghost var g : Nat = 10;
  requires n > g;  // ERROR M0316
  n
}

Ghost variables are implementation details. Use parameters and results in contracts.

Mutating Runtime from Ghost

// WRONG: Ghost blocks cannot mutate runtime state
public func bad() : async ()
  modifies balance
{
  ghost { balance := 100; };  // ERROR: unsound
}

Ghost code is erased at runtime. Mutating runtime state from ghost would break the program.

Summary

• Shadow pattern: Ghost variable mirrors runtime state, synchronized by invariant
• Conservation pattern: Track inflows and outflows, prove resources balance
• History pattern: Accumulate information about all operations
• Loop synchronization: Ghost variable tracks loop progress with loop:invariant
• Abstract model: Ghost fields as module specifications, hidden from clients
• Composition: Layer ghost state across modules for multi-level properties
• Proof step: Use ghost assertions to guide the verifier

Choose patterns based on what you need to prove:

• Balance correctness: Conservation
• Operation counts: History
• Loop termination: Loop synchronization
• Module encapsulation: Abstract model

Related Topics

• Ghost variables for shadow and history fields
• Ghost blocks for synchronized proof-only updates
• Ghost modules for abstract model and composition patterns
• Collection linearity for threading immutable ghost models