Skip to content

Commit 7ac70ae

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
ABI Layer 3: McCarthy store/select array-update laws (write-then-read, read-other) (#43)
* feat(abi): add Semantics flagship proof — bounded array access safety 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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx * abi(idrisiser): add Layer-3 array-update law proofs (Invariants) 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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --------- Co-authored-by: Claude <noreply@anthropic.com>
1 parent 29e9bec commit 7ac70ae

2 files changed

Lines changed: 178 additions & 0 deletions

File tree

‎src/interface/abi/Idrisiser/ABI/Invariants.idr‎

Lines changed: 177 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,177 @@
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+
||| Array-update invariants for Idrisiser (ABI Layer 3).
5+
|||
6+
||| Layer 2 (`Idrisiser.ABI.Semantics`) proved the *in-bounds totality* of the
7+
||| generated accessor: an index is representable EXACTLY when it is `< n`, and
8+
||| out-of-range reads are unrepresentable. That is a property of READING.
9+
|||
10+
||| This module proves a genuinely DEEPER and DISTINCT class of property: the
11+
||| algebraic LAWS that relate a generated WRITE to a subsequent READ — the
12+
||| "memory model" correctness of the wrapper Idrisiser emits. These are the
13+
||| canonical store/select axioms of McCarthy's theory of arrays:
14+
|||
15+
||| * WRITE-THEN-READ (read-over-write, same index):
16+
||| reading slot `i` immediately after writing `v` into slot `i`
17+
||| returns exactly `v`. `safeReadAfterWriteSame`
18+
|||
19+
||| * READ-OTHER (read-over-write, different index):
20+
||| a write at slot `j` leaves every OTHER slot `i /= j` untouched.
21+
||| `safeReadAfterWriteOther`
22+
|||
23+
||| * DECISIVE READ-OVER-WRITE: a single, sound decision procedure on the two
24+
||| indices that returns the value a post-write read must yield, together
25+
||| with a proof it is correct. `safeReadOverWrite`
26+
|||
27+
||| Everything is built over the SAME model exported by Layer 2 — the same
28+
||| `SafeArray`, the same `safeIndex` — so the two layers compose. The new
29+
||| accessor `safeWrite` is the formal dual of `safeIndex`. The Vect-level
30+
||| lemmas are proved here by hand (induction on the index / vector), NOT
31+
||| delegated to a library lemma, so this is a self-contained genuine proof.
32+
|||
33+
||| Controls: a POSITIVE witness that a concrete write-then-read returns the
34+
||| written element, a POSITIVE witness that a neighbouring slot is preserved,
35+
||| and a NEGATIVE / non-vacuity control (`Not (... = oldValue)`) showing the
36+
||| write genuinely changed the slot — machine-checked.
37+
38+
module Idrisiser.ABI.Invariants
39+
40+
import Idrisiser.ABI.Semantics
41+
import Data.Fin
42+
import Data.Vect
43+
import Decidable.Equality
44+
45+
%default total
46+
47+
--------------------------------------------------------------------------------
48+
-- 1. The write accessor: formal dual of Layer 2's `safeIndex`
49+
--------------------------------------------------------------------------------
50+
51+
||| Write `v` into slot `i` of a length-indexed buffer. Like `safeIndex`, it
52+
||| takes a *proven* index `Fin n`, so there is no error path and the length is
53+
||| preserved in the TYPE: a write can never resize or escape the buffer. This
54+
||| is the store half of the generated read/write pair.
55+
public export
56+
safeWrite : SafeArray n a -> Fin n -> a -> SafeArray n a
57+
safeWrite (MkSafeArray xs) i v = MkSafeArray (replaceAt i v xs)
58+
59+
--------------------------------------------------------------------------------
60+
-- 2. Vect-level lemmas (proved by hand here)
61+
--------------------------------------------------------------------------------
62+
63+
||| WRITE-THEN-READ at the Vect level: after replacing slot `i` with `v`,
64+
||| reading slot `i` yields `v`. Proved by induction on the index, mirroring
65+
||| the recursive structure of both `index` and `replaceAt`.
66+
export
67+
indexReplaceAtSame : (i : Fin n) -> (v : a) -> (xs : Vect n a) ->
68+
index i (replaceAt i v xs) = v
69+
indexReplaceAtSame FZ v (_ :: _) = Refl
70+
indexReplaceAtSame (FS k) v (_ :: ys) = indexReplaceAtSame k v ys
71+
72+
||| READ-OTHER at the Vect level: a write at slot `j` does not disturb a
73+
||| DIFFERENT slot `i /= j`. Proved by induction on both indices; the two
74+
||| `FZ`/`FS` cross cases are immediate, the `FS`/`FS` case recurses with the
75+
||| tail-level distinctness derived from injectivity of `FS`.
76+
export
77+
indexReplaceAtOther : (i, j : Fin n) -> Not (i = j) -> (v : a) ->
78+
(xs : Vect n a) ->
79+
index i (replaceAt j v xs) = index i xs
80+
indexReplaceAtOther FZ FZ neq _ (_ :: _) = absurd (neq Refl)
81+
indexReplaceAtOther FZ (FS _) _ _ (_ :: _) = Refl
82+
indexReplaceAtOther (FS _) FZ _ _ (_ :: _) = Refl
83+
indexReplaceAtOther (FS k) (FS m) neq v (_ :: ys) =
84+
indexReplaceAtOther k m (\eq => neq (cong FS eq)) v ys
85+
86+
--------------------------------------------------------------------------------
87+
-- 3. The Layer-3 laws, lifted to the SafeArray model
88+
--------------------------------------------------------------------------------
89+
90+
||| WRITE-THEN-READ LAW (read-over-write, same index): reading slot `i` of the
91+
||| array produced by writing `v` into slot `i` returns exactly `v`. This is
92+
||| the store/select axiom for matching indices.
93+
public export
94+
safeReadAfterWriteSame : (arr : SafeArray n a) -> (i : Fin n) -> (v : a) ->
95+
safeIndex (safeWrite arr i v) i = v
96+
safeReadAfterWriteSame (MkSafeArray xs) i v = indexReplaceAtSame i v xs
97+
98+
||| READ-OTHER LAW (read-over-write, different index): writing `v` into slot `j`
99+
||| leaves every other slot `i /= j` exactly as it was. This is the locality /
100+
||| non-interference axiom that makes the generated buffer a real array.
101+
public export
102+
safeReadAfterWriteOther : (arr : SafeArray n a) -> (i, j : Fin n) ->
103+
Not (i = j) -> (v : a) ->
104+
safeIndex (safeWrite arr j v) i = safeIndex arr i
105+
safeReadAfterWriteOther (MkSafeArray xs) i j neq v =
106+
indexReplaceAtOther i j neq v xs
107+
108+
--------------------------------------------------------------------------------
109+
-- 4. Decisive read-over-write: sound decision procedure
110+
--------------------------------------------------------------------------------
111+
112+
||| The value a post-write read MUST return, decided on the two indices.
113+
|||
114+
||| `decEq` on `Fin n` is the natural, sound+complete decision here. When the
115+
||| indices coincide we know (by the write-then-read law) the result is the
116+
||| written value; when they differ we know (by the read-other law) the result
117+
||| is the original element. `safeReadOverWriteCorrect` proves this dispatch
118+
||| agrees with the actual accessor on the actual array — no case is guessed.
119+
public export
120+
predictReadOverWrite : (arr : SafeArray n a) -> (i, j : Fin n) -> (v : a) -> a
121+
predictReadOverWrite arr i j v = case decEq i j of
122+
Yes _ => v
123+
No _ => safeIndex arr i
124+
125+
||| SOUNDNESS of the prediction: an actual read after the actual write equals
126+
||| the predicted value, in BOTH branches of the decision.
127+
public export
128+
safeReadOverWriteCorrect : (arr : SafeArray n a) -> (i, j : Fin n) -> (v : a) ->
129+
safeIndex (safeWrite arr j v) i =
130+
predictReadOverWrite arr i j v
131+
safeReadOverWriteCorrect arr i j v with (decEq i j)
132+
safeReadOverWriteCorrect arr i j v | Yes eq =
133+
-- i = j, so a read at i is a read at the slot just written.
134+
rewrite eq in safeReadAfterWriteSame arr j v
135+
safeReadOverWriteCorrect arr i j v | No neq =
136+
safeReadAfterWriteOther arr i j neq v
137+
138+
--------------------------------------------------------------------------------
139+
-- 5. Controls
140+
--------------------------------------------------------------------------------
141+
142+
||| A concrete 3-element array used by the controls (independent of the Layer-2
143+
||| `demoArray` so the controls here stand alone).
144+
public export
145+
ctrlArray : SafeArray 3 String
146+
ctrlArray = MkSafeArray ["alpha", "beta", "gamma"]
147+
148+
||| POSITIVE control (write-then-read): writing "delta" into slot 1 and reading
149+
||| slot 1 back returns "delta". Concrete, so it reduces by `Refl`.
150+
public export
151+
writeThenReadDelta : safeIndex (safeWrite Invariants.ctrlArray 1 "delta") 1 = "delta"
152+
writeThenReadDelta = Refl
153+
154+
||| POSITIVE control (read-other): writing "delta" into slot 1 leaves slot 0
155+
||| ("alpha") untouched. Concrete, reduces by `Refl`.
156+
public export
157+
otherSlotPreserved : safeIndex (safeWrite Invariants.ctrlArray 1 "delta") 0 = "alpha"
158+
otherSlotPreserved = Refl
159+
160+
||| POSITIVE control (decision agrees): the predictor for a same-index read
161+
||| returns the written value "delta". Reduces by `Refl`.
162+
public export
163+
predictionAtSameSlot : predictReadOverWrite Invariants.ctrlArray 1 1 "delta" = "delta"
164+
predictionAtSameSlot = Refl
165+
166+
||| NEGATIVE / non-vacuity control: the write GENUINELY changed slot 1 — after
167+
||| writing "delta", slot 1 is NOT the old value "beta". Were the laws vacuous
168+
||| or `safeWrite` a no-op, this refutation would be unprovable. Machine-checked
169+
||| via `safeReadAfterWriteSame` (slot 1 reads "delta") and the concrete fact
170+
||| that "delta" /= "beta".
171+
public export
172+
writeReallyChangedSlot :
173+
Not (safeIndex (safeWrite Invariants.ctrlArray 1 "delta") 1 = "beta")
174+
writeReallyChangedSlot eq =
175+
-- The accessor reads "delta" (law); chaining gives "delta" = "beta", absurd.
176+
case trans (sym (safeReadAfterWriteSame Invariants.ctrlArray 1 "delta")) eq of
177+
Refl impossible

‎src/interface/abi/idrisiser-abi.ipkg‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,3 +10,4 @@ modules = Idrisiser.ABI.Types
1010
, Idrisiser.ABI.Foreign
1111
, Idrisiser.ABI.Proofs
1212
, Idrisiser.ABI.Semantics
13+
, Idrisiser.ABI.Invariants

0 commit comments

Comments
 (0)