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.