chore(spdx): add Copyright (c) headers to Idris2 files (batch 5/7)

10 .idr files. Uses -- line comments. Files with pre-existing SPDX
get the Copyright line inserted after; files without get a 2-line
SPDX+Copyright block prepended.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

alkahest-shell-transmuter/src/abi/Foreign.idr

@@ -1,3 +1,5 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 ||| Foreign Function Interface Declarations
 |||
 ||| This module declares all C-compatible functions that will be

alkahest-shell-transmuter/src/abi/Layout.idr

@@ -1,3 +1,5 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 ||| Memory Layout Proofs
 |||
 ||| This module provides formal proofs about memory layout, alignment,

alkahest-shell-transmuter/src/abi/Types.idr

@@ -1,3 +1,5 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 ||| ALKAHEST-SHELL-TRANSMUTER — ABI Type Definitions
 |||
 ||| This module defines the Application Binary Interface for the Alkahest 

proofs/idris2/src/Filesystem/Composition.idr

@@ -1,4 +1,5 @@
 -- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -- Filesystem Composition - Operation Sequences and Undo/Redo
 --
 -- Proves that sequences of reversible operations are themselves reversible.

proofs/idris2/src/Filesystem/Model.idr

@@ -1,4 +1,5 @@
 -- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -- Filesystem Model - Core Types and Definitions
 --
 -- This module defines the abstract filesystem model used throughout

proofs/idris2/src/Filesystem/Operations.idr

@@ -1,4 +1,5 @@
 -- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -- Filesystem Operations - mkdir, rmdir, touch, rm
 --
 -- All operations are total (guaranteed to terminate) and proven

proofs/idris2/src/Filesystem/RMO.idr

@@ -1,4 +1,5 @@
 -- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -- RMO (Remove-Match-Obliterate) - Irreversible Operations
 --
 -- Implements GDPR "right to be forgotten" with mathematical guarantees.

src/abi/Foreign.idr

@@ -1,4 +1,5 @@
 ||| SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 ||| Foreign Function Interface Declarations for VALENCE_SHELL
 |||
 ||| This module declares all C-compatible functions that will be

src/abi/Layout.idr

@@ -1,4 +1,5 @@
 -- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 ||| Memory Layout Proofs — ABI Foundation.
 |||
 ||| This module provides the formal proofs required to ensure that 

src/abi/Types.idr

@@ -1,4 +1,5 @@
 -- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 ||| VALENCE-SHELL (vsh) — ABI Type Definitions
 |||
 ||| This module defines the Application Binary Interface for the Valence Shell.