Ghost Variables (ghost var)

Ghost variables are verification-only state that exists during proof checking but is erased from runtime output. They let you track abstract properties and maintain invariants without affecting the compiled program.

Basic Syntax

Declare a ghost variable with ghost var:

persistent actor {
  ghost var counter : Nat = 0;
  ghost var flag : Bool = true;
  ghost var value : Int = -42;
}

Ghost variables:

• Must have an initial value
• Are typed like regular variables
• Can use any spec-compatible type (Nat, Int, Bool, Text, records, variants, options, spec collections)

Actor-Level Ghost Fields

Ghost variables declared at actor level become ghost fields. They persist across method calls (for verification purposes) but are erased from the compiled actor.

ghost-var-basic.sr9

// Basic ghost variable example

persistent actor {
  // Runtime state
  var counter : Nat = 0;

  // Ghost state - exists only for verification
  ghost var shadow : Nat = 0;

  // Invariant relates ghost and runtime state
  invariant counter == shadow;

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

  public func get() : async Nat
    reads counter
    ensures result == counter;
  {
    counter
  };
}

The shadow field tracks the counter's value for verification. The invariant counter == shadow proves they stay synchronized. At runtime, only counter exists.

Local Ghost Variables

Ghost variables can also be declared inside function bodies:

ghost-var-local.sr9

// Local ghost variables in function bodies

persistent actor {
  public func compute(n : Nat) : async Nat
    entry_requires n <= 10;
    requires n <= 10;
    ensures result == n + 1;
  {
    // Runtime local
    var acc : Nat = 0;

    // Ghost local - for proof tracking
    ghost var proof_acc : Nat = 0;

    acc := n;
    ghost { proof_acc := n; };

    acc += 1;
    ghost { proof_acc := proof_acc + 1; };

    // Assert ghost and runtime are synchronized
    assert acc == proof_acc;

    acc
  };
}

Local ghost variables help track intermediate proof state within a function. They are scoped to the function body and erased from runtime.

Mutating Ghost Variables

Ghost variables can only be mutated inside ghost blocks:

ghost { counter := counter + 1; };

Ghost blocks contain statements that execute only during verification. See Ghost Blocks for details.

The modifies Clause

When a function modifies a ghost field, you must declare it in the modifies clause:

public func update() : async ()
  modifies ghostCounter
  ensures ghostCounter == 10;
{
  ghost { ghostCounter := 10; };
}

This is the same requirement as runtime fields. The verifier tracks permissions for ghost fields.

Using Ghost Variables in Invariants

Ghost variables are particularly useful in invariants to express conservation laws and abstract properties:

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

  invariant balance + totalWithdrawals == totalDeposits;

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

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

The ghost variables prove that balance correctly reflects all deposits and withdrawals, even though only balance exists at runtime.

Using Ghost Variables with old()

Ghost fields work with old() in postconditions:

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

The old(ghostCounter) captures the ghost field's value at method entry.

Restrictions

Cannot Use in Runtime Code

Ghost variables cannot be read or written outside ghost blocks:

ghost-var-runtime_reject.sr9

// ERROR: Ghost variable used in runtime code

persistent actor {
  public func bad(n : Nat) : async Nat {
    ghost var g : Nat = 0;
    g := n;  // ERROR M0314: ghost variable cannot be used in runtime code
    g
  };
}

Error M0314: ghost variable cannot be used in runtime code

Local Ghost Variables Cannot Escape Into Contracts

Local ghost variables are scoped to the body or ghost block where they are declared, so they cannot appear in function contracts:

// WRONG - ghost variable not visible to callers
public func bad(n : Nat) : async Nat {
  ghost var g : Nat = 10;
  requires n > g;  // ERROR M0316
  n
}

Error M0316: ghost variable cannot be used in contract

Actor and module ghost fields can appear in verifier-only contracts such as requires, ensures, and modifies. They cannot appear in entry_requires, because entry guards are emitted as runtime checks.

Ghost Blocks Cannot Mutate Runtime Fields

Ghost code is erased at runtime, so it cannot modify runtime state:

ghost-var-field-mutate_reject.sr9

// ERROR: Ghost block cannot mutate runtime fields

persistent actor {
  var balance : Nat = 0;

  public func bad() : async ()
    modifies balance
  {
    ghost { balance := 1; };  // ERROR: ghost code cannot update runtime fields
  };
}

This would be unsound: the proof depends on balance being 1, but runtime code never sets it.

Cannot Mutate Arrays or Mutable Records in Ghost Blocks

Similarly, ghost blocks cannot mutate array elements or mutable record fields:

// WRONG
public func bad() : async () modifies data {
  ghost { data[0] := 42; };  // ERROR: cannot mutate array in ghost
}

Ghost vs Runtime: Key Differences

Aspect	Runtime Variable	Ghost Variable
Declaration	var x	ghost var x
Runtime code access	Allowed	Error M0314
Ghost block access	Allowed	Allowed
In requires/ensures	Allowed (actor fields)	Allowed for actor/module ghost fields; local ghosts are out of scope
Compiled output	Included	Erased
Mutated from ghost	Error (erased code cannot change runtime state)	Allowed

When to Use Ghost Variables

Use ghost variables when you need to:

1. Track abstract state - Model high-level properties that don't exist at runtime
2. Prove conservation laws - Track totals, sums, or counts across operations
3. Shadow runtime state - Maintain a parallel ghost model for complex proofs
4. Express invariants - State properties that relate multiple operations

Ghost variables add no runtime overhead since they are completely erased.

Common Patterns

Conservation Pattern

Track what goes in and out:

ghost var totalIn : Nat = 0;
ghost var totalOut : Nat = 0;
invariant balance + totalOut == totalIn;

History Pattern

Track sequence of events:

ghost var history : Seq<Event> = Seq.empty<Event>();
invariant Seq.len(history) >= 0;

Permission Pattern

Track who has access:

ghost var permissions : Set<Nat> = Set.empty<Nat>();
invariant Set.contains(0, permissions);

Summary

• ghost var declares verification-only variables erased from runtime
• Ghost variables are mutated only inside ghost { } blocks
• Declare ghost field modifications with modifies in contracts
• Actor/module ghost fields can appear in verifier-only contracts; local ghost variables cannot escape their scope
• Ghost blocks cannot mutate runtime fields (would be unsound)
• Use ghost variables for conservation laws, abstract state, and complex invariants
• No runtime overhead: ghost state is completely erased during compilation

Related Topics

• Ghost blocks for updating ghost variables
• Ghost functions for reusable proof-only computations
• Actor invariants for global facts over ghost and runtime state
• Spec collections for richer ghost models