Skip to content

Commit ab9ee37

Browse files
claudeclaude
committed
abi: add Layer 4 FfiSeam proof sealing ABI<->FFI result-code seam
Prove the Result FFI result-code encoding is sound: - resultToIntInjective: distinct ABI outcomes never collide on the wire (direct nested-case proof, off-diagonals refuted via Refl impossible). - intToResult + resultRoundTrip: faithful, lossless decoding (Refl-checked). - roundTripInjective: injectivity derived from the round-trip via a local Just-injectivity lemma + cong. - Positive controls (decode 0->Ok, 7->ShapeMismatch, 8->Nothing) and non-vacuity controls (Ok/Error and Ok/ShapeMismatch ints distinct). No ProofStatus/statusToInt in this repo, so part (c) is vacuous. Genuine total proof; no believe_me/postulate/assert_total/idris_crash. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx
1 parent a31ce65 commit ab9ee37

2 files changed

Lines changed: 201 additions & 0 deletions

File tree

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

Lines changed: 200 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,200 @@
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 proof for Futharkiser.
5+
|||
6+
||| The structural gate (scripts/abi-ffi-gate.py) checks that the Idris
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+
||| (a) `resultToIntInjective` — distinct ABI outcomes never collide on the
11+
||| wire: if two `Result`s encode to the same C integer, they are equal.
12+
||| (b) `intToResult` / `resultRoundTrip` — the encoding is faithful and
13+
||| lossless: decoding the encoded integer recovers the original value.
14+
|||
15+
||| Together these certify that the C integer crossing the FFI boundary
16+
||| faithfully round-trips back to the ABI value, with no aliasing.
17+
|||
18+
||| The repo's only canonical FFI result-code encoder in the ABI Types module
19+
||| is `resultToInt`; there is no `ProofStatus`/`statusToInt` here, so part (c)
20+
||| of the seam mandate is vacuous for this repo.
21+
22+
module Futharkiser.ABI.FfiSeam
23+
24+
import Futharkiser.ABI.Types
25+
26+
%default total
27+
28+
--------------------------------------------------------------------------------
29+
-- Primitive Bits32 disequality helpers
30+
--------------------------------------------------------------------------------
31+
32+
||| Distinct primitive Bits32 literals are provably unequal. Idris's coverage
33+
||| checker discharges `Refl impossible` for distinct primitive constants, so
34+
||| each pair we actually need can be refuted directly at the use site below.
35+
36+
--------------------------------------------------------------------------------
37+
-- (a) Injectivity of the encoding (proved directly)
38+
--------------------------------------------------------------------------------
39+
40+
||| The result-code encoding is injective: if two outcomes encode to the same
41+
||| C integer they must be the same outcome. Distinct outcomes therefore never
42+
||| collide on the wire. Proved by nested case on both results: the diagonal is
43+
||| `Refl`; every off-diagonal case is refuted because the two distinct integer
44+
||| literals cannot be equal (`\case Refl impossible`).
45+
public export
46+
resultToIntInjective : (a, b : Result) ->
47+
resultToInt a = resultToInt b -> a = b
48+
resultToIntInjective Ok Ok _ = Refl
49+
resultToIntInjective Error Error _ = Refl
50+
resultToIntInjective InvalidParam InvalidParam _ = Refl
51+
resultToIntInjective OutOfMemory OutOfMemory _ = Refl
52+
resultToIntInjective NullPointer NullPointer _ = Refl
53+
resultToIntInjective CompilationFailed CompilationFailed _ = Refl
54+
resultToIntInjective BackendUnavailable BackendUnavailable _ = Refl
55+
resultToIntInjective ShapeMismatch ShapeMismatch _ = Refl
56+
resultToIntInjective Ok Error prf = case prf of Refl impossible
57+
resultToIntInjective Ok InvalidParam prf = case prf of Refl impossible
58+
resultToIntInjective Ok OutOfMemory prf = case prf of Refl impossible
59+
resultToIntInjective Ok NullPointer prf = case prf of Refl impossible
60+
resultToIntInjective Ok CompilationFailed prf = case prf of Refl impossible
61+
resultToIntInjective Ok BackendUnavailable prf = case prf of Refl impossible
62+
resultToIntInjective Ok ShapeMismatch prf = case prf of Refl impossible
63+
resultToIntInjective Error Ok prf = case prf of Refl impossible
64+
resultToIntInjective Error InvalidParam prf = case prf of Refl impossible
65+
resultToIntInjective Error OutOfMemory prf = case prf of Refl impossible
66+
resultToIntInjective Error NullPointer prf = case prf of Refl impossible
67+
resultToIntInjective Error CompilationFailed prf = case prf of Refl impossible
68+
resultToIntInjective Error BackendUnavailable prf = case prf of Refl impossible
69+
resultToIntInjective Error ShapeMismatch prf = case prf of Refl impossible
70+
resultToIntInjective InvalidParam Ok prf = case prf of Refl impossible
71+
resultToIntInjective InvalidParam Error prf = case prf of Refl impossible
72+
resultToIntInjective InvalidParam OutOfMemory prf = case prf of Refl impossible
73+
resultToIntInjective InvalidParam NullPointer prf = case prf of Refl impossible
74+
resultToIntInjective InvalidParam CompilationFailed prf = case prf of Refl impossible
75+
resultToIntInjective InvalidParam BackendUnavailable prf = case prf of Refl impossible
76+
resultToIntInjective InvalidParam ShapeMismatch prf = case prf of Refl impossible
77+
resultToIntInjective OutOfMemory Ok prf = case prf of Refl impossible
78+
resultToIntInjective OutOfMemory Error prf = case prf of Refl impossible
79+
resultToIntInjective OutOfMemory InvalidParam prf = case prf of Refl impossible
80+
resultToIntInjective OutOfMemory NullPointer prf = case prf of Refl impossible
81+
resultToIntInjective OutOfMemory CompilationFailed prf = case prf of Refl impossible
82+
resultToIntInjective OutOfMemory BackendUnavailable prf = case prf of Refl impossible
83+
resultToIntInjective OutOfMemory ShapeMismatch prf = case prf of Refl impossible
84+
resultToIntInjective NullPointer Ok prf = case prf of Refl impossible
85+
resultToIntInjective NullPointer Error prf = case prf of Refl impossible
86+
resultToIntInjective NullPointer InvalidParam prf = case prf of Refl impossible
87+
resultToIntInjective NullPointer OutOfMemory prf = case prf of Refl impossible
88+
resultToIntInjective NullPointer CompilationFailed prf = case prf of Refl impossible
89+
resultToIntInjective NullPointer BackendUnavailable prf = case prf of Refl impossible
90+
resultToIntInjective NullPointer ShapeMismatch prf = case prf of Refl impossible
91+
resultToIntInjective CompilationFailed Ok prf = case prf of Refl impossible
92+
resultToIntInjective CompilationFailed Error prf = case prf of Refl impossible
93+
resultToIntInjective CompilationFailed InvalidParam prf = case prf of Refl impossible
94+
resultToIntInjective CompilationFailed OutOfMemory prf = case prf of Refl impossible
95+
resultToIntInjective CompilationFailed NullPointer prf = case prf of Refl impossible
96+
resultToIntInjective CompilationFailed BackendUnavailable prf = case prf of Refl impossible
97+
resultToIntInjective CompilationFailed ShapeMismatch prf = case prf of Refl impossible
98+
resultToIntInjective BackendUnavailable Ok prf = case prf of Refl impossible
99+
resultToIntInjective BackendUnavailable Error prf = case prf of Refl impossible
100+
resultToIntInjective BackendUnavailable InvalidParam prf = case prf of Refl impossible
101+
resultToIntInjective BackendUnavailable OutOfMemory prf = case prf of Refl impossible
102+
resultToIntInjective BackendUnavailable NullPointer prf = case prf of Refl impossible
103+
resultToIntInjective BackendUnavailable CompilationFailed prf = case prf of Refl impossible
104+
resultToIntInjective BackendUnavailable ShapeMismatch prf = case prf of Refl impossible
105+
resultToIntInjective ShapeMismatch Ok prf = case prf of Refl impossible
106+
resultToIntInjective ShapeMismatch Error prf = case prf of Refl impossible
107+
resultToIntInjective ShapeMismatch InvalidParam prf = case prf of Refl impossible
108+
resultToIntInjective ShapeMismatch OutOfMemory prf = case prf of Refl impossible
109+
resultToIntInjective ShapeMismatch NullPointer prf = case prf of Refl impossible
110+
resultToIntInjective ShapeMismatch CompilationFailed prf = case prf of Refl impossible
111+
resultToIntInjective ShapeMismatch BackendUnavailable prf = case prf of Refl impossible
112+
113+
--------------------------------------------------------------------------------
114+
-- (b) Faithful (lossless) decoding
115+
--------------------------------------------------------------------------------
116+
117+
||| Decode a C integer back into a `Result`. Built with boolean `==` on
118+
||| concrete `Bits32` literals (which reduces definitionally), so the
119+
||| round-trip lemma's `Refl`s check. Out-of-range integers decode to
120+
||| `Nothing` (no spurious ABI value is invented from the wire).
121+
public export
122+
intToResult : Bits32 -> Maybe Result
123+
intToResult x =
124+
if x == 0 then Just Ok
125+
else if x == 1 then Just Error
126+
else if x == 2 then Just InvalidParam
127+
else if x == 3 then Just OutOfMemory
128+
else if x == 4 then Just NullPointer
129+
else if x == 5 then Just CompilationFailed
130+
else if x == 6 then Just BackendUnavailable
131+
else if x == 7 then Just ShapeMismatch
132+
else Nothing
133+
134+
||| Faithful round-trip: encoding a `Result` and decoding the integer recovers
135+
||| exactly the original value. This certifies the C integer crossing the FFI
136+
||| boundary loses no information.
137+
public export
138+
resultRoundTrip : (r : Result) -> intToResult (resultToInt r) = Just r
139+
resultRoundTrip Ok = Refl
140+
resultRoundTrip Error = Refl
141+
resultRoundTrip InvalidParam = Refl
142+
resultRoundTrip OutOfMemory = Refl
143+
resultRoundTrip NullPointer = Refl
144+
resultRoundTrip CompilationFailed = Refl
145+
resultRoundTrip BackendUnavailable = Refl
146+
resultRoundTrip ShapeMismatch = Refl
147+
148+
||| `Just` is injective (local lemma; not exported by the stdlib used here).
149+
justEq : {0 x, y : Result} -> Just x = Just y -> x = y
150+
justEq Refl = Refl
151+
152+
||| Injectivity DERIVED from the round-trip (independent of the direct proof
153+
||| above): if two results encode equally, decoding both gives the same
154+
||| `Just`, and `Just` is injective. Demonstrates the round-trip is strong
155+
||| enough to imply non-collision on its own.
156+
public export
157+
roundTripInjective : (a, b : Result) ->
158+
resultToInt a = resultToInt b -> a = b
159+
roundTripInjective a b prf =
160+
justEq $
161+
rewrite sym (resultRoundTrip a) in
162+
rewrite sym (resultRoundTrip b) in
163+
cong intToResult prf
164+
165+
--------------------------------------------------------------------------------
166+
-- Positive controls (concrete decodes, machine-checked)
167+
--------------------------------------------------------------------------------
168+
169+
||| Positive control: the integer 0 decodes to `Ok`.
170+
public export
171+
decodeOk : intToResult 0 = Just Ok
172+
decodeOk = Refl
173+
174+
||| Positive control: the integer 7 decodes to `ShapeMismatch` (the top code).
175+
public export
176+
decodeShapeMismatch : intToResult 7 = Just ShapeMismatch
177+
decodeShapeMismatch = Refl
178+
179+
||| Positive control: an out-of-range integer decodes to `Nothing` (the wire
180+
||| cannot smuggle in an undefined ABI outcome).
181+
public export
182+
decodeOutOfRange : intToResult 8 = Nothing
183+
decodeOutOfRange = Refl
184+
185+
--------------------------------------------------------------------------------
186+
-- Negative / non-vacuity control (machine-checked)
187+
--------------------------------------------------------------------------------
188+
189+
||| Non-vacuity: two DISTINCT result codes have DISTINCT integer encodings.
190+
||| If this were not machine-checkable, injectivity could hold vacuously. The
191+
||| coverage checker discharges the impossible `Refl` for distinct primitive
192+
||| `Bits32` constants (0 vs 1), so the disequality is genuinely inhabited.
193+
public export
194+
okErrorDistinct : Not (resultToInt Ok = resultToInt Error)
195+
okErrorDistinct = \case Refl impossible
196+
197+
||| A second non-vacuity witness across a non-adjacent pair (0 vs 7).
198+
public export
199+
okShapeMismatchDistinct : Not (resultToInt Ok = resultToInt ShapeMismatch)
200+
okShapeMismatchDistinct = \case Refl impossible

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

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

0 commit comments

Comments
 (0)