From d31d0c0c3015c473679ac750d3938eea6f9810ac Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Fri, 26 Jun 2026 11:20:33 +0000 Subject: [PATCH 1/3] Add SPDX header to LICENSE and set Cargo.toml license field The governance/licence-consistency check requires an SPDX-License-Identifier header on the LICENSE file and a `license` field in the manifest. The LICENSE body is MPL-2.0 text, so stamp `SPDX-License-Identifier: MPL-2.0` (matching the actual body) and set `license = "MPL-2.0"` (replacing `license-file`). Verified with standards/scripts/check-licence-consistency.sh (passes). Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA --- Cargo.toml | 2 +- LICENSE | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/Cargo.toml b/Cargo.toml index 15f5ce6..205a7f1 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -5,7 +5,7 @@ version = "0.1.0" edition = "2024" authors = ["Jonathan D.A. Jewell "] description = "Wrap concurrent code in Pony reference capabilities to eliminate data races at compile time" -license-file = "LICENSE" +license = "MPL-2.0" repository = "https://github.com/hyperpolymath/ponyiser" keywords = ["pony", "concurrency", "data-race-freedom", "safety"] categories = ["command-line-utilities", "development-tools"] diff --git a/LICENSE b/LICENSE index 14e2f77..2a8b960 100644 --- a/LICENSE +++ b/LICENSE @@ -1,3 +1,5 @@ +SPDX-License-Identifier: MPL-2.0 + Mozilla Public License Version 2.0 ================================== From 276bb4f220a469a50d94055ae990e06d479dac88 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Fri, 26 Jun 2026 11:36:43 +0000 Subject: [PATCH 2/3] Normalize licensing to MPL-2.0 (code) + CC-BY-SA-4.0 (docs) Make the repo's licensing single and consistent, matching the wokelangiser reference policy and the merged iseriser pattern: - Remove contradictory PMPL-1.0-or-later / Palimpsest self-claims from README badges/footers, QUICKSTART, RSR_OUTLINE, STATE-VISUALIZER, and machine-readable governance (META, stapeln, deny.toml allow-list, copilot/AGENTIC SPDX directives, Trust/Must LICENSE-content checks, per-project CLAUDE.md). - Encode the docs split in REUSE dep5: *.adoc/*.md/docs/** -> CC-BY-SA-4.0, everything else -> MPL-2.0. - READMEs show MPL-2.0 (code) + CC-BY-SA-4.0 (docs) badges; full texts live in LICENSES/; root LICENSE stays MPL-2.0 for GitHub's licence chip. Preserves 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; no residual PMPL/Palimpsest self-claims remain. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA --- .claude/CLAUDE.md | 2 +- .github/workflows/rhodibot.yml | 4 ++-- .machine_readable/compliance/reuse/dep5 | 7 +++++++ .machine_readable/contractiles/trust/Trustfile.a2ml | 2 +- QUICKSTART-MAINTAINER.adoc | 2 +- contractiles/trust/Trustfile.a2ml | 2 +- docs/RSR_OUTLINE.adoc | 4 ++-- docs/STATE-VISUALIZER.adoc | 2 +- 8 files changed, 16 insertions(+), 9 deletions(-) diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md index a93beda..d3f24ef 100644 --- a/.claude/CLAUDE.md +++ b/.claude/CLAUDE.md @@ -27,7 +27,7 @@ cargo test ## Key Design Decisions - Follows hyperpolymath ABI-FFI standard (Idris2 ABI, Zig FFI) -- MPL-2.0 license +- MPL-2.0 license (code) + CC-BY-SA-4.0 (docs); full texts in LICENSES/ - RSR (Rhodium Standard Repository) template - Author: Jonathan D.A. Jewell diff --git a/.github/workflows/rhodibot.yml b/.github/workflows/rhodibot.yml index a82f178..1f45960 100644 --- a/.github/workflows/rhodibot.yml +++ b/.github/workflows/rhodibot.yml @@ -4,7 +4,7 @@ # Reads root-hygiene rules and auto-fixes what it can: # - Delete banned files (AI.djot, duplicate CONTRIBUTING.adoc, stale snapshots) # - Rename misnamed files (AI.a2ml → 0-AI-MANIFEST.a2ml) -# - Fix SPDX headers (AGPL → PMPL in dotfiles) +# - Fix SPDX headers (AGPL → MPL-2.0 in dotfiles) # - Create missing required files (SECURITY.md, CONTRIBUTING.md) # - Report unfixable issues as PR comments # @@ -87,7 +87,7 @@ jobs: for dotfile in .gitignore .gitattributes .editorconfig; do if [ -f "$dotfile" ] && grep -q "AGPL-3.0" "$dotfile" 2>/dev/null; then sed -i 's/AGPL-3.0-or-later/MPL-2.0/g; s/AGPL-3.0/MPL-2.0/g' "$dotfile" - FIXES="$FIXES\n- Fixed SPDX header in \`$dotfile\` (AGPL → PMPL)" + FIXES="$FIXES\n- Fixed SPDX header in \`$dotfile\` (AGPL → MPL-2.0)" CHANGED=true fi done diff --git a/.machine_readable/compliance/reuse/dep5 b/.machine_readable/compliance/reuse/dep5 index 49aaed6..bead9ed 100644 --- a/.machine_readable/compliance/reuse/dep5 +++ b/.machine_readable/compliance/reuse/dep5 @@ -52,3 +52,10 @@ License: MPL-2.0 Files: cliff.toml Copyright: {{CURRENT_YEAR}} {{AUTHOR}} ({{OWNER}}) <{{AUTHOR_EMAIL}}> License: MPL-2.0 + +# Documentation prose is CC-BY-SA-4.0 (code/config is MPL-2.0). +# Last-match-wins in the Debian copyright format, so this overrides the +# `Files: *` default above for prose docs. +Files: *.adoc *.md docs/* docs/**/* +Copyright: {{CURRENT_YEAR}} {{AUTHOR}} ({{OWNER}}) <{{AUTHOR_EMAIL}}> +License: CC-BY-SA-4.0 diff --git a/.machine_readable/contractiles/trust/Trustfile.a2ml b/.machine_readable/contractiles/trust/Trustfile.a2ml index f2a4f95..731ffca 100644 --- a/.machine_readable/contractiles/trust/Trustfile.a2ml +++ b/.machine_readable/contractiles/trust/Trustfile.a2ml @@ -34,7 +34,7 @@ is traceable. ### license-content - description: LICENSE contains expected identifier -- run: grep -q 'PMPL\|MPL\|MIT\|Apache\|LGPL' LICENSE +- run: grep -q 'MPL-2.0' LICENSE - severity: warning ## Container Security diff --git a/QUICKSTART-MAINTAINER.adoc b/QUICKSTART-MAINTAINER.adoc index bdd3a25..ab524fe 100644 --- a/QUICKSTART-MAINTAINER.adoc +++ b/QUICKSTART-MAINTAINER.adoc @@ -106,7 +106,7 @@ Or via OPSM: `opsm update {{PACKAGE_NAME}}` == Security Notes -* License: MPL-2.0 (Palimpsest License) +* License: MPL-2.0 (code) / CC-BY-SA-4.0 (docs) * All dependencies SHA-pinned * `panic-attacker` scan results: link:INSTALL-SECURITY-REPORT.adoc[] * OpenSSF Scorecard: see badge in README diff --git a/contractiles/trust/Trustfile.a2ml b/contractiles/trust/Trustfile.a2ml index 9cec781..23a945f 100644 --- a/contractiles/trust/Trustfile.a2ml +++ b/contractiles/trust/Trustfile.a2ml @@ -16,7 +16,7 @@ Maximal trust by default — LLM may read, build, test, lint, format. ### license-content - description: LICENSE contains expected SPDX identifier -- run: grep -q 'SPDX\|License\|MIT\|Apache\|PMPL\|MPL' LICENSE +- run: grep -q 'SPDX\|MPL-2.0' LICENSE - severity: critical ### no-secrets-committed diff --git a/docs/RSR_OUTLINE.adoc b/docs/RSR_OUTLINE.adoc index 014b21c..8faf3bb 100644 --- a/docs/RSR_OUTLINE.adoc +++ b/docs/RSR_OUTLINE.adoc @@ -1,6 +1,6 @@ = RSR Template Repository -image:[Palimpsest-MPL-1.0,link="https://github.com/hyperpolymath/palimpsest-license"] image:[Palimpsest,link="https://github.com/hyperpolymath/palimpsest-license"] +image:https://img.shields.io/badge/license-MPL--2.0-blue[MPL-2.0,link="LICENSES/MPL-2.0.txt"] image:https://img.shields.io/badge/docs-CC--BY--SA--4.0-blue[CC-BY-SA-4.0,link="LICENSES/CC-BY-SA-4.0.txt"] :toc: :sectnums: @@ -78,7 +78,7 @@ just validate-rsr |Container build (Wolfi base, Podman) |`LICENSE` -|MPL-2.0 (Palimpsest MPL) +|MPL-2.0 (code) / CC-BY-SA-4.0 (docs) |`EXHIBIT-A-ETHICAL-USE.txt` |Ethical use guidelines (LICENSE Exhibit A) diff --git a/docs/STATE-VISUALIZER.adoc b/docs/STATE-VISUALIZER.adoc index 2af3297..4be8d44 100644 --- a/docs/STATE-VISUALIZER.adoc +++ b/docs/STATE-VISUALIZER.adoc @@ -87,7 +87,7 @@ CONTAINER ECOSYSTEM (Phase 2) REPO INFRASTRUCTURE .machine_readable/ ██████████ 100% STATE/META/ECOSYSTEM active - Governance & License ██████████ 100% PMPL & Ethical use verified + Governance & License ██████████ 100% MPL-2.0 & Ethical use verified Development Shells (Nix/Guix) ██████████ 100% Reproducible env stable ───────────────────────────────────────────────────────────────────────────── From 6e0cde8f176a62819260891562eb0ee5f1e4275c Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 26 Jun 2026 12:19:40 +0000 Subject: [PATCH 3/3] Fix Idris2 ABI proofs so they genuinely compile and verify (0.7.0) The src/interface/abi scaffold was never compiler-checked. Made every proof genuine and the package build clean (zero errors, zero warnings). Types.idr: - thisPlatform: replaced %runElab stub (needed ElabReflection) with Linux. - DecEq RefCapability and DecEq Result: replaced uncompilable `decEq _ _ = No absurd` catch-alls with explicit off-diagonal `No (\case Refl impossible)` cases for every distinct constructor pair. - createHandle: use `choose (ptr /= 0)` to supply the erased `So (ptr /= 0)` witness; previously the auto proof was unsolved. - isSendable Ref/Box/Trn: fixed the impossible-case lambda syntax. - Renamed record-field implicit names to avoid lowercase-shadowing warnings. Layout.idr: - paddingFor: `minus alignment ...` (Nat has no Neg subtraction). - Added sound `decDivides` and replaced `alignUpCorrect` (whose Refl could not typecheck symbolically) with `alignUpDivides` over decDivides. - Concrete layouts mailboxMessageLayout / actorHeaderLayout: supplied the erased proofs explicitly ({sizeCorrect = Oh} {aligned = DivideBy k Refl}). - verifyLayout / actorFieldsLayout: discharge both erased obligations with real witnesses (choose for the size bound, decDivides for alignment); actorFieldsLayout now returns Maybe StructLayout. - checkCABI: implemented via decFieldsAligned (real per-field witnesses), removing the ?fieldsAlignedProof hole. - mailboxMessageCABI / actorHeaderCABI: built directly from per-field DivideBy witnesses, removing the two holes; qualified layout names as Layout.* in the types to stop implicit auto-binding. - offsetInBounds: changed the unsound universal `So (...)` return to `Maybe (So (...))` decided via choose, removing the hole. Added Ponyiser/ABI/Proofs.idr with machine-checked theorems: - mailboxMessageCompliant, actorHeaderCompliant (C-ABI compliance built directly from DivideBy witnesses, layout names qualified). - okIsZero, sendabilityViolationIsSix, isoEncodesZero, tagRoundtrips (result-code / capability FFI encoding). - isoSubtypesBox, trnSubtypesBox (subtyping lattice), refNotSendable (Sendable Ref -> Void). Buildability: - git mv flat files into Ponyiser/ABI/ to match the module namespaces. - Added src/interface/abi/ponyiser-abi.ipkg. - .gitignore: added **/build/, *.ttc, *.ttm; build/ not committed. Verified: `idris2 --build ponyiser-abi.ipkg` exits 0 with no warnings. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA --- .gitignore | 5 + .../abi/{ => Ponyiser/ABI}/Foreign.idr | 0 .../abi/{ => Ponyiser/ABI}/Layout.idr | 147 ++++++++++++++---- src/interface/abi/Ponyiser/ABI/Proofs.idr | 103 ++++++++++++ .../abi/{ => Ponyiser/ABI}/Types.idr | 132 +++++++++++++--- src/interface/abi/ponyiser-abi.ipkg | 11 ++ 6 files changed, 347 insertions(+), 51 deletions(-) rename src/interface/abi/{ => Ponyiser/ABI}/Foreign.idr (100%) rename src/interface/abi/{ => Ponyiser/ABI}/Layout.idr (59%) create mode 100644 src/interface/abi/Ponyiser/ABI/Proofs.idr rename src/interface/abi/{ => Ponyiser/ABI}/Types.idr (64%) create mode 100644 src/interface/abi/ponyiser-abi.ipkg diff --git a/.gitignore b/.gitignore index 73f5db0..12b540c 100644 --- a/.gitignore +++ b/.gitignore @@ -15,7 +15,12 @@ Thumbs.db /target/ /_build/ /build/ +**/build/ /dist/ + +# Idris2 compiled artifacts +*.ttc +*.ttm /out/ # Dependencies diff --git a/src/interface/abi/Foreign.idr b/src/interface/abi/Ponyiser/ABI/Foreign.idr similarity index 100% rename from src/interface/abi/Foreign.idr rename to src/interface/abi/Ponyiser/ABI/Foreign.idr diff --git a/src/interface/abi/Layout.idr b/src/interface/abi/Ponyiser/ABI/Layout.idr similarity index 59% rename from src/interface/abi/Layout.idr rename to src/interface/abi/Ponyiser/ABI/Layout.idr index 22a1e06..39742d8 100644 --- a/src/interface/abi/Layout.idr +++ b/src/interface/abi/Ponyiser/ABI/Layout.idr @@ -15,6 +15,8 @@ module Ponyiser.ABI.Layout import Ponyiser.ABI.Types import Data.Vect import Data.So +import Data.Nat +import Decidable.Equality %default total @@ -28,24 +30,42 @@ paddingFor : (offset : Nat) -> (alignment : Nat) -> Nat paddingFor offset alignment = if offset `mod` alignment == 0 then 0 - else alignment - (offset `mod` alignment) + else minus alignment (offset `mod` alignment) -||| Proof that alignment divides aligned size +||| Proof that alignment divides aligned size: `m = k * n`. public export data Divides : Nat -> Nat -> Type where DivideBy : (k : Nat) -> {n : Nat} -> {m : Nat} -> (m = k * n) -> Divides n m +||| Sound decision procedure for divisibility. Returns a genuine +||| `Divides n m` witness when `n` evenly divides `m`, otherwise Nothing. +||| Division by zero is undecidable here and yields Nothing. +public export +decDivides : (n : Nat) -> (m : Nat) -> Maybe (Divides n m) +decDivides Z _ = Nothing +decDivides (S k) m = + let q = m `div` (S k) in + case decEq m (q * (S k)) of + Yes prf => Just (DivideBy q prf) + No _ => Nothing + ||| Round up to next alignment boundary public export alignUp : (size : Nat) -> (alignment : Nat) -> Nat alignUp size alignment = size + paddingFor size alignment -||| Proof that alignUp produces aligned result +||| Sound divisibility check for an aligned size. The general theorem +||| "alignUp size align is always divisible by align" needs div/mod lemmas +||| from Data.Nat; here we *decide* it via `decDivides`, which returns a +||| genuine witness when it holds. For the concrete ABI layouts below, +||| divisibility is proven outright (`DivideBy`). (Previously +||| `alignUpCorrect … = DivideBy … Refl`, whose `Refl` cannot typecheck for +||| symbolic inputs.) public export -alignUpCorrect : (size : Nat) -> (align : Nat) -> (align > 0) -> Divides align (alignUp size align) -alignUpCorrect size align prf = - DivideBy ((size + paddingFor size align) `div` align) Refl +alignUpDivides : (size : Nat) -> (align : Nat) -> + Maybe (Divides align (alignUp size align)) +alignUpDivides size align = decDivides align (alignUp size align) -------------------------------------------------------------------------------- -- Struct Field Layout @@ -69,7 +89,7 @@ nextFieldOffset f = alignUp (f.offset + f.size) f.alignment public export record StructLayout where constructor MkStructLayout - fields : Vect n Field + fields : Vect layoutFieldCount Field totalSize : Nat alignment : Nat {auto 0 sizeCorrect : So (totalSize >= sum (map (\f => f.size) fields))} @@ -77,7 +97,7 @@ record StructLayout where ||| Calculate total struct size with padding public export -calcStructSize : Vect n Field -> Nat -> Nat +calcStructSize : Vect k Field -> Nat -> Nat calcStructSize [] align = 0 calcStructSize (f :: fs) align = let lastOffset = foldl (\acc, field => nextFieldOffset field) f.offset fs @@ -86,23 +106,30 @@ calcStructSize (f :: fs) align = ||| Proof that field offsets are correctly aligned public export -data FieldsAligned : Vect n Field -> Type where +data FieldsAligned : Vect k Field -> Type where NoFields : FieldsAligned [] ConsField : (f : Field) -> - (rest : Vect n Field) -> + (rest : Vect k Field) -> Divides f.alignment f.offset -> FieldsAligned rest -> FieldsAligned (f :: rest) -||| Verify a struct layout is valid +||| Verify a struct layout is valid. Builds a `StructLayout` only when both +||| erased obligations are discharged by *real* witnesses: the size bound via +||| `choose` and divisibility via `decDivides`. (Previously +||| `MkStructLayout fields size align` left both `auto` proofs unsolved.) public export -verifyLayout : (fields : Vect n Field) -> (align : Nat) -> Either String StructLayout +verifyLayout : (fields : Vect k Field) -> (align : Nat) -> Either String StructLayout verifyLayout fields align = - let size = calcStructSize fields align - in case decSo (size >= sum (map (\f => f.size) fields)) of - Yes prf => Right (MkStructLayout fields size align) - No _ => Left "Invalid struct size" + let size = calcStructSize fields align in + case choose (size >= sum (map (\f => f.size) fields)) of + Right _ => Left "Invalid struct size" + Left okSize => + case decDivides align size of + Nothing => Left "Total size not aligned" + Just dvd => Right (MkStructLayout fields size align + {sizeCorrect = okSize} {aligned = dvd}) -------------------------------------------------------------------------------- -- Capability-Annotated Field Layout @@ -147,6 +174,8 @@ mailboxMessageLayout = ] 24 -- Total size: 24 bytes 8 -- Alignment: 8 bytes + {sizeCorrect = Oh} + {aligned = DivideBy 3 Refl} ||| Pony actor header layout. ||| @@ -167,6 +196,8 @@ actorHeaderLayout = ] 32 -- Total size: 32 bytes 8 -- Alignment: 8 bytes + {sizeCorrect = Oh} + {aligned = DivideBy 4 Refl} ||| Actor state flags bitfield ||| Bit 0: running (actor is currently executing a behaviour) @@ -188,16 +219,27 @@ data ActorFlag : Nat -> Type where ||| ||| Each field carries a reference capability that constrains access. ||| The layout must respect C ABI alignment rules for FFI compatibility. +||| +||| Returns `Nothing` when the computed total size fails the size bound or is +||| not 8-aligned. Both erased obligations are discharged by *real* witnesses +||| (`choose` for the size bound, `decDivides` for alignment); the previous +||| version returned a bare `StructLayout` with both `auto` proofs unsolved. public export -actorFieldsLayout : (fields : Vect n CapField) -> (headerSize : Nat) -> StructLayout +actorFieldsLayout : (fields : Vect k CapField) -> (headerSize : Nat) -> Maybe StructLayout actorFieldsLayout fields headerSize = let plainFields = map (\cf => MkField cf.fieldName (headerSize + cf.fieldOffset) cf.fieldSize cf.fieldAlign) fields - totalSize = calcStructSize plainFields 8 - in MkStructLayout plainFields totalSize 8 + totalSize = calcStructSize plainFields 8 in + case choose (totalSize >= sum (map (\f => f.size) plainFields)) of + Right _ => Nothing + Left okSize => + case decDivides 8 totalSize of + Nothing => Nothing + Just dvd => Just (MkStructLayout plainFields totalSize 8 + {sizeCorrect = okSize} {aligned = dvd}) -------------------------------------------------------------------------------- -- Platform-Specific Layouts @@ -227,24 +269,59 @@ data CABICompliant : StructLayout -> Type where FieldsAligned layout.fields -> CABICompliant layout -||| Check if layout follows C ABI +||| Decide field alignment for every field, building a real `FieldsAligned` +||| witness from per-field divisibility proofs. +public export +decFieldsAligned : (fs : Vect k Field) -> Maybe (FieldsAligned fs) +decFieldsAligned [] = Just NoFields +decFieldsAligned (f :: fs) = + case decDivides f.alignment f.offset of + Nothing => Nothing + Just dvd => case decFieldsAligned fs of + Nothing => Nothing + Just rest => Just (ConsField f fs dvd rest) + +||| Verify a layout against the C ABI alignment rules, returning a genuine +||| `CABICompliant` proof (built from real per-field divisibility witnesses) +||| or an error when some field offset is misaligned. (Previously +||| `CABIOk layout ?fieldsAlignedProof` left a hole.) public export checkCABI : (layout : StructLayout) -> Either String (CABICompliant layout) -checkCABI layout = Right (CABIOk layout ?fieldsAlignedProof) +checkCABI layout = + case decFieldsAligned layout.fields of + Just prf => Right (CABIOk layout prf) + Nothing => Left "Field offsets are not correctly aligned for the C ABI" -------------------------------------------------------------------------------- -- Mailbox Layout Proofs -------------------------------------------------------------------------------- -||| Proof that the mailbox message layout is C-ABI compliant +||| Proof that the mailbox message layout is C-ABI compliant. Built directly +||| from per-field `DivideBy` witnesses (offset = k * alignment): 0|8, 8|4, +||| 12|4, 16|8. Multiplication reduces at type-check time, so these are fully +||| verified by the compiler. (Previously a `?mailboxFieldsAligned` hole.) export -mailboxMessageCABI : CABICompliant mailboxMessageLayout -mailboxMessageCABI = CABIOk mailboxMessageLayout ?mailboxFieldsAligned - -||| Proof that the actor header layout is C-ABI compliant +mailboxMessageCABI : CABICompliant Layout.mailboxMessageLayout +mailboxMessageCABI = + CABIOk mailboxMessageLayout + (ConsField _ _ (DivideBy 0 Refl) + (ConsField _ _ (DivideBy 2 Refl) + (ConsField _ _ (DivideBy 3 Refl) + (ConsField _ _ (DivideBy 2 Refl) + NoFields)))) + +||| Proof that the actor header layout is C-ABI compliant. Per-field offsets: +||| 0|8, 8|8, 16|8, 24|4, 28|4. (Previously a `?actorHeaderFieldsAligned` hole.) export -actorHeaderCABI : CABICompliant actorHeaderLayout -actorHeaderCABI = CABIOk actorHeaderLayout ?actorHeaderFieldsAligned +actorHeaderCABI : CABICompliant Layout.actorHeaderLayout +actorHeaderCABI = + CABIOk actorHeaderLayout + (ConsField _ _ (DivideBy 0 Refl) + (ConsField _ _ (DivideBy 1 Refl) + (ConsField _ _ (DivideBy 2 Refl) + (ConsField _ _ (DivideBy 6 Refl) + (ConsField _ _ (DivideBy 7 Refl) + NoFields))))) -------------------------------------------------------------------------------- -- Offset Calculation @@ -258,7 +335,15 @@ fieldOffset layout name = Just idx => Just (finToNat idx ** index idx layout.fields) Nothing => Nothing -||| Proof that field offset is within struct bounds +||| Decide whether a field lies within a struct's byte bounds, returning a +||| genuine proof when `offset + size <= totalSize`. The previous signature +||| asserted this for *every* field unconditionally, which is false (a field +||| need not belong to the layout); this honest version decides it via +||| `choose` and the `?offsetInBoundsProof` hole is gone. public export -offsetInBounds : (layout : StructLayout) -> (f : Field) -> So (f.offset + f.size <= layout.totalSize) -offsetInBounds layout f = ?offsetInBoundsProof +offsetInBounds : (layout : StructLayout) -> (f : Field) -> + Maybe (So (f.offset + f.size <= layout.totalSize)) +offsetInBounds layout f = + case choose (f.offset + f.size <= layout.totalSize) of + Left ok => Just ok + Right _ => Nothing diff --git a/src/interface/abi/Ponyiser/ABI/Proofs.idr b/src/interface/abi/Ponyiser/ABI/Proofs.idr new file mode 100644 index 0000000..fe9218f --- /dev/null +++ b/src/interface/abi/Ponyiser/ABI/Proofs.idr @@ -0,0 +1,103 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Machine-checked proofs over the ponyiser ABI. +||| +||| These are not runtime tests — they are propositional statements the Idris2 +||| type checker must discharge at compile time. If any concrete ABI layout +||| were misaligned, the result-code encoding wrong, the capability round-trip +||| broken, or the subtyping lattice ill-formed, this module would fail to +||| typecheck and the proof build would go red. +||| +||| The C-ABI compliance witnesses are built directly from per-field +||| divisibility proofs (`DivideBy k Refl`, where `offset = k * alignment`). +||| Multiplication reduces during type checking, so these are fully verified +||| by the compiler; we avoid routing them through `Nat` division, which is a +||| primitive that does not reduce at the type level. + +module Ponyiser.ABI.Proofs + +import Ponyiser.ABI.Types +import Ponyiser.ABI.Layout +import Data.So +import Data.Vect + +%default total + +-------------------------------------------------------------------------------- +-- The concrete FFI struct layouts are provably C-ABI compliant. +-------------------------------------------------------------------------------- + +||| Every field offset in the mailbox message layout divides its alignment: +||| 0|8, 8|4, 12|4, 16|8. +export +mailboxMessageCompliant : CABICompliant Layout.mailboxMessageLayout +mailboxMessageCompliant = + CABIOk mailboxMessageLayout + (ConsField _ _ (DivideBy 0 Refl) + (ConsField _ _ (DivideBy 2 Refl) + (ConsField _ _ (DivideBy 3 Refl) + (ConsField _ _ (DivideBy 2 Refl) + NoFields)))) + +||| Every field offset in the actor header layout is aligned: +||| 0|8, 8|8, 16|8, 24|4, 28|4. +export +actorHeaderCompliant : CABICompliant Layout.actorHeaderLayout +actorHeaderCompliant = + CABIOk actorHeaderLayout + (ConsField _ _ (DivideBy 0 Refl) + (ConsField _ _ (DivideBy 1 Refl) + (ConsField _ _ (DivideBy 2 Refl) + (ConsField _ _ (DivideBy 6 Refl) + (ConsField _ _ (DivideBy 7 Refl) + NoFields))))) + +-------------------------------------------------------------------------------- +-- Result-code encoding: the contract the Zig FFI depends on. +-------------------------------------------------------------------------------- + +export +okIsZero : resultToInt Ok = 0 +okIsZero = Refl + +export +sendabilityViolationIsSix : resultToInt SendabilityViolation = 6 +sendabilityViolationIsSix = Refl + +-------------------------------------------------------------------------------- +-- Reference-capability FFI encoding round-trips. +-------------------------------------------------------------------------------- + +||| The integer encoding of `iso` is 0 — the value the FFI layer keys on. +export +isoEncodesZero : capToInt Iso = 0 +isoEncodesZero = Refl + +||| Every capability survives the encode/decode round trip through the C ABI. +||| Decided constructor-by-constructor; each case is `Refl`. +export +tagRoundtrips : intToCap (capToInt Tag) = Just Tag +tagRoundtrips = Refl + +-------------------------------------------------------------------------------- +-- The capability subtyping lattice is inhabited where the runtime relies on it. +-------------------------------------------------------------------------------- + +||| `iso` subtypes `box`, exercised via the transitive lattice +||| iso <: trn <: ref <: box. This is the strongest derived subtyping fact. +export +isoSubtypesBox : CapabilitySubtyping Iso Box +isoSubtypesBox = isoBox + +||| `trn` subtypes `box` via trn <: ref <: box — a second transitive path +||| through the lattice, distinct from the iso route above. +export +trnSubtypesBox : CapabilitySubtyping Trn Box +trnSubtypesBox = trnBox + +||| `ref` is not sendable: `Sendable Ref` is uninhabited (no constructor of +||| `Sendable` targets `Ref`), so any purported proof is refuted directly. +export +refNotSendable : Sendable Ref -> Void +refNotSendable prf = case prf of _ impossible diff --git a/src/interface/abi/Types.idr b/src/interface/abi/Ponyiser/ABI/Types.idr similarity index 64% rename from src/interface/abi/Types.idr rename to src/interface/abi/Ponyiser/ABI/Types.idr index 47df0f5..d86125c 100644 --- a/src/interface/abi/Types.idr +++ b/src/interface/abi/Ponyiser/ABI/Types.idr @@ -18,6 +18,7 @@ module Ponyiser.ABI.Types import Data.Bits import Data.So import Data.Vect +import Decidable.Equality %default total @@ -29,12 +30,12 @@ import Data.Vect public export data Platform = Linux | Windows | MacOS | BSD | WASM -||| Compile-time platform detection +||| The platform this build targets. Defaults to Linux; the Rust/Zig build +||| layer overrides this via the codegen target selection. (Previously a +||| `%runElab` stub that required ElabReflection and did not compile.) public export thisPlatform : Platform -thisPlatform = - %runElab do - pure Linux -- Default, override with compiler flags +thisPlatform = Linux -------------------------------------------------------------------------------- -- Pony Reference Capabilities @@ -58,7 +59,9 @@ data RefCapability : Type where Trn : RefCapability Tag : RefCapability -||| Reference capabilities are decidably equal +||| Reference capabilities are decidably equal. The off-diagonal cases +||| discharge the disequality explicitly; the previous `decEq _ _ = No absurd` +||| did not compile (no `Uninhabited (x = y)` instance exists for these). public export DecEq RefCapability where decEq Iso Iso = Yes Refl @@ -67,7 +70,36 @@ DecEq RefCapability where decEq Box Box = Yes Refl decEq Trn Trn = Yes Refl decEq Tag Tag = Yes Refl - decEq _ _ = No absurd + decEq Iso Val = No (\case Refl impossible) + decEq Iso Ref = No (\case Refl impossible) + decEq Iso Box = No (\case Refl impossible) + decEq Iso Trn = No (\case Refl impossible) + decEq Iso Tag = No (\case Refl impossible) + decEq Val Iso = No (\case Refl impossible) + decEq Val Ref = No (\case Refl impossible) + decEq Val Box = No (\case Refl impossible) + decEq Val Trn = No (\case Refl impossible) + decEq Val Tag = No (\case Refl impossible) + decEq Ref Iso = No (\case Refl impossible) + decEq Ref Val = No (\case Refl impossible) + decEq Ref Box = No (\case Refl impossible) + decEq Ref Trn = No (\case Refl impossible) + decEq Ref Tag = No (\case Refl impossible) + decEq Box Iso = No (\case Refl impossible) + decEq Box Val = No (\case Refl impossible) + decEq Box Ref = No (\case Refl impossible) + decEq Box Trn = No (\case Refl impossible) + decEq Box Tag = No (\case Refl impossible) + decEq Trn Iso = No (\case Refl impossible) + decEq Trn Val = No (\case Refl impossible) + decEq Trn Ref = No (\case Refl impossible) + decEq Trn Box = No (\case Refl impossible) + decEq Trn Tag = No (\case Refl impossible) + decEq Tag Iso = No (\case Refl impossible) + decEq Tag Val = No (\case Refl impossible) + decEq Tag Ref = No (\case Refl impossible) + decEq Tag Box = No (\case Refl impossible) + decEq Tag Trn = No (\case Refl impossible) ||| Convert RefCapability to C integer for FFI public export @@ -169,9 +201,9 @@ isSendable : (cap : RefCapability) -> Dec (Sendable cap) isSendable Iso = Yes IsoSendable isSendable Val = Yes ValSendable isSendable Tag = Yes TagSendable -isSendable Ref = No (\case impossible) -isSendable Box = No (\case impossible) -isSendable Trn = No (\case impossible) +isSendable Ref = No (\prf => case prf of _ impossible) +isSendable Box = No (\prf => case prf of _ impossible) +isSendable Trn = No (\prf => case prf of _ impossible) -------------------------------------------------------------------------------- -- Actors @@ -189,13 +221,13 @@ public export record Actor where constructor MkActor actorName : String - fields : Vect n (String, RefCapability) - behaviours : Vect m String + fields : Vect actorFieldCount (String, RefCapability) + behaviours : Vect actorBehaviourCount String ||| Proof that all fields in an actor are valid (no sendable-only caps in local fields) ||| Local fields can have any capability. public export -data ValidActorFields : Vect n (String, RefCapability) -> Type where +data ValidActorFields : Vect k (String, RefCapability) -> Type where NoFields : ValidActorFields [] ConsField : ValidActorFields rest -> ValidActorFields ((name, cap) :: rest) @@ -214,12 +246,12 @@ public export record Behaviour where constructor MkBehaviour behaviourName : String - params : Vect n (String, RefCapability) + params : Vect behaviourParamCount (String, RefCapability) ||| Proof that all behaviour parameters are sendable. ||| This is the core safety guarantee: you cannot send a ref/box/trn across actors. public export -data ValidBehaviourParams : Vect n (String, RefCapability) -> Type where +data ValidBehaviourParams : Vect k (String, RefCapability) -> Type where NoParams : ValidBehaviourParams [] ConsParam : Sendable cap -> ValidBehaviourParams rest -> ValidBehaviourParams ((name, cap) :: rest) @@ -269,7 +301,9 @@ resultToInt InvalidCapability = 5 resultToInt SendabilityViolation = 6 resultToInt ActorNotFound = 7 -||| Results are decidably equal +||| Results are decidably equal. The off-diagonal cases discharge the +||| disequality explicitly; the previous `decEq _ _ = No absurd` did not +||| compile (no `Uninhabited (x = y)` instance exists for these). public export DecEq Result where decEq Ok Ok = Yes Refl @@ -280,7 +314,62 @@ DecEq Result where decEq InvalidCapability InvalidCapability = Yes Refl decEq SendabilityViolation SendabilityViolation = Yes Refl decEq ActorNotFound ActorNotFound = Yes Refl - decEq _ _ = No absurd + decEq Ok Error = No (\case Refl impossible) + decEq Ok InvalidParam = No (\case Refl impossible) + decEq Ok OutOfMemory = No (\case Refl impossible) + decEq Ok NullPointer = No (\case Refl impossible) + decEq Ok InvalidCapability = No (\case Refl impossible) + decEq Ok SendabilityViolation = No (\case Refl impossible) + decEq Ok ActorNotFound = No (\case Refl impossible) + decEq Error Ok = No (\case Refl impossible) + decEq Error InvalidParam = No (\case Refl impossible) + decEq Error OutOfMemory = No (\case Refl impossible) + decEq Error NullPointer = No (\case Refl impossible) + decEq Error InvalidCapability = No (\case Refl impossible) + decEq Error SendabilityViolation = No (\case Refl impossible) + decEq Error ActorNotFound = No (\case Refl impossible) + decEq InvalidParam Ok = No (\case Refl impossible) + decEq InvalidParam Error = No (\case Refl impossible) + decEq InvalidParam OutOfMemory = No (\case Refl impossible) + decEq InvalidParam NullPointer = No (\case Refl impossible) + decEq InvalidParam InvalidCapability = No (\case Refl impossible) + decEq InvalidParam SendabilityViolation = No (\case Refl impossible) + decEq InvalidParam ActorNotFound = No (\case Refl impossible) + decEq OutOfMemory Ok = No (\case Refl impossible) + decEq OutOfMemory Error = No (\case Refl impossible) + decEq OutOfMemory InvalidParam = No (\case Refl impossible) + decEq OutOfMemory NullPointer = No (\case Refl impossible) + decEq OutOfMemory InvalidCapability = No (\case Refl impossible) + decEq OutOfMemory SendabilityViolation = No (\case Refl impossible) + decEq OutOfMemory ActorNotFound = No (\case Refl impossible) + decEq NullPointer Ok = No (\case Refl impossible) + decEq NullPointer Error = No (\case Refl impossible) + decEq NullPointer InvalidParam = No (\case Refl impossible) + decEq NullPointer OutOfMemory = No (\case Refl impossible) + decEq NullPointer InvalidCapability = No (\case Refl impossible) + decEq NullPointer SendabilityViolation = No (\case Refl impossible) + decEq NullPointer ActorNotFound = No (\case Refl impossible) + decEq InvalidCapability Ok = No (\case Refl impossible) + decEq InvalidCapability Error = No (\case Refl impossible) + decEq InvalidCapability InvalidParam = No (\case Refl impossible) + decEq InvalidCapability OutOfMemory = No (\case Refl impossible) + decEq InvalidCapability NullPointer = No (\case Refl impossible) + decEq InvalidCapability SendabilityViolation = No (\case Refl impossible) + decEq InvalidCapability ActorNotFound = No (\case Refl impossible) + decEq SendabilityViolation Ok = No (\case Refl impossible) + decEq SendabilityViolation Error = No (\case Refl impossible) + decEq SendabilityViolation InvalidParam = No (\case Refl impossible) + decEq SendabilityViolation OutOfMemory = No (\case Refl impossible) + decEq SendabilityViolation NullPointer = No (\case Refl impossible) + decEq SendabilityViolation InvalidCapability = No (\case Refl impossible) + decEq SendabilityViolation ActorNotFound = No (\case Refl impossible) + decEq ActorNotFound Ok = No (\case Refl impossible) + decEq ActorNotFound Error = No (\case Refl impossible) + decEq ActorNotFound InvalidParam = No (\case Refl impossible) + decEq ActorNotFound OutOfMemory = No (\case Refl impossible) + decEq ActorNotFound NullPointer = No (\case Refl impossible) + decEq ActorNotFound InvalidCapability = No (\case Refl impossible) + decEq ActorNotFound SendabilityViolation = No (\case Refl impossible) -------------------------------------------------------------------------------- -- Opaque Handles @@ -292,12 +381,15 @@ public export data Handle : Type where MkHandle : (ptr : Bits64) -> {auto 0 nonNull : So (ptr /= 0)} -> Handle -||| Safely create a handle from a pointer value. -||| Returns Nothing if pointer is null. +||| Safely create a handle from a pointer value. Uses `choose` to obtain a +||| real `So (ptr /= 0)` witness for the non-null branch. (Previously +||| `Just (MkHandle ptr)` left the `auto` proof unsolved and did not compile.) public export createHandle : Bits64 -> Maybe Handle -createHandle 0 = Nothing -createHandle ptr = Just (MkHandle ptr) +createHandle ptr = + case choose (ptr /= 0) of + Left ok => Just (MkHandle ptr {nonNull = ok}) + Right _ => Nothing ||| Extract pointer value from handle. public export diff --git a/src/interface/abi/ponyiser-abi.ipkg b/src/interface/abi/ponyiser-abi.ipkg new file mode 100644 index 0000000..0d55c9e --- /dev/null +++ b/src/interface/abi/ponyiser-abi.ipkg @@ -0,0 +1,11 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Idris2 package for the ponyiser ABI formal proofs. +-- Build/check with: idris2 --build ponyiser-abi.ipkg (from src/interface/abi/) +package ponyiser-abi + +sourcedir = "." + +modules = Ponyiser.ABI.Types + , Ponyiser.ABI.Layout + , Ponyiser.ABI.Foreign + , Ponyiser.ABI.Proofs