Skip to content

Commit d8ce701

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

2 files changed

Lines changed: 165 additions & 0 deletions

File tree

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

Lines changed: 164 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,164 @@
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 BQNiser.
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+value. This module
8+
||| supplies the PROOF-SIDE guarantee: that the encoding `resultToInt` is
9+
||| SOUND — distinct ABI outcomes never collide on the wire, and the C
10+
||| integer faithfully round-trips back to the ABI value.
11+
|||
12+
||| We prove:
13+
||| (a) resultToIntInjective — the encoding is unambiguous (injective).
14+
||| (b) intToResult / resultRoundTrip — the encoding is lossless: the
15+
||| decoder recovers the original Result from its integer.
16+
||| (c) bqnTypeToIntInjective — the SAME injectivity for the other FFI
17+
||| enum encoder in this ABI (`bqnTypeToInt : BQNType -> Bits32`).
18+
|||
19+
||| Controls: positive (concrete decode = Refl), and a non-vacuity /
20+
||| negative control (two distinct codes have distinct ints, machine-checked).
21+
|||
22+
||| @see Bqniser.ABI.Types (Result, resultToInt, BQNType, bqnTypeToInt)
23+
24+
module Bqniser.ABI.FfiSeam
25+
26+
import Bqniser.ABI.Types
27+
28+
%default total
29+
30+
--------------------------------------------------------------------------------
31+
-- Injectivity of the Just constructor
32+
--------------------------------------------------------------------------------
33+
34+
||| `Just` is injective: equal `Just` wrappers have equal contents.
35+
||| Used to lift the decoder round-trip back to equality of the originals.
36+
justInj : {0 a, b : t} -> Just a = Just b -> a = b
37+
justInj Refl = Refl
38+
39+
--------------------------------------------------------------------------------
40+
-- (b) Faithful decoder + round-trip for Result
41+
--------------------------------------------------------------------------------
42+
43+
||| Decode a C integer back into a Result. Built with boolean Bits32 `==`
44+
||| (which reduces on concrete literals) so the round-trip Refls check.
45+
||| Any out-of-range integer decodes to Nothing.
46+
public export
47+
intToResult : Bits32 -> Maybe Result
48+
intToResult x =
49+
if x == 0 then Just Ok
50+
else if x == 1 then Just Error
51+
else if x == 2 then Just InvalidParam
52+
else if x == 3 then Just OutOfMemory
53+
else if x == 4 then Just NullPointer
54+
else if x == 5 then Just EvalError
55+
else Nothing
56+
57+
||| The encoding is lossless: decoding an encoded Result recovers it exactly.
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 EvalError = Refl
66+
67+
--------------------------------------------------------------------------------
68+
-- (a) Injectivity of resultToInt
69+
--------------------------------------------------------------------------------
70+
71+
||| The encoding is unambiguous: equal integer encodings imply equal Results.
72+
||| DERIVED from the round-trip (cleanest): if resultToInt a = resultToInt b,
73+
||| then applying intToResult to both sides and using the round-trip gives
74+
||| Just a = Just b, whence a = b by injectivity of Just.
75+
public export
76+
resultToIntInjective : (a, b : Result)
77+
-> resultToInt a = resultToInt b
78+
-> a = b
79+
resultToIntInjective a b prf =
80+
justInj $
81+
trans (sym (resultRoundTrip a)) (trans (cong intToResult prf) (resultRoundTrip b))
82+
83+
--------------------------------------------------------------------------------
84+
-- (c) Injectivity of bqnTypeToInt (the other FFI enum encoder)
85+
--------------------------------------------------------------------------------
86+
87+
||| Decode a CBQN type tag back into a BQNType.
88+
public export
89+
intToBQNType : Bits32 -> Maybe BQNType
90+
intToBQNType x =
91+
if x == 0 then Just BQNNumber
92+
else if x == 1 then Just BQNCharacter
93+
else if x == 2 then Just BQNFunction
94+
else if x == 3 then Just BQN1Modifier
95+
else if x == 4 then Just BQN2Modifier
96+
else if x == 5 then Just BQNNamespace
97+
else if x == 6 then Just BQNArray
98+
else Nothing
99+
100+
||| The type-tag encoding is lossless.
101+
public export
102+
bqnTypeRoundTrip : (t : BQNType) -> intToBQNType (bqnTypeToInt t) = Just t
103+
bqnTypeRoundTrip BQNNumber = Refl
104+
bqnTypeRoundTrip BQNCharacter = Refl
105+
bqnTypeRoundTrip BQNFunction = Refl
106+
bqnTypeRoundTrip BQN1Modifier = Refl
107+
bqnTypeRoundTrip BQN2Modifier = Refl
108+
bqnTypeRoundTrip BQNNamespace = Refl
109+
bqnTypeRoundTrip BQNArray = Refl
110+
111+
||| The type-tag encoding is unambiguous (injective), derived from round-trip.
112+
public export
113+
bqnTypeToIntInjective : (a, b : BQNType)
114+
-> bqnTypeToInt a = bqnTypeToInt b
115+
-> a = b
116+
bqnTypeToIntInjective a b prf =
117+
justInj $
118+
trans (sym (bqnTypeRoundTrip a)) (trans (cong intToBQNType prf) (bqnTypeRoundTrip b))
119+
120+
--------------------------------------------------------------------------------
121+
-- Positive controls (concrete decodes reduce to Refl)
122+
--------------------------------------------------------------------------------
123+
124+
||| Positive control: 0 decodes to Ok.
125+
public export
126+
decodeOkControl : intToResult 0 = Just Ok
127+
decodeOkControl = Refl
128+
129+
||| Positive control: 5 decodes to EvalError (last code).
130+
public export
131+
decodeEvalErrorControl : intToResult 5 = Just EvalError
132+
decodeEvalErrorControl = Refl
133+
134+
||| Positive control: an out-of-range integer decodes to Nothing.
135+
public export
136+
decodeOutOfRangeControl : intToResult 6 = Nothing
137+
decodeOutOfRangeControl = Refl
138+
139+
||| Positive control for the type-tag decoder: 6 decodes to BQNArray.
140+
public export
141+
decodeArrayControl : intToBQNType 6 = Just BQNArray
142+
decodeArrayControl = Refl
143+
144+
--------------------------------------------------------------------------------
145+
-- Negative / non-vacuity control
146+
--------------------------------------------------------------------------------
147+
148+
||| Non-vacuity control: two DISTINCT result codes have DISTINCT ints.
149+
||| If this were not so, injectivity would be vacuous. Machine-checked:
150+
||| the coverage checker refutes `resultToInt Ok = resultToInt Error`
151+
||| (i.e. (the Bits32 0) = 1) as impossible.
152+
public export
153+
okNeqError : Not (resultToInt Ok = resultToInt Error)
154+
okNeqError = \case Refl impossible
155+
156+
||| A second non-vacuity control across non-adjacent codes.
157+
public export
158+
okNeqEvalError : Not (resultToInt Ok = resultToInt EvalError)
159+
okNeqEvalError = \case Refl impossible
160+
161+
||| Non-vacuity control for the type-tag encoder.
162+
public export
163+
numberNeqArray : Not (bqnTypeToInt BQNNumber = bqnTypeToInt BQNArray)
164+
numberNeqArray = \case Refl impossible

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

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

0 commit comments

Comments
 (0)