ABI Layer 2: prove array-rewrite semantics preservation (+´⌽ ⇒ +´) — flagship Idris2 proof (#33)

## Summary

Raises bqniser's Idris2 ABI to **Layer 2** with its first flagship
semantic proof. bqniser's headline is detecting array patterns and
rewriting them as optimised BQN primitives; the correctness obligation
is that a rewrite is **semantics-preserving**. This proves a concrete
BQN rewrite — `+´⌽𝕩 ⇒ +´𝕩` (drop the reverse before a fold-sum) — via
`sumRev : bsum (brev xs) = bsum xs` (summation is reverse-invariant),
proven by induction.

Mirrors the estate flagship-proof pattern: array model, the equivalence
proven by induction, certifier proven sound, non-vacuous negative
control.

## Changes

- Adds `src/interface/abi/Bqniser/ABI/Semantics.idr` — `bsum`/`brev`,
`sumSnoc`, `sumRev` (the rewrite equivalence), `certifyRewriteSound`,
and negative control `revChangesOrder`.
- Registers the module in `bqniser-abi.ipkg`.

## RSR Quality Checklist

### Required
- [x] Tests pass — ABI builds clean (see Testing)
- [x] Linter clean — zero warnings
- [x] No banned language patterns
- [x] No banned functions — genuine proof
- [x] SPDX headers present
- [x] No secrets

### As Applicable
- [x] ABI/FFI changes validated — additive proof; FFI untouched

## Testing

Verified with **Idris2 0.7.0**: `idris2 --build bqniser-abi.ipkg` → exit
0, zero warnings. **Adversarial check**: a deliberately-false proof
(`brev [1,2] = [1,2]`) was rejected. `build/` removed.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx

---
_Generated by [Claude
Code](https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx)_

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

src/interface/abi/Bqniser/ABI/Semantics.idr

@@ -0,0 +1,95 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+--
+||| Flagship semantic proof for Bqniser (Idris2 ABI Layer 2).
+|||
+||| Bqniser's headline is "detect array patterns and rewrite as optimised BQN
+||| primitives". The correctness obligation for any such rewrite is that it is
+||| *semantics-preserving*. This module proves a concrete, real BQN rewrite:
+|||
+|||   +´⌽𝕩   ==>   +´𝕩          (sum-of-reverse  ==>  sum)
+|||
+||| i.e. detecting a fold-sum applied to a reversed array and dropping the
+||| reverse, because summation is invariant under reversal. The equivalence
+||| `sumRev : bsum (brev xs) = bsum xs` is proven by induction; a certifier is
+||| proven sound against it; and a negative control machine-checks that the
+||| rewrite is non-trivial (reversal genuinely changes the array).
+|||
+||| (`bsum`/`brev` are named to avoid clashing with Prelude `sum`.)
+
+module Bqniser.ABI.Semantics
+
+import Bqniser.ABI.Types
+import Data.Nat
+
+%default total
+
+--------------------------------------------------------------------------------
+-- A minimal array model with the two primitives the rewrite touches
+--------------------------------------------------------------------------------
+
+||| Fold-sum (`+´`).
+public export
+bsum : List Nat -> Nat
+bsum []        = 0
+bsum (x :: xs) = x + bsum xs
+
+||| Reverse (`⌽`), defined directly so it is convenient to induct over.
+public export
+brev : List Nat -> List Nat
+brev []        = []
+brev (x :: xs) = brev xs ++ [x]
+
+--------------------------------------------------------------------------------
+-- Semantics-preservation of the rewrite
+--------------------------------------------------------------------------------
+
+||| Sum distributes over a snoc: bsum (xs ++ [y]) = bsum xs + y.
+export
+sumSnoc : (xs : List Nat) -> (y : Nat) -> bsum (xs ++ [y]) = bsum xs + y
+sumSnoc []        y = plusZeroRightNeutral y
+sumSnoc (x :: xs) y =
+  trans (cong (x +) (sumSnoc xs y))
+        (plusAssociative x (bsum xs) y)
+
+||| The headline equivalence: summing a reversed array equals summing it, so the
+||| `+´⌽ ==> +´` rewrite preserves semantics for all inputs.
+export
+sumRev : (xs : List Nat) -> bsum (brev xs) = bsum xs
+sumRev []        = Refl
+sumRev (x :: xs) =
+  trans (sumSnoc (brev xs) x)
+        (trans (cong (+ x) (sumRev xs))
+               (plusCommutative (bsum xs) x))
+
+--------------------------------------------------------------------------------
+-- Certifier into the ABI Result, proven sound against the equivalence
+--------------------------------------------------------------------------------
+
+||| The rewrite is unconditionally valid, so the certifier always reports `Ok`.
+public export
+certifyRewrite : List Nat -> Result
+certifyRewrite _ = Ok
+
+||| Soundness: whenever the certifier reports `Ok`, the rewrite genuinely
+||| preserves the computed result for that input.
+export
+certifyRewriteSound : (xs : List Nat) -> certifyRewrite xs = Ok -> bsum (brev xs) = bsum xs
+certifyRewriteSound xs _ = sumRev xs
+
+--------------------------------------------------------------------------------
+-- Positive control
+--------------------------------------------------------------------------------
+
+export
+rewritePreservesConcrete : bsum (brev [1, 2, 3]) = bsum [1, 2, 3]
+rewritePreservesConcrete = sumRev [1, 2, 3]
+
+--------------------------------------------------------------------------------
+-- Negative control: the rewrite is non-trivial — reversal really changes the
+-- array, so the equivalence is a genuine theorem, not reverse = id.
+--------------------------------------------------------------------------------
+
+export
+revChangesOrder : Not (brev [1, 2] = [1, 2])
+revChangesOrder Refl impossible

src/interface/abi/bqniser-abi.ipkg

@@ -9,3 +9,4 @@ modules = Bqniser.ABI.Types
         , Bqniser.ABI.Layout
         , Bqniser.ABI.Foreign
         , Bqniser.ABI.Proofs
+        , Bqniser.ABI.Semantics