|
| 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 Proof for Lustreiser |
| 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 and value. This module |
| 8 | +||| supplies the *proof-side* guarantee that the encoding itself is SOUND: |
| 9 | +||| |
| 10 | +||| (a) `resultToInt` is INJECTIVE — distinct ABI outcomes never collide on |
| 11 | +||| the wire (no two `Result` values map to the same C integer). |
| 12 | +||| (b) A decoder `intToResult : Bits32 -> Maybe Result` round-trips every |
| 13 | +||| `Result` faithfully (`resultRoundTrip`), proving the encoding is |
| 14 | +||| lossless; injectivity is then DERIVED from the round-trip. |
| 15 | +||| |
| 16 | +||| Together these seal the seam: the C integer returned by the Zig FFI |
| 17 | +||| faithfully and unambiguously reconstructs the ABI `Result` it came from. |
| 18 | +||| |
| 19 | +||| Lustreiser defines exactly one FFI result-code encoder (`resultToInt`); |
| 20 | +||| there is no `ProofStatus`/`statusToInt` (or other FFI enum encoder), so |
| 21 | +||| clause (c) is vacuous here. |
| 22 | + |
| 23 | +module Lustreiser.ABI.FfiSeam |
| 24 | + |
| 25 | +import Lustreiser.ABI.Types |
| 26 | + |
| 27 | +%default total |
| 28 | + |
| 29 | +-------------------------------------------------------------------------------- |
| 30 | +-- Local lemma: Just is injective |
| 31 | +-------------------------------------------------------------------------------- |
| 32 | + |
| 33 | +||| `Just` is injective. Defined locally (Idris2 0.7.0 has no `justInjective` |
| 34 | +||| in scope here). The implicit equands are erased to avoid auto-binding a |
| 35 | +||| free lowercase name with a warning. |
| 36 | +justInj : {0 x, y : t} -> Just x = Just y -> x = y |
| 37 | +justInj Refl = Refl |
| 38 | + |
| 39 | +-------------------------------------------------------------------------------- |
| 40 | +-- (b) Faithful decoder and round-trip |
| 41 | +-------------------------------------------------------------------------------- |
| 42 | + |
| 43 | +||| Decode a C integer back into a `Result`. Built with boolean `==` on |
| 44 | +||| concrete `Bits32` literals, which reduces definitionally on each constant, |
| 45 | +||| so the round-trip `Refl`s below check. |
| 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 DeadlineViolation |
| 55 | + else if x == 6 then Just ClockError |
| 56 | + else Nothing |
| 57 | + |
| 58 | +||| Faithful (lossless) encoding: decoding the encoding of any `Result` |
| 59 | +||| recovers exactly that `Result`. Each case reduces because `intToResult` |
| 60 | +||| branches on concrete `Bits32` literals via boolean `==`. |
| 61 | +public export |
| 62 | +resultRoundTrip : (r : Result) -> intToResult (resultToInt r) = Just r |
| 63 | +resultRoundTrip Ok = Refl |
| 64 | +resultRoundTrip Error = Refl |
| 65 | +resultRoundTrip InvalidParam = Refl |
| 66 | +resultRoundTrip OutOfMemory = Refl |
| 67 | +resultRoundTrip NullPointer = Refl |
| 68 | +resultRoundTrip DeadlineViolation = Refl |
| 69 | +resultRoundTrip ClockError = Refl |
| 70 | + |
| 71 | +-------------------------------------------------------------------------------- |
| 72 | +-- (a) Injectivity of the encoding (derived from the round-trip) |
| 73 | +-------------------------------------------------------------------------------- |
| 74 | + |
| 75 | +||| The encoding is unambiguous: if two `Result`s encode to the same C |
| 76 | +||| integer, they are the same `Result`. Derived cleanly from the round-trip: |
| 77 | +||| `intToResult` applied to both sides yields `Just a = Just b`, and |
| 78 | +||| `justInj` strips the constructor. |
| 79 | +public export |
| 80 | +resultToIntInjective : (a, b : Result) -> |
| 81 | + resultToInt a = resultToInt b -> a = b |
| 82 | +resultToIntInjective a b prf = |
| 83 | + justInj $ |
| 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 | +||| Decoding 0 yields `Ok`. |
| 92 | +decodeOk : intToResult 0 = Just Ok |
| 93 | +decodeOk = Refl |
| 94 | + |
| 95 | +||| Decoding 6 yields `ClockError` (the largest code). |
| 96 | +decodeClockError : intToResult 6 = Just ClockError |
| 97 | +decodeClockError = Refl |
| 98 | + |
| 99 | +||| An out-of-range code decodes to `Nothing`. |
| 100 | +decodeUnknown : intToResult 7 = Nothing |
| 101 | +decodeUnknown = Refl |
| 102 | + |
| 103 | +-------------------------------------------------------------------------------- |
| 104 | +-- Negative / non-vacuity control (distinct codes are distinct on the wire) |
| 105 | +-------------------------------------------------------------------------------- |
| 106 | + |
| 107 | +||| Two DISTINCT result codes map to DISTINCT C integers. This is the |
| 108 | +||| non-vacuity witness: injectivity would be trivially true if every |
| 109 | +||| `Result` collapsed to one integer. `resultToInt Ok` reduces to the |
| 110 | +||| primitive `Bits32` literal 0 and `resultToInt Error` to 1; the coverage |
| 111 | +||| checker discharges `Refl impossible` for the two distinct constants. |
| 112 | +okNotError : Not (resultToInt Ok = resultToInt Error) |
| 113 | +okNotError Refl impossible |
| 114 | + |
| 115 | +||| A second distinct-code witness, away from the 0/1 boundary (5 vs 6). |
| 116 | +deadlineNotClock : Not (resultToInt DeadlineViolation = resultToInt ClockError) |
| 117 | +deadlineNotClock Refl impossible |
0 commit comments