Skip to content

Commit cec1666

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

2 files changed

Lines changed: 155 additions & 0 deletions

File tree

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

Lines changed: 154 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,154 @@
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 Betlangiser.
5+
|||
6+
||| The structural gate (scripts/abi-ffi-gate.py) checks that the Idris2
7+
||| `Result` enum and the Zig FFI enum agree by name and value. This module
8+
||| supplies the PROOF-SIDE guarantee that the C-integer encoding is SOUND:
9+
|||
10+
||| (a) `resultToIntInjective` — distinct ABI outcomes never collide on the
11+
||| wire (the encoding is unambiguous);
12+
||| (b) `intToResult` + `resultRoundTrip` — the C integer faithfully and
13+
||| losslessly round-trips back to the ABI value, and injectivity is
14+
||| DERIVED from the round-trip via `justInjective`;
15+
||| (c) the SAME guarantees for the `TernaryBool` FFI enum encoder
16+
||| (`ternaryToInt` / `intToTernary`), which is the other C-integer
17+
||| result-style encoder this ABI exposes across the seam.
18+
|||
19+
||| Method: the decoders are built with boolean `==` on `Bits32` so that the
20+
||| round-trip `Refl`s reduce definitionally on the concrete primitive
21+
||| literals. Injectivity is then derived from the round-trip. Positive
22+
||| controls (concrete `decode = Refl`) and a machine-checked negative /
23+
||| non-vacuity control (two distinct codes have distinct ints) are included.
24+
|||
25+
||| No `believe_me`, `idris_crash`, `assert_total`, `postulate`, or `sorry`:
26+
||| this is a genuine, total proof.
27+
28+
module Betlangiser.ABI.FfiSeam
29+
30+
import Betlangiser.ABI.Types
31+
32+
%default total
33+
34+
--------------------------------------------------------------------------------
35+
-- Generic helper: injectivity of the `Just` constructor
36+
--------------------------------------------------------------------------------
37+
38+
||| `Just` is injective. (Idris2 0.7.0 base does not export `justInjective`,
39+
||| so we prove it locally by pattern matching on the equality witness.)
40+
private
41+
justInj : {0 x, y : a} -> Just x = Just y -> x = y
42+
justInj Refl = Refl
43+
44+
--------------------------------------------------------------------------------
45+
-- (b) Decoder + round-trip for Result
46+
--------------------------------------------------------------------------------
47+
48+
||| Decode a C integer back into a `Result`. Total: every `Bits32` not in the
49+
||| valid range maps to `Nothing`. Uses boolean `==` so the comparisons reduce
50+
||| on concrete primitive literals (enabling the round-trip `Refl`s to check).
51+
public export
52+
intToResult : Bits32 -> Maybe Result
53+
intToResult x =
54+
if x == 0 then Just Ok
55+
else if x == 1 then Just Error
56+
else if x == 2 then Just InvalidParam
57+
else if x == 3 then Just OutOfMemory
58+
else if x == 4 then Just NullPointer
59+
else if x == 5 then Just InvalidDistribution
60+
else if x == 6 then Just SamplingFailed
61+
else Nothing
62+
63+
||| Faithful / lossless encoding: decoding the encoding of any `Result`
64+
||| recovers exactly that `Result`. This is the core seam-soundness theorem —
65+
||| no ABI outcome is lost or corrupted when it crosses to C and back.
66+
public export
67+
resultRoundTrip : (r : Result) -> intToResult (resultToInt r) = Just r
68+
resultRoundTrip Ok = Refl
69+
resultRoundTrip Error = Refl
70+
resultRoundTrip InvalidParam = Refl
71+
resultRoundTrip OutOfMemory = Refl
72+
resultRoundTrip NullPointer = Refl
73+
resultRoundTrip InvalidDistribution = Refl
74+
resultRoundTrip SamplingFailed = Refl
75+
76+
--------------------------------------------------------------------------------
77+
-- (a) Injectivity of resultToInt, DERIVED from the round-trip
78+
--------------------------------------------------------------------------------
79+
80+
||| The encoding is unambiguous: distinct `Result` outcomes never collide on
81+
||| the wire. Derived cleanly from `resultRoundTrip` via `justInj`:
82+
||| if `resultToInt a = resultToInt b`, then applying `intToResult` to both
83+
||| sides gives `Just a = Just b`, whence `a = b`.
84+
public export
85+
resultToIntInjective : (a, b : Result) ->
86+
resultToInt a = resultToInt b -> a = b
87+
resultToIntInjective a b prf =
88+
justInj (rewrite sym (resultRoundTrip a) in
89+
rewrite prf in
90+
resultRoundTrip b)
91+
92+
--------------------------------------------------------------------------------
93+
-- (c) Same guarantees for the TernaryBool FFI enum encoder
94+
--------------------------------------------------------------------------------
95+
-- Types.idr already defines `ternaryToInt` (0=False,1=True,2=Unknown) and the
96+
-- decoder `intToTernary`. We prove the same round-trip and injectivity here so
97+
-- the second C-integer encoder crossing the seam is equally sealed.
98+
99+
||| Faithful / lossless encoding for the ternary-logic FFI enum.
100+
public export
101+
ternaryRoundTrip : (x : TernaryBool) -> intToTernary (ternaryToInt x) = Just x
102+
ternaryRoundTrip TFalse = Refl
103+
ternaryRoundTrip TTrue = Refl
104+
ternaryRoundTrip TUnknown = Refl
105+
106+
||| The ternary encoding is unambiguous, derived from its round-trip.
107+
public export
108+
ternaryToIntInjective : (x, y : TernaryBool) ->
109+
ternaryToInt x = ternaryToInt y -> x = y
110+
ternaryToIntInjective x y prf =
111+
justInj (rewrite sym (ternaryRoundTrip x) in
112+
rewrite prf in
113+
ternaryRoundTrip y)
114+
115+
--------------------------------------------------------------------------------
116+
-- Positive controls (concrete decodes, machine-checked by Refl)
117+
--------------------------------------------------------------------------------
118+
119+
||| Positive control: the wire value 0 decodes to `Ok`.
120+
public export
121+
decodeOkControl : intToResult 0 = Just Ok
122+
decodeOkControl = Refl
123+
124+
||| Positive control: the wire value 6 decodes to `SamplingFailed`.
125+
public export
126+
decodeSamplingFailedControl : intToResult 6 = Just SamplingFailed
127+
decodeSamplingFailedControl = Refl
128+
129+
||| Positive control: the wire value 2 decodes to `TUnknown` (ternary enum).
130+
public export
131+
decodeTUnknownControl : intToTernary 2 = Just TUnknown
132+
decodeTUnknownControl = Refl
133+
134+
--------------------------------------------------------------------------------
135+
-- Negative / non-vacuity controls (distinct codes => distinct ints)
136+
--------------------------------------------------------------------------------
137+
-- These guarantee the injectivity theorems are not vacuously true: there
138+
-- genuinely EXIST distinct outcomes whose encodings differ. The refutations
139+
-- are discharged by the coverage checker on distinct primitive Bits32 literals.
140+
141+
||| Non-vacuity: `Ok` and `Error` do NOT collide on the wire.
142+
public export
143+
okErrorDistinct : Not (resultToInt Ok = resultToInt Error)
144+
okErrorDistinct = \case Refl impossible
145+
146+
||| Non-vacuity: `OutOfMemory` and `SamplingFailed` do NOT collide on the wire.
147+
public export
148+
oomSamplingDistinct : Not (resultToInt OutOfMemory = resultToInt SamplingFailed)
149+
oomSamplingDistinct = \case Refl impossible
150+
151+
||| Non-vacuity for the ternary enum: `TTrue` and `TUnknown` do NOT collide.
152+
public export
153+
ternaryTrueUnknownDistinct : Not (ternaryToInt TTrue = ternaryToInt TUnknown)
154+
ternaryTrueUnknownDistinct = \case Refl impossible

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

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

0 commit comments

Comments
 (0)