iseriser: normalize licensing to MPL-2.0 (code) + CC-BY-SA-4.0 (docs)#68
Merged
Merged
Conversation
The hand-written Idris2 ABI was never compiler-checked and did not
typecheck under Idris2 0.7.0. Make the foundation real and machine-verified.
Layout.idr
- Discharge the two open holes: ?fieldsAlignedProof and ?offsetInBoundsProof.
- Add a sound decDivides decision procedure (builds genuine m = k*n
witnesses) and decFieldsAligned; checkCABI now returns a real
CABICompliant proof or an error.
- offsetInBounds had an unsound signature (claimed every field fits any
layout); make it an honest decidable Maybe.
- Fix paddingFor (Nat has no Neg; use minus) and give the three concrete
struct layouts explicit alignment witnesses.
- Replace alignUpCorrect's non-compiling Refl proof with a sound
alignUpDivides decision; the general lemma is noted as residual work.
Types.idr
- FullyResolved and GenerationComplete carried no obligation; give them
real So-proofs (no {{/}} markers remain; all seven categories present).
- thisPlatform was a %runElab stub needing ElabReflection; make it total.
- DecEq Result used `No absurd` with no Uninhabited instance; discharge
the off-diagonal cases explicitly.
- createHandle left the auto So (ptr /= 0) unsolved; use choose.
Proofs.idr (new)
- Machine-checked theorems: the three concrete FFI struct layouts are
provably C-ABI aligned; Result→C-int pins; generation-completeness.
Structure / tooling
- Move ABI into src/interface/abi/Iseriser/ABI/ so it builds as an Idris2
package (matches the chapeliser layout); add iseriser-abi.ipkg.
- Add `just proofs` recipe; ignore Idris build artifacts.
- verification/proofs/ now documents and points at the verified proofs.
Verified: `idris2 --build iseriser-abi.ipkg` clean (0 warnings);
cargo test green (57 unit + 9 integration).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA
The governance/licence-consistency check requires an SPDX-License-Identifier header on the LICENSE file and a `license` field in the manifest. The LICENSE body is MPL-2.0 text, so stamp `SPDX-License-Identifier: MPL-2.0` (matching the actual body) and set `license = "MPL-2.0"` (replacing `license-file`). Verified with standards/scripts/check-licence-consistency.sh (passes). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA
Make the repo's licensing story single and consistent: code/config under MPL-2.0, documentation prose under CC-BY-SA-4.0, with both full texts in LICENSES/ and the MPL-2.0 LICENSE at root for GitHub's licence chip. - README: replace the PMPL-1.0/Palimpsest-Covenant badges and the "Licensed under the Palimpsest License" footer with MPL-2.0 (code) + CC-BY-SA-4.0 (docs) badges/text linking LICENSES/. - dep5: add a docs carve-out (*.adoc, *.md, docs/**) -> CC-BY-SA-4.0 so the two-SPDX split is actually encoded (was *-> MPL-2.0 with no docs split). - Remove contradictory self-licence claims from QUICKSTART-MAINTAINER.adoc, docs/RSR_OUTLINE.adoc, docs/STATE-VISUALIZER.adoc, rhodibot.yml comments, and the two Trustfile LICENSE-content checks. - Preserve legitimate non-self references: cargo-deny's AGPL deny-list, the "never use AGPL" estate policy, and the Contributor Covenant CoC. Verified: standards/scripts/check-licence-consistency.sh passes. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Reference implementation of the estate licensing normalization (to be propagated family-wide). Makes iseriser's licensing single and consistent: code/config = MPL-2.0, documentation prose = CC-BY-SA-4.0, both full texts in
LICENSES/, MPL-2.0LICENSEat root so GitHub's licence chip shows MPL-2.0.Changes
PMPL-1.0-or-laterbadge + "Palimpsest Covenant" badge + "Licensed under the Palimpsest License" footer with MPL-2.0 (code) + CC-BY-SA-4.0 (docs) badges/text linkingLICENSES/.*.adoc,*.md,docs/**) →CC-BY-SA-4.0so the two-SPDX split is actually encoded (was*→ MPL-2.0 with no docs split).QUICKSTART-MAINTAINER.adoc,docs/RSR_OUTLINE.adoc,docs/STATE-VISUALIZER.adoc,rhodibot.ymlcomments, and the twoTrustfile.a2mlLICENSE-content checks.Deliberately preserved (not self-claims)
AGPLdeny-list (dependency policy);copilot-instructions.md/AGENTIC.a2ml;Verification
standards/scripts/check-licence-consistency.sh iseriser→ all[OK], passes.Note
The two pre-existing CI reds (rust-ci
toolchaininput bug; Hypatia baseline) are unrelated to this change and were present before #67.🤖 Generated with Claude Code
Generated by Claude Code