|
| 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 k9iser. |
| 5 | +||| |
| 6 | +||| The structural gate (scripts/abi-ffi-gate.py) checks that the Idris `Result` |
| 7 | +||| enum and the Zig FFI enum agree by name and value. This module supplies the |
| 8 | +||| PROOF-SIDE guarantee that the encoding itself is SOUND: |
| 9 | +||| |
| 10 | +||| (a) `resultToIntInjective` — distinct ABI outcomes never collide on the |
| 11 | +||| wire (the C integer unambiguously identifies the ABI value). |
| 12 | +||| (b) `intToResult` + `resultRoundTrip` — the encoding is faithful/lossless: |
| 13 | +||| decoding the wire integer recovers exactly the ABI value. Injectivity |
| 14 | +||| is then DERIVED from the round-trip via `justInjective`+`cong`. |
| 15 | +||| |
| 16 | +||| Positive controls (concrete decode = Refl) and a non-vacuity / negative |
| 17 | +||| control (two distinct codes have distinct ints) are machine-checked below. |
| 18 | +||| |
| 19 | +||| k9iser defines only the `Result` FFI enum encoder (`resultToInt`); there is |
| 20 | +||| no `ProofStatus`/`statusToInt` or other FFI enum encoder, so clause (c) of |
| 21 | +||| the seam obligation is vacuous here. |
| 22 | + |
| 23 | +module K9iser.ABI.FfiSeam |
| 24 | + |
| 25 | +import K9iser.ABI.Types |
| 26 | +import Control.Function |
| 27 | +import Data.Maybe |
| 28 | + |
| 29 | +%default total |
| 30 | + |
| 31 | +-------------------------------------------------------------------------------- |
| 32 | +-- Decoder (faithful inverse of resultToInt) |
| 33 | +-------------------------------------------------------------------------------- |
| 34 | + |
| 35 | +||| Decode a C wire integer back to a `Result`. |
| 36 | +||| |
| 37 | +||| Built with boolean `Bits32` equality (`==`) on concrete literals so that |
| 38 | +||| `intToResult (resultToInt r)` reduces definitionally for each constructor, |
| 39 | +||| letting the round-trip lemma below be proved by `Refl`. |
| 40 | +public export |
| 41 | +intToResult : Bits32 -> Maybe Result |
| 42 | +intToResult x = |
| 43 | + if x == 0 then Just Ok |
| 44 | + else if x == 1 then Just Error |
| 45 | + else if x == 2 then Just InvalidParam |
| 46 | + else if x == 3 then Just OutOfMemory |
| 47 | + else if x == 4 then Just NullPointer |
| 48 | + else if x == 5 then Just ParseError |
| 49 | + else if x == 6 then Just ConstraintViolation |
| 50 | + else if x == 7 then Just TrustFailure |
| 51 | + else Nothing |
| 52 | + |
| 53 | +-------------------------------------------------------------------------------- |
| 54 | +-- (b) Round-trip: the encoding is faithful / lossless |
| 55 | +-------------------------------------------------------------------------------- |
| 56 | + |
| 57 | +||| Decoding the encoded form of any `Result` recovers exactly that `Result`. |
| 58 | +||| This is the master soundness fact for the seam: nothing is lost on the wire. |
| 59 | +public export |
| 60 | +resultRoundTrip : (r : Result) -> intToResult (resultToInt r) = Just r |
| 61 | +resultRoundTrip Ok = Refl |
| 62 | +resultRoundTrip Error = Refl |
| 63 | +resultRoundTrip InvalidParam = Refl |
| 64 | +resultRoundTrip OutOfMemory = Refl |
| 65 | +resultRoundTrip NullPointer = Refl |
| 66 | +resultRoundTrip ParseError = Refl |
| 67 | +resultRoundTrip ConstraintViolation = Refl |
| 68 | +resultRoundTrip TrustFailure = Refl |
| 69 | + |
| 70 | +-------------------------------------------------------------------------------- |
| 71 | +-- (a) Injectivity: distinct ABI outcomes never collide on the wire |
| 72 | +-------------------------------------------------------------------------------- |
| 73 | + |
| 74 | +||| The encoding is unambiguous: equal wire integers imply equal ABI values. |
| 75 | +||| DERIVED from the round-trip — if `resultToInt a = resultToInt b` then |
| 76 | +||| applying `intToResult` to both sides (via `cong`) gives `Just a = Just b`, |
| 77 | +||| and `injective` (the `Injective Just` instance) strips the `Just`. No case |
| 78 | +||| analysis on constructors is needed; the proof rides on `resultRoundTrip`. |
| 79 | +public export |
| 80 | +resultToIntInjective : (a : Result) -> (b : Result) -> |
| 81 | + resultToInt a = resultToInt b -> a = b |
| 82 | +resultToIntInjective a b prf = |
| 83 | + injective $ |
| 84 | + trans (sym (resultRoundTrip a)) $ |
| 85 | + trans (cong intToResult prf) (resultRoundTrip b) |
| 86 | + |
| 87 | +-------------------------------------------------------------------------------- |
| 88 | +-- Positive controls (concrete decodes, machine-checked = Refl) |
| 89 | +-------------------------------------------------------------------------------- |
| 90 | + |
| 91 | +||| The wire integer 0 decodes to `Ok`. |
| 92 | +public export |
| 93 | +decodeOk : intToResult 0 = Just Ok |
| 94 | +decodeOk = Refl |
| 95 | + |
| 96 | +||| The wire integer 7 decodes to `TrustFailure` (the last code). |
| 97 | +public export |
| 98 | +decodeTrustFailure : intToResult 7 = Just TrustFailure |
| 99 | +decodeTrustFailure = Refl |
| 100 | + |
| 101 | +||| An out-of-range wire integer decodes to `Nothing` (no spurious result). |
| 102 | +public export |
| 103 | +decodeOutOfRange : intToResult 8 = Nothing |
| 104 | +decodeOutOfRange = Refl |
| 105 | + |
| 106 | +-------------------------------------------------------------------------------- |
| 107 | +-- Negative / non-vacuity control |
| 108 | +-------------------------------------------------------------------------------- |
| 109 | + |
| 110 | +||| Two DISTINCT result codes have DISTINCT wire integers — machine-checked. |
| 111 | +||| This rules out the vacuous reading of injectivity (where the premise could |
| 112 | +||| never be satisfied): `Ok` and `Error` genuinely differ on the wire. |
| 113 | +public export |
| 114 | +okNotError : Not (resultToInt Ok = resultToInt Error) |
| 115 | +okNotError = \case Refl impossible |
| 116 | + |
| 117 | +||| A second distinct pair, for good measure: `OutOfMemory` (3) /= `ParseError` (5). |
| 118 | +public export |
| 119 | +oomNotParse : Not (resultToInt OutOfMemory = resultToInt ParseError) |
| 120 | +oomNotParse = \case Refl impossible |
0 commit comments