fix(ci): green the three required gates + redirect stale stance doc

- vclt-gate bin: replace the panicking .expect() in parse_vql_type with a
  match returning Err on the (impossible) empty-object case, and add
  #![deny(clippy::unwrap_used, clippy::expect_used)] so the bin meets the
  Aspect/SPARK gate's no-panic posture (the lib already carries it). #49
- echidna-client: declare an own [workspace] so it is a standalone root
  (its transitive echidna-core path-dep breaks the default standalone
  build); Backend-Matrix now runs it via --manifest-path instead of `-p`,
  which could not select a non-member package.
- scorecard-enforcer: move the run: "Check minimum score" gate into a
  separate `enforce` job consuming the SARIF artifact, so the scorecard
  job stays uses-only (publish_results:true rejects mixed run/uses, 400).
- docs/VERIFICATION-STANCE.adoc: replace the stale duplicate (claimed
  predicates vacuous / not end-to-end proven) with a redirect to the
  canonical verification/proofs/ copy; SPDX header preserved.

Verified locally: corpus build exit 0, honesty-guard Clean,
cargo clippy --bin vclt-gate -D expect_used -D unwrap_used rc=0,
both workspaces resolve.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.github/workflows/backend-matrix.yml

@@ -102,4 +102,9 @@ jobs:
         run: git clone --depth 1 https://github.com/hyperpolymath/echidna ../echidna
 
       - name: Client wiremock suite (ECHIDNA_PROVER=${{ matrix.prover }})
-        run: cargo test -p vcltotal-echidna-client --tests --locked
+        # `vcltotal-echidna-client` is intentionally NOT a member of the root
+        # workspace (v0.2.0 workspace cleanup: its transitive echidna-core
+        # path-dep breaks standalone CI), so `-p` cannot select it. It is its
+        # own standalone workspace root; run it by manifest path now that the
+        # echidna sibling has been cloned above.
+        run: cargo test --manifest-path src/interface/echidna-client/Cargo.toml --tests --locked

.github/workflows/scorecard-enforcer.yml

@@ -44,6 +44,28 @@ jobs:
         with:
           sarif_file: results.sarif
 
+      - name: Upload SARIF artifact
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4.6.2
+        with:
+          name: scorecard-results
+          path: results.sarif
+          retention-days: 5
+
+  # Gating job: kept separate so the scorecard job above remains
+  # uses-only. GitHub rejects a publish_results: true job that also
+  # contains run: steps with HTTP 400 ("job must only have steps with
+  # uses"). The minimum-score gate therefore runs here against the
+  # SARIF uploaded as an artifact by the scorecard job.
+  enforce:
+    runs-on: ubuntu-latest
+    timeout-minutes: 15
+    needs: scorecard
+    steps:
+      - name: Download SARIF artifact
+        uses: actions/download-artifact@fa0a91b85d4f404e444e00e005971372dc801d16 # v4
+        with:
+          name: scorecard-results
+
       - name: Check minimum score
         run: |
           # Parse score from results

docs/VERIFICATION-STANCE.adoc

@@ -1,73 +1,23 @@
-= VCL-total Verification Stance
+= VCL-total Verification Stance (moved)
 :toc:
 :sectnums:
 
 // SPDX-License-Identifier: MPL-2.0
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 
-WARNING: vcl-ut is the interface between *hypatia* and *verisim*. Both sides
-trust safety claims made here. This document states *precisely* what is and is
-not currently proven, so that neither consumer over-trusts the boundary. It
-takes precedence over any "verified" / "type-safe" / "proven" phrasing in
-`README.adoc`, `PROOF-NEEDS.md`, or module doc-comments.
+NOTE: This file is a pointer only. The canonical, current verification stance
+for vcl-ut now lives at `verification/proofs/VERIFICATION-STANCE.adoc`.
 
-== Summary
+The canonical document is proof-backed and supersedes this `docs/` copy. As of
+2026-06-14, the Idris2 proof corpus is machine-checked: all ten safety levels
+(L1–L10) carry genuine soundness, and
+`idris2 0.8.0 --build verification/proofs/vclut-core.ipkg` exits 0.
 
-The 10-level safety story is, at present, *architecturally typed but not
-end-to-end proven*. The dependent-type apparatus exists but is *not connected*
-to the runtime checker or the FFI boundary that hypatia/verisim consume.
+The earlier text of this `docs/` file (which described the apparatus as
+architecturally typed but not end-to-end proven, with vacuous level predicates)
+is no longer accurate and has been removed. This copy is retained only as a
+redirect so existing links do not break.
 
-== What IS genuinely established
+See `verification/proofs/VERIFICATION-STANCE.adoc` for the authoritative,
+detail-complete stance.
 
-* `src/interface/abi/Types.idr` — `SafetyLevel`, `VclTotalError`, `QueryMode`
-  are real ADTs with total `DecEq` instances and total int<->tag round-trip
-  functions. The `Verify` namespace proves tag ranges with `So`. These are
-  sound, non-vacuous proofs.
-* `QueryHandle` is a genuine opaque type with an `So (ptr /= 0)` non-null
-  witness; it cannot be constructed null through the public API.
-* `src/core/Levels.idr` `SafetyCertificate` / `CanWeaken` define a real
-  subsumption lattice *at the type level*.
-
-== What is NOT proven (the honest gaps)
-
-. *The certificate is disconnected from the checker.* `src/core/Checker.idr`
-  decides every level with `Bool`-returning `checkLevelN` functions and never
-  constructs a `SafetyCertificate`. A query reported "Level 10" carries *no*
-  `Levels.idr` proof object. The dependent types are decorative w.r.t. the
-  actual decision procedure.
-. *Several level predicates are vacuous.* `NoRawUserInput` has the single
-  constructor `AllParameterised : NoRawUserInput stmt` (provable for *any*
-  statement, including injection-bearing ones); `AllNullableFieldsGuarded`'s
-  `GuardedNull` accepts *any* expression; `AllSelectItemsTyped`'s `ConsTyped`
-  requires no actual per-item typing evidence. As written, Levels 3, 4 and 5
-  prove nothing about the property they name.
-. *The FFI boundary is stringly/int-typed.* `src/interface/abi/Foreign.idr`
-  returns a bare `Bits32` error tag; the `parse` wrapper is an explicit
-  placeholder (returns `Left InternalError` on success). hypatia/verisim
-  receive an *asserted* level integer, not a transported proof.
-. *Layout/size proofs are vacuous.* `HasSize` / `HasAlignment` constructors
-  accept any `n`; `queryPlanHeaderSize : ... HasSize QueryPlanHeader 24` type-
-  checks regardless of the real layout. The 24-byte/8-align claim is unverified.
-
-== Consumer guidance
-
-* *hypatia / verisim*: treat the FFI level integer as an *advisory claim*, not
-  a proof carrier. Do not weaken your own checks on the strength of a VCL-total
-  level tag until gap (1) and (3) are closed.
-* Do not cite vcl-ut as "formally verified query safety" in downstream docs.
-
-== Closing the gaps
-
-The high-value, low-risk path (per `PROOF-NEEDS.md`): make `checkLevelN` return
-`Dec (Ln_... )` instead of `Bool`, give the vacuous predicates real
-constructors carrying evidence, and have the checker emit a `SafetyCertificate`
-that the Zig FFI transports as an opaque proof token. Tracked under
-hyperpolymath/standards#124.
-
-== Provenance
-
-Audit 2026-05-18 (corpus grep + read; no proof-escape symbols
-`believe_me`/`assert_total`/`postulate`/`sorry` are *applied* anywhere in
-`src/**` — the only match is a self-attesting comment in `Composition.idr`).
-The risk here is *not* proof escapes; it is *absent* proof masquerading as
-present proof at a trusted interface.

src/interface/echidna-client/Cargo.toml

@@ -1,4 +1,16 @@
 # SPDX-License-Identifier: MPL-2.0
+
+# Standalone workspace root: this crate is deliberately NOT a member of the
+# parent virtual workspace (root `Cargo.toml`), because it depends on
+# `vcltotal-interface`, which carries an external path-dep
+# (`../../../echidna/crates/echidna-core`) that does not resolve on a
+# standalone checkout. Declaring an own `[workspace]` lets the estate e2e
+# CI job (`.github/workflows/backend-matrix.yml`) build/test it by
+# `--manifest-path` once the echidna sibling is present, without dragging
+# the unresolved path-dep into the default standalone build. Mirrors the
+# same pattern used by `src/interface/parse/Cargo.toml`.
+[workspace]
+
 [package]
 name = "vcltotal-echidna-client"
 version = "0.1.0"

src/interface/parse/src/bin/vclt-gate.rs

@@ -15,6 +15,8 @@
 //! Pure function of (statement, schema): no network, no filesystem,
 //! no clock, no env-dependent behaviour beyond stdin/stdout/stderr.
 
+#![deny(clippy::unwrap_used, clippy::expect_used)]
+
 use serde_json::{json, Value};
 use std::io::{self, Read};
 use vcltotal_parse::schema::{FieldDef, ModalitySchema, VqlType};
@@ -267,10 +269,10 @@ fn parse_field_def(v: &Value) -> Result<FieldDef, String> {
 fn parse_vql_type(v: &Value) -> Result<VqlType, String> {
     match v {
         Value::String(s) => parse_nullary_type(s),
-        Value::Object(map) if map.len() == 1 => {
-            let (key, inner) = map.iter().next().expect("len==1 checked");
-            parse_parameterised_type(key, inner)
-        }
+        Value::Object(map) if map.len() == 1 => match map.iter().next() {
+            Some((key, inner)) => parse_parameterised_type(key, inner),
+            None => Err("expected single-key object for VqlType, found empty object".to_string()),
+        },
         other => Err(format!(
             "expected string or single-key object for VqlType, got {other}"
         )),