|
| 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 a2mliser. |
| 5 | +||| |
| 6 | +||| The structural gate (scripts/abi-ffi-gate.py) checks that the Idris ABI |
| 7 | +||| `resultToInt` encoder and the Zig FFI result enum agree by name+value. |
| 8 | +||| This module supplies the PROOF-SIDE guarantee that the encoding itself is |
| 9 | +||| SOUND: distinct ABI outcomes never collide on the wire, and the C integer |
| 10 | +||| faithfully round-trips back to the ABI value. |
| 11 | +||| |
| 12 | +||| THEOREMS: |
| 13 | +||| * intToResult — a total decoder Bits32 -> Maybe AttestationResult |
| 14 | +||| * resultRoundTrip — intToResult (resultToInt r) = Just r (lossless) |
| 15 | +||| * resultToIntInjective — derived from the round-trip via justInjective+cong |
| 16 | +||| |
| 17 | +||| Plus positive controls (concrete decode = Refl) and a machine-checked |
| 18 | +||| non-vacuity / negative control (distinct codes have distinct ints). |
| 19 | + |
| 20 | +module A2mliser.ABI.FfiSeam |
| 21 | + |
| 22 | +import A2mliser.ABI.Types |
| 23 | + |
| 24 | +%default total |
| 25 | + |
| 26 | +-------------------------------------------------------------------------------- |
| 27 | +-- Decoder (faithful inverse of resultToInt) |
| 28 | +-------------------------------------------------------------------------------- |
| 29 | + |
| 30 | +||| Decode a C integer back to an AttestationResult. |
| 31 | +||| |
| 32 | +||| Built with boolean Bits32 `==` (which reduces on concrete literals) rather |
| 33 | +||| than by pattern-matching on Bits32 literals (which does not reduce |
| 34 | +||| definitionally). This makes the round-trip Refls below check. |
| 35 | +public export |
| 36 | +intToResult : Bits32 -> Maybe AttestationResult |
| 37 | +intToResult x = |
| 38 | + if x == 0 then Just Ok |
| 39 | + else if x == 1 then Just Error |
| 40 | + else if x == 2 then Just InvalidParam |
| 41 | + else if x == 3 then Just OutOfMemory |
| 42 | + else if x == 4 then Just NullPointer |
| 43 | + else if x == 5 then Just SignatureInvalid |
| 44 | + else if x == 6 then Just DigestMismatch |
| 45 | + else if x == 7 then Just ChainBroken |
| 46 | + else if x == 8 then Just KeyExpired |
| 47 | + else Nothing |
| 48 | + |
| 49 | +-------------------------------------------------------------------------------- |
| 50 | +-- (b) Faithful / lossless round-trip |
| 51 | +-------------------------------------------------------------------------------- |
| 52 | + |
| 53 | +||| The encoding is lossless: decoding an encoded result recovers it exactly. |
| 54 | +||| Each clause reduces by computing the concrete boolean `==` chain. |
| 55 | +public export |
| 56 | +resultRoundTrip : (r : AttestationResult) -> intToResult (resultToInt r) = Just r |
| 57 | +resultRoundTrip Ok = Refl |
| 58 | +resultRoundTrip Error = Refl |
| 59 | +resultRoundTrip InvalidParam = Refl |
| 60 | +resultRoundTrip OutOfMemory = Refl |
| 61 | +resultRoundTrip NullPointer = Refl |
| 62 | +resultRoundTrip SignatureInvalid = Refl |
| 63 | +resultRoundTrip DigestMismatch = Refl |
| 64 | +resultRoundTrip ChainBroken = Refl |
| 65 | +resultRoundTrip KeyExpired = Refl |
| 66 | + |
| 67 | +-------------------------------------------------------------------------------- |
| 68 | +-- (a) Injectivity, DERIVED from the round-trip |
| 69 | +-------------------------------------------------------------------------------- |
| 70 | + |
| 71 | +||| Injectivity of the `Just` constructor (proved locally to avoid any |
| 72 | +||| dependency beyond the prelude). |
| 73 | +justInj : {0 x, y : AttestationResult} -> Just x = Just y -> x = y |
| 74 | +justInj Refl = Refl |
| 75 | + |
| 76 | +||| The encoding is unambiguous: distinct ABI outcomes never collide on the |
| 77 | +||| wire. Derived cleanly from the round-trip: if `resultToInt a = resultToInt b` |
| 78 | +||| then applying `intToResult` to both sides and using the round-trip on each |
| 79 | +||| gives `Just a = Just b`, whence `a = b` by injectivity of `Just`. |
| 80 | +public export |
| 81 | +resultToIntInjective : (a, b : AttestationResult) |
| 82 | + -> resultToInt a = resultToInt b |
| 83 | + -> a = b |
| 84 | +resultToIntInjective a b prf = |
| 85 | + justInj $ |
| 86 | + trans (sym (resultRoundTrip a)) $ |
| 87 | + trans (cong intToResult prf) (resultRoundTrip b) |
| 88 | + |
| 89 | +-------------------------------------------------------------------------------- |
| 90 | +-- Positive controls (concrete decodes) |
| 91 | +-------------------------------------------------------------------------------- |
| 92 | + |
| 93 | +||| Decoding 0 yields Ok. |
| 94 | +public export |
| 95 | +decodeZeroIsOk : intToResult 0 = Just Ok |
| 96 | +decodeZeroIsOk = Refl |
| 97 | + |
| 98 | +||| Decoding 8 yields KeyExpired (the largest valid code). |
| 99 | +public export |
| 100 | +decodeEightIsKeyExpired : intToResult 8 = Just KeyExpired |
| 101 | +decodeEightIsKeyExpired = Refl |
| 102 | + |
| 103 | +||| Decoding an out-of-range code yields Nothing. |
| 104 | +public export |
| 105 | +decodeNineIsNothing : intToResult 9 = Nothing |
| 106 | +decodeNineIsNothing = Refl |
| 107 | + |
| 108 | +-------------------------------------------------------------------------------- |
| 109 | +-- Negative / non-vacuity control |
| 110 | +-------------------------------------------------------------------------------- |
| 111 | + |
| 112 | +||| Non-vacuity: two DISTINCT result codes encode to DISTINCT ints, machine |
| 113 | +||| checked. `resultToInt Ok` reduces to `0` and `resultToInt Error` to `1`; |
| 114 | +||| distinct primitive Bits32 literals are provably unequal, so the coverage |
| 115 | +||| checker discharges `Refl impossible`. |
| 116 | +public export |
| 117 | +okNotError : Not (resultToInt Ok = resultToInt Error) |
| 118 | +okNotError = \case Refl impossible |
| 119 | + |
| 120 | +||| A second distinct pair, for good measure. |
| 121 | +public export |
| 122 | +okNotKeyExpired : Not (resultToInt Ok = resultToInt KeyExpired) |
| 123 | +okNotKeyExpired = \case Refl impossible |
0 commit comments