From 2de801fc3ba081074a998ad4928c5aedb0b29cd0 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 19:29:38 +0000 Subject: [PATCH 1/3] =?UTF-8?q?feat(abi):=20add=20Semantics=20flagship=20p?= =?UTF-8?q?roof=20=E2=80=94=20bounded=20array=20access=20safety?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Raise the Idrisiser Idris2 ABI to Layer 2 with a genuine, machine-checked semantic proof of the repo's headline domain property (proven-correct wrappers via dependent types). Module Idrisiser.ABI.Semantics models a length-indexed SafeArray (Vect n a) with a total accessor safeIndex : SafeArray n a -> Fin n -> a, and proves: - InBounds i n is inhabited exactly when i < n (carries an LT i n proof); the out-of-range case has no constructor. - Uninhabited (InBounds i 0): no index exists into an empty array, so out-of-range access is unrepresentable. - decInBounds : sound + complete Dec (InBounds i n), backed by isLT. - finToNatNatToFinLT / safeIndexUsesExactSlot: the proven index round-trips exactly to the requested raw position (no off-by-one, no runtime failure). - certifyBounded + certifyBoundedSound: certifier into the ABI Totality witness, returning Total only when genuinely in bounds. - Positive control (idx2InBounds reads "gamma") and negative controls (Not (InBounds 5 3), Not (InBounds i 0)), all machine-checked. No believe_me / postulate / assert; the headline property is non-vacuous (a deliberately-false InBounds 5 3 witness is rejected by idris2 0.7.0). Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- src/interface/abi/Idrisiser/ABI/Semantics.idr | 179 ++++++++++++++++++ src/interface/abi/idrisiser-abi.ipkg | 1 + 2 files changed, 180 insertions(+) create mode 100644 src/interface/abi/Idrisiser/ABI/Semantics.idr diff --git a/src/interface/abi/Idrisiser/ABI/Semantics.idr b/src/interface/abi/Idrisiser/ABI/Semantics.idr new file mode 100644 index 0000000..e8eb928 --- /dev/null +++ b/src/interface/abi/Idrisiser/ABI/Semantics.idr @@ -0,0 +1,179 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Flagship semantic proof for Idrisiser (ABI Layer 2). +||| +||| Idrisiser's headline promise is to "generate proven-correct wrappers using +||| Idris2 dependent types". The canonical such wrapper is a *bounded array +||| accessor*: a generated function that reads element `i` of an `n`-element +||| array and is GUARANTEED never to read out of bounds at runtime. +||| +||| This module gives that promise a real, machine-checked meaning: +||| +||| 1. A faithful model of a length-indexed array (`SafeArray n a` wrapping a +||| `Vect n a`) and its total accessor `safeIndex : SafeArray n a -> Fin n +||| -> a`. +||| 2. The headline property `InBounds i n` — inhabited EXACTLY when `i < n` +||| (it carries an `LT i n` proof). The out-of-range case has no +||| constructor, and in particular NO index exists into an empty array +||| (`Uninhabited (InBounds i 0)`): out-of-range access is unrepresentable. +||| 3. A sound AND complete decision procedure `decInBounds` returning a real +||| `Dec (InBounds i n)`, backed by `Data.Nat.isLT`. +||| 4. A totality / no-off-by-one fact: the proven index round-trips exactly to +||| the requested raw position (`finToNat (toFin ok) = i`), via the +||| hand-proved `finToNatNatToFinLT`. `safeIndex` is total — no error code, +||| no partiality. +||| 5. A certifier into the ABI's `Totality` witness with a soundness proof +||| (`certifyBounded` returns `Total` only when the index is genuinely in +||| bounds). +||| 6. A POSITIVE control (an inhabited witness that reads the expected +||| element) and NEGATIVE controls (`Not (InBounds 5 3)` and the empty +||| array), all machine-checked. + +module Idrisiser.ABI.Semantics + +import Idrisiser.ABI.Types +import Data.Fin +import Data.Nat +import Data.Vect +import Decidable.Equality + +%default total + +-------------------------------------------------------------------------------- +-- 1. Faithful model +-------------------------------------------------------------------------------- + +||| A generated bounded-array wrapper: a length-indexed buffer. The length `n` +||| is part of the TYPE, so it cannot drift from the data at runtime. +public export +record SafeArray (n : Nat) (a : Type) where + constructor MkSafeArray + buffer : Vect n a + +||| The total, never-failing accessor that Idrisiser's codegen emits. It takes +||| a *proven* index `Fin n`; there is no error path and no partiality, so the +||| result is always a genuine element of the array. +public export +safeIndex : SafeArray n a -> Fin n -> a +safeIndex (MkSafeArray xs) i = index i xs + +-------------------------------------------------------------------------------- +-- 2. The headline property: InBounds +-------------------------------------------------------------------------------- + +||| `InBounds i n` is inhabited exactly when the raw natural index `i` is a +||| legal index into an `n`-element array, i.e. `i < n`. The witness carries an +||| `LT i n` proof, from which a real `Fin n` safe index is computed. +||| +||| There is deliberately no constructor for the out-of-range case: when +||| `i >= n` there is no `LT i n`, so `InBounds i n` cannot be built. +public export +data InBounds : (i : Nat) -> (n : Nat) -> Type where + MkInBounds : (prf : LT i n) -> InBounds i n + +||| Compute the proven safe index from an in-bounds witness. +public export +toFin : {i, n : Nat} -> InBounds i n -> Fin n +toFin (MkInBounds prf) = natToFinLT i {prf} + +||| There is NO index at all into an empty array, so any claim that some `i` is +||| in bounds of a 0-length array is absurd. This is the formal statement that +||| out-of-range access is unrepresentable in the model. +public export +Uninhabited (InBounds i 0) where + uninhabited (MkInBounds prf) = absurd prf + +-------------------------------------------------------------------------------- +-- 3. Sound + complete decision procedure +-------------------------------------------------------------------------------- + +||| Decide whether raw index `i` is in bounds of an `n`-element array. +||| +||| SOUND: a `Yes` carries a genuine `LT i n` proof. +||| COMPLETE: a `No` is a real refutation — any `InBounds i n` would yield the +||| very `LT i n` that `isLT` has just shown impossible. +public export +decInBounds : (i : Nat) -> (n : Nat) -> Dec (InBounds i n) +decInBounds i n = case isLT i n of + Yes prf => Yes (MkInBounds prf) + No contra => No (\(MkInBounds prf) => contra prf) + +-------------------------------------------------------------------------------- +-- 4. Totality / no-off-by-one fact +-------------------------------------------------------------------------------- + +||| The proven index lands exactly on the requested raw position: converting an +||| `LT i n` proof to a `Fin n` and back to a `Nat` returns `i`. Proved by +||| induction on the `LT` witness — no `believe_me`, no `assert`. +public export +finToNatNatToFinLT : (i : Nat) -> (prf : LT i n) -> + finToNat (natToFinLT i {prf}) = i +finToNatNatToFinLT Z (LTESucc _) = Refl +finToNatNatToFinLT (S k) (LTESucc p) = cong S (finToNatNatToFinLT k p) + +||| For any proven index into any array, the index the accessor uses round-trips +||| back to the requested raw position `i`. This is the "no off-by-one, no +||| runtime failure" guarantee: `safeIndex` reads precisely slot `i`. +public export +safeIndexUsesExactSlot : {i, n : Nat} -> (arr : SafeArray n a) -> + (ok : InBounds i n) -> finToNat (toFin ok) = i +safeIndexUsesExactSlot arr (MkInBounds prf) = finToNatNatToFinLT i prf + +-------------------------------------------------------------------------------- +-- 5. Certifier into the ABI Totality witness +-------------------------------------------------------------------------------- + +||| Certify a candidate (raw index, length) pair: `Total` when the generated +||| accessor is provably never-failing for that index, `Covering` otherwise. +public export +certifyBounded : (i : Nat) -> (n : Nat) -> Totality +certifyBounded i n = case decInBounds i n of + Yes _ => Total + No _ => Covering + +||| Soundness of the certifier: it returns `Total` only when the index really +||| is in bounds (so the generated wrapper really is failure-free). +public export +certifyBoundedSound : (i : Nat) -> (n : Nat) -> + certifyBounded i n = Total -> InBounds i n +certifyBoundedSound i n eq with (decInBounds i n) + certifyBoundedSound i n eq | Yes ok = ok + certifyBoundedSound i n Refl | No _ impossible + +-------------------------------------------------------------------------------- +-- 6. Controls +-------------------------------------------------------------------------------- + +||| A concrete 3-element array used by the controls. +public export +demoArray : SafeArray 3 String +demoArray = MkSafeArray ["alpha", "beta", "gamma"] + +||| POSITIVE control: index 2 is in bounds of a 3-element array (explicit, +||| inhabited witness carrying a real `LT 2 3` proof). +public export +idx2InBounds : InBounds 2 3 +idx2InBounds = MkInBounds (LTESucc (LTESucc (LTESucc LTEZero))) + +||| The positive control actually reads the expected element through the total +||| accessor. Concrete, so it reduces by `Refl`. +public export +demoReadsGamma : safeIndex Semantics.demoArray (toFin Semantics.idx2InBounds) = "gamma" +demoReadsGamma = Refl + +||| The positive control's proven index round-trips to raw position 2. +public export +idx2RoundTrips : finToNat (toFin Semantics.idx2InBounds) = 2 +idx2RoundTrips = Refl + +||| NEGATIVE control: index 5 is NOT in bounds of a 3-element array — a +||| machine-checked refutation of the bad case (no `LT 5 3` exists). +public export +idx5OutOfBounds : Not (InBounds 5 3) +idx5OutOfBounds (MkInBounds prf) = absurd prf + +||| NEGATIVE control: there is no index at all into an empty array. +public export +noIndexIntoEmpty : Not (InBounds i 0) +noIndexIntoEmpty = absurd diff --git a/src/interface/abi/idrisiser-abi.ipkg b/src/interface/abi/idrisiser-abi.ipkg index b781fb7..ea9b663 100644 --- a/src/interface/abi/idrisiser-abi.ipkg +++ b/src/interface/abi/idrisiser-abi.ipkg @@ -9,3 +9,4 @@ modules = Idrisiser.ABI.Types , Idrisiser.ABI.Layout , Idrisiser.ABI.Foreign , Idrisiser.ABI.Proofs + , Idrisiser.ABI.Semantics From 8c917637ced667cccf27fd9917bb251d3ff32327 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 22:57:10 +0000 Subject: [PATCH 2/3] abi(idrisiser): add Layer-3 array-update law proofs (Invariants) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add a second, deeper machine-checked theorem over the SAME Layer-2 model (SafeArray/Vect/Fin), raising the Idris2 ABI to Layer 3. New module Idrisiser.ABI.Invariants proves McCarthy's store/select array axioms — distinct from Layer-2 in-bounds totality: - safeReadAfterWriteSame: read i after write v@i = v (write-then-read) - safeReadAfterWriteOther: write@j leaves slot i/=j unchanged (read-other) - predictReadOverWrite + safeReadOverWriteCorrect: sound decEq-driven decision procedure with correctness proof in both branches Vect-level lemmas (indexReplaceAtSame, indexReplaceAtOther) proved by hand via induction, not delegated to a library lemma. Defines safeWrite as the formal dual of safeIndex. Positive controls (write-then-read, other-slot preserved, prediction agrees) plus a negative/non-vacuity control (writeReallyChangedSlot: the write genuinely changed the slot). %default total, no believe_me/postulate/assert. Clean build, zero warnings; adversarial false-equality check rejected. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- .../abi/Idrisiser/ABI/Invariants.idr | 177 ++++++++++++++++++ src/interface/abi/idrisiser-abi.ipkg | 1 + 2 files changed, 178 insertions(+) create mode 100644 src/interface/abi/Idrisiser/ABI/Invariants.idr diff --git a/src/interface/abi/Idrisiser/ABI/Invariants.idr b/src/interface/abi/Idrisiser/ABI/Invariants.idr new file mode 100644 index 0000000..eb6ccbb --- /dev/null +++ b/src/interface/abi/Idrisiser/ABI/Invariants.idr @@ -0,0 +1,177 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Array-update invariants for Idrisiser (ABI Layer 3). +||| +||| Layer 2 (`Idrisiser.ABI.Semantics`) proved the *in-bounds totality* of the +||| generated accessor: an index is representable EXACTLY when it is `< n`, and +||| out-of-range reads are unrepresentable. That is a property of READING. +||| +||| This module proves a genuinely DEEPER and DISTINCT class of property: the +||| algebraic LAWS that relate a generated WRITE to a subsequent READ — the +||| "memory model" correctness of the wrapper Idrisiser emits. These are the +||| canonical store/select axioms of McCarthy's theory of arrays: +||| +||| * WRITE-THEN-READ (read-over-write, same index): +||| reading slot `i` immediately after writing `v` into slot `i` +||| returns exactly `v`. `safeReadAfterWriteSame` +||| +||| * READ-OTHER (read-over-write, different index): +||| a write at slot `j` leaves every OTHER slot `i /= j` untouched. +||| `safeReadAfterWriteOther` +||| +||| * DECISIVE READ-OVER-WRITE: a single, sound decision procedure on the two +||| indices that returns the value a post-write read must yield, together +||| with a proof it is correct. `safeReadOverWrite` +||| +||| Everything is built over the SAME model exported by Layer 2 — the same +||| `SafeArray`, the same `safeIndex` — so the two layers compose. The new +||| accessor `safeWrite` is the formal dual of `safeIndex`. The Vect-level +||| lemmas are proved here by hand (induction on the index / vector), NOT +||| delegated to a library lemma, so this is a self-contained genuine proof. +||| +||| Controls: a POSITIVE witness that a concrete write-then-read returns the +||| written element, a POSITIVE witness that a neighbouring slot is preserved, +||| and a NEGATIVE / non-vacuity control (`Not (... = oldValue)`) showing the +||| write genuinely changed the slot — machine-checked. + +module Idrisiser.ABI.Invariants + +import Idrisiser.ABI.Semantics +import Data.Fin +import Data.Vect +import Decidable.Equality + +%default total + +-------------------------------------------------------------------------------- +-- 1. The write accessor: formal dual of Layer 2's `safeIndex` +-------------------------------------------------------------------------------- + +||| Write `v` into slot `i` of a length-indexed buffer. Like `safeIndex`, it +||| takes a *proven* index `Fin n`, so there is no error path and the length is +||| preserved in the TYPE: a write can never resize or escape the buffer. This +||| is the store half of the generated read/write pair. +public export +safeWrite : SafeArray n a -> Fin n -> a -> SafeArray n a +safeWrite (MkSafeArray xs) i v = MkSafeArray (replaceAt i v xs) + +-------------------------------------------------------------------------------- +-- 2. Vect-level lemmas (proved by hand here) +-------------------------------------------------------------------------------- + +||| WRITE-THEN-READ at the Vect level: after replacing slot `i` with `v`, +||| reading slot `i` yields `v`. Proved by induction on the index, mirroring +||| the recursive structure of both `index` and `replaceAt`. +export +indexReplaceAtSame : (i : Fin n) -> (v : a) -> (xs : Vect n a) -> + index i (replaceAt i v xs) = v +indexReplaceAtSame FZ v (_ :: _) = Refl +indexReplaceAtSame (FS k) v (_ :: ys) = indexReplaceAtSame k v ys + +||| READ-OTHER at the Vect level: a write at slot `j` does not disturb a +||| DIFFERENT slot `i /= j`. Proved by induction on both indices; the two +||| `FZ`/`FS` cross cases are immediate, the `FS`/`FS` case recurses with the +||| tail-level distinctness derived from injectivity of `FS`. +export +indexReplaceAtOther : (i, j : Fin n) -> Not (i = j) -> (v : a) -> + (xs : Vect n a) -> + index i (replaceAt j v xs) = index i xs +indexReplaceAtOther FZ FZ neq _ (_ :: _) = absurd (neq Refl) +indexReplaceAtOther FZ (FS _) _ _ (_ :: _) = Refl +indexReplaceAtOther (FS _) FZ _ _ (_ :: _) = Refl +indexReplaceAtOther (FS k) (FS m) neq v (_ :: ys) = + indexReplaceAtOther k m (\eq => neq (cong FS eq)) v ys + +-------------------------------------------------------------------------------- +-- 3. The Layer-3 laws, lifted to the SafeArray model +-------------------------------------------------------------------------------- + +||| WRITE-THEN-READ LAW (read-over-write, same index): reading slot `i` of the +||| array produced by writing `v` into slot `i` returns exactly `v`. This is +||| the store/select axiom for matching indices. +public export +safeReadAfterWriteSame : (arr : SafeArray n a) -> (i : Fin n) -> (v : a) -> + safeIndex (safeWrite arr i v) i = v +safeReadAfterWriteSame (MkSafeArray xs) i v = indexReplaceAtSame i v xs + +||| READ-OTHER LAW (read-over-write, different index): writing `v` into slot `j` +||| leaves every other slot `i /= j` exactly as it was. This is the locality / +||| non-interference axiom that makes the generated buffer a real array. +public export +safeReadAfterWriteOther : (arr : SafeArray n a) -> (i, j : Fin n) -> + Not (i = j) -> (v : a) -> + safeIndex (safeWrite arr j v) i = safeIndex arr i +safeReadAfterWriteOther (MkSafeArray xs) i j neq v = + indexReplaceAtOther i j neq v xs + +-------------------------------------------------------------------------------- +-- 4. Decisive read-over-write: sound decision procedure +-------------------------------------------------------------------------------- + +||| The value a post-write read MUST return, decided on the two indices. +||| +||| `decEq` on `Fin n` is the natural, sound+complete decision here. When the +||| indices coincide we know (by the write-then-read law) the result is the +||| written value; when they differ we know (by the read-other law) the result +||| is the original element. `safeReadOverWriteCorrect` proves this dispatch +||| agrees with the actual accessor on the actual array — no case is guessed. +public export +predictReadOverWrite : (arr : SafeArray n a) -> (i, j : Fin n) -> (v : a) -> a +predictReadOverWrite arr i j v = case decEq i j of + Yes _ => v + No _ => safeIndex arr i + +||| SOUNDNESS of the prediction: an actual read after the actual write equals +||| the predicted value, in BOTH branches of the decision. +public export +safeReadOverWriteCorrect : (arr : SafeArray n a) -> (i, j : Fin n) -> (v : a) -> + safeIndex (safeWrite arr j v) i = + predictReadOverWrite arr i j v +safeReadOverWriteCorrect arr i j v with (decEq i j) + safeReadOverWriteCorrect arr i j v | Yes eq = + -- i = j, so a read at i is a read at the slot just written. + rewrite eq in safeReadAfterWriteSame arr j v + safeReadOverWriteCorrect arr i j v | No neq = + safeReadAfterWriteOther arr i j neq v + +-------------------------------------------------------------------------------- +-- 5. Controls +-------------------------------------------------------------------------------- + +||| A concrete 3-element array used by the controls (independent of the Layer-2 +||| `demoArray` so the controls here stand alone). +public export +ctrlArray : SafeArray 3 String +ctrlArray = MkSafeArray ["alpha", "beta", "gamma"] + +||| POSITIVE control (write-then-read): writing "delta" into slot 1 and reading +||| slot 1 back returns "delta". Concrete, so it reduces by `Refl`. +public export +writeThenReadDelta : safeIndex (safeWrite Invariants.ctrlArray 1 "delta") 1 = "delta" +writeThenReadDelta = Refl + +||| POSITIVE control (read-other): writing "delta" into slot 1 leaves slot 0 +||| ("alpha") untouched. Concrete, reduces by `Refl`. +public export +otherSlotPreserved : safeIndex (safeWrite Invariants.ctrlArray 1 "delta") 0 = "alpha" +otherSlotPreserved = Refl + +||| POSITIVE control (decision agrees): the predictor for a same-index read +||| returns the written value "delta". Reduces by `Refl`. +public export +predictionAtSameSlot : predictReadOverWrite Invariants.ctrlArray 1 1 "delta" = "delta" +predictionAtSameSlot = Refl + +||| NEGATIVE / non-vacuity control: the write GENUINELY changed slot 1 — after +||| writing "delta", slot 1 is NOT the old value "beta". Were the laws vacuous +||| or `safeWrite` a no-op, this refutation would be unprovable. Machine-checked +||| via `safeReadAfterWriteSame` (slot 1 reads "delta") and the concrete fact +||| that "delta" /= "beta". +public export +writeReallyChangedSlot : + Not (safeIndex (safeWrite Invariants.ctrlArray 1 "delta") 1 = "beta") +writeReallyChangedSlot eq = + -- The accessor reads "delta" (law); chaining gives "delta" = "beta", absurd. + case trans (sym (safeReadAfterWriteSame Invariants.ctrlArray 1 "delta")) eq of + Refl impossible diff --git a/src/interface/abi/idrisiser-abi.ipkg b/src/interface/abi/idrisiser-abi.ipkg index ea9b663..4a05ff5 100644 --- a/src/interface/abi/idrisiser-abi.ipkg +++ b/src/interface/abi/idrisiser-abi.ipkg @@ -10,3 +10,4 @@ modules = Idrisiser.ABI.Types , Idrisiser.ABI.Foreign , Idrisiser.ABI.Proofs , Idrisiser.ABI.Semantics + , Idrisiser.ABI.Invariants From a97f2f57197287cf2626cc27329f5f3064d3bdde Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 28 Jun 2026 05:58:47 +0000 Subject: [PATCH 3/3] abi: seal ABI<->FFI seam with Layer 4 soundness proof Add Idrisiser.ABI.FfiSeam proving the resultToInt encoding is sound: - resultRoundTrip: total decoder intToResult faithfully recovers every Result (lossless C-integer encoding). - resultToIntInjective: distinct ABI outcomes never collide on the wire, derived cleanly from the round-trip via cong + Just-injectivity. - positive controls (concrete decodes = Refl) and a machine-checked non-vacuity control (Ok and Error map to distinct wire integers). Genuine proof: no believe_me/postulate/assert_total/idris_crash. %default total, zero warnings. Registered in idrisiser-abi.ipkg. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- src/interface/abi/Idrisiser/ABI/FfiSeam.idr | 132 ++++++++++++++++++++ src/interface/abi/idrisiser-abi.ipkg | 1 + 2 files changed, 133 insertions(+) create mode 100644 src/interface/abi/Idrisiser/ABI/FfiSeam.idr diff --git a/src/interface/abi/Idrisiser/ABI/FfiSeam.idr b/src/interface/abi/Idrisiser/ABI/FfiSeam.idr new file mode 100644 index 0000000..eb2b5bf --- /dev/null +++ b/src/interface/abi/Idrisiser/ABI/FfiSeam.idr @@ -0,0 +1,132 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Layer 4 — Sealing the ABI<->FFI seam. +||| +||| The structural gate (scripts/abi-ffi-gate.py) checks that the Idris2 and +||| Zig result-code enums agree by name and value. This module supplies the +||| PROOF-SIDE guarantee that the encoding `resultToInt : Result -> Bits32` +||| is SOUND: +||| +||| * distinct ABI outcomes never collide on the wire (injectivity), and +||| * the C integer faithfully round-trips back to the ABI value +||| (a total decoder `intToResult` with `intToResult (resultToInt r) = Just r`). +||| +||| Injectivity is DERIVED from the round-trip (the cleanest route): if +||| `resultToInt a = resultToInt b` then applying `intToResult` to both sides +||| (via `cong`) and using the round-trip identities forces `Just a = Just b`, +||| whence `a = b` by injectivity of `Just`. +||| +||| The decoder is built with boolean `Bits32` `==` (which reduces on concrete +||| literals) so the round-trip proofs discharge by `Refl`. + +module Idrisiser.ABI.FfiSeam + +import Idrisiser.ABI.Types + +%default total + +-------------------------------------------------------------------------------- +-- Local helper: Just is injective +-------------------------------------------------------------------------------- + +||| `Just` is injective. Proved locally to avoid depending on a particular +||| base-library name; the single `Refl` clause forces the two payloads equal. +private +justInj : {0 x, y : a} -> Just x = Just y -> x = y +justInj Refl = Refl + +-------------------------------------------------------------------------------- +-- Decoder: C integer -> ABI Result +-------------------------------------------------------------------------------- + +||| Decode a C result code back into the ABI `Result`. +||| +||| Built with chained boolean `==` on `Bits32` rather than literal +||| pattern-matching: `==` reduces definitionally on concrete constants, so the +||| round-trip lemmas below check by `Refl`. Any integer outside the known +||| range decodes to `Nothing` (faithful: the encoder is not surjective). +public 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 ProofFailure + else Nothing + +-------------------------------------------------------------------------------- +-- (b) Faithful / lossless round-trip +-------------------------------------------------------------------------------- + +||| Encoding then decoding recovers the original ABI value: the C integer is a +||| faithful representation of every `Result`. Each clause reduces because the +||| corresponding `==` test on the concrete literal evaluates to `True`. +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 ProofFailure = Refl + +-------------------------------------------------------------------------------- +-- (a) Injectivity, derived from the round-trip +-------------------------------------------------------------------------------- + +||| The encoding is unambiguous: distinct outcomes never collide on the wire. +||| Derived from `resultRoundTrip` — no case explosion, no `believe_me`. +||| +||| Given `resultToInt a = resultToInt b`, `cong intToResult` yields +||| `intToResult (resultToInt a) = intToResult (resultToInt b)`; rewriting both +||| ends by the round-trip gives `Just a = Just b`, and injectivity of `Just` +||| strips the constructor. +export +resultToIntInjective : (a, b : Result) + -> resultToInt a = resultToInt b + -> a = b +resultToIntInjective a b prf = + justInj $ + rewrite sym (resultRoundTrip a) in + rewrite sym (resultRoundTrip b) in + cong intToResult prf + +-------------------------------------------------------------------------------- +-- Positive controls (concrete decodes, machine-checked) +-------------------------------------------------------------------------------- + +||| Decoding 0 yields Ok. +decodeZeroIsOk : intToResult 0 = Just Ok +decodeZeroIsOk = Refl + +||| Decoding 5 yields ProofFailure (the top of the range). +decodeFiveIsProofFailure : intToResult 5 = Just ProofFailure +decodeFiveIsProofFailure = Refl + +||| Decoding an out-of-range code yields Nothing (encoder is not surjective). +decodeOutOfRangeIsNothing : intToResult 99 = Nothing +decodeOutOfRangeIsNothing = Refl + +||| Round-trip control for a specific value. +roundTripOk : intToResult (resultToInt Ok) = Just Ok +roundTripOk = Refl + +-------------------------------------------------------------------------------- +-- Negative / non-vacuity control +-------------------------------------------------------------------------------- + +||| Two DISTINCT result codes have DISTINCT wire integers. This rules out the +||| vacuous reading of injectivity: the encoding genuinely separates outcomes. +||| `0 = 1` on `Bits32` is refuted by the coverage checker on distinct +||| primitive constants. +export +okWireDistinctFromError : Not (resultToInt Ok = resultToInt Error) +okWireDistinctFromError = \case Refl impossible + +||| A second non-vacuity witness across a non-adjacent pair. +export +okWireDistinctFromProofFailure : Not (resultToInt Ok = resultToInt ProofFailure) +okWireDistinctFromProofFailure = \case Refl impossible diff --git a/src/interface/abi/idrisiser-abi.ipkg b/src/interface/abi/idrisiser-abi.ipkg index 4a05ff5..6997c17 100644 --- a/src/interface/abi/idrisiser-abi.ipkg +++ b/src/interface/abi/idrisiser-abi.ipkg @@ -11,3 +11,4 @@ modules = Idrisiser.ABI.Types , Idrisiser.ABI.Proofs , Idrisiser.ABI.Semantics , Idrisiser.ABI.Invariants + , Idrisiser.ABI.FfiSeam