Add TLA+ verification suite for OLC ART concurrency

.gitignore

@@ -53,3 +53,8 @@ examples/compile_commands.json
 **/*#*
 
 /docs/
+# TLC model checker artifacts
+spec/tla/*_TTrace_*.bin
+spec/tla/*_TTrace_*.tla
+spec/tla/states/
+

spec/tla/ARTTreeMaintenance.cfg

@@ -0,0 +1,13 @@
+SPECIFICATION Spec
+
+CONSTANTS
+    PrefixCapacity = 2
+
+INVARIANTS
+    TypeOK
+    NoOrphans
+    KeyPreservation
+    WellFormed
+
+CONSTRAINT
+    StateConstraint

spec/tla/ARTTreeMaintenance_NoAncestorCollapse.cfg

@@ -0,0 +1,13 @@
+SPECIFICATION BuggySpec
+
+CONSTANTS
+    PrefixCapacity = 2
+
+INVARIANTS
+    TypeOK
+    NoOrphans
+    KeyPreservation
+    WellFormed
+
+CONSTRAINT
+    StateConstraint

spec/tla/Inode256VIS.cfg

@@ -0,0 +1,14 @@
+SPECIFICATION Spec
+
+CONSTANTS
+    N = 4
+    Values = {0, 1, 2}
+
+INVARIANTS
+    CorrectScanInvariant
+    BitmaskConsistency
+    IteratorSafety
+
+\* This invariant should be VIOLATED — demonstrates the bug with nullptr-only checks.
+\* Uncomment to see the counterexample:
+\* INVARIANT BuggyScanInvariant

spec/tla/Inode256VIS.tla

@@ -0,0 +1,112 @@
+--------------------------- MODULE Inode256VIS ---------------------------
+\* TLA+ specification for inode256 value-in-slot (VIS) correctness.
+\*
+\* Models a single inode256 with N slots. Each slot is either:
+\*   - Empty (no child, no value)
+\*   - Pointer (holds a child node reference)
+\*   - Value (holds a packed user value, bitmask bit set)
+\*
+\* Key invariant: every scan for "occupied" slots must find exactly
+\* the union of pointer-slots and value-slots. With bitmask-only
+\* encoding, pack(0) = 0 = NULL, so `slot[i] # 0` is INSUFFICIENT.
+\*
+\* Domain: N=4 slots, values in {0,1,2}, pointers in {-1,-2,-3,-4}.
+\* NULL = 0. Pointers are negative (always non-zero). Values are >= 0.
+
+EXTENDS Integers, FiniteSets
+
+CONSTANTS
+    N,          \* Number of slots (4 for model checking)
+    Values      \* Set of user values (e.g., {0, 1, 2})
+
+VARIABLES
+    slot,       \* slot[i] \in Int (0=NULL, <0=pointer, >=0=packed value)
+    bitmask,    \* bitmask[i] \in BOOLEAN (TRUE = value-in-slot)
+    hasPtr      \* hasPtr[i] \in BOOLEAN (TRUE = slot holds a pointer)
+
+NULL == 0
+Pointers == {-1, -2, -3, -4}
+Pack(v) == v    \* Identity encoding. pack(0) = 0 = NULL.
+Slots == 1..N
+vars == <<slot, bitmask, hasPtr>>
+
+-----------------------------------------------------------------------------
+\* PREDICATES
+
+\* Ground truth: a slot is occupied if it holds a pointer OR a value.
+Occupied(i) == hasPtr[i] \/ bitmask[i]
+
+OccupiedSet == {i \in Slots : Occupied(i)}
+
+\* BUGGY: nullptr check only. Misses value=0 slots.
+BuggyOccupied(i) == slot[i] # NULL
+
+BuggyOccupiedSet == {i \in Slots : BuggyOccupied(i)}
+
+\* CORRECT: nullptr OR bitmask.
+CorrectOccupied(i) == slot[i] # NULL \/ bitmask[i]
+
+CorrectOccupiedSet == {i \in Slots : CorrectOccupied(i)}
+
+-----------------------------------------------------------------------------
+\* INITIAL STATE
+
+Init ==
+    /\ slot = [i \in Slots |-> NULL]
+    /\ bitmask = [i \in Slots |-> FALSE]
+    /\ hasPtr = [i \in Slots |-> FALSE]
+
+-----------------------------------------------------------------------------
+\* OPERATIONS
+
+InsertValue(i, v) ==
+    /\ ~Occupied(i)
+    /\ slot' = [slot EXCEPT ![i] = Pack(v)]
+    /\ bitmask' = [bitmask EXCEPT ![i] = TRUE]
+    /\ hasPtr' = [hasPtr EXCEPT ![i] = FALSE]
+
+InsertPointer(i, p) ==
+    /\ ~Occupied(i)
+    /\ p \in Pointers
+    /\ slot' = [slot EXCEPT ![i] = p]
+    /\ bitmask' = [bitmask EXCEPT ![i] = FALSE]
+    /\ hasPtr' = [hasPtr EXCEPT ![i] = TRUE]
+
+Remove(i) ==
+    /\ Occupied(i)
+    /\ slot' = [slot EXCEPT ![i] = NULL]
+    /\ bitmask' = [bitmask EXCEPT ![i] = FALSE]
+    /\ hasPtr' = [hasPtr EXCEPT ![i] = FALSE]
+
+-----------------------------------------------------------------------------
+\* NEXT STATE
+
+Step ==
+    \/ \E i \in Slots, v \in Values : InsertValue(i, v)
+    \/ \E i \in Slots, p \in Pointers : InsertPointer(i, p)
+    \/ \E i \in Slots : Remove(i)
+
+Spec == Init /\ [][Step]_vars
+
+-----------------------------------------------------------------------------
+\* INVARIANTS
+
+\* The correct check (slot#NULL \/ bitmask) matches ground truth.
+CorrectScanInvariant == CorrectOccupiedSet = OccupiedSet
+
+\* The buggy check (slot#NULL only) should be VIOLATED by TLC.
+BuggyScanInvariant == BuggyOccupiedSet = OccupiedSet
+
+\* Structural consistency of the state.
+BitmaskConsistency ==
+    \A i \in Slots :
+        /\ (bitmask[i] => ~hasPtr[i])
+        /\ (hasPtr[i] => ~bitmask[i])
+        /\ (hasPtr[i] => slot[i] \in Pointers)
+        /\ (~Occupied(i) => slot[i] = NULL)
+
+\* Iterator safety: value slots are never pointers.
+IteratorSafety ==
+    \A i \in Slots : (bitmask[i] => ~hasPtr[i])
+
+=============================================================================

spec/tla/Inode256VIS_BugDemo.cfg

@@ -0,0 +1,11 @@
+\* This config demonstrates the VIS bug: BuggyScanInvariant will be VIOLATED.
+\* The counterexample shows: insert value 0 into a slot → pack(0) = NULL →
+\* buggy nullptr-only scan misses the slot.
+
+SPECIFICATION Spec
+
+CONSTANTS
+    N = 4
+    Values = {0, 1, 2}
+
+INVARIANT BuggyScanInvariant

spec/tla/OLCChainCut.cfg

@@ -0,0 +1,17 @@
+\* OLCChainCut model configuration
+
+SPECIFICATION Spec
+
+CONSTANTS
+    MaxVersion = 6
+
+CONSTRAINT
+    StateConstraint
+
+CHECK_DEADLOCK FALSE
+
+INVARIANTS
+    TypeOK
+    RemoverLockedImpliesChainSingle
+    ParentNotEmpty
+    GPConnected