chore(license): flip 32 PMPL→AGPL-3.0-or-later SPDX stamps (per 2026-06-02 estate policy) (#46)

hyperpolymath · claude · web-flow · commit e5a14be1f676 · 2026-06-02T20:48:50.000+01:00
Co-authored-by: Claude Opus 4.7 (1M context) &lt;noreply@anthropic.com&gt;
diff --git a/.github/workflows/parse-gate.yml b/.github/workflows/parse-gate.yml
@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # parse-gate.yml — Gates the trusted String->Statement parser
diff --git a/.github/workflows/proof-corpus.yml b/.github/workflows/proof-corpus.yml
@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-License-Identifier: AGPL-3.0-or-later
 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 #
 # proof-corpus.yml — Machine-checks the VclTotal Idris2 proof corpus.
diff --git a/docs/VERIFICATION-STANCE.adoc b/docs/VERIFICATION-STANCE.adoc
@@ -2,7 +2,7 @@
 :toc:
 :sectnums:
 
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: AGPL-3.0-or-later
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 
 WARNING: vcl-ut is the interface between *hypatia* and *verisim*. Both sides
diff --git a/docs/decisions/0002-ffi-attestation-trust-boundary.adoc b/docs/decisions/0002-ffi-attestation-trust-boundary.adoc
@@ -1,5 +1,5 @@
 = Architecture Decision Record: 0002-ffi-attestation-trust-boundary
-<!-- SPDX-License-Identifier: PMPL-1.0-or-later -->
+<!-- SPDX-License-Identifier: AGPL-3.0-or-later -->
 <!-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> -->
 
 # 2. FFI trust boundary: recompute-PCC over wasm32 (Tier-1), C-ABI attestation (Tier-2)
diff --git a/src/core/Decide.idr b/src/core/Decide.idr
@@ -1,4 +1,4 @@
--- SPDX-License-Identifier: PMPL-1.0-or-later
+-- SPDX-License-Identifier: AGPL-3.0-or-later
 -- Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
 ||| VCL-total Core Decide — canonical safety deciders (single source of truth)
diff --git a/src/interface/WireConformance.idr b/src/interface/WireConformance.idr
@@ -1,4 +1,4 @@
--- SPDX-License-Identifier: PMPL-1.0-or-later
+-- SPDX-License-Identifier: AGPL-3.0-or-later
 -- Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
 ||| VCL-total Interface — Cross-language Wire + Decision Conformance
diff --git a/src/interface/WireDecode.idr b/src/interface/WireDecode.idr
@@ -1,4 +1,4 @@
--- SPDX-License-Identifier: PMPL-1.0-or-later
+-- SPDX-License-Identifier: AGPL-3.0-or-later
 -- Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 
 ||| VCL-total Interface — Wire Decoder (P5b step 2, vcl-ut#25)
diff --git a/src/interface/abi/LayoutProofs.idr b/src/interface/abi/LayoutProofs.idr
@@ -1,4 +1,4 @@
--- SPDX-License-Identifier: PMPL-1.0-or-later
+-- SPDX-License-Identifier: AGPL-3.0-or-later
 -- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 
 ||| VCL-cap ABI Layout — genuine alignment / no-padding / bounds proofs
diff --git a/src/interface/attest/ATTESTATION-FORMAT.adoc b/src/interface/attest/ATTESTATION-FORMAT.adoc
@@ -1,7 +1,7 @@
 = VCL-total Tier-2 Attestation Format v1 (P5d, vcl-ut#25)
 :toc:
 
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: AGPL-3.0-or-later
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 
 Normative format for the **Tier-2 (C-ABI trusted-certifier
diff --git a/src/interface/attest/Cargo.toml b/src/interface/attest/Cargo.toml
@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-License-Identifier: AGPL-3.0-or-later
 
 # Standalone workspace root (same rationale as ../parse, ../recompute-wasm):
 # decoupled from the broken parent virtual workspace. This is the Tier-2
diff --git a/src/interface/attest/README.adoc b/src/interface/attest/README.adoc
@@ -1,7 +1,7 @@
 = vcltotal-attest
 :toc:
 
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: AGPL-3.0-or-later
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 
 P5d of hyperpolymath/vcl-ut#25 — **Tier-2: C-ABI trusted-certifier
diff --git a/src/interface/attest/src/lib.rs b/src/interface/attest/src/lib.rs
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: AGPL-3.0-or-later
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 
 //! P5d (#25) — **Tier-2: C-ABI trusted-certifier attestation
diff --git a/src/interface/parse/Cargo.toml b/src/interface/parse/Cargo.toml
@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-License-Identifier: AGPL-3.0-or-later
 
 # Standalone workspace root: decouples this trusted boundary crate from
 # the parent virtual workspace, whose pre-existing `src/interface`
diff --git a/src/interface/parse/WIRE-FORMAT.adoc b/src/interface/parse/WIRE-FORMAT.adoc
@@ -1,7 +1,7 @@
 = VCL-total Statement Wire Format v1 (P5b, vcl-ut#25)
 :toc:
 
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: AGPL-3.0-or-later
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 
 The `Statement` marshalling format. The Rust encoder/decoder
diff --git a/src/interface/parse/src/ast.rs b/src/interface/parse/src/ast.rs
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: AGPL-3.0-or-later
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 
 //! Faithful Rust mirror of the Idris2 query AST in `src/core/Grammar.idr`
diff --git a/src/interface/parse/src/decider.rs b/src/interface/parse/src/decider.rs
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: AGPL-3.0-or-later
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 
 //! P5c (recompute tier) — a **faithful** Rust port of the certified
diff --git a/src/interface/parse/src/lexer.rs b/src/interface/parse/src/lexer.rs
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: AGPL-3.0-or-later
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 
 //! Total, panic-free tokenizer. Every code path returns a `Result`; the
diff --git a/src/interface/parse/src/lib.rs b/src/interface/parse/src/lib.rs
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: AGPL-3.0-or-later
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 
 //! `vcltotal-parse` — P5a of issue #25 (reinforce the verified-corpus
diff --git a/src/interface/parse/src/parser.rs b/src/interface/parse/src/parser.rs
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: AGPL-3.0-or-later
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 
 //! Total, panic-free recursive-descent parser for the VCL-total
diff --git a/src/interface/parse/src/schema.rs b/src/interface/parse/src/schema.rs
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: AGPL-3.0-or-later
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 
 //! Faithful Rust mirror of `src/core/Schema.idr`'s `OctadSchema`
diff --git a/src/interface/parse/src/wire.rs b/src/interface/parse/src/wire.rs
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: AGPL-3.0-or-later
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 
 //! P5b (#25): the C-ABI marshalling codec — `Statement` <-> a
diff --git a/src/interface/parse/tests/conformance_emit.rs b/src/interface/parse/tests/conformance_emit.rs
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: AGPL-3.0-or-later
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 
 //! P5b cross-language conformance: the **regeneration oracle** for the
diff --git a/src/interface/parse/tests/parse.rs b/src/interface/parse/tests/parse.rs
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: AGPL-3.0-or-later
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 
 //! Totality / panic-freedom property for the trusted parser (P5a, #25).
diff --git a/src/interface/parse/tests/wire.rs b/src/interface/parse/tests/wire.rs
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: AGPL-3.0-or-later
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 
 //! P5b (#25) wire-codec properties: the machine witnesses for
diff --git a/src/interface/recompute-wasm/AFFINESCRIPTISER-NA.adoc b/src/interface/recompute-wasm/AFFINESCRIPTISER-NA.adoc
@@ -1,7 +1,7 @@
 = Why affinescriptiser is not used for the recompute-wasm entry
 :toc:
 
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: AGPL-3.0-or-later
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 
 P5c (vcl-ut#25) ships the recompute-PCC tier as a `wasm32` module
diff --git a/src/interface/recompute-wasm/Cargo.toml b/src/interface/recompute-wasm/Cargo.toml
@@ -1,4 +1,4 @@
-# SPDX-License-Identifier: PMPL-1.0-or-later
+# SPDX-License-Identifier: AGPL-3.0-or-later
 
 # Standalone workspace root (same rationale as ../parse/Cargo.toml): the
 # parent virtual workspace has a pre-existing unresolvable external
diff --git a/src/interface/recompute-wasm/README.adoc b/src/interface/recompute-wasm/README.adoc
@@ -1,7 +1,7 @@
 = vcltotal-recompute-wasm
 :toc:
 
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: AGPL-3.0-or-later
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 
 P5c of hyperpolymath/vcl-ut#25 — the **recompute-PCC tier's `wasm32`
diff --git a/src/interface/recompute-wasm/src/lib.rs b/src/interface/recompute-wasm/src/lib.rs
@@ -1,4 +1,4 @@
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: AGPL-3.0-or-later
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 
 //! P5c (#25) — the recompute-PCC tier's `wasm32` entry point.
diff --git a/verification/proofs/README.adoc b/verification/proofs/README.adoc
@@ -1,6 +1,6 @@
 = Proofs Unit
 
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: AGPL-3.0-or-later
 
 This directory holds the *machine-verified* proof artefacts for vcl-ut.
 
diff --git a/verification/proofs/SafetyL4Model.idr b/verification/proofs/SafetyL4Model.idr
@@ -1,4 +1,4 @@
--- SPDX-License-Identifier: PMPL-1.0-or-later
+-- SPDX-License-Identifier: AGPL-3.0-or-later
 -- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 
 ||| Self-contained machine-checked model of the Level-4 (SQL-injection)
diff --git a/verification/proofs/VERIFICATION-STANCE.adoc b/verification/proofs/VERIFICATION-STANCE.adoc
@@ -2,7 +2,7 @@
 :toc:
 :sectnums:
 
-// SPDX-License-Identifier: PMPL-1.0-or-later
+// SPDX-License-Identifier: AGPL-3.0-or-later
 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 
 WARNING: vcl-ut is the interface between *hypatia* and *verisim*; both sides
diff --git a/verification/proofs/vclut-core.ipkg b/verification/proofs/vclut-core.ipkg
@@ -1,4 +1,4 @@
--- SPDX-License-Identifier: PMPL-1.0-or-later
+-- SPDX-License-Identifier: AGPL-3.0-or-later
 -- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>
 --
 -- Machine-check package for the VclTotal proof corpus (Phase 1,

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: AGPL-3.0-or-later`
`2`	`2`	`# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk>`
`3`	`3`	`#`
`4`	`4`	`# parse-gate.yml — Gates the trusted String->Statement parser`
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: AGPL-3.0-or-later`
`2`	`2`	`-- Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>`
`3`	`3`
`4`	`4`	`\|\|\| VCL-total Core Decide — canonical safety deciders (single source of truth)`