Collection Snapshots

Collection snapshots are proof facts that connect a runtime enumeration to a spec collection model. They are value snapshots, not permission shortcuts.

For BSeq.XSeq<T>, toArray, toList, and freeze expose exact ordered snapshots of BSeq.Spec.model(seq). Use the core bridge lemmas when a proof needs explicit facts:

BSeq.arrayToSeq_toArray_len<Nat>(seq);
BSeq.arrayToSeq_toArray_get<Nat>(seq, i);
BSeq.model_from_toList<Nat>(seq);

For BMap and MBMap, full entries snapshots expose paired key/value sequences. The entry snapshot lemmas prove length, per-index key/value pairing, map-domain coverage, and duplicate-free keys. MBMap entry snapshots cite an explicit call-time Map<K,V> model, so the facts do not describe the live mutable map after a later mutation.

Opaque and token handles are identity values in these snapshots. A snapshot can prove that a handle was enumerated, but it does not prove that the owner's payload model stayed unchanged. Use owner-module observers while holding the required owner authority when the proof needs payload facts.

Unsupported collection metadata fails closed. Direct BMap.toArray over handle values and broad payload aggregation over arbitrary handle collections remain unsupported until a route provides explicit snapshot facts and owner authority.