refactor(rename): VQL → VCL + verisimdb → verisim

Ecosystem-consistency follow-on: matches the canonical rename landed
2026-04-05 in verisimdb, hypatia, gitbot-fleet, echidna, and vql-ut.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.github/workflows/dogfood-gate.yml

@@ -345,7 +345,7 @@ print(f'Valid: {project[\"name\"]} ({len(functions)} function(s))')
           fi
 
           # VeriSimDB integration?
-          if grep -rl 'verisimdb\|VeriSimDB' --include='*.toml' --include='*.yaml' --include='*.yml' --include='*.json' --include='*.rs' --include='*.ex' . 2>/dev/null | head -1 | grep -q .; then
+          if grep -rl 'verisim\|VeriSimDB' --include='*.toml' --include='*.yaml' --include='*.yml' --include='*.json' --include='*.rs' --include='*.ex' . 2>/dev/null | head -1 | grep -q .; then
             SCORE=$((SCORE + 1))
             VSDB_STATUS=":white_check_mark:"
           else

…ine_readable/integrations/verisimdb.a2ml …chine_readable/integrations/verisim.a2ml.machine_readable/integrations/verisimdb.a2ml renamed to .machine_readable/integrations/verisim.a2ml .machine_readable/integrations/verisimdb.a2ml renamed to .machine_readable/integrations/verisim.a2ml

@@ -4,7 +4,7 @@ name = "typedqliser"
 version = "0.1.0"
 edition = "2024"
 authors = ["Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"]
-description = "Add formal type safety (10 levels, dependent/linear/session types) to any query language — SQL, GraphQL, Cypher, SPARQL, VQL"
+description = "Add formal type safety (10 levels, dependent/linear/session types) to any query language — SQL, GraphQL, Cypher, SPARQL, VCL"
 license-file = "LICENSE"
 repository = "https://github.com/hyperpolymath/typedqliser"
 keywords = ["type-safety", "sql", "graphql", "formal-verification", "query"]

Cargo.toml

@@ -9,7 +9,7 @@ The README makes claims. This file backs them up.
 
 === Claim 1: 10-Level Type Safety for Any Query Language Without Modifying the Database
 
-*From README:* "TypedQLiser adds formal type safety to any query language — SQL, GraphQL, Cypher, SPARQL, KQL, VQL, or anything else — without modifying the database... Queries go in, TypedQLiser proves properties about them... and then passes the original query through unchanged. The database never knows it's there."
+*From README:* "TypedQLiser adds formal type safety to any query language — SQL, GraphQL, Cypher, SPARQL, KQL, VCL, or anything else — without modifying the database... Queries go in, TypedQLiser proves properties about them... and then passes the original query through unchanged. The database never knows it's there."
 
 *Evidence:* The core type system at `src/abi/` defines 10 levels of type safety as dependent types: Level 1 (Parse-time safety) proves syntactic validity; Level 2 (Schema-binding) proves table/field references exist; Level 3 (Type-compatible operations) proves no type mismatches; Level 4 (Null-safety) proves nullable paths are handled; Level 5 (Injection-proof) proves user input cannot alter query structure; Level 6 (Result-type safety) proves return type is known at compile time; Levels 7-10 (Cardinality, Effect-tracking, Temporal, Linearity) prove resource consumption and execution properties. The plugin architecture at `src/plugins/` allows each query language (SQL, GraphQL, Cypher, etc.) to provide its own parser and type rules. The critical property is that TypedQLiser is a compile-time tool, not a rewriter: the original query passes through unchanged to the database. See `docs/architecture.adoc` for proofs and type kernel design. **Caveat:** This is pre-alpha; only the architecture and Idris2 proof framework are designed. SQL and GraphQL plugins are priority but not yet implemented.
 
@@ -37,11 +37,11 @@ The README makes claims. This file backs them up.
 TypedQLiser is the #1 priority in the -iser ecosystem (TypedQLiser → Chapeliser → VeriSimiser → Squeakwell). Uses:
 - **Idris2 ABI + Zig FFI standard** — Same architecture as https://github.com/hyperpolymath/proven[proven], https://github.com/hyperpolymath/gossamer[gossamer], https://github.com/hyperpolymath/idaptik[idaptik]
 - **TypeLL type theory** — Shared foundation for all query type checking
-- **VQL-UT** — Can be deployed as a TypedQLiser plugin for VeriSimDB queries
+- **VCL-total** — Can be deployed as a TypedQLiser plugin for VeriSimDB queries
 
 Related projects:
 - https://github.com/hyperpolymath/typell[TypeLL] — Type theory foundation (10 levels)
-- https://github.com/hyperpolymath/vql-ut[VQL-UT] — VQL-specific type safety (VeriSimDB queries)
+- https://github.com/hyperpolymath/vql-ut[VCL-total] — VCL-specific type safety (VeriSimDB queries)
 - https://github.com/hyperpolymath/iseriser[-iser ecosystem] — Meta-framework for domain-specific query tools
 
 == File Map
@@ -61,7 +61,7 @@ Related projects:
 | `src/plugins/graphql.rs` | GraphQL plugin — Level 6 support
 | `src/plugins/cypher.rs` | Cypher plugin (Neo4j, Memgraph, AGE) — Level 4 support (planned)
 | `src/plugins/sparql.rs` | SPARQL plugin (RDF triplestores) — Level 4 support (planned)
-| `src/plugins/vql.rs` | VQL plugin (VeriSimDB) — Level 10 support (planned, via VQL-UT)
+| `src/plugins/vcl.rs` | VCL plugin (VeriSimDB) — Level 10 support (planned, via VCL-total)
 | `src/manifest.rs` | TOML manifest parser for typedqliser.toml
 | `src/schema.rs` | Schema representation and introspection handling
 | `src/ast.rs` | Abstract syntax tree types (language-agnostic)

EXPLAINME.adoc

@@ -35,7 +35,7 @@
 
 ## Priority
 
-**MEDIUM** — Code generator correctness is important but downstream of VQL-UT and TypeLL. Focus proofs on SQL generation first as it directly affects data integrity.
+**MEDIUM** — Code generator correctness is important but downstream of VCL-total and TypeLL. Focus proofs on SQL generation first as it directly affects data integrity.
 
 ## Template ABI Cleanup (2026-03-29)
 

PROOF-NEEDS.md

@@ -10,7 +10,7 @@ Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 == What Is This?
 
 TypedQLiser adds **formal type safety** to any query language — SQL, GraphQL,
-Cypher, SPARQL, KQL, VQL, or anything else — without modifying the database.
+Cypher, SPARQL, KQL, VCL, or anything else — without modifying the database.
 
 It sits in front of your database as a compile-time type checker. Queries go in,
 TypedQLiser proves properties about them (no nulls where you don't expect them,
@@ -29,14 +29,14 @@ Every database has a query language. None of them have deep type safety:
 * **GraphQL**: Schema types exist but no dependent types, no linearity, no effects
 * **Cypher**: Pattern matching with no formal verification
 * **SPARQL**: RDF types are stringly-typed at best
-* **VQL**: VeriSimDB's query language has VQL-DT/VQL-UT extensions, but they're VQL-specific
+* **VCL**: VeriSimDB's query language has VCL-DT/VCL-total extensions, but they're VCL-specific
 
 TypedQLiser makes the type safety **portable across all query languages**.
 
 == The 10 Type Safety Levels
 
 Derived from https://github.com/hyperpolymath/typell[TypeLL]'s type theory
-and https://github.com/hyperpolymath/vql-ut[VQL-UT]'s 10-level hierarchy:
+and https://github.com/hyperpolymath/vql-ut[VCL-total]'s 10-level hierarchy:
 
 === Established (Levels 1-6)
 
@@ -113,7 +113,7 @@ TypedQLiser uses a plugin architecture. Each query language gets a parser plugin
 | **GraphQL** | Any GraphQL API | 6 | Priority
 | **Cypher** | Neo4j, Memgraph, AGE | 4 | Planned
 | **SPARQL** | Any RDF triplestore | 4 | Planned
-| **VQL** | VeriSimDB | 10 | Planned (via VQL-UT)
+| **VCL** | VeriSimDB | 10 | Planned (via VCL-total)
 | **KQL** | Azure Data Explorer, Kusto | 4 | Planned
 | **GQL** | ISO GQL databases | 4 | Planned
 | **FQLDT** | Lithoglyph | 10 | Planned (dependent types native)
@@ -233,13 +233,13 @@ typedqliser check --ci
 typedqliser info
 ----
 
-== Relationship to TypeLL, VQL-UT, and the -iser Family
+== Relationship to TypeLL, VCL-total, and the -iser Family
 
 * **TypeLL** provides the type theory (10 levels, type kernel, verification protocol)
-* **VQL-UT** applies those levels specifically to VeriSimDB's VQL
+* **VCL-total** applies those levels specifically to VeriSimDB's VCL
 * **TypedQLiser** makes them portable to *any* query language
 * TypedQLiser's Idris2 kernel can use TypeLL as a shared dependency
-* VQL-UT becomes the VQL plugin within TypedQLiser
+* VCL-total becomes the VCL plugin within TypedQLiser
 
 == Status
 

README.adoc

@@ -128,8 +128,8 @@ pub fn print_languages() {
         "wasm", "WebAssembly linear memory (typed-wasm)", "10"
     );
     println!(
-        "  {:12} {:40} {:10} Planned (via VQL-UT)",
-        "vql", "VeriSimDB", "10"
+        "  {:12} {:40} {:10} Planned (via VCL-total)",
+        "vcl", "VeriSimDB", "10"
     );
     println!(
         "  {:12} {:40} {:10} Planned",