diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index a0faa51..d339165 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -47,11 +47,11 @@ verisimdb/ │ ├── verisim-drift/ # Drift detection │ ├── verisim-normalizer/ # Self-normalization │ ├── verisim-planner/ # Cost-based query planner -│ ├── verisim-repl/ # Interactive VQL REPL +│ ├── verisim-repl/ # Interactive VCL REPL │ ├── verisim-wal/ # Write-ahead log │ └── verisim-storage/ # Storage backend abstraction ├── elixir-orchestration/ # Elixir/OTP coordination layer -├── playground/ # VQL Playground PWA (ReScript) +├── playground/ # VCL Playground PWA (ReScript) ├── container/ # Containerfile for Podman builds ├── docs/ # Architecture and design documents ├── contractiles/ # Trust, security, and policy contracts @@ -158,8 +158,8 @@ cargo fmt --check |----------|----------| | **Rust** | Core database engine, modality stores, CLI tools | | **Elixir** | OTP orchestration, distributed coordination | -| **ReScript** | VQL parser, playground PWA | -| **VQL** | VeriSim Consonance Language (query interface) | +| **ReScript** | VCL parser, playground PWA | +| **VCL** | VeriSim Consonance Language (query interface) | ### Not Accepted diff --git a/KNOWN-ISSUES.adoc b/KNOWN-ISSUES.adoc index 1841625..57178d8 100644 --- a/KNOWN-ISSUES.adoc +++ b/KNOWN-ISSUES.adoc @@ -50,14 +50,14 @@ VeriSimDB is a working system with real implementations in its core modality sto **Original issue:** Drift detection had to be triggered manually. No scheduled or event-driven trigger existed. -=== 5. VCL-DT Not Connected to VQL PROOF Runtime — ✅ RESOLVED +=== 5. VCL-DT Not Connected to VCL PROOF Runtime — ✅ RESOLVED -**Location:** `elixir-orchestration/lib/verisim/query/vql_type_checker.ex`, `vql_executor.ex`, `vql_bridge.ex` +**Location:** `elixir-orchestration/lib/verisim/query/vcl_type_checker.ex`, `vcl_executor.ex`, `vcl_bridge.ex` **Resolved:** 2026-02-28. VCL-DT proof pipeline is now fully wired end-to-end with a three-tier type checking strategy: -1. **ReScript bidirectional type checker** (VQLBidir.res, 852 lines) — full formal system with subtyping, invoked via VQLBridge.typecheck/2 when Deno subprocess available -2. **Elixir-native type checker** (VQLTypeChecker, 320 lines) — validates proof types, modality compatibility, composition rules; generates structured obligations with witness fields and circuit names. Used when ReScript subprocess unavailable. +1. **ReScript bidirectional type checker** (VQLBidir.res, 852 lines) — full formal system with subtyping, invoked via VCLBridge.typecheck/2 when Deno subprocess available +2. **Elixir-native type checker** (VCLTypeChecker, 320 lines) — validates proof types, modality compatibility, composition rules; generates structured obligations with witness fields and circuit names. Used when ReScript subprocess unavailable. 3. **Bare AST extraction** — last resort, no longer needed since the native checker handles all cases Additionally: @@ -72,15 +72,15 @@ Additionally: === 6. ZKP / Sanctify Library Integration — ✅ RESOLVED -**Location:** `rust-core/verisim-semantic/src/{zkp.rs, zkp_bridge.rs, sanctify_bridge.rs}`, `elixir-orchestration/lib/verisim/query/vql_executor.ex`, `vql_type_checker.ex` +**Location:** `rust-core/verisim-semantic/src/{zkp.rs, zkp_bridge.rs, sanctify_bridge.rs}`, `elixir-orchestration/lib/verisim/query/vcl_executor.ex`, `vcl_type_checker.ex` -**Resolved:** ZKP and sanctify integrations are implemented across three Rust modules and routed through the VQL pipeline: +**Resolved:** ZKP and sanctify integrations are implemented across three Rust modules and routed through the VCL pipeline: - `zkp.rs` (367 LOC) — hash commitments (SHA-256), Merkle proofs, and verification primitives. - `zkp_bridge.rs` (628 LOC) — wires ZKP primitives to the `ProofBlob`/`SemanticStore` types so CBOR-encoded `VerifiableProofData` round-trips through the semantic modality. - `sanctify_bridge.rs` (413 LOC) — consumes sanctify-php JSON reports, maps OWASP/WordPress security findings into security contracts, and binds them to octads as semantic annotations. -- VQL type checker (`vql_type_checker.ex`) registers `ZKP` and `SANCTIFY` as first-class proof types with modality compatibility (`semantic`), required witness fields, and circuit names (`zkp-base`, `sanctify-v1`). -- VQL executor (`vql_executor.ex`) routes `PROOF ZKP(...)` queries to `RustClient.post("/proofs/generate", ...)` and `PROOF SANCTIFY(...)` to contract-existence validation against the semantic store. +- VCL type checker (`vcl_type_checker.ex`) registers `ZKP` and `SANCTIFY` as first-class proof types with modality compatibility (`semantic`), required witness fields, and circuit names (`zkp-base`, `sanctify-v1`). +- VCL executor (`vcl_executor.ex`) routes `PROOF ZKP(...)` queries to `RustClient.post("/proofs/generate", ...)` and `PROOF SANCTIFY(...)` to contract-existence validation against the semantic store. **Original issue:** ZKP/sanctify integration was documented as a consultation paper only; no circuits, proofs, or runtime verification existed. Resolution was blocked on VCL-DT (issue 5), which has also been resolved. @@ -145,15 +145,15 @@ Added `rescript.json` for build configuration. === 12. Cross-Modal Drift/Consistency Were Stubs — ✅ RESOLVED -**Location:** `elixir-orchestration/lib/verisim/query/vql_executor.ex` +**Location:** `elixir-orchestration/lib/verisim/query/vcl_executor.ex` **Resolved:** 2026-02-13. `compute_modality_drift/3` now fetches drift from the Rust drift API when available, falling back to cosine distance between extracted modality embeddings (with content fingerprinting for non-vector modalities). `compute_consistency/4` now computes real scores using the specified metric (COSINE, EUCLIDEAN, DOT_PRODUCT, JACCARD). Both functions previously returned hardcoded constants (0.0 and 0.5). **Original issue:** Cross-modal correlation queries parsed correctly but evaluation returned fake scores, making WHERE DRIFT(...) and CONSISTENT(...) conditions meaningless. -=== 13. VQL WHERE Condition Routing Was Broken — ✅ RESOLVED +=== 13. VCL WHERE Condition Routing Was Broken — ✅ RESOLVED -**Location:** `elixir-orchestration/lib/verisim/query/vql_executor.ex` +**Location:** `elixir-orchestration/lib/verisim/query/vcl_executor.ex` **Resolved:** 2026-02-13. `has_fulltext_condition?/1`, `has_vector_condition?/1`, and `has_graph_pattern?/1` now walk the AST recursively to detect actual condition types. `extract_text_query/1`, `extract_vector_query/1`, and `extract_graph_query/1` now parse actual values from the AST instead of returning hardcoded placeholders. All queries were previously routed to `:multi` type regardless of conditions. @@ -161,11 +161,11 @@ Added `rescript.json` for build configuration. === 14. Proof Verification Was No-Op — ✅ RESOLVED -**Location:** `elixir-orchestration/lib/verisim/query/vql_executor.ex` +**Location:** `elixir-orchestration/lib/verisim/query/vcl_executor.ex` **Resolved:** 2026-02-13. `verify_single_proof/1` now validates proof type, extracts contract names, and checks contract existence against the semantic store. It properly rejects queries with invalid or missing contracts for CITATION, INTEGRITY, and CUSTOM proof types. Previously it always returned `:ok`. -**Original issue:** PROOF clauses in VQL queries were parsed but never verified. All proofs silently passed, making the entire proof system decorative. +**Original issue:** PROOF clauses in VCL queries were parsed but never verified. All proofs silently passed, making the entire proof system decorative. === 15. believe_me in Idris2 ABI Files — ✅ RESOLVED @@ -175,9 +175,9 @@ Added `rescript.json` for build configuration. **Original issue:** `registerCallback` used `believe_me` to cast a callback function to `AnyPtr`, a BANNED unsafe pattern that bypasses the type checker. -=== 16. Atom Table Exhaustion Risk in VQL Bridge — ✅ RESOLVED +=== 16. Atom Table Exhaustion Risk in VCL Bridge — ✅ RESOLVED -**Location:** `elixir-orchestration/lib/verisim/query/vql_bridge.ex` +**Location:** `elixir-orchestration/lib/verisim/query/vcl_bridge.ex` **Resolved:** 2026-02-13. All 8 `String.to_atom` calls replaced with `safe_to_atom/1` helper that uses an explicit allowlist map for the known atom values (6 modalities + 5 aggregate functions + `all`), falling back to `String.to_existing_atom/1`. @@ -193,15 +193,15 @@ Added `rescript.json` for build configuration. === 18. EXPLAIN Returns Hardcoded Plan — ✅ RESOLVED -**Location:** `elixir-orchestration/lib/verisim/query/vql_executor.ex` +**Location:** `elixir-orchestration/lib/verisim/query/vcl_executor.ex` **Resolved:** 2026-02-13. `generate_explain_plan/1` now analyzes the actual query AST to produce cost estimates based on source type, modality count, WHERE clause complexity, cross-modal conditions, GROUP BY presence, and proof obligations. Delegates to the Rust verisim-planner API when available, with local estimation as fallback. **Original issue:** EXPLAIN returned a static plan with hardcoded step names and costs totalling 71ms, regardless of the actual query structure. -=== 19. VQL Executor Federation Stub — ✅ RESOLVED +=== 19. VCL Executor Federation Stub — ✅ RESOLVED -**Location:** `elixir-orchestration/lib/verisim/query/vql_executor.ex`, `rust-core/verisim-api/src/federation.rs` +**Location:** `elixir-orchestration/lib/verisim/query/vcl_executor.ex`, `rust-core/verisim-api/src/federation.rs` **Resolved:** 2026-02-13. Added `GET /octads` list endpoint with `?limit=N&offset=M` pagination to the Rust API. The `OctadStore` trait now includes a `list(limit, offset)` method. Federation `query_single_peer()` now falls back to the `/octads` list endpoint when neither text_query nor vector_query is provided, so bare `SELECT * FROM FEDERATION /pattern/*` returns actual octad data instead of empty results. @@ -214,14 +214,14 @@ Added `rescript.json` for build configuration. - Circuit Registry: named circuit storage with register/get/verify/list/unregister operations - Circuit Compiler: DSL gates (AND, OR, XOR, NOT, LinearCombination) compiled to R1CS constraints - Verification Key Store: per-circuit keys with rotation support and federation export/import -- VQL Circuit DSL: ReScript types for circuit definition with `PROOF CUSTOM "name" WITH (param=value)` +- VCL Circuit DSL: ReScript types for circuit definition with `PROOF CUSTOM "name" WITH (param=value)` - 25 semantic tests pass covering circuit operations **Original issue:** The `CUSTOM` proof type used a hardcoded circuit configuration with no DSL, compiler, or registry. -=== 21. VCL-DT Not Connected to VQL PROOF Runtime — ✅ RESOLVED +=== 21. VCL-DT Not Connected to VCL PROOF Runtime — ✅ RESOLVED -**Location:** `elixir-orchestration/lib/verisim/query/vql_type_checker.ex` +**Location:** `elixir-orchestration/lib/verisim/query/vcl_type_checker.ex` **Resolved:** 2026-02-28. Superseded by issue #5 resolution. The VCL-DT pipeline is now wired with an Elixir-native type checker that validates proof types, modality compatibility, and composition rules without requiring the ReScript subprocess or a Lean checker. The Lean formal verification path remains aspirational (no Lean files were ever created); the practical implementation uses the ReScript bidirectional type checker (852 lines) backed by an Elixir fallback (320 lines). @@ -231,7 +231,7 @@ Added `rescript.json` for build configuration. **Location:** `rust-core/verisim-semantic/src/proven_bridge.rs` -**Resolved:** 2026-02-13. Created `proven_bridge.rs` (277 LOC) that parses JSON/CBOR proof certificates from the proven library, verifies signatures, and converts certificates to ProofBlob format for storage in the semantic modality. VQL executor routes `PROOF PROVEN(...)` queries through the bridge. Integration is certificate-based (JSON exchange) rather than direct Idris2 FFI. +**Resolved:** 2026-02-13. Created `proven_bridge.rs` (277 LOC) that parses JSON/CBOR proof certificates from the proven library, verifies signatures, and converts certificates to ProofBlob format for storage in the semantic modality. VCL executor routes `PROOF PROVEN(...)` queries through the bridge. Integration is certificate-based (JSON exchange) rather than direct Idris2 FFI. === 23. verisim-repl Has Build Issues — ✅ RESOLVED diff --git a/ROADMAP.md b/ROADMAP.md index 7b70a63..634f6f5 100644 --- a/ROADMAP.md +++ b/ROADMAP.md @@ -5,7 +5,7 @@ Criticality-ordered plan. Toolchain first, then infrastructure, then ecosystem. **Completed prerequisites** (this session): - [x] verisim-planner crate (cost-based query planning) - [x] Triple API (REST + GraphQL + gRPC) -- [x] VQL AST → LogicalPlan bridge +- [x] VCL AST → LogicalPlan bridge - [x] Proof obligation costing (per-type: existence→ZKP) - [x] Adaptive tuning (actual vs estimated latency feedback) - [x] Post-processing + cross-modal cost models @@ -13,33 +13,33 @@ Criticality-ordered plan. Toolchain first, then infrastructure, then ecosystem. --- -## Phase 1: VQL Toolchain (HIGHEST PRIORITY) +## Phase 1: VCL Toolchain (HIGHEST PRIORITY) -### 1.1 VQL REPL — Rust CLI +### 1.1 VCL REPL — Rust CLI **Criticality: CRITICAL** | Effort: Medium | Crate: `verisim-repl` Every database has an interactive shell. Without one, VeriSimDB is unusable for exploration and debugging. -- Rust CLI binary (`vql` command) +- Rust CLI binary (`vcl` command) - Readline/rustyline for input editing, history, multiline - HTTP client to verisim-api (configurable endpoint) - Commands: `\connect`, `\explain`, `\timing`, `\format json|table|csv` -- Syntax highlighting for VQL keywords +- Syntax highlighting for VCL keywords - Tab completion for modalities, proof types - Output formatters: table (default), JSON, CSV -- `.vqlrc` config file support +- `.vclrc` config file support -### 1.2 VQL REPL — Elixir IEx Extension -**Criticality: HIGH** | Effort: Small | Module: `VeriSim.VQL.IEx` +### 1.2 VCL REPL — Elixir IEx Extension +**Criticality: HIGH** | Effort: Small | Module: `VeriSim.VCL.IEx` -- `use VeriSim.VQL.IEx` in IEx sessions -- `vql("SELECT GRAPH FROM OCTAD ...")` function +- `use VeriSim.VCL.IEx` in IEx sessions +- `vcl("SELECT GRAPH FROM OCTAD ...")` function - Pretty-printed results with modality indicators -- `vql_explain/1` for EXPLAIN output +- `vcl_explain/1` for EXPLAIN output - Direct in-process execution (no HTTP round-trip) -### 1.3 VQL Language Server (LSP) +### 1.3 VCL Language Server (LSP) **Criticality: HIGH** | Effort: Large | Crate: `verisim-lsp` - Diagnostics: parse errors, unknown modalities, type mismatches @@ -49,11 +49,11 @@ for exploration and debugging. - VS Code extension + Neovim plugin - Uses existing ReScript parser via JSON bridge -### 1.4 VQL Formatter +### 1.4 VCL Formatter **Criticality: MEDIUM** | Effort: Small | Module in `verisim-repl` -- `vql fmt` subcommand -- Canonical formatting for VQL queries +- `vcl fmt` subcommand +- Canonical formatting for VCL queries - Keyword uppercasing, consistent indentation - Integrates with LSP `textDocument/formatting` @@ -202,7 +202,7 @@ Close the loop between estimated and actual costs. - Parse-once, execute-many for repeated queries - Plan caching (skip re-optimization for identical plans) -- Parameterized queries (prevent VQL injection) +- Parameterized queries (prevent VCL injection) - Cache invalidation on schema/config changes ### 5.3 Result Streaming @@ -245,7 +245,7 @@ Close the loop between estimated and actual costs. **Criticality: MEDIUM** | Effort: Large - Federation resolver returns real results (currently empty) -- Cross-instance VQL queries +- Cross-instance VCL queries - Drift-aware federation (respect drift policies) - Federation discovery protocol @@ -266,16 +266,16 @@ Can't claim best-in-class without numbers. ### 7.2 Client Libraries **Criticality: HIGH** | Effort: Medium -- Rust SDK (typed, async, with VQL builder) +- Rust SDK (typed, async, with VCL builder) - Elixir SDK (direct BEAM integration) -- ReScript SDK (VQL builder + type-safe results) +- ReScript SDK (VCL builder + type-safe results) - Each SDK: connection pooling, retry logic, auth ### 7.3 Documentation Site **Criticality: MEDIUM** | Effort: Medium - API reference (auto-generated from proto + GraphQL schema) -- VQL language guide with examples +- VCL language guide with examples - Architecture guide (Marr's three levels) - Tutorial: "Build a multimodal search in 10 minutes" - Deployment guide (Podman + Containerfile) @@ -323,23 +323,23 @@ Can't claim best-in-class without numbers. | # | Item | Phase | Criticality | |---|------|-------|-------------| -| 1 | VQL REPL (Rust CLI) | 1.1 | CRITICAL | +| 1 | VCL REPL (Rust CLI) | 1.1 | CRITICAL | | 2 | Write-Ahead Log | 2.1 | CRITICAL | | 3 | Real normalizer regeneration | 4.1 | CRITICAL | | 4 | Authentication | 3.1 | CRITICAL | | 5 | ACID transactions | 2.2 | CRITICAL | -| 6 | VQL REPL (Elixir IEx) | 1.2 | HIGH | +| 6 | VCL REPL (Elixir IEx) | 1.2 | HIGH | | 7 | ZKP/PLONK integration | 3.4 | HIGH | | 8 | Authorization (RBAC) | 3.2 | HIGH | | 9 | Query profiling (EXPLAIN ANALYZE) | 5.1 | HIGH | -| 10 | VQL LSP | 1.3 | HIGH | +| 10 | VCL LSP | 1.3 | HIGH | | 11 | Persistence backends | 2.3 | HIGH | | 12 | Benchmarks vs ArangoDB/SurrealDB/Virtuoso | 7.1 | HIGH | | 13 | Client libraries | 7.2 | HIGH | | 14 | Snapshots & backup | 2.4 | HIGH | | 15 | Conflict resolution | 4.2 | HIGH | | 16 | Replication | 6.1 | HIGH | -| 17 | VQL formatter | 1.4 | MEDIUM | +| 17 | VCL formatter | 1.4 | MEDIUM | | 18 | Encryption at rest | 3.3 | MEDIUM | | 19 | Result streaming | 5.3 | MEDIUM | | 20 | Prepared statements | 5.2 | MEDIUM | diff --git a/TESTING.md b/TESTING.md index e8068b7..03e8cc6 100644 --- a/TESTING.md +++ b/TESTING.md @@ -26,7 +26,7 @@ Rust core and integration tests at the Elixir↔Rust HTTP boundary. The coverage floor is set at **60%** to start, with the intention of ratcheting upward as the test suite matures. The industry baseline is 80% line coverage (per Codecov's published guidance); we'll move there once -the bigger gap modules (vql_executor) have richer coverage. +the bigger gap modules (vcl_executor) have richer coverage. ## Rust standards @@ -108,7 +108,7 @@ Patterns adopted: Established examples: - `test/verisim/property/schema_registry_props_test.exs` (7 properties) -- `test/verisim/property/vql_bridge_props_test.exs` (6 properties) +- `test/verisim/property/vcl_bridge_props_test.exs` (6 properties) ### Benchmarks — `benchee` @@ -225,7 +225,7 @@ Mutation score targets: These are documented for future work; no current CI gate enforces them. -- **Snapshot testing (Elixir)**: `mneme` for built-in VQL parser output. +- **Snapshot testing (Elixir)**: `mneme` for built-in VCL parser output. Skipped initially because `mneme`'s interactive accept/reject doesn't fit batch CI; we'd need to wire `MNEME_REPLY=accept` workflow. - **Differential testing**: SQLancer-style queries through redb vs @@ -235,6 +235,6 @@ These are documented for future work; no current CI gate enforces them. transactions; `concuerror` for Elixir supervision tree. - **Bench-as-PR-gate**: `codspeed-criterion-compat` or `bencher.dev` for noise-resistant perf regression detection. -- **AFL++ alongside libFuzzer**: structure-aware fuzzing of the VQL +- **AFL++ alongside libFuzzer**: structure-aware fuzzing of the VCL grammar via `arbitrary` derive on AST types, corpus sync across cargo-fuzz / AFL++ / honggfuzz. diff --git a/connectors/README.adoc b/connectors/README.adoc index d46085e..309f842 100644 --- a/connectors/README.adoc +++ b/connectors/README.adoc @@ -22,7 +22,7 @@ target store. **Inbound (Client SDKs)**:: External applications reach _in_ to VeriSimDB through idiomatic client libraries. Each SDK wraps the REST / gRPC API, handles authentication, connection pooling, and provides type-safe access to -octad entities, VQL queries, and drift reports. +octad entities, VCL queries, and drift reports. === Architecture Diagram diff --git a/connectors/clients/zig/README.adoc b/connectors/clients/zig/README.adoc index c0de131..ec0e503 100644 --- a/connectors/clients/zig/README.adoc +++ b/connectors/clients/zig/README.adoc @@ -27,7 +27,7 @@ rather than via a maintained per-language SDK. | `src/drift.zig` | Drift: `score / status / normalize`. | `src/provenance.zig` | Provenance: `chain / record / verify`. | `src/search.zig` | Multi-modal search: text / vector / spatial / nearest / related. -| `src/vql.zig` | VQL: `execute / explain`. +| `src/vql.zig` | VCL: `execute / explain`. | `src/federation.zig` | Federation: `registerPeer / listPeers / query`. |=== diff --git a/docs/INDEX.md b/docs/INDEX.md index e44bacd..69c1fe2 100644 --- a/docs/INDEX.md +++ b/docs/INDEX.md @@ -82,17 +82,17 @@ The repo root holds only documents that need maximum visibility for new readers, - [docs/design/DESIGN-2026-02-27-vcl-dt-assessment.adoc](design/DESIGN-2026-02-27-vcl-dt-assessment.adoc) - [docs/design/DESIGN-2026-02-28-panll-interop-telemetry.md](design/DESIGN-2026-02-28-panll-interop-telemetry.md) -### VQL language +### VCL language -- [docs/getting-started.adoc](getting-started.adoc) — VQL getting started -- [docs/VCL-SPEC.adoc](VCL-SPEC.adoc) — Full VQL specification +- [docs/getting-started.adoc](getting-started.adoc) — VCL getting started +- [docs/VCL-SPEC.adoc](VCL-SPEC.adoc) — Full VCL specification - [docs/vcl-grammar.ebnf](vcl-grammar.ebnf) — ISO/IEC 14977 EBNF grammar - [docs/vcl-architecture.adoc](vcl-architecture.adoc) — Parser / executor architecture - [docs/vcl-type-system.adoc](vcl-type-system.adoc) — VCL-DT dependent type system - [docs/vcl-formal-semantics.adoc](vcl-formal-semantics.adoc) — Formal semantics - [docs/vcl-examples.adoc](vcl-examples.adoc) — Worked examples -- [docs/vcl-vs-vcl-dt.adoc](vcl-vs-vcl-dt.adoc) — VQL vs VCL-DT comparison -- [docs/vcl-vs-sql.adoc](vcl-vs-sql.adoc) — VQL vs SQL comparison +- [docs/vcl-vs-vcl-dt.adoc](vcl-vs-vcl-dt.adoc) — VCL vs VCL-DT comparison +- [docs/vcl-vs-sql.adoc](vcl-vs-sql.adoc) — VCL vs SQL comparison - [docs/rescript-registry-types.adoc](rescript-registry-types.adoc) — ReScript registry types ### Operational concerns @@ -156,16 +156,16 @@ Under [`.github/workflows/`](../.github/workflows/): | Path | Language | Purpose | |---|---|---| | `rust-core/` | Rust | Core database engine (8 modality stores + octad + drift + normalizer + api + planner) | -| `elixir-orchestration/` | Elixir | OTP orchestration layer (DriftMonitor, EntityServer, VQLExecutor, VQLBridge, SchemaRegistry, federation adapters) | -| `src/` | ReScript | VQL parser, type checker, federation registry | -| `playground/` | ReScript + HTML | VQL Playground web UI | +| `elixir-orchestration/` | Elixir | OTP orchestration layer (DriftMonitor, EntityServer, VCLExecutor, VCLBridge, SchemaRegistry, federation adapters) | +| `src/` | ReScript | VCL parser, type checker, federation registry | +| `playground/` | ReScript + HTML | VCL Playground web UI | | `connectors/` | Multi | Federation adapters, client SDKs (Rust, Elixir, ReScript, Julia, Zig), test infrastructure. Other BEAM languages (Gleam, Erlang) access via the SNIFs WASM bridge — see `hyperpolymath/snifs`. | | `debugger/` | Idris2 + Rust | ABI/FFI debugger | | `ffi/zig/` | Zig | Zig FFI | | `v-api-gateway/` | V | V-language API gateway | | `fuzz/`, `rust-core/fuzz/` | Rust | Fuzz harnesses (libFuzzer via cargo-fuzz) | | `benches/` | Rust | Criterion benchmarks (all 8 modalities + cross-modal + octad + drift) | -| `elixir-orchestration/bench/` | Elixir | Benchee benchmark scripts (DriftMonitor, QueryRouter, VQLExecutor, VQLBridge, SchemaRegistry) | +| `elixir-orchestration/bench/` | Elixir | Benchee benchmark scripts (DriftMonitor, QueryRouter, VCLExecutor, VCLBridge, SchemaRegistry) | ## Container & deployment diff --git a/docs/VCL-SPEC.adoc b/docs/VCL-SPEC.adoc index 4da4caf..5249ec9 100644 --- a/docs/VCL-SPEC.adoc +++ b/docs/VCL-SPEC.adoc @@ -517,16 +517,16 @@ In slipstream mode, the type checker validates: .ReScript type representation [source,rescript] ---- -type rec vqlType = +type rec vclType = | Primitive(primitiveType) - | ArrayType(vqlType) + | ArrayType(vclType) | ModalityType(modalityType) | OctadType(array) | QueryResultType(queryResultInfo) | ProofType(proofKind, string) | ProvedResultType(queryResultInfo, proofKind, string) - | PiType(string, vqlType, vqlType) - | SigmaType(string, vqlType, vqlType) + | PiType(string, vclType, vclType) + | SigmaType(string, vclType, vclType) | UnitType | NeverType ---- @@ -696,7 +696,7 @@ There are three kinds of select items: Select entire modalities by name: -[source,vql] +[source,vcl] ---- SELECT GRAPH -- single modality SELECT GRAPH, VECTOR, DOCUMENT -- multiple modalities @@ -714,14 +714,14 @@ SELECT DOCUMENT(title, abstract) -- document fields only Select specific fields from a modality using dot notation (`MODALITY.field`): -[source,vql] +[source,vcl] ---- SELECT DOCUMENT.name, DOCUMENT.severity ---- Field projections may be mixed with full modality selections: -[source,vql] +[source,vcl] ---- SELECT GRAPH, DOCUMENT.name, DOCUMENT.severity ---- @@ -766,7 +766,7 @@ SELECT SUM(DOCUMENT.title) -- ERROR: AggregateTypeMismatch ---- .Example: aggregates -[source,vql] +[source,vcl] ---- SELECT COUNT(*), AVG(DOCUMENT.severity), MAX(DOCUMENT.severity) FROM FEDERATION /scans/* @@ -788,7 +788,7 @@ source_spec = octad_source | federation_source | store_source ; Query a specific octad by UUID: -[source,vql] +[source,vcl] ---- FROM HEXAD 550e8400-e29b-41d4-a716-446655440000 ---- @@ -799,7 +799,7 @@ Type: stem:[\text{Octad}(\text{UUID})] Query across multiple VeriSimDB instances matching a pattern: -[source,vql] +[source,vcl] ---- FROM FEDERATION /universities/* -- glob pattern FROM FEDERATION /universities/* WITH DRIFT STRICT -- with drift policy @@ -829,7 +829,7 @@ Drift policies control how inter-node inconsistency is handled: |=== .Example: federation with drift policies -[source,vql] +[source,vcl] ---- -- Strict: fail on any drift SELECT * @@ -861,7 +861,7 @@ LIMIT 10 Query a specific modality store directly, bypassing federation: -[source,vql] +[source,vcl] ---- FROM STORE milvus-us-east-1 -- direct store access FROM STORE oxigraph-node-1 -- specific graph store @@ -914,7 +914,7 @@ Path quantifiers control traversal depth: * `{m,n}` — Between _m_ and _n_ hops .Examples: graph conditions -[source,vql] +[source,vcl] ---- -- Direct citation WHERE (h)-[:CITES]->(target) @@ -951,7 +951,7 @@ metric_type = 'USING' , ('COSINE' | 'EUCLIDEAN' | 'DOT_PRODUCT') ; ---- .Examples: vector conditions -[source,vql] +[source,vcl] ---- -- Approximate nearest neighbor with threshold WHERE h.embedding SIMILAR TO [0.12, 0.45, 0.78, ...] WITHIN 0.8 @@ -986,7 +986,7 @@ tensor_op = '==' | '>' | '<' | '>=' | '<=' | 'SHAPE' | 'RANK' ; ---- .Examples: tensor conditions -[source,vql] +[source,vcl] ---- -- Shape filtering WHERE tensor.data SHAPE == [256, 256, 3] @@ -1013,7 +1013,7 @@ param_list = identifier , '=' , literal , { ',' , identifier , '=' , literal } ; ---- .Examples: semantic conditions -[source,vql] +[source,vcl] ---- -- Contract satisfaction WHERE SATISFIES AccessControlContract(role=researcher, institution=MIT) @@ -1044,7 +1044,7 @@ document_condition = 'FULLTEXT' , 'CONTAINS' , string_literal ---- .Examples: document conditions -[source,vql] +[source,vcl] ---- -- Full-text search WHERE FULLTEXT CONTAINS "quantum computing" @@ -1077,7 +1077,7 @@ temporal_condition = 'AS' , 'OF' , timestamp ---- .Examples: temporal conditions -[source,vql] +[source,vcl] ---- -- Point-in-time query WHERE AS OF 2024-06-15T10:30:00Z @@ -1116,7 +1116,7 @@ Compare field values from different modalities on the same octad: cross_modal_field_compare = field_ref , comparison_op , field_ref ; ---- -[source,vql] +[source,vcl] ---- WHERE DOCUMENT.severity > GRAPH.centrality ---- @@ -1137,7 +1137,7 @@ Measure representation drift between two modalities: drift_condition = 'DRIFT' , '(' , modality , ',' , modality , ')' , comparison_op , float ; ---- -[source,vql] +[source,vcl] ---- WHERE DRIFT(VECTOR, DOCUMENT) > 0.3 ---- @@ -1156,7 +1156,7 @@ consistency_condition = 'CONSISTENT' , '(' , modality , ',' , modality , ')' , metric_name = 'COSINE' | 'EUCLIDEAN' | 'DOT_PRODUCT' | 'JACCARD' ; ---- -[source,vql] +[source,vcl] ---- WHERE CONSISTENT(VECTOR, SEMANTIC) USING COSINE ---- @@ -1172,7 +1172,7 @@ exists_condition = modality_name , 'EXISTS' ; not_exists_condition = modality_name , 'NOT' , 'EXISTS' ; ---- -[source,vql] +[source,vcl] ---- -- Octads with vectors but without tensors WHERE VECTOR EXISTS @@ -1180,7 +1180,7 @@ WHERE VECTOR EXISTS ---- .Combined example: cross-modal with standard conditions -[source,vql] +[source,vcl] ---- SELECT GRAPH, VECTOR, DOCUMENT FROM FEDERATION /research-db/* WITH DRIFT REPAIR @@ -1210,7 +1210,7 @@ proof_params = 'WITH' , param_list ; Multiple proofs are composed with `AND` — all must pass before results are returned. .Examples: proof clause -[source,vql] +[source,vcl] ---- -- Single proof PROOF EXISTENCE(ExistenceContract) @@ -1250,7 +1250,7 @@ having_clause = 'HAVING' , condition ; `HAVING` requires `GROUP BY` — using HAVING without GROUP BY produces `HavingWithoutGroupBy` error. .Example: grouping with aggregate filter -[source,vql] +[source,vcl] ---- SELECT DOCUMENT.name, COUNT(*), AVG(DOCUMENT.severity) FROM FEDERATION /universities/* @@ -1276,7 +1276,7 @@ sort_direction = 'ASC' | 'DESC' ; Default sort direction is `ASC` when omitted. .Example: multi-field sort -[source,vql] +[source,vcl] ---- SELECT DOCUMENT.name, DOCUMENT.severity FROM FEDERATION /archives/* @@ -1299,7 +1299,7 @@ offset_clause = 'OFFSET' , integer ; ---- .Example: pagination -[source,vql] +[source,vcl] ---- SELECT DOCUMENT FROM FEDERATION /archives/* @@ -1362,7 +1362,7 @@ Each modality data type has its own syntax: |=== .Examples: INSERT -[source,vql] +[source,vcl] ---- -- Basic insert with document and vector INSERT HEXAD WITH @@ -1399,7 +1399,7 @@ set_assignment = field_ref , '=' , literal ; ---- .Examples: UPDATE -[source,vql] +[source,vcl] ---- -- Simple field update UPDATE HEXAD 550e8400-e29b-41d4-a716-446655440000 @@ -1427,7 +1427,7 @@ delete_mutation = 'DELETE' , 'HEXAD' , uuid , [proof_clause] ; ---- .Examples: DELETE -[source,vql] +[source,vcl] ---- -- Simple deletion DELETE HEXAD 550e8400-e29b-41d4-a716-446655440000 @@ -1557,7 +1557,7 @@ The proof system is the core differentiator between VCL and traditional query la Multiple proofs are composed with `AND`. Composition is **conjunctive** — all proofs must hold simultaneously: -[source,vql] +[source,vcl] ---- PROOF ACCESS(InstitutionalAccessContract) AND PROVENANCE(ClinicalTrialContract) @@ -1629,7 +1629,7 @@ The execution pipeline flows through three layers: .Execution pipeline ---- VCL String - → Parser (ReScript VQLParser.res / Elixir vql_bridge.ex fallback) + → Parser (ReScript VQLParser.res / Elixir vcl_bridge.ex fallback) → AST → Type Checker (VQLBidir.res) → Query Plan Generator (VQLExplain.res) @@ -1657,7 +1657,7 @@ The executor separates conditions into two categories: VCL does not have explicit JOIN syntax. Instead, cross-modal querying is implicit — every octad is already the join of all its modalities. When you write: -[source,vql] +[source,vcl] ---- SELECT GRAPH, VECTOR, DOCUMENT FROM HEXAD 550e8400-e29b-41d4-a716-446655440000 @@ -1678,7 +1678,7 @@ The executor: Prefix a query with `EXPLAIN` to see the execution plan without executing: -[source,vql] +[source,vcl] ---- EXPLAIN SELECT GRAPH, VECTOR, DOCUMENT FROM FEDERATION /research-db/* @@ -1749,23 +1749,23 @@ VCL provides structured error responses with error codes, messages, and recovery | Category | Error Code Pattern | Recoverable? | Parse errors -| `VQL_PARSE_ERROR` +| `VCL_PARSE_ERROR` | No | Type errors -| `VQL_TYPE_ERROR` +| `VCL_TYPE_ERROR` | No | Runtime errors -| `VQL_STORE_UNAVAILABLE`, `VQL_QUERY_TIMEOUT`, `VQL_DRIFT_DETECTED`, `VQL_PERMISSION_DENIED`, `VQL_RESOURCE_EXHAUSTED`, `VQL_RUNTIME_ERROR` +| `VCL_STORE_UNAVAILABLE`, `VCL_QUERY_TIMEOUT`, `VCL_DRIFT_DETECTED`, `VCL_PERMISSION_DENIED`, `VCL_RESOURCE_EXHAUSTED`, `VCL_RUNTIME_ERROR` | Varies | Modality errors -| `VQL_GRAPH_ERROR`, `VQL_VECTOR_ERROR`, `VQL_TENSOR_ERROR`, `VQL_SEMANTIC_ERROR`, `VQL_DOCUMENT_ERROR`, `VQL_TEMPORAL_ERROR` +| `VCL_GRAPH_ERROR`, `VCL_VECTOR_ERROR`, `VCL_TENSOR_ERROR`, `VCL_SEMANTIC_ERROR`, `VCL_DOCUMENT_ERROR`, `VCL_TEMPORAL_ERROR` | No | Federation errors -| `VQL_FEDERATION_ERROR` +| `VCL_FEDERATION_ERROR` | `PartialResults` and `RemoteStoreUnreachable` are recoverable |=== @@ -1774,7 +1774,7 @@ VCL provides structured error responses with error codes, messages, and recovery [source,json] ---- { - "error_code": "VQL_PARSE_ERROR", + "error_code": "VCL_PARSE_ERROR", "message": "Parse Error at 3:27-3:27: Expected ']->', found end of input", "recoverable": false } @@ -1865,7 +1865,7 @@ This section provides an honest assessment of what is implemented, partially imp | VCL Parser (Elixir fallback) | 2.0 -| Built into `vql_bridge.ex` (672 lines). No external Deno/Node dependency needed. +| Built into `vcl_bridge.ex` (672 lines). No external Deno/Node dependency needed. | Bidirectional Type Checker | 2.0 @@ -1885,7 +1885,7 @@ This section provides an honest assessment of what is implemented, partially imp | Query Executor | 2.0 -| `vql_executor.ex` (1162 lines). Full pipeline: parse, type check, plan, route, aggregate. +| `vcl_executor.ex` (1162 lines). Full pipeline: parse, type check, plan, route, aggregate. | Query Router | 2.0 @@ -2354,52 +2354,52 @@ Complete alphabetical list of all 70 reserved keywords. Keywords are case-insens |=== | Code | Description -| `VQL_PARSE_ERROR` +| `VCL_PARSE_ERROR` | Syntax error during parsing -| `VQL_TYPE_ERROR` +| `VCL_TYPE_ERROR` | Type system violation -| `VQL_STORE_UNAVAILABLE` +| `VCL_STORE_UNAVAILABLE` | A modality store is unreachable -| `VQL_QUERY_TIMEOUT` +| `VCL_QUERY_TIMEOUT` | Query exceeded time limit -| `VQL_DRIFT_DETECTED` +| `VCL_DRIFT_DETECTED` | Cross-node inconsistency with STRICT policy -| `VQL_PERMISSION_DENIED` +| `VCL_PERMISSION_DENIED` | Insufficient access rights -| `VQL_RESOURCE_EXHAUSTED` +| `VCL_RESOURCE_EXHAUSTED` | System resource limit reached -| `VQL_RUNTIME_ERROR` +| `VCL_RUNTIME_ERROR` | General runtime error -| `VQL_GRAPH_ERROR` +| `VCL_GRAPH_ERROR` | Graph-specific error (Oxigraph) -| `VQL_VECTOR_ERROR` +| `VCL_VECTOR_ERROR` | Vector-specific error (HNSW) -| `VQL_TENSOR_ERROR` +| `VCL_TENSOR_ERROR` | Tensor-specific error (Burn/ndarray) -| `VQL_SEMANTIC_ERROR` +| `VCL_SEMANTIC_ERROR` | Semantic-specific error (ZKP/CBOR) -| `VQL_DOCUMENT_ERROR` +| `VCL_DOCUMENT_ERROR` | Document-specific error (Tantivy) -| `VQL_TEMPORAL_ERROR` +| `VCL_TEMPORAL_ERROR` | Temporal-specific error (Merkle trees) -| `VQL_FEDERATION_ERROR` +| `VCL_FEDERATION_ERROR` | Federation-specific error -| `VQL_MULTIPLE_ERRORS` +| `VCL_MULTIPLE_ERRORS` | Multiple errors occurred |=== @@ -2769,10 +2769,10 @@ This specification is the authoritative reference for VCL language behaviour. Th | `elixir-orchestration/lib/verisim/query/query_router.ex` | Elixir query router GenServer (187 lines). Routes by modality. -| `elixir-orchestration/lib/verisim/query/vql_bridge.ex` +| `elixir-orchestration/lib/verisim/query/vcl_bridge.ex` | Elixir ↔ ReScript bridge (672 lines). Built-in fallback parser. -| `elixir-orchestration/lib/verisim/query/vql_executor.ex` +| `elixir-orchestration/lib/verisim/query/vcl_executor.ex` | Full VCL executor (1162 lines). Parse → type check → plan → route → aggregate. |=== @@ -2797,7 +2797,7 @@ This specification resolves all three inconsistencies in favour of the implement VCL-dt++ extends VCL v3.0 with six optional clauses that provide maximal type-theoretic strictness. These extensions are consumed by the **Typell verification kernel** (the formal verification substrate for PanLL) and are specified normatively in the grammar delta file: -* link:../../typeql-experimental/docs/vql-dtpp-grammar.ebnf[`vql-dtpp-grammar.ebnf`] — EBNF grammar delta (199 lines) +* link:../../typeql-experimental/docs/vcl-dtpp-grammar.ebnf[`vcl-dtpp-grammar.ebnf`] — EBNF grammar delta (199 lines) All six clauses are optional and composable in any combination. They append after the standard query structure with no keyword conflicts against VCL v3.0's 60+ reserved keywords. @@ -3003,7 +3003,7 @@ VCL-dt++ queries are verified by the Typell kernel via JSON-RPC: [source] ---- -typell.check(query, "vql-dt++") → TypeResult +typell.check(query, "vcl-dt++") → TypeResult ---- The kernel returns: types, proof obligations, linear tracking, session protocol compliance, effect analysis, modal scope verification, and proof certificates. See the link:../../typell/docs/design/DESIGN-2026-03-01-typell-vision.md[Typell Vision Document] for the full verification protocol specification. diff --git a/docs/adoption-strategy.adoc b/docs/adoption-strategy.adoc index 0ea65f9..82545a8 100644 --- a/docs/adoption-strategy.adoc +++ b/docs/adoption-strategy.adoc @@ -387,8 +387,8 @@ Any external adopter should know: | VCL-DT proofs incomplete | PROOF clauses parse but don't generate verifiable certificates yet. Lean type checker integration planned Q2 2026. -| No SQL dialect | VQL is intentionally not SQL. Users wanting familiar syntax - need to learn VQL (comprehensive docs provided). +| No SQL dialect | VCL is intentionally not SQL. Users wanting familiar syntax + need to learn VCL (comprehensive docs provided). | Query planner is basic | Queries using all 8 modalities may not be optimally planned. Single-modality queries perform well. diff --git a/docs/architecture/topology.md b/docs/architecture/topology.md index 5fad656..fad7209 100644 --- a/docs/architecture/topology.md +++ b/docs/architecture/topology.md @@ -21,7 +21,7 @@ │ │ octad) │ │ Schema Registry │ │ │ └──────────┘ └──────────────────┘ │ │ ┌──────────┐ ┌──────────────────┐ │ - │ │ Query │ │ VQL Parser │ │ + │ │ Query │ │ VCL Parser │ │ │ │ Router │ │ (ReScript) │ │ │ └──────────┘ └──────────────────┘ │ └────────────────┬────────────────────┘ @@ -71,7 +71,7 @@ | verisim-normalizer | `██████░░░░` 60% | Active | | verisim-api | `████████░░` 80% | Active | | Elixir OTP layer | `███████░░░` 70% | Active | -| VQL parser | `█████████░` 95% | Active | +| VCL parser | `█████████░` 95% | Active | | VCL-DT (Lean checker) | `░░░░░░░░░░` 0% | Not started | | Idris2 ABI | `████░░░░░░` 40% | In progress | | Zig FFI | `████░░░░░░` 40% | In progress | diff --git a/docs/backwards-compatibility.adoc b/docs/backwards-compatibility.adoc index d24d3c6..d7619f8 100644 --- a/docs/backwards-compatibility.adoc +++ b/docs/backwards-compatibility.adoc @@ -1,30 +1,30 @@ // SPDX-License-Identifier: MPL-2.0 -= VQL Backwards Compatibility Strategy += VCL Backwards Compatibility Strategy :toc: :toc-placement!: -Strategy for maintaining backwards compatibility across VQL versions, schema evolution, and API changes. +Strategy for maintaining backwards compatibility across VCL versions, schema evolution, and API changes. toc::[] == Overview -VeriSimDB follows **semantic versioning** (SemVer) for VQL and API compatibility: +VeriSimDB follows **semantic versioning** (SemVer) for VCL and API compatibility: - **Major version** (1.x.x → 2.x.x): Breaking changes allowed - **Minor version** (1.1.x → 1.2.x): New features, backwards compatible - **Patch version** (1.1.1 → 1.1.2): Bug fixes only, backwards compatible -Current VQL version: **1.0.0** +Current VCL version: **1.0.0** == Compatibility Guarantees === What We Guarantee -**Query Syntax (VQL):** +**Query Syntax (VCL):** -- Valid VQL 1.x queries will parse and execute correctly in all 1.x releases +- Valid VCL 1.x queries will parse and execute correctly in all 1.x releases - New keywords/operators are additive (won't conflict with existing identifiers) - Deprecations announced at least 2 minor versions before removal @@ -59,11 +59,11 @@ Current VQL version: **1.0.0** == Versioning Strategy -=== VQL Syntax Versions +=== VCL Syntax Versions Each query can optionally specify a version: -```vql +```vcl VERSION 1.0; FROM verisim:semantic @@ -123,7 +123,7 @@ LIMIT 10; **Safe to add in 1.x.x releases:** -- New VQL keywords (if not previously valid identifiers) +- New VCL keywords (if not previously valid identifiers) - New modality types - New query operators (`INTERSECT`, `UNION ALL`) - New API endpoints @@ -133,7 +133,7 @@ LIMIT 10; **Example: Adding `INTERSECT` operator** -```vql +```vcl -- Version 1.2.0 introduces INTERSECT -- Old queries (1.0.0) continue to work @@ -148,7 +148,7 @@ INTERSECT **Requires 2.0.0:** -- Removing VQL keywords +- Removing VCL keywords - Changing query semantics (e.g., `LIMIT` behavior) - Removing API endpoints - Removing response fields @@ -156,7 +156,7 @@ INTERSECT **Example: Removing deprecated `USING` clause** -```vql +```vcl -- Version 1.0.0 syntax (deprecated in 1.2.0) FROM verisim:graph USING CONTRACT CitationContract @@ -189,7 +189,7 @@ WHERE octad.types INCLUDES "Paper"; === Deprecation Warnings -**VQL Parser:** +**VCL Parser:** ```rescript // VQLParser.res @@ -221,7 +221,7 @@ Link: ; rel="sunset" ```elixir # config.exs config :verisim, - vql_version: "1.0.0", # Pin to specific version + vcl_version: "1.0.0", # Pin to specific version api_version: "v1" ``` @@ -240,7 +240,7 @@ config :verisim, ```yaml # Dockerfile -ENV VQL_VERSION="1.x" # Auto-upgrade within major version +ENV VCL_VERSION="1.x" # Auto-upgrade within major version ``` **Trade-offs:** @@ -260,7 +260,7 @@ ENV VQL_VERSION="1.x" # Auto-upgrade within major version ``` 2. **Update queries gradually:** - ```vql + ```vcl -- Old query (1.0.0) FROM verisim:graph USING CONTRACT CitationContract @@ -275,8 +275,8 @@ ENV VQL_VERSION="1.x" # Auto-upgrade within major version 3. **Test both versions side-by-side:** ```elixir - old_result = VQL.parse_and_execute(old_query, version: "1.0.0") - new_result = VQL.parse_and_execute(new_query, version: "1.2.0") + old_result = VCL.parse_and_execute(old_query, version: "1.0.0") + new_result = VCL.parse_and_execute(new_query, version: "1.2.0") assert old_result.data == new_result.data ``` @@ -292,14 +292,14 @@ ENV VQL_VERSION="1.x" # Auto-upgrade within major version === Version Compatibility Matrix -**Test all VQL versions against current parser:** +**Test all VCL versions against current parser:** ```elixir -# test/vql_compatibility_test.exs -defmodule VeriSim.VQLCompatibilityTest do +# test/vcl_compatibility_test.exs +defmodule VeriSim.VCLCompatibilityTest do use ExUnit.Case - @vql_versions ["1.0.0", "1.1.0", "1.2.0"] + @vcl_versions ["1.0.0", "1.1.0", "1.2.0"] @test_queries [ # Basic SELECT """ @@ -325,7 +325,7 @@ defmodule VeriSim.VQLCompatibilityTest do test "parse all versions" do for query <- @test_queries do - assert {:ok, _ast} = VQL.parse(query) + assert {:ok, _ast} = VCL.parse(query) end end @@ -335,9 +335,9 @@ defmodule VeriSim.VQLCompatibilityTest do FROM verisim:graph LIMIT 10; """ - for version <- @vql_versions do - config = %{vql_version: version} - assert {:ok, _result} = VQL.execute(query_1_0, config) + for version <- @vcl_versions do + config = %{vcl_version: version} + assert {:ok, _result} = VCL.execute(query_1_0, config) end end end @@ -377,10 +377,10 @@ defmodule VeriSim.UpgradeTest do WHERE octad.id = @id; """ - Application.put_env(:verisim, :vql_version, "2.0.0") + Application.put_env(:verisim, :vcl_version, "2.0.0") assert {:error, {:deprecated_syntax, "USING clause removed in 2.0.0"}} = - VQL.parse(deprecated_query) + VCL.parse(deprecated_query) end end ``` @@ -520,7 +520,7 @@ X-VQL-Version-Supported: 1.0.0, 1.1.0 **Version compatibility rules:** -1. **VQL version:** Query must use syntax supported by remote store +1. **VCL version:** Query must use syntax supported by remote store - If remote supports `[1.0.0, 1.1.0]` and query uses `1.2.0` → error - Client downgrades query syntax if possible @@ -536,7 +536,7 @@ X-VQL-Version-Supported: 1.0.0, 1.1.0 ```elixir def query_federation(stores, query) do # Check if all stores support required features - required_features = VQL.detect_features(query) + required_features = VCL.detect_features(query) # [:zkp_verification, :tensor_modality, :drift_detection] compatible_stores = Enum.filter(stores, fn store -> @@ -560,7 +560,7 @@ GET /api/v1/capabilities HTTP/1.1 Response: { "verisimdb_version": "1.2.0", - "vql_versions": ["1.0.0", "1.1.0", "1.2.0"], + "vcl_versions": ["1.0.0", "1.1.0", "1.2.0"], "modalities": ["graph", "vector", "semantic", "document", "temporal"], "features": [ "zkp_verification", @@ -605,14 +605,14 @@ verisim-client = "1.2.0" # Client version matches server minor version ```rust // Stable API pub trait VeriSimClient { - fn query(&self, vql: &str) -> Result; + fn query(&self, vcl: &str) -> Result; fn create_octad(&self, octad: Octad) -> Result; fn get_octad(&self, id: OctadId) -> Result; } // Adding new methods is OK (minor version bump) pub trait VeriSimClient { - fn query(&self, vql: &str) -> Result; + fn query(&self, vcl: &str) -> Result; fn create_octad(&self, octad: Octad) -> Result; fn get_octad(&self, id: OctadId) -> Result; @@ -630,7 +630,7 @@ pub trait VeriSimClient { - [ ] Deprecation warnings added for features planned for removal - [ ] Documentation updated with new features - [ ] `CHANGELOG.md` updated with new features -- [ ] No breaking changes to API, VQL syntax, or data formats +- [ ] No breaking changes to API, VCL syntax, or data formats - [ ] Federation compatibility tested with previous minor version === Before Releasing Major Version (1.x.x → 2.x.x) @@ -652,7 +652,7 @@ VeriSimDB maintains backwards compatibility through: 2. **Deprecation timeline** - At least 6 months notice before removal 3. **Format versioning** - Auto-migration for data formats 4. **API versioning** - Multiple API versions supported concurrently -5. **VQL versioning** - Explicit version markers in queries +5. **VCL versioning** - Explicit version markers in queries 6. **Feature detection** - Capability negotiation for federation 7. **Comprehensive testing** - Compatibility test suite diff --git a/docs/business/business-case.adoc b/docs/business/business-case.adoc index 9739117..f7bfffb 100644 --- a/docs/business/business-case.adoc +++ b/docs/business/business-case.adoc @@ -135,7 +135,7 @@ When drift exceeds configurable thresholds, VeriSimDB can: === Formal Verification: VCL-DT -VeriSimDB's query language, VQL (Verisimilitude Query Language), includes an +VeriSimDB's query language, VCL (Verisimilitude Query Language), includes an optional dependent-type layer (VCL-DT) that provides *compile-time proofs* of query correctness. This means: @@ -346,7 +346,7 @@ dynamics are: | *Community Edition (MPL-2.0)* | Full-featured VeriSimDB with all 8 modalities, drift detection, - self-normalisation, VQL, and federation. Free, open source under MPL-2.0. + self-normalisation, VCL, and federation. Free, open source under MPL-2.0. | *Commercial Support License* | Enterprise SLA (99.9% uptime guarantee), priority security patches (24-hour @@ -374,7 +374,7 @@ The community edition is intentionally full-featured. Revenue comes from the organisation size and SLA level 2. *Deployment consulting* -- architecture review, migration planning, performance tuning, integration with existing infrastructure -3. *Training and certification* -- VQL/VCL-DT training for development teams +3. *Training and certification* -- VCL/VCL-DT training for development teams 4. *OEM licensing* -- for vendors embedding VeriSimDB in their products == Financial Projections @@ -520,7 +520,7 @@ profitability faster and at higher margins. | VCL-DT complexity deters adoption | Developers find dependent-type proofs intimidating -| VQL (without DT) is the default; VCL-DT is opt-in for teams that want formal +| VCL (without DT) is the default; VCL-DT is opt-in for teams that want formal guarantees. Progressive disclosure: start simple, add proofs when ready. | Federation reliability across heterogeneous backends diff --git a/docs/business/marketing/feature-comparison.adoc b/docs/business/marketing/feature-comparison.adoc index 478342d..859c054 100644 --- a/docs/business/marketing/feature-comparison.adoc +++ b/docs/business/marketing/feature-comparison.adoc @@ -152,7 +152,7 @@ Legend: {check} = Full support | {half} = Partial/limited | {cross} = Not suppor 7+h| *Query Language* | Purpose-built query language -| VQL +| VCL | Cypher | N/A (API) | GraphQL diff --git a/docs/business/marketing/one-pager.adoc b/docs/business/marketing/one-pager.adoc index 2a78a96..f83f9c4 100644 --- a/docs/business/marketing/one-pager.adoc +++ b/docs/business/marketing/one-pager.adoc @@ -36,7 +36,7 @@ cross-modal consistency monitoring. representations diverge, before downstream systems consume inconsistent data * *Self-normalisation* -- Automatic reconciliation of drifted data using configurable resolution strategies (alert, quarantine, or repair) -* *VQL query language* -- Purpose-built query language for cross-modal operations +* *VCL query language* -- Purpose-built query language for cross-modal operations with optional dependent-type proofs (VCL-DT) for compile-time query verification * *Federation* -- Bring drift detection to existing infrastructure by federating across PostgreSQL, ArangoDB, Elasticsearch, Neo4j, and more @@ -60,7 +60,7 @@ cross-modal consistency monitoring. | *Community (Free)* | Full VeriSimDB with all 8 modalities, drift detection, self-normalisation, - VQL, and federation. MPL-2.0 license. + VCL, and federation. MPL-2.0 license. | *Commercial Support* | Enterprise SLA (99.9%), priority security patches, dedicated support channel, diff --git a/docs/business/marketing/pitch-deck-outline.adoc b/docs/business/marketing/pitch-deck-outline.adoc index 85cba59..d1251a5 100644 --- a/docs/business/marketing/pitch-deck-outline.adoc +++ b/docs/business/marketing/pitch-deck-outline.adoc @@ -110,7 +110,7 @@ representations that together provide a complete picture of each entity. ---- ┌─────────────────────────┐ - │ VQL Engine │ + │ VCL Engine │ │ (Query + VCL-DT) │ └────────────┬────────────┘ │ @@ -142,7 +142,7 @@ representations that together provide a complete picture of each entity. === Speaker Notes -Three layers: the VQL query engine parses and type-checks queries; the drift +Three layers: the VCL query engine parses and type-checks queries; the drift detection engine continuously monitors coherence across modalities; the storage layer handles the octad per entity. Federation allows VeriSimDB to bring drift detection to existing databases without data migration. Rust provides performance, @@ -173,7 +173,7 @@ pinecone.query(vector=[0.23, 0.87, ...], top_k=10) [source] ---- --- VQL: Query across modalities with coherence check +-- VCL: Query across modalities with coherence check SELECT entity, coherence_score, drifted_modalities FROM entities WHERE entity.id = "jane-doe" @@ -191,7 +191,7 @@ WHERE entity.id = "jane-doe" Walk through both examples. In the "before" scenario, a developer queries two separate databases and has no way to know if the results are consistent. In the -"after" scenario, VeriSimDB's VQL query spans modalities and includes the +"after" scenario, VeriSimDB's VCL query spans modalities and includes the coherence score directly in the result set. When the score drops below the configured threshold, self-normalisation is triggered automatically. The developer does not need to write reconciliation logic. @@ -216,7 +216,7 @@ does not need to write reconciliation logic. | *ReScript* -- ML-family type system compiling to JavaScript | Query language -| *VQL* -- Purpose-built for cross-modal operations +| *VCL* -- Purpose-built for cross-modal operations | Formal verification | *VCL-DT* -- Dependent-type proofs of query correctness @@ -235,7 +235,7 @@ does not need to write reconciliation logic. Emphasise the engineering quality. Rust + Elixir is an increasingly popular combination for data infrastructure (used by Discord, Fly.io, and others). The test suite is comprehensive and runs in CI on every commit. VCL-DT's dependent -types are optional -- teams can start with plain VQL and adopt formal verification +types are optional -- teams can start with plain VCL and adopt formal verification incrementally. == Slide 7: Market Opportunity @@ -293,7 +293,7 @@ the category rather than compete within an established one. ┌─────────────────────────────────────────────┐ │ Community Edition (MPL-2.0) │ │ All 8 modalities, drift detection, │ -│ self-normalisation, VQL, federation │ +│ self-normalisation, VCL, federation │ │ FREE — forever │ ├─────────────────────────────────────────────┤ │ Commercial Support License │ @@ -364,7 +364,7 @@ coherence from the ground up. * *662 tests* (510 Rust + 152 Elixir), *0 failures* * *8 modalities* fully architected and implemented -* *VQL grammar* specified in EBNF with formal semantics +* *VCL grammar* specified in EBNF with formal semantics * *VCL-DT* dependent-type layer with Idris2 proofs * *Federation connectors* for PostgreSQL, ArangoDB, Elasticsearch * *Comprehensive documentation:* Architecture, deployment, query language, diff --git a/docs/business/marketing/use-cases.adoc b/docs/business/marketing/use-cases.adoc index cc2a82b..6cd6c83 100644 --- a/docs/business/marketing/use-cases.adoc +++ b/docs/business/marketing/use-cases.adoc @@ -59,7 +59,7 @@ The system can then: re-embedded * *Self-normalise* by triggering an automatic re-embedding pipeline -=== Example VQL Query +=== Example VCL Query [source] ---- @@ -117,7 +117,7 @@ consistency window. The provenance modality provides an immutable audit trail of every change, who made it, and from what source -- satisfying regulatory traceability requirements. -=== Example VQL Query +=== Example VCL Query [source] ---- @@ -181,7 +181,7 @@ Federation allows VeriSimDB to connect to the existing core banking, fraud detection, and compliance systems, bringing cross-modal consistency checking to current infrastructure without data migration. -=== Example VQL Query +=== Example VCL Query [source] ---- @@ -248,7 +248,7 @@ The spatial modality tracks goods in real time and cross-checks against complian documents. The temporal modality provides a complete timeline of every change. The provenance modality establishes an immutable chain of custody. -=== Example VQL Query +=== Example VCL Query [source] ---- @@ -315,7 +315,7 @@ Federation allows VeriSimDB to connect to existing collection management systems (MuseumPlus, TMS, ArchivesSpace) and bring cross-modal consistency checking to existing catalogues without requiring data migration. -=== Example VQL Query +=== Example VCL Query [source] ---- @@ -378,7 +378,7 @@ the tensor (corrected data) and provenance (updated methodology). This does not automatically retract papers -- it surfaces the inconsistency so that researchers, journal editors, and data stewards can take appropriate action. -=== Example VQL Query +=== Example VCL Query [source] ---- @@ -446,7 +446,7 @@ been updated to reflect the new behaviour. Federation allows VeriSimDB to connect to existing SIEM, SOAR, and TIP platforms, bringing cross-modal consistency to current CTI infrastructure. -=== Example VQL Query +=== Example VCL Query [source] ---- diff --git a/docs/business/pr/faq.adoc b/docs/business/pr/faq.adoc index f4c5f51..db9640a 100644 --- a/docs/business/pr/faq.adoc +++ b/docs/business/pr/faq.adoc @@ -170,20 +170,20 @@ commercial use, while VeriSimDB is released under MPL-2.0, an OSI-approved licen * *Zig:* FFI (Foreign Function Interface) implementation for C-compatible bindings. -=== What is VQL? +=== What is VCL? -VQL (Verisimilitude Query Language) is VeriSimDB's purpose-built query language -for cross-modal operations. VQL allows queries to span multiple modalities in +VCL (Verisimilitude Query Language) is VeriSimDB's purpose-built query language +for cross-modal operations. VCL allows queries to span multiple modalities in a single expression, include coherence scores in result sets, and filter by drift thresholds. -VQL is designed to be familiar to SQL users while supporting modality-specific +VCL is designed to be familiar to SQL users while supporting modality-specific operations (graph traversals, vector similarity, tensor operations, temporal time-travel, spatial containment, etc.) in a unified syntax. === What are dependent-type proofs (VCL-DT)? -VCL-DT is an optional extension to VQL that adds dependent-type verification. +VCL-DT is an optional extension to VCL that adds dependent-type verification. When enabled, VCL-DT uses the Idris2 type system to prove properties of queries at compile time: @@ -194,14 +194,14 @@ at compile time: meaningful * *Threshold validity:* Prove that coherence thresholds are within valid ranges -VCL-DT is entirely optional. Teams can use plain VQL for standard operations and +VCL-DT is entirely optional. Teams can use plain VCL for standard operations and adopt VCL-DT incrementally when they want formal guarantees. === How does federation work? VeriSimDB can federate across heterogeneous database backends, bringing drift detection to existing infrastructure without requiring data migration. Federation -connectors translate between VQL and native query languages: +connectors translate between VCL and native query languages: * *PostgreSQL:* SQL translation, table-to-document mapping * *ArangoDB:* AQL translation, graph-to-graph mapping @@ -219,7 +219,7 @@ operate as a standalone database without any external connections. Yes. VeriSimDB is released under the *Mozilla Public License 2.0 (MPL-2.0)*, a permissive open-source license. The community edition is full-featured with no artificial restrictions -- all 8 modalities, drift detection, -self-normalisation, VQL, and federation are included. +self-normalisation, VCL, and federation are included. === What licence is VeriSimDB under? @@ -257,12 +257,12 @@ j.d.a.jewell@open.ac.uk for a quote. 1. Clone the repository: `git clone https://github.com/hyperpolymath/verisimdb` 2. Follow the getting-started guide: `docs/getting-started.adoc` 3. Run the test suite: `cargo test` (Rust) and `mix test` (Elixir) -4. Explore the VQL examples: `docs/vcl-examples.adoc` +4. Explore the VCL examples: `docs/vcl-examples.adoc` === Is VeriSimDB production-ready? VeriSimDB is in *alpha stage*. The core architecture, modality model, drift -detection engine, and VQL language are implemented and tested (662 tests, 0 +detection engine, and VCL language are implemented and tested (662 tests, 0 failures). However, production deployment requires: * Performance benchmarking at enterprise scale @@ -312,6 +312,6 @@ See `CONTRIBUTING.md` in the repository for contribution guidelines. * *Repository:* https://github.com/hyperpolymath/verisimdb * *Documentation:* `docs/` directory in the repository -* *VQL specification:* `docs/VCL-SPEC.adoc` +* *VCL specification:* `docs/VCL-SPEC.adoc` * *Architecture:* `docs/vcl-architecture.adoc` * *Contact:* j.d.a.jewell@open.ac.uk diff --git a/docs/business/pr/key-messages.adoc b/docs/business/pr/key-messages.adoc index d86a69f..a9b0882 100644 --- a/docs/business/pr/key-messages.adoc +++ b/docs/business/pr/key-messages.adoc @@ -66,16 +66,16 @@ alertable condition -- not an invisible failure mode. reloading, and battle-tested concurrency. Rust provides near-C performance with memory safety. -* *VQL (Verisimilitude Query Language)*: Purpose-built query language for +* *VCL (Verisimilitude Query Language)*: Purpose-built query language for cross-modal operations. Familiar to SQL users but supports modality-specific operations (graph traversals, vector similarity, tensor ops, temporal time-travel, spatial containment) in a unified syntax. * *VCL-DT*: Optional dependent-type layer using Idris2. Proves query type correctness, semantic compatibility of cross-modal joins, and threshold - validity at compile time. Entirely opt-in -- plain VQL works without it. + validity at compile time. Entirely opt-in -- plain VCL works without it. -* *Federation*: Connectors translate between VQL and native query languages +* *Federation*: Connectors translate between VCL and native query languages (SQL, Cypher, AQL, Query DSL). Each connector independently tested with fallback to local-only mode. No vendor lock-in. @@ -112,7 +112,7 @@ alertable condition -- not an invisible failure mode. (federation) or operates standalone; it does not replace PostgreSQL * "AI-native database" -- VeriSimDB serves AI workloads (GraphRAG) but is not limited to AI; the core value is data consistency -* "NoSQL" -- VeriSimDB has its own query language (VQL); calling it NoSQL implies +* "NoSQL" -- VeriSimDB has its own query language (VCL); calling it NoSQL implies it competes with document stores == Business Audience (CTOs, VP Engineering, Data Leaders) @@ -198,7 +198,7 @@ proofs of query correctness. multi-model databases store multiple models but do not track inter-model consistency. -* *Formal semantics*: VQL has published formal semantics (denotational and +* *Formal semantics*: VCL has published formal semantics (denotational and operational). VCL-DT extends these with dependent-type judgements formalised in Idris2, providing machine-checkable proofs of query properties. @@ -221,7 +221,7 @@ proofs of query correctness. in Heterogeneous Database Federations" * Case study: IDApTIK game level architecture with Idris2 dependent-type proofs * 14-module ABI with 5 cross-domain proofs, zero `believe_me` usage -* Formal VQL grammar (EBNF) and type system specification +* Formal VCL grammar (EBNF) and type system specification === Venues @@ -256,7 +256,7 @@ proofs of query correctness. [quote] VeriSimDB is a full-featured multimodal database released under a permissive open-source licence (MPL-2.0, with MPL-2.0 fallback). All 8 -modalities, drift detection, self-normalisation, VQL, and federation are in the +modalities, drift detection, self-normalisation, VCL, and federation are in the community edition. There is no "enterprise edition" that gates features. === Supporting Points diff --git a/docs/business/pr/press-release.adoc b/docs/business/pr/press-release.adoc index 540a4b0..ef02fd4 100644 --- a/docs/business/pr/press-release.adoc +++ b/docs/business/pr/press-release.adoc @@ -38,7 +38,7 @@ designed from the ground up to detect and repair this kind of inconsistency." VeriSimDB is built on a *Rust core* for performance and memory safety, with *Elixir/OTP orchestration* for fault-tolerant concurrency. The database includes -VQL (Verisimilitude Query Language), a purpose-built query language for +VCL (Verisimilitude Query Language), a purpose-built query language for cross-modal operations, and an optional dependent-type layer (VCL-DT) that provides compile-time proofs of query correctness using Idris2. diff --git a/docs/business/strategy/adoption-roadmap.adoc b/docs/business/strategy/adoption-roadmap.adoc index 50897a0..323204e 100644 --- a/docs/business/strategy/adoption-roadmap.adoc +++ b/docs/business/strategy/adoption-roadmap.adoc @@ -64,7 +64,7 @@ The GraphRAG community is the ideal starting point for three reasons: | 1 | Public repository launch -| README with architecture diagram, getting-started guide, VQL examples, +| README with architecture diagram, getting-started guide, VCL examples, CONTRIBUTING.md | Founder @@ -99,8 +99,8 @@ deadline) | Founder | 8 -| VQL tutorial series -| 3-part tutorial: basic VQL queries, cross-modal queries, drift detection +| VCL tutorial series +| 3-part tutorial: basic VCL queries, cross-modal queries, drift detection queries | Founder @@ -283,11 +283,11 @@ Revenue comes from consulting, not software licences: | Training workshop | $2,000-$5,000 -| Half-day or full-day VQL training for the institution's development team +| Half-day or full-day VCL training for the institution's development team | Ongoing consulting | $150-$250/hour -| Architecture guidance, performance tuning, VQL query optimisation +| Architecture guidance, performance tuning, VCL query optimisation |=== *Target:* 3-5 consulting engagements, $50,000-$150,000 total revenue. @@ -440,7 +440,7 @@ After establishing 5-10 commercial customers: * Engage system integrators (Accenture, Deloitte, Thoughtworks) who advise enterprise clients on data infrastructure -* Create partner training programme (VQL certification) +* Create partner training programme (VCL certification) * Provide referral incentives (10-15% of first-year ACV) === Success Criteria (Phase 3) @@ -469,8 +469,8 @@ priorities, not marketing milestones. | Core octad storage (all 8 modalities) | Required | Required | Required | Drift detection and coherence scoring | Required | Required | Required | Self-normalisation (configurable strategies) | Required | Required | Required -| VQL parser and query execution | Required | Required | Required -| Getting-started guide and VQL examples | Required | Required | Required +| VCL parser and query execution | Required | Required | Required +| Getting-started guide and VCL examples | Required | Required | Required | Federation (PostgreSQL connector) | Demo quality | Production quality | Production quality | Federation (ArangoDB, Elasticsearch, Neo4j) | Not required | Demo quality | Production quality | VCL-DT proof certificates | Documented design | Prototype | Production quality diff --git a/docs/business/strategy/economics-analysis.adoc b/docs/business/strategy/economics-analysis.adoc index ac7cb20..f70f273 100644 --- a/docs/business/strategy/economics-analysis.adoc +++ b/docs/business/strategy/economics-analysis.adoc @@ -227,7 +227,7 @@ not additional features. ==== Principle: No Feature Gating VeriSimDB's commercial licence does *not* add features beyond the community -edition. All 8 modalities, drift detection, self-normalisation, VQL, VCL-DT, +edition. All 8 modalities, drift detection, self-normalisation, VCL, VCL-DT, and federation ship in the open-source release. This is a deliberate strategic choice: diff --git a/docs/business/strategy/functional-units.adoc b/docs/business/strategy/functional-units.adoc index cbae04e..ebe3a1b 100644 --- a/docs/business/strategy/functional-units.adoc +++ b/docs/business/strategy/functional-units.adoc @@ -151,13 +151,13 @@ The Stage 1 engineering team expands with: ==== Query Engine Engineer (1 person) -*Justification:* VQL and VCL-DT require dedicated attention as query complexity +*Justification:* VCL and VCL-DT require dedicated attention as query complexity grows. The query planner (currently basic) needs optimisation for cross-modal queries spanning all 8 modalities. *Responsibilities:* -* VQL parser and query planner development +* VCL parser and query planner development * VCL-DT type checker integration (Idris2 bridge) * Query performance optimisation (cost-based planning, modality pushdown) * Query language evolution (new syntax, new operators) @@ -171,7 +171,7 @@ targets require dedicated attention. *Responsibilities:* * Property-based test development (QuickCheck patterns for Rust + Elixir) -* Fuzz testing (VQL parser, drift detection algorithm) +* Fuzz testing (VCL parser, drift detection algorithm) * Integration testing (federation connectors, container deployment) * Performance benchmarking (automated regression detection) diff --git a/docs/business/strategy/go-to-market.adoc b/docs/business/strategy/go-to-market.adoc index 6c8f0a5..6e59d1e 100644 --- a/docs/business/strategy/go-to-market.adoc +++ b/docs/business/strategy/go-to-market.adoc @@ -95,7 +95,7 @@ cross-modal drift * Repository: https://github.com/hyperpolymath/verisimdb * Actions: Comprehensive README with architecture diagram, getting-started guide, - VQL examples, contribution guidelines + VCL examples, contribution guidelines * Metrics: Stars, forks, issues, PRs, unique cloners ==== Blog Posts (Hosted on GitHub Pages) @@ -145,7 +145,7 @@ Target conferences for Year 1: * Respond to every GitHub issue within 48 hours * Engage in relevant Reddit/HN/Lobsters threads (with disclosure) * Contribute to adjacent projects (LangChain, Qdrant) where VeriSimDB adds value -* Publish VQL examples and tutorials in `docs/` +* Publish VCL examples and tutorials in `docs/` === Success Metrics (Month 12) @@ -315,7 +315,7 @@ After establishing 5-10 commercial customers through developer-led adoption: * Engage system integrators (Accenture, Deloitte, Thoughtworks) who advise enterprise clients on data infrastructure -* Create partner training programme (VQL certification) +* Create partner training programme (VCL certification) * Provide referral incentives (10-15% of first-year ACV) === Commercial Support Licence diff --git a/docs/cache-sharing-strategy.adoc b/docs/cache-sharing-strategy.adoc index 45dbf00..082a249 100644 --- a/docs/cache-sharing-strategy.adoc +++ b/docs/cache-sharing-strategy.adoc @@ -740,6 +740,6 @@ end == References - link:caching-strategy.adoc[Caching Strategy Overview] -- link:vcl-architecture.adoc[VQL Architecture] +- link:vcl-architecture.adoc[VCL Architecture] - link:challenges-federated.adoc[Federated Deployment Challenges] - link:../lib/verisim/query_cache.ex[Query Cache Implementation] diff --git a/docs/caching-strategy.adoc b/docs/caching-strategy.adoc index 8719c1a..d137f06 100644 --- a/docs/caching-strategy.adoc +++ b/docs/caching-strategy.adoc @@ -21,7 +21,7 @@ VeriSimDB implements a **multi-layer, drift-aware caching system** that dramatic |On drift, on write |**Parsed ASTs** -|Parsed VQL abstract syntax trees +|Parsed VCL abstract syntax trees |1 hour |Never (queries don't change) @@ -589,6 +589,6 @@ QueryCache.invalidate_by_tag("project:thesis-2025") - link:query-optimization-overview.adoc[Query Optimization Overview] - link:reversibility-design.adoc[Reversibility Design] -- link:vcl-architecture.adoc[VQL Architecture] +- link:vcl-architecture.adoc[VCL Architecture] - link:../lib/verisim/query_cache.ex[Query Cache Implementation] - link:../lib/verisim/query_router_cached.ex[Cached Query Router] diff --git a/docs/consultation-dependent-types-zkp.adoc b/docs/consultation-dependent-types-zkp.adoc index 1043a84..1297aed 100644 --- a/docs/consultation-dependent-types-zkp.adoc +++ b/docs/consultation-dependent-types-zkp.adoc @@ -52,7 +52,7 @@ VeriSimDB must support **two fundamentally different query execution models**: **Example query that exposes the challenge**: -```vql +```vcl -- Dependent-type query: Prove that ALL results satisfy predicate SELECT GRAPH, DOCUMENT FROM verisim:semantic @@ -159,8 +159,8 @@ and expr = {x : Int | x > 0} ``` -In VQL: -```vql +In VCL: +```vcl VERIFIED(citation_count > 0) -- Type: {n : Int | n > 0} ``` @@ -170,8 +170,8 @@ VERIFIED(citation_count > 0) -- Type: {n : Int | n > 0} {xs : List[String] | length(xs) > 0} ``` -In VQL: -```vql +In VCL: +```vcl VERIFIED(authors != []) -- Type: {as : List[String] | length(as) > 0} ``` @@ -182,8 +182,8 @@ VERIFIED(authors != []) -- Type: {as : List[String] | length(as) > 0} Proof[∀ h ∈ r. h.document.peer_reviewed = true] ``` -In VQL: -```vql +In VCL: +```vcl PROOF EXISTENCE { ∀ r ∈ Result. r.document.peer_reviewed = true } @@ -300,7 +300,7 @@ let rec check ctx expr expected_type = **Example**: -```vql +```vcl -- Query SELECT GRAPH FROM verisim:semantic @@ -357,7 +357,7 @@ let implies (phi1 : expr) (phi2 : expr) : bool = === 3.1 Proof Contracts -**Four types of proofs** in VQL: +**Four types of proofs** in VCL: [cols="1,2,2",options="header"] |=== @@ -372,9 +372,9 @@ let implies (phi1 : expr) (phi2 : expr) : bool = |**INTEGRITY** |`∀ r ∈ Result. hash(r) = expected` |Prove data integrity (no tampering) |=== -**VQL examples**: +**VCL examples**: -```vql +```vcl -- EXISTENCE proof: At least one peer-reviewed paper exists SELECT * FROM verisim:semantic @@ -408,7 +408,7 @@ PROOF ACCESS { ``` ┌─────────────────┐ -│ VQL Query │ +│ VCL Query │ │ (with PROOF) │ └────────┬────────┘ │ @@ -478,7 +478,7 @@ impl CircuitBuilder { **Example circuit**: -```vql +```vcl PROOF UNIVERSAL { ∀ r ∈ Result. r.document.peer_reviewed = true } @@ -504,7 +504,7 @@ PROOF UNIVERSAL { use proven::{Circuit, Proof, ProvingKey, VerifyingKey}; pub async fn generate_proof( - query: &VQLQuery, + query: &VCLQuery, result: &QueryResult, contract: &ProofContract, ) -> Result { @@ -628,7 +628,7 @@ pub fn verify_proof( **Attack 1: Malicious query (invalid proof claim)** -```vql +```vcl -- Attacker tries to prove false statement SELECT * FROM verisim:semantic @@ -659,7 +659,7 @@ Attacker tries to construct fake proof without executing query. **Attack 3: Type confusion** -```vql +```vcl -- Attacker tries to confuse type checker SELECT GRAPH FROM verisim:semantic @@ -710,7 +710,7 @@ if not (equal_type t1 TInt && equal_type t2 TInt) then // 1. Cache type-checking results static TYPE_CACHE: Lazy>> = ...; -pub fn type_check_cached(query: &VQLQuery) -> Result { +pub fn type_check_cached(query: &VCLQuery) -> Result { let hash = compute_hash(query); if let Some(ty) = TYPE_CACHE.lock().unwrap().get(&hash) { @@ -724,8 +724,8 @@ pub fn type_check_cached(query: &VQLQuery) -> Result { // 2. Incremental type checking (only check changed parts) pub fn type_check_incremental( - query: &VQLQuery, - prev_query: &VQLQuery, + query: &VCLQuery, + prev_query: &VCLQuery, prev_type: &DependentType, ) -> Result { // Diff queries, only re-check changed AST nodes @@ -738,7 +738,7 @@ pub fn type_check_incremental( // 3. Parallel proof generation (batch queries) pub async fn generate_proofs_batch( - queries: Vec<(VQLQuery, QueryResult)>, + queries: Vec<(VCLQuery, QueryResult)>, ) -> Result, ProofError> { use tokio::task::spawn; @@ -795,7 +795,7 @@ Int **Benefit**: Slipstream execution uses erased types (faster, no proof generation). ```rust -pub fn execute_query_erased(query: &VQLQuery) -> Result { +pub fn execute_query_erased(query: &VCLQuery) -> Result { // Type check with dependent types let full_type = type_check(query)?; @@ -849,7 +849,7 @@ pub extern "C" fn type_check_query( query_json: *const c_char, ) -> *mut c_char { let query_str = unsafe { CStr::from_ptr(query_json).to_str().unwrap() }; - let query: VQLQuery = serde_json::from_str(query_str).unwrap(); + let query: VCLQuery = serde_json::from_str(query_str).unwrap(); let type_checker = TypeChecker::new(); match type_checker.check(&query) { @@ -872,8 +872,8 @@ pub extern "C" fn type_check_query( @module("./native/type_checker.node") external typeCheckQuery: string => string = "type_check_query" -let checkQuery = (query: VQLQuery.t): result => { - let queryJson = query->VQLQuery.toJson->Js.Json.stringify +let checkQuery = (query: VCLQuery.t): result => { + let queryJson = query->VCLQuery.toJson->Js.Json.stringify let resultJson = typeCheckQuery(queryJson) switch resultJson->Js.Json.parseExn { @@ -895,7 +895,7 @@ let checkQuery = (query: VQLQuery.t): result => { **Example**: -```vql +```vcl -- 1000 results, each with 10-field record PROOF UNIVERSAL { ∀ r ∈ Result. r.document.word_count > 1000 @@ -961,7 +961,7 @@ prove φ(sample(Result, 100)) with high probability ```rescript // VQLTypeChecker.res -let isVerifiable = (expr: VQLExpr.t): bool => { +let isVerifiable = (expr: VCLExpr.t): bool => { switch expr { | EBinOp(Eq, _, _) => true | EBinOp(Lt | Gt | Lte | Gte, _, _) => true @@ -1123,7 +1123,7 @@ See docs/vcl-type-system.adoc for full 30+ typing rules. === B.1 EXISTENCE Proof **Query**: -```vql +```vcl SELECT * FROM verisim:semantic WHERE octad.types INCLUDES "Paper" @@ -1145,7 +1145,7 @@ Output: proof π === B.2 UNIVERSAL Proof **Query**: -```vql +```vcl SELECT * FROM verisim:restricted WHERE octad.types INCLUDES "MedicalRecord" diff --git a/docs/consultation-normalization-strategy.adoc b/docs/consultation-normalization-strategy.adoc index 9167703..61b78f1 100644 --- a/docs/consultation-normalization-strategy.adoc +++ b/docs/consultation-normalization-strategy.adoc @@ -208,9 +208,9 @@ From Kafka's migration to KRaft (similar problem domain): └─────────────────┘ ``` -**VQL query-time repair**: +**VCL query-time repair**: -```vql +```vcl -- User's query SELECT GRAPH, DOCUMENT FROM verisim:semantic @@ -229,9 +229,9 @@ LIMIT 100; impl OctadStore { pub async fn query_with_repair( &self, - query: &VQLQuery, + query: &VCLQuery, repair_policy: RepairPolicy, - ) -> Result { + ) -> Result { // Execute query let raw_results = self.execute_query(query).await?; @@ -243,7 +243,7 @@ impl OctadStore { let repaired = match repair_policy { RepairPolicy::LatestWins => self.repair_latest_wins(raw_results, drift_detected), RepairPolicy::Quorum => self.repair_quorum(raw_results, drift_detected).await?, - RepairPolicy::Manual => return Err(VQLError::ManualRepairRequired(drift_detected)), + RepairPolicy::Manual => return Err(VCLError::ManualRepairRequired(drift_detected)), }; // Cache repaired results diff --git a/docs/design/DESIGN-2026-02-27-strategic-improvements.adoc b/docs/design/DESIGN-2026-02-27-strategic-improvements.adoc index 59cab15..bda8bd0 100644 --- a/docs/design/DESIGN-2026-02-27-strategic-improvements.adoc +++ b/docs/design/DESIGN-2026-02-27-strategic-improvements.adoc @@ -81,9 +81,9 @@ automatically. This is genuinely novel. |=== | Problem | Severity | Detail -| **VQL is incomplete** +| **VCL is incomplete** | HIGH -| VQL parses and executes basic queries, but the language is not fully specified +| VCL parses and executes basic queries, but the language is not fully specified and lacks documentation. Without a usable query language, VerisimDB is an HTTP CRUD API with caching. _This is the single biggest gap._ @@ -175,7 +175,7 @@ automatically. This is genuinely novel. | **Query language** | SPARQL + SQL (both mature, standardised) -| VQL (custom, incomplete) +| VCL (custom, incomplete) | **Linked Data / LOD** | First-class citizen -- LOD cloud backbone @@ -199,7 +199,7 @@ automatically. This is genuinely novel. | **Documentation** | Extensive (if sometimes dated) -| Sparse (VQL docs incomplete) +| Sparse (VCL docs incomplete) | **Operational complexity** | Moderate-high (multi-port, config-heavy) @@ -483,11 +483,11 @@ The provenance modality is structurally simpler than graph or vector: `WHERE provenance.chain CONTAINS 'spark-etl-step-3'` - Drift integration: when drift is detected, provenance can pinpoint _which transformation step_ introduced the inconsistency -- VQL extension: `PROVENANCE` clause alongside existing `PROOF` clause +- VCL extension: `PROVENANCE` clause alongside existing `PROOF` clause ==== Priority -**CRITICAL.** Implement after VQL (Priority 1) and the drift demo +**CRITICAL.** Implement after VCL (Priority 1) and the drift demo (Priority 2), but before or alongside heterogeneous federation (Priority 5). Provenance and federation are mutually reinforcing — federation without provenance tells you data disagrees; federation _with_ provenance tells you @@ -506,7 +506,7 @@ fleet management system has this. - **Spatial index** — R-tree for efficient proximity and containment queries - **CRS metadata** — coordinate reference system (WGS84, UTM, etc.) -==== Spatial Queries in VQL +==== Spatial Queries in VCL - `WHERE spatial.within(polygon)` — containment - `WHERE spatial.distance(point) < 5000` — proximity (metres) @@ -528,16 +528,16 @@ compounds with drift detection and federation; spatial is additive. Ordered by impact. Each item is self-contained and can be picked up in any future session. -=== Priority 1: Finish VQL (HIGH) +=== Priority 1: Finish VCL (HIGH) **Why:** A database without a usable query language is a key-value store with extra steps. This is the single highest-impact improvement. -**Scope:** Not VCL-DT. Just VQL. The query language that end users type. +**Scope:** Not VCL-DT. Just VCL. The query language that end users type. **What "finished" means:** -1. **Language specification** -- a document (adoc or djot) that defines VQL +1. **Language specification** -- a document (adoc or djot) that defines VCL syntax and semantics exhaustively. Every valid query form documented with examples. Every error case specified. @@ -604,7 +604,7 @@ find assumptions you did not know you made. - Find one other project -- academic, open-source, or a friend's -- that has multi-representation data and would benefit from drift detection - The demo from Priority 2 is the sales pitch -- Do not wait for VQL to be perfect; the REST API is sufficient for a first +- Do not wait for VCL to be perfect; the REST API is sufficient for a first user === Priority 4: Positioning and Documentation (MEDIUM) @@ -672,11 +672,11 @@ peers via HTTP adapters. The `GraphStore` trait abstraction already exists, so this is a backend swap. -=== Priority 7: Wire VCL-DT (HIGH — but after VQL) +=== Priority 7: Wire VCL-DT (HIGH — but after VCL) **Why:** VCL-DT is the technical moat — the reason nobody can clone VerisimDB quickly. Formally verified query results via Lean type checking is genuinely -unique in the database world. But VQL must work reliably first (Priority 1). +unique in the database world. But VCL must work reliably first (Priority 1). No point verifying proofs in a query language that cannot execute reliably. **Why it matters more than it might seem:** @@ -696,7 +696,7 @@ No other database can do this. Not Virtuoso, not ArangoDB, not Postgres. The Lean type definitions already exist. The proof obligation generation is designed. The gap is wiring the Lean checker into the execution path. -**Defer until:** VQL spec is complete and integration-tested (Priority 1). +**Defer until:** VCL spec is complete and integration-tested (Priority 1). Then this becomes the highest priority. **See:** KNOWN-ISSUES #21, `docs/vcl-vs-vcl-dt.adoc` for the phased roadmap. @@ -734,13 +734,13 @@ and zero external validation. The path forward (priority order): -1. **Finish VQL** so the database is _queryable_ +1. **Finish VCL** so the database is _queryable_ 2. **Drift detection demo** so the differentiator is _undeniable_ 3. **Provenance / lineage modality** so cross-system data origins are _traceable_ (CRITICAL) 4. **One external user** so the assumptions are _tested_ 5. **Heterogeneous federation** so enterprise adoption is _practical_ 6. **Reposition** around drift detection so the value proposition is _clear_ -7. **Wire VCL-DT** so the technical moat is _operational_ (after VQL is solid) +7. **Wire VCL-DT** so the technical moat is _operational_ (after VCL is solid) The layered pitch: diff --git a/docs/design/DESIGN-2026-02-27-vcl-dt-assessment.adoc b/docs/design/DESIGN-2026-02-27-vcl-dt-assessment.adoc index e13cb9b..a395128 100644 --- a/docs/design/DESIGN-2026-02-27-vcl-dt-assessment.adoc +++ b/docs/design/DESIGN-2026-02-27-vcl-dt-assessment.adoc @@ -104,12 +104,12 @@ end-to-end pipeline does not). nodes. Hardcoded cost estimates per modality (reasonable heuristics). | `VQLTypeChecker.res` (355 lines) -| *FULLY IMPLEMENTED.* Thin facade over VQLBidir. Backward-compatible API. +| *FULLY IMPLEMENTED.* Thin facade over VCLBidir. Backward-compatible API. |=== ==== What Is Stubbed/Incomplete -1. **VQLSubtyping Rule 6** — Refinement subsumption needs an SMT solver +1. **VCLSubtyping Rule 6** — Refinement subsumption needs an SMT solver (e.g., Z3 or CVC5). This is required for proving that a refined type (with proof) is a subtype of another refined type. @@ -126,8 +126,8 @@ end-to-end pipeline does not). 1. **No integration with Elixir executor.** The ReScript type checker runs entirely client-side (in the browser or via Deno/Node). The Elixir VCL - executor comment says "Type-check if PROOF clause present (VQLTypeChecker - -> VQLBidir)" but this invocation never happens. The Elixir executor + executor comment says "Type-check if PROOF clause present (VCLTypeChecker + -> VCLBidir)" but this invocation never happens. The Elixir executor parses VCL independently using its own built-in parser. 2. **No proof generation triggered from type checker.** The type checker @@ -238,14 +238,14 @@ endpoint would fail or be silently ignored. |=== | File | Status -| `vql_bridge.ex` (672 lines) +| `vcl_bridge.ex` (672 lines) | *IMPLEMENTED with degraded fallback.* GenServer managing a Deno/Node subprocess that runs compiled ReScript VCL parser. Falls back to built-in Elixir parser when subprocess unavailable. `parse_dependent/2` exists but the fallback parser only collects PROOF tokens as raw strings, not structured proof specs. -| `vql_executor.ex` (~1000 lines) +| `vcl_executor.ex` (~1000 lines) | *PARTIALLY IMPLEMENTED.* Full SELECT/INSERT/UPDATE/DELETE execution, cross-modal condition evaluation (DRIFT, CONSISTENT, EXISTS/NOT EXISTS between modalities), pagination, ORDER BY, GROUP BY, aggregates. BUT: proof @@ -258,7 +258,7 @@ endpoint would fail or be silently ignored. ==== The Critical Proof Verification Gap -The `verify_single_proof/1` function in `vql_executor.ex` (lines 514-592) +The `verify_single_proof/1` function in `vcl_executor.ex` (lines 514-592) reveals the core disconnect: [source,elixir] @@ -392,14 +392,14 @@ Client sends VCL with PROOF clause The ReScript type checker is the most complete component but is entirely disconnected. Wire it: -1. Ensure `vql_bridge.ex` reliably spawns the ReScript parser process (or +1. Ensure `vcl_bridge.ex` reliably spawns the ReScript parser process (or compile ReScript to a standalone binary via Deno). -2. Add a `typecheck/2` function to `vql_bridge.ex` that sends the parsed AST +2. Add a `typecheck/2` function to `vcl_bridge.ex` that sends the parsed AST to the ReScript type checker and receives back: - Inferred types - Proof obligations (from `VQLProofObligation.res`) - Composition strategy -3. In `vql_executor.ex`, after parsing a query with PROOF clause, call the +3. In `vcl_executor.ex`, after parsing a query with PROOF clause, call the type checker before executing. 4. Use the returned proof obligations to drive actual proof generation (Priority 2). @@ -429,7 +429,7 @@ Replace the stubbed `verify_single_proof/1` with real proof generation: rather than generating new hash commitments. 4. For `:sanctify` type, call the sanctify bridge's contract validation. -=== Priority 4: VQLSubtyping Rule 6 — Refinement Subsumption (MEDIUM) +=== Priority 4: VCLSubtyping Rule 6 — Refinement Subsumption (MEDIUM) **Effort: 3-5 days (significant)** @@ -483,7 +483,7 @@ checker is sufficient for practical use. | 95% | 0% -| ReScript Type Checker (VQLBidir) +| ReScript Type Checker (VCLBidir) | 85% | 85% | 0% diff --git a/docs/design/DESIGN-2026-02-28-panll-interop-telemetry.md b/docs/design/DESIGN-2026-02-28-panll-interop-telemetry.md index 36c02cc..bf17c2e 100644 --- a/docs/design/DESIGN-2026-02-28-panll-interop-telemetry.md +++ b/docs/design/DESIGN-2026-02-28-panll-interop-telemetry.md @@ -12,7 +12,7 @@ in PanLL's Model, with VeriSimDB-specific messages and Tauri commands. This mean 1. **No plugin architecture** for other databases (QuandleDB, LithoGlyph) 2. **No telemetry** — we have `:telemetry` events defined but no aggregation, export, or UI 3. **No product development feedback loop** — we don't know how the system is used -4. **Each playground is standalone** — VQL Playground, future KQL/GQL playgrounds are islands +4. **Each playground is standalone** — VCL Playground, future KQL/GQL playgrounds are islands ## Design Goals @@ -119,7 +119,7 @@ The reporter aggregates raw telemetry into actionable insights: - `Model.res` — `verisimdbState` with drift scores, proof obligations - `Msg.res` — `verisimdbMsg` with health, query, drift, normalise, entity detail - `TauriCmd.res` — 7 VeriSimDB Tauri commands -- `PaneW.res` — Database tools panel, drift heatmap, VQL query area +- `PaneW.res` — Database tools panel, drift heatmap, VCL query area **New (this session):** - `Model.res` — add `telemetryState` to verisimdbState @@ -156,9 +156,9 @@ The reporter aggregates raw telemetry into actionable insights: ### Phase 4: Playground Gallery (Future) -1. Abstract VQL Playground as a PanLL module +1. Abstract VCL Playground as a PanLL module 2. Define playground protocol (editor, linter, formatter, executor) -3. Register VQL, future KQL, future GQL playgrounds +3. Register VCL, future KQL, future GQL playgrounds 4. PanLL manages playground lifecycle ## Files Changed/Created diff --git a/docs/drift-handling.adoc b/docs/drift-handling.adoc index d380a37..f28b4f9 100644 --- a/docs/drift-handling.adoc +++ b/docs/drift-handling.adoc @@ -14,7 +14,7 @@ toc::[] 1. **Drift Detection** - Automatic monitoring across modalities 2. **Drift Repair** - Reconciliation strategies to restore consistency -3. **Drift-Aware Queries** - VQL extensions for querying drifted data +3. **Drift-Aware Queries** - VCL extensions for querying drifted data 4. **Drift Tolerance** - Configurable policies for acceptable inconsistency == Types of Drift @@ -146,11 +146,11 @@ defmodule VeriSim.DriftMonitor do end ``` -=== On-Demand Detection (VQL) +=== On-Demand Detection (VCL) **Explicit drift check query:** -```vql +```vcl DRIFT DETECT FROM verisim:graph WHERE octad.id = @id; @@ -179,7 +179,7 @@ WHERE octad.id = @id; **Batch drift detection:** -```vql +```vcl DRIFT DETECT FROM verisim:graph WHERE octad.types INCLUDES "https://schema.org/Paper" @@ -194,7 +194,7 @@ LIMIT 100; Most recent update across all modalities becomes canonical. -```vql +```vcl DRIFT REPAIR FROM verisim:graph WHERE octad.id = @id @@ -234,7 +234,7 @@ pub fn repair_latest_wins(octad_id: &Uuid) -> Result { Value that appears in majority of modalities wins. -```vql +```vcl DRIFT REPAIR FROM verisim:graph WHERE octad.id = @id @@ -274,7 +274,7 @@ pub fn repair_quorum(octad_id: &Uuid) -> Result { Present conflict to user for manual decision. -```vql +```vcl DRIFT REPAIR FROM verisim:graph WHERE octad.id = @id @@ -322,7 +322,7 @@ POST /api/v1/drift/resolve HTTP/1.1 Combine values intelligently (domain-specific). -```vql +```vcl DRIFT REPAIR FROM verisim:graph WHERE octad.id = @id @@ -364,7 +364,7 @@ config :verisim, **After repair, verify consistency:** -```vql +```vcl DRIFT VERIFY FROM verisim:graph WHERE octad.id = @id; @@ -388,7 +388,7 @@ WHERE octad.id = @id; **Accept some drift** (performance optimization): -```vql +```vcl FROM verisim:graph WITH DRIFT TOLERANCE 0.1 -- Allow 10% drift WHERE octad.types INCLUDES "https://schema.org/Paper" @@ -420,7 +420,7 @@ LIMIT 100; **Require perfect consistency** (default): -```vql +```vcl FROM verisim:graph WITH DRIFT TOLERANCE 0.0 -- No drift allowed WHERE octad.types INCLUDES "https://schema.org/Paper" @@ -437,7 +437,7 @@ LIMIT 100; **Time-travel query** using temporal modality: -```vql +```vcl -- Query BEFORE repair (as of specific time) FROM verisim:temporal WHERE octad.id = @id @@ -454,7 +454,7 @@ WHERE octad.id = @id; **Query across federated stores with mixed drift:** -```vql +```vcl FROM verisim:federation WHERE octad.types INCLUDES "https://schema.org/Paper" WITH DRIFT TOLERANCE 0.2 -- Tolerate 20% drift across federation @@ -540,7 +540,7 @@ pub fn classify_drift_severity(drift: &Drift) -> DriftSeverity { **Detection:** -```vql +```vcl DRIFT DETECT FEDERATION FROM verisim:federation WHERE octad.id = @id @@ -589,9 +589,9 @@ Store E reports: title = "HACKED!!!" ❌ BYZANTINE Action: Exclude Store E from quorum, investigate tampering ``` -**VQL query with Byzantine tolerance:** +**VCL query with Byzantine tolerance:** -```vql +```vcl FROM verisim:federation WHERE octad.id = @id WITH BYZANTINE TOLERANCE 1 -- Tolerate 1 faulty node @@ -607,9 +607,9 @@ MIN QUORUM 3; 3. **Propagation phase** - Leader broadcasts canonical value 4. **Verification phase** - All stores confirm consistency -**VQL:** +**VCL:** -```vql +```vcl DRIFT REPAIR FEDERATION FROM verisim:federation WHERE octad.id = @id @@ -623,7 +623,7 @@ COORDINATOR @university_a; **View all drift events for a Octad:** -```vql +```vcl DRIFT HISTORY FROM verisim:temporal WHERE octad.id = @id @@ -661,7 +661,7 @@ LIMIT 10; **System-wide drift statistics:** -```vql +```vcl DRIFT METRICS FROM verisim:system WHERE period = 'last_24_hours'; @@ -824,9 +824,9 @@ end VeriSimDB provides comprehensive drift handling through: -1. **Detection** - Automatic monitoring + on-demand VQL queries +1. **Detection** - Automatic monitoring + on-demand VCL queries 2. **Repair** - Multiple strategies (latest_wins, quorum, manual, merge) -3. **Query Integration** - Drift-aware VQL with tolerance controls +3. **Query Integration** - Drift-aware VCL with tolerance controls 4. **Federation** - Cross-org drift detection and Byzantine tolerance 5. **Audit** - Complete drift history in verisim-temporal diff --git a/docs/error-handling-strategy.adoc b/docs/error-handling-strategy.adoc index d2e2778..7ef0acd 100644 --- a/docs/error-handling-strategy.adoc +++ b/docs/error-handling-strategy.adoc @@ -1,6 +1,6 @@ // SPDX-License-Identifier: MPL-2.0 -= VQL Error Handling Strategy += VCL Error Handling Strategy :toc: left :toclevels: 3 :sectnums: @@ -26,7 +26,7 @@ VeriSimDB's error handling provides **comprehensive, actionable feedback** acros |Category |When It Happens |Recoverable? |Example |**Parse Errors** -|Invalid VQL syntax +|Invalid VCL syntax |No (client fix) |`SELECT GRPH FROM ...` (typo) @@ -53,7 +53,7 @@ VeriSimDB's error handling provides **comprehensive, actionable feedback** acros == Parse Errors -**Cause:** Invalid VQL syntax detected by parser +**Cause:** Invalid VCL syntax detected by parser **Characteristics:** @@ -64,7 +64,7 @@ VeriSimDB's error handling provides **comprehensive, actionable feedback** acros === Example: Unexpected Token -[source,vql] +[source,vcl] ---- SELECT GRAPH, VECTRO FROM octad abc-123 ^^^^^^ @@ -137,7 +137,7 @@ ParseError({ === Example: Contract Violation -[source,vql] +[source,vcl] ---- SELECT SEMANTIC FROM octad abc-123 PROOF ACCESS(EthicsApprovalContract) @@ -204,7 +204,7 @@ TypeError({ === Example: Store Unavailable -[source,vql] +[source,vcl] ---- SELECT GRAPH FROM store milvus-1 WHERE ... ---- @@ -360,7 +360,7 @@ Each modality has its own error types due to domain-specific constraints. === Example: Partial Results -[source,vql] +[source,vcl] ---- SELECT GRAPH FROM FEDERATION /universities/* LIMIT 100 ---- @@ -621,12 +621,12 @@ defmodule VeriSim.ErrorLogger do def log_error(error, context) do entry = %{ timestamp: DateTime.utc_now(), - error_code: VQLError.get_error_code(error), - error_message: VQLError.format(error), + error_code: VCLError.get_error_code(error), + error_message: VCLError.format(error), query_id: context.query_id, user_id: context.user_id, octad_ids: context.octad_ids, - recoverable: VQLError.is_recoverable?(error), + recoverable: VCLError.is_recoverable?(error), recovery_attempted: context.recovery_attempted, recovery_successful: context.recovery_successful } @@ -638,7 +638,7 @@ end **Audit queries:** -[source,vql] +[source,vcl] ---- -- Find all errors for a user SELECT TEMPORAL FROM audit_log @@ -655,7 +655,7 @@ WHERE event_type = 'error' -- Find stores with high error rates SELECT TEMPORAL FROM audit_log WHERE event_type = 'error' - AND error_code LIKE 'VQL_STORE_%' + AND error_code LIKE 'VCL_STORE_%' GROUP BY store_id ORDER BY COUNT(*) DESC ---- @@ -668,7 +668,7 @@ ORDER BY COUNT(*) DESC ---- { "error": { - "code": "VQL_PARSE_ERROR", + "code": "VCL_PARSE_ERROR", "message": "Parse Error at 1:14-1:20: Expected 'VECTOR', found 'VECTRO'", "hint": "Did you mean 'VECTOR'?", "recoverable": false, @@ -710,7 +710,7 @@ ORDER BY COUNT(*) DESC ---- type queryResult<'a> = | Ok('a) - | Error(vqlError) + | Error(vclError) | Partial({data: 'a, failed: array}) ---- @@ -772,7 +772,7 @@ Logger.error("Query execution failed", [source,elixir] ---- -case VQLParser.parse(query_string) do +case VCLParser.parse(query_string) do {:ok, ast} -> execute(ast) {:error, parse_error} -> # Don't retry parse errors @@ -851,7 +851,7 @@ end == Verbosity Levels -VQL supports **four verbosity levels** for error and diagnostic output: +VCL supports **four verbosity levels** for error and diagnostic output: [cols="1,2,3"] |=== @@ -883,8 +883,8 @@ verisim query --verbosity=verbose query.vql verisim query --verbosity=silent query.vql # CI/CD mode ---- -**VQL pragma:** -[source,vql] +**VCL pragma:** +[source,vcl] ---- SET VERBOSITY VERBOSE; @@ -965,7 +965,7 @@ Query returned 10 results in 234ms == Friendly Notices and Warnings -Beyond errors, VQL provides **helpful notices** for non-error situations: +Beyond errors, VCL provides **helpful notices** for non-error situations: === Notice Types @@ -1002,7 +1002,7 @@ Query returned 10 results in 23ms ==== Deprecated Syntax (Warning) -[source,vql] +[source,vcl] ---- VERSION 0.9; SELECT * FROM HEXAD abc-123; @@ -1016,7 +1016,7 @@ SELECT * FROM HEXAD abc-123; ==== Missing LIMIT (Hint) -[source,vql] +[source,vcl] ---- SELECT GRAPH, DOCUMENT FROM FEDERATION /universities/* @@ -1062,7 +1062,7 @@ verisim query --strict query.vql **Status:** STUB - Planned for v3.0 -VQL error handling will integrate with **miniKanren** (link:minikanren-integration-v3.adoc[see roadmap]) to: +VCL error handling will integrate with **miniKanren** (link:minikanren-integration-v3.adoc[see roadmap]) to: 1. **Learn error patterns** - Synthesize predicates from error examples 2. **Suggest fixes** - Generate correction rules from observed errors @@ -1203,7 +1203,7 @@ end # lib/verisim/query_parser.ex (v3 - suggest fixes) defmodule VeriSim.QueryParser do def parse(query_string) do - case VQLParser.parse(query_string) do + case VCLParser.parse(query_string) do {:ok, ast} -> {:ok, ast} {:error, parse_error} -> # v3: Ask miniKanren for fix suggestions @@ -1252,8 +1252,8 @@ Parse Error at 1:8: Expected 'GRAPH', 'VECTOR', ..., found 'GRPH' == References -- link:vcl-architecture.adoc[VQL Architecture] +- link:vcl-architecture.adoc[VCL Architecture] - link:caching-strategy.adoc[Caching Strategy] - link:reversibility-design.adoc[Reversibility Design] -- link:../src/vql/VQLError.res[VQL Error Types] +- link:../src/vql/VQLError.res[VCL Error Types] - link:../lib/verisim/error_recovery.ex[Error Recovery Implementation] diff --git a/docs/federation-readiness.adoc b/docs/federation-readiness.adoc index e72e74a..5a3ce8a 100644 --- a/docs/federation-readiness.adoc +++ b/docs/federation-readiness.adoc @@ -12,9 +12,9 @@ Federation is the ability for multiple VeriSimDB instances to coordinate queries Federation in VeriSimDB is distinct from database replication. Replicated databases maintain identical copies of the same data. Federated VeriSimDB instances hold _different_ octad entities that may reference each other through graph edges, share semantic vocabularies, or have vector embeddings in the same latent space. The federation layer coordinates cross-instance queries while each instance retains sovereignty over its own data. -The VQL query language supports federation natively: +The VCL query language supports federation natively: -[source,vql] +[source,vcl] ---- SELECT GRAPH, SEMANTIC FROM FEDERATION cross_org_research @@ -36,25 +36,25 @@ The `verisim-api` Rust crate includes API endpoints for federation peer manageme These routes accept and return JSON. Peer metadata includes the instance URL, supported modalities, version, and last-seen timestamp. Peer registration works and persists across restarts. -=== VQL Parser Accepts FEDERATION Queries +=== VCL Parser Accepts FEDERATION Queries -The VQL parser (ReScript) correctly parses `FROM FEDERATION ` clauses and `DRIFT POLICY ` directives. These produce valid AST nodes that flow through the query router. The parser also handles federation-scoped `WHERE` clauses and multi-modality `SELECT` statements against federation targets. +The VCL parser (ReScript) correctly parses `FROM FEDERATION ` clauses and `DRIFT POLICY ` directives. These produce valid AST nodes that flow through the query router. The parser also handles federation-scoped `WHERE` clauses and multi-modality `SELECT` statements against federation targets. === Hypatia FileExecutor Handles FEDERATION Queries Hypatia's `FileExecutor` module can execute `FEDERATION` queries against local flat files (the verisimdb-data git-backed store). It performs cross-store matching by loading scan results from multiple repositories and correlating them by entity identifiers. This is a file-based simulation of federation, not true distributed query execution, but it validates the query structure and result format. -== What VeriSimDB Loses Without VQL +== What VeriSimDB Loses Without VCL -If VQL were removed or not used, VeriSimDB would lose the following federation-critical capabilities: +If VCL were removed or not used, VeriSimDB would lose the following federation-critical capabilities: -* **No structured query language for multi-store coordination.** Without VQL, federated queries would require hand-written API calls to each peer, manual result merging, and no unified query plan. VQL provides a single declarative interface that the federation layer decomposes into per-peer sub-queries. +* **No structured query language for multi-store coordination.** Without VCL, federated queries would require hand-written API calls to each peer, manual result merging, and no unified query plan. VCL provides a single declarative interface that the federation layer decomposes into per-peer sub-queries. -* **No drift policy enforcement on federated queries.** Drift policies (`DRIFT POLICY strict_consistency`, `DRIFT POLICY eventual`, etc.) are expressed in VQL and enforced by the query router. Without VQL, there is no standard mechanism to declare or enforce consistency requirements across federated peers. +* **No drift policy enforcement on federated queries.** Drift policies (`DRIFT POLICY strict_consistency`, `DRIFT POLICY eventual`, etc.) are expressed in VCL and enforced by the query router. Without VCL, there is no standard mechanism to declare or enforce consistency requirements across federated peers. -* **No cross-modal consistency checks across instances.** VQL's `PROOF CONSISTENCY` clause can request verification that graph, vector, and semantic modalities agree across federation peers. Without VCL-DT, there is no way to express or verify cross-instance consistency at query time. +* **No cross-modal consistency checks across instances.** VCL's `PROOF CONSISTENCY` clause can request verification that graph, vector, and semantic modalities agree across federation peers. Without VCL-DT, there is no way to express or verify cross-instance consistency at query time. -* **No unified result format.** VQL queries return results in a consistent format regardless of whether the data came from one instance or twenty. Without VQL, each peer's API response format would need to be handled individually. +* **No unified result format.** VCL queries return results in a consistent format regardless of whether the data came from one instance or twenty. Without VCL, each peer's API response format would need to be handled individually. == Current Gaps @@ -95,7 +95,7 @@ Drift detection works: the `verisim-drift` crate computes drift scores across mo |Ready |Endpoints work, persistence confirmed. Peer metadata stored and retrievable. -|**VQL Parser (FEDERATION syntax)** +|**VCL Parser (FEDERATION syntax)** |Ready |Parses `FROM FEDERATION`, `DRIFT POLICY`, and federation-scoped queries correctly. Produces valid AST. @@ -159,7 +159,7 @@ Drift detection works: the `verisim-drift` crate computes drift scores across mo **Goal:** VCL-DT proofs work across federation boundaries. -* Wire Lean type checker into the VCL-DT execution path (prerequisite: VCL-DT Phase 3 from link:vcl-vs-vcl-dt.adoc[VQL Slipstream vs VCL-DT]). +* Wire Lean type checker into the VCL-DT execution path (prerequisite: VCL-DT Phase 3 from link:vcl-vs-vcl-dt.adoc[VCL Slipstream vs VCL-DT]). * Implement proof witness collection across peers: each peer contributes its portion of the proof. * Implement Raft consensus for coordinated writes (cross-instance referential integrity). * Implement `PROOF CONSISTENCY` verification across federation peers (cross-instance modal agreement). diff --git a/docs/getting-started.adoc b/docs/getting-started.adoc index b1a054e..fc5a137 100644 --- a/docs/getting-started.adoc +++ b/docs/getting-started.adoc @@ -40,7 +40,7 @@ repair it. │ Elixir/OTP Orchestration Layer │ │ ├── EntityServer (GenServer per entity) │ │ ├── DriftMonitor (continuous consistency check) │ -│ ├── QueryRouter (distributes VQL queries) │ +│ ├── QueryRouter (distributes VCL queries) │ │ ├── SchemaRegistry (type system coordination) │ │ └── Federation (heterogeneous peer queries) │ │ ↕ HTTP / NIF │ @@ -64,7 +64,7 @@ repair it. === Optional Dependencies -* **Deno** 2.0+ (for VQL parser bridge -- falls back to built-in parser) +* **Deno** 2.0+ (for VCL parser bridge -- falls back to built-in parser) * **pgvector**, **PostGIS** (if federating with PostgreSQL) == Installation @@ -289,10 +289,10 @@ VeriSimDB identifies the document as the authoritative modality and regenerates the vector embedding to match. Re-checking drift will show all scores back near zero. -== Querying with VQL +== Querying with VCL -VeriSimDB uses its own query language, *VQL* (VeriSim Consonance Language), -designed for cross-modal queries. VQL is not SQL -- it natively +VeriSimDB uses its own query language, *VCL* (VeriSim Consonance Language), +designed for cross-modal queries. VCL is not SQL -- it natively understands modalities and drift. === Basic Queries @@ -335,7 +335,7 @@ WHERE DOCUMENT.severity > GRAPH.importance === VCL-DT (Formally Verified Queries) -VCL-DT extends VQL with proof certificates. Every result includes a +VCL-DT extends VCL with proof certificates. Every result includes a cryptographic proof that the data satisfies stated constraints: [source,sql] @@ -353,7 +353,7 @@ verifiable certificates require the Lean type checker integration == Federation VeriSimDB can federate queries across heterogeneous databases. A single -VQL query can transparently route to PostgreSQL, ArangoDB, Elasticsearch, +VCL query can transparently route to PostgreSQL, ArangoDB, Elasticsearch, and other VeriSimDB instances. === Registering Peers @@ -568,16 +568,16 @@ curl http://localhost:8080/api/v1/health export VERISIM_RUST_CORE_URL=http://localhost:8080/api/v1 ---- -=== VQL parser falls back to built-in +=== VCL parser falls back to built-in -This is normal. The external Deno-based VQL parser provides richer +This is normal. The external Deno-based VCL parser provides richer error messages but the built-in Elixir parser handles all standard queries. The fallback warning can be safely ignored. == Next Steps -* Read the link:VCL-SPEC.adoc[VQL Specification] for the full query language -* See link:vcl-examples.adoc[VQL Examples] for more query patterns +* Read the link:VCL-SPEC.adoc[VCL Specification] for the full query language +* See link:vcl-examples.adoc[VCL Examples] for more query patterns * Review link:federation-readiness.adoc[Federation Readiness] for deployment planning * Explore link:drift-handling.adoc[Drift Handling] for advanced configuration * Check link:deployment-modes.adoc[Deployment Modes] for production setup diff --git a/docs/papers/verisimdb-federated-consistency.adoc b/docs/papers/verisimdb-federated-consistency.adoc index fe3e6af..1ec6b99 100644 --- a/docs/papers/verisimdb-federated-consistency.adoc +++ b/docs/papers/verisimdb-federated-consistency.adoc @@ -369,17 +369,17 @@ Normalisation results are recorded as telemetry events including the entity ID, // ============================================================================ -// 6. VQL AND VCL-DT +// 6. VCL AND VCL-DT // ============================================================================ -== VQL and VCL-DT +== VCL and VCL-DT -=== VQL Syntax and Semantics +=== VCL Syntax and Semantics The VeriSim Consonance Language (VCL) is the native query interface for VeriSimDB. Its grammar is specified in ISO/IEC 14977 EBNF notation <> and supports `SELECT`, `INSERT`, `UPDATE`, and `DELETE` operations across octad entities. -A VQL query comprises: +A VCL query comprises: [source,ebnf] ---- @@ -391,7 +391,7 @@ query = select_clause, from_clause, [where_clause], The `SELECT` clause specifies which modalities to retrieve, with optional per-modality projections: -[source,vql] +[source,vcl] ---- SELECT GRAPH((?s)-[:CITES]->(?target)), DOCUMENT(title, abstract) FROM STORE research_papers @@ -401,12 +401,12 @@ LIMIT 50 The `FROM` clause supports three source types: `HEXAD ` for direct entity access, `STORE ` for collection queries, and `FEDERATION ` for cross-instance queries. -VQL is not SQL. +VCL is not SQL. Key differences include: no table schemas (entities are schema-flexible with type annotations in the Semantic modality), modality-scoped projections rather than column selections, graph pattern matching in `WHERE` clauses, and cross-modal conditions such as `DRIFT_SCORE(semantic, vector) > 0.5`. === The PROOF Clause and 11 Proof Types -VCL-DT (VQL with Dependent Types) is activated by the presence of a `PROOF` clause. +VCL-DT (VCL with Dependent Types) is activated by the presence of a `PROOF` clause. When a query includes `PROOF`, the query router directs it through the formal verification pipeline rather than the standard (slipstream) execution path. The `PROOF` clause takes the form `PROOF ()` and supports 11 proof types: @@ -452,7 +452,7 @@ The `PROOF` clause takes the form `PROOF ()` and supports 11 pro Multiple proofs can be composed in a single query: -[source,vql] +[source,vcl] ---- SELECT * FROM HEXAD 550e8400-e29b-41d4-a716-446655440000 @@ -495,11 +495,11 @@ VCL-DT supports three composition strategies for multi-proof queries: === Adapter-Based Federation Architecture VeriSimDB federation enables cross-instance queries over heterogeneous databases. -The federation layer is adapter-based: each external database type implements a `FederationAdapter` trait that translates VQL queries into the native query language of the target system and maps results back into octad entities. +The federation layer is adapter-based: each external database type implements a `FederationAdapter` trait that translates VCL queries into the native query language of the target system and maps results back into octad entities. Four adapters are currently defined: -1. **VeriSimDB-native** -- Peer VeriSimDB instances communicating via the HTTP API. This is the primary federation mode, supporting all VQL features including drift policies and proof clauses. +1. **VeriSimDB-native** -- Peer VeriSimDB instances communicating via the HTTP API. This is the primary federation mode, supporting all VCL features including drift policies and proof clauses. 2. **PostgreSQL** -- Queries relational tables via SQL, mapping rows to Document and Semantic modalities. Graph modalities require explicit relationship tables. @@ -558,16 +558,16 @@ The Elixir layer coordinates distributed operations using OTP's battle-tested su - **VeriSim.EntityServer**: A GenServer per entity, managing the entity's lifecycle and serialising concurrent updates. Entity servers are distributed across the cluster using Horde (a distributed DynamicSupervisor). - **VeriSim.DriftMonitor**: A GenServer that sweeps entities on a configurable interval, dispatching drift computation to the Rust core and queuing normalisation tasks. -- **VeriSim.QueryRouter**: Routes VQL queries to the appropriate execution pipeline (slipstream vs VCL-DT) and handles federation decomposition. +- **VeriSim.QueryRouter**: Routes VCL queries to the appropriate execution pipeline (slipstream vs VCL-DT) and handles federation decomposition. - **VeriSim.SchemaRegistry**: Manages entity type schemas and proof contracts, coordinating with the Semantic modality store. - **VeriSim.Consensus**: A KRaft-inspired (Kafka Raft) consensus implementation for metadata replication in clustered deployments. === ReScript Components -The VQL parser is implemented in ReScript, compiling to JavaScript and running under Deno. +The VCL parser is implemented in ReScript, compiling to JavaScript and running under Deno. This layer handles: -- VQL tokenisation and parsing to AST. +- VCL tokenisation and parsing to AST. - Federation registry management (mapping peer names to endpoints and capabilities). - PanLL database module protocol integration (registering VeriSimDB as a panel-capable database in the broader ecosystem). @@ -576,7 +576,7 @@ This layer handles: The test suite comprises 510 Rust tests and 152 Elixir tests, totalling 662 tests with 0 failures. Test categories include: -- **Unit tests**: Per-crate tests for each modality store, drift calculator, normaliser strategy, and VQL parser. +- **Unit tests**: Per-crate tests for each modality store, drift calculator, normaliser strategy, and VCL parser. - **Integration tests**: Cross-crate tests verifying drift detection triggers normalisation, federation queries span peers, and proof certificates verify correctly. - **Property tests**: Proptest-based generative testing for the drift calculator, verifying that drift scores are always in [0, 1] and that normalisation reduces drift scores. @@ -810,7 +810,7 @@ The 11 proof types cover a range of assurance levels from basic existence checki Federation extends these guarantees across organisational boundaries, enabling multi-institutional data sharing with configurable drift policies that balance consistency against latency and autonomy. -VeriSimDB is open source under the Mozilla Public License 2.0 (MPL-2.0), with the Rust core, Elixir orchestration layer, and VQL parser available at https://github.com/hyperpolymath/verisimdb. +VeriSimDB is open source under the Mozilla Public License 2.0 (MPL-2.0), with the Rust core, Elixir orchestration layer, and VCL parser available at https://github.com/hyperpolymath/verisimdb. // ============================================================================ diff --git a/docs/papers/verisimdb-idaptik-case-study.adoc b/docs/papers/verisimdb-idaptik-case-study.adoc index f7a4ab1..cb1bfac 100644 --- a/docs/papers/verisimdb-idaptik-case-study.adoc +++ b/docs/papers/verisimdb-idaptik-case-study.adoc @@ -598,7 +598,7 @@ Storage overhead:: Query complexity:: Cross-modal queries (e.g., "find all guards in zones near a specific device, - sorted by level similarity") require understanding VQL's modality-spanning + sorted by level similarity") require understanding VCL's modality-spanning syntax. Single-modality queries are straightforward. The overhead is justified when the benefits -- drift detection, version history, diff --git a/docs/query-optimization-overview.adoc b/docs/query-optimization-overview.adoc index 140c008..d7390a6 100644 --- a/docs/query-optimization-overview.adoc +++ b/docs/query-optimization-overview.adoc @@ -1,6 +1,6 @@ // SPDX-License-Identifier: MPL-2.0 -= VQL Query Optimization: Complete Guide += VCL Query Optimization: Complete Guide :toc: left :toclevels: 3 :sectnums: @@ -19,7 +19,7 @@ VeriSimDB provides comprehensive query optimization through three integrated sys To understand how your query will execute: -[source,vql] +[source,vcl] ---- EXPLAIN SELECT GRAPH, VECTOR @@ -33,7 +33,7 @@ LIMIT 10 [source,text] ---- ╔════════════════════════════════════════════════════════════════╗ -║ VQL QUERY EXECUTION PLAN ║ +║ VCL QUERY EXECUTION PLAN ║ ╚════════════════════════════════════════════════════════════════╝ Strategy: Sequential Pipeline (operations run in series) @@ -154,7 +154,7 @@ When enabled, the system: **Push optimizations from query to stores:** 1. **Predicate Pushdown** - [source,vql] + [source,vcl] ---- -- Query SELECT VECTOR, DOCUMENT @@ -168,14 +168,14 @@ When enabled, the system: ---- 2. **Projection Pushdown** - [source,vql] + [source,vcl] ---- -- Only request needed fields SELECT GRAPH(nodes, edges) -- Don't fetch properties ---- 3. **LIMIT Pushdown** - [source,vql] + [source,vcl] ---- -- Tell stores to limit results early LIMIT 10 → Each store returns ~20 (buffer for joins) @@ -204,7 +204,7 @@ When enabled, the system: === Example Optimization Flow **Initial Query:** -[source,vql] +[source,vcl] ---- SELECT GRAPH, VECTOR, DOCUMENT FROM FEDERATION /universities/* @@ -257,7 +257,7 @@ VeriSimDB's architecture provides **80% reversibility with zero overhead:** === Time-Travel Query Syntax -[source,vql] +[source,vcl] ---- -- Query historical state SELECT * @@ -345,7 +345,7 @@ end === 1. Use EXPLAIN for Slow Queries -[source,vql] +[source,vcl] ---- -- If query is slow, explain it EXPLAIN SELECT ... @@ -377,7 +377,7 @@ QueryPlannerConfig.set_adaptive(true) === 4. Use Time-Travel for Debugging -[source,vql] +[source,vcl] ---- -- Query was working yesterday, broken today? -- Compare states @@ -402,7 +402,7 @@ curl -X POST /tantivy/schema -d '{"indexed_fields": ["title", "author"]}' **Complete workflow showing all features:** -[source,vql] +[source,vcl] ---- -- 1. Check query plan EXPLAIN @@ -475,8 +475,8 @@ LIMIT 10 == References -- link:vcl-architecture.adoc[VQL Architecture] - Dual-path router design -- link:vcl-examples.adoc[VQL Examples] - 35+ example queries +- link:vcl-architecture.adoc[VCL Architecture] - Dual-path router design +- link:vcl-examples.adoc[VCL Examples] - 35+ example queries - link:reversibility-design.adoc[Reversibility Design] - Full technical specification - link:../lib/verisim/query_planner_config.ex[Query Planner Config] - Source code - link:../lib/verisim/query_planner_bidirectional.ex[Bidirectional Optimization] - Source code diff --git a/docs/releases/v0.1.0-alpha.md b/docs/releases/v0.1.0-alpha.md index f029b84..336ac19 100644 --- a/docs/releases/v0.1.0-alpha.md +++ b/docs/releases/v0.1.0-alpha.md @@ -16,12 +16,12 @@ VeriSimDB operates as both a standalone database (like PostgreSQL) and a federat ## ✨ Key Features -### 🔍 VQL Query Language (100% Complete) +### 🔍 VCL Query Language (100% Complete) - **VQLParser.res** - Full parser with combinator library (633 lines) - **VQLError.res** - Comprehensive error types for all failure modes (14K+ lines) - **VQLExplain.res** - Query execution plan visualization (7K+ lines) - **VQLTypeChecker.res** - Dependent-type verification with ZKP integration -- **VQLExecutor** - Bridges ReScript parser to Elixir orchestration +- **VCLExecutor** - Bridges ReScript parser to Elixir orchestration - ISO/IEC 14977 EBNF compliant grammar - Two execution paths: Slipstream (fast) and Dependent-type (verified) @@ -84,7 +84,7 @@ Comprehensive test coverage: - DriftMonitor - SchemaRegistry - EntityServer -- VQLExecutor +- VCLExecutor - End-to-end integration ### ⚡ Performance Benchmarks (100% Complete) @@ -156,7 +156,7 @@ Comprehensive 100+ section guide covering: ### Code Statistics - **Total Lines Written:** ~3,839 lines in final session -- **VQL Implementation:** ~22K lines +- **VCL Implementation:** ~22K lines - **Rust Core:** ~3,860 lines - **Elixir Orchestration:** ~2,000+ lines - **ReScript Registry:** ~900 lines @@ -166,7 +166,7 @@ Comprehensive 100+ section guide covering: ### Project Completion - Overall: **100%** ✅ -- VQL: **100%** ✅ +- VCL: **100%** ✅ - Elixir: **100%** ✅ - Rust Stores: **80%** 🟡 - Registry: **100%** ✅ @@ -230,7 +230,7 @@ curl -X POST http://localhost:8080/api/v1/octads \ }' ``` -**Query with VQL:** +**Query with VCL:** ```bash curl -X POST http://localhost:4000/api/v1/query \ -H "Content-Type: application/json" \ @@ -319,7 +319,7 @@ Run full benchmarks: `cd benches && cargo bench` - Full ZKP proof generation/verification - Performance optimizations - Federation production testing -- Additional VQL features (aggregations, joins) +- Additional VCL features (aggregations, joins) ### v0.3.0 (Q3 2026) - Horizontal scaling enhancements @@ -378,7 +378,7 @@ See `LICENSE` for full terms. 1. **Deploy:** Follow `DEPLOYMENT.adoc` for your environment 2. **Test:** Run integration tests and benchmarks -3. **Experiment:** Create octads and run VQL queries +3. **Experiment:** Create octads and run VCL queries 4. **Feedback:** Report issues and contribute 5. **Community:** Join discussions and share use cases diff --git a/docs/reversibility-design.adoc b/docs/reversibility-design.adoc index 449ee41..b23f82b 100644 --- a/docs/reversibility-design.adoc +++ b/docs/reversibility-design.adoc @@ -312,7 +312,7 @@ impl EventLog { **Event sourcing enables query replay:** -[source,vql] +[source,vcl] ---- -- Original query (3 hours ago) SELECT GRAPH, VECTOR @@ -402,8 +402,8 @@ end 1. Enable reversibility for Temporal + Semantic (already done!) 2. Add snapshot infrastructure for Document/Graph 3. Design CoW layer for Vector/Tensor -4. Create VQL syntax for time-travel queries: - ```vql +4. Create VCL syntax for time-travel queries: + ```vcl SELECT * FROM HEXAD abc-123 AS OF '2026-01-22T12:00:00Z' REVERT TO '2026-01-22T12:00:00Z' ``` @@ -412,5 +412,5 @@ end - link:../WHITEPAPER.md[VeriSimDB White Paper] - Temporal modality design - link:technical-specification-kraft-metadata-log.adoc[KRaft Log] - Append-only log -- link:vcl-architecture.adoc[VQL Architecture] - Query execution +- link:vcl-architecture.adoc[VCL Architecture] - Query execution - https://martin.kleppmann.com/2015/05/27/logs-for-data-infrastructure.html[Designing Data-Intensive Applications] diff --git a/docs/reviews/2026-06-11-deep-review-and-july-1-plan.adoc b/docs/reviews/2026-06-11-deep-review-and-july-1-plan.adoc index 750e76d..0404d6d 100644 --- a/docs/reviews/2026-06-11-deep-review-and-july-1-plan.adoc +++ b/docs/reviews/2026-06-11-deep-review-and-july-1-plan.adoc @@ -8,7 +8,7 @@ == Purpose and verdict -A full fresh review of VeriSimDB (Rust core, Elixir orchestration, VQL/VCL +A full fresh review of VeriSimDB (Rust core, Elixir orchestration, VCL/VCL surface, docs, CI), conducted 2026-06-11, with a targeted three-week plan to make the project genuinely plausible and respectable by 2026-07-01. The plan optimises for *truth and demonstrability*, not feature count: close the gap @@ -34,7 +34,7 @@ work is wiring, not invention. (this session). * Test culture is substantive: dedicated atomicity suite for the octad store, proptests on the WAL, insta snapshot tests on the planner, - criterion benches, a libfuzzer target for the VQL tokenizer. + criterion benches, a libfuzzer target for the VCL tokenizer. * Zero `todo!`/`unimplemented!`/`FIXME` in the Rust tree; several crates carry `#![forbid(unsafe_code)]`. @@ -109,7 +109,7 @@ EXPLAIN/EXPLAIN ANALYZE; wired into `/query/plan` + `/query/explain`. No executor consumes `PhysicalPlan` yet — honest framing needed. |verisim-api (9.0k, 53 tests) -|REAL CRUD/search/VQL; theatre at drift/normalize endpoints +|REAL CRUD/search/VCL; theatre at drift/normalize endpoints |REST + GraphQL + gRPC genuinely served. `/drift/status` returns initialized-to-zero metrics forever; `/drift/entity/{id}` returns global zeros labelled per-entity (`lib.rs:1189-1233`); `POST @@ -135,9 +135,9 @@ DynamicSupervisor, DriftMonitor, QueryRouter, SchemaRegistry, KRaft consensus node (single-node bootstrap), Federation Resolver. Transport defaults to HTTP. 14 federation adapters (237–650 LOC each) with real modality->capability mapping and optional native wire drivers (postgrex, -redix, exqlite, bolt_sips). VQL surface exists three times over: ReScript +redix, exqlite, bolt_sips). VCL surface exists three times over: ReScript (`src/vql`, incl. bidirectional type checker + proof obligations), Elixir -(`query/vql_*`), and the Rust planner bridge consuming the ReScript AST +(`query/vcl_*`), and the Rust planner bridge consuming the ReScript AST JSON. Coq models for Octad/Drift/Normalizer/Planner under `formal/` with a CI build. @@ -226,7 +226,7 @@ M = 1–2 days. `vcltotal-parse` already builds standalone (verified: 19/19 tests) and has a wire format + decider. Ship a tiny `vclt-gate` binary there (stdin: statement, stdout: verdict JSON with level-tagged reasons, - static levels L1–L4). VeriSimDB's VQL execute path invokes it when + static levels L1–L4). VeriSimDB's VCL execute path invokes it when present (env/feature-gated). The README triad becomes executable. . *Scripted demo II: admissibility (S).* Well-formed DECLARE/ASSERT admitted; malformed/unsafe statement rejected with reasons. Transcript diff --git a/docs/safety-and-fault-tolerance.adoc b/docs/safety-and-fault-tolerance.adoc index d9fa526..f68b7a6 100644 --- a/docs/safety-and-fault-tolerance.adoc +++ b/docs/safety-and-fault-tolerance.adoc @@ -1155,7 +1155,7 @@ Invariant: - link:error-handling-strategy.adoc[Error Handling Strategy] - link:reversibility-design.adoc[Reversibility Design] -- link:vcl-architecture.adoc[VQL Architecture] +- link:vcl-architecture.adoc[VCL Architecture] - link:../lib/verisim/supervisor.ex[Supervisor Tree Implementation] - https://www.erlang.org/doc/design_principles/des_princ.html[OTP Design Principles] - https://doc.rust-lang.org/book/ch04-01-what-is-ownership.html[Rust Ownership System] diff --git a/docs/status/implementation-plan.adoc b/docs/status/implementation-plan.adoc index 25e1d49..32e5a89 100644 --- a/docs/status/implementation-plan.adoc +++ b/docs/status/implementation-plan.adoc @@ -13,14 +13,14 @@ toc::[] * **Completion**: 10% * **Phase**: Implementation ramp-up -* **What exists**: Architecture docs, VQL grammar, Rust crate scaffolds, Elixir stubs -* **What's missing**: Actual modality store implementations, VQL execution engine +* **What exists**: Architecture docs, VCL grammar, Rust crate scaffolds, Elixir stubs +* **What's missing**: Actual modality store implementations, VCL execution engine == Goal **Week 16 target**: 70% completion - All 6 modality stores operational -- VQL execution engine working +- VCL execution engine working - Testing framework complete - Basic federation capability @@ -253,22 +253,22 @@ impl DriftDetector { --- -== Milestone V3: VQL Execution Engine (Weeks 9-11) +== Milestone V3: VCL Execution Engine (Weeks 9-11) -**Goal**: Execute VQL queries across all modalities +**Goal**: Execute VCL queries across all modalities === Week 9: Parser Integration ```rust // verisim-api/src/vql_bridge.rs -use rescript_parser::VQLParser; // ReScript → Rust FFI +use rescript_parser::VCLParser; // ReScript → Rust FFI -pub fn parse_vql(query: &str) -> Result; -pub fn execute_vql(ast: VQLAst, octad_store: &OctadStore) -> Result; +pub fn parse_vcl(query: &str) -> Result; +pub fn execute_vcl(ast: VCLAst, octad_store: &OctadStore) -> Result; ``` **Integration**: -- ReScript VQL parser → Rust execution engine +- ReScript VCL parser → Rust execution engine - AST serialization (CBOR or JSON) --- @@ -282,7 +282,7 @@ pub struct QueryPlan { pub estimated_cost: f64, } -pub fn plan_query(ast: VQLAst) -> Result; +pub fn plan_query(ast: VCLAst) -> Result; ``` **Optimization**: @@ -306,7 +306,7 @@ pub struct ExplainOutput { pub fn explain(query: &str) -> Result; ``` -**Deliverable**: VQL queries execute, EXPLAIN works +**Deliverable**: VCL queries execute, EXPLAIN works --- @@ -348,11 +348,11 @@ language: rust // fuzz/fuzz_targets/fuzz_vql.rs #![no_main] use libfuzzer_sys::fuzz_target; -use verisim_api::parse_vql; +use verisim_api::parse_vcl; fuzz_target!(|data: &[u8]| { if let Ok(s) = std::str::from_utf8(data) { - let _ = parse_vql(s); + let _ = parse_vcl(s); } }); ``` @@ -411,7 +411,7 @@ pub struct QueryCache { **Create**: - `QUICKSTART.adoc` - Get running in 5 minutes - `API-REFERENCE.adoc` - All Rust APIs documented -- `VQL-TUTORIAL.adoc` - 10 example queries +- `VCL-TUTORIAL.adoc` - 10 example queries - `DEPLOYMENT-GUIDE.adoc` - Standalone mode setup **Deliverable**: VeriSimDB at 70% completion @@ -475,7 +475,7 @@ cargo fuzz run fuzz_vql -- -max_total_time=300 - [ ] Completion: 40% → 55% ### Week 11 -- [ ] VQL execution engine complete +- [ ] VCL execution engine complete - [ ] EXPLAIN working - [ ] Completion: 55% → 65% @@ -502,7 +502,7 @@ cargo fuzz run fuzz_vql -- -max_total_time=300 **The only connection**: VeriSimDB could eventually federate to FormBD as an external data source: ```sql --- VQL federating to FormBD (future feature) +-- VCL federating to FormBD (future feature) SELECT * FROM octads@formbd_instance WHERE modality = 'document'; ``` diff --git a/docs/status/planner.md b/docs/status/planner.md index d148f4f..0655aa1 100644 --- a/docs/status/planner.md +++ b/docs/status/planner.md @@ -7,7 +7,7 @@ ## Overview Adding a cost-based query planner (`verisim-planner`) to VeriSimDB's Rust core, plus -triple API (REST + GraphQL + gRPC) and VQL integration. +triple API (REST + GraphQL + gRPC) and VCL integration. --- @@ -142,9 +142,9 @@ service VeriSimOctad { --- -## Phase 3: VQL AST → LogicalPlan Bridge — NOT STARTED +## Phase 3: VCL AST → LogicalPlan Bridge — NOT STARTED -**Plan:** Add `rust-core/verisim-planner/src/vql_bridge.rs` that deserializes the ReScript VQL AST JSON format into the planner's `LogicalPlan`. +**Plan:** Add `rust-core/verisim-planner/src/vql_bridge.rs` that deserializes the ReScript VCL AST JSON format into the planner's `LogicalPlan`. **Key mappings:** - `AST.modality` → `Modality` (direct, except `All` → expand to 6) @@ -153,7 +153,7 @@ service VeriSimOctad { - `AST.query.limit` → `PlanNode.early_limit` - `AST.query.proof` → proof obligation nodes (Phase 4) -**New endpoint:** `POST /query/vql` — accepts VQL AST JSON, returns PhysicalPlan. +**New endpoint:** `POST /query/vcl` — accepts VCL AST JSON, returns PhysicalPlan. **Feasibility:** YES — both sides use JSON serde. ~150-200 lines. @@ -210,7 +210,7 @@ service VeriSimOctad { ``` Phase 1 (DONE) ─┬─► Phase 2b (GraphQL) ├─► Phase 2c (gRPC) - ├─► Phase 3 (VQL Bridge) ──► Phase 4 (Proof Costing) + ├─► Phase 3 (VCL Bridge) ──► Phase 4 (Proof Costing) ├─► Phase 5 (Statistics) └─► Phase 6 (Cross-Modal) ``` @@ -226,7 +226,7 @@ All phases are independent except Phase 4 depends on Phase 3 (bridge must exist | 1. Planner crate | YES — DONE | Done | None | | 2b. GraphQL | YES | ~300 lines | Low — async-graphql is mature | | 2c. gRPC | YES | ~400 lines + proto | Low — tonic is mature | -| 3. VQL Bridge | YES | ~200 lines | Low — JSON↔JSON mapping | +| 3. VCL Bridge | YES | ~200 lines | Low — JSON↔JSON mapping | | 4. Proof Costing | YES | ~200 lines | Low — pure arithmetic | | 5. Stats Feedback | YES | ~150 lines | Low — extending existing code | | 6. Cross-Modal | YES | ~100 lines | Low — extending existing enums | diff --git a/docs/vcl-architecture.adoc b/docs/vcl-architecture.adoc index 864dbed..e0fd0c9 100644 --- a/docs/vcl-architecture.adoc +++ b/docs/vcl-architecture.adoc @@ -98,7 +98,7 @@ module VCL = { if (useDependentTypes) { // Dependent-Type Path rawQuery - -> VQLParser.parseToTypedAST + -> VCLParser.parseToTypedAST -> TypeChecker.validateWithProvenLibrary -> DriftMonitor.checkConsistency // Check for drift -> FederatedExecutor.executeWithZKP @@ -107,7 +107,7 @@ module VCL = { } else { // Slipstream Path rawQuery - -> VQLParser.parseToUntypedAST + -> VCLParser.parseToUntypedAST -> FederatedExecutor.executeUnverified -> TemporalLog.appendResult(queryId) // Still log (no proof) -> Response.withoutProof @@ -444,22 +444,22 @@ module Endpoint = { [source,rescript] // Client SDK for VCL -module VQLClient = { +module VCLClient = { type queryOptions = { useDependentTypes: bool, driftPolicy: option<[#Strict | #Repair | #Tolerate | #Latest]>, timeout: option, } - let query = async (vql: string, options: queryOptions) => { + let query = async (vcl: string, options: queryOptions) => { let headers = options.useDependentTypes - ? {"X-VCL-Safe": "true", "Content-Type": "text/vql"} - : {"Content-Type": "text/vql"} + ? {"X-VCL-Safe": "true", "Content-Type": "text/vcl"} + : {"Content-Type": "text/vcl"} let response = await fetch("/api/v1/query", { method: "POST", headers: headers, - body: vql, + body: vcl, }) let result = await response->Response.json @@ -480,7 +480,7 @@ module VQLClient = { // Usage example let searchPapers = async () => { - let vql = ` + let vcl = ` SELECT GRAPH, VECTOR FROM FEDERATION /universities/* WHERE (h)-[:CITES]->(target) @@ -489,7 +489,7 @@ let searchPapers = async () => { LIMIT 100 ` - let result = await VQLClient.query(vql, { + let result = await VCLClient.query(vcl, { useDependentTypes: true, driftPolicy: Some(#Repair), timeout: Some(30000), diff --git a/docs/vcl-examples.adoc b/docs/vcl-examples.adoc index c0a4091..ef3cf75 100644 --- a/docs/vcl-examples.adoc +++ b/docs/vcl-examples.adoc @@ -14,14 +14,14 @@ This document provides **63 comprehensive examples** of VCL queries and mutation === Example 1: Simple Octad Retrieval **Slipstream** (no proof): -[source,vql] +[source,vcl] ---- SELECT * FROM HEXAD 550e8400-e29b-41d4-a716-446655440000 ---- **Dependent-Type** (with proof): -[source,vql] +[source,vcl] ---- SELECT * FROM HEXAD 550e8400-e29b-41d4-a716-446655440000 @@ -31,7 +31,7 @@ PROOF EXISTENCE(ExistenceContract) === Example 2: Modality-Specific Selection **Graph Only:** -[source,vql] +[source,vcl] ---- SELECT GRAPH FROM HEXAD 550e8400-e29b-41d4-a716-446655440000 @@ -39,7 +39,7 @@ WHERE (h)-[:CITES]->(target) ---- **Vector Only:** -[source,vql] +[source,vcl] ---- SELECT VECTOR FROM HEXAD 550e8400-e29b-41d4-a716-446655440000 @@ -47,7 +47,7 @@ WHERE h.embedding SIMILAR TO [0.1, 0.2, 0.3, 0.4] ---- **Multiple Modalities:** -[source,vql] +[source,vcl] ---- SELECT GRAPH, VECTOR, SEMANTIC FROM HEXAD 550e8400-e29b-41d4-a716-446655440000 @@ -59,7 +59,7 @@ PROOF INTEGRITY(DataIntegrityContract) === Example 3: Citation Chain Traversal **Slipstream:** -[source,vql] +[source,vcl] ---- SELECT GRAPH FROM FEDERATION /universities/* @@ -69,7 +69,7 @@ LIMIT 100 ---- **Dependent-Type:** -[source,vql] +[source,vcl] ---- SELECT GRAPH FROM FEDERATION /universities/* WITH DRIFT STRICT @@ -82,7 +82,7 @@ LIMIT 100 === Example 4: Bidirectional Graph Traversal -[source,vql] +[source,vcl] ---- SELECT GRAPH FROM HEXAD abc12345-0000-0000-0000-000000000000 @@ -93,7 +93,7 @@ WHERE (h)-[:CO_AUTHOR]-(colleague) === Example 5: Property Graph Query -[source,vql] +[source,vcl] ---- SELECT GRAPH FROM STORE oxigraph-node-1 @@ -108,7 +108,7 @@ PROOF ACCESS(ReadAccessContract) === Example 6: Similarity Search (ANN) **Slipstream:** -[source,vql] +[source,vcl] ---- SELECT VECTOR FROM FEDERATION /embeddings/* @@ -117,7 +117,7 @@ LIMIT 10 ---- **Dependent-Type:** -[source,vql] +[source,vcl] ---- SELECT VECTOR FROM FEDERATION /embeddings/* WITH DRIFT REPAIR @@ -131,7 +131,7 @@ LIMIT 20 === Example 7: K-Nearest Neighbors -[source,vql] +[source,vcl] ---- SELECT VECTOR FROM HEXAD query-embedding-uuid @@ -141,7 +141,7 @@ WHERE h.embedding NEAREST 15 USING DOT_PRODUCT === Example 8: Filtered Vector Search -[source,vql] +[source,vcl] ---- SELECT VECTOR, DOCUMENT FROM FEDERATION /research-papers/* @@ -156,7 +156,7 @@ LIMIT 50 === Example 9: ZKP-Verified Access **Dependent-Type:** -[source,vql] +[source,vcl] ---- SELECT SEMANTIC, DOCUMENT FROM HEXAD confidential-data-uuid @@ -168,7 +168,7 @@ PROOF ACCESS(InstitutionalAccessContract) WITH verifier=ethics-board === Example 10: Provenance Verification **Dependent-Type:** -[source,vql] +[source,vcl] ---- SELECT SEMANTIC, TEMPORAL FROM FEDERATION /clinical-trials/* @@ -181,7 +181,7 @@ PROOF PROVENANCE(ClinicalTrialContract) === Example 11: Multi-Contract Validation **Dependent-Type:** -[source,vql] +[source,vcl] ---- SELECT * FROM HEXAD research-dataset-uuid @@ -196,7 +196,7 @@ PROOF CUSTOM(ComplianceContract) WITH auditor=legal-team === Example 12: Full-Text Search **Slipstream:** -[source,vql] +[source,vcl] ---- SELECT DOCUMENT FROM FEDERATION /archives/* @@ -205,7 +205,7 @@ LIMIT 1000 ---- **Dependent-Type:** -[source,vql] +[source,vcl] ---- SELECT DOCUMENT FROM FEDERATION /archives/* WITH DRIFT TOLERATE @@ -217,7 +217,7 @@ LIMIT 100 === Example 13: Regex Pattern Matching -[source,vql] +[source,vcl] ---- SELECT DOCUMENT FROM STORE tantivy-node-3 @@ -228,7 +228,7 @@ WHERE FULLTEXT MATCHES /\b(AI|ML|DL)\b.*ethics/ === Example 14: Structured Field Queries -[source,vql] +[source,vcl] ---- SELECT DOCUMENT, SEMANTIC FROM FEDERATION /journals/* @@ -241,7 +241,7 @@ WHERE FIELD doi LIKE "10.1234/%" === Example 15: Tensor Shape Filtering -[source,vql] +[source,vcl] ---- SELECT TENSOR FROM HEXAD tensor-data-uuid @@ -251,7 +251,7 @@ WHERE tensor.data SHAPE == [256, 256, 3] === Example 16: Tensor Operations -[source,vql] +[source,vcl] ---- SELECT TENSOR FROM STORE burn-node-2 @@ -265,7 +265,7 @@ WHERE tensor.data RANK == 3 === Example 17: Point-in-Time Query **Dependent-Type:** -[source,vql] +[source,vcl] ---- SELECT TEMPORAL, DOCUMENT FROM HEXAD legal-document-uuid @@ -275,7 +275,7 @@ PROOF PROVENANCE(TemporalContract) === Example 18: Version Range Query -[source,vql] +[source,vcl] ---- SELECT TEMPORAL, GRAPH FROM FEDERATION /contracts/* @@ -286,7 +286,7 @@ WHERE BETWEEN 2024-01-01T00:00:00Z AND 2024-12-31T23:59:59Z === Example 19: Specific Version **Dependent-Type:** -[source,vql] +[source,vcl] ---- SELECT * FROM HEXAD retracted-paper-uuid @@ -300,7 +300,7 @@ PROOF PROVENANCE(RetractionContract) === Example 20: Neurosymbolic AI Query **Dependent-Type:** -[source,vql] +[source,vcl] ---- -- Find papers similar to embedding that cite a specific work SELECT GRAPH, VECTOR, DOCUMENT @@ -317,7 +317,7 @@ LIMIT 50 === Example 21: Cross-Modal Consistency Check **Dependent-Type:** -[source,vql] +[source,vcl] ---- -- Verify document content matches vector embedding SELECT DOCUMENT, VECTOR, SEMANTIC @@ -332,7 +332,7 @@ PROOF INTEGRITY(CrossModalContract) === Example 22: Federated Provenance Audit **Dependent-Type:** -[source,vql] +[source,vcl] ---- -- Audit trail across multiple institutions SELECT TEMPORAL, SEMANTIC, GRAPH @@ -350,7 +350,7 @@ PROOF PROVENANCE(MultiInstitutionalContract) WITH auditor=nsf === Example 23: Strict Drift (Fail on Inconsistency) **Dependent-Type:** -[source,vql] +[source,vcl] ---- SELECT * FROM FEDERATION /legal-records/* WITH DRIFT STRICT @@ -363,7 +363,7 @@ PROOF INTEGRITY(LegalContract) === Example 24: Auto-Repair Drift **Dependent-Type:** -[source,vql] +[source,vcl] ---- SELECT GRAPH, DOCUMENT FROM FEDERATION /collaborative-wiki/* WITH DRIFT REPAIR @@ -377,7 +377,7 @@ PROOF EXISTENCE(WikiContract) === Example 25: Tolerate Drift (Return Inconsistent Data) **Slipstream:** -[source,vql] +[source,vcl] ---- SELECT * FROM FEDERATION /mirrors/* WITH DRIFT TOLERATE @@ -390,7 +390,7 @@ LIMIT 1000 === Example 26: Latest Version (Ignore Drift) **Slipstream:** -[source,vql] +[source,vcl] ---- SELECT DOCUMENT FROM FEDERATION /news-feeds/* WITH DRIFT LATEST @@ -404,7 +404,7 @@ LIMIT 10 === Example 27: Pagination for Large Result Sets -[source,vql] +[source,vcl] ---- SELECT DOCUMENT FROM FEDERATION /archives/* @@ -415,7 +415,7 @@ OFFSET 500 === Example 28: Store-Specific Query (Bypass Federation) -[source,vql] +[source,vcl] ---- -- Query specific store for lowest latency SELECT VECTOR @@ -425,7 +425,7 @@ WHERE h.embedding NEAREST 20 USING COSINE === Example 29: Minimal Modality Selection -[source,vql] +[source,vcl] ---- -- Only request needed modalities to reduce data transfer SELECT GRAPH(nodes, edges) @@ -438,7 +438,7 @@ WHERE (h)-[:CITES]->(target) === Example 30: Proof Verification Failure **Query:** -[source,vql] +[source,vcl] ---- SELECT SEMANTIC FROM HEXAD protected-data-uuid @@ -462,7 +462,7 @@ PROOF ACCESS(GuestAccessContract) === Example 31: Drift Detection Failure **Query:** -[source,vql] +[source,vcl] ---- SELECT * FROM FEDERATION /distributed-ledger/* WITH DRIFT STRICT @@ -486,7 +486,7 @@ WHERE AS OF 2024-01-01T00:00:00Z === Example 32: Malformed Query **Query:** -[source,vql] +[source,vcl] ---- SELECT GRAPH FROM HEXAD not-a-valid-uuid @@ -512,7 +512,7 @@ WHERE (h)-[:INVALID_SYNTAX === Example 33: Recursive Citation Network **Dependent-Type:** -[source,vql] +[source,vcl] ---- -- Find all papers in transitive citation closure SELECT GRAPH @@ -528,7 +528,7 @@ LIMIT 1000 === Example 34: Multi-Institutional Data Aggregation **Dependent-Type:** -[source,vql] +[source,vcl] ---- -- Aggregate COVID-19 data from multiple hospitals SELECT SEMANTIC, TEMPORAL, DOCUMENT @@ -544,7 +544,7 @@ PROOF PROVENANCE(MultiInstitutionalHealthContract) === Example 35: Real-Time Embeddings Query **Slipstream:** -[source,vql] +[source,vcl] ---- -- Fast similarity search for recommendation system SELECT VECTOR @@ -560,7 +560,7 @@ LIMIT 20 === Same Query, Two Paths **Slipstream (Fast, Unverified):** -[source,vql] +[source,vcl] ---- SELECT GRAPH, VECTOR FROM FEDERATION /papers/* @@ -570,7 +570,7 @@ LIMIT 100 ---- **Dependent-Type (Slow, Verified):** -[source,vql] +[source,vcl] ---- SELECT GRAPH, VECTOR FROM FEDERATION /papers/* WITH DRIFT STRICT @@ -637,7 +637,7 @@ Use slipstream path for: === Example 36: Version Pinning **Query with explicit VCL version:** -[source,vql] +[source,vcl] ---- VERSION 1.0; @@ -648,7 +648,7 @@ LIMIT 10; ---- **Query using deprecated syntax (with warning):** -[source,vql] +[source,vcl] ---- VERSION 0.9; -- Deprecated syntax accepted @@ -661,7 +661,7 @@ LIMIT 10; === Example 37: Federation Version Negotiation **Query with version compatibility check:** -[source,vql] +[source,vcl] ---- VERSION 1.0; @@ -677,7 +677,7 @@ LIMIT 100; === Example 38: Drift Detection **Detect cross-modal drift:** -[source,vql] +[source,vcl] ---- SELECT DRIFT FROM verisim:all_modalities @@ -693,7 +693,7 @@ WHERE octad.id = @octad_id; === Example 39: Drift Repair - Latest Wins **Repair using most recent version:** -[source,vql] +[source,vcl] ---- DRIFT REPAIR FROM verisim:graph @@ -704,7 +704,7 @@ USING STRATEGY latest_wins; === Example 40: Drift Repair - Quorum **Repair using majority voting:** -[source,vql] +[source,vcl] ---- DRIFT REPAIR FROM verisim:federation /universities/* @@ -715,7 +715,7 @@ USING STRATEGY quorum; === Example 41: Drift-Aware Query **Query with drift tolerance:** -[source,vql] +[source,vcl] ---- SELECT GRAPH, DOCUMENT FROM FEDERATION /universities/* @@ -727,7 +727,7 @@ LIMIT 100; === Example 42: Byzantine-Resistant Query **Query with drift repair:** -[source,vql] +[source,vcl] ---- SELECT GRAPH, DOCUMENT FROM FEDERATION /universities/* @@ -741,14 +741,14 @@ LIMIT 100; === Example 43: Column Selection within Modality **Select specific fields from a modality (slipstream):** -[source,vql] +[source,vcl] ---- SELECT DOCUMENT.name, DOCUMENT.severity FROM HEXAD 550e8400-e29b-41d4-a716-446655440000 ---- **Mixed modalities and column projections:** -[source,vql] +[source,vcl] ---- SELECT GRAPH, DOCUMENT.name, DOCUMENT.severity FROM FEDERATION /universities/* @@ -758,7 +758,7 @@ LIMIT 50 === Example 44: ORDER BY — Sort Results **Sort by severity descending:** -[source,vql] +[source,vcl] ---- SELECT DOCUMENT FROM STORE archive-1 @@ -768,7 +768,7 @@ LIMIT 50 ---- **Multi-field sort:** -[source,vql] +[source,vcl] ---- SELECT DOCUMENT.name, DOCUMENT.severity FROM FEDERATION /archives/* @@ -779,7 +779,7 @@ LIMIT 100 === Example 45: COUNT(*), SUM, AVG — Aggregate Functions **Count all matching octads:** -[source,vql] +[source,vcl] ---- SELECT COUNT(*) FROM FEDERATION /archives/* @@ -787,14 +787,14 @@ WHERE FULLTEXT CONTAINS "vulnerability" ---- **Aggregate with field reference:** -[source,vql] +[source,vcl] ---- SELECT AVG(DOCUMENT.severity), MIN(DOCUMENT.severity), MAX(DOCUMENT.severity) FROM FEDERATION /scans/* ---- **Sum and count together:** -[source,vql] +[source,vcl] ---- SELECT COUNT(*), SUM(DOCUMENT.severity) FROM STORE tantivy-node-1 @@ -804,7 +804,7 @@ WHERE FIELD severity > 3 === Example 46: GROUP BY / HAVING — Grouping with Filters **Group results by field:** -[source,vql] +[source,vcl] ---- SELECT DOCUMENT.name, COUNT(*), AVG(DOCUMENT.severity) FROM FEDERATION /universities/* @@ -813,7 +813,7 @@ LIMIT 100 ---- **GROUP BY with HAVING filter:** -[source,vql] +[source,vcl] ---- SELECT DOCUMENT.name, COUNT(*) FROM FEDERATION /archives/* @@ -826,7 +826,7 @@ LIMIT 50 === Example 47: Full SQL-Compatible Query **Combining all SQL-compatible features with VCL's model:** -[source,vql] +[source,vcl] ---- SELECT DOCUMENT.name, DOCUMENT.severity, COUNT(*), SUM(DOCUMENT.severity), AVG(DOCUMENT.severity) FROM FEDERATION /universities/* WITH DRIFT REPAIR @@ -841,7 +841,7 @@ OFFSET 20 === Example 48: SQL-Compatible with Dependent-Type Verification **Combining aggregates with formal verification (VCL-dt path):** -[source,vql] +[source,vcl] ---- SELECT DOCUMENT.name, COUNT(*) FROM FEDERATION /universities/* WITH DRIFT STRICT @@ -859,7 +859,7 @@ guarantee — the ZKP witnesses include the aggregate computation, ensuring veri === Example 49: Dual Proof — Existence and Integrity **Dependent-Type:** -[source,vql] +[source,vcl] ---- SELECT * FROM HEXAD 550e8400-e29b-41d4-a716-446655440000 @@ -872,7 +872,7 @@ are generated independently and composed into a single proof bundle. === Example 50: Triple Proof — Access, Provenance, and Integrity **Dependent-Type:** -[source,vql] +[source,vcl] ---- SELECT SEMANTIC, TEMPORAL, DOCUMENT FROM FEDERATION /hospitals/* WITH DRIFT STRICT @@ -888,7 +888,7 @@ must hold simultaneously. === Example 51: Citation and Custom Proof **Dependent-Type:** -[source,vql] +[source,vcl] ---- SELECT GRAPH, DOCUMENT FROM FEDERATION /journals/* WITH DRIFT REPAIR @@ -903,7 +903,7 @@ LIMIT 50 === Example 52: Cross-Modal Field Compare **Compare fields across modalities:** -[source,vql] +[source,vcl] ---- SELECT DOCUMENT, GRAPH FROM HEXAD 550e8400-e29b-41d4-a716-446655440000 @@ -916,7 +916,7 @@ field against the graph centrality field on the same octad. === Example 53: Drift Between Modalities **Detect embedding drift:** -[source,vql] +[source,vcl] ---- SELECT VECTOR, DOCUMENT FROM FEDERATION /research-papers/* @@ -930,7 +930,7 @@ document representation. Useful for identifying stale embeddings. === Example 54: Consistency Check **Verify cross-modal consistency:** -[source,vql] +[source,vcl] ---- SELECT VECTOR, SEMANTIC FROM HEXAD suspicious-entry-uuid @@ -944,7 +944,7 @@ using cosine similarity as the metric. === Example 55: Modality Existence Check **Filter by available modalities:** -[source,vql] +[source,vcl] ---- SELECT * FROM FEDERATION /archives/* @@ -959,7 +959,7 @@ identifying octads that need tensor representations generated. === Example 56: Combined Cross-Modal and Standard Conditions **Mix cross-modal with single-modality conditions:** -[source,vql] +[source,vcl] ---- SELECT GRAPH, VECTOR, DOCUMENT FROM FEDERATION /research-db/* WITH DRIFT REPAIR @@ -980,7 +980,7 @@ on full octad data. === Example 57: Insert a New Octad **Insert with document and vector data:** -[source,vql] +[source,vcl] ---- INSERT HEXAD WITH DOCUMENT(title = "New Research Paper", author = "Jane Doe", severity = 3), @@ -993,7 +993,7 @@ The octad ID is auto-generated and returned in the result. === Example 58: Insert with Graph Relationship **Insert with cross-modal data:** -[source,vql] +[source,vcl] ---- INSERT HEXAD WITH DOCUMENT(title = "Follow-Up Study", year = 2026), @@ -1007,7 +1007,7 @@ Creates a octad with document content, embedding, and a graph edge === Example 59: Verified Insert with Proof **Insert with integrity verification:** -[source,vql] +[source,vcl] ---- INSERT HEXAD WITH DOCUMENT(title = "Clinical Trial Result", status = "verified"), @@ -1022,7 +1022,7 @@ insert is verified and auditable. === Example 60: Update Octad Fields **Update specific fields:** -[source,vql] +[source,vcl] ---- UPDATE HEXAD 550e8400-e29b-41d4-a716-446655440000 SET DOCUMENT.title = "Corrected Title", DOCUMENT.severity = 5 @@ -1034,7 +1034,7 @@ Drift detection will fire if the change creates cross-modal inconsistency. === Example 61: Verified Update with Proof **Update with access proof:** -[source,vql] +[source,vcl] ---- UPDATE HEXAD 550e8400-e29b-41d4-a716-446655440000 SET DOCUMENT.status = "retracted", DOCUMENT.retraction_reason = "Data fabrication" @@ -1047,7 +1047,7 @@ of the retraction in the audit trail. === Example 62: Delete a Octad **Simple deletion:** -[source,vql] +[source,vcl] ---- DELETE HEXAD 550e8400-e29b-41d4-a716-446655440000 ---- @@ -1058,7 +1058,7 @@ in verisim-temporal for auditability. === Example 63: Verified Delete with Proof **Delete with access and provenance proof:** -[source,vql] +[source,vcl] ---- DELETE HEXAD 550e8400-e29b-41d4-a716-446655440000 PROOF ACCESS(AdminAccessContract) AND PROVENANCE(DeletionAuditContract) diff --git a/docs/vcl-formal-semantics.adoc b/docs/vcl-formal-semantics.adoc index a9e36d1..8715d74 100644 --- a/docs/vcl-formal-semantics.adoc +++ b/docs/vcl-formal-semantics.adoc @@ -617,7 +617,7 @@ Conditions compose via logical operators: Future versions may support **refinement predicates** in query syntax: -[source,vql] +[source,vcl] ---- SELECT GRAPH, VECTOR FROM verisim:semantic diff --git a/docs/vcl-type-system.adoc b/docs/vcl-type-system.adoc index 92744a0..fe1031c 100644 --- a/docs/vcl-type-system.adoc +++ b/docs/vcl-type-system.adoc @@ -778,7 +778,7 @@ Some VCL constructs support **type inference**: From vector literal: -[source,vql] +[source,vcl] ---- WHERE h.embedding SIMILAR TO [0.1, 0.2, 0.3] ---- @@ -789,7 +789,7 @@ Inferred: `Vector[3]` From conditions: -[source,vql] +[source,vcl] ---- WHERE h.embedding SIMILAR TO v WITHIN 0.8 ---- diff --git a/docs/vcl-vs-sql.adoc b/docs/vcl-vs-sql.adoc index ba06186..1df0ce3 100644 --- a/docs/vcl-vs-sql.adoc +++ b/docs/vcl-vs-sql.adoc @@ -134,7 +134,7 @@ WHERE id = '550e8400-e29b-41d4-a716-446655440000'; ---- **VCL (Slipstream):** -[source,vql] +[source,vcl] ---- SELECT * FROM HEXAD 550e8400-e29b-41d4-a716-446655440000 @@ -156,7 +156,7 @@ WHERE e1.id = '550e8400-e29b-41d4-a716-446655440000' ---- **VCL (graph traversal):** -[source,vql] +[source,vcl] ---- SELECT GRAPH FROM HEXAD 550e8400-e29b-41d4-a716-446655440000 @@ -176,7 +176,7 @@ WHERE to_tsvector('english', content) @@ to_tsquery('quantum & computing'); ---- **VCL:** -[source,vql] +[source,vcl] ---- SELECT DOCUMENT FROM STORE research_papers @@ -196,7 +196,7 @@ LIMIT 10; ---- **VCL:** -[source,vql] +[source,vcl] ---- SELECT VECTOR FROM STORE research_papers @@ -207,7 +207,7 @@ LIMIT 10 === Verified Query (No SQL Equivalent) **VCL-DT (dependent type path):** -[source,vql] +[source,vcl] ---- SELECT * FROM HEXAD 550e8400-e29b-41d4-a716-446655440000 diff --git a/docs/vcl-vs-vcl-dt.adoc b/docs/vcl-vs-vcl-dt.adoc index 304e176..6caff58 100644 --- a/docs/vcl-vs-vcl-dt.adoc +++ b/docs/vcl-vs-vcl-dt.adoc @@ -86,7 +86,7 @@ Use for: * **Performance-sensitive workloads** -- No proof generation cost Example: -[source,vql] +[source,vcl] ---- SELECT GRAPH, DOCUMENT FROM STORE research_papers @@ -108,7 +108,7 @@ Use for: * **Cross-instance federation** -- When trust is not assumed Example: -[source,vql] +[source,vcl] ---- SELECT * FROM HEXAD 550e8400-e29b-41d4-a716-446655440000 @@ -126,7 +126,7 @@ Every `PROOF` clause takes the form `PROOF ()`: Verifies the requested octad entity exists and has data in the requested modalities. -[source,vql] +[source,vcl] ---- PROOF EXISTENCE(ExistenceContract) ---- @@ -135,7 +135,7 @@ PROOF EXISTENCE(ExistenceContract) Verifies returned data matches stored data exactly (Merkle root / hash chain). -[source,vql] +[source,vcl] ---- PROOF INTEGRITY(DataIntegrityContract) ---- @@ -144,7 +144,7 @@ PROOF INTEGRITY(DataIntegrityContract) Verifies all modalities of the octad are mutually consistent (no drift). -[source,vql] +[source,vcl] ---- PROOF CONSISTENCY(CrossModalConsistencyContract) ---- @@ -153,7 +153,7 @@ PROOF CONSISTENCY(CrossModalConsistencyContract) Traces the chain of custody — creation, updates, drift repairs, normalizations. -[source,vql] +[source,vcl] ---- PROOF PROVENANCE(DataLineageContract) ---- @@ -162,7 +162,7 @@ PROOF PROVENANCE(DataLineageContract) Verifies data is no older than a specified time bound. -[source,vql] +[source,vcl] ---- PROOF FRESHNESS(FreshnessContract) ---- @@ -171,7 +171,7 @@ PROOF FRESHNESS(FreshnessContract) Verifies the requesting entity has appropriate permissions. -[source,vql] +[source,vcl] ---- PROOF AUTHORIZATION(AccessControlContract) ---- diff --git a/formal/CROSS-REPO-MAP.adoc b/formal/CROSS-REPO-MAP.adoc index 6cebf5e..ac34e8f 100644 --- a/formal/CROSS-REPO-MAP.adoc +++ b/formal/CROSS-REPO-MAP.adoc @@ -74,7 +74,7 @@ Concretely: | `EchoSearchExample.agda` (existing) — "find the witness" pattern + `EchoTruncation.agda` | The `winner` function is a SEARCH for the authoritative modality — exactly `EchoSearchExample`'s pattern. The `winner_stable_off_drifted` axiom is the "search result depends only on non-drifted modalities" — direct lift of `EchoTruncation`'s decoupling lemma. N2 idempotence is then "search is idempotent on its own result" — a *truncated echo* fixed point. -| V2 `vql_preservation` + `vql_progress` +| V2 `vcl_preservation` + `vcl_progress` | `formal/VCL.v` | `EchoGradedComonadInterface.agda` (existing) — graded comonad for "well-typed at type τ" | Type-preservation under reduction is the comonad ε ∘ δ = id property in the graded comonad of "well-typed terms at type τ". Reduction is the comonad action. The V2 mechanisation here is the MINIMUM-VIABLE core (booleans + opaque proof terms + conditional), closing #92 blockers 1 (big-step → small-step) and 2 (proof terms as values, no β-reduction). Full VCL extends mechanically per added expression form. Progress bundled as the type-soundness companion.