Pillar E primer + related work + estate PMPL→MPL-2.0 sweep (harden integration) (#73)

hyperpolymath · claude · web-flow · commit 888dee09419f · 2026-05-20T15:28:26.000+01:00
## Summary Brings the `harden/ci-flake-pin-2026-05-18` stack onto main, with three logical groupings: * **Harden foundation (P0/P1)** — closure-hole closure, external fibre triangulation against stdlib, reproducible CI-via-flake exact pin (additive verifier). These are the earlier commits on the branch; structural work, no Agda regressions. * **Pillar E expansion (commit `8a24530`)** — clears two `[EXPAND]` tags on `docs/echo-types/paper.adoc`: - **Background and notation** primer: 6 subsections (type-theoretic setting, Σ-types + identity, HoTT fibres, coeffect/graded-modality lineage, thin-poset reindexing modalities, notation summary) plus an 18-row notation table whose every symbol is sourced from a real Agda module. Explicit on the post-retraction framing. - **Related work**: 8 per-neighbour subsections (HoTT fibres, graded comonad/coeffect/QTT, lenses/optics, refinement types, setoid quotients, provenance semirings, IFC/modal type theories, synthesis). All `<<reframing-note>>` xrefs resolve. - `types-abstract.adoc`: per-neighbour related-work positioning block mirroring the paper. Abstract status remains "NOT submission-ready, pending re-review" — content alignment only. * **Licence sweep (commit `2e78761`)** — collapses the `PMPL-1.0-or-later` SPDX identifier to `MPL-2.0` per owner direction 2026-05-20. 29 source/config files swept; README badge updated; `stapeln.toml` + `arghda-core/Cargo.toml` license fields; new `docs/PMPL-NARRATIVE.adoc` records the cultural/discipline overlay PMPL represented (no legal effect change — MPL-2.0 was already the lawyer-confirmed operative legal effect). ## Reconciliation needed before merge `origin/main` has advanced by 7 PRs (#64–#70) since this branch's last merge from main: * #64–#66 bridge work (CNO Agda↔Coq↔Lean4 correspondence, EchoTropical correspondence appendix, EchoJanusBridge OpKind mirror — substantive `EchoJanusBridge.agda` +221 / `EchoApprox.agda` +132) * #67 docs: rule out 2-categorical shape + roadmap credits * #68 theory: Axis 8 graded access modality (new `EchoAccess.agda`, 262 lines) * #69 theory: AntiEcho thin slice (new `AntiEcho.agda`, 93 lines) * #70 theory: EchoApprox composition rung first slice **Expected conflicts** (deliberate, owner-resolved): * `paper.adoc` — this PR adds Background primer + Related work; parallel sessions may have edited adjacent sections * `types-abstract.adoc` — this PR adds a related-work block * `flake.nix` — this PR is the full harden-P1 flake; parallel sessions retained the simpler devShell flake * `.github/workflows/*.yml`, `.machine_readable/6a2/*.a2ml`, `contractiles/*.a2ml`, `stapeln.toml`, `README.md`, `arghda-core/Cargo.toml`, `Containerfile`, `EXPLAINME.adoc`, `QUICKSTART-*.adoc`, `TOPOLOGY.adoc`, `docs/echidna-design-search-2026-04-28.adoc`, `docs/echo-types/MAP.adoc`, `docs/echo-types/echo-kernel-note.adoc`, `scripts/kernel-guard.sh`, `tools/check-guardrails.sh` — licence sweep; conflicts with parallel sessions that kept PMPL headers (resolve by taking this PR's MPL-2.0) ## Test plan - [ ] CI green: governance + Agda + Hypatia scans + Scorecard - [ ] `flake.nix` `nix flake check` passes (additive verifier) - [ ] `agda proofs/agda/All.agda` and `agda proofs/agda/Smoke.agda` both exit 0 under `--safe --without-K`, zero postulates (no Agda was touched by this branch's recent commits, so this should be a verification-only step) - [ ] AsciiDoc render of `paper.adoc` — confirm all `<<reframing-note>>` xrefs resolve - [ ] `docs/PMPL-NARRATIVE.adoc` reads coherently - [ ] No remaining `PMPL`/`Palimpsest` strings outside `docs/PMPL-NARRATIVE.adoc` + the one intentional pointer in `ECOSYSTEM.a2ml` 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
diff --git a/.editorconfig b/.editorconfig
@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 root = true
 
 [*]
diff --git a/.envrc b/.envrc
@@ -1,2 +1,2 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 use flake
diff --git a/.github/workflows/agda.yml b/.github/workflows/agda.yml
@@ -1,5 +1,4 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
-# (MPL-2.0 is automatic legal fallback until PMPL is formally recognised)
+# SPDX-License-Identifier: MPL-2.0
 
 name: Agda
 
@@ -199,3 +198,28 @@ jobs:
           agda --ignore-interfaces -i proofs/agda proofs/agda/Smoke.agda
           agda --ignore-interfaces -i proofs/agda proofs/agda/characteristic/All.agda
           agda --ignore-interfaces -i proofs/agda proofs/agda/examples/All.agda
+
+  flake-check:
+    # Foundation P1: the reproducible, exactly-pinned toolchain.
+    # `nix flake check` runs flake.nix's hermetic `checks.suite`
+    # (flake-pinned Agda + PINNED stdlib v2.3 + PINNED absolute-zero
+    # @3ff5cee, guardrail + 4 roots + N5 xfail). ADDITIVE: the apt
+    # `check` and `cold-check` jobs remain the gate, so a version
+    # delta surfaced here (e.g. 2.7.0.1 vs verified 2.8.0) is
+    # informative, not a regression. Its first green run IS the P1
+    # verification (the dev env has no nix; CI is the verifier).
+    # Flip continue-on-error to false once it is first green.
+    runs-on: ubuntu-latest
+    continue-on-error: true
+    steps:
+      - name: Checkout
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd  # v6.0.2
+
+      - name: Install Nix (pinned action)
+        uses: cachix/install-nix-action@08dcb3a5e62fa31e2da3d490afc4176ef55ecd72  # v30
+        with:
+          extra_nix_config: |
+            experimental-features = nix-command flakes
+
+      - name: nix flake check (hermetic, reproducible)
+        run: nix flake check --print-build-logs
diff --git a/.github/workflows/governance.yml b/.github/workflows/governance.yml
@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # governance.yml — single wrapper calling the shared estate governance bundle
 # in hyperpolymath/standards instead of carrying per-repo copies.
 #
diff --git a/.github/workflows/hypatia-scan.yml b/.github/workflows/hypatia-scan.yml
@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # Hypatia Neurosymbolic CI/CD Security Scan
 name: Hypatia Security Scan
 
diff --git a/.github/workflows/mirror.yml b/.github/workflows/mirror.yml
@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell
 name: Mirror to Git Forges
 
diff --git a/.github/workflows/scorecard.yml b/.github/workflows/scorecard.yml
@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 name: OSSF Scorecard
 on:
   push:
diff --git a/.machine_readable/6a2/AGENTIC.a2ml b/.machine_readable/6a2/AGENTIC.a2ml
@@ -14,7 +14,7 @@
 ;;; closed questions, redo superseded work, or violate forbidden
 ;;; rebrandings.
 ;;;
-;;; SPDX-License-Identifier: PMPL-1.0-or-later
+;;; SPDX-License-Identifier: MPL-2.0
 ;;; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
 
 (define-module (echo-types agentic)
diff --git a/.machine_readable/6a2/ECOSYSTEM.a2ml b/.machine_readable/6a2/ECOSYSTEM.a2ml
@@ -13,7 +13,7 @@
 ;;; session understands echo-types' position in the constellation
 ;;; without re-deriving it.
 ;;;
-;;; SPDX-License-Identifier: PMPL-1.0-or-later
+;;; SPDX-License-Identifier: MPL-2.0
 ;;; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
 
 (define-module (echo-types ecosystem)
@@ -101,10 +101,11 @@
      (source . "Standing decision sd-003 in STATE.scm")
      (artefacts . (".github/workflows/mirror.yml" "MIRROR_SETUP.adoc")))
 
-    ((convention . "License: PMPL-1.0-or-later for code and docs")
-     (source . "META.scm SPDX header pattern; constellation default")
-     (artefacts . ("LICENSE-PMPL-1.0.txt" ; if present
-                   "SPDX headers in all .scm files")))
+    ((convention . "License: MPL-2.0 for code (PMPL retained as narrative/cultural overlay only; see docs/PMPL-NARRATIVE.adoc — owner direction 2026-05-20)")
+     (source . "META.scm SPDX header pattern; owner direction 2026-05-20 supersedes PMPL-1.0-or-later policy")
+     (artefacts . ("LICENSE" ; MPL-2.0
+                   "docs/PMPL-NARRATIVE.adoc" ; cultural overlay
+                   "SPDX headers in all .a2ml files")))
 
     ((convention . "Cross-platform builds: Linux primary, Windows secondary")
      (source . "Standing decision sd-004 in STATE.scm")
diff --git a/.machine_readable/6a2/META.a2ml b/.machine_readable/6a2/META.a2ml
@@ -6,7 +6,7 @@
 ;;; Schema reference:
 ;;;   github.com/hyperpolymath/standards/blob/main/meta-a2ml/spec/abnf/meta.abnf
 ;;;
-;;; SPDX-License-Identifier: PMPL-1.0-or-later
+;;; SPDX-License-Identifier: MPL-2.0
 ;;; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
 
 (define-module (echo-types meta)
diff --git a/.machine_readable/6a2/NEUROSYM.a2ml b/.machine_readable/6a2/NEUROSYM.a2ml
@@ -13,7 +13,7 @@
 ;;; it implies, and what was deliberately NOT proved (PATH B
 ;;; obligations).
 ;;;
-;;; SPDX-License-Identifier: PMPL-1.0-or-later
+;;; SPDX-License-Identifier: MPL-2.0
 ;;; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
 
 (define-module (echo-types neurosym)
diff --git a/.machine_readable/6a2/PLAYBOOK.a2ml b/.machine_readable/6a2/PLAYBOOK.a2ml
@@ -14,7 +14,7 @@
 ;;; (architectural decisions) and gated by AGENTIC.scm. PLAYBOOKs
 ;;; introduce no new authority; they execute permitted plans.
 ;;;
-;;; SPDX-License-Identifier: PMPL-1.0-or-later
+;;; SPDX-License-Identifier: MPL-2.0
 ;;; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
 
 (define-module (echo-types playbook)
diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml
@@ -12,7 +12,7 @@
 ;;; concluded; the verdict is negative; the documentation cascade has been
 ;;; applied; the recipe is no longer a candidate locus of distinctness.
 ;;;
-;;; SPDX-License-Identifier: PMPL-1.0-or-later
+;;; SPDX-License-Identifier: MPL-2.0
 ;;; SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
 
 (define-module (echo-types ei-2 state)
@@ -36,7 +36,7 @@
     (canonical-host . github)                ; per current forge workflow
     (mirrors        . (gitlab codeberg))
     (version-target . "0.1.1")
-    (license        . "PMPL-1.0-or-later")))
+    (license        . "MPL-2.0")))
 
 ;;; ============================================================
 ;;; Session header
diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml
@@ -1,4 +1,4 @@
-; SPDX-License-Identifier: PMPL-1.0-or-later
+; SPDX-License-Identifier: MPL-2.0
 ; 0-AI-MANIFEST.a2ml — echo-types
 
 [ai-contract]
diff --git a/Containerfile b/Containerfile
@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-License-Identifier: MPL-2.0
 # Containerfile — podman-build fallback when stapeln is unavailable.
 
 # TODO(scaffold): pin @sha256
diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: MPL-2.0
 = echo-types: explain me
 :icons: font
 
diff --git a/QUICKSTART-DEV.adoc b/QUICKSTART-DEV.adoc
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: MPL-2.0
 = QUICKSTART-DEV: echo-types
 :toc:
 
diff --git a/QUICKSTART-MAINTAINER.adoc b/QUICKSTART-MAINTAINER.adoc
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: MPL-2.0
 = QUICKSTART-MAINTAINER: echo-types
 :toc:
 
diff --git a/QUICKSTART-USER.adoc b/QUICKSTART-USER.adoc
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: MPL-2.0
 = QUICKSTART-USER: echo-types
 :toc:
 
diff --git a/README.md b/README.md
@@ -1,10 +1,10 @@
-<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
+<!-- SPDX-License-Identifier: MPL-2.0 -->
 <!-- SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
 
 # echo-types
 
 [![OpenSSF Best Practices](https://img.shields.io/badge/OpenSSF-Best_Practices-green?logo=opensourcesecurity)](https://www.bestpractices.dev/en/projects/new?repo_url=https://github.com/hyperpolymath/echo-types)
-[![License: PMPL-1.0](https://img.shields.io/badge/License-PMPL--1.0-blue.svg)](https://github.com/hyperpolymath/palimpsest-license)
+[![License: MPL-2.0](https://img.shields.io/badge/License-MPL--2.0-blue.svg)](https://www.mozilla.org/en-US/MPL/2.0/)
 [![Green Web](https://api.thegreenwebfoundation.org/greencheckimage/github.com)](https://www.thegreenwebfoundation.org/green-web-check/?url=github.com)
 
 Constructive Agda development for echo types as a first-class notion of structured loss:
diff --git a/TOPOLOGY.adoc b/TOPOLOGY.adoc
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: MPL-2.0
 = echo-types: topology
 :toc:
 
diff --git a/arghda-core/Cargo.toml b/arghda-core/Cargo.toml
@@ -3,7 +3,7 @@ name = "arghda-core"
 version = "0.1.0"
 edition = "2021"
 description = "Lightweight proof-workspace manager for Agda"
-license = "PMPL-1.0-or-later"
+license = "MPL-2.0"
 repository = "https://github.com/hyperpolymath/echo-types"
 
 [[bin]]
diff --git a/contractiles/Dustfile.a2ml b/contractiles/Dustfile.a2ml
@@ -1,4 +1,4 @@
-; SPDX-License-Identifier: PMPL-1.0-or-later
+; SPDX-License-Identifier: MPL-2.0
 ; Dustfile.a2ml — recovery & rollback for echo-types.
 
 (contractile :kind dust :version 1)
diff --git a/contractiles/Intentfile.a2ml b/contractiles/Intentfile.a2ml
@@ -1,4 +1,4 @@
-; SPDX-License-Identifier: PMPL-1.0-or-later
+; SPDX-License-Identifier: MPL-2.0
 ; Intentfile.a2ml — declared future intent for echo-types.
 
 (contractile :kind intent :version 1)
diff --git a/contractiles/Mustfile.a2ml b/contractiles/Mustfile.a2ml
@@ -1,4 +1,4 @@
-; SPDX-License-Identifier: PMPL-1.0-or-later
+; SPDX-License-Identifier: MPL-2.0
 ; Mustfile.a2ml — physical state invariants for echo-types.
 
 (contractile :kind must :version 1)
diff --git a/contractiles/Trustfile.a2ml b/contractiles/Trustfile.a2ml
@@ -1,11 +1,11 @@
-; SPDX-License-Identifier: PMPL-1.0-or-later
+; SPDX-License-Identifier: MPL-2.0
 ; Trustfile.a2ml — integrity & provenance for echo-types.
 
 (contractile :kind trust :version 1)
 
 (trust license-content
   :doc "LICENSE contains expected SPDX identifier."
-  :cmd "grep -q 'PMPL\\|License' LICENSE")
+  :cmd "grep -q 'Mozilla Public License' LICENSE")
 
 (trust no-secrets-committed
   :doc "No credential files committed."
diff --git a/docs/PMPL-NARRATIVE.adoc b/docs/PMPL-NARRATIVE.adoc
@@ -0,0 +1,106 @@
+// SPDX-License-Identifier: MPL-2.0
+// SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+= PMPL as Narrative Overlay
+:toc: macro
+:toclevels: 2
+:sectnums:
+:icons: font
+
+[.lead]
+This repository is licensed under *MPL-2.0* (see `LICENSE`). The
+*PMPL* (Palimpsest-MPL) name remains as a *narrative / cultural /
+discipline overlay* documented here, NOT as an SPDX identifier and
+NOT as a separate legal text. This file exists to record what the
+PMPL framing contributes that the bare MPL-2.0 identifier does not.
+
+== Policy in one paragraph
+
+*Stated licence (legal):* MPL-2.0. This is the licence the SPDX
+headers carry, the LICENSE file contains, the README badge displays,
+and downstream consumers / registries / scanners see. There is no
+"PMPL-1.0-or-later" SPDX identifier in this repository.
+
+*PMPL (narrative):* the working-discipline framing under which this
+code was developed. Palimpsest-MPL was, in its prior incarnation, an
+overlay licence whose text incorporated MPL-2.0 by reference. The
+owner direction of 2026-05-20 collapsed the overlay into MPL-2.0
+proper and lifted the *posture* it represented into this narrative
+document. No legal content was lost: PMPL's operative legal effect
+*was* MPL-2.0 (lawyer-confirmed). What was discarded is a stated
+SPDX identifier that registries, scanners, and downstream tooling
+treated as foreign.
+
+== What PMPL represented
+
+The Palimpsest framing carried three commitments that survive intact
+under MPL-2.0:
+
+. *Multi-author authorship as the default reading.* "Palimpsest"
+  named the working assumption that a meaningful body of code is
+  *layered*: contributions overwrite, gloss, and re-purpose
+  predecessors, and the licence regime should reflect that no single
+  author owns the latest layer cleanly. MPL-2.0's file-level
+  copyleft realises exactly this: each file is its own unit, and the
+  layering is visible in the file's history.
+. *Source availability as a discipline, not a strategy.* PMPL was
+  written to make source release the *default* rather than an
+  opt-in. MPL-2.0's "any covered file you distribute, you make the
+  source available for" clause is the operative version of the same
+  commitment.
+. *Narrative coherence over registry convenience.* PMPL's text spent
+  prose on the *why* of its terms; MPL-2.0 spends none. This
+  document is where the *why* now lives, divorced from the legal
+  text it used to be attached to.
+
+== What we no longer claim
+
+. *That PMPL is a distinct licence at registries.* It never was at
+  any standard SPDX registry. crates.io, npm, Hackage, Debian's
+  copyright scanners and similar all treated `PMPL-1.0-or-later` as
+  foreign and required an OSI-recognised fallback (which is
+  precisely MPL-2.0). Carrying both identifiers was friction
+  without legal effect.
+. *That there is a separate Palimpsest copyleft regime.* There
+  isn't. The legal regime is MPL-2.0; the working discipline that
+  PMPL named is documented here.
+. *That `palimpsest-license` is a co-licensing dependency.* It is
+  reference-only documentation of the prior framing. Downstream
+  consumers do not need to read it.
+
+== Header convention going forward
+
+Source files carry exactly:
+
+[source]
+----
+SPDX-License-Identifier: MPL-2.0
+SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+----
+
+No `PMPL-1.0-or-later`, no compound `MPL-2.0 OR …` clauses, no
+inline comment explaining "MPL-2.0 is the legal fallback for PMPL".
+The header is the legal statement; this document is the narrative.
+Authoring new files: use the two lines above verbatim (substitute
+copyright holder as appropriate); do not invent overlays.
+
+== History
+
+* *Prior to 2026-05-20*: `PMPL-1.0-or-later` was the stated SPDX
+  identifier across this and ~69 other repositories in the estate.
+  MPL-2.0 was named as the automatic legal fallback (lawyer-confirmed).
+* *2026-05-20 (owner direction)*: collapse the SPDX identifier to
+  MPL-2.0; preserve the PMPL framing as this narrative document.
+* *Drift note*: SPDX headers across the wider estate may still carry
+  `PMPL-1.0-or-later` and will be migrated in their own time. The
+  legal effect is unchanged (MPL-2.0 is the operative licence in
+  either case); the stated identifier is the only thing that
+  differs. Migration is owner-paced and manual.
+
+== References
+
+* `LICENSE` (MPL-2.0 full text, this repository).
+* `LICENSE-docs` (CC-BY-4.0 full text for documentation, this
+  repository).
+* Mozilla Public License v2.0 — https://www.mozilla.org/en-US/MPL/2.0/
+* SPDX licence list — https://spdx.org/licenses/MPL-2.0.html
diff --git a/docs/echidna-design-search-2026-04-28.adoc b/docs/echidna-design-search-2026-04-28.adoc
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: MPL-2.0
 = Echidna design-search findings — Phase 1.3 + unbudgeted wf-<ᵇʳᶠ_
 :date: 2026-04-28
 :toc:
diff --git a/docs/echo-types/MAP.adoc b/docs/echo-types/MAP.adoc
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: MPL-2.0
 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 = echo-types: Master Map
 :toc: macro
diff --git a/docs/echo-types/echo-kernel-note.adoc b/docs/echo-types/echo-kernel-note.adoc
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: MPL-2.0
 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 = echo-types: kernel vs derived (one-page note)
 :toc: macro
diff --git a/docs/echo-types/paper.adoc b/docs/echo-types/paper.adoc
diff --git a/docs/echo-types/types-abstract.adoc b/docs/echo-types/types-abstract.adoc
diff --git a/docs/foundation.adoc b/docs/foundation.adoc
diff --git a/flake.nix b/flake.nix
diff --git a/scripts/kernel-guard.sh b/scripts/kernel-guard.sh
diff --git a/stapeln.toml b/stapeln.toml
diff --git a/tools/check-guardrails.sh b/tools/check-guardrails.sh

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-# SPDX-License-Identifier: PMPL-1.0-or-later`
	`1`	`+# SPDX-License-Identifier: MPL-2.0`
`2`	`2`	`root = true`
`3`	`3`
`4`	`4`	`[*]`
Original file line number	Diff line number	Diff line change
`@@ -1,2 +1,2 @@`
`1`		`-# SPDX-License-Identifier: PMPL-1.0-or-later`
	`1`	`+# SPDX-License-Identifier: MPL-2.0`
`2`	`2`	`use flake`