From 3ba8988966851c0ee842bef7cfe63362d5c5b1aa Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 21 Jul 2026 13:22:07 +0100 Subject: [PATCH 1/5] fix(ci): repair dogfood-gate YAML and trim dependabot to real ecosystems MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two independent, measured CI faults. 1. .github/workflows/dogfood-gate.yml was MALFORMED YAML. The `run: |` literal block scalar takes its indentation indicator from its first line (10 spaces), but the embedded Python validator started at column 1. YAML therefore terminated the block scalar and tried to read `import tomllib, sys` as a mapping key: while scanning a simple key ... could not find expected ':' Consequences, both measured: - the workflow has failed EVERY run in 0s (startup_failure) since at least 2026-07-06 — it has never once validated anything; - it broke Dependabot's github_actions updater with `dependency_file_not_parseable`, which is why trimming the ecosystem list alone would NOT have made Dependabot green. Fix: indent the Python into the block scalar. Because YAML strips the block indentation uniformly, the shell still receives the script at column 0, and relative (Python-significant) indentation is preserved. Verified by execution, not inspection: the step was extracted from the parsed YAML and run against both a valid and an invalid manifest — exit 0 with `Valid: ...`, and exit 1 with the `::error` annotation respectively. All 22 workflows now parse. NOTE: this file is a template copied across the estate; ~80 of 266 copies carry the identical fault. Fixing the template is tracked separately. 2. .github/dependabot.yml was the unedited RSR template. It declared mix / npm / pip / nix, none of which have a manifest in this Rust-only repository (verified absent: mix.exs, package.json, requirements.txt, pyproject.toml, flake.nix). Those four ecosystems accounted for four of the five recurring weekly failures since 2026-07-13. Also: this repository has FIVE cargo workspace roots, and the single `directory: "/"` entry covered only the root one — so the crates holding most of the real code, including the parser and vclt-gate, were invisible to Dependabot. Added explicit entries for src/interface/{parse,attest,recompute-wasm}, each self-contained. src/interface/echidna-client remains deliberately excluded: it reaches ../../interface, which carries an out-of-tree path dependency on the echidna sibling repo that Dependabot cannot resolve. Declaring it would reintroduce exactly the always-red job this trim removes. Verification: reuse lint -> compliant, 458/458 (MPL-2.0, CC-BY-SA-4.0) 22 workflows -> 0 malformed cargo test --workspace -> 102 passed cargo test (parse workspace) -> 36 passed Co-Authored-By: Claude Opus 4.8 --- .github/dependabot.yml | 67 +++++++++++++++++++----------- .github/workflows/dogfood-gate.yml | 40 +++++++++--------- 2 files changed, 63 insertions(+), 44 deletions(-) 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 } From ca9fe5030df87716e425c92e2ec7e821fbe4d176 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 21 Jul 2026 13:45:50 +0100 Subject: [PATCH 2/5] fix(ci): repair two silently-rotted crates and close the CI coverage gaps MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit vcl-ut has FIVE cargo workspace roots. CI covered three of them, and the two it missed had stopped compiling without anyone noticing. WHAT ROTTED `ast::Statement` gained the S1 consonance field `verb` (Select / Inspect / Verify / Assert / Declare / Retract / Merge / Split / Normalise) — the consonance turn itself. Two downstream crates were never updated: src/interface/attest E0063: missing field `verb` src/interface/recompute-wasm E0063: missing field `verb` In both cases only the in-file `#[cfg(test)]` module was stale; the libraries still built. That is why nothing downstream complained — 12 tests had simply stopped running, in the crates carrying the attestation and recompute boundaries. Fixed by supplying `verb: Verb::Select` at both sites. Both constructions are the bare `SELECT * FROM STORE "s"` case and both already used the full eight-modality `OctadSchema`, so the octad was already correct there; only the verb was missing. attest 9 tests, now green recompute-wasm 3 tests, now green Their Cargo.lock files had also drifted (recompute-wasm's recorded only the two in-repo path crates and no external deps at all — it had not been resolved since its manifest grew dependencies). Regenerated and committed. WHY IT ROTTED — coverage map, measured 2026-07-21 / e2e.yml PARTIAL (see below) /src/interface/parse parse-gate.yml full /src/interface/echidna-client backend-matrix.yml needs echidna sibling /src/interface/attest NOTHING /src/interface/recompute-wasm NOTHING New satellite-crates-gate.yml gates the last two: clippy `-D warnings` plus tests, over a matrix. Both were verified to pass `-D warnings` cleanly before the gate was added, so this is a real gate that is green, not an aspirational one. It mirrors parse-gate.yml's deliberate use of preinstalled rustup over a third-party toolchain action. `--locked` is deliberately omitted there for now, and the reason is recorded in the workflow: the lockfiles are freshly regenerated after a long ungated drift. It should be restored once a Dependabot cycle has run against them. ALSO FIXED IN e2e.yml 1. The root job ran `--test property_test` + `--test integration_test` only: 69 of the root workspace's 102 tests. Every test in tests/e2e_test.rs (20) and tests/fuzz_test.rs (13) was skipped. Now `cargo test --workspace --all-targets --locked`, verified locally at 102 passed / 0 failed. 2. Removed both "Provide echidna sibling" steps, which 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 the root tests nor tests/e2e.sh ever resolve it. Verified with no sibling present: 102 tests pass, e2e.sh reports 19/19. echidna-client remains gated by backend-matrix.yml, which does need it. CORRECTION TO AN EARLIER FINDING An earlier read of this repository recorded "0 unit tests; root cargo test is a fake gate". That was wrong, and was an artefact of truncating the log to its last lines. The root crate is a re-export facade over fmt + lint, so per-crate UNIT counts are legitimately zero and the entire surface lives in tests/. The README's `tests-102 pass` badge is exact. Recorded in the e2e.yml header so the same misreading is not repeated. Verification: reuse lint -> compliant, 459/459 23 workflows -> 0 malformed cargo test --workspace --locked -> 102 passed cargo test (parse) -> 36 passed cargo test (attest) -> 9 passed cargo test (recompute-wasm) -> 3 passed bash tests/e2e.sh -> 19/19, no echidna sibling 150 tests total Co-Authored-By: Claude Opus 4.8 --- .github/workflows/e2e.yml | 43 ++++++--- .github/workflows/satellite-crates-gate.yml | 85 ++++++++++++++++++ src/interface/attest/Cargo.lock | 34 +++++++ src/interface/attest/src/lib.rs | 4 + src/interface/recompute-wasm/Cargo.lock | 98 +++++++++++++++++++++ src/interface/recompute-wasm/src/lib.rs | 3 + 6 files changed, 256 insertions(+), 11 deletions(-) create mode 100644 .github/workflows/satellite-crates-gate.yml 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/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/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 { From d9969389db1b28e2268279456686a71e5021ec03 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 21 Jul 2026 13:52:24 +0100 Subject: [PATCH 3/5] docs(levels): reconcile the level ladder with the code, and document L10 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The flagship explanatory document disagreed with the implementation on the numbering, the vocabulary and the number of levels. All three are corrected against `src/interface/parse/src/ast.rs` and `src/core/Levels.idr`, which are canonical because the numbers are wire tags, not prose. 1. NUMBERING WAS OFF BY ONE Doc: Level 1 Parse ... Level 10 Linearity. Code: ParseSafe = 0 ... LinearSafe = 9, EpistemicSafe = 10. A reader who requested level 7 expecting Cardinality Safety would have got Effect-Tracking. Every heading, table and diagram shifted down by one; a mapping note added so old citations can be translated. 2. THE DOCUMENTED VOCABULARY DOES NOT PARSE The document taught `FETCH` and `REMOVE`. Neither appears anywhere in the parser. Measured against the real parser: FETCH users.name EFFECTS { Read } -> REJECTED "expected keyword SELECT" REMOVE users WHERE ... -> REJECTED "expected keyword SELECT" SELECT * FROM STORE main -> parses, verb=Select ASSERT * FROM STORE main -> parses, verb=Assert DECLARE * FROM STORE main -> parses, verb=Declare The real keyword surface is SELECT / INSPECT / VERIFY / ASSERT / DECLARE / RETRACT / MERGE / SPLIT / NORMALISE. Replaced 19 FETCH and 3 REMOVE. The implementation is well AHEAD of the prose here: the consonance verbs are fully parseable and carry the right verb tag. Only the documentation was still speaking the pre-consonance language. 3. THERE ARE ELEVEN LEVELS, NOT TEN — AND THE ELEVENTH WAS UNDOCUMENTED L10 `EpistemicSafe` appeared in no document anywhere in the repository. It now has a full section, written from `Levels.idr` and `Decide` rather than invented: the four `EpistemicRequirement` forms, and the four conditions `epistemicConsistentStmt` actually decides (clause present; >=1 agent; every referenced agent declared; no direct ENTAILS cycle). Its two owed obligations are stated plainly rather than glossed — transitive ENTAILS-cycle detection and proposition well-typedness are disclosed residuals in VERIFICATION-STANCE.adoc. A safety level that overstates itself is worse than no level at all. L10 is also flagged as different in KIND. L0-L9 are safety properties: they rule out executions that go wrong. L10 is a warrant property: it rules out answers the engine is not entitled to give, though every step was well-typed. A passive store cannot need it — one witness cannot disagree with itself. A consonance engine over eight modal witnesses can. Correspondingly, the TypeLL inheritance diagram is corrected: L10 is NOT inherited from TypeLL. A UI panel has no federation and no warrant question. L10 originates in VCL-UT — the first level this domain contributed back to the theory rather than received from it. 4. NEW: THE UPPER LADDER HAS NO SURFACE SYNTAX (measured) `parse_statement` hardcodes proof_clause, effect_decl, version_const, linear_annot and epistemic_clause to None, while `infer_requested_level` awards L7-L10 on exactly those fields. So no parsed statement can reach them. Measured ceiling: L1 SELECT * FROM STORE a L4 SELECT * FROM STORE a WHERE GRAPH.x > 1 L6 SELECT * FROM STORE a LIMIT 10 -- EFFECTS / AS OF / USE ONCE / AGENTS -> all rejected Highest level reachable from VCL source: L6. Ladder defines: L10. This is a DISCLOSED, fail-closed gap, not silent rot — the parser rejects EFFECTS with a message naming the P5a slice and issue #25 rather than accepting and ignoring it. Fail-closed is correct. But the honest claim is now recorded in the document: eleven levels are specified and proved; six are expressible. Title changed from "The 10 Levels of Type Safety" to "The Levels of Type Safety" — the count was the false part. The filename is left alone so no existing link breaks; whether to rebrand around eleven levels is a naming decision for the owner, not something to settle in a doc fix. Verification: reuse lint -> compliant, 459/459 all level headings cross-checked one-by-one against ast.rs SafetyLevel no residual "10 levels" / "levels 1-N" claims remain Co-Authored-By: Claude Opus 4.8 --- docs/THE-10-LEVELS-EXPLAINED.adoc | 315 ++++++++++++++++++++++-------- 1 file changed, 237 insertions(+), 78 deletions(-) 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". From efd257f50fcd48235eebeb13ce8745b02dfdcbe1 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 21 Jul 2026 13:55:11 +0100 Subject: [PATCH 4/5] docs: truth pass on README, ROADMAP and the stale repository URLs MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Naming, counts and status claims brought into line with what is measurably true, following the owner's decision that VCL-UT = *Usage-Tracked* is canon and that this repository is the source of truth for the level ladder. README.adoc - Title and 18 body occurrences: VCL-total -> VCL-UT. - The "Ubiquitous Type-safe" gloss is removed and explicitly retired. Both superseded expansions ("Ubiquitous Type-safe", "-total") are named so they stop recirculating. Usage-Tracked is also the accurate one: what distinguishes this tier is that resource usage is tracked in the type system, L9 LinearSafe via QTT. - "-total" is noted as surviving in the crate name `vcl-total` and the Idris namespace `VclTotal`; renaming those is invasive and deliberately not bundled here. - Tests badge 102 -> 150. 102 was correct for the root workspace but counted only one of the five workspace roots. Measured: 102 root + 36 parse + 9 attest + 3 recompute-wasm. - "all 10 levels of type safety" -> eleven, L0-L10, with L10 EpistemicSafe identified as a warrant property rather than a safety property. - Added the honest qualification up front: eleven levels are specified and proved, six are expressible (surface-syntax ceiling is L6). - Pipeline diagram: "(10 progressive levels)" -> "(11 levels, L0-L10)". Left deliberately unchanged: the four "10 levels" references that describe TypeLL. Under the corrected framing those are correct — TypeLL defines L0-L9, exactly ten, and VCL-UT contributes the eleventh. ROADMAP.adoc — rewritten, because nearly every claim was false - "Parser work not yet started" was false: a Rust parser exists with 36 green tests, gated by parse-gate.yml under a SPARK-grade clippy set. - "Idris2 parser with totality proof" was never what shipped. The Idris corpus proves; the Rust port re-establishes independently. - Every milestone box was unchecked despite most of v0.1-v0.3 being done. Boxes now reflect measured state. - Level numbering corrected 1-10 -> L0-L10 throughout. - "VeriSimDB 6-modal query planner" -> octad transition planner. - Added a measured status table and a "Nearest Work" section ordered by value: surface syntax for L7-L10; wiring vclt-gate into VeriSimDB; discharging the two disclosed L10 residuals; retiring the HEXAD keyword. - New v0.4.0 milestone for the consonance level, which the old roadmap had no place for at all. Cargo manifests (8 files) - repository = ".../vql-ut" -> ".../vcl-ut". Correction to an earlier note: that URL does not 404. GitHub still redirects vql-ut -> vcl-ut after the rename. It is stale rather than broken, and the reason to fix it is that the redirect stops working if the old name is ever reused. Measured with `gh api repos/hyperpolymath/vql-ut`, which returns full_name "hyperpolymath/vcl-ut". CHANGELOG.md's "still hyperpolymath/vql-ut" line is left alone: it is a dated historical entry, not a live claim. Verification: reuse lint -> compliant, 459/459 cargo test --workspace --locked -> 102 passed Co-Authored-By: Claude Opus 4.8 --- Cargo.toml | 2 +- README.adoc | 81 +++++++----- ROADMAP.adoc | 159 ++++++++++++++++++------ src/core/Cargo.toml | 2 +- src/interface/Cargo.toml | 2 +- src/interface/dap/Cargo.toml | 2 +- src/interface/echidna-client/Cargo.toml | 2 +- src/interface/fmt/Cargo.toml | 2 +- src/interface/lint/Cargo.toml | 2 +- src/interface/lsp/Cargo.toml | 2 +- 10 files changed, 183 insertions(+), 73 deletions(-) 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/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/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" From 37b7ab638f53e4ffb00f9444ac1a19d5f9f6e78a Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Tue, 21 Jul 2026 13:58:08 +0100 Subject: [PATCH 5/5] =?UTF-8?q?docs:=20two-strand=20work-up=20=E2=80=94=20?= =?UTF-8?q?the=20consonance=20claim=20and=20the=20VeriSimDB=20application?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The strategic deliverable. Two strands kept deliberately separate because they have different success conditions: Strand A succeeds if the theoretical claim is novel and defensible; Strand B succeeds if VeriSimDB is measurably safer. Neither implies the other. STRAND A — the theoretical claim Argues that consonance languages are a distinct class, not query languages with extra types, on three grounds: statements are propositions and epistemic requests rather than read requests; retraction is not deletion and drift is a typed condition rather than an error; and well-typedness stops being sufficient once several modal witnesses can disagree. The gap in the world is stated honestly. Type-safe query languages are a crowded, mature field — LINQ, Quill, Diesel, jOOQ, TypeQL, EdgeQL for L0-L5, and substantial literature for effects, temporal, linear and cardinality. A "ten levels of query safety" paper enters that field as a thorough synthesis and will be read as one. What none of them do is type WARRANT: every one assumes a single source of truth that cannot disagree with itself. Epistemic logic, provenance and truth-maintenance all exist, but beside the query path — never as a type that can refuse a statement. The decisive evidence came from the code rather than from taste. The ladder has eleven levels; the eleventh is not a query-safety property; and it is the one level NOT inherited from TypeLL, because a UI panel has no federation and so no warrant question. A framework whose eleventh member does not fit its own name is telling you the name is wrong. WHITEPAPER REFRAME IS A PROPOSAL, NOT AN EXECUTED REWRITE Deliberate. The direction is settled, but how a paper argues its claim is the author's call and is the least testable, highest-blast-radius change available here. The 1,909-line .tex is untouched. What is offered is a section-by-section structure and a complete draft abstract, for approval first. STRAND B — the VeriSimDB application Opens with the uncomfortable fact: VCL-UT delivers nothing to VeriSimDB at runtime today. The proof corpus is real, the parser is real and gated, the gate binary exists and Contract v1 is frozen — but the seam is built on one side only. The producer is finished and the consumer was never written. Defends the subprocess/JSON-line seam against the obvious objection that it looks unfashionable, using evidence from this repository: src/interface's external path-dep on an echidna sibling is exactly the build coupling the CLI seam avoids, and it is why echidna-client cannot even be covered by Dependabot. Sets out what VeriSimDB actually gets — a fail-closed admissibility check before statements touch consonance state; one level ladder instead of two divergent ones; independently-verifiable attestation; and vocabulary discipline — and gives a migration path that keeps VeriSimDB's genuinely good ReScript surface parser and diagnostics while replacing only the verdict. Two concrete defects, both located precisely: - VCLTypeChecker.res:60 builds the default context with six modalities though the type admits eight. Provenance and Spatial are silently absent from every default type-check. The hexad-to-octad migration reached the variants and stopped before the defaults and the names — HexadType is still the type name in four places. - The seam is unwired (zero vclt-gate references in verisim-api/src/vcl.rs). Sequenced plan, ordered by value per unit of risk, with the repository each item belongs to marked — items 3-5 are VeriSimDB changes and cannot be committed from this repository. Closes with a falsification section, so the plan can be argued with rather than assumed: if VeriSimDB's ReScript checker is materially more capable than the corpus, "vcl-ut is source of truth" costs capability; if subprocess latency is material on the hot path, the CLI seam is wrong and should be measured BEFORE the wiring work rather than after; and if the consonance claim has prior art under another name, Strand A weakens to a synthesis claim. The prior-art search behind the gap argument was not exhaustive and says so. Verification: reuse lint -> compliant, 460/460 every factual claim in the Ground Truth table measured against the working tree on 2026-07-21, including the two VeriSimDB defects Co-Authored-By: Claude Opus 4.8 --- ...6-07-21-workup-consonance-and-verisim.adoc | 507 ++++++++++++++++++ 1 file changed, 507 insertions(+) create mode 100644 docs/2026-07-21-workup-consonance-and-verisim.adoc 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.