diff --git a/src/interface/abi/Anvomidaviser/ABI/FfiSeam.idr b/src/interface/abi/Anvomidaviser/ABI/FfiSeam.idr new file mode 100644 index 0000000..f8ea965 --- /dev/null +++ b/src/interface/abi/Anvomidaviser/ABI/FfiSeam.idr @@ -0,0 +1,147 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Layer-4 ABI<->FFI seam proof for Anvomidaviser. +||| +||| The structural gate (scripts/abi-ffi-gate.py) checks that the Idris `Result` +||| enum and the Zig FFI enum agree by name and value. This module supplies the +||| PROOF-SIDE guarantee that the encoding itself is SOUND: +||| +||| * `resultToIntInjective` — distinct ABI outcomes never collide on the wire. +||| * `intToResult` / `resultRoundTrip` — the C integer faithfully round-trips +||| back to the originating ABI value (the encoding is lossless). +||| +||| Together these seal the seam: an FFI result code carries exactly one ABI +||| meaning, and that meaning is recoverable. + +module Anvomidaviser.ABI.FfiSeam + +import Anvomidaviser.ABI.Types + +%default total + +-------------------------------------------------------------------------------- +-- Injectivity of the encoding +-------------------------------------------------------------------------------- + +||| The result-code encoding is injective: if two `Result`s encode to the same +||| C integer, they are the same `Result`. Proved directly by nested case on +||| both arguments; the diagonal is `Refl`, every off-diagonal pair is refuted +||| because its two distinct primitive `Bits32` literals cannot be equal. +export +resultToIntInjective : (a : Result) -> (b : Result) + -> resultToInt a = resultToInt b -> a = b +resultToIntInjective Ok Ok _ = Refl +resultToIntInjective Error Error _ = Refl +resultToIntInjective InvalidParam InvalidParam _ = Refl +resultToIntInjective OutOfMemory OutOfMemory _ = Refl +resultToIntInjective NullPointer NullPointer _ = Refl +resultToIntInjective RuleViolation RuleViolation _ = Refl +resultToIntInjective Ok Error prf = void (the Void (case prf of Refl impossible)) +resultToIntInjective Ok InvalidParam prf = void (the Void (case prf of Refl impossible)) +resultToIntInjective Ok OutOfMemory prf = void (the Void (case prf of Refl impossible)) +resultToIntInjective Ok NullPointer prf = void (the Void (case prf of Refl impossible)) +resultToIntInjective Ok RuleViolation prf = void (the Void (case prf of Refl impossible)) +resultToIntInjective Error Ok prf = void (the Void (case prf of Refl impossible)) +resultToIntInjective Error InvalidParam prf = void (the Void (case prf of Refl impossible)) +resultToIntInjective Error OutOfMemory prf = void (the Void (case prf of Refl impossible)) +resultToIntInjective Error NullPointer prf = void (the Void (case prf of Refl impossible)) +resultToIntInjective Error RuleViolation prf = void (the Void (case prf of Refl impossible)) +resultToIntInjective InvalidParam Ok prf = void (the Void (case prf of Refl impossible)) +resultToIntInjective InvalidParam Error prf = void (the Void (case prf of Refl impossible)) +resultToIntInjective InvalidParam OutOfMemory prf = void (the Void (case prf of Refl impossible)) +resultToIntInjective InvalidParam NullPointer prf = void (the Void (case prf of Refl impossible)) +resultToIntInjective InvalidParam RuleViolation prf = void (the Void (case prf of Refl impossible)) +resultToIntInjective OutOfMemory Ok prf = void (the Void (case prf of Refl impossible)) +resultToIntInjective OutOfMemory Error prf = void (the Void (case prf of Refl impossible)) +resultToIntInjective OutOfMemory InvalidParam prf = void (the Void (case prf of Refl impossible)) +resultToIntInjective OutOfMemory NullPointer prf = void (the Void (case prf of Refl impossible)) +resultToIntInjective OutOfMemory RuleViolation prf = void (the Void (case prf of Refl impossible)) +resultToIntInjective NullPointer Ok prf = void (the Void (case prf of Refl impossible)) +resultToIntInjective NullPointer Error prf = void (the Void (case prf of Refl impossible)) +resultToIntInjective NullPointer InvalidParam prf = void (the Void (case prf of Refl impossible)) +resultToIntInjective NullPointer OutOfMemory prf = void (the Void (case prf of Refl impossible)) +resultToIntInjective NullPointer RuleViolation prf = void (the Void (case prf of Refl impossible)) +resultToIntInjective RuleViolation Ok prf = void (the Void (case prf of Refl impossible)) +resultToIntInjective RuleViolation Error prf = void (the Void (case prf of Refl impossible)) +resultToIntInjective RuleViolation InvalidParam prf = void (the Void (case prf of Refl impossible)) +resultToIntInjective RuleViolation OutOfMemory prf = void (the Void (case prf of Refl impossible)) +resultToIntInjective RuleViolation NullPointer prf = void (the Void (case prf of Refl impossible)) + +-------------------------------------------------------------------------------- +-- Faithful decoder + round-trip +-------------------------------------------------------------------------------- + +||| Decode a C integer back into a `Result`. Unknown codes map to `Nothing`. +||| Implemented with boolean `Bits32` `==`, which reduces on concrete literals, +||| so the round-trip property below holds definitionally. +export +intToResult : Bits32 -> Maybe Result +intToResult x = + if x == 0 then Just Ok + else if x == 1 then Just Error + else if x == 2 then Just InvalidParam + else if x == 3 then Just OutOfMemory + else if x == 4 then Just NullPointer + else if x == 5 then Just RuleViolation + else Nothing + +||| The encoding is lossless: decoding the encoding of any `Result` recovers it. +export +resultRoundTrip : (r : Result) -> intToResult (resultToInt r) = Just r +resultRoundTrip Ok = Refl +resultRoundTrip Error = Refl +resultRoundTrip InvalidParam = Refl +resultRoundTrip OutOfMemory = Refl +resultRoundTrip NullPointer = Refl +resultRoundTrip RuleViolation = Refl + +||| `Just` is injective (local lemma, used by the round-trip derivation below). +justInj : {0 x, y : Result} -> Just x = Just y -> x = y +justInj Refl = Refl + +||| Injectivity, re-derived from the round-trip law: if the encodings agree then +||| their decodings agree, and the decoder pins each back to its own `Just`. +||| An independent witness corroborating `resultToIntInjective`. +export +resultToIntInjectiveViaRoundTrip : (a : Result) -> (b : Result) + -> resultToInt a = resultToInt b -> a = b +resultToIntInjectiveViaRoundTrip a b prf = + justInj $ + rewrite sym (resultRoundTrip a) in + rewrite sym (resultRoundTrip b) in + cong intToResult prf + +-------------------------------------------------------------------------------- +-- Positive controls (concrete decodes) +-------------------------------------------------------------------------------- + +||| Decoding 0 yields Ok. +export +decodeZeroIsOk : intToResult 0 = Just Ok +decodeZeroIsOk = Refl + +||| Decoding 5 yields RuleViolation (the highest defined code). +export +decodeFiveIsRuleViolation : intToResult 5 = Just RuleViolation +decodeFiveIsRuleViolation = Refl + +||| Decoding an out-of-range code yields Nothing. +export +decodeSixIsNothing : intToResult 6 = Nothing +decodeSixIsNothing = Refl + +-------------------------------------------------------------------------------- +-- Negative / non-vacuity control +-------------------------------------------------------------------------------- + +||| Non-vacuity: two DISTINCT result codes encode to DISTINCT integers, so the +||| injectivity theorem is not trivially satisfied by an empty domain. +export +okEncodingNotErrorEncoding : Not (resultToInt Ok = resultToInt Error) +okEncodingNotErrorEncoding = \case Refl impossible + +||| A second distinct pair, for good measure: Ok and RuleViolation differ. +export +okEncodingNotRuleViolationEncoding : Not (resultToInt Ok = resultToInt RuleViolation) +okEncodingNotRuleViolationEncoding = \case Refl impossible diff --git a/src/interface/abi/anvomidaviser-abi.ipkg b/src/interface/abi/anvomidaviser-abi.ipkg index 4eaa2b5..30d8ea2 100644 --- a/src/interface/abi/anvomidaviser-abi.ipkg +++ b/src/interface/abi/anvomidaviser-abi.ipkg @@ -1,4 +1,4 @@ -- SPDX-License-Identifier: MPL-2.0 package anvomidaviser-abi sourcedir = "." -modules = Anvomidaviser.ABI.Types, Anvomidaviser.ABI.Layout, Anvomidaviser.ABI.Foreign, Anvomidaviser.ABI.Proofs, Anvomidaviser.ABI.Semantics, Anvomidaviser.ABI.Invariants +modules = Anvomidaviser.ABI.Types, Anvomidaviser.ABI.Layout, Anvomidaviser.ABI.Foreign, Anvomidaviser.ABI.Proofs, Anvomidaviser.ABI.Semantics, Anvomidaviser.ABI.Invariants, Anvomidaviser.ABI.FfiSeam