vcl-ut: reinforce the verified-corpus boundary — FFI proof-attestation transport + string->Statement parser (post-Phase-4 residual)

[hyperpolymath]

Summary

Phase 4 (PR #24) retired the enumerated phased proof debt for the
VclTotal corpus: it compiles green (10 modules, idris2 --build,
exit 0, %default total, zero proof-escape symbols, CI-gated),
L1–L10 have soundness lemmas, and Checker.certifyAt/certifyRequested
assemble a genuine dependent SafetyCertificate.

That proven safety is real but stops at the corpus boundary. This
issue tracks the disclosed, precisely-scoped residual so it is
reinforced deliberately rather than forgotten. It is not Phase-4
residue — it is a new, distinct workstream. Authoritative catalogue:
verification/proofs/VERIFICATION-STANCE.adoc (OWED section).

The core gap — the FFI / boundary (priority 1)

The dependent SafetyCertificate is not transported across the C
ABI; the FFI is honestly fail-closed. A hypatia/verisim caller
receives at most a trusted-certifier attestation (proof-carrying-code
style), never a re-checkable proof object — and a C ABI carrying a
re-checkable dependent proof is impossible by construction, so the
honest target is attestation, not transport. Until the pieces below
exist, the FFI stays fail-closed and consumers MUST NOT weaken their
own checks on a vcl-ut level tag.

Concretely missing (each is genuine engineering, not a proof tweak):

• A String -> Statement parser. None exists anywhere in the
  repo. The verify(query_string) FFI shape presupposes a component
  nobody has written; the corpus only ever certifies an
  already-built AST.
• C-ABI Statement / OctadSchema marshalling.
• The Idris→C build linking the shim to
  Checker.certifiedLevel (the existing proof-gated mint).
• The real backend symbol (vclut_rs_verify) is declared in
  intent but not linked.
• Attestation design: an opaque proof token / signed
  attestation contract the caller can trust, with the trust boundary
  explicitly stated (extend the ADR set under docs/decisions/).

Secondary residual (lower value; track, don't swarm)

• L9/L10 predicate depth. Predicates assert "clause/annotation
  present" + decider — shallower than full checkLevelN semantics
  (L9 ≠ LinUnlimited; L10 acyclic ENTAILS as a predicate, not
  only the JoinSideCondition). Strengthening these is genuine proof
  work. (L10 no-ENTAILS-cycle is provably not join-closed — the
  explicit JoinSideCondition is by-design, not debt.)
• alignUpAdditiveEquivOWED — the additive (Layout.alignUp = size + paddingFor) ↔ ceil (alignTo = ⌈size/a⌉ * a) equivalence
  for a > 0. Currently a documented String scope note (NOT a
  believe_me); needs the Data.Nat Euclidean identity + a
  Bool↔Prop bridge for paddingFor's conditional.
• ABI.Foreign — contains no proofs; does not compile as-is
  (FFI plumbing: missing Data.Bits, etc.); deliberately excluded
  from vclut-core.ipkg.
• L3 disclosed scoping — ESubquery treated opaque; the
  NULL-guard recogniser is the structural heuristic, not dataflow.
  Sound but bounded; only revisit if a consumer needs the stronger
  property.

Out of scope here (aspirational, never in #124)

Grammar unambiguity, schema-evolution backward-compat, and
ReScript-bridge faithfulness (listed in PROOF-NEEDS.md "What Needs
Proving") — separate efforts if/when prioritised.

Acceptance

The FFI section (priority 1) is "done" when a query string can be
parsed → checked → and the level a C caller receives is structurally
gated behind a real certifiedLevel certificate (no proof-escape),
with the attestation trust boundary documented in an ADR and the
VERIFICATION-STANCE.adoc OWED entries for the FFI updated to
RESOLVED. The build oracle remains idris2 --build verification/proofs/vclut-core.ipkg (exit 0, zero escapes); never
admin-merge past a non-green build.

Refs hyperpolymath/standards#124. Follows PR #24 (Phase 4).

[hyperpolymath]

Architecture decided (2026-05-19)

Three forks resolved:

1. Parser home — Rust/SPARK-grade + marshalling. The trusted
   String -> Statement parser is a Rust crate held to a SPARK-grade
   posture (#![forbid(unsafe_code)], panic-free / total: no
   unwrap/expect/panic/indexing/arith-overflow, every failure a
   typed Result), parsing into a faithful Rust mirror of the Idris2
   Statement (src/core/Grammar.idr). It then marshals across a
   stable C-ABI into the Idris2 Statement the proof corpus certifies.
   Two proved components (parser, certifier) + one explicit marshalling
   seam to audit. (Not the ReScript bridge parser — that stays a
   standalone frontend; it is NOT on the verified path.)

2. Trust model — signed attestation token. The certifier signs
   (sha256(query_bytes), schema_id, level); hypatia/verisim verify
   the signature against the certifier public key before trusting the
   level. This is provenance, not a re-checkable dependent proof
   (impossible across a C ABI by construction). The trust boundary is
   stated in an ADR, not hidden.

3. Sequencing — phased (P5a..P5d), like Phases 1-4.

Phased roadmap

• P5a — Rust/SPARK-grade String -> Statement parser.
  New workspace crate src/interface/parse (vcltotal-parse).
  Faithful AST mirror of Grammar.idr (expr type slots are always
  TAny at parse time, per the grammar — elided, set by the
  marshaller). Total tokenizer + recursive-descent. Fail-closed:
  unsupported syntax => typed error, never a wrong AST. proptest
  invariant: parse never panics on arbitrary input. clippy panic-free
  lint gate in CI. First slice this session; full grammar coverage
  iterates.
• P5b — Statement/OctadSchema C-ABI marshalling.
  A stable wire format pinned by the Phase-4 ABI.Layout/LayoutProofs
  byte-layout proofs; Rust serialiser + a total Idris2 deserialiser
  (in or adjacent to the corpus) with a round-trip property.
• P5c — Idris2 -> C build + link.
  Idris2 RefC backend builds Checker.certifiedLevel (proof-gated
  mint) into a C-callable lib; the Zig shim (ffi/zig/src/lib.zig,
  currently fail-closed) calls parser -> marshal -> certifier. Wire
  into Justfile + guix.scm (primary) / flake.nix (fallback) + CI.
• P5d — signed attestation contract + ADR + stance RESOLVED.
  Certifier signs (sha256(query), schema_id, level); consumer-side
  verify path; ADR docs/decisions/0002-ffi-attestation-trust-boundary.adoc;
  flip the FFI OWED items in VERIFICATION-STANCE.adoc to RESOLVED and
  update consumer guidance; key-management noted in the ADR.

Acceptance (whole workstream)

vclut_verify_query("SELECT ... FROM ...", schema_id) returns a signed
attestation whose level is structurally gated behind a real
certifyRequested certificate (no proof-escape), the parser is
panic-free/total under CI, the marshalling round-trip is property-tested,
and the trust boundary is documented in an ADR. Build oracle unchanged
(idris2 --build vclut-core.ipkg, exit 0, zero escapes). The doc nit
(PROOF-NEEDS.md describing the ReScript bridge as connecting to the
Idris2/Rust core — it does not) is corrected as part of P5a.

Starting P5a now on branch reinforce/vclut-25-phase5a-rust-parser.