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

hyperpolymath · claude · hyperpolymath · commit a3f38ec6b00f · 2026-04-05T16:49:23.000+01:00
Co-Authored-By: Claude Opus 4.6 (1M context) &lt;noreply@anthropic.com&gt;
diff --git a/.machine_readable/integrations/verisim.a2ml b/.machine_readable/integrations/verisim.a2ml
diff --git a/Cargo.toml b/Cargo.toml
@@ -66,7 +66,7 @@ uuid = { version = "1", features = ["v4", "serde"] }
 # Lazy statics
 lazy_static = "1"
 
-# VeriSimDB integration (optional — behind "verisimdb" feature)
+# VeriSimDB integration (optional — behind "verisim" feature)
 serde_cbor = { version = "0.11", optional = true }
 sha2 = { version = "0.10", optional = true }
 
@@ -79,7 +79,7 @@ tempfile = "3"
 [features]
 default = []
 chapel = []       # Enable Chapel parallel proof search (requires Zig FFI library)
-verisimdb = [     # Enable VeriSimDB persistent proof storage (8-modality octads)
+verisim = [     # Enable VeriSimDB persistent proof storage (8-modality octads)
     "dep:serde_cbor",
     "dep:sha2",
 ]
diff --git a/PROOF-NEEDS.md b/PROOF-NEEDS.md
@@ -13,7 +13,7 @@ following the pattern in repos like `typed-wasm`, `proven`, `echidna`, or `boj-s
 - **Axiom tracking completeness**: Proven in `verification/proofs/idris2/AxiomCompleteness.idr`. (23 patterns, no false negatives). `unsafeCoerce` added to `axiom_tracker.rs`.
 - **Prover dispatch correctness**: Proven in `verification/proofs/idris2/DispatchCorrectness.idr`. (Logic family compatibility). `DispatchOrdering.idr` (Pipeline stages).
 - **Proof composition**: Proven in `proofs/agda/ProofComposition.agda`. (Soundness preservation, axiom conflict detection).
-- **VQL-UT query safety**: Proven in `EchidnaABI/VqlUt.idr`. (L5 Injection-free, L3 Type-safe boundary).
+- **VCL-UT query safety**: Proven in `EchidnaABI/VqlUt.idr`. (L5 Injection-free, L3 Type-safe boundary).
 - **GNN embedding faithfulness**: Documented in `EchidnaABI/Gnn.idr`. (Structural properties, feature bounds, score normalisation).
 - Extensive Idris2 ABI: `EchidnaABI/Types.idr` (655 lines), `EchidnaABI/Foreign.idr` (445 lines), `EchidnaABI/Layout.idr` (236 lines)
 
@@ -22,7 +22,7 @@ following the pattern in repos like `typed-wasm`, `proven`, `echidna`, or `boj-s
 - **Axiom tracking completeness**: Prove `axiom_tracker.rs` detects ALL dangerous patterns (no false negatives for `sorry`, `Admitted`, `believe_me`, `postulate`, `assert_total`, `unsafeCoerce`)
 - **Prover dispatch correctness**: Prove that proof goals are dispatched to compatible provers (e.g., linear logic goals do not go to first-order ATP)
 - **GNN embedding faithfulness**: Prove that proof-graph GNN embeddings preserve structural properties of the original proof tree
-- **VQL-UT query safety**: Prove VQL queries are injection-free and type-safe at the ABI boundary
+- **VCL-UT query safety**: Prove VCL queries are injection-free and type-safe at the ABI boundary
 - **Proof composition**: Prove that combining sub-proofs from different provers preserves overall soundness (no implicit axiom conflicts)
 
 ## Recommended prover
diff --git a/docs/ECOSYSTEM-INTEGRATION.md b/docs/ECOSYSTEM-INTEGRATION.md
@@ -83,15 +83,15 @@ fleet.complete(findings.len(), errors, files_analyzed)?;
 **How It Works**:
 1. Run `panic-attack assail` on echidna repo
 2. Generate JSON output with weak points
-3. Run `verisimdb-data/scripts/ingest-scan.sh echidna /tmp/scan.json`
-4. Push to verisimdb-data repo
+3. Run `verisim-data/scripts/ingest-scan.sh echidna /tmp/scan.json`
+4. Push to verisim-data repo
 5. Hypatia processes findings and learns patterns
 
 **Command**:
 ```bash
 cd "$REPOS_DIR/echidna"        # Set REPOS_DIR to your local repos root
 panic-attack assail . --output /tmp/echidna-scan.json
-cd "$REPOS_DIR/verisimdb-data"
+cd "$REPOS_DIR/verisim-data"
 ./scripts/ingest-scan.sh echidna /tmp/echidna-scan.json
 git push && git push gitlab main
 ```
@@ -173,7 +173,7 @@ cd "$REPOS_DIR/gitbot-fleet"
 - Gitbot-fleet: `$REPOS_DIR/gitbot-fleet/`
 - Echidnabot: `$REPOS_DIR/echidna/echidnabot/`
 - Panic-attacker: `$REPOS_DIR/panic-attacker/`
-- VeriSimDB: `$REPOS_DIR/verisimdb-data/`
+- VeriSimDB: `$REPOS_DIR/verisim-data/`
 - Hypatia: `$REPOS_DIR/hypatia/`
 - Git-private-farm: `$REPOS_DIR/.git-private-farm/`
 
diff --git a/echidnabot/src/config.rs b/echidnabot/src/config.rs
@@ -73,7 +73,7 @@ fn default_host() -> String {
 fn default_port() -> u16 {
     // 9001 is echidnabot's canonical port in the hyperpolymath port map.
     // (9000 = echidna core, 9001 = echidnabot, 9090 = hypatia.)
-    // Was 8080 which collided with verisimdb and gitbot-fleet.
+    // Was 8080 which collided with verisim and gitbot-fleet.
     9001
 }
 
diff --git a/ffi/zig/src/provers/vcl_ut.zig b/ffi/zig/src/provers/vcl_ut.zig
diff --git a/llm-warmup-user.md b/llm-warmup-user.md
@@ -106,4 +106,4 @@ PMPL-1.0-or-later. Author: Jonathan D.A. Jewell.
 
 - **Depends on**: proven (verified safety), Z3/CVC5/Lean/etc. (solver binaries)
 - **Used by**: hypatia (CI/CD intelligence), ecosystem-wide proof checking
-- **Siblings**: panic-attacker (scanning), verisimdb (data layer)
+- **Siblings**: panic-attacker (scanning), verisim (data layer)
diff --git a/src/rust/agent/memory.rs b/src/rust/agent/memory.rs
@@ -234,11 +234,11 @@ impl ProofMemory for SqliteMemory {
 /// while maintaining an in-memory cache for fast find_similar lookups.
 /// Falls back gracefully to in-memory-only if VeriSimDB is unreachable.
 ///
-/// Enabled with `--features verisimdb` in Cargo.toml.
-#[cfg(feature = "verisimdb")]
+/// Enabled with `--features verisim` in Cargo.toml.
+#[cfg(feature = "verisim")]
 pub struct VeriSimDBProofStore {
     /// VeriSimDB HTTP client
-    client: crate::verisimdb_bridge::VeriSimDBClient,
+    client: crate::verisim_bridge::VeriSimDBClient,
 
     /// In-memory cache (fast lookups + fallback)
     local_successes: RwLock<Vec<CachedProof>>,
@@ -248,15 +248,15 @@ pub struct VeriSimDBProofStore {
     connected: RwLock<bool>,
 }
 
-#[cfg(feature = "verisimdb")]
+#[cfg(feature = "verisim")]
 impl VeriSimDBProofStore {
     /// Create a new VeriSimDB proof store.
     ///
     /// # Arguments
-    /// * `verisimdb_url` — Base URL of the VeriSimDB instance (e.g., "http://localhost:8081")
-    pub fn new(verisimdb_url: &str) -> Self {
+    /// * `verisim_url` — Base URL of the VeriSimDB instance (e.g., "http://localhost:8081")
+    pub fn new(verisim_url: &str) -> Self {
         VeriSimDBProofStore {
-            client: crate::verisimdb_bridge::VeriSimDBClient::new(verisimdb_url),
+            client: crate::verisim_bridge::VeriSimDBClient::new(verisim_url),
             local_successes: RwLock::new(Vec::new()),
             local_failures: RwLock::new(Vec::new()),
             connected: RwLock::new(false),
@@ -327,7 +327,7 @@ impl VeriSimDBProofStore {
     }
 }
 
-#[cfg(feature = "verisimdb")]
+#[cfg(feature = "verisim")]
 #[async_trait]
 impl ProofMemory for VeriSimDBProofStore {
     async fn store_success(
@@ -351,7 +351,7 @@ impl ProofMemory for VeriSimDBProofStore {
 
         // Build octad and send to VeriSimDB (best-effort)
         if *self.connected.read().await {
-            use crate::verisimdb_bridge::{ProofOctadBuilder, ProofStatus};
+            use crate::verisim_bridge::{ProofOctadBuilder, ProofStatus};
 
             // Fetch goal embedding from Julia inference service (best-effort)
             let embedding = self
@@ -398,7 +398,7 @@ impl ProofMemory for VeriSimDBProofStore {
 
         // Store failure in VeriSimDB (best-effort)
         if *self.connected.read().await {
-            use crate::verisimdb_bridge::{ProofOctadBuilder, ProofStatus};
+            use crate::verisim_bridge::{ProofOctadBuilder, ProofStatus};
 
             let prover = goal.preferred_prover.unwrap_or(ProverKind::Z3);
             let octad = ProofOctadBuilder::new(&goal.goal.id, &goal.goal, prover)
diff --git a/src/rust/lib.rs b/src/rust/lib.rs
@@ -20,14 +20,14 @@ pub mod integrity;
 pub mod llm; // Frontier LLM advisor (via BoJ Server)
 pub mod neural;
 pub mod parsers;
-#[cfg(feature = "verisimdb")]
+#[cfg(feature = "verisim")]
 pub mod proof_encoding; // CBOR encoding + proof identity hashing
 pub mod proof_search; // Chapel parallel proof search (optional feature)
 pub mod provers;
 pub mod verification;
-#[cfg(feature = "verisimdb")]
-pub mod verisimdb_bridge; // VeriSimDB 8-modality octad integration
-pub mod vql_ut; // VQL-UT: 10-level type-safe cross-prover query language
+#[cfg(feature = "verisim")]
+pub mod verisim_bridge; // VeriSimDB 8-modality octad integration
+pub mod vcl_ut; // VCL-UT: 10-level type-safe cross-prover query language
 
 pub use agent::{AgentConfig, AgentCore};
 pub use core::{ProofState, Tactic, TacticResult, Term};
diff --git a/src/rust/vcl_ut.rs b/src/rust/vcl_ut.rs
@@ -1,11 +1,11 @@
 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 // SPDX-License-Identifier: PMPL-1.0-or-later
 
-//! VQL-UT: Cross-Prover Query Language for ECHIDNA
+//! VCL-UT: Cross-Prover Query Language for ECHIDNA
 //!
 //! Typed query builder and executor for querying proof state across all 30
 //! prover backends via VeriSimDB's octad storage. Implements a subset of
-//! VQL-UT with progressive type safety enforcement.
+//! VCL-UT with progressive type safety enforcement.
 //!
 //! Query types:
 //!   - `FindProof` — retrieve a specific proof by theorem + prover
@@ -26,10 +26,10 @@ use tracing::{debug, info};
 
 use crate::provers::ProverKind;
 
-#[cfg(feature = "verisimdb")]
+#[cfg(feature = "verisim")]
 use crate::proof_encoding;
-#[cfg(feature = "verisimdb")]
-use crate::verisimdb_bridge::{OctadPayload, VeriSimDBClient};
+#[cfg(feature = "verisim")]
+use crate::verisim_bridge::{OctadPayload, VeriSimDBClient};
 
 // ═══════════════════════════════════════════════════════════════════════
 // Type Safety Levels
@@ -300,7 +300,7 @@ impl CrossProverQueryBuilder {
         // Level 7: Cardinality — must have a limit
         if level >= 7 && self.query.limit.is_none() {
             anyhow::bail!(
-                "VQL-UT Level {} requires a cardinality limit (use .with_limit())",
+                "VCL-UT Level {} requires a cardinality limit (use .with_limit())",
                 level
             );
         }
@@ -311,7 +311,7 @@ impl CrossProverQueryBuilder {
         // Level 9: Temporal safety — must have a version constraint
         if level >= 9 && self.query.min_version.is_none() {
             anyhow::bail!(
-                "VQL-UT Level {} requires a version constraint (use .with_min_version())",
+                "VCL-UT Level {} requires a version constraint (use .with_min_version())",
                 level
             );
         }
@@ -320,7 +320,7 @@ impl CrossProverQueryBuilder {
         // (enforced by VeriSimDB's provenance modality)
 
         debug!(
-            "VQL-UT query built: {:?} at level {} for {:?}",
+            "VCL-UT query built: {:?} at level {} for {:?}",
             self.query.operation, level, self.query.theorem_name,
         );
 
@@ -332,37 +332,37 @@ impl CrossProverQueryBuilder {
 // Query Executor
 // ═══════════════════════════════════════════════════════════════════════
 
-/// Executes VQL-UT queries against VeriSimDB.
+/// Executes VCL-UT queries against VeriSimDB.
 ///
-/// Uses the VeriSimDBClient from the verisimdb_bridge module when
-/// the `verisimdb` feature is enabled. Falls back to a no-op executor
+/// Uses the VeriSimDBClient from the verisim_bridge module when
+/// the `verisim` feature is enabled. Falls back to a no-op executor
 /// when VeriSimDB is not available.
 pub struct QueryExecutor {
-    #[cfg(feature = "verisimdb")]
+    #[cfg(feature = "verisim")]
     client: VeriSimDBClient,
 
-    #[cfg(not(feature = "verisimdb"))]
+    #[cfg(not(feature = "verisim"))]
     _phantom: std::marker::PhantomData<()>,
 }
 
 impl QueryExecutor {
     /// Create a new query executor.
-    #[cfg(feature = "verisimdb")]
-    pub fn new(verisimdb_url: &str) -> Self {
+    #[cfg(feature = "verisim")]
+    pub fn new(verisim_url: &str) -> Self {
         QueryExecutor {
-            client: VeriSimDBClient::new(verisimdb_url),
+            client: VeriSimDBClient::new(verisim_url),
         }
     }
 
     /// Create a new query executor (no VeriSimDB — stub mode).
-    #[cfg(not(feature = "verisimdb"))]
+    #[cfg(not(feature = "verisim"))]
     pub fn new(_verisimdb_url: &str) -> Self {
         QueryExecutor {
             _phantom: std::marker::PhantomData,
         }
     }
 
-    /// Validate a query against TypeLL's VQL-UT 10-level type checker.
+    /// Validate a query against TypeLL's VCL-UT 10-level type checker.
     ///
     /// Calls the TypeLL server at localhost:7800 to verify that the query
     /// meets its declared safety level. Returns the verified level and any
@@ -383,7 +383,7 @@ impl QueryExecutor {
             .context("Failed to create HTTP client for TypeLL")?;
 
         match client
-            .post(format!("{}/api/v1/vql-ut/check", typell_url))
+            .post(format!("{}/api/v1/vcl-ut/check", typell_url))
             .json(&check_body)
             .send()
             .await
@@ -409,11 +409,11 @@ impl QueryExecutor {
                                     .join("; ")
                             })
                             .unwrap_or_default();
-                        anyhow::bail!("TypeLL VQL-UT validation failed: {}", errors);
+                        anyhow::bail!("TypeLL VCL-UT validation failed: {}", errors);
                     }
 
                     info!(
-                        "TypeLL verified VQL-UT level {}/10 for {:?}",
+                        "TypeLL verified VCL-UT level {}/10 for {:?}",
                         max_level, query.operation,
                     );
 
@@ -459,7 +459,7 @@ impl QueryExecutor {
     /// execution. Falls back to local validation if TypeLL is unreachable.
     pub async fn execute(&self, query: &ProofQuery) -> Result<QueryResult> {
         info!(
-            "Executing VQL-UT query: {:?} at level {:?}",
+            "Executing VCL-UT query: {:?} at level {:?}",
             query.operation, query.level,
         );
 
@@ -493,7 +493,7 @@ impl QueryExecutor {
     async fn execute_find_proof(&self, query: &ProofQuery) -> Result<QueryResult> {
         let _theorem = query.theorem_name.as_deref().unwrap_or("");
 
-        #[cfg(feature = "verisimdb")]
+        #[cfg(feature = "verisim")]
         if let Some(prover) = query.prover {
             // Generate the octad key and look it up directly
             if let Some(ref goal_display) = query.goal_display {
@@ -529,7 +529,7 @@ impl QueryExecutor {
         let limit = query.limit.unwrap_or(10);
         let goal_display = query.goal_display.as_deref().unwrap_or("");
 
-        #[cfg(feature = "verisimdb")]
+        #[cfg(feature = "verisim")]
         {
             // Request a goal embedding from the Julia inference service
             let embedding = self
@@ -582,7 +582,7 @@ impl QueryExecutor {
         let theorem = query.theorem_name.as_deref().unwrap_or("");
         let limit = query.limit.unwrap_or(100);
 
-        #[cfg(feature = "verisimdb")]
+        #[cfg(feature = "verisim")]
         {
             let url = format!(
                 "{}/api/v1/search/text?q={}&limit={}",
@@ -624,7 +624,7 @@ impl QueryExecutor {
     /// Get the provenance trace for a proof.
     /// Calls VeriSimDB GET /api/v1/octads/{key} and extracts provenance modality.
     async fn execute_provenance(&self, query: &ProofQuery) -> Result<QueryResult> {
-        #[cfg(feature = "verisimdb")]
+        #[cfg(feature = "verisim")]
         if let Some(ref theorem) = query.theorem_name {
             if let Some(ref goal_display) = query.goal_display {
                 if let Some(prover) = query.prover {
@@ -668,7 +668,7 @@ impl QueryExecutor {
     async fn execute_dependency(&self, query: &ProofQuery) -> Result<QueryResult> {
         let limit = query.limit.unwrap_or(50);
 
-        #[cfg(feature = "verisimdb")]
+        #[cfg(feature = "verisim")]
         if let Some(ref theorem) = query.theorem_name {
             if let Some(ref goal_display) = query.goal_display {
                 if let Some(prover) = query.prover {
@@ -736,7 +736,7 @@ impl QueryExecutor {
 
     /// Fetch a goal embedding from the Julia inference service (port 8090).
     /// Returns a 512-dim f32 vector, or empty vec on failure.
-    #[cfg(feature = "verisimdb")]
+    #[cfg(feature = "verisim")]
     async fn fetch_goal_embedding(&self, goal_display: &str) -> Result<Vec<f32>> {
         let julia_url = std::env::var("ECHIDNA_JULIA_URL")
             .unwrap_or_else(|_| "http://localhost:8090".to_string());
@@ -774,7 +774,7 @@ impl QueryExecutor {
 }
 
 /// Convert a VeriSimDB search result JSON value to a QueryResultEntry.
-#[cfg(feature = "verisimdb")]
+#[cfg(feature = "verisim")]
 fn search_result_to_entry(value: &serde_json::Value) -> Option<QueryResultEntry> {
     Some(QueryResultEntry {
         key: value.get("key")?.as_str()?.to_string(),
@@ -852,7 +852,7 @@ mod urlencoding {
 }
 
 /// Convert an OctadPayload to a QueryResultEntry.
-#[cfg(feature = "verisimdb")]
+#[cfg(feature = "verisim")]
 fn octad_to_entry(octad: &OctadPayload) -> QueryResultEntry {
     QueryResultEntry {
         key: octad.key.clone(),
diff --git a/src/rust/verisim_bridge.rs b/src/rust/verisim_bridge.rs
@@ -17,7 +17,7 @@
 //!   - **Spatial**: Reserved for proof origin metadata (future)
 //!
 //! The bridge uses VeriSimDB's HTTP API via reqwest. For BoJ-integrated deployments,
-//! the V-lang adapter (`echidna_llm_verisimdb.v`) routes through verisimdb.zig FFI.
+//! the V-lang adapter (`echidna_llm_verisimdb.v`) routes through verisim.zig FFI.
 
 use anyhow::{Context, Result};
 use chrono::Utc;

Original file line number	Diff line number	Diff line change
`@@ -73,7 +73,7 @@ fn default_host() -> String {`
`73`	`73`	`fn default_port() -> u16 {`
`74`	`74`	`// 9001 is echidnabot's canonical port in the hyperpolymath port map.`
`75`	`75`	`// (9000 = echidna core, 9001 = echidnabot, 9090 = hypatia.)`
`76`		`- // Was 8080 which collided with verisimdb and gitbot-fleet.`
	`76`	`+ // Was 8080 which collided with verisim and gitbot-fleet.`
`77`	`77`	`9001`
`78`	`78`	`}`
`79`	`79`