From a1c7c573b4045747e21350fa6bab7205e0571b0d Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Fri, 9 Oct 2026 00:27:14 +0100 Subject: [PATCH 1/2] chore(licence): MPL-2.0 for code, CC-BY-SA-4.0 for prose MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Owner ruling 2026-10-09: "mpl-2.0 code, and cc-by-sa-4.0 prose". Applies docs/migrations/pmpl-to-mpl-sweep-runbook.adoc §5/§6 (standards) per file. SPDX header PMPL-1.0-or-later -> MPL-2.0 (18 code/config files): container/compose.example.toml container/compose.toml container/Containerfile container/ct-build.sh container/deploy.k9.ncl container/entrypoint.sh container/.gatekeeper.yaml container/manifest.toml container/vordr.toml contractile.just .devcontainer/Containerfile .devcontainer/devcontainer.json features/ssg/ssg-bootstrap.sh .gitlab-ci.yml Justfile .machine_readable/contractiles/Justfile .pre-commit-config.yaml scripts/validate-template.sh SPDX header MPL-2.0 -> CC-BY-SA-4.0 (30 prose files): AUDIT.adoc .claude/CLAUDE.md container/README.adoc .devcontainer/README.adoc EXPLAINME.adoc features/boj-server/README.adoc features/panic-attacker/README.adoc features/README.adoc features/ssg/README.adoc .machine_readable/README.adoc MAINTAINERS.adoc ROADMAP.adoc src/aspects/integrity/README.adoc src/aspects/observability/README.adoc src/aspects/README.adoc src/aspects/security/README.adoc src/contracts/README.adoc src/definitions/README.adoc src/errors/README.adoc src/interface/Abi/README.adoc src/interface/ffi/README.adoc src/interface/ffi/src/README.adoc src/interface/ffi/test/README.adoc src/interface/generated/abi/README.adoc src/interface/generated/README.adoc src/interface/README.adoc src/README.adoc TEMPLATE-STANDARDS-AUDIT.adoc tools/invariant-path/README.adoc www/.well-known/README.adoc New CC-BY-SA-4.0 header (16 unlabelled .adoc files): .claude/PROJECT.adoc ARCHITECTURE.adoc CHANGELOG.adoc GOVERNANCE.adoc PROOF-NEEDS.adoc PROOF-STATUS.adoc READINESS.adoc README.adoc SECURITY.adoc TEST-NEEDS.adoc TOPOLOGY.adoc docs/reports/audit/audit-2026-04-15-post.adoc docs/tech-debt-2026-05-26.adoc llm-warmup-dev.adoc llm-warmup-user.adoc session/README.adoc New MPL-2.0 header (4 unlabelled shell scripts): .machine_readable/scripts/forge/git-cleanup.sh scripts/invariant-path.sh session/dispatch.sh session/local-hooks.sh Licence rule text updated to the two-tier rule: .github/copilot-instructions.md .github/GOVERNANCE.md .github/pull_request_template.md .machine_readable/ai/{.clinerules,.cursorrules,.windsurfrules,PLACEHOLDERS.adoc} .machine_readable/compliance/reuse/dep5 (prose stanza added; .a2ml stanza kept to match those headers) Justfile, .machine_readable/contractiles/Justfile ({{LICENSE}} -> MPL-2.0) QUICKSTART-MAINTAINER.adoc TEST-NEEDS.adoc docs/practice/AI-CONVENTIONS.adoc llm-warmup-dev.adoc llm-warmup-user.adoc stapeln.toml docs/attribution/CITATION.cff docs/attribution/CITATIONS.adoc www/.well-known/ai.txt (PMPL "Emotional Lineage" line removed) www/.well-known/humans.txt Removed tracked duplicates (31 files; every difference was a licence header): www/.well-known/.well-known/ (3) verification/verification/ (28; its README title and copyright line moved into verification/README.adoc) Kept, deliberately: - every .a2ml header (A2ML is retired; the deed migration owns them) - .machine_readable/.machine_readable/ (nested copy; owner decision pending) - docs/legal/EXHIBIT-{A,B}-*.txt (licence exhibit text) - www/.well-known/{ai,humans,security}.txt stay MPL-2.0 (machine-read data) - CODE_OF_CONDUCT.adoc (adapted from the Contributor Covenant; not relabelled) - LICENSE, LICENSES/, .machine_readable/compliance/rust/deny.toml - history: docs/tech-debt-2026-05-26.adoc body, docs/decisions/0001-*, docs/STATE-VISUALIZER.adoc, docs/RSR_OUTLINE.adoc - k9 example bodies, contractile.just:65, Justfile:224/:1057 (licence-file tooling) Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01GpUzjdhWFi26k6s7AWxYcf --- .claude/CLAUDE.md | 2 +- .claude/PROJECT.adoc | 1 + .devcontainer/Containerfile | 2 +- .devcontainer/README.adoc | 2 +- .devcontainer/devcontainer.json | 2 +- .github/GOVERNANCE.md | 2 +- .github/copilot-instructions.md | 2 +- .github/pull_request_template.md | 2 +- .gitlab-ci.yml | 2 +- .machine_readable/README.adoc | 2 +- .machine_readable/ai/.clinerules | 4 +- .machine_readable/ai/.cursorrules | 4 +- .machine_readable/ai/.windsurfrules | 4 +- .machine_readable/ai/PLACEHOLDERS.adoc | 2 +- .machine_readable/compliance/reuse/dep5 | 27 +++--- .machine_readable/contractiles/Justfile | 4 +- .../scripts/forge/git-cleanup.sh | 1 + .pre-commit-config.yaml | 2 +- ARCHITECTURE.adoc | 1 + AUDIT.adoc | 2 +- CHANGELOG.adoc | 1 + EXPLAINME.adoc | 2 +- GOVERNANCE.adoc | 1 + Justfile | 4 +- MAINTAINERS.adoc | 2 +- PROOF-NEEDS.adoc | 1 + PROOF-STATUS.adoc | 1 + QUICKSTART-MAINTAINER.adoc | 2 +- READINESS.adoc | 1 + README.adoc | 1 + ROADMAP.adoc | 2 +- SECURITY.adoc | 1 + TEMPLATE-STANDARDS-AUDIT.adoc | 2 +- TEST-NEEDS.adoc | 3 +- TOPOLOGY.adoc | 1 + container/.gatekeeper.yaml | 2 +- container/Containerfile | 2 +- container/README.adoc | 2 +- container/compose.example.toml | 2 +- container/compose.toml | 2 +- container/ct-build.sh | 2 +- container/deploy.k9.ncl | 2 +- container/entrypoint.sh | 2 +- container/manifest.toml | 2 +- container/vordr.toml | 2 +- contractile.just | 2 +- docs/attribution/CITATION.cff | 2 +- docs/attribution/CITATIONS.adoc | 2 +- docs/practice/AI-CONVENTIONS.adoc | 6 +- docs/reports/audit/audit-2026-04-15-post.adoc | 1 + docs/tech-debt-2026-05-26.adoc | 1 + features/README.adoc | 2 +- features/boj-server/README.adoc | 2 +- features/panic-attacker/README.adoc | 2 +- features/ssg/README.adoc | 2 +- features/ssg/ssg-bootstrap.sh | 2 +- llm-warmup-dev.adoc | 3 +- llm-warmup-user.adoc | 3 +- scripts/invariant-path.sh | 1 + scripts/validate-template.sh | 2 +- session/README.adoc | 1 + session/dispatch.sh | 1 + session/local-hooks.sh | 1 + src/README.adoc | 2 +- src/aspects/README.adoc | 2 +- src/aspects/integrity/README.adoc | 2 +- src/aspects/observability/README.adoc | 2 +- src/aspects/security/README.adoc | 2 +- src/contracts/README.adoc | 2 +- src/definitions/README.adoc | 2 +- src/errors/README.adoc | 2 +- src/interface/Abi/README.adoc | 2 +- src/interface/README.adoc | 2 +- src/interface/ffi/README.adoc | 2 +- src/interface/ffi/src/README.adoc | 2 +- src/interface/ffi/test/README.adoc | 2 +- src/interface/generated/README.adoc | 2 +- src/interface/generated/abi/README.adoc | 2 +- stapeln.toml | 2 +- tools/invariant-path/README.adoc | 2 +- verification/README.adoc | 7 +- .../verification/0.1-AI-MANIFEST.a2ml | 27 ------ verification/verification/README.adoc | 3 - .../benchmarks/0.2-AI-MANIFEST.a2ml | 11 --- .../verification/benchmarks/README.adoc | 3 - .../coverage/0.2-AI-MANIFEST.a2ml | 12 --- .../verification/coverage/README.adoc | 3 - .../verification/fuzzing/0.2-AI-MANIFEST.a2ml | 11 --- verification/verification/fuzzing/README.adoc | 3 - .../verification/proofs/0.2-AI-MANIFEST.a2ml | 11 --- verification/verification/proofs/README.adoc | 60 ------------ .../verification/proofs/agda/Properties.agda | 37 -------- .../verification/proofs/coq/TypeSafety.v | 73 --------------- .../proofs/idris2/ABI/Compliance.idr | 41 --------- .../proofs/idris2/ABI/Foreign.idr | 53 ----------- .../verification/proofs/idris2/ABI/Layout.idr | 63 ------------- .../proofs/idris2/ABI/Platform.idr | 63 ------------- .../proofs/idris2/ABI/Pointers.idr | 52 ----------- .../verification/proofs/idris2/Types.idr | 38 -------- .../verification/proofs/lean4/ApiTypes.lean | 44 --------- .../proofs/tlaplus/StateMachine.tla | 91 ------------------- .../safety_case/0.2-AI-MANIFEST.a2ml | 12 --- .../verification/safety_case/README.adoc | 3 - .../simulations/0.2-AI-MANIFEST.a2ml | 11 --- .../verification/simulations/README.adoc | 3 - .../verification/tests/0.2-AI-MANIFEST.a2ml | 1 - verification/verification/tests/README.adoc | 3 - .../traceability/0.2-AI-MANIFEST.a2ml | 12 --- .../verification/traceability/README.adoc | 3 - www/.well-known/.well-known/ai.txt | 18 ---- www/.well-known/.well-known/humans.txt | 14 --- www/.well-known/.well-known/security.txt | 11 --- www/.well-known/README.adoc | 2 +- www/.well-known/ai.txt | 3 +- www/.well-known/humans.txt | 2 +- 115 files changed, 113 insertions(+), 876 deletions(-) delete mode 100644 verification/verification/0.1-AI-MANIFEST.a2ml delete mode 100644 verification/verification/README.adoc delete mode 100644 verification/verification/benchmarks/0.2-AI-MANIFEST.a2ml delete mode 100644 verification/verification/benchmarks/README.adoc delete mode 100644 verification/verification/coverage/0.2-AI-MANIFEST.a2ml delete mode 100644 verification/verification/coverage/README.adoc delete mode 100644 verification/verification/fuzzing/0.2-AI-MANIFEST.a2ml delete mode 100644 verification/verification/fuzzing/README.adoc delete mode 100644 verification/verification/proofs/0.2-AI-MANIFEST.a2ml delete mode 100644 verification/verification/proofs/README.adoc delete mode 100644 verification/verification/proofs/agda/Properties.agda delete mode 100644 verification/verification/proofs/coq/TypeSafety.v delete mode 100644 verification/verification/proofs/idris2/ABI/Compliance.idr delete mode 100644 verification/verification/proofs/idris2/ABI/Foreign.idr delete mode 100644 verification/verification/proofs/idris2/ABI/Layout.idr delete mode 100644 verification/verification/proofs/idris2/ABI/Platform.idr delete mode 100644 verification/verification/proofs/idris2/ABI/Pointers.idr delete mode 100644 verification/verification/proofs/idris2/Types.idr delete mode 100644 verification/verification/proofs/lean4/ApiTypes.lean delete mode 100644 verification/verification/proofs/tlaplus/StateMachine.tla delete mode 100644 verification/verification/safety_case/0.2-AI-MANIFEST.a2ml delete mode 100644 verification/verification/safety_case/README.adoc delete mode 100644 verification/verification/simulations/0.2-AI-MANIFEST.a2ml delete mode 100644 verification/verification/simulations/README.adoc delete mode 100644 verification/verification/tests/0.2-AI-MANIFEST.a2ml delete mode 100644 verification/verification/tests/README.adoc delete mode 100644 verification/verification/traceability/0.2-AI-MANIFEST.a2ml delete mode 100644 verification/verification/traceability/README.adoc delete mode 100644 www/.well-known/.well-known/ai.txt delete mode 100644 www/.well-known/.well-known/humans.txt delete mode 100644 www/.well-known/.well-known/security.txt diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md index e25b8ac..ec75f13 100644 --- a/.claude/CLAUDE.md +++ b/.claude/CLAUDE.md @@ -1,5 +1,5 @@ # CLAUDE.md - AI Assistant Instructions diff --git a/.claude/PROJECT.adoc b/.claude/PROJECT.adoc index 379e40d..e06e6a4 100644 --- a/.claude/PROJECT.adoc +++ b/.claude/PROJECT.adoc @@ -1,3 +1,4 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 == Jaffascript - Claude Code Instructions This repository contains the Jaffascript project. diff --git a/.devcontainer/Containerfile b/.devcontainer/Containerfile index d9a54f6..b0a6fd1 100644 --- a/.devcontainer/Containerfile +++ b/.devcontainer/Containerfile @@ -1,4 +1,4 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later +# SPDX-License-Identifier: MPL-2.0 # Copyright (c) {{CURRENT_YEAR}} {{AUTHOR}} ({{OWNER}}) <{{AUTHOR_EMAIL}}> # # Dev Container image for {{PROJECT_NAME}} diff --git a/.devcontainer/README.adoc b/.devcontainer/README.adoc index 04377b3..848e64d 100644 --- a/.devcontainer/README.adoc +++ b/.devcontainer/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell = Dev Container Usage :author: Jonathan D.A. Jewell diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json index 4ad379e..77de100 100644 --- a/.devcontainer/devcontainer.json +++ b/.devcontainer/devcontainer.json @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: PMPL-1.0-or-later +// SPDX-License-Identifier: MPL-2.0 // Copyright (c) {{CURRENT_YEAR}} Jonathan D.A. Jewell (hyperpolymath) // // Dev Container configuration for {{PROJECT_NAME}} diff --git a/.github/GOVERNANCE.md b/.github/GOVERNANCE.md index 43c16ea..5270c8b 100644 --- a/.github/GOVERNANCE.md +++ b/.github/GOVERNANCE.md @@ -157,4 +157,4 @@ with the community before adoption, even though the BDFL retains final authority --- -Copyright (c) {{CURRENT_YEAR}} hyperpolymath. Licensed under PMPL-1.0-or-later. +Copyright (c) {{CURRENT_YEAR}} hyperpolymath. Licensed under CC-BY-SA-4.0. diff --git a/.github/copilot-instructions.md b/.github/copilot-instructions.md index 01eebc4..eb05fcc 100644 --- a/.github/copilot-instructions.md +++ b/.github/copilot-instructions.md @@ -14,7 +14,7 @@ Copyright (c) Jonathan D.A. Jewell ## License -- SPDX: `PMPL-1.0-or-later` on all new files. +- SPDX: `MPL-2.0` on code, `CC-BY-SA-4.0` on prose (`.adoc`, `.md`, docs), on all new files. - Never use AGPL-3.0. - Copyright: `Jonathan D.A. Jewell (hyperpolymath) ` diff --git a/.github/pull_request_template.md b/.github/pull_request_template.md index 2ff95ee..5c32b02 100644 --- a/.github/pull_request_template.md +++ b/.github/pull_request_template.md @@ -35,7 +35,7 @@ Copyright (c) Jonathan D.A. Jewell - [ ] Documentation updated for user-facing changes - [ ] `TOPOLOGY.md` updated (if architecture changed) - [ ] `CHANGELOG` or release notes updated -- [ ] New dependencies reviewed for license compatibility (PMPL-1.0-or-later / MPL-2.0) +- [ ] New dependencies reviewed for license compatibility (code MPL-2.0 / prose CC-BY-SA-4.0) - [ ] ABI/FFI changes validated (`src/interface/abi/` and `src/interface/ffi/` consistent) ## Testing diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index e00028b..b08314a 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -1,4 +1,4 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later +# SPDX-License-Identifier: MPL-2.0 # Primary CI/CD - GitLab is the source of truth stages: diff --git a/.machine_readable/README.adoc b/.machine_readable/README.adoc index 34f152c..da5a8a5 100644 --- a/.machine_readable/README.adoc +++ b/.machine_readable/README.adoc @@ -1,3 +1,3 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Machine-readable metadata and configuration for RSR compliance. // See: https://github.com/hyperpolymath/rsr-template-repo diff --git a/.machine_readable/ai/.clinerules b/.machine_readable/ai/.clinerules index 854d2ee..f9ec408 100644 --- a/.machine_readable/ai/.clinerules +++ b/.machine_readable/ai/.clinerules @@ -5,8 +5,8 @@ # STARTUP: Read 0-AI-MANIFEST.a2ml first, then .machine_readable/STATE.a2ml. # LICENSE -# All original code: PMPL-1.0-or-later. -# Never AGPL-3.0. MPL-2.0 only as platform-required fallback. +# Original code: MPL-2.0. Prose (.adoc, .md, docs): CC-BY-SA-4.0. +# Never AGPL-3.0. # SPDX header required on every source file. # Copyright: {{AUTHOR}} ({{OWNER}}) <{{AUTHOR_EMAIL}}> diff --git a/.machine_readable/ai/.cursorrules b/.machine_readable/ai/.cursorrules index d3b9cee..abfca22 100644 --- a/.machine_readable/ai/.cursorrules +++ b/.machine_readable/ai/.cursorrules @@ -5,8 +5,8 @@ # Read 0-AI-MANIFEST.a2ml in the repo root FIRST for canonical file locations. # LICENSE -# All original code: PMPL-1.0-or-later (SPDX header required on every file). -# Never use AGPL-3.0. Fallback to MPL-2.0 only when platform requires it. +# Original code: MPL-2.0. Prose (.adoc, .md, docs): CC-BY-SA-4.0. SPDX header required on every file. +# Never use AGPL-3.0. # Copyright: {{AUTHOR}} ({{OWNER}}) <{{AUTHOR_EMAIL}}> # STATE FILES diff --git a/.machine_readable/ai/.windsurfrules b/.machine_readable/ai/.windsurfrules index 854d2ee..f9ec408 100644 --- a/.machine_readable/ai/.windsurfrules +++ b/.machine_readable/ai/.windsurfrules @@ -5,8 +5,8 @@ # STARTUP: Read 0-AI-MANIFEST.a2ml first, then .machine_readable/STATE.a2ml. # LICENSE -# All original code: PMPL-1.0-or-later. -# Never AGPL-3.0. MPL-2.0 only as platform-required fallback. +# Original code: MPL-2.0. Prose (.adoc, .md, docs): CC-BY-SA-4.0. +# Never AGPL-3.0. # SPDX header required on every source file. # Copyright: {{AUTHOR}} ({{OWNER}}) <{{AUTHOR_EMAIL}}> diff --git a/.machine_readable/ai/PLACEHOLDERS.adoc b/.machine_readable/ai/PLACEHOLDERS.adoc index 677546e..5277a8c 100644 --- a/.machine_readable/ai/PLACEHOLDERS.adoc +++ b/.machine_readable/ai/PLACEHOLDERS.adoc @@ -88,7 +88,7 @@ sed -i "s/{{CURRENT_DATE}}/$(date +%Y-%m-%d)/g" $(grep -rl '{{CURRENT_DATE}}' .) | Placeholder | Description | Example | Files | |---|---|---|---| -| `{{LICENSE}}` | License name | `PMPL-1.0-or-later` | ABI-FFI-README.md | +| `{{LICENSE}}` | License name | `MPL-2.0` | ABI-FFI-README.md | | `{{PROJECT_PURPOSE}}` | One-line project description | `FFI bridges between languages` | STATE.a2ml | ### AI Manifest diff --git a/.machine_readable/compliance/reuse/dep5 b/.machine_readable/compliance/reuse/dep5 index 10e50c2..2bbc4d4 100644 --- a/.machine_readable/compliance/reuse/dep5 +++ b/.machine_readable/compliance/reuse/dep5 @@ -3,17 +3,17 @@ Upstream-Name: {{PROJECT_NAME}} Upstream-Contact: {{AUTHOR}} <{{AUTHOR_EMAIL}}> Source: https://github.com/{{OWNER}}/{{REPO}} -# Default: all files are PMPL-1.0-or-later +# Default: code is MPL-2.0. Prose is CC-BY-SA-4.0 (last stanza; the last match wins). Files: * Copyright: {{CURRENT_YEAR}} {{AUTHOR}} ({{OWNER}}) <{{AUTHOR_EMAIL}}> -License: PMPL-1.0-or-later +License: MPL-2.0 # Configuration files that cannot carry headers Files: .editorconfig .gitignore .gitattributes .tool-versions .mailmap Copyright: {{CURRENT_YEAR}} {{AUTHOR}} ({{OWNER}}) <{{AUTHOR_EMAIL}}> -License: PMPL-1.0-or-later +License: MPL-2.0 -# Machine-readable state files +# Machine-readable state files. The .a2ml headers stay PMPL until the deed migration; this stanza matches them. Files: .machine_readable/*.a2ml Copyright: {{CURRENT_YEAR}} {{AUTHOR}} ({{OWNER}}) <{{AUTHOR_EMAIL}}> License: PMPL-1.0-or-later @@ -21,34 +21,39 @@ License: PMPL-1.0-or-later # Bot directives Files: .machine_readable/bot_directives/* Copyright: {{CURRENT_YEAR}} {{AUTHOR}} ({{OWNER}}) <{{AUTHOR_EMAIL}}> -License: PMPL-1.0-or-later +License: MPL-2.0 # Contractiles Files: .machine_readable/contractiles/* Copyright: {{CURRENT_YEAR}} {{AUTHOR}} ({{OWNER}}) <{{AUTHOR_EMAIL}}> -License: PMPL-1.0-or-later +License: MPL-2.0 # GitHub/CI configuration Files: .github/* .github/**/* Copyright: {{CURRENT_YEAR}} {{AUTHOR}} ({{OWNER}}) <{{AUTHOR_EMAIL}}> -License: PMPL-1.0-or-later +License: MPL-2.0 # Generated files Files: generated/* Copyright: {{CURRENT_YEAR}} {{AUTHOR}} ({{OWNER}}) <{{AUTHOR_EMAIL}}> -License: PMPL-1.0-or-later +License: MPL-2.0 # Lockfiles and auto-generated Files: *.lock Cargo.lock flake.lock Copyright: {{CURRENT_YEAR}} {{AUTHOR}} ({{OWNER}}) <{{AUTHOR_EMAIL}}> -License: PMPL-1.0-or-later +License: MPL-2.0 # Devcontainer config (JSON, no comments) Files: .devcontainer/*.json Copyright: {{CURRENT_YEAR}} {{AUTHOR}} ({{OWNER}}) <{{AUTHOR_EMAIL}}> -License: PMPL-1.0-or-later +License: MPL-2.0 # Git-cliff config Files: cliff.toml Copyright: {{CURRENT_YEAR}} {{AUTHOR}} ({{OWNER}}) <{{AUTHOR_EMAIL}}> -License: PMPL-1.0-or-later +License: MPL-2.0 + +# Prose +Files: *.adoc *.md +Copyright: {{CURRENT_YEAR}} {{AUTHOR}} ({{OWNER}}) <{{AUTHOR_EMAIL}}> +License: CC-BY-SA-4.0 diff --git a/.machine_readable/contractiles/Justfile b/.machine_readable/contractiles/Justfile index 197f61b..bc86a12 100644 --- a/.machine_readable/contractiles/Justfile +++ b/.machine_readable/contractiles/Justfile @@ -1,4 +1,4 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later +# SPDX-License-Identifier: MPL-2.0 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) # # RSR Standard Justfile Template @@ -201,7 +201,7 @@ init: -e "s|${LB}DATE${RB}|${CURRENT_DATE}|g" -e "s|${LB}SECURITY_EMAIL${RB}|${SECURITY_EMAIL}|g" -e "s|${LB}CONDUCT_EMAIL${RB}|${CONDUCT_EMAIL}|g" - -e "s|${LB}LICENSE${RB}|PMPL-1.0-or-later|g" + -e "s|${LB}LICENSE${RB}|MPL-2.0|g" -e "s|${LB}CONDUCT_TEAM${RB}|Code of Conduct Committee|g" -e "s|${LB}RESPONSE_TIME${RB}|48 hours|g" -e "s|${LB}MAIN_BRANCH${RB}|main|g" diff --git a/.machine_readable/scripts/forge/git-cleanup.sh b/.machine_readable/scripts/forge/git-cleanup.sh index 4fec1a2..c8303ad 100755 --- a/.machine_readable/scripts/forge/git-cleanup.sh +++ b/.machine_readable/scripts/forge/git-cleanup.sh @@ -1,4 +1,5 @@ #!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 # git-cleanup.sh — Repository hygiene script set -euo pipefail echo "Cleaning up merged branches..." diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml index 6a93de7..b048d1c 100644 --- a/.pre-commit-config.yaml +++ b/.pre-commit-config.yaml @@ -1,4 +1,4 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later +# SPDX-License-Identifier: MPL-2.0 # Pre-commit hooks for hyperpolymath RSR repos. # Install: pip install pre-commit && pre-commit install # Run manually: pre-commit run --all-files diff --git a/ARCHITECTURE.adoc b/ARCHITECTURE.adoc index 1c0a7a6..b50914e 100644 --- a/ARCHITECTURE.adoc +++ b/ARCHITECTURE.adoc @@ -1,3 +1,4 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 == Architecture === Overview diff --git a/AUDIT.adoc b/AUDIT.adoc index 0f4f5ac..d4363c5 100644 --- a/AUDIT.adoc +++ b/AUDIT.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell = Audit Gate Codex diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 0051cb5..571a336 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -1,3 +1,4 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 == Changelog for jaffascript All changes are tracked in the main AffineScript repository. This is a diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index fcade57..46a2b9c 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell // SPDX-FileCopyrightText: 2024-2026 Jonathan D.A. Jewell (hyperpolymath) = JaffaScript - Face Repository diff --git a/GOVERNANCE.adoc b/GOVERNANCE.adoc index 9b836fb..db14743 100644 --- a/GOVERNANCE.adoc +++ b/GOVERNANCE.adoc @@ -1,3 +1,4 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 == Governance === Overview diff --git a/Justfile b/Justfile index 197f61b..bc86a12 100644 --- a/Justfile +++ b/Justfile @@ -1,4 +1,4 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later +# SPDX-License-Identifier: MPL-2.0 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) # # RSR Standard Justfile Template @@ -201,7 +201,7 @@ init: -e "s|${LB}DATE${RB}|${CURRENT_DATE}|g" -e "s|${LB}SECURITY_EMAIL${RB}|${SECURITY_EMAIL}|g" -e "s|${LB}CONDUCT_EMAIL${RB}|${CONDUCT_EMAIL}|g" - -e "s|${LB}LICENSE${RB}|PMPL-1.0-or-later|g" + -e "s|${LB}LICENSE${RB}|MPL-2.0|g" -e "s|${LB}CONDUCT_TEAM${RB}|Code of Conduct Committee|g" -e "s|${LB}RESPONSE_TIME${RB}|48 hours|g" -e "s|${LB}MAIN_BRANCH${RB}|main|g" diff --git a/MAINTAINERS.adoc b/MAINTAINERS.adoc index 9910dd8..daf8a78 100644 --- a/MAINTAINERS.adoc +++ b/MAINTAINERS.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 = Maintainers :toc: preamble diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index ba4f03b..63a67e4 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -1,3 +1,4 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 == Proof Requirements — \{\{PROJECT}} === Proof Tier diff --git a/PROOF-STATUS.adoc b/PROOF-STATUS.adoc index 2f531bd..7eaab87 100644 --- a/PROOF-STATUS.adoc +++ b/PROOF-STATUS.adoc @@ -1,3 +1,4 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 == Proof Status — \{\{PROJECT}} === Summary diff --git a/QUICKSTART-MAINTAINER.adoc b/QUICKSTART-MAINTAINER.adoc index 1347c83..11f4de0 100644 --- a/QUICKSTART-MAINTAINER.adoc +++ b/QUICKSTART-MAINTAINER.adoc @@ -107,7 +107,7 @@ Or via OPSM: `opsm update {{PACKAGE_NAME}}` == Security Notes -* License: PMPL-1.0-or-later (Palimpsest License) +* License: MPL-2.0 for code, CC-BY-SA-4.0 for prose * All dependencies SHA-pinned * `panic-attacker` scan results: link:INSTALL-SECURITY-REPORT.adoc[] * OpenSSF Scorecard: see badge in README diff --git a/READINESS.adoc b/READINESS.adoc index 4962c9a..1c355cb 100644 --- a/READINESS.adoc +++ b/READINESS.adoc @@ -1,3 +1,4 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 == rattlescript Component Readiness Assessment *Standard:* diff --git a/README.adoc b/README.adoc index 4f5ef81..94a1085 100644 --- a/README.adoc +++ b/README.adoc @@ -1,3 +1,4 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 https://opensource.org/licenses/MPL-2.0[image:https://img.shields.io/badge/License-MPL_2.0-blue.svg[License: MPL-2.0]] diff --git a/ROADMAP.adoc b/ROADMAP.adoc index 46484c5..06acef1 100644 --- a/ROADMAP.adoc +++ b/ROADMAP.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell // SPDX-FileCopyrightText: 2024-2026 Jonathan D.A. Jewell (hyperpolymath) = Jaffascript Roadmap diff --git a/SECURITY.adoc b/SECURITY.adoc index e47fdd9..390c456 100644 --- a/SECURITY.adoc +++ b/SECURITY.adoc @@ -1,3 +1,4 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 == Security Policy === Reporting a Vulnerability diff --git a/TEMPLATE-STANDARDS-AUDIT.adoc b/TEMPLATE-STANDARDS-AUDIT.adoc index edd8c2c..3d1d551 100644 --- a/TEMPLATE-STANDARDS-AUDIT.adoc +++ b/TEMPLATE-STANDARDS-AUDIT.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell = Template Standards Audit Codex diff --git a/TEST-NEEDS.adoc b/TEST-NEEDS.adoc index 167becf..6b8731a 100644 --- a/TEST-NEEDS.adoc +++ b/TEST-NEEDS.adoc @@ -1,3 +1,4 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 == TEST-NEEDS: rsr-template-repo === CRG Grade: C — ACHIEVED 2026-04-04 @@ -114,7 +115,7 @@ validation, benchmarks) documentation * *Author Attribution*: Jonathan D.A. Jewell 6759885+hyperpolymath@users.noreply.github.com -* *License*: PMPL-1.0-or-later on all new files +* *License*: MPL-2.0 (code) or CC-BY-SA-4.0 (prose) on all new files * *Automation*: All scripts executable + working === FLAGGED ISSUES - ALL RESOLVED diff --git a/TOPOLOGY.adoc b/TOPOLOGY.adoc index a975f58..79830cc 100644 --- a/TOPOLOGY.adoc +++ b/TOPOLOGY.adoc @@ -1,3 +1,4 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 == Architecture Topology === System Overview diff --git a/container/.gatekeeper.yaml b/container/.gatekeeper.yaml index cffda23..4aac671 100644 --- a/container/.gatekeeper.yaml +++ b/container/.gatekeeper.yaml @@ -1,4 +1,4 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later +# SPDX-License-Identifier: MPL-2.0 # # Svalinn gatekeeper policy for {{PROJECT_NAME}} # diff --git a/container/Containerfile b/container/Containerfile index efcafa2..ba85260 100644 --- a/container/Containerfile +++ b/container/Containerfile @@ -1,4 +1,4 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later +# SPDX-License-Identifier: MPL-2.0 # {{PROJECT_NAME}} Container Image # # Multi-stage build template for Chainguard Wolfi base images. diff --git a/container/README.adoc b/container/README.adoc index 0db8201..78275d2 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 // Copyright (c) Jonathan D.A. Jewell = {{PROJECT_NAME}} Container Templates :toc: left diff --git a/container/compose.example.toml b/container/compose.example.toml index 4bce828..d8d717c 100644 --- a/container/compose.example.toml +++ b/container/compose.example.toml @@ -1,4 +1,4 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later +# SPDX-License-Identifier: MPL-2.0 # # Example selur-compose configuration — multi-service stack # diff --git a/container/compose.toml b/container/compose.toml index 19eda0f..a14f8a0 100644 --- a/container/compose.toml +++ b/container/compose.toml @@ -1,4 +1,4 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later +# SPDX-License-Identifier: MPL-2.0 # # {{PROJECT_NAME}} selur-compose configuration # diff --git a/container/ct-build.sh b/container/ct-build.sh index 527325d..a54a541 100755 --- a/container/ct-build.sh +++ b/container/ct-build.sh @@ -1,5 +1,5 @@ #!/usr/bin/env bash -# SPDX-License-Identifier: PMPL-1.0-or-later +# SPDX-License-Identifier: MPL-2.0 # # {{PROJECT_NAME}} — Cerro Torre build, sign, and verify pipeline # diff --git a/container/deploy.k9.ncl b/container/deploy.k9.ncl index b283a7c..0ad0d04 100644 --- a/container/deploy.k9.ncl +++ b/container/deploy.k9.ncl @@ -1,4 +1,4 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later +# SPDX-License-Identifier: MPL-2.0 # deploy.k9.ncl — {{PROJECT_NAME}} deployment component (Hunt level) # # k9-svc deployment specification with full pedigree (L1-L5). diff --git a/container/entrypoint.sh b/container/entrypoint.sh index 72ace9c..a7a0369 100755 --- a/container/entrypoint.sh +++ b/container/entrypoint.sh @@ -1,5 +1,5 @@ #!/bin/sh -# SPDX-License-Identifier: PMPL-1.0-or-later +# SPDX-License-Identifier: MPL-2.0 # {{PROJECT_NAME}} container entrypoint # # Handles signal propagation, startup logging, and health check diff --git a/container/manifest.toml b/container/manifest.toml index 08be36f..46f2e40 100644 --- a/container/manifest.toml +++ b/container/manifest.toml @@ -1,4 +1,4 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later +# SPDX-License-Identifier: MPL-2.0 # # Cerro Torre manifest for {{PROJECT_NAME}} .ctp bundle # diff --git a/container/vordr.toml b/container/vordr.toml index 0fb7fd5..af38fc5 100644 --- a/container/vordr.toml +++ b/container/vordr.toml @@ -1,4 +1,4 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later +# SPDX-License-Identifier: MPL-2.0 # # Vordr runtime monitoring configuration for {{PROJECT_NAME}} # diff --git a/contractile.just b/contractile.just index 8f99137..9a5827b 100644 --- a/contractile.just +++ b/contractile.just @@ -2,7 +2,7 @@ # Source directory: contractiles # Re-generate with: contractile gen-just --dir contractiles # -# SPDX-License-Identifier: PMPL-1.0-or-later +# SPDX-License-Identifier: MPL-2.0 # === DUST (Recovery & Rollback) === # Source: Dustfile.a2ml diff --git a/docs/attribution/CITATION.cff b/docs/attribution/CITATION.cff index 4d562f4..05d36d9 100644 --- a/docs/attribution/CITATION.cff +++ b/docs/attribution/CITATION.cff @@ -9,7 +9,7 @@ version: 0.1.0 date-released: {{CURRENT_DATE}} url: "https://{{FORGE}}/{{OWNER}}/{{REPO}}" repository-code: "https://{{FORGE}}/{{OWNER}}/{{REPO}}" -license: PMPL-1.0-or-later +license: MPL-2.0 keywords: - "rsr" - "formal-verification" diff --git a/docs/attribution/CITATIONS.adoc b/docs/attribution/CITATIONS.adoc index 0832416..b606e80 100644 --- a/docs/attribution/CITATIONS.adoc +++ b/docs/attribution/CITATIONS.adoc @@ -12,7 +12,7 @@ title = {{{PROJECT_NAME}}}, year = {{{CURRENT_YEAR}}}, url = {https://github.com/hyperpolymath/{{PROJECT_NAME}}}, - license = {PMPL-1.0-or-later} + license = {MPL-2.0} } ---- diff --git a/docs/practice/AI-CONVENTIONS.adoc b/docs/practice/AI-CONVENTIONS.adoc index 4ee9897..f5d52fb 100644 --- a/docs/practice/AI-CONVENTIONS.adoc +++ b/docs/practice/AI-CONVENTIONS.adoc @@ -21,11 +21,11 @@ Per-tool config files (.cursorrules, .clinerules, etc.) reference this document. ## License -- All original code: **PMPL-1.0-or-later** -- Fallback (platform-required only): MPL-2.0 with comment explaining why. +- All original code: **MPL-2.0** +- All prose (`.adoc`, `.md`, docs): **CC-BY-SA-4.0** - NEVER use AGPL-3.0. - Preserve third-party licenses verbatim. -- Every source file needs `# SPDX-License-Identifier: CC-BY-SA-4.0`. +- Every file needs an SPDX header: `SPDX-License-Identifier: MPL-2.0` on code, `SPDX-License-Identifier: CC-BY-SA-4.0` on prose. ## Author Attribution diff --git a/docs/reports/audit/audit-2026-04-15-post.adoc b/docs/reports/audit/audit-2026-04-15-post.adoc index 2faec23..11edf33 100644 --- a/docs/reports/audit/audit-2026-04-15-post.adoc +++ b/docs/reports/audit/audit-2026-04-15-post.adoc @@ -1,3 +1,4 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 == Post-audit Status Report: jaffascript * *Date:* 2026-04-15 diff --git a/docs/tech-debt-2026-05-26.adoc b/docs/tech-debt-2026-05-26.adoc index da26e7f..9bb3a6e 100644 --- a/docs/tech-debt-2026-05-26.adoc +++ b/docs/tech-debt-2026-05-26.adoc @@ -1,3 +1,4 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 == Tech-Debt Audit — jaffascript — 2026-05-26 *Source:* estate-wide automated scan 2026-05-26. *Companion:* diff --git a/features/README.adoc b/features/README.adoc index 4922891..5c24f38 100644 --- a/features/README.adoc +++ b/features/README.adoc @@ -1,3 +1,3 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell = Project Features diff --git a/features/boj-server/README.adoc b/features/boj-server/README.adoc index 0ef0376..25f08a1 100644 --- a/features/boj-server/README.adoc +++ b/features/boj-server/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell = BoJ Server Integration :icons: font diff --git a/features/panic-attacker/README.adoc b/features/panic-attacker/README.adoc index de0bd9b..deff9f1 100644 --- a/features/panic-attacker/README.adoc +++ b/features/panic-attacker/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell = Panic Attacker Feature :icons: font diff --git a/features/ssg/README.adoc b/features/ssg/README.adoc index a6ef262..a6063e1 100644 --- a/features/ssg/README.adoc +++ b/features/ssg/README.adoc @@ -1,3 +1,3 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell = Ssg Feature diff --git a/features/ssg/ssg-bootstrap.sh b/features/ssg/ssg-bootstrap.sh index 620c765..0ce6171 100755 --- a/features/ssg/ssg-bootstrap.sh +++ b/features/ssg/ssg-bootstrap.sh @@ -1,5 +1,5 @@ #!/usr/bin/env bash -# SPDX-License-Identifier: PMPL-1.0-or-later +# SPDX-License-Identifier: MPL-2.0 # # ssg-bootstrap.sh — Universal SSG Initialisation Helper # diff --git a/llm-warmup-dev.adoc b/llm-warmup-dev.adoc index e47a82c..08ea553 100644 --- a/llm-warmup-dev.adoc +++ b/llm-warmup-dev.adoc @@ -1,3 +1,4 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 == LLM Warmup — rsr-template-repo (Developer) === What is rsr-template-repo? @@ -14,6 +15,6 @@ See README.adoc for overview. === Quick Context -* License: PMPL-1.0-or-later +* License: MPL-2.0 for code, CC-BY-SA-4.0 for prose * Part of hyperpolymath ecosystem * See EXPLAINME.adoc for architecture diff --git a/llm-warmup-user.adoc b/llm-warmup-user.adoc index 7d5d7e5..e327fbf 100644 --- a/llm-warmup-user.adoc +++ b/llm-warmup-user.adoc @@ -1,3 +1,4 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 == LLM Warmup — rsr-template-repo (User) === What is rsr-template-repo? @@ -14,6 +15,6 @@ See README.adoc for overview. === Quick Context -* License: PMPL-1.0-or-later +* License: MPL-2.0 for code, CC-BY-SA-4.0 for prose * Part of hyperpolymath ecosystem * See EXPLAINME.adoc for architecture diff --git a/scripts/invariant-path.sh b/scripts/invariant-path.sh index 3f7c05b..e6fdef8 100755 --- a/scripts/invariant-path.sh +++ b/scripts/invariant-path.sh @@ -1,4 +1,5 @@ #!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 set -euo pipefail SCRIPT_DIR="$(cd -- "$(dirname -- "${BASH_SOURCE[0]}")" && pwd)" diff --git a/scripts/validate-template.sh b/scripts/validate-template.sh index 0d6eefc..f053202 100755 --- a/scripts/validate-template.sh +++ b/scripts/validate-template.sh @@ -1,5 +1,5 @@ #!/bin/bash -# SPDX-License-Identifier: PMPL-1.0-or-later +# SPDX-License-Identifier: MPL-2.0 # Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) # # RSR Template Validation Script diff --git a/session/README.adoc b/session/README.adoc index d14a6d7..5cc8b0c 100644 --- a/session/README.adoc +++ b/session/README.adoc @@ -1,3 +1,4 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 == Session Bindings (Thin Local Layer) This directory provides local integration for central session-management diff --git a/session/dispatch.sh b/session/dispatch.sh index 61dc720..5a1768e 100755 --- a/session/dispatch.sh +++ b/session/dispatch.sh @@ -1,4 +1,5 @@ #!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 set -euo pipefail if [ "$#" -lt 3 ]; then diff --git a/session/local-hooks.sh b/session/local-hooks.sh index 20e9fae..12ed294 100755 --- a/session/local-hooks.sh +++ b/session/local-hooks.sh @@ -1,4 +1,5 @@ #!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 set -euo pipefail verb="${1:-}" diff --git a/src/README.adoc b/src/README.adoc index d8c8116..9e5bd3c 100644 --- a/src/README.adoc +++ b/src/README.adoc @@ -1,3 +1,3 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell = src Pillar diff --git a/src/aspects/README.adoc b/src/aspects/README.adoc index 9b7b80f..c4ef693 100644 --- a/src/aspects/README.adoc +++ b/src/aspects/README.adoc @@ -1,3 +1,3 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell = Aspects Pillar diff --git a/src/aspects/integrity/README.adoc b/src/aspects/integrity/README.adoc index 17a09db..d3e1ee1 100644 --- a/src/aspects/integrity/README.adoc +++ b/src/aspects/integrity/README.adoc @@ -1,3 +1,3 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell = Integrity Aspect diff --git a/src/aspects/observability/README.adoc b/src/aspects/observability/README.adoc index df2ca36..8a2151c 100644 --- a/src/aspects/observability/README.adoc +++ b/src/aspects/observability/README.adoc @@ -1,3 +1,3 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell = Observability Aspect diff --git a/src/aspects/security/README.adoc b/src/aspects/security/README.adoc index 11ad21b..e28b5da 100644 --- a/src/aspects/security/README.adoc +++ b/src/aspects/security/README.adoc @@ -1,3 +1,3 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell = Security Aspect diff --git a/src/contracts/README.adoc b/src/contracts/README.adoc index 20dd4ca..657be1f 100644 --- a/src/contracts/README.adoc +++ b/src/contracts/README.adoc @@ -1,3 +1,3 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell = Contracts Unit diff --git a/src/definitions/README.adoc b/src/definitions/README.adoc index 5a9912f..02ecc4f 100644 --- a/src/definitions/README.adoc +++ b/src/definitions/README.adoc @@ -1,3 +1,3 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell = Definitions Unit diff --git a/src/errors/README.adoc b/src/errors/README.adoc index eff7b29..b03a1c4 100644 --- a/src/errors/README.adoc +++ b/src/errors/README.adoc @@ -1,3 +1,3 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell = Errors Unit diff --git a/src/interface/Abi/README.adoc b/src/interface/Abi/README.adoc index 46743d7..4a99517 100644 --- a/src/interface/Abi/README.adoc +++ b/src/interface/Abi/README.adoc @@ -1,3 +1,3 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell = abi Logic diff --git a/src/interface/README.adoc b/src/interface/README.adoc index 727b9e7..4fde708 100644 --- a/src/interface/README.adoc +++ b/src/interface/README.adoc @@ -1,3 +1,3 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell = interface Unit diff --git a/src/interface/ffi/README.adoc b/src/interface/ffi/README.adoc index b402d64..ca14320 100644 --- a/src/interface/ffi/README.adoc +++ b/src/interface/ffi/README.adoc @@ -1,3 +1,3 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell = ffi Logic diff --git a/src/interface/ffi/src/README.adoc b/src/interface/ffi/src/README.adoc index 4228438..d5631f6 100644 --- a/src/interface/ffi/src/README.adoc +++ b/src/interface/ffi/src/README.adoc @@ -1,3 +1,3 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell = Src Logic diff --git a/src/interface/ffi/test/README.adoc b/src/interface/ffi/test/README.adoc index cdbb47d..e6ff267 100644 --- a/src/interface/ffi/test/README.adoc +++ b/src/interface/ffi/test/README.adoc @@ -1,3 +1,3 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell = Test Logic diff --git a/src/interface/generated/README.adoc b/src/interface/generated/README.adoc index 93daef2..9e94b29 100644 --- a/src/interface/generated/README.adoc +++ b/src/interface/generated/README.adoc @@ -1,3 +1,3 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell = generated Logic diff --git a/src/interface/generated/abi/README.adoc b/src/interface/generated/abi/README.adoc index 0e29b69..f3b3808 100644 --- a/src/interface/generated/abi/README.adoc +++ b/src/interface/generated/abi/README.adoc @@ -1,3 +1,3 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell = Abi Logic diff --git a/stapeln.toml b/stapeln.toml index 703372f..eb3785e 100644 --- a/stapeln.toml +++ b/stapeln.toml @@ -9,7 +9,7 @@ name = "rsr-template-repo" version = "0.1.0" description = "rsr-template-repo container service" author = "Jonathan D.A. Jewell " -license = "PMPL-1.0-or-later" +license = "MPL-2.0" registry = "ghcr.io/hyperpolymath" [build] diff --git a/tools/invariant-path/README.adoc b/tools/invariant-path/README.adoc index 57c4e3d..040d7a2 100644 --- a/tools/invariant-path/README.adoc +++ b/tools/invariant-path/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) Jonathan D.A. Jewell = Invariant Path Integration (RSR Template) diff --git a/verification/README.adoc b/verification/README.adoc index d572c1b..e9a402d 100644 --- a/verification/README.adoc +++ b/verification/README.adoc @@ -1,2 +1,5 @@ -// SPDX-License-Identifier: MPL-2.0 -// Verification scripts and test suites for jaffascript. +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) Jonathan D.A. Jewell += Verification Pillar + +Verification scripts and test suites for jaffascript. diff --git a/verification/verification/0.1-AI-MANIFEST.a2ml b/verification/verification/0.1-AI-MANIFEST.a2ml deleted file mode 100644 index 39b370f..0000000 --- a/verification/verification/0.1-AI-MANIFEST.a2ml +++ /dev/null @@ -1,27 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later ---- -### [META] -id: "verification-pillar" -level: 1 -parent: "../0-AI-MANIFEST.a2ml" - ---- -### [AI_MANIFEST] -description: | - Primary verification pillar. Contains evidence for correctness, - performance, formal proofs, randomized testing, and aerospace-grade - high-assurance metrics (MC/DC coverage, traceability, safety cases). - -canonical_locations: - tests: "tests/" - benchmarks: "benchmarks/" - proofs: "proofs/" - fuzzing: "fuzzing/" - simulations: "simulations/" - coverage: "coverage/" - traceability: "traceability/" - safety_case: "safety_case/" - -invariants: - - "Evidence MUST be reproducible and documented" - - "High-assurance deployments MUST satisfy traceability and safety_case requirements" diff --git a/verification/verification/README.adoc b/verification/verification/README.adoc deleted file mode 100644 index efa7fb2..0000000 --- a/verification/verification/README.adoc +++ /dev/null @@ -1,3 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// Copyright (c) Jonathan D.A. Jewell -= Verification Pillar diff --git a/verification/verification/benchmarks/0.2-AI-MANIFEST.a2ml b/verification/verification/benchmarks/0.2-AI-MANIFEST.a2ml deleted file mode 100644 index 6416309..0000000 --- a/verification/verification/benchmarks/0.2-AI-MANIFEST.a2ml +++ /dev/null @@ -1,11 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later ---- -### [META] -id: "benches-pillar" -level: 2 -parent: "../0.1-AI-MANIFEST.a2ml" - ---- -### [AI_MANIFEST] -description: | - Benches pillar. diff --git a/verification/verification/benchmarks/README.adoc b/verification/verification/benchmarks/README.adoc deleted file mode 100644 index beb83cd..0000000 --- a/verification/verification/benchmarks/README.adoc +++ /dev/null @@ -1,3 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// Copyright (c) Jonathan D.A. Jewell -= Benchmarks Unit diff --git a/verification/verification/coverage/0.2-AI-MANIFEST.a2ml b/verification/verification/coverage/0.2-AI-MANIFEST.a2ml deleted file mode 100644 index fc15bd3..0000000 --- a/verification/verification/coverage/0.2-AI-MANIFEST.a2ml +++ /dev/null @@ -1,12 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later ---- -### [META] -id: "verification-unit-coverage" -level: 2 -parent: "../0.1-AI-MANIFEST.a2ml" - ---- -### [AI_MANIFEST] -description: | - High-assurance verification unit for coverage. - Critical for safety-of-life and aerospace-grade deployment standards. diff --git a/verification/verification/coverage/README.adoc b/verification/verification/coverage/README.adoc deleted file mode 100644 index c10a6ac..0000000 --- a/verification/verification/coverage/README.adoc +++ /dev/null @@ -1,3 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// Copyright (c) Jonathan D.A. Jewell -= Coverage Unit diff --git a/verification/verification/fuzzing/0.2-AI-MANIFEST.a2ml b/verification/verification/fuzzing/0.2-AI-MANIFEST.a2ml deleted file mode 100644 index 79c4fef..0000000 --- a/verification/verification/fuzzing/0.2-AI-MANIFEST.a2ml +++ /dev/null @@ -1,11 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later ---- -### [META] -id: "fuzzing-unit" -level: 2 -parent: "../0.1-AI-MANIFEST.a2ml" - ---- -### [AI_MANIFEST] -description: | - Fuzzing unit for high-rigor verification. diff --git a/verification/verification/fuzzing/README.adoc b/verification/verification/fuzzing/README.adoc deleted file mode 100644 index b07ea68..0000000 --- a/verification/verification/fuzzing/README.adoc +++ /dev/null @@ -1,3 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// Copyright (c) Jonathan D.A. Jewell -= Fuzzing Unit diff --git a/verification/verification/proofs/0.2-AI-MANIFEST.a2ml b/verification/verification/proofs/0.2-AI-MANIFEST.a2ml deleted file mode 100644 index 0e5666f..0000000 --- a/verification/verification/proofs/0.2-AI-MANIFEST.a2ml +++ /dev/null @@ -1,11 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later ---- -### [META] -id: "verification-unit-proofs" -level: 2 -parent: "../0.1-AI-MANIFEST.a2ml" - ---- -### [AI_MANIFEST] -description: | - Sub-unit focusing on proofs. diff --git a/verification/verification/proofs/README.adoc b/verification/verification/proofs/README.adoc deleted file mode 100644 index 520f5e9..0000000 --- a/verification/verification/proofs/README.adoc +++ /dev/null @@ -1,60 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// Copyright (c) Jonathan D.A. Jewell -= Formal Verification Proofs - -This directory contains formal proofs organised by proof assistant. - -== Directory Structure - -[source] ----- -proofs/ -├── idris2/ # Idris2 proofs (ABI, dependent types) -│ ├── ABI/ # ABI-specific proofs (mandatory) -│ │ ├── Pointers.idr # Non-null pointer safety -│ │ ├── Layout.idr # Memory layout correctness -│ │ ├── Platform.idr # Platform type size proofs -│ │ ├── Foreign.idr # FFI return type proofs -│ │ └── Compliance.idr # C ABI compliance -│ └── Types.idr # Core data type well-formedness -├── lean4/ # Lean4 proofs (algebra, lattices) -│ └── ApiTypes.lean -├── agda/ # Agda proofs (induction, metatheory) -│ └── Properties.agda -├── coq/ # Coq proofs (type systems, compilation) -│ └── TypeSafety.v -└── tlaplus/ # TLA+ specs (distributed protocols) - └── StateMachine.tla ----- - -== Verification Commands - -[source,bash] ----- -just proof-check-all # Run all proof checkers -just proof-check-idris2 # Idris2 only -just proof-check-lean4 # Lean4 only -just proof-check-agda # Agda only -just proof-check-coq # Coq only ----- - -== Banned Patterns - -The following MUST NOT appear in any proof file: - -- `believe_me` (Idris2) -- `assert_total` (Idris2) -- `postulate` (Idris2/Agda) -- `sorry` (Lean4) -- `Admitted` (Coq) -- `unsafeCoerce` (Haskell) - -CI enforces this via `panic-attack assail --proofs-only`. - -== Adding New Proofs - -1. Choose the appropriate prover (see PROOF-NEEDS.md) -2. Create the `.idr`/`.lean`/`.agda`/`.v`/`.tla` file in the right directory -3. Ensure `%default total` (Idris2) or equivalent -4. Run the verification command -5. Update PROOF-STATUS.md diff --git a/verification/verification/proofs/agda/Properties.agda b/verification/verification/proofs/agda/Properties.agda deleted file mode 100644 index 90e4c3c..0000000 --- a/verification/verification/proofs/agda/Properties.agda +++ /dev/null @@ -1,37 +0,0 @@ --- SPDX-License-Identifier: PMPL-1.0-or-later --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- --- Agda Proof Template: Inductive and coinductive properties --- Replace with your project's domain-specific proofs. --- All proofs must be total (no postulate, no {-# TERMINATING #-}). - -module Properties where - -open import Data.Nat using (ℕ; zero; suc; _+_; _≤_; z≤n; s≤s; _<_) -open import Data.Nat.Properties using (+-comm; +-assoc; ≤-refl; ≤-trans) -open import Data.List using (List; []; _∷_; length; _++_) -open import Data.List.Properties using (length-++ ) -open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym; trans) - --- Example: Proof that list append preserves total length --- Replace with your project's domain proofs. - -append-length : ∀ {A : Set} (xs ys : List A) → - length (xs ++ ys) ≡ length xs + length ys -append-length xs ys = length-++ xs - --- Example: Monotonicity proof template --- Use for state machines, confidence scores, trust levels -record Monotone {A : Set} (_≤A_ : A → A → Set) (f : A → A) : Set where - field - preserves : ∀ {x y} → x ≤A y → f x ≤A f y - --- Example: Idempotence proof template --- Use for normalisation, deduplication, formatting -record Idempotent {A : Set} (_≡A_ : A → A → Set) (f : A → A) : Set where - field - idem : ∀ (x : A) → f (f x) ≡A f x - --- Example: Natural number successor is monotone -suc-monotone : Monotone _≤_ suc -suc-monotone = record { preserves = s≤s } diff --git a/verification/verification/proofs/coq/TypeSafety.v b/verification/verification/proofs/coq/TypeSafety.v deleted file mode 100644 index c2ec6eb..0000000 --- a/verification/verification/proofs/coq/TypeSafety.v +++ /dev/null @@ -1,73 +0,0 @@ -(* SPDX-License-Identifier: PMPL-1.0-or-later *) -(* Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) *) -(* - Coq Proof Template: Type system soundness - Replace with your project's type system proofs. - All proofs must be complete — NO Admitted allowed. -*) - -Require Import Coq.Lists.List. -Require Import Coq.Arith.Arith. -Require Import Coq.Bool.Bool. -Import ListNotations. - -(** * Example: Simple expression language with type safety *) -(** Replace this entire section with your project's type system. *) - -(** Types *) -Inductive ty : Type := - | TyNat : ty - | TyBool : ty. - -(** Expressions *) -Inductive expr : Type := - | EConst : nat -> expr - | ETrue : expr - | EFalse : expr - | EPlus : expr -> expr -> expr - | EEq : expr -> expr -> expr. - -(** Values *) -Inductive value : Type := - | VNat : nat -> value - | VBool : bool -> value. - -(** Typing relation *) -Inductive has_type : expr -> ty -> Prop := - | T_Const : forall n, has_type (EConst n) TyNat - | T_True : has_type ETrue TyBool - | T_False : has_type EFalse TyBool - | T_Plus : forall e1 e2, - has_type e1 TyNat -> has_type e2 TyNat -> - has_type (EPlus e1 e2) TyNat - | T_Eq : forall e1 e2, - has_type e1 TyNat -> has_type e2 TyNat -> - has_type (EEq e1 e2) TyBool. - -(** Evaluation *) -Inductive eval : expr -> value -> Prop := - | E_Const : forall n, eval (EConst n) (VNat n) - | E_True : eval ETrue (VBool true) - | E_False : eval EFalse (VBool false) - | E_Plus : forall e1 e2 n1 n2, - eval e1 (VNat n1) -> eval e2 (VNat n2) -> - eval (EPlus e1 e2) (VNat (n1 + n2)) - | E_Eq : forall e1 e2 n1 n2, - eval e1 (VNat n1) -> eval e2 (VNat n2) -> - eval (EEq e1 e2) (VBool (Nat.eqb n1 n2)). - -(** Value typing *) -Definition value_has_type (v : value) (t : ty) : Prop := - match v, t with - | VNat _, TyNat => True - | VBool _, TyBool => True - | _, _ => False - end. - -(** Type soundness: well-typed expressions evaluate to well-typed values *) -Theorem type_soundness : forall e t v, - has_type e t -> eval e v -> value_has_type v t. -Proof. - intros e t v Htype Heval. - induction Htype; inversion Heval; subst; simpl; auto. -Qed. diff --git a/verification/verification/proofs/idris2/ABI/Compliance.idr b/verification/verification/proofs/idris2/ABI/Compliance.idr deleted file mode 100644 index b94a5db..0000000 --- a/verification/verification/proofs/idris2/ABI/Compliance.idr +++ /dev/null @@ -1,41 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) Jonathan D.A. Jewell --- --- ABI Proof: C ABI compliance --- Proves that struct layouts are C ABI compliant. --- All proofs MUST be constructive (no believe_me, no assert_total). - -module ABI.Compliance - -import ABI.Layout -import ABI.Platform - -%default total - -||| Evidence that every field in a layout is correctly aligned. -public export -data AllFieldsAligned : List StructField -> Type where - AFANil : AllFieldsAligned [] - AFACons : FieldAligned f -> AllFieldsAligned fs -> AllFieldsAligned (f :: fs) - -||| Evidence that every field is within the struct bounds. -public export -data AllFieldsInBounds : (size : Nat) -> List StructField -> Type where - AFBNil : AllFieldsInBounds size [] - AFBCons : FieldInBounds size f -> AllFieldsInBounds size fs -> AllFieldsInBounds size (f :: fs) - -||| A struct layout is C ABI compliant when: -||| 1. All fields are aligned to their natural alignment -||| 2. All fields are within bounds of the struct size -||| 3. The struct size is a multiple of the struct alignment -public export -record CABICompliant (layout : StructLayout) where - constructor MkCompliant - fieldsAligned : AllFieldsAligned (layoutFields layout) - fieldsInBounds : AllFieldsInBounds (layoutSize layout) (layoutFields layout) - sizeAligned : modNatNZ (layoutSize layout) (layoutAlignment layout) SIsNonZero = 0 - -||| An empty struct is trivially compliant (size=1, alignment=1). -export -emptyStructCompliant : CABICompliant (MkLayout "empty" [] 1 1) -emptyStructCompliant = MkCompliant AFANil AFBNil Refl diff --git a/verification/verification/proofs/idris2/ABI/Foreign.idr b/verification/verification/proofs/idris2/ABI/Foreign.idr deleted file mode 100644 index 1e550dd..0000000 --- a/verification/verification/proofs/idris2/ABI/Foreign.idr +++ /dev/null @@ -1,53 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) Jonathan D.A. Jewell --- --- ABI Proof: FFI function return type proofs --- Proves that all FFI functions return expected types. --- All proofs MUST be constructive (no believe_me, no assert_total). - -module ABI.Foreign - -%default total - -||| Result type for FFI operations. -||| All FFI functions must return through this type. -public export -data FFIResult : Type -> Type where - FFISuccess : (value : a) -> FFIResult a - FFIError : (code : Int) -> (msg : String) -> FFIResult a - -||| Proof that FFIResult is a functor (map preserves structure). -export -mapFFIResult : (a -> b) -> FFIResult a -> FFIResult b -mapFFIResult f (FFISuccess value) = FFISuccess (f value) -mapFFIResult f (FFIError code msg) = FFIError code msg - -||| Proof that mapping identity preserves the result. -export -mapIdPreserves : (r : FFIResult a) -> mapFFIResult Prelude.id r = r -mapIdPreserves (FFISuccess value) = Refl -mapIdPreserves (FFIError code msg) = Refl - -||| An FFI function specification: name, argument types, return type. -public export -record FFISpec where - constructor MkFFISpec - ffiName : String - ffiReturnType : Type - -||| Proof that an FFI spec has a specific return type. -||| Use this to verify at compile time that FFI functions return the -||| types we expect across the C ABI boundary. -public export -FFIReturns : FFISpec -> Type -> Type -FFIReturns spec ty = ffiReturnType spec = ty - -||| C calling convention marker. -||| Proofs about calling convention compatibility. -public export -data CallingConv = CDecl | StdCall | FastCall - -||| All hyperpolymath FFI uses CDecl. -public export -defaultCallingConv : CallingConv -defaultCallingConv = CDecl diff --git a/verification/verification/proofs/idris2/ABI/Layout.idr b/verification/verification/proofs/idris2/ABI/Layout.idr deleted file mode 100644 index 9040a5e..0000000 --- a/verification/verification/proofs/idris2/ABI/Layout.idr +++ /dev/null @@ -1,63 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) Jonathan D.A. Jewell --- --- ABI Proof: Memory layout correctness --- Proves struct size, alignment, and padding properties. --- All proofs MUST be constructive (no believe_me, no assert_total). - -module ABI.Layout - -%default total - -||| Witness that a type has a known size in bytes at compile time. -public export -interface HasSize (ty : Type) where - sizeOf : Nat - -||| Witness that a type has a known alignment in bytes. -public export -interface HasAlignment (ty : Type) where - alignOf : Nat - -||| Calculate padding needed to reach the next aligned offset. -||| paddingFor offset alignment = bytes to add so (offset + padding) `mod` alignment == 0 -public export -paddingFor : (offset : Nat) -> (alignment : Nat) -> {auto 0 ok : NonZero alignment} -> Nat -paddingFor offset alignment = let r = modNatNZ offset alignment ok - in case r of - Z => Z - (S _) => minus alignment r - -||| Proof that an offset with zero remainder needs zero padding. -export -alignedNeedsPadding : (n : Nat) -> (a : Nat) -> {auto 0 ok : NonZero a} -> - modNatNZ n a ok = 0 -> paddingFor n a = 0 -alignedNeedsPadding n a prf = rewrite prf in Refl - -||| A field within a struct, carrying its offset and size. -public export -record StructField where - constructor MkField - fieldName : String - fieldOffset : Nat - fieldSize : Nat - fieldAlignment : Nat - -||| Proof that a field is correctly aligned within a struct. -public export -FieldAligned : StructField -> Type -FieldAligned f = modNatNZ (fieldOffset f) (fieldAlignment f) SIsNonZero = 0 - -||| Proof that a field does not overflow past a given struct size. -public export -FieldInBounds : (structSize : Nat) -> StructField -> Type -FieldInBounds sz f = LTE (fieldOffset f + fieldSize f) sz - -||| A struct layout is a list of fields with a total size. -public export -record StructLayout where - constructor MkLayout - layoutName : String - layoutFields : List StructField - layoutSize : Nat - layoutAlignment : Nat diff --git a/verification/verification/proofs/idris2/ABI/Platform.idr b/verification/verification/proofs/idris2/ABI/Platform.idr deleted file mode 100644 index a8d6b94..0000000 --- a/verification/verification/proofs/idris2/ABI/Platform.idr +++ /dev/null @@ -1,63 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) Jonathan D.A. Jewell --- --- ABI Proof: Platform-specific type size proofs --- Proves that C type sizes are correct per platform. --- All proofs MUST be constructive (no believe_me, no assert_total). - -module ABI.Platform - -%default total - -||| Supported target platforms for ABI verification. -public export -data Platform = Linux64 | LinuxARM64 | MacOS64 | MacOSARM64 - | Windows64 | FreeBSD64 | WASM32 - -||| Pointer size in bytes for each platform. -public export -ptrSize : Platform -> Nat -ptrSize WASM32 = 4 -ptrSize _ = 8 - -||| C `int` size in bytes. -public export -cIntSize : Platform -> Nat -cIntSize _ = 4 - -||| C `size_t` size in bytes (matches pointer size). -public export -cSizeT : Platform -> Nat -cSizeT = ptrSize - -||| Proof that size_t always equals pointer size on all platforms. -export -sizeTEqPtrSize : (p : Platform) -> cSizeT p = ptrSize p -sizeTEqPtrSize _ = Refl - -||| Proof that pointer size is always 4 or 8 bytes. -export -ptrSizeValid : (p : Platform) -> Either (ptrSize p = 4) (ptrSize p = 8) -ptrSizeValid WASM32 = Left Refl -ptrSizeValid Linux64 = Right Refl -ptrSizeValid LinuxARM64 = Right Refl -ptrSizeValid MacOS64 = Right Refl -ptrSizeValid MacOSARM64 = Right Refl -ptrSizeValid Windows64 = Right Refl -ptrSizeValid FreeBSD64 = Right Refl - -||| Proof that C int is always 4 bytes on all platforms. -export -cIntAlways4 : (p : Platform) -> cIntSize p = 4 -cIntAlways4 _ = Refl - -||| Proof that pointer size is always at least 4 bytes. -export -ptrSizeAtLeast4 : (p : Platform) -> LTE 4 (ptrSize p) -ptrSizeAtLeast4 WASM32 = lteRefl -ptrSizeAtLeast4 Linux64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl))) -ptrSizeAtLeast4 LinuxARM64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl))) -ptrSizeAtLeast4 MacOS64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl))) -ptrSizeAtLeast4 MacOSARM64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl))) -ptrSizeAtLeast4 Windows64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl))) -ptrSizeAtLeast4 FreeBSD64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl))) diff --git a/verification/verification/proofs/idris2/ABI/Pointers.idr b/verification/verification/proofs/idris2/ABI/Pointers.idr deleted file mode 100644 index 31b6c5f..0000000 --- a/verification/verification/proofs/idris2/ABI/Pointers.idr +++ /dev/null @@ -1,52 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) Jonathan D.A. Jewell --- --- ABI Proof: Non-null pointer safety --- Template proof — customise for your project's pointer types. --- All proofs MUST be constructive (no believe_me, no assert_total). - -module ABI.Pointers - -import Data.So - -%default total - -||| A pointer value that has been proven non-null. -||| The `So` constraint carries a compile-time witness that `ptr /= 0`. -public export -record SafePtr where - constructor MkSafePtr - ptr : Bits64 - {auto 0 nonNull : So (ptr /= 0)} - -||| Proof that SafePtr can never hold a null (zero) value. -||| This is enforced by the `So` constraint in the record. -export -safePtrNeverNull : (sp : SafePtr) -> So (sp.ptr /= 0) -safePtrNeverNull sp = sp.nonNull - -||| Wrap a raw pointer with a runtime null check. -||| Returns Nothing if the pointer is null. -export -checkPtr : (raw : Bits64) -> Maybe SafePtr -checkPtr 0 = Nothing -checkPtr raw = case choose (raw /= 0) of - Left prf => Just (MkSafePtr raw) - Right _ => Nothing - -||| Proof that checkPtr 0 always returns Nothing. -export -checkPtrZeroIsNothing : checkPtr 0 = Nothing -checkPtrZeroIsNothing = Refl - -||| An opaque handle backed by a non-null pointer. -||| Use this for FFI resource handles (file descriptors, sockets, etc.). -public export -record Handle (tag : String) where - constructor MkHandle - safePtr : SafePtr - -||| Proof that two handles with equal pointers are equal. -export -handlePtrEq : (h1, h2 : Handle tag) -> h1.safePtr.ptr = h2.safePtr.ptr -> h1 = h2 -handlePtrEq (MkHandle (MkSafePtr p)) (MkHandle (MkSafePtr p)) Refl = Refl diff --git a/verification/verification/proofs/idris2/Types.idr b/verification/verification/proofs/idris2/Types.idr deleted file mode 100644 index cc7cce8..0000000 --- a/verification/verification/proofs/idris2/Types.idr +++ /dev/null @@ -1,38 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) Jonathan D.A. Jewell --- --- Typing Proof: Core data type well-formedness --- Template — replace with your project's core types. --- All proofs MUST be constructive (no believe_me, no assert_total). - -module Types - -%default total - -||| Example: A bounded natural number (0 to max). -||| Replace with your project's core types. -public export -record Bounded (max : Nat) where - constructor MkBounded - value : Nat - {auto 0 inBounds : LTE value max} - -||| Proof that a Bounded value is always <= max. -export -boundedLeMax : (b : Bounded max) -> LTE b.value max -boundedLeMax b = b.inBounds - -||| Proof that zero is always a valid Bounded value. -export -zeroIsBounded : {max : Nat} -> Bounded (S max) -zeroIsBounded = MkBounded 0 - -||| Example: A non-empty list with a compile-time guarantee. -public export -data NonEmpty : List a -> Type where - IsNonEmpty : NonEmpty (x :: xs) - -||| Proof that cons always produces a non-empty list. -export -consIsNonEmpty : (x : a) -> (xs : List a) -> NonEmpty (x :: xs) -consIsNonEmpty _ _ = IsNonEmpty diff --git a/verification/verification/proofs/lean4/ApiTypes.lean b/verification/verification/proofs/lean4/ApiTypes.lean deleted file mode 100644 index 144a943..0000000 --- a/verification/verification/proofs/lean4/ApiTypes.lean +++ /dev/null @@ -1,44 +0,0 @@ --- SPDX-License-Identifier: PMPL-1.0-or-later --- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) --- --- Typing Proof: Public API type safety --- Template — replace with your project's API types. --- Proves properties about exported function signatures. - --- Example: Result type used across API boundaries -inductive ApiResult (α : Type) where - | ok : α → ApiResult α - | error : Nat → String → ApiResult α - -namespace ApiResult - -- Proof: map preserves structure (functor law: map id = id) - def map (f : α → β) : ApiResult α → ApiResult β - | .ok v => .ok (f v) - | .error c m => .error c m - - theorem map_id : ∀ (r : ApiResult α), map id r = r := by - intro r - cases r with - | ok v => simp [map] - | error c m => simp [map] - - -- Proof: map composition (functor law: map (g ∘ f) = map g ∘ map f) - theorem map_comp (f : α → β) (g : β → γ) : - ∀ (r : ApiResult α), map (g ∘ f) r = map g (map f r) := by - intro r - cases r with - | ok v => simp [map, Function.comp] - | error c m => simp [map] - --- Example: Bounded confidence value (0.0 to 1.0 modelled as Nat/1000) --- Replace with your project's numeric invariants -structure BoundedNat (max : Nat) where - val : Nat - le_max : val ≤ max - -theorem bounded_nat_le (b : BoundedNat max) : b.val ≤ max := - b.le_max - --- Proof: zero is always bounded -def zeroBounded (h : 0 < max) : BoundedNat max := - ⟨0, Nat.zero_le max⟩ diff --git a/verification/verification/proofs/tlaplus/StateMachine.tla b/verification/verification/proofs/tlaplus/StateMachine.tla deleted file mode 100644 index 27f2d69..0000000 --- a/verification/verification/proofs/tlaplus/StateMachine.tla +++ /dev/null @@ -1,91 +0,0 @@ ---------------------------- MODULE StateMachine ---------------------------- -(* SPDX-License-Identifier: PMPL-1.0-or-later *) -(* Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) *) -(* *) -(* TLA+ Specification Template: State Machine *) -(* Replace with your project's distributed protocol or state machine. *) -(* Use TLC model checker to verify properties. *) -(* *) -(* Example: A simple request pipeline with safety properties. *) -(* Replace States, Init, Next with your project's actual states. *) -(***************************************************************************) - -EXTENDS Naturals, Sequences, FiniteSets - -CONSTANTS - MaxRequests \* Upper bound on concurrent requests (for model checking) - -VARIABLES - state, \* Current pipeline state - processed, \* Number of processed requests - queue \* Request queue - -vars == <> - -\* Pipeline states — replace with your project's states -States == {"idle", "scanning", "routing", "dispatching", "done", "failed"} - -\* Valid transitions — replace with your project's transition rules -ValidTransition(from, to) == - \/ from = "idle" /\ to = "scanning" - \/ from = "scanning" /\ to = "routing" - \/ from = "scanning" /\ to = "failed" - \/ from = "routing" /\ to = "dispatching" - \/ from = "routing" /\ to = "failed" - \/ from = "dispatching" /\ to = "done" - \/ from = "dispatching" /\ to = "failed" - \/ from = "done" /\ to = "idle" - \/ from = "failed" /\ to = "idle" - -\* Initial state -Init == - /\ state = "idle" - /\ processed = 0 - /\ queue = <<>> - -\* Transition action -Transition(newState) == - /\ ValidTransition(state, newState) - /\ state' = newState - /\ IF newState = "done" - THEN processed' = processed + 1 - ELSE processed' = processed - /\ UNCHANGED queue - -\* Enqueue a request (only when idle or scanning) -Enqueue == - /\ state \in {"idle", "scanning"} - /\ Len(queue) < MaxRequests - /\ queue' = Append(queue, "request") - /\ UNCHANGED <> - -\* Next-state relation -Next == - \/ \E s \in States : Transition(s) - \/ Enqueue - -\* Fairness: the system must eventually process -Spec == Init /\ [][Next]_vars /\ WF_vars(Next) - -\* ---- SAFETY PROPERTIES ---- - -\* State is always valid -TypeInvariant == state \in States - -\* Processed count never decreases (monotonicity) -ProcessedMonotonic == processed >= 0 - -\* Queue never exceeds max -QueueBounded == Len(queue) <= MaxRequests - -\* No impossible transitions (e.g., idle -> done) -NoSkipStates == - [][state' # state => - ValidTransition(state, state')]_state - -\* ---- LIVENESS PROPERTIES ---- - -\* Every request eventually completes or fails -EventualCompletion == <>(state = "done" \/ state = "failed") - -============================================================================ diff --git a/verification/verification/safety_case/0.2-AI-MANIFEST.a2ml b/verification/verification/safety_case/0.2-AI-MANIFEST.a2ml deleted file mode 100644 index 818fba4..0000000 --- a/verification/verification/safety_case/0.2-AI-MANIFEST.a2ml +++ /dev/null @@ -1,12 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later ---- -### [META] -id: "verification-unit-safety_case" -level: 2 -parent: "../0.1-AI-MANIFEST.a2ml" - ---- -### [AI_MANIFEST] -description: | - High-assurance verification unit for safety case. - Critical for safety-of-life and aerospace-grade deployment standards. diff --git a/verification/verification/safety_case/README.adoc b/verification/verification/safety_case/README.adoc deleted file mode 100644 index ffb53bd..0000000 --- a/verification/verification/safety_case/README.adoc +++ /dev/null @@ -1,3 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// Copyright (c) Jonathan D.A. Jewell -= Safety case Unit diff --git a/verification/verification/simulations/0.2-AI-MANIFEST.a2ml b/verification/verification/simulations/0.2-AI-MANIFEST.a2ml deleted file mode 100644 index f40fc1c..0000000 --- a/verification/verification/simulations/0.2-AI-MANIFEST.a2ml +++ /dev/null @@ -1,11 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later ---- -### [META] -id: "simulations-unit" -level: 2 -parent: "../0.1-AI-MANIFEST.a2ml" - ---- -### [AI_MANIFEST] -description: | - Simulations unit for high-rigor verification. diff --git a/verification/verification/simulations/README.adoc b/verification/verification/simulations/README.adoc deleted file mode 100644 index 42e184c..0000000 --- a/verification/verification/simulations/README.adoc +++ /dev/null @@ -1,3 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// Copyright (c) Jonathan D.A. Jewell -= Simulations Unit diff --git a/verification/verification/tests/0.2-AI-MANIFEST.a2ml b/verification/verification/tests/0.2-AI-MANIFEST.a2ml deleted file mode 100644 index 0008fcf..0000000 --- a/verification/verification/tests/0.2-AI-MANIFEST.a2ml +++ /dev/null @@ -1 +0,0 @@ -# AI Manifest - Level 1: tests diff --git a/verification/verification/tests/README.adoc b/verification/verification/tests/README.adoc deleted file mode 100644 index 3930981..0000000 --- a/verification/verification/tests/README.adoc +++ /dev/null @@ -1,3 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// Copyright (c) Jonathan D.A. Jewell -= Tests Unit diff --git a/verification/verification/traceability/0.2-AI-MANIFEST.a2ml b/verification/verification/traceability/0.2-AI-MANIFEST.a2ml deleted file mode 100644 index defa125..0000000 --- a/verification/verification/traceability/0.2-AI-MANIFEST.a2ml +++ /dev/null @@ -1,12 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later ---- -### [META] -id: "verification-unit-traceability" -level: 2 -parent: "../0.1-AI-MANIFEST.a2ml" - ---- -### [AI_MANIFEST] -description: | - High-assurance verification unit for traceability. - Critical for safety-of-life and aerospace-grade deployment standards. diff --git a/verification/verification/traceability/README.adoc b/verification/verification/traceability/README.adoc deleted file mode 100644 index e6e54bc..0000000 --- a/verification/verification/traceability/README.adoc +++ /dev/null @@ -1,3 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// Copyright (c) Jonathan D.A. Jewell -= Traceability Unit diff --git a/www/.well-known/.well-known/ai.txt b/www/.well-known/.well-known/ai.txt deleted file mode 100644 index 6668d66..0000000 --- a/www/.well-known/.well-known/ai.txt +++ /dev/null @@ -1,18 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later -# ai.txt - AI interaction policy -# See: https://site.spawning.ai/spawning-ai-txt - -User-Agent: * -Disallow-Training: yes -Disallow-Summarization: no -Disallow-Generation: yes - -# This project's code is licensed under PMPL-1.0-or-later. -# AI agents may read and analyze this code for assisting contributors. -# AI agents must NOT use this code for model training without explicit consent. -# AI agents must preserve Emotional Lineage per PMPL Section 3. -# -# For AI agent integration instructions, see: -# 0-AI-MANIFEST.a2ml (universal AI entry point) -# AI.a2ml (Claude-specific instructions) -# .machine_readable/ (structured project state) diff --git a/www/.well-known/.well-known/humans.txt b/www/.well-known/.well-known/humans.txt deleted file mode 100644 index 60be6cf..0000000 --- a/www/.well-known/.well-known/humans.txt +++ /dev/null @@ -1,14 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later -# humanstxt.org - -/* TEAM */ -Maintainer: {{AUTHOR}} ({{OWNER}}) -Contact: {{AUTHOR_EMAIL}} -From: United Kingdom - -/* SITE */ -Last update: {{CURRENT_DATE}} -Standards: RSR (Rhodium Standard Repository) -License: PMPL-1.0-or-later (Palimpsest MPL) -Components: Idris2 ABI, Zig FFI -Tools: just, Podman, Guix diff --git a/www/.well-known/.well-known/security.txt b/www/.well-known/.well-known/security.txt deleted file mode 100644 index 93ce46e..0000000 --- a/www/.well-known/.well-known/security.txt +++ /dev/null @@ -1,11 +0,0 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later -# RFC 9116 - security.txt -# https://securitytxt.org/ - -Contact: mailto:{{SECURITY_EMAIL}} -Expires: {{CURRENT_YEAR}}-12-31T23:59:59.000Z -Encryption: {{PGP_KEY_URL}} -Preferred-Languages: en -Canonical: https://{{FORGE}}/{{OWNER}}/{{REPO}}/.well-known/security.txt -Policy: https://{{FORGE}}/{{OWNER}}/{{REPO}}/blob/main/SECURITY.md -Hiring: https://{{WEBSITE}}/careers diff --git a/www/.well-known/README.adoc b/www/.well-known/README.adoc index 822f626..88c2ea1 100644 --- a/www/.well-known/README.adoc +++ b/www/.well-known/README.adoc @@ -1,2 +1,2 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Well-known files for jaffascript (security.txt, ai.txt, etc.) diff --git a/www/.well-known/ai.txt b/www/.well-known/ai.txt index cc7cbc3..b80fa9b 100644 --- a/www/.well-known/ai.txt +++ b/www/.well-known/ai.txt @@ -7,10 +7,9 @@ Disallow-Training: yes Disallow-Summarization: no Disallow-Generation: yes -# This project's code is licensed under PMPL-1.0-or-later. +# This project's code is licensed under MPL-2.0; its prose under CC-BY-SA-4.0. # AI agents may read and analyze this code for assisting contributors. # AI agents must NOT use this code for model training without explicit consent. -# AI agents must preserve Emotional Lineage per PMPL Section 3. # # For AI agent integration instructions, see: # 0-AI-MANIFEST.a2ml (universal AI entry point) diff --git a/www/.well-known/humans.txt b/www/.well-known/humans.txt index f57452c..9af2e56 100644 --- a/www/.well-known/humans.txt +++ b/www/.well-known/humans.txt @@ -9,6 +9,6 @@ From: United Kingdom /* SITE */ Last update: {{CURRENT_DATE}} Standards: RSR (Rhodium Standard Repository) -License: PMPL-1.0-or-later (Palimpsest MPL) +License: MPL-2.0 (code), CC-BY-SA-4.0 (prose) Components: Idris2 ABI, Zig FFI Tools: just, Podman, Guix From 97377c577ca4c75d6a86e3dfe524a4efb26ebad6 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Fri, 9 Oct 2026 00:38:23 +0100 Subject: [PATCH 2/2] chore(licence): move the nested-duplicate removal to its own PR The parent commit also deleted two tracked nested copies, verification/verification/ (28 files) and www/.well-known/.well-known/ (3 files). Those deletions are not part of the licence change, and they took this PR to 115 files, over CodeRabbit's 100-file review limit. This commit restores both trees exactly as they are on main (589e1be). A separate PR deletes them. After this commit the PR changes 84 files, all modified and none deleted, so the squash commit contains only the licence change. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01GpUzjdhWFi26k6s7AWxYcf --- .../verification/0.1-AI-MANIFEST.a2ml | 27 ++++++ verification/verification/README.adoc | 3 + .../benchmarks/0.2-AI-MANIFEST.a2ml | 11 +++ .../verification/benchmarks/README.adoc | 3 + .../coverage/0.2-AI-MANIFEST.a2ml | 12 +++ .../verification/coverage/README.adoc | 3 + .../verification/fuzzing/0.2-AI-MANIFEST.a2ml | 11 +++ verification/verification/fuzzing/README.adoc | 3 + .../verification/proofs/0.2-AI-MANIFEST.a2ml | 11 +++ verification/verification/proofs/README.adoc | 60 ++++++++++++ .../verification/proofs/agda/Properties.agda | 37 ++++++++ .../verification/proofs/coq/TypeSafety.v | 73 +++++++++++++++ .../proofs/idris2/ABI/Compliance.idr | 41 +++++++++ .../proofs/idris2/ABI/Foreign.idr | 53 +++++++++++ .../verification/proofs/idris2/ABI/Layout.idr | 63 +++++++++++++ .../proofs/idris2/ABI/Platform.idr | 63 +++++++++++++ .../proofs/idris2/ABI/Pointers.idr | 52 +++++++++++ .../verification/proofs/idris2/Types.idr | 38 ++++++++ .../verification/proofs/lean4/ApiTypes.lean | 44 +++++++++ .../proofs/tlaplus/StateMachine.tla | 91 +++++++++++++++++++ .../safety_case/0.2-AI-MANIFEST.a2ml | 12 +++ .../verification/safety_case/README.adoc | 3 + .../simulations/0.2-AI-MANIFEST.a2ml | 11 +++ .../verification/simulations/README.adoc | 3 + .../verification/tests/0.2-AI-MANIFEST.a2ml | 1 + verification/verification/tests/README.adoc | 3 + .../traceability/0.2-AI-MANIFEST.a2ml | 12 +++ .../verification/traceability/README.adoc | 3 + www/.well-known/.well-known/ai.txt | 18 ++++ www/.well-known/.well-known/humans.txt | 14 +++ www/.well-known/.well-known/security.txt | 11 +++ 31 files changed, 790 insertions(+) create mode 100644 verification/verification/0.1-AI-MANIFEST.a2ml create mode 100644 verification/verification/README.adoc create mode 100644 verification/verification/benchmarks/0.2-AI-MANIFEST.a2ml create mode 100644 verification/verification/benchmarks/README.adoc create mode 100644 verification/verification/coverage/0.2-AI-MANIFEST.a2ml create mode 100644 verification/verification/coverage/README.adoc create mode 100644 verification/verification/fuzzing/0.2-AI-MANIFEST.a2ml create mode 100644 verification/verification/fuzzing/README.adoc create mode 100644 verification/verification/proofs/0.2-AI-MANIFEST.a2ml create mode 100644 verification/verification/proofs/README.adoc create mode 100644 verification/verification/proofs/agda/Properties.agda create mode 100644 verification/verification/proofs/coq/TypeSafety.v create mode 100644 verification/verification/proofs/idris2/ABI/Compliance.idr create mode 100644 verification/verification/proofs/idris2/ABI/Foreign.idr create mode 100644 verification/verification/proofs/idris2/ABI/Layout.idr create mode 100644 verification/verification/proofs/idris2/ABI/Platform.idr create mode 100644 verification/verification/proofs/idris2/ABI/Pointers.idr create mode 100644 verification/verification/proofs/idris2/Types.idr create mode 100644 verification/verification/proofs/lean4/ApiTypes.lean create mode 100644 verification/verification/proofs/tlaplus/StateMachine.tla create mode 100644 verification/verification/safety_case/0.2-AI-MANIFEST.a2ml create mode 100644 verification/verification/safety_case/README.adoc create mode 100644 verification/verification/simulations/0.2-AI-MANIFEST.a2ml create mode 100644 verification/verification/simulations/README.adoc create mode 100644 verification/verification/tests/0.2-AI-MANIFEST.a2ml create mode 100644 verification/verification/tests/README.adoc create mode 100644 verification/verification/traceability/0.2-AI-MANIFEST.a2ml create mode 100644 verification/verification/traceability/README.adoc create mode 100644 www/.well-known/.well-known/ai.txt create mode 100644 www/.well-known/.well-known/humans.txt create mode 100644 www/.well-known/.well-known/security.txt diff --git a/verification/verification/0.1-AI-MANIFEST.a2ml b/verification/verification/0.1-AI-MANIFEST.a2ml new file mode 100644 index 0000000..39b370f --- /dev/null +++ b/verification/verification/0.1-AI-MANIFEST.a2ml @@ -0,0 +1,27 @@ +# SPDX-License-Identifier: PMPL-1.0-or-later +--- +### [META] +id: "verification-pillar" +level: 1 +parent: "../0-AI-MANIFEST.a2ml" + +--- +### [AI_MANIFEST] +description: | + Primary verification pillar. Contains evidence for correctness, + performance, formal proofs, randomized testing, and aerospace-grade + high-assurance metrics (MC/DC coverage, traceability, safety cases). + +canonical_locations: + tests: "tests/" + benchmarks: "benchmarks/" + proofs: "proofs/" + fuzzing: "fuzzing/" + simulations: "simulations/" + coverage: "coverage/" + traceability: "traceability/" + safety_case: "safety_case/" + +invariants: + - "Evidence MUST be reproducible and documented" + - "High-assurance deployments MUST satisfy traceability and safety_case requirements" diff --git a/verification/verification/README.adoc b/verification/verification/README.adoc new file mode 100644 index 0000000..efa7fb2 --- /dev/null +++ b/verification/verification/README.adoc @@ -0,0 +1,3 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) Jonathan D.A. Jewell += Verification Pillar diff --git a/verification/verification/benchmarks/0.2-AI-MANIFEST.a2ml b/verification/verification/benchmarks/0.2-AI-MANIFEST.a2ml new file mode 100644 index 0000000..6416309 --- /dev/null +++ b/verification/verification/benchmarks/0.2-AI-MANIFEST.a2ml @@ -0,0 +1,11 @@ +# SPDX-License-Identifier: PMPL-1.0-or-later +--- +### [META] +id: "benches-pillar" +level: 2 +parent: "../0.1-AI-MANIFEST.a2ml" + +--- +### [AI_MANIFEST] +description: | + Benches pillar. diff --git a/verification/verification/benchmarks/README.adoc b/verification/verification/benchmarks/README.adoc new file mode 100644 index 0000000..beb83cd --- /dev/null +++ b/verification/verification/benchmarks/README.adoc @@ -0,0 +1,3 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) Jonathan D.A. Jewell += Benchmarks Unit diff --git a/verification/verification/coverage/0.2-AI-MANIFEST.a2ml b/verification/verification/coverage/0.2-AI-MANIFEST.a2ml new file mode 100644 index 0000000..fc15bd3 --- /dev/null +++ b/verification/verification/coverage/0.2-AI-MANIFEST.a2ml @@ -0,0 +1,12 @@ +# SPDX-License-Identifier: PMPL-1.0-or-later +--- +### [META] +id: "verification-unit-coverage" +level: 2 +parent: "../0.1-AI-MANIFEST.a2ml" + +--- +### [AI_MANIFEST] +description: | + High-assurance verification unit for coverage. + Critical for safety-of-life and aerospace-grade deployment standards. diff --git a/verification/verification/coverage/README.adoc b/verification/verification/coverage/README.adoc new file mode 100644 index 0000000..c10a6ac --- /dev/null +++ b/verification/verification/coverage/README.adoc @@ -0,0 +1,3 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) Jonathan D.A. Jewell += Coverage Unit diff --git a/verification/verification/fuzzing/0.2-AI-MANIFEST.a2ml b/verification/verification/fuzzing/0.2-AI-MANIFEST.a2ml new file mode 100644 index 0000000..79c4fef --- /dev/null +++ b/verification/verification/fuzzing/0.2-AI-MANIFEST.a2ml @@ -0,0 +1,11 @@ +# SPDX-License-Identifier: PMPL-1.0-or-later +--- +### [META] +id: "fuzzing-unit" +level: 2 +parent: "../0.1-AI-MANIFEST.a2ml" + +--- +### [AI_MANIFEST] +description: | + Fuzzing unit for high-rigor verification. diff --git a/verification/verification/fuzzing/README.adoc b/verification/verification/fuzzing/README.adoc new file mode 100644 index 0000000..b07ea68 --- /dev/null +++ b/verification/verification/fuzzing/README.adoc @@ -0,0 +1,3 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) Jonathan D.A. Jewell += Fuzzing Unit diff --git a/verification/verification/proofs/0.2-AI-MANIFEST.a2ml b/verification/verification/proofs/0.2-AI-MANIFEST.a2ml new file mode 100644 index 0000000..0e5666f --- /dev/null +++ b/verification/verification/proofs/0.2-AI-MANIFEST.a2ml @@ -0,0 +1,11 @@ +# SPDX-License-Identifier: PMPL-1.0-or-later +--- +### [META] +id: "verification-unit-proofs" +level: 2 +parent: "../0.1-AI-MANIFEST.a2ml" + +--- +### [AI_MANIFEST] +description: | + Sub-unit focusing on proofs. diff --git a/verification/verification/proofs/README.adoc b/verification/verification/proofs/README.adoc new file mode 100644 index 0000000..520f5e9 --- /dev/null +++ b/verification/verification/proofs/README.adoc @@ -0,0 +1,60 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) Jonathan D.A. Jewell += Formal Verification Proofs + +This directory contains formal proofs organised by proof assistant. + +== Directory Structure + +[source] +---- +proofs/ +├── idris2/ # Idris2 proofs (ABI, dependent types) +│ ├── ABI/ # ABI-specific proofs (mandatory) +│ │ ├── Pointers.idr # Non-null pointer safety +│ │ ├── Layout.idr # Memory layout correctness +│ │ ├── Platform.idr # Platform type size proofs +│ │ ├── Foreign.idr # FFI return type proofs +│ │ └── Compliance.idr # C ABI compliance +│ └── Types.idr # Core data type well-formedness +├── lean4/ # Lean4 proofs (algebra, lattices) +│ └── ApiTypes.lean +├── agda/ # Agda proofs (induction, metatheory) +│ └── Properties.agda +├── coq/ # Coq proofs (type systems, compilation) +│ └── TypeSafety.v +└── tlaplus/ # TLA+ specs (distributed protocols) + └── StateMachine.tla +---- + +== Verification Commands + +[source,bash] +---- +just proof-check-all # Run all proof checkers +just proof-check-idris2 # Idris2 only +just proof-check-lean4 # Lean4 only +just proof-check-agda # Agda only +just proof-check-coq # Coq only +---- + +== Banned Patterns + +The following MUST NOT appear in any proof file: + +- `believe_me` (Idris2) +- `assert_total` (Idris2) +- `postulate` (Idris2/Agda) +- `sorry` (Lean4) +- `Admitted` (Coq) +- `unsafeCoerce` (Haskell) + +CI enforces this via `panic-attack assail --proofs-only`. + +== Adding New Proofs + +1. Choose the appropriate prover (see PROOF-NEEDS.md) +2. Create the `.idr`/`.lean`/`.agda`/`.v`/`.tla` file in the right directory +3. Ensure `%default total` (Idris2) or equivalent +4. Run the verification command +5. Update PROOF-STATUS.md diff --git a/verification/verification/proofs/agda/Properties.agda b/verification/verification/proofs/agda/Properties.agda new file mode 100644 index 0000000..90e4c3c --- /dev/null +++ b/verification/verification/proofs/agda/Properties.agda @@ -0,0 +1,37 @@ +-- SPDX-License-Identifier: PMPL-1.0-or-later +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Agda Proof Template: Inductive and coinductive properties +-- Replace with your project's domain-specific proofs. +-- All proofs must be total (no postulate, no {-# TERMINATING #-}). + +module Properties where + +open import Data.Nat using (ℕ; zero; suc; _+_; _≤_; z≤n; s≤s; _<_) +open import Data.Nat.Properties using (+-comm; +-assoc; ≤-refl; ≤-trans) +open import Data.List using (List; []; _∷_; length; _++_) +open import Data.List.Properties using (length-++ ) +open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym; trans) + +-- Example: Proof that list append preserves total length +-- Replace with your project's domain proofs. + +append-length : ∀ {A : Set} (xs ys : List A) → + length (xs ++ ys) ≡ length xs + length ys +append-length xs ys = length-++ xs + +-- Example: Monotonicity proof template +-- Use for state machines, confidence scores, trust levels +record Monotone {A : Set} (_≤A_ : A → A → Set) (f : A → A) : Set where + field + preserves : ∀ {x y} → x ≤A y → f x ≤A f y + +-- Example: Idempotence proof template +-- Use for normalisation, deduplication, formatting +record Idempotent {A : Set} (_≡A_ : A → A → Set) (f : A → A) : Set where + field + idem : ∀ (x : A) → f (f x) ≡A f x + +-- Example: Natural number successor is monotone +suc-monotone : Monotone _≤_ suc +suc-monotone = record { preserves = s≤s } diff --git a/verification/verification/proofs/coq/TypeSafety.v b/verification/verification/proofs/coq/TypeSafety.v new file mode 100644 index 0000000..c2ec6eb --- /dev/null +++ b/verification/verification/proofs/coq/TypeSafety.v @@ -0,0 +1,73 @@ +(* SPDX-License-Identifier: PMPL-1.0-or-later *) +(* Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) *) +(* + Coq Proof Template: Type system soundness + Replace with your project's type system proofs. + All proofs must be complete — NO Admitted allowed. +*) + +Require Import Coq.Lists.List. +Require Import Coq.Arith.Arith. +Require Import Coq.Bool.Bool. +Import ListNotations. + +(** * Example: Simple expression language with type safety *) +(** Replace this entire section with your project's type system. *) + +(** Types *) +Inductive ty : Type := + | TyNat : ty + | TyBool : ty. + +(** Expressions *) +Inductive expr : Type := + | EConst : nat -> expr + | ETrue : expr + | EFalse : expr + | EPlus : expr -> expr -> expr + | EEq : expr -> expr -> expr. + +(** Values *) +Inductive value : Type := + | VNat : nat -> value + | VBool : bool -> value. + +(** Typing relation *) +Inductive has_type : expr -> ty -> Prop := + | T_Const : forall n, has_type (EConst n) TyNat + | T_True : has_type ETrue TyBool + | T_False : has_type EFalse TyBool + | T_Plus : forall e1 e2, + has_type e1 TyNat -> has_type e2 TyNat -> + has_type (EPlus e1 e2) TyNat + | T_Eq : forall e1 e2, + has_type e1 TyNat -> has_type e2 TyNat -> + has_type (EEq e1 e2) TyBool. + +(** Evaluation *) +Inductive eval : expr -> value -> Prop := + | E_Const : forall n, eval (EConst n) (VNat n) + | E_True : eval ETrue (VBool true) + | E_False : eval EFalse (VBool false) + | E_Plus : forall e1 e2 n1 n2, + eval e1 (VNat n1) -> eval e2 (VNat n2) -> + eval (EPlus e1 e2) (VNat (n1 + n2)) + | E_Eq : forall e1 e2 n1 n2, + eval e1 (VNat n1) -> eval e2 (VNat n2) -> + eval (EEq e1 e2) (VBool (Nat.eqb n1 n2)). + +(** Value typing *) +Definition value_has_type (v : value) (t : ty) : Prop := + match v, t with + | VNat _, TyNat => True + | VBool _, TyBool => True + | _, _ => False + end. + +(** Type soundness: well-typed expressions evaluate to well-typed values *) +Theorem type_soundness : forall e t v, + has_type e t -> eval e v -> value_has_type v t. +Proof. + intros e t v Htype Heval. + induction Htype; inversion Heval; subst; simpl; auto. +Qed. diff --git a/verification/verification/proofs/idris2/ABI/Compliance.idr b/verification/verification/proofs/idris2/ABI/Compliance.idr new file mode 100644 index 0000000..b94a5db --- /dev/null +++ b/verification/verification/proofs/idris2/ABI/Compliance.idr @@ -0,0 +1,41 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) Jonathan D.A. Jewell +-- +-- ABI Proof: C ABI compliance +-- Proves that struct layouts are C ABI compliant. +-- All proofs MUST be constructive (no believe_me, no assert_total). + +module ABI.Compliance + +import ABI.Layout +import ABI.Platform + +%default total + +||| Evidence that every field in a layout is correctly aligned. +public export +data AllFieldsAligned : List StructField -> Type where + AFANil : AllFieldsAligned [] + AFACons : FieldAligned f -> AllFieldsAligned fs -> AllFieldsAligned (f :: fs) + +||| Evidence that every field is within the struct bounds. +public export +data AllFieldsInBounds : (size : Nat) -> List StructField -> Type where + AFBNil : AllFieldsInBounds size [] + AFBCons : FieldInBounds size f -> AllFieldsInBounds size fs -> AllFieldsInBounds size (f :: fs) + +||| A struct layout is C ABI compliant when: +||| 1. All fields are aligned to their natural alignment +||| 2. All fields are within bounds of the struct size +||| 3. The struct size is a multiple of the struct alignment +public export +record CABICompliant (layout : StructLayout) where + constructor MkCompliant + fieldsAligned : AllFieldsAligned (layoutFields layout) + fieldsInBounds : AllFieldsInBounds (layoutSize layout) (layoutFields layout) + sizeAligned : modNatNZ (layoutSize layout) (layoutAlignment layout) SIsNonZero = 0 + +||| An empty struct is trivially compliant (size=1, alignment=1). +export +emptyStructCompliant : CABICompliant (MkLayout "empty" [] 1 1) +emptyStructCompliant = MkCompliant AFANil AFBNil Refl diff --git a/verification/verification/proofs/idris2/ABI/Foreign.idr b/verification/verification/proofs/idris2/ABI/Foreign.idr new file mode 100644 index 0000000..1e550dd --- /dev/null +++ b/verification/verification/proofs/idris2/ABI/Foreign.idr @@ -0,0 +1,53 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) Jonathan D.A. Jewell +-- +-- ABI Proof: FFI function return type proofs +-- Proves that all FFI functions return expected types. +-- All proofs MUST be constructive (no believe_me, no assert_total). + +module ABI.Foreign + +%default total + +||| Result type for FFI operations. +||| All FFI functions must return through this type. +public export +data FFIResult : Type -> Type where + FFISuccess : (value : a) -> FFIResult a + FFIError : (code : Int) -> (msg : String) -> FFIResult a + +||| Proof that FFIResult is a functor (map preserves structure). +export +mapFFIResult : (a -> b) -> FFIResult a -> FFIResult b +mapFFIResult f (FFISuccess value) = FFISuccess (f value) +mapFFIResult f (FFIError code msg) = FFIError code msg + +||| Proof that mapping identity preserves the result. +export +mapIdPreserves : (r : FFIResult a) -> mapFFIResult Prelude.id r = r +mapIdPreserves (FFISuccess value) = Refl +mapIdPreserves (FFIError code msg) = Refl + +||| An FFI function specification: name, argument types, return type. +public export +record FFISpec where + constructor MkFFISpec + ffiName : String + ffiReturnType : Type + +||| Proof that an FFI spec has a specific return type. +||| Use this to verify at compile time that FFI functions return the +||| types we expect across the C ABI boundary. +public export +FFIReturns : FFISpec -> Type -> Type +FFIReturns spec ty = ffiReturnType spec = ty + +||| C calling convention marker. +||| Proofs about calling convention compatibility. +public export +data CallingConv = CDecl | StdCall | FastCall + +||| All hyperpolymath FFI uses CDecl. +public export +defaultCallingConv : CallingConv +defaultCallingConv = CDecl diff --git a/verification/verification/proofs/idris2/ABI/Layout.idr b/verification/verification/proofs/idris2/ABI/Layout.idr new file mode 100644 index 0000000..9040a5e --- /dev/null +++ b/verification/verification/proofs/idris2/ABI/Layout.idr @@ -0,0 +1,63 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) Jonathan D.A. Jewell +-- +-- ABI Proof: Memory layout correctness +-- Proves struct size, alignment, and padding properties. +-- All proofs MUST be constructive (no believe_me, no assert_total). + +module ABI.Layout + +%default total + +||| Witness that a type has a known size in bytes at compile time. +public export +interface HasSize (ty : Type) where + sizeOf : Nat + +||| Witness that a type has a known alignment in bytes. +public export +interface HasAlignment (ty : Type) where + alignOf : Nat + +||| Calculate padding needed to reach the next aligned offset. +||| paddingFor offset alignment = bytes to add so (offset + padding) `mod` alignment == 0 +public export +paddingFor : (offset : Nat) -> (alignment : Nat) -> {auto 0 ok : NonZero alignment} -> Nat +paddingFor offset alignment = let r = modNatNZ offset alignment ok + in case r of + Z => Z + (S _) => minus alignment r + +||| Proof that an offset with zero remainder needs zero padding. +export +alignedNeedsPadding : (n : Nat) -> (a : Nat) -> {auto 0 ok : NonZero a} -> + modNatNZ n a ok = 0 -> paddingFor n a = 0 +alignedNeedsPadding n a prf = rewrite prf in Refl + +||| A field within a struct, carrying its offset and size. +public export +record StructField where + constructor MkField + fieldName : String + fieldOffset : Nat + fieldSize : Nat + fieldAlignment : Nat + +||| Proof that a field is correctly aligned within a struct. +public export +FieldAligned : StructField -> Type +FieldAligned f = modNatNZ (fieldOffset f) (fieldAlignment f) SIsNonZero = 0 + +||| Proof that a field does not overflow past a given struct size. +public export +FieldInBounds : (structSize : Nat) -> StructField -> Type +FieldInBounds sz f = LTE (fieldOffset f + fieldSize f) sz + +||| A struct layout is a list of fields with a total size. +public export +record StructLayout where + constructor MkLayout + layoutName : String + layoutFields : List StructField + layoutSize : Nat + layoutAlignment : Nat diff --git a/verification/verification/proofs/idris2/ABI/Platform.idr b/verification/verification/proofs/idris2/ABI/Platform.idr new file mode 100644 index 0000000..a8d6b94 --- /dev/null +++ b/verification/verification/proofs/idris2/ABI/Platform.idr @@ -0,0 +1,63 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) Jonathan D.A. Jewell +-- +-- ABI Proof: Platform-specific type size proofs +-- Proves that C type sizes are correct per platform. +-- All proofs MUST be constructive (no believe_me, no assert_total). + +module ABI.Platform + +%default total + +||| Supported target platforms for ABI verification. +public export +data Platform = Linux64 | LinuxARM64 | MacOS64 | MacOSARM64 + | Windows64 | FreeBSD64 | WASM32 + +||| Pointer size in bytes for each platform. +public export +ptrSize : Platform -> Nat +ptrSize WASM32 = 4 +ptrSize _ = 8 + +||| C `int` size in bytes. +public export +cIntSize : Platform -> Nat +cIntSize _ = 4 + +||| C `size_t` size in bytes (matches pointer size). +public export +cSizeT : Platform -> Nat +cSizeT = ptrSize + +||| Proof that size_t always equals pointer size on all platforms. +export +sizeTEqPtrSize : (p : Platform) -> cSizeT p = ptrSize p +sizeTEqPtrSize _ = Refl + +||| Proof that pointer size is always 4 or 8 bytes. +export +ptrSizeValid : (p : Platform) -> Either (ptrSize p = 4) (ptrSize p = 8) +ptrSizeValid WASM32 = Left Refl +ptrSizeValid Linux64 = Right Refl +ptrSizeValid LinuxARM64 = Right Refl +ptrSizeValid MacOS64 = Right Refl +ptrSizeValid MacOSARM64 = Right Refl +ptrSizeValid Windows64 = Right Refl +ptrSizeValid FreeBSD64 = Right Refl + +||| Proof that C int is always 4 bytes on all platforms. +export +cIntAlways4 : (p : Platform) -> cIntSize p = 4 +cIntAlways4 _ = Refl + +||| Proof that pointer size is always at least 4 bytes. +export +ptrSizeAtLeast4 : (p : Platform) -> LTE 4 (ptrSize p) +ptrSizeAtLeast4 WASM32 = lteRefl +ptrSizeAtLeast4 Linux64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl))) +ptrSizeAtLeast4 LinuxARM64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl))) +ptrSizeAtLeast4 MacOS64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl))) +ptrSizeAtLeast4 MacOSARM64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl))) +ptrSizeAtLeast4 Windows64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl))) +ptrSizeAtLeast4 FreeBSD64 = lteSuccRight (lteSuccRight (lteSuccRight (lteSuccRight lteRefl))) diff --git a/verification/verification/proofs/idris2/ABI/Pointers.idr b/verification/verification/proofs/idris2/ABI/Pointers.idr new file mode 100644 index 0000000..31b6c5f --- /dev/null +++ b/verification/verification/proofs/idris2/ABI/Pointers.idr @@ -0,0 +1,52 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) Jonathan D.A. Jewell +-- +-- ABI Proof: Non-null pointer safety +-- Template proof — customise for your project's pointer types. +-- All proofs MUST be constructive (no believe_me, no assert_total). + +module ABI.Pointers + +import Data.So + +%default total + +||| A pointer value that has been proven non-null. +||| The `So` constraint carries a compile-time witness that `ptr /= 0`. +public export +record SafePtr where + constructor MkSafePtr + ptr : Bits64 + {auto 0 nonNull : So (ptr /= 0)} + +||| Proof that SafePtr can never hold a null (zero) value. +||| This is enforced by the `So` constraint in the record. +export +safePtrNeverNull : (sp : SafePtr) -> So (sp.ptr /= 0) +safePtrNeverNull sp = sp.nonNull + +||| Wrap a raw pointer with a runtime null check. +||| Returns Nothing if the pointer is null. +export +checkPtr : (raw : Bits64) -> Maybe SafePtr +checkPtr 0 = Nothing +checkPtr raw = case choose (raw /= 0) of + Left prf => Just (MkSafePtr raw) + Right _ => Nothing + +||| Proof that checkPtr 0 always returns Nothing. +export +checkPtrZeroIsNothing : checkPtr 0 = Nothing +checkPtrZeroIsNothing = Refl + +||| An opaque handle backed by a non-null pointer. +||| Use this for FFI resource handles (file descriptors, sockets, etc.). +public export +record Handle (tag : String) where + constructor MkHandle + safePtr : SafePtr + +||| Proof that two handles with equal pointers are equal. +export +handlePtrEq : (h1, h2 : Handle tag) -> h1.safePtr.ptr = h2.safePtr.ptr -> h1 = h2 +handlePtrEq (MkHandle (MkSafePtr p)) (MkHandle (MkSafePtr p)) Refl = Refl diff --git a/verification/verification/proofs/idris2/Types.idr b/verification/verification/proofs/idris2/Types.idr new file mode 100644 index 0000000..cc7cce8 --- /dev/null +++ b/verification/verification/proofs/idris2/Types.idr @@ -0,0 +1,38 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) Jonathan D.A. Jewell +-- +-- Typing Proof: Core data type well-formedness +-- Template — replace with your project's core types. +-- All proofs MUST be constructive (no believe_me, no assert_total). + +module Types + +%default total + +||| Example: A bounded natural number (0 to max). +||| Replace with your project's core types. +public export +record Bounded (max : Nat) where + constructor MkBounded + value : Nat + {auto 0 inBounds : LTE value max} + +||| Proof that a Bounded value is always <= max. +export +boundedLeMax : (b : Bounded max) -> LTE b.value max +boundedLeMax b = b.inBounds + +||| Proof that zero is always a valid Bounded value. +export +zeroIsBounded : {max : Nat} -> Bounded (S max) +zeroIsBounded = MkBounded 0 + +||| Example: A non-empty list with a compile-time guarantee. +public export +data NonEmpty : List a -> Type where + IsNonEmpty : NonEmpty (x :: xs) + +||| Proof that cons always produces a non-empty list. +export +consIsNonEmpty : (x : a) -> (xs : List a) -> NonEmpty (x :: xs) +consIsNonEmpty _ _ = IsNonEmpty diff --git a/verification/verification/proofs/lean4/ApiTypes.lean b/verification/verification/proofs/lean4/ApiTypes.lean new file mode 100644 index 0000000..144a943 --- /dev/null +++ b/verification/verification/proofs/lean4/ApiTypes.lean @@ -0,0 +1,44 @@ +-- SPDX-License-Identifier: PMPL-1.0-or-later +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- Typing Proof: Public API type safety +-- Template — replace with your project's API types. +-- Proves properties about exported function signatures. + +-- Example: Result type used across API boundaries +inductive ApiResult (α : Type) where + | ok : α → ApiResult α + | error : Nat → String → ApiResult α + +namespace ApiResult + -- Proof: map preserves structure (functor law: map id = id) + def map (f : α → β) : ApiResult α → ApiResult β + | .ok v => .ok (f v) + | .error c m => .error c m + + theorem map_id : ∀ (r : ApiResult α), map id r = r := by + intro r + cases r with + | ok v => simp [map] + | error c m => simp [map] + + -- Proof: map composition (functor law: map (g ∘ f) = map g ∘ map f) + theorem map_comp (f : α → β) (g : β → γ) : + ∀ (r : ApiResult α), map (g ∘ f) r = map g (map f r) := by + intro r + cases r with + | ok v => simp [map, Function.comp] + | error c m => simp [map] + +-- Example: Bounded confidence value (0.0 to 1.0 modelled as Nat/1000) +-- Replace with your project's numeric invariants +structure BoundedNat (max : Nat) where + val : Nat + le_max : val ≤ max + +theorem bounded_nat_le (b : BoundedNat max) : b.val ≤ max := + b.le_max + +-- Proof: zero is always bounded +def zeroBounded (h : 0 < max) : BoundedNat max := + ⟨0, Nat.zero_le max⟩ diff --git a/verification/verification/proofs/tlaplus/StateMachine.tla b/verification/verification/proofs/tlaplus/StateMachine.tla new file mode 100644 index 0000000..27f2d69 --- /dev/null +++ b/verification/verification/proofs/tlaplus/StateMachine.tla @@ -0,0 +1,91 @@ +--------------------------- MODULE StateMachine ---------------------------- +(* SPDX-License-Identifier: PMPL-1.0-or-later *) +(* Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) *) +(* *) +(* TLA+ Specification Template: State Machine *) +(* Replace with your project's distributed protocol or state machine. *) +(* Use TLC model checker to verify properties. *) +(* *) +(* Example: A simple request pipeline with safety properties. *) +(* Replace States, Init, Next with your project's actual states. *) +(***************************************************************************) + +EXTENDS Naturals, Sequences, FiniteSets + +CONSTANTS + MaxRequests \* Upper bound on concurrent requests (for model checking) + +VARIABLES + state, \* Current pipeline state + processed, \* Number of processed requests + queue \* Request queue + +vars == <> + +\* Pipeline states — replace with your project's states +States == {"idle", "scanning", "routing", "dispatching", "done", "failed"} + +\* Valid transitions — replace with your project's transition rules +ValidTransition(from, to) == + \/ from = "idle" /\ to = "scanning" + \/ from = "scanning" /\ to = "routing" + \/ from = "scanning" /\ to = "failed" + \/ from = "routing" /\ to = "dispatching" + \/ from = "routing" /\ to = "failed" + \/ from = "dispatching" /\ to = "done" + \/ from = "dispatching" /\ to = "failed" + \/ from = "done" /\ to = "idle" + \/ from = "failed" /\ to = "idle" + +\* Initial state +Init == + /\ state = "idle" + /\ processed = 0 + /\ queue = <<>> + +\* Transition action +Transition(newState) == + /\ ValidTransition(state, newState) + /\ state' = newState + /\ IF newState = "done" + THEN processed' = processed + 1 + ELSE processed' = processed + /\ UNCHANGED queue + +\* Enqueue a request (only when idle or scanning) +Enqueue == + /\ state \in {"idle", "scanning"} + /\ Len(queue) < MaxRequests + /\ queue' = Append(queue, "request") + /\ UNCHANGED <> + +\* Next-state relation +Next == + \/ \E s \in States : Transition(s) + \/ Enqueue + +\* Fairness: the system must eventually process +Spec == Init /\ [][Next]_vars /\ WF_vars(Next) + +\* ---- SAFETY PROPERTIES ---- + +\* State is always valid +TypeInvariant == state \in States + +\* Processed count never decreases (monotonicity) +ProcessedMonotonic == processed >= 0 + +\* Queue never exceeds max +QueueBounded == Len(queue) <= MaxRequests + +\* No impossible transitions (e.g., idle -> done) +NoSkipStates == + [][state' # state => + ValidTransition(state, state')]_state + +\* ---- LIVENESS PROPERTIES ---- + +\* Every request eventually completes or fails +EventualCompletion == <>(state = "done" \/ state = "failed") + +============================================================================ diff --git a/verification/verification/safety_case/0.2-AI-MANIFEST.a2ml b/verification/verification/safety_case/0.2-AI-MANIFEST.a2ml new file mode 100644 index 0000000..818fba4 --- /dev/null +++ b/verification/verification/safety_case/0.2-AI-MANIFEST.a2ml @@ -0,0 +1,12 @@ +# SPDX-License-Identifier: PMPL-1.0-or-later +--- +### [META] +id: "verification-unit-safety_case" +level: 2 +parent: "../0.1-AI-MANIFEST.a2ml" + +--- +### [AI_MANIFEST] +description: | + High-assurance verification unit for safety case. + Critical for safety-of-life and aerospace-grade deployment standards. diff --git a/verification/verification/safety_case/README.adoc b/verification/verification/safety_case/README.adoc new file mode 100644 index 0000000..ffb53bd --- /dev/null +++ b/verification/verification/safety_case/README.adoc @@ -0,0 +1,3 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) Jonathan D.A. Jewell += Safety case Unit diff --git a/verification/verification/simulations/0.2-AI-MANIFEST.a2ml b/verification/verification/simulations/0.2-AI-MANIFEST.a2ml new file mode 100644 index 0000000..f40fc1c --- /dev/null +++ b/verification/verification/simulations/0.2-AI-MANIFEST.a2ml @@ -0,0 +1,11 @@ +# SPDX-License-Identifier: PMPL-1.0-or-later +--- +### [META] +id: "simulations-unit" +level: 2 +parent: "../0.1-AI-MANIFEST.a2ml" + +--- +### [AI_MANIFEST] +description: | + Simulations unit for high-rigor verification. diff --git a/verification/verification/simulations/README.adoc b/verification/verification/simulations/README.adoc new file mode 100644 index 0000000..42e184c --- /dev/null +++ b/verification/verification/simulations/README.adoc @@ -0,0 +1,3 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) Jonathan D.A. Jewell += Simulations Unit diff --git a/verification/verification/tests/0.2-AI-MANIFEST.a2ml b/verification/verification/tests/0.2-AI-MANIFEST.a2ml new file mode 100644 index 0000000..0008fcf --- /dev/null +++ b/verification/verification/tests/0.2-AI-MANIFEST.a2ml @@ -0,0 +1 @@ +# AI Manifest - Level 1: tests diff --git a/verification/verification/tests/README.adoc b/verification/verification/tests/README.adoc new file mode 100644 index 0000000..3930981 --- /dev/null +++ b/verification/verification/tests/README.adoc @@ -0,0 +1,3 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) Jonathan D.A. Jewell += Tests Unit diff --git a/verification/verification/traceability/0.2-AI-MANIFEST.a2ml b/verification/verification/traceability/0.2-AI-MANIFEST.a2ml new file mode 100644 index 0000000..defa125 --- /dev/null +++ b/verification/verification/traceability/0.2-AI-MANIFEST.a2ml @@ -0,0 +1,12 @@ +# SPDX-License-Identifier: PMPL-1.0-or-later +--- +### [META] +id: "verification-unit-traceability" +level: 2 +parent: "../0.1-AI-MANIFEST.a2ml" + +--- +### [AI_MANIFEST] +description: | + High-assurance verification unit for traceability. + Critical for safety-of-life and aerospace-grade deployment standards. diff --git a/verification/verification/traceability/README.adoc b/verification/verification/traceability/README.adoc new file mode 100644 index 0000000..e6e54bc --- /dev/null +++ b/verification/verification/traceability/README.adoc @@ -0,0 +1,3 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) Jonathan D.A. Jewell += Traceability Unit diff --git a/www/.well-known/.well-known/ai.txt b/www/.well-known/.well-known/ai.txt new file mode 100644 index 0000000..6668d66 --- /dev/null +++ b/www/.well-known/.well-known/ai.txt @@ -0,0 +1,18 @@ +# SPDX-License-Identifier: PMPL-1.0-or-later +# ai.txt - AI interaction policy +# See: https://site.spawning.ai/spawning-ai-txt + +User-Agent: * +Disallow-Training: yes +Disallow-Summarization: no +Disallow-Generation: yes + +# This project's code is licensed under PMPL-1.0-or-later. +# AI agents may read and analyze this code for assisting contributors. +# AI agents must NOT use this code for model training without explicit consent. +# AI agents must preserve Emotional Lineage per PMPL Section 3. +# +# For AI agent integration instructions, see: +# 0-AI-MANIFEST.a2ml (universal AI entry point) +# AI.a2ml (Claude-specific instructions) +# .machine_readable/ (structured project state) diff --git a/www/.well-known/.well-known/humans.txt b/www/.well-known/.well-known/humans.txt new file mode 100644 index 0000000..60be6cf --- /dev/null +++ b/www/.well-known/.well-known/humans.txt @@ -0,0 +1,14 @@ +# SPDX-License-Identifier: PMPL-1.0-or-later +# humanstxt.org + +/* TEAM */ +Maintainer: {{AUTHOR}} ({{OWNER}}) +Contact: {{AUTHOR_EMAIL}} +From: United Kingdom + +/* SITE */ +Last update: {{CURRENT_DATE}} +Standards: RSR (Rhodium Standard Repository) +License: PMPL-1.0-or-later (Palimpsest MPL) +Components: Idris2 ABI, Zig FFI +Tools: just, Podman, Guix diff --git a/www/.well-known/.well-known/security.txt b/www/.well-known/.well-known/security.txt new file mode 100644 index 0000000..93ce46e --- /dev/null +++ b/www/.well-known/.well-known/security.txt @@ -0,0 +1,11 @@ +# SPDX-License-Identifier: PMPL-1.0-or-later +# RFC 9116 - security.txt +# https://securitytxt.org/ + +Contact: mailto:{{SECURITY_EMAIL}} +Expires: {{CURRENT_YEAR}}-12-31T23:59:59.000Z +Encryption: {{PGP_KEY_URL}} +Preferred-Languages: en +Canonical: https://{{FORGE}}/{{OWNER}}/{{REPO}}/.well-known/security.txt +Policy: https://{{FORGE}}/{{OWNER}}/{{REPO}}/blob/main/SECURITY.md +Hiring: https://{{WEBSITE}}/careers