Skip to content

Commit 039fe39

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
ABI Layer 4: prove the FFI result-code seam is injective + faithful (#35)
## 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 9d8062b commit 039fe39

2 files changed

Lines changed: 200 additions & 0 deletions

File tree

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

Lines changed: 199 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,199 @@
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 Phronesiser.
5+
|||
6+
||| The structural gate (scripts/abi-ffi-gate.py) checks the Idris and Zig
7+
||| result-code enums agree by name+value. This module is the PROOF-SIDE
8+
||| guarantee that the encoding is SOUND:
9+
|||
10+
||| * distinct ABI outcomes never collide on the wire (injectivity), and
11+
||| * the C integer faithfully round-trips back to the ABI value
12+
||| (a total decoder `intToResult` is a left inverse of `resultToInt`).
13+
|||
14+
||| Injectivity is DERIVED from the round-trip via `justInj` + `cong`,
15+
||| which is the cleanest route once the decoder's round-trip `Refl`s reduce.
16+
||| The decoder is written with boolean `Bits32` `==` (which reduces on
17+
||| concrete literals), so `resultRoundTrip Ok = Refl` etc. all check
18+
||| definitionally.
19+
|||
20+
||| The same injectivity is also proved for the other FFI enum encoders
21+
||| present in `Types`: `modalityToInt` (DeonticModality) and `severityToInt`
22+
||| (HarmSeverity). (There is no `ProofStatus`/`statusToInt` in this repo.)
23+
|||
24+
||| Controls: positive (concrete decode = Refl), and a machine-checked
25+
||| NON-VACUITY control that two DISTINCT result codes have distinct ints.
26+
|||
27+
||| Genuine proof only — no believe_me / idris_crash / assert_total /
28+
||| postulate / sorry. %default total.
29+
30+
module Phronesiser.ABI.FfiSeam
31+
32+
import Phronesiser.ABI.Types
33+
34+
%default total
35+
36+
--------------------------------------------------------------------------------
37+
-- Generic helper
38+
--------------------------------------------------------------------------------
39+
40+
||| `Just` is injective. Used to turn a round-trip equality through the
41+
||| decoder back into an equality of the underlying ABI values.
42+
public export
43+
justInj : {0 a, b : ty} -> Just a = Just b -> a = b
44+
justInj Refl = Refl
45+
46+
--------------------------------------------------------------------------------
47+
-- Result: faithful decoder + round-trip + derived injectivity
48+
--------------------------------------------------------------------------------
49+
50+
||| Decode a C integer back into a `Result`.
51+
||| Written with boolean `Bits32` `==` so it reduces on concrete literals,
52+
||| making the round-trip `Refl`s check definitionally. Unknown codes
53+
||| decode to `Nothing` (the wire space is larger than the ABI space).
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 ConstraintViolation
63+
else if x == 6 then Just ConstraintConflict
64+
else Nothing
65+
66+
||| The decoder is a left inverse of the encoder: every ABI value round-trips
67+
||| losslessly through its C integer. FAITHFULNESS of the encoding.
68+
public export
69+
resultRoundTrip : (r : Result) -> intToResult (resultToInt r) = Just r
70+
resultRoundTrip Ok = Refl
71+
resultRoundTrip Error = Refl
72+
resultRoundTrip InvalidParam = Refl
73+
resultRoundTrip OutOfMemory = Refl
74+
resultRoundTrip NullPointer = Refl
75+
resultRoundTrip ConstraintViolation = Refl
76+
resultRoundTrip ConstraintConflict = Refl
77+
78+
||| The encoding is UNAMBIGUOUS: distinct ABI outcomes never collide on the
79+
||| wire. Derived from the round-trip (a function with a left inverse is
80+
||| injective) via `cong` + `justInj`.
81+
public export
82+
resultToIntInjective : (a, b : Result) -> resultToInt a = resultToInt b -> a = b
83+
resultToIntInjective a b prf =
84+
justInj $
85+
trans (sym (resultRoundTrip a))
86+
(trans (cong intToResult prf) (resultRoundTrip b))
87+
88+
--------------------------------------------------------------------------------
89+
-- DeonticModality: same guarantees (task (c))
90+
--------------------------------------------------------------------------------
91+
92+
||| Decode a C integer back into a `DeonticModality`.
93+
public export
94+
intToModality : Bits32 -> Maybe DeonticModality
95+
intToModality x =
96+
if x == 0 then Just Obligation
97+
else if x == 1 then Just Permission
98+
else if x == 2 then Just Prohibition
99+
else Nothing
100+
101+
||| Round-trip / faithfulness for the deontic-modality encoder.
102+
public export
103+
modalityRoundTrip : (m : DeonticModality) ->
104+
intToModality (modalityToInt m) = Just m
105+
modalityRoundTrip Obligation = Refl
106+
modalityRoundTrip Permission = Refl
107+
modalityRoundTrip Prohibition = Refl
108+
109+
||| Injectivity for the deontic-modality encoder, derived from round-trip.
110+
public export
111+
modalityToIntInjective : (a, b : DeonticModality) ->
112+
modalityToInt a = modalityToInt b -> a = b
113+
modalityToIntInjective a b prf =
114+
justInj $
115+
trans (sym (modalityRoundTrip a))
116+
(trans (cong intToModality prf) (modalityRoundTrip b))
117+
118+
--------------------------------------------------------------------------------
119+
-- HarmSeverity: same guarantees (task (c))
120+
--------------------------------------------------------------------------------
121+
122+
||| Decode a C integer back into a `HarmSeverity`.
123+
public export
124+
intToSeverity : Bits32 -> Maybe HarmSeverity
125+
intToSeverity x =
126+
if x == 0 then Just Negligible
127+
else if x == 1 then Just Minor
128+
else if x == 2 then Just Moderate
129+
else if x == 3 then Just Severe
130+
else if x == 4 then Just Critical
131+
else Nothing
132+
133+
||| Round-trip / faithfulness for the harm-severity encoder.
134+
public export
135+
severityRoundTrip : (s : HarmSeverity) ->
136+
intToSeverity (severityToInt s) = Just s
137+
severityRoundTrip Negligible = Refl
138+
severityRoundTrip Minor = Refl
139+
severityRoundTrip Moderate = Refl
140+
severityRoundTrip Severe = Refl
141+
severityRoundTrip Critical = Refl
142+
143+
||| Injectivity for the harm-severity encoder, derived from round-trip.
144+
public export
145+
severityToIntInjective : (a, b : HarmSeverity) ->
146+
severityToInt a = severityToInt b -> a = b
147+
severityToIntInjective a b prf =
148+
justInj $
149+
trans (sym (severityRoundTrip a))
150+
(trans (cong intToSeverity prf) (severityRoundTrip b))
151+
152+
--------------------------------------------------------------------------------
153+
-- Positive controls (concrete decode = Refl, machine-checked)
154+
--------------------------------------------------------------------------------
155+
156+
||| Positive control: 0 decodes to Ok.
157+
public export
158+
decodeOkControl : FfiSeam.intToResult 0 = Just Ok
159+
decodeOkControl = Refl
160+
161+
||| Positive control: 6 decodes to ConstraintConflict (the top code).
162+
public export
163+
decodeConflictControl : FfiSeam.intToResult 6 = Just ConstraintConflict
164+
decodeConflictControl = Refl
165+
166+
||| Positive control: an out-of-range code decodes to Nothing.
167+
public export
168+
decodeUnknownControl : FfiSeam.intToResult 7 = Nothing
169+
decodeUnknownControl = Refl
170+
171+
--------------------------------------------------------------------------------
172+
-- Negative / non-vacuity controls (machine-checked)
173+
--------------------------------------------------------------------------------
174+
175+
||| NON-VACUITY: two DISTINCT result codes have DISTINCT C integers.
176+
||| If `resultToInt` were constant the seam would be vacuously "sound";
177+
||| this rules that out. `Ok` -> 0, `Error` -> 1, and `0 = 1` is impossible
178+
||| for distinct primitive `Bits32` literals.
179+
public export
180+
okErrorDistinct : Not (resultToInt Ok = resultToInt Error)
181+
okErrorDistinct = \case Refl impossible
182+
183+
||| Non-vacuity at the other end of the enum: the two highest codes differ.
184+
public export
185+
violationConflictDistinct :
186+
Not (resultToInt ConstraintViolation = resultToInt ConstraintConflict)
187+
violationConflictDistinct = \case Refl impossible
188+
189+
||| Non-vacuity for the deontic-modality encoder.
190+
public export
191+
obligationProhibitionDistinct :
192+
Not (modalityToInt Obligation = modalityToInt Prohibition)
193+
obligationProhibitionDistinct = \case Refl impossible
194+
195+
||| Non-vacuity for the harm-severity encoder.
196+
public export
197+
negligibleCriticalDistinct :
198+
Not (severityToInt Negligible = severityToInt Critical)
199+
negligibleCriticalDistinct = \case Refl impossible

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

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

0 commit comments

Comments
 (0)