Skip to content

Commit 5cbd874

Browse files
hyperpolymathclaude
andcommitted
refactor(rename): VQL → VCL (VeriSim Consonance Language) — complete propagation
VQL (VeriSim Query Language) has been renamed to VCL (VeriSim Consonance Language) across the entire nextgen-databases monorepo. File renames (58 files): - verisimdb/src/vql/ → verisimdb/src/vcl/ (11 ReScript modules) - verisimdb/playground/src/VqlKeywords.res → VclKeywords.res - verisimdb/elixir-orchestration/lib/verisim/query/vql_*.ex → vcl_*.ex (4 files) - verisimdb/elixir-orchestration/test/**vql*.ex/exs → vcl* (10 files) - verisimdb/rust-core/**/vql*.rs → vcl*.rs (4 files) - verisimdb/connectors/clients/*/vql.* → vcl.* (6 files across all SDKs) - verisimdb/connectors/clients/rescript/src/VeriSimVql.res → VeriSimVcl.res - verisimdb/vql-bridge/ → verisimdb/vcl-bridge/ - verisimdb/examples/vql-queries/ → vcl-queries/ + .vql → .vcl (10 files) - verisimdb/elixir-orchestration/test/fixtures/vql/ → vcl/ + .vql → .vcl - verisimdb/docs/vql-*.adoc → vcl-*.adoc + VQL-SPEC → VCL-SPEC (8 files) - typeql-experimental/docs/vql-dtpp-grammar.ebnf → vcl-dtpp-grammar.ebnf - typeql-experimental/examples/*.vqlut → *.vclut (7 files) Content updates: all VQL/vql/Vql occurrences → VCL/vcl/Vcl in ~160 files (source, docs, configs, specs — excluding .verisimdb/octads/ historical data) Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
1 parent 999ce70 commit 5cbd874

File tree

303 files changed

+2762
-2762
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

303 files changed

+2762
-2762
lines changed

.machine_readable/6a2/STATE.a2ml

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,7 @@ vcl-clauses = "ProofIntegrity, ProofConsistency, ProofFreshness, ProofConsonance
3333
[test-coverage]
3434
unit-tests = "~40 (Elixir consensus + federation adapters)"
3535
integration-tests = "~12 (federation adapter integration)"
36-
e2e-tests = "18 (e2e_verisimdb_test.exs — lifecycle, VQL, schema, error handling)"
36+
e2e-tests = "18 (e2e_verisimdb_test.exs — lifecycle, VCL, schema, error handling)"
3737
p2p-property-tests = "5 properties + 1 unit (kraft_property_test.exs)"
3838
aspect-security = "10 tests (aspect/security_test.exs)"
3939
aspect-concurrency = "14 tests (aspect/concurrency_test.exs)"
@@ -42,24 +42,24 @@ benchmarks = "2 Rust files (modality_benchmarks.rs + throughput_benchmarks.rs)"
4242
total-new-tests = "43 new tests + 5 properties (2026-04-04)"
4343

4444
[test-status]
45-
mix-test-failures = "6 pre-existing (VQLTypeChecker binary_to_existing_atom crash, KRaft remove_server timeout)"
45+
mix-test-failures = "6 pre-existing (VCLTypeChecker binary_to_existing_atom crash, KRaft remove_server timeout)"
4646
new-test-failures = "0"
4747
cargo-bench-compile = "PASS (throughput_benchmarks.rs — no errors, no warnings in bench file)"
4848
gleam-smoke = "Written; requires compiled lith_nif.so to run connection/lifecycle tests"
4949

5050
[blockers]
51-
- "VQLTypeChecker calls :erlang.binary_to_existing_atom for unknown proof types → ArgumentError (P1 hardening gap)"
52-
- "VQL parser does not strip null bytes from entity IDs (C-string truncation risk at FFI, P1)"
51+
- "VCLTypeChecker calls :erlang.binary_to_existing_atom for unknown proof types → ArgumentError (P1 hardening gap)"
52+
- "VCL parser does not strip null bytes from entity IDs (C-string truncation risk at FFI, P1)"
5353
- "Integration test (tests/integration_test.rs) uses old API — does not compile (pre-existing)"
5454
- "modality_benchmarks.rs uses old API — does not compile (pre-existing)"
5555

5656
[route-to-mvp]
5757
next = "Add Tropical_Determinants.thy + ProofOptimalAssignment VCL clause"
58-
then = "Fix VQLTypeChecker binary_to_existing_atom crash (P1 hardening)"
59-
then = "Fix null-byte entity ID sanitisation in VQL parser"
58+
then = "Fix VCLTypeChecker binary_to_existing_atom crash (P1 hardening)"
59+
then = "Fix null-byte entity ID sanitisation in VCL parser"
6060
then = "Update integration_test.rs to current API"
6161

6262
[critical-next-actions]
6363
1 = "Tropical_Determinants.thy new file — permanent = optimal assignment"
64-
2 = "Fix VQLTypeChecker to use String.to_existing_atom with rescue guard (P1)"
65-
3 = "Add null-byte sanitisation in VQLBridge built-in parser (P1)"
64+
2 = "Fix VCLTypeChecker to use String.to_existing_atom with rescue guard (P1)"
65+
3 = "Add null-byte sanitisation in VCLBridge built-in parser (P1)"

EXPLAINME.adoc

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,7 @@ The architecture shared across all three databases follows a layered stack:
3939
Web Frontend (ReScript SPA)
4040
----
4141

42-
Each layer is domain-specific. VeriSimDB uses VQL over a Rust/Elixir engine.
42+
Each layer is domain-specific. VeriSimDB uses VCL over a Rust/Elixir engine.
4343
QuandleDB uses KQL over a Julia (Skein.jl) engine. LithoGlyph uses GQL over
4444
a Forth/Factor/Zig engine with Idris2 proofs.
4545

@@ -59,7 +59,7 @@ cd verisimdb/elixir-orchestration && mix run ../demos/drift-detection/run_demo.e
5959
This demo creates 1000 entities, corrupts 50, and verifies that the drift
6060
detector identifies all 50 with zero false positives (in the sample output).
6161
The Elixir orchestration layer (`verisimdb/elixir-orchestration/`) coordinates
62-
the Rust core (`verisimdb/src/`) and the VQL parser (`verisimdb/src/vql/`).
62+
the Rust core (`verisimdb/src/`) and the VCL parser (`verisimdb/src/vcl/`).
6363

6464
The ABI layer at `verisimdb/src/abi/` (Idris2: `Types.idr`, `Layout.idr`,
6565
`Foreign.idr`) provides machine-checked memory layout proofs for the C-ABI
@@ -68,9 +68,9 @@ bridge between Rust and Elixir. The capability registry at
6868

6969
=== Honest caveat
7070

71-
VeriSimDB is at beta. The drift detection loop works (demo is live). The VQL
71+
VeriSimDB is at beta. The drift detection loop works (demo is live). The VCL
7272
query language is approximately 40% complete — basic entity CRUD and
73-
cross-modal consistency queries work; advanced dependent-type queries (VQL-DT)
73+
cross-modal consistency queries work; advanced dependent-type queries (VCL-DT)
7474
are planned. The "formally verified queries" claim in the README refers to
7575
the Idris2 ABI proofs, not end-to-end query verification (which is roadmap).
7676

@@ -92,7 +92,7 @@ ____
9292

9393
| *VeriSimDB*
9494
| PRIMARY — active development
95-
| Beta. Drift detection, octad entity model, Elixir orchestration, VQL parser
95+
| Beta. Drift detection, octad entity model, Elixir orchestration, VCL parser
9696
(~40% complete), Idris2 ABI proofs. Deployed with per-project instances
9797
(per VeriSimDB policy: one instance per consumer repo, never shared).
9898

@@ -136,15 +136,15 @@ use VeriSimDB.
136136
| Technology | Role in Next-Gen Databases | Also Used In
137137

138138
| *Rust* (VeriSimDB core)
139-
| Storage engine, VQL parser, drift detection algorithms
139+
| Storage engine, VCL parser, drift detection algorithms
140140
| ephapax, gitbot-fleet, protocol-squisher
141141

142142
| *Elixir* (VeriSimDB orchestration)
143143
| Distributed coordination, Phoenix API, BEAM fault tolerance
144144
| burble (voice platform), gossamer (service discovery target)
145145

146146
| *ReScript* (all frontends)
147-
| VQL query UI, QuandleDB frontend, planned LithoGlyph frontend
147+
| VCL query UI, QuandleDB frontend, planned LithoGlyph frontend
148148
| idaptik, panll, gossamer-powered SPAs
149149

150150
| *Idris2 ABI* (VeriSimDB + planned LithoGlyph)
@@ -180,10 +180,10 @@ repo for cross-modal entity consistency
180180
| Path | What It Proves
181181

182182
| `verisimdb/`
183-
| Primary database. `src/` — Rust core (storage, drift detection, VQL parser).
183+
| Primary database. `src/` — Rust core (storage, drift detection, VCL parser).
184184
`src/abi/` — Idris2 ABI proofs (Types.idr, Layout.idr, Foreign.idr).
185185
`src/registry/` — modality capability registry.
186-
`src/vql/` — VQL query language parser and evaluator.
186+
`src/vcl/` — VCL query language parser and evaluator.
187187
`elixir-orchestration/` — Elixir/Phoenix distributed coordinator.
188188
`api/` — JSON HTTP API surface.
189189
`demos/` — drift-detection demo (the live proof that octad consistency works).

ROADMAP.adoc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -21,8 +21,8 @@ Portfolio established with four database projects.
2121

2222
=== VeriSimDB
2323
* [x] Rust core engine
24-
* [x] VQL parser (ReScript)
25-
* [ ] VQL executor (Elixir)
24+
* [x] VCL parser (ReScript)
25+
* [ ] VCL executor (Elixir)
2626
* [ ] Web frontend
2727

2828
=== Lithoglyph

TEST-NEEDS.md

Lines changed: 15 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -11,43 +11,43 @@
1111
|-------------|--------|-------|
1212
| Unit tests | ~40 | VeriSimDB Elixir: consensus (kraft_node, kraft_wal, kraft_recovery, kraft_transport), federation adapters (mongodb, redis, duckdb, clickhouse, surrealdb, sqlite, neo4j, vector_db, influxdb, object_storage), resolver, adapter + base tests |
1313
| Integration | ~12 | Federation adapter integration tests (mongodb, redis, neo4j, clickhouse, surrealdb, influxdb) |
14-
| E2E | 18 | `verisimdb/elixir-orchestration/test/verisim/e2e_verisimdb_test.exs` — lifecycle, VQL, schema, error handling |
14+
| E2E | 18 | `verisimdb/elixir-orchestration/test/verisim/e2e_verisimdb_test.exs` — lifecycle, VCL, schema, error handling |
1515
| P2P (property) | 5 props + 1 test | `verisimdb/elixir-orchestration/test/verisim/consensus/kraft_property_test.exs` — leader uniqueness, log replication, state machine, partition tolerance, read-your-writes |
16-
| Aspect: Security | 10 tests | `verisimdb/elixir-orchestration/test/verisim/aspect/security_test.exs`VQL injection, unauthorised access, cross-tenant isolation, error disclosure |
17-
| Aspect: Concurrency | 14 tests | `verisimdb/elixir-orchestration/test/verisim/aspect/concurrency_test.exs` — concurrent entity writes, parallel VQL, concurrent Kraft proposals, DriftMonitor load, SchemaRegistry concurrency |
16+
| Aspect: Security | 10 tests | `verisimdb/elixir-orchestration/test/verisim/aspect/security_test.exs`VCL injection, unauthorised access, cross-tenant isolation, error disclosure |
17+
| Aspect: Concurrency | 14 tests | `verisimdb/elixir-orchestration/test/verisim/aspect/concurrency_test.exs` — concurrent entity writes, parallel VCL, concurrent Kraft proposals, DriftMonitor load, SchemaRegistry concurrency |
1818
| lithoglyph smoke | Gleam | `lithoglyph/beam/test/lith_beam_smoke_test.gleam` — version, connect, lifecycle, error handling |
19-
| Benchmarks | 2 real files | `verisimdb/benches/modality_benchmarks.rs` (Rust, pre-existing), `verisimdb/benches/throughput_benchmarks.rs` (Rust, new — write throughput, read latency, VQL complexity) |
19+
| Benchmarks | 2 real files | `verisimdb/benches/modality_benchmarks.rs` (Rust, pre-existing), `verisimdb/benches/throughput_benchmarks.rs` (Rust, new — write throughput, read latency, VCL complexity) |
2020

2121
**Source modules:** ~833 across 2 major subsystems. verisimdb: ~248 files (Rust core, Elixir orchestration, Gleam, Idris2 ABI, Zig FFI, ReScript). lithoglyph: ~212 files (Gleam, Rust, Factor).
2222

2323
## What's Done (2026-04-04)
2424

2525
### Completed
26-
- [x] VeriSimDB E2E tests (18 tests): write→read lifecycle, VQL pipeline, schema validation, error handling
26+
- [x] VeriSimDB E2E tests (18 tests): write→read lifecycle, VCL pipeline, schema validation, error handling
2727
- [x] Kraft consensus P2P property tests (5 properties + 1 unit): leader uniqueness, log replication, state machine safety, partition tolerance, read-your-writes
28-
- [x] VQL security aspect tests (10 tests): injection hardening, auth rejection, cross-tenant isolation, error disclosure
29-
- [x] Concurrency aspect tests (14 tests): concurrent EntityServer writes, parallel VQL, concurrent Kraft proposals, DriftMonitor load, SchemaRegistry concurrent registration
28+
- [x] VCL security aspect tests (10 tests): injection hardening, auth rejection, cross-tenant isolation, error disclosure
29+
- [x] Concurrency aspect tests (14 tests): concurrent EntityServer writes, parallel VCL, concurrent Kraft proposals, DriftMonitor load, SchemaRegistry concurrent registration
3030
- [x] lithoglyph Gleam smoke test: lifecycle smoke (graceful-failure when NIF not compiled)
31-
- [x] Rust throughput benchmarks: write throughput (1/10/100 batch), read latency (hot/cold), VQL complexity tiers, write-read round-trip latency
31+
- [x] Rust throughput benchmarks: write throughput (1/10/100 batch), read latency (hot/cold), VCL complexity tiers, write-read round-trip latency
3232

3333
### Known Gaps Surfaced by Tests
34-
- VQLTypeChecker calls `:erlang.binary_to_existing_atom/1` for unknown proof types → ArgumentError (hardening gap, P1)
35-
- VQL built-in parser does NOT strip null bytes from entity IDs (C-string truncation risk at FFI layer, P1)
34+
- VCLTypeChecker calls `:erlang.binary_to_existing_atom/1` for unknown proof types → ArgumentError (hardening gap, P1)
35+
- VCL built-in parser does NOT strip null bytes from entity IDs (C-string truncation risk at FFI layer, P1)
3636
- SchemaRegistry.register_type/1 returns `{:error, :already_exists}` for duplicate IRIs rather than idempotent `:ok` (P2)
3737
- `kraft_node_test.exs` `remove_server` test has a GenServer timeout (pre-existing, P2)
3838

3939
## What's Still Missing
4040

4141
### P2P (Property-Based) Tests
4242
- [ ] CRDT convergence: property tests for VeriSimDB's CRDT operations
43-
- [ ] VQL query parsing: arbitrary query fuzzing (replace fuzz placeholder)
43+
- [ ] VCL query parsing: arbitrary query fuzzing (replace fuzz placeholder)
4444
- [ ] Federation: property tests for data consistency across adapters
4545
- [ ] lithoglyph: data structure invariant tests
4646

4747
### E2E Tests
4848
- [ ] Federation: write through adapter → verify in external DB → read back
4949
- [ ] Kraft consensus: cluster formation → leader election → write → node failure → recovery
50-
- [ ] VQL: complex query execution with joins/aggregations
50+
- [ ] VCL: complex query execution with joins/aggregations
5151

5252
### Build & Execution
5353
- [ ] `mix test` for VeriSimDB Elixir (currently 6 pre-existing failures, not from new tests)
@@ -73,11 +73,11 @@
7373
- Unit + smoke: pre-existing + new E2E lifecycle tests
7474
- Build verification: `mix test` runs (6 pre-existing failures, not from new tests)
7575
- P2P: KRaft property tests
76-
- E2E: full lifecycle + VQL + schema + error paths
76+
- E2E: full lifecycle + VCL + schema + error paths
7777
- Reflexive: type hierarchy, schema self-validation
78-
- Contract: VQL proof certificate tests (pre-existing)
78+
- Contract: VCL proof certificate tests (pre-existing)
7979
- Aspect: security injection + concurrency tests
80-
- Benchmarks: Rust throughput/latency/VQL complexity baselines
80+
- Benchmarks: Rust throughput/latency/VCL complexity baselines
8181

8282
## FAKE-FUZZ ALERT
8383

TOOLING-STATUS.adoc

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ management, query execution, and PanLL dashboard panels.
1818
| Database | Query Language | BoJ ID | Status | Key Components
1919

2020
| **VeriSimDB**
21-
| VQL (Verified Query Language)
21+
| VCL (Verified Query Language)
2222
| 1
2323
| Mature
2424
| 10 ReScript modules: Parser, TypeChecker, BiDir, Subtyping, ProofObligation, Circuit, Explain, Context, Error, Types
@@ -65,7 +65,7 @@ Located at `boj-server/cartridges/database-mcp/`:
6565
* `db_connect_sqlite(path) → slot`
6666
* `db_disconnect(slot) → result`
6767
* `db_execute_sql(slot, query) → result` — PostgreSQL, SQLite
68-
* `db_execute_vql(slot, query) → result` — VeriSimDB
68+
* `db_execute_vcl(slot, query) → result` — VeriSimDB
6969
* `db_execute_kql(slot, query) → result` — QuandleDB
7070
* `db_execute_gql(slot, query) → result` — LithoGlyph
7171
* `db_begin_query(slot) / db_end_query(slot)` — Transaction boundaries
@@ -80,23 +80,23 @@ Located at `boj-server/cartridges/database-mcp/`:
8080
| `db-status` | Connection pool health across all backends
8181
| `db-connections` | Active connections, QPS metrics
8282
| `db-verisimdb` | Octad counts, proof counts, modality status
83-
| `vql-ut-safety-dashboard` | 10-level safety pipeline visualisation
84-
| `vql-ut-query-editor` | Live type-checking with Idris2 kernel (TypeLL)
85-
| `vql-ut-proof-explorer` | Obligation tracking and proof certificates
86-
| `vql-ut-horror-stories` | Interactive education — what each safety level prevents
83+
| `vcl-ut-safety-dashboard` | 10-level safety pipeline visualisation
84+
| `vcl-ut-query-editor` | Live type-checking with Idris2 kernel (TypeLL)
85+
| `vcl-ut-proof-explorer` | Obligation tracking and proof certificates
86+
| `vcl-ut-horror-stories` | Interactive education — what each safety level prevents
8787
|===
8888

8989
== Universal Safety Pipeline (TypeLL → Query Languages)
9090

9191
All query languages share the same 10-level safety model, originating in TypeLL.
92-
VQL-UT is the reference implementation. KQL and GQL map their constructs to the
92+
VCL-UT is the reference implementation. KQL and GQL map their constructs to the
9393
same levels — no separate "-UT" or "-DT" repos needed.
9494

9595
[source]
9696
----
9797
TypeLL (type theory core — defines the 10 levels)
9898
99-
├──→ VQL-UT (reference implementation, VeriSimDB)
99+
├──→ VCL-UT (reference implementation, VeriSimDB)
100100
├──→ KQL (applies same levels, QuandleDB)
101101
└──→ GQL (applies same levels, LithoGlyph)
102102
----
@@ -105,11 +105,11 @@ TypeLL (type theory core — defines the 10 levels)
105105

106106
Each query language has the same two tiers:
107107

108-
1. **The language** (VQL / KQL / GQL) — what users write
108+
1. **The language** (VCL / KQL / GQL) — what users write
109109
2. **The safety pipeline** — TypeLL's 10 levels applied progressively behind the
110110
language. Simple queries exit early at L1-L2. Proof-carrying queries go to L9-L10.
111111

112-
There is no "VQL-DT", "KQL-DT", or "GQL-DT" as separate products. Dependent type
112+
There is no "VCL-DT", "KQL-DT", or "GQL-DT" as separate products. Dependent type
113113
features are part of the safety pipeline at the appropriate levels.
114114

115115
=== The 10 Safety Levels
@@ -161,7 +161,7 @@ features are part of the safety pipeline at the appropriate levels.
161161

162162
=== Per-Database Safety Documentation
163163

164-
* **VQL:** `verisimdb/docs/vql-vs-vql-dt.adoc` — full spec with architecture diagram
164+
* **VCL:** `verisimdb/docs/vcl-vs-vcl-dt.adoc` — full spec with architecture diagram
165165
* **KQL:** `quandledb/docs/kql-safety-model.adoc` — KQL-specific mappings + Idris2 proofs
166166
* **GQL:** `lithoglyph/docs/gql-safety-model.adoc` — GQL-specific mappings + dependent types
167167

TOPOLOGY.md

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@
99
```
1010
┌─────────────────────────────────────────┐
1111
│ DB ANALYST / USER │
12-
│ (KQL, VQL, Web Dashboards) │
12+
│ (KQL, VCL, Web Dashboards) │
1313
└───────────────────┬─────────────────────┘
1414
1515
@@ -31,7 +31,7 @@
3131
┌─────────────────────────────────────────┐
3232
│ SATELLITE REPOSITORIES │
3333
│ ┌───────────┐ ┌───────────┐ ┌───────┐│
34-
│ │ Skein.jl │ │ VQL Parser│ │ FBQL- ││
34+
│ │ Skein.jl │ │ VCL Parser│ │ FBQL- ││
3535
│ │ (Engine) │ │ (ReScript)│ │ DT ││
3636
│ └───────────┘ └───────────┘ └───────┘│
3737
│ ┌───────────┐ ┌───────────┐ ┌───────┐│
@@ -67,7 +67,7 @@ DATABASE PORTFOLIO
6767
6868
QUERY LANGUAGES
6969
KQL (Knot Query) ██████░░░░ 60% Topology invariants active
70-
VQL (Verification) ████░░░░░░ 40% Compiler in progress
70+
VCL (Verification) ████░░░░░░ 40% Compiler in progress
7171
FBQL-DT (Dependently Typed) █████░░░░░ 50% Compile-time proofs active
7272
7373
REPO INFRASTRUCTURE

0 commit comments

Comments
 (0)