feat: clean build + crossmodal.tla + TLA+ symmetry (v1.0.0-prep)

Build warnings cleanup (0 warnings): - Suppress threadpool deprecation warning (baradadb.nim) - Remove unused 'os' import (logging.nim) - Fix ImplicitDefaultValue for newNode params (ast.nim) - Add explicit cstring cast for posix.open (wal.nim) - Fix HoleEnumConv for MsgKind parsing (server.nim) TLA+ Formal Verification: - Add symmetry reduction (Permutations) to all 9 existing specs - Add SYMMETRY directive to all .cfg files - New crossmodal.tla: cross-modal consistency spec * MetadataVectorConsistency, HybridResultValid * CommittedAtomicity, AbortedAtomicity, TxnStateValid - New models/crossmodal.cfg Tests: - Add Cross-Modal TLA+ Faithfulness tests (4 tests) Docs: - Update PLAN.md and BUG_AUDIT.md with completed tasks
2026-05-13 09:24:04 +03:00
parent d08de7a062
commit 422df08ab9
28 changed files with 354 additions and 18 deletions
@@ -177,4 +177,7 @@ VerifyProgress ==
 \* Specification with weak fairness.
 Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

+\* Symmetry reduction for model checking.
+Symmetry == Permutations({f1, f2}) \cup Permutations({c1, c2})
+
 =============================================================================
@@ -0,0 +1,197 @@
+-------------------------------- MODULE crossmodal --------------------------------
+(*
+  TLA+ specification of Cross-Modal consistency in BaraDB.
+  Models: document store, vector index, graph index, FTS index,
+          metadata consistency, hybrid queries, and 2PC transactions.
+
+  Key properties verified:
+    - MetadataVectorConsistency: metadata always matches vector index.
+    - HybridResultValid: hybrid query results are drawn from queried indices.
+    - CommittedAtomicity: if txn committed, all participants committed.
+    - AbortedAtomicity: if txn aborted, all participants aborted.
+    - TxnStateValid: 2PC participant states align with coordinator state.
+*)
+
+EXTENDS Integers, Sequences, FiniteSets, TLC
+
+CONSTANTS Entities,       \* set of entity IDs
+          Participants,   \* set of 2PC participant IDs
+          MaxSteps,       \* bound total actions for model checking
+          Nil,            \* distinguished nil value (model value)
+          Doc, Vec, Graph, Fts  \* model values for query modes
+
+ASSUME IsFiniteSet(Entities) /\ IsFiniteSet(Participants)
+ASSUME MaxSteps >= 1
+ASSUME {Doc, Vec, Graph, Fts} \cap (Entities \cup Participants \cup {Nil}) = {}
+
+Modes == {Doc, Vec, Graph, Fts}
+
+VARIABLES
+  index,          \* index[m] \in SUBSET Entities for each m \in Modes
+  metadata,       \* metadata \subseteq Entities — linked to vector index
+  txnState,       \* txnState \in {"None","Active","Prepared","Committed","Aborted"}
+  participantState, \* participantState[p] for each p \in Participants
+  lastQueryModes, \* lastQueryModes \subseteq Modes
+  lastQueryResult,\* lastQueryResult \subseteq Entities
+  steps           \* steps \in 0..MaxSteps — action counter bound
+
+vars == <<index, metadata, txnState, participantState,
+          lastQueryModes, lastQueryResult, steps>>
+
+\* Union of indices for a set of modes
+IndexUnion(modes) == UNION {index[m] : m \in modes}
+
+-----------------------------------------------------------------------------
+\* Initial state
+
+Init ==
+  /\ index = [m \in Modes |-> {}]
+  /\ metadata = {}
+  /\ txnState = "None"
+  /\ participantState = [p \in Participants |-> "None"]
+  /\ lastQueryModes = {}
+  /\ lastQueryResult = {}
+  /\ steps = 0
+
+-----------------------------------------------------------------------------
+\* State transitions
+
+\* Insert entity into document store.
+InsertDoc(e) ==
+  /\ e \in Entities
+  /\ steps < MaxSteps
+  /\ index' = [index EXCEPT ![Doc] = @ \union {e}]
+  /\ steps' = steps + 1
+  /\ UNCHANGED <<metadata, txnState, participantState, lastQueryModes, lastQueryResult>>
+
+\* Insert entity into vector index (also updates metadata).
+InsertVec(e) ==
+  /\ e \in Entities
+  /\ steps < MaxSteps
+  /\ index' = [index EXCEPT ![Vec] = @ \union {e}]
+  /\ metadata' = metadata \union {e}
+  /\ steps' = steps + 1
+  /\ UNCHANGED <<txnState, participantState, lastQueryModes, lastQueryResult>>
+
+\* Insert entity into graph index.
+InsertGraph(e) ==
+  /\ e \in Entities
+  /\ steps < MaxSteps
+  /\ index' = [index EXCEPT ![Graph] = @ \union {e}]
+  /\ steps' = steps + 1
+  /\ UNCHANGED <<metadata, txnState, participantState, lastQueryModes, lastQueryResult>>
+
+\* Insert entity into FTS index.
+InsertFts(e) ==
+  /\ e \in Entities
+  /\ steps < MaxSteps
+  /\ index' = [index EXCEPT ![Fts] = @ \union {e}]
+  /\ steps' = steps + 1
+  /\ UNCHANGED <<metadata, txnState, participantState, lastQueryModes, lastQueryResult>>
+
+\* Delete entity from document store.
+DeleteDoc(e) ==
+  /\ e \in Entities
+  /\ steps < MaxSteps
+  /\ index' = [index EXCEPT ![Doc] = @ \ {e}]
+  /\ steps' = steps + 1
+  /\ UNCHANGED <<metadata, txnState, participantState, lastQueryModes, lastQueryResult>>
+
+\* Hybrid query over a non-empty set of modes.
+HybridQuery(qmodes) ==
+  /\ qmodes \subseteq Modes
+  /\ qmodes /= {}
+  /\ steps < MaxSteps
+  /\ lastQueryModes' = qmodes
+  /\ lastQueryResult' = IndexUnion(qmodes)
+  /\ steps' = steps + 1
+  /\ UNCHANGED <<index, metadata, txnState, participantState>>
+
+\* 2PC: begin transaction.
+BeginTxn ==
+  /\ txnState = "None"
+  /\ steps < MaxSteps
+  /\ txnState' = "Active"
+  /\ participantState' = [p \in Participants |-> "None"]
+  /\ steps' = steps + 1
+  /\ UNCHANGED <<index, metadata, lastQueryModes, lastQueryResult>>
+
+\* 2PC: prepare.
+PrepareTxn ==
+  /\ txnState = "Active"
+  /\ steps < MaxSteps
+  /\ txnState' = "Prepared"
+  /\ participantState' = [p \in Participants |-> "Prepared"]
+  /\ steps' = steps + 1
+  /\ UNCHANGED <<index, metadata, lastQueryModes, lastQueryResult>>
+
+\* 2PC: commit.
+CommitTxn ==
+  /\ txnState = "Prepared"
+  /\ steps < MaxSteps
+  /\ txnState' = "Committed"
+  /\ participantState' = [p \in Participants |-> "Committed"]
+  /\ steps' = steps + 1
+  /\ UNCHANGED <<index, metadata, lastQueryModes, lastQueryResult>>
+
+\* 2PC: abort / rollback.
+AbortTxn ==
+  /\ txnState \in {"Active", "Prepared"}
+  /\ steps < MaxSteps
+  /\ txnState' = "Aborted"
+  /\ participantState' = [p \in Participants |-> "Aborted"]
+  /\ steps' = steps + 1
+  /\ UNCHANGED <<index, metadata, lastQueryModes, lastQueryResult>>
+
+Next ==
+  \/ \E e \in Entities : InsertDoc(e)
+  \/ \E e \in Entities : InsertVec(e)
+  \/ \E e \in Entities : InsertGraph(e)
+  \/ \E e \in Entities : InsertFts(e)
+  \/ \E e \in Entities : DeleteDoc(e)
+  \/ \E qmodes \in (SUBSET Modes \ {{}}) : HybridQuery(qmodes)
+  \/ BeginTxn
+  \/ PrepareTxn
+  \/ CommitTxn
+  \/ AbortTxn
+
+Spec == Init /\ [][Next]_vars /\ WF_vars(Next)
+
+-----------------------------------------------------------------------------
+\* Invariants
+
+TypeOk ==
+  /\ \A m \in Modes : index[m] \subseteq Entities
+  /\ metadata \subseteq Entities
+  /\ txnState \in {"None", "Active", "Prepared", "Committed", "Aborted"}
+  /\ \A p \in Participants : participantState[p] \in {"None", "Prepared", "Committed", "Aborted"}
+  /\ lastQueryModes \subseteq Modes
+  /\ lastQueryResult \subseteq Entities
+  /\ steps \in 0..MaxSteps
+
+\* Metadata is always consistent with vector index.
+MetadataVectorConsistency ==
+  metadata = index[Vec]
+
+\* Hybrid query results are valid (drawn from queried indices).
+HybridResultValid ==
+  lastQueryResult \subseteq IndexUnion(lastQueryModes)
+
+\* If transaction is committed, all participants are committed.
+CommittedAtomicity ==
+  txnState = "Committed" => \A p \in Participants : participantState[p] = "Committed"
+
+\* If transaction is aborted, all participants are aborted.
+AbortedAtomicity ==
+  txnState = "Aborted" => \A p \in Participants : participantState[p] = "Aborted"
+
+\* 2PC state machine alignment.
+TxnStateValid ==
+  /\ (txnState = "None" => \A p \in Participants : participantState[p] = "None")
+  /\ (txnState = "Active" => \A p \in Participants : participantState[p] \in {"None", "Prepared"})
+  /\ (txnState = "Prepared" => \A p \in Participants : participantState[p] = "Prepared")
+
+\* Symmetry reduction for model checking.
+Symmetry == Permutations(Entities) \cup Permutations(Participants)
+
+=============================================================================
@@ -62,4 +62,7 @@ TypeOk ==
  /\ edges \subseteq (TxnIds \X TxnIds)
  /\ Cardinality(edges) <= MaxEdges

+\* Symmetry reduction for model checking.
+Symmetry == Permutations({t1, t2, t3, t4, t5})
+
 =============================================================================
@@ -141,4 +141,7 @@ DeadDetectedEventually ==
 \* Specification with weak fairness.
 Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

+\* Symmetry reduction for model checking.
+Symmetry == Permutations({n1, n2, n3})
+
 =============================================================================
@@ -18,3 +18,4 @@ INVARIANTS
  RetentionInvariant
  HistoryConsistency
  BackupIdValid
+SYMMETRY Symmetry
@@ -0,0 +1,23 @@
+CONSTANTS
+  Entities = {e1, e2}
+  Participants = {p1, p2}
+  Doc = Doc
+  Vec = Vec
+  Graph = Graph
+  Fts = Fts
+  MaxSteps = 6
+  Nil = Nil
+
+SPECIFICATION Spec
+
+CHECK_DEADLOCK FALSE
+
+INVARIANTS
+  TypeOk
+  MetadataVectorConsistency
+  HybridResultValid
+  CommittedAtomicity
+  AbortedAtomicity
+  TxnStateValid
+
+SYMMETRY Symmetry
@@ -12,3 +12,4 @@ INVARIANTS
  TypeOk
  GraphIntegrity
  NoSelfLoops
+SYMMETRY Symmetry
@@ -13,3 +13,4 @@ INVARIANTS
  IncarnationMonotonic
  DeadConsistency

+SYMMETRY Symmetry
@@ -19,3 +19,4 @@ INVARIANTS

 PROPERTIES
  CommitProgress
+SYMMETRY Symmetry
@@ -17,3 +17,4 @@ INVARIANTS
  LogMatching
  LeaderHasSelfHeartbeat

+SYMMETRY Symmetry
@@ -16,3 +16,4 @@ INVARIANTS
  RedoCommitted
  RecoveryCompleteness
  WalIntegrity
+SYMMETRY Symmetry
@@ -16,3 +16,4 @@ INVARIANTS

 PROPERTIES
  MonotonicLsn
+SYMMETRY Symmetry
@@ -15,3 +15,4 @@ INVARIANTS
  VirtualNodeMapping
  NodeAssignmentConsistency
  VnodeOrdering
+SYMMETRY Symmetry
@@ -16,3 +16,4 @@ INVARIANTS
  ParticipantStateValid
  RecoveryConsistency

+SYMMETRY Symmetry
@@ -186,4 +186,7 @@ CommitProgress ==
 \* Specification with weak fairness.
 Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

+\* Symmetry reduction for model checking.
+Symmetry == Permutations({k1, k2}) \cup Permutations({v1, v2})
+
 =============================================================================
@@ -302,4 +302,7 @@ LeaderProgress ==
 \* Specification with weak fairness (all actions get a fair chance).
 Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

+\* Symmetry reduction for model checking.
+Symmetry == Permutations({n1, n2, n3})
+
 =============================================================================
@@ -269,4 +269,7 @@ RecoveryProgress ==
 \* Specification with weak fairness.
 Spec == Init /\ [][Next]_vars /\ WF_vars(Next)

+\* Symmetry reduction for model checking.
+Symmetry == Permutations({k1, k2}) \cup Permutations({v1, v2})
+
 =============================================================================
@@ -157,4 +157,7 @@ TypeOk ==
  /\ appliedLsn \in 0..MaxLsn
  /\ ackedBy \in [0..MaxLsn -> SUBSET Replicas]

+\* Symmetry reduction for model checking.
+Symmetry == Permutations({r1, r2, r3})
+
 =============================================================================
@@ -119,4 +119,7 @@ TypeOk ==
  /\ shardToNodes \in [Shards -> SUBSET Nodes]
  /\ nextPosition \in 1..(MaxVnode + 1)

+\* Symmetry reduction for model checking.
+Symmetry == Permutations({s1, s2, s3}) \cup Permutations({n1, n2})
+
 =============================================================================
@@ -238,4 +238,7 @@ DecideAbortAction == \E t \in 1..MaxTxnId : DecideAbort(t)
 Spec == Init /\ [][Next]_vars /\ WF_vars(Next)
           /\ SF_vars(DecideCommitAction) /\ SF_vars(DecideAbortAction)

+\* Symmetry reduction for model checking.
+Symmetry == Permutations({p1, p2, p3})
+
 =============================================================================