Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 4 additions & 4 deletions CONTRIBUTING.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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

Expand Down
44 changes: 22 additions & 22 deletions KNOWN-ISSUES.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand All @@ -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.

Expand Down Expand Up @@ -145,27 +145,27 @@ 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.

**Original issue:** All six condition detection and extraction functions were stubs (returning `false` and hardcoded values), causing every query to be routed as a multi-modal query even when a single modality was targeted.

=== 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

Expand All @@ -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`.

Expand All @@ -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.

Expand All @@ -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).

Expand All @@ -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

Expand Down
48 changes: 24 additions & 24 deletions ROADMAP.md
Original file line number Diff line number Diff line change
Expand Up @@ -5,41 +5,41 @@ 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
- [x] ZKP scheme decision: PLONK (documented in Trustfile)

---

## 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
Expand All @@ -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`

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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

Expand All @@ -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)
Expand Down Expand Up @@ -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 |
Expand Down
8 changes: 4 additions & 4 deletions TESTING.md
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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`

Expand Down Expand Up @@ -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
Expand All @@ -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.
2 changes: 1 addition & 1 deletion connectors/README.adoc
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
Loading
Loading