|
| 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 for Oblibeniser. |
| 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 supplies the |
| 8 | +||| PROOF-SIDE guarantee that the encoding `resultToInt : Result -> Bits32` 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 Result. |
| 14 | +||| * resultRoundTrip — intToResult (resultToInt r) = Just r (lossless). |
| 15 | +||| * resultToIntInjective — distinct Results never share an int code, |
| 16 | +||| DERIVED from the round-trip via justInjective + cong. |
| 17 | +||| |
| 18 | +||| Plus positive controls (concrete decodes by Refl) and a non-vacuity / |
| 19 | +||| negative control (Ok and Error provably differ on the wire). |
| 20 | + |
| 21 | +module Oblibeniser.ABI.FfiSeam |
| 22 | + |
| 23 | +import Oblibeniser.ABI.Types |
| 24 | + |
| 25 | +%default total |
| 26 | + |
| 27 | +-------------------------------------------------------------------------------- |
| 28 | +-- Local lemma |
| 29 | +-------------------------------------------------------------------------------- |
| 30 | + |
| 31 | +||| `Just` is injective: peel it off both sides. Genuine proof by matching the |
| 32 | +||| single inhabiting `Refl`. |
| 33 | +private |
| 34 | +justInj : {0 a, b : ty} -> Just a = Just b -> a = b |
| 35 | +justInj Refl = Refl |
| 36 | + |
| 37 | +-------------------------------------------------------------------------------- |
| 38 | +-- Decoder |
| 39 | +-------------------------------------------------------------------------------- |
| 40 | + |
| 41 | +||| Decode a C integer back to a Result. Built with boolean `==` on Bits32 |
| 42 | +||| literals (which reduces definitionally on concrete constants), so the |
| 43 | +||| round-trip Refls below check. Any value outside 0..7 is unrepresentable |
| 44 | +||| and decodes to Nothing. |
| 45 | +public export |
| 46 | +intToResult : Bits32 -> Maybe Result |
| 47 | +intToResult x = |
| 48 | + if x == 0 then Just Ok |
| 49 | + else if x == 1 then Just Error |
| 50 | + else if x == 2 then Just InvalidParam |
| 51 | + else if x == 3 then Just OutOfMemory |
| 52 | + else if x == 4 then Just NullPointer |
| 53 | + else if x == 5 then Just NotReversible |
| 54 | + else if x == 6 then Just AuditViolation |
| 55 | + else if x == 7 then Just InverseProofFailed |
| 56 | + else Nothing |
| 57 | + |
| 58 | +-------------------------------------------------------------------------------- |
| 59 | +-- Round-trip: the encoding is lossless |
| 60 | +-------------------------------------------------------------------------------- |
| 61 | + |
| 62 | +||| Encoding then decoding recovers the original Result exactly. |
| 63 | +||| Each clause reduces through the boolean `==` ladder above. |
| 64 | +public export |
| 65 | +resultRoundTrip : (r : Result) -> intToResult (resultToInt r) = Just r |
| 66 | +resultRoundTrip Ok = Refl |
| 67 | +resultRoundTrip Error = Refl |
| 68 | +resultRoundTrip InvalidParam = Refl |
| 69 | +resultRoundTrip OutOfMemory = Refl |
| 70 | +resultRoundTrip NullPointer = Refl |
| 71 | +resultRoundTrip NotReversible = Refl |
| 72 | +resultRoundTrip AuditViolation = Refl |
| 73 | +resultRoundTrip InverseProofFailed = Refl |
| 74 | + |
| 75 | +-------------------------------------------------------------------------------- |
| 76 | +-- Injectivity, derived from the round-trip |
| 77 | +-------------------------------------------------------------------------------- |
| 78 | + |
| 79 | +||| The encoding is unambiguous: distinct ABI outcomes never collide on the |
| 80 | +||| wire. Derived purely from `resultRoundTrip`: if two Results encode to the |
| 81 | +||| same int, then decoding that int gives `Just a` and `Just b` for the same |
| 82 | +||| value, so `Just a = Just b`, hence `a = b`. |
| 83 | +public export |
| 84 | +resultToIntInjective : (a, b : Result) -> resultToInt a = resultToInt b -> a = b |
| 85 | +resultToIntInjective a b prf = |
| 86 | + justInj $ |
| 87 | + trans (sym (resultRoundTrip a)) (trans (cong intToResult prf) (resultRoundTrip b)) |
| 88 | + |
| 89 | +-------------------------------------------------------------------------------- |
| 90 | +-- Positive controls (concrete decodes by Refl) |
| 91 | +-------------------------------------------------------------------------------- |
| 92 | + |
| 93 | +||| Decoding 0 yields Ok. |
| 94 | +decodeZeroIsOk : intToResult 0 = Just Ok |
| 95 | +decodeZeroIsOk = Refl |
| 96 | + |
| 97 | +||| Decoding 7 yields InverseProofFailed (the last code). |
| 98 | +decodeSevenIsInverseProofFailed : intToResult 7 = Just InverseProofFailed |
| 99 | +decodeSevenIsInverseProofFailed = Refl |
| 100 | + |
| 101 | +||| Out-of-range codes decode to Nothing. |
| 102 | +decodeEightIsNothing : intToResult 8 = Nothing |
| 103 | +decodeEightIsNothing = Refl |
| 104 | + |
| 105 | +-------------------------------------------------------------------------------- |
| 106 | +-- Non-vacuity / negative control |
| 107 | +-------------------------------------------------------------------------------- |
| 108 | + |
| 109 | +||| Machine-checked proof that two DISTINCT result codes have DISTINCT ints: |
| 110 | +||| Ok (0) and Error (1) cannot share a wire value. This rules out a vacuous |
| 111 | +||| injectivity statement (which would hold trivially if the encoding were |
| 112 | +||| constant). The witness is `\case Refl impossible`: the coverage checker |
| 113 | +||| discharges it because the primitive Bits32 literals 0 and 1 differ. |
| 114 | +okErrorDistinctOnWire : Not (resultToInt Ok = resultToInt Error) |
| 115 | +okErrorDistinctOnWire = \case Refl impossible |
0 commit comments