Earn-core: formal-proof runtime-enforcement PoC for one ABI module (ADR-0008 Option C)

[hyperpolymath]

Context

ADR-0008 was decided: Option C (hybrid). Two consequences flow from it; this issue tracks the second.

1. Scope the claim now — the "formally verified" wording is corrected to "ABI proofs compile/type-check; runtime enforcement is roadmap." Handled under the doc-reality audit Earn-core: doc-reality claim audit (claims → code+test or labelled experimental) #51 / ADR-0007.
2. Schedule a single-module enforcement PoC — this issue.

Problem

The six Idris2 ABI proof modules compile and type-check, but none is enforced at the Elixir/Zig runtime boundary (Burble.Verification.Avow is data-type-only — BURBLE-PROOF-STATUS.md, READINESS.adoc). ADR-0008 Option C commits to proving the enforcement bridge is viable on one high-value module before committing to the full bridge.

Scope (deliberately one module)

• Select the PoC module — Avow (attestation-chain non-circularity; security-relevant, currently the explicit data-type-only gap) or Permissions (capability lattice). Decide in the first task; document why.
• Build a proof-derived validator at the Elixir↔Zig ABI boundary for that module: values violating the proven invariants are rejected at runtime, not merely typed.
• Property tests demonstrating rejected/accepted cases align with the Idris2 proof.
• Telemetry + a short design note (docs/...) on the bridge mechanism, so the full-bridge go/no-go has real data.

Exit criteria

A working enforcement bridge for one module + a written recommendation: extend to all modules (Route B "Majestic" moat), or stop at PoC and keep proofs as design assurance. That recommendation closes ADR-0008's follow-through.

References

ADR-0008 (Accepted, Option C), ADR-0007, BURBLE-PROOF-STATUS.md, PROOF-NEEDS.md, verification/. Part of the Earn-the-Core epic #53.

[hyperpolymath]

Tracked under the Earn-the-Core epic #53; implements ADR-0008 Option C.

[hyperpolymath]

Decision (2026-05-19): PoC module = Avow. Per ADR-0008 Option C, the single-module runtime-enforcement proof-of-concept targets Burble.ABI.Avow (attestation-chain non-circularity — the explicit data-type-only gap in BURBLE-PROOF-STATUS, and security-relevant). Burble.ABI.Avow compiles clean under idris2 0.8.0 (verified, PR #61), so the PoC starts from a green proof. Scope unchanged: build the Idris2→Elixir/Zig enforcement bridge for Avow only; report a full-bridge go/no-go. Blocked by: #60 is independent; this needs the green proof (have it) — proceed when scheduled.