diff --git a/.github/workflows/scorecard.yml b/.github/workflows/scorecard.yml index be695c7..a85faf2 100644 --- a/.github/workflows/scorecard.yml +++ b/.github/workflows/scorecard.yml @@ -1,4 +1,5 @@ -# SPDX-License-Identifier: PMPL-1.0 +# SPDX-License-Identifier: MPL-2.0 +# SPDX-License-Identifier: CC-BY-SA-4.0 name: Scorecards supply-chain security on: branch_protection_rule: diff --git a/.github/workflows/secret-scanner.yml b/.github/workflows/secret-scanner.yml index 99e513f..c0b5aa8 100644 --- a/.github/workflows/secret-scanner.yml +++ b/.github/workflows/secret-scanner.yml @@ -1,4 +1,5 @@ -# SPDX-License-Identifier: PMPL-1.0 +# SPDX-License-Identifier: MPL-2.0 +# SPDX-License-Identifier: CC-BY-SA-4.0 name: Secret Scanner on: pull_request: diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index e8e73bb..d7a07ee 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -5,9 +5,9 @@ [metadata] project = "phronesis" version = "0.9.0" -last-updated = "2026-06-20" +last-updated = "2026-06-21" status = "active" -session = "docs refresh + RSR/bot-doc compliance + root cleanup — 2026-06-20" +session = "licensing dual-header standard + closeout triage (issues #59, #60) — 2026-06-21" [project-context] name = "Phronesis" @@ -37,11 +37,13 @@ issues = [ [critical-next-actions] actions = [ + "Complete the dual-SPDX-header migration repo-wide (issue #59)", + "Wiki overhaul: audience-divided dev/maintainer/user + depth + re-frame (issue #60)", "Wire reflexion claim ingest for the compiler, formal/proof, and benchmark sources", "Advance the Rust to WASM production compiler beyond AST scaffolding", "Add Idris2 ABI definitions and the Zig FFI layer", ] [maintenance-status] -last-run-utc = "2026-06-20T00:00:00Z" +last-run-utc = "2026-06-21T00:00:00Z" last-result = "pass" # unknown | pass | warn | fail (full ExUnit suite green; consensus/Raft cases skipped pending :ra) diff --git a/.machine_readable/licensing-policy.toml b/.machine_readable/licensing-policy.toml index d2eaa6f..f34fb98 100644 --- a/.machine_readable/licensing-policy.toml +++ b/.machine_readable/licensing-policy.toml @@ -1,9 +1,9 @@ # SPDX-License-Identifier: MPL-2.0 +# SPDX-License-Identifier: CC-BY-SA-4.0 # SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) # # Machine-readable form of LICENSING.adoc. Tools enforce from this; humans read # the .adoc (the .adoc is the source of truth — keep in sync, do not diverge). -# NOT a REUSE per-file dep5 map: this encodes the RULES, not per-file claims. schema = "hyperpolymath.licensing-policy/1" repo = "hyperpolymath/phronesis" @@ -11,17 +11,12 @@ classification = "sole-owner" # estate category 1 revised = "2026-06-21" human-source = "LICENSING.adoc" upstream-canonical = "hyperpolymath/standards: LICENCE-POLICY.adoc + .claude/CLAUDE.md §License Policy" -note = "Sole-owner repo: code = MPL-2.0, prose docs = CC-BY-SA-4.0 (owner ruling 2026-06-04). Not a PMPL/AGPL/007 case. No automated/bulk SPDX edits." +note = "Dual-licensed: every source file carries BOTH MPL-2.0 and CC-BY-SA-4.0 SPDX lines. Root LICENSE is MPL-2.0 (GitHub community-health marker). No automated/bulk SPDX edits." -[default] # code/config/scripts/build/metadata/specs -spdx = "MPL-2.0" -scope = "*.ex, *.exs, *.rs, *.idr, *.tla, *.scm, mix.exs, Justfile, Mustfile, *.a2ml, *.toml" -status = "the stated, legally-operative standard for code" - -[default_docs] # prose documentation -spdx = "CC-BY-SA-4.0" -scope = "narrative *.adoc and *.md (README, EXPLAINME, AUDIT, docs/, wiki/, academic/ prose)" -status = "owner ruling 2026-06-04 — docs are CC-BY-SA-4.0; code stays MPL-2.0" +[standard] # the per-file rule +spdx = ["MPL-2.0", "CC-BY-SA-4.0"] +form = "two SPDX-License-Identifier lines per file, in the file's comment syntax" +scope = "all estate-authored source — code, config, build, workflows, formal specs/proofs, metadata, and prose docs" [github_marker] # GitHub community-health / 'git health' file = "LICENSE" @@ -31,7 +26,6 @@ note = "root LICENSE carries plain MPL-2.0 text; GitHub detects one licence — [platform_exception] # registries spdx = "MPL-2.0" applies = "Hex / crates.io and other OSI-only registries; mix.exs package licenses = [MPL-2.0]" -note = "explicit MPL-2.0 is compliance, not preference" [third_party] rule = "preserve original SPDX exactly; never relicense; flag-not-edit" @@ -45,8 +39,8 @@ pmpl_carveout = "PMPL is exactly 3 repos (palimpsest-license, palimpsest-plasma, [automation] # estate Addendum A2 allowed = false rule = "no bulk/sed/script/agent licence-SPDX changes; remediation is manual, per-file, owner-only" -exception = "an agent may author NEW files with correct SPDX from birth" +exception = "an agent may author NEW files with the correct dual header from birth" -[flagged] # known deviations — owner-only to resolve, NOT swept -apache_proofs = "academic/formal-verification/{agda/*.agda, coq/Phronesis.v, lean4/Phronesis.lean, lean4/lakefile.lean} carry Apache-2.0 (Lean/Coq/Agda ecosystem convention vs MPL-2.0 estate default — owner decision)" -pmpl_workflows = ".github/workflows/{scorecard.yml, secret-scanner.yml} carry PMPL-1.0 — drift (not a carve-out repo); owner-only flip to MPL-2.0" +[migration] # dual-header rollout +done = "academic/formal-verification/{agda/*.agda, coq/Phronesis.v, lean4/*.lean}; .github/workflows/{scorecard,secret-scanner}.yml (previously Apache-2.0-OR-MIT and PMPL-1.0)" +pending = "remaining single-SPDX estate files migrate to the dual header incrementally; mixed single/dual is owner-sanctioned during transition" diff --git a/LICENSING.adoc b/LICENSING.adoc index 213a9ad..2e91010 100644 --- a/LICENSING.adoc +++ b/LICENSING.adoc @@ -1,3 +1,4 @@ +// SPDX-License-Identifier: MPL-2.0 // SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell = Phronesis — Licensing @@ -5,92 +6,69 @@ :icons: font The standard, authoritative statement of how Phronesis is licensed. Phronesis is -a sole-owner hyperpolymath repository, so it follows the estate default: a -*dual* licence — code under MPL-2.0, prose documentation under CC-BY-SA-4.0. +a sole-owner hyperpolymath repository, dual-licensed: every source file is +offered under *both* MPL-2.0 and CC-BY-SA-4.0. This document is the human source of truth; `.machine_readable/licensing-policy.toml` -is its machine-readable twin (tools enforce from the TOML, humans read this — -keep them in sync). The canonical estate policy is -https://github.com/hyperpolymath/standards[`standards`] `LICENCE-POLICY.adoc` -and `.claude/CLAUDE.md` §License Policy; this file is the Phronesis-local -instance of it. +is its machine-readable twin (keep them in sync). The canonical estate policy is +https://github.com/hyperpolymath/standards[`standards`] `LICENCE-POLICY.adoc`. -== The standard (dual labelling) +== The standard — dual SPDX header on every file -Two SPDX identifiers are in normal use across the repository — one per file, -by file class: +Every source file carries *two* SPDX identifier lines, in the file's comment +syntax: [source] ---- -# Code, configuration, scripts, build files, A2ML metadata, formal specs: SPDX-License-Identifier: MPL-2.0 - -# Prose documentation (*.adoc, narrative *.md): SPDX-License-Identifier: CC-BY-SA-4.0 ---- MPL-2.0 (file-level copyleft) keeps the implementation free and open even in -networked deployments; CC-BY-SA-4.0 opens the documentation and research content -under attribution and share-alike. Both licence texts live in `LICENSES/` +networked deployments; CC-BY-SA-4.0 opens the same content for documentation and +research reuse under attribution and share-alike. Both texts live in `LICENSES/` (`MPL-2.0.txt`, `CC-BY-SA-4.0.txt`), REUSE-style. -== GitHub marker - -The root `LICENSE` file carries the plain *MPL-2.0* text. That is deliberate: -it is the single licence GitHub detects for the repository's community-health -profile ("git health") and the licence shown in the sidebar and API. CC-BY-SA-4.0 -is declared per-file and in `LICENSES/`, not in the root `LICENSE` (GitHub -detects one). The distributed Hex package (`mix.exs`) also declares -`licenses: ["MPL-2.0"]` — the code artefact. - -== Mapping +This applies to all estate-authored source — `*.ex`, `*.exs`, `*.rs`, `*.idr`, +`*.tla`, `*.agda`, `*.v`, `*.lean`, `*.scm`, `*.a2ml`, `*.toml`, build files, +workflows, and prose docs (`*.adoc`, narrative `*.md`) alike. -[cols="2,1,3"] -|=== -| File class | SPDX | Examples +== GitHub marker (community health) -| Source code | `MPL-2.0` | `*.ex`, `*.exs`, `*.rs`, `*.idr` -| Formal specs / semantics | `MPL-2.0` | `*.tla`, `spec/SPEC.core.scm` -| Build / config / metadata | `MPL-2.0` | `mix.exs`, `Justfile`, `Mustfile`, `*.a2ml`, `*.toml` -| Prose documentation | `CC-BY-SA-4.0` | `README.adoc`, `EXPLAINME.adoc`, `AUDIT.adoc`, `docs/**`, `wiki/**`, `academic/**` prose -| Root licence text | `MPL-2.0` | `LICENSE` (GitHub marker) -|=== +The root `LICENSE` file carries the plain *MPL-2.0* text. That is the single +licence GitHub detects for the repository's community-health profile ("git +health") and shows in the sidebar and API. The dual per-file labelling above is +declared in headers and in `LICENSES/`; the root `LICENSE` stays MPL-2.0 so the +community-health marker is MPL-2.0. The distributed Hex package (`mix.exs`) also +declares `licenses: ["MPL-2.0"]`. == Exclusion cases -The dual standard above is the *normal*. It does not apply in these cases: - -* *Third-party / vendored* (`deps/**`, any upstream code): preserve the - original SPDX exactly — flag, never edit or relicense. -* *Platform registries* (Hex, crates.io): an explicit `MPL-2.0` declaration is - a compliance requirement, not a preference. -* *Not applicable to Phronesis:* the estate's other categories — All-Rights-Reserved - (`007`), `AGPL-3.0-or-later` (repos shared with the owner's son), and - `PMPL-1.0-or-later` (the three Palimpsest carve-out repos only) — do **not** - apply here. Phronesis is a plain sole-owner repo. - -== Known deviations (flagged, owner-only to resolve) - -Per estate policy, licence-SPDX changes are *manual, per-file, owner-only* — no -bulk or automated edits (see `standards` `LICENCE-POLICY.adoc` Addendum A2 and -the neurophone#99 post-mortem). The following currently deviate from the -standard and are recorded here for an owner decision rather than swept: - -[cols="2,1,3"] -|=== -| Files | Current SPDX | Note - -| `academic/formal-verification/{agda/*.agda, coq/Phronesis.v, lean4/Phronesis.lean, lean4/lakefile.lean}` (5) -| `Apache-2.0` -| Estate-authored proof files. Apache-2.0 is the convention of the Lean/Coq/Agda - proof ecosystems; confirm whether to keep (ecosystem convention) or normalise - to `MPL-2.0` (estate default for code). - -| `.github/workflows/{scorecard.yml, secret-scanner.yml}` (2) -| `PMPL-1.0` -| Drift — Phronesis is not a Palimpsest carve-out repo, so these workflow files - should be `MPL-2.0`. PMPL flips are owner-only; not auto-changed. -|=== +The dual standard is the *normal*. It does not apply to: + +* *Third-party / vendored* (`deps/**`, any upstream code): preserve the original + SPDX exactly — flag, never edit or relicense. +* *The root `LICENSE` file*: the verbatim MPL-2.0 text (the GitHub marker), not a + dual-headed source file. +* *Not applicable to Phronesis:* the estate's other categories — ARR (`007`), + `AGPL-3.0-or-later` (son-shared repos), `PMPL-1.0-or-later` (the three + Palimpsest carve-out repos only) — do not apply here. + +== Migration status + +The dual-header standard is being rolled out per-file (manual, owner-directed — +no bulk/automated SPDX sweeps, per `standards` `LICENCE-POLICY.adoc` Addendum A2 +and the neurophone#99 post-mortem). + +* *Done:* the formal-verification proof files + (`academic/formal-verification/{agda/*.agda, coq/Phronesis.v, lean4/*.lean}`) + and the two affected workflows + (`.github/workflows/{scorecard.yml, secret-scanner.yml}`) now carry the dual + header (previously `Apache-2.0 OR MIT` and `PMPL-1.0` respectively). +* *Pending:* the remaining estate-authored files that still carry a single SPDX + line are migrated to the dual header incrementally. Until then the repository + legitimately mixes single- and dual-headed files; both are owner-sanctioned + during the transition. == See also diff --git a/academic/formal-verification/agda/Phronesis.agda b/academic/formal-verification/agda/Phronesis.agda index c69a91e..f0d04d6 100644 --- a/academic/formal-verification/agda/Phronesis.agda +++ b/academic/formal-verification/agda/Phronesis.agda @@ -1,4 +1,5 @@ --- SPDX-License-Identifier: Apache-2.0 OR MIT +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-License-Identifier: CC-BY-SA-4.0 -- Phronesis Formalization in Agda -- Intrinsically typed representation with dependent types diff --git a/academic/formal-verification/agda/PhronesisEcho.agda b/academic/formal-verification/agda/PhronesisEcho.agda index bead3a2..512f391 100644 --- a/academic/formal-verification/agda/PhronesisEcho.agda +++ b/academic/formal-verification/agda/PhronesisEcho.agda @@ -1,4 +1,5 @@ --- SPDX-License-Identifier: Apache-2.0 OR MIT +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-License-Identifier: CC-BY-SA-4.0 -- Copyright (c) 2026 Jonathan D.A. Jewell -- -- ===================================================================== diff --git a/academic/formal-verification/coq/Phronesis.v b/academic/formal-verification/coq/Phronesis.v index 50c5229..4637aa3 100644 --- a/academic/formal-verification/coq/Phronesis.v +++ b/academic/formal-verification/coq/Phronesis.v @@ -1,4 +1,5 @@ -(* SPDX-License-Identifier: Apache-2.0 OR MIT *) +(* SPDX-License-Identifier: MPL-2.0 *) +(* SPDX-License-Identifier: CC-BY-SA-4.0 *) (* Phronesis Formalization in Coq *) (* Complete mechanized proofs of type safety, termination, and security properties *) diff --git a/academic/formal-verification/lean4/Phronesis.lean b/academic/formal-verification/lean4/Phronesis.lean index 31b32ce..3835b5e 100644 --- a/academic/formal-verification/lean4/Phronesis.lean +++ b/academic/formal-verification/lean4/Phronesis.lean @@ -1,4 +1,5 @@ --- SPDX-License-Identifier: Apache-2.0 OR MIT +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-License-Identifier: CC-BY-SA-4.0 -- Phronesis Formalization in Lean 4 -- Mechanized proofs of type safety, termination, and security properties. -- diff --git a/academic/formal-verification/lean4/lakefile.lean b/academic/formal-verification/lean4/lakefile.lean index 2203966..670b686 100644 --- a/academic/formal-verification/lean4/lakefile.lean +++ b/academic/formal-verification/lean4/lakefile.lean @@ -1,4 +1,5 @@ --- SPDX-License-Identifier: Apache-2.0 OR MIT +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-License-Identifier: CC-BY-SA-4.0 -- Minimal Lake build for the Phronesis Lean 4 metatheory. -- No external dependencies (no Mathlib): builds on core Lean only, so CI -- needs nothing but the toolchain pinned in `lean-toolchain`.