Collections and Iteration

Common collection abstractions and iteration helpers.

Iter (mo:core/Iter)

Iterator record type and constructors. See Iter for the full API and spec helpers.

Example: Iter and BSeq

iter-xseq.sr9

import Iter "mo:core/Iter";
import BSeq "mo:core/pure/BSeq";

module {
  public func singletonIter<T>(x : T) : Iter.Iter<T>
    requires true;
    ensures true;
  {
    let it = Iter.singleton<T>(x);
    Iter.reverse<T>(Iter.reverse<T>(it))
  };

  public func pairSeq<T>(x : T, y : T) : BSeq.XSeq<T>
    requires true;
    ensures true;
  {
    let s1 = BSeq.singleton<T>(x);
    let s2 = BSeq.singleton<T>(y);
    BSeq.concat<T>(s1, s2)
  };
}

Stack (mo:core/Stack)

A persistent-data-structure stack built on BSeq.XSeq with a spec model. Here "persistent" means immutable structural sharing, not actor upgrade persistence. See Stack for the full API and spec helpers.

VarArray (mo:core/VarArray)

Helpers for mutable arrays. These are trusted constructors and transformations; verified callers still need ordinary array bounds and footprint facts when reading or mutating arrays. See VarArray for the full API.

BSeq (mo:core/pure/BSeq)

A persistent-data-structure sequence with tree-based representation and rich spec model. BSeq.Spec.model connects the runtime-friendly BSeq.XSeq<T> representation to the verifier's mathematical Seq<T>, and lemmas such as model_len, model_get, and model_update expose that relationship to proofs. See BSeq for the full API and spec helpers.

BSeq, BMap, and MBMap may store opaque/token handles as values. Their models expose handle identity and collection structure, not snapshots of the owner module's hidden payload. Use owner APIs to reason about or mutate the payload behind a handle. Exact BMap.entries / MBMap.entries snapshots and BSeq.toArray / BSeq.toList / BSeq.freeze snapshots preserve that same identity-only meaning for handle elements; see Collection Snapshots.

Summary

• Iter provides a minimal iterator abstraction with spec predicates.
• Stack and BSeq are immutable persistent data structures with spec models for proofs.
• BMap, MBMap, and BSeq can carry opaque/token handles by identity.
• BMap.entries, MBMap.entries, and BSeq conversions expose exact proof snapshots when their contracts provide the descriptor-backed bridge.
• VarArray offers simple constructors for mutable arrays.