Skip to content

Commit 87aad80

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

2 files changed

Lines changed: 129 additions & 0 deletions

File tree

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

Lines changed: 128 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,128 @@
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 atsiser.
5+
|||
6+
||| The structural gate (scripts/abi-ffi-gate.py) checks that the Idris
7+
||| `Result` enum and the Zig FFI enum agree by name and value. This module
8+
||| supplies the PROOF-SIDE guarantee that the integer encoding `resultToInt`
9+
||| is SOUND:
10+
|||
11+
||| * Faithfulness (round-trip): a decoder `intToResult` recovers exactly
12+
||| the `Result` that `resultToInt` produced — the C integer faithfully
13+
||| round-trips back to the ABI value, losing nothing.
14+
||| * Injectivity: distinct ABI outcomes never collide on the wire. This is
15+
||| DERIVED from the round-trip via `justInjective` + `cong`, the cleanest
16+
||| route, since the round-trip `Refl`s reduce definitionally.
17+
|||
18+
||| Positive controls (concrete decodes = Refl) and a non-vacuity / negative
19+
||| control (two distinct codes have distinct ints, machine-checked) guard
20+
||| against a vacuously-true encoding.
21+
22+
module Atsiser.ABI.FfiSeam
23+
24+
import Atsiser.ABI.Types
25+
26+
%default total
27+
28+
--------------------------------------------------------------------------------
29+
-- Decoder
30+
--------------------------------------------------------------------------------
31+
32+
||| Decode a C integer back into a `Result`.
33+
|||
34+
||| Built with boolean `Bits32` `==` chained through `if ... then ... else`,
35+
||| because that form reduces definitionally on concrete literals — so the
36+
||| round-trip `Refl`s below check. Any integer outside the defined range
37+
||| decodes to `Nothing` (no spurious ABI value is fabricated).
38+
public export
39+
intToResult : Bits32 -> Maybe Result
40+
intToResult x =
41+
if x == 0 then Just Ok
42+
else if x == 1 then Just Error
43+
else if x == 2 then Just InvalidParam
44+
else if x == 3 then Just OutOfMemory
45+
else if x == 4 then Just NullPointer
46+
else if x == 5 then Just OwnershipViolation
47+
else if x == 6 then Just BoundsViolation
48+
else Nothing
49+
50+
--------------------------------------------------------------------------------
51+
-- Faithfulness: round-trip
52+
--------------------------------------------------------------------------------
53+
54+
||| The encoding is lossless: decoding the encoding of any `Result` returns
55+
||| exactly that `Result`. Each case reduces by `Refl` because the `if`/`==`
56+
||| decoder evaluates on the concrete `Bits32` literal that `resultToInt`
57+
||| emits.
58+
public export
59+
resultRoundTrip : (r : Result) -> intToResult (resultToInt r) = Just r
60+
resultRoundTrip Ok = Refl
61+
resultRoundTrip Error = Refl
62+
resultRoundTrip InvalidParam = Refl
63+
resultRoundTrip OutOfMemory = Refl
64+
resultRoundTrip NullPointer = Refl
65+
resultRoundTrip OwnershipViolation = Refl
66+
resultRoundTrip BoundsViolation = Refl
67+
68+
--------------------------------------------------------------------------------
69+
-- Injectivity (derived from the round-trip)
70+
--------------------------------------------------------------------------------
71+
72+
||| The encoding is injective: distinct ABI outcomes never collide on the
73+
||| wire. If `resultToInt a = resultToInt b`, then decoding both sides yields
74+
||| the same `Just`, and `justInjective` extracts `a = b`.
75+
|||
76+
||| Derivation:
77+
||| Just a = intToResult (resultToInt a) -- sym (resultRoundTrip a)
78+
||| = intToResult (resultToInt b) -- cong intToResult prf
79+
||| = Just b -- resultRoundTrip b
80+
||| then `Just a = Just b` is inverted to `a = b` (constructors are injective).
81+
public export
82+
resultToIntInjective : (a, b : Result)
83+
-> resultToInt a = resultToInt b
84+
-> a = b
85+
resultToIntInjective a b prf =
86+
let justEq : (the (Maybe Result) (Just a) = Just b)
87+
= trans (sym (resultRoundTrip a))
88+
(trans (cong intToResult prf) (resultRoundTrip b))
89+
in case justEq of Refl => Refl
90+
91+
--------------------------------------------------------------------------------
92+
-- Positive controls (concrete decodes)
93+
--------------------------------------------------------------------------------
94+
95+
||| Concrete decode: integer 0 decodes to success.
96+
export
97+
decodeZeroIsOk : intToResult 0 = Just Ok
98+
decodeZeroIsOk = Refl
99+
100+
||| Concrete decode: integer 6 decodes to the bounds-violation code.
101+
export
102+
decodeSixIsBounds : intToResult 6 = Just BoundsViolation
103+
decodeSixIsBounds = Refl
104+
105+
||| Concrete decode: an out-of-range integer decodes to nothing — no ABI
106+
||| value is invented for codes the contract does not define.
107+
export
108+
decodeOutOfRangeIsNothing : intToResult 7 = Nothing
109+
decodeOutOfRangeIsNothing = Refl
110+
111+
--------------------------------------------------------------------------------
112+
-- Negative / non-vacuity control
113+
--------------------------------------------------------------------------------
114+
115+
||| Non-vacuity: two DISTINCT result codes encode to DISTINCT integers, so
116+
||| the injectivity theorem above is not vacuously true. Discharged by the
117+
||| coverage checker — distinct primitive `Bits32` literals (0 and 1) are
118+
||| provably unequal.
119+
export
120+
okEncodesDistinctFromError : Not (resultToInt Ok = resultToInt Error)
121+
okEncodesDistinctFromError = \case Refl impossible
122+
123+
||| A second distinct pair, machine-checked the same way (success vs. the
124+
||| highest code), to underline that the separation is not an artefact of one
125+
||| adjacent pair.
126+
export
127+
okEncodesDistinctFromBounds : Not (resultToInt Ok = resultToInt BoundsViolation)
128+
okEncodesDistinctFromBounds = \case Refl impossible

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

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

0 commit comments

Comments
 (0)