Skip to content

Commit 4e6560c

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

2 files changed

Lines changed: 147 additions & 0 deletions

File tree

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

Lines changed: 146 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,146 @@
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 Wokelangiser.
5+
|||
6+
||| The structural gate (scripts/abi-ffi-gate.py) checks that the Idris and Zig
7+
||| result-code enums agree by name+value. This module supplies the *proof-side*
8+
||| guarantee that the encoding itself is SOUND:
9+
|||
10+
||| * faithful/lossless: a decoder round-trips every ABI value through its
11+
||| C integer (`resultRoundTrip`, reused from Types via `resultFromInt`);
12+
||| * unambiguous: distinct ABI outcomes never collide on the wire
13+
||| (`resultToIntInjective`), DERIVED from the round-trip via
14+
||| `justInjective . cong`;
15+
||| * non-vacuous: at least two distinct codes carry distinct integers,
16+
||| machine-checked (`okErrorDistinct`).
17+
|||
18+
||| The same injectivity is established for the other FFI enum encoders that
19+
||| ship in this ABI: `consentToInt` and `wcagToInt`.
20+
|||
21+
||| All proofs are genuine: no believe_me / idris_crash / assert_total /
22+
||| postulate / %hint hacks.
23+
24+
module Wokelangiser.ABI.FfiSeam
25+
26+
import Wokelangiser.ABI.Types
27+
28+
%default total
29+
30+
--------------------------------------------------------------------------------
31+
-- Constructor injectivity helper
32+
--------------------------------------------------------------------------------
33+
34+
||| `Just` is injective. Used to peel the `Just` wrapper off the round-trip
35+
||| equality when deriving encoder injectivity. (Standalone helper because this
36+
||| stdlib exposes injectivity only through the `Injective Just` interface
37+
||| method, not a named `justInjective`.)
38+
public export
39+
justInj : {0 a, b : t} -> Just a = Just b -> a = b
40+
justInj Refl = Refl
41+
42+
--------------------------------------------------------------------------------
43+
-- Result: faithful round-trip and derived injectivity
44+
--------------------------------------------------------------------------------
45+
46+
||| The Result encoding round-trips losslessly through its C integer.
47+
||| (Re-exported through the seam module from the decoder/proof in Types so the
48+
||| seam guarantee stands on its own named theorem.)
49+
public export
50+
resultRoundTripSeam : (r : Result) -> resultFromInt (resultToInt r) = Just r
51+
resultRoundTripSeam = resultRoundTrip
52+
53+
||| The Result encoding is injective: distinct ABI outcomes never collide on the
54+
||| wire. Derived from the round-trip — if `resultToInt a = resultToInt b`, then
55+
||| applying `resultFromInt` (via cong) to both sides and the round-trip law
56+
||| gives `Just a = Just b`, whence `a = b` by `justInjective`.
57+
public export
58+
resultToIntInjective : (a, b : Result)
59+
-> resultToInt a = resultToInt b
60+
-> a = b
61+
resultToIntInjective a b prf =
62+
justInj $
63+
trans (sym (resultRoundTripSeam a)) $
64+
trans (cong resultFromInt prf) (resultRoundTripSeam b)
65+
66+
--------------------------------------------------------------------------------
67+
-- ConsentType: faithful round-trip and derived injectivity
68+
--------------------------------------------------------------------------------
69+
70+
||| The ConsentType encoding round-trips losslessly through its C integer.
71+
public export
72+
consentRoundTripSeam : (ct : ConsentType)
73+
-> consentFromInt (consentToInt ct) = Just ct
74+
consentRoundTripSeam = consentRoundTrip
75+
76+
||| The ConsentType encoding is injective, derived from the round-trip.
77+
public export
78+
consentToIntInjective : (a, b : ConsentType)
79+
-> consentToInt a = consentToInt b
80+
-> a = b
81+
consentToIntInjective a b prf =
82+
justInj $
83+
trans (sym (consentRoundTripSeam a)) $
84+
trans (cong consentFromInt prf) (consentRoundTripSeam b)
85+
86+
--------------------------------------------------------------------------------
87+
-- WCAGLevel: faithful round-trip and derived injectivity
88+
--------------------------------------------------------------------------------
89+
90+
||| The WCAGLevel encoding round-trips losslessly through its C integer.
91+
public export
92+
wcagRoundTripSeam : (wl : WCAGLevel) -> wcagFromInt (wcagToInt wl) = Just wl
93+
wcagRoundTripSeam = wcagRoundTrip
94+
95+
||| The WCAGLevel encoding is injective, derived from the round-trip.
96+
public export
97+
wcagToIntInjective : (a, b : WCAGLevel)
98+
-> wcagToInt a = wcagToInt b
99+
-> a = b
100+
wcagToIntInjective a b prf =
101+
justInj $
102+
trans (sym (wcagRoundTripSeam a)) $
103+
trans (cong wcagFromInt prf) (wcagRoundTripSeam b)
104+
105+
--------------------------------------------------------------------------------
106+
-- Positive controls (concrete decodes = Refl)
107+
--------------------------------------------------------------------------------
108+
109+
||| Concrete decode control: integer 0 decodes to Ok.
110+
public export
111+
decodeOkControl : resultFromInt (the Bits32 0) = Just Ok
112+
decodeOkControl = Refl
113+
114+
||| Concrete decode control: integer 7 decodes to I18nError (last code).
115+
public export
116+
decodeLastControl : resultFromInt (the Bits32 7) = Just I18nError
117+
decodeLastControl = Refl
118+
119+
||| Concrete round-trip control for a mid-range code.
120+
public export
121+
roundTripNullPointerControl
122+
: resultFromInt (resultToInt NullPointer) = Just NullPointer
123+
roundTripNullPointerControl = Refl
124+
125+
||| Concrete out-of-range decode control: 8 is not a valid code.
126+
public export
127+
decodeOutOfRangeControl : resultFromInt (the Bits32 8) = Nothing
128+
decodeOutOfRangeControl = Refl
129+
130+
--------------------------------------------------------------------------------
131+
-- Negative / non-vacuity control
132+
--------------------------------------------------------------------------------
133+
134+
||| Non-vacuity: two DISTINCT result codes carry DISTINCT integers, so the
135+
||| injectivity statement is not vacuously true. Machine-checked: the two
136+
||| primitive Bits32 literals (0 and 1) are provably unequal, refuted by the
137+
||| coverage checker discharging `Refl impossible`.
138+
public export
139+
okErrorDistinct : Not (resultToInt Ok = resultToInt Error)
140+
okErrorDistinct = \case Refl impossible
141+
142+
||| A second non-vacuity witness across a wider gap (NullPointer=4 vs
143+
||| I18nError=7) to underline the encoding genuinely separates outcomes.
144+
public export
145+
nullI18nDistinct : Not (resultToInt NullPointer = resultToInt I18nError)
146+
nullI18nDistinct = \case Refl impossible

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

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

0 commit comments

Comments
 (0)