chore(rename): VQL → VCL + VQL-dt++ → VCL-UT estate-wide

VQL (old name) is now VCL (VeriSim Consonance Language) everywhere.
The type-theoretic extension VQL-dt++ is now VCL-UT (matching the
.vclut file extension already in use).

Changed:
- nqc/spec/SPEC.core.scm: profile id vql→vcl, path /vql/→/vcl/, docs
- nqc/ffi/zig/src/main.zig: DatabaseId enum .vql→.vcl, execute path
- nqc/web/nqc-web.desktop: Keywords vql→vcl
- typeql-experimental/typeql-experimental.ipkg: brief updated
- typeql-experimental/ffi/zig/src/bridge.zig: comment updated
- typeql-experimental/examples/*.vclut: VQL-dt++→VCL-UT, VQL base→VCL base
- verisimdb/.github/CODEOWNERS: /src/vql/→/src/vcl/
- PROOF-NEEDS.md: V2/V3 labels updated

Note: nqc/web/src/Database.res.mjs is a generated build artifact;
the source Database.res already uses VCL — regenerate to sync.

Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>

Author: hyperpolymath

PROOF-NEEDS.md

@@ -15,8 +15,8 @@
 | # | Component | Prover | Notes |
 |---|-----------|--------|-------|
 | V1 | Octad coherence invariant | I2 | 8 modalities mutually consistent post-operation |
-| V2 | VQL type inference soundness | Cq/L4 | Bidirectional inference correct |
-| **V3** | **VQL subtyping transitivity + decidability** | **L4** | **DONE 2026-04-11** — `verisimdb/verification/proofs/lean4/VCLSubtyping.lean` |
+| V2 | VCL type inference soundness | Cq/L4 | Bidirectional inference correct |
+| **V3** | **VCL subtyping transitivity + decidability** | **L4** | **DONE 2026-04-11** — `verisimdb/verification/proofs/lean4/VCLSubtyping.lean` |
 | **V4** | **Raft consensus safety** | **L4** | **DONE 2026-04-11** — `verisimdb/verification/proofs/lean4/RaftSafety.lean` (single-node; distributed in TLA+) |
 | V5 | Transaction atomicity | TLA | All-or-nothing across 8 modalities |
 

nqc/ffi/zig/src/main.zig

@@ -59,15 +59,15 @@ pub fn formatToString(fmt: OutputFormat) []const u8 {
 
 /// Known database backend identifiers, matching Layout.idr tag values.
 pub const DatabaseId = enum(u8) {
-    vql = 0,
+    vcl = 0,
     gql = 1,
     kql = 2,
 };
 
 /// Default port for each database.
 pub fn defaultPort(db: DatabaseId) u16 {
     return switch (db) {
-        .vql => 8080,
+        .vcl => 8080,
         .gql => 8081,
         .kql => 8082,
     };
@@ -76,7 +76,7 @@ pub fn defaultPort(db: DatabaseId) u16 {
 /// Execute path for each database.
 pub fn executePath(db: DatabaseId) []const u8 {
     return switch (db) {
-        .vql => "/vql/execute",
+        .vcl => "/vcl/execute",
         .gql => "/gql/execute",
         .kql => "/kql/execute",
     };
@@ -310,13 +310,13 @@ test "formatToString roundtrips" {
 }
 
 test "defaultPort values" {
-    try std.testing.expectEqual(@as(u16, 8080), defaultPort(.vql));
+    try std.testing.expectEqual(@as(u16, 8080), defaultPort(.vcl));
     try std.testing.expectEqual(@as(u16, 8081), defaultPort(.gql));
     try std.testing.expectEqual(@as(u16, 8082), defaultPort(.kql));
 }
 
 test "executePath values" {
-    try std.testing.expectEqualStrings("/vql/execute", executePath(.vql));
+    try std.testing.expectEqualStrings("/vcl/execute", executePath(.vcl));
     try std.testing.expectEqualStrings("/gql/execute", executePath(.gql));
     try std.testing.expectEqualStrings("/kql/execute", executePath(.kql));
 }

nqc/spec/SPEC.core.scm

@@ -52,9 +52,9 @@
     (type DatabaseProfile
       (doc "Everything NQC needs to know about a database backend.")
       (fields
-        (id            String   (doc "Short identifier, e.g. 'vql'. Must be unique."))
+        (id            String   (doc "Short identifier, e.g. 'vcl'. Must be unique."))
         (display-name  String   (doc "Human-readable name, e.g. 'VeriSimDB'."))
-        (language-name String   (doc "Query language name, e.g. 'VQL'."))
+        (language-name String   (doc "Query language name, e.g. 'VCL'."))
         (description   String   (doc "Short description for menus."))
         (aliases       (List String) (doc "Alternative names for lookup."))
         (default-host  String   (doc "Default server hostname."))
@@ -179,13 +179,13 @@
     ;; --- Built-in profiles ---
 
     (builtin-profiles
-      (profile vql
+      (profile vcl
         (display-name "VeriSimDB")
-        (language-name "VQL")
+        (language-name "VCL")
         (description "6-core multimodal database with self-normalization")
         (aliases "verisimdb" "verisim")
         (default-port 8080)
-        (execute-path "/vql/execute")
+        (execute-path "/vcl/execute")
         (supports-dt #t))
 
       (profile gql
@@ -254,7 +254,7 @@
     (format table
       (doc "ASCII table with auto-detected columns.")
       (algorithm
-        (step 1 "Extract 'data' field if present (VQL response shape),"
+        (step 1 "Extract 'data' field if present (VCL response shape),"
                 "otherwise use raw value.")
         (step 2 "Coerce to list. If not a list, format as single object"
                 "or fall back to JSON.")

nqc/web/nqc-web.desktop

@@ -12,5 +12,5 @@ Exec=bash -c 'cd /var$REPOS_DIR/nextgen-databases/nqc/web && bash nqc-launcher.s
 Terminal=true
 Icon=utilities-terminal
 Categories=Development;Database;
-Keywords=database;query;vql;gql;kql;verisimdb;lithoglyph;quandledb;
+Keywords=database;query;vcl;gql;kql;verisimdb;lithoglyph;quandledb;
 StartupNotify=true

typeql-experimental/examples/01-linear-connection.vclut

@@ -1,4 +1,4 @@
--- VQL-dt++ Example 01: Linear Connection (CONSUME AFTER N USE)
+-- VCL-UT Example 01: Linear Connection (CONSUME AFTER N USE)
 -- SPDX-License-Identifier: PMPL-1.0-or-later
 --
 -- This example demonstrates resource-counted connections via linear types.

typeql-experimental/examples/02-session-protocol.vclut

@@ -1,4 +1,4 @@
--- VQL-dt++ Example 02: Session Protocol (WITH SESSION)
+-- VCL-UT Example 02: Session Protocol (WITH SESSION)
 -- SPDX-License-Identifier: PMPL-1.0-or-later
 --
 -- This example demonstrates session type protocols. The WITH SESSION clause

typeql-experimental/examples/03-effect-tracking.vclut

@@ -1,4 +1,4 @@
--- VQL-dt++ Example 03: Effect Tracking (EFFECTS { ... })
+-- VCL-UT Example 03: Effect Tracking (EFFECTS { ... })
 -- SPDX-License-Identifier: PMPL-1.0-or-later
 --
 -- This example demonstrates declarative effect tracking. The EFFECTS clause

typeql-experimental/examples/04-modal-scoping.vclut

@@ -1,4 +1,4 @@
--- VQL-dt++ Example 04: Modal Scoping (IN TRANSACTION)
+-- VCL-UT Example 04: Modal Scoping (IN TRANSACTION)
 -- SPDX-License-Identifier: PMPL-1.0-or-later
 --
 -- This example demonstrates world-indexed access scoping via modal types.

typeql-experimental/examples/05-proof-attachment.vclut

@@ -1,13 +1,13 @@
--- VQL-dt++ Example 05: Proof Attachment (PROOF ATTACHED)
+-- VCL-UT Example 05: Proof Attachment (PROOF ATTACHED)
 -- SPDX-License-Identifier: PMPL-1.0-or-later
 --
 -- This example demonstrates proof-carrying code. The PROOF ATTACHED clause
 -- attaches a formal theorem to the query result. The result type becomes a
 -- sigma pair: (result, proof) where the proof certifies a property.
 --
--- This is DIFFERENT from VQL's existing PROOF clause:
---   PROOF EXISTENCE(...)       — pre-condition verification (VQL base)
---   PROOF ATTACHED theorem     — post-condition proof attachment (VQL-dt++)
+-- This is DIFFERENT from VCL's existing PROOF clause:
+--   PROOF EXISTENCE(...)       — pre-condition verification (VCL base)
+--   PROOF ATTACHED theorem     — post-condition proof attachment (VCL-UT)
 --
 -- Available theorems:
 --   IntegrityTheorem    — result data has not been tampered with

typeql-experimental/examples/06-usage-limit.vclut

@@ -1,13 +1,13 @@
--- VQL-dt++ Example 06: Usage Limit (USAGE LIMIT)
+-- VCL-UT Example 06: Usage Limit (USAGE LIMIT)
 -- SPDX-License-Identifier: PMPL-1.0-or-later
 --
 -- This example demonstrates quantitative type theory for resource budgeting.
 -- The USAGE LIMIT clause caps the total resource consumption across the
 -- entire query plan — connections, API calls, compute units, etc.
 --
--- This is DIFFERENT from VQL's LIMIT clause:
---   LIMIT 50          — caps result row count (VQL base)
---   USAGE LIMIT 100   — caps resource consumption (VQL-dt++)
+-- This is DIFFERENT from VCL's LIMIT clause:
+--   LIMIT 50          — caps result row count (VCL base)
+--   USAGE LIMIT 100   — caps resource consumption (VCL-UT)
 --
 -- The type system tracks consumption through the query plan and rejects
 -- plans that exceed the budget.