From 9b0f8d041ad70b879881e95c6b44ca60a7aa366f Mon Sep 17 00:00:00 2001 From: hyperpolymath <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 24 Jun 2026 16:26:51 +0100 Subject: [PATCH] chore(licence): normalise to MPL-2.0 (code) + CC-BY-SA-4.0 (docs) - LICENSES/ = {MPL-2.0.txt, CC-BY-SA-4.0.txt}; root LICENSE = verbatim MPL-2.0 (GitHub display) - SPDX: code -> MPL-2.0, docs (.md/.adoc) -> CC-BY-SA-4.0; metadata/badge fixes; vendored untouched Co-Authored-By: Claude Opus 4.8 (1M context) --- .clusterfuzzlite/Dockerfile | 8 +- .githooks/pre-commit | 2 +- .gitlab/issue_templates/bug.md | 2 +- .gitlab/issue_templates/feature.md | 2 +- .gitlab/merge_request_templates/default.md | 2 +- .../agent_instructions/README.adoc | 2 +- .machine_readable/svc/k9/README.adoc | 2 +- .trivyignore | 2 +- AFFIRMATION.adoc | 2 +- AUTHORS.md | 2 +- CHANGELOG.md | 2 +- CODE_OF_CONDUCT.md | 2 +- CONTRIBUTING.adoc | 4 +- CONTRIBUTING.md | 2 +- EXPLAINME.adoc | 2 +- LICENSE | 1036 ++++++----------- LICENSES/CC-BY-SA-4.0.txt | 170 +++ LICENSES/MIT.txt | 21 - LICENSES/PMPL-1.0-or-later.txt | 162 --- LICENSES/PMPL-1.0.txt | 153 --- LICENSES/Palimpsest-0.6.txt | 93 -- MAINTAINERS.adoc | 2 +- QUICKSTART-USER.adoc | 2 +- README.adoc | 2 +- README.md | 2 +- RSR_COMPLIANCE.adoc | 2 +- SECURITY.md | 2 +- TEST_CI_ECHIDNA.md | 2 +- container/README.adoc | 2 +- crates/echidna-core-spark/CREUSOT-SETUP.md | 2 +- crates/echidna-mcp/README.md | 2 +- crates/echidna-wire/schemas/VERSIONING.md | 2 +- data/synonyms/README.adoc | 2 +- docs/ARCHITECTURE.md | 2 +- docs/ASPECT_QUICK_START.md | 2 +- docs/ASPECT_TAGGING.md | 2 +- docs/CORPUS-ADAPTERS.md | 2 +- docs/CORPUS.md | 2 +- docs/ENV-VARS.md | 2 +- docs/HP-BACKEND-ONBOARDING.md | 4 +- docs/LEARNING-ARCHITECTURE.adoc | 2 +- docs/PROVER_COUNT.md | 2 +- docs/ROADMAP.md | 2 +- docs/SSG_ROADMAP.adoc | 2 +- docs/SUPPORTED_PROVERS.md | 2 +- docs/architecture/CHAPEL-SATURATION-HOOKS.md | 2 +- docs/architecture/CROSS-REPO-PROOF-DAG.md | 2 +- docs/architecture/JULIA-SATURATION-HOOKS.md | 2 +- .../architecture/TYPE-DISCIPLINE-EMBEDDING.md | 2 +- docs/architecture/VERISIM-ER-SCHEMA.md | 2 +- docs/bench/2026-05-30-chapel-mrr-baseline.md | 2 +- .../2026-04-28-corpus-and-design-search.md | 2 +- .../2026-05-19-ci-baseline-triage.md | 2 +- .../2026-05-30-chapel-l23-cancel-token.md | 2 +- .../2026-05-30-chapel-pic-rebuild.md | 2 +- .../2026-05-30-chapel-rehabilitation.md | 2 +- .../2026-05-31-chapel-prover-spawn-hooks.md | 2 +- .../2026-06-01-saturation-campaign.md | 2 +- docs/deployment/DEPLOYMENT_GUIDE.md | 2 +- ...IDNA-VERISIM-TRIANGULATION-2026-04-17.adoc | 2 +- docs/design/SPARK_ADOPTION_PLAN.md | 2 +- docs/governance/JUST_AND_MUST_FRAMEWORK.md | 6 +- docs/handover/B7-AUDIT-CORRECTION.md | 2 +- docs/handover/HANDOVER-INDEX.md | 2 +- docs/handover/L3-GATE-PATH.adoc | 2 +- docs/handover/PHASE-3-PROMPT.md | 2 +- .../handover/PROVER-CORPUS-SATURATION-LANE.md | 2 +- docs/handover/README.md | 2 +- docs/handover/S4-LOOP-CLOSURE-RUNBOOK.md | 2 +- docs/handover/SESSION-HANDOFF-2026-06-15.md | 2 +- docs/handover/SUGGEST-CLI-PROMPT.md | 2 +- docs/handover/THEOREM-METADATA-MIGRATION.md | 2 +- docs/handover/llm-warmup-dev.md | 2 +- docs/handover/llm-warmup-user.md | 2 +- docs/maintenance/MAINTENANCE-CHECKLIST.adoc | 2 +- .../SOFTWARE-DEVELOPMENT-APPROACH.adoc | 2 +- .../audit/2026-03-31-echidna-audit.adoc | 2 +- docs/tech-debt-2026-05-26.md | 2 +- docs/training-runs/2026-06-02.md | 2 +- docs/wiki/Architecture.md | 2 +- docs/wiki/FAQ.md | 2 +- docs/wiki/Getting-Started.md | 2 +- docs/wiki/Guides.md | 2 +- docs/wiki/Home.md | 2 +- docs/wiki/Troubleshooting.md | 2 +- echidna-playground/.github/CODEOWNERS | 2 +- echidna-playground/CONTRIBUTING.adoc | 2 +- echidna-playground/MAINTAINERS.adoc | 2 +- echidna-playground/README.adoc | 2 +- echidna-playground/RSR_OUTLINE.adoc | 2 +- examples/simple_proof.v | 2 +- hooks/README.md | 2 +- meta-checker/README.adoc | 2 +- metrics/README.md | 2 +- proofs/acl2/associativity.lisp | 2 +- proofs/acl2/binary_trees.lisp | 2 +- proofs/acl2/factorial.lisp | 2 +- proofs/acl2/list_append.lisp | 2 +- proofs/acl2/sorting.lisp | 2 +- proofs/agda/Basic.agda | 2 +- proofs/hol4/arithmetic.sml | 2 +- proofs/hol4/binary_tree.sml | 2 +- proofs/hol4/list_append.sml | 2 +- proofs/hol4/set_theory.sml | 2 +- proofs/hol4/sorting.sml | 2 +- proofs/lean/Basic.lean | 2 +- proofs/lean/List.lean | 2 +- proofs/lean/Propositional.lean | 2 +- proofs/lean/README.md | 2 +- proofs/lean/THEOREMS.md | 2 +- proofs/pvs/arithmetic.pvs | 2 +- proofs/pvs/binary_search.pvs | 2 +- proofs/pvs/list_theory.pvs | 2 +- proofs/pvs/set_theory.pvs | 2 +- proofs/pvs/sorting.pvs | 2 +- reports/audits/audit-ffi-boundary.md | 2 +- .../audits/audit-pa021-axioms-2026-05-26.md | 2 +- rules/security_learning.lgt | 2 +- schemas/VERSIONING.md | 2 +- scripts/build-production.sh | 2 +- scripts/demo-proof.sh | 2 +- scripts/expand_training_data.sh | 2 +- scripts/test-integration.sh | 2 +- spark/README.adoc | 2 +- src/julia/README.md | 4 +- src/julia/retrain_from_verisim.jl | 2 +- src/julia/test_server.jl | 2 +- src/ui/tea/echidna_gui.affine | 2 +- src/ui/tea/echidna_tea.js | 2 +- src/zig/ffi/echidna_ffi.h | 2 +- training_data/proof_states_v2.jsonl | 10 +- 131 files changed, 683 insertions(+), 1226 deletions(-) mode change 120000 => 100644 .clusterfuzzlite/Dockerfile create mode 100644 LICENSES/CC-BY-SA-4.0.txt delete mode 100644 LICENSES/MIT.txt delete mode 100644 LICENSES/PMPL-1.0-or-later.txt delete mode 100644 LICENSES/PMPL-1.0.txt delete mode 100644 LICENSES/Palimpsest-0.6.txt diff --git a/.clusterfuzzlite/Dockerfile b/.clusterfuzzlite/Dockerfile deleted file mode 120000 index 5240dc01..00000000 --- a/.clusterfuzzlite/Dockerfile +++ /dev/null @@ -1 +0,0 @@ -Containerfile \ No newline at end of file diff --git a/.clusterfuzzlite/Dockerfile b/.clusterfuzzlite/Dockerfile new file mode 100644 index 00000000..43f88636 --- /dev/null +++ b/.clusterfuzzlite/Dockerfile @@ -0,0 +1,7 @@ +# SPDX-License-Identifier: MPL-2.0 +FROM gcr.io/oss-fuzz-base/base-builder-rust@sha256:73c1d5648db54100639339d411a5d192cbc8bf413ee91e843a07cf6f0e319dc7 + +COPY . $SRC/echidna +WORKDIR $SRC/echidna + +COPY .clusterfuzzlite/build.sh $SRC/ diff --git a/.githooks/pre-commit b/.githooks/pre-commit index dce58237..92c8d936 100755 --- a/.githooks/pre-commit +++ b/.githooks/pre-commit @@ -3,7 +3,7 @@ # ECHIDNA Pre-commit Hook # Enforces npm ban and runs checks # -# SPDX-License-Identifier: MIT OR AGPL-3.0-or-later +# SPDX-License-Identifier: MPL-2.0 OR AGPL-3.0-or-later set -euo pipefail diff --git a/.gitlab/issue_templates/bug.md b/.gitlab/issue_templates/bug.md index 2c841086..435015a0 100644 --- a/.gitlab/issue_templates/bug.md +++ b/.gitlab/issue_templates/bug.md @@ -1,5 +1,5 @@ diff --git a/.gitlab/issue_templates/feature.md b/.gitlab/issue_templates/feature.md index bd275ddd..43070c55 100644 --- a/.gitlab/issue_templates/feature.md +++ b/.gitlab/issue_templates/feature.md @@ -1,5 +1,5 @@ diff --git a/.gitlab/merge_request_templates/default.md b/.gitlab/merge_request_templates/default.md index 0557d276..fcfc2e2a 100644 --- a/.gitlab/merge_request_templates/default.md +++ b/.gitlab/merge_request_templates/default.md @@ -1,5 +1,5 @@ diff --git a/.machine_readable/agent_instructions/README.adoc b/.machine_readable/agent_instructions/README.adoc index 9bc2e24b..1cc7487e 100644 --- a/.machine_readable/agent_instructions/README.adoc +++ b/.machine_readable/agent_instructions/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) = Agent Instructions :toc: preamble diff --git a/.machine_readable/svc/k9/README.adoc b/.machine_readable/svc/k9/README.adoc index 9c3099fd..16107f14 100644 --- a/.machine_readable/svc/k9/README.adoc +++ b/.machine_readable/svc/k9/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 = K9 Contractiles :toc: left :icons: font diff --git a/.trivyignore b/.trivyignore index fd38d441..e9a06537 100644 --- a/.trivyignore +++ b/.trivyignore @@ -1,4 +1,4 @@ -# SPDX-License-Identifier: MIT AND Palimpsest-0.6 +# SPDX-License-Identifier: MPL-2.0 AND Palimpsest-0.6 # SPDX-FileCopyrightText: 2024-2025 ECHIDNA Project Contributors # # Trivy ignore file for ECHIDNA diff --git a/AFFIRMATION.adoc b/AFFIRMATION.adoc index cf077390..67f6ffb3 100644 --- a/AFFIRMATION.adoc +++ b/AFFIRMATION.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell = ECHIDNA — Affirmation of Honest State diff --git a/AUTHORS.md b/AUTHORS.md index fdb6befc..6388b8ab 100644 --- a/AUTHORS.md +++ b/AUTHORS.md @@ -1,6 +1,6 @@ diff --git a/CHANGELOG.md b/CHANGELOG.md index 0e76027a..efc80f77 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,5 @@ - + # Changelog All notable changes to ECHIDNA will be documented in this file. diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md index 7293ffc5..b1194f09 100644 --- a/CODE_OF_CONDUCT.md +++ b/CODE_OF_CONDUCT.md @@ -1,6 +1,6 @@ diff --git a/CONTRIBUTING.adoc b/CONTRIBUTING.adoc index e2dcea9e..06ed4b7e 100644 --- a/CONTRIBUTING.adoc +++ b/CONTRIBUTING.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell = ECHIDNA — Contributing :toc: macro @@ -156,7 +156,7 @@ header: [source] ---- -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-FileCopyrightText: ---- diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 644fb6a8..b9aa0c91 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -1,5 +1,5 @@ diff --git a/TEST_CI_ECHIDNA.md b/TEST_CI_ECHIDNA.md index daccbfa8..f9230a88 100644 --- a/TEST_CI_ECHIDNA.md +++ b/TEST_CI_ECHIDNA.md @@ -1,6 +1,6 @@ # CI Test for ECHIDNA -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 This is a test file to trigger CI workflows for echidna. diff --git a/container/README.adoc b/container/README.adoc index 8dec1f72..e10644b4 100644 --- a/container/README.adoc +++ b/container/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 = ECHIDNA Container Ecosystem (Stapeln) :author: Jonathan D.A. Jewell diff --git a/crates/echidna-core-spark/CREUSOT-SETUP.md b/crates/echidna-core-spark/CREUSOT-SETUP.md index afea85d5..2caa775c 100644 --- a/crates/echidna-core-spark/CREUSOT-SETUP.md +++ b/crates/echidna-core-spark/CREUSOT-SETUP.md @@ -1,4 +1,4 @@ - + # Creusot Setup Guide diff --git a/crates/echidna-mcp/README.md b/crates/echidna-mcp/README.md index 9ebeeda1..960888d1 100644 --- a/crates/echidna-mcp/README.md +++ b/crates/echidna-mcp/README.md @@ -1,4 +1,4 @@ - + # echidna-mcp diff --git a/crates/echidna-wire/schemas/VERSIONING.md b/crates/echidna-wire/schemas/VERSIONING.md index 8148a549..fc3c1b7f 100644 --- a/crates/echidna-wire/schemas/VERSIONING.md +++ b/crates/echidna-wire/schemas/VERSIONING.md @@ -1,4 +1,4 @@ - + # ECHIDNA Wire Schema Versioning Policy (`crates/echidna-wire`) diff --git a/data/synonyms/README.adoc b/data/synonyms/README.adoc index c1f2c30c..cdfa8cbc 100644 --- a/data/synonyms/README.adoc +++ b/data/synonyms/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 = Tactic / Lemma Synonym Tables :toc: macro diff --git a/docs/ARCHITECTURE.md b/docs/ARCHITECTURE.md index 2b76eeea..6b289a7c 100644 --- a/docs/ARCHITECTURE.md +++ b/docs/ARCHITECTURE.md @@ -1,4 +1,4 @@ - + # ECHIDNA Architecture diff --git a/docs/ASPECT_QUICK_START.md b/docs/ASPECT_QUICK_START.md index 46886616..79170fe7 100644 --- a/docs/ASPECT_QUICK_START.md +++ b/docs/ASPECT_QUICK_START.md @@ -161,4 +161,4 @@ cargo test --lib aspect ## License -SPDX-License-Identifier: MPL-2.0 +SPDX-License-Identifier: CC-BY-SA-4.0 diff --git a/docs/ASPECT_TAGGING.md b/docs/ASPECT_TAGGING.md index 0d802134..a6a99b95 100644 --- a/docs/ASPECT_TAGGING.md +++ b/docs/ASPECT_TAGGING.md @@ -351,4 +351,4 @@ cargo run --example aspect_tagging_demo ## License SPDX-FileCopyrightText: 2025 ECHIDNA Project Team -SPDX-License-Identifier: MPL-2.0 +SPDX-License-Identifier: CC-BY-SA-4.0 diff --git a/docs/CORPUS-ADAPTERS.md b/docs/CORPUS-ADAPTERS.md index 44311c64..594ac534 100644 --- a/docs/CORPUS-ADAPTERS.md +++ b/docs/CORPUS-ADAPTERS.md @@ -1,6 +1,6 @@ # Corpus Adapters — Index diff --git a/docs/CORPUS.md b/docs/CORPUS.md index 7bde3a7f..66d89a6a 100644 --- a/docs/CORPUS.md +++ b/docs/CORPUS.md @@ -1,4 +1,4 @@ - + # Echidna Corpus — N-dimensional, octad-shaped, cross-prover diff --git a/docs/ENV-VARS.md b/docs/ENV-VARS.md index b620e9d6..94be7b66 100644 --- a/docs/ENV-VARS.md +++ b/docs/ENV-VARS.md @@ -1,4 +1,4 @@ - + # ECHIDNA Environment Variables diff --git a/docs/HP-BACKEND-ONBOARDING.md b/docs/HP-BACKEND-ONBOARDING.md index b4f9aa29..398df125 100644 --- a/docs/HP-BACKEND-ONBOARDING.md +++ b/docs/HP-BACKEND-ONBOARDING.md @@ -1,5 +1,5 @@ @@ -112,7 +112,7 @@ parametric `TypeInfo` so the unified verifier knows what to check. `tests/fixtures/hp/foo_trivial.tll`: ``` -# SPDX-License-Identifier: MPL-2.0 +# SPDX-License-Identifier: CC-BY-SA-4.0 #discipline: foo theorem foo_identity : ... . diff --git a/docs/LEARNING-ARCHITECTURE.adoc b/docs/LEARNING-ARCHITECTURE.adoc index b9d87e05..80415270 100644 --- a/docs/LEARNING-ARCHITECTURE.adoc +++ b/docs/LEARNING-ARCHITECTURE.adoc @@ -4,7 +4,7 @@ :revdate: 2026-04-17 :toc: preamble -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 == Problem diff --git a/docs/PROVER_COUNT.md b/docs/PROVER_COUNT.md index f447a8d7..c9ba6347 100644 --- a/docs/PROVER_COUNT.md +++ b/docs/PROVER_COUNT.md @@ -1,4 +1,4 @@ - + # Canonical Prover Count and Tier Table diff --git a/docs/ROADMAP.md b/docs/ROADMAP.md index cbe99e6f..42f10c88 100644 --- a/docs/ROADMAP.md +++ b/docs/ROADMAP.md @@ -1,4 +1,4 @@ - + # ECHIDNA Roadmap diff --git a/docs/SSG_ROADMAP.adoc b/docs/SSG_ROADMAP.adoc index 57fca2cc..29443b41 100644 --- a/docs/SSG_ROADMAP.adoc +++ b/docs/SSG_ROADMAP.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-FileCopyrightText: 2024-2025 ECHIDNA Project Contributors = SSG Integration Roadmap diff --git a/docs/SUPPORTED_PROVERS.md b/docs/SUPPORTED_PROVERS.md index fe3b9de7..4a161bf7 100644 --- a/docs/SUPPORTED_PROVERS.md +++ b/docs/SUPPORTED_PROVERS.md @@ -1,6 +1,6 @@ # Supported Provers diff --git a/docs/architecture/CHAPEL-SATURATION-HOOKS.md b/docs/architecture/CHAPEL-SATURATION-HOOKS.md index 7c50fe99..5fbce037 100644 --- a/docs/architecture/CHAPEL-SATURATION-HOOKS.md +++ b/docs/architecture/CHAPEL-SATURATION-HOOKS.md @@ -1,6 +1,6 @@ # Chapel ↔ Saturation Campaign Integration Hooks diff --git a/docs/architecture/CROSS-REPO-PROOF-DAG.md b/docs/architecture/CROSS-REPO-PROOF-DAG.md index 494f1da8..308fa3f8 100644 --- a/docs/architecture/CROSS-REPO-PROOF-DAG.md +++ b/docs/architecture/CROSS-REPO-PROOF-DAG.md @@ -1,5 +1,5 @@ diff --git a/docs/architecture/JULIA-SATURATION-HOOKS.md b/docs/architecture/JULIA-SATURATION-HOOKS.md index c9ba13b0..5714195f 100644 --- a/docs/architecture/JULIA-SATURATION-HOOKS.md +++ b/docs/architecture/JULIA-SATURATION-HOOKS.md @@ -1,6 +1,6 @@ # Julia Saturation Hooks — Rust corpus adapters → Julia GNN pipeline diff --git a/docs/architecture/TYPE-DISCIPLINE-EMBEDDING.md b/docs/architecture/TYPE-DISCIPLINE-EMBEDDING.md index 7a8ad1ab..29b884cc 100644 --- a/docs/architecture/TYPE-DISCIPLINE-EMBEDDING.md +++ b/docs/architecture/TYPE-DISCIPLINE-EMBEDDING.md @@ -1,6 +1,6 @@ # Type-Discipline Embedding — 39-Discipline Corpus Annotation diff --git a/docs/architecture/VERISIM-ER-SCHEMA.md b/docs/architecture/VERISIM-ER-SCHEMA.md index 02b6c97b..af11c159 100644 --- a/docs/architecture/VERISIM-ER-SCHEMA.md +++ b/docs/architecture/VERISIM-ER-SCHEMA.md @@ -1,6 +1,6 @@ # VeriSim ↔ ECHIDNA Entity-Relationship Schema diff --git a/docs/bench/2026-05-30-chapel-mrr-baseline.md b/docs/bench/2026-05-30-chapel-mrr-baseline.md index acf5045c..34c5352a 100644 --- a/docs/bench/2026-05-30-chapel-mrr-baseline.md +++ b/docs/bench/2026-05-30-chapel-mrr-baseline.md @@ -1,4 +1,4 @@ - + # Chapel speedup baseline — 2026-05-30 diff --git a/docs/decisions/2026-04-28-corpus-and-design-search.md b/docs/decisions/2026-04-28-corpus-and-design-search.md index a72598be..a4685cba 100644 --- a/docs/decisions/2026-04-28-corpus-and-design-search.md +++ b/docs/decisions/2026-04-28-corpus-and-design-search.md @@ -1,4 +1,4 @@ - + # 2026-04-28 — Corpus, design-search, swarm, and the N-dim VeriSim plan diff --git a/docs/decisions/2026-05-19-ci-baseline-triage.md b/docs/decisions/2026-05-19-ci-baseline-triage.md index 252fcd30..cb643cfb 100644 --- a/docs/decisions/2026-05-19-ci-baseline-triage.md +++ b/docs/decisions/2026-05-19-ci-baseline-triage.md @@ -1,4 +1,4 @@ - + # 2026-05-19 — CI baseline triage: real defects vs baseline-rot vs infra jam diff --git a/docs/decisions/2026-05-30-chapel-l23-cancel-token.md b/docs/decisions/2026-05-30-chapel-l23-cancel-token.md index bd6141e8..ecfc6e84 100644 --- a/docs/decisions/2026-05-30-chapel-l23-cancel-token.md +++ b/docs/decisions/2026-05-30-chapel-l23-cancel-token.md @@ -1,4 +1,4 @@ - + # 2026-05-30 — L2.3 cancel-token preemption for speculative search diff --git a/docs/decisions/2026-05-30-chapel-pic-rebuild.md b/docs/decisions/2026-05-30-chapel-pic-rebuild.md index 16acde34..e0923afb 100644 --- a/docs/decisions/2026-05-30-chapel-pic-rebuild.md +++ b/docs/decisions/2026-05-30-chapel-pic-rebuild.md @@ -1,4 +1,4 @@ - + # 2026-05-30 — Chapel PIC rebuild from source for `--library --dynamic` diff --git a/docs/decisions/2026-05-30-chapel-rehabilitation.md b/docs/decisions/2026-05-30-chapel-rehabilitation.md index 5993d8ff..9649efc9 100644 --- a/docs/decisions/2026-05-30-chapel-rehabilitation.md +++ b/docs/decisions/2026-05-30-chapel-rehabilitation.md @@ -1,4 +1,4 @@ - + # 2026-05-30 — Chapel metalayer rehabilitation: rewrite, not park diff --git a/docs/decisions/2026-05-31-chapel-prover-spawn-hooks.md b/docs/decisions/2026-05-31-chapel-prover-spawn-hooks.md index c22cd2e3..012c5473 100644 --- a/docs/decisions/2026-05-31-chapel-prover-spawn-hooks.md +++ b/docs/decisions/2026-05-31-chapel-prover-spawn-hooks.md @@ -1,4 +1,4 @@ - + # 2026-05-31 — Per-prover spawn hooks: cwd + filenameOverride diff --git a/docs/decisions/2026-06-01-saturation-campaign.md b/docs/decisions/2026-06-01-saturation-campaign.md index 1f812a0f..8023effe 100644 --- a/docs/decisions/2026-06-01-saturation-campaign.md +++ b/docs/decisions/2026-06-01-saturation-campaign.md @@ -1,6 +1,6 @@ # ADR 2026-06-01 — Prover / Corpus / Vocab / Synonyms / Arbitration Saturation Campaign diff --git a/docs/deployment/DEPLOYMENT_GUIDE.md b/docs/deployment/DEPLOYMENT_GUIDE.md index 45e3ac6a..32533c25 100644 --- a/docs/deployment/DEPLOYMENT_GUIDE.md +++ b/docs/deployment/DEPLOYMENT_GUIDE.md @@ -1,5 +1,5 @@ diff --git a/docs/design/ECHIDNA-VERISIM-TRIANGULATION-2026-04-17.adoc b/docs/design/ECHIDNA-VERISIM-TRIANGULATION-2026-04-17.adoc index 7f0fc9b1..0cda21bf 100644 --- a/docs/design/ECHIDNA-VERISIM-TRIANGULATION-2026-04-17.adoc +++ b/docs/design/ECHIDNA-VERISIM-TRIANGULATION-2026-04-17.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell :toc: left :toclevels: 3 diff --git a/docs/design/SPARK_ADOPTION_PLAN.md b/docs/design/SPARK_ADOPTION_PLAN.md index a86b9af3..8636f786 100644 --- a/docs/design/SPARK_ADOPTION_PLAN.md +++ b/docs/design/SPARK_ADOPTION_PLAN.md @@ -1,4 +1,4 @@ - + # SPARK Adoption Plan — Echidna Trust Pipeline **Status:** Proposal diff --git a/docs/governance/JUST_AND_MUST_FRAMEWORK.md b/docs/governance/JUST_AND_MUST_FRAMEWORK.md index 6acd7d63..370d997e 100644 --- a/docs/governance/JUST_AND_MUST_FRAMEWORK.md +++ b/docs/governance/JUST_AND_MUST_FRAMEWORK.md @@ -35,7 +35,7 @@ Together, these create a **stable, predictable development experience**. **Justfile** (complete, comprehensive): ```justfile -# SPDX-License-Identifier: MIT OR Palimpsest-0.6 +# SPDX-License-Identifier: CC-BY-SA-4.0 OR Palimpsest-0.6 # ECHIDNA Standard Build System # List all available commands @@ -370,7 +370,7 @@ dev-cycle: ```bash #!/usr/bin/env bash -# SPDX-License-Identifier: MIT OR Palimpsest-0.6 +# SPDX-License-Identifier: CC-BY-SA-4.0 OR Palimpsest-0.6 # Must Validation System # # Exit codes: @@ -570,7 +570,7 @@ jobs: ```bash #!/usr/bin/env bash -# SPDX-License-Identifier: MIT OR Palimpsest-0.6 +# SPDX-License-Identifier: CC-BY-SA-4.0 OR Palimpsest-0.6 # Pre-commit hook: Run quick validation set -e diff --git a/docs/handover/B7-AUDIT-CORRECTION.md b/docs/handover/B7-AUDIT-CORRECTION.md index b9aa71e7..a103010c 100644 --- a/docs/handover/B7-AUDIT-CORRECTION.md +++ b/docs/handover/B7-AUDIT-CORRECTION.md @@ -1,5 +1,5 @@ diff --git a/docs/handover/HANDOVER-INDEX.md b/docs/handover/HANDOVER-INDEX.md index 4077e8ff..19581109 100644 --- a/docs/handover/HANDOVER-INDEX.md +++ b/docs/handover/HANDOVER-INDEX.md @@ -1,4 +1,4 @@ - + # Handover Index diff --git a/docs/handover/L3-GATE-PATH.adoc b/docs/handover/L3-GATE-PATH.adoc index 886e3f3f..85d10009 100644 --- a/docs/handover/L3-GATE-PATH.adoc +++ b/docs/handover/L3-GATE-PATH.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell :toc: left :toclevels: 2 diff --git a/docs/handover/PHASE-3-PROMPT.md b/docs/handover/PHASE-3-PROMPT.md index 321dadc6..2d6c9364 100644 --- a/docs/handover/PHASE-3-PROMPT.md +++ b/docs/handover/PHASE-3-PROMPT.md @@ -1,4 +1,4 @@ - + # Echidna Phase 3 — Real-Algebraic + Modal/Hybrid Backends — Opus Handoff Prompt **Context**: Phase 3 of the ECHIDNA expansion is the diff --git a/docs/handover/PROVER-CORPUS-SATURATION-LANE.md b/docs/handover/PROVER-CORPUS-SATURATION-LANE.md index d9909b1f..937eca74 100644 --- a/docs/handover/PROVER-CORPUS-SATURATION-LANE.md +++ b/docs/handover/PROVER-CORPUS-SATURATION-LANE.md @@ -1,6 +1,6 @@ # Saturation Lane — Prover/Corpus/Vocab/Synonyms/Arbitration diff --git a/docs/handover/README.md b/docs/handover/README.md index 3df0787e..4bcedc8e 100644 --- a/docs/handover/README.md +++ b/docs/handover/README.md @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 # Echidna Handover Prompts diff --git a/docs/handover/S4-LOOP-CLOSURE-RUNBOOK.md b/docs/handover/S4-LOOP-CLOSURE-RUNBOOK.md index 8d8aa7ec..b10adb76 100644 --- a/docs/handover/S4-LOOP-CLOSURE-RUNBOOK.md +++ b/docs/handover/S4-LOOP-CLOSURE-RUNBOOK.md @@ -1,4 +1,4 @@ - + # S4 Loop-Closure Runbook diff --git a/docs/handover/SESSION-HANDOFF-2026-06-15.md b/docs/handover/SESSION-HANDOFF-2026-06-15.md index 481c2e67..672aa23d 100644 --- a/docs/handover/SESSION-HANDOFF-2026-06-15.md +++ b/docs/handover/SESSION-HANDOFF-2026-06-15.md @@ -1,4 +1,4 @@ - + # Session handoff — 2026-06-15 diff --git a/docs/handover/SUGGEST-CLI-PROMPT.md b/docs/handover/SUGGEST-CLI-PROMPT.md index cfe15f08..47de8d2f 100644 --- a/docs/handover/SUGGEST-CLI-PROMPT.md +++ b/docs/handover/SUGGEST-CLI-PROMPT.md @@ -1,4 +1,4 @@ - + # Echidna `suggest` — CLI Verb + Variant Tester — Sonnet Handoff Prompt **Context**: Echidna's `prove` CLI is a one-shot dispatcher. When a proof diff --git a/docs/handover/THEOREM-METADATA-MIGRATION.md b/docs/handover/THEOREM-METADATA-MIGRATION.md index b3046d27..a0c66f6a 100644 --- a/docs/handover/THEOREM-METADATA-MIGRATION.md +++ b/docs/handover/THEOREM-METADATA-MIGRATION.md @@ -1,5 +1,5 @@ - + # Theorem Metadata Migration (deferred) diff --git a/docs/handover/llm-warmup-dev.md b/docs/handover/llm-warmup-dev.md index 7bc21815..f7a8d45c 100644 --- a/docs/handover/llm-warmup-dev.md +++ b/docs/handover/llm-warmup-dev.md @@ -1,4 +1,4 @@ - + diff --git a/docs/handover/llm-warmup-user.md b/docs/handover/llm-warmup-user.md index 840d9a03..efd0e92f 100644 --- a/docs/handover/llm-warmup-user.md +++ b/docs/handover/llm-warmup-user.md @@ -1,4 +1,4 @@ - + diff --git a/docs/maintenance/MAINTENANCE-CHECKLIST.adoc b/docs/maintenance/MAINTENANCE-CHECKLIST.adoc index 0aa3e1b6..09a43d24 100644 --- a/docs/maintenance/MAINTENANCE-CHECKLIST.adoc +++ b/docs/maintenance/MAINTENANCE-CHECKLIST.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 = ECHIDNA Maintenance Checklist :author: Jonathan D.A. Jewell :toc: diff --git a/docs/practice/SOFTWARE-DEVELOPMENT-APPROACH.adoc b/docs/practice/SOFTWARE-DEVELOPMENT-APPROACH.adoc index 854c368f..42439fa0 100644 --- a/docs/practice/SOFTWARE-DEVELOPMENT-APPROACH.adoc +++ b/docs/practice/SOFTWARE-DEVELOPMENT-APPROACH.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 = ECHIDNA Software Development Approach :author: Jonathan D.A. Jewell :toc: diff --git a/docs/reports/audit/2026-03-31-echidna-audit.adoc b/docs/reports/audit/2026-03-31-echidna-audit.adoc index cebe8caf..c3b3b2a0 100644 --- a/docs/reports/audit/2026-03-31-echidna-audit.adoc +++ b/docs/reports/audit/2026-03-31-echidna-audit.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 = ECHIDNA Audit 2026-03-31 :revdate: 2026-03-31 diff --git a/docs/tech-debt-2026-05-26.md b/docs/tech-debt-2026-05-26.md index 12ead3fc..5f497196 100644 --- a/docs/tech-debt-2026-05-26.md +++ b/docs/tech-debt-2026-05-26.md @@ -1,5 +1,5 @@ diff --git a/docs/training-runs/2026-06-02.md b/docs/training-runs/2026-06-02.md index e593c4d3..a14aabf5 100644 --- a/docs/training-runs/2026-06-02.md +++ b/docs/training-runs/2026-06-02.md @@ -1,5 +1,5 @@ diff --git a/docs/wiki/Architecture.md b/docs/wiki/Architecture.md index f68f5075..46a87f40 100644 --- a/docs/wiki/Architecture.md +++ b/docs/wiki/Architecture.md @@ -1,5 +1,5 @@ - + # Architecture The canonical, current architecture overview lives in the repo at diff --git a/docs/wiki/FAQ.md b/docs/wiki/FAQ.md index 300fb4fe..2ae4a6f5 100644 --- a/docs/wiki/FAQ.md +++ b/docs/wiki/FAQ.md @@ -1,5 +1,5 @@ - + # FAQ ## How many provers are supported? diff --git a/docs/wiki/Getting-Started.md b/docs/wiki/Getting-Started.md index ea1dd1dc..431ab98c 100644 --- a/docs/wiki/Getting-Started.md +++ b/docs/wiki/Getting-Started.md @@ -1,5 +1,5 @@ - + # Getting Started The canonical quickstart docs live in the repo: diff --git a/docs/wiki/Guides.md b/docs/wiki/Guides.md index 1f22df64..143ca1e0 100644 --- a/docs/wiki/Guides.md +++ b/docs/wiki/Guides.md @@ -1,5 +1,5 @@ - + # Guides ## Adding a new prover backend diff --git a/docs/wiki/Home.md b/docs/wiki/Home.md index 0e629f74..aeb4899e 100644 --- a/docs/wiki/Home.md +++ b/docs/wiki/Home.md @@ -1,5 +1,5 @@ - + # ECHIDNA Wiki **ECHIDNA** — Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance — is a trust-hardened neurosymbolic theorem-proving platform supporting **128 prover backends** (12 core, exposed by default API; see [`docs/PROVER_COUNT.md`](https://github.com/hyperpolymath/echidna/blob/main/docs/PROVER_COUNT.md) for the tier breakdown). diff --git a/docs/wiki/Troubleshooting.md b/docs/wiki/Troubleshooting.md index 768a8b8a..58c93454 100644 --- a/docs/wiki/Troubleshooting.md +++ b/docs/wiki/Troubleshooting.md @@ -1,5 +1,5 @@ - + # Troubleshooting ## Build fails with `openssl` errors diff --git a/echidna-playground/.github/CODEOWNERS b/echidna-playground/.github/CODEOWNERS index a2f47751..a4e8fd3b 100644 --- a/echidna-playground/.github/CODEOWNERS +++ b/echidna-playground/.github/CODEOWNERS @@ -1,4 +1,4 @@ -# SPDX-License-Identifier: AGPL-3.0-or-later +# SPDX-License-Identifier: MPL-2.0 # CODEOWNERS - Defines code ownership for mandatory review requirements # # These owners will be requested for review when someone opens a pull request diff --git a/echidna-playground/CONTRIBUTING.adoc b/echidna-playground/CONTRIBUTING.adoc index 1f34e602..eb045d61 100644 --- a/echidna-playground/CONTRIBUTING.adoc +++ b/echidna-playground/CONTRIBUTING.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 = Contributing Guide == Getting Started diff --git a/echidna-playground/MAINTAINERS.adoc b/echidna-playground/MAINTAINERS.adoc index a1c65443..48d97817 100644 --- a/echidna-playground/MAINTAINERS.adoc +++ b/echidna-playground/MAINTAINERS.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 = Maintainers :toc: preamble diff --git a/echidna-playground/README.adoc b/echidna-playground/README.adoc index 5a129498..7f94b4ff 100644 --- a/echidna-playground/README.adoc +++ b/echidna-playground/README.adoc @@ -1,5 +1,5 @@ = Coq-Jr: Web-Native Interactive Theorem Proving -image:https://img.shields.io/badge/License-PMPL--1.0-blue.svg[License: PMPL-1.0,link="https://github.com/hyperpolymath/palimpsest-license"] +image:https://img.shields.io/badge/License-MPL--2.0-blue.svg[License: PMPL-1.0,link="https://github.com/hyperpolymath/palimpsest-license"] diff --git a/echidna-playground/RSR_OUTLINE.adoc b/echidna-playground/RSR_OUTLINE.adoc index 46adb909..d73bbf60 100644 --- a/echidna-playground/RSR_OUTLINE.adoc +++ b/echidna-playground/RSR_OUTLINE.adoc @@ -209,7 +209,7 @@ This template is part of: == License -SPDX-License-Identifier: MPL-2.0 +SPDX-License-Identifier: CC-BY-SA-4.0 == Links diff --git a/examples/simple_proof.v b/examples/simple_proof.v index 898425d5..3f0c8109 100644 --- a/examples/simple_proof.v +++ b/examples/simple_proof.v @@ -1,4 +1,4 @@ -(* SPDX-License-Identifier: MIT OR Palimpsest-0.6 *) +(* SPDX-License-Identifier: MPL-2.0 OR Palimpsest-0.6 *) (* Simple Coq proof demonstrating ECHIDNA capabilities *) (** * Simple Arithmetic Proof diff --git a/hooks/README.md b/hooks/README.md index e3af2e68..46069db5 100644 --- a/hooks/README.md +++ b/hooks/README.md @@ -1,4 +1,4 @@ - + # Git hooks diff --git a/meta-checker/README.adoc b/meta-checker/README.adoc index 5d6b3ef0..8b7ce9ac 100644 --- a/meta-checker/README.adoc +++ b/meta-checker/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) = ECHIDNA Meta-Checker diff --git a/metrics/README.md b/metrics/README.md index e47de728..cbcccdb1 100644 --- a/metrics/README.md +++ b/metrics/README.md @@ -1,6 +1,6 @@ # ECHIDNA metrics suite - + Measures the cross-prover corpus along eight axes that together bound the vocabulary horizon and triangulation capacity. Every metric diff --git a/proofs/acl2/associativity.lisp b/proofs/acl2/associativity.lisp index 87e4a8d2..4b60d509 100644 --- a/proofs/acl2/associativity.lisp +++ b/proofs/acl2/associativity.lisp @@ -1,5 +1,5 @@ ; SPDX-FileCopyrightText: 2025 ECHIDNA Project Team -; SPDX-License-Identifier: MIT OR Palimpsest-0.6 +; SPDX-License-Identifier: MPL-2.0 OR Palimpsest-0.6 ;; Associativity of addition ;; Demonstrates ACL2's automated proof with induction diff --git a/proofs/acl2/binary_trees.lisp b/proofs/acl2/binary_trees.lisp index b19b9892..30457274 100644 --- a/proofs/acl2/binary_trees.lisp +++ b/proofs/acl2/binary_trees.lisp @@ -1,5 +1,5 @@ ; SPDX-FileCopyrightText: 2025 ECHIDNA Project Team -; SPDX-License-Identifier: MIT OR Palimpsest-0.6 +; SPDX-License-Identifier: MPL-2.0 OR Palimpsest-0.6 ;; Binary tree operations ;; Demonstrates data structure reasoning diff --git a/proofs/acl2/factorial.lisp b/proofs/acl2/factorial.lisp index 9018ff6a..4a1faa0c 100644 --- a/proofs/acl2/factorial.lisp +++ b/proofs/acl2/factorial.lisp @@ -1,5 +1,5 @@ ; SPDX-FileCopyrightText: 2025 ECHIDNA Project Team -; SPDX-License-Identifier: MIT OR Palimpsest-0.6 +; SPDX-License-Identifier: MPL-2.0 OR Palimpsest-0.6 ;; Factorial function with guards ;; Demonstrates ACL2's guard verification and executable specifications diff --git a/proofs/acl2/list_append.lisp b/proofs/acl2/list_append.lisp index e2c0f142..b03594b3 100644 --- a/proofs/acl2/list_append.lisp +++ b/proofs/acl2/list_append.lisp @@ -1,5 +1,5 @@ ; SPDX-FileCopyrightText: 2025 ECHIDNA Project Team -; SPDX-License-Identifier: MIT OR Palimpsest-0.6 +; SPDX-License-Identifier: MPL-2.0 OR Palimpsest-0.6 ;; List append properties ;; Demonstrates recursive definitions and list reasoning diff --git a/proofs/acl2/sorting.lisp b/proofs/acl2/sorting.lisp index a0746f33..0dd4d53b 100644 --- a/proofs/acl2/sorting.lisp +++ b/proofs/acl2/sorting.lisp @@ -1,5 +1,5 @@ ; SPDX-FileCopyrightText: 2025 ECHIDNA Project Team -; SPDX-License-Identifier: MIT OR Palimpsest-0.6 +; SPDX-License-Identifier: MPL-2.0 OR Palimpsest-0.6 ;; Insertion sort correctness ;; Demonstrates algorithm verification diff --git a/proofs/agda/Basic.agda b/proofs/agda/Basic.agda index 5441bd74..17574fbd 100644 --- a/proofs/agda/Basic.agda +++ b/proofs/agda/Basic.agda @@ -1,5 +1,5 @@ -- SPDX-FileCopyrightText: 2025 ECHIDNA Project Team --- SPDX-License-Identifier: MIT AND Palimpsest-0.6 +-- SPDX-License-Identifier: MPL-2.0 AND Palimpsest-0.6 -- -- Basic.agda - Simple proofs demonstrating fundamental logical principles -- diff --git a/proofs/hol4/arithmetic.sml b/proofs/hol4/arithmetic.sml index a9f28a67..d5badb14 100644 --- a/proofs/hol4/arithmetic.sml +++ b/proofs/hol4/arithmetic.sml @@ -1,5 +1,5 @@ (* SPDX-FileCopyrightText: 2025 ECHIDNA Project Team *) -(* SPDX-License-Identifier: MIT OR Palimpsest-0.6 *) +(* SPDX-License-Identifier: MPL-2.0 OR Palimpsest-0.6 *) (* Arithmetic properties in HOL4 *) (* Demonstrates decision procedures and automation *) diff --git a/proofs/hol4/binary_tree.sml b/proofs/hol4/binary_tree.sml index 91294e04..4de270de 100644 --- a/proofs/hol4/binary_tree.sml +++ b/proofs/hol4/binary_tree.sml @@ -1,5 +1,5 @@ (* SPDX-FileCopyrightText: 2025 ECHIDNA Project Team *) -(* SPDX-License-Identifier: MIT OR Palimpsest-0.6 *) +(* SPDX-License-Identifier: MPL-2.0 OR Palimpsest-0.6 *) (* Binary tree operations in HOL4 *) (* Demonstrates datatype definitions and structural induction *) diff --git a/proofs/hol4/list_append.sml b/proofs/hol4/list_append.sml index ac4c3b85..4f877161 100644 --- a/proofs/hol4/list_append.sml +++ b/proofs/hol4/list_append.sml @@ -1,5 +1,5 @@ (* SPDX-FileCopyrightText: 2025 ECHIDNA Project Team *) -(* SPDX-License-Identifier: MIT OR Palimpsest-0.6 *) +(* SPDX-License-Identifier: MPL-2.0 OR Palimpsest-0.6 *) (* List append properties in HOL4 *) (* Demonstrates inductive proofs over lists *) diff --git a/proofs/hol4/set_theory.sml b/proofs/hol4/set_theory.sml index aeb4d939..2c8eede6 100644 --- a/proofs/hol4/set_theory.sml +++ b/proofs/hol4/set_theory.sml @@ -1,5 +1,5 @@ (* SPDX-FileCopyrightText: 2025 ECHIDNA Project Team *) -(* SPDX-License-Identifier: MIT OR Palimpsest-0.6 *) +(* SPDX-License-Identifier: MPL-2.0 OR Palimpsest-0.6 *) (* Set theory properties in HOL4 *) (* Demonstrates higher-order reasoning *) diff --git a/proofs/hol4/sorting.sml b/proofs/hol4/sorting.sml index 188b5100..a81ce2fd 100644 --- a/proofs/hol4/sorting.sml +++ b/proofs/hol4/sorting.sml @@ -1,5 +1,5 @@ (* SPDX-FileCopyrightText: 2025 ECHIDNA Project Team *) -(* SPDX-License-Identifier: MIT OR Palimpsest-0.6 *) +(* SPDX-License-Identifier: MPL-2.0 OR Palimpsest-0.6 *) (* Sorting algorithm verification in HOL4 *) (* Demonstrates algorithm correctness proofs *) diff --git a/proofs/lean/Basic.lean b/proofs/lean/Basic.lean index 1ea009fb..c9337b75 100644 --- a/proofs/lean/Basic.lean +++ b/proofs/lean/Basic.lean @@ -1,6 +1,6 @@ /- SPDX-FileCopyrightText: 2025 ECHIDNA Project Team -SPDX-License-Identifier: MIT +SPDX-License-Identifier: MPL-2.0 Basic Lean 4 Proofs - Foundation Level diff --git a/proofs/lean/List.lean b/proofs/lean/List.lean index 279ae54d..e286d96e 100644 --- a/proofs/lean/List.lean +++ b/proofs/lean/List.lean @@ -1,6 +1,6 @@ /- SPDX-FileCopyrightText: 2025 ECHIDNA Project Team -SPDX-License-Identifier: MIT +SPDX-License-Identifier: MPL-2.0 List Proofs in Lean 4 diff --git a/proofs/lean/Propositional.lean b/proofs/lean/Propositional.lean index 14079a33..a6d85fff 100644 --- a/proofs/lean/Propositional.lean +++ b/proofs/lean/Propositional.lean @@ -1,6 +1,6 @@ /- SPDX-FileCopyrightText: 2025 ECHIDNA Project Team -SPDX-License-Identifier: MIT +SPDX-License-Identifier: MPL-2.0 Propositional Logic Proofs in Lean 4 diff --git a/proofs/lean/README.md b/proofs/lean/README.md index 71c2d1f9..aba26392 100644 --- a/proofs/lean/README.md +++ b/proofs/lean/README.md @@ -1,6 +1,6 @@ # ECHIDNA Lean 4 Proof Examples diff --git a/proofs/lean/THEOREMS.md b/proofs/lean/THEOREMS.md index 54a7d276..1bbd52e2 100644 --- a/proofs/lean/THEOREMS.md +++ b/proofs/lean/THEOREMS.md @@ -1,6 +1,6 @@ # ECHIDNA Lean 4 Theorems Reference diff --git a/proofs/pvs/arithmetic.pvs b/proofs/pvs/arithmetic.pvs index b94000f5..339885c9 100644 --- a/proofs/pvs/arithmetic.pvs +++ b/proofs/pvs/arithmetic.pvs @@ -1,5 +1,5 @@ % SPDX-FileCopyrightText: 2025 ECHIDNA Project Team -% SPDX-License-Identifier: MIT OR Palimpsest-0.6 +% SPDX-License-Identifier: MPL-2.0 OR Palimpsest-0.6 % Arithmetic properties % Demonstrates PVS's powerful decision procedures diff --git a/proofs/pvs/binary_search.pvs b/proofs/pvs/binary_search.pvs index fd7e804e..0cfdfca1 100644 --- a/proofs/pvs/binary_search.pvs +++ b/proofs/pvs/binary_search.pvs @@ -1,5 +1,5 @@ % SPDX-FileCopyrightText: 2025 ECHIDNA Project Team -% SPDX-License-Identifier: MIT OR Palimpsest-0.6 +% SPDX-License-Identifier: MPL-2.0 OR Palimpsest-0.6 % Binary search on sorted arrays % Demonstrates PVS's specification and verification capabilities diff --git a/proofs/pvs/list_theory.pvs b/proofs/pvs/list_theory.pvs index 57edefa9..9bc21488 100644 --- a/proofs/pvs/list_theory.pvs +++ b/proofs/pvs/list_theory.pvs @@ -1,5 +1,5 @@ % SPDX-FileCopyrightText: 2025 ECHIDNA Project Team -% SPDX-License-Identifier: MIT OR Palimpsest-0.6 +% SPDX-License-Identifier: MPL-2.0 OR Palimpsest-0.6 % List theory with append and length % Demonstrates PVS's dependent types and TCCs diff --git a/proofs/pvs/set_theory.pvs b/proofs/pvs/set_theory.pvs index e3a10674..5bffbebf 100644 --- a/proofs/pvs/set_theory.pvs +++ b/proofs/pvs/set_theory.pvs @@ -1,5 +1,5 @@ % SPDX-FileCopyrightText: 2025 ECHIDNA Project Team -% SPDX-License-Identifier: MIT OR Palimpsest-0.6 +% SPDX-License-Identifier: MPL-2.0 OR Palimpsest-0.6 % Set operations and properties % Demonstrates higher-order reasoning in PVS diff --git a/proofs/pvs/sorting.pvs b/proofs/pvs/sorting.pvs index 3c0a307d..f7b58488 100644 --- a/proofs/pvs/sorting.pvs +++ b/proofs/pvs/sorting.pvs @@ -1,5 +1,5 @@ % SPDX-FileCopyrightText: 2025 ECHIDNA Project Team -% SPDX-License-Identifier: MIT OR Palimpsest-0.6 +% SPDX-License-Identifier: MPL-2.0 OR Palimpsest-0.6 % Insertion sort specification and verification % Demonstrates algorithm correctness in PVS diff --git a/reports/audits/audit-ffi-boundary.md b/reports/audits/audit-ffi-boundary.md index e5d707b6..0bd637cf 100644 --- a/reports/audits/audit-ffi-boundary.md +++ b/reports/audits/audit-ffi-boundary.md @@ -1,5 +1,5 @@ diff --git a/reports/audits/audit-pa021-axioms-2026-05-26.md b/reports/audits/audit-pa021-axioms-2026-05-26.md index 745a64b4..d885e3f1 100644 --- a/reports/audits/audit-pa021-axioms-2026-05-26.md +++ b/reports/audits/audit-pa021-axioms-2026-05-26.md @@ -1,5 +1,5 @@ diff --git a/rules/security_learning.lgt b/rules/security_learning.lgt index 39ad9adc..02d00851 100644 --- a/rules/security_learning.lgt +++ b/rules/security_learning.lgt @@ -1,4 +1,4 @@ -%% SPDX-License-Identifier: MIT OR Palimpsest-0.6 +%% SPDX-License-Identifier: MPL-2.0 OR Palimpsest-0.6 %% ECHIDNA Security Rule Learning Module %% Learns security patterns from cicd-hyper-a audit data diff --git a/schemas/VERSIONING.md b/schemas/VERSIONING.md index c511c2b9..d5224ce8 100644 --- a/schemas/VERSIONING.md +++ b/schemas/VERSIONING.md @@ -1,5 +1,5 @@ diff --git a/scripts/build-production.sh b/scripts/build-production.sh index 49ca61d2..970c8266 100755 --- a/scripts/build-production.sh +++ b/scripts/build-production.sh @@ -1,5 +1,5 @@ #!/bin/bash -# SPDX-License-Identifier: MIT OR Palimpsest-0.6 +# SPDX-License-Identifier: MPL-2.0 OR Palimpsest-0.6 # Production build script for ECHIDNA set -e diff --git a/scripts/demo-proof.sh b/scripts/demo-proof.sh index fa8f9095..cbc2cdab 100755 --- a/scripts/demo-proof.sh +++ b/scripts/demo-proof.sh @@ -1,5 +1,5 @@ #!/bin/bash -# SPDX-License-Identifier: MIT OR Palimpsest-0.6 +# SPDX-License-Identifier: MPL-2.0 OR Palimpsest-0.6 # ECHIDNA Interactive Demo - Proof of Commutativity set -e diff --git a/scripts/expand_training_data.sh b/scripts/expand_training_data.sh index 2ed91522..ae70788f 100755 --- a/scripts/expand_training_data.sh +++ b/scripts/expand_training_data.sh @@ -1,5 +1,5 @@ #!/bin/bash -# SPDX-License-Identifier: MIT OR Palimpsest-0.6 +# SPDX-License-Identifier: MPL-2.0 OR Palimpsest-0.6 # Quick training data expansion script for ECHIDNA set -e diff --git a/scripts/test-integration.sh b/scripts/test-integration.sh index 451dee76..0d9dc180 100755 --- a/scripts/test-integration.sh +++ b/scripts/test-integration.sh @@ -1,6 +1,6 @@ #!/bin/bash # SPDX-FileCopyrightText: 2025 ECHIDNA Project Team -# SPDX-License-Identifier: MIT OR Palimpsest-0.6 +# SPDX-License-Identifier: MPL-2.0 OR Palimpsest-0.6 # Integration test runner for Rust↔Julia communication # Starts Julia test server, runs Rust integration tests, then stops server diff --git a/spark/README.adoc b/spark/README.adoc index d7416074..25dfa36e 100644 --- a/spark/README.adoc +++ b/spark/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 = SPARK Companions :toc: :toc-placement: preamble diff --git a/src/julia/README.md b/src/julia/README.md index 7c08b832..5bc753b1 100644 --- a/src/julia/README.md +++ b/src/julia/README.md @@ -1,5 +1,5 @@ # SPDX-FileCopyrightText: 2025 ECHIDNA Project Team -# SPDX-License-Identifier: MPL-2.0 +# SPDX-License-Identifier: CC-BY-SA-4.0 # ECHIDNA Julia ML Components @@ -496,7 +496,7 @@ See LICENSE files for details. diff --git a/src/julia/retrain_from_verisim.jl b/src/julia/retrain_from_verisim.jl index 9ee3c089..1e3903d3 100644 --- a/src/julia/retrain_from_verisim.jl +++ b/src/julia/retrain_from_verisim.jl @@ -1,4 +1,4 @@ -# SPDX-License-Identifier: EUPL-1.2 +# SPDX-License-Identifier: MPL-2.0 # SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) # # retrain_from_verisim.jl — Retrain ECHIDNA's logistic-regression premise diff --git a/src/julia/test_server.jl b/src/julia/test_server.jl index be3949f4..4f160844 100644 --- a/src/julia/test_server.jl +++ b/src/julia/test_server.jl @@ -1,5 +1,5 @@ # SPDX-FileCopyrightText: 2025 ECHIDNA Project Team -# SPDX-License-Identifier: MIT AND Palimpsest-0.6 +# SPDX-License-Identifier: MPL-2.0 AND Palimpsest-0.6 """ test_server.jl diff --git a/src/ui/tea/echidna_gui.affine b/src/ui/tea/echidna_gui.affine index 71a4b65a..9334e355 100644 --- a/src/ui/tea/echidna_gui.affine +++ b/src/ui/tea/echidna_gui.affine @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-License-Identifier: MPL-2.0 // Echidna GUI — AffineScript TEA Interface // Underpinned by Cadre Router (Affine Stack Implementation) // diff --git a/src/ui/tea/echidna_tea.js b/src/ui/tea/echidna_tea.js index f6fed2b7..73972847 100644 --- a/src/ui/tea/echidna_tea.js +++ b/src/ui/tea/echidna_tea.js @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: AGPL-3.0-or-later +// SPDX-License-Identifier: MPL-2.0 // Echidna GUI Bridge /** diff --git a/src/zig/ffi/echidna_ffi.h b/src/zig/ffi/echidna_ffi.h index bf75b2f5..500cafc9 100644 --- a/src/zig/ffi/echidna_ffi.h +++ b/src/zig/ffi/echidna_ffi.h @@ -1,5 +1,5 @@ // SPDX-FileCopyrightText: 2025 ECHIDNA Project Team -// SPDX-License-Identifier: MIT OR Palimpsest-0.6 +// SPDX-License-Identifier: MPL-2.0 OR Palimpsest-0.6 /** * @file echidna_ffi.h diff --git a/training_data/proof_states_v2.jsonl b/training_data/proof_states_v2.jsonl index e6031ad2..393f83b4 100644 --- a/training_data/proof_states_v2.jsonl +++ b/training_data/proof_states_v2.jsonl @@ -1,6 +1,6 @@ {"id":1,"prover":"PVS","goal":"fib(n: nat): RECURSIVE nat =","theorem":"n","file":"arithmetic.pvs"} {"id":2,"prover":"PVS","goal":"1: 1","theorem":"1","file":"arithmetic.pvs"} -{"id":3,"prover":"PVS","goal":"% SPDX-License-Identifier: MIT OR Palimpsest-0.6","theorem":"Identifier","file":"list_theory.pvs"} +{"id":3,"prover":"PVS","goal":"% SPDX-License-Identifier: MPL-2.0 OR Palimpsest-0.6","theorem":"Identifier","file":"list_theory.pvs"} {"id":4,"prover":"PVS","goal":"append(l1, l2: list): RECURSIVE list =","theorem":"l2","file":"list_theory.pvs"} {"id":5,"prover":"PVS","goal":"null: l2,","theorem":"null","file":"list_theory.pvs"} {"id":6,"prover":"PVS","goal":"length(l: list): RECURSIVE nat =","theorem":"l","file":"list_theory.pvs"} @@ -285,7 +285,7 @@ {"id":285,"prover":"Isabelle","goal":"Part of the ECHIDNA theorem proving platform","theorem":"proving","file":"List.thy"} {"id":286,"prover":"Isabelle","goal":"Part of the ECHIDNA theorem proving platform","theorem":"proving","file":"Nat.thy"} {"id":287,"prover":"Isabelle","goal":"Part of the ECHIDNA theorem proving platform","theorem":"proving","file":"Propositional.thy"} -{"id":288,"prover":"Agda","goal":"-- SPDX-License-Identifier: MIT AND Palimpsest-0.6","theorem":"Identifier","file":"Basic.agda"} +{"id":288,"prover":"Agda","goal":"-- SPDX-License-Identifier: MPL-2.0 AND Palimpsest-0.6","theorem":"Identifier","file":"Basic.agda"} {"id":289,"prover":"Agda","goal":"-- Type: A → A","theorem":"Type","file":"Basic.agda"} {"id":290,"prover":"Agda","goal":"suc : ℕ → ℕ","theorem":"suc","file":"Basic.agda"} {"id":291,"prover":"Agda","goal":"-- Modus ponens: if we have A → B and we have A, then we can derive B","theorem":"ponens","file":"Basic.agda"} @@ -293,7 +293,7 @@ {"id":293,"prover":"Agda","goal":"-- Example: if ⊤ → ⊤ and we have ⊤, we get ⊤","theorem":"Example","file":"Basic.agda"} {"id":294,"prover":"Agda","goal":"trans : {A B C : Set} → (A → B) → (B → C) → (A → C)","theorem":"trans","file":"Basic.agda"} {"id":295,"prover":"Agda","goal":"SKK : {A : Set} → (x : A) → S const const x ≡ id x","theorem":"SKK","file":"Basic.agda"} -{"id":296,"prover":"Agda","goal":"-- SPDX-License-Identifier: MIT AND Palimpsest-0.6","theorem":"Identifier","file":"List.agda"} +{"id":296,"prover":"Agda","goal":"-- SPDX-License-Identifier: MPL-2.0 AND Palimpsest-0.6","theorem":"Identifier","file":"List.agda"} {"id":297,"prover":"Agda","goal":"filter : {A : Set} → (A → Bool) → List A → List A","theorem":"filter","file":"List.agda"} {"id":298,"prover":"Agda","goal":"reverse : {A : Set} → List A → List A","theorem":"reverse","file":"List.agda"} {"id":299,"prover":"Agda","goal":"reverse′ : {A : Set} → List A → List A","theorem":"A","file":"List.agda"} @@ -313,7 +313,7 @@ {"id":313,"prover":"Agda","goal":"length-foldr : {A : Set} → (xs : List A)","theorem":"foldr","file":"List.agda"} {"id":314,"prover":"Agda","goal":"there : {x : A} {xs : List A} → Any P xs → Any P (x ∷ xs)","theorem":"there","file":"List.agda"} {"id":315,"prover":"Agda","goal":"Any-++ : {A : Set} {P : A → Set} {xs ys : List A}","theorem":"A","file":"List.agda"} -{"id":316,"prover":"Agda","goal":"-- SPDX-License-Identifier: MIT AND Palimpsest-0.6","theorem":"Identifier","file":"Nat.agda"} +{"id":316,"prover":"Agda","goal":"-- SPDX-License-Identifier: MPL-2.0 AND Palimpsest-0.6","theorem":"Identifier","file":"Nat.agda"} {"id":317,"prover":"Agda","goal":"subst : {A : Set} {x y : A} → (P : A → Set) → x ≡ y → P x → P y","theorem":"subst","file":"Nat.agda"} {"id":318,"prover":"Agda","goal":"_+_ : ℕ → ℕ → ℕ","theorem":"_","file":"Nat.agda"} {"id":319,"prover":"Agda","goal":"+-zero : (n : ℕ) → n + zero ≡ n","theorem":"zero","file":"Nat.agda"} @@ -324,7 +324,7 @@ {"id":324,"prover":"Agda","goal":"s≤s : {m n : ℕ} → m ≤ n → suc m ≤ suc n","theorem":"s","file":"Nat.agda"} {"id":325,"prover":"Agda","goal":"min-comm : (m n : ℕ) → min m n ≡ min n m","theorem":"comm","file":"Nat.agda"} {"id":326,"prover":"Agda","goal":"even-or-odd : (n : ℕ) → Even n ⊎ Odd n","theorem":"odd","file":"Nat.agda"} -{"id":327,"prover":"Agda","goal":"-- SPDX-License-Identifier: MIT AND Palimpsest-0.6","theorem":"Identifier","file":"Propositional.agda"} +{"id":327,"prover":"Agda","goal":"-- SPDX-License-Identifier: MPL-2.0 AND Palimpsest-0.6","theorem":"Identifier","file":"Propositional.agda"} {"id":328,"prover":"Agda","goal":"tt : ⊤","theorem":"tt","file":"Propositional.agda"} {"id":329,"prover":"Agda","goal":"-- Ex falso quodlibet: from falsehood, anything follows","theorem":"quodlibet","file":"Propositional.agda"} {"id":330,"prover":"Agda","goal":"de-morgan₂-iff : {A B : Set} → ¬ (A ∨ B) ⇔ (¬ A ∧ ¬ B)","theorem":"iff","file":"Propositional.agda"}