Skip to content

Commit 9efc926

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

2 files changed

Lines changed: 132 additions & 0 deletions

File tree

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

Lines changed: 131 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,131 @@
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 — Sealing the ABI<->FFI seam for Tlaiser.
5+
|||
6+
||| The estate's structural gate (scripts/abi-ffi-gate.py) checks that the
7+
||| Idris `Result` enum and the Zig FFI enum agree by name+value. This module
8+
||| supplies the PROOF-SIDE guarantee that the wire encoding `resultToInt`
9+
||| is SOUND:
10+
|||
11+
||| * injective — distinct ABI outcomes never collide on the wire, so a
12+
||| C caller can never confuse two error conditions;
13+
||| * lossless — there is a total decoder `intToResultSeam` such that
14+
||| every `Result` round-trips faithfully through the C
15+
||| integer (encode-then-decode = identity).
16+
|||
17+
||| Injectivity is DERIVED from the round-trip (the cleanest route): the
18+
||| decoder is built with boolean `Bits32` `==` so the round-trip `Refl`s
19+
||| reduce definitionally on each concrete literal, and injectivity then
20+
||| follows from `cong` + `justInjective`.
21+
|||
22+
||| Genuine proof only: no believe_me / idris_crash / assert_total / postulate.
23+
|||
24+
||| @see Tlaiser.ABI.Types for the `Result` enum and `resultToInt` encoder.
25+
26+
module Tlaiser.ABI.FfiSeam
27+
28+
import Tlaiser.ABI.Types
29+
30+
%default total
31+
32+
--------------------------------------------------------------------------------
33+
-- Local lemma: Just is injective
34+
--------------------------------------------------------------------------------
35+
36+
||| `Just` is injective. Proved structurally (single `Refl` clause); no
37+
||| appeal to any unsafe primitive. Used to peel the `Just` off both sides
38+
||| of the round-trip equation when deriving injectivity.
39+
justInjectiveSeam : {0 x, y : a} -> Just x = Just y -> x = y
40+
justInjectiveSeam Refl = Refl
41+
42+
--------------------------------------------------------------------------------
43+
-- Faithful decoder (Bits32 -> Maybe Result)
44+
--------------------------------------------------------------------------------
45+
46+
||| Total decoder from the C wire integer back to a `Result`. Built with
47+
||| boolean `Bits32` equality (`==`) so that each concrete literal branch
48+
||| reduces definitionally — this is what lets the round-trip proofs below
49+
||| close with `Refl`. Unknown codes decode to `Nothing` (the encoding is
50+
||| total but not surjective: only 0..7 are valid).
51+
public export
52+
intToResultSeam : Bits32 -> Maybe Result
53+
intToResultSeam 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 TlcError
60+
else if x == 6 then Just SpecSyntaxError
61+
else if x == 7 then Just StateSpaceExhausted
62+
else Nothing
63+
64+
--------------------------------------------------------------------------------
65+
-- (b) Faithful / lossless encoding: round-trip
66+
--------------------------------------------------------------------------------
67+
68+
||| The encoding is lossless: decoding the C integer produced for any
69+
||| `Result` recovers exactly that `Result`. Each clause closes with `Refl`
70+
||| because `resultToInt` yields a concrete literal and the `==` branches
71+
||| of `intToResultSeam` reduce on it.
72+
export
73+
resultRoundTrip : (r : Result) -> intToResultSeam (resultToInt r) = Just r
74+
resultRoundTrip Ok = Refl
75+
resultRoundTrip Error = Refl
76+
resultRoundTrip InvalidParam = Refl
77+
resultRoundTrip OutOfMemory = Refl
78+
resultRoundTrip NullPointer = Refl
79+
resultRoundTrip TlcError = Refl
80+
resultRoundTrip SpecSyntaxError = Refl
81+
resultRoundTrip StateSpaceExhausted = Refl
82+
83+
--------------------------------------------------------------------------------
84+
-- (a) Encoding is unambiguous: injectivity (DERIVED from round-trip)
85+
--------------------------------------------------------------------------------
86+
87+
||| `resultToInt` is injective: distinct ABI outcomes can never collide on
88+
||| the wire. Derived from `resultRoundTrip` via `cong` + `justInjectiveSeam`:
89+
||| if `resultToInt a = resultToInt b`, applying the decoder to both sides
90+
||| gives `Just a = Just b`, hence `a = b`.
91+
export
92+
resultToIntInjective : (a, b : Result) -> resultToInt a = resultToInt b -> a = b
93+
resultToIntInjective a b prf =
94+
justInjectiveSeam
95+
(trans (sym (resultRoundTrip a))
96+
(trans (cong intToResultSeam prf)
97+
(resultRoundTrip b)))
98+
99+
--------------------------------------------------------------------------------
100+
-- Positive controls (concrete decodes, machine-checked = Refl)
101+
--------------------------------------------------------------------------------
102+
103+
||| Positive control: code 0 decodes to `Ok`.
104+
export
105+
decodeOk : intToResultSeam 0 = Just Ok
106+
decodeOk = Refl
107+
108+
||| Positive control: code 7 decodes to `StateSpaceExhausted` (the highest
109+
||| valid code — guards the upper end of the table).
110+
export
111+
decodeStateSpaceExhausted : intToResultSeam 7 = Just StateSpaceExhausted
112+
decodeStateSpaceExhausted = Refl
113+
114+
||| Positive control: an out-of-range code decodes to `Nothing` (the
115+
||| encoding is not surjective — only 0..7 are valid wire values).
116+
export
117+
decodeUnknownIsNothing : intToResultSeam 8 = Nothing
118+
decodeUnknownIsNothing = Refl
119+
120+
--------------------------------------------------------------------------------
121+
-- Negative / non-vacuity control
122+
--------------------------------------------------------------------------------
123+
124+
||| Non-vacuity: two DISTINCT result codes have DISTINCT wire integers. This
125+
||| rules out the degenerate world in which every `resultToInt` collapsed to
126+
||| one value (where injectivity would hold vacuously). `resultToInt Ok` is
127+
||| `0` and `resultToInt Error` is `1`; the two primitive `Bits32` literals
128+
||| are provably unequal, discharged by the coverage checker.
129+
export
130+
okNeqErrorOnWire : Not (resultToInt Ok = resultToInt Error)
131+
okNeqErrorOnWire = \case Refl impossible

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

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

0 commit comments

Comments
 (0)