Invariant Preservation

Every public/exported method must maintain actor invariants. The verifier checks this by injecting invariant conditions into method contracts automatically, and by checking the invariant around suspending await points.

How Preservation Works

When you declare an actor invariant, the verifier transforms every public method to:

1. Require the invariant holds on entry
2. Ensure the invariant holds on exit

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

  // The verifier sees this as:
  // requires balance >= 0
  // ensures balance >= 0
  public func deposit(amount : Nat) : async ()
    modifies balance
    ensures balance == old(balance) + amount;
  {
    balance += amount;
  }
}

The invariant balance >= 0 becomes an implicit precondition and postcondition for every public method. It is a verification obligation, not a generated runtime guard; use entry_requires or runtime:assert when a runtime boundary check is needed.

Establishment vs Preservation

There are two distinct verification obligations:

Obligation	Applies To	What It Checks
Establishment	__init__	Invariant holds after initialization
Preservation	All other public methods	If invariant holds on entry, it holds on exit

Establishment in __init__

The __init__ method does not assume the invariant holds (the actor is not yet initialized). Instead, it must establish the invariant:

persistent actor {
  var count : Nat = 0;  // Initial value must satisfy invariant
  invariant count <= 100;

  // __init__ does NOT require count <= 100
  // __init__ MUST ensure count <= 100
}

If the initial values violate the invariant, verification fails:

persistent actor {
  var count : Nat = 200;  // ERROR: 200 > 100
  invariant count <= 100;  // Verification fails
}

Preservation in Public Methods

Every public method assumes the invariant holds on entry and must prove it holds on exit:

persistent actor {
  var count : Nat = 0;
  invariant count <= 100;

  public func increment() : async ()
    modifies count
    entry_requires count < 100;
    requires count < 100;  // Needed to preserve invariant
  {
    count += 1;
    // Verifier checks: count <= 100 still holds
  }
}

Without the precondition count < 100, the method could violate the invariant by incrementing count from 100 to 101.

Verification Failures

When a method fails to preserve an invariant, the verifier reports a fold failure:

Folding $Inv($Self) might fail. Assertion balance >= 0 might not hold.

This means the method modified state in a way that violates the invariant constraint.

Example: Failing Preservation

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

  public func withdraw(amount : Nat) : async ()
    modifies balance
  {
    balance -= amount;  // ERROR: Could make balance negative
  }
}

The verifier cannot prove balance >= 0 after an arbitrary withdrawal. Fix by adding a precondition:

public func withdraw(amount : Nat) : async ()
  modifies balance
  entry_requires amount <= balance;
  requires amount <= balance;  // Ensures preservation
{
  balance -= amount;
}

Private Methods and Invariants

Private methods are not checked for invariant preservation at their own boundaries. They can temporarily violate invariants as long as the calling public method restores them before the next public boundary or suspending await:

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

  private func helper() : () modifies x {
    x := -1;  // Temporarily violates invariant
    x := 0;   // Restores invariant
  }

  public func run() : async () modifies x {
    helper();
    // Invariant must hold here when run() returns
  }
}

The verifier only checks that x >= 0 holds when run() returns, not at the boundaries of helper(). If a helper itself performs a suspending await, the invariant must hold at that await.

Invariants Across Await

At suspending await boundaries, the invariant is temporarily released and then re-assumed. This models the possibility that other actors called public methods while waiting:

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 is re-assumed here
    assert counter >= 0;  // Valid: invariant holds after await
  }
}

The verification models await as:

1. Prove invariant holds before the await
2. Release (exhale) the invariant
3. Assume (inhale) the invariant after await resumes

Violation Before Await

The invariant must hold before each await point:

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

  private func noop() : async () {}

  public func run() : async () modifies counter {
    counter := -1;  // ERROR: Invariant violated
    try { await noop(); } catch (_) {};  // Verification fails here
  }
}

Proving Preservation

To prove an invariant is preserved, ensure every code path maintains the invariant property.

Conservation Laws

For resource-like invariants, track that additions and removals balance:

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;
    // Sum remains 100
  }
}

Bounds Preservation

For bounded invariants, add preconditions that prevent violations:

persistent actor {
  var count : Nat = 0;
  invariant count <= 1000;

  public func add(n : Nat) : async ()
    modifies count
    entry_requires count + n <= 1000;
    requires count + n <= 1000;  // Prevents overflow of bound
  {
    count += n;
  }
}

Conditional Invariants

When invariants use implication, ensure the antecedent is properly tracked:

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

  public func lock() : async ()
    modifies locked
    entry_requires balance > 0;
    requires balance > 0;  // Ensure implication holds
  {
    locked := true;
  }

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

Common Mistakes

Missing Precondition

// WRONG - no precondition to prevent violation
persistent actor {
  var x : Nat = 0;
  invariant x <= 10;

  public func add(n : Nat) : async () modifies x {
    x += n;  // Could exceed 10
  }
}

// CORRECT - precondition ensures preservation
persistent actor {
  var x : Nat = 0;
  invariant x <= 10;

  public func add(n : Nat) : async () modifies x
    entry_requires x + n <= 10;
    requires x + n <= 10;
  {
    x += n;
  }
}

Forgetting Await Boundaries

// WRONG - invariant violated before await
persistent actor {
  var flag : Bool = true;
  invariant flag;

  private func doWork() : async () {}

  public func process() : async () modifies flag {
    flag := false;
    try { await doWork(); } catch (_) {};  // ERROR: invariant must hold here
    flag := true;
  }
}

// CORRECT - maintain invariant at await boundaries
persistent actor {
  var flag : Bool = true;
  invariant flag;

  private func doWork() : async () {}

  public func process() : async () modifies flag {
    try { await doWork(); } catch (_) {};
    // All modifications happen between awaits
  }
}

Unbalanced Resource Updates

// WRONG - conservation law violated
persistent actor {
  var a : Nat = 50;
  var b : Nat = 50;
  invariant a + b == 100;

  public func transfer(n : Nat) : async ()
    modifies a, b
    entry_requires n <= a;
    requires n <= a;
  {
    a -= n;
    // ERROR: forgot to add to b
  }
}

// CORRECT - both sides updated
persistent actor {
  var a : Nat = 50;
  var b : Nat = 50;
  invariant a + b == 100;

  public func transfer(n : Nat) : async ()
    modifies a, b
    entry_requires n <= a;
    requires n <= a;
  {
    a -= n;
    b += n;
  }
}

Debugging Preservation Failures

When the verifier reports a preservation failure:

1. Identify the invariant - Which invariant condition failed?
2. Check the modification - What field changes could violate it?
3. Add preconditions - What input constraints prevent violation?
4. Use assertions - Add assert statements to isolate where preservation breaks

public func problematic(x : Nat) : async () modifies count {
  assert count + x <= 100;  // Check before modification
  count += x;
  assert count <= 100;      // Verify preservation
}

Summary

• The verifier injects invariants as implicit pre/postconditions on public methods
• __init__ must establish invariants; other methods must preserve them
• Private methods can temporarily violate invariants
• Invariants must hold at each await boundary
• Preservation failures indicate missing preconditions or logic errors
• Use preconditions to constrain inputs that could violate invariants

Related Topics

• Declaring invariants for syntax and allowed expressions
• entry_requires for runtime entry guards that complement invariant proofs
• assert for isolating preservation failures
• Async await semantics for interleaving after suspension