From b2de295c8ca2482a9f0fcd7a35e482b52b9e1ff9 Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 1 Jun 2026 21:22:16 +0100 Subject: [PATCH] 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) --- alkahest-shell-transmuter/src/abi/Foreign.idr | 2 ++ alkahest-shell-transmuter/src/abi/Layout.idr | 2 ++ alkahest-shell-transmuter/src/abi/Types.idr | 2 ++ proofs/idris2/src/Filesystem/Composition.idr | 1 + proofs/idris2/src/Filesystem/Model.idr | 1 + proofs/idris2/src/Filesystem/Operations.idr | 1 + proofs/idris2/src/Filesystem/RMO.idr | 1 + src/abi/Foreign.idr | 1 + src/abi/Layout.idr | 1 + src/abi/Types.idr | 1 + 10 files changed, 13 insertions(+) diff --git a/alkahest-shell-transmuter/src/abi/Foreign.idr b/alkahest-shell-transmuter/src/abi/Foreign.idr index 9535898e..ffa5d539 100644 --- a/alkahest-shell-transmuter/src/abi/Foreign.idr +++ b/alkahest-shell-transmuter/src/abi/Foreign.idr @@ -1,3 +1,5 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) Jonathan D.A. Jewell ||| Foreign Function Interface Declarations ||| ||| This module declares all C-compatible functions that will be diff --git a/alkahest-shell-transmuter/src/abi/Layout.idr b/alkahest-shell-transmuter/src/abi/Layout.idr index 638be6a8..0a38f801 100644 --- a/alkahest-shell-transmuter/src/abi/Layout.idr +++ b/alkahest-shell-transmuter/src/abi/Layout.idr @@ -1,3 +1,5 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) Jonathan D.A. Jewell ||| Memory Layout Proofs ||| ||| This module provides formal proofs about memory layout, alignment, diff --git a/alkahest-shell-transmuter/src/abi/Types.idr b/alkahest-shell-transmuter/src/abi/Types.idr index 6688c2a2..067f8ef3 100644 --- a/alkahest-shell-transmuter/src/abi/Types.idr +++ b/alkahest-shell-transmuter/src/abi/Types.idr @@ -1,3 +1,5 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) Jonathan D.A. Jewell ||| ALKAHEST-SHELL-TRANSMUTER — ABI Type Definitions ||| ||| This module defines the Application Binary Interface for the Alkahest diff --git a/proofs/idris2/src/Filesystem/Composition.idr b/proofs/idris2/src/Filesystem/Composition.idr index 74a40f1e..bb3c7829 100644 --- a/proofs/idris2/src/Filesystem/Composition.idr +++ b/proofs/idris2/src/Filesystem/Composition.idr @@ -1,4 +1,5 @@ -- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) Jonathan D.A. Jewell -- Filesystem Composition - Operation Sequences and Undo/Redo -- -- Proves that sequences of reversible operations are themselves reversible. diff --git a/proofs/idris2/src/Filesystem/Model.idr b/proofs/idris2/src/Filesystem/Model.idr index a735b285..46ef8b04 100644 --- a/proofs/idris2/src/Filesystem/Model.idr +++ b/proofs/idris2/src/Filesystem/Model.idr @@ -1,4 +1,5 @@ -- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) Jonathan D.A. Jewell -- Filesystem Model - Core Types and Definitions -- -- This module defines the abstract filesystem model used throughout diff --git a/proofs/idris2/src/Filesystem/Operations.idr b/proofs/idris2/src/Filesystem/Operations.idr index e791a7e1..357576dc 100644 --- a/proofs/idris2/src/Filesystem/Operations.idr +++ b/proofs/idris2/src/Filesystem/Operations.idr @@ -1,4 +1,5 @@ -- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) Jonathan D.A. Jewell -- Filesystem Operations - mkdir, rmdir, touch, rm -- -- All operations are total (guaranteed to terminate) and proven diff --git a/proofs/idris2/src/Filesystem/RMO.idr b/proofs/idris2/src/Filesystem/RMO.idr index dbe19a0f..73651e9a 100644 --- a/proofs/idris2/src/Filesystem/RMO.idr +++ b/proofs/idris2/src/Filesystem/RMO.idr @@ -1,4 +1,5 @@ -- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) Jonathan D.A. Jewell -- RMO (Remove-Match-Obliterate) - Irreversible Operations -- -- Implements GDPR "right to be forgotten" with mathematical guarantees. diff --git a/src/abi/Foreign.idr b/src/abi/Foreign.idr index ae37cea2..7e1295d0 100644 --- a/src/abi/Foreign.idr +++ b/src/abi/Foreign.idr @@ -1,4 +1,5 @@ ||| SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) Jonathan D.A. Jewell ||| Foreign Function Interface Declarations for VALENCE_SHELL ||| ||| This module declares all C-compatible functions that will be diff --git a/src/abi/Layout.idr b/src/abi/Layout.idr index bad92a58..a46e26fc 100644 --- a/src/abi/Layout.idr +++ b/src/abi/Layout.idr @@ -1,4 +1,5 @@ -- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) Jonathan D.A. Jewell ||| Memory Layout Proofs — ABI Foundation. ||| ||| This module provides the formal proofs required to ensure that diff --git a/src/abi/Types.idr b/src/abi/Types.idr index 8e50c090..03db4fe1 100644 --- a/src/abi/Types.idr +++ b/src/abi/Types.idr @@ -1,4 +1,5 @@ -- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) Jonathan D.A. Jewell ||| VALENCE-SHELL (vsh) — ABI Type Definitions ||| ||| This module defines the Application Binary Interface for the Valence Shell.