Upgrade Compatibility

When upgrading an actor, the runtime checks that stable variable types are compatible between versions. This prevents data loss and forces intentional migrations for breaking schema changes.

Stable Subtyping

Upgrade compatibility uses stable subtyping, which is stricter than regular subtyping. While regular subtyping allows data loss (like dropping record fields), stable subtyping prevents it:

Rule	Regular Subtyping	Stable Subtyping
Drop record fields	Allowed	Rejected
Remove variant cases	Allowed	Rejected
Promote to `Any`	Allowed	Rejected
Narrow types (Int to Nat)	Allowed	Rejected
Widen types (Nat to Int)	Allowed	Allowed
Add variant cases	Allowed	Allowed
Add optional fields	Allowed	Allowed

Safe Changes

These changes are always safe during upgrades:

Adding New Fields

New stable fields are initialized from their declaration when the upgraded canister first runs. This is safe because no previous value exists for the new field:

compat-safe-add.sr9
// Safe upgrade: adding new stable fields
// Version 2 adds 'total' and 'lastUpdate' fields - compatible with version 1

persistent actor {
  var counter : Nat = 0;                // Existing field - preserved
  var total : Nat = 0;                  // New field - initialized to default
  var lastUpdate : ?Int = null;         // New optional field - safe to add

  invariant counter >= 0;
  invariant total >= 0;

  public func increment() : async Nat
    modifies counter, total, lastUpdate
    ensures counter == old(counter) + 1;
    ensures total == old(total) + 1;
    ensures result == counter;
  {
    counter += 1;
    total += 1;
    lastUpdate := ?42;
    counter
  };

  public query func getTotal() : async Nat
    reads total
    ensures result == total;
  {
    total
  };
}

Widening Types

A type can be widened if every old value is also valid in the new type:

compat-safe-widen.sr9
// Safe upgrade: widening types (Nat to Int)
// If old version had 'var amount : Nat', changing to Int is safe
// because every Nat value is also a valid Int

persistent actor {
  var amount : Int = 0;                 // Widened from Nat - safe upgrade
  var balance : Int = 100;              // Widened from Nat - safe upgrade

  invariant balance >= 0;               // Invariant still valid after widening

  public func transfer(delta : Int) : async Int
    modifies amount
    ensures amount == old(amount) + delta;
    ensures result == amount;
  {
    amount += delta;
    amount
  };
}

Common safe widenings:

Nat to Int (every natural number is an integer)
Nat8 to Nat16 to Nat32 to Nat64
T to ?T (value becomes optional)

Adding Variant Cases

New variant cases can be added because existing data already has one of the old cases:

compat-safe-variant.sr9
// Safe upgrade: adding new variant cases
// Old version had { #pending; #done }, new version adds #cancelled

persistent actor {
  var status : { #pending; #done; #cancelled } = #pending;  // Added #cancelled

  public func cancel() : async ()
    modifies status
    ensures status == #cancelled;
  {
    status := #cancelled;
  };

  public func complete() : async ()
    modifies status
    ensures status == #done;
  {
    status := #done;
  };

  public query func isPending() : async Bool
    reads status
    ensures result == (status == #pending);
  {
    status == #pending
  };
}

Breaking Changes

These changes break upgrade compatibility when compared against a previous deployed version. The standalone snippets can typecheck; the compatibility error is produced by the upgrade/stability comparison.

Removing Stable Fields

Removing a stable field without a migration function causes error M0169:

compat-break-remove.sr9
// BREAKING: removing a stable field without migration
// Error M0169: the stable variable 'oldField' cannot be implicitly discarded

persistent actor {
  var counter : Nat = 0;
  // Error: 'oldField' was in previous version but is now missing
  // This would cause data loss - requires migration function

  // To fix, either:
  // 1. Keep the field (even if unused)
  // 2. Add an explicit migration function

  public func get() : async Nat reads counter {
    counter
  };
}

Narrowing Types

Changing to a smaller type that cannot hold all old values causes error M0216:

compat-break-narrow.sr9
// BREAKING: narrowing types (Int to Nat)
// Error M0216: implicit data loss - Int values may not fit in Nat

persistent actor {
  // If old version had 'var amount : Int = -5'
  // Changing to Nat would lose negative values
  var amount : Nat = 0;  // Error: narrowing from Int loses data

  // To fix:
  // 1. Keep the type as Int
  // 2. Use a migration function to handle negative values

  public func get() : async Nat reads amount {
    amount
  };
}

Removing Variant Cases

Removing a variant case breaks existing data that uses that case, causing error M0170:

compat-break-variant_reject.sr9
// BREAKING: removing variant cases
// Error M0170: Missing tag '#cancelled' in new type

persistent actor {
  // If old version had { #pending; #done; #cancelled }
  // Removing #cancelled breaks existing data with that case
  var status : { #pending; #done } = #pending;  // Error: removed #cancelled

  // To fix:
  // 1. Keep all existing variant cases
  // 2. Use migration to convert #cancelled to another case

  public func complete() : async ()
    modifies status
    ensures status == #done
  {
    status := #done;
  };
}

Migration Functions

When you need to make a breaking change, use a migration function to explicitly transform the old state:

Migration snippets are typechecked as source examples. They are not sent through the Viper --verify lane, which currently does not lower top-level migration clauses.

Basic Migration

Combine or transform fields during upgrade:

compat-migration-basic.sr9
// Migration function: explicit transformation during upgrade
// Builds the new stable-field record from the previous stable-field record.

(with migration =
  func (previous : { var first : [Nat]; var second : [Nat] })
     : { var combined : [(Nat, Nat)] } =
    { var combined = [] }
)
persistent actor {
  var combined : [(Nat, Nat)] = [];

  public query func getAt(i : Nat) : async ?(Nat, Nat)
    reads combined
  {
    if (i < combined.size()) ?combined[i] else null
  };
}

Removing Fields with Migration

Explicitly discard obsolete fields:

compat-migration-remove.sr9
// Migration function: removing a field explicitly
// The migration function discards 'obsolete' field data

(with migration =
  func (previous : { var count : Nat; var obsolete : Text })
     : { var count : Nat } =
    // Keep count, discard obsolete
    { var count = previous.count }
)
persistent actor {
  var count : Nat = 0;

  invariant count >= 0;

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

Migration Function Requirements

A migration function must:

Be a non-generic function
Accept a record type (the old state)
Return a record type (the new state)
Use only stable types in both domain and codomain

Compatibility Matrix

Old Type	New Type	Compatible	Notes
`Nat`	`Int`	Yes	Widening
`Int`	`Nat`	No	Narrowing loses negatives
`{ a : T }`	`{ a : T; b : U }`	Yes	New field gets its initializer
`{ a : T; b : U }`	`{ a : T }`	No	Dropping field
`{ #a; #b }`	`{ #a; #b; #c }`	Yes	Adding case
`{ #a; #b; #c }`	`{ #a; #b }`	No	Removing case
`T`	`?T`	Yes	Making optional
`?T`	`T`	No	Requires value present
`[T]`	`[var T]`	Yes	Mutability can change
`Any`	`T`	No	Cannot narrow from Any
`T`	`Any`	No	Loses type info

Type Compatibility Rules

compat-rules.sr9
// Type compatibility rules demonstration
persistent actor {
  // SAFE changes (compatible upgrades):
  var count : Nat = 0;                    // Can widen to Int
  var items : [Nat] = [];                 // Can widen element type
  var status : { #on; #off } = #off;      // Can add new cases
  var config : { a : Nat } = { a = 0 };   // Can add optional fields
  var maybe : ?Nat = null;                // Optional is always safe to add

  // Type compatibility follows stable subtyping:
  // - Nat <: Int (every Nat is an Int)
  // - { #a; #b } <: { #a; #b; #c } (subset of cases)
  // - { a : T; b : U } <: { a : T } (has all required fields)

  // But these rules are STRICTER than regular subtyping:
  // - Cannot drop record fields (data loss)
  // - Cannot remove variant cases (data loss)
  // - Cannot promote to Any (type info loss)

  public query func getCount() : async Nat reads count {
    count
  };
}

The compatibility checker uses these rules:

Field matching: Old fields must exist in the new version
Type compatibility: Each field's old type must be a stable subtype of the new type
New fields: Are allowed and initialized from their declaration
No data loss: Cannot promote to Any or drop information

Error Messages

Code	Message	Cause	Fix
M0169	Stable variable cannot be discarded	Removing field without migration	Add migration function or keep field
M0170	Type not compatible	Old type is not subtype of new	Use compatible type or migration
M0216	Implicit data loss	Stable subtyping violation	Keep wider type or use migration
M0201	Non-stable type in migration	Migration uses async/function/module	Use only stable types
M0202	Non-object type in migration	Migration domain/codomain not record	Use record types
M0203	Migration not a function	Migration expression is not a function	Provide a function
M0204	Wrong field type	Migration produces wrong type	Fix the field type
M0205	Unexpected field	Migration produces undeclared field	Remove extra field

Mutability Changes

Stable fields can change mutability during upgrades because they are never aliased. Both of these changes are safe:

var [Nat] to [Nat] (mutable to immutable)
[Nat] to var [Nat] (immutable to mutable)

The underlying element types must still satisfy stable subtyping.

Verification Impact

Type compatibility is checked by the upgrade/stability path, not by ordinary method verification. However, verification helps ensure the code that runs after migration preserves the actor's contracts:

Actor invariants must hold after migration
Postconditions on initialization functions are checked
The old() expression in contracts refers to method entry, not pre-upgrade state

Summary

Upgrade compatibility uses stable subtyping, which is stricter than regular subtyping
Safe changes: add fields, widen types, add variant cases
Breaking changes: remove fields, narrow types, remove variant cases
Use migration functions for breaking changes
Migration functions must use stable types and be non-generic
Mutability of stable fields can change freely

Stable variables for stable type requirements
Orthogonal persistence for the runtime persistence model
Subtyping rules for ordinary type compatibility
Actor invariants for post-upgrade state properties

Stable Subtyping​

Safe Changes​

Adding New Fields​

Widening Types​

Adding Variant Cases​

Breaking Changes​

Removing Stable Fields​

Narrowing Types​

Removing Variant Cases​

Migration Functions​

Basic Migration​

Removing Fields with Migration​

Migration Function Requirements​

Compatibility Matrix​

Type Compatibility Rules​

Error Messages​

Mutability Changes​

Verification Impact​

Summary​

Related Topics​