Quint formal model verifying MVCC snapshot safety for btcd treap node recycling (PR follow-up to #2425)

treap_mvcc.qnt

// treap_mvcc.qnt -- Formal model of the immutable treap MVCC snapshot
// system with sync.Pool node recycling.
//
// This model verifies that recycling intermediate treap nodes during batched
// Put() and Delete() operations does not corrupt MVCC snapshots.
//
// Key invariants verified:
//   1. snapshotSafety: No node reachable from any snapshot is ever recycled.
//   2. currentTreapIntegrity: No recycled node is in the current treap.
//   3. noUseAfterRecycle: Combined -- no recycled node is live anywhere.
//
// To verify:
//   quint run treap_mvcc.qnt --invariant noUseAfterRecycle --max-steps=20
//   quint verify treap_mvcc.qnt --invariant noUseAfterRecycle

module treap_mvcc {

  // The set of node IDs currently in the "live" treap.
  var currentNodes: Set[int]

  // Set of snapshot node-ID sets (each snapshot captures a treap version).
  var snapshots: Set[Set[int]]

  // The pool of recycled node IDs available for reuse.
  var pool: Set[int]

  // Set of all node IDs ever recycled.
  var recycledNodes: Set[int]

  // Counter for generating fresh node IDs.
  var nextId: int

  // ---------------------------------------------------------------
  // Helper: all node IDs across all snapshots.
  // ---------------------------------------------------------------
  pure def allSnapshotNodes(snaps: Set[Set[int]]): Set[int] = {
    snaps.fold(Set(), (acc, s) => acc.union(s))
  }

  // ---------------------------------------------------------------
  // INVARIANTS
  // ---------------------------------------------------------------

  // INV-1: No recycled node is reachable from any snapshot.
  val snapshotSafety: bool = {
    allSnapshotNodes(snapshots).intersect(recycledNodes) == Set()
  }

  // INV-2: No recycled node is in the current treap.
  val currentTreapIntegrity: bool = {
    currentNodes.intersect(recycledNodes) == Set()
  }

  // INV-3: No recycled node is live anywhere.
  val noUseAfterRecycle: bool = {
    val allLive = currentNodes.union(allSnapshotNodes(snapshots))
    allLive.intersect(recycledNodes) == Set()
  }

  // ---------------------------------------------------------------
  // ACTIONS
  // ---------------------------------------------------------------

  action init = all {
    currentNodes' = Set(),
    snapshots' = Set(),
    pool' = Set(),
    recycledNodes' = Set(),
    nextId' = 1,
  }

  // Model a single put(): clones a subset of current nodes (the
  // root-to-leaf path), producing fresh IDs, and adds a new leaf.
  // The cloned "path" nodes are removed from the current treap and
  // replaced by fresh clones.  The originals remain in snapshots.
  action doPut: bool = {
    nondet pathNodes = currentNodes.powerset().oneOf()
    val numClones = pathNodes.size()
    val numNew = numClones + 1
    val newIds = nextId.to(nextId + numNew - 1)
    val newCurrent = currentNodes.exclude(pathNodes).union(newIds)

    all {
      currentNodes' = newCurrent,
      nextId' = nextId + numNew,
      pool' = pool,
      recycledNodes' = recycledNodes,
      snapshots' = snapshots,
    }
  }

  // Take a snapshot of the current treap.
  action takeSnapshot: bool = all {
    snapshots' = snapshots.union(Set(currentNodes)),
    pool' = pool,
    nextId' = nextId,
    currentNodes' = currentNodes,
    recycledNodes' = recycledNodes,
  }

  // Release a snapshot.
  action releaseSnapshot: bool = {
    nondet snap = snapshots.oneOf()
    all {
      snapshots' = snapshots.exclude(Set(snap)),
      pool' = pool,
      nextId' = nextId,
      currentNodes' = currentNodes,
      recycledNodes' = recycledNodes,
    }
  }

  // Model a batch Put with 2 sequential put() calls and recycling.
  // This is the core model of the safety-critical recycling logic.
  //
  // The key safety argument:
  //   - put() #1 creates fresh node IDs (>= nextId). These are NOT in
  //     any snapshot (snapshots only contain IDs < nextId).
  //   - put() #2 takes treap1 (containing IDs from put #1) and clones
  //     a subset of it (pathNodes2 = the "replaced sources").
  //   - Recycling: prevCreated1 intersect pathNodes2 are nodes from
  //     put #1 that were re-cloned by put #2. They are:
  //       (a) Not in any snapshot (fresh IDs from put #1).
  //       (b) Not in treap2 (replaced by new clones from put #2).
  //     Therefore safe to recycle.
  action doBatchPut: bool = {
    // -- Put #1 --
    nondet pathNodes1 = currentNodes.powerset().oneOf()
    val numNew1 = pathNodes1.size() + 1
    val newIds1 = nextId.to(nextId + numNew1 - 1)
    val treap1 = currentNodes.exclude(pathNodes1).union(newIds1)
    val prevCreated1 = newIds1

    // -- Put #2 on treap1 --
    nondet pathNodes2 = treap1.powerset().oneOf()
    val numNew2 = pathNodes2.size() + 1
    val newIds2 = (nextId + numNew1).to(nextId + numNew1 + numNew2 - 1)
    val treap2 = treap1.exclude(pathNodes2).union(newIds2)

    // -- Recycling between put #1 and put #2 --
    // prevCreated1 nodes that were in pathNodes2 (re-cloned) are dead.
    val deadNodes = prevCreated1.intersect(pathNodes2)

    // SAFETY PROOF:
    // deadNodes subset of prevCreated1 subset of newIds1.
    // newIds1 are IDs >= nextId, allocated fresh by put #1.
    // All snapshot IDs are < nextId (captured before put #1).
    // Therefore deadNodes intersect allSnapshotNodes == empty.
    // deadNodes are excluded from treap2 (replaced by newIds2).
    // Therefore deadNodes intersect treap2 == empty.
    // QED: deadNodes are not live anywhere.

    all {
      currentNodes' = treap2,
      nextId' = nextId + numNew1 + numNew2,
      pool' = pool.union(deadNodes),
      recycledNodes' = recycledNodes.union(deadNodes),
      snapshots' = snapshots,
    }
  }

  // Model a batch Delete with 2 sequential delete() calls.
  // Same recycling pattern as batch Put.
  action doBatchDelete: bool = {
    // -- Delete #1: clone path + remove target --
    nondet pathNodes1 = currentNodes.powerset().oneOf()
    nondet removeNode1 = currentNodes.powerset()
                           .filter(s => s.size() <= 1).oneOf()
    val numClones1 = pathNodes1.size()
    val cloneIds1 = nextId.to(nextId + numClones1 - 1)
    val treap1 = currentNodes.exclude(pathNodes1).exclude(removeNode1)
                   .union(cloneIds1)
    val prevCreated1 = cloneIds1

    // -- Delete #2 on treap1 --
    nondet pathNodes2 = treap1.powerset().oneOf()
    nondet removeNode2 = treap1.powerset()
                           .filter(s => s.size() <= 1).oneOf()
    val numClones2 = pathNodes2.size()
    val start2 = nextId + numClones1
    val end2 = nextId + numClones1 + numClones2 - 1
    val cloneIds2 = start2.to(end2)
    val treap2 = treap1.exclude(pathNodes2).exclude(removeNode2)
                   .union(cloneIds2)

    // -- Recycling --
    val deadNodes = prevCreated1.intersect(pathNodes2)

    all {
      currentNodes' = treap2,
      nextId' = nextId + numClones1 + numClones2,
      pool' = pool.union(deadNodes),
      recycledNodes' = recycledNodes.union(deadNodes),
      snapshots' = snapshots,
    }
  }

  // Non-deterministically choose an action.
  action step = any {
    doPut,
    doBatchPut,
    doBatchDelete,
    takeSnapshot,
    all { snapshots.size() > 0, releaseSnapshot },
  }
}

treap_mvcc_model.md

Quint Formal Model: Immutable Treap MVCC Snapshot Safety

Background

This model was developed as part of a follow-up to btcd PR #2425, which introduced sync.Pool-based node recycling in the immutable treap during batched Put() operations. The immutable treap serves as btcd's UTXO cache layer, providing O(1) MVCC snapshots by structural sharing of nodes across treap versions.

The central concern is: can recycling intermediate cloned nodes corrupt MVCC snapshots held by concurrent readers?

What the Model Captures

The model abstracts the treap as a set of node IDs (representing pointer identity) and tracks:

• currentNodes: The set of node IDs in the current live treap.
• snapshots: A set of node-ID sets, each representing a snapshot captured before some mutation.
• recycledNodes: The set of all node IDs that have been recycled (zeroed and returned to the pool).
• nextId: A monotonically increasing counter for fresh allocations.

Actions

Action	Models
doPut	A single put() call: clones a non-deterministic subset of current nodes (the root-to-leaf path), producing fresh IDs.
doBatchPut	Two sequential put() calls with inter-step recycling. The recycling rule: a node from put #1's "created" set is recycled iff it appears in put #2's "replaced sources" set.
doBatchDelete	Two sequential delete() calls with the same recycling pattern.
takeSnapshot	Captures currentNodes into the snapshot set (models dbCacheSnapshot).
releaseSnapshot	Removes a snapshot (models dbCacheSnapshot.Release()).

The Safety Argument (Encoded in doBatchPut)

The model includes an inline proof sketch:

1. deadNodes ⊆ prevCreated1 ⊆ newIds1
2. newIds1 are IDs ≥ nextId, allocated fresh by put #1.
3. All snapshot IDs are < nextId (captured before put #1).
4. Therefore deadNodes ∩ allSnapshotNodes == ∅.
5. deadNodes are excluded from treap2 (replaced by newIds2).
6. Therefore deadNodes ∩ treap2 == ∅.
7. QED: deadNodes are not live anywhere.

Invariants Verified

Invariant	Description
snapshotSafety	No recycled node is reachable from any snapshot.
currentTreapIntegrity	No recycled node is in the current treap.
noUseAfterRecycle	Combined: no recycled node is live anywhere.

Results

All three invariants passed across 30,000 randomized traces (10,000 per invariant, 15 steps each) using quint run:

$ quint run treap_mvcc.qnt --invariant noUseAfterRecycle --max-steps=15 --max-samples=10000
[ok] No violation found (37544ms at 266 traces/second).

$ quint run treap_mvcc.qnt --invariant snapshotSafety --max-steps=15 --max-samples=10000
[ok] No violation found (5445ms at 1837 traces/second).

$ quint run treap_mvcc.qnt --invariant currentTreapIntegrity --max-steps=15 --max-samples=10000
[ok] No violation found (4591ms at 2178 traces/second).

How This Helped

The model confirmed that the pointer-set recycling approach (tracking "created" and "replaced" node arrays) is fundamentally sound. The key insight it validates is that fresh clone IDs are always >= nextId at allocation time, so they can never appear in any pre-existing snapshot. This allowed us to replace the original get()-based liveness check (which traversed the treap per node) with a simple pointer-set membership test, reducing the recycling check from O(depth × log n) to O(depth²).

Running the Model

Install Quint and run:

npm install -g @informalsystems/quint
quint run treap_mvcc.qnt --invariant noUseAfterRecycle --max-steps=20