abi(nimiser): prove C-binding signature preservation (Layer 2)

Add Nimiser.ABI.Semantics, a machine-checked semantic proof that the
Nim->C code generator preserves source signatures: same name, same
arity, and every argument/return type lowered by the canonical injective
nimToC mapping. An arity or type mismatch is unrepresentable as a
SigPreserved witness.

Contents:
- Faithful model: NimT / CT type universes, NimSig / CSig signatures,
  total nimToC lowering, genBinding code generator.
- Headline property SigPreserved with no constructor for any mismatch.
- genBindingPreserves: the generator ALWAYS preserves (soundness).
- nimToCInjective: the lowering is injective (non-vacuity engine).
- decSigPreserved: sound + complete Dec decision procedure.
- certifyBinding + certifyBindingSound tied to the project Result type;
  generatedAlwaysCertifies corollary.
- Positive control samplePreserved (explicit witness) and three
  negative controls (wrong return type, wrong arity, wrong arg type),
  all machine-checked.

Build: idris2 --build nimiser-abi.ipkg exits 0, zero warnings.
Adversarial false proof (claiming a type-mismatched binding is
preserved) is rejected by the type-checker, confirming non-vacuity.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx

Author: claude