Skip to content

Commit d1aae11

Browse files
claudeclaude
committed
abi: seal ABI<->FFI seam with Layer-4 soundness proof (FfiSeam)
Add Iseriser.ABI.FfiSeam proving the resultToInt encoding is sound: - intToResult decoder + resultRoundTrip (lossless/faithful encoding) - resultToIntInjective derived from round-trip (distinct outcomes never collide on the wire) - positive controls (concrete decodes by Refl) and a machine-checked non-vacuity control (resultToInt Ok /= resultToInt Error) Genuine total proof: no believe_me/postulate/assert_total/etc. Registered in iseriser-abi.ipkg; package builds clean with zero warnings. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx
1 parent ccac6a8 commit d1aae11

2 files changed

Lines changed: 118 additions & 0 deletions

File tree

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

Lines changed: 117 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,117 @@
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 proof: SEALING THE ABI<->FFI SEAM for iseriser.
5+
|||
6+
||| The ABI defines `resultToInt : Result -> Bits32`, the integer the Zig FFI
7+
||| returns to C. The estate's structural gate (`scripts/abi-ffi-gate.py`)
8+
||| checks the Idris and Zig enums agree by name+value. THIS module supplies
9+
||| the PROOF-SIDE guarantee that the encoding is SOUND:
10+
|||
11+
||| * `intToResult` — a decoder Bits32 -> Maybe Result
12+
||| * `resultRoundTrip` — the encoding is faithful/lossless: decoding an
13+
||| encoded result recovers exactly that result
14+
||| * `resultToIntInjective`— distinct ABI outcomes never collide on the wire,
15+
||| DERIVED from the round-trip via cong + justInjective
16+
|||
17+
||| Plus positive controls (concrete decodes by Refl) and a machine-checked
18+
||| NON-VACUITY control (two distinct codes have distinct ints).
19+
20+
module Iseriser.ABI.FfiSeam
21+
22+
import Iseriser.ABI.Types
23+
24+
%default total
25+
26+
--------------------------------------------------------------------------------
27+
-- Decoder: the inverse of resultToInt
28+
--------------------------------------------------------------------------------
29+
30+
||| Decode a C integer back to a `Result`. Built with boolean `==` on Bits32
31+
||| literals (which reduces on concrete constants) so the round-trip `Refl`s
32+
||| check definitionally. Any value outside 0..5 is not a valid ABI code.
33+
public export
34+
intToResult : Bits32 -> Maybe Result
35+
intToResult x =
36+
if x == 0 then Just Ok
37+
else if x == 1 then Just Error
38+
else if x == 2 then Just InvalidLanguage
39+
else if x == 3 then Just TemplateError
40+
else if x == 4 then Just OutputError
41+
else if x == 5 then Just NullPointer
42+
else Nothing
43+
44+
--------------------------------------------------------------------------------
45+
-- Faithfulness: the encoding is lossless (round-trips through the wire)
46+
--------------------------------------------------------------------------------
47+
48+
||| Decoding the encoding of any `Result` recovers exactly that `Result`.
49+
||| Each clause reduces because `resultToInt` produces a concrete Bits32
50+
||| literal and the decoder's boolean `==` chain evaluates on that literal.
51+
public export
52+
resultRoundTrip : (r : Result) -> intToResult (resultToInt r) = Just r
53+
resultRoundTrip Ok = Refl
54+
resultRoundTrip Error = Refl
55+
resultRoundTrip InvalidLanguage = Refl
56+
resultRoundTrip TemplateError = Refl
57+
resultRoundTrip OutputError = Refl
58+
resultRoundTrip NullPointer = Refl
59+
60+
--------------------------------------------------------------------------------
61+
-- Injectivity: distinct ABI outcomes never collide on the wire
62+
--------------------------------------------------------------------------------
63+
64+
||| `Just` is injective: recover the underlying equality from wrapped values.
65+
||| (Local helper to avoid depending on a Prelude name that may not be in
66+
||| scope; the off-diagonal `Just x = Nothing` cannot arise here.)
67+
justEq : {0 x, y : Result} -> Just x = Just y -> x = y
68+
justEq Refl = Refl
69+
70+
||| The encoding is unambiguous: if two results encode to the same integer,
71+
||| they ARE the same result. Derived from the round-trip — applying the
72+
||| decoder to both sides of `resultToInt a = resultToInt b` and chaining the
73+
||| two round-trip facts forces `Just a = Just b`, hence `a = b`.
74+
public export
75+
resultToIntInjective : (a, b : Result) ->
76+
resultToInt a = resultToInt b -> a = b
77+
resultToIntInjective a b prf =
78+
justEq $
79+
trans (sym (resultRoundTrip a))
80+
(trans (cong intToResult prf) (resultRoundTrip b))
81+
82+
--------------------------------------------------------------------------------
83+
-- Positive controls (concrete decodes by Refl)
84+
--------------------------------------------------------------------------------
85+
86+
||| Decoding 0 yields Ok.
87+
decodeZeroIsOk : intToResult 0 = Just Ok
88+
decodeZeroIsOk = Refl
89+
90+
||| Decoding 5 yields NullPointer (the highest valid code).
91+
decodeFiveIsNullPointer : intToResult 5 = Just NullPointer
92+
decodeFiveIsNullPointer = Refl
93+
94+
||| An out-of-range code decodes to Nothing.
95+
decodeSixIsNothing : intToResult 6 = Nothing
96+
decodeSixIsNothing = Refl
97+
98+
||| Concrete round-trip control through the middle of the range.
99+
roundTripTemplateError : intToResult (resultToInt TemplateError) = Just TemplateError
100+
roundTripTemplateError = Refl
101+
102+
--------------------------------------------------------------------------------
103+
-- Negative / non-vacuity control (machine-checked)
104+
--------------------------------------------------------------------------------
105+
106+
||| Distinct primitive Bits32 literals are provably unequal: the coverage
107+
||| checker discharges `Refl impossible` for `0 = 1`.
108+
okIntNotErrorInt : Not (the Bits32 0 = the Bits32 1)
109+
okIntNotErrorInt = \case Refl impossible
110+
111+
||| NON-VACUITY: two DISTINCT result codes have DISTINCT wire integers.
112+
||| `resultToInt Ok = 0` and `resultToInt Error = 1` reduce, so any proof
113+
||| that they are equal would prove `0 = 1`, which is refuted above. This
114+
||| guarantees `resultToIntInjective` is not vacuously true.
115+
public export
116+
okEncodingNotErrorEncoding : Not (resultToInt Ok = resultToInt Error)
117+
okEncodingNotErrorEncoding prf = okIntNotErrorInt prf

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

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

0 commit comments

Comments
 (0)