Skip to main content

Ghost State and Verification

Ghost state exists only for verification. It has no runtime cost — the compiler strips it from the generated bytecode. Use ghost state to track properties that the contract's actual storage can't express.

Ghost storage​

contract Vault {
    storage var totalDeposits: u256 = 0;
    ghost storage spec_sum: u256 = 0;
}

ghost storage spec_sum is a specification-only variable. It tracks the expected sum of all deposits for verification purposes. It can be read in ensures clauses and updated in function bodies, but it generates no SLOAD or SSTORE opcodes.

Using ghost state in specifications​

Inside a contract, assuming std is imported:

pub fn deposit(amount: MinValue<u256, 1>)
    ensures(spec_sum == old(spec_sum) + amount)
{
    let sender: NonZeroAddress = std.msg.sender();
    balances[sender] += amount;
    totalDeposits += amount;
    spec_sum += amount;    // ghost update — no gas cost
}

The ensures clause checks that spec_sum tracks totalDeposits correctly. If the implementation has a bug (e.g., updating totalDeposits but forgetting spec_sum), the verifier catches the discrepancy.

Quantifiers​

For expressing properties over all values, Ora supports forall and exists:

// Every depositor's balance is non-negative
forall account: address => balances[account] >= 0

// There exists an account with a positive balance
exists account: address => balances[account] > 0

Quantifiers appear in specification clauses and ghost blocks. They are checked by the Z3 solver, not at runtime.

The verification pipeline​

When you compile with --verify:

./zig-out/bin/ora build contract.ora --verify

The compiler:

  1. Extracts annotations — finds all requires, ensures, invariant, assert, and assume in the MLIR
  2. Encodes to SMT — translates each annotation into Z3 bitvector/boolean/array expressions
  3. Queries Z3 — for each obligation, checks if assumptions ∧ ¬obligation is satisfiable
  4. Reports results — UNSAT means proven, SAT means counterexample found, UNKNOWN means timeout

Reading verification output​

verification: deposit [ensures] -> UNSAT (12ms)
verification: withdraw [ensures] -> UNSAT (8ms)

UNSAT on an obligation means it's proven — the postcondition holds for all valid inputs.

If a proof fails:

verification: deposit [ensures] -> SAT (15ms)
  counterexample: amount = 0, totalDeposits = 115792...

The counterexample shows specific values that violate the property.

Verification reports​

Use --emit-smt-report to generate detailed audit reports:

./zig-out/bin/ora build contract.ora --verify --emit-smt-report

This produces .smt.report.md and .smt.report.json files with:

  • Every SMT query in SMT-LIB format
  • SAT/UNSAT/UNKNOWN status for each
  • Timing information
  • Counterexamples for failures

Guard elimination​

When the verifier proves a refinement guard is always satisfied, the compiler removes the runtime check. The --verify-stats flag shows how many guards were proven vs. kept:

verification stats: queries=12 sat=2 unsat=10 unknown=0

The vault with ghost state​

error InsufficientBalance(required: u256, available: u256);

comptime const std = @import("std");

contract Vault {
    storage var totalDeposits: u256 = 0;
    storage var balances: map<address, u256>;

    ghost storage spec_sum: u256 = 0;

    log Deposit(account: address, amount: u256);
    log Withdrawal(account: address, amount: u256);

    pub fn deposit(amount: MinValue<u256, 1>)
        requires(amount > 0)
        requires(totalDeposits <= std.constants.U256_MAX - amount)
        ensures(totalDeposits == old(totalDeposits) + amount)
        ensures(spec_sum == old(spec_sum) + amount)
    {
        let sender: NonZeroAddress = std.msg.sender();
        balances[sender] += amount;
        totalDeposits += amount;
        spec_sum += amount;
        log Deposit(sender, amount);
    }

    pub fn withdraw(amount: MinValue<u256, 1>) -> !bool | InsufficientBalance
        requires(amount > 0)
        requires(balances[std.msg.sender()] >= amount)
        ensures(totalDeposits == old(totalDeposits) - amount)
        ensures(spec_sum == old(spec_sum) - amount)
    {
        let sender: NonZeroAddress = std.msg.sender();
        let current: u256 = balances[sender];
        if (current < amount) { return InsufficientBalance(amount, current); }
        balances[sender] = current - amount;
        totalDeposits -= amount;
        spec_sum -= amount;
        log Withdrawal(sender, amount);
        return true;
    }

    pub fn balanceOf(account: address) -> u256 {
        return balances[account];
    }

    pub fn getTotalDeposits() -> u256 {
        return totalDeposits;
    }
}

The ghost storage spec_sum independently tracks the total. The verifier checks that spec_sum stays in sync with totalDeposits across all operations — a conservation proof.

Further reading​