From 69e710d27538cfcd6c7df755ea5371caa73c8a53 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 1 Nov 2026 17:37:12 +0000 Subject: [PATCH 1/7] docs: audit VCL levels and plan Agda proof port Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- README.adoc | 72 +- ROADMAP.adoc | 48 +- docs/QUICKSTART.adoc | 11 + docs/THE-10-LEVELS-EXPLAINED.adoc | 153 ++-- docs/architecture/ARCHITECTURE.adoc | 702 ++++-------------- docs/architecture/DECISIONS.adoc | 591 +++------------ .../K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc | 136 ++++ .../proofs/AGDA-GRADE3-PORT-PLAN.adoc | 178 +++++ verification/proofs/README.adoc | 5 + 9 files changed, 747 insertions(+), 1149 deletions(-) create mode 100644 docs/audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc create mode 100644 verification/proofs/AGDA-GRADE3-PORT-PLAN.adoc diff --git a/README.adoc b/README.adoc index 7d9fd0d..b1dde74 100644 --- a/README.adoc +++ b/README.adoc @@ -19,11 +19,12 @@ 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. +"-total". *Usage-Tracked* is the canonical name and design direction. The +current L9 `LinearSafe` predicate checks an AST annotation (`UseOnce` or +`Bounded`); that annotation 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.** @@ -32,25 +33,32 @@ invasive change and is deliberately not bundled here. VCL-UT is the next-generation interaction language for https://github.com/hyperpolymath/verisimdb[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. +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, both measured on 2026-07-21: +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. -* 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 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, @@ -131,10 +139,11 @@ IdentityState_before 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). +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] ==== @@ -221,23 +230,20 @@ TypeLL (type theory core — defines the 10 levels) | **VCL** | The consonance language -| Parser (ReScript) → AST → execution. What users write to propose, inspect, or verify. +| Surface language for proposing, inspecting, or verifying identity-state changes. | **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. +| 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: 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. +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]. === Adoption Strategy diff --git a/ROADMAP.adoc b/ROADMAP.adoc index 6326dbd..b8beefe 100644 --- a/ROADMAP.adoc +++ b/ROADMAP.adoc @@ -50,30 +50,47 @@ What exists, measured: | 150 across all workspace roots. |=== -The single most important qualification: *eleven levels are specified and -proved; six are expressible.* `parse_statement` fixes `proof_clause`, +The single most important qualification: *the L0–L10 predicates and +certificates are specified/proved over `Statement` values; VCL source reaches +at most L6.* `parse_statement` fixes `proof_clause`, `effect_decl`, `version_const`, `linear_annot` and `epistemic_clause` at -`None`, and `infer_requested_level` awards L7-L10 on exactly those fields, so -the highest level reachable from VCL source text is *L6 `CardinalitySafe`*. -The gap is fail-closed and disclosed (unsupported clauses are rejected with an -explicit message, never silently ignored) — but it is the gap that matters -most. +`None`, and `infer_requested_level` awards L7–L10 on exactly those fields, so +the highest level reachable from source text is *L6 `CardinalitySafe`*. The +parser also fail-closes on modal expressions (`KNOWS`, `BELIEVES`, +`ANNOUNCE`, `COMMON`). The missing work is L7–L10 source grammar and +parse-to-AST elaboration/binding; ordinary schema binding of field references +already exists. Issue #25 concerned parser/corpus-boundary work, not K-CUT, +and is closed. See the +link:docs/audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc[relationship and +source-gap audit] for the exact evidence and limits. == Nearest Work These are ordered by value, not by version number. -. *Surface syntax for L7-L10.* Close the gap above. Without it the upper - ladder — including the entire consonance level — is reachable only by - constructing a `Statement` programmatically or decoding one off the wire. - Tracked in #25. +. *Surface syntax and elaboration for L7-L10.* Add parser support that + constructs and binds `effect_decl`, `version_const`, `linear_annot`, and + `epistemic_clause` (including the modal expression forms), then reconcile + level inference across the source frontends. Until then, upper-level fields + can only arrive through a constructed `Statement` or wire decode; they are + not expressible in source. Issue #25 covered the earlier parser/boundary + work and is closed; it did not establish a K-CUT dependency. +. *Execute the staged Agda Grade 3 port plan.* The current Idris2 corpus is + engineering-proof evidence, not a Mathesis Grade 3 theorem receipt. Port the + exact L0–L10 predicate/certificate statements in reviewable slices, with + pinned Agda CI receipts and theorem-by-theorem assumption records. The plan + is `verification/proofs/AGDA-GRADE3-PORT-PLAN.adoc`; no Grade 3 status is + claimed until each in-scope theorem checks in Agda. . *Wire `vclt-gate` into VeriSimDB.* Contract v1 is frozen and the producer works; the consumer (`rust-core/verisim-api/src/vcl.rs`) does not invoke it. Until it does, VCL-UT proves things about statements VeriSimDB never asks about. -. *Discharge the two disclosed L10 residuals.* Transitive `ENTAILS`-cycle - detection and proposition well-typedness, both recorded as owed in - `verification/proofs/VERIFICATION-STANCE.adoc`. +. *Close the remaining L10 boundary gaps.* Proposition well-typedness of + requirement expressions against the schema remains owed. Also align the + Rust decider's direct reciprocal-cycle check with the Idris predicate's + transitive-cycle check before relying on non-source (wire/programmatic) L10 + statements. The Idris transitive-cycle proof is already implemented; do not + track it as outstanding. . *Optional syntax cleanup: retire the legacy `HEXAD` spelling* when all supported frontends can do so compatibly. The current Rust parser accepts both `OCTAD` and `HEXAD` as the same `Source::Octad`; this is a source-name @@ -112,8 +129,9 @@ These are ordered by value, not by version number. * [x] S2 transitions MERGE / SPLIT / NORMALISE, with NORMALISE fail-closed without an explicit justification * [ ] Surface syntax for epistemic clauses -* [ ] Transitive `ENTAILS`-cycle detection +* [x] Transitive `ENTAILS`-cycle detection in the Idris proof predicate * [ ] Proposition well-typedness against the schema +* [ ] Align the Rust L10 cycle check with the Idris transitive predicate === v0.5.0 — VCL-DT Supersession * [ ] All 6 VCL-DT PROOF types expressible in VCL-UT diff --git a/docs/QUICKSTART.adoc b/docs/QUICKSTART.adoc index 4ec3131..56e5f33 100644 --- a/docs/QUICKSTART.adoc +++ b/docs/QUICKSTART.adoc @@ -10,6 +10,17 @@ Jonathan D.A. Jewell toc::[] +[WARNING] +==== +This March 2026 quickstart is historical, not a current executable guide. +Its parser/toolchain instructions and sample reports predate the trusted Rust +parser and the canonical L0–L10 names. In particular, its claim that L9 is +Proof Attachment and L10 is Cross-Cutting is false; source currently reaches +only through L6 `CardinalitySafe`. Do not treat the sample PASS report as a +runtime test or proof receipt. See `README.adoc`, `ROADMAP.adoc`, and the +link:audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc[audit] for current scope. +==== + == Prerequisites VCL-total requires the following tools. All can be managed via diff --git a/docs/THE-10-LEVELS-EXPLAINED.adoc b/docs/THE-10-LEVELS-EXPLAINED.adoc index 47eec8a..c7645d4 100644 --- a/docs/THE-10-LEVELS-EXPLAINED.adoc +++ b/docs/THE-10-LEVELS-EXPLAINED.adoc @@ -658,16 +658,13 @@ held indefinitely. == Level 10: Epistemic Safety -This is the consonance level, and it is the one level that is not about the -statement at all. Levels 0-9 ask *"will this statement behave?"*. Level 10 asks -*"is the engine entitled to believe the answer?"*. - -That question only arises because VCL-UT does not address a passive store. It -addresses a consonance engine holding eight modal witnesses -- graph, vector, -tensor, semantic, document, temporal, provenance, spatial -- which can -disagree. A result assembled from disagreeing witnesses is not wrong in the -way a type error is wrong; it is *unwarranted*. No amount of levels 0-9 will -detect it, because every individual step was well-typed. +L10 `EpistemicSafe` is the epistemic-labelled predicate over a `Statement`; +it is not a proof that the engine is entitled to believe an answer. The current +checker validates the structure of a populated epistemic clause (agent +declarations and entailment-cycle conditions). It does not run the standalone +Kripke semantics, establish factivity for `Knows`, or prove that modal +witnesses agree. Do not infer any of those properties, or a K-CUT deployment +dependency, from the level name. === What It Checks @@ -692,99 +689,89 @@ forms (`ast.rs`, mirroring `Grammar.idr`): | Agent `a`'s warrant for `p` derives from agent `b`'s. |=== -The certificate `L10_EpistemicSafe` is witnessed by +The Idris certificate `L10_EpistemicSafe` is witnessed by `Decide.epistemicConsistentStmt stmt = True`, which requires: . an epistemic clause is present; . at least one agent is declared; . every agent referenced by a requirement is among the declared agents; -. there is no direct `ENTAILS` cycle -- no pair with both `a ⊨ b` and `b ⊨ a`. - -Condition (4) is the substantive one. A mutual entailment is a citation loop: -two witnesses each grounding their warrant in the other, with nothing outside -the pair supporting either. That is exactly how a federation manufactures -false confidence, and it is invisible to every lower level. +. the `ENTAILS` graph is acyclic (including transitive cycles). -=== Disclosed Residual -- Read This +The Idris proof corpus now checks transitive cycles using +`Decide.hasTransitiveCycle`, and `Checker.checkLevel10Sound` proves soundness +for that implemented structural predicate. This is not semantic soundness of +the standalone Kripke model, and not a factive-warrant theorem. -Two obligations are *owed, not discharged*, and are recorded as such in -`verification/proofs/VERIFICATION-STANCE.adoc`: +=== Disclosed Residual -* **Transitive `ENTAILS`-cycle detection.** Only the *direct* two-party - symmetry violation is checked. A three-party loop (`a ⊨ b`, `b ⊨ c`, - `c ⊨ a`) passes today. -* **Proposition well-typedness.** The `Expr` carried by a requirement is not - checked against the schema. +* **Proposition well-typedness.** The `Expr` carried by an epistemic + requirement is not yet checked against the schema. +* **Rust/Idris cycle-check alignment.** The Idris predicate detects + transitive cycles; the Rust mirror in `src/interface/parse/src/decider.rs` + currently detects direct reciprocal `ENTAILS` pairs only. Preserve this + cross-implementation difference when describing the certified path; it + does not change the fact that source syntax cannot currently request L10. -These are stated here because a safety level that quietly overstates itself is -worse than no level at all. The decider and the Idris checker agree exactly -(`Checker.checkLevel10Sound`); what they agree on is a *partial* condition. +The L10 soundness theorem is real but has a defined scope: it proves the +Idris checker agrees with the Idris structural predicate, not that an agent +knows a proposition or that another system is a deployment prerequisite. -=== Implementation Status -- No Surface Syntax Yet +=== Implementation Status -- L7–L10 Source Gap [WARNING] ==== -As of 2026-07-21, *L10 cannot be requested from VCL source text*, and neither -can L7, L8 or L9. - -`parse_statement` in `src/interface/parse/src/parser.rs` constructs every -`Statement` with `proof_clause`, `effect_decl`, `version_const`, -`linear_annot` and `epistemic_clause` all fixed at `None`. -`infer_requested_level` awards L7-L10 on precisely those fields, so no parsed -statement can ever reach them. Measured ceiling: - -[cols="1,3"] -|=== -| Reached | Input - -| L1 | `SELECT * FROM STORE a` -| L4 | `SELECT * FROM STORE a WHERE GRAPH.x > 1` -| L6 | `SELECT * FROM STORE a LIMIT 10` -| -- | `... EFFECTS { Read }` -- rejected, "not yet supported by the P5a parser slice" -| -- | `... AS OF NOW - 5 SECONDS` -- rejected -| -- | `... USE ONCE` -- rejected -| -- | `AGENTS { ... } KNOWS ...` -- rejected +The Idris proof predicates cover L0–L10 for already-constructed `Statement` +values. The trusted Rust parser reaches at most L6 `CardinalitySafe`; L7, L8, +L9 and L10 cannot currently be requested from VCL source. + +`parse_statement` in `src/interface/parse/src/parser.rs` initializes +`proof_clause`, `effect_decl`, `version_const`, `linear_annot` and +`epistemic_clause` to `None`. `infer_requested_level` awards L7–L10 only when +the corresponding extension fields are populated. The AST's epistemic +constructors describe intended meanings; L10 does not validate them against +the Kripke model. The parser rejects +`PROOF`, `EFFECTS`, `AT`, `CONSUME`, `USAGE` and `EPISTEMIC` clauses, as well +as modal expressions `KNOWS`, `BELIEVES`, `ANNOUNCE` and `COMMON`. + +[cols="1,2,3"] |=== +| Level | Intended AST field | Source path today -This is a *disclosed, fail-closed* gap, not a silent one: the parser rejects -`EFFECTS` with an explicit message naming the P5a slice and issue #25, rather -than accepting the clause and ignoring it. Fail-closed is the correct -behaviour. But it does mean the upper ladder is, for now, reachable only by -constructing a `Statement` programmatically or by decoding one off the wire -- -not by writing VCL. +| L7 `EffectTracked` | `effect_decl` | `EFFECTS` rejected +| L8 `TemporalSafe` | `version_const` | `AT VERSION` rejected +| L9 `LinearSafe` | `linear_annot` | `CONSUME` / `USAGE` rejected +| L10 `EpistemicSafe` | `epistemic_clause` | `EPISTEMIC` and modal expressions rejected +|=== -Closing this is the single highest-value piece of work outstanding on the -language surface. Until it is closed, the honest claim is: *eleven levels are -specified and proved; six are expressible.* +This is a *disclosed, fail-closed* gap: unsupported syntax returns a typed +error rather than being accepted and ignored. Ordinary schema binding for +field references exists; the missing work is source grammar and elaboration / +binding of these extension fields. A programmatically constructed or +wire-decoded `Statement` can carry them, but that does not make them +expressible from source. Issue #25 concerned parser/corpus-boundary work and +is closed; it does not establish a K-CUT dependency. See +link:audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc[the audit]. + +The language-surface status is: the proof predicates and certificates are +specified over Idris `Statement` values; VCL source currently reaches only +through L6 `CardinalitySafe`. See the +link:audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc[audit] for the parser +and clause-elaboration gap. ==== -== How TypeLL Provides the Foundation - -All 10 levels are defined in **TypeLL**, the core type theory. VCL-total -_inherits_ these levels rather than inventing them. This means: - ----- -TypeLL (core type theory) - │ - │ Defines: the levels of type safety as formal constructs - │ - ├──→ PanLL (panel framework) - │ Uses L0-L9 for UI component safety - │ - └──→ VCL-UT (consonance statements) - Uses L0-L9 for statement safety, and adds L10 ----- +== Cross-Project Type-Theory Relationship -The same mathematical proofs that ensure a PanLL UI panel cannot render invalid -state also ensure a VCL-UT statement cannot execute an invalid operation. The -theory is shared; only the application domain differs. +No one-to-one mapping between VCL-UT safety levels and TypeLL or PanLL levels +is established by this repository's imports, proof corpus, or a versioned +interface contract. Shared names, numbers, or type-theoretic vocabulary are +not evidence that the same theorem is implemented in each project. Any +cross-project correspondence needs an explicit mapping of the constructs, +assumptions, and proved propositions. -L10 is the exception, and the asymmetry is informative. `EpistemicSafe` is -*not* inherited from TypeLL: a UI panel has no federation of disagreeing -witnesses and therefore no warrant question to answer. L10 originates in -VCL-UT, in the shift from querying a store to addressing a consonance engine. -It is the first level in this family that the domain contributed back to the -theory rather than receiving from it. +L10 `EpistemicSafe` is a local structural predicate over the `Statement` AST; +it is not inferred from another project's level name, and does not establish a +K-CUT deployment requirement. See the +link:audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc[audit]. == Summary: What Each Level Prevents diff --git a/docs/architecture/ARCHITECTURE.adoc b/docs/architecture/ARCHITECTURE.adoc index 9ceda2b..49b3855 100644 --- a/docs/architecture/ARCHITECTURE.adoc +++ b/docs/architecture/ARCHITECTURE.adoc @@ -1,622 +1,224 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) 2026 Jonathan D.A. Jewell -= VCL-total Architecture += VCL-UT Architecture Jonathan D.A. Jewell -:date: 2026-03-16 +:date: 2026-11-01 :toc: macro :toclevels: 3 :icons: font -:description: Comprehensive architecture document for VCL-total (Verified Query Language — Unified Types) +:description: Current architecture and proof boundaries for VCL-UT toc::[] == System Overview -VCL-total (Verified Query Language — Unified Types) is a dependently-typed query -language compiler that produces machine-checkable proofs of query safety. It -extends VCL-dt (VeriSimDB's existing dependent type system, ~35% wired) to -cover the full spectrum of safety properties through 10 formally verified -levels. +VCL-UT is a dependently typed safety checker for VCL. Its canonical ladder has +eleven tags, L0–L10. The Idris proof predicates and dependent certificates +apply to already-constructed `Statement` values; the trusted Rust source parser +currently reaches only through L6 `CardinalitySafe`. The external gate does not +transport the Idris dependent certificate as a re-checkable proof object. -Every query entering VCL-total passes through a six-stage pipeline. Each stage -is responsible for enforcing one or more of the 10 safety levels. The pipeline -output is not merely a compiled query — it is a *proof certificate* attesting -that every safety property holds. +[WARNING] +==== +This architecture document previously contained pipeline diagrams and +implementation descriptions that predated the canonical L0–L10 ladder and the +current parser / gate boundary. The sections below have been narrowed to the +implemented scope. Treat the level table and the 2026-11-01 audit as authoritative +for level names, proof scope, and source expressibility. +==== -=== Pipeline: Parse → Bind → Check → Analyse → Compile → Execute +=== Implemented Pipeline Boundary [source] ---- - VCL-total PIPELINE - ═══════════════ - - ┌──────────────┐ ┌──────────────┐ ┌──────────────┐ - │ 1. PARSE │───▶│ 2. BIND │───▶│ 3. CHECK │ - │ │ │ │ │ │ - │ ReScript │ │ Idris2 │ │ Idris2 │ - │ Tokenise & │ │ Resolve │ │ Type-check │ - │ parse VCL-total │ │ names & │ │ all 10 │ - │ surface │ │ schema refs │ │ safety │ - │ syntax │ │ │ │ levels │ - └──────────────┘ └──────────────┘ └──────────────┘ - │ │ │ - │ AST │ Bound AST │ Typed AST + - │ │ │ Obligations - ▼ ▼ ▼ - ┌──────────────┐ ┌──────────────┐ ┌──────────────┐ - │ 4. ANALYSE │───▶│ 5. COMPILE │───▶│ 6. EXECUTE │ - │ │ │ │ │ │ - │ Idris2 │ │ Zig │ │ Elixir │ - │ Discharge │ │ Generate │ │ Dispatch to │ - │ proof │ │ optimised │ │ VeriSimDB │ - │ obligations │ │ query plan │ │ engine │ - │ │ │ via C ABI │ │ │ - └──────────────┘ └──────────────┘ └──────────────┘ - │ │ │ - │ Proof │ Native │ Result + - │ Certificate │ Query Plan │ Certificate - ▼ ▼ ▼ - ┌─────────────────────────────────────────────────────┐ - │ PROOF CERTIFICATE OUTPUT │ - │ │ - │ Machine-checkable evidence that the query passed │ - │ all 10 safety levels. Independently verifiable. │ - └─────────────────────────────────────────────────────┘ +VCL source -> Rust lexer/parser -> AST -> Rust decider / Idris proof corpus + -> gate verdict (not a transported proof) ---- +The source parser is syntax-only and fail-closed on unsupported L7–L10 +clauses. Schema resolution happens in the decider for ordinary field refs. +The VeriSimDB consumer-side gate integration is a separate outstanding item; +this repository does not currently establish a full parse-to-execution path. + == The 11 Safety Levels -VCL-total enforces 11 distinct safety levels (L0–L10), each targeting a specific -class of bug. The levels are cumulative — a query at Level N has passed all -checks from Levels 0 through N. +The proof corpus defines eleven predicates and dependent certificates, +`ParseSafe` through `EpistemicSafe` (L0–L10), over the `Statement` AST. A +certificate at Level N includes the lower-level obligations; source +expressibility remains bounded by the parser's L6 ceiling. [cols="1,2,3,2,2"] |=== -|Level |Name |What It Prevents |Idris2 Module |Pipeline Stage +|Level |Canonical name |Current predicate scope |Idris2 source |Pipeline stage + +|L0 +|`ParseSafe` +|Statement is in the represented AST +|`Core.Grammar`, `Core.Levels` +|AST / certification |L1 -|Construction Safety -|SQL/VCL injection attacks -|`Injection.idr` -|Parse + Bind +|`SchemaBound` +|Ordinary field references resolve against `OctadSchema` +|`Core.Decide`, `Core.Checker` +|Schema check |L2 -|Schema Pinning -|Schema drift (query vs database mismatch) -|`SchemaEvol.idr` -|Bind +|`TypeCompat` +|Compared expression types are compatible +|`Core.Decide`, `Core.Checker` +|Type check |L3 -|Resource Linearity -|Connection leaks, double-use bugs -|`Linear.idr` +|`NullSafe` +|Implemented null-safety predicate holds +|`Core.Decide`, `Core.Checker` |Check |L4 -|Session Protocols -|Use-after-commit, auth bypass, double-close -|`Session.idr` +|`InjectionProof` +|Implemented raw-string-literal predicate holds +|`Core.Decide`, `Core.Checker` |Check |L5 -|Effect Tracking -|Undeclared side effects (writes in read-only context) -|`Effects.idr` -|Check +|`ResultTyped` +|Selected result expressions satisfy the type predicate +|`Core.Decide`, `Core.Checker` +|Result check |L6 -|Scope Isolation -|Cross-transaction data leaks -|`Modal.idr` +|`CardinalitySafe` +|A `LIMIT` is present +|`Core.Decide`, `Core.Checker` |Check |L7 -|Information Flow -|Security classification violations (secret → public) -|`InfoFlow.idr` -|Check + Analyse +|`EffectTracked` +|An effect declaration is present +|`Core.Decide`, `Core.Checker` +|Check |L8 -|Quantitative Bounds -|Resource overuse beyond declared limits -|`Quantitative.idr` +|`TemporalSafe` +|A version constraint is present +|`Core.Decide`, `Core.Checker` |Check |L9 -|Proof Attachment -|Unverified claims about query results -|`ProofCarrying.idr` -|Analyse +|`LinearSafe` +|A `UseOnce` or bounded linear annotation is present +|`Core.Decide`, `Core.Checker` +|Check |L10 -|Cross-Cutting Invariants -|Violations of compositional properties -|`Proofs.idr` -|Analyse - -|L11 -|Epistemic Safety -|Inconsistent knowledge states across federated agents; unverified claims treated as knowledge; circular epistemic dependencies -|`Epistemic.idr` +|`EpistemicSafe` +|Epistemic clause has declared agents and passes the implemented `ENTAILS`-cycle condition +|`Core.Decide`, `Core.Checker`, `Core.Levels` |Check |=== -NOTE: Level 11 (Epistemic Safety) uses S5 modal logic with Kripke frame -semantics embedded in the Idris2 type system. The EPISTEMIC clause specifies -agents, their knowledge/belief requirements, and common knowledge properties. -The type checker becomes the epistemic model checker — a term of type -`Knows a P` is constructive evidence that agent `a` knows `P`. +NOTE: These are the canonical L0–L10 tags, not the obsolete L1–L11 ladder +in older architecture prose. The proof predicates apply to an already-built +`Statement`; VCL source reaches only through L6 today. L10's current checker +is structural and does not invoke the standalone +Kripke-style S5 formalisation in `Core.Epistemic`. See +link:../audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc[the audit] for the +parser/binder gap and the boundary of the L10 claim. === Level Detail -==== L1: Construction Safety (Injection.idr) - -Queries are unforgeable by construction. The `SafeQuery` type is an opaque AST -indexed by a parameter schema. There is no function `String -> SafeQuery` — user -input can only appear in typed parameter slots, never in query structure -positions. Injection is impossible because the path from untrusted input to -query structure simply does not exist in the type system. - -==== L2: Schema Pinning (SchemaEvol.idr) - -Every query is indexed by the schema version it was validated against. A -`SchemaQuery v` can only execute against a database at version `v`. Schema -migrations produce `Migration from to` proofs, and queries must be explicitly -re-validated via `migrateQuery` with evidence that all referenced columns -survive the migration. - -==== L3: Resource Linearity (Linear.idr) - -Database connections carry a usage count at the type level. A `LinConn (S n)` -must be consumed exactly once per scope — the Idris2 compiler enforces this -via QTT quantity `1`. Dropped connections are compile-time errors. Double-use -is impossible. - -==== L4: Session Protocols (Session.idr) - -Sessions are state machines indexed by their protocol state. The type -`Session : SessionState -> Type` ensures transitions follow the protocol: -`Fresh → Authenticated → InTransaction → Committed → Closed`. Querying after -commit, committing without a transaction, and closing twice are all type errors. - -==== L5: Effect Tracking (Effects.idr) - -Each query declares its effects (`Read`, `Write`, `Cite`, `Audit`, `Transform`, -`Federate`). The `Subsumes` proof verifies that actual operations are a subset -of declared effects. A query declared `EFFECTS { Read }` that attempts a write -is rejected at compile time. - -==== L6: Scope Isolation (Modal.idr) - -Data accessed in one transaction scope is wrapped in `Box w a`, where `w` is a -world tag representing the scope. Extracting data requires proof of being in the -same scope (`InScope w`). Cross-scope data flow requires explicit `marshal` -calls, making all boundary crossings visible in the type signature. - -==== L7: Information Flow (InfoFlow.idr) - -Data carries security classifications (`Public`, `Internal`, `Confidential`, -`Secret`, `TopSecret`) forming a lattice. The `FlowsTo` relation ensures data -can only move upward in classification. Reading a `Secret` value requires -`HasClearance Secret` evidence and a `FlowsTo Secret readerLevel` proof. -Downward flows are impossible — the constructor does not exist. - -==== L8: Quantitative Bounds (Quantitative.idr) - -Generalises linearity from "exactly once" to "at most N". A -`BoundedResource n a` can be consumed `n` times before depletion. Parallel -query branches can split a resource budget via `merge`/`split`. This enforces -API rate limits, connection pool bounds, and quota compliance at compile time. - -==== L9: Proof Attachment (ProofCarrying.idr) - -Query results carry formal theorems as dependent pairs: -`ProvedResult a thm` bundles data with a proof of integrity, freshness, -provenance, or consistency. The proof can be independently verified via -`verify`, which returns `Either VerifyError (result : a ** Holds thm result)`. - -==== L10: Cross-Cutting Invariants (Proofs.idr) +The canonical level names and actual predicate scopes are listed in the table +above. Implementation anchors are `src/core/Levels.idr`, +`src/core/Decide.idr`, and `src/core/Checker.idr`; the source parser and its +fail-closed L7–L10 gap are in `src/interface/parse/src/parser.rs`. Do not use +the historical L1–L11 names or module mappings from earlier versions of this +architecture as a description of the current implementation. -Compositional properties that span multiple levels: subset transitivity, -subsumption monotonicity, flow lattice transitivity. These proofs ensure that -the safety levels compose correctly — e.g., adding effects never breaks -existing subsumption proofs, and chained migrations preserve column survival. +== Implemented Components -== Technology Stack - -[cols="1,2,3"] -|=== -|Technology |Role |Rationale - -|**Idris2** -|ABI definitions, type kernel, proof obligations -|Native QTT (quantity `0`/`1`/`ω`) makes linear types and resource tracking -first-class. Dependent types enable schema-indexed queries. `%default total` -with zero `believe_me` guarantees all proofs are real. - -|**Zig** -|FFI bridge, native codegen -|C-ABI compatible without overhead. Cross-compilation built-in. Zero runtime -dependencies. Exports the type checker's validation functions to non-Idris2 -consumers via the hyperpolymath ABI/FFI standard. - -|**ReScript** -|Surface syntax parser -|Consistent with existing VCL parser patterns in VeriSimDB. Compiles to -JavaScript for browser-based tooling. Extends the VCL v3.0 grammar with 6 -new optional clauses. - -|**zig** -|HTTP API gateway -|Exposes VCL-total as a REST API for external consumers. Fast compilation, -minimal runtime. Follows the hyperpolymath zig API triple pattern. - -|**Elixir** -|VeriSimDB integration, query orchestration -|BEAM runtime for distributed query dispatch. Phoenix for real-time feedback. -Zig NIFs for performance-critical paths. Native supervision trees for fault -tolerance. +[cols="1,2"] |=== +|Component |Current role -=== Technology Interaction - -[source] ----- - ┌──────────────────────────────────────────────────────────┐ - │ CLIENT (Browser/CLI) │ - └──────────────────────┬───────────────────────────────────┘ - │ HTTP/WebSocket - ▼ - ┌──────────────────────────────────────────────────────────┐ - │ zig API GATEWAY (v-api/) │ - │ Routes: POST /check, POST /compile, GET /levels/:id │ - └──────────────────────┬───────────────────────────────────┘ - │ FFI (C ABI) - ▼ - ┌──────────────────────────────────────────────────────────┐ - │ ZIG FFI BRIDGE (ffi/zig/) │ - │ Exports: vqlut_parse, vqlut_check, vqlut_compile │ - │ Generates: C headers (generated/abi/*.h) │ - └──────┬──────────────────────────────┬────────────────────┘ - │ Parse │ Check + Compile - ▼ ▼ - ┌────────────────┐ ┌─────────────────────────────┐ - │ RESCRIPT PARSER │ │ IDRIS2 TYPE KERNEL │ - │ (src/parser/) │ │ (src/abi/) │ - │ │ │ │ - │ Tokenise │ │ 12 modules: │ - │ Parse │──AST──▶ │ Core + 10 safety levels + │ - │ Surface check │ │ Checker (unified validator) │ - └─────────────────┘ └──────────────┬──────────────┘ - │ Proof Certificate - ▼ - ┌─────────────────────────────┐ - │ ELIXIR ORCHESTRATION │ - │ (elixir/) │ - │ │ - │ Dispatch to VeriSimDB engine │ - │ Real-time feedback via │ - │ Phoenix Channels │ - │ Zig NIFs for hot paths │ - └──────────────────────────────┘ ----- +|Rust (`src/interface/parse`) +|Trusted, panic-free source parser, AST/wire codec, independent decider, + and `vclt-gate` producer. Source support currently reaches L6. -== The TypeLL Connection +|Idris2 (`src/core`, `verification/proofs`) +|Total proof corpus for the represented AST, including L0–L10 predicates, + soundness and dependent `SafetyCertificate` values. -VCL-total's 10 safety levels map 1:1 to TypeLL's 10 type theory levels. This is -not a coincidence — VCL-total is the *database specialisation* of TypeLL's -general-purpose type system. +|VeriSimDB consumer integration +|The gate producer contract exists; the consumer does not yet invoke it. -[cols="1,2,2,2"] +|External proof transport +|The dependent Idris proof object is not transported as a re-checkable proof. |=== -|Level |TypeLL Concept |VCL-total Instantiation |Module - -|1 -|Construction Types -|Unforgeable query ASTs -|`Injection.idr` - -|2 -|Indexed Types -|Schema-versioned queries -|`SchemaEvol.idr` - -|3 -|Linear Types -|Resource-counted connections -|`Linear.idr` - -|4 -|Session Types -|Database protocol state machines -|`Session.idr` - -|5 -|Effect Types -|Declared vs actual effect sets -|`Effects.idr` - -|6 -|Modal Types -|Transaction scope isolation -|`Modal.idr` - -|7 -|Information Flow Types -|Security classification lattice -|`InfoFlow.idr` - -|8 -|Quantitative Types -|Bounded resource accounting -|`Quantitative.idr` - -|9 -|Proof-Relevant Types -|Theorem-carrying query results -|`ProofCarrying.idr` - -|10 -|Metatheoretic Types -|Cross-cutting compositional invariants -|`Proofs.idr` -|=== - -TypeLL provides the *theory*; VCL-total provides the *practice*. Every TypeLL level -has a concrete, tested implementation in VCL-total's Idris2 kernel. This makes -VCL-total both a useful tool and a validation of TypeLL's design. - -== Data Flow - -=== Parse Stage -[source] ----- - VCL-total Source Text - ───────────────── - "SELECT GRAPH, DOCUMENT - FROM HEXAD 550e8400-... - WHERE FULLTEXT CONTAINS $query - CONSUME AFTER 1 USE - EFFECTS { Read, Cite } - PROOF ATTACHED IntegrityTheorem" - - │ - │ ReScript Tokeniser - ▼ - - Token Stream - ──────────── - [SELECT, GRAPH, COMMA, DOCUMENT, FROM, HEXAD, UUID(...), - WHERE, FULLTEXT, CONTAINS, PARAM("query"), - CONSUME, AFTER, INT(1), USE, - EFFECTS, LBRACE, READ, COMMA, CITE, RBRACE, - PROOF, ATTACHED, IDENT("IntegrityTheorem")] - - │ - │ ReScript Parser - ▼ - - Untyped AST (TQLAst.res) - ───────────────────────── - Select { - modalities: [Graph, Document], - source: Hexad("550e8400-..."), - where: Fulltext(ParamRef("query")), - extensions: [ - ConsumeAfter(1), - Effects([Read, Cite]), - ProofAttached("IntegrityTheorem") - ] - } ----- +== Cross-Project Relationship -=== Bind Stage +Earlier versions of this document claimed a 1:1 mapping between VCL-UT levels +and TypeLL levels. That mapping is not established by the VCL-UT source or proof +corpus and is withdrawn here. Shared terminology, a level number, or a similar +type name is not an interface contract or a proof of dependency. Any +cross-project dependency must cite an explicit versioned artefact, import, +enforced build/deployment rule, or local theorem. -[source] ----- - Untyped AST + Schema v3 - ───────────────────────── - - │ - │ Idris2 Schema Resolution - │ (SchemaEvol.idr) - ▼ - - Bound AST - ────────── - SchemaQuery 3 { - select: SafeSelect [Graph, Document] hexadRef, - params: [MkTypedParam "query" PString], - schema: schemaV3 - } - - + ColumnExists proofs for each referenced column - + SchemaQuery indexed by version 3 ----- - -=== Check Stage - -[source] ----- - Bound AST - ────────── - - │ - │ 10 Safety Level Checks (Idris2) - ▼ - - Typed AST + Proof Obligations - ───────────────────────────── - L1: SafeQuery searchSchema ✓ (construction safety) - L2: SchemaQuery 3 ✓ (schema pinning) - L3: LinConn 1 ✓ (single use) - L4: Session InTransaction ✓ (protocol state) - L5: Subsumes [Read,Cite] [Read,Cite] ✓ (effects subset) - L6: Box txWorld result ✓ (scope isolation) - L7: Labeled Public result ✓ (classification) - L8: BoundedResource 1 conn ✓ (quantitative) - L9: ProvedResult a IntegrityThm ○ (obligation: prove integrity) - L10: flowTransitive, subsetTransitive ✓ (compositional) - - Outstanding obligations: [IntegrityTheorem discharge] ----- +The same rule applies to choreographic K-CUT: no local artifact establishes it +as a VCL-UT deployment blocker. See +link:../audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc[the relationship audit]. -=== Analyse Stage - -[source] ----- - Typed AST + Obligations - ──────────────────────── - - │ - │ Proof Discharge (Idris2) - ▼ - - Proof Certificate - ───────────────── - Certificate { - query_hash: "sha256:abc123...", - safety_levels: [L1..L10], - each_level: PASS, - proofs_discharged: [IntegrityTheorem], - verified_at: "2026-03-16T10:30:00Z", - schema_version: 3, - idris2_version: "0.8.0" - } ----- +== Data Flow -=== Compile + Execute Stages +The current implemented boundary is intentionally narrower than the historical +diagram that previously appeared here: [source] ---- - Proof Certificate + Typed AST - ────────────────────────────── - - │ - │ Zig Codegen (ffi/zig/) - ▼ - - Native Query Plan - ───────────────── - Optimised execution plan with: - - Parameter binding slots - - Modality access pattern - - Resource budget annotations - - │ - │ Elixir Dispatch - ▼ - - VeriSimDB Engine - ──────────────── - Execute query plan, return result + certificate ----- - -== Error Propagation - -Each safety level produces typed errors that propagate through the pipeline: - -[cols="1,2,3"] -|=== -|Level |Error Type |Example - -|L1 -|`InjectionError` -|"Untrusted string in query structure position" - -|L2 -|`SchemaMismatch` -|"Column 'age' does not exist at schema version 2" - -|L3 -|`LinearityViolation` -|"Connection used twice in linear context" - -|L4 -|`ProtocolViolation` -|"Cannot query in state Committed" - -|L5 -|`EffectViolation` -|"Write effect not declared (declared: [Read])" - -|L6 -|`ScopeEscape` -|"Data from transaction scope 'tx1' leaked to 'tx2'" - -|L7 -|`ClassificationViolation` -|"Secret data cannot flow to Public context" - -|L8 -|`ResourceExhausted` -|"Resource limit 5 exceeded (attempted 6 uses)" - -|L9 -|`ProofFailure` -|"IntegrityTheorem could not be discharged" - -|L10 -|`CompositionError` -|"Subsumption monotonicity violated after effect addition" -|=== - -Errors are *structured*, not string messages. Each error carries the evidence -needed to understand and fix the problem — including the safety level, the -specific obligation that failed, and the source location. - -== The Proof Certificate Concept - -A proof certificate is a machine-checkable artefact produced by VCL-total's -pipeline. It attests that a query has passed all applicable safety levels. - -Properties of a proof certificate: - -1. **Independently verifiable**: Any party with the Idris2 type kernel can - re-check the certificate without trusting VCL-total's implementation. - -2. **Tamper-evident**: The certificate includes a SHA-256 hash of the query - AST. Modifying the query invalidates the certificate. - -3. **Level-granular**: The certificate reports each safety level individually. - A query might pass L1–L8 but fail L9 (proof attachment). This granularity - enables graduated deployment. - -4. **Composable**: Certificates for sub-queries compose into certificates for - compound queries, subject to L10 (cross-cutting invariant) checks. - -5. **Versioned**: Certificates are pinned to schema version, Idris2 kernel - version, and VCL-total grammar version. Version mismatches require - re-certification. - -=== Certificate Format - -[source,json] ----- -{ - "version": "1.0.0", - "query_hash": "sha256:2cf24dba5fb0a30e26e83b2ac5b9e29e1b161e5c1fa7425e73043362938b9824", - "schema_version": 3, - "certified_at": "2026-03-16T10:30:00Z", - "kernel_version": "vcl-total-0.1.0", - "idris2_version": "0.8.0", - "levels": { - "L1_construction": { "status": "pass", "module": "Injection.idr" }, - "L2_schema": { "status": "pass", "module": "SchemaEvol.idr" }, - "L3_linearity": { "status": "pass", "module": "Linear.idr" }, - "L4_session": { "status": "pass", "module": "Session.idr" }, - "L5_effects": { "status": "pass", "module": "Effects.idr" }, - "L6_modal": { "status": "pass", "module": "Modal.idr" }, - "L7_infoflow": { "status": "pass", "module": "InfoFlow.idr" }, - "L8_quantitative": { "status": "pass", "module": "Quantitative.idr" }, - "L9_proof": { "status": "pass", "module": "ProofCarrying.idr" }, - "L10_metatheory": { "status": "pass", "module": "Proofs.idr" } - }, - "obligations_discharged": ["IntegrityTheorem", "FreshnessTheorem"], - "signature": "ed25519:..." -} ----- +VCL source text + -> Rust lexer/parser (`src/interface/parse`) + -> syntax AST (`Statement` / `VclOp`) + -> versioned wire representation / gate request + -> safety decider and Idris proof corpus + -> verdict / certificate status +---- + +The parser establishes syntax, not schema-bound types or a full certificate. +It rejects `PROOF`, `EFFECTS`, `AT`, `CONSUME`, `USAGE`, `EPISTEMIC`, and modal +expressions fail-closed. Consequently source reaches only through L6. The AST +and wire format contain extension fields, so constructed or wire-decoded +statements may carry L7–L10 data; that is distinct from source expressibility. +Ordinary field-reference resolution against `OctadSchema` occurs in the +decider. + +The gate consumer is not yet wired into VeriSimDB. The Idris dependent +`SafetyCertificate` is not transported as a re-checkable proof object across +the external boundary; see `verification/proofs/VERIFICATION-STANCE.adoc` and +`docs/vclt-gate-contract.adoc` for the exact current contract. + +== Gate Verdict and Proof Boundary + +The Rust parser returns a typed `ParseError` and fails closed on unsupported +syntax. `vclt-gate` reports a schema-versioned JSON verdict with `requested_level`, +`certified_level`, per-level results, and reason categories; see +`docs/vclt-gate-contract.adoc` for the normative wire schema. A `certified_level` +tag is a verdict from the gate, not a serialized Idris proof object. + +The Idris corpus contains dependent `SafetyCertificate` constructors and +soundness lemmas over `Statement`. That proof object is not transported across +the external boundary. Consumers must not treat the numeric level alone as a +re-checkable proof or as evidence of properties outside the corresponding local +predicate. See `verification/proofs/VERIFICATION-STANCE.adoc`. + +== Certificate Scope + +The term *certificate* is used for the dependent Idris value assembled by +`Checker.certifyAt` / `certifyRequested` inside the proof corpus. It does not +mean the current Rust gate emits a serialized dependent proof. Keep three +claims distinct: the predicates and certificates are specified/proved over an +AST; the source parser reaches only through L6; and no external deployment +dependency follows from those proofs without an explicit bridge artefact. == Licence diff --git a/docs/architecture/DECISIONS.adoc b/docs/architecture/DECISIONS.adoc index f0d3253..b878ef6 100644 --- a/docs/architecture/DECISIONS.adoc +++ b/docs/architecture/DECISIONS.adoc @@ -1,12 +1,12 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) 2026 Jonathan D.A. Jewell -= VCL-total Architecture Decision Records += VCL-UT Architecture Decision Records Jonathan D.A. Jewell :date: 2026-03-16 :toc: macro :toclevels: 3 :icons: font -:description: Architecture Decision Records for VCL-total design choices +:description: Architecture Decision Records for VCL-UT design choices toc::[] @@ -22,29 +22,29 @@ toc::[] |2026-03-01 |ADR-0002 -|Use Idris2 over Lean for the type kernel -|Accepted -|2026-03-01 +|Idris2 engineering proof kernel (scope clarified) +|Accepted, clarified +|2026-11-01 |ADR-0003 -|10 safety levels, not fewer -|Accepted -|2026-03-16 +|Historical level count and taxonomy +|Superseded +|2026-11-01 |ADR-0004 -|VCL-total supersedes VCL-DT -|Accepted -|2026-03-16 +|Historical VCL-DT supersession proposal +|Superseded +|2026-11-01 |ADR-0005 -|ReScript for the parser -|Accepted -|2026-03-01 +|ReScript parser decision +|Superseded +|2026-11-01 |ADR-0006 -|Epistemic types via S5 modal logic -|Accepted -|2026-04-10 +|Epistemic formalisation and L10 scope +|Accepted, clarified +|2026-11-01 |ADR-0007 |Separate modality profiles from the fixed Octad schema (see link:../decisions/0007-modality-profiles-vs-octad-schema.adoc[record]) @@ -54,513 +54,168 @@ toc::[] --- -== ADR-0002: Use Idris2 over Lean for the Type Kernel +== ADR-0002: Idris2 Engineering Proof Kernel (Scope Clarified) === Status -Accepted (2026-03-01) - -=== Context - -VCL-total requires a dependently-typed language for its type kernel — the -component that formally specifies and checks the 10 safety levels. The two -serious candidates were **Idris2** and **Lean 4**. - -Both are mature dependently-typed languages with: - -- Full dependent types (Pi, Sigma, indexed families) -- Totality checking -- Compiled backends (not just interpreted) -- Active development and community - -The choice affects every safety level module and the project's long-term -maintainability. +Accepted, scope clarified (2026-11-01; original decision 2026-03-01) === Decision -Use **Idris2** for the type kernel. - -=== Rationale - -==== 1. Quantitative Type Theory (QTT) is Native - -Idris2 is built on QTT. Every variable binding carries a quantity: - -- `0` — erased at compile time (type-level only) -- `1` — used exactly once (linear) -- `omega` — used any number of times (unrestricted) - -This means VCL-total's L3 (Resource Linearity) and L8 (Quantitative Bounds) are -*first-class features of the language*, not encodings. A linear connection is -simply: - -[source,idris] ----- -useConn : (1 conn : Connection) -> IO Result ----- - -The Idris2 compiler enforces linearity. No custom checker needed. - -In Lean 4, linearity must be encoded manually — typically via monadic wrappers -or custom elaboration. This encoding is heavier, more fragile, and harder to -audit. - -==== 2. Erasure Annotations - -Idris2's quantity `0` means "erased at runtime". This is critical for VCL-total's -proof certificates: the proofs exist at the type level but are erased from the -compiled output. The compiled query plan carries no proof overhead. - -Lean 4 has `@[reducible]` and `noncomputable`, but the erasure story is less -precise and less integrated with the type system. - -==== 3. Totality Checking Built In - -Idris2's `%default total` directive makes totality the default, with explicit -opt-out via `%default covering` or `partial`. This matches VCL-total's invariant -that all functions must be total. - -Lean 4 also has totality checking, but it is less strict by default and requires -more manual annotation. - -==== 4. Hyperpolymath Ecosystem Alignment - -Idris2 is the standard formal verification language across the hyperpolymath -ecosystem (proven-servers, TypeLL, ABI definitions). Using Lean would introduce -a second formal language, complicating tooling, CI, and developer onboarding. - -==== 5. Practical Concern: Build Speed - -Idris2 compiles faster than Lean 4 for the size of modules in VCL-total (typically -100–300 lines). The type-check-edit cycle is noticeably faster. - -=== Alternatives Considered - -[cols="1,3"] -|=== -|Alternative |Why Rejected - -|**Lean 4** -|No native QTT. Linearity requires encoding. Different ecosystem from -hyperpolymath. Heavier toolchain. - -|**Agda** -|Excellent type theory but no practical compilation backend. Research tool, -not production tool. - -|**Coq/Rocq** -|Tactics-based proof style is powerful but harder to read. Extraction to -OCaml adds a translation layer. Licence (LGPL) less compatible. +Retain Idris2 for the repository's dependent AST, level predicates, +certificates, and engineering/interface obligations in the checked proof +corpus. This is a repository-specific tool choice, not a claim that Idris2 is +the estate-wide verifier for every proof class. -|**F*** -|Strong on effects but less expressive dependent types. Tied to the .NET -ecosystem. +=== Policy alignment -|**ATS2** -|Rejected per hyperpolymath policy. Idris2 is the designated formal -verification language. -|=== +Apply the current Standards proof mapping: Idris2 for engineering/API/ABI +contracts; Creusot for first-party Rust code; Agda as source for +implementation-independent theory, with rechecks in Rocq and Lean. Mathesis +Grade 3 denotes a locally checked Agda formulation, not an Idris2 build. The +separate `../../verification/proofs/AGDA-GRADE3-PORT-PLAN.adoc` records that proposed theory work. -=== Consequences +Do not derive safety-level meanings from Idris2 features: canonical L3 is +`NullSafe`, L8 is `TemporalSafe`, and L9 is `LinearSafe`. The present L9 +predicate checks an AST annotation; it is not a proof of runtime resource +linearity. QTT or erased proof terms do not establish source-parser correctness, +external proof transport, or a deployment property. -- All 10 safety levels are implemented as Idris2 modules. -- L3 and L8 use native QTT quantities, making them simpler and more trustworthy - than they would be in any other language. -- Developers contributing to the type kernel must learn Idris2. -- Proofs are erased from compiled output, so runtime performance is unaffected. +For current proof claims and residuals see +`../../verification/proofs/VERIFICATION-STANCE.adoc`; for the estate proof-grade +and verifier policy mapping see the +link:../audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc[audit]. ---- - -== ADR-0003: 10 Safety Levels, Not Fewer +== ADR-0003: Historical Level Count and Taxonomy === Status -Accepted (2026-03-16) - -=== Context - -The original VCL-dt system had 6 PROOF types. During the design of VCL-total, the -question arose: why not consolidate into fewer, broader levels? Fewer levels -would be simpler to explain and implement. - -=== Decision - -VCL-total has exactly **10 safety levels**, each targeting a distinct class of bug. - -=== Rationale - -==== Each Level Catches a Distinct Class of Bug - -The 10 levels are not arbitrary subdivisions — each one prevents a specific, -well-documented category of failure: - -[cols="1,2,3"] -|=== -|Level |Class of Bug |Real-World Example - -|L1 -|Injection attacks -|SQL injection via string concatenation (OWASP Top 10 #1) - -|L2 -|Schema drift -|Query references column dropped in migration (silent runtime failure) - -|L3 -|Resource leaks -|Database connection not closed (pool exhaustion, OOM) - -|L4 -|Protocol violations -|Query executed after transaction committed (stale data) - -|L5 -|Undeclared effects -|Read-only API endpoint that silently writes to the database - -|L6 -|Scope escapes -|Data from rolled-back transaction used in committed context - -|L7 -|Classification leaks -|Confidential data appearing in public API response - -|L8 -|Resource overuse -|API key used beyond its rate limit (account suspension) - -|L9 -|Unverified claims -|"Data is fresh" claim without a freshness proof - -|L10 -|Composition bugs -|Two safety levels interact to create a loophole -|=== - -Merging any two of these would lose the ability to independently control and -report on each class. For example, merging L3 (linearity) and L8 (quantitative) -would conflate "exactly once" with "at most N" — these are related but -distinct properties. - -==== Graduated Adoption - -10 levels enable graduated adoption. A team can start at L1 (injection safety) -and progressively enable higher levels as confidence grows. With fewer levels, -the jumps would be larger and harder to adopt incrementally. - -==== 1:1 Mapping to TypeLL - -TypeLL defines exactly 10 type theory levels. The 1:1 mapping between TypeLL -and VCL-total means VCL-total serves as both a useful tool and a concrete validation -of TypeLL's design. Changing the number of levels would break this alignment. - -==== Independent Modules - -Each level is implemented as an independent Idris2 module. This means: - -- Levels can be developed, tested, and reviewed independently. -- A bug in one level's implementation does not affect other levels. -- New levels can be added without modifying existing modules. - -=== Alternatives Considered - -[cols="1,3"] -|=== -|Alternative |Why Rejected - -|**6 levels** (matching VCL-dt's 6 PROOF types) -|Misses injection safety (L1), schema pinning (L2), information flow (L7), -and quantitative bounds (L8). These are critical for production safety. +Superseded (2026-11-01; original decision 2026-03-16) -|**3 levels** (parse safety, type safety, proof safety) -|Too coarse. "Type safety" would be a grab-bag of linearity, effects, sessions, -modality, and information flow. Loses granular control and reporting. +=== Record -|**Unlimited levels** (extensible without bound) -|The 10-level structure provides a clear mental model. Extensibility is -supported (new levels can be added), but the core 10 are fixed. -|=== +This ADR captured a design proposal for ten levels numbered 1–10 and asserted +a one-to-one correspondence with TypeLL. Those statements are superseded and +must not be used as current implementation or cross-repository evidence. -=== Consequences +The canonical code and wire tags are eleven levels, L0–L10: +`ParseSafe`, `SchemaBound`, `TypeCompat`, `NullSafe`, `InjectionProof`, +`ResultTyped`, `CardinalitySafe`, `EffectTracked`, `TemporalSafe`, +`LinearSafe`, and `EpistemicSafe`. The trusted Rust source parser reaches only +through L6. The L0–L10 Idris predicates and certificates apply to an already +constructed `Statement`. -- VCL-total always reports 10 levels in its safety dashboard and proof certificates. -- Each level has its own error type, Idris2 module, and documentation section. -- TypeLL and VCL-total remain in 1:1 correspondence. -- The `safety_level` API parameter accepts values 1–10 for graduated checking. +No exact interface, source import, or theorem in this repository establishes +a one-to-one mapping to TypeLL or another repository's level numbering. +Shared ordinal numbers or similar names do not establish correspondence. +Use the canonical table in `ARCHITECTURE.adoc` and the +link:../audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc[2026-11-01 audit]. --- -== ADR-0004: VCL-total Supersedes VCL-DT +== ADR-0004: Historical VCL-DT Supersession Proposal === Status -Accepted (2026-03-16) - -=== Context - -VeriSimDB currently has two query type systems: - -- **VCL-DT** (Dependently Typed): covers 6 PROOF types (Pi, Sigma, dependent - pattern matching, basic type checking, universe polymorphism, implicit - arguments). ~35% wired into VeriSimDB. - -- **VCL-total** (Unified Types): covers 10 safety levels with full formal - verification. Successor to VCL-dt++ (typeql-experimental). - -The question: should VCL-total replace VCL-DT, or coexist alongside it? - -=== Decision - -VCL-total **supersedes** VCL-DT. VCL-DT remains available as a legacy path but -receives no further development. - -=== Rationale - -==== VCL-total is a Strict Superset - -Every safety property that VCL-DT checks is also checked by VCL-total: - -[cols="2,1,1"] -|=== -|VCL-DT Feature |VCL-total Coverage |Level - -|Pi types (function types) -|Covered -|L1 (Construction Safety — typed parameter schemas) +Superseded / scope withdrawn (2026-11-01; original decision 2026-03-16) -|Sigma types (dependent pairs) -|Covered -|L9 (Proof Attachment — ProvedResult is a sigma pair) +=== Record -|Dependent pattern matching -|Covered -|All levels (native Idris2 feature) +The earlier claim that VCL-UT is a strict superset of VCL-DT, including the +claim that VCL-DT's six `PROOF` types are covered by VCL-UT L9–L10, is +withdrawn. The current canonical meanings are L9 `LinearSafe` and L10 +`EpistemicSafe`; they are not `Proof Attachment` and `Cross-Cutting Invariants`. +The trusted Rust parser rejects `PROOF`, and no current source path establishes +automatic proof-type validation by L9–L10. -|Basic type checking -|Covered -|L1–L2 (construction + schema) - -|Universe polymorphism -|Covered -|Core.idr foundation types - -|Implicit arguments -|Covered -|All levels (native Idris2 feature) -|=== - -VCL-total additionally covers linearity (L3), sessions (L4), effects (L5), -modality (L6), information flow (L7), quantitative bounds (L8), and -compositional invariants (L10) — none of which VCL-DT addresses. - -==== Single Codebase Reduces Maintenance - -Maintaining two type systems creates confusion about which one to use, -duplicates testing effort, and risks divergent semantics. A single type system -(VCL-total) with configurable safety levels (`--level 1` through `--level 10`) -provides the same flexibility without duplication. - -==== Graduated Migration Path - -VCL-DT's existing ~35% wiring in VeriSimDB is not wasted. VCL-total's L1 and L2 -levels approximately correspond to VCL-DT's type checking. Teams currently -using VCL-DT can migrate to VCL-total at level 2 with minimal disruption, then -increase levels over time. - -=== Alternatives Considered - -[cols="1,3"] -|=== -|Alternative |Why Rejected - -|**Keep both active** -|Doubles maintenance, creates confusion about which to use, risks semantic -divergence. - -|**Merge VCL-DT into VCL-total** -|VCL-DT's implementation is too different (no Idris2, no formal proofs). A -clean reimplementation in VCL-total's framework is more reliable than a merge. - -|**Deprecate without replacement** -|Removes safety guarantees. Unacceptable. -|=== - -=== Consequences - -- VCL-DT enters maintenance mode (security fixes only, no new features). -- The Slipstream (untyped) and VCL-total paths are the two active query paths. -- VeriSimDB documentation points to VCL-total for all new safety-critical work. -- The `typeql-experimental` directory in `nextgen-databases` is the historical - prototype; `vcl-total` is the production successor. +This record does not decide whether VCL-DT should be retired or how a future +migration should work. Any such relationship requires an explicit current +interface contract and proof/evidence mapping. See the current parser status +in `ROADMAP.adoc` and the +link:../audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc[audit]. --- -== ADR-0005: ReScript for the Parser +== ADR-0005: ReScript Parser Decision (Superseded) === Status -Accepted (2026-03-01) - -=== Context - -VCL-total needs a parser for its surface syntax. The parser must: - -1. Extend the existing VCL v3.0 grammar with 6 new optional clauses. -2. Run both server-side (API gateway) and client-side (PanLL query editor panel). -3. Be maintainable by the existing team. -4. Produce an AST that can be consumed by the Idris2 type kernel. - -=== Decision - -Use **ReScript** for the VCL-total parser. - -=== Rationale - -==== 1. Extends Existing VCL Parser - -VeriSimDB's existing VCL parser is written in ReScript. VCL-total's parser extends -this parser with new clauses rather than reimplementing from scratch. This -ensures consistency between VCL and VCL-total surface syntax and reduces the -risk of subtle parsing differences. - -==== 2. Runs Everywhere - -ReScript compiles to JavaScript, which runs: - -- Server-side via Deno (API gateway and build tooling) -- Client-side in the browser (PanLL query editor panel) -- In Elixir via embedded V8 (for hot-path parsing in the orchestration layer) - -This universality means one parser implementation serves all deployment targets. - -==== 3. Team Expertise - -The hyperpolymath team has deep ReScript expertise (the maintainer is on the -ReScript core team). This reduces ramp-up time and ensures idiomatic code. - -==== 4. Type-Safe Without TypeScript - -ReScript provides OCaml-grade type safety (algebraic data types, exhaustive -pattern matching, type inference) without TypeScript's unsoundness. This is -critical for a parser that must correctly represent VCL-total's rich syntax. - -==== 5. No Keyword Conflicts +Superseded (2026-11-01; original decision 2026-03-01) -VCL-total's 6 new clause keywords (`CONSUME`, `SESSION`, `EFFECTS`, `TRANSACTION`, -`ATTACHED`, `USAGE`) were chosen to be disjoint from VCL's 60+ reserved -keywords. The ReScript parser handles these as simple token extensions with no -ambiguity. +=== Record -=== Alternatives Considered +The ReScript parser decision predates the trusted parser now used at the +VCL-UT boundary. The trusted, fail-closed source parser is the Rust crate +`src/interface/parse`; it produces the mirrored AST, wire representation, +and `vclt-gate` input. Its current source ceiling is L6. ReScript-side/editor +frontends, where present, are not the trusted parser unless their output +correspondence is separately established. -[cols="1,3"] -|=== -|Alternative |Why Rejected - -|**Idris2 parser** -|Idris2's parsing libraries are immature. Running an Idris2 parser in the -browser would require compilation to JavaScript, which is not well supported. - -|**Zig parser** -|Cannot run in the browser without WASM compilation. Does not extend the -existing VCL parser. - -|**Rust parser (nom/pest)** -|Cannot run in the browser without WASM. Does not extend the existing VCL -parser. Would require maintaining two parser codebases (Rust for VCL-total, -ReScript for VCL). - -|**Tree-sitter grammar** -|Good for syntax highlighting but not for producing typed ASTs. Would still -need a separate semantic parser. - -|**TypeScript** -|Banned per hyperpolymath policy. ReScript is the designated replacement. -|=== - -=== Consequences - -- The VCL-total parser lives in `src/parser/` and is written entirely in ReScript. -- The parser produces `TQLAst.res` nodes that are serialised to JSON for - consumption by the Idris2 type kernel. -- The parser runs in Deno (server), the browser (PanLL panels), and embedded - V8 (Elixir NIFs). -- Parser changes require corresponding grammar updates in - `docs/vcl-dtpp-grammar.ebnf`. +The Rust parser rejects the L7–L10 extension clauses and modal expressions; +closing that gap requires source syntax plus elaboration/binding and explicit +cross-frontend reconciliation. The earlier claims in this ADR about one +ReScript parser serving all deployment targets are design history, not a +current trust or deployment dependency. See `ROADMAP.adoc` and the +link:../audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc[audit]. --- -== ADR-0006: Epistemic Types via S5 Modal Logic +== ADR-0006: Epistemic Formalisation and L10 Scope === Status -Accepted (2026-04-10) +Accepted; scope clarified (2026-11-01; original decision 2026-04-10) === Context -VCL-total's 10 safety levels (L0–L9) cover syntactic, type-theoretic, and -resource-level properties. However, in a federated consonance engine where -multiple agents (provers, validators, users) interact, there is no mechanism -to reason about *what agents know* about the system state. - -Without epistemic types, a prover's verification result and a user's -unverified claim have the same type. This conflation undermines the trust -model of the consonance engine. +The canonical safety ladder has eleven tags, L0–L10. L10 is named +`EpistemicSafe`. The repository also contains epistemic type constructors and +an Idris2 Kripke-style S5 formalisation. These are distinct pieces of work: +the presence of the semantics module does not by itself show that L10's +source syntax or deployment path uses that model. === Decision -Introduce Level 10 (EpistemicSafe) using S5 epistemic modal logic embedded -in Idris2's dependent type system. The implementation includes: - -1. **Kripke frame semantics** with S5 equivalence relation proofs - (reflexive, symmetric, transitive accessibility) -2. **Knowledge (K) and Belief (B) type constructors** as first-class VqlTypes - (`TKnows`, `TBelieves`, `TCommonKnowledge`) -3. **Common knowledge (C)** for federation-wide consensus properties -4. **Public Announcement Logic (PAL)** for modelling epistemic state changes -5. **Knowledge transfer proofs** (ENTAILS) for inter-agent reasoning +Retain L10 `EpistemicSafe` as a specified and proved predicate over the +`Statement` AST. Its current checker condition is structural: the statement +has an epistemic clause, declares at least one agent, references only declared +agents, and satisfies the implemented `ENTAILS`-cycle condition. The proof +certificate establishes that checker predicate, not a general semantic +warrant and not a deployment dependency on choreographic K-CUT. -The S5 axioms (T, K, 4, 5) are encoded as dependent types, making the -Idris2 type checker the epistemic model checker. +`src/core/Epistemic.idr` separately formalises Kripke-style S5 frames, +accessibility properties, satisfaction and epistemic operators. It is included +in the proof package, but the L10 `Checker`/`Decide` path does not import or +invoke it. No local theorem connects that module to L10 certification, K-CUT, +or a deployment requirement. Preserve this separation unless an explicit +interface and proof establish a bridge. === Rationale -==== 1. The Trust Gap - -In VeriSimDB, a prover verifying a theorem and a user claiming a theorem -produce structurally identical data. Without epistemic types, the system -cannot distinguish: - -- `Knows ENGINE (status = 'verified')` — the engine has checked this -- `Believes USER:alice (status = 'verified')` — Alice claims this - -This distinction is fundamental to the consonance model. - -==== 2. S5 is the Right Logic - -S5 epistemic logic (with equivalence relation accessibility) is the -standard for knowledge representation. The key axiom is T (veridicality): -`K_a(P) → P` — what is known is true. Belief (KD45) relaxes this, -allowing agents to hold false beliefs. This precisely models the -prover vs user distinction. - -==== 3. Type-Level Encoding - -Embedding the Kripke semantics at the type level means: +The distinction between knowledge-like and belief-like data remains a useful +design motivation. However, names and motivation are not evidence that the +current checker implements the complete S5 model, that its L10 result is +factive knowledge, or that a separate choreography system is required to +deploy VCL-UT. -- The type checker IS the model checker (no separate verification step) -- Proofs are erased at runtime (zero overhead) -- Epistemic properties compose with all other safety levels +The standalone model and the L10 structural predicate must be described at +their actual scopes. L10 source expressions are currently fail-closed in the +Rust parser, and the proposition carried by a programmatically constructed +L10 requirement is not yet schema-type-checked. See the parser/binder gap in +`ROADMAP.adoc` and the +link:../audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc[2026-11-01 audit]. === Consequences -- Queries can now distinguish verified knowledge from unverified belief -- Federation consensus properties are machine-checkable -- The EPISTEMIC clause syntax extends VCL-total without breaking existing queries -- The accessibility relation proofs add compile-time cost for L10 queries -- VCL-total becomes the first query language with formal epistemic types +- The standalone Kripke formalisation remains available as formal content; it + is not represented as the runtime/deployment L10 model without a proved + bridge. +- L10 is reported as a structural predicate over an existing `Statement`, + not as proof that agents actually know or believe a proposition. +- The VCL parser does not yet expose the L7–L10 extension fields as source + syntax; unsupported forms fail closed. +- K-CUT is not listed as a VCL-UT deployment blocker absent an explicit + artefact establishing that relationship. == Licence diff --git a/docs/audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc b/docs/audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc new file mode 100644 index 0000000..782768e --- /dev/null +++ b/docs/audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc @@ -0,0 +1,136 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += Audit: VCL-UT Levels and Choreographic K-CUT +:revdate: 2026-11-01 + +== Finding + +No exact local design document, issue, import, build/runtime dependency, or +machine-checked theorem makes choreographic K-CUT a VCL-UT deployment blocker. +Do not infer such a dependency from shared terms such as *epistemic*, +*choreographic*, *Kripke*, or from level names. + +This is a repository-scoped finding, not a claim that K-CUT can never be useful +or required by a particular deployment. A deployment-specific requirement +needs an explicit artefact (for example, a versioned interface contract, +consumer import, enforced build/deployment rule, or local theorem establishing +the dependency). + +== Evidence and limits + +* The repository has no `K-CUT`/`K-Cut`/`KCut` design reference, import, or + deployment rule. The local issue inventory contains no K-CUT issue. +* Issue + https://github.com/hyperpolymath/vcl-ut/issues/25[#25] is about the VCL + parser / verified-corpus boundary. It is not a K-CUT dependency. It is now + closed; its historical description that no parser existed is stale because + the Rust parser in `src/interface/parse` now exists. +* `verification/proofs/vclut-core.ipkg` includes + `VclTotal.Core.Epistemic`. `src/core/Epistemic.idr` contains a standalone + Kripke-style S5 formalisation (frames, accessibility properties, satisfaction + and epistemic operators). That is real local formal content, but the + deployment-facing L10 checker does not import or invoke this module. +* L10's local `Checker.checkLevel10` / `Decide.epistemicConsistentStmt` path + checks a populated `EpistemicClause` structurally (declared agents and + `ENTAILS`-cycle conditions). The L10 soundness theorem is about that + predicate over a `Statement`; it does not establish a bridge to the Kripke + model, choreographic K-CUT, or any deployment requirement. + +Therefore the Kripke module is not evidence of a K-CUT deployment dependency, +and no such blocker should be stated absent a new explicit artefact. + +== Actual L7–L10 source and binding gap + +Keep these two statements separate: + +. **Specified/proved:** the L0–L10 level constructors and proof predicates + exist over the Idris `Statement` representation. A certificate can be + constructed for an already-built statement satisfying the relevant + predicate. The L10 predicate is the structural condition described above; + it is not equivalent to invoking the standalone Kripke semantics. +. **Expressible from source:** the trusted Rust source parser currently reaches + at most L6 `CardinalitySafe`. Its AST mirrors the extension fields, but + `parse_statement` initializes `proof_clause`, `effect_decl`, + `version_const`, `linear_annot`, and `epistemic_clause` to `None`. + `infer_requested_level` awards L7–L10 only when the corresponding upper-level + fields are populated. The unsupported source clauses and modal expressions + fail closed. + +The missing work is source syntax plus elaboration/binding for those clauses: + +[cols="1,2,3"] +|=== +| Level | AST field / source feature | Current source-path gap + +| L7 `EffectTracked` +| `effect_decl` / `EFFECTS` +| Clause is rejected; no parse-to-AST elaboration or binding. + +| L8 `TemporalSafe` +| `version_const` / `AT VERSION` +| Clause is rejected; no parse-to-AST elaboration or binding. + +| L9 `LinearSafe` +| `linear_annot` / `CONSUME` or `USAGE` +| Clauses are rejected; no parse-to-AST elaboration or binding. + +| L10 `EpistemicSafe` +| `epistemic_clause`; `EPISTEMIC` and modal `KNOWS` / `BELIEVES` / `ANNOUNCE` / `COMMON` +| Clauses/expressions are rejected; no source elaboration binds the epistemic AST. Separately, proposition well-typedness against the schema remains a disclosed limitation. +|=== + +This is not a claim that all schema binding is absent: the existing decider +resolves ordinary field references against `OctadSchema`. The gap is that the +source parser does not construct/bind the L7–L10 extension data required by +the level inference and certifier. A wire-decoded or programmatically +constructed `Statement` can carry those fields, but that does not make them +expressible in VCL source. + +== Proof grade and verifier policy + +Apply the estate policies without conflating the proof lanes: + +* The Mathesis `estate-mathematical-architecture` defines **Grade 3** as a + locally type-checked Agda formulation that has not yet been translated to an + independent foundational system. It also requires exact proof-state and + receipt tracking; Mathesis is an index, not an endorsement of theorem status. +* The Standards `PROOF-POLICY.adoc` maps first-party Rust code to Creusot, + engineering/API/ABI properties to Idris2, and implementation-independent + theory to Agda with rechecks in Rocq and Lean. The policy requires theorem + statements, assumptions, revisions, tool versions, invocations, and observed + results to be recorded; a successful build alone does not establish + correspondence between differently stated theorems. +* VCL-UT's current L0–L10 safety corpus is Idris2 engineering evidence over its + AST. It is **not Mathesis Grade 3**, because it is not an Agda formulation. + Preserve the local Idris2 proof status in + `verification/proofs/VERIFICATION-STANCE.adoc`; do not replace it with an + invented Grade 3 label. Rust implementation obligations belong in the Rust + verification lane, not in an Agda grade by association. +* If Grade 3 is the target for a language-independent claim (for example, + soundness of a VCL predicate), first formulate the exact proposition and + assumptions in Agda, use the estate's canonical profile + `agda --safe --without-K --cubical-compatible `, pin Agda and + standard-library versions, and retain a reproducible CI receipt. Record it + as Grade 3 only after local checking. Translation and reconciliation in + Rocq/Lean are subsequent stages, not implied by the Idris2 corpus build. + This is new proof work; a prose reclassification does not achieve it. + +Normative references, inspected at these exact revisions: + +* [Mathesis estate mathematical architecture](https://github.com/hyperpolymath/mathesis/blob/50a012dba57fe90c9aca8d57241690c133ab117c/estate-mathematical-architecture) (`estate-mathematical-architecture`, blob `65c7f3f...`). +* [Standards proof and verification policy](https://github.com/metadatastician/standards/blob/46ee18323305d5b36e2eef936e47dd54c39ea736/3-practice/PROOF-POLICY.adoc) (policy blob `49abdbd...`). +* Local proof ledger: `verification/proofs/VERIFICATION-STANCE.adoc`. +* Staged Agda Grade 3 port plan (not proof evidence): + `verification/proofs/AGDA-GRADE3-PORT-PLAN.adoc`. + +== Source anchors + +* Canonical names/tags: `src/interface/parse/src/ast.rs` and + `src/interface/abi/Types.idr`. +* Fail-closed source grammar and `None` initialization: + `src/interface/parse/src/parser.rs` (`parse_statement`, + `infer_requested_level`). +* Checker predicates: `src/core/Decide.idr`, `src/core/Checker.idr`, + `src/core/Levels.idr`. +* Standalone Kripke formalisation: `src/core/Epistemic.idr`; proof package + membership: `verification/proofs/vclut-core.ipkg`. +* Parser-scope issue: GitHub #25, not a K-CUT issue. diff --git a/verification/proofs/AGDA-GRADE3-PORT-PLAN.adoc b/verification/proofs/AGDA-GRADE3-PORT-PLAN.adoc new file mode 100644 index 0000000..be63ffa --- /dev/null +++ b/verification/proofs/AGDA-GRADE3-PORT-PLAN.adoc @@ -0,0 +1,178 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 += VCL-UT L0–L10 Agda Grade 3 Port Plan +:revdate: 2026-11-01 +:status: proposed, not proof evidence + +== Purpose and status + +Plan to formulate the current language-independent L0–L10 predicate and +certificate claims in Agda, targeting Mathesis **Grade 3** theorem-by-theorem. +This document is a work plan only: it contains no Agda proof, no CI receipt, +and grants no Grade 3 status. No `.agda` proof source is present in this +checkout, and the Agda compiler is unavailable in the current environment. + +The current proof corpus is Idris2 engineering/formalisation evidence over the +repository's `Statement` AST. Under the Standards proof policy, repository +interfaces and engineering obligations stay in Idris2; first-party Rust code +belongs in the Creusot lane. Grade 3 is not a label for an Idris2 build: the +Mathesis architecture defines it as a locally type-checked Agda formulation +not yet translated to an independent foundational system. Do not replace or +downgrade existing Idris2 proof status by relabelling it. + +== Normative policy and source baseline + +* Mathesis estate mathematics architecture, exact reviewed source revision: + [mathesis `estate-mathematical-architecture`](https://github.com/hyperpolymath/mathesis/blob/50a012dba57fe90c9aca8d57241690c133ab117c/estate-mathematical-architecture). +* Estate verifier mapping and rechecking policy, exact reviewed source + revision: [Standards `PROOF-POLICY.adoc`](https://github.com/metadatastician/standards/blob/46ee18323305d5b36e2eef936e47dd54c39ea736/3-practice/PROOF-POLICY.adoc). +* Current theorem statements, premises, residues, and proof-corpus status: + `VERIFICATION-STANCE.adoc` (authoritative local ledger). +* Current definitions and implementations: `src/core/{Grammar,Schema,Decide, + Levels,Checker,Composition}.idr`. +* K-CUT relationship and L7–L10 source boundary: + `../../docs/audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc`. + +Standards' canonical Agda entrypoint is: + +[source,shell] +---- +agda --safe --without-K --cubical-compatible +---- + +Pin and record the Agda and standard-library versions. The requested +installation target includes full Cubical Agda, separate from the estate +default profile; Creusot is to use its repository-pinned nightly alongside +latest stable Rust for VCL-UT. Full Cubical use in theorem source still needs +a separately reviewed proof profile with a theorem-specific rationale, +exact flags, and pinned versions. The current L0–L10 AST predicates do not by +themselves demonstrate a need for Cubical semantics. Failed or unavailable +tools leave the obligation open; flags must not be weakened to make a check +pass. + +== Port inventory + +The Agda theorem must preserve the *current proved predicate*, not strengthen +a safety-level name into a stronger semantic guarantee. The initial scope is +the Idris checker-acceptance implication and the dependent level/certificate +structure. Every row needs a side-by-side statement and assumption review +before implementation. + +[cols="1,2,3,3",options="header"] +|=== +|Level |Current Idris predicate |Agda Grade 3 target |Explicit boundary / non-claim +|L0 `ParseSafe` |AST membership is true by construction (`MkL0`); not a parser theorem. |Represented `Statement` values inhabit the L0 witness; prove only the construction-level fact. |Does not prove Rust parser correctness, grammar unambiguity, or source-to-AST refinement. +|L1 `SchemaBound` |Every extracted field reference resolves in the supplied `OctadSchema`; `checkLevel1Sound` constructs `AllFieldsBound`. |Formalise schema, reference extraction, resolution, and acceptance implies all referenced fields are bound. |Does not authenticate runtime schema metadata or prove schema matches the deployed database. +|L2 `TypeCompat` |WHERE comparison operands satisfy the implemented schema-aware compatibility predicate; `checkLevel2Sound`. |Formalise the exact VQL type relation and prove checker acceptance implies the predicate. |Do not extend to HAVING, subquery scoping, or general language type safety unless separately specified and proved. +|L3 `NullSafe` |The implemented null-guard predicate holds over covered WHERE/HAVING structure; `checkLevel3Sound`. |Formalise the exact structural guard recogniser and its acceptance theorem. |Does not imply general branch-sensitive null-flow analysis or resolve documented subquery/scoping limits. +|L4 `InjectionProof` |WHERE has no embedded string literal under `whereHasStringLit`; `checkLevel4Sound` and `noRawUserInputCompose`. |Formalise the AST predicate, checker soundness, and existing join-closure claim. |Does not prove arbitrary execution is injection-free, source parser refinement, or runtime parameter binding. +|L5 `ResultTyped` |Every selected item resolves to the implemented non-`TAny` result type; `checkLevel5Sound`. |Formalise selected-item typing against `OctadSchema` and checker acceptance. |Does not establish runtime result representation or universal typing of clauses not covered by the predicate. +|L6 `CardinalitySafe` |A `LIMIT` value is present; `checkLevel6Sound`. |Formalise the exact presence predicate and acceptance theorem. |Does not prove a numeric bound on actual returned rows, engine compliance, or resource cost. +|L7 `EffectTracked` |`effectDecl` is present; `checkLevel7Sound`. |Formalise the exact AST field and presence predicate. |Presence is not effect correctness or proof execution stays within the declaration; no source syntax currently populates it. +|L8 `TemporalSafe` |`versionConst` is present; `checkLevel8Sound`. |Formalise the exact AST field and presence predicate. |Presence is not freshness, clock correctness, or snapshot fidelity; no source syntax currently populates it. +|L9 `LinearSafe` |`LinUseOnce` or `LinBounded`; `LinUnlimited` and absence fail; `checkLevel9Sound`. |Formalise the annotation datatype, enforcement predicate, and acceptance theorem. |Does not prove runtime resource use or affine behavior of an external handle; no source syntax currently populates it. +|L10 `EpistemicSafe` |A populated clause has a declared agent set, all referenced agents declared, and an acyclic `ENTAILS` graph; `checkLevel10Sound`. |Formalise that structural predicate, including transitive cycle detection, and the exact acceptance theorem. |Does not prove factivity, proposition typing, Kripke-model soundness, real-world truth, or a K-CUT/deployment dependency. Rust currently checks direct reciprocal cycles only. +|=== + +== Stages and gates + +=== Stage 0 — Freeze the statement inventory + +For each `checkLevelNSound`, level witness, certificate constructor, +`CanWeaken` rule, and composition-preservation lemma: + +. copy its exact type and referenced predicate from the current Idris source; +. list all explicit and implicit premises, schema inputs, and universe/type + assumptions; +. map every constructor and predicate to its Agda counterpart; +. mark unresolved or excluded behavior; and +. record the VCL-UT source commit and the source files reviewed. + +Acceptance: a reviewer can compare Idris and Agda propositions line-by-line. +No theorem is represented by a matching name alone. + +=== Stage 1 — Agda core model and L0–L1 + +Define the minimal statement/field/schema model needed for the first two +predicates. Keep the model independent of parser implementation details. +Prove the construction-level L0 fact and L1 field-resolution acceptance +implication. Pin the Agda toolchain/profile and run the real command in CI. + +Acceptance: the proof and its assumptions type-check under the normative +profile; no `postulate`, unsafe option, or unreviewed foreign axiom discharges +the target theorem. + +=== Stage 2 — L2–L5 typing, null, and injection predicates + +Port the exact current comparison compatibility, null-guard, no-string-literal, +and selected-result predicates. Add acceptance-implies-predicate theorems for +each level. Port join-closure only where the current Idris theorem states it; +write separate counterexamples or explicit limitations for unproved stronger +claims. + +Acceptance: positive and negative fixtures exercise each exact predicate, and +the Agda proposition is reviewed against the Idris source—not merely against +the level label. + +=== Stage 3 — L6–L10 upper-level predicates + +Port cardinality/effect/version presence, the enforced linear annotation, and +the structural epistemic predicate. For L10, prove finite transitive cycle +closure correctness and acceptance implies the specified structural +acyclicity. Keep proposition typing and Kripke semantics out of scope unless +separately formulated as additional theorems with explicit premises. + +Acceptance: each predicate's intentional weakness is recorded; unsupported +source syntax remains a parser obligation and cannot be claimed as covered by +the Agda AST proof. + +=== Stage 4 — Certificates, ordering, and composition + +Port the dependent `SafetyCertificate` cases, `certifyAt` / `certifyRequested` +behavior, `CanWeaken` rules, and `compositionPreservation` obligations. Preserve +L10's non-join-closed cycle condition as an explicit side-condition; do not +weaken it to obtain a spurious unconditional composition result. + +Acceptance: every certificate constructor is tied to its level predicate and +lower-level premises; every composition hypothesis appears in the Agda theorem +type. State separately what is not closed under composition. + +=== Stage 5 — Grade 3 receipt and subsequent verification + +For each theorem—not just for the package—retain: proposition, assumptions, +Agda source hash, VCL-UT source revision, Agda and library versions, exact +invocation, CI job/run URL, result, and reviewer comparison notes. Record a +Mathesis Grade 3 status only for the theorem with a successful local Agda +receipt and no missing assumption disclosure. Partial work remains theorem- +scoped; no umbrella Grade 3 claim for L0–L10 is allowed until every in-scope +row passes. + +Grade 3 is the initial target, not the end of the Standards policy. Reconcile +theory statements with Rocq and Lean according to `PROOF-POLICY.adoc`; record +whether each leg was transported or re-proved and how proposition correspondence +was checked. Never infer cross-prover identity from filenames or theorem names. + +== Separate engineering obligations + +This Agda plan does not discharge these distinct obligations: + +* Rust parser/decider implementation correctness: Rust verification lane + (Creusot under the Standards policy), plus tests and explicit conformance + evidence. +* Rust–Idris/Agda wire and predicate correspondence: exact schema/AST mapping, + golden-vector evidence, and explicit refinement or conformance proofs. +* Parser source reachability: implement and bind L7–L10 syntax before claiming + those levels are expressible from VCL source. +* Runtime schema, identity, evidence authenticity, clocks, resource behavior, + database commits, and deployment integration: external assumptions and + consumer-side evidence; not proved by AST theorems. +* Choreographic K-CUT dependency: no claim until a concrete interface, + deployment rule, import, or theorem makes the dependency explicit. + +== Current decision + +**No Grade 3 claim is assigned by this plan.** The L0–L10 proof corpus remains +reported Idris2 evidence under `VERIFICATION-STANCE.adoc`; Rust source claims +remain in their implementation lane. The plan establishes how to begin an +Agda Grade 3 formulation and prevents that future work from being confused +with source expressibility, implementation correctness, or deployment +requirements. diff --git a/verification/proofs/README.adoc b/verification/proofs/README.adoc index 2443866..854b405 100644 --- a/verification/proofs/README.adoc +++ b/verification/proofs/README.adoc @@ -52,6 +52,11 @@ This directory holds the *machine-verified* proof artefacts for vcl-ut. Rust parser+codec, certified Idris wire decoder) and the precisely-scoped residual OWED items. +`AGDA-GRADE3-PORT-PLAN.adoc`:: + Proposed, staged plan for formulating exact language-independent L0–L10 + theorem claims in Agda toward Mathesis Grade 3. It is a plan only, not a + proof receipt or a change to the current Idris2 engineering-proof status. + == Verifying [source,sh] From 7c77eb2cc7b2ee35ad2d1ccb4c26c5a897c861c8 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 1 Nov 2026 17:53:38 +0000 Subject: [PATCH 2/7] Address review feedback on level claims Signed-off-by: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- docs/THE-10-LEVELS-EXPLAINED.adoc | 54 ++++++++++++------- docs/architecture/ARCHITECTURE.adoc | 23 +++++--- .../K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc | 12 +++-- 3 files changed, 58 insertions(+), 31 deletions(-) diff --git a/docs/THE-10-LEVELS-EXPLAINED.adoc b/docs/THE-10-LEVELS-EXPLAINED.adoc index c7645d4..71d4509 100644 --- a/docs/THE-10-LEVELS-EXPLAINED.adoc +++ b/docs/THE-10-LEVELS-EXPLAINED.adoc @@ -65,14 +65,13 @@ in various real-world systems (though rarely all six together). They address real failure modes that levels 0-5 leave uncovered. These levels use TypeQL-Experimental extension mechanisms. -**Level 10, Epistemic Safety, is different in kind from all the others.** -Levels 0-9 ask whether a statement is *well-formed* — whether it will do what -it says without crashing, leaking or corrupting. Level 10 asks whether the -engine is entitled to *believe* the result: whether the modalities consulted -agree, whether the authority answering is competent for the question, and -whether a disagreement between witnesses has been resolved rather than -silently averaged. That is not a query-safety property. It is a consonance -property, and it is the reason this ladder has eleven rungs and not ten. +**Level 10, `EpistemicSafe`, is a separate structural predicate over a +`Statement`.** The current predicate requires a populated epistemic clause, +declared agents, references only to declared agents, and an acyclic `ENTAILS` +graph. It does not establish whether the engine is entitled to believe or give +an answer, whether modalities agree, or whether an authority is competent. That +scope is distinct from the structural and operational checks at Levels 0-9; it +is the reason this ladder has eleven rungs and not ten. == The Progression at a Glance @@ -427,6 +426,12 @@ processes only the first of many results, silently ignoring the rest. == Level 7: Effect-Tracking Safety +[NOTE] +==== +The `EFFECTS` forms shown in this section are illustrative design syntax and +are not accepted by the current VCL-UT source parser. +==== + === What It Checks Every query is classified by its effects: @@ -492,6 +497,12 @@ triggers a write. An analytics query modifies production data. == Level 8: Temporal Safety +[NOTE] +==== +The `AS OF` forms shown in this section are illustrative design syntax and are +not accepted by the current VCL-UT source parser. +==== + === What It Checks Queries that involve time carry their temporal bounds in the type system. @@ -563,6 +574,12 @@ list instead of the current one. == Level 9: Linearity Safety +[NOTE] +==== +The `CONSUME` and `USAGE` forms shown in this section are illustrative design +syntax and are not accepted by the current VCL-UT source parser. +==== + === What It Checks Resources that must be used exactly once -- database connections, transaction @@ -810,21 +827,18 @@ link:audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc[audit]. | Connection leaks, use-after-close, double-commit | 10 -- Epistemic -| Unwarranted answers: disagreeing modal witnesses silently reconciled, - circular warrant, an authority answering outside its competence +| A populated epistemic clause with declared agents and no `ENTAILS` cycles |=== Levels 0-9 cover the vast majority of database bugs that have caused real-world catastrophes, and the goal is to eliminate them at compile time with zero runtime overhead. -Level 10 is doing something else, and it is worth being precise about the -difference. Levels 0-9 are *safety* properties in the ordinary sense: they -rule out executions that go wrong. Level 10 is a *warrant* property: it rules -out answers the engine is not entitled to give, even though every step that -produced them was well-typed. A query engine over a passive store has no need -of such a level, because a passive store has exactly one witness and it cannot -disagree with itself. A consonance engine over eight modal witnesses does. - -That is why the ladder has eleven rungs, and why the eleventh is not simply -"one more safety level". +Level 10 is a separate *structural* predicate over an already-constructed +`Statement`. It requires a populated epistemic clause, at least one declared +agent, references only to declared agents, and an acyclic `ENTAILS` graph. It +does not establish whether the engine is entitled to believe or give an answer; +in particular, it does not prove modal witnesses agree or an authority is +competent. The Idris predicate is proved over the AST, while the Rust mirror +currently checks direct reciprocal entailment pairs only. The ladder therefore +has eleven distinct predicates, not a theorem of epistemic warrant. diff --git a/docs/architecture/ARCHITECTURE.adoc b/docs/architecture/ARCHITECTURE.adoc index 49b3855..30eca05 100644 --- a/docs/architecture/ARCHITECTURE.adoc +++ b/docs/architecture/ARCHITECTURE.adoc @@ -31,14 +31,20 @@ for level names, proof scope, and source expressibility. [source] ---- -VCL source -> Rust lexer/parser -> AST -> Rust decider / Idris proof corpus - -> gate verdict (not a transported proof) +Runtime gate: + VCL source -> Rust lexer/parser -> AST -> Rust `certified_level` -> verdict + +Offline verification: + Idris proof corpus checks corresponding predicates over the mirrored AST ---- The source parser is syntax-only and fail-closed on unsupported L7–L10 -clauses. Schema resolution happens in the decider for ordinary field refs. -The VeriSimDB consumer-side gate integration is a separate outstanding item; -this repository does not currently establish a full parse-to-execution path. +clauses. Schema resolution happens in the Rust decider for ordinary field +references. The runtime `vclt-gate` calls the Rust `certified_level` decider; +it does not invoke or link the Idris proof corpus. Idris checks the corresponding +predicate and certificate claims offline over the mirrored AST. The VeriSimDB +consumer-side gate integration is a separate outstanding item; this repository +does not currently establish a full parse-to-execution path. == The 11 Safety Levels @@ -180,8 +186,11 @@ VCL source text -> Rust lexer/parser (`src/interface/parse`) -> syntax AST (`Statement` / `VclOp`) -> versioned wire representation / gate request - -> safety decider and Idris proof corpus - -> verdict / certificate status + -> Rust `certified_level` decider + -> runtime gate verdict + +Separately, the Idris proof corpus checks corresponding predicates over the +mirrored AST offline; it does not feed the runtime gate verdict. ---- The parser establishes syntax, not schema-bound types or a full certificate. diff --git a/docs/audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc b/docs/audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc index 782768e..c66b220 100644 --- a/docs/audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc +++ b/docs/audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc @@ -4,8 +4,10 @@ == Finding -No exact local design document, issue, import, build/runtime dependency, or -machine-checked theorem makes choreographic K-CUT a VCL-UT deployment blocker. +No pre-existing or independently enforced artefact establishes choreographic +K-CUT as a VCL-UT deployment dependency. This audit names K-CUT only to record +that repository-scoped finding; it is not itself a design reference, import, +build/runtime dependency, or machine-checked theorem establishing a blocker. Do not infer such a dependency from shared terms such as *epistemic*, *choreographic*, *Kripke*, or from level names. @@ -17,8 +19,10 @@ the dependency). == Evidence and limits -* The repository has no `K-CUT`/`K-Cut`/`KCut` design reference, import, or - deployment rule. The local issue inventory contains no K-CUT issue. +* Apart from this audit, the repository has no pre-existing + `K-CUT`/`K-Cut`/`KCut` design reference, import, or deployment rule. This + audit is descriptive, not an independently enforced dependency. The local + issue inventory contains no K-CUT issue. * Issue https://github.com/hyperpolymath/vcl-ut/issues/25[#25] is about the VCL parser / verified-corpus boundary. It is not a K-CUT dependency. It is now From d3e51915f8754d7b509d9ac5bb0d6877440dd4c1 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 1 Nov 2026 18:08:45 +0000 Subject: [PATCH 3/7] Clarify AST predicates and dependency claims Signed-off-by: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- README.adoc | 22 +-- ROADMAP.adoc | 24 ++- docs/THE-10-LEVELS-EXPLAINED.adoc | 154 ++++++++++-------- docs/architecture/ARCHITECTURE.adoc | 11 +- .../K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc | 9 +- 5 files changed, 121 insertions(+), 99 deletions(-) diff --git a/README.adoc b/README.adoc index b1dde74..e0f94a6 100644 --- a/README.adoc +++ b/README.adoc @@ -207,20 +207,14 @@ 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**. - -[source] ----- -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) ----- +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 diff --git a/ROADMAP.adoc b/ROADMAP.adoc index b8beefe..fe8e333 100644 --- a/ROADMAP.adoc +++ b/ROADMAP.adoc @@ -146,13 +146,23 @@ These are ordered by value, not by version number. == Dependencies -* **TypeLL** type theory must stabilise for L6-L9. Note that L10 does *not* - depend on TypeLL: `EpistemicSafe` originates here, in the shift from - querying a store to addressing a consonance engine. -* **VeriSimDB** statement router must support VCL-UT as a third path alongside - Slipstream (VCL) and VCL-DT. -* **ReScript evangeliser** must prove concept first — VCL-UT and AffineScript - are the two showcase languages that follow. +The TypeLL item below is a historical planning assumption, not an established +build or deployment dependency. The current repository does not contain a +versioned interface, import, theorem, or enforced rule establishing a TypeLL +mapping for VCL-UT L6-L9. VCL-UT's local predicates and certificates are +specified in its Rust and Idris sources; revise this planning assumption only +if an explicit integration artefact establishes the relationship. + +* **TypeLL (unverified planning assumption):** Earlier roadmap text listed + TypeLL stabilization as a prerequisite for L6-L9. That prerequisite is not + established by the current local implementation. L10 is also defined here as + a VCL-UT predicate; this is not a claim that it has a cross-project mapping. +* **VeriSimDB:** The statement router is planned to support VCL-UT as a third + path alongside Slipstream (VCL) and VCL-DT; consumer integration remains + outstanding. +* **ReScript evangeliser:** A proof of concept is listed as a planning + prerequisite for the proposed VCL-UT and AffineScript showcase languages; + this is not a VCL-UT build dependency. == Future Directions diff --git a/docs/THE-10-LEVELS-EXPLAINED.adoc b/docs/THE-10-LEVELS-EXPLAINED.adoc index 71d4509..eb95511 100644 --- a/docs/THE-10-LEVELS-EXPLAINED.adoc +++ b/docs/THE-10-LEVELS-EXPLAINED.adoc @@ -61,17 +61,19 @@ floor without the second, and you cannot build the second without the first. **Levels 0-5** are well-established in the academic literature and implemented in various real-world systems (though rarely all six together). -**Levels 6-9** are additional protections identified through our research. -They address real failure modes that levels 0-5 leave uncovered. These levels -use TypeQL-Experimental extension mechanisms. +**Levels 6-9** name additional safety dimensions. The examples in the L7-L9 +sections are design sketches, not accepted VCL-UT source syntax. The current +AST predicates have narrower scopes, stated at the start of each section and +in the progression summary below. **Level 10, `EpistemicSafe`, is a separate structural predicate over a `Statement`.** The current predicate requires a populated epistemic clause, declared agents, references only to declared agents, and an acyclic `ENTAILS` graph. It does not establish whether the engine is entitled to believe or give an answer, whether modalities agree, or whether an authority is competent. That -scope is distinct from the structural and operational checks at Levels 0-9; it -is the reason this ladder has eleven rungs and not ten. +scope is distinct from the AST predicates at Levels 0-9, including the +presence/annotation checks at L7-L9; it is the reason this ladder has eleven +rungs and not ten. == The Progression at a Glance @@ -115,19 +117,19 @@ is the reason this ladder has eleven rungs and not ten. | Code assumes one row, gets zero or thousands | 7 -- Effects -| Does this query read, write, or modify structure? -| Compile time -| Read-only functions accidentally delete data +| Does a constructed statement contain an effect declaration? +| AST predicate; not operation enforcement +| A missing effect declaration fails L7 | 8 -- Temporal -| Is the data fresh enough for the intended use? -| Compile time (bounds in types) -| Stale data treated as current +| Does a constructed statement contain a version constraint? +| AST predicate; not freshness validation +| A missing version constraint fails L8 | 9 -- Linearity -| Are resources used exactly once? -| Compile time (via QTT) -| Connection leaks, use-after-close +| Does a constructed statement contain a supported bounded-use annotation? +| AST predicate; not runtime resource tracking +| A missing or unsupported annotation fails L9 |=== == Level 0: Parse-Time Safety @@ -429,27 +431,30 @@ processes only the first of many results, silently ignoring the rest. [NOTE] ==== The `EFFECTS` forms shown in this section are illustrative design syntax and -are not accepted by the current VCL-UT source parser. +are not accepted by the current VCL-UT source parser. The current L7 AST +predicate checks only that an effect declaration is present; it does not +compare operations with the declared effects or enforce read-only behavior. ==== === What It Checks -Every query is classified by its effects: +The intended effect system classifies queries by their effects: - **Read** -- retrieves data without modification - **Write** -- inserts, updates, or deletes data - **DDL** -- modifies schema structure (create table, alter column) -A function that only has `Read` permission _cannot_ perform writes. This is -enforced at compile time, not by convention. +A complete effect checker could reject writes in a read-only context. The +current L7 predicate does not provide that enforcement. === When It Checks -At **compile time**, using an effect system encoded in Idris2. +The L7 predicate checks the `effect_decl` field on an already-constructed +`Statement`; it is not a compile-time source check in the current parser. -=== How VCL-total Implements It +=== VCL-total Design Sketch -This level uses the **effect system** extension from TypeQL-Experimental: +The syntax table below sketches a proposed effect-system extension: [cols="1,2"] |=== @@ -476,9 +481,9 @@ RETRACT users WHERE users.expired = true EFFECTS { Read, Write } -- OK: Write effect is available. ---- -=== TypeQL-Experimental Encoding +=== Illustrative TypeQL-Experimental Encoding -Effects are tracked using an effect set with subsumption proofs in Idris2: +A full effect checker could track an effect set with subsumption proofs in Idris2: ---- data Effect = Read | Write | DDL @@ -490,8 +495,10 @@ data Effect = Read | Write | DDL === What You Lose Without It -A "reporting" function accidentally executes a DELETE. A monitoring dashboard -triggers a write. An analytics query modifies production data. +Without effect enforcement in a complete implementation, a "reporting" +function could accidentally execute a DELETE, a monitoring dashboard could +trigger a write, or an analytics query could modify production data. The +current L7 predicate alone does not prevent these outcomes. --- @@ -499,28 +506,33 @@ triggers a write. An analytics query modifies production data. [NOTE] ==== -The `AS OF` forms shown in this section are illustrative design syntax and are -not accepted by the current VCL-UT source parser. +The temporal forms shown in this section, including `AS OF`, are illustrative +design syntax and are not accepted by the current VCL-UT source parser. The +current L8 AST predicate +checks only that a version constraint is present; it does not establish +freshness or validate temporal bounds. ==== === What It Checks -Queries that involve time carry their temporal bounds in the type system. -The compiler ensures: +A complete temporal type system could carry bounds and validate: -- Historical queries actually get historical data -- Freshness guarantees are met (data is not staler than claimed) -- Bi-temporal queries correctly distinguish between "when it happened" (valid +- Whether historical queries actually get historical data +- Whether freshness guarantees are met (data is not staler than claimed) +- Whether bi-temporal queries distinguish between "when it happened" (valid time) and "when we recorded it" (transaction time) +The current L8 predicate checks the `version_const` field only; it does not +perform those temporal validations. + === When It Checks -At **compile time**, using temporal type annotations. +The L8 predicate checks `version_const` on an already-constructed `Statement`; +it is not a compile-time temporal analysis in the current source parser. -=== How VCL-total Implements It +=== VCL-total Design Sketch -This level uses the **modal type** and **session type** extensions from -TypeQL-Experimental: +The syntax table below sketches proposed modal-type and session-type extensions: [cols="1,2"] |=== @@ -554,9 +566,9 @@ SELECT orders.status -- Every result carries a timestamp within the specified range. ---- -=== TypeQL-Experimental Encoding +=== Illustrative TypeQL-Experimental Encoding -Temporal safety uses box types indexed by world/scope: +A complete temporal checker could use box types indexed by world/scope: ---- -- Modal type: data tagged with its temporal context @@ -566,9 +578,10 @@ data Temporal : Type -> TemporalBound -> Type where === What You Lose Without It -Code treats yesterday's cached data as if it were live. Financial decisions -are made on stale price data. Medical records show a patient's old medication -list instead of the current one. +Without temporal validation in a complete implementation, code could treat +yesterday's cached data as live, financial decisions could use stale prices, +and medical records could show an old medication list. The current L8 +predicate alone does not rule out these cases. --- @@ -576,30 +589,28 @@ list instead of the current one. [NOTE] ==== -The `CONSUME` and `USAGE` forms shown in this section are illustrative design -syntax and are not accepted by the current VCL-UT source parser. +The `CONSUME`, `USAGE`, and `WITH SESSION` forms shown in this section are +illustrative design syntax and are not accepted by the current VCL-UT source +parser. The current L9 AST predicate accepts a `LinUseOnce` or `LinBounded` +annotation; it does not +inspect or prove actual runtime resource consumption or session behavior. ==== === What It Checks -Resources that must be used exactly once -- database connections, transaction -handles, cursor positions -- are tracked by the type system. You cannot: - -- **Forget** to close a connection (it would be unused -- the compiler rejects it) -- **Use** a connection after closing it (it has been consumed -- the compiler - rejects it) -- **Share** a transaction handle between two threads (it is linear -- only one - owner at a time) +A complete linear-use checker could track resources such as database +connections, transaction handles, and cursor positions, preventing forgotten, +reused, or improperly shared resources. The current L9 predicate only +recognizes the bounded-use annotation on a constructed `Statement`. === When It Checks -At **compile time**, using Quantitative Type Theory (QTT) -- the same -theoretical foundation that powers Idris2's resource tracking. +The L9 predicate checks `linear_annot` on an already-constructed `Statement`; +it does not track resource use at runtime or in the current source parser. -=== How VCL-total Implements It +=== VCL-total Design Sketch -This level uses the **linear type** and **QTT** extensions from -TypeQL-Experimental: +The syntax table below sketches proposed linear-type and QTT extensions: [cols="1,2"] |=== @@ -630,9 +641,9 @@ COMMIT txn -- It cannot be used again. It cannot be forgotten (unused linear resource). ---- -=== TypeQL-Experimental Encoding +=== Illustrative Idris2/QTT Encoding -Linearity is encoded using Idris2's native QTT support: +A complete linear-use checker could encode the resource constraints using Idris2's native QTT support: ---- -- Connection with quantity 1 (must be used exactly once) @@ -644,9 +655,9 @@ close : (1 _ : Connection) -> IO () -- If you close twice, the compiler rejects your code. ---- -=== Session Types for Protocol Safety +=== Illustrative Session Types for Protocol Safety -Session types enforce a communication protocol between client and database: +In a complete implementation, session types could enforce a communication protocol between client and database: ---- data SessionState = Ready | InTransaction | Closed @@ -667,9 +678,10 @@ close : Session Ready -> Session Closed === What You Lose Without It -Connection leaks exhaust the connection pool. Use-after-close corrupts data. -Double-commits create duplicate transactions. Forgotten rollbacks leave locks -held indefinitely. +Without linear-use enforcement in a complete implementation, connection leaks +could exhaust the pool, use-after-close could corrupt data, double-commits could +create duplicate transactions, and forgotten rollbacks could leave locks held. +The current L9 predicate alone does not prevent these outcomes. --- @@ -818,21 +830,25 @@ link:audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc[audit]. | Wrong assumptions about how many results a query returns | 7 -- Effects -| Accidental data modification by read-only code +| Missing effect declaration; this predicate does not block writes | 8 -- Temporal -| Stale data treated as current, mixed time contexts +| Missing version constraint; this predicate does not validate freshness | 9 -- Linearity -| Connection leaks, use-after-close, double-commit +| Missing supported bounded-use annotation; this predicate does not track runtime use | 10 -- Epistemic | A populated epistemic clause with declared agents and no `ENTAILS` cycles |=== -Levels 0-9 cover the vast majority of database bugs that have caused -real-world catastrophes, and the goal is to eliminate them at compile time -with zero runtime overhead. +The level names describe distinct safety dimensions, but they do not by +themselves establish that each dimension is enforced by the source parser or at +runtime. In particular, the current L7-L9 predicates inspect fields on an +already-constructed `Statement`: effect-declaration presence, version-constraint +presence, and a supported bounded-use annotation, respectively. They do not +implement the operational effect, freshness, or resource-use guarantees sketched +in those sections. Level 10 is a separate *structural* predicate over an already-constructed `Statement`. It requires a populated epistemic clause, at least one declared diff --git a/docs/architecture/ARCHITECTURE.adoc b/docs/architecture/ARCHITECTURE.adoc index 30eca05..9282beb 100644 --- a/docs/architecture/ARCHITECTURE.adoc +++ b/docs/architecture/ARCHITECTURE.adoc @@ -182,15 +182,16 @@ diagram that previously appeared here: [source] ---- -VCL source text - -> Rust lexer/parser (`src/interface/parse`) - -> syntax AST (`Statement` / `VclOp`) - -> versioned wire representation / gate request +Runtime gate request (VCL source text) + -> Rust `parse_op` (`src/interface/parse`) + -> `Statement` AST -> Rust `certified_level` decider -> runtime gate verdict Separately, the Idris proof corpus checks corresponding predicates over the -mirrored AST offline; it does not feed the runtime gate verdict. +mirrored AST offline; it does not feed the runtime gate verdict. The versioned +wire codec is a separate interface and is not an intermediate step in this +`vclt-gate` runtime path. ---- The parser establishes syntax, not schema-bound types or a full certificate. diff --git a/docs/audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc b/docs/audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc index c66b220..05fdcc2 100644 --- a/docs/audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc +++ b/docs/audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc @@ -47,10 +47,11 @@ and no such blocker should be stated absent a new explicit artefact. Keep these two statements separate: . **Specified/proved:** the L0–L10 level constructors and proof predicates - exist over the Idris `Statement` representation. A certificate can be - constructed for an already-built statement satisfying the relevant - predicate. The L10 predicate is the structural condition described above; - it is not equivalent to invoking the standalone Kripke semantics. + exist over the Idris `Statement` representation. A cumulative certificate + at level N requires every predicate through N to hold; satisfying only the + named upper-level predicate is not sufficient. The L10 predicate is the + structural condition described above; it is not equivalent to invoking the + standalone Kripke semantics. . **Expressible from source:** the trusted Rust source parser currently reaches at most L6 `CardinalitySafe`. Its AST mirrors the extension fields, but `parse_statement` initializes `proof_clause`, `effect_decl`, From 5ad2372f45f50ae2ca85546034de75c4c08a6a37 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 1 Nov 2026 18:27:41 +0000 Subject: [PATCH 4/7] Align level documentation with implemented predicates Signed-off-by: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- README.adoc | 196 +++++++----------- ROADMAP.adoc | 21 +- docs/THE-10-LEVELS-EXPLAINED.adoc | 108 ++++++---- docs/architecture/ARCHITECTURE.adoc | 36 ++-- .../K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc | 10 +- 5 files changed, 174 insertions(+), 197 deletions(-) diff --git a/README.adoc b/README.adoc index e0f94a6..1b164b8 100644 --- a/README.adoc +++ b/README.adoc @@ -20,9 +20,9 @@ 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 checks an AST annotation (`UseOnce` or -`Bounded`); that annotation is not yet expressible from source and is not a -runtime resource-use proof. "-total" survives in the crate name `vcl-total` +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. @@ -111,7 +111,9 @@ an actively maintained identity-consonance system. 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: +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] ---- @@ -161,19 +163,14 @@ contract]. [source] ---- -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) +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 @@ -239,134 +236,83 @@ 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]. -=== Adoption Strategy +== Canonical Safety Levels (L0-L10) -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 +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"] |=== -| 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. +| 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` | Implemented raw-string-literal predicate holds +| 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 |=== -=== TypeQL-Experimental Extension Mechanisms (Levels 7-10) - -The https://github.com/hyperpolymath/nextgen-databases[typeql-experimental] -sub-project within nextgen-databases prototyped 6 mechanisms that map to -levels 7-10: - -[cols="1,2,2"] -|=== -| 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 -|=== +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. -== Architecture +== Current Architecture [source] ---- - +---------------+ - | 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 - +-----------------------+ +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. ---- -== Technology Stack +The versioned wire codec is a separate interface, not an intermediate step in +the `vclt-gate` request path. VeriSimDB consumer integration remains outstanding. -[cols="1,1,2"] -|=== -| Layer | Language | Purpose +== Technology Stack -| 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. +[cols="1,2"] |=== +| Component | Current role -== Roadmap +| Rust (`src/interface/parse`) +| Source parser, AST/wire codec, independent decider, and `vclt-gate` producer. -=== 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 +| Idris2 (`src/core`, `verification/proofs`) +| Predicates, soundness proofs, and cumulative dependent certificates over the AST. -[cols="1,2"] +| VeriSimDB consumer +| Planned integration target; it does not yet invoke the gate producer. |=== -| Project | Relationship - -| https://github.com/hyperpolymath/verisimdb[verisimdb] -| Target consonance engine (8-modal octad storage) -| verisimdb/docs/VCL-SPEC.adoc -| Base VCL grammar specification (EBNF appendix) +== Roadmap -| nextgen-databases/typeql-experimental -| 6 extension mechanisms for levels 7-10 (Idris2 kernel + ReScript parser) +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. -| https://github.com/hyperpolymath/typell[typell] -| Core type theory — the 10 levels originate here +== Related Projects -| https://github.com/hyperpolymath/panll[panll] -| Panel framework applying the same 10 levels to UI type safety -|=== +* 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. diff --git a/ROADMAP.adoc b/ROADMAP.adoc index fe8e333..20c632d 100644 --- a/ROADMAP.adoc +++ b/ROADMAP.adoc @@ -88,9 +88,11 @@ These are ordered by value, not by version number. . *Close the remaining L10 boundary gaps.* Proposition well-typedness of requirement expressions against the schema remains owed. Also align the Rust decider's direct reciprocal-cycle check with the Idris predicate's - transitive-cycle check before relying on non-source (wire/programmatic) L10 - statements. The Idris transitive-cycle proof is already implemented; do not - track it as outstanding. + transitive-cycle detection before relying on non-source (wire/programmatic) + L10 statements. Idris implements a finite-fuel transitive-closure check, but + the corpus does not prove that this helper is equivalent to a formal + graph-reachability/acyclicity definition; that correctness theorem remains + outstanding, as does Rust/Idris alignment. . *Optional syntax cleanup: retire the legacy `HEXAD` spelling* when all supported frontends can do so compatibly. The current Rust parser accepts both `OCTAD` and `HEXAD` as the same `Source::Octad`; this is a source-name @@ -118,10 +120,12 @@ These are ordered by value, not by version number. * [x] Property-based tests (`tests/property_test.rs`, `tests/fuzz_test.rs`) === v0.3.0 — Research Levels (L6-L9) -* [x] Cardinality annotations and inference (reachable: `LIMIT` ⇒ L6) -* [ ] Effect system (Read/Write/DDL) — proved; *no surface syntax* -* [ ] Temporal type annotations — proved; *no surface syntax* -* [ ] Linear types via Idris2 QTT — proved; *no surface syntax* +* [x] `CardinalitySafe` LIMIT-presence predicate (source reachable; no exact + result-count inference) +* [ ] Effect-declaration predicate (AST only; no surface syntax or operation + enforcement) +* [ ] Version-constraint presence predicate and proof over AST — no surface syntax or freshness validation +* [ ] L9 bounded-use annotation predicate and proof — no surface syntax or runtime resource enforcement * [ ] Integrate TypeQL-Experimental mechanisms === v0.4.0 — Consonance Level (L10) @@ -129,7 +133,8 @@ These are ordered by value, not by version number. * [x] S2 transitions MERGE / SPLIT / NORMALISE, with NORMALISE fail-closed without an explicit justification * [ ] Surface syntax for epistemic clauses -* [x] Transitive `ENTAILS`-cycle detection in the Idris proof predicate +* [x] Finite-fuel transitive `ENTAILS`-cycle detection implemented in the Idris predicate +* [ ] Prove the detector equivalent to a formal graph-reachability/acyclicity definition * [ ] Proposition well-typedness against the schema * [ ] Align the Rust L10 cycle check with the Idris transitive predicate diff --git a/docs/THE-10-LEVELS-EXPLAINED.adoc b/docs/THE-10-LEVELS-EXPLAINED.adoc index eb95511..95513ed 100644 --- a/docs/THE-10-LEVELS-EXPLAINED.adoc +++ b/docs/THE-10-LEVELS-EXPLAINED.adoc @@ -61,15 +61,16 @@ floor without the second, and you cannot build the second without the first. **Levels 0-5** are well-established in the academic literature and implemented in various real-world systems (though rarely all six together). -**Levels 6-9** name additional safety dimensions. The examples in the L7-L9 -sections are design sketches, not accepted VCL-UT source syntax. The current -AST predicates have narrower scopes, stated at the start of each section and -in the progression summary below. +**Levels 6-9** name additional safety dimensions. The L6 `SELECT UNIQUE` and +`SELECT OPTIONAL` examples and the L7-L9 forms are design sketches, not +accepted VCL-UT source syntax (the parser does accept `LIMIT`). The current AST +predicates have narrower scopes, stated at the start of those sections and in +the progression summary below. **Level 10, `EpistemicSafe`, is a separate structural predicate over a `Statement`.** The current predicate requires a populated epistemic clause, -declared agents, references only to declared agents, and an acyclic `ENTAILS` -graph. It does not establish whether the engine is entitled to believe or give +declared agents, references only to declared agents, and no cycle detected by +the implemented `ENTAILS` check. It does not establish whether the engine is entitled to believe or give an answer, whether modalities agree, or whether an authority is competent. That scope is distinct from the AST predicates at Levels 0-9, including the presence/annotation checks at L7-L9; it is the reason this ladder has eleven @@ -112,9 +113,9 @@ rungs and not ten. | Runtime crashes on unexpected data shapes | 6 -- Cardinality -| How many results will the query return? -| Compile time -| Code assumes one row, gets zero or thousands +| Does a constructed statement contain a `LIMIT`? +| AST predicate; not exact cardinality inference +| A missing `LIMIT` fails L6 | 7 -- Effects | Does a constructed statement contain an effect declaration? @@ -364,23 +365,30 @@ when the code is compiled. == Level 6: Cardinality Safety -=== What It Checks +[NOTE] +==== +The current L6 AST predicate checks only that a `LIMIT` is present. It does +not infer `ExactlyOne`, `AtMostOne`, or any other exact result cardinality from +a schema or query. The parser accepts `LIMIT`; the `SELECT UNIQUE` and +`SELECT OPTIONAL` forms in the design sketch below are not established parser +features. +==== -The number of results a query returns is part of the return type: +=== What It Checks -- `ExactlyOne` -- guaranteed to return exactly one result -- `AtMostOne` -- returns zero or one result -- `NonEmpty` -- returns at least one result -- `List` -- returns zero or more results +The current predicate checks for a `limit` value on an already-constructed +`Statement`. A present limit bounds a query syntactically; it does not prove +how many rows the query will return. === When It Checks -At **compile time**, using schema constraints (unique keys, NOT NULL) and query -structure (LIMIT, DISTINCT, aggregation). +The L6 predicate checks the AST field; it does not perform compile-time +cardinality inference from schema constraints or query semantics. -=== How VCL-total Implements It +=== VCL-total Design Sketch -This level uses the **TypeQL-Experimental** extension mechanisms: +The table below sketches stronger result-cardinality types beyond the current +L6 predicate: [cols="1,2"] |=== @@ -409,9 +417,9 @@ SELECT OPTIONAL users WHERE users.email = ?email -- The caller MUST pattern-match on Some/None. ---- -=== TypeQL-Experimental Encoding +=== Illustrative Cardinality Encoding -Cardinality is encoded in Idris2 using dependent types: +A full cardinality analysis could encode result bounds using dependent types: ---- data Cardinality = ExactlyOne | AtMostOne | NonEmpty | Many @@ -421,8 +429,9 @@ Query : (card : Cardinality) -> Schema -> Type -> Type === What You Lose Without It -Code assumes a query returns one row and crashes when it returns zero. Or code -processes only the first of many results, silently ignoring the rest. +Without other query limits, a request can return zero or many rows when the +caller assumed one. The current L6 presence check rejects an absent `LIMIT`, +but does not establish an exact result count or prevent an overly large limit. --- @@ -724,21 +733,27 @@ The Idris certificate `L10_EpistemicSafe` is witnessed by . an epistemic clause is present; . at least one agent is declared; . every agent referenced by a requirement is among the declared agents; -. the `ENTAILS` graph is acyclic (including transitive cycles). +. the implemented finite-fuel transitive-cycle predicate reports no cycle; its + equivalence to a formal graph-acyclicity definition is not yet proved. -The Idris proof corpus now checks transitive cycles using -`Decide.hasTransitiveCycle`, and `Checker.checkLevel10Sound` proves soundness -for that implemented structural predicate. This is not semantic soundness of -the standalone Kripke model, and not a factive-warrant theorem. +The Idris decider implements transitive-cycle detection using +`Decide.hasTransitiveCycle`. `Checker.checkLevel10Sound` proves that checker +acceptance implies the Boolean structural predicate; it does not prove that +the finite-fuel helper is equivalent to formal graph reachability or acyclicity. +This is not semantic soundness of the standalone Kripke model, and not a +factive-warrant theorem. === Disclosed Residual * **Proposition well-typedness.** The `Expr` carried by an epistemic requirement is not yet checked against the schema. -* **Rust/Idris cycle-check alignment.** The Idris predicate detects - transitive cycles; the Rust mirror in `src/interface/parse/src/decider.rs` - currently detects direct reciprocal `ENTAILS` pairs only. Preserve this - cross-implementation difference when describing the certified path; it +* **Cycle-detector correctness.** The Idris implementation uses finite-fuel + transitive closure, but no theorem establishes equivalence with a formal + graph-reachability/acyclicity definition. +* **Rust/Idris cycle-check alignment.** The Idris implementation attempts to + detect transitive cycles; the Rust mirror in + `src/interface/parse/src/decider.rs` currently detects direct reciprocal + `ENTAILS` pairs only. Preserve this difference when describing the gate; it does not change the fact that source syntax cannot currently request L10. The L10 soundness theorem is real but has a defined scope: it proves the @@ -827,7 +842,7 @@ link:audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc[audit]. | Runtime type mismatches when processing query results | 6 -- Cardinality -| Wrong assumptions about how many results a query returns +| Missing `LIMIT`; the predicate does not establish result cardinality | 7 -- Effects | Missing effect declaration; this predicate does not block writes @@ -839,22 +854,25 @@ link:audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc[audit]. | Missing supported bounded-use annotation; this predicate does not track runtime use | 10 -- Epistemic -| A populated epistemic clause with declared agents and no `ENTAILS` cycles +| Populated clause, declared agents, and no cycle reported by the current detector |=== The level names describe distinct safety dimensions, but they do not by themselves establish that each dimension is enforced by the source parser or at -runtime. In particular, the current L7-L9 predicates inspect fields on an -already-constructed `Statement`: effect-declaration presence, version-constraint -presence, and a supported bounded-use annotation, respectively. They do not -implement the operational effect, freshness, or resource-use guarantees sketched -in those sections. +runtime. In particular, the current L6-L9 predicates inspect fields on an +already-constructed `Statement`: a `LIMIT`, effect-declaration presence, +version-constraint presence, and a supported bounded-use annotation, +respectively. They do not infer exact result cardinality or implement the +operational effect, freshness, or resource-use guarantees sketched in those +sections. Level 10 is a separate *structural* predicate over an already-constructed `Statement`. It requires a populated epistemic clause, at least one declared -agent, references only to declared agents, and an acyclic `ENTAILS` graph. It -does not establish whether the engine is entitled to believe or give an answer; -in particular, it does not prove modal witnesses agree or an authority is -competent. The Idris predicate is proved over the AST, while the Rust mirror -currently checks direct reciprocal entailment pairs only. The ladder therefore -has eleven distinct predicates, not a theorem of epistemic warrant. +agent, references only to declared agents, and no cycle reported by the +implemented finite-fuel `ENTAILS` detector. No theorem proves that detector +matches formal graph acyclicity. L10 does not establish whether the engine is +entitled to believe or give an answer; in particular, it does not prove modal +witnesses agree or an authority is competent. The Idris predicate is proved +over the AST, while the Rust mirror currently checks direct reciprocal +entailment pairs only. The ladder therefore has eleven distinct predicates, +not a theorem of epistemic warrant. diff --git a/docs/architecture/ARCHITECTURE.adoc b/docs/architecture/ARCHITECTURE.adoc index 9282beb..65db4b5 100644 --- a/docs/architecture/ARCHITECTURE.adoc +++ b/docs/architecture/ARCHITECTURE.adoc @@ -32,7 +32,9 @@ for level names, proof scope, and source expressibility. [source] ---- Runtime gate: - VCL source -> Rust lexer/parser -> AST -> Rust `certified_level` -> verdict + VCL source -> Rust `parse_op` -> `VclOp` + Query(Statement) -> `certified_level` -> query verdict + Transit(Transition) -> `certified_transition_level` -> transition verdict (L4 ceiling) Offline verification: Idris proof corpus checks corresponding predicates over the mirrored AST @@ -40,11 +42,13 @@ Offline verification: The source parser is syntax-only and fail-closed on unsupported L7–L10 clauses. Schema resolution happens in the Rust decider for ordinary field -references. The runtime `vclt-gate` calls the Rust `certified_level` decider; -it does not invoke or link the Idris proof corpus. Idris checks the corresponding -predicate and certificate claims offline over the mirrored AST. The VeriSimDB -consumer-side gate integration is a separate outstanding item; this repository -does not currently establish a full parse-to-execution path. +references. For `VclOp::Query`, `vclt-gate` calls the Rust +`certified_level` decider; `VclOp::Transit` is routed separately through +`certified_transition_level`, with an L4 ceiling and a transition-shaped +response. Neither runtime path invokes or links the Idris proof corpus. Idris +checks corresponding predicate and certificate claims offline over the mirrored +AST. The VeriSimDB consumer-side gate integration remains outstanding; this +repository does not establish a full parse-to-execution path. == The 11 Safety Levels @@ -71,7 +75,7 @@ expressibility remains bounded by the parser's L6 ceiling. |L2 |`TypeCompat` -|Compared expression types are compatible +|Types are compatible for comparisons in the `WHERE` clause |`Core.Decide`, `Core.Checker` |Type check @@ -113,17 +117,20 @@ expressibility remains bounded by the parser's L6 ceiling. |L9 |`LinearSafe` -|A `UseOnce` or bounded linear annotation is present +|A `LinUseOnce` or `LinBounded` annotation is present |`Core.Decide`, `Core.Checker` |Check |L10 |`EpistemicSafe` -|Epistemic clause has declared agents and passes the implemented `ENTAILS`-cycle condition +|Populated clause has declared agents and no cycle reported by the implemented `ENTAILS` detector |`Core.Decide`, `Core.Checker`, `Core.Levels` |Check |=== +NOTE: The L10 row names the implemented Boolean cycle check; it is not a theorem +that the finite-fuel helper computes formal graph acyclicity. See the audit. + NOTE: These are the canonical L0–L10 tags, not the obsolete L1–L11 ladder in older architecture prose. The proof predicates apply to an already-built `Statement`; VCL source reaches only through L6 today. L10's current checker @@ -183,15 +190,14 @@ diagram that previously appeared here: [source] ---- Runtime gate request (VCL source text) - -> Rust `parse_op` (`src/interface/parse`) - -> `Statement` AST - -> Rust `certified_level` decider - -> runtime gate verdict + -> Rust `parse_op` (`src/interface/parse`) -> `VclOp` + -> `Query(Statement)` -> `certified_level` -> query verdict + -> `Transit(Transition)` -> `certified_transition_level` -> transition verdict (L4 ceiling) Separately, the Idris proof corpus checks corresponding predicates over the -mirrored AST offline; it does not feed the runtime gate verdict. The versioned +mirrored AST offline; it does not feed either runtime verdict. The versioned wire codec is a separate interface and is not an intermediate step in this -`vclt-gate` runtime path. +`vclt-gate` request path. ---- The parser establishes syntax, not schema-bound types or a full certificate. diff --git a/docs/audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc b/docs/audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc index 05fdcc2..cf51d8f 100644 --- a/docs/audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc +++ b/docs/audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc @@ -34,10 +34,12 @@ the dependency). and epistemic operators). That is real local formal content, but the deployment-facing L10 checker does not import or invoke this module. * L10's local `Checker.checkLevel10` / `Decide.epistemicConsistentStmt` path - checks a populated `EpistemicClause` structurally (declared agents and - `ENTAILS`-cycle conditions). The L10 soundness theorem is about that - predicate over a `Statement`; it does not establish a bridge to the Kripke - model, choreographic K-CUT, or any deployment requirement. + checks a populated `EpistemicClause` structurally (declared agents and the + implemented finite-fuel `ENTAILS`-cycle detector). The L10 soundness theorem + proves checker acceptance implies that Boolean predicate; it does not prove + the helper equivalent to formal graph reachability/acyclicity, nor establish + a bridge to the Kripke model, choreographic K-CUT, or any deployment + requirement. Therefore the Kripke module is not evidence of a K-CUT deployment dependency, and no such blocker should be stated absent a new explicit artefact. From 28693d454c3afd616692e9a46a3662d3c392db28 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 1 Nov 2026 18:40:33 +0000 Subject: [PATCH 5/7] Narrow injection and upper-level predicate claims Signed-off-by: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- README.adoc | 2 +- ROADMAP.adoc | 10 +++++--- docs/THE-10-LEVELS-EXPLAINED.adoc | 39 +++++++++++++++++++---------- docs/architecture/ARCHITECTURE.adoc | 2 +- 4 files changed, 34 insertions(+), 19 deletions(-) diff --git a/README.adoc b/README.adoc index 1b164b8..45ee0ee 100644 --- a/README.adoc +++ b/README.adoc @@ -252,7 +252,7 @@ scope, not the stronger design semantics sketched in older material. | 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` | Implemented raw-string-literal 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 diff --git a/ROADMAP.adoc b/ROADMAP.adoc index 20c632d..798574a 100644 --- a/ROADMAP.adoc +++ b/ROADMAP.adoc @@ -122,10 +122,12 @@ These are ordered by value, not by version number. === v0.3.0 — Research Levels (L6-L9) * [x] `CardinalitySafe` LIMIT-presence predicate (source reachable; no exact result-count inference) -* [ ] Effect-declaration predicate (AST only; no surface syntax or operation - enforcement) -* [ ] Version-constraint presence predicate and proof over AST — no surface syntax or freshness validation -* [ ] L9 bounded-use annotation predicate and proof — no surface syntax or runtime resource enforcement +* [x] Effect-declaration-presence predicate and proof over AST +* [ ] `EFFECTS` source syntax/elaboration and operation enforcement +* [x] Version-constraint-presence predicate and proof over AST +* [ ] Temporal source syntax/elaboration and freshness validation +* [x] L9 bounded-use annotation predicate and proof over AST +* [ ] Linear source syntax/elaboration and runtime resource enforcement * [ ] Integrate TypeQL-Experimental mechanisms === v0.4.0 — Consonance Level (L10) diff --git a/docs/THE-10-LEVELS-EXPLAINED.adoc b/docs/THE-10-LEVELS-EXPLAINED.adoc index 95513ed..58f20ea 100644 --- a/docs/THE-10-LEVELS-EXPLAINED.adoc +++ b/docs/THE-10-LEVELS-EXPLAINED.adoc @@ -103,9 +103,9 @@ rungs and not ten. | Silent blanks in results | 4 -- Injection -| Is user input separated from query structure? -| Compile time (by construction) -| Attackers run arbitrary commands +| Does the `WHERE` clause contain an embedded string literal? +| AST predicate; only `WHERE` is inspected +| An embedded string literal in `WHERE` fails L4 | 5 -- Result | Is the return type known? @@ -292,21 +292,32 @@ but violate every reasonable expectation. --- -== Level 4: Injection-Proof Safety +== Level 4: InjectionProof — WHERE Literal Predicate + +[NOTE] +==== +The current L4 predicate checks only for embedded string literals in the +`WHERE` expression. It does not inspect `HAVING` or other clauses, and it does +not prove a general no-injection property for the whole statement. +==== === What It Checks -User input is a fundamentally different type from query structure. They _cannot_ -be combined. This is not sanitisation or escaping -- it is a structural -impossibility enforced by the type system. +`InjectionProof` is witnessed by the structural condition that the `WHERE` +clause contains no string literal. This is narrower than proving that user +input can never be combined with query structure. === When It Checks -At **compile time**, by construction. The parser produces a typed AST where -parameters are typed slots, not string holes. There is no string concatenation -path that could produce a query. +The predicate inspects the `where_clause` field on an already-constructed +`Statement`; it is not a general compile-time proof about how the statement was +created or how values will be bound. -=== How VCL-total Implements It +=== Intended Design Sketch + +Typed parameters are one intended way to keep user input separate from query +structure. The following pseudocode illustrates that design goal; it is not the +full guarantee provided by the current L4 predicate. ---- -- VCL-total query with typed parameter @@ -324,7 +335,9 @@ SELECT users WHERE users.id = ?id === What You Lose Without It -Injection attacks. The #1 web application security risk for over a decade. +Without broader parameterization and validation, injection risks remain. The +current L4 predicate rejects embedded string literals in `WHERE`; it is not a +general injection proof for all clauses or for the full source-to-runtime path. --- @@ -836,7 +849,7 @@ link:audits/K-CUT-VCL-UT-RELATIONSHIP-2026-11-01.adoc[audit]. | Null pointer exceptions, silent blanks in results | 4 -- Injection -| SQL/VCL injection attacks -- the #1 web security risk +| Embedded string literal in `WHERE`; not a general injection proof | 5 -- Result | Runtime type mismatches when processing query results diff --git a/docs/architecture/ARCHITECTURE.adoc b/docs/architecture/ARCHITECTURE.adoc index 65db4b5..6441e8f 100644 --- a/docs/architecture/ARCHITECTURE.adoc +++ b/docs/architecture/ARCHITECTURE.adoc @@ -87,7 +87,7 @@ expressibility remains bounded by the parser's L6 ceiling. |L4 |`InjectionProof` -|Implemented raw-string-literal predicate holds +|No embedded string literal in `WHERE`; other clauses are not checked |`Core.Decide`, `Core.Checker` |Check From a903bed14695d53eebf721a2cfa37cea39ca594c Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 1 Nov 2026 18:54:55 +0000 Subject: [PATCH 6/7] Document transition verdict contract and L10 detector scope Signed-off-by: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- docs/vclt-gate-contract.adoc | 183 +++++++++++------- .../proofs/AGDA-GRADE3-PORT-PLAN.adoc | 2 +- 2 files changed, 116 insertions(+), 69 deletions(-) diff --git a/docs/vclt-gate-contract.adoc b/docs/vclt-gate-contract.adoc index aff367e..48c4a33 100644 --- a/docs/vclt-gate-contract.adoc +++ b/docs/vclt-gate-contract.adoc @@ -18,9 +18,11 @@ a `schema_version` bump and an update here. Owners: * *Producer* (this repo): the `vclt-gate` binary — a thin, pure wrapper over - `vcltotal-parse`'s lexer/parser + `decider::certified_level`. + `vcltotal-parse`'s `parse_op`, routing query statements to + `decider::certified_level` and transitions to + `decider::certified_transition_level`. * *Consumer* (VeriSimDB): invokes the binary on the VCL execute path before - a statement is allowed to affect live consonance state. + a query or transition is allowed to affect live consonance state. == Why a CLI subprocess (and not FFI / a library / a network call) @@ -40,19 +42,26 @@ defined here so the verdict semantics are unchanged. == What the gate decides (and what it does NOT) -The gate answers one question: - -____ -Is this VCL statement *admissible up to its declared static safety level*? -____ - -It computes the *recompute-tier verdict* `decider::certified_level(stmt, -schema)` — an independent re-establishment of the corpus-proved safety -predicate `checkLevelNSound` (machine-checked once in -`verification/proofs/corpus/VclTotal/Core/Checker.idr`). The ten levels -are structurally decidable from the parsed statement + schema alone (see -§"Safety levels"), so the gate needs *no* theorem prover and *no* engine -state. +The gate handles two variants of parsed VCL operations: + +* A query (`VclOp::Query`) is admissible up to its declared static safety + level, using `decider::certified_level(stmt, schema)`. +* A consonance transition (`VclOp::Transit`) is checked by + `decider::certified_transition_level(transition, schema)`. Its response has + a single L4 `InjectionProof` entry; transitions do not use the query ladder + above L4. The current transition predicate checks required subject + distinctness, absence of raw string literals in optional evidence, and + evidence-comparison type compatibility. It does not establish provenance + descent, engine liveness, modality presence, or identity-versus-location. + +For query statements, the Rust decider is the runtime recompute tier and the +Idris `checkLevelNSound` lemmas establish agreement between checker acceptance +and the corresponding Boolean predicates (machine-checked in +`verification/proofs/corpus/VclTotal/Core/Checker.idr`). This does not extend +the predicates' semantic scope; for example, no theorem currently proves that +the finite-fuel L10 cycle helper is equivalent to formal graph acyclicity. +Both runtime variants are structurally decided from parsed input and schema; +the gate needs *no* theorem prover and *no* live engine state. The gate explicitly does **NOT**: @@ -62,8 +71,8 @@ The gate explicitly does **NOT**: downstream. * Touch live consonance state, the network, the filesystem (beyond its own stdin/stdout and an `--input` request file), or any clock. It is a pure function of its input (§"Purity"). -* Maintain state between invocations. One statement per call (batching is a - reserved future `schema_version`). +* Maintain state between invocations. One parsed operation per call (batching + is a reserved future `schema_version`). == Transport @@ -106,15 +115,15 @@ The gate explicitly does **NOT**: |`schema_version` |yes |Integer. The binary MUST reject a version it does not understand with exit code 2 and `error.kind = "unsupported_version"`. -|`statement` |yes |The VCL statement *text*. The binary lexes + parses it; -a parse failure is a verdict (`certified_level = -1`, reason category -`syntactic`), *not* a gate error. +|`statement` |yes |VCL query or transition *source text*. The binary lexes and parses it with `parse_op`; a parse failure is rendered as an inadmissible parse verdict (L0 `ParseSafe`), *not* a gate error. Parsed queries and transitions follow their separate verdict variants below. -|`schema` |no |The octad schema the schema-dependent levels (L1/L2/L3/L5) +|`schema` |no |The octad schema the query's schema-dependent levels (L1/L2/L3/L5) recompute against, in the JSON form of §"Schema payload". If omitted, the -binary uses the empty schema; schema-dependent levels then fail closed -(an unknown field cannot be certified type-compatible). Statements whose -requested level is schema-independent (L4, L6–L10) are unaffected. +binary uses the empty schema; schema-dependent query levels then fail closed +(an unknown field cannot be certified type-compatible). Schema-independent +query levels (L4, L6–L10) are unaffected. Transition verdicts also use the +schema for evidence type compatibility; omitting it can therefore affect a +transition verdict. |=== Unknown request fields MUST be ignored (forward-compat). @@ -145,20 +154,13 @@ Unknown request fields MUST be ignored (forward-compat). |=== |Field |Meaning -|`admissible` |`true` iff `certified_level == requested_level` (i.e. -`certified_level != -1`). This is the single boolean the consumer gates on. +|`admissible` |`true` iff `certified_level == requested_level` (i.e. `certified_level != -1`). This is the single boolean the consumer gates on for either response variant. -|`requested_level` |Integer 0–10: the level the statement declares -(`Statement.requested_level`, the `SafetyLevel` tag). +|`requested_level` |For a query, integer 0–10 from `Statement.requested_level`. For a transition, fixed at 4 (`InjectionProof`). -|`certified_level` |Integer. `-1` if the statement fails any level `1..k` -(where `k = requested_level`); otherwise `k`. Faithful return of -`decider::certified_level`. +|`certified_level` |For a query, `-1` if any level `1..k` fails, otherwise `k`, faithfully returned by `decider::certified_level`. For a transition, `-1` on failure or `4` on success, returned by `decider::certified_transition_level`. -|`levels` |Per-level breakdown for `1..k`. `status ∈ {pass, fail}`. The -binary SHOULD evaluate all of `1..k` (not just up to the first failure) so -the array is a complete diagnostic; `certified_level` still reflects the -short-circuit semantics. A failing level SHOULD carry a human `reason`. +|`levels` |For a query, per-level breakdown for `1..k`. For a transition, one entry for L4 `InjectionProof`; transitions have no L5+ result-set ladder. Each entry has `status ∈ {pass, fail}`. A failing query entry SHOULD carry a human `reason`; a transition rejection carries its reason in the top-level `reasons` array. |`reasons` |Flat list of human-readable rejection reasons (empty when admissible). Stable enough to surface to an API caller. @@ -167,11 +169,47 @@ admissible). Stable enough to surface to an API caller. A `syntactic` (parse) failure renders as `certified_level: -1`, an empty or single-entry `levels` array, and a `reasons` entry prefixed `L0 ParseSafe:`. +=== Transition response variant (`schema_version: 1`) + +`parse_op` routes `MERGE`, `SPLIT`, and `NORMALISE` to the transition decider. +These responses use the same v1 request and exit-code conventions, but a +transition-specific response body: + +[source,json] +---- +{ + "schema_version": 1, + "kind": "transition", + "verb": "MERGE", + "subjects": ["left", "right", "out"], + "admissible": true, + "requested_level": 4, + "certified_level": 4, + "levels": [ + { "level": 4, "name": "InjectionProof", "status": "pass" } + ], + "reasons": [] +} +---- + +For this variant, `kind` is exactly `"transition"`; query responses retain +the response shape above without a `kind` field. `verb` is `MERGE`, `SPLIT`, +or `NORMALISE`; `subjects` contains the transition's subject handles in +constructor order. `requested_level` is fixed at L4. The transition +decider returns `certified_level` 4 on acceptance or -1 on rejection, and the +`levels` array contains the single L4 entry with `status: "pass"` or +`"fail"`. A rejection puts the current generic reason in the top-level +`reasons` array: `transition inadmissible: self-merge / non-distinct outputs, +or evidence carries a raw string literal / type-incompatible comparison`. +Exit codes remain 0 (admissible) and 1 (inadmissible). This is the transition +response already emitted by the v1 producer, not a change to its wire shape. + == Safety levels (authoritative) -The level vocabulary is owned by `src/interface/parse/src/ast.rs` -(`enum SafetyLevel`, tags 0–10) and `decider::check_level`. The gate MUST -use these names and numbers verbatim: +The query-level vocabulary is owned by `src/interface/parse/src/ast.rs` +(`enum SafetyLevel`, tags 0–10) and `decider::check_level`. This table +covers the query ladder; transitions use the separate L4 verdict variant +documented above. The gate MUST use these names and numbers verbatim: [cols="1,2,4"] |=== @@ -187,16 +225,23 @@ use these names and numbers verbatim: |7 |EffectTracked |`effect_decl.is_some()` — an effect declaration is present |8 |TemporalSafe |`version_const.is_some()` — a version constraint is present |9 |LinearSafe |`linear_enforced` — linear-resource annotation satisfied -|10 |EpistemicSafe |`epistemic_consistent_stmt` — epistemic clause well-formed + acyclic +|10 |EpistemicSafe |`epistemic_consistent_stmt` — populated clause and declared agents; the finite-fuel cycle detector reports no `ENTAILS` cycle |=== -*Subsumption* (proved in `Core/Levels.idr`): certification at level N implies -levels `1..N` all pass. The consumer therefore needs only `admissible` + -`certified_level`; the `levels` array is diagnostic. +*Subsumption* (proved in `Core/Levels.idr`): a query certificate at level N +requires levels `1..N` to pass. The consumer therefore needs only +`admissible` + `certified_level`; the `levels` array is diagnostic. + +For L10, `checkLevel10Sound` proves checker acceptance implies the Boolean +`epistemic_consistent_stmt` predicate. It does not prove that the finite-fuel +cycle detector is equivalent to a formal graph-reachability/acyclicity +definition; that correctness obligation remains outstanding. -The producer binary MUST obtain its verdict by calling -`decider::certified_level`, never by re-implementing the predicates, so the -corpus soundness proof carries through to the gate. +The producer binary MUST obtain query verdicts by calling +`decider::certified_level` and transition verdicts by calling +`decider::certified_transition_level`, never by re-implementing their +predicates. The Idris checker soundness proofs apply to their stated Boolean +predicates, not to unstated semantic guarantees. == Schema payload @@ -271,28 +316,27 @@ the safety-level predicates or their tags. Consumers that omitted |Code |Meaning |Consumer action |0 |Admissible (`certified_level == requested_level`) |Proceed; the -statement may affect live state. +query or transition may affect live state. |1 |Inadmissible — verdict rendered (`certified_level == -1`) |Reject the -statement; surface `reasons` to the caller (e.g. HTTP 422). +query or transition; surface `reasons` to the caller (e.g. HTTP 422). |2 |Gate error — no verdict (bad request JSON, unsupported version, internal guard) |Treat as gate-unavailable; apply the fail policy (§Consumer). |=== -The binary MUST NOT exit non-zero-2 for an *inadmissible* statement: a -rejection is a successful decision (exit 1), distinct from a gate fault +The binary MUST NOT exit non-zero-2 for an *inadmissible* query or transition: +a rejection is a successful decision (exit 1), distinct from a gate fault (exit 2). On exit 2 it SHOULD still emit a JSON object with an `error` field (`{ "schema_version": 1, "error": { "kind": "...", "message": "..." } }`). == Purity guarantee (producer) -The binary is a pure function of (`statement`, `schema`): no network, no -filesystem access beyond stdin/stdout and the request file named by +The binary is a pure function of the parsed operation and schema: no network, +no filesystem access beyond stdin/stdout and the request file named by `--input` (which is the request itself, read once, not ambient state), no -clock, no environment-dependent -behaviour, no randomness, deterministic for identical input. This is what -makes it safe to call synchronously on the consumer's write path. -`decider::certified_level` already satisfies this; the wrapper MUST NOT add -impurity. +clock, no environment-dependent behaviour, no randomness, deterministic for +identical input. This is what makes it safe to call synchronously on the +consumer's write path. Both deciders already satisfy this; the wrapper MUST +NOT add impurity. == Consumer integration (VeriSimDB) @@ -348,9 +392,11 @@ treat a timeout as exit 2. nor the response shape, so no `schema_version` bump; stdin remains the default and every existing consumer is unaffected. Covered by `src/interface/parse/tests/gate_transport.rs`. -* The L5–L10 predicates already evaluate today; no part of this contract is - blocked on the echidna proof tier. The proof tier, when wired, is a - *separate* downstream check, not a change to this gate. +* The Idris/Rust AST-level predicates L5–L10 are implemented, but the current + Rust source parser does not yet expose the extension syntax needed to express + L7–L10 through this text request path. This contract does not depend on the + echidna proof tier; proof discharge, when wired, remains a *separate* + downstream check, not a change to this gate. == Worked examples @@ -403,12 +449,14 @@ Response (exit 1): *Producer (this repo) — the `vclt-gate` binary:* -. New bin crate (or `[[bin]]` on `vcltotal-parse`) reading the request JSON, - calling the existing lexer/parser then `decider::certified_level`. -. Serialise the response per §"Response schema"; map verdict to exit codes. -. Implement `OctadSchema` JSON (de)serialisation consistent with `wire.rs`. -. Conformance tests from fixture request/response pairs (the two worked - examples are the first two fixtures). +. Read request JSON, call `parse_op`, and route queries to + `decider::certified_level` and transitions to + `decider::certified_transition_level`. +. Serialise the matching response variant per §"Response schema" and map the + verdict to the exit codes. +. Keep `OctadSchema` JSON (de)serialisation consistent with `wire.rs`. +. Maintain conformance fixtures for admitted/rejected queries and transition + verdicts. *Consumer (VeriSimDB):* @@ -417,6 +465,5 @@ Response (exit 1): . Build the request (`statement` text + `schema` from `SchemaRegistry`, or omit `schema` for the conservative default). . Branch on exit code per §"Fail policy"; surface `reasons` on rejection. -. An integration test: admitted statement proceeds; injection statement is - rejected with the gate's reason — the executable form of the README's - engine / VCL / VCL-total triad. +. Integration tests: an admitted query proceeds; an inadmissible query and + transition are rejected before any write, with the gate's reasons surfaced. diff --git a/verification/proofs/AGDA-GRADE3-PORT-PLAN.adoc b/verification/proofs/AGDA-GRADE3-PORT-PLAN.adoc index be63ffa..b89115e 100644 --- a/verification/proofs/AGDA-GRADE3-PORT-PLAN.adoc +++ b/verification/proofs/AGDA-GRADE3-PORT-PLAN.adoc @@ -70,7 +70,7 @@ before implementation. |L7 `EffectTracked` |`effectDecl` is present; `checkLevel7Sound`. |Formalise the exact AST field and presence predicate. |Presence is not effect correctness or proof execution stays within the declaration; no source syntax currently populates it. |L8 `TemporalSafe` |`versionConst` is present; `checkLevel8Sound`. |Formalise the exact AST field and presence predicate. |Presence is not freshness, clock correctness, or snapshot fidelity; no source syntax currently populates it. |L9 `LinearSafe` |`LinUseOnce` or `LinBounded`; `LinUnlimited` and absence fail; `checkLevel9Sound`. |Formalise the annotation datatype, enforcement predicate, and acceptance theorem. |Does not prove runtime resource use or affine behavior of an external handle; no source syntax currently populates it. -|L10 `EpistemicSafe` |A populated clause has a declared agent set, all referenced agents declared, and an acyclic `ENTAILS` graph; `checkLevel10Sound`. |Formalise that structural predicate, including transitive cycle detection, and the exact acceptance theorem. |Does not prove factivity, proposition typing, Kripke-model soundness, real-world truth, or a K-CUT/deployment dependency. Rust currently checks direct reciprocal cycles only. +|L10 `EpistemicSafe` |A populated clause has a declared agent set, all referenced agents declared, and no cycle reported by the current finite-fuel `ENTAILS` detector; `checkLevel10Sound` proves checker acceptance implies this Boolean predicate. |Formalise the exact implemented predicate and acceptance theorem; separately prove whether the finite-fuel detector is equivalent to a stated graph-reachability/acyclicity definition. |Does not establish graph-theoretic cycle-detector correctness, factivity, proposition typing, Kripke-model soundness, real-world truth, or a K-CUT/deployment dependency. Rust currently checks direct reciprocal cycles only. |=== == Stages and gates From 68eb6921c14c912d10fccdffc20b22b83fa54ba6 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Sun, 1 Nov 2026 19:06:35 +0000 Subject: [PATCH 7/7] Clarify runtime L10 and cardinality bounds Signed-off-by: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- docs/THE-10-LEVELS-EXPLAINED.adoc | 20 ++++++++-------- docs/vclt-gate-contract.adoc | 39 +++++++++++++++---------------- 2 files changed, 29 insertions(+), 30 deletions(-) diff --git a/docs/THE-10-LEVELS-EXPLAINED.adoc b/docs/THE-10-LEVELS-EXPLAINED.adoc index 58f20ea..d8fffdf 100644 --- a/docs/THE-10-LEVELS-EXPLAINED.adoc +++ b/docs/THE-10-LEVELS-EXPLAINED.adoc @@ -407,11 +407,11 @@ L6 predicate: |=== | VCL-total Syntax | Meaning -| `SELECT UNIQUE ...` -| Returns `ExactlyOne` -- compile error if uniqueness cannot be proved +| `SELECT UNIQUE ...` (illustrative unique-key lookup) +| Returns `AtMostOne` -- a uniqueness proof bounds matches to one, but does not prove a match exists -| `SELECT OPTIONAL ...` -| Returns `AtMostOne` -- caller must handle the empty case +| `SELECT ... LIMIT 1` +| Returns `AtMostOne` -- the caller must handle the empty case | `SELECT ...` | Returns `List` -- zero or more results @@ -421,13 +421,13 @@ L6 predicate: -- Schema: users.id has UNIQUE constraint SELECT UNIQUE users WHERE users.id = ?id --- Return type: ExactlyOne --- The compiler proves this from the UNIQUE constraint on users.id. - -SELECT OPTIONAL users WHERE users.email = ?email -- Return type: AtMostOne --- Email is not unique, so we might get zero results. --- The caller MUST pattern-match on Some/None. +-- The UNIQUE constraint proves at most one match, not that the id exists. +-- The caller MUST handle the zero-result case. + +SELECT users WHERE users.email = ?email +-- Return type: List +-- Email is not unique, so this may return multiple rows. ---- === Illustrative Cardinality Encoding diff --git a/docs/vclt-gate-contract.adoc b/docs/vclt-gate-contract.adoc index 48c4a33..f0d147a 100644 --- a/docs/vclt-gate-contract.adoc +++ b/docs/vclt-gate-contract.adoc @@ -54,14 +54,17 @@ The gate handles two variants of parsed VCL operations: evidence-comparison type compatibility. It does not establish provenance descent, engine liveness, modality presence, or identity-versus-location. -For query statements, the Rust decider is the runtime recompute tier and the -Idris `checkLevelNSound` lemmas establish agreement between checker acceptance -and the corresponding Boolean predicates (machine-checked in -`verification/proofs/corpus/VclTotal/Core/Checker.idr`). This does not extend -the predicates' semantic scope; for example, no theorem currently proves that -the finite-fuel L10 cycle helper is equivalent to formal graph acyclicity. -Both runtime variants are structurally decided from parsed input and schema; -the gate needs *no* theorem prover and *no* live engine state. +For query statements, the Rust decider is the runtime recompute tier. The +Idris `checkLevelNSound` lemmas separately establish checker acceptance +implies the Idris-side Boolean predicates over `Statement` values +(machine-checked in `verification/proofs/corpus/VclTotal/Core/Checker.idr`). +The runtime binary does not invoke or link that corpus; these lemmas do not by +themselves prove Rust correctness or Rust/Idris refinement. In particular, +Idris uses a finite-fuel transitive L10 cycle detector, while Rust currently +checks direct reciprocal `ENTAILS` pairs only. No theorem proves the Idris +detector equivalent to formal graph acyclicity. Both runtime variants are +structurally decided from parsed input and schema; the gate needs *no* theorem +prover and *no* live engine state. The gate explicitly does **NOT**: @@ -117,13 +120,7 @@ not understand with exit code 2 and `error.kind = "unsupported_version"`. |`statement` |yes |VCL query or transition *source text*. The binary lexes and parses it with `parse_op`; a parse failure is rendered as an inadmissible parse verdict (L0 `ParseSafe`), *not* a gate error. Parsed queries and transitions follow their separate verdict variants below. -|`schema` |no |The octad schema the query's schema-dependent levels (L1/L2/L3/L5) -recompute against, in the JSON form of §"Schema payload". If omitted, the -binary uses the empty schema; schema-dependent query levels then fail closed -(an unknown field cannot be certified type-compatible). Schema-independent -query levels (L4, L6–L10) are unaffected. Transition verdicts also use the -schema for evidence type compatibility; omitting it can therefore affect a -transition verdict. +|`schema` |no |The octad schema used by schema-dependent query predicates (L1/L2/L3/L5), in the JSON form of §"Schema payload". If omitted, the binary uses the empty schema and unknown fields fail closed. Although the individual L4 and L6–L10 query predicates do not inspect the schema, certification at a requested level still evaluates every preceding level; missing schema metadata can therefore make the overall verdict inadmissible at an earlier level. Transition verdicts also use the schema for evidence type compatibility, so omitting it can affect that verdict too. |=== Unknown request fields MUST be ignored (forward-compat). @@ -225,17 +222,19 @@ documented above. The gate MUST use these names and numbers verbatim: |7 |EffectTracked |`effect_decl.is_some()` — an effect declaration is present |8 |TemporalSafe |`version_const.is_some()` — a version constraint is present |9 |LinearSafe |`linear_enforced` — linear-resource annotation satisfied -|10 |EpistemicSafe |`epistemic_consistent_stmt` — populated clause and declared agents; the finite-fuel cycle detector reports no `ENTAILS` cycle +|10 |EpistemicSafe |Rust `epistemic_consistent_stmt` — populated clause, declared agents, and no direct reciprocal `ENTAILS` pair; not a general transitive-cycle check |=== *Subsumption* (proved in `Core/Levels.idr`): a query certificate at level N requires levels `1..N` to pass. The consumer therefore needs only `admissible` + `certified_level`; the `levels` array is diagnostic. -For L10, `checkLevel10Sound` proves checker acceptance implies the Boolean -`epistemic_consistent_stmt` predicate. It does not prove that the finite-fuel -cycle detector is equivalent to a formal graph-reachability/acyclicity -definition; that correctness obligation remains outstanding. +The Idris `checkLevel10Sound` theorem proves Idris checker acceptance implies +its Boolean `epistemicConsistentStmt` predicate, whose implementation uses a +finite-fuel transitive cycle detector. It does not prove that detector +is equivalent to a formal graph-reachability/acyclicity definition. The Rust +gate implementation differs: it rejects direct reciprocal `ENTAILS` pairs +only, and no theorem here proves Rust/Idris alignment. The producer binary MUST obtain query verdicts by calling `decider::certified_level` and transition verdicts by calling