iseriser: codegen emits verified, compiling Idris2 ABI (P2)

[hyperpolymath]

What & why

iseriser's scaffold generator still emitted the old flat, never-compiled ABI for every new -iser:

• files at src/interface/abi/{Types,Layout,Foreign}.idr whose path did not match their <Mod>.ABI.* namespace,
• a Layout.idr whose So (modNatNZ contextSize 8 SIsNonZero == 0) proof does not reduce at the type level,
• no Proofs.idr and no .ipkg at all.

So every freshly-generated -iser started life with the exact broken ABI a prior session had to hand-fix across the whole family. This closes that regression source (kickoff P2).

Change

Rewrote the Idris2 ABI generators to emit the verified reference pattern (the form proven to compile clean under Idris2 0.7.0, zero warnings, no believe_me/postulate/holes):

• Paths/packaging — nested modules at src/interface/abi/<Mod>/ABI/{Types,Layout,Foreign,Proofs}.idr (path matches namespace) + src/interface/abi/<iser>-abi.ipkg (sourcedir=".", lists all four modules).
• Types.idr — Result with a complete DecEq (explicit off-diagonals, not No absurd); a non-null Handle constructed via choose; a primitive enum with a tag-based Eq that stays warning-free for any number of primitives.
• Layout.idr — real Divides / StructLayout / FieldsAligned machinery and one concrete, provably C-ABI-compliant context layout.
• Proofs.idr — a non-vacuous CABICompliant theorem (each field offset pinned by DivideBy k Refl; qualified layout name so it doesn't auto-bind as an implicit), the result-code round-trip, and a Nat-level negative control.

Verification

• cargo test green (lib + integration).
• New end-to-end test runs idris2 --build on a freshly-generated repo's ABI and asserts a clean, warning-free build (no-ops where idris2 isn't installed, so CI without the toolchain stays green).
• Built the generated ABI with Idris2 0.7.0 by hand for three distinct manifests (Julia/dependent/3 primitives, Chapel, and a digit-in-module-name Idris2iser/1 primitive) — all idris2 --build exit 0, zero warnings.
• Adversarial / non-vacuity check: perturbing a generated field offset (16→17) makes DivideBy 4 Refl fail to typecheck at Proofs.idr, confirming the headline theorem genuinely pins the offsets rather than passing vacuously.
• Fakery scan of generated output: no believe_me / postulate / holes.

Scope / not included

• Per-language deep semantic proofs (kickoff P3) are out of scope here; this unifies all languages on the verified structural ABI, which strictly improves on the previous vacuous DeepProof stub.
• The Zig FFI cross-check (P1) needs Zig 0.14.0, which is currently blocked by the environment proxy (ziglang.org returns 403), so it isn't part of this PR.

🤖 Generated with Claude Code

https://claude.ai/code/session_019xMKB3T4Vo5FYC7Czx3JSH

---

Generated by Claude Code