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

The scaffold generator still emitted the old flat, never-compiled ABI
template: files at `src/interface/abi/{Types,Layout,Foreign}.idr` with a
namespace they didn't match, a `Layout.idr` whose `modNatNZ ... == 0`
proof does not reduce at the type level, no `Proofs.idr`, and no `.ipkg`.
Every newly-generated -iser therefore started with a broken ABI — exactly
the bug a prior session hand-fixed across the family.

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

- Nested modules at `src/interface/abi/<Mod>/ABI/{Types,Layout,Foreign,
  Proofs}.idr` so each file's path matches its namespace, plus
  `src/interface/abi/<iser>-abi.ipkg` (sourcedir=".", lists all four).
- Types: `Result` with a complete `DecEq` (explicit off-diagonals, not
  `No absurd`), a non-null `Handle` built via `choose`, and a primitive
  enum with a tag-based `Eq` that is warning-free for any arity.
- Layout: real `Divides`/`StructLayout`/`FieldsAligned` machinery and one
  concrete, provably C-ABI-compliant context layout.
- Proofs: a non-vacuous `CABICompliant` theorem (each offset pinned by
  `DivideBy k Refl`, qualified layout name so it doesn't auto-bind), the
  result-code round-trip, and a Nat-level negative control. Verified:
  perturbing a field offset makes the proof fail to typecheck.

Tests: assert the generated tree is self-consistent (every ipkg module
present at its namespace path, no leftover template tokens, old flat path
gone) and add an end-to-end test that runs `idris2 --build` on the
generated ABI when the toolchain is present (no-op otherwise, so CI
without idris2 stays green). Update the integration tests for the new
paths and the real proof module.


Claude-Session: https://claude.ai/code/session_019xMKB3T4Vo5FYC7Czx3JSH

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath