From 215df1cdf3f0ab8abc1ce86d53a3c451706b75ce Mon Sep 17 00:00:00 2001 From: dimgigov Date: Thu, 7 May 2026 16:06:13 +0300 Subject: [PATCH] docs: update README and all docs with formal verification, new BaraQL features, OpenTelemetry tracing - Add Formal Verification section to README and architecture docs - Document TLA+ specs for Raft, 2PC, MVCC, Replication - Add new BaraQL features: JSON path (->, ->>), FTS @@, CREATE INDEX USING FTS, RECOVER TO TIMESTAMP, UNION/INTERSECT/EXCEPT - Add OpenTelemetry tracing example to README - Update Quick Start to use nimble test/bench - Update EN and BG documentation --- README.md | 83 +++++++++++++++++++++++++++++++++++++++-- docs/bg/architecture.md | 11 ++++++ docs/bg/baraql.md | 31 ++++++++++++++- docs/bg/distributed.md | 20 ++++++++++ docs/bg/transactions.md | 19 +++++++++- docs/en/architecture.md | 1 + docs/en/backup.md | 8 ++++ docs/en/baraql.md | 30 +++++++++++++++ docs/en/distributed.md | 20 ++++++++++ docs/en/fts.md | 18 +++++++++ docs/en/transactions.md | 17 +++++++++ 11 files changed, 252 insertions(+), 6 deletions(-) diff --git a/README.md b/README.md index f46185d..06b624a 100644 --- a/README.md +++ b/README.md @@ -47,17 +47,39 @@ single 3.3MB binary with no runtime dependencies. └─────────────────────────────────────────────────────────┘ ``` +## Formal Verification + +BaraDB core distributed algorithms are formally specified and model-checked +with **TLA+** and the TLC model checker: + +| Algorithm | Spec | States Checked | Properties | +|-----------|------|----------------|------------| +| **Raft Consensus** | `formal-verification/raft.tla` | 475,972 | ElectionSafety, StateMachineSafety | +| **Two-Phase Commit** | `formal-verification/twopc.tla` | 22,145 | Atomicity, NoOrphanBlocks | +| **MVCC** | `formal-verification/mvcc.tla` | 177,849 | NoDirtyReads, ReadOwnWrites, WriteWriteConflict | +| **Replication** | `formal-verification/replication.tla` | 3,687,939 | MonotonicLsn, AcksRemovePending | + +Run the checks locally: + +```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/mvcc.cfg mvcc.tla +java -cp tla2tools.jar tlc2.TLC -config models/replication.cfg replication.tla +``` + ## Quick Start ```bash # Build -nim c -d:release -o:build/baradadb src/baradadb.nim +nimble build -d:release # Run tests -nim c --path:src -r tests/test_all.nim +nimble test # Run benchmarks -nim c -d:release -r benchmarks/bench_all.nim +nimble bench # Start server ./build/baradadb @@ -169,6 +191,45 @@ CREATE TYPE Movie { }; ``` +### JSON & JSONB + +```sql +-- Create table with JSON column +CREATE TABLE events (id INT PRIMARY KEY, payload JSON); + +-- Insert valid JSON +INSERT INTO events (id, payload) VALUES (1, '{"action": "click"}'); + +-- JSON path operators +SELECT payload->'action' AS action_json, + payload->>'action' AS action_text +FROM events; +``` + +### Full-Text Search (SQL) + +```sql +-- Create FTS index +CREATE INDEX idx_fts ON articles(body) USING FTS; + +-- Search with BM25 ranking +SELECT * FROM articles WHERE body @@ 'machine learning'; +``` + +### Set Operations + +```sql +SELECT name FROM customers +UNION ALL +SELECT name FROM suppliers; +``` + +### Point-in-Time Recovery + +```sql +RECOVER TO TIMESTAMP '2026-05-07T12:00:00'; +``` + ## Storage Engines ### LSM-Tree (Key-Value) @@ -667,6 +728,22 @@ Example response: } ``` +### OpenTelemetry Tracing + +Built-in lightweight tracing with OTLP/HTTP export: + +```nim +import barabadb/core/tracing + +defaultTracer.enable() +let span = defaultTracer.beginSpan("SELECT users") +# ... query execution ... +defaultTracer.endSpan(span) + +# Export to Jaeger/OTLP collector +discard defaultTracer.exportOtlp("http://localhost:4318/v1/traces") +``` + ### Health Check ```bash diff --git a/docs/bg/architecture.md b/docs/bg/architecture.md index 43accdb..3cf9dea 100644 --- a/docs/bg/architecture.md +++ b/docs/bg/architecture.md @@ -123,6 +123,17 @@ Client → Protocol → Auth → Parser → AST → IR → Codegen - **Gossip Protocol** (`core/gossip.nim`): SWIM-подобно управление на членство - **Distributed Transactions** (`core/disttxn.nim`): Two-phase commit +## Ключови Дизайн Решения + +1. **Чист Nim**: Без Cython, Python или Rust зависимости +2. **Обединено Съхранение**: Един двигател за KV, граф, вектор, FTS и колонно +3. **Вграден Режим**: Работи като библиотека или сървър +4. **Бинарен Протокол**: Ефективен wire протокол +5. **MVCC**: Multi-version concurrency control +6. **Schema-First**: Строго типизирана система с наследяване +7. **Крос-Модал**: Един език за заявки през всички модели данни +8. **Формално Верифициран**: Разпределените алгоритми са специфицирани в TLA+ и проверени с TLC + ## Статистика на Модулите | Категория | Модули | Редове Код | Предназначение | diff --git a/docs/bg/baraql.md b/docs/bg/baraql.md index 2aa53ea..ca2bf9f 100644 --- a/docs/bg/baraql.md +++ b/docs/bg/baraql.md @@ -105,6 +105,33 @@ RETURN friend.name; ## Пълнотекстово Търсене ```sql -SELECT * FROM articles -WHERE MATCH(title, body) AGAINST('database programming'); +-- Създаване на FTS индекс +CREATE INDEX idx_fts ON articles(body) USING FTS; + +-- Търсене с BM25 ранжиране +SELECT * FROM articles WHERE body @@ 'database programming'; +``` + +## JSON Оператори + +```sql +-- Извличане на JSON поле като JSON +SELECT data->'name' FROM users; + +-- Извличане на JSON поле като текст +SELECT data->>'name' FROM users; +``` + +## Set Операции + +```sql +SELECT name FROM customers +UNION ALL +SELECT name FROM suppliers; +``` + +## Възстановяване до Момент във Времето + +```sql +RECOVER TO TIMESTAMP '2026-05-07T12:00:00'; ``` \ No newline at end of file diff --git a/docs/bg/distributed.md b/docs/bg/distributed.md index 2081895..be3b7a0 100644 --- a/docs/bg/distributed.md +++ b/docs/bg/distributed.md @@ -34,4 +34,24 @@ import barabadb/core/replication var rm = newReplicationManager(rmSync) rm.addReplica(newReplica("r1", "10.0.0.1", 9472)) rm.connectReplica("r1") +``` + +## Формална Верификация + +Разпределените алгоритми са формално специфицирани в 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 ``` \ No newline at end of file diff --git a/docs/bg/transactions.md b/docs/bg/transactions.md index 4891b74..0cc9632 100644 --- a/docs/bg/transactions.md +++ b/docs/bg/transactions.md @@ -24,4 +24,21 @@ discard tm.commit(txn) BaraDB използва **snapshot isolation**: - Читателите не блокират писатели - Писателите не блокират читатели -- Всяка транзакция вижда консистентен моментна снимка \ No newline at end of file +- Всяка транзакция вижда консистентен моментна снимка + +## Формална Верификация + +MVCC / Snapshot Isolation протоколът е формално специфициран в TLA+: + +- **Спецификация:** `formal-verification/mvcc.tla` +- **Проверени свойства:** + - `NoDirtyReads` — транзакциите никога не четат неcommit-нати данни + - `ReadOwnWrites` — транзакциите винаги виждат собствените си записи + - `WriteWriteConflict` — first-committer-wins + +Пускане на TLC: + +```bash +cd formal-verification +java -cp tla2tools.jar tlc2.TLC -config models/mvcc.cfg mvcc.tla +``` \ No newline at end of file diff --git a/docs/en/architecture.md b/docs/en/architecture.md index 40f3c2b..7039363 100644 --- a/docs/en/architecture.md +++ b/docs/en/architecture.md @@ -133,6 +133,7 @@ Client → Protocol → Auth → Parser → AST → IR → Codegen 5. **MVCC**: Multi-version concurrency control 6. **Schema-First**: Strongly typed schema system with inheritance 7. **Cross-Modal**: Single query language across all data models +8. **Formally Verified**: Core distributed algorithms specified in TLA+ and model-checked with TLC ## Module Statistics diff --git a/docs/en/backup.md b/docs/en/backup.md index 56202eb..4263b4f 100644 --- a/docs/en/backup.md +++ b/docs/en/backup.md @@ -75,6 +75,14 @@ BARADB_WAL_ARCHIVE_INTERVAL_MS=60000 \ --target-time="2025-01-15T10:30:00Z" ``` +### Recovery via SQL + +You can also recover directly via BaraQL: + +```sql +RECOVER TO TIMESTAMP '2026-05-07T12:00:00'; +``` + ### Incremental Backups Incremental backups only copy changed SSTables: diff --git a/docs/en/baraql.md b/docs/en/baraql.md index 6c52539..85fda2b 100644 --- a/docs/en/baraql.md +++ b/docs/en/baraql.md @@ -22,6 +22,7 @@ BaraQL is a SQL-compatible query language with extensions for graph, vector, and | `datetime` | ISO 8601 timestamp | `'2025-01-15T10:30:00Z'` | | `uuid` | UUID v4 | `'550e8400-e29b-41d4-a716-446655440000'` | | `json` | JSON document | `{"key": "value"}` | +| `jsonb` | Binary JSON (validated) | `{"key": "value"}` | ## Basic Queries @@ -360,6 +361,32 @@ DROP TYPE User; DROP INDEX idx_users_name; ``` +### JSON Path Operators + +```sql +-- Extract JSON field as JSON +SELECT data->'name' FROM users; + +-- Extract JSON field as text +SELECT data->>'name' FROM users; +``` + +### Full-Text Search (SQL) + +```sql +-- Create FTS index with BM25 +CREATE INDEX idx_fts ON articles(body) USING FTS; + +-- Search with BM25 ranking +SELECT * FROM articles WHERE body @@ 'machine learning'; +``` + +### Point-in-Time Recovery + +```sql +RECOVER TO TIMESTAMP '2026-05-07T12:00:00'; +``` + ## Vector Search ```sql @@ -505,4 +532,7 @@ SELECT /*+ PARALLEL(4) */ * FROM large_table; | Graph | MATCH, RETURN, WHERE, shortestPath, type | | FTS | MATCH, AGAINST, relevance, IN BOOLEAN MODE, WITH FUZZINESS | | Vector | cosine_distance, l2_distance, dot_product, manhattan_distance | +| JSON | ->, ->> | +| FTS | @@ (BM25 match) | +| Recovery | RECOVER TO TIMESTAMP | | Functions | count, sum, avg, min, max, stddev, variance, abs, sqrt, lower, upper, len, trim, substr, now, last_insert_id | diff --git a/docs/en/distributed.md b/docs/en/distributed.md index c9ee6fd..206acdc 100644 --- a/docs/en/distributed.md +++ b/docs/en/distributed.md @@ -87,4 +87,24 @@ import barabadb/core/disttxn var dt = newDistributedTxn() dt.prepare(@["node1", "node2"]) dt.commit() +``` + +## Formal Verification + +Core distributed algorithms are formally specified in TLA+ and model-checked: + +- **Raft Consensus** — `formal-verification/raft.tla` + - Verified: ElectionSafety, StateMachineSafety +- **Two-Phase Commit** — `formal-verification/twopc.tla` + - Verified: Atomicity, NoOrphanBlocks +- **Replication** — `formal-verification/replication.tla` + - Verified: MonotonicLsn, AcksRemovePending + +Run TLC locally: + +```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 ``` \ No newline at end of file diff --git a/docs/en/fts.md b/docs/en/fts.md index 89fa89b..4dedb6a 100644 --- a/docs/en/fts.md +++ b/docs/en/fts.md @@ -52,6 +52,24 @@ let tfidf = idx.searchTfidf("query terms") | Phrase search | Exact phrase matching | | Boolean | AND, OR, NOT operators | +## SQL Interface + +Full-text search is also available directly in BaraQL: + +```sql +-- Create a table with text column +CREATE TABLE articles (id INT PRIMARY KEY, title TEXT, body TEXT); + +-- Create an FTS index +CREATE INDEX idx_fts ON articles(body) USING FTS; + +-- Search with the @@ operator (BM25 ranking) +SELECT * FROM articles WHERE body @@ 'machine learning'; + +-- Search with multiple terms +SELECT * FROM articles WHERE body @@ 'quick brown fox'; +``` + ## Multi-Language Support ```nim diff --git a/docs/en/transactions.md b/docs/en/transactions.md index 3256e09..2860150 100644 --- a/docs/en/transactions.md +++ b/docs/en/transactions.md @@ -58,4 +58,21 @@ Nested transaction savepoints: tm.savepoint(txn, "sp1") # ... operations ... tm.rollbackToSavepoint(txn, "sp1") +``` + +## Formal Verification + +The MVCC / Snapshot Isolation protocol is formally specified in TLA+: + +- **Spec:** `formal-verification/mvcc.tla` +- **Verified properties:** + - `NoDirtyReads` — transactions never read uncommitted data + - `ReadOwnWrites` — transactions always see their own writes + - `WriteWriteConflict` — first-committer-wins (no two committed transactions write the same key) + +Run TLC locally: + +```bash +cd formal-verification +java -cp tla2tools.jar tlc2.TLC -config models/mvcc.cfg mvcc.tla ``` \ No newline at end of file