Ghost Functions (ghost func)

Ghost functions are proof-only pure helpers. They let you name reusable specification logic, compute ghost values, and keep complex contracts readable without adding runtime code.

Use a ghost function when the logic is needed by verification but should not exist in the deployed program.

Basic Syntax

Declare a ghost function with ghost func:

ghost func name(x : Nat) : Nat
  requires x > 0;
  ensures result >= x;
{
  x + 1
};

Ghost functions:

• Are verification-only and erased from runtime output
• Are pure helpers, so they return values instead of mutating state
• Can be used from contracts, lemmas, ghost blocks, and other ghost functions
• Use requires and ensures, not entry_requires
• Can be public in proof-facing modules; actor-local ghost helpers are usually private because public actor methods are runtime entry points

Runtime and Ghost State

The common pattern is to update runtime state normally, then use a ghost function inside a ghost { } block to update the proof model.

ghost-func-basic.sr9

// Ghost functions are proof-only pure helpers erased from runtime output.
persistent actor {
  var balance : Nat = 0;
  ghost var model : Nat = 0;

  invariant balance == model;

  ghost func addModel(current : Nat, amount : Nat) : Nat
    ensures result == current + amount;
  {
    current + amount
  };

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

Here addModel is not a runtime helper. It only computes the next ghost model value during verification. The compiled actor keeps balance, but the model field, addModel, and the ghost block are erased.

Threading Spec Collections

Ghost functions are useful with spec collections because collection updates return new immutable values. A helper can package a repeated update pattern and return the next collection value.

threading-function.sr9

// Threading through functions: pass and return collections
persistent actor {
  // Ghost function that returns an updated map value.
  ghost func addEntry(m : Map<Nat, Int>, k : Nat, v : Int) : Map<Nat, Int> {
    Map.update(m, k, v)
  };

  // Function that adds multiple entries
  ghost func addThree(m : Map<Nat, Int>) : Map<Nat, Int> {
    let m1 = addEntry(m, 1, 100);
    let m2 = addEntry(m1, 2, 200);
    addEntry(m2, 3, 300)
  };

  public func demo() : async () {
    ghost {
      let empty : Map<Nat, Int> = Map.empty();

      // Function call returns a new map; empty remains usable.
      let result = addThree(empty);

      // result is the final threaded value.
      assert Map.card(result) == 3;
      assert Map.contains(1, result);
      assert Map.contains(2, result);
      assert Map.contains(3, result);
    };
  };

  public func chainFunctions() : async () {
    ghost {
      let m0 : Map<Nat, Int> = Map.empty();

      // Chain function calls by threading the returned values.
      let m1 = addEntry(m0, 1, 10);
      let m2 = addEntry(m1, 2, 20);
      let m3 = addEntry(m2, 3, 30);

      assert Map.card(m3) == 3;
    };
  };
}

This example calls ghost functions from a ghost block. That is valid: the calls are proof-only and disappear from runtime output.

Abstract Ghost Functions

When you want a proof helper interface before writing the body, use ghost abstract func and omit the body:

module {
  public ghost abstract func distance(a : Int, b : Int) : Nat
    requires true;
    ensures result >= 0;
}

An abstract ghost function has contracts but no implementation. Callers must prove its requires clauses, and the verifier may use its ensures clauses after a call. The postconditions are assumptions until the abstract declaration is refined with a body.

signature-basic.sr9

// Abstract signature-only declarations: proof-only functions with contracts but no body
module {
  // Abstract ghost function with contract only - no runtime implementation
  public ghost abstract func abs(x : Int) : Nat
    requires true;
    ensures result >= 0;
    ensures x >= 0 ==> result == x;
    ensures x < 0 ==> result == -x;

  // Another abstract signature-only proof helper
  public ghost abstract func max(a : Nat, b : Nat) : Nat
    requires true;
    ensures result >= a;
    ensures result >= b;
    ensures result == a or result == b;

  // Proof-only code can use signature-only declarations.
  public ghost func demo(x : Int) : Nat
    ensures result >= 0;
  {
    abs(x)
  };
}

Use abstract for VDD placeholders and proof interfaces. Do not mark these as trusted unless you are intentionally adding a permanent unchecked assumption to the trusted base.

Where Ghost Functions Can Be Used

Context	Allowed
requires / ensures	Yes
assert proof steps	Yes
ghost { } blocks	Yes
Lemma bodies	Yes
Other ghost functions	Yes
Runtime expressions	No
entry_requires	No

entry_requires is executable runtime-entry checking for concrete public runtime functions. Ghost functions are verification-only, so they should use logical requires clauses instead.

Ghost Function vs Ghost Block

Use a ghost function to compute or specify a value. Use a ghost block to perform proof-only statements, especially ghost variable updates.

ghost func next(current : Nat, delta : Nat) : Nat
  ensures result == current + delta;
{
  current + delta
};

ghost {
  model := next(model, amount);
};

The function is reusable and pure. The block is where the ghost field mutation happens.

Ghost Function vs Lemma

Both are proof-only, but they have different jobs:

Construct	Typical Result	Use It For
ghost func	A value	Reusable proof-only computations and specification helpers
lemma	Usually ()	Establishing facts for later proof steps
abstract ghost func	A specified value with no body	VDD proof interfaces and temporary mathematical placeholders
abstract lemma	A specified fact with no proof body	VDD proof obligations and proof-module interfaces

If you need a value in a contract, use a ghost function. If you need to establish a fact before an assertion or postcondition, use a lemma.

Restrictions

Ghost functions are proof-only, so they cannot be used to implement runtime behavior:

• Do not call ghost functions from runtime code.
• Do not put ghost functions in entry_requires.
• Do not mutate actor fields, arrays, or mutable records from a ghost function.
• Do not use shared, query, or caller patterns on ghost functions.
• Do not treat abstract ghost functions as proved implementations; their postconditions are assumptions until refined.

If the helper is needed at runtime, write a normal function or a pure func with a body and keep its implementation runtime-safe.

Summary

• ghost func defines a reusable proof-only pure helper.
• Ghost functions are erased from runtime output.
• They can appear in contracts, ghost blocks, lemmas, and other ghost functions.
• Use ghost abstract func for bodyless proof interfaces and VDD placeholders.
• Use ghost blocks, not ghost functions, to mutate ghost variables.
• Use requires for ghost function preconditions; entry_requires is for concrete public runtime entry points.

Related Topics

• Ghost blocks for mutating ghost state
• Ghost modules for packaging proof helpers behind module boundaries
• Pure functions for runtime-available side-effect-free helpers
• Trusted code for deliberate unchecked proof boundaries