chore(licence): apply + enforce MPL-2.0 / CC-BY-SA-4.0 SPDX invariant

claude · claude · commit af5fa44ef334 · 2026-06-20T05:14:30.000Z
Owner-directed (satisfies LICENCE-POLICY.adoc A2's "manual, per-file, by the owner" gate). Makes the licence split a formal, enforced invariant. - Applied SPDX headers per file: MPL-2.0 to all code/config/scripts/state (25 src+tests .rs, Cargo.toml, .gitignore); CC-BY-SA-4.0 to prose. Fixed prose drift: CHANGELOG/CONTRIBUTING/SECURITY MPL-2.0 -> CC-BY-SA-4.0, and docs/*.adoc CC-BY-4.0 -> CC-BY-SA-4.0 (the check caught the missing -SA). - New scripts/check-spdx.sh enforces the invariant; wired into `just check` (new `license-check` recipe) and .github/workflows/rust-ci.yml. - New .machine_readable/licensing-policy.toml declares the rule + the excluded set machine-readably. Third-party protection: nothing not ours is relicensed. Cargo.lock (generated, enumerates third-party deps), LICENSE (the MPL text itself), and tests/fixtures/ (Agda test-input data) are excluded. There is no vendored third-party source in-tree; if any is added, the checker FAILS until it is listed as excluded with its original SPDX preserved — that failure is the guard against silent relicensing. `bash scripts/check-spdx.sh` OK; fmt/clippy/test green. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019GiSiEfgZCte35dyykgBHs
diff --git a/.github/workflows/rust-ci.yml b/.github/workflows/rust-ci.yml
@@ -49,6 +49,9 @@ jobs:
           cargo --version
           rustup component add clippy rustfmt
 
+      - name: SPDX licence invariant
+        run: bash scripts/check-spdx.sh
+
       - name: cargo fmt --check
         run: cargo fmt --all -- --check
 
diff --git a/.gitignore b/.gitignore
@@ -1,3 +1,6 @@
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
 # Rust build artefacts
 target/
 
diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml
@@ -34,15 +34,13 @@ milestones = [
 ]
 
 [blockers-and-issues]
-# No active blockers. v0.1 lint set + DAG schema (arghda-spec.adoc) are complete.
-# Known compliance gap (owner-manual only, per LICENCE-POLICY A2 — never an
-# agent sweep): src/*.rs lack per-file `// SPDX-License-Identifier: MPL-2.0`
-# headers. The repo is declared MPL-2.0 (Cargo.toml, LICENSE); applying the
-# per-file headers is owner-driven manual work.
+# No active blockers. v0.1 lint set + DAG schema (arghda-spec.adoc) are
+# complete. The SPDX licence invariant is applied and enforced
+# (scripts/check-spdx.sh; .machine_readable/licensing-policy.toml).
 
 [critical-next-actions]
 actions = [
-  "Owner-manual: apply MPL-2.0 SPDX headers to src/*.rs (no agent bulk sweep — LICENCE-POLICY A2)",
+  "Formalise template-applicability rules (capability-gated RSR profile: carry a template module iff the repo declares the capability it serves) — estate-wide, candidate for hyperpolymath/standards",
   "Extend content-hash invalidation to cover transitive imports (needs include-root tracking)",
   "Serve /.well-known/groove for PanLL discovery (Groove protocol)",
   "Scaffold arghda-studio (AffineScript visual layer consuming the dag JSON)",
diff --git a/.machine_readable/licensing-policy.toml b/.machine_readable/licensing-policy.toml
@@ -0,0 +1,36 @@
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# Licence invariant for arghda-core — machine-readable declaration of the rule
+# enforced by scripts/check-spdx.sh (run in `just check` + Rust CI). The split
+# itself comes from hyperpolymath/standards LICENCE-POLICY.adoc Rule 1.
+
+[invariant]
+enforced = true
+checker = "scripts/check-spdx.sh"
+wired-into = ["Justfile (just check / just license-check)", ".github/workflows/rust-ci.yml"]
+
+[licences]
+# By content type, not by directory.
+code = "MPL-2.0"        # *.rs, *.toml, *.a2ml, *.yml, *.sh, Justfile, .gitignore, .well-known/*
+prose = "CC-BY-SA-4.0"  # *.adoc, *.md narrative
+# Canonical texts: MPL-2.0 -> ./LICENSE ; CC-BY-SA-4.0 -> standards/LICENSES/CC-BY-SA-4.0.txt
+
+[excluded]
+# NOT ours, generated, or test-input data. These never carry the repo's
+# licence choices; the checker skips them.
+paths = [
+  "Cargo.lock",      # generated by cargo; enumerates third-party dependencies
+  "LICENSE",         # the MPL-2.0 licence text itself
+  "target/",         # cargo build output (gitignored)
+  "tests/fixtures/", # Agda test-input data (some deliberately malformed)
+]
+
+[third-party]
+# arghda-core vendors NO third-party source in-tree: every dependency is
+# fetched by cargo (declared in Cargo.toml, pinned in Cargo.lock) and is never
+# relicensed. If third-party source is ever vendored in-tree, add its path to
+# [excluded] above and preserve its ORIGINAL SPDX header verbatim. The checker
+# fails on any unrecognised in-tree file until it is excluded — that failure is
+# the intended guard against silently relicensing others' code.
+vendored-in-tree = []
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -1,4 +1,4 @@
-<!-- SPDX-License-Identifier: MPL-2.0 -->
+<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->
 # Changelog
 
 All notable changes to arghda-core are documented here. The format follows
@@ -16,8 +16,15 @@ All notable changes to arghda-core are documented here. The format follows
   docs carry `CC-BY-SA-4.0`; code/config/state stay `MPL-2.0` (per the estate
   licence policy). Refreshed `.machine_readable/6a2/STATE.a2ml` + `META.a2ml`
   and the `0-AI-MANIFEST.a2ml` read-order; removed local `dist-newstyle/`
-  build cruft. (Per-file SPDX headers on `src/*.rs` remain owner-manual by
-  policy — never an agent bulk sweep.)
+  build cruft.
+- Formal SPDX licence invariant (owner-directed): every tracked file carries
+  the correct header — `MPL-2.0` for code/config/scripts/state, `CC-BY-SA-4.0`
+  for prose — applied per file (incl. all `src/*.rs`) and enforced by
+  `scripts/check-spdx.sh`, wired into `just check` and Rust CI. Third-party,
+  generated (`Cargo.lock`), and test-data (`tests/fixtures/`) files are
+  explicitly excluded and never relicensed; `docs/*.adoc` normalised from
+  `CC-BY-4.0` to `CC-BY-SA-4.0`. Declared in
+  `.machine_readable/licensing-policy.toml`.
 
 ### Added
 
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
@@ -1,4 +1,4 @@
-<!-- SPDX-License-Identifier: MPL-2.0 -->
+<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->
 # Contributing to arghda-core
 
 arghda-core is the Rust engine for the arghda proof-workspace tool.
diff --git a/Cargo.toml b/Cargo.toml
@@ -1,3 +1,6 @@
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
 [package]
 name = "arghda-core"
 version = "0.1.0"
diff --git a/Justfile b/Justfile
@@ -32,8 +32,13 @@ fmt-check:
 lint:
     cargo clippy --all-targets -- -D warnings
 
+# SPDX licence invariant: MPL-2.0 for code/config/scripts, CC-BY-SA-4.0 for
+# prose; third-party / generated / test data excluded (CI gate).
+license-check:
+    bash scripts/check-spdx.sh
+
 # The full CI gate, exactly what .github/workflows/rust-ci.yml runs.
-check: fmt-check lint build test
+check: fmt-check lint license-check build test
 
 # Alias for CI.
 ci: check
diff --git a/README.adoc b/README.adoc
@@ -137,5 +137,10 @@ link:EXPLAINME.adoc[`EXPLAINME.adoc`] as the orientation pointer.
 
 Code, configuration and scripts are `MPL-2.0` (see link:LICENSE[LICENSE]);
 prose documentation is `CC-BY-SA-4.0`, per the
-https://github.com/hyperpolymath/standards[hyperpolymath licence policy].
-SPDX headers are owner-managed and applied manually per file.
+https://github.com/hyperpolymath/standards[hyperpolymath licence policy] (Rule
+1). This split is a **formal invariant**: every tracked file carries the
+appropriate SPDX header, checked by `scripts/check-spdx.sh` in `just check` and
+in CI. Third-party, generated, and test-data files are explicitly excluded
+(link:.machine_readable/licensing-policy.toml[`licensing-policy.toml`]) and are
+never relicensed — vendoring third-party source in-tree fails the check until
+it is listed as excluded with its original SPDX preserved.
diff --git a/SECURITY.md b/SECURITY.md
@@ -1,4 +1,4 @@
-<!-- SPDX-License-Identifier: MPL-2.0 -->
+<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->
 # Security Policy
 
 ## Supported versions
diff --git a/docs/arghda-spec.adoc b/docs/arghda-spec.adoc
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: CC-BY-4.0
+// SPDX-License-Identifier: CC-BY-SA-4.0
 // SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 = ArghDA MVP Specification
 :toc: macro
diff --git a/docs/arghda-vision.adoc b/docs/arghda-vision.adoc
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: CC-BY-4.0
+// SPDX-License-Identifier: CC-BY-SA-4.0
 // SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 = ArghDA — Vision, Architecture & Roadmap
 :toc: macro
diff --git a/scripts/check-spdx.sh b/scripts/check-spdx.sh
@@ -0,0 +1,58 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+#
+# Licence invariant for arghda-core (enforced by `just check` + Rust CI).
+#
+#   code / config / scripts / state   ->  SPDX-License-Identifier: MPL-2.0
+#   prose documentation (*.adoc, *.md) ->  SPDX-License-Identifier: CC-BY-SA-4.0
+#
+# Files that are NOT ours, generated, or test-input data are EXCLUDED and must
+# never carry the repo's licence choices. The machine-readable declaration of
+# this rule is .machine_readable/licensing-policy.toml; the split itself comes
+# from hyperpolymath/standards LICENCE-POLICY.adoc Rule 1.
+#
+# Guard for third-party code: any tracked, non-excluded file that lacks our
+# header FAILS the check. Vendoring third-party source therefore forces a
+# conscious exclusion (and the file keeps its original SPDX) rather than being
+# silently relicensed.
+set -euo pipefail
+cd "$(git rev-parse --show-toplevel)"
+
+MPL='SPDX-License-Identifier: MPL-2.0'
+CC='SPDX-License-Identifier: CC-BY-SA-4.0'
+fail=0
+
+# Not ours / generated / test-input data — see [excluded] in the policy file.
+excluded() {
+  case "$1" in
+    Cargo.lock | LICENSE) return 0 ;;          # generated lockfile / the licence text itself
+    target/* | tests/fixtures/*) return 0 ;;   # build output / Agda test-input data
+    *) return 1 ;;
+  esac
+}
+
+while IFS= read -r f; do
+  excluded "$f" && continue
+  case "$f" in
+    *.adoc | *.md) want="$CC"; label="CC-BY-SA-4.0 (prose)" ;;
+    *) want="$MPL"; label="MPL-2.0 (code/config/script/state)" ;;
+  esac
+  if ! grep -qF "$want" "$f"; then
+    echo "  MISSING $label: $f"
+    fail=1
+  fi
+done < <(git ls-files)
+
+if [ "$fail" -ne 0 ]; then
+  cat >&2 <<'MSG'
+SPDX licence invariant: FAIL (see above).
+Fix one of:
+  * add the correct SPDX header to the file, OR
+  * if the file is third-party / generated / test data, add it to the
+    excluded set in scripts/check-spdx.sh AND
+    .machine_readable/licensing-policy.toml — never relicense others' code.
+MSG
+  exit 1
+fi
+echo "SPDX licence invariant: OK"
diff --git a/src/agda.rs b/src/agda.rs
@@ -1,3 +1,6 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
 //! Shelling out to `agda` to typecheck a file.
 //!
 //! ArghDA never proves anything itself — it asks Agda. This module runs
diff --git a/src/config.rs b/src/config.rs
@@ -1,3 +1,6 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
 //! Operator configuration from `.arghda/config.toml`.
 //!
 //! The spec makes the `unpinned-headline` pattern operator-overridable
diff --git a/src/dag.rs b/src/dag.rs
@@ -1,3 +1,6 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
 //! The DAG document — the JSON contract a visual layer consumes.
 //!
 //! Builds on the import graph (`crate::graph`) plus a lint pass over every
diff --git a/src/diagnostic.rs b/src/diagnostic.rs
@@ -1,3 +1,6 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
 use serde::{Deserialize, Serialize};
 use std::path::PathBuf;
 
diff --git a/src/event.rs b/src/event.rs
@@ -1,3 +1,6 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
 //! The triage event stream.
 //!
 //! Every state transition appends one JSON object (one line) to
diff --git a/src/graph.rs b/src/graph.rs
@@ -1,3 +1,6 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
 //! First-class Agda import graph.
 //!
 //! The reachability primitives (`module_name_of`, `module_to_path`,
diff --git a/src/hash.rs b/src/hash.rs
@@ -1,3 +1,6 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
 //! Dependency-free SHA-256 (FIPS 180-4).
 //!
 //! Used for `proven`-state content hashing — detecting when a file changes
diff --git a/src/lib.rs b/src/lib.rs
@@ -1,3 +1,6 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
 //! arghda-core: proof-workspace manager for Agda.
 //!
 //! Public surface is intentionally small: `Workspace`, the lint traits,
diff --git a/src/lint/escape_hatch.rs b/src/lint/escape_hatch.rs
@@ -1,3 +1,6 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
 //! `escape-hatch` (warn) — surface soundness escape hatches.
 //!
 //! Flags termination-checker overrides (`{-# TERMINATING #-}`,
diff --git a/src/lint/mod.rs b/src/lint/mod.rs
@@ -1,3 +1,6 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
 use crate::diagnostic::LintReport;
 use anyhow::Result;
 use std::path::{Path, PathBuf};
diff --git a/src/lint/orphan_module.rs b/src/lint/orphan_module.rs
@@ -1,3 +1,6 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
 use super::{LintContext, LintRule};
 use crate::diagnostic::{Diagnostic, LintReport, Severity};
 use crate::graph::{module_name_of, reachable_from_roots};
diff --git a/src/lint/postulate.rs b/src/lint/postulate.rs
@@ -1,3 +1,6 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
 //! `unjustified-postulate` — flag `postulate` openers that lack an
 //! adjacent `-- JUSTIFY:` rationale.
 //!
diff --git a/src/lint/safe_pragma.rs b/src/lint/safe_pragma.rs
@@ -1,3 +1,6 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
 use super::{LintContext, LintRule};
 use crate::diagnostic::{Diagnostic, LintReport, Severity};
 use anyhow::{Context, Result};
diff --git a/src/lint/tab_mix.rs b/src/lint/tab_mix.rs
@@ -1,3 +1,6 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
 //! `tab-mix` (warn) — flag tabs used for indentation.
 //!
 //! Agda's layout rule and the estate style use spaces; a stray tab in
diff --git a/src/lint/unpinned_headline.rs b/src/lint/unpinned_headline.rs
@@ -1,3 +1,6 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
 //! `unpinned-headline` (warn) — a module declares a top-level theorem whose
 //! name matches the headline pattern, but the name is not pinned in any
 //! `Smoke.agda` via a `using ( … )` clause.
diff --git a/src/main.rs b/src/main.rs
@@ -1,3 +1,6 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
 use anyhow::{Context, Result};
 use arghda_core::lint::LintContext;
 use arghda_core::{
diff --git a/src/proven.rs b/src/proven.rs
@@ -1,3 +1,6 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
 //! The `proven`-state content-hash manifest (`.arghda/hashes.json`).
 //!
 //! When a file is promoted to `proven`, its content hash is recorded here.
diff --git a/src/timestamp.rs b/src/timestamp.rs
@@ -1,3 +1,6 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
 //! Dependency-free UTC timestamps.
 //!
 //! Emits RFC 3339 / ISO-8601 strings (e.g. `2026-06-18T11:45:32Z`) without
diff --git a/src/unused.rs b/src/unused.rs
@@ -1,3 +1,6 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
 //! Shelling out to `agda-unused` to find unused code (the `unused-import` rule).
 //!
 //! Like [`crate::agda`], ArghDA does not analyse for unused code itself — it
diff --git a/src/watcher.rs b/src/watcher.rs
@@ -1,3 +1,6 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
 use anyhow::Result;
 use notify::{RecommendedWatcher, RecursiveMode, Watcher};
 use std::path::Path;
diff --git a/src/workspace.rs b/src/workspace.rs
@@ -1,3 +1,6 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
 use crate::event::{self, Event, EventKind};
 use crate::proven::{self, ProvenRecord};
 use anyhow::{Context, Result};
diff --git a/tests/dag.rs b/tests/dag.rs
@@ -1,3 +1,6 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
 //! `dag` document construction over the fixtures.
 
 use arghda_core::lint::unpinned_headline::DEFAULT_HEADLINE_PATTERN;
diff --git a/tests/proven.rs b/tests/proven.rs
@@ -1,3 +1,6 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
 //! Proven-state content hashing and staleness detection.
 
 use arghda_core::{proven, State, Workspace};
diff --git a/tests/smoke.rs b/tests/smoke.rs
@@ -1,3 +1,6 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
 //! End-to-end smoke tests for the v0.1 lint pack.
 //!
 //! Each test runs the default rule pack against a self-contained
diff --git a/tests/transitions.rs b/tests/transitions.rs
@@ -1,3 +1,6 @@
+// SPDX-License-Identifier: MPL-2.0
+// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
+
 //! Workspace state-machine transitions and the event log.
 
 use arghda_core::{event, EventKind, State, Workspace};

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-<!-- SPDX-License-Identifier: MPL-2.0 -->`
	`1`	`+<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->`
`2`	`2`	`# Contributing to arghda-core`
`3`	`3`
`4`	`4`	`arghda-core is the Rust engine for the arghda proof-workspace tool.`