Skip to main content

Element Type Restrictions

Spec collections (Map, Set, Seq, Multiset) only accept spec-immutable key, value, and element types in verification mode, except opaque/token handles by identity. This page explains what types are allowed, what types are rejected, and why.

What is Spec-Immutable?​

A type is spec-immutable if it contains no mutable state. The verifier checks this recursively: a record is spec-immutable only if all its fields are immutable and their types are also spec-immutable.

Spec-immutability is required because collections represent mathematical values. In mathematics, a set containing an element is well-defined. But if that element could mutate, the set's membership would become ambiguous. Restricting element types to immutable values preserves sound verification reasoning over trusted primitive collections. Opaque/token handles are admitted as sealed identities: collection equality and exact descriptor-backed snapshots prove the same handles are present, not that owner payload models are unchanged.

Allowed Types​

The following types can be used as collection elements, map keys, and map values:

Primitive Types​

All primitive types are spec-immutable:

ghost {
  let s1 : Set<Nat> = Set.singleton(42);
  let s2 : Set<Int> = Set.singleton(-10);
  let s3 : Set<Bool> = Set.singleton(true);
  let s4 : Set<Text> = Set.singleton("hello");
}

Primitives include: Nat, Int, Nat8-Nat64, Int8-Int64, Bool, Text, Char, Float.

Immutable Records​

Records without var fields are spec-immutable:

type Point = { x : Nat; y : Nat };  // No var fields

ghost {
  let s : Set<Point> = Set.singleton({ x = 0; y = 0 });
  assert Set.card(s) == 1;
}

The record must have all immutable fields, and the field types themselves must be spec-immutable.

Tuples​

Tuples are spec-immutable when all their elements are:

ghost {
  let m : Map<(Nat, Nat), Int> = Map.empty();
  let m2 = Map.update(m, (1, 2), 100);
  assert Map.get(m2, (1, 2)) == 100;
}

Options​

Options (?T) are spec-immutable when their inner type is:

ghost {
  let s : Set<?Nat> = Set.singleton(?5);
  assert Set.contains(?5, s);
}

Variants​

Variant types are spec-immutable when all constructor payloads are:

type Status = { #pending; #complete : Nat };

ghost {
  let s : Set<Status> = Set.singleton(#pending);
  let s2 = Set.union(s, Set.singleton(#complete(42)));
}

Nested Collections​

Spec collections themselves are immutable values, so they can be nested:

ghost {
  let m : Map<Nat, Set<Nat>> = Map.empty();
  let inner = Set.singleton(1);
  let m2 = Map.update(m, 0, inner);
}

Rejected Types​

The following types are rejected as collection elements in verification/Viper mode. Using them produces error M0242.

Mutable Records (var fields)​

Records with var fields are rejected:

set-immutable-reject_reject.sr9
// Set element types must be spec-immutable
persistent actor {
  type MutableCell = { var value : Int };  // Has var field

  public func check() : async () {
    ghost {
      // ERROR: Mutable record cannot be Set element
      let s : Set<MutableCell> = Set.empty();
    };
  };
}

Error message:

type error [M0242], Set element type must be immutable (field value is mutable; no var fields or mutable arrays)

The var value field makes MutableCell mutable, so it cannot be a Set element.

Mutable Arrays​

Both mutable arrays ([var T]) and immutable arrays ([T]) are rejected:

seq-immutable-reject_reject.sr9
// ERROR: Seq elements must be immutable
persistent actor {
  type MutArr = [var Int];

  public func demo() : async () {
    ghost {
      // This is rejected - mutable arrays cannot be Seq elements
      let s : Seq<MutArr> = Seq.empty();
      assert true;
    };
  };
}

Error message:

type error [M0242], Seq element type must be immutable (contains a mutable array; no var fields or mutable arrays)

Arrays are rejected because they have reference semantics: two variables can point to the same array, and modifications through one affect the other. This aliasing breaks the mathematical model.

Functions​

Function types cannot be collection elements:

// REJECTED
type Callback = (Nat) -> Int;
ghost {
  let s : Set<Callback> = Set.empty();  // Error M0242
}

Functions are not comparable or serializable in the verification model.

Actors and Modules​

Actor types are rejected:

// REJECTED
type A = actor {};
ghost {
  let m : Map<A, Int> = Map.empty();  // Error M0242
}

Actors have identity-based semantics that are incompatible with mathematical collections. Module values are proof/code structure rather than comparable mathematical data, so model the specific immutable facts you need instead of placing modules in spec collections.

Async Types​

Async types represent pending computations and are rejected:

// REJECTED
ghost {
  let s : Set<async Nat> = Set.empty();  // Error M0242
}

Nested Mutability​

The check is recursive. A record containing a mutable array is rejected even if the record itself has no var fields:

// REJECTED
type Container = { data : [var Int] };  // Contains mutable array
ghost {
  let s : Set<Container> = Set.empty();  // Error M0242
}

Similarly, a record containing another record with var fields is rejected:

// REJECTED
type Inner = { var x : Int };
type Outer = { inner : Inner };  // Contains mutable record
ghost {
  let s : Set<Outer> = Set.empty();  // Error M0242
}

Map Keys vs Values​

For Maps, both the key type and value type must be spec-immutable, except opaque/token handle values by identity:

map-immutable-reject_reject.sr9
// REJECT: Map keys and values must be immutable types
persistent actor {
  public func demo() : async () {
    ghost {
      // This is rejected: mutable record as Map value
      type MutableBox = { var x : Nat };
      let m : Map<Nat, MutableBox> = Map.empty();
    };
  };
}

This applies to keys:

type error [M0242], Map key type must be immutable (...; no var fields or mutable arrays)

And to values:

type error [M0242], Map value type must be immutable (...; no var fields or mutable arrays)

Why This Restriction?​

Spec collections are verification-only constructs that model mathematical collections. They require immutable elements for several reasons:

  1. Equality semantics: Mathematical sets and maps compare elements by value. Mutable elements would break this: if you add an element to a set and then mutate it, is it still in the set?

  2. Value semantics: Updates produce new collection values. Mutable elements could change across versions without any collection update, breaking reasoning about snapshots.

  3. Sound verification: The SMT solver reasons about collections using mathematical axioms. These axioms assume elements do not change. Mutable elements would make the axioms unsound.

  4. Serialization: Spec collections are modeled using backend theories (Viper sequences, sets, maps). These theories require elements to be pure values.

Quick Reference​

Type CategorySpec-ImmutableReason
Nat, Int, Bool, TextYesPrimitives are immutable
Nat8-Nat64, Int8-Int64YesPrimitives are immutable
Record without varYesAll fields immutable
Record with varNoContains mutable state
TupleYes (if elements are)Recursively checked
Option ?TYes (if T is)Recursively checked
VariantYes (if payloads are)Recursively checked
Array [T]NoReference semantics
Mutable array [var T]NoMutable reference
Function T -> UNoNot comparable
ActorNoIdentity semantics
Module valueNoProof/code structure, not comparable data
AsyncNoTemporal type
Nested collectionsYesCollections are values

Summary​

  • Spec collection elements must be spec-immutable: no mutable state, checked recursively, except opaque/token handles by identity
  • Allowed: primitives, immutable records, tuples, options, variants, nested collections, opaque/token handles by identity
  • Rejected: records with var fields, arrays (all), functions, actors, modules, async types
  • The restriction ensures sound mathematical reasoning about collection membership
  • Error code M0242 indicates a spec-immutability violation in verification/Viper mode