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

.claude/CLAUDE.md

@@ -41,7 +41,7 @@ cd src/abi && idris2 --check Proofs.idr
 
 - **TypeLL**: Type theory foundation — typed-wasm implements TypeLL's levels for WASM
 - **TypedQLiser**: Could become a TypedQLiser plugin (WASM as a "query target")
-- **VQL-UT**: Sibling project — same levels, different domain (database vs memory)
+- **VCL-total**: Sibling project — same levels, different domain (database vs memory)
 - **ECHIDNA**: Property-based testing of proof soundness
 - **GraalVM/Truffle**: Potential future target for the same approach
 

.github/workflows/dogfood-gate.yml

@@ -282,7 +282,7 @@ jobs:
           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

@@ -55,7 +55,7 @@ ____
 
 Uses the hyperpolymath type safety stack (Idris2 + TypeLL + 10-level verification). Same pattern across:
 - https://github.com/hyperpolymath/typedqliser[TypedQLiser] — 10 levels for database query languages (origin)
-- https://github.com/hyperpolymath/vql-ut[VQL-UT] — 10 levels for VeriSimDB
+- https://github.com/hyperpolymath/vql-ut[VCL-total] — 10 levels for VeriSimDB
 - https://github.com/hyperpolymath/typell[TypeLL] — Type theory foundation (shared)
 - https://github.com/hyperpolymath/echidna[ECHIDNA] — Property-based prover testing (integrated)
 

EXPLAINME.adoc

@@ -150,7 +150,7 @@ aspect coverage, and either complete or withdraw the higher-level claims.
 
 - https://github.com/hyperpolymath/typell[TypeLL] — Type theory foundation
 - https://github.com/hyperpolymath/typedqliser[TypedQLiser] — 10-level safety for query languages
-- https://github.com/hyperpolymath/vql-ut[VQL-UT] — 10-level safety for VeriSimDB
+- https://github.com/hyperpolymath/vql-ut[VCL-total] — 10-level safety for VeriSimDB
 - https://github.com/hyperpolymath/echidna[ECHIDNA] — Property-based prover testing
 
 == GraalVM Implications

README.adoc

@@ -60,7 +60,7 @@ Known audit constraints:
 == v0.4.0 -- Ecosystem Integration (Partially Complete)
 
 * [x] TypedQLiser plugin (WASM as a "query target") — typedqliser/src/plugins/wasm.rs (541 lines)
-* [ ] VQL-UT sibling integration (same levels, different domain)
+* [ ] VCL-total sibling integration (same levels, different domain)
 * [ ] GraalVM/Truffle target (multi-language shared state type safety)
 
 == v1.0.0 -- Stable Release

ROADMAP.adoc

@@ -514,12 +514,12 @@ offset, schema ID, generation counter (for lifetime tracking), and
 ownership flag in a 64-bit value.
 
 **ReScript parser.** The surface syntax parser is written in ReScript,
-consistent with the VQL-UT parser in the TypedQL ecosystem. ReScript
+consistent with the VCL-total parser in the TypedQL ecosystem. ReScript
 compiles to JavaScript/Wasm via Deno.
 
 **TypedQLiser integration.** typed-wasm implements the `QueryLanguagePlugin`
 trait from TypedQLiser, making Wasm memory a target alongside SQL,
-GraphQL, and VQL. This enables end-to-end verification: a database query
+GraphQL, and VCL. This enables end-to-end verification: a database query
 is type-checked by TypedQLiser, and the memory region holding its results
 is type-checked by typed-wasm.
 

docs/WHITEPAPER.md

@@ -196,7 +196,7 @@ proven safe before compilation to raw WASM instructions.
 
 === Implementation
 
-The parser is written in ReScript (consistent with VQL-UT) and produces a
+The parser is written in ReScript (consistent with VCL-total) and produces a
 typed abstract syntax tree. Parse failure at this level produces a clear
 error with source location.
 
@@ -647,7 +647,7 @@ does NOT address:
 | Segments with bounds checking
 | typed-wasm adds schema-level types, not just bounds
 
-| TypedQL / VQL-UT
+| TypedQL / VCL-total
 | Type-safe database queries
 | typed-wasm applies the same principle to memory, not databases
 

spec/type-safety-levels-for-wasm.adoc

@@ -8,7 +8,7 @@
 -- reference after its lifetime has ended (use-after-free) is a compile-time
 -- error, not a runtime crash.
 --
--- The database analogy: this is temporal safety. Just as VQL-UT's
+-- The database analogy: this is temporal safety. Just as VCL-total's
 -- FRESH WITHIN clause ensures data is temporally valid, typed-wasm's
 -- lifetimes ensure references are spatially valid — the memory they
 -- point to is still allocated.

src/abi/TypedWasm/ABI/Lifetime.idr

@@ -180,7 +180,7 @@ data NoDoubleFree : Type where
 
 ||| A resource that can be used exactly N times (generalisation of linear).
 ||| Linear is the special case where N = 1.
-||| This corresponds to VQL-UT's CONSUME AFTER N USE clause.
+||| This corresponds to VCL-total's CONSUME AFTER N USE clause.
 public export
 data BoundedUse : (remaining : Nat) -> Type where
   ||| A resource with N remaining uses.