Skip to main content

Ghost Modules

Ghost modules encapsulate ghost state, ghost functions, and proof abstractions into reusable components. They allow you to build verified libraries where implementation details are hidden behind contracts, and clients reason about behavior through ghost state specifications.

Why Ghost Modules​

Individual ghost variables and blocks work well for single-actor verification. But as systems grow, you need:

  • Reusability - Define ghost abstractions once, use in multiple places
  • Encapsulation - Hide implementation details behind contracts
  • Composition - Build complex verified systems from simpler verified parts
  • Abstraction - Let clients reason about module behavior without seeing internals

Ghost modules provide all of these while maintaining the zero-runtime-overhead property of ghost state.

Basic Structure​

A ghost module combines runtime state with ghost state, exposing behavior 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
    };
  };
}

This module demonstrates the core pattern:

  1. Runtime field (balance) - The actual state that exists at runtime
  2. Ghost field (abstract_balance) - The verification model, erased at runtime
  3. Contracts - Specify behavior in terms of ghost state
  4. Ghost blocks - Update ghost state alongside runtime operations

Clients can reason about the Token class through its contracts without knowing the implementation details.

Ghost Fields in Modules​

Ghost fields declared in a module or class are encapsulated within that module. They:

  • Are visible only inside the defining module
  • Cannot be accessed by external callers
  • Can appear in the module's own contracts
  • Are completely erased from compiled output

The modifies Clause​

When a method modifies a ghost field, you must declare it in modifies:

public func deposit(amount : Nat) : ()
  modifies balance, abstract_balance  // Both runtime and ghost
  ensures abstract_balance == old(abstract_balance) + amount;

This mirrors the requirement for runtime fields. The verifier tracks permissions for ghost fields just like runtime fields.

The reads Clause​

Ghost fields can also appear in reads clauses:

public func get_balance() : Nat
  reads abstract_balance
  ensures result == abstract_balance;

Composing Ghost Modules​

Ghost modules can be composed by importing and using them. Each module maintains its own ghost state:

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

Key composition patterns:

  1. Import - The Wallet imports Token to use its verified behavior
  2. Nested objects - Wallet contains a Token instance as a runtime field
  3. Independent ghost state - Wallet has its own total_deposited ghost variable
  4. Contract chaining - add_funds relies on token.deposit's contract

The verifier reasons about each module's ghost state independently. When add_funds calls token.deposit(amount), it uses the contract to conclude the deposit occurred.

Client Reasoning​

Clients of ghost modules reason about behavior through contracts, not implementation:

ghost-module-client.sr9
// Client reasoning about ghost state via contracts
import Inner "./ghost-module-token";

persistent actor {
  transient let tok = Inner.Token();

  public func test_deposit() : async () reads tok {
    let b0 = tok.get_balance();
    tok.deposit(100);
    let b1 = tok.get_balance();
    assert b1 == b0 + 100;
  };
}

The client proves the assertion using only the contracts:

  1. get_balance() ensures result == abstract_balance
  2. deposit(100) ensures abstract_balance == old(abstract_balance) + 100
  3. Second get_balance() returns the new abstract balance
  4. Therefore b1 == b0 + 100

The client never sees balance or abstract_balance directly. It reasons entirely through contracts.

Multiple Ghost Fields​

Modules can have multiple ghost fields tracking different aspects of state:

ghost-module-counter.sr9
// Module with multiple runtime and ghost fields
module {
  public class Counter() {
    // Runtime fields
    var count : Nat = 0;
    var last_increment : Nat = 0;
    var enabled : Bool = true;

    // Ghost model fields
    ghost var model_count : Nat = 0;
    ghost var model_last : Nat = 0;

    public func increment(n : Nat) : ()
      reads enabled
      modifies count, last_increment, model_count, model_last
      requires enabled;
      ensures model_count == old(model_count) + n;
      ensures model_last == n;
    {
      count += n;
      last_increment := n;
      ghost {
        model_count := model_count + n;
        model_last := n;
      };
    };

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

    public func disable() : ()
      modifies enabled
      ensures not enabled;
    {
      enabled := false;
    };
  };
}

This pattern is useful when:

  • Different methods modify different aspects of state
  • You need to track multiple invariants
  • The abstract model requires several components

Ghost State Encapsulation​

Ghost fields are strictly encapsulated within their defining module:

// In module A
module {
  ghost var secret : Nat = 0;  // Only visible inside this module
}

// In module B - WRONG
import A "./module_a";
let x = A.secret;  // ERROR M0318: ghost field is internal

Error M0318: ghost field is internal to its defining module

This encapsulation ensures:

  • Modules control their own abstractions
  • Clients cannot depend on implementation details
  • Ghost state remains a proof artifact, not an interface

Contracts as the Module Interface​

Since ghost fields are internal, the module's contracts form its interface:

ElementVisible to Clients
Method signaturesYes
requires clausesYes
ensures clausesYes
Runtime fieldsOnly if public
Ghost fieldsNo
Ghost blocksNo

Clients verify their code against contracts. The module verifies that its implementation satisfies those contracts. If a client needs an observable value derived from ghost state, expose it through a method contract or proof-only helper rather than direct field access.

How Ghost Modules Translate​

During verification, ghost modules translate to the verification backend with ghost fields as regular verification fields:

// Conceptual Viper output
method Token$deposit($obj: Ref, amount: Int)
  requires acc($obj.fld$balance, write)
  requires acc($obj.fld$abstract_balance, write)
  ensures $obj.fld$abstract_balance == old($obj.fld$abstract_balance) + amount
{
  $obj.fld$balance := $obj.fld$balance + amount;
  $obj.fld$abstract_balance := $obj.fld$abstract_balance + amount;
}

During compilation to WebAssembly, ghost fields and ghost blocks are erased:

;; Compiled output - only runtime field operations remain
(func $deposit (param $amount i32)
  ;; balance += amount
  ;; abstract_balance operations are erased
)

Design Guidelines​

Keep Ghost State Simple​

Ghost state should model the essential abstraction:

// Good - simple abstract model
ghost var total : Nat = 0;

// Avoid - overly complex ghost state
ghost var history : Seq<(Nat, Nat, Bool, Text)> = Seq.empty();

Match Ghost to Runtime Boundaries​

Update ghost state at the same points as runtime state:

public func process(n : Nat) : ()
  modifies data, ghost_model
{
  data := transform(n);          // Runtime update
  ghost { ghost_model := n; };   // Ghost update mirrors it
}

Use Contracts for Specification​

Specify module behavior in contracts, not just ghost state:

// Good - contract specifies observable behavior
public func deposit(amount : Nat) : ()
  ensures abstract_balance == old(abstract_balance) + amount;

// Less useful - contract doesn't specify behavior
public func deposit(amount : Nat) : ()
  modifies abstract_balance  // What happens to it?

Compose Through Contracts​

When building on other ghost modules, rely on their contracts:

public func add_funds(amount : Nat) : ()
  modifies token, total_deposited
  ensures total_deposited == old(total_deposited) + amount;
{
  token.deposit(amount);  // Uses Token's contract
  ghost { total_deposited := total_deposited + amount };
}

Common Patterns​

Abstract Model Pattern​

Maintain a ghost model that simplifies the runtime representation:

// Runtime: complex data structure
var items : [var Item] = [var];

// Ghost: simple abstract view
ghost var item_count : Nat = 0;

Conservation Pattern​

Track what goes in and out across module boundaries:

ghost var total_in : Nat = 0;
ghost var total_out : Nat = 0;
invariant balance + total_out == total_in;

Protocol Pattern​

Track state machine transitions:

type State = { #Initial; #Running };

ghost var state : State = #Initial;

public func start() : ()
  modifies state
  requires state == #Initial;
  ensures state == #Running;
{
  ghost { state := #Running; };
}

Summary​

  • Ghost modules encapsulate ghost state within reusable components
  • Ghost fields are internal to their defining module (Error M0318 if accessed externally)
  • Contracts form the public interface; clients reason through contracts
  • Modules compose by importing and using other modules' contracts
  • Ghost fields appear in modifies and reads clauses like runtime fields
  • Ghost modules translate to verification backend with ghost fields included, but are erased at runtime
  • Design ghost state to be simple abstractions that mirror runtime behavior