Pure B+Tree Map

A persistent (immutable) B+tree map with structural sharing and a verification-friendly spec model.

Quick Start

import BMap "mo:core/pure/BMap";
import Types "mo:core/Types";

pure func compareNat(a : Nat, b : Nat) : Types.Order {
  if (a < b) { #less } else if (a > b) { #greater } else { #equal }
};

let m0 = BMap.empty<Nat, Text>();
let m1 = BMap.add<Nat, Text>(m0, compareNat, 1, "one");
let m2 = BMap.add<Nat, Text>(m1, compareNat, 2, "two");
let v = BMap.get<Nat, Text>(m2, compareNat, 1); // ?"one"
let it = BMap.entries<Nat, Text>(m2);

Example: Building and Querying a Map

map.sr9

import BMap "mo:core/pure/BMap";
import Types "mo:core/Types";

module {
  public func compareNat(a : Nat, b : Nat) : Types.Order
    requires true;
    ensures true;
  {
    if (a < b) { #less } else if (a > b) { #greater } else { #equal }
  };

  public func demo() : ?Text
    requires true;
    ensures true;
  {
    let m0 = BMap.empty<Nat, Text>();
    let m1 = BMap.add<Nat, Text>(m0, compareNat, 1, "one");
    let m2 = BMap.add<Nat, Text>(m1, compareNat, 2, "two");
    BMap.get<Nat, Text>(m2, compareNat, 1)
  };
}

Constants and Types

• btreeOrder, maxKeys, minKeys, maxChildren, minChildren: fixed tuning parameters for order 32.
• BMap<K,V>, Node<K,V>, Leaf<K,V>, Internal<K,V>: core tree types.
• SearchResult, InsertResult, DeleteResult, DeleteTopResult, GrowResult, SplitResult, BorrowResult, MergeResult: helper result variants.
• NodeCursor, IterState, IterDirection, Bound<K>: iterator and range machinery.
• Builder<K,V>: bulk build buffer.

Spec Module (BMap.Spec)

Spec-only helpers expose the mathematical model behind BMap<K, V>. Use them from contracts and ghost code when a proof needs key/value facts rather than only runtime lookup behavior. entries and reverseEntries expose exact key/value snapshot facts through the Spec.entrySnapshot lemmas. See pure/BMap for the full API with types and descriptions.

Mutable Wrapper (mo:core/mutable/MBMap)

A small mutable wrapper around the pure map (useful for performance baselines). See mutable/MBMap for the full API.

Internal Modules (Unstable)

These modules are public for tests and internal reuse. Treat them as unstable. See pure/BMapInternal and internal/BTreeHelper for the full APIs.

Complexity Summary

• Lookup: O(log_32 n)
• Insert: O(log_32 n) with path copying
• Delete: O(log_32 n) with rebalancing
• Iteration: O(n) time, O(log n) stack
• Range seek: O(log n) init, O(1) per element

Summary

• pure/BMap provides an immutable persistent-data-structure B+tree map with rich iteration and spec support.
• Use mutable/MBMap only when you need a mutable facade over the pure map; keep the pure map in contracts when you want persistent snapshots and simpler framing.
• BMapInternal and BTreeHelper are internal and not part of the stable API.