Skip to content

Commit 7c7452a

Browse files
claudeclaude
committed
Add Layer-4 ABI<->FFI seam soundness proof (A2mliser.ABI.FfiSeam)
Proves the resultToInt encoding is sound: a faithful decoder intToResult with resultRoundTrip (lossless), resultToIntInjective derived from the round-trip via justInj+cong, plus positive controls and a machine-checked non-vacuity control (distinct codes encode to distinct ints). %default total, no believe_me/postulate/sorry. Wires FfiSeam into a2mliser-abi.ipkg. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx
1 parent 442ee6a commit 7c7452a

2 files changed

Lines changed: 124 additions & 1 deletion

File tree

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

Lines changed: 123 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,123 @@
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 a2mliser.
5+
|||
6+
||| The structural gate (scripts/abi-ffi-gate.py) checks that the Idris ABI
7+
||| `resultToInt` encoder and the Zig FFI result enum agree by name+value.
8+
||| This module supplies the PROOF-SIDE guarantee that the encoding itself is
9+
||| SOUND: distinct ABI outcomes never collide on the wire, and the C integer
10+
||| faithfully round-trips back to the ABI value.
11+
|||
12+
||| THEOREMS:
13+
||| * intToResult — a total decoder Bits32 -> Maybe AttestationResult
14+
||| * resultRoundTrip — intToResult (resultToInt r) = Just r (lossless)
15+
||| * resultToIntInjective — derived from the round-trip via justInjective+cong
16+
|||
17+
||| Plus positive controls (concrete decode = Refl) and a machine-checked
18+
||| non-vacuity / negative control (distinct codes have distinct ints).
19+
20+
module A2mliser.ABI.FfiSeam
21+
22+
import A2mliser.ABI.Types
23+
24+
%default total
25+
26+
--------------------------------------------------------------------------------
27+
-- Decoder (faithful inverse of resultToInt)
28+
--------------------------------------------------------------------------------
29+
30+
||| Decode a C integer back to an AttestationResult.
31+
|||
32+
||| Built with boolean Bits32 `==` (which reduces on concrete literals) rather
33+
||| than by pattern-matching on Bits32 literals (which does not reduce
34+
||| definitionally). This makes the round-trip Refls below check.
35+
public export
36+
intToResult : Bits32 -> Maybe AttestationResult
37+
intToResult x =
38+
if x == 0 then Just Ok
39+
else if x == 1 then Just Error
40+
else if x == 2 then Just InvalidParam
41+
else if x == 3 then Just OutOfMemory
42+
else if x == 4 then Just NullPointer
43+
else if x == 5 then Just SignatureInvalid
44+
else if x == 6 then Just DigestMismatch
45+
else if x == 7 then Just ChainBroken
46+
else if x == 8 then Just KeyExpired
47+
else Nothing
48+
49+
--------------------------------------------------------------------------------
50+
-- (b) Faithful / lossless round-trip
51+
--------------------------------------------------------------------------------
52+
53+
||| The encoding is lossless: decoding an encoded result recovers it exactly.
54+
||| Each clause reduces by computing the concrete boolean `==` chain.
55+
public export
56+
resultRoundTrip : (r : AttestationResult) -> intToResult (resultToInt r) = Just r
57+
resultRoundTrip Ok = Refl
58+
resultRoundTrip Error = Refl
59+
resultRoundTrip InvalidParam = Refl
60+
resultRoundTrip OutOfMemory = Refl
61+
resultRoundTrip NullPointer = Refl
62+
resultRoundTrip SignatureInvalid = Refl
63+
resultRoundTrip DigestMismatch = Refl
64+
resultRoundTrip ChainBroken = Refl
65+
resultRoundTrip KeyExpired = Refl
66+
67+
--------------------------------------------------------------------------------
68+
-- (a) Injectivity, DERIVED from the round-trip
69+
--------------------------------------------------------------------------------
70+
71+
||| Injectivity of the `Just` constructor (proved locally to avoid any
72+
||| dependency beyond the prelude).
73+
justInj : {0 x, y : AttestationResult} -> Just x = Just y -> x = y
74+
justInj Refl = Refl
75+
76+
||| The encoding is unambiguous: distinct ABI outcomes never collide on the
77+
||| wire. Derived cleanly from the round-trip: if `resultToInt a = resultToInt b`
78+
||| then applying `intToResult` to both sides and using the round-trip on each
79+
||| gives `Just a = Just b`, whence `a = b` by injectivity of `Just`.
80+
public export
81+
resultToIntInjective : (a, b : AttestationResult)
82+
-> resultToInt a = resultToInt b
83+
-> a = b
84+
resultToIntInjective a b prf =
85+
justInj $
86+
trans (sym (resultRoundTrip a)) $
87+
trans (cong intToResult prf) (resultRoundTrip b)
88+
89+
--------------------------------------------------------------------------------
90+
-- Positive controls (concrete decodes)
91+
--------------------------------------------------------------------------------
92+
93+
||| Decoding 0 yields Ok.
94+
public export
95+
decodeZeroIsOk : intToResult 0 = Just Ok
96+
decodeZeroIsOk = Refl
97+
98+
||| Decoding 8 yields KeyExpired (the largest valid code).
99+
public export
100+
decodeEightIsKeyExpired : intToResult 8 = Just KeyExpired
101+
decodeEightIsKeyExpired = Refl
102+
103+
||| Decoding an out-of-range code yields Nothing.
104+
public export
105+
decodeNineIsNothing : intToResult 9 = Nothing
106+
decodeNineIsNothing = Refl
107+
108+
--------------------------------------------------------------------------------
109+
-- Negative / non-vacuity control
110+
--------------------------------------------------------------------------------
111+
112+
||| Non-vacuity: two DISTINCT result codes encode to DISTINCT ints, machine
113+
||| checked. `resultToInt Ok` reduces to `0` and `resultToInt Error` to `1`;
114+
||| distinct primitive Bits32 literals are provably unequal, so the coverage
115+
||| checker discharges `Refl impossible`.
116+
public export
117+
okNotError : Not (resultToInt Ok = resultToInt Error)
118+
okNotError = \case Refl impossible
119+
120+
||| A second distinct pair, for good measure.
121+
public export
122+
okNotKeyExpired : Not (resultToInt Ok = resultToInt KeyExpired)
123+
okNotKeyExpired = \case Refl impossible

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
11
-- SPDX-License-Identifier: MPL-2.0
22
package a2mliser-abi
33
sourcedir = "."
4-
modules = A2mliser.ABI.Types, A2mliser.ABI.Layout, A2mliser.ABI.Foreign, A2mliser.ABI.Proofs, A2mliser.ABI.Semantics, A2mliser.ABI.Invariants
4+
modules = A2mliser.ABI.Types, A2mliser.ABI.Layout, A2mliser.ABI.Foreign, A2mliser.ABI.Proofs, A2mliser.ABI.Semantics, A2mliser.ABI.Invariants, A2mliser.ABI.FfiSeam

0 commit comments

Comments
 (0)