Ghost Blocks (ghost { })

Ghost blocks contain verification-only statements that are erased from runtime output. They are the mechanism for updating ghost state alongside runtime operations.

Basic Syntax

A ghost block wraps statements in ghost { }:

ghost { statement1; statement2; };

Ghost blocks can contain:

• Ghost variable assignments
• Assertions (assert)
• Calls to ghost functions and proof-only helpers
• Multiple statements
• old() expressions

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; };
  };
}

Each ghost { } block updates the ghost state to mirror the runtime operation. The invariant proves that every deposited unit is either still in balance or has been withdrawn.

What Ghost Blocks Can Do

Update Ghost Variables

Ghost blocks are the only way to modify ghost variables:

ghost var counter : Nat = 0;

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

Contain Multiple Statements

A single ghost block can update multiple ghost variables:

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;
    };
  };
}

Include Assertions

Ghost blocks can contain assert statements for intermediate proof steps:

persistent actor {
  ghost var tracking : Nat = 0;

  public func process(n : Nat) : async ()
    modifies tracking
    entry_requires n > 0;
    requires n > 0;
  {
    ghost {
      assert n >= 1;
      tracking := n;
      assert tracking == n;
    };
  };
}

Use old() Expressions

Ghost blocks can access pre-state values:

public func update(delta : Nat) : async ()
  modifies value
{
  let prev = value;
  value += delta;
  ghost {
    let entry = old(value);
    assert prev == entry;
    history := entry;
  };
}

Ghost Blocks in Loops

Ghost blocks work inside loops and must maintain loop invariants:

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 the loop count. The loop invariant iterations == i connects ghost and runtime state on each iteration.

What Ghost Blocks Cannot Do

Ghost blocks enforce strict soundness rules. Violations are rejected at translation time.

Cannot Mutate Runtime Fields

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 is unsound: the proof would depend on balance being 1, but the runtime code never sets it. Ghost code is erased, so runtime state must be unchanged.

Cannot Mutate Array Elements

ghost-block-array-mutate_reject.sr9

// ERROR: Ghost block cannot mutate array elements

persistent actor {
  public func bad() : async () {
    var xs : [var Nat] = [var 1, 2, 3];
    ghost { xs[0] := 9; };  // ERROR: ghost block mutating array element
  };
}

Array elements are modeled as heap state. Ghost blocks cannot modify heap locations.

Cannot Mutate Mutable Record Fields

// WRONG
type Cell = { var value : Nat };

public func bad() : async () {
  var c : Cell = { var value = 0 };
  ghost { c.value := 1; };  // ERROR: cannot mutate record field
}

Mutable record fields follow the same restriction as array elements.

Cannot Use runtime:assert or trap

Runtime assertions are not allowed in ghost blocks:

// WRONG
ghost {
  runtime:assert x > 0;  // ERROR: runtime construct in ghost context
}

Use assert instead for verification-only checks.

How Ghost Blocks Work

Verification Phase

During verification, ghost blocks are processed alongside runtime code. The verifier:

1. Tracks ghost variable values
2. Checks assertions in ghost blocks
3. Verifies invariants are maintained
4. Proves postconditions using ghost state

Runtime Phase

During compilation to WebAssembly, ghost blocks are completely erased:

// Source
balance += amount;
ghost { totalDeposits := totalDeposits + amount; };

// Compiled output (conceptual)
balance += amount;
// Ghost block erased - no bytecode generated

This means:

• Zero runtime overhead
• No memory for ghost variables
• No execution time for ghost statements

Placement Rules

Ghost blocks can appear:

Context	Allowed
Inside public methods	Yes
Inside private methods	Yes
Inside loops	Yes
Inside conditionals	Yes
At actor level	No for verifier-visible blocks; initialize ghost fields directly
Inside pure functions	No
Inside contracts	No

Common Patterns

Mirror Pattern

Update ghost state to mirror runtime operations:

runtime_field := new_value;
ghost { ghost_field := new_value; };

Tracking Pattern

Track cumulative values:

balance += amount;
ghost { totalIn := totalIn + amount; };

Proof Step Pattern

Break complex proofs into steps:

ghost {
  assert precondition;
  helper_value := compute();
  assert intermediate_property;
};
runtime_operation();
ghost {
  assert postcondition;
};

Loop Synchronization Pattern

Keep ghost state synchronized across iterations:

while (condition) {
  loop:invariant ghost_var == runtime_var;

  runtime_var += 1;
  ghost { ghost_var := ghost_var + 1; };
}

Allowed vs Disallowed Operations

Operation	In Ghost Block
Assign ghost variables	Yes
Read ghost variables	Yes
Read runtime fields	Yes
Mutate runtime fields	No
Mutate array elements	No
Mutate record fields	No
Use assert	Yes
Use old()	Yes
Use runtime:assert	No
Use trap	No
Call ghost functions	Yes
Call runtime/update functions	No

An actor-level ghost { } block may parse, but it is not a supported verifier pattern and fails Viper translation. Use ghost var x : T = initialValue; for initial proof state, and update it from methods with ghost blocks.

Summary

• ghost { } blocks contain verification-only code erased at runtime
• Ghost blocks are the only way to mutate ghost variables
• Ghost blocks can contain assertions, old() expressions, and multiple statements
• Ghost blocks can call ghost func helpers
• Ghost blocks cannot mutate runtime state (fields, arrays, records)
• Ghost blocks cannot use runtime constructs (runtime:assert, trap)
• Zero runtime overhead: all ghost code is erased during compilation
• Use ghost blocks to mirror runtime operations for proof purposes

Related Topics

• Ghost variables for proof-only fields and locals
• Ghost functions for reusable computations inside ghost blocks
• Loop invariants for ghost state in loops
• Assertions for proof checkpoints inside ghost blocks