Declaring Invariants

An invariant is a property that must hold at the actor boundaries the verifier cares about: after initialization, at public/exported method boundaries, and before/after suspending await points. Actor invariants express global facts that every public operation must preserve.

Basic Syntax

Declare invariants at the actor or object level using the invariant keyword:

persistent actor Counter {
  var count : Nat = 0;

  invariant count <= 1000;

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

The invariant count <= 1000 must hold:

After actor initialization
On entry to each public/exported method
On exit from each public/exported method
At suspending await boundaries

Invariants vs Contracts

Feature	`invariant`	`requires`/`ensures`
Scope	Entire actor	Single method
Checked	All public methods	That method only
Purpose	Global state properties	Method-specific contracts

Invariants are implicitly conjoined with every public method's verification contract:

persistent actor {
  var balance : Int = 0;
  invariant balance >= 0;

  // Effectively becomes:
  // requires balance >= 0
  // ensures balance >= 0
  public func deposit(amount : Nat) : async ()
    modifies balance
    ensures balance == old(balance) + amount;
  {
    balance += amount;
  }
}

Where Invariants Can Appear

Actor Level

persistent actor Account {
  var balance : Nat = 0;
  var frozen : Bool = false;

  invariant balance >= 0;
  invariant frozen ==> balance > 0;
}

Object Level

Objects created with object { } can also have invariants:

module Factory {
  public let MAX : Nat = 100;

  public func create(init : Nat) : { get : () -> Nat }
    requires init <= MAX;
  {
    object {
      var count : Nat = init;

      invariant count <= MAX;

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

Multiple Invariants

Declare multiple invariants as separate statements. They are conjoined (AND-ed together):

persistent actor Token {
  var supply : Nat = 1000;
  var locked : Bool = false;

  invariant supply <= 10000;
  invariant locked ==> supply > 0;
  invariant supply >= 0;
}

This is equivalent to:

(supply <= 10000) and (locked ==> supply > 0) and (supply >= 0)

What Can Appear in Invariants

Allowed

Actor fields: Direct references to var fields
Record field access: range.min <= range.max
Comparisons: ==, !=, <, <=, >, >=
Logical operators: and, or, not, ==>
Arithmetic: +, -, *
Pure function calls: Calls to pure functions
Quantifiers: forall, exists over arrays

persistent actor {
  var data : [var Int] = [var 1, 2, 3];

  invariant forall<Nat>(pure func (i : Nat) : Bool =
    i < data.size() ==> data[i] >= 0);
}

Not Allowed

Expression	Reason
`old(x)`	Invariants describe current state, not change
External heap	Must access only actor's own fields
Method calls	Side effects not allowed
Allocations	`[]` or record literals not allowed

The `old()` Restriction

Invariants cannot use old():

// WRONG - old() not allowed in invariants
persistent actor {
  var counter : Int = 0;
  invariant counter >= old(counter);  // ERROR
}

Invariants must describe a property of the current state. If you need to express monotonicity or change bounds, use ensures in method contracts:

// CORRECT - express change in postcondition
persistent actor {
  var counter : Int = 0;
  invariant counter >= 0;

  public func increment() : async ()
    modifies counter
    ensures counter >= old(counter);  // Monotonicity here
  {
    counter += 1;
  }
}

Self-Rooted Heap Access

Invariants may only access heap locations belonging to the actor itself. External state is not allowed:

module Ext {
  public type Cell = { var x : Int };
  public let cell : Cell = { var x = 0 };
}

// WRONG - accesses external state
persistent actor {
  var local : Int = 0;
  invariant Ext.cell.x >= 0;  // ERROR: non-self heap access
}

Record Field Invariants

Invariants can reference fields of record-typed state:

persistent actor {
  type Range = { min : Int; max : Int };
  transient var range : Range = { min = 0; max = 100 };

  invariant range.min <= range.max;

  public func expand(delta : Int) : async ()
    modifies range
    entry_requires delta >= 0;
    requires delta >= 0;
    ensures range.min == old(range.min) - delta;
    ensures range.max == old(range.max) + delta;
  {
    range := { min = range.min - delta; max = range.max + delta };
  }
}

Initialization and `init`

The initialization method (__init__) is special:

Does NOT require the invariant as a precondition (actor isn't yet initialized)
MUST establish the invariant as a postcondition

The verifier checks that initial field values satisfy all invariants:

persistent actor {
  var balance : Int = 0;  // Initial value must satisfy invariant
  invariant balance >= 0;  // OK: 0 >= 0
}

persistent actor {
  var balance : Int = -1;  // Initial value violates invariant
  invariant balance >= 0;  // ERROR: verification fails
}

Public vs Private Methods

Invariants apply to public/exported method boundaries. Private helpers are checked through the public method that calls them, so they may temporarily break an invariant if the caller restores it before returning or suspending:

persistent actor {
  var counter : Int = 0;
  invariant counter >= 0;

  // Private: invariant not checked at helper boundaries
  private func helper() : () modifies counter {
    counter := -1;  // Temporarily violates invariant
    counter := 0;   // Restores invariant
  }

  // Public: invariant must hold before and after
  public func run() : async () modifies counter {
    helper();       // Invariant temporarily violated inside
    assert counter >= 0;  // Must hold when run() returns
  }
}

Invariants Across Await

Actor invariants are proved before a suspending await and re-assumed after it resumes:

persistent actor {
  var counter : Int = 0;
  invariant counter >= 0;

  private func bump() : async () modifies counter {
    counter += 1;
  }

  public func run() : async () modifies counter {
    try { await bump(); } catch (_) {};
    // Invariant holds here: counter >= 0
    assert counter >= 0;
  }
}

After each suspending await, you can assume the invariant holds because any interleaving public call must also preserve it. You cannot assume fields kept the exact values they had before the await unless a stronger invariant or frame fact proves that.

Common Mistakes

Invariant in Function Body

// WRONG - invariant cannot appear inside a method
persistent actor {
  var x : Int = 0;

  public func bad() : async () {
    invariant x >= 0;  // ERROR: unexpected token
  }
}

// CORRECT - invariant at actor level
persistent actor {
  var x : Int = 0;
  invariant x >= 0;

  public func good() : async () { }
}

Invariant in Stateless Object

// WRONG - no mutable state to constrain
module Empty {
  invariant true;  // ERROR: invariant requires mutable state
}

// Objects/actors need mutable fields for invariants to make sense
persistent actor Valid {
  var state : Int = 0;
  invariant state >= 0;
}

Invariant preservation for how methods prove they maintain global facts
Invariant patterns for conservation, bounds, and conditional rules
old() restrictions for why invariants describe current state only
Async commit points for invariant checks around suspension
Footprints for the fields a method may read or modify while preserving invariants

Using `old()` in Invariants

// WRONG
persistent actor {
  var x : Int = 0;
  invariant x >= old(x);  // ERROR: old() not allowed
}

// CORRECT - use ensures in methods
persistent actor {
  var x : Int = 0;
  invariant x >= 0;

  public func increase() : async () modifies x
    ensures x >= old(x);
  { x += 1; }
}

Loop Invariants Are Different

Actor/object invariants (invariant) and loop invariants (loop:invariant) are distinct:

persistent actor {
  var total : Nat = 0;
  invariant total <= 1000;  // Actor invariant

  public func sum(n : Nat) : async Nat
    modifies total
    entry_requires total + n <= 1000;
    requires total + n <= 1000;
    ensures result == old(total) + n;
  {
    var i = 0;
    while (i < n) {
      loop:invariant i <= n;         // Loop invariant
      loop:invariant total <= 1000;  // Can reference actor state
      total += 1;
      i += 1;
    };
    total
  }
}

See Loop Invariants for details on loop:invariant.

Summary

invariant declares properties that hold at public method boundaries
Place invariants at actor or object level, not inside methods
Multiple invariants are conjoined (AND-ed)
Allowed: actor fields, record access, comparisons, logic, pure calls, quantifiers
Not allowed: old(), external heap, method calls, allocations
__init__ must establish invariants; other methods must preserve them
Private methods can temporarily violate invariants
Invariants are re-established after each await

Basic Syntax​

Invariants vs Contracts​

Where Invariants Can Appear​

Actor Level​

Object Level​

Multiple Invariants​

What Can Appear in Invariants​

Allowed​

Not Allowed​

The old() Restriction​

Self-Rooted Heap Access​

Record Field Invariants​

Initialization and __init__​

Public vs Private Methods​

Invariants Across Await​

Common Mistakes​

Invariant in Function Body​

Invariant in Stateless Object​

Related Topics​

Using old() in Invariants​

Loop Invariants Are Different​

Summary​