vcl-ut Phase 3: L1/L6–L10 soundness + dependent SafetyCertificate + sound ABI.Layout (stacked on #22) — Refs standards#124

[hyperpolymath]

Stacked on #22 (Phase 2), which is stacked on #21 (Phase 1). Refs hyperpolymath/standards#124. Does not close the issue. Retarget down the stack as #21/#22 merge.

What this does (Phase 3 of the standards#124 vcl-ut HOLE remediation)

3a — soundness for all remaining levels

checkLevel1Sound … checkLevel10Sound, same machine-checked with … proof p shape as checkLevel4Sound, no proof-escape. L1's Decide.allFieldsBoundFromResolve builds the genuine inductive AllFieldsBound (each FieldBound carries the real resolveFieldRef ref schema = Just fd), connected to the checker without disturbing the genuine Composition.l1Compose. With Phase 2, all of L1–L10 now have genuine checker→predicate soundness.

3b — checkQuery emits a real dependent SafetyCertificate

tryL1..tryL10 run each decision procedure and, on acceptance, return the genuine LN_* witness via the Sound lemmas; certifyAt/certifyRequested assemble them into the cumulative dependent SafetyCertificate. A Just from certifyRequested stmt schema is a machine-checked proof the query meets its declared requestedLevel. The previously-decorative dependent certificate is now produced by the decision procedure. checkQuery (C-ABI Bool path) retained unchanged.

3c — ABI.Layout made sound + CI-gated (honest, not faked)

The only false proofs in the entire codebase were two items in ABI.Layout; deleted rather than forced: alignUpCorrect ((align > 0) Bool-as-Type + bogus Refl), offsetInBounds (open ?metavariable), queryPlanHeaderNoPadding (over-claimed + non-reducing). paddingFor's genuine non-compile ((-) needs Neg Nat) fixed to minus. The sound content (roundtrip Refl proofs, layout data) is kept; VclTotal.ABI.Layout is now the 9th ipkg module, CI-gated. ABI.Foreign stays excluded but is not unsound (FFI plumbing, no proofs) — stub-transport is precisely-disclosed Phase 3+ architecture.

Verification

• Clean idris2 0.8.0 --build verification/proofs/vclut-core.ipkg → EXIT=0, 9/9 modules, %default total.
• Zero proof-escape symbols (CI escape-grep updated for Layout.idr); SafetyL4Model.idr still --check EXIT=0.
• No fake green: every undischarged obligation (FFI transport, genuine ABI.Layout alignment/no-padding theorems, L6–L10 predicate shallowness, L3 subquery/heuristic scoping) is scoped OWED in VERIFICATION-STANCE.adoc, not masked. Headline residuals (non-compiling corpus, vacuous L2/L3/L5, decorative certificate, unsound ABI.Layout) are all resolved.

🤖 Generated with Claude Code

[hyperpolymath]

Update — Phase 3d added to this PR (commit `28cbe71`): FFI honesty.

The FFI fabricated a result — `ffi/zig/src/lib.zig` returned `2` (`Verified L2`) for any query containing the substring `SELECT`, with a Zig test enshrining it. A fake green is worse than a red, so:

• Lie deleted: `vclut_verify_query` is now fail-closed — returns `-1` (Rejected, explicit "no verifier backend linked"), never a level it did not establish. The enshrining test was rewritten to assert the fail-closed contract; `zig build test` EXIT=0.
• Genuine proof-gated mint in the CI-gated corpus: `Checker.certifiedLevel : Statement -> OctadSchema -> Int` returns a level only on the `Just`-certificate branch of `certifyRequested` (structural, no proof-escape).
• Honest trust model documented in both `Foreign.idr` copies + `VERIFICATION-STANCE.adoc`: a C int is a trusted-certifier attestation, not a transported dependent proof (impossible by construction over any FFI). Named OWED (absent, not faked): there is no string→`Statement` parser anywhere in the repo — the `verify(query_string)` FFI shape presupposes an unwritten component; plus C-ABI `Statement` marshalling, the Idris→C build, and the real backend link.

Authoritative verification: corpus `idris2 0.8.0 --build` EXIT=0 (9/9), `SafetyL4Model` EXIT=0, `zig build test` EXIT=0, zero proof-escapes. Refs hyperpolymath/standards#124; does not close.