vcl-ut #25 P5a: trusted Rust/SPARK-grade String->Statement parser

.github/workflows/parse-gate.yml

@@ -0,0 +1,59 @@
+# SPDX-License-Identifier: PMPL-1.0-or-later
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# parse-gate.yml — Gates the trusted String->Statement parser
+# (`vcltotal-parse`, P5a of #25 reinforcing the verified-corpus
+# boundary). vcl-ut is the doubly-trusted hypatia<->verisim interface,
+# so the boundary parser must stay panic-free / total: clippy's
+# SPARK-grade lint set (no unsafe / unwrap / expect / panic / indexing /
+# unchecked arithmetic) is a HARD gate, and the proptest panic-free
+# invariant must pass. Tracked: hyperpolymath/standards#124, vcl-ut#25.
+
+name: Parse Gate
+
+on:
+  pull_request:
+    branches: ['**']
+  push:
+    branches: [main, master]
+
+permissions:
+  contents: read
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+jobs:
+  parse-gate:
+    name: vcltotal-parse — panic-free / clippy / tests
+    runs-on: ubuntu-latest
+
+    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).
+      - name: Pin toolchain + components
+        run: |
+          set -euo pipefail
+          rustup show active-toolchain || rustup default stable
+          rustup component add clippy
+          cargo --version && cargo clippy --version
+
+      # `vcltotal-parse` is its own workspace root (see its Cargo.toml).
+      # Operate via its manifest path so CI never traverses the parent
+      # virtual workspace (whose pre-existing `src/interface` member has
+      # an external path-dep that does not resolve in a standalone
+      # checkout). Self-contained: no external path-deps here.
+      - name: Clippy — SPARK-grade lint set as a hard gate
+        run: |
+          set -euo pipefail
+          cargo clippy --manifest-path src/interface/parse/Cargo.toml \
+            --all-targets --locked -- -D warnings
+
+      - name: Tests + panic-free proptest invariant
+        run: |
+          set -euo pipefail
+          cargo test --manifest-path src/interface/parse/Cargo.toml --locked

Cargo.toml

@@ -34,3 +34,12 @@ members = [
     "src/interface/lsp",
     "src/interface/dap",
 ]
+# NOTE: `src/interface/parse` (vcltotal-parse, #25 P5a) is deliberately
+# NOT a member here. The pre-existing `src/interface` member carries an
+# external path-dependency (`echidna-core = { path =
+# "../../../echidna/..." }`) that only resolves on the estate's
+# sibling-repo layout, so the whole virtual workspace fails to load in a
+# standalone checkout (e.g. CI). The trusted boundary parser must build
+# and gate in isolation, so it is its own workspace root (see
+# src/interface/parse/Cargo.toml `[workspace]`). Tracked separately:
+# the parent-workspace external-path-dep breakage is NOT a #25 concern.

PROOF-NEEDS.md

@@ -33,8 +33,19 @@
 - Debug adapter and formatter — lower priority but should preserve query semantics
 
 ### ReScript Bridge (src/bridges/)
-- `VclTotalParser.res`, `VclTotalBridge.res` — bridge between ReScript frontend and Idris2/Rust core
-- Prove: bridge faithfully translates between ReScript and core representations
+- `VclTotalParser.res`, `VclTotalBridge.res` — a **standalone ReScript
+  frontend** (a working recursive-descent parser producing a *ReScript*
+  AST). It is **not** on the verified path: it does not connect to, or
+  marshal into, the Idris2 `Statement` the proof corpus certifies, nor
+  the Rust core. (`VERIFICATION-STANCE.adoc` "no string→`Statement`
+  parser exists" is precise — it means no parser whose output is the
+  *certified* Idris2 `Statement`.)
+- The *trusted* boundary parser is the Rust/SPARK-grade
+  `src/interface/parse` crate (`vcltotal-parse`, P5a of vcl-ut#25),
+  which mirrors `Grammar.idr` and feeds the certifier across the C-ABI.
+- Optional future work: prove the ReScript frontend faithfully tracks
+  the Idris2 grammar (low priority; it is a convenience frontend, not a
+  trust anchor).
 
 ## Recommended Prover