Skip to content

Commit a7ba064

Browse files
claudeclaude
committed
abi: seal ABI<->FFI seam with Layer-4 soundness proof (Halideiser.ABI.FfiSeam)
Prove the FFI Result encoding is sound: resultToInt round-trips through a decoder intToResult (resultRoundTrip) and is therefore injective (resultToIntInjective, derived via justInj+cong). Adds positive decode controls and a machine-checked non-vacuity control (Ok and Error encode to distinct ints). Genuine proof: no believe_me/postulate/assert_total. %default total, zero warnings. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx
1 parent 222c50b commit a7ba064

2 files changed

Lines changed: 142 additions & 0 deletions

File tree

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

Lines changed: 141 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,141 @@
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 for halideiser.
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+value. This module is
8+
||| the PROOF-SIDE complement: it shows the on-the-wire encoding is SOUND.
9+
|||
10+
||| * `resultToInt` is INJECTIVE — distinct ABI outcomes never collide on
11+
||| the C integer they are transmitted as.
12+
||| * a decoder `intToResult` exists and the encoding ROUND-TRIPS losslessly
13+
||| (`intToResult (resultToInt r) = Just r`), so the C integer faithfully
14+
||| reconstructs the ABI value on the far side of the seam.
15+
|||
16+
||| Injectivity is then DERIVED from the round-trip (the cleanest route):
17+
||| if two results encode to the same int, applying the decoder to both
18+
||| sides yields `Just a = Just b`, and `Just` is injective.
19+
|||
20+
||| Genuine proof only: no believe_me / postulate / assert_total / idris_crash.
21+
22+
module Halideiser.ABI.FfiSeam
23+
24+
import Halideiser.ABI.Types
25+
26+
%default total
27+
28+
--------------------------------------------------------------------------------
29+
-- Local lemma: Just is injective
30+
--------------------------------------------------------------------------------
31+
32+
||| Total extractor with an explicit fallback, used to make `Just` injective
33+
||| via `cong`. The fallback is supplied so `fromMaybe` is total.
34+
private
35+
fromMaybe : ty -> Maybe ty -> ty
36+
fromMaybe _ (Just x) = x
37+
fromMaybe d Nothing = d
38+
39+
||| `Just` is injective. Proved by `cong` through `fromMaybe a`, which maps
40+
||| `Just a` to `a` and `Just b` to `b`.
41+
private
42+
justInj : {a, b : ty} -> Just a = Just b -> a = b
43+
justInj prf = cong (fromMaybe a) prf
44+
45+
--------------------------------------------------------------------------------
46+
-- Decoder
47+
--------------------------------------------------------------------------------
48+
49+
||| Decode a C integer back into a `Result`.
50+
|||
51+
||| Built with boolean `==` on concrete `Bits32` literals (rather than
52+
||| pattern-matching on literals) so that the round-trip equations below
53+
||| reduce definitionally and check by `Refl`.
54+
public export
55+
intToResult : Bits32 -> Maybe Result
56+
intToResult x =
57+
if x == 0 then Just Ok
58+
else if x == 1 then Just Error
59+
else if x == 2 then Just InvalidParam
60+
else if x == 3 then Just OutOfMemory
61+
else if x == 4 then Just NullPointer
62+
else if x == 5 then Just CompileFailed
63+
else if x == 6 then Just InvalidSchedule
64+
else if x == 7 then Just DimensionMismatch
65+
else Nothing
66+
67+
--------------------------------------------------------------------------------
68+
-- Round-trip (faithful / lossless encoding)
69+
--------------------------------------------------------------------------------
70+
71+
||| The encoding round-trips: decoding the encoded value of any `Result`
72+
||| recovers exactly that `Result`. This is the load-bearing seam guarantee.
73+
export
74+
resultRoundTrip : (r : Result) -> intToResult (resultToInt r) = Just r
75+
resultRoundTrip Ok = Refl
76+
resultRoundTrip Error = Refl
77+
resultRoundTrip InvalidParam = Refl
78+
resultRoundTrip OutOfMemory = Refl
79+
resultRoundTrip NullPointer = Refl
80+
resultRoundTrip CompileFailed = Refl
81+
resultRoundTrip InvalidSchedule = Refl
82+
resultRoundTrip DimensionMismatch = Refl
83+
84+
--------------------------------------------------------------------------------
85+
-- Injectivity (derived from the round-trip)
86+
--------------------------------------------------------------------------------
87+
88+
||| `resultToInt` is injective: distinct ABI outcomes never share a wire code.
89+
|||
90+
||| Proof: if `resultToInt a = resultToInt b`, then applying the decoder to
91+
||| both sides (via `cong`) gives `intToResult (resultToInt a)
92+
||| = intToResult (resultToInt b)`. Rewriting both ends with the round-trip
93+
||| yields `Just a = Just b`, whose `Just`-injectivity delivers `a = b`.
94+
export
95+
resultToIntInjective : (a, b : Result) -> resultToInt a = resultToInt b -> a = b
96+
resultToIntInjective a b prf =
97+
justInj $
98+
rewrite sym (resultRoundTrip a) in
99+
rewrite sym (resultRoundTrip b) in
100+
cong intToResult prf
101+
102+
--------------------------------------------------------------------------------
103+
-- Positive controls (concrete decodes, machine-checked by Refl)
104+
--------------------------------------------------------------------------------
105+
106+
||| Decoding 0 yields Ok.
107+
export
108+
decodeZeroIsOk : intToResult 0 = Just Ok
109+
decodeZeroIsOk = Refl
110+
111+
||| Decoding 7 yields DimensionMismatch (the last code).
112+
export
113+
decodeSevenIsDimensionMismatch : intToResult 7 = Just DimensionMismatch
114+
decodeSevenIsDimensionMismatch = Refl
115+
116+
||| Decoding an out-of-range code fails (no spurious `Result` is invented).
117+
export
118+
decodeOutOfRangeIsNothing : intToResult 8 = Nothing
119+
decodeOutOfRangeIsNothing = Refl
120+
121+
||| A concrete round-trip instance.
122+
export
123+
roundTripCompileFailed : intToResult (resultToInt CompileFailed) = Just CompileFailed
124+
roundTripCompileFailed = Refl
125+
126+
--------------------------------------------------------------------------------
127+
-- Negative / non-vacuity control
128+
--------------------------------------------------------------------------------
129+
130+
||| Distinct primitive `Bits32` literals are provably unequal; the coverage
131+
||| checker discharges `Refl impossible`.
132+
distinctCodes : Not (the Bits32 0 = 1)
133+
distinctCodes = \case Refl impossible
134+
135+
||| NON-VACUITY: two DISTINCT result codes really do encode to DISTINCT ints.
136+
||| If `resultToInt Ok = resultToInt Error` held, then `0 = 1` would hold —
137+
||| which `distinctCodes` refutes. This proves the seam is not trivially
138+
||| satisfiable (e.g. by a constant encoder).
139+
export
140+
okEncodesDistinctlyFromError : Not (resultToInt Ok = resultToInt Error)
141+
okEncodesDistinctlyFromError prf = distinctCodes prf

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

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

0 commit comments

Comments
 (0)