Skip to content

TOOLING-STATUS.adoc

Latest commit

 

History

History
174 lines (132 loc) · 5.33 KB

TOOLING-STATUS.adoc

File metadata and controls

174 lines (132 loc) · 5.33 KB

Nextgen Databases — Query Languages & Integration Status

Table of Contents

Last verified: 2026-03-21

Overview

This monorepo contains 5 database engines, each with its own query language. Three are registered in the BoJ Server database-mcp cartridge with connection management, query execution, and PanLL dashboard panels.

Database & Query Language Matrix

Database Query Language BoJ ID Status Key Components

VeriSimDB

VCL (Verified Query Language)

1

Mature

10 ReScript modules: Parser, TypeChecker, BiDir, Subtyping, ProofObligation, Circuit, Explain, Context, Error, Types

LithoGlyph

GQL (Graph Query Language)

6

Beta

Graph algebra in src/Lith/, GQL execution via database-mcp

QuandleDB

KQL (Knot Query Language)

5

Early

Connector-based architecture, minimal source

NQC

NQC (Nested Query Calculus)

—

Alpha

Pure Gleam implementation with Erlang FFI, not yet in database-mcp

TypeQL-Exp.

TypeQL (Type-Safe QL)

—

Stub

Parser skeleton, Idris2 ABI definitions, spec only

BoJ Server Integration

database-mcp Cartridge

Located at boj-server/cartridges/database-mcp/:

Adapter: adapter/database_adapter.v (V-lang)

FFI functions (C ABI via Zig):

  • db_connect(backend_id) → slot

  • db_connect_verisimdb(url) → slot

  • db_connect_quandledb(url) → slot

  • db_connect_lithoglyph(url) → slot

  • db_connect_sqlite(path) → slot

  • db_disconnect(slot) → result

  • db_execute_sql(slot, query) → result — PostgreSQL, SQLite

  • db_execute_vcl(slot, query) → result — VeriSimDB

  • db_execute_kql(slot, query) → result — QuandleDB

  • db_execute_gql(slot, query) → result — LithoGlyph

  • db_begin_query(slot) / db_end_query(slot) — Transaction boundaries

  • db_state(slot) — Connection state (disconnected/connected/querying/error)

PanLL Dashboard Panels

Panel Purpose

db-status

Connection pool health across all backends

db-connections

Active connections, QPS metrics

db-verisimdb

Octad counts, proof counts, modality status

vcl-ut-safety-dashboard

10-level safety pipeline visualisation

vcl-ut-query-editor

Live type-checking with Idris2 kernel (TypeLL)

vcl-ut-proof-explorer

Obligation tracking and proof certificates

vcl-ut-horror-stories

Interactive education — what each safety level prevents

Universal Safety Pipeline (TypeLL → Query Languages)

All query languages share the same 10-level safety model, originating in TypeLL. VCL-UT is the reference implementation. KQL and GQL map their constructs to the same levels — no separate "-UT" or "-DT" repos needed.

TypeLL (type theory core — defines the 10 levels)
   │
   ├──→ VCL-UT  (reference implementation, VeriSimDB)
   ├──→ KQL     (applies same levels, QuandleDB)
   └──→ GQL     (applies same levels, LithoGlyph)

The Two-Tier Model (All Query Languages)

Each query language has the same two tiers:

  1. The language (VCL / KQL / GQL) — what users write

  2. The safety pipeline — TypeLL’s 10 levels applied progressively behind the language. Simple queries exit early at L1-L2. Proof-carrying queries go to L9-L10.

There is no "VCL-UT", "KQL-DT", or "GQL-DT" as separate products. Dependent type features are part of the safety pipeline at the appropriate levels.

The 10 Safety Levels

Level Name What It Prevents KQL Mapping GQL Mapping

L1

Construction Safety

Query injection

Pipeline parsing

Graph traversal parsing

L2

Schema Pinning

Schema drift

Dependent projection

Collection dependent types

L3

Resource Linearity

Connection leaks

Skein.jl connections

Graph cursor management

L4

Session Protocols

State violations

Query sessions

Traversal sessions

L5

Effect Tracking

Unaudited side effects

Future (read-only now)

Mutation auditing

L6

Scope Isolation

Namespace violations

Knot table boundaries

Collection boundaries

L7

Information Flow

Lineage failures

Invariant provenance

Graph provenance tracking

L8

Quantitative Bounds

Resource exhaustion

Stratum-bounded eval

Bounded traversal depth

L9

Proof Attachment

Missing evidence

Confidence-indexed results

Dependent type proofs

L10

Cross-Cutting

Composition bugs

Pipeline composition

Cross-collection joins

Per-Database Safety Documentation

  • VCL: verisimdb/docs/vcl-vs-vcl-dt.adoc — full spec with architecture diagram

  • KQL: quandledb/docs/kql-safety-model.adoc — KQL-specific mappings + Idris2 proofs

  • GQL: lithoglyph/docs/gql-safety-model.adoc — GQL-specific mappings + dependent types

Not Yet Integrated

  • NQC — Gleam-based Nested Query Calculus. Working implementation in nqc/src/nqc.gleam with Erlang FFI. Needs a db_execute_nqc() FFI function and database-mcp registration. Safety pipeline mapping not yet designed.

  • TypeQL-Experimental — Idris2 ABI definitions exist at typeql-experimental/src/abi/. Parser is stub-phase. Needs compiler work before integration.