Skip to content

Commit f058fca

Browse files
claudeclaude
committed
Add Layer 4 ABI<->FFI seam soundness proof (FfiSeam)
Prove the FFI result-code wire encoding is sound for Julianiser: - intToResult decoder + resultRoundTrip: faithful/lossless round-trip - resultToIntInjective: derived from round-trip via cong + justInj - positive controls (decode 0/6/7) and negative non-vacuity controls (distinct codes have distinct ints, machine-checked) Genuine proof only; no believe_me/postulate/etc. %default total, zero warnings. Julianiser has only Result/resultToInt as an FFI enum encoder (no ProofStatus/statusToInt), so clause (c) is vacuous. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx
1 parent b08520c commit f058fca

2 files changed

Lines changed: 132 additions & 0 deletions

File tree

‎src/interface/abi/Julianiser/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: ABI <-> FFI seam soundness proofs for Julianiser.
5+
|||
6+
||| The structural gate (scripts/abi-ffi-gate.py) checks that the Idris2 `Result`
7+
||| enum and the Zig FFI enum agree by name+value. THIS module is the proof-side
8+
||| guarantee that the wire encoding is itself SOUND:
9+
|||
10+
||| (a) `resultToIntInjective` — distinct ABI `Result` outcomes never collide
11+
||| on the wire (the encoding is unambiguous).
12+
||| (b) `intToResult` + `resultRoundTrip` — the C integer faithfully and
13+
||| losslessly round-trips back to the originating ABI `Result`.
14+
|||
15+
||| Injectivity (a) is DERIVED from the round-trip (b) via `cong` + `justInj`,
16+
||| which is the cleanest argument: if two results encode to the same int, then
17+
||| decoding that int yields the same `Just`, hence the results are equal.
18+
|||
19+
||| Julianiser has exactly one FFI enum encoder (`Result`/`resultToInt`); there
20+
||| is no `ProofStatus`/`statusToInt` or other encoder to mirror, so clause (c)
21+
||| of the seam obligation is vacuous here.
22+
|||
23+
||| Genuine proof only: no `believe_me`, `idris_crash`, `assert_total`,
24+
||| `postulate`, `sorry`. Decidable primitive Bits32 equality discharges the
25+
||| negative (non-vacuity) control.
26+
27+
module Julianiser.ABI.FfiSeam
28+
29+
import Julianiser.ABI.Types
30+
31+
%default total
32+
33+
--------------------------------------------------------------------------------
34+
-- Local lemma
35+
--------------------------------------------------------------------------------
36+
37+
||| `Just` is injective. Proved by pattern matching on the single inhabitant
38+
||| of the equality (the `Just x = Just y` shape forces `x = y`).
39+
private
40+
justInj : {0 x, y : a} -> Just x = Just y -> x = y
41+
justInj Refl = Refl
42+
43+
--------------------------------------------------------------------------------
44+
-- Decoder: the inverse of resultToInt
45+
--------------------------------------------------------------------------------
46+
47+
||| Decode a C integer result code back to the ABI `Result`. Built with nested
48+
||| boolean `if`/`==` on concrete Bits32 literals so the round-trip equalities
49+
||| reduce definitionally to `Refl`. Unknown codes decode to `Nothing`.
50+
public export
51+
intToResult : Bits32 -> Maybe Result
52+
intToResult x =
53+
if x == 0 then Just Ok
54+
else if x == 1 then Just Error
55+
else if x == 2 then Just InvalidParam
56+
else if x == 3 then Just OutOfMemory
57+
else if x == 4 then Just NullPointer
58+
else if x == 5 then Just ParseError
59+
else if x == 6 then Just CodegenError
60+
else Nothing
61+
62+
--------------------------------------------------------------------------------
63+
-- (b) Faithful / lossless round-trip
64+
--------------------------------------------------------------------------------
65+
66+
||| The wire encoding is lossless: decoding the encoding of any `Result`
67+
||| recovers exactly that `Result`. Each clause reduces through the boolean
68+
||| `==` comparisons on concrete literals.
69+
export
70+
resultRoundTrip : (r : Result) -> intToResult (resultToInt r) = Just r
71+
resultRoundTrip Ok = Refl
72+
resultRoundTrip Error = Refl
73+
resultRoundTrip InvalidParam = Refl
74+
resultRoundTrip OutOfMemory = Refl
75+
resultRoundTrip NullPointer = Refl
76+
resultRoundTrip ParseError = Refl
77+
resultRoundTrip CodegenError = Refl
78+
79+
--------------------------------------------------------------------------------
80+
-- (a) Injectivity, DERIVED from the round-trip
81+
--------------------------------------------------------------------------------
82+
83+
||| The encoding is unambiguous: distinct `Result` values never map to the same
84+
||| C integer. Derived from the round-trip — if `resultToInt a = resultToInt b`,
85+
||| then applying `intToResult` to both sides (via `cong`) gives
86+
||| `Just a = Just b` (using both round-trips), and `justInj` yields
87+
||| `a = b`. No case analysis on the 49-cell matrix is needed.
88+
export
89+
resultToIntInjective : (a, b : Result) ->
90+
resultToInt a = resultToInt b -> a = b
91+
resultToIntInjective a b prf =
92+
justInj $
93+
rewrite sym (resultRoundTrip a) in
94+
rewrite sym (resultRoundTrip b) in
95+
cong intToResult prf
96+
97+
--------------------------------------------------------------------------------
98+
-- Positive controls (concrete decodes machine-checked = Refl)
99+
--------------------------------------------------------------------------------
100+
101+
||| Positive control: code 0 decodes to Ok.
102+
export
103+
decodeZeroIsOk : intToResult 0 = Just Ok
104+
decodeZeroIsOk = Refl
105+
106+
||| Positive control: code 6 decodes to CodegenError (the largest code).
107+
export
108+
decodeSixIsCodegenError : intToResult 6 = Just CodegenError
109+
decodeSixIsCodegenError = Refl
110+
111+
||| Positive control: an out-of-range code decodes to Nothing.
112+
export
113+
decodeSevenIsNothing : intToResult 7 = Nothing
114+
decodeSevenIsNothing = Refl
115+
116+
--------------------------------------------------------------------------------
117+
-- Negative / non-vacuity control (machine-checked)
118+
--------------------------------------------------------------------------------
119+
120+
||| Non-vacuity: two DISTINCT result codes have DISTINCT wire integers. If this
121+
||| were not machine-checkable the injectivity theorem above would be vacuously
122+
||| true. Discharged by Idris's coverage checker on distinct primitive Bits32
123+
||| literals (0 vs 1).
124+
export
125+
okIntNotErrorInt : Not (resultToInt Ok = resultToInt Error)
126+
okIntNotErrorInt = \case Refl impossible
127+
128+
||| A second distinct-pair witness across non-adjacent codes (0 vs 6).
129+
export
130+
okIntNotCodegenInt : Not (resultToInt Ok = resultToInt CodegenError)
131+
okIntNotCodegenInt = \case Refl impossible

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

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

0 commit comments

Comments
 (0)