Invariant Patterns

Common invariant shapes that appear in real actor-based systems. Use these patterns as building blocks for expressing the global correctness properties every public method must preserve.

Non-Negativity

The simplest pattern: a numeric field must never go negative.

persistent actor {
  var balance : Int = 0;

  invariant balance >= 0;

  public func deposit(amount : Nat) : async ()
    modifies balance
    ensures balance == old(balance) + amount;
  {
    balance += amount;
  };

  public func withdraw(amount : Nat) : async Bool
    modifies balance
    ensures result == (old(balance) >= amount);
    ensures result ==> balance == old(balance) - amount;
    ensures (not result) ==> balance == old(balance);
  {
    if (balance >= amount) {
      balance -= amount;
      true
    } else {
      false
    }
  };
}

The withdrawal returns false instead of violating the invariant. This is a common pattern: guard the operation rather than trap.

Bounded Counters

A variation constrains both lower and upper bounds:

persistent actor {
  var count : Nat = 0;

  invariant count <= 1000;

  public func increment() : async Bool
    modifies count
    ensures result ==> count == old(count) + 1;
    ensures (not result) ==> count == old(count);
  {
    if (count < 1000) {
      count += 1;
      true
    } else {
      false
    }
  };
}

Conservation Laws

When resources move between fields, the total remains constant.

persistent actor {
  var available : Nat = 100;
  var locked : Nat = 0;

  invariant available + locked == 100;

  public func lock(amount : Nat) : async ()
    modifies available, locked
    entry_requires amount <= available;
    requires amount <= available;
  {
    available -= amount;
    locked += amount;
  };

  public func unlock(amount : Nat) : async ()
    modifies available, locked
    entry_requires amount <= locked;
    requires amount <= locked;
  {
    locked -= amount;
    available += amount;
  };
}

Both operations modify two fields symmetrically. The invariant is preserved because every subtraction has a matching addition.

Tracking with Ghost State

For more complex conservation laws, ghost state tracks the abstract property:

persistent actor {
  var balance : Nat = 0;
  ghost var totalDeposits : Nat = 0;
  ghost var totalWithdrawals : Nat = 0;

  invariant balance == totalDeposits - totalWithdrawals;

  public func deposit(amount : Nat) : async ()
    entry_requires amount > 0;
    requires amount > 0;
    modifies balance
  {
    balance += amount;
    ghost { totalDeposits += amount; };
  };

  public func withdraw(amount : Nat) : async ()
    entry_requires amount <= balance;
    requires amount <= balance;
    modifies balance
  {
    balance -= amount;
    ghost { totalWithdrawals += amount; };
  };
}

The ghost variables exist only for verification. They prove that the balance correctly reflects all deposits and withdrawals without adding runtime storage or API surface.

Conditional Invariants

Properties that depend on state flags use implication (==>).

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

  invariant locked ==> balance > 50;

  public func lock() : async Bool
    modifies locked
    reads balance
    ensures result == true ==> locked == true;
    ensures result == false ==> locked == old(locked);
  {
    if (balance > 50) {
      locked := true;
      true
    } else {
      false
    }
  };

  public func unlock() : async ()
    modifies locked
  {
    locked := false;
    // Safe: implication vacuously true when locked = false
  };

  public func withdraw(amount : Nat) : async Bool
    modifies balance
    reads locked
    ensures result == true ==> balance == old(balance) - amount;
    ensures result == false ==> balance == old(balance);
  {
    // If locked, must preserve minimum balance
    if (not locked or balance > amount + 50) {
      if (balance >= amount) {
        balance -= amount;
        true
      } else {
        false
      }
    } else {
      false
    }
  };
}

When locked is false, the implication locked ==> balance > 50 is vacuously true. When locked is true, every operation must maintain balance > 50.

Multi-Field Relationships

Complex invariants relate multiple fields:

persistent actor {
  var balance : Nat = 100;
  var debt : Nat = 0;
  var locked : Bool = false;

  invariant balance >= debt;          // Solvency
  invariant locked ==> balance > 50;  // Lock floor
  invariant debt <= 1000;             // Debt cap

  public func borrow(amount : Nat) : async Bool
    modifies debt
    reads balance
    ensures result == true ==> debt == old(debt) + amount;
    ensures result == false ==> debt == old(debt);
  {
    if (debt + amount <= balance and debt + amount <= 1000) {
      debt += amount;
      true
    } else {
      false
    }
  };

  public func withdraw(amount : Nat) : async Bool
    modifies balance
    reads debt, locked
    ensures result == true ==> balance == old(balance) - amount;
    ensures result == false ==> balance == old(balance);
  {
    // Must stay solvent and respect lock floor
    if (balance >= amount + debt and (not locked or balance > amount + 50)) {
      balance -= amount;
      true
    } else {
      false
    }
  };
}

Each invariant is checked independently. The guards in each method ensure all three hold after modification.

Record Field Relationships

Invariants can express relationships within record-typed fields:

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

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

The shrink precondition ensures min never exceeds max after the modification.

Array Element Invariants

Use quantifiers to express properties over all array elements:

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

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

  public func setPositive(idx : Nat, value : Nat) : async ()
    modifies data
    entry_requires idx < data.size();
    requires idx < data.size();
  {
    data[idx] := value;  // Nat is always >= 0
  };
}

The quantified invariant says: for every valid index, the element is non-negative. Methods that modify array elements must ensure the property holds for all elements, not just the modified one.

Fixed Size Arrays

persistent actor {
  var buffer : [var Nat] = [var 0, 0, 0];

  invariant buffer.size() == 3;

  public func update(idx : Nat, val : Nat) : async ()
    modifies buffer
    entry_requires idx < 3;
    requires idx < 3;
  {
    buffer[idx] := val;
    // Size unchanged, invariant preserved
  };
}

Pure Function Invariants

When invariant expressions become complex, extract them into pure functions:

persistent actor {
  var x : Int = 5;
  var y : Int = 3;

  pure func max(a : Int, b : Int) : Int {
    if (a > b) a else b
  };

  invariant max(x, y) <= 100;

  public func setX(v : Int) : async ()
    modifies x
    entry_requires v <= 100;
    requires v <= 100;
  {
    x := v;
  };

  public func setY(v : Int) : async ()
    modifies y
    entry_requires v <= 100;
    requires v <= 100;
  {
    y := v;
  };
}

The pure function max can appear in the invariant because it has no side effects.

Invariants Across Await

After a suspending await, you can assume the invariant holds:

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 (_) {};
    assert counter >= 0;  // Valid: invariant re-established
  };
}

The verifier models this as: prove the invariant holds before await, then assume it holds after. This reflects that other actors may have called public methods during the await.

What Can Change

Across await, actor state that other public methods can touch may have changed. The invariant is the main guaranteed property; exact values need a stronger invariant, a fresh local snapshot, or an explicit post-await re-check:

persistent actor {
  var value : Int = 0;

  invariant value >= 0;

  private func work() : async () { };

  public func process() : async ()
    modifies value
    ensures value >= 0;  // Invariant holds, but exact value unknown
  {
    value := 10;
    try { await work(); } catch (_) {};
    // value could be anything >= 0 here
    assert value >= 0;  // Valid
    // assert value == 10;  // WRONG: may have changed
  };
}

Anti-Patterns to Avoid

Too-Strict Invariants

// WRONG - invariant impossible to satisfy during operations
persistent actor {
  var processing : Bool = false;
  var data : Nat = 0;

  invariant not processing;  // Can never set processing = true

  public func process() : async ()
    modifies processing, data
  {
    processing := true;   // Violates invariant
    data += 1;
    processing := false;
  };
}

Invariants must hold at public method boundaries, not necessarily during the method body. But this invariant says processing can never be true at any boundary, which prevents its use.

Trivially True Invariants

// USELESS - adds no verification value
persistent actor {
  var x : Nat = 0;
  invariant true;  // Always holds, proves nothing
}

Invariants should express meaningful properties about the state.

Overlapping Responsibilities

// REDUNDANT - same constraint expressed twice
persistent actor {
  var count : Nat = 0;

  invariant count >= 0;  // Nat is already >= 0
  invariant count <= 100;  // This is the meaningful constraint
}

The first invariant is redundant because Nat is already non-negative. Focus on properties that aren't guaranteed by the type system.

Choosing the Right Pattern

Situation	Pattern	Example
Resource tracking	Non-negativity	balance >= 0
Fixed resources	Conservation	a + b == total
State-dependent rules	Conditional	locked ==> balance > 0
Multiple constraints	Multi-field	balance >= debt
Structured data	Record fields	range.min <= range.max
Collection properties	Quantified	forall(i): data[i] >= 0
Complex expressions	Pure functions	max(x, y) <= limit

Summary

• Non-negativity prevents resources from going negative
• Conservation laws ensure resources move between fields without loss
• Conditional invariants use implication for state-dependent rules
• Multi-field relationships express constraints across multiple fields
• Quantified invariants express properties over all collection elements
• Pure functions simplify complex invariant expressions
• Guard operations instead of trapping when invariant would be violated
• Use ghost state to track abstract properties for conservation proofs

Related Topics

• Declaring invariants for syntax and allowed expressions
• Invariant preservation for failure modes and debugging
• Ghost variables for abstract accounting state
• Quantifiers for array and collection-wide properties
• Async verification frames for what can change across await