Baradb/formal-verification/UNIFIED_PLAN.md

БарaDB — Обединен план за подобрение (верификация + софтуер)

Версия: 2.0
Дата: 2026-05-07
Контекст: 7 TLA+ спека (11.6M състояния), 51 Nim модула (16K реда), 262 теста

---

Принцип

Формалната верификация е безползна ако не води до подобряване на кода. Всяка
стъпка по-долу има две страни: какво трябва да се докаже (TLA+) и какво
трябва да се поправи/добави в Nim кода. Когато TLA+ моделът открие
несъответствие с кода — това е бъг в кода или в модела. И двете се оправят.

---

Приоритет 1 — Критични разминавания между модел и код

1.1. Raft: Replicate без prevLogIndex проверка

Състояние:

• Nim (raft.nim:190-197): handleAppendEntries проверява prevLogIndex и prevLogTerm — ако follower няма entry на този индекс с този term, заявката се отхвърля.
• TLA+ (raft.tla:104-114): Replicate действието НЕ проверява това. LogMatching инвариантата беше премахната защото моделът я нарушава.

Какво да се направи:

#	Задача	Файл	Тип
1	Добави prevLogIndex/prevLogTerm precondition към Replicate	raft.tla	TLA+
2	Добави RejectAppendEntries действие (follower отхвърля при mismatch)	raft.tla	TLA+
3	Върни LogMatching инвариантата	raft.tla	TLA+
4	Добави тест "follower rejects append with wrong prevLogTerm"	test_all.nim	Nim
5	Поправи handleAppendEntries ако тестът покаже бъг	raft.nim	Nim

Критерий за успех: LogMatching минава в TLC + Nim тестът минава.

1.2. Replication: writeLsn не изпраща данни

Състояние:

• PLAN.md казва: "replication: writeLsn не изпраща данни към replicas"
• TLA+ (replication.tla): WriteLsn действието увеличава currentLsn и създава pendingAcks, но не моделира реален data transfer.
• Nim (replication.nim): writeLsn вероятно само increment-ва LSN без да праща data.

Какво да се направи:

#	Задача	Файл	Тип
6	Добави DataPayload променлива в TLA+ модела (кой LSN има какви данни)	replication.tla	TLA+
7	Инвариант: DataConsistency — ако replica ack-не LSN, данните са изпратени	replication.tla	TLA+
8	Имплементирай реално data изпращане в writeLsn	replication.nim	Nim
9	Добави тест "replica receives data for acked LSN"	test_all.nim	Nim

Критерий за успех: DataConsistency минава + Nim тестът потвърждава data transfer.

1.3. Sharding: rebalance не мигрира данни

Състояние:

• PLAN.md: "sharding: rebalance не мигрира данни"
• TLA+ (sharding.tla): Rebalance действието само променя shardToNodes mapping, не мигрира записи.
• Nim (sharding.nim:126-137): rebalance() само пренарежда nodeIds в shard-овете.

Какво да се направи:

#	Задача	Файл	Тип
10	Добави DataKeys променлива — множество ключове на всеки shard	sharding.tla	TLA+
11	Rebalance да мигрира ключове: DataKeys' = migrate(DataKeys, shardToNodes')	sharding.tla	TLA+
12	Инвариант: NoDataLoss — след rebalance, всички ключове са достъпни	sharding.tla	TLA+
13	Имплементирай migrateData() в Nim — read от стар shard, write в нов	sharding.nim	Nim
14	Тест "rebalance preserves all data"	test_all.nim	Nim

---

Приоритет 2 — Непокрити критични модули

2.1. Backup/Restore

Състояние: backup.nim (498 реда) няма тестове нито в TLA+, нито в Nim.
Това е единственият голям модул без никакво покритие.

#	Задача	Файл	Тип
15	TLA+ спек backup.tla — модел на backup/restore/cleanup цикъл	backup.tla	TLA+
16	Инвариант: RestoreAtomicity — restore или succeed-ва напълно, или rollback-ва	backup.tla	TLA+
17	Инвариант: CleanupPreservesNewest — cleanup никога не трие последния backup	backup.tla	TLA+
18	Nim тест suite: backup create, verify, restore, cleanup, history	test_all.nim	Nim
19	Nim тест: backup + restore round-trip с проверка на съдържанието	test_all.nim	Nim

Критерий за успех: TLC минава + 5+ Nim теста за backup.

2.2. Cross-Modal Consistency

Състояние: crossmodal.nim (250 реда) има тест в test_all.nim, но TLA+
моделът не проверява consistency между storage engines.

#	Задача	Файл	Тип
20	TLA+ спек crossmodal.tla — обект индексиран в 4-те engine-а	crossmodal.tla	TLA+
21	Инвариант: IndexConsistency — ако обект е в 3 индекса, е и в 4-тия	crossmodal.tla	TLA+
22	Инвариант: HybridScoreMonotonic — повече индекси → по-добър score	crossmodal.tla	TLA+
23	Nim тест: insert във всички engines → hybrid search намира обекта	test_all.nim	Nim

2.3. WAL Recovery

Състояние: recovery.nim (177 реда) има REDO/UNDO логика. TLA+ не я
моделира. Ако recovery е грешно — загуба на данни при crash.

#	Задача	Файл	Тип
24	TLA+ спек recovery.tla — модел на WAL replay с committed/uncommitted	recovery.tla	TLA+
25	Инвариант: CommittedSurvives — committed записи оцеляват след crash+recovery	recovery.tla	TLA+
26	Инвариант: UncommittedRolledBack — uncommitted записи се undo-ват	recovery.tla	TLA+
27	Nim тест: write → crash (без flush) → reopen → verify recovery	test_all.nim	Nim
28	Nim тест: write+commit → crash → reopen → committed данни са налице	test_all.nim	Nim

---

Приоритет 3 — Liveness и по-силни свойства

3.1. Liveness свойства (TLA+)

Без liveness, TLA+ проверява safety (лоши неща не се случват) но не
прогрес (добри неща се случват).

#	Спек	Liveness свойство	Защо
29	raft.tla	LeaderElectedEventually	Клъстерът в крайна сметка има лидер
30	twopc.tla	Termination	Всички транзакции в крайна сметка commit или abort
31	gossip.tla	DeadDetectedEventually	Мъртъв възел в крайна сметка е открит
32	replication.tla	LsnProgresses	appliedLsn в крайна сметка расте

Изисква: FAIRNESS WF_vars(Next) в .cfg файловете.
Внимание: TLC liveness проверката е 2-5x по-бавна от safety.

3.2. MVCC Write Skew Detection

Състояние: Snapshot isolation допуска write skew — класически проблем.
Нито TLA+ моделът, нито Nim кодът го проверяват.

#	Задача	Файл	Тип
33	Добави readPredicate[t] в mvcc.tla	mvcc.tla	TLA+
34	Инвариант: NoWriteSkew — два committed txn не могат да имат overlapping predicates	mvcc.tla	TLA+
35	Имплементирай predicate tracking в mvcc.nim	mvcc.nim	Nim
36	Тест "write skew is detected/prevented"	test_all.nim	Nim

3.3. 2PC Coordinator Crash/Recovery

Състояние: disttxn.nim има 2PC но без coordinator failure handling.

#	Задача	Файл	Тип
37	Добави CrashCoordinator(t) и RecoverCoordinator(t) в twopc.tla	twopc.tla	TLA+
38	Инвариант: RecoveryConsistency — решението е същото след recovery	twopc.tla	TLA+
39	Добави coordinator WAL в disttxn.nim — записва решението преди изпращане	disttxn.nim	Nim
40	Тест "coordinator recovery after crash"	test_all.nim	Nim

---

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

4.1. CI поправка

Проблем: verify job в CI използва container: което не работи с actions/checkout.

#	Задача	Файл
41	Замени container: eclipse-temurin:21-jre с setup-java action	.github/workflows/ci.yml
42	Добави continue-on-error: true за TLC стъпката	.github/workflows/ci.yml
43	Кеширай tla2tools.jar с actions/cache	.github/workflows/ci.yml

4.2. Symmetry Reduction

Проблем: TLC проверява симетрични пермутации отделно. С 3 нода има 3!=6
еквивалентни състояния за всяко реално състояние.

#	Задача	Файл
44	Добави Symmetry sets в raft.cfg, gossip.cfg, replication.cfg	models/*.cfg
45	Увеличи границите: raft 5 nodes, gossip 5 nodes	models/*.cfg

4.3. Липсващи Nim тестове

Проблем: 4 модула нямат dedicated тест suite.

#	Модул	Тестове за добавяне
46	core/logging	JSON формат, нива, файл output
47	core/websocket	Frame parsing, SUBSCRIBE/UNSUBSCRIBE
48	core/config	Env vars, JSON файл, defaults, validation
49	core/backup	Вж. 2.1 по-горе

4.4. Inter-module интеграция

Проблем: PLAN.md казва "няма raft→disttxn, gossip→sharding, replication→disttxn връзки".

#	Връзка	Какво липсва	Тип
50	Raft → DistTxn	2PC решенията трябва да се replic-ват през Raft	Nim
51	Gossip → Sharding	При node failure, gossip нотифицира sharding за rebalance	Nim
52	Replication → DistTxn	Distributed txn commit изисква replication ack	Nim
53	TLA+ модел на интеграцията	Raft + 2PC + Replication в един спек	TLA+ (дългосрочно)

---

Хронограма

Седмица	Задачи	Резултат
1	#1-5 (Raft prevLogIndex + LogMatching)	Raft модел по-точен от кода, 1 нов тест
2	#6-14 (Replication data + Sharding migration)	2 distributed gap-а затворени, 3 нови теста
3	#15-28 (Backup, CrossModal, Recovery спекове + тестове)	3 нови TLA+ спека, 8+ нови теста
4	#29-32 (Liveness)	4 темпорални свойства добавени
5	#33-40 (Write skew, 2PC crash)	2 критични safety gap-а затворени
6	#41-53 (CI, Symmetry, тестове, интеграция)	Инфраструктурата стабилна

---

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

Метрика	Сега	След плана
TLA+ спекове	7	10 (+backup, crossmodal, recovery)
TLA+ инварианти	26	42
TLA+ темпорални свойства	1	5
Проверени състояния	11.6M	50M+ (със symmetry)
Nim тестове	262	285+
Покрити модули (test)	47/51	51/51
Distributed gaps (PLAN.md)	4	0
Inter-module връзки	0	3