Skip to content

Commit 29e9bec

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
feat(abi): add Semantics flagship proof — bounded array access safety (#42)
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). Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx Co-authored-by: Claude <noreply@anthropic.com>
1 parent 5f53198 commit 29e9bec

2 files changed

Lines changed: 180 additions & 0 deletions

File tree

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

Lines changed: 179 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,179 @@
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+
||| Flagship semantic proof for Idrisiser (ABI Layer 2).
5+
|||
6+
||| Idrisiser's headline promise is to "generate proven-correct wrappers using
7+
||| Idris2 dependent types". The canonical such wrapper is a *bounded array
8+
||| accessor*: a generated function that reads element `i` of an `n`-element
9+
||| array and is GUARANTEED never to read out of bounds at runtime.
10+
|||
11+
||| This module gives that promise a real, machine-checked meaning:
12+
|||
13+
||| 1. A faithful model of a length-indexed array (`SafeArray n a` wrapping a
14+
||| `Vect n a`) and its total accessor `safeIndex : SafeArray n a -> Fin n
15+
||| -> a`.
16+
||| 2. The headline property `InBounds i n` — inhabited EXACTLY when `i < n`
17+
||| (it carries an `LT i n` proof). The out-of-range case has no
18+
||| constructor, and in particular NO index exists into an empty array
19+
||| (`Uninhabited (InBounds i 0)`): out-of-range access is unrepresentable.
20+
||| 3. A sound AND complete decision procedure `decInBounds` returning a real
21+
||| `Dec (InBounds i n)`, backed by `Data.Nat.isLT`.
22+
||| 4. A totality / no-off-by-one fact: the proven index round-trips exactly to
23+
||| the requested raw position (`finToNat (toFin ok) = i`), via the
24+
||| hand-proved `finToNatNatToFinLT`. `safeIndex` is total — no error code,
25+
||| no partiality.
26+
||| 5. A certifier into the ABI's `Totality` witness with a soundness proof
27+
||| (`certifyBounded` returns `Total` only when the index is genuinely in
28+
||| bounds).
29+
||| 6. A POSITIVE control (an inhabited witness that reads the expected
30+
||| element) and NEGATIVE controls (`Not (InBounds 5 3)` and the empty
31+
||| array), all machine-checked.
32+
33+
module Idrisiser.ABI.Semantics
34+
35+
import Idrisiser.ABI.Types
36+
import Data.Fin
37+
import Data.Nat
38+
import Data.Vect
39+
import Decidable.Equality
40+
41+
%default total
42+
43+
--------------------------------------------------------------------------------
44+
-- 1. Faithful model
45+
--------------------------------------------------------------------------------
46+
47+
||| A generated bounded-array wrapper: a length-indexed buffer. The length `n`
48+
||| is part of the TYPE, so it cannot drift from the data at runtime.
49+
public export
50+
record SafeArray (n : Nat) (a : Type) where
51+
constructor MkSafeArray
52+
buffer : Vect n a
53+
54+
||| The total, never-failing accessor that Idrisiser's codegen emits. It takes
55+
||| a *proven* index `Fin n`; there is no error path and no partiality, so the
56+
||| result is always a genuine element of the array.
57+
public export
58+
safeIndex : SafeArray n a -> Fin n -> a
59+
safeIndex (MkSafeArray xs) i = index i xs
60+
61+
--------------------------------------------------------------------------------
62+
-- 2. The headline property: InBounds
63+
--------------------------------------------------------------------------------
64+
65+
||| `InBounds i n` is inhabited exactly when the raw natural index `i` is a
66+
||| legal index into an `n`-element array, i.e. `i < n`. The witness carries an
67+
||| `LT i n` proof, from which a real `Fin n` safe index is computed.
68+
|||
69+
||| There is deliberately no constructor for the out-of-range case: when
70+
||| `i >= n` there is no `LT i n`, so `InBounds i n` cannot be built.
71+
public export
72+
data InBounds : (i : Nat) -> (n : Nat) -> Type where
73+
MkInBounds : (prf : LT i n) -> InBounds i n
74+
75+
||| Compute the proven safe index from an in-bounds witness.
76+
public export
77+
toFin : {i, n : Nat} -> InBounds i n -> Fin n
78+
toFin (MkInBounds prf) = natToFinLT i {prf}
79+
80+
||| There is NO index at all into an empty array, so any claim that some `i` is
81+
||| in bounds of a 0-length array is absurd. This is the formal statement that
82+
||| out-of-range access is unrepresentable in the model.
83+
public export
84+
Uninhabited (InBounds i 0) where
85+
uninhabited (MkInBounds prf) = absurd prf
86+
87+
--------------------------------------------------------------------------------
88+
-- 3. Sound + complete decision procedure
89+
--------------------------------------------------------------------------------
90+
91+
||| Decide whether raw index `i` is in bounds of an `n`-element array.
92+
|||
93+
||| SOUND: a `Yes` carries a genuine `LT i n` proof.
94+
||| COMPLETE: a `No` is a real refutation — any `InBounds i n` would yield the
95+
||| very `LT i n` that `isLT` has just shown impossible.
96+
public export
97+
decInBounds : (i : Nat) -> (n : Nat) -> Dec (InBounds i n)
98+
decInBounds i n = case isLT i n of
99+
Yes prf => Yes (MkInBounds prf)
100+
No contra => No (\(MkInBounds prf) => contra prf)
101+
102+
--------------------------------------------------------------------------------
103+
-- 4. Totality / no-off-by-one fact
104+
--------------------------------------------------------------------------------
105+
106+
||| The proven index lands exactly on the requested raw position: converting an
107+
||| `LT i n` proof to a `Fin n` and back to a `Nat` returns `i`. Proved by
108+
||| induction on the `LT` witness — no `believe_me`, no `assert`.
109+
public export
110+
finToNatNatToFinLT : (i : Nat) -> (prf : LT i n) ->
111+
finToNat (natToFinLT i {prf}) = i
112+
finToNatNatToFinLT Z (LTESucc _) = Refl
113+
finToNatNatToFinLT (S k) (LTESucc p) = cong S (finToNatNatToFinLT k p)
114+
115+
||| For any proven index into any array, the index the accessor uses round-trips
116+
||| back to the requested raw position `i`. This is the "no off-by-one, no
117+
||| runtime failure" guarantee: `safeIndex` reads precisely slot `i`.
118+
public export
119+
safeIndexUsesExactSlot : {i, n : Nat} -> (arr : SafeArray n a) ->
120+
(ok : InBounds i n) -> finToNat (toFin ok) = i
121+
safeIndexUsesExactSlot arr (MkInBounds prf) = finToNatNatToFinLT i prf
122+
123+
--------------------------------------------------------------------------------
124+
-- 5. Certifier into the ABI Totality witness
125+
--------------------------------------------------------------------------------
126+
127+
||| Certify a candidate (raw index, length) pair: `Total` when the generated
128+
||| accessor is provably never-failing for that index, `Covering` otherwise.
129+
public export
130+
certifyBounded : (i : Nat) -> (n : Nat) -> Totality
131+
certifyBounded i n = case decInBounds i n of
132+
Yes _ => Total
133+
No _ => Covering
134+
135+
||| Soundness of the certifier: it returns `Total` only when the index really
136+
||| is in bounds (so the generated wrapper really is failure-free).
137+
public export
138+
certifyBoundedSound : (i : Nat) -> (n : Nat) ->
139+
certifyBounded i n = Total -> InBounds i n
140+
certifyBoundedSound i n eq with (decInBounds i n)
141+
certifyBoundedSound i n eq | Yes ok = ok
142+
certifyBoundedSound i n Refl | No _ impossible
143+
144+
--------------------------------------------------------------------------------
145+
-- 6. Controls
146+
--------------------------------------------------------------------------------
147+
148+
||| A concrete 3-element array used by the controls.
149+
public export
150+
demoArray : SafeArray 3 String
151+
demoArray = MkSafeArray ["alpha", "beta", "gamma"]
152+
153+
||| POSITIVE control: index 2 is in bounds of a 3-element array (explicit,
154+
||| inhabited witness carrying a real `LT 2 3` proof).
155+
public export
156+
idx2InBounds : InBounds 2 3
157+
idx2InBounds = MkInBounds (LTESucc (LTESucc (LTESucc LTEZero)))
158+
159+
||| The positive control actually reads the expected element through the total
160+
||| accessor. Concrete, so it reduces by `Refl`.
161+
public export
162+
demoReadsGamma : safeIndex Semantics.demoArray (toFin Semantics.idx2InBounds) = "gamma"
163+
demoReadsGamma = Refl
164+
165+
||| The positive control's proven index round-trips to raw position 2.
166+
public export
167+
idx2RoundTrips : finToNat (toFin Semantics.idx2InBounds) = 2
168+
idx2RoundTrips = Refl
169+
170+
||| NEGATIVE control: index 5 is NOT in bounds of a 3-element array — a
171+
||| machine-checked refutation of the bad case (no `LT 5 3` exists).
172+
public export
173+
idx5OutOfBounds : Not (InBounds 5 3)
174+
idx5OutOfBounds (MkInBounds prf) = absurd prf
175+
176+
||| NEGATIVE control: there is no index at all into an empty array.
177+
public export
178+
noIndexIntoEmpty : Not (InBounds i 0)
179+
noIndexIntoEmpty = absurd

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,3 +9,4 @@ modules = Idrisiser.ABI.Types
99
, Idrisiser.ABI.Layout
1010
, Idrisiser.ABI.Foreign
1111
, Idrisiser.ABI.Proofs
12+
, Idrisiser.ABI.Semantics

0 commit comments

Comments
 (0)