Baradb/formal-verification/IMPROVEMENT_PLAN.md

План за подобрения на формалната верификация на BaraDB

Към: formal-verification/IMPROVEMENT_PLAN.md
Дата: 2026-05-07
Автор: Kilo (formal-verification v1.0.0)
Статус: За изпълнение

---

Общ преглед на слабите места

Текущата верификация (7 TLA+ спека, 26 инварианти, 11.6M проверени състояния) покрива 4 от 15-те Nim модула в core/. Анализът идентифицира 8 категории слаби места, всяко с конкретни последствия за коректността на системата.

---

Приоритет 1 — Критични (влияят на вече проверените спекове)

1.1. Raft: липсва prevLogIndex/prevLogTerm проверка в Replicate

Проблем: Имплементацията (raft.nim:190-197) извършва prevLogIndex/prevLogTerm проверка при handleAppendEntries. TLA+ моделът (raft.tla:104-114) НЕ проверява дали follower има съвместим префикс преди репликация. Резултатът: LogMatching инвариантата е неизпълнима и беше премахната.

Въздействие: Моделът разрешава състояния, които реалната имплементация не би — follower може да получи entry с непоследователен prefix, което води до невалидни log състояния.

Стъпки:

1. Добавяне на prevLogIndex и prevLogTerm към Replicate действието в raft.tla
2. Precondition: nextIndex[i][j] > 1 => log[j][nextIndex[i][j]-1][1] = log[i][nextIndex[i][j]-1][1]
3. Ако precondition не е изпълнен: follower отхвърля, leader декрементира nextIndex[j]
4. Възстановяване на LogMatching инвариантата
5. Добавяне на TruncateConflict действие (follower трие конфликтни entries)

Очакван резултат: LogMatching минава, моделът по-точно отразява raft.nim

1.2. Raft: липсва leader step-down при partition

Проблем: StepDown действието изисква изричен newTerm > currentTerm. Няма механизъм за leader lease или heartbeat fail detection. Реалният raft (raft.nim:327-329) използва electionTimeout за detect на мъртъв leader.

Въздействие: Моделът не проверява, че leader се отказва при partition.

Стъпки:

1. Добавяне на HeartbeatTimeout(i) действие: follower/candidate който не е получил heartbeat в рамките на election timeout започва нова електората
2. Добавяне на LeaderLeaseExpired(i) действие: leader чийто lease е изтекъл става follower
3. Инвариант: LeaderLeaseSafety — два лидери нямат overlapping lease

1.3. 2PC: липсва coordinator failure/recovery

Проблем: Имплементацията (crossmodal.nim:222-245) има prepare/commit/rollback но не моделира coordinator crash. TLA+ спекът (twopc.tla) няма CrashCoordinator или RecoverCoordinator действие.

Въздействие: Ако coordinator крашне след DecideCommit, participant-ите остават в Prepared без да разберат решението.

Стъпки:

1. Добавяне на coordinatorLog променлива — персистентен лог на решението
2. CrashCoordinator(t) — coordinator спира, coordinatorDecided[t] остава но coordinator не отговаря
3. RecoverCoordinator(t) — coordinator чете coordinatorLog[t] и възстановява decidedAction[t]
4. ParticipantTimeout(t, p) — participant който не е получил решение в рамките на timeout решава ABORT
5. Инвариант: RecoveryConsistency — след recovery, coordinator решението е същото като преди crash

---

Приоритет 2 — Важни (нови свойства на съществуващи спекове)

2.1. Liveness свойства (темпорални)

Проблем: Само replication.tla има темпорално свойство (MonotonicLsn). Без liveness, моделите потвърждават safety (лоши неща не се случват) но не liveness (добри неща се случват).

Спек	Liveness свойство	Формула
raft	LeaderElectedEventually	<>(\E i \in Nodes : state[i] = "Leader")
twopc	Termination	<>[](\A t : txnState[t] \in {"Committed", "Aborted"})
mvcc	CommitProgress	<>(\A t : txnState[t] /= "Active" \/ txnStartTs[t] > 0)
gossip	DeadDetected	[]<>(\A n : state[n] = "Dead" => knownState[n][n] = "Dead")

Стъпки:

1. Добавяне на FAIRNESS условия в models/*.cfg (weak fairness: WF_vars(Next))
2. Добавяне на PROPERTIES секции към .cfg файловете
3. Проверка че liveness минава с fairness (TLC ще провери че всички fair behaviors задоволяват liveness)

Забележка: TLC проверката на liveness е по-бавна (изисква strongly-connected component analysis). Очаквано 2-5x забавяне.

2.2. MVCC: Write Skew Detection

Проблем: Snapshot isolation допуска write skew — два конкурентни транзакции четат различни ключове и записват на обратните. Имплементацията (mvcc.nim) не проверява за predicate-based конфликти.

Пример: T1 чете k1=0, T2 чете k2=0. T1 записва k2=1 (като k1=0). T2 записва k1=1 (като k2=0). И двете комитват — резултатът е нелегален.

Стъпки:

1. Добавяне на readPredicate[t] — множество ключове които t е прочел и използвал за решение
2. WriteSkewCheck в CommitTxn(t) — проверка че няма друг committed txn с overlapping predicate
3. Инвариант: NoWriteSkew — няма committed txn двойки с overlapping read predicates и disjoint write sets

2.3. Replication: SyncDurability поправка

Проблем: SyncDurability инвариантата беше премахната защото TLC я намираше за violated при appliedLsn=0. Причината: TLC обхожда IF/THEN/ELSE по различен начин от стандартната TLA+ семантика.

Стъпки:

1. Пренаписване на SyncDurability като чист implication: ~(mode = "Sync" /\ appliedLsn > 0) \/ (\A l \in 1..appliedLsn : pendingAcks[l] = {})
2. Добавяне на SyncCommitSafety — в sync mode, commitIndex се движи само когато всички replica ack-ове са получени

---

Приоритет 3 — Нови спекове

3.1. backup.tla — Backup/Restore протокол

Покрива: src/barabadb/core/backup.nim (498 реда)

Ключови свойства:

• BackupIntegrity — ако backup е създаден успешно, archive съдържа всички файлове от dataDir
• RestoreAtomicity — restore или напълно заменя dataDir, или rollback-ва до предишно състояние
• CleanupPreservesNewest — cleanup никога не трие най-новия backup
• NoDataLoss — след backup + restore, данните са идентични на оригинала

Стъпки:

1. Моделиране на DataDir като множество файлове
2. CreateBackup, RestoreBackup, CleanupOld действия
3. VerifyArchive действие — проверка на checksum
4. 4 инварианти + 1 liveness (restore в крайна сметка завършва)

3.2. crossmodal.tla — Cross-Modal Consistency

Покрива: src/barabadb/core/crossmodal.nim (250 реда)

Ключови свойства:

• CrossModalConsistency — обект който е в document store е достъпен и чрез vector/graph/FTS
• HybridScoreMonotonic — хибридният резултат не намалява при добавяне на повече индекси
• TPCAtomicity — cross-modal 2PC транзакцията е атомарна (вече покрито от twopc.tla, но тук е с concrete participants)

Стъпки:

1. Моделиране на IndexedObject — обект с id, който може да бъде в document/vector/graph/FTS индекс
2. InsertDocument, InsertVector, InsertGraph, IndexText действия
3. CrossModalInsert — атомарно инсъртване във всички индекси
4. Инвариант: ако обект е в 3 индекса, той е и в 4-тия

3.3. raft.tla — Membership Changes (Phase 2)

Покрива: raft cluster config промени (не е директно в raft.nim, но е критично за production)

Стъпки:

1. Добавяне на Config променлива — множество от активни възли
2. AddNode(i), RemoveNode(i) действия — joint consensus
3. ConfigCommitted — новата конфигурация е committed
4. Инвариант: JointConsensusSafety — по време на преход няма два лидера в различни конфигурации

---

Приоритет 4 — Инфраструктурни подобрения

4.1. CI поправка

Проблем: Текущият verify job в .github/workflows/ci.yml използва container: eclipse-temurin:21-jre което не споделя работната директория.

Стъпки:

1. Премахване на container: блока
2. Добавяне на setup-java action: uses: actions/setup-java@v4 с distribution: temurin и java-version: 21
3. Добавяне на continue-on-error: true за TLC стъпката (да не блокира PR-и при timeout)
4. Кеширане на tla2tools.jar с actions/cache

4.2. Симетрични редукции

Проблем: TLC проверява състояния които са симетрични пермутации (напр. {n1=Leader, n2=Follower, n3=Follower} е еквивалентно на {n2=Leader, n1=Follower, n3=Follower}).

Стъпки:

1. Добавяне на Symmetry в конфигурациите: SYMMETRY SymmetrySet
2. Дефиниране на SymmetrySet като пермутации на Nodes/Replicas/TxnIds
3. Очаквано 3-10x намаляване на състоянията → по-големи граници

4.3. Apalache migration (дългосрочно)

Проблем: TLC е explicit-state model checker — обхожда всяко състояние поотделно. Apalache е symbolic — използва SMT solver и може да проверява по-големи пространства.

Стъпки:

1. Инсталиране на Apalache (apalache-mc)
2. Конвертиране на 1-2 спека (започвайки с twopc.tla — най-простия)
3. Сравнение на резултати: TLC vs Apalache
4. Ако Apalache е по-бързо — миграция на всички спекове

---

Хронограма

Седмица	Задачи	Очакван резултат
1	1.1 Raft prevLogIndex + LogMatching, 4.1 CI	Raft спек по-точен, CI работи
2	1.3 2PC recovery, 2.3 SyncDurability	2PC по-реалистичен, replication по-силен
3	2.1 Liveness свойства (raft, twopc, gossip)	4 liveness свойства добавени
4	3.1 backup.tla	Нов спек за backup/restore
5-6	2.2 MVCC write skew, 3.2 crossmodal.tla	2 нови спека, по-силни инварианти
7-8	4.2 Symmetry reduction, 4.3 Apalache	5x повече проверени състояния

---

Метрики за успех

Метрика	Текущо	След Фаза 1	След Фаза 2
Спекове	7	8	10
Инварианти	26	34	45
Темпорални свойства	1	4	6
Покрити Nim модули	4/15	5/15	7/15
Проверени състояния (общо)	11.6M	25M	100M
CI време	~120s	~180s	~300s