test: Zig FFI (18 exports, 16 connectors) has no CI gate; Idris2 ABI duplicated byte-for-byte

[hyperpolymath]

Two languages in this repo carry correctness claims that no gate checks.

Zig FFI is entirely ungated

ffi/zig/ holds 20+ files: main.zig with 18 export fn declarations, hexadeca.zig, and 16 protocol connectors (grpc, graphql, capnproto, flatbuffers, arrow_flight, mqtt, ipfs, …).

grep -rn zig .github/workflows/*.yml returns only incidental --include='*.zig' grep filters in dogfood-gate.yml and language-blockers.yml. There is no zig build and no zig build test in any workflow. Justfile:94 has cd ffi/zig && zig build, never invoked by CI.

So the C ABI compatibility invariant in MUST.contractile is unverified by anything, and a breaking change to any of the 18 exports would land silently.

Idris2 ABI sources are duplicated byte-for-byte

src/Hypatia/ABI/{FFI,GRPC,GraphQL,REST,RuleEngine,Types}.idr and src/abi/{same six}.idr are all six pairs diff-identical.

src/abi/hypatia-abi.ipkg:17 sets sourcedir = ".." and resolves modules as Hypatia.ABI.* — so src/Hypatia/ABI/ is what actually compiles, and src/abi/*.idr is a six-file copy that nothing builds. Divergence between them is undetectable today, and every doc that pointed at the ABI pointed at the dead copy until the 2026-08-07 docs pass.

Fix: delete src/abi/*.idr, keep src/abi/hypatia-abi.ipkg and src/abi/README.adoc.

For contrast — the proof gate itself is genuine

Worth recording, since fake gates are a recurring estate problem: verify-proofs.yml is not one. It runs a real per-file loop under set -euo pipefail with failure counting and exit 1, real idris2 --build of both ipkgs, a real lake build, and a real TLC model-check. Last three runs on main: success. No || true, no continue-on-error.

Escape-hatch counts are also better than documented: across 22 .idr files there are 0 assert_total, 0 postulate, 0 %hint, and the 8 believe_me hits are all non-executing (4 in comments carrying an explicit -- hypatia: allow pragma, 4 in a deliberate scanner fixture). The 5 Lean proofs contain no sorry.

Two consequences:

• AFFIRMATION.adoc's "zero escape hatches" claim should be scoped to "outside test/soundness/fixtures/" to be exactly true.
• docs/proof-debt.md is stale: it instructs readers to run scripts/check-trusted-base.sh and claims a check-trusted-base CI job enforces annotation. Neither exists. Its headline count is derived from "agent worktrees under .claude/worktrees/", a directory that no longer exists.

Evidence: docs/DEBT-REGISTER.md (P-1, P-2, P-3, C-4).