# План за подобрения на формалната верификация на 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 |