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 the canonical name and design direction. The current L9 LinearSafe predicate accepts a LinUseOnce or LinBounded AST annotation; it is not yet expressible from source and is not a runtime resource-use proof. "-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
• Canonical Safety Levels (L0-L10)
• Current Architecture
• Technology Stack
• Roadmap
• Related Projects

Overview

VCL-UT is the next-generation interaction language for Verisim (engine formerly known in discussion as VeriSimDB), designed around eleven safety tags, L0–L10. L10 is named EpistemicSafe; its proved checker predicate tests the structure of an epistemic clause over an existing Statement. It is not by itself a factive warrant or a connection to a deployment-level choreography system. See the level walkthrough.

Important

Two honest qualifications: 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. The L0–L10 predicates and certificates are specified/proved over an already-constructed Statement; that does not mean all levels are expressible from source or that the predicates establish a deployment dependency. The highest level expressible from VCL source today is L6. The Rust parser leaves the L7–L10 extension fields empty and rejects their source clauses fail-closed. The missing work is parser syntax and clause elaboration/binding, not a missing proof of a K-CUT deployment requirement. Under the estate policy, the existing Idris2 corpus remains engineering-proof evidence, not Mathesis Grade 3; the Agda port plan is here. See also the K-CUT and levels audit.

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.

Status: transition admissibility checks implemented (structural identity- distinctness, evidence injection-safety, and evidence type-compatibility); the proof-supported layer is intended (witness independence first).

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 those listed below; this design-level catalogue does not imply that each obligation is implemented by the current parser or gate. The current predicate scopes are in the canonical-level table below.

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 typed validation layer behind it. The current trusted source parser reaches only through L6 CardinalitySafe. L7–L10 predicates can check populated AST fields, but their extension clauses are not yet expressible or elaborated from source; the parser fails closed on them.

Note

Keep a generic, implementation-specific modality profile (which modalities an implementation or deployment supports or enables) separate from the Octad and VCL-UT’s OctadSchema. The Octad is the fixed eight-modality model; a subject may have data in only some of its slots. OctadSchema still has all eight schema slots, even when a slot has no field definitions, and remains fixed at eight slots unless its contract is deliberately changed. The current VCLS v1 wire format is fixed-arity and does not carry a modality profile or support arbitrary cardinalities. See the terminology and compatibility contract.

Runtime gate request (VCL source text)
  -> Rust `parse_op` -> `VclOp`
       -> `Query(Statement)` -> `certified_level` -> query verdict
       -> `Transit(Transition)` -> `certified_transition_level` -> transition verdict (L4 ceiling)

Idris proof predicates and cumulative certificates are checked offline; they do
not feed the Rust runtime verdict. VeriSimDB consumer integration remains
outstanding.

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. When discussing implementation/deployment modality support, use modality profile; reserve OctadSchema for the fixed eight-slot schema.

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

Earlier editions of this README described the levels as originating in TypeLL and flowing through PanLL into VCL-UT. That is an unverified historical/design attribution, not an established implementation dependency or a verified one-to-one mapping. VCL-UT’s canonical eleven tags (L0–L10) and predicates are specified by local Rust and Idris artefacts; do not infer cross-project correspondence or deployment dependencies from shared names. See docs/architecture/ARCHITECTURE.adoc and docs/audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc for the current scope.

The Two-Tier Model

Tier	What	How
VCL	The consonance language	Surface language for proposing, inspecting, or verifying identity-state changes.
VCL-UT	The proof-bearing safety pipeline	Canonical safety tags L0–L10. The trusted Rust parser currently reaches L6; L7–L10 AST predicates are not yet reachable through their source clauses.

Note

Historical VCL-DT / PROOF-clause descriptions do not map to the canonical L9 LinearSafe and L10 EpistemicSafe tags. The current Rust parser rejects PROOF and the other unsupported extension clauses; do not claim proof-type validation or automatic L9/L10 execution from that syntax. See the level walkthrough and the parser and K-CUT audit.

Canonical Safety Levels (L0-L10)

The Idris predicates and cumulative SafetyCertificate values apply to an already-constructed Statement. Each certificate at level N requires all predicates through N. The trusted Rust source parser currently reaches L6; L7-L10 source clauses fail closed. The table records implemented predicate scope, not the stronger design semantics sketched in older material.

Tag	Canonical name	Current predicate scope
L0	ParseSafe	Statement is in the represented AST
L1	SchemaBound	Ordinary field references resolve against OctadSchema
L2	TypeCompat	Type compatibility of comparisons in WHERE
L3	NullSafe	Implemented null-safety predicate holds
L4	InjectionProof	No embedded string literal in WHERE (other clauses are not checked)
L5	ResultTyped	Selected expressions satisfy the result-type predicate
L6	CardinalitySafe	A LIMIT is present; no exact result count is inferred
L7	EffectTracked	An effect declaration is present
L8	TemporalSafe	A version constraint is present
L9	LinearSafe	A LinUseOnce or LinBounded annotation is present
L10	EpistemicSafe	Populated clause; declared agents; no cycle reported by implemented detector

L7-L9 are AST predicates, not operational enforcement of effects, freshness, or resource use. L10 does not establish epistemic warrant. The Idris L10 predicate calls a transitive-cycle detection implementation, but the corpus does not prove that its finite-fuel closure is equivalent to a formal graph reachability/acyclicity definition. The Rust mirror currently checks direct reciprocal ENTAILS pairs only. See docs/THE-10-LEVELS-EXPLAINED.adoc and docs/audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc for detailed scope.

Current Architecture

Runtime gate request (VCL source text)
  -> Rust `parse_op` -> `VclOp`
       -> `Query(Statement)` -> Rust `certified_level` -> query verdict
       -> `Transit(Transition)` -> `certified_transition_level` -> transition verdict (L4 ceiling)

Offline: Idris checks the mirrored AST predicates and dependent certificates;
it does not feed or run inside the Rust runtime verdict path.

The versioned wire codec is a separate interface, not an intermediate step in the vclt-gate request path. VeriSimDB consumer integration remains outstanding.

Technology Stack

Component	Current role
Rust (src/interface/parse)	Source parser, AST/wire codec, independent decider, and vclt-gate producer.
Idris2 (src/core, verification/proofs)	Predicates, soundness proofs, and cumulative dependent certificates over the AST.
VeriSimDB consumer	Planned integration target; it does not yet invoke the gate producer.

Roadmap

See ROADMAP.adoc for staged work. Its TypeLL entry is explicitly an unverified planning assumption, not an established build or deployment dependency. Do not infer a cross-project level mapping from shared names.

Related Projects

• VeriSimDB is the planned consumer of the VCL-UT gate; integration is not yet implemented.

• TypeLL and PanLL are related projects. This repository establishes no one-to-one level mapping or deployment dependency on them.

• TypeQL-Experimental examples in the level walkthrough are design sketches, not accepted VCL-UT syntax or an implementation dependency.