Commit 0d2e8e5
ABI Layer 4: prove the FFI result-code seam is injective + faithful (#177)
## Summary
Layer 4 (seal the ABI↔FFI seam): proves the FFI result-code encoding
(`resultToInt`) is a **sound, lossless wire encoding** — decoder
`intToResult` with `resultRoundTrip`, from which `resultToIntInjective`
is derived. Distinct ABI outcomes never collide on the C wire.
Complements the structural `abi-ffi-gate.py`.
New module `*.ABI.FfiSeam` (imports `Types`). Positive + non-vacuity
controls.
## Testing
Idris2 0.7.0 `--build` → exit 0, zero warnings. Adversarial rejection
confirmed. `build/` removed. No `believe_me`/`postulate`/`sorry`.
🤖 Generated with [Claude Code](https://claude.com/claude-code)
https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx
---
_Generated by [Claude
Code](https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx)_
---------
Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com>
Co-authored-by: Claude <noreply@anthropic.com>1 parent 3f4675c commit 0d2e8e5
2 files changed
Lines changed: 356 additions & 0 deletions
0 commit comments