Merge pull request #24 from hyperpolymath/proof-debt/vclut-124-phase4-owed

vcl-ut Phase 4: discharge layout + L6-L10 join-closure proof debt (standards#124)

Author: hyperpolymath

.github/workflows/proof-corpus.yml

@@ -37,12 +37,24 @@ jobs:
       - name: Checkout repository
         uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
 
-      # NOTE: pin to a commit SHA per repo security posture once a stable
-      # release SHA is recorded (TODO(SHA-pin); tags used here interim).
-      - name: Set up Idris2 0.8.0
-        uses: idris-community/setup-idris@v1
-        with:
-          idris-version: 0.8.0
+      # Idris2 0.8.0 is built from PINNED official source. The former
+      # `idris-community/setup-idris` action's repository no longer
+      # resolves (404), and no maintained equivalent exists; a
+      # SHA-pinned source build is deterministic, version-exact, and
+      # depends on no third-party action (matches the repo's pin
+      # posture). `idris-lang/Idris2` tag v0.8.0 == commit
+      # 15a3e4e70843f7a34100f6470c04b791330788df.
+      - name: Build & install Idris2 0.8.0 from pinned source
+        run: |
+          set -euo pipefail
+          sudo apt-get update -qq
+          sudo apt-get install -y --no-install-recommends chezscheme make gcc
+          git clone --no-checkout https://github.com/idris-lang/Idris2.git /tmp/Idris2
+          git -C /tmp/Idris2 checkout 15a3e4e70843f7a34100f6470c04b791330788df
+          make -C /tmp/Idris2 bootstrap SCHEME=chezscheme
+          make -C /tmp/Idris2 install PREFIX="$HOME/.idris2"
+          echo "$HOME/.idris2/bin" >> "$GITHUB_PATH"
+          echo "IDRIS2_PREFIX=$HOME/.idris2" >> "$GITHUB_ENV"
 
       - name: Proof-escape audit (no believe_me / postulate / assert_* / sorry)
         run: |
@@ -51,7 +63,8 @@ jobs:
           files="src/core/Grammar.idr src/core/Schema.idr src/core/Decide.idr \
                  src/core/Levels.idr src/core/Checker.idr \
                  src/core/Composition.idr src/core/Epistemic.idr \
-                 src/interface/abi/Types.idr src/interface/abi/Layout.idr"
+                 src/interface/abi/Types.idr src/interface/abi/Layout.idr \
+                 src/interface/abi/LayoutProofs.idr"
           if grep -nE '\b(believe_me|really_believe_me|assert_total|assert_smaller|idris_crash|postulate|sorry)\b' \
                $files | grep -vE ':\s*(--|\|\|\|)' ; then
             echo "::error::proof-escape symbol found in the Phase-1 corpus"

CHANGELOG.md

@@ -10,6 +10,33 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+### Verified
+
+**VclTotal proof corpus — Phase 0→4 remediation** (2026-05-18/19,
+hyperpolymath/standards#124). The `src/core/**` Idris2 corpus, which at
+Phase 0 did not compile and had never been machine-checked, is now
+CI-gated and green:
+
+- `verification/proofs/vclut-core.ipkg` builds clean under idris2 0.8.0
+  (`idris2 --build`, exit 0, `%default total`) as **10 modules**, with
+  **zero proof-escape symbols** (no `believe_me`/`postulate`/`assert_*`/
+  `idris_crash`/`sorry`), enforced by `.github/workflows/proof-corpus.yml`.
+- Phase 1 (#21): corpus resurrection — `ABI.Types`/`Grammar` repaired,
+  `.ipkg`/CI added, L4 verified in situ.
+- Phase 2 (#22): L2/L3/L5 de-vacuized over the shared `Core.Decide`
+  deciders + `checkLevel2/3/5Sound` + genuine `composeJoin` closure.
+- Phase 3 (#23): L1 + L6–L10 soundness; `Checker.certifyAt`/
+  `certifyRequested` assemble a genuine dependent `SafetyCertificate`;
+  `ABI.Layout` made sound; Phase 3d removed the fabricating Zig FFI
+  (now fail-closed) and added the proof-gated `Checker.certifiedLevel`.
+- Phase 4 (PR #24): `ABI.LayoutProofs` (genuine alignment/no-padding/
+  bounds) + L6–L10 `composeJoin` closure (`l6..l9Compose`,
+  `epiStructJoin`); L10 acyclicity carried by the explicit
+  `JoinSideCondition` (provably non-closed, not faked).
+
+`verification/proofs/VERIFICATION-STANCE.adoc` is the authoritative,
+precisely-scoped catalogue (residual OWED items disclosed, not masked).
+
 ### Renamed
 
 **V{Q→C}L-{UT→total}** (2026-04-05). Full repo-wide migration of the project

CLAUDE-CROSS-SESSION-NOTE.md

@@ -6,8 +6,8 @@
 - **LOC**: ~8,000
 - **Languages**: Rust, ReScript, Idris2, Zig
 - **Existing ABI proofs**: `src/interface/abi/*.idr` + domain-specific Idris2: `src/core/Checker.idr`, `Grammar.idr`, `Levels.idr`, `Schema.idr`, `Composition.idr`
-- **Machine-verified**: `verification/proofs/SafetyL4Model.idr` only (idris2 0.8.0 `--check`, exit 0, zero proof escapes) — the Level-4 SQL-injection remediation
-- **Dangerous patterns**: ⚠️ The `src/core/**` Idris2 corpus **does not compile** on `origin/main` and has **never been machine-checked** (no `.ipkg`/CI). `ABI.Types` has ≥4 type errors; `Grammar.idr` forward-references types with no `mutual` block. L2/L3/L5 safety predicates are **vacuous** (inhabited for any input, incl. injection); `SafetyCertificate` is never constructed by `checkQuery`; the Zig FFI is a `SELECT`-substring stub. See `verification/proofs/VERIFICATION-STANCE.adoc` for the authoritative, proof-backed catalogue. The earlier "None detected" line was wrong.
+- **Machine-verified**: the full `VclTotal` proof corpus — `verification/proofs/vclut-core.ipkg` builds clean under idris2 0.8.0 (`idris2 --build`, exit 0, `%default total`, **zero proof-escape symbols**, CI-gated by `.github/workflows/proof-corpus.yml`) as **10 modules** (`ABI.{Types,Layout,LayoutProofs}` + `Core.{Grammar,Schema,Decide,Levels,Checker,Composition,Epistemic}`), plus the self-contained `verification/proofs/SafetyL4Model.idr` (`--check`, exit 0). Phases 1–3 are on `origin/main` (PRs #21/#22/#23); Phase 4 (`LayoutProofs` + L6–L10 `composeJoin` closure) is **PR #24**, pending merge.
+- **Status (Phase 0 → 4 RESOLVED, honestly)**: the Phase-0 blockers are fixed, not faked — the corpus compiles and is machine-checked; `ABI.Types`/`Grammar` errors repaired; **L2/L3/L5 de-vacuized** (Phase 2, evidence-carrying predicates over `Core.Decide`); all ten levels carry `checkLevelNSound` and `Checker.certifyAt`/`certifyRequested` assemble a genuine dependent `SafetyCertificate` (Phase 3); the Zig FFI is no longer a fabricating stub — it is **fail-closed** with a proof-gated `Checker.certifiedLevel` mint (Phase 3d). Remaining honest gaps are precisely scoped (FFI proof-transport, string→`Statement` parser, L3 subquery/heuristic scoping, L9/L10 predicate depth, the additive↔ceil `alignUp` sliver). `verification/proofs/VERIFICATION-STANCE.adoc` is the authoritative, proof-backed catalogue and takes precedence over this file.
 
 ## What Needs Proving
 
@@ -20,8 +20,9 @@
 - Prove: parser (ReScript side) accepts exactly the Idris2-specified grammar
 
 ### Level System (src/core/Levels.idr)
-- ✅ L4 `NoRawUserInput` de-vacuized + `checkLevel4Sound` + `noRawUserInputCompose` (verified in `verification/proofs/SafetyL4Model.idr`)
-- ⚠️ L2/L3/L5 predicates still vacuous — de-vacuize with evidence-carrying constructors and prove each `checkLevelN` sound (as done for L4)
+- ✅ L4 `NoRawUserInput` de-vacuized + `checkLevel4Sound` + `noRawUserInputCompose` (verified in `verification/proofs/SafetyL4Model.idr` and in situ in the corpus)
+- ✅ L2/L3/L5 de-vacuized (Phase 2) — evidence-carrying predicates over `Core.Decide`, with `checkLevel2/3/5Sound` and genuine `composeJoin` closure
+- ✅ L1 + L6–L10 sound (Phase 3) + genuine L6–L10 `composeJoin` closure (Phase 4: `l6..l9Compose`, `epiStructJoin`); L10 acyclicity carried by the explicit `JoinSideCondition` (provably non-closed, not faked)
 - 10-level type safety hierarchy — prove level ordering is a lattice
 - Prove: level promotion/demotion preserves query safety