You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Sweeps the documentation-prose half of the VQL->VCL rename, staged
separately from code per the repo's own doc-consonance policy
(tests/doc-consonance-gate.sh: code identifiers and changelog history are
out of scope for the docs gate and tracked under #84).
Renamed across 50 prose docs (.adoc/.md):
- Language name "VQL" -> "VCL" (incl. "VQL-DT" -> "VCL-DT" where it names
the language); [source,vql] / ```vql fence tags -> vcl.
- Stale Stage-C Elixir identifiers updated to match merged reality (#136):
vql_{executor,bridge,type_checker,proof_certificate}.ex -> vcl_*.ex;
VeriSim.Query.VQL{Executor,Bridge,TypeChecker,ProofCertificate} -> VCL*.
Deliberately preserved (unrenamed code + wire contracts -> Stage B):
- ReScript src/vql/VQL*.res, VeriSimVql, VqlKeywords
- Rust vql.rs / vql_bridge.rs / vql_fmt.rs, Julia vql.jl, Zig vql.zig
- fuzz target fuzz_vql_parser, .vql example files, examples/vql-queries
- API path /api/v1/vql/execute, header X-VQL-Version, type:vql_query tag
- CHANGELOG.adoc (allow-listed history), docs/papers/*.{tex,bib} (citation
integrity), *.a2ml machine-readable metadata
Verified: doc-consonance gate stays GREEN (no "VeriSim Query Language"
misnomer); no vql/vcl xref or anchor breakage; every residual "vql" token
is an intentionally-preserved Stage-B identifier/contract; symmetric
533/533 diff (equal-length token swaps, no structural change).
Refs #84.
https://claude.ai/code/session_01W9Voe3JceP66Bna9FT4jME
**Resolved:** 2026-02-28. VCL-DT proof pipeline is now fully wired end-to-end with a three-tier type checking strategy:
58
58
59
-
1. **ReScript bidirectional type checker** (VQLBidir.res, 852 lines) — full formal system with subtyping, invoked via VQLBridge.typecheck/2 when Deno subprocess available
60
-
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.
59
+
1. **ReScript bidirectional type checker** (VQLBidir.res, 852 lines) — full formal system with subtyping, invoked via VCLBridge.typecheck/2 when Deno subprocess available
60
+
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.
61
61
3. **Bare AST extraction** — last resort, no longer needed since the native checker handles all cases
- `zkp_bridge.rs` (628 LOC) — wires ZKP primitives to the `ProofBlob`/`SemanticStore` types so CBOR-encoded `VerifiableProofData` round-trips through the semantic modality.
81
81
- `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.
82
-
- 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`).
83
-
- 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.
82
+
- 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`).
83
+
- 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.
84
84
85
85
**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.
86
86
@@ -145,27 +145,27 @@ Added `rescript.json` for build configuration.
145
145
146
146
=== 12. Cross-Modal Drift/Consistency Were Stubs — ✅ RESOLVED
**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).
151
151
152
152
**Original issue:** Cross-modal correlation queries parsed correctly but evaluation returned fake scores, making WHERE DRIFT(...) and CONSISTENT(...) conditions meaningless.
153
153
154
-
=== 13. VQL WHERE Condition Routing Was Broken — ✅ RESOLVED
154
+
=== 13. VCL WHERE Condition Routing Was Broken — ✅ RESOLVED
**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.
159
159
160
160
**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.
**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`.
167
167
168
-
**Original issue:** PROOF clauses in VQL queries were parsed but never verified. All proofs silently passed, making the entire proof system decorative.
168
+
**Original issue:** PROOF clauses in VCL queries were parsed but never verified. All proofs silently passed, making the entire proof system decorative.
169
169
170
170
=== 15. believe_me in Idris2 ABI Files — ✅ RESOLVED
171
171
@@ -175,9 +175,9 @@ Added `rescript.json` for build configuration.
175
175
176
176
**Original issue:** `registerCallback` used `believe_me` to cast a callback function to `AnyPtr`, a BANNED unsafe pattern that bypasses the type checker.
177
177
178
-
=== 16. Atom Table Exhaustion Risk in VQL Bridge — ✅ RESOLVED
178
+
=== 16. Atom Table Exhaustion Risk in VCL Bridge — ✅ RESOLVED
**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`.
183
183
@@ -193,15 +193,15 @@ Added `rescript.json` for build configuration.
193
193
194
194
=== 18. EXPLAIN Returns Hardcoded Plan — ✅ RESOLVED
**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.
199
199
200
200
**Original issue:** EXPLAIN returned a static plan with hardcoded step names and costs totalling 71ms, regardless of the actual query structure.
**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.
207
207
@@ -214,14 +214,14 @@ Added `rescript.json` for build configuration.
214
214
- Circuit Registry: named circuit storage with register/get/verify/list/unregister operations
**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).
227
227
@@ -231,7 +231,7 @@ Added `rescript.json` for build configuration.
**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.
234
+
**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.
235
235
236
236
=== 23. verisim-repl Has Build Issues — ✅ RESOLVED
0 commit comments