iseriser: normalize licensing to MPL-2.0 (code) + CC-BY-SA-4.0 (docs) (#68)

* iseriser: make Phase 0 ABI proofs genuinely compile and verify

The hand-written Idris2 ABI was never compiler-checked and did not
typecheck under Idris2 0.7.0. Make the foundation real and machine-verified.

Layout.idr
- Discharge the two open holes: ?fieldsAlignedProof and ?offsetInBoundsProof.
- Add a sound decDivides decision procedure (builds genuine m = k*n
  witnesses) and decFieldsAligned; checkCABI now returns a real
  CABICompliant proof or an error.
- offsetInBounds had an unsound signature (claimed every field fits any
  layout); make it an honest decidable Maybe.
- Fix paddingFor (Nat has no Neg; use minus) and give the three concrete
  struct layouts explicit alignment witnesses.
- Replace alignUpCorrect's non-compiling Refl proof with a sound
  alignUpDivides decision; the general lemma is noted as residual work.

Types.idr
- FullyResolved and GenerationComplete carried no obligation; give them
  real So-proofs (no {{/}} markers remain; all seven categories present).
- thisPlatform was a %runElab stub needing ElabReflection; make it total.
- DecEq Result used `No absurd` with no Uninhabited instance; discharge
  the off-diagonal cases explicitly.
- createHandle left the auto So (ptr /= 0) unsolved; use choose.

Proofs.idr (new)
- Machine-checked theorems: the three concrete FFI struct layouts are
  provably C-ABI aligned; Result→C-int pins; generation-completeness.

Structure / tooling
- Move ABI into src/interface/abi/Iseriser/ABI/ so it builds as an Idris2
  package (matches the chapeliser layout); add iseriser-abi.ipkg.
- Add `just proofs` recipe; ignore Idris build artifacts.
- verification/proofs/ now documents and points at the verified proofs.

Verified: `idris2 --build iseriser-abi.ipkg` clean (0 warnings);
cargo test green (57 unit + 9 integration).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA

* Add SPDX header to LICENSE and set Cargo.toml license field

The governance/licence-consistency check requires an SPDX-License-Identifier
header on the LICENSE file and a `license` field in the manifest. The LICENSE
body is MPL-2.0 text, so stamp `SPDX-License-Identifier: MPL-2.0` (matching the
actual body) and set `license = "MPL-2.0"` (replacing `license-file`).

Verified with standards/scripts/check-licence-consistency.sh (passes).

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA

* iseriser: normalize licensing to MPL-2.0 (code) + CC-BY-SA-4.0 (docs)

Make the repo's licensing story single and consistent: code/config under
MPL-2.0, documentation prose under CC-BY-SA-4.0, with both full texts in
LICENSES/ and the MPL-2.0 LICENSE at root for GitHub's licence chip.

- README: replace the PMPL-1.0/Palimpsest-Covenant badges and the
  "Licensed under the Palimpsest License" footer with MPL-2.0 (code) +
  CC-BY-SA-4.0 (docs) badges/text linking LICENSES/.
- dep5: add a docs carve-out (*.adoc, *.md, docs/**) -> CC-BY-SA-4.0 so the
  two-SPDX split is actually encoded (was *-> MPL-2.0 with no docs split).
- Remove contradictory self-licence claims from QUICKSTART-MAINTAINER.adoc,
  docs/RSR_OUTLINE.adoc, docs/STATE-VISUALIZER.adoc, rhodibot.yml comments,
  and the two Trustfile LICENSE-content checks.
- Preserve legitimate non-self references: cargo-deny's AGPL deny-list, the
  "never use AGPL" estate policy, and the Contributor Covenant CoC.

Verified: standards/scripts/check-licence-consistency.sh passes.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA

---------

Co-authored-by: Jonathan D.A. Jewell <paraordinate@yahoo.co.uk>
Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

Author: 3 people

.github/workflows/rhodibot.yml

@@ -4,7 +4,7 @@
 # Reads root-hygiene rules and auto-fixes what it can:
 #   - Delete banned files (AI.djot, duplicate CONTRIBUTING.adoc, stale snapshots)
 #   - Rename misnamed files (AI.a2ml → 0-AI-MANIFEST.a2ml)
-#   - Fix SPDX headers (AGPL → PMPL in dotfiles)
+#   - Fix SPDX headers (AGPL → MPL-2.0 in dotfiles)
 #   - Create missing required files (SECURITY.md, CONTRIBUTING.md)
 #   - Report unfixable issues as PR comments
 #
@@ -87,7 +87,7 @@ jobs:
           for dotfile in .gitignore .gitattributes .editorconfig; do
             if [ -f "$dotfile" ] && grep -q "AGPL-3.0" "$dotfile" 2>/dev/null; then
               sed -i 's/AGPL-3.0-or-later/MPL-2.0/g; s/AGPL-3.0/MPL-2.0/g' "$dotfile"
-              FIXES="$FIXES\n- Fixed SPDX header in \`$dotfile\` (AGPL → PMPL)"
+              FIXES="$FIXES\n- Fixed SPDX header in \`$dotfile\` (AGPL → MPL-2.0)"
               CHANGED=true
             fi
           done

.machine_readable/compliance/reuse/dep5

@@ -52,3 +52,10 @@ License: MPL-2.0
 Files: cliff.toml
 Copyright: {{CURRENT_YEAR}} {{AUTHOR}} ({{OWNER}}) <{{AUTHOR_EMAIL}}>
 License: MPL-2.0
+
+# Documentation prose is CC-BY-SA-4.0 (code/config is MPL-2.0).
+# Last-match-wins in the Debian copyright format, so this overrides the
+# `Files: *` default above for prose docs.
+Files: *.adoc *.md docs/* docs/**/*
+Copyright: {{CURRENT_YEAR}} {{AUTHOR}} ({{OWNER}}) <{{AUTHOR_EMAIL}}>
+License: CC-BY-SA-4.0

.machine_readable/contractiles/trust/Trustfile.a2ml

@@ -34,7 +34,7 @@ is traceable.
 
 ### license-content
 - description: LICENSE contains expected identifier
-- run: grep -q 'PMPL\|MPL\|MIT\|Apache\|LGPL' LICENSE
+- run: grep -q 'MPL-2.0' LICENSE
 - severity: warning
 
 ## Container Security

QUICKSTART-MAINTAINER.adoc

@@ -106,7 +106,7 @@ Or via OPSM: `opsm update {{PACKAGE_NAME}}`
 
 == Security Notes
 
-* License: MPL-2.0 (Palimpsest License)
+* License: MPL-2.0 (code) / CC-BY-SA-4.0 (docs)
 * All dependencies SHA-pinned
 * `panic-attacker` scan results: link:INSTALL-SECURITY-REPORT.adoc[]
 * OpenSSF Scorecard: see badge in README

README.md

@@ -3,8 +3,7 @@ SPDX-License-Identifier: CC-BY-SA-4.0
 SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 -->
 
-[![License: MPL-2.0](https://img.shields.io/badge/license-PMPL--1.0--or--later-blue)](LICENSE) ![Palimpsest
-Covenant](https://img.shields.io/badge/Palimpsest-Covenant-purple) ![29
+[![License: MPL-2.0](https://img.shields.io/badge/license-MPL--2.0-blue)](LICENSE) [![Docs: CC-BY-SA-4.0](https://img.shields.io/badge/docs-CC--BY--SA--4.0-blue)](LICENSES/CC-BY-SA-4.0.txt) ![29
 repos](https://img.shields.io/badge/-iser_family-29_repos-brightgreen)
 ![Idris2 ABI](https://img.shields.io/badge/ABI-Idris2-red) ![Zig
 FFI](https://img.shields.io/badge/FFI-Zig-orange)
@@ -303,9 +302,7 @@ Hypatia neurosymbolic scanning.
 
 # License
 
-SPDX-License-Identifier: `MPL-2.0`
+Code is licensed under `MPL-2.0`; documentation under `CC-BY-SA-4.0`.
+Full licence texts are in [`LICENSES/`](LICENSES/).
 
 Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath)
-
-Licensed under the [Palimpsest
-License](https://github.com/hyperpolymath/palimpsest-license).

contractiles/trust/Trustfile.a2ml

@@ -16,7 +16,7 @@ Maximal trust by default — LLM may read, build, test, lint, format.
 
 ### license-content
 - description: LICENSE contains expected SPDX identifier
-- run: grep -q 'SPDX\|License\|MIT\|Apache\|PMPL\|MPL' LICENSE
+- run: grep -q 'SPDX\|MPL-2.0' LICENSE
 - severity: critical
 
 ### no-secrets-committed

docs/RSR_OUTLINE.adoc

@@ -1,6 +1,6 @@
 = RSR Template Repository
 
-image:[Palimpsest-MPL-1.0,link="https://github.com/hyperpolymath/palimpsest-license"] image:[Palimpsest,link="https://github.com/hyperpolymath/palimpsest-license"]
+image:https://img.shields.io/badge/license-MPL--2.0-blue[MPL-2.0,link="LICENSES/MPL-2.0.txt"] image:https://img.shields.io/badge/docs-CC--BY--SA--4.0-blue[CC-BY-SA-4.0,link="LICENSES/CC-BY-SA-4.0.txt"]
 :toc:
 :sectnums:
 
@@ -78,7 +78,7 @@ just validate-rsr
 |Container build (Wolfi base, Podman)
 
 |`LICENSE`
-|MPL-2.0 (Palimpsest MPL)
+|MPL-2.0 (code) / CC-BY-SA-4.0 (docs)
 
 |`EXHIBIT-A-ETHICAL-USE.txt`
 |Ethical use guidelines (LICENSE Exhibit A)

docs/STATE-VISUALIZER.adoc

@@ -87,7 +87,7 @@ CONTAINER ECOSYSTEM (Phase 2)
 
 REPO INFRASTRUCTURE
   .machine_readable/                ██████████ 100%    STATE/META/ECOSYSTEM active
-  Governance & License              ██████████ 100%    PMPL & Ethical use verified
+  Governance & License              ██████████ 100%    MPL-2.0 & Ethical use verified
   Development Shells (Nix/Guix)     ██████████ 100%    Reproducible env stable
 
 ─────────────────────────────────────────────────────────────────────────────