// SPDX-License-Identifier: CC-BY-SA-4.0 = VCL-UT (VeriSim Consonance Language, Usage-Tracked) Jonathan D.A. Jewell :spdx: MPL-2.0 :status: Pre-Alpha :toc: preamble :icons: font image:https://zenodo.org/badge/DOI/10.5281/zenodo.19329501.svg[DOI,link="https://doi.org/10.5281/zenodo.19329501"] image:https://img.shields.io/badge/believe__me-0-brightgreen[believe_me: 0] image:https://img.shields.io/badge/tests-150_pass-brightgreen[tests: 150 pass] image:https://img.shields.io/badge/OpenSSF-Best_Practices-green?logo=opensourcesecurity[OpenSSF Best Practices,link="https://www.bestpractices.dev/en/projects/new?repo_url=https://github.com/hyperpolymath/vcl-ut"] 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. [.lead] **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.** == Overview VCL-UT is the next-generation interaction language for https://github.com/hyperpolymath/verisimdb[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 link:docs/THE-10-LEVELS-EXPLAINED.adoc[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 link:verification/proofs/AGDA-GRADE3-PORT-PLAN.adoc[here]. See also link:docs/audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc[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: [cols="1,3"] |=== |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. [source] ---- 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: [source] ---- 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 link:docs/standards/MODALITY-PROFILES.adoc[the terminology and compatibility contract]. ==== [source] ---- 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 [cols="1,2,3"] |=== | 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 link:docs/audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc[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. [cols="1,2,3"] |=== | 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 [source] ---- 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 [cols="1,2"] |=== | 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.