hyperpolymath · hyperpolymath · Jun 26, 2026 · Jun 26, 2026 · Jun 26, 2026 · Jun 26, 2026
diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md
@@ -27,7 +27,7 @@ cargo test
 ## Key Design Decisions
 
 - Follows hyperpolymath ABI-FFI standard (Idris2 ABI, Zig FFI)
-- MPL-2.0 license
+- MPL-2.0 license (code) + CC-BY-SA-4.0 (docs); full texts in LICENSES/
 - RSR (Rhodium Standard Repository) template
 - Author: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 

diff --git a/.github/workflows/rhodibot.yml b/.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

diff --git a/.gitignore b/.gitignore
@@ -18,6 +18,11 @@ Thumbs.db
 /dist/
 /out/
 
+# Idris2 build artifacts
+**/build/
+*.ttc
+*.ttm
+
 # Dependencies
 /node_modules/
 /vendor/

diff --git a/.machine_readable/compliance/reuse/dep5 b/.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
diff --git a/.machine_readable/contractiles/trust/Trustfile.a2ml b/.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

diff --git a/Cargo.toml b/Cargo.toml
@@ -5,7 +5,7 @@ version = "0.1.0"
 edition = "2024"
 authors = ["Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>"]
 description = "Generate formally verified real-time embedded code via Lustre/Esterel synchronous reactive programming"
-license-file = "LICENSE"
+license = "MPL-2.0"
 repository = "https://github.com/hyperpolymath/lustreiser"
 keywords = ["lustre", "esterel", "embedded", "real-time", "safety"]
 categories = ["command-line-utilities", "development-tools"]

diff --git a/LICENSE b/LICENSE
@@ -1,3 +1,5 @@
+SPDX-License-Identifier: MPL-2.0
+
 Mozilla Public License Version 2.0
 ==================================
 

diff --git a/QUICKSTART-MAINTAINER.adoc b/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

diff --git a/contractiles/trust/Trustfile.a2ml b/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

diff --git a/docs/RSR_OUTLINE.adoc b/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)

diff --git a/docs/STATE-VISUALIZER.adoc b/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
 
 ─────────────────────────────────────────────────────────────────────────────

diff --git a/src/interface/abi/Foreign.idr → src/interface/abi/Lustreiser/ABI/Foreign.idr b/src/interface/abi/Foreign.idr → src/interface/abi/Lustreiser/ABI/Foreign.idr
@@ -171,6 +171,9 @@ getClockTree h = do
   if ptr == 0
     then pure Nothing
     else pure (Just (prim__getString ptr))
+  where
+    %foreign "support:idris2_getString, libidris2_support"
+    prim__getString : Bits64 -> String
 
 --------------------------------------------------------------------------------
 -- Stream Buffer Management
@@ -211,11 +214,6 @@ checkMemoryFit h ram = do
 -- String Operations
 --------------------------------------------------------------------------------
 
-||| Convert C string to Idris String
-export
-%foreign "support:idris2_getString, libidris2_support"
-prim__getString : Bits64 -> String
-
 ||| Free C string allocated by the library
 export
 %foreign "C:lustreiser_free_string, liblustreiser"
@@ -237,6 +235,9 @@ getString h = do
       let str = prim__getString ptr
       primIO (prim__freeString ptr)
       pure (Just str)
+  where
+    %foreign "support:idris2_getString, libidris2_support"
+    prim__getString : Bits64 -> String
 
 --------------------------------------------------------------------------------
 -- Error Handling
@@ -255,6 +256,9 @@ lastError = do
   if ptr == 0
     then pure Nothing
     else pure (Just (prim__getString ptr))
+  where
+    %foreign "support:idris2_getString, libidris2_support"
+    prim__getString : Bits64 -> String
 
 ||| Get error description for result code
 export
@@ -282,6 +286,9 @@ version : IO String
 version = do
   ptr <- primIO prim__version
   pure (prim__getString ptr)
+  where
+    %foreign "support:idris2_getString, libidris2_support"
+    prim__getString : Bits64 -> String
 
 ||| Get library build info
 export
@@ -294,6 +301,9 @@ buildInfo : IO String
 buildInfo = do
   ptr <- primIO prim__buildInfo
   pure (prim__getString ptr)
+  where
+    %foreign "support:idris2_getString, libidris2_support"
+    prim__getString : Bits64 -> String
 
 --------------------------------------------------------------------------------
 -- Callback Support