From 2de801fc3ba081074a998ad4928c5aedb0b29cd0 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 19:29:38 +0000 Subject: [PATCH 1/2] =?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/2] 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