[#446 Tier 1 #5 follow-up] Idris2 ABI proof-carrier doc for wasm_export_call

[hyperpolymath]

Context

Closed #455 (the WASM-exports calling pattern kickoff) shipped via PR #467 with the Deno-ESM lowering of wasm_export_call + the WasmValue opaque type.

Per the owner's Option-B scope breakdown, the Idris2 ABI pattern doc was deferred to a follow-up per the estate directive "Zig = APIs + FFIs, Idris2 = ABIs":

Idris2 ABI: pattern doc per estate convention (Zig=APIs/FFIs, Idris2=ABIs)

This issue tracks that.

Scope

A proof-carrier-shaped Idris2 ABI document for the wasm_export_call surface and its WasmValue tagged scalar. The general estate Idris2-ABI pattern is documented at docs/reference/ABI-FFI.md (RSR-template form, project-agnostic); this issue specialises it for the wasm-exports binding.

What to ship

A new spec under docs/specs/ (suggested: wasm-export-call-idris2-abi.adoc) covering:

• Idris2-side type signatures for WasmValue as a dependent or refinement-shaped carrier (WasmI32 : Bits32 -> WasmValue, etc.), expressing the four-variant kind discipline that the JS/Zig FFI implementations check at runtime.
• Proof obligation for wasm_export_call's name-lookup-by-string side condition (export name resolves; failure mode is Option<WasmValue> or Result<WasmValue, WasmCallErr>).
• Marshalling proof linking the Idris2 ABI's typed surface to the Zig FFI's untagged WasmValueRepr (paired with the Zig dispatcher in the sister follow-up).
• Layout proof for the i64 case (BigInt on Deno-ESM, native i64 on Zig wasm host) — ensures the host-language round-trip is lossless.
• DOC-DEDUP boundary against docs/reference/ABI-FFI.md (general pattern) + docs/specs/zig-ffi-patterns.adoc (FFI half) + bindings-roadmap.adoc row 41 (Idris2 ABI Tier 5 binding).

Acceptance

• Doc lands under docs/specs/ with proper DOC-FORMAT + SPDX header.
• Cross-referenced from bindings-roadmap.adoc (Tier 5 row Document the migration story for code that needs algebraic effect handling #41) and from the Zig-FFI patterns doc.
• Idris2 source skeleton (or actual .idr file under idris2/abi/ if the tree has that convention) referenced and committed.

Refs

• Closed kickoff: [#446 Tier 1 #5] WASM-exports calling pattern (recommended kickoff) #455
• Shipped surface: PR feat(stdlib): WasmValue + wasm_export_call typed wasm-exports binding (closes #455) #467 (Deno-ESM lowering)
• Companion FFI half follow-up: (this issue's Zig sibling)
• General Idris2-ABI doc: docs/reference/ABI-FFI.md (template)
• Zig-FFI patterns doc: docs/specs/zig-ffi-patterns.adoc (PR Roadmap tracking + Zig-FFI doc (#19) + hex/base64 encoding (#25) + Int-division codegen fix (#478) #474)
• Umbrella: [campaign] AffineScript top-50 framework bindings roadmap (UMBRELLA) #446 (Tier 1 — idaptik blockers; cross-axis to Tier 5 Document the migration story for code that needs algebraic effect handling #41)
• Tier sub-issue: [#446 STEP 2] Tier 1 — idaptik blockers (10 bindings) #450
• Estate directive: "Idris2 = ABIs"