Skip to content

Commit 2e9d19f

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
ABI Layer 4: prove the FFI result-code seam is injective + faithful (#75)
* feat(abi): prove Conformant scaffold property (Layer 2 Semantics) Add Iseriser.ABI.Semantics proving the headline domain property: a generated -iser scaffold is Conformant exactly when all five required components (Manifest, Idris2 ABI, Zig FFI, Codegen, Rust CLI) are present. Conformant is built from genuine Data.List.Elem membership obligations with no catch-all constructor, so a scaffold missing any component has no witness. Includes a sound+complete decConformant : (s) -> Dec (Conformant s), a soundness fact certifyConformantSound, a positive control (completeIsConformant via explicit Elem positions), and a negative control (ffiMissingNotConformant : Not (Conformant ffiMissing)). Non-vacuity confirmed: a deliberately-false Has Ffi witness for the FFI-missing scaffold is rejected by idris2. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx * abi: add Layer-3 Invariants (generation soundness + conformance closure) Add Iseriser.ABI.Invariants over the existing Layer-2 Semantics model (Component/Scaffold/Has/Conformant). Two new, deeper, distinct theorems: 1. Generation soundness (correct-by-construction): genScaffold provably emits (s ** Conformant s) for any LanguageModel, with a corollary tying it back to the Layer-2 certifier (conformantCertifies). 2. Upward-closure / monotonicity: conformantStable proves Conformance is preserved under extension, via a genuine Elem-weakening lemma (elemAppendRight) — an algebraic closure law, not the Layer-2 decision. Includes a sound+complete Dec (decExtendConformant), a positive control (extendedGeneratedConformant) and a non-vacuity negative control (extendedBrokenNotConformant : Not ...). Builds clean with zero warnings; adversarial false proof rejected. No believe_me/postulate/assert_total. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx * abi: seal ABI<->FFI seam with Layer-4 soundness proof (FfiSeam) Add Iseriser.ABI.FfiSeam proving the resultToInt encoding is sound: - intToResult decoder + resultRoundTrip (lossless/faithful encoding) - resultToIntInjective derived from round-trip (distinct outcomes never collide on the wire) - positive controls (concrete decodes by Refl) and a machine-checked non-vacuity control (resultToInt Ok /= resultToInt Error) Genuine total proof: no believe_me/postulate/assert_total/etc. Registered in iseriser-abi.ipkg; package builds clean with zero warnings. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: 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 10b0a71 commit 2e9d19f

2 files changed

Lines changed: 118 additions & 0 deletions

File tree

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

Lines changed: 117 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,117 @@
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 iseriser.
5+
|||
6+
||| The ABI defines `resultToInt : Result -> Bits32`, the integer the Zig FFI
7+
||| returns to C. The estate's structural gate (`scripts/abi-ffi-gate.py`)
8+
||| checks the Idris and Zig enums agree by name+value. THIS module supplies
9+
||| the PROOF-SIDE guarantee that the encoding is SOUND:
10+
|||
11+
||| * `intToResult` — a decoder Bits32 -> Maybe Result
12+
||| * `resultRoundTrip` — the encoding is faithful/lossless: decoding an
13+
||| encoded result recovers exactly that result
14+
||| * `resultToIntInjective`— distinct ABI outcomes never collide on the wire,
15+
||| DERIVED from the round-trip via cong + justInjective
16+
|||
17+
||| Plus positive controls (concrete decodes by Refl) and a machine-checked
18+
||| NON-VACUITY control (two distinct codes have distinct ints).
19+
20+
module Iseriser.ABI.FfiSeam
21+
22+
import Iseriser.ABI.Types
23+
24+
%default total
25+
26+
--------------------------------------------------------------------------------
27+
-- Decoder: the inverse of resultToInt
28+
--------------------------------------------------------------------------------
29+
30+
||| Decode a C integer back to a `Result`. Built with boolean `==` on Bits32
31+
||| literals (which reduces on concrete constants) so the round-trip `Refl`s
32+
||| check definitionally. Any value outside 0..5 is not a valid ABI code.
33+
public export
34+
intToResult : Bits32 -> Maybe Result
35+
intToResult x =
36+
if x == 0 then Just Ok
37+
else if x == 1 then Just Error
38+
else if x == 2 then Just InvalidLanguage
39+
else if x == 3 then Just TemplateError
40+
else if x == 4 then Just OutputError
41+
else if x == 5 then Just NullPointer
42+
else Nothing
43+
44+
--------------------------------------------------------------------------------
45+
-- Faithfulness: the encoding is lossless (round-trips through the wire)
46+
--------------------------------------------------------------------------------
47+
48+
||| Decoding the encoding of any `Result` recovers exactly that `Result`.
49+
||| Each clause reduces because `resultToInt` produces a concrete Bits32
50+
||| literal and the decoder's boolean `==` chain evaluates on that literal.
51+
public export
52+
resultRoundTrip : (r : Result) -> intToResult (resultToInt r) = Just r
53+
resultRoundTrip Ok = Refl
54+
resultRoundTrip Error = Refl
55+
resultRoundTrip InvalidLanguage = Refl
56+
resultRoundTrip TemplateError = Refl
57+
resultRoundTrip OutputError = Refl
58+
resultRoundTrip NullPointer = Refl
59+
60+
--------------------------------------------------------------------------------
61+
-- Injectivity: distinct ABI outcomes never collide on the wire
62+
--------------------------------------------------------------------------------
63+
64+
||| `Just` is injective: recover the underlying equality from wrapped values.
65+
||| (Local helper to avoid depending on a Prelude name that may not be in
66+
||| scope; the off-diagonal `Just x = Nothing` cannot arise here.)
67+
justEq : {0 x, y : Result} -> Just x = Just y -> x = y
68+
justEq Refl = Refl
69+
70+
||| The encoding is unambiguous: if two results encode to the same integer,
71+
||| they ARE the same result. Derived from the round-trip — applying the
72+
||| decoder to both sides of `resultToInt a = resultToInt b` and chaining the
73+
||| two round-trip facts forces `Just a = Just b`, hence `a = b`.
74+
public export
75+
resultToIntInjective : (a, b : Result) ->
76+
resultToInt a = resultToInt b -> a = b
77+
resultToIntInjective a b prf =
78+
justEq $
79+
trans (sym (resultRoundTrip a))
80+
(trans (cong intToResult prf) (resultRoundTrip b))
81+
82+
--------------------------------------------------------------------------------
83+
-- Positive controls (concrete decodes by Refl)
84+
--------------------------------------------------------------------------------
85+
86+
||| Decoding 0 yields Ok.
87+
decodeZeroIsOk : intToResult 0 = Just Ok
88+
decodeZeroIsOk = Refl
89+
90+
||| Decoding 5 yields NullPointer (the highest valid code).
91+
decodeFiveIsNullPointer : intToResult 5 = Just NullPointer
92+
decodeFiveIsNullPointer = Refl
93+
94+
||| An out-of-range code decodes to Nothing.
95+
decodeSixIsNothing : intToResult 6 = Nothing
96+
decodeSixIsNothing = Refl
97+
98+
||| Concrete round-trip control through the middle of the range.
99+
roundTripTemplateError : intToResult (resultToInt TemplateError) = Just TemplateError
100+
roundTripTemplateError = Refl
101+
102+
--------------------------------------------------------------------------------
103+
-- Negative / non-vacuity control (machine-checked)
104+
--------------------------------------------------------------------------------
105+
106+
||| Distinct primitive Bits32 literals are provably unequal: the coverage
107+
||| checker discharges `Refl impossible` for `0 = 1`.
108+
okIntNotErrorInt : Not (the Bits32 0 = the Bits32 1)
109+
okIntNotErrorInt = \case Refl impossible
110+
111+
||| NON-VACUITY: two DISTINCT result codes have DISTINCT wire integers.
112+
||| `resultToInt Ok = 0` and `resultToInt Error = 1` reduce, so any proof
113+
||| that they are equal would prove `0 = 1`, which is refuted above. This
114+
||| guarantees `resultToIntInjective` is not vacuously true.
115+
public export
116+
okEncodingNotErrorEncoding : Not (resultToInt Ok = resultToInt Error)
117+
okEncodingNotErrorEncoding prf = okIntNotErrorInt prf

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

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

0 commit comments

Comments
 (0)