# Разпределена Система

BaraDB поддържа разпределено внедряване с Raft консенсус, шардиране, репликация и gossip протокол.

> ⚠️ **Ограничение при множество бази данни**
> Разпределените модули (Raft, шардиране и репликация) в момента работят само с **`default`** базата данни. Ако използвате множество бази (`CREATE DATABASE`, `USE DATABASE`), разпределените функции още не ги обхващат. Всяка база данни се нуждае от отделна кластър конфигурация.

## Raft Консенсус

Leader election и log репликация през TCP. Включване:

| Env | Значение |
|-----|----------|
| `BARADB_RAFT_ENABLED=true` | Включва Raft |
| `BARADB_RAFT_NODE_ID` | Id на този възел |
| `BARADB_RAFT_PORT` | Raft TCP порт |
| `BARADB_RAFT_PEERS` | Списък `id@host:port` (вкл. себе си) |
| `BARADB_RAFT_WRITE_TIMEOUT_MS` | Макс. изчакване за majority commit при SQL записи (по подразбиране 5000) |
| `BARADB_RAFT_CLIENT_PEERS` | Опционален `id@host:clientPort` map за leader write forwarding |
| `BARADB_RAFT_LOG_MAX_ENTRIES` | Лимит на in-memory raft log (по подразбиране 256); safe prefix compact |

Когато Raft е активен, SQL DML и schema DDL се приемат само от лидера на **`default`**. DML отива като put/delete; DDL — като `ddl` запис. Followers **препращат** write/DDL към лидера, ако е зададен `BARADB_RAFT_CLIENT_PEERS`; иначе връщат `not leader; leader is '…'`. Записи към друга database name се отказват. `CREATE`/`DROP DATABASE` не се репликират. Приложен DML обновява и secondary индекси/графи.

**Log compaction (v1):** след apply node-ът може да изреже safe prefix, когато log-ът надхвърли `BARADB_RAFT_LOG_MAX_ENTRIES`. Leader не реже след matchIndex на peer (catch-up с AppendEntries). Snapshot metadata се пази в `raft_state.bin`.

**Metrics:** при включен raft `GET /metrics` (HTTP = `BARADB_PORT + 440`) дава Prometheus редове: `baradb_raft_is_leader`, `baradb_raft_term`, `baradb_raft_log_entries`, `baradb_raft_apply_lag`, `baradb_raft_commit_wait_ms_total`, `baradb_raft_elections_total`, `baradb_raft_forwards_total`, `baradb_raft_compactions_total`. `GET /health` включва обект `raft` (`role`, `term`, `leader_id`, …).

```nim
import barabadb/core/raft

var cluster = newRaftCluster()
cluster.addNode("node1")
cluster.addNode("node2")
cluster.addNode("node3")

let n1 = cluster.nodes["n1"]
n1.becomeCandidate()
n1.becomeLeader()
let entry = n1.appendLog("SET key1 value1")
```

## Шардиране

Разпределение на данни между възли:

```nim
import barabadb/core/sharding

var router = newShardRouter(ShardConfig(
  numShards: 4,
  replicas: 2,
  strategy: ssHash
))
router.rebalance(@["node1", "node2", "node3"])
let shard = router.getShard("user_123")
```

### Стратегии за Шардиране

| Стратегия | Описание |
|-----------|----------|
| `ssHash` | Хеш-базирано шардиране |
| `ssRange` | Range-базирано шардиране |
| `ssConsistent` | Consistent hashing |

## Репликация

```nim
import barabadb/core/replication

var rm = newReplicationManager(rmSync)
rm.addReplica(newReplica("r1", "10.0.0.1", 9472))
rm.connectReplica("r1")
let lsn = rm.writeLsn(@[1'u8, 2, 3])
rm.ackLsn("r1", lsn)
```

### Режими на Репликация

| Режим | Описание |
|--------|----------|
| `rmSync` | Синхронна репликация |
| `rmAsync` | Асинхронна репликация |
| `rmSemiSync` | Полу-синхронна репликация |

## Gossip Протокол

Управление на членство и детекция на откази:

```nim
import barabadb/core/gossip

var g = newGossipProtocol("node1", "localhost", 9472, gossipPort = 9572)
g.join(newGossipNode("node2", "10.0.0.2", 9472))
```

## Разпределени Транзакции

Two-phase commit между възли:

```nim
import barabadb/core/disttxn

var tm = newDistTxnManager()
let txn = tm.beginTransaction("node1")
txn.addParticipant("node2", "10.0.0.2", 9472)
txn.prepare()
txn.commit()
```

## Формална Верификация

Основните разпределени алгоритми са формално специфицирани в TLA+ и проверени с TLC:

- **Raft Консенсус** — `formal-verification/raft.tla`
  - Проверено: ElectionSafety, StateMachineSafety
- **Two-Phase Commit** — `formal-verification/twopc.tla`
  - Проверено: Atomicity, NoOrphanBlocks
- **Репликация** — `formal-verification/replication.tla`
  - Проверено: MonotonicLsn, AcksRemovePending

Пускане на TLC локално:

```bash
cd formal-verification
java -cp tla2tools.jar tlc2.TLC -config models/raft.cfg raft.tla
java -cp tla2tools.jar tlc2.TLC -config models/twopc.cfg twopc.tla
java -cp tla2tools.jar tlc2.TLC -config models/replication.cfg replication.tla
```