diff --git a/.github/dependabot.yml b/.github/dependabot.yml index 4d9ae2f..9ffdd74 100644 --- a/.github/dependabot.yml +++ b/.github/dependabot.yml @@ -1,10 +1,34 @@ # SPDX-License-Identifier: MPL-2.0 -# Dependabot configuration for RSR-compliant repositories -# Covers common ecosystems - remove unused ones for your project +# Dependabot configuration for vcl-ut. +# +# Trimmed from the RSR template on 2026-07-21. Only ecosystems with an actual +# manifest in this repository are declared. Declaring an ecosystem with no +# manifest makes the corresponding Dependabot job fail on EVERY run — this +# repository was failing `hex`, `pip`, `nix` and `npm_and_yarn` weekly for +# exactly that reason (measured: 5 consecutive red runs from 2026-07-13). +# +# vcl-ut is Rust-only. Verified absent at the root: mix.exs, package.json, +# requirements.txt, pyproject.toml, flake.nix. +# +# Cargo note: this repository has FIVE cargo workspace roots, not one. A single +# `directory: "/"` entry covers the root workspace only, so the crates holding +# most of the actual code were invisible to Dependabot. Each self-contained +# workspace root is now declared explicitly: +# +# / root workspace (vcl-ut, fmt, lint, core) +# /src/interface/parse parser + decider + vclt-gate <- the real spine +# /src/interface/attest depends on ../parse (in-repo) +# /src/interface/recompute-wasm depends on ../parse (in-repo) +# +# DELIBERATELY EXCLUDED: /src/interface/echidna-client. It depends on +# ../../interface, which in turn carries an out-of-tree path dependency +# (`echidna-core = { path = "../../../echidna/..." }`). Dependabot cannot +# resolve a path dependency outside the repository, so declaring it would +# reintroduce exactly the always-red job this trim removes. version: 2 updates: - # GitHub Actions - always include + # GitHub Actions — always include. - package-ecosystem: "github-actions" directory: "/" schedule: @@ -14,38 +38,33 @@ updates: patterns: - "*" - # Rust/Cargo + # Rust/Cargo — one entry per self-contained workspace root. + # + # `open-pull-requests-limit: 0` suppresses routine version-update PRs while + # leaving Dependabot SECURITY PRs flowing. The previous `ignore: "*" patch` + # rule also silenced security PRs under GitHub's current Dependabot + # behaviour. See rsr-template-repo commit 78b050e and + # 007-lang/audits/audit-dependabot-automation-gap-2026-04-17.md. - package-ecosystem: "cargo" directory: "/" schedule: interval: "weekly" - # `open-pull-requests-limit: 0` suppresses routine version-update PRs - # while leaving Dependabot SECURITY PRs flowing. The previous - # `ignore: "*" patch` rule also silenced security PRs under GitHub\'s - # current Dependabot behaviour. See rsr-template-repo commit 78b050e - # and 007-lang/audits/audit-dependabot-automation-gap-2026-04-17.md. open-pull-requests-limit: 0 - # Elixir/Mix - - package-ecosystem: "mix" - directory: "/" - schedule: - interval: "weekly" - - # Node.js/npm - - package-ecosystem: "npm" - directory: "/" + - package-ecosystem: "cargo" + directory: "/src/interface/parse" schedule: interval: "weekly" + open-pull-requests-limit: 0 - # Python/pip - - package-ecosystem: "pip" - directory: "/" + - package-ecosystem: "cargo" + directory: "/src/interface/attest" schedule: interval: "weekly" + open-pull-requests-limit: 0 - # Nix flakes - - package-ecosystem: "nix" - directory: "/" + - package-ecosystem: "cargo" + directory: "/src/interface/recompute-wasm" schedule: interval: "weekly" + open-pull-requests-limit: 0 diff --git a/.github/workflows/dogfood-gate.yml b/.github/workflows/dogfood-gate.yml index 875ac5a..44199a7 100644 --- a/.github/workflows/dogfood-gate.yml +++ b/.github/workflows/dogfood-gate.yml @@ -280,26 +280,26 @@ jobs: # Validate TOML structure using Python 3.11+ tomllib python3 -c " -import tomllib, sys -with open('eclexiaiser.toml', 'rb') as f: - data = tomllib.load(f) -project = data.get('project', {}) -if not project.get('name', '').strip(): - print('ERROR: project.name is required', file=sys.stderr) - sys.exit(1) -functions = data.get('functions', []) -if not functions: - print('ERROR: at least one [[functions]] entry is required', file=sys.stderr) - sys.exit(1) -for fn in functions: - if not fn.get('name', '').strip(): - print('ERROR: function name cannot be empty', file=sys.stderr) - sys.exit(1) - if not fn.get('source', '').strip(): - print(f'ERROR: function {fn[\"name\"]} has no source path', file=sys.stderr) - sys.exit(1) -print(f'Valid: {project[\"name\"]} ({len(functions)} function(s))') -" || { + import tomllib, sys + with open('eclexiaiser.toml', 'rb') as f: + data = tomllib.load(f) + project = data.get('project', {}) + if not project.get('name', '').strip(): + print('ERROR: project.name is required', file=sys.stderr) + sys.exit(1) + functions = data.get('functions', []) + if not functions: + print('ERROR: at least one [[functions]] entry is required', file=sys.stderr) + sys.exit(1) + for fn in functions: + if not fn.get('name', '').strip(): + print('ERROR: function name cannot be empty', file=sys.stderr) + sys.exit(1) + if not fn.get('source', '').strip(): + print(f'ERROR: function {fn[\"name\"]} has no source path', file=sys.stderr) + sys.exit(1) + print(f'Valid: {project[\"name\"]} ({len(functions)} function(s))') + " || { echo "::error file=eclexiaiser.toml::Invalid eclexiaiser.toml — see step output for details" exit 1 } diff --git a/.github/workflows/e2e.yml b/.github/workflows/e2e.yml index 49b65c8..e06356a 100644 --- a/.github/workflows/e2e.yml +++ b/.github/workflows/e2e.yml @@ -1,4 +1,30 @@ # SPDX-License-Identifier: MPL-2.0 +# +# e2e.yml — Root-workspace test gate. +# +# The root workspace has four members (vcl-total, vcltotal-fmt, vcltotal-lint, +# vcltotal-core) and its whole test surface lives in `tests/`, because the root +# crate is a re-export facade over fmt + lint. Per-crate UNIT counts are +# therefore all zero, which makes a truncated `cargo test` log look like an +# empty gate; it is not. Measured 2026-07-21: 102 tests. +# +# tests/e2e_test.rs 20 +# tests/fuzz_test.rs 13 +# tests/integration_test.rs 59 +# tests/property_test.rs 10 +# +# This job previously ran only property_test + integration_test, so 33 of the +# 102 — every e2e and fuzz test — never ran in CI. It now runs the whole +# workspace. +# +# The former "Provide echidna sibling" steps have been removed. They cloned a +# whole repository on every run for nothing: `src/interface` (the member that +# carries the external `echidna-core` path-dep) is deliberately NOT a root +# workspace member, so neither `cargo test --workspace` nor `tests/e2e.sh` +# ever resolves it. Verified 2026-07-21 by running both with no sibling +# present: 102 tests pass, e2e.sh reports 19/19. echidna-client is gated +# separately in backend-matrix.yml, which does need the sibling. + name: E2E, Property and Aspect Tests on: push: { branches: [main] } @@ -15,13 +41,10 @@ jobs: - name: Install Rust uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7 # stable - uses: Swatinem/rust-cache@779680da715d629ac1d338a641029a2f4372abb5 # v2 - # echidna-core path-dependency (src/interface/Cargo.toml) — provide as sibling. - - name: Provide echidna sibling - run: git clone --depth 1 https://github.com/hyperpolymath/echidna ../echidna - name: Run E2E validation run: bash tests/e2e.sh property: - name: Property and integration tests + name: Root workspace tests runs-on: ubuntu-latest timeout-minutes: 15 steps: @@ -29,13 +52,11 @@ jobs: - name: Install Rust uses: dtolnay/rust-toolchain@4be9e76fd7c4901c61fb841f559994984270fce7 # stable - uses: Swatinem/rust-cache@779680da715d629ac1d338a641029a2f4372abb5 # v2 - # echidna-core path-dependency (src/interface/Cargo.toml) — provide as sibling. - - name: Provide echidna sibling - run: git clone --depth 1 https://github.com/hyperpolymath/echidna ../echidna - - name: Run property tests - run: cargo test --test property_test - - name: Run integration tests - run: cargo test --test integration_test + # Whole workspace, all targets — not a hand-picked subset. Previously + # `--test property_test` + `--test integration_test` only, which silently + # skipped tests/e2e_test.rs and tests/fuzz_test.rs. + - name: Run root workspace tests (expect 102) + run: cargo test --workspace --all-targets --locked aspect: name: Aspect tests runs-on: ubuntu-latest diff --git a/.github/workflows/satellite-crates-gate.yml b/.github/workflows/satellite-crates-gate.yml new file mode 100644 index 0000000..406808f --- /dev/null +++ b/.github/workflows/satellite-crates-gate.yml @@ -0,0 +1,85 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# satellite-crates-gate.yml — Gates the self-contained satellite workspaces. +# +# vcl-ut has FIVE cargo workspace roots, not one. Before this workflow, CI +# covered only three of them: +# +# / e2e.yml +# /src/interface/parse parse-gate.yml +# /src/interface/echidna-client backend-matrix.yml (needs echidna sibling) +# /src/interface/attest NOTHING <- gated here +# /src/interface/recompute-wasm NOTHING <- gated here +# +# The cost of that gap was measured on 2026-07-21: both ungated crates had +# stopped compiling. `ast::Statement` gained the S1 consonance field `verb` +# (DECLARE / ASSERT / RETRACT / MERGE / ...), and neither crate's test module +# was updated, so both failed with E0063 `missing field 'verb'`. Their +# libraries still built, so nothing downstream noticed; 12 tests had simply +# stopped running. Silent rot in exactly the crates that carry the +# attestation and recompute boundaries. +# +# Both crates are self-contained (in-repo path deps only), so unlike +# echidna-client they need no sibling checkout and can be gated cheaply. +# +# Tracked: vcl-ut#25. + +name: Satellite Crates Gate + +on: + pull_request: + branches: ['**'] + push: + branches: [main, master] + +permissions: + contents: read + +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +jobs: + satellite-gate: + name: ${{ matrix.crate }} — clippy / tests + runs-on: ubuntu-latest + timeout-minutes: 15 + + strategy: + fail-fast: false + matrix: + crate: [attest, recompute-wasm] + + steps: + - name: Checkout repository + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2 + + # rustup is preinstalled on ubuntu-latest; no third-party action + # (avoids the action-pinning / deprecated-cache hazards). Mirrors + # parse-gate.yml deliberately. + - name: Pin toolchain + components + run: | + set -euo pipefail + rustup show active-toolchain || rustup default stable + rustup component add clippy + cargo --version && cargo clippy --version + + # Operate via the manifest path so CI never traverses the parent + # virtual workspace, whose `src/interface` member carries an external + # path-dep that does not resolve in a standalone checkout. + # + # `--locked` is deliberately NOT used: these two lockfiles drifted while + # the crates were ungated. They are regenerated and committed as part of + # the repair; once a Dependabot cycle has run against them, `--locked` + # should be restored here to make lockfile drift itself a gate. + - name: Clippy — warnings are errors + run: | + set -euo pipefail + cargo clippy --manifest-path src/interface/${{ matrix.crate }}/Cargo.toml \ + --all-targets -- -D warnings + + - name: Tests + run: | + set -euo pipefail + cargo test --manifest-path src/interface/${{ matrix.crate }}/Cargo.toml diff --git a/Cargo.toml b/Cargo.toml index 2478507..1dbd498 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -5,7 +5,7 @@ version = "0.1.0" edition = "2021" license = "MPL-2.0" authors = ["Jonathan D.A. Jewell "] -repository = "https://github.com/hyperpolymath/vql-ut" +repository = "https://github.com/hyperpolymath/vcl-ut" description = "VCL-total: 10-level type-safe query language for VeriSimDB" # The top-level crate re-exports the formatter and linter for integration testing. diff --git a/README.adoc b/README.adoc index 059047e..c172f5c 100644 --- a/README.adoc +++ b/README.adoc @@ -1,5 +1,5 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 -= VCL-ut (VeriSim Consonance Language) += VCL-UT (VeriSim Consonance Language, Usage-Tracked) Jonathan D.A. Jewell :spdx: MPL-2.0 :status: Pre-Alpha @@ -8,27 +8,50 @@ Jonathan D.A. Jewell image:https://zenodo.org/badge/DOI/10.5281/zenodo.19329501.svg[DOI,link="https://doi.org/10.5281/zenodo.19329501"] image:https://img.shields.io/badge/believe__me-0-brightgreen[believe_me: 0] -image:https://img.shields.io/badge/tests-102_pass-brightgreen[tests: 102 pass] +image:https://img.shields.io/badge/tests-150_pass-brightgreen[tests: 150 pass] image:https://img.shields.io/badge/OpenSSF-Best_Practices-green?logo=opensourcesecurity[OpenSSF Best Practices,link="https://www.bestpractices.dev/en/projects/new?repo_url=https://github.com/hyperpolymath/vcl-ut"] IMPORTANT: This project was renamed on 2026-04-05. Its former name used the letter sequence "V-Q-L-hyphen-U-T" (read: "vee-queue-ell-you-tee") and -stood for "Ultimate Type-safe". The canonical name is now **VCL-total** -(VeriSim Consonance Language — Ubiquitous Type-safe). See CHANGELOG.md for -the full rename scope. The GitHub repository URL is unchanged. +stood for "Ultimate Type-safe". The canonical name is now **VCL-UT** — +*VeriSim Consonance Language, Usage-Tracked*. See CHANGELOG.md for the full +rename scope. The GitHub repository URL is unchanged. + +NOTE: Two superseded expansions of "UT" are still in circulation and should +not be used: "Ubiquitous Type-safe" (which appeared in this README) and +"-total". *Usage-Tracked* is canon, and it is the accurate one: the +distinguishing feature of this tier is that resource usage is tracked in the +type system (L9 `LinearSafe`, via QTT). "-total" survives in the crate name +`vcl-total` and the Idris namespace `VclTotal`; renaming those is a separate, +invasive change and is deliberately not bundled here. [.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-total validates whether proposed identity transitions are admissible.** +**VeriSimDB does not merely store records. It maintains identity consonance across modal witnesses and federation boundaries. VCL expresses propositions and epistemic requests over that consonance state. VCL-UT validates whether proposed identity transitions are admissible.** == Overview -VCL-total is the next-generation interaction language for +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 **all 10 levels of type -safety** — the 6 established IO-covered forms and the 4 additional forms -identified through our research. The `-total` suffix denotes totality in -the dependent-type sense: no partial functions, no undefined behaviour at -type level. +in discussion as VeriSimDB), designed to satisfy **eleven levels of type +safety, L0–L10** — the 6 established IO-covered forms, the 4 additional forms +identified through our research, and L10 `EpistemicSafe`, the consonance +level, which is not a query-safety property at all but a *warrant* property. +See link:docs/THE-10-LEVELS-EXPLAINED.adoc[the level walkthrough]. + +[IMPORTANT] +==== +Two honest qualifications, both measured on 2026-07-21: + +* The ladder is *eleven* levels (L0–L10), not ten. Older prose says ten and + numbers them 1–10; the code numbers them 0–10 and the code is canonical, + because those numbers are wire tags. +* Eleven levels are specified and proved; **six are expressible**. The parser + cannot yet populate the clauses that L7–L10 are inferred from, so the + highest level reachable from VCL source text is L6 `CardinalitySafe`. The + gap is fail-closed and disclosed (issue #25) — unsupported clauses are + rejected, never silently ignored — but it is a gap, and closing it is the + top outstanding item on the language surface. +==== The goal is production-worthy VCL that is provably correct at every layer, from parse to execution. At minimum, this repo serves as a research @@ -41,9 +64,9 @@ queries against a passive store. Operations split into propositional "Query language" is therefore a misnomer; "consonance language" names the actual thing. -== VCL-total in One Sentence +== VCL-UT in One Sentence -VCL-total is the proof-bearing safety pipeline for VCL, the VeriSim Consonance +VCL-UT is the proof-bearing safety pipeline for VCL, the VeriSim Consonance Language. It checks whether identity transitions proposed to VeriSimDB are well-formed, type-safe, authorised, resource-safe, proof-supported, and _admissible_ before they affect live consonance state. @@ -72,9 +95,9 @@ The surface language may look query-like in places, but the semantics are not "read rows from a passive store": VCL statements propose or inspect changes in an actively maintained identity-consonance system. -== What VCL-total Proves +== What VCL-UT Proves -VCL-total does not prove the entire database is globally correct. It checks +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: @@ -104,7 +127,7 @@ 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-total is the fully-typed validation layer behind +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). @@ -117,7 +140,7 @@ User / system writes VCL VCL parser and binder | v -VCL-total safety pipeline (10 progressive levels) +VCL-UT safety pipeline (11 levels, L0-L10) | v verified transition plan @@ -138,8 +161,8 @@ provenance event, or a federated conflict does not destroy the subject identity. It creates a _typed condition_ requiring inspection, repair, quarantine, retraction, or arbitration. -*VCL-total is not the expert-facing product.* The ordinary production language is -VCL; VCL-total is the proof-bearing substrate that validates VCL statements. It +*VCL-UT is not the expert-facing product.* The ordinary production language is +VCL; VCL-UT is the proof-bearing substrate that validates VCL statements. It may expose expert syntax for proof attachment, but its main role is to make routine VCL safe. @@ -157,7 +180,7 @@ consonance state_. 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-total**. +consonance statements as **VCL-UT**. [source] ---- @@ -165,7 +188,7 @@ TypeLL (type theory core — defines the 10 levels) │ ├──→ PanLL (panel framework type safety) │ - └──→ VCL-total (consonance-statement type safety) + └──→ VCL-UT (consonance-statement type safety) │ └──→ Verisim (8-modal octad consonance engine) ---- @@ -180,7 +203,7 @@ TypeLL (type theory core — defines the 10 levels) | The consonance language | Parser (ReScript) → AST → execution. What users write to propose, inspect, or verify. -| **VCL-total** +| **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 @@ -190,19 +213,19 @@ TypeLL (type theory core — defines the 10 levels) 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-total's L9 (Proof Attachment) and L10 (Cross-Cutting) levels. +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-total levels L9-L10. +clause and validated by VCL-UT levels L9-L10. === Adoption Strategy The type safety story unfolds in three phases: 1. **ReScript evangeliser** proves the concept first — demonstrate the value of these type safety levels in ReScript itself, where the developer community can experience them firsthand -2. Once proven, **VCL-total** and **AffineScript** become the two showcase languages for teaching people the 10 levels of type safety -3. VCL-total handles the database-interaction domain; AffineScript handles general-purpose programming +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 @@ -228,7 +251,7 @@ levels 7-10: [cols="1,2,2"] |=== -| Mechanism | VCL-total Syntax | Idris2 Encoding +| 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 @@ -288,7 +311,7 @@ levels 7-10: == Roadmap === Phase 1 — Foundation (Levels 1-3) -- [ ] VCL-total grammar specification (EBNF, extending VCL v3.0) +- [ ] VCL-UT grammar specification (EBNF, extending VCL v3.0) - [ ] Idris2 parser with totality proof - [ ] Schema representation as dependent types - [ ] Type-compatible operation checker diff --git a/ROADMAP.adoc b/ROADMAP.adoc index 0298ad0..ae67c9d 100644 --- a/ROADMAP.adoc +++ b/ROADMAP.adoc @@ -1,59 +1,146 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 -= VCL-total Roadmap += VCL-UT Roadmap Jonathan D.A. Jewell == Current Status -Pre-Alpha. ABI/FFI skeleton created. 10 type safety levels documented. -Parser work not yet started. +Pre-Alpha, but substantially further along than this file previously claimed. +Everything below was measured on 2026-07-21 rather than asserted. + +[NOTE] +==== +The previous version of this file said *"Parser work not yet started"* and +planned an *Idris2* parser. Both statements were false. A parser exists, is +written in *Rust*, and has 36 green tests; it is gated in CI by +`parse-gate.yml` under a SPARK-grade clippy set (no `unsafe`, `unwrap`, +`expect`, `panic`, indexing or unchecked arithmetic). Level numbering has also +been corrected throughout from 1-10 to the canonical L0-L10 — see +link:docs/THE-10-LEVELS-EXPLAINED.adoc[]. +==== + +What exists, measured: + +[cols="2,3"] +|=== +| Component | State + +| Idris2 proof corpus (`src/core`) +| ~12.4k LOC, `%default total`, zero escape hatches (no `believe_me`, + `postulate`, `assert_total`, `sorry`). Proves subsumption, soundness, + totality and monotonicity over L0-L10. + +| Rust parser (`src/interface/parse`) +| Lexer, parser, wire codec, decider, `vclt-gate` binary. 36 tests green. + Consonance verbs SELECT / INSPECT / VERIFY / ASSERT / DECLARE / RETRACT and + the S2 transitions MERGE / SPLIT / NORMALISE all parse. + +| Root workspace +| Re-export facade over `fmt` + `lint`. 102 tests green. + +| `attest`, `recompute-wasm` +| 9 + 3 tests green. Both had silently stopped compiling before 2026-07-21 + and are now gated by `satellite-crates-gate.yml`. + +| `vclt-gate` seam +| Producer side implemented; Contract v1 frozen + (link:docs/vclt-gate-contract.adoc[]). *Not yet wired on the VeriSimDB + consumer side* — see "Nearest Work" below. + +| Test total +| 150 across all workspace roots. +|=== + +The single most important qualification: *eleven levels are specified and +proved; six are expressible.* `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. + +== 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. +. *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`. +. *Retire the `HEXAD` keyword* once VeriSimDB's default modality context + carries all eight witnesses. The parser accepts both `OCTAD` and `HEXAD` + today for compatibility. == Milestones -=== v0.1.0 — Foundation (Levels 1-3) -* [ ] VCL-total grammar specification (EBNF extending VCL v3.0) -* [ ] Idris2 parser with totality proof -* [ ] Schema representation as dependent types -* [ ] Type-compatible operation checker -* [ ] Zig FFI for query plan emission -* [ ] Basic test suite against VeriSimDB - -=== v0.2.0 — Safety Core (Levels 4-6) -* [ ] Null-tracking through join algebra -* [ ] Injection-proof parameterisation (type-level enforcement) -* [ ] Result-type inference with compile-time guarantees -* [ ] Property-based tests - -=== v0.3.0 — Research Levels (Levels 7-10) -* [ ] Cardinality annotations and inference -* [ ] Effect system (Read/Write/DDL) -* [ ] Temporal type annotations for bi-temporal queries -* [ ] Linear types for connections/transactions (Idris2 QTT) +=== v0.1.0 — Foundation (L0-L2) +* [x] VCL-UT grammar specification (`src/core/Grammar.idr`) +* [x] Total parser with panic-freedom gated in CI (Rust, not Idris2 as + originally planned — the Idris corpus proves, the Rust port re-establishes + independently) +* [x] Schema representation as dependent types (`src/core/Schema.idr`, + `OctadSchema`) +* [x] Type-compatible operation checker +* [ ] Zig FFI for transition-plan emission +* [x] Test suite (150 tests) + +=== v0.2.0 — Safety Core (L3-L5) +* [x] Null-tracking through join algebra +* [x] Injection-proof parameterisation (type-level enforcement) +* [x] Result-type inference with compile-time guarantees +* [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* * [ ] Integrate TypeQL-Experimental mechanisms -=== v0.4.0 — VCL-DT Supersession -* [ ] All 6 VCL-DT PROOF types expressible in VCL-total -* [ ] Migration guide from VCL-DT to VCL-total -* [ ] Benchmark: VCL-total overhead vs VCL-DT overhead +=== v0.4.0 — Consonance Level (L10) +* [x] `L10_EpistemicSafe` certificate and shared decider +* [x] S2 transitions MERGE / SPLIT / NORMALISE, with NORMALISE fail-closed + without an explicit justification +* [ ] Surface syntax for epistemic clauses +* [ ] Transitive `ENTAILS`-cycle detection +* [ ] Proposition well-typedness against the schema + +=== v0.5.0 — VCL-DT Supersession +* [ ] All 6 VCL-DT PROOF types expressible in VCL-UT +* [ ] Migration guide from VCL-DT to VCL-UT +* [ ] Benchmark: VCL-UT overhead vs VCL-DT overhead === v1.0.0 — Production Release * [ ] Performance benchmarks against raw SQL -* [ ] VeriSimDB 6-modal query planner integration +* [ ] VeriSimDB octad transition planner integration * [ ] ReScript client SDK with type generation * [ ] Documentation and specification publishing == Dependencies -* **ReScript evangeliser** must prove concept first — VCL-total and AffineScript - are the two showcase languages that follow -* **TypeLL** type theory must stabilise for levels 7-10 -* **VeriSimDB** query router must support VCL-total as a third path alongside - Slipstream (VCL) and VCL-DT +* **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. == Future Directions Once v1.0.0 ships: -* Federation support (VCL-total queries across federated VeriSimDB instances) -* VCL-total as LSP language server for IDE integration -* Formal security audit of injection-proof guarantees (level 5) -* Academic publication of the 10-level type safety framework +* Federation support (VCL-UT statements across federated VeriSimDB instances) +* VCL-UT LSP language server for IDE integration +* Formal security audit of the injection-proof guarantee (L4) +* Academic publication — reframed around *consonance languages as a class* + rather than a decalogue of query safety. The eleventh level is the reason: + `EpistemicSafe` is not a query-safety property, and a paper titled after ten + of them cannot house it. diff --git a/docs/2026-07-21-workup-consonance-and-verisim.adoc b/docs/2026-07-21-workup-consonance-and-verisim.adoc new file mode 100644 index 0000000..db6abcf --- /dev/null +++ b/docs/2026-07-21-workup-consonance-and-verisim.adoc @@ -0,0 +1,507 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + += VCL-UT Work-Up: The Consonance Claim, and the VeriSimDB Application +Jonathan D.A. Jewell +2026-07-21 +:toc: preamble +:icons: font +:sectnums: + +This document does two separate jobs and keeps them separate on purpose. + +*Strand A* is about VCL-UT as a contribution to the world: what a _consonance +language_ is, why it is a distinct class rather than a query language with +extra types, and what gap it fills that nothing currently fills. + +*Strand B* is about VCL-UT as infrastructure for VeriSimDB specifically: what +concrete, tethered value it delivers to one working database, and what has to +be built for that value to be realised. + +They are separated because they have different success conditions. Strand A +succeeds if the claim is novel and defensible. Strand B succeeds if VeriSimDB +is measurably safer. Neither implies the other, and conflating them is how a +research vehicle ends up serving nobody. + +Everything factual here was measured on 2026-07-21 against the working tree. +Where something is owed rather than done, it says so. + +== Executive Summary + +. *The strongest evidence for the consonance reframe came from the code, not + from taste.* The ladder has eleven levels, not ten. The eleventh, + `EpistemicSafe`, is not a query-safety property — it is a property about + whether the engine is _entitled to believe_ an answer. The whitepaper is + titled "A Decalogue of Database Query Safety". Its own title cannot house + its own eleventh level. That is a structural argument for reframing, not an + aesthetic one. + +. *The gap in the world is not "safer queries".* That field is crowded and + well served. The gap is that every existing type-safe query language + assumes _one witness_. When a system maintains several modal witnesses that + can disagree, well-typedness stops being sufficient: a result can be + perfectly typed and still unwarranted. No language in the field types that + distinction. VCL-UT does, at L10. + +. *The most valuable single piece of work outstanding is surface syntax for + L7-L10.* Eleven levels are specified and proved; six are expressible. + Measured: the highest level reachable from VCL source text is L6. + +. *The second most valuable is wiring the `vclt-gate` seam.* Contract v1 is + frozen and the producer works. VeriSimDB does not call it. Until it does, + VCL-UT proves things about statements VeriSimDB never asks about. + +. *There is a small, precisely-located bug worth fixing immediately in + VeriSimDB:* `src/vcl/VCLTypeChecker.res:60` builds the default type context + with six modalities. The type admits eight. Provenance and Spatial are + silently absent from every default type-check. + +== Ground Truth, Measured + +Recorded so that later strategy arguments rest on facts rather than memory. + +[cols="3,2"] +|=== +| Claim | Status 2026-07-21 + +| Idris2 corpus, `%default total`, zero escape hatches +| TRUE. No `believe_me` / `postulate` / `assert_total` / `sorry`. + +| Level ladder is L0-L10, eleven levels +| TRUE in `ast.rs` and `Levels.idr`. All prose said ten, numbered 1-10, until + corrected today. + +| L10 `EpistemicSafe` documented anywhere +| WAS FALSE. Appeared in no document in the repository. Now documented. + +| Consonance verbs parse +| TRUE. SELECT / INSPECT / VERIFY / ASSERT / DECLARE / RETRACT, plus the S2 + transitions MERGE / SPLIT / NORMALISE. + +| Documented verbs `FETCH` / `REMOVE` parse +| FALSE. Rejected outright: "expected keyword SELECT". 22 occurrences, now + corrected. + +| L7-L10 reachable from source text +| FALSE. Ceiling is L6. `parse_statement` fixes the five clause fields at + `None`; `infer_requested_level` awards L7-L10 on exactly those fields. + +| `vclt-gate` invoked by VeriSimDB +| FALSE. Zero references in `rust-core/verisim-api/src/vcl.rs`. + +| VeriSimDB default type context carries the octad +| FALSE. Six of eight. `VCLTypeChecker.res:60`. + +| Test count +| 150 across five workspace roots (102 + 36 + 9 + 3). + +| Two crates compiled +| WAS FALSE. `attest` and `recompute-wasm` had silently stopped compiling. + Fixed and gated today. +|=== + +// ============================================================================ += Strand A — The Theoretical Claim +// ============================================================================ + +== What a Consonance Language Is + +A query language addresses a store. The store is passive: it holds what was +put in it, and a query is a request to read some of it back. The store has one +witness — itself — and it cannot disagree with itself. Correctness of a query +is therefore exhausted by well-formedness plus faithfulness of execution. + +A consonance language addresses an _engine_ that maintains identity claims +across several modal witnesses simultaneously — in VeriSimDB's case eight: +graph, vector, tensor, semantic, document, temporal, provenance, spatial. +Those witnesses are independently maintained and can drift apart. The engine's +job is not storage; it is keeping them _consonant_. + +Three consequences follow, and together they are what make this a class rather +than a dialect. + +*1. Statements are propositions, not requests.* `DECLARE`, `ASSERT`, `RETRACT` +propose changes to identity state. `INSPECT` and `VERIFY` are epistemic +requests — they ask what the engine knows and on what warrant. `MERGE`, +`SPLIT`, `NORMALISE` are consonance transitions: they do not return a result +set at all, which is precisely why the implementation could not model them as +statements and introduced a separate `Transition` type summed into `VclOp`. +That structural split in the AST is the class distinction showing up in code. + +*2. Retraction is not deletion, and drift is not death.* A retracted claim +usually remains visible to provenance, audit and federation. A drifted witness +creates a _typed condition_ requiring inspection, repair, quarantine or +arbitration — not an error. A query language has no vocabulary for either, +because a passive store has nothing to be inconsistent with. + +*3. Well-typedness stops being sufficient.* This is the load-bearing one, and +it is developed next. + +== The Gap in the World + +The honest version of the competitive picture: + +Type-safe query languages are a *crowded and mature* field. LINQ, Quill, Slick, +Diesel, jOOQ, sqlx, TypeQL, EdgeQL and PostgREST between them cover schema +binding, type-compatible operations, null tracking, injection resistance and +result typing. Effect systems, temporal types, linear/session types and +cardinality inference all have substantial literature. A paper claiming +"ten levels of query safety" enters that field as an unusually thorough +_synthesis_ — genuinely useful, genuinely not novel. Reviewers will say so. + +Here is what none of them do. + +Every one of those systems assumes a single source of truth. Their type +systems answer *"is this query well-formed against the schema?"* They cannot +answer *"is the system entitled to this answer?"* because in their world the +question does not arise: there is one witness, and it cannot disagree with +itself. + +The moment a system maintains multiple modal witnesses that can drift, a new +failure mode appears that is invisible to all ten of the safety levels: + +[quote] +____ +Every step was well-typed. The schema bound. The types were compatible. Nulls +were handled. Nothing was injected. The result type was known, the cardinality +right, the effects declared, the freshness bounded, the resources balanced. + +And the answer is still unwarranted — because the graph witness and the +document witness disagreed, and the engine silently preferred one. +____ + +That is not a safety bug. It is a *warrant* bug. Safety properties rule out +executions that go wrong. Warrant properties rule out answers a system is not +entitled to give, even when every step was correct. + +*The gap: there is no type system for warrant in data systems.* Epistemic and +doxastic logics have modelled knowledge and belief formally since Hintikka. +Multi-agent epistemic logic has `Knows`, `Believes`, common knowledge and +entailment between agents. Provenance research (PROV-O, why/where/how +provenance) tracks derivation. Truth-maintenance systems and belief revision +(AGM) handle retraction. But these live in reasoners, audit layers and +metadata — *beside* the query path, consulted after the fact, if at all. None +of them is a type in the language you write your statement in. None can refuse +your statement at compile time. + +VCL-UT's L10 puts that structure into the type system of the statement +language itself, where it can fail closed before execution. + +== Why the Eleventh Level Is the Argument + +L10's certificate `L10_EpistemicSafe` is witnessed by +`Decide.epistemicConsistentStmt`, which requires: an epistemic clause; at +least one declared agent; every requirement-referenced agent declared; and *no +direct `ENTAILS` cycle*. + +The fourth condition is the interesting one. A mutual entailment — `a ⊨ b` and +`b ⊨ a` — is a citation loop: two witnesses each grounding their warrant in +the other, with nothing outside the pair supporting either. It is exactly how +a federation manufactures false confidence, and it is invisible to every lower +level, because each individual statement is impeccably typed. + +Note also the asymmetry with TypeLL. Levels L0-L9 are inherited from TypeLL, +the shared core type theory, and PanLL applies the same ten to UI panels. L10 +is *not* inherited. A UI panel has no federation of disagreeing witnesses and +therefore no warrant question to answer. L10 originates in this domain — the +first level the application contributed back to the theory rather than +receiving from it. A framework whose eleventh member does not fit its own +name is telling you the name is wrong. + +=== Disclosed residuals + +Stated plainly, because a level that overstates itself is worse than no level: + +* Only the *direct* two-party `ENTAILS` cycle is detected. A three-party loop + (`a ⊨ b`, `b ⊨ c`, `c ⊨ a`) passes today. +* The proposition carried by a requirement is not checked against the schema. + +Both are recorded as owed in `verification/proofs/VERIFICATION-STANCE.adoc`. +The Idris checker and the Rust decider agree exactly +(`Checker.checkLevel10Sound`); what they agree on is a partial condition. + +== Proposal: Reframing the Whitepaper + +NOTE: This section is a *proposal*, not an executed rewrite. The direction — +reframe to consonance — is settled. How a paper argues its claim is the +author's call, and it is the least testable, highest-blast-radius change in +this work-up. The structure below is offered for approval before the 1,909-line +`.tex` is restructured. + +Current: `docs/whitepapers/arcvix-10-level-query-safety.tex`, "A Decalogue of +Database Query Safety", cs.PL / cs.DB. + +Three problems with the present framing: + +. *"Decalogue" is now false.* There are eleven levels. +. *"Query safety" is a crowded field.* The decalogue is a synthesis, and will + be read as one. +. *The eleventh level does not fit the title*, and it is the novel one. + +=== Proposed structure + +[cols="1,4"] +|=== +| Section | Content + +| 1. Introduction +| Lead with the warrant failure, not the level count. Open on a concrete + scenario: a well-typed statement returning an unwarranted answer because two + modal witnesses disagreed. Establish that no existing type system can refuse + it. + +| 2. Consonance Languages +| Define the class. Statements as propositions and epistemic requests; + transitions that return nothing; retraction ≠ deletion; drift as a typed + condition. The `Statement` / `Transition` / `VclOp` split as evidence that + the distinction is structural, not stylistic. + +| 3. Related Work — honest positioning +| Concede the crowded field explicitly. LINQ / Quill / Diesel / jOOQ / TypeQL + / EdgeQL for L0-L5; effect, temporal, linear and session type literature for + L6-L9. Then the gap: epistemic logic, provenance, truth maintenance all + exist, but *beside* the query path, never as a type that can refuse a + statement. + +| 4. The Safety Ladder L0-L9 +| The technical core, retained essentially as-is. Reframed as *the + well-formedness ladder* — necessary, not sufficient, and explicitly not the + paper's novelty claim. + +| 5. Warrant: the Epistemic Level +| The contribution. Agents, the four `EpistemicRequirement` forms, the + consistency decider, the cycle condition. Why warrant is not safety. The + TypeLL asymmetry as evidence. + +| 6. Formal Properties +| Subsumption, soundness, totality, monotonicity — as now. Plus the honest + statement of the two disclosed residuals. + +| 7. Implementation +| Idris2 corpus with zero escape hatches; independent Rust re-establishment; + the `vclt-gate` seam. Include the *measured* expressibility gap. A paper + that discloses that eleven levels are proved and six expressible is more + credible, not less. + +| 8. Evaluation / Conclusion +| The claim to defend: consonance languages are a distinct class, and warrant + is a type-level property that class requires. +|=== + +=== Draft abstract, for approval + +[quote] +____ +Type-safe query languages have made large gains against a well-understood +family of defects: malformed syntax, unbound schema references, incompatible +operations, unhandled nulls, injection, untyped results, and more recently +cardinality, effects, time and resource usage. Every such system, however, +shares an assumption so basic it is rarely stated: that there is one source of +truth, and it cannot disagree with itself. + +Systems that maintain identity across multiple modal witnesses violate that +assumption by construction. In such systems a statement can satisfy every +safety property in the literature and still yield an answer the system is not +entitled to give, because independently-maintained witnesses disagreed and the +disagreement was resolved silently. This is not a safety failure — no +execution went wrong — but a failure of _warrant_. + +We introduce *consonance languages*: languages whose statements are +propositions and epistemic requests addressed to an engine that maintains +consonance, rather than queries addressed to a passive store. We present +VCL-UT, a consonance language with a cumulative eleven-level type-safety +ladder, mechanised in Idris2 with no escape hatches. The first ten levels +formalise the well-formedness properties above. The eleventh, *epistemic +safety*, is of a different kind: it types the conditions under which an answer +is warranted — that consulted agents are declared, that requirements reference +only declared agents, and that no agent's warrant is circular. + +We show that epistemic safety is not derivable from the other ten, that it +does not arise in single-witness systems, and that it is not inherited from +the shared core type theory the other ten come from but originates in the +consonance domain. We report an implementation, an independently-re-established +decision procedure, and — because a safety claim should not exceed what is +proved — the specific obligations that remain owed. +____ + +// ============================================================================ += Strand B — The VeriSimDB Application +// ============================================================================ + +Strand A argues the class is worth defining. This strand is narrower and more +demanding: what does VCL-UT do for *this* database, concretely, and what has +to exist for that to be true? + +== The Honest Current Position + +VCL-UT delivers, today, *nothing* to VeriSimDB at runtime. + +Not because the work is bad — the proof corpus is real, the parser is real and +gated, the gate binary exists and Contract v1 is frozen — but because the seam +is only built on one side. `rust-core/verisim-api/src/vcl.rs` contains zero +references to `vclt-gate`. VeriSimDB has its own ReScript checker and uses it. + +That is the whole applied problem in one sentence: *the producer is finished +and the consumer was never written.* + +== The Architecture That Was Chosen, and Why It Is Right + +`docs/vclt-gate-contract.adoc` freezes Contract v1: `vclt-gate` is a CLI +subprocess speaking a JSON-line protocol. Producer is this repository; +consumer is VeriSimDB. + +This deserves defending because it looks unfashionable. It was chosen over FFI +to avoid coupling VeriSimDB's build to this repository's workspace — and the +evidence that this was correct is in this very repository: `src/interface` +carries an external path-dependency on a sibling `echidna` checkout, which is +exactly why it is excluded from the root workspace and why `echidna-client` +cannot be covered by Dependabot. A subprocess seam has none of that. It also +means a VeriSimDB deployment can upgrade its gate independently, and that gate +failures are isolated rather than in-process. + +The gate is also correctly scoped: it computes `decider::certified_level(stmt, +schema)` and explicitly does *not* verify PROOF clauses or touch live state. It +is a static admissibility check, not an execution path. + +== What VeriSimDB Actually Gets + +Four things, in descending order of concreteness. + +=== 1. A fail-closed admissibility check before statements touch consonance state + +The immediate value. Every VCL statement gets a certified level *before* +execution, computed by a decision procedure that was proved sound in Idris2 and +re-established independently in Rust. VeriSimDB can then set a floor — refuse +anything below L4 `InjectionProof` on a public endpoint, require L6 +`CardinalitySafe` for anything that feeds a UI list — and enforce it uniformly. + +Today that policy cannot be expressed at all, because nothing computes the +level. + +=== 2. One level ladder instead of two divergent ones + +Right now there are two independent implementations of VCL type checking: the +Idris/Rust corpus here, and ~4,974 LOC of ReScript in VeriSimDB +(`VCLBidir.res`, `VCLSubtyping.res`, `VCLProofObligation.res`, `VCLTypes.res`, +`VCLTypeChecker.res`). Two implementations of the same semantics will drift; +the divergences already found are evidence that they have. + +Per the settled decision, *vcl-ut is the source of truth*. The migration path +that preserves VeriSimDB's genuinely good UX work: + +* *Keep* the ReScript surface parser, error rendering and editor integration. + These are user-facing and better done close to the client. +* *Replace* the ReScript checker's verdict with the gate's. `VCLTypeChecker.res` + is already a thin facade, which makes it the right seam. +* *Retain* `VCLSubtyping.res` rule 6 (refinement subsumption, deferred pending + SMT) as a VeriSimDB-local extension until the corpus covers it. + +=== 3. Attestation + +`src/interface/attest` mints a signed attestation over `(statement, schema)` +carrying the certified level, verifiable independently. For a database whose +selling point is maintained identity consonance, being able to prove *after +the fact* that a transition was admitted at a stated level — and have a third +party verify it without trusting the engine — is a distinguishing capability, +not a nicety. This crate is 9 tests and was, until today, not compiling. + +=== 4. Vocabulary discipline + +`README.adoc`'s terminology guidance ("prefer consonance language, statement, +transition, modal witness, octad; avoid query, record, CRUD, delete, 6-modal +engine, passive store") is the class distinction made operational. The cost of +letting it slip is visible right now, in the next section. + +== Concrete Defects Found in VeriSimDB + +Both located precisely, both small. + +=== The default type context carries six modalities, not eight + +`src/vcl/VCLTypeChecker.res:60`: + +[source] +---- +availableModalities: [Graph, Vector, Tensor, Semantic, Document, Temporal], +---- + +`VCLTypes.res` defines all eight modality variants, up to `SpatialModality`. +The type admits the octad; the default context omits *Provenance* and +*Spatial*. Every type-check performed against a default context therefore +treats two of the eight witnesses as unavailable. + +This is a partial migration, not an oversight in isolation: the type is still +named `HexadType` throughout (`VCLTypes.res:50`, `:206`, `:270`, +`VCLSubtyping.res:101`). The hexad-to-octad migration reached the variants and +stopped before the defaults and the names. + +Note the same legacy is visible here: the parser still accepts `HEXAD` +alongside `OCTAD`. That is deliberate compatibility, and it should be retired +once VeriSimDB's default context carries all eight — not before. + +=== The seam is unwired + +Covered above. It is the single highest-value applied change. + +== Sequenced Plan + +Ordered by value delivered per unit of risk. Items 1-2 are in this repository; +3-5 are in VeriSimDB and cannot be committed from here. + +[cols="1,3,2"] +|=== +| # | Work | Where + +| 1 +| *Surface syntax for L7-L10.* Extend the parser to populate `effect_decl`, + `version_const`, `linear_annot`, `proof_clause` and `epistemic_clause`. + Until this lands, four rungs including the entire consonance level are + unreachable from source text and the ladder's top half is theoretical. + Tracked in #25. +| vcl-ut + +| 2 +| *Discharge the two L10 residuals* — transitive `ENTAILS`-cycle detection and + proposition well-typedness. These are what stand between "L10 exists" and + "L10 means what it says". +| vcl-ut + +| 3 +| *Fix the six-modality default context* (`VCLTypeChecker.res:60`). One line, + and it silently weakens every default type-check today. +| verisimdb + +| 4 +| *Wire `vclt-gate` into the execute path.* Invoke the gate from + `rust-core/verisim-api/src/vcl.rs`, adopt its verdict, enforce a configurable + minimum level. Contract v1 is frozen, so this is integration, not design. +| verisimdb + +| 5 +| *Converge the checkers.* Once (4) is live, retire the ReScript checker's + independent verdict in favour of the gate's, keeping the ReScript surface + parser and diagnostics. Then rename `HexadType` and retire the `HEXAD` + keyword together. +| both + +| 6 +| *Restructure the whitepaper* per the Strand A proposal — after approval. +| vcl-ut +|=== + +== What Would Falsify This + +Recorded so the plan can be argued with rather than assumed. + +* *If VeriSimDB's ReScript checker is materially more capable than the + corpus*, then "vcl-ut is source of truth" costs capability. The known + candidate is `VCLSubtyping.res` rule 6 (refinement subsumption). The + mitigation above — retain it as a local extension — assumes it is the only + one. That assumption has not been exhaustively checked. +* *If subprocess latency per statement is material* on VeriSimDB's hot path, + the CLI seam is wrong and the FFI coupling cost has to be paid after all. + This has not been measured. It should be, before item 4 rather than after. +* *If the consonance-language claim has prior art* under another name — + belief-revision query languages, epistemic database logics — Strand A + weakens to a synthesis claim and the paper should be positioned accordingly. + The search behind Section "The Gap in the World" was not exhaustive. diff --git a/docs/THE-10-LEVELS-EXPLAINED.adoc b/docs/THE-10-LEVELS-EXPLAINED.adoc index 3d5bc3f..47eec8a 100644 --- a/docs/THE-10-LEVELS-EXPLAINED.adoc +++ b/docs/THE-10-LEVELS-EXPLAINED.adoc @@ -1,15 +1,37 @@ // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -= The 10 Levels of Type Safety -- Explained += The Levels of Type Safety -- Explained Jonathan D.A. Jewell :toc: preamble :icons: font :sectnums: -This document is a detailed walkthrough of all 10 type safety levels in VCL-total. +This document is a detailed walkthrough of the type safety levels in VCL-UT. Each level builds on the previous -- you cannot skip ahead. The foundations -(levels 1-3) must be solid before the higher levels make sense. +(levels 0-2) must be solid before the higher levels make sense. + +[IMPORTANT] +.Numbering was corrected on 2026-07-21 -- read this before citing a level +==== +This document previously numbered the levels *1-10*. The implementation +numbers them *0-10*, and the implementation is canonical: the numbers are wire +tags, not prose. `SafetyLevel` in `src/interface/parse/src/ast.rs` and +`src/core/Levels.idr` both run `ParseSafe = 0` through `EpistemicSafe = 10`, +and `safetyLevelToInt` serialises exactly those values across the +`vclt-gate` boundary. + +Under the old numbering a reader who requested level 7 expecting Cardinality +Safety would have received Effect-Tracking instead. Every heading, table and +diagram below has been shifted down by one to match. + +There are therefore *eleven* levels, L0-L10, not ten. The eleventh, +`EpistemicSafe`, arrived with the consonance turn and had never been +documented anywhere. It is described in its own section below. + +Mapping from the old numbering: *old level N is new level N-1*, and there is +no old level corresponding to L10. +==== == How the Levels Stack @@ -18,87 +40,98 @@ floor without the second, and you cannot build the second without the first. ---- ┌─────────────────────────────────────────────┐ -│ Level 10: Linearity Safety │ ← Research -│ Level 9: Temporal Safety │ ← Research -│ Level 8: Effect-Tracking Safety │ ← Research -│ Level 7: Cardinality Safety │ ← Research +│ Level 10: Epistemic Safety │ ← Consonance ├─────────────────────────────────────────────┤ -│ Level 6: Result-Type Safety │ ← Established -│ Level 5: Injection-Proof Safety │ ← Established -│ Level 4: Null Safety │ ← Established -│ Level 3: Type-Compatible Operations │ ← Established -│ Level 2: Schema-Binding Safety │ ← Established -│ Level 1: Parse-Time Safety │ ← Established +│ Level 9: Linearity Safety │ ← Research +│ Level 8: Temporal Safety │ ← Research +│ Level 7: Effect-Tracking Safety │ ← Research +│ Level 6: Cardinality Safety │ ← Research ├─────────────────────────────────────────────┤ -│ Level 0: No type safety (raw strings) │ ← The danger zone +│ Level 5: Result-Type Safety │ ← Established +│ Level 4: Injection-Proof Safety │ ← Established +│ Level 3: Null Safety │ ← Established +│ Level 2: Type-Compatible Operations │ ← Established +│ Level 1: Schema-Binding Safety │ ← Established +│ Level 0: Parse-Time Safety │ ← Established +├─────────────────────────────────────────────┤ +│ (no level): raw strings │ ← The danger zone └─────────────────────────────────────────────┘ ---- -**Levels 1-6** are well-established in the academic literature and implemented +**Levels 0-5** are well-established in the academic literature and implemented in various real-world systems (though rarely all six together). -**Levels 7-10** are additional protections identified through our research. -They address real failure modes that levels 1-6 leave uncovered. These levels +**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. +**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. + == The Progression at a Glance [cols="1,2,2,2"] |=== | Level | What It Checks | When It Checks | What Happens Without It -| 1 -- Parse +| 0 -- Parse | Is the query well-formed? | Parse time (before anything else) | Garbage reaches the database -| 2 -- Schema +| 1 -- Schema | Do referenced tables and columns exist? | Compile time (against live schema) | Queries silently return nothing -| 3 -- Type ops +| 2 -- Type ops | Are operations applied to compatible types? | Compile time | Nonsense computations (date + colour) -| 4 -- Null +| 3 -- Null | Are nullable values handled explicitly? | Compile time | Silent blanks in results -| 5 -- Injection +| 4 -- Injection | Is user input separated from query structure? | Compile time (by construction) | Attackers run arbitrary commands -| 6 -- Result +| 5 -- Result | Is the return type known? | Compile time | Runtime crashes on unexpected data shapes -| 7 -- Cardinality +| 6 -- Cardinality | How many results will the query return? | Compile time | Code assumes one row, gets zero or thousands -| 8 -- Effects +| 7 -- Effects | Does this query read, write, or modify structure? | Compile time | Read-only functions accidentally delete data -| 9 -- Temporal +| 8 -- Temporal | Is the data fresh enough for the intended use? | Compile time (bounds in types) | Stale data treated as current -| 10 -- Linearity +| 9 -- Linearity | Are resources used exactly once? | Compile time (via QTT) | Connection leaks, use-after-close |=== -== Level 1: Parse-Time Safety +== Level 0: Parse-Time Safety === What It Checks @@ -121,8 +154,8 @@ Input: "SELCT users WHERE id = 1" ^^^^^ Parser: Error at position 0: Unknown keyword "SELCT". Did you mean "SELECT"? -Input: "FETCH users WHERE id = 1" -Parser: OK → AST { kind: Fetch, target: "users", filter: Eq("id", 1) } +Input: "SELECT users WHERE id = 1" +Parser: OK → AST { kind: Select, target: "users", filter: Eq("id", 1) } ---- === What You Lose Without It @@ -133,7 +166,7 @@ silently ignore the error, some execute a partial query. --- -== Level 2: Schema-Binding Safety +== Level 1: Schema-Binding Safety === What It Checks @@ -159,7 +192,7 @@ Schema "mydb" has: email : Text (nullable) age : Int (nullable) -Query: FETCH users.emial WHERE users.id = ?id +Query: SELECT users.emial WHERE users.id = ?id ^^^^^ Schema Binder: Error: "emial" is not a column in "users". Available columns: id, name, email, age. @@ -174,7 +207,7 @@ systems. --- -== Level 3: Type-Compatible Operations +== Level 2: Type-Compatible Operations === What It Checks @@ -192,11 +225,11 @@ The type checker (Idris2) verifies that operators receive arguments of the correct types: ---- -Query: FETCH users WHERE users.name > 42 +Query: SELECT users WHERE users.name > 42 Type Checker: Error: operator (>) expects compatible types, but got Text > Int. Cannot compare Text with Int. -Query: FETCH users WHERE users.age > 42 +Query: SELECT users WHERE users.age > 42 Type Checker: OK. Int > Int is valid. ---- @@ -213,7 +246,7 @@ _undefined_. --- -== Level 4: Null Safety +== Level 3: Null Safety === What It Checks @@ -231,12 +264,12 @@ propagated through joins, subqueries, and projections. ---- Schema: users.email is Nullable -Query: FETCH UPPER(users.email) FROM users +Query: SELECT UPPER(users.email) FROM users Type Checker: Error: UPPER expects Text, but users.email is Nullable. Use COALESCE(users.email, "unknown") to provide a default, or add WHERE users.email IS NOT NULL to narrow the type. -Query: FETCH UPPER(COALESCE(users.email, "N/A")) FROM users +Query: SELECT UPPER(COALESCE(users.email, "N/A")) FROM users Type Checker: OK. COALESCE returns Text (non-null guaranteed). ---- @@ -257,7 +290,7 @@ but violate every reasonable expectation. --- -== Level 5: Injection-Proof Safety +== Level 4: Injection-Proof Safety === What It Checks @@ -275,7 +308,7 @@ path that could produce a query. ---- -- VCL-total query with typed parameter -FETCH users WHERE users.id = ?id +SELECT users WHERE users.id = ?id -- ?id has type Param. It is not a string. -- The only way to fill ?id is to provide a UserId value. @@ -293,7 +326,7 @@ Injection attacks. The #1 web application security risk for over a decade. --- -== Level 6: Result-Type Safety +== Level 5: Result-Type Safety === What It Checks @@ -309,7 +342,7 @@ and makes it available to the calling code. === How VCL-total Implements It ---- -Query: FETCH users.name, users.age WHERE users.active = true +Query: SELECT users.name, users.age WHERE users.active = true Result Type (inferred at compile time): List<{ name : Text, age : Nullable }> @@ -328,7 +361,7 @@ when the code is compiled. --- -== Level 7: Cardinality Safety +== Level 6: Cardinality Safety === What It Checks @@ -352,24 +385,24 @@ This level uses the **TypeQL-Experimental** extension mechanisms: |=== | VCL-total Syntax | Meaning -| `FETCH UNIQUE ...` +| `SELECT UNIQUE ...` | Returns `ExactlyOne` -- compile error if uniqueness cannot be proved -| `FETCH OPTIONAL ...` +| `SELECT OPTIONAL ...` | Returns `AtMostOne` -- caller must handle the empty case -| `FETCH ...` +| `SELECT ...` | Returns `List` -- zero or more results |=== ---- -- Schema: users.id has UNIQUE constraint -FETCH UNIQUE users WHERE users.id = ?id +SELECT UNIQUE users WHERE users.id = ?id -- Return type: ExactlyOne -- The compiler proves this from the UNIQUE constraint on users.id. -FETCH OPTIONAL users WHERE users.email = ?email +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. @@ -392,7 +425,7 @@ processes only the first of many results, silently ignoring the rest. --- -== Level 8: Effect-Tracking Safety +== Level 7: Effect-Tracking Safety === What It Checks @@ -428,13 +461,13 @@ This level uses the **effect system** extension from TypeQL-Experimental: |=== ---- -FETCH users.name EFFECTS { Read } --- OK: FETCH is a read operation. +SELECT users.name EFFECTS { Read } +-- OK: SELECT is a read operation. -REMOVE users WHERE users.expired = true EFFECTS { Read } --- Compile error: REMOVE requires Write effect, but only Read is permitted. +RETRACT users WHERE users.expired = true EFFECTS { Read } +-- Compile error: RETRACT requires Write effect, but only Read is permitted. -REMOVE users WHERE users.expired = true EFFECTS { Read, Write } +RETRACT users WHERE users.expired = true EFFECTS { Read, Write } -- OK: Write effect is available. ---- @@ -457,7 +490,7 @@ triggers a write. An analytics query modifies production data. --- -== Level 9: Temporal Safety +== Level 8: Temporal Safety === What It Checks @@ -496,14 +529,14 @@ TypeQL-Experimental: |=== ---- -FETCH stocks.price +SELECT stocks.price WHERE stocks.ticker = "FTSE100" AS OF NOW - 5 SECONDS -- Return type: Temporal> -- If the most recent data is older than 5 seconds, the query fails -- rather than returning stale data. -FETCH orders.status +SELECT orders.status WHERE orders.id = ?id BETWEEN "2026-01-01" AND "2026-01-31" -- Return type: List>> @@ -528,7 +561,7 @@ list instead of the current one. --- -== Level 10: Linearity Safety +== Level 9: Linearity Safety === What It Checks @@ -567,8 +600,8 @@ TypeQL-Experimental: ---- OPEN CONNECTION conn - FETCH users USING conn - FETCH orders USING conn + SELECT users USING conn + SELECT orders USING conn CLOSE conn -- conn is linear (quantity 1 in QTT terms). -- After CLOSE, conn does not exist. Using it is a compile error. @@ -621,6 +654,110 @@ Connection leaks exhaust the connection pool. Use-after-close corrupts data. Double-commits create duplicate transactions. Forgotten rollbacks leave locks 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. + +=== What It Checks + +An epistemic clause names the agents whose knowledge is in play, and states +the requirements that must hold among them. `EpistemicRequirement` has four +forms (`ast.rs`, mirroring `Grammar.idr`): + +[cols="1,3"] +|=== +| Form | Meaning + +| `Knows(agent, p)` +| The agent's knowledge of `p` is factive -- it is warranted and `p` holds. + +| `Believes(agent, p)` +| The agent holds `p`, without the claim that `p` is true. + +| `Common(p)` +| `p` is common knowledge across all declared agents. + +| `Entails(a, b, p)` +| Agent `a`'s warrant for `p` derives from agent `b`'s. +|=== + +The 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. + +=== Disclosed Residual -- Read This + +Two obligations are *owed, not discharged*, and are recorded as such in +`verification/proofs/VERIFICATION-STANCE.adoc`: + +* **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. + +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. + +=== Implementation Status -- No Surface Syntax Yet + +[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 +|=== + +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. + +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.* +==== + == How TypeLL Provides the Foundation All 10 levels are defined in **TypeLL**, the core type theory. VCL-total @@ -629,56 +766,78 @@ _inherits_ these levels rather than inventing them. This means: ---- TypeLL (core type theory) │ - │ Defines: 10 levels of type safety as formal constructs + │ Defines: the levels of type safety as formal constructs │ ├──→ PanLL (panel framework) - │ Uses levels 1-10 for UI component safety + │ Uses L0-L9 for UI component safety │ - └──→ VCL-total (database queries) - Uses levels 1-10 for query safety + └──→ VCL-UT (consonance statements) + Uses L0-L9 for statement safety, and adds L10 ---- The same mathematical proofs that ensure a PanLL UI panel cannot render invalid -state also ensure a VCL-total query cannot execute an invalid operation. The +state also ensure a VCL-UT statement cannot execute an invalid operation. The theory is shared; only the application domain differs. +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. + == Summary: What Each Level Prevents [cols="1,3"] |=== | Level | Category of Bug Eliminated -| 1 -- Parse +| 0 -- Parse | Malformed queries, syntax errors reaching the database -| 2 -- Schema +| 1 -- Schema | References to non-existent tables, columns, or relationships -| 3 -- Type ops +| 2 -- Type ops | Nonsense operations (adding a name to a date) -| 4 -- Null +| 3 -- Null | Null pointer exceptions, silent blanks in results -| 5 -- Injection +| 4 -- Injection | SQL/VCL injection attacks -- the #1 web security risk -| 6 -- Result +| 5 -- Result | Runtime type mismatches when processing query results -| 7 -- Cardinality +| 6 -- Cardinality | Wrong assumptions about how many results a query returns -| 8 -- Effects +| 7 -- Effects | Accidental data modification by read-only code -| 9 -- Temporal +| 8 -- Temporal | Stale data treated as current, mixed time contexts -| 10 -- Linearity +| 9 -- Linearity | Connection leaks, use-after-close, double-commit + +| 10 -- Epistemic +| Unwarranted answers: disagreeing modal witnesses silently reconciled, + circular warrant, an authority answering outside its competence |=== -Together, these 10 levels cover the vast majority of database-related bugs -that have caused real-world catastrophes. The goal of VCL-total is to eliminate -all of them at compile time, with zero runtime overhead. +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". diff --git a/src/core/Cargo.toml b/src/core/Cargo.toml index 38006a8..df85953 100644 --- a/src/core/Cargo.toml +++ b/src/core/Cargo.toml @@ -5,7 +5,7 @@ version = "0.1.0" edition = "2021" license = "MPL-2.0" authors = ["Jonathan D.A. Jewell "] -repository = "https://github.com/hyperpolymath/vql-ut" +repository = "https://github.com/hyperpolymath/vcl-ut" description = "VCL-total Core: Idris-based type checker and grammar" [lib] diff --git a/src/interface/Cargo.toml b/src/interface/Cargo.toml index 010a7c5..4ff5717 100644 --- a/src/interface/Cargo.toml +++ b/src/interface/Cargo.toml @@ -5,7 +5,7 @@ version = "0.1.0" edition = "2021" license = "MPL-2.0" authors = ["Jonathan D.A. Jewell "] -repository = "https://github.com/hyperpolymath/vql-ut" +repository = "https://github.com/hyperpolymath/vcl-ut" description = "VCL-total Interface: Common interface types" [lib] diff --git a/src/interface/attest/Cargo.lock b/src/interface/attest/Cargo.lock index de35178..c74cdfc 100644 --- a/src/interface/attest/Cargo.lock +++ b/src/interface/attest/Cargo.lock @@ -146,12 +146,24 @@ dependencies = [ "wasi", ] +[[package]] +name = "itoa" +version = "1.0.18" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8f42a60cbdf9a97f5d2305f08a87dc4e09308d1276d28c869c684d7777685682" + [[package]] name = "libc" version = "0.2.186" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "68ab91017fe16c622486840e4c83c9a37afeff978bd239b5293d61ece587de66" +[[package]] +name = "memchr" +version = "2.8.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cf8baf1c55e62ffcace7a9f06f4bd9cd3f0c4beb022d3b367256b91b87513d98" + [[package]] name = "pkcs8" version = "0.10.2" @@ -233,6 +245,19 @@ dependencies = [ "syn", ] +[[package]] +name = "serde_json" +version = "1.0.151" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c841b55ecdae098c80dcae9cf767f6f8a0c2cdb3416bbef72181df4d0fe73f14" +dependencies = [ + "itoa", + "memchr", + "serde", + "serde_core", + "zmij", +] + [[package]] name = "sha2" version = "0.10.9" @@ -304,6 +329,9 @@ dependencies = [ [[package]] name = "vcltotal-parse" version = "0.1.0" +dependencies = [ + "serde_json", +] [[package]] name = "version_check" @@ -322,3 +350,9 @@ name = "zeroize" version = "1.8.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b97154e67e32c85465826e8bcc1c59429aaaf107c1e4a9e53c8d8ccd5eff88d0" + +[[package]] +name = "zmij" +version = "1.0.23" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "29666d0abbfad1e3dc4dcf6144730dd3a3ab225bbbdac83319345b1b44ccfc1b" diff --git a/src/interface/attest/src/lib.rs b/src/interface/attest/src/lib.rs index c71ee43..6e600f4 100644 --- a/src/interface/attest/src/lib.rs +++ b/src/interface/attest/src/lib.rs @@ -226,6 +226,10 @@ mod tests { linear_annot: None, epistemic_clause: None, requested_level: SafetyLevel::ParseSafe, + // S1 consonance verb. A bare `SELECT * FROM STORE "s"` is the + // epistemically-neutral read, so `Select` is the right witness + // here; the attestation path is verb-agnostic. + verb: Verb::Select, } } diff --git a/src/interface/dap/Cargo.toml b/src/interface/dap/Cargo.toml index 0c7a88f..d6dbec2 100644 --- a/src/interface/dap/Cargo.toml +++ b/src/interface/dap/Cargo.toml @@ -5,7 +5,7 @@ version = "0.1.0" edition = "2021" license = "MPL-2.0" authors = ["Jonathan D.A. Jewell "] -repository = "https://github.com/hyperpolymath/vql-ut" +repository = "https://github.com/hyperpolymath/vcl-ut" [lib] name = "vcltotal_dap" diff --git a/src/interface/echidna-client/Cargo.toml b/src/interface/echidna-client/Cargo.toml index 5322a50..7d78792 100644 --- a/src/interface/echidna-client/Cargo.toml +++ b/src/interface/echidna-client/Cargo.toml @@ -17,7 +17,7 @@ version = "0.1.0" edition = "2021" license = "MPL-2.0" authors = ["Jonathan D.A. Jewell "] -repository = "https://github.com/hyperpolymath/vql-ut" +repository = "https://github.com/hyperpolymath/vcl-ut" description = "Async REST client for echidna proof engine (localhost:8000 by default)" [lib] diff --git a/src/interface/fmt/Cargo.toml b/src/interface/fmt/Cargo.toml index 9042b0c..fe5b802 100644 --- a/src/interface/fmt/Cargo.toml +++ b/src/interface/fmt/Cargo.toml @@ -5,7 +5,7 @@ version = "0.1.0" edition = "2021" license = "MPL-2.0" authors = ["Jonathan D.A. Jewell "] -repository = "https://github.com/hyperpolymath/vql-ut" +repository = "https://github.com/hyperpolymath/vcl-ut" [lib] name = "vcltotal_fmt" diff --git a/src/interface/lint/Cargo.toml b/src/interface/lint/Cargo.toml index 63a667c..8e2a8d9 100644 --- a/src/interface/lint/Cargo.toml +++ b/src/interface/lint/Cargo.toml @@ -5,7 +5,7 @@ version = "0.1.0" edition = "2021" license = "MPL-2.0" authors = ["Jonathan D.A. Jewell "] -repository = "https://github.com/hyperpolymath/vql-ut" +repository = "https://github.com/hyperpolymath/vcl-ut" [lib] name = "vcltotal_lint" diff --git a/src/interface/lsp/Cargo.toml b/src/interface/lsp/Cargo.toml index d77bea9..c978f0a 100644 --- a/src/interface/lsp/Cargo.toml +++ b/src/interface/lsp/Cargo.toml @@ -5,7 +5,7 @@ version = "0.1.0" edition = "2021" license = "MPL-2.0" authors = ["Jonathan D.A. Jewell "] -repository = "https://github.com/hyperpolymath/vql-ut" +repository = "https://github.com/hyperpolymath/vcl-ut" [lib] name = "vcltotal_lsp" diff --git a/src/interface/recompute-wasm/Cargo.lock b/src/interface/recompute-wasm/Cargo.lock index 3aa45f5..7f3e45e 100644 --- a/src/interface/recompute-wasm/Cargo.lock +++ b/src/interface/recompute-wasm/Cargo.lock @@ -2,9 +2,101 @@ # It is not intended for manual editing. version = 4 +[[package]] +name = "itoa" +version = "1.0.18" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8f42a60cbdf9a97f5d2305f08a87dc4e09308d1276d28c869c684d7777685682" + +[[package]] +name = "memchr" +version = "2.8.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "cf8baf1c55e62ffcace7a9f06f4bd9cd3f0c4beb022d3b367256b91b87513d98" + +[[package]] +name = "proc-macro2" +version = "1.0.107" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "985e7ec9bb745e6ce6535b544d84d6cd6f7ad8bd711c398938ae983b91a766d9" +dependencies = [ + "unicode-ident", +] + +[[package]] +name = "quote" +version = "1.0.47" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1fbf4db142a473a8d80c26bbf18454ed458bf8d26c8219c331daecfdbd079001" +dependencies = [ + "proc-macro2", +] + +[[package]] +name = "serde" +version = "1.0.229" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "4148590afebada386688f18773da617792bf2ef03ffc1e4cbd2b1d45b023e0ba" +dependencies = [ + "serde_core", +] + +[[package]] +name = "serde_core" +version = "1.0.229" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "67dca2c9c51e58a4791a4b1ed58308b39c64224d349a935ab5039aa360942a48" +dependencies = [ + "serde_derive", +] + +[[package]] +name = "serde_derive" +version = "1.0.229" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e7a5d71263a5a7d47b41f6b3f06ba276f10cc18b0931f1799f710578e2309348" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "serde_json" +version = "1.0.151" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c841b55ecdae098c80dcae9cf767f6f8a0c2cdb3416bbef72181df4d0fe73f14" +dependencies = [ + "itoa", + "memchr", + "serde", + "serde_core", + "zmij", +] + +[[package]] +name = "syn" +version = "3.0.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a207d6d6a2b7fc470b80443726053f18a2481b7e1eee970597051596567987a3" +dependencies = [ + "proc-macro2", + "quote", + "unicode-ident", +] + +[[package]] +name = "unicode-ident" +version = "1.0.24" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75" + [[package]] name = "vcltotal-parse" version = "0.1.0" +dependencies = [ + "serde_json", +] [[package]] name = "vcltotal-recompute-wasm" @@ -12,3 +104,9 @@ version = "0.1.0" dependencies = [ "vcltotal-parse", ] + +[[package]] +name = "zmij" +version = "1.0.23" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "29666d0abbfad1e3dc4dcf6144730dd3a3ab225bbbdac83319345b1b44ccfc1b" diff --git a/src/interface/recompute-wasm/src/lib.rs b/src/interface/recompute-wasm/src/lib.rs index de96539..be629a8 100644 --- a/src/interface/recompute-wasm/src/lib.rs +++ b/src/interface/recompute-wasm/src/lib.rs @@ -181,6 +181,9 @@ mod tests { linear_annot: None, epistemic_clause: None, requested_level: SafetyLevel::ParseSafe, + // S1 consonance verb — see the comment above: this is the plain + // `SELECT` read, the neutral case for the recompute boundary. + verb: Verb::Select, }; let m = |modality, fields| ModalitySchema { modality, fields }; let sc = OctadSchema {