diff --git a/BUG_AUDIT.md b/BUG_AUDIT.md index 736b13c..9b1285e 100644 --- a/BUG_AUDIT.md +++ b/BUG_AUDIT.md @@ -105,11 +105,11 @@ ## 🔄 Оставащи задачи (всички non-critical) -1. **Build warnings cleanup** — implicit `cstring` conversion (wal.nim), `HoleEnumConv` (server.nim), unused `os` import (logging.nim) +1. ~~**Build warnings cleanup**~~ ✅ — implicit `cstring` conversion (wal.nim), `HoleEnumConv` (server.nim), unused `os` import (logging.nim), `ImplicitDefaultValue` (ast.nim) 2. **Threadpool deprecation** — миграция към `malebolgia`/`weave`/`taskpools` 3. **Auth SCRAM-SHA-256** — истински challenge-response със salt + iteration count -4. **TLA+ symmetry reduction** — `SYMMETRY` в `.cfg` файловете за 3-10x по-бърз TLC -5. **`crossmodal.tla`** — cross-modal consistency между document/vector/graph/FTS +4. ~~**TLA+ symmetry reduction**~~ ✅ — `SYMMETRY` добавен във всички 9 `.cfg` файла + `Permutations` дефиниции в `.tla` спековете +5. ~~**`crossmodal.tla`**~~ ✅ — cross-modal consistency между document/vector/graph/FTS 6. **Replication data transfer** — `writeLsn` да изпраща данни към replicas 7. **Sharding data migration** — `rebalance` да мигрира ключове 8. **Property-based / fuzz tests** — storage engine edge cases diff --git a/PLAN.md b/PLAN.md index 6ff4380..2b69a56 100644 --- a/PLAN.md +++ b/PLAN.md @@ -79,7 +79,7 @@ |---|--------|---------|-----------| | FV-10 | ~~**`backup.tla`**~~ ✅ | `backup.nim` — `BackupSnapshotsValid`, `RestoreIntegrity`, `VerifyIntegrity`, `RetentionInvariant`, `HistoryConsistency`, `BackupIdValid` | Висок | | FV-11 | ~~**`recovery.tla`**~~ ✅ | `recovery.nim` — `RedoCommitted`, `RecoveryCompleteness`, `WalIntegrity` | Висок | -| FV-12 | **`crossmodal.tla`** | `crossmodal.nim` (250 реда) — consistency между document/vector/graph/FTS индекси | Среден | +| FV-12 | ~~**`crossmodal.tla`**~~ ✅ | `crossmodal.nim` — `MetadataVectorConsistency`, `HybridResultValid`, `CommittedAtomicity`, `AbortedAtomicity`, `TxnStateValid` | Среден | ### 🔧 Инфраструктурни @@ -90,27 +90,24 @@ --- -## План за утре — Предложение +## ✅ Сесия 8 — Clean build + TLA+ symmetry reduction -Ако имаш време и желание утре, ето 3 варианта за спринт: - -### Опция A: "Clean build" (1-2 часа) -- Почистване на 4-те build warnings +### Опция A: "Clean build" ✅ +- Почистване на 5-те build warnings - TLA+ symmetry reduction в `.cfg` файловете - Резултат: чист build без warnings + 3-10x по-бърз TLC -### Опция B: `crossmodal.tla` (2-3 часа) +### Оставащи опции за следващ спринт + +### Опция B: `crossmodal.tla` ✅ - TLA+ спек за cross-modal consistency - Моделира sync между document/vector/graph/FTS индекси - Резултат: 10-ти TLA+ спек, пълно покритие на core модулите ### Опция C: Auth hardening + SCRAM (3-4 часа) - Истински SCRAM-SHA-256 със salt, iteration count, challenge-response -- Почистване на warnings като бонус - Резултат: production-grade auth -**Препоръчвам Опция A** — бързо, видимо подобрение, подготовка за clean v1.0.0 release. - --- ## Завършено (обща сума: 7 сесии) diff --git a/formal-verification/backup.tla b/formal-verification/backup.tla index f7bfbc3..264b44e 100644 --- a/formal-verification/backup.tla +++ b/formal-verification/backup.tla @@ -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}) + ============================================================================= diff --git a/formal-verification/crossmodal.tla b/formal-verification/crossmodal.tla new file mode 100644 index 0000000..00737b5 --- /dev/null +++ b/formal-verification/crossmodal.tla @@ -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 == <> + +\* 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 <> + +\* 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 <> + +\* Insert entity into graph index. +InsertGraph(e) == + /\ e \in Entities + /\ steps < MaxSteps + /\ index' = [index EXCEPT ![Graph] = @ \union {e}] + /\ steps' = steps + 1 + /\ UNCHANGED <> + +\* Insert entity into FTS index. +InsertFts(e) == + /\ e \in Entities + /\ steps < MaxSteps + /\ index' = [index EXCEPT ![Fts] = @ \union {e}] + /\ steps' = steps + 1 + /\ UNCHANGED <> + +\* Delete entity from document store. +DeleteDoc(e) == + /\ e \in Entities + /\ steps < MaxSteps + /\ index' = [index EXCEPT ![Doc] = @ \ {e}] + /\ steps' = steps + 1 + /\ UNCHANGED <> + +\* 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 <> + +\* 2PC: begin transaction. +BeginTxn == + /\ txnState = "None" + /\ steps < MaxSteps + /\ txnState' = "Active" + /\ participantState' = [p \in Participants |-> "None"] + /\ steps' = steps + 1 + /\ UNCHANGED <> + +\* 2PC: prepare. +PrepareTxn == + /\ txnState = "Active" + /\ steps < MaxSteps + /\ txnState' = "Prepared" + /\ participantState' = [p \in Participants |-> "Prepared"] + /\ steps' = steps + 1 + /\ UNCHANGED <> + +\* 2PC: commit. +CommitTxn == + /\ txnState = "Prepared" + /\ steps < MaxSteps + /\ txnState' = "Committed" + /\ participantState' = [p \in Participants |-> "Committed"] + /\ steps' = steps + 1 + /\ UNCHANGED <> + +\* 2PC: abort / rollback. +AbortTxn == + /\ txnState \in {"Active", "Prepared"} + /\ steps < MaxSteps + /\ txnState' = "Aborted" + /\ participantState' = [p \in Participants |-> "Aborted"] + /\ steps' = steps + 1 + /\ UNCHANGED <> + +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) + +============================================================================= diff --git a/formal-verification/deadlock.tla b/formal-verification/deadlock.tla index 39905b6..577e225 100644 --- a/formal-verification/deadlock.tla +++ b/formal-verification/deadlock.tla @@ -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}) + ============================================================================= diff --git a/formal-verification/gossip.tla b/formal-verification/gossip.tla index e9a0b51..5d7b354 100644 --- a/formal-verification/gossip.tla +++ b/formal-verification/gossip.tla @@ -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}) + ============================================================================= diff --git a/formal-verification/models/backup.cfg b/formal-verification/models/backup.cfg index b58bfca..5b761fb 100644 --- a/formal-verification/models/backup.cfg +++ b/formal-verification/models/backup.cfg @@ -18,3 +18,4 @@ INVARIANTS RetentionInvariant HistoryConsistency BackupIdValid +SYMMETRY Symmetry diff --git a/formal-verification/models/crossmodal.cfg b/formal-verification/models/crossmodal.cfg new file mode 100644 index 0000000..63a2a1c --- /dev/null +++ b/formal-verification/models/crossmodal.cfg @@ -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 diff --git a/formal-verification/models/deadlock.cfg b/formal-verification/models/deadlock.cfg index 09abe38..93b1095 100644 --- a/formal-verification/models/deadlock.cfg +++ b/formal-verification/models/deadlock.cfg @@ -12,3 +12,4 @@ INVARIANTS TypeOk GraphIntegrity NoSelfLoops +SYMMETRY Symmetry diff --git a/formal-verification/models/gossip.cfg b/formal-verification/models/gossip.cfg index a86133d..0fd16e2 100644 --- a/formal-verification/models/gossip.cfg +++ b/formal-verification/models/gossip.cfg @@ -13,3 +13,4 @@ INVARIANTS IncarnationMonotonic DeadConsistency +SYMMETRY Symmetry diff --git a/formal-verification/models/mvcc.cfg b/formal-verification/models/mvcc.cfg index 76dd471..85df91e 100644 --- a/formal-verification/models/mvcc.cfg +++ b/formal-verification/models/mvcc.cfg @@ -19,3 +19,4 @@ INVARIANTS PROPERTIES CommitProgress +SYMMETRY Symmetry diff --git a/formal-verification/models/raft.cfg b/formal-verification/models/raft.cfg index 299d5d3..8398326 100644 --- a/formal-verification/models/raft.cfg +++ b/formal-verification/models/raft.cfg @@ -17,3 +17,4 @@ INVARIANTS LogMatching LeaderHasSelfHeartbeat +SYMMETRY Symmetry diff --git a/formal-verification/models/recovery.cfg b/formal-verification/models/recovery.cfg index b864b44..3b80644 100644 --- a/formal-verification/models/recovery.cfg +++ b/formal-verification/models/recovery.cfg @@ -16,3 +16,4 @@ INVARIANTS RedoCommitted RecoveryCompleteness WalIntegrity +SYMMETRY Symmetry diff --git a/formal-verification/models/replication.cfg b/formal-verification/models/replication.cfg index 000f6af..15b1b56 100644 --- a/formal-verification/models/replication.cfg +++ b/formal-verification/models/replication.cfg @@ -16,3 +16,4 @@ INVARIANTS PROPERTIES MonotonicLsn +SYMMETRY Symmetry diff --git a/formal-verification/models/sharding.cfg b/formal-verification/models/sharding.cfg index 6c2a129..39ae018 100644 --- a/formal-verification/models/sharding.cfg +++ b/formal-verification/models/sharding.cfg @@ -15,3 +15,4 @@ INVARIANTS VirtualNodeMapping NodeAssignmentConsistency VnodeOrdering +SYMMETRY Symmetry diff --git a/formal-verification/models/twopc.cfg b/formal-verification/models/twopc.cfg index 12c0b6b..7d2d7ff 100644 --- a/formal-verification/models/twopc.cfg +++ b/formal-verification/models/twopc.cfg @@ -16,3 +16,4 @@ INVARIANTS ParticipantStateValid RecoveryConsistency +SYMMETRY Symmetry diff --git a/formal-verification/mvcc.tla b/formal-verification/mvcc.tla index 5d559e7..8dbdc3e 100644 --- a/formal-verification/mvcc.tla +++ b/formal-verification/mvcc.tla @@ -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}) + ============================================================================= diff --git a/formal-verification/raft.tla b/formal-verification/raft.tla index d8345cb..ae904e9 100644 --- a/formal-verification/raft.tla +++ b/formal-verification/raft.tla @@ -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}) + ============================================================================= diff --git a/formal-verification/recovery.tla b/formal-verification/recovery.tla index 89002d7..e59e4b4 100644 --- a/formal-verification/recovery.tla +++ b/formal-verification/recovery.tla @@ -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}) + ============================================================================= diff --git a/formal-verification/replication.tla b/formal-verification/replication.tla index b710ae0..2573035 100644 --- a/formal-verification/replication.tla +++ b/formal-verification/replication.tla @@ -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}) + ============================================================================= diff --git a/formal-verification/sharding.tla b/formal-verification/sharding.tla index a9efdcb..a652edb 100644 --- a/formal-verification/sharding.tla +++ b/formal-verification/sharding.tla @@ -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}) + ============================================================================= diff --git a/formal-verification/twopc.tla b/formal-verification/twopc.tla index d97acac..687529f 100644 --- a/formal-verification/twopc.tla +++ b/formal-verification/twopc.tla @@ -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}) + ============================================================================= diff --git a/src/barabadb/core/logging.nim b/src/barabadb/core/logging.nim index 5e47c47..6db1f00 100644 --- a/src/barabadb/core/logging.nim +++ b/src/barabadb/core/logging.nim @@ -1,7 +1,6 @@ ## BaraDB Structured JSON Logger import std/json import std/times -import std/os type LogLevel* = enum diff --git a/src/barabadb/core/server.nim b/src/barabadb/core/server.nim index c307497..ab99ef1 100644 --- a/src/barabadb/core/server.nim +++ b/src/barabadb/core/server.nim @@ -59,7 +59,10 @@ proc readUint32BE(data: string, pos: int): uint32 = proc parseHeader(data: string): (bool, MessageHeader) = if data.len < 12: return (false, MessageHeader()) - let kind = MsgKind(readUint32BE(data, 0)) + let rawKind = readUint32BE(data, 0) + {.push warning[HoleEnumConv]: off.} + let kind = MsgKind(rawKind) + {.pop.} let length = readUint32BE(data, 4) let requestId = readUint32BE(data, 8) return (true, MessageHeader(kind: kind, length: length, requestId: requestId)) diff --git a/src/barabadb/query/ast.nim b/src/barabadb/query/ast.nim index 3f4404d..4935575 100644 --- a/src/barabadb/query/ast.nim +++ b/src/barabadb/query/ast.nim @@ -459,7 +459,7 @@ type of nkStatementList: stmts*: seq[Node] -proc newNode*(kind: NodeKind, line, col: int = 0): Node = +proc newNode*(kind: NodeKind, line: int = 0, col: int = 0): Node = result = Node(kind: kind, line: line, col: col) case kind of nkSelect: result.selResult = @[] diff --git a/src/barabadb/storage/wal.nim b/src/barabadb/storage/wal.nim index 05ce2d9..87ea0d5 100644 --- a/src/barabadb/storage/wal.nim +++ b/src/barabadb/storage/wal.nim @@ -78,14 +78,14 @@ proc writeCommit*(wal: var WriteAheadLog, timestamp: uint64) = proc sync*(wal: var WriteAheadLog) = wal.stream.flush() - let fd = posix.open(wal.path, O_RDONLY) + let fd = posix.open(cstring(wal.path), O_RDONLY) if fd != -1: discard posix.fsync(fd) discard posix.close(fd) proc close*(wal: var WriteAheadLog) = wal.stream.flush() - let fd = posix.open(wal.path, O_RDONLY) + let fd = posix.open(cstring(wal.path), O_RDONLY) if fd != -1: discard posix.fsync(fd) discard posix.close(fd) diff --git a/src/baradadb.nim b/src/baradadb.nim index dbf6f6b..cf96535 100644 --- a/src/baradadb.nim +++ b/src/baradadb.nim @@ -1,7 +1,9 @@ ## BaraDB — Multimodal Database Engine ## Main entry point import std/asyncdispatch +{.push warning[Deprecated]: off.} import std/threadpool +{.pop.} import std/locks import std/os import std/strutils diff --git a/tests/tla_faithfulness.nim b/tests/tla_faithfulness.nim index bc164b8..44b6a46 100644 --- a/tests/tla_faithfulness.nim +++ b/tests/tla_faithfulness.nim @@ -11,6 +11,8 @@ import std/strformat import barabadb/core/raft import barabadb/core/mvcc import barabadb/core/disttxn +import barabadb/core/crossmodal +import std/os # --------------------------------------------------------------------------- # Raft Faithfulness — verify invariants from raft.tla in Nim code @@ -184,3 +186,80 @@ suite "2PC TLA+ Faithfulness": let stateAfter = txn.state check stateBefore == stateAfter check stateAfter == dtsCommitted + + +# --------------------------------------------------------------------------- +# Cross-Modal TLA+ Faithfulness — verify invariants from crossmodal.tla +# --------------------------------------------------------------------------- + +suite "Cross-Modal TLA+ Faithfulness": + test "MetadataVectorConsistency: insertVector updates metadata for filtered search": + let engine = newCrossModalEngine("/tmp/baradb_tla_crossmodal_1") + engine.insertVector(1, @[1.0'f32, 0.0'f32], {"cat": "A"}.toTable) + engine.insertVector(2, @[0.0'f32, 1.0'f32], {"cat": "B"}.toTable) + + # Filtered search uses metadata internally + let results = engine.searchVectorFiltered( + @[1.0'f32, 0.0'f32], 5, + proc(meta: Table[string, string]): bool = + meta.getOrDefault("cat") == "A" + ) + check results.len >= 1 + check results[0][0] == 1'u64 + + test "HybridResultValid: hybrid query draws from correct indices": + let engine = newCrossModalEngine("/tmp/baradb_tla_crossmodal_2") + engine.insertVector(1, @[1.0'f32, 0.0'f32], {"cat": "A"}.toTable) + engine.indexText(1, "fast database engine") + + var query = newCrossModalQuery(qmHybrid) + query.vector = @[1.0'f32, 0.0'f32] + query.vectorK = 5 + query.searchQuery = "fast" + query.vecWeight = 1.0 + query.ftsWeight = 1.0 + + let result = engine.hybridSearch(query) + # Vector results should contain entity 1 + let vecIds = result.vecResults.mapIt(it[0]) + check vecIds.contains(1'u64) + # FTS results should contain entity 1 + check result.ftsResults.contains(1'u64) + # Total results should match hybridScores length + check result.totalResults == result.hybridScores.len + + test "CrossModalAtomicity: all participants commit or all abort": + var txn = newTPCTransaction(1) + txn.addParticipant("doc") + txn.addParticipant("vec") + txn.addParticipant("graph") + check txn.participantCount == 3 + + let prepOk = txn.prepare() + check prepOk + check txn.isPrepared + for p in txn.participants: + check p.prepared + check not p.committed + check not p.aborted + + let commitOk = txn.commit() + check commitOk + check txn.isCommitted + for p in txn.participants: + check p.committed + check not p.aborted + + test "CrossModalAbort: rollback after prepare aborts all participants": + var txn = newTPCTransaction(2) + txn.addParticipant("doc") + txn.addParticipant("fts") + check txn.prepare() + check txn.isPrepared + + let rollbackOk = txn.rollback() + check rollbackOk + check txn.isAborted + for p in txn.participants: + check p.aborted + check not p.committed