Skip to content

Commit bb2b581

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
ABI Layer 4: prove the FFI result-code seam is injective + faithful (#44)
## 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 7ac70ae commit bb2b581

2 files changed

Lines changed: 133 additions & 0 deletions

File tree

‎src/interface/abi/Idrisiser/ABI/FfiSeam.idr‎

Lines changed: 132 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,132 @@
1+
-- SPDX-License-Identifier: MPL-2.0
2+
-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
3+
--
4+
||| Layer 4 — Sealing the ABI<->FFI seam.
5+
|||
6+
||| The structural gate (scripts/abi-ffi-gate.py) checks that the Idris2 and
7+
||| Zig result-code enums agree by name and value. This module supplies the
8+
||| PROOF-SIDE guarantee that the encoding `resultToInt : Result -> Bits32`
9+
||| is SOUND:
10+
|||
11+
||| * distinct ABI outcomes never collide on the wire (injectivity), and
12+
||| * the C integer faithfully round-trips back to the ABI value
13+
||| (a total decoder `intToResult` with `intToResult (resultToInt r) = Just r`).
14+
|||
15+
||| Injectivity is DERIVED from the round-trip (the cleanest route): if
16+
||| `resultToInt a = resultToInt b` then applying `intToResult` to both sides
17+
||| (via `cong`) and using the round-trip identities forces `Just a = Just b`,
18+
||| whence `a = b` by injectivity of `Just`.
19+
|||
20+
||| The decoder is built with boolean `Bits32` `==` (which reduces on concrete
21+
||| literals) so the round-trip proofs discharge by `Refl`.
22+
23+
module Idrisiser.ABI.FfiSeam
24+
25+
import Idrisiser.ABI.Types
26+
27+
%default total
28+
29+
--------------------------------------------------------------------------------
30+
-- Local helper: Just is injective
31+
--------------------------------------------------------------------------------
32+
33+
||| `Just` is injective. Proved locally to avoid depending on a particular
34+
||| base-library name; the single `Refl` clause forces the two payloads equal.
35+
private
36+
justInj : {0 x, y : a} -> Just x = Just y -> x = y
37+
justInj Refl = Refl
38+
39+
--------------------------------------------------------------------------------
40+
-- Decoder: C integer -> ABI Result
41+
--------------------------------------------------------------------------------
42+
43+
||| Decode a C result code back into the ABI `Result`.
44+
|||
45+
||| Built with chained boolean `==` on `Bits32` rather than literal
46+
||| pattern-matching: `==` reduces definitionally on concrete constants, so the
47+
||| round-trip lemmas below check by `Refl`. Any integer outside the known
48+
||| range decodes to `Nothing` (faithful: the encoder is not surjective).
49+
public export
50+
intToResult : Bits32 -> Maybe Result
51+
intToResult x =
52+
if x == 0 then Just Ok
53+
else if x == 1 then Just Error
54+
else if x == 2 then Just InvalidParam
55+
else if x == 3 then Just OutOfMemory
56+
else if x == 4 then Just NullPointer
57+
else if x == 5 then Just ProofFailure
58+
else Nothing
59+
60+
--------------------------------------------------------------------------------
61+
-- (b) Faithful / lossless round-trip
62+
--------------------------------------------------------------------------------
63+
64+
||| Encoding then decoding recovers the original ABI value: the C integer is a
65+
||| faithful representation of every `Result`. Each clause reduces because the
66+
||| corresponding `==` test on the concrete literal evaluates to `True`.
67+
export
68+
resultRoundTrip : (r : Result) -> intToResult (resultToInt r) = Just r
69+
resultRoundTrip Ok = Refl
70+
resultRoundTrip Error = Refl
71+
resultRoundTrip InvalidParam = Refl
72+
resultRoundTrip OutOfMemory = Refl
73+
resultRoundTrip NullPointer = Refl
74+
resultRoundTrip ProofFailure = Refl
75+
76+
--------------------------------------------------------------------------------
77+
-- (a) Injectivity, derived from the round-trip
78+
--------------------------------------------------------------------------------
79+
80+
||| The encoding is unambiguous: distinct outcomes never collide on the wire.
81+
||| Derived from `resultRoundTrip` — no case explosion, no `believe_me`.
82+
|||
83+
||| Given `resultToInt a = resultToInt b`, `cong intToResult` yields
84+
||| `intToResult (resultToInt a) = intToResult (resultToInt b)`; rewriting both
85+
||| ends by the round-trip gives `Just a = Just b`, and injectivity of `Just`
86+
||| strips the constructor.
87+
export
88+
resultToIntInjective : (a, b : Result)
89+
-> resultToInt a = resultToInt b
90+
-> a = b
91+
resultToIntInjective a b prf =
92+
justInj $
93+
rewrite sym (resultRoundTrip a) in
94+
rewrite sym (resultRoundTrip b) in
95+
cong intToResult prf
96+
97+
--------------------------------------------------------------------------------
98+
-- Positive controls (concrete decodes, machine-checked)
99+
--------------------------------------------------------------------------------
100+
101+
||| Decoding 0 yields Ok.
102+
decodeZeroIsOk : intToResult 0 = Just Ok
103+
decodeZeroIsOk = Refl
104+
105+
||| Decoding 5 yields ProofFailure (the top of the range).
106+
decodeFiveIsProofFailure : intToResult 5 = Just ProofFailure
107+
decodeFiveIsProofFailure = Refl
108+
109+
||| Decoding an out-of-range code yields Nothing (encoder is not surjective).
110+
decodeOutOfRangeIsNothing : intToResult 99 = Nothing
111+
decodeOutOfRangeIsNothing = Refl
112+
113+
||| Round-trip control for a specific value.
114+
roundTripOk : intToResult (resultToInt Ok) = Just Ok
115+
roundTripOk = Refl
116+
117+
--------------------------------------------------------------------------------
118+
-- Negative / non-vacuity control
119+
--------------------------------------------------------------------------------
120+
121+
||| Two DISTINCT result codes have DISTINCT wire integers. This rules out the
122+
||| vacuous reading of injectivity: the encoding genuinely separates outcomes.
123+
||| `0 = 1` on `Bits32` is refuted by the coverage checker on distinct
124+
||| primitive constants.
125+
export
126+
okWireDistinctFromError : Not (resultToInt Ok = resultToInt Error)
127+
okWireDistinctFromError = \case Refl impossible
128+
129+
||| A second non-vacuity witness across a non-adjacent pair.
130+
export
131+
okWireDistinctFromProofFailure : Not (resultToInt Ok = resultToInt ProofFailure)
132+
okWireDistinctFromProofFailure = \case Refl impossible

‎src/interface/abi/idrisiser-abi.ipkg‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,3 +11,4 @@ modules = Idrisiser.ABI.Types
1111
, Idrisiser.ABI.Proofs
1212
, Idrisiser.ABI.Semantics
1313
, Idrisiser.ABI.Invariants
14+
, Idrisiser.ABI.FfiSeam

0 commit comments

Comments
 (0)