Skip to content

Commit 0d7b247

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
ABI Layer 4: prove the FFI result-code seam is injective + faithful (#43)
## Summary Layer 4 (seal the ABI↔FFI seam): proves the FFI result-code encoding (`resultToInt`) is a **sound, lossless wire encoding** — decoder `intToResult` with `resultRoundTrip`, from which `resultToIntInjective` is derived. Distinct ABI outcomes never collide on the C wire. Complements the structural `abi-ffi-gate.py`. New module `*.ABI.FfiSeam` (imports `Types`). Positive + non-vacuity controls. ## Testing Idris2 0.7.0 `--build` → exit 0, zero warnings. Adversarial rejection confirmed. `build/` removed. No `believe_me`/`postulate`/`sorry`. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- _Generated by [Claude Code](https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx)_ --------- Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> Co-authored-by: Claude <noreply@anthropic.com>
1 parent 7d3668b commit 0d7b247

2 files changed

Lines changed: 148 additions & 1 deletion

File tree

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

Lines changed: 147 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,147 @@
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 proof for Anvomidaviser.
5+
|||
6+
||| The structural gate (scripts/abi-ffi-gate.py) checks that the Idris `Result`
7+
||| enum and the Zig FFI enum agree by name and value. This module supplies the
8+
||| PROOF-SIDE guarantee that the encoding itself is SOUND:
9+
|||
10+
||| * `resultToIntInjective` — distinct ABI outcomes never collide on the wire.
11+
||| * `intToResult` / `resultRoundTrip` — the C integer faithfully round-trips
12+
||| back to the originating ABI value (the encoding is lossless).
13+
|||
14+
||| Together these seal the seam: an FFI result code carries exactly one ABI
15+
||| meaning, and that meaning is recoverable.
16+
17+
module Anvomidaviser.ABI.FfiSeam
18+
19+
import Anvomidaviser.ABI.Types
20+
21+
%default total
22+
23+
--------------------------------------------------------------------------------
24+
-- Injectivity of the encoding
25+
--------------------------------------------------------------------------------
26+
27+
||| The result-code encoding is injective: if two `Result`s encode to the same
28+
||| C integer, they are the same `Result`. Proved directly by nested case on
29+
||| both arguments; the diagonal is `Refl`, every off-diagonal pair is refuted
30+
||| because its two distinct primitive `Bits32` literals cannot be equal.
31+
export
32+
resultToIntInjective : (a : Result) -> (b : Result)
33+
-> resultToInt a = resultToInt b -> a = b
34+
resultToIntInjective Ok Ok _ = Refl
35+
resultToIntInjective Error Error _ = Refl
36+
resultToIntInjective InvalidParam InvalidParam _ = Refl
37+
resultToIntInjective OutOfMemory OutOfMemory _ = Refl
38+
resultToIntInjective NullPointer NullPointer _ = Refl
39+
resultToIntInjective RuleViolation RuleViolation _ = Refl
40+
resultToIntInjective Ok Error prf = void (the Void (case prf of Refl impossible))
41+
resultToIntInjective Ok InvalidParam prf = void (the Void (case prf of Refl impossible))
42+
resultToIntInjective Ok OutOfMemory prf = void (the Void (case prf of Refl impossible))
43+
resultToIntInjective Ok NullPointer prf = void (the Void (case prf of Refl impossible))
44+
resultToIntInjective Ok RuleViolation prf = void (the Void (case prf of Refl impossible))
45+
resultToIntInjective Error Ok prf = void (the Void (case prf of Refl impossible))
46+
resultToIntInjective Error InvalidParam prf = void (the Void (case prf of Refl impossible))
47+
resultToIntInjective Error OutOfMemory prf = void (the Void (case prf of Refl impossible))
48+
resultToIntInjective Error NullPointer prf = void (the Void (case prf of Refl impossible))
49+
resultToIntInjective Error RuleViolation prf = void (the Void (case prf of Refl impossible))
50+
resultToIntInjective InvalidParam Ok prf = void (the Void (case prf of Refl impossible))
51+
resultToIntInjective InvalidParam Error prf = void (the Void (case prf of Refl impossible))
52+
resultToIntInjective InvalidParam OutOfMemory prf = void (the Void (case prf of Refl impossible))
53+
resultToIntInjective InvalidParam NullPointer prf = void (the Void (case prf of Refl impossible))
54+
resultToIntInjective InvalidParam RuleViolation prf = void (the Void (case prf of Refl impossible))
55+
resultToIntInjective OutOfMemory Ok prf = void (the Void (case prf of Refl impossible))
56+
resultToIntInjective OutOfMemory Error prf = void (the Void (case prf of Refl impossible))
57+
resultToIntInjective OutOfMemory InvalidParam prf = void (the Void (case prf of Refl impossible))
58+
resultToIntInjective OutOfMemory NullPointer prf = void (the Void (case prf of Refl impossible))
59+
resultToIntInjective OutOfMemory RuleViolation prf = void (the Void (case prf of Refl impossible))
60+
resultToIntInjective NullPointer Ok prf = void (the Void (case prf of Refl impossible))
61+
resultToIntInjective NullPointer Error prf = void (the Void (case prf of Refl impossible))
62+
resultToIntInjective NullPointer InvalidParam prf = void (the Void (case prf of Refl impossible))
63+
resultToIntInjective NullPointer OutOfMemory prf = void (the Void (case prf of Refl impossible))
64+
resultToIntInjective NullPointer RuleViolation prf = void (the Void (case prf of Refl impossible))
65+
resultToIntInjective RuleViolation Ok prf = void (the Void (case prf of Refl impossible))
66+
resultToIntInjective RuleViolation Error prf = void (the Void (case prf of Refl impossible))
67+
resultToIntInjective RuleViolation InvalidParam prf = void (the Void (case prf of Refl impossible))
68+
resultToIntInjective RuleViolation OutOfMemory prf = void (the Void (case prf of Refl impossible))
69+
resultToIntInjective RuleViolation NullPointer prf = void (the Void (case prf of Refl impossible))
70+
71+
--------------------------------------------------------------------------------
72+
-- Faithful decoder + round-trip
73+
--------------------------------------------------------------------------------
74+
75+
||| Decode a C integer back into a `Result`. Unknown codes map to `Nothing`.
76+
||| Implemented with boolean `Bits32` `==`, which reduces on concrete literals,
77+
||| so the round-trip property below holds definitionally.
78+
export
79+
intToResult : Bits32 -> Maybe Result
80+
intToResult x =
81+
if x == 0 then Just Ok
82+
else if x == 1 then Just Error
83+
else if x == 2 then Just InvalidParam
84+
else if x == 3 then Just OutOfMemory
85+
else if x == 4 then Just NullPointer
86+
else if x == 5 then Just RuleViolation
87+
else Nothing
88+
89+
||| The encoding is lossless: decoding the encoding of any `Result` recovers it.
90+
export
91+
resultRoundTrip : (r : Result) -> intToResult (resultToInt r) = Just r
92+
resultRoundTrip Ok = Refl
93+
resultRoundTrip Error = Refl
94+
resultRoundTrip InvalidParam = Refl
95+
resultRoundTrip OutOfMemory = Refl
96+
resultRoundTrip NullPointer = Refl
97+
resultRoundTrip RuleViolation = Refl
98+
99+
||| `Just` is injective (local lemma, used by the round-trip derivation below).
100+
justInj : {0 x, y : Result} -> Just x = Just y -> x = y
101+
justInj Refl = Refl
102+
103+
||| Injectivity, re-derived from the round-trip law: if the encodings agree then
104+
||| their decodings agree, and the decoder pins each back to its own `Just`.
105+
||| An independent witness corroborating `resultToIntInjective`.
106+
export
107+
resultToIntInjectiveViaRoundTrip : (a : Result) -> (b : Result)
108+
-> resultToInt a = resultToInt b -> a = b
109+
resultToIntInjectiveViaRoundTrip a b prf =
110+
justInj $
111+
rewrite sym (resultRoundTrip a) in
112+
rewrite sym (resultRoundTrip b) in
113+
cong intToResult prf
114+
115+
--------------------------------------------------------------------------------
116+
-- Positive controls (concrete decodes)
117+
--------------------------------------------------------------------------------
118+
119+
||| Decoding 0 yields Ok.
120+
export
121+
decodeZeroIsOk : intToResult 0 = Just Ok
122+
decodeZeroIsOk = Refl
123+
124+
||| Decoding 5 yields RuleViolation (the highest defined code).
125+
export
126+
decodeFiveIsRuleViolation : intToResult 5 = Just RuleViolation
127+
decodeFiveIsRuleViolation = Refl
128+
129+
||| Decoding an out-of-range code yields Nothing.
130+
export
131+
decodeSixIsNothing : intToResult 6 = Nothing
132+
decodeSixIsNothing = Refl
133+
134+
--------------------------------------------------------------------------------
135+
-- Negative / non-vacuity control
136+
--------------------------------------------------------------------------------
137+
138+
||| Non-vacuity: two DISTINCT result codes encode to DISTINCT integers, so the
139+
||| injectivity theorem is not trivially satisfied by an empty domain.
140+
export
141+
okEncodingNotErrorEncoding : Not (resultToInt Ok = resultToInt Error)
142+
okEncodingNotErrorEncoding = \case Refl impossible
143+
144+
||| A second distinct pair, for good measure: Ok and RuleViolation differ.
145+
export
146+
okEncodingNotRuleViolationEncoding : Not (resultToInt Ok = resultToInt RuleViolation)
147+
okEncodingNotRuleViolationEncoding = \case Refl impossible

‎src/interface/abi/anvomidaviser-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 anvomidaviser-abi
33
sourcedir = "."
4-
modules = Anvomidaviser.ABI.Types, Anvomidaviser.ABI.Layout, Anvomidaviser.ABI.Foreign, Anvomidaviser.ABI.Proofs, Anvomidaviser.ABI.Semantics, Anvomidaviser.ABI.Invariants
4+
modules = Anvomidaviser.ABI.Types, Anvomidaviser.ABI.Layout, Anvomidaviser.ABI.Foreign, Anvomidaviser.ABI.Proofs, Anvomidaviser.ABI.Semantics, Anvomidaviser.ABI.Invariants, Anvomidaviser.ABI.FfiSeam

0 commit comments

Comments
 (0)