Skip to content

Commit 5b37667

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
ABI Layer 4: prove the FFI result-code seam is injective + faithful (#39)
## Summary Layer 4 (seal the ABI↔FFI seam): proves the FFI result-code encoding (`resultToInt`) is a **sound, lossless wire encoding** — a decoder `intToResult` with `resultRoundTrip : intToResult (resultToInt r) = Just r`, from which `resultToIntInjective` is derived. Distinct ABI outcomes never collide on the C wire; the C integer always recovers the exact ABI value. 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: a false `resultToInt Ok = resultToInt Error` was rejected. `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 befb22e commit 5b37667

2 files changed

Lines changed: 131 additions & 0 deletions

File tree

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

Lines changed: 130 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,130 @@
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 — ABI<->FFI seam soundness proofs for Affinescriptiser.
5+
|||
6+
||| The structural gate (scripts/abi-ffi-gate.py) checks that the Idris2
7+
||| `Result` enum and the Zig FFI enum agree by name and value. This module
8+
||| supplies the PROOF-SIDE guarantee that the encoding itself is sound:
9+
|||
10+
||| * `resultToIntInjective` — distinct ABI outcomes never collide on the
11+
||| wire (the encoding is unambiguous).
12+
||| * `intToResult` + `resultRoundTrip` — the C integer faithfully
13+
||| round-trips back to the exact ABI value (the encoding is lossless).
14+
|||
15+
||| Injectivity is then DERIVED from the round-trip via `justInjective . cong`,
16+
||| so the two guarantees share a single source of truth.
17+
|||
18+
||| The decoder is written with boolean `Bits32` equality (`if x == n`), which
19+
||| reduces on concrete literals, so each `resultRoundTrip r = Refl` checks
20+
||| definitionally.
21+
22+
module Affinescriptiser.ABI.FfiSeam
23+
24+
import Affinescriptiser.ABI.Types
25+
26+
%default total
27+
28+
--------------------------------------------------------------------------------
29+
-- Local helper: Just is injective
30+
--------------------------------------------------------------------------------
31+
32+
||| `Just` is injective: equal options carrying `Just` have equal payloads.
33+
||| Proved here directly (rather than imported) so the module's only
34+
||| dependency is the ABI Types it certifies.
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` value.
44+
||| Built with boolean `Bits32` equality so the encode/decode round-trip
45+
||| reduces definitionally on the concrete literals 0..6.
46+
public export
47+
intToResult : Bits32 -> Maybe Result
48+
intToResult x =
49+
if x == 0 then Just Ok
50+
else if x == 1 then Just Error
51+
else if x == 2 then Just InvalidParam
52+
else if x == 3 then Just OutOfMemory
53+
else if x == 4 then Just NullPointer
54+
else if x == 5 then Just AffineViolation
55+
else if x == 6 then Just ResourceLeak
56+
else Nothing
57+
58+
--------------------------------------------------------------------------------
59+
-- Round-trip: encoding is faithful / lossless
60+
--------------------------------------------------------------------------------
61+
62+
||| The C integer faithfully round-trips back to the exact ABI value.
63+
||| `intToResult (resultToInt r) = Just r` for every result code.
64+
public export
65+
resultRoundTrip : (r : Result) -> intToResult (resultToInt r) = Just r
66+
resultRoundTrip Ok = Refl
67+
resultRoundTrip Error = Refl
68+
resultRoundTrip InvalidParam = Refl
69+
resultRoundTrip OutOfMemory = Refl
70+
resultRoundTrip NullPointer = Refl
71+
resultRoundTrip AffineViolation = Refl
72+
resultRoundTrip ResourceLeak = Refl
73+
74+
--------------------------------------------------------------------------------
75+
-- Injectivity: distinct outcomes never collide on the wire
76+
--------------------------------------------------------------------------------
77+
78+
||| The encoding is unambiguous: equal C integers imply equal ABI outcomes.
79+
||| Derived from the round-trip — if `resultToInt a = resultToInt b` then
80+
||| `Just a = Just b` (by `cong intToResult` + round-trip rewriting), and
81+
||| `justInjective` strips the `Just`.
82+
public export
83+
resultToIntInjective : (a, b : Result)
84+
-> resultToInt a = resultToInt b
85+
-> a = b
86+
resultToIntInjective a b prf =
87+
justInj $
88+
rewrite sym (resultRoundTrip a) in
89+
rewrite sym (resultRoundTrip b) in
90+
cong intToResult prf
91+
92+
--------------------------------------------------------------------------------
93+
-- Positive controls (concrete decodes, machine-checked)
94+
--------------------------------------------------------------------------------
95+
96+
||| Decoding 0 yields Ok.
97+
public export
98+
decodeZeroIsOk : intToResult 0 = Just Ok
99+
decodeZeroIsOk = Refl
100+
101+
||| Decoding 6 yields ResourceLeak (the highest code).
102+
public export
103+
decodeSixIsResourceLeak : intToResult 6 = Just ResourceLeak
104+
decodeSixIsResourceLeak = Refl
105+
106+
||| An out-of-range code (7) decodes to Nothing (no spurious value).
107+
public export
108+
decodeSevenIsNothing : intToResult 7 = Nothing
109+
decodeSevenIsNothing = Refl
110+
111+
--------------------------------------------------------------------------------
112+
-- Negative / non-vacuity control
113+
--------------------------------------------------------------------------------
114+
115+
||| Non-vacuity: two DISTINCT result codes encode to DISTINCT C integers.
116+
||| If `resultToInt Ok = resultToInt Error` then by injectivity `Ok = Error`,
117+
||| which is refuted by coverage. This guards against a degenerate encoder
118+
||| that maps everything to the same wire value.
119+
public export
120+
okErrorDistinctOnWire : Not (resultToInt Ok = resultToInt Error)
121+
okErrorDistinctOnWire prf = case resultToIntInjective Ok Error prf of
122+
Refl impossible
123+
124+
||| A second distinct pair, proved directly from the primitive literals:
125+
||| the C integer 5 (AffineViolation) is not the C integer 6 (ResourceLeak).
126+
public export
127+
affineViolationResourceLeakDistinct
128+
: Not (resultToInt AffineViolation = resultToInt ResourceLeak)
129+
affineViolationResourceLeakDistinct prf = case resultToIntInjective AffineViolation ResourceLeak prf of
130+
Refl impossible

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,3 +9,4 @@ modules = Affinescriptiser.ABI.Types
99
, Affinescriptiser.ABI.Proofs
1010
, Affinescriptiser.ABI.Semantics
1111
, Affinescriptiser.ABI.Invariants
12+
, Affinescriptiser.ABI.FfiSeam

0 commit comments

Comments
 (0)