0-AI-MANIFEST.a2ml

# SPDX-License-Identifier: MPL-2.0
# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>

# ⚠️ STOP - CRITICAL READING REQUIRED

**THIS FILE MUST BE READ FIRST BY ALL AI AGENTS**

## WHAT IS THIS?

This is the AI manifest for **vcl-total** (VCL Ultimate Type-Safe) — the 10-level
type-safe query language for VeriSimDB. It supersedes VCL-DT (dependent types
only) as THE formally verified query path.

## NAMING

- ALWAYS: "VCL-total", "vcl-total"
- NEVER: "vcl++", "vqlpp", "VCL Plus Plus" (old names, killed 2026-03-16)
- File extension: `.vcltotal` (NOT `.vqlpp`)

## LINEAGE (CRITICAL CONTEXT)

```
TypeLL (type theory core)
   │
   ├──→ PanLL (panel framework type safety)
   │
   └──→ VCL-total (database query language type safety)
             │
             └──→ VeriSimDB (6-modal execution engine)
```

- **TypeLL** defines the 10 type safety levels as core type theory
- **PanLL** integrates TypeLL's type safety via TypeLL-PanLL assimilation
- **VCL-total** applies those same 10 levels to VeriSimDB's query language
- The 6 TypeQL-Experimental extensions (linear, session, effect, modal,
  proof-carrying, QTT) map to VCL-total levels 7-10

### The 3 Query Paths in VeriSimDB

| Path | Purpose | Type Safety |
|------|---------|-------------|
| VCL (Slipstream) | Standard routine queries, fast | None (runtime only) |
| VCL-DT | PROOF clauses (6 proof types) | Dependent types via Lean |
| VCL-total | All 10 levels, research → production | Full formal verification via Idris2 |

If VCL-total succeeds, it replaces VCL-DT entirely.

### Adoption Path

1. **ReScript evangeliser** proves the type-safety concept first (in ReScript)
2. Once proven, **VCL-total** and **AffineScript** are the two showcase languages
   for teaching people the 10 levels of type safety
3. VCL-total for database queries, AffineScript for general programming

## CANONICAL LOCATIONS (UNIVERSAL RULE)

### Machine-Readable Metadata: `.machine_readable/` ONLY

These a2ml files MUST exist in `.machine_readable/` directory ONLY:
1. **STATE.a2ml** - Project state, progress, blockers
2. **META.a2ml** - Architecture decisions, governance
3. **ECOSYSTEM.a2ml** - Position in ecosystem, relationships

**CRITICAL:** If ANY of these files exist in the root directory, this is an ERROR.

### Source Code

- `src/interface/abi/` — Idris2 ABI (type kernel, formal proofs)
- `src/interface/ffi/` — Zig FFI (C-ABI query plan compilation)
- `src/contracts/` — VCL proof contracts
- `src/parser/` — ReScript parser (surface syntax)
- `adapter/` — zig API layer

### Build Artefacts

- `Justfile` — Task runner
- `ffi/zig/build.zig` — Zig build configuration

## CORE INVARIANTS

1. **No `believe_me`** — Zero instances in any Idris2 code. All proofs are real.
2. **No `assert_total`** — All functions provably total via `%default total`.
3. **No `assert_smaller`** — Termination proved structurally.
4. **No SCM duplication** — `.machine_readable/` is authoritative.
5. **Idris2 over Ephapax** — When proven Idris2 code conflicts with Ephapax
   linear types, always choose Idris2. Dependability first.
6. **License** — MPL-2.0 throughout.
7. **Author** — Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
8. **Container images** — Chainguard base, Podman, Containerfile.

## THE 10 LEVELS OF TYPE SAFETY

### Established (IO-Covered) — Levels 1-6

| Level | Name | What it Guarantees |
|-------|------|--------------------|
| 1 | Parse-time safety | Malformed queries rejected before processing |
| 2 | Schema-binding safety | Column/table references validated against live schema |
| 3 | Type-compatible ops | Arithmetic/comparison only on compatible types |
| 4 | Null-safety | Nullable vs non-nullable tracked through joins |
| 5 | Injection-proof | Parameterised queries enforced at type level |
| 6 | Result-type safety | Return types known at compile time |

### Research-Identified — Levels 7-10

| Level | Name | What it Guarantees |
|-------|------|--------------------|
| 7 | Cardinality safety | Return count guarantees in the type system |
| 8 | Effect-tracking | Read vs write vs DDL distinguished at type level |
| 9 | Temporal safety | Bi-temporal queries carry time bounds in types |
| 10 | Linearity safety | Connection/transaction handles are linear types |

### TypeQL-Experimental Extension Mechanisms (for Levels 7-10)

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

## RELATED PROJECTS

| Project | Relationship |
|---------|-------------|
| nextgen-databases/verisimdb | Target database engine (6-modal) |
| nextgen-databases/verisimdb/docs/VCL-SPEC.adoc | Base VCL grammar (26KB) |
| nextgen-databases/verisimdb/docs/vcl-vs-vcl-dt.adoc | VCL-DT spec (superseded by VCL-total) |
| nextgen-databases/typeql-experimental | 6 extension mechanisms for levels 7-10 |
| typell | Core type theory (10 levels originate here) |
| panll | Panel framework (integrates TypeLL type safety) |
| nextgen-languages/affinescript | Sister showcase for type safety adoption |

## VERISIMDB INSTANCE POLICY (CRITICAL)

VCL-total connects to **whichever VeriSimDB instance the user's project runs**.
Every project has its own VeriSimDB on a unique port. The LSP's `verisimdb_url`
defaults to empty and MUST be configured per-workspace.

- **NEVER** default to `localhost:8080` — that is VeriSimDB's own dev server.
- **NEVER** hardcode any port — each project chooses its own.
- The user configures the URL via workspace settings or `connect_verisimdb()`.

## SESSION STARTUP CHECKLIST

✅ Read THIS file (0-AI-MANIFEST.a2ml) first
✅ Understand: VCL-total supersedes VCL-DT
✅ Understand: 10 levels from TypeLL → PanLL → VCL-total
✅ NEVER use vcl++/vqlpp naming
✅ Canonical location: `.machine_readable/`