Skip to content

Commit c68d317

Browse files
claudeclaude
committed
abi: seal ABI<->FFI seam with Layer 4 soundness proof (FfiSeam)
Add Eclexiaiser.ABI.FfiSeam proving the on-the-wire encoding resultToInt : Result -> Bits32 is sound: - resultRoundTrip: faithful/lossless — a decoder intToResult round-trips every Result through its C integer back to itself. - resultToIntInjective: distinct ABI outcomes never collide on the wire, DERIVED from the round-trip via a local justInj + cong/trans/sym. - Positive controls (concrete decodes = Refl) and two non-vacuity controls (distinct codes -> distinct ints, machine-checked). Genuine proof: no believe_me/postulate/assert_total/sorry. Builds with zero warnings; adversarial false claim (resultToInt Ok = resultToInt Error) is rejected by the checker. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx
1 parent e0782ed commit c68d317

2 files changed

Lines changed: 134 additions & 0 deletions

File tree

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

Lines changed: 133 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,133 @@
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 Eclexiaiser.
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 is
8+
||| the proof-side counterpart: it shows the on-the-wire encoding
9+
||| `resultToInt : Result -> Bits32` is SOUND.
10+
|||
11+
||| Soundness here means two things:
12+
||| 1. FAITHFUL / LOSSLESS — there is a decoder `intToResult` such that
13+
||| every ABI outcome round-trips through the C integer back to itself
14+
||| (`resultRoundTrip`).
15+
||| 2. UNAMBIGUOUS / INJECTIVE — distinct ABI outcomes never collide on the
16+
||| wire (`resultToIntInjective`), DERIVED from the round-trip so the two
17+
||| facts cannot drift apart.
18+
|||
19+
||| Genuine proof only: no believe_me / idris_crash / assert_total / postulate /
20+
||| sorry. Every claim is machine-checked by the totality + coverage checker.
21+
|||
22+
||| @see Eclexiaiser.ABI.Types for the `Result` enum and `resultToInt`.
23+
24+
module Eclexiaiser.ABI.FfiSeam
25+
26+
import Eclexiaiser.ABI.Types
27+
28+
%default total
29+
30+
--------------------------------------------------------------------------------
31+
-- Decoder: C integer -> ABI Result
32+
--------------------------------------------------------------------------------
33+
34+
||| Decode a C integer (as produced by the Zig FFI) back into an ABI `Result`.
35+
||| Unknown codes decode to `Nothing` — the wire format is closed.
36+
|||
37+
||| Built with concrete `==` tests on primitive `Bits32` literals: these reduce
38+
||| definitionally on concrete constants, so the round-trip proofs below check
39+
||| by `Refl`.
40+
public export
41+
intToResult : Bits32 -> Maybe Result
42+
intToResult x =
43+
if x == 0 then Just Ok
44+
else if x == 1 then Just Error
45+
else if x == 2 then Just InvalidParam
46+
else if x == 3 then Just OutOfMemory
47+
else if x == 4 then Just NullPointer
48+
else if x == 5 then Just BudgetExceeded
49+
else if x == 6 then Just CarbonLimitExceeded
50+
else if x == 7 then Just CounterUnavailable
51+
else Nothing
52+
53+
--------------------------------------------------------------------------------
54+
-- (b) Faithful / lossless encoding: the round-trip law
55+
--------------------------------------------------------------------------------
56+
57+
||| FAITHFULNESS: encoding a `Result` to its C integer and decoding it back
58+
||| recovers exactly the original outcome. Nothing is lost across the seam.
59+
export
60+
resultRoundTrip : (r : Result) -> intToResult (resultToInt r) = Just r
61+
resultRoundTrip Ok = Refl
62+
resultRoundTrip Error = Refl
63+
resultRoundTrip InvalidParam = Refl
64+
resultRoundTrip OutOfMemory = Refl
65+
resultRoundTrip NullPointer = Refl
66+
resultRoundTrip BudgetExceeded = Refl
67+
resultRoundTrip CarbonLimitExceeded = Refl
68+
resultRoundTrip CounterUnavailable = Refl
69+
70+
--------------------------------------------------------------------------------
71+
-- (a) Unambiguous encoding: injectivity, DERIVED from the round-trip
72+
--------------------------------------------------------------------------------
73+
74+
||| `Just` is injective — local lemma so injectivity is derived cleanly from the
75+
||| round-trip without depending on a particular base-library name.
76+
||| Both arguments are bound explicitly as erased implicits (no auto-bind warn).
77+
private
78+
justInj : {0 a, b : Result} -> Just a = Just b -> a = b
79+
justInj Refl = Refl
80+
81+
||| UNAMBIGUITY: `resultToInt` is injective — distinct ABI outcomes can never
82+
||| collide on the wire. Derived from `resultRoundTrip`: if two results encode
83+
||| to the same integer, decoding that integer gives the same `Just`, and the
84+
||| round-trip law pins each side back to its own constructor.
85+
export
86+
resultToIntInjective : (a, b : Result) -> resultToInt a = resultToInt b -> a = b
87+
resultToIntInjective a b prf =
88+
justInj $
89+
trans (sym (resultRoundTrip a))
90+
(trans (cong intToResult prf) (resultRoundTrip b))
91+
92+
--------------------------------------------------------------------------------
93+
-- Positive controls (concrete decodes, machine-checked = Refl)
94+
--------------------------------------------------------------------------------
95+
96+
||| The success code 0 decodes to `Ok`.
97+
export
98+
decodeZeroIsOk : intToResult 0 = Just Ok
99+
decodeZeroIsOk = Refl
100+
101+
||| The budget-exceeded code 5 decodes to `BudgetExceeded` (Zig FFI contract).
102+
export
103+
decodeFiveIsBudgetExceeded : intToResult 5 = Just BudgetExceeded
104+
decodeFiveIsBudgetExceeded = Refl
105+
106+
||| The highest defined code 7 decodes to `CounterUnavailable`.
107+
export
108+
decodeSevenIsCounterUnavailable : intToResult 7 = Just CounterUnavailable
109+
decodeSevenIsCounterUnavailable = Refl
110+
111+
||| An out-of-range code decodes to `Nothing` — the wire format is closed.
112+
export
113+
decodeUnknownIsNothing : intToResult 8 = Nothing
114+
decodeUnknownIsNothing = Refl
115+
116+
--------------------------------------------------------------------------------
117+
-- Negative / non-vacuity control
118+
--------------------------------------------------------------------------------
119+
120+
||| NON-VACUITY: two DISTINCT result codes really do encode to DISTINCT
121+
||| integers. Without this, an encoding mapping everything to 0 would satisfy
122+
||| injectivity vacuously. Machine-checked: 0 = 1 is refuted by the coverage
123+
||| checker on primitive `Bits32` literals.
124+
export
125+
okEncodingDiffersFromError : Not (resultToInt Ok = resultToInt Error)
126+
okEncodingDiffersFromError = \case Refl impossible
127+
128+
||| A second non-vacuity witness on a non-adjacent pair, to pin that the
129+
||| separation is not an artefact of the first two codes.
130+
export
131+
okEncodingDiffersFromCounterUnavailable :
132+
Not (resultToInt Ok = resultToInt CounterUnavailable)
133+
okEncodingDiffersFromCounterUnavailable = \case Refl impossible

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

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

0 commit comments

Comments
 (0)