VCL-UT (VeriSim Consonance Language, Usage-Tracked)

Important

This project was renamed on 2026-04-05. Its former name used the letter sequence "V-Q-L-hyphen-U-T" (read: "vee-queue-ell-you-tee") and stood for "Ultimate Type-safe". The canonical name is now VCL-UT — VeriSim Consonance Language, Usage-Tracked. See CHANGELOG.md for the full rename scope. The GitHub repository URL is unchanged.

Note

Two superseded expansions of "UT" are still in circulation and should not be used: "Ubiquitous Type-safe" (which appeared in this README) and "-total". Usage-Tracked is canon, and it is the accurate one: the distinguishing feature of this tier is that resource usage is tracked in the type system (L9 LinearSafe, via QTT). "-total" survives in the crate name vcl-total and the Idris namespace VclTotal; renaming those is a separate, invasive change and is deliberately not bundled here.

VeriSimDB does not merely store records. It maintains identity consonance across modal witnesses and federation boundaries. VCL expresses propositions and epistemic requests over that consonance state. VCL-UT validates whether proposed identity transitions are admissible.

Table of Contents

• Overview
• VCL-UT in One Sentence
• What VCL Is
• What VCL-UT Proves
• Relationship to VeriSimDB
• Important Distinctions
• Terminology Guidance
• Lineage
  • The Two-Tier Model
  • Adoption Strategy
• The 10 Levels of Type Safety
  • Established (IO-Covered) — 6 Levels
  • TypeQL-Experimental Extension Mechanisms (Levels 7-10)
• Architecture
• Technology Stack
• Roadmap
  • Phase 1 — Foundation (Levels 1-3)
  • Phase 2 — Safety Core (Levels 4-6)
  • Phase 3 — Advanced Safety (Levels 7-10)
• Related Projects

Overview

VCL-UT is the next-generation interaction language for Verisim (engine formerly known in discussion as VeriSimDB), designed to satisfy eleven levels of type safety, L0–L10 — the 6 established IO-covered forms, the 4 additional forms identified through our research, and L10 EpistemicSafe, the consonance level, which is not a query-safety property at all but a warrant property. See the level walkthrough.

Important

Two honest qualifications, both measured on 2026-07-21: The ladder is eleven levels (L0–L10), not ten. Older prose says ten and numbers them 1–10; the code numbers them 0–10 and the code is canonical, because those numbers are wire tags. Eleven levels are specified and proved; six are expressible. The parser cannot yet populate the clauses that L7–L10 are inferred from, so the highest level reachable from VCL source text is L6 CardinalitySafe. The gap is fail-closed and disclosed (issue #25) — unsupported clauses are rejected, never silently ignored — but it is a gap, and closing it is the top outstanding item on the language surface.

The goal is production-worthy VCL that is provably correct at every layer, from parse to execution. At minimum, this repo serves as a research vehicle for exploring the boundaries of type-safe interaction languages for consonance engines.

Note	Verisim operations are propositions to a consonance engine, not queries against a passive store. Operations split into propositional (DECLARE, ASSERT, RETRACT) and epistemic (INSPECT, VERIFY). "Query language" is therefore a misnomer; "consonance language" names the actual thing.

VCL-UT in One Sentence

VCL-UT is the proof-bearing safety pipeline for VCL, the VeriSim Consonance Language. It checks whether identity transitions proposed to VeriSimDB are well-formed, type-safe, authorised, resource-safe, proof-supported, and admissible before they affect live consonance state.

What VCL Is

VCL is not SQL with extra types. VCL is a language of propositions and epistemic requests to a consonance engine. Typical VCL operations are identity-lifecycle operations:

Operation	Meaning
DECLARE	introduce a candidate identity claim
ASSERT	strengthen or add evidence to an identity claim
RETRACT	revoke, weaken, or retire a live claim
INSPECT	observe consonance, drift, provenance, or federation state
VERIFY	request proof-bearing validation of a claim or transition
MERGE	join identities when consonance evidence supports it
SPLIT	separate an over-coalesced identity
NORMALISE	repair drift when a justified repair path exists

The surface language may look query-like in places, but the semantics are not "read rows from a passive store": VCL statements propose or inspect changes in an actively maintained identity-consonance system.

What VCL-UT Proves

VCL-UT does not prove the entire database is globally correct. It checks whether a particular VCL statement or transition is admissible. A transition may require obligations such as:

syntactic validity         schema conformance     type compatibility
nullability safety         injection resistance   resource-usage bounds
session/protocol validity  effect compatibility   modal consistency
provenance integrity       freshness              authorisation
federation trust           proof attachment

The practical proof shape is:

IdentityState_before
  + VCL transition
  + evidence
  + proof obligations
  -> VerifiedTransition
  -> IdentityState_after

Relationship to VeriSimDB

VeriSimDB maintains continuously-maintained identity claims across an octad of modal witnesses: graph, vector, tensor, semantic, document, temporal, provenance, and spatial. VCL is the production language for interacting with that consonance engine; VCL-UT is the fully-typed validation layer behind it. Simple statements short-circuit at the early safety levels; proof-bearing statements and high-risk lifecycle transitions go through the deeper proof, effect, resource, and cross-cutting checks (L9-L10).

User / system writes VCL
        |
        v
VCL parser and binder
        |
        v
VCL-UT safety pipeline    (11 levels, L0-L10)
        |
        v
verified transition plan
        |
        v
VeriSimDB consonance engine (octad of modal witnesses)

Important Distinctions

Retraction is not deletion. A retracted identity claim usually remains visible to provenance, audit, federation, and proof systems. Retraction means "this claim is no longer live"; tombstoning means "this identity or claim has been durably retired"; expungement is a separate, policy-governed operation.

Drift is not identity death. A stale vector, a changed document, a broken provenance event, or a federated conflict does not destroy the subject identity. It creates a typed condition requiring inspection, repair, quarantine, retraction, or arbitration.

VCL-UT is not the expert-facing product. The ordinary production language is VCL; VCL-UT is the proof-bearing substrate that validates VCL statements. It may expose expert syntax for proof attachment, but its main role is to make routine VCL safe.

Terminology Guidance

Prefer: consonance language, statement, transition, identity claim, consonance subject, modal witness, proof-bearing statement, verified transition, octad.

Avoid or qualify: query language, query, record, CRUD, delete, proof-carrying query, 6-modal engine, passive store. Use "query" only for a read-only syntactic convenience, and make clear the semantic model is epistemic inspection of consonance state.

Lineage

The 10 type safety levels originate in TypeLL (the core type theory), flow into PanLL (panel framework type safety), and are now applied to consonance statements as VCL-UT.

TypeLL (type theory core — defines the 10 levels)
   │
   ├──→ PanLL (panel framework type safety)
   │
   └──→ VCL-UT (consonance-statement type safety)
             │
             └──→ Verisim (8-modal octad consonance engine)

The Two-Tier Model

Tier	What	How
VCL	The consonance language	Parser (ReScript) → AST → execution. What users write to propose, inspect, or verify.
VCL-UT	The safety pipeline	10 progressive levels. Sits behind VCL, applies automatically. Simple statements short-circuit at L1-L2. Proof-carrying statements (with PROOF clause) go through L9-L10. Invisible to the user except when they add a PROOF clause.

Note	The dependent-types variant was originally labelled with the suffix "-DT" (Dependent Types) as the proof-bearing execution mode (statements with PROOF clauses). It is not a separate product — it is folded into VCL-UT’s L9 (Proof Attachment) and L10 (Cross-Cutting) levels.

The 6 proof types (EXISTENCE, INTEGRITY, CONSISTENCY, PROVENANCE, FRESHNESS, AUTHORIZATION) remain — they are activated by VCL’s PROOF clause and validated by VCL-UT levels L9-L10.

Adoption Strategy

The type safety story unfolds in three phases:

1. ReScript evangeliser proves the concept first — demonstrate the value of these type safety levels in ReScript itself, where the developer community can experience them firsthand

2. Once proven, VCL-UT and AffineScript become the two showcase languages for teaching people the 10 levels of type safety

3. VCL-UT handles the database-interaction domain; AffineScript handles general-purpose programming

The 10 Levels of Type Safety

Established (IO-Covered) — 6 Levels

Level	Name	Description
L1	Syntactic parsability	Parser accepts the input.
L2	Well-formedness	Structure matches the grammar.
L3	Schema conformance	References resolve to declared entities.
L4	Type compatibility	Operator arities and types align.
L5	Nullability tracking	NULL propagates explicitly through joins.
L6	Injection resistance	Parameterisation and escaping are type-level invariants.

TypeQL-Experimental Extension Mechanisms (Levels 7-10)

The typeql-experimental sub-project within nextgen-databases prototyped 6 mechanisms that map to levels 7-10:

Mechanism	VCL-UT Syntax	Idris2 Encoding
Linear types	CONSUME AFTER N USE	QTT quantity 1 on Connection
Session types	WITH SESSION protocol	Session : SessionState → Type indexed type
Effect systems	EFFECTS { Read, Write }	Effect set with subsumption proofs
Modal types	IN TRANSACTION	Box types indexed by world/scope
Proof-carrying code	PROOF ATTACHED theorem	ProvedResult sigma type
Quantitative type theory	USAGE LIMIT n	Bounded resource tracking via QTT

Architecture

                        +---------------+
                        |  VCL Source   |
                        |  (.vcltotal)  |
                        +-------+-------+
                                |
                    +-----------v-----------+
                    |  Parser (Level 1)     |  ReScript — extends Verisim VCL parser
                    +-----------+-----------+
                                |
                    +-----------v-----------+
                    |  Schema Binder (2)    |  Idris2 — dependent types on schema
                    +-----------+-----------+
                                |
                    +-----------v-----------+
                    |  Type Checker (3-6)   |  Idris2 — nullability, injection, results
                    +-----------+-----------+
                                |
                    +-----------v-----------+
                    |  Safety Checker (7-10)|  Idris2 — linear, session, effects, proofs
                    +-----------+-----------+
                                |
                    +-----------v-----------+
                    |  FFI Bridge           |  Zig — C-ABI, zero-copy plan emission
                    +-----------+-----------+
                                |
                    +-----------v-----------+
                    |  Verisim              |  8-modal octad storage engine
                    +-----------------------+

Technology Stack

Layer	Language	Purpose
Core type system	Idris2	Dependent types for all 10 safety levels. %default total.
FFI bridge	Zig	C-ABI plan compilation. Zero-copy result sets.
Parser	ReScript	Surface syntax parsing, extending Verisim’s VCL parser.
API layer	zig	REST/gRPC/GraphQL endpoints for statement submission.
Verisim integration	Elixir	8-modal octad storage connection via NIFs.

Roadmap

Phase 1 — Foundation (Levels 1-3)

• ❏ VCL-UT grammar specification (EBNF, extending VCL v3.0)

• ❏ Idris2 parser with totality proof

• ❏ Schema representation as dependent types

• ❏ Type-compatible operation checker

• ❏ Zig FFI for plan emission

• ❏ Basic test suite against Verisim

Phase 2 — Safety Core (Levels 4-6)

• ❏ Null-tracking through join algebra

• ❏ Injection-resistant parameterisation

• ❏ Integration with Verisim’s 8-modal execution

Phase 3 — Advanced Safety (Levels 7-10)

• ❏ Linear resource tracking (QTT)

• ❏ Session-typed protocols

• ❏ Effect inference

• ❏ Proof-attached statement execution

Related Projects

Project	Relationship
verisimdb	Target consonance engine (8-modal octad storage)
verisimdb/docs/VCL-SPEC.adoc	Base VCL grammar specification (EBNF appendix)
nextgen-databases/typeql-experimental	6 extension mechanisms for levels 7-10 (Idris2 kernel + ReScript parser)
typell	Core type theory — the 10 levels originate here
panll	Panel framework applying the same 10 levels to UI type safety