From 55bd3035ed784dfbd38c0daa402f8aaf7edf9795 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Fri, 26 Jun 2026 11:20:29 +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 2c3c974..07f4ff9 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -5,7 +5,7 @@ version = "0.1.0" edition = "2024" authors = ["Jonathan D.A. Jewell "] description = "Wrap C codebases in ATS linear types for zero-cost memory safety without rewrites" -license-file = "LICENSE" +license = "MPL-2.0" repository = "https://github.com/hyperpolymath/atsiser" keywords = ["ats", "linear-types", "memory-safety", "c-interop"] 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 0436d585ca0bf98d07cc50a141862a94adcc08be Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Fri, 26 Jun 2026 11:36:22 +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/must/Mustfile.a2ml | 2 +- .machine_readable/contractiles/trust/Trustfile.a2ml | 4 ++-- contractiles/trust/Trustfile.a2ml | 2 +- docs/RSR_OUTLINE.adoc | 4 ++-- docs/STATE-VISUALIZER.adoc | 2 +- 8 files changed, 17 insertions(+), 10 deletions(-) diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md index ffe5eb8..b23b9e0 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/must/Mustfile.a2ml b/.machine_readable/contractiles/must/Mustfile.a2ml index e7bdf36..9c13ea2 100644 --- a/.machine_readable/contractiles/must/Mustfile.a2ml +++ b/.machine_readable/contractiles/must/Mustfile.a2ml @@ -57,7 +57,7 @@ These are hard requirements — CI fails if any check fails. - severity: warning ### no-agpl -- description: No AGPL-3.0 references (superseded by PMPL) +- description: No AGPL-3.0 references (superseded by MPL-2.0) - run: "! grep -r 'AGPL-3.0' .gitignore .gitattributes .editorconfig 2>/dev/null | head -1 | grep -q ." - severity: critical diff --git a/.machine_readable/contractiles/trust/Trustfile.a2ml b/.machine_readable/contractiles/trust/Trustfile.a2ml index dd33a53..9667f5a 100644 --- a/.machine_readable/contractiles/trust/Trustfile.a2ml +++ b/.machine_readable/contractiles/trust/Trustfile.a2ml @@ -33,8 +33,8 @@ is traceable. - severity: warning ### license-content -- description: LICENSE contains PMPL identifier -- run: grep -q 'PMPL' LICENSE +- description: LICENSE contains MPL-2.0 identifier +- run: grep -q 'MPL-2.0' LICENSE - severity: warning ### ci-pipeline-present diff --git a/contractiles/trust/Trustfile.a2ml b/contractiles/trust/Trustfile.a2ml index 7961db6..b5c097e 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 7850d5839e3ce08e94d82083acb9c4d5ff470029 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 26 Jun 2026 13:39:51 +0000 Subject: [PATCH 3/3] Fix Idris2 ABI proofs to genuinely compile and verify under 0.7.0 Make the scaffolded src/interface/abi proofs typecheck cleanly (zero errors, zero warnings) under Idris2 0.7.0, with genuine machine-checked proofs. Types.idr: - Replace %runElab thisPlatform (needs ElabReflection) with plain Linux value. - Replace the non-compiling DecEq Result catch-all (No absurd) with explicit off-diagonal No (\case Refl impossible) for every distinct constructor pair. - Fix createHandle to discharge the {auto So (ptr /= 0)} proof via choose. - Drop unmatchable CInt/CSize cases in cSizeOf/cAlignOf (type synonyms reduce to Bits32/Bits64, already covered). - import Decidable.Equality. Layout.idr: - paddingFor: use minus alignment (mod ...) (Nat has no Neg). - Add sound decDivides : (n m : Nat) -> Maybe (Divides n m) via div + decEq. - Replace unsound alignUpCorrect (Refl over division, Bool-typed bound) with a decision returning Maybe (Divides align (alignUp size align)). - Implement checkCABI via decFieldsAligned (no ?fieldsAlignedProof hole). - verifyLayout: discharge both MkStructLayout obligations with real witnesses (choose for size bound, decDivides for alignment). - offsetInBounds: change unsound universal So return to Maybe (So ...) via choose. - Supply explicit erased proofs {sizeCorrect = Oh} {aligned = DivideBy 2 Refl} on exampleOwnedLayout and exampleBorrowedLayout. - Rename shadowing lowercase n -> len to clear implicit-bind warnings. - import Data.Nat, Decidable.Equality. Proofs.idr (new): machine-checked theorems - exampleOwnedCompliant, exampleBorrowedCompliant : CABICompliant built directly with one DivideBy per field (offset = k * alignment). - okIsZero, errorIsOne, okNotBounds pin the result-code encoding. Build: move flat files to Atsiser/ABI/ nested layout; add atsiser-abi.ipkg. Add **/build/, *.ttc, *.ttm to .gitignore. No believe_me/postulate/holes. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA --- .gitignore | 3 + .../abi/{ => Atsiser/ABI}/Foreign.idr | 0 .../abi/{ => Atsiser/ABI}/Layout.idr | 82 +++++++++++++++---- src/interface/abi/Atsiser/ABI/Proofs.idr | 65 +++++++++++++++ src/interface/abi/{ => Atsiser/ABI}/Types.idr | 65 ++++++++++++--- src/interface/abi/atsiser-abi.ipkg | 9 ++ 6 files changed, 194 insertions(+), 30 deletions(-) rename src/interface/abi/{ => Atsiser/ABI}/Foreign.idr (100%) rename src/interface/abi/{ => Atsiser/ABI}/Layout.idr (71%) create mode 100644 src/interface/abi/Atsiser/ABI/Proofs.idr rename src/interface/abi/{ => Atsiser/ABI}/Types.idr (77%) create mode 100644 src/interface/abi/atsiser-abi.ipkg diff --git a/.gitignore b/.gitignore index 73f5db0..f539f3d 100644 --- a/.gitignore +++ b/.gitignore @@ -15,6 +15,9 @@ Thumbs.db /target/ /_build/ /build/ +**/build/ +*.ttc +*.ttm /dist/ /out/ diff --git a/src/interface/abi/Foreign.idr b/src/interface/abi/Atsiser/ABI/Foreign.idr similarity index 100% rename from src/interface/abi/Foreign.idr rename to src/interface/abi/Atsiser/ABI/Foreign.idr diff --git a/src/interface/abi/Layout.idr b/src/interface/abi/Atsiser/ABI/Layout.idr similarity index 71% rename from src/interface/abi/Layout.idr rename to src/interface/abi/Atsiser/ABI/Layout.idr index ddf27df..e678b43 100644 --- a/src/interface/abi/Layout.idr +++ b/src/interface/abi/Atsiser/ABI/Layout.idr @@ -16,6 +16,8 @@ module Atsiser.ABI.Layout import Atsiser.ABI.Types import Data.Vect import Data.So +import Data.Nat +import Decidable.Equality %default total @@ -29,24 +31,39 @@ 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 public export data Divides : Nat -> Nat -> Type where DivideBy : (k : Nat) -> {n : Nat} -> {m : Nat} -> (m = k * n) -> Divides n m +||| Sound decision procedure: does `n` divide `m`? +||| For n = S k, compute the quotient and check m = q * (S k) by decidable +||| equality. Division does not reduce during typechecking, so the equation +||| is genuinely checked at runtime rather than asserted. +public export +decDivides : (n : Nat) -> (m : Nat) -> Maybe (Divides n m) +decDivides Z _ = Nothing +decDivides (S k) m = + let q = div m (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 +||| Decide that `alignUp size align` is divisible by `align`. +||| Returns a genuine `Divides` witness when the quotient checks out, and +||| `Nothing` otherwise (e.g. align = 0). A `Refl`-only proof is impossible +||| here because division does not reduce during typechecking. 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 +alignUpCorrect : (size : Nat) -> (align : Nat) -> Maybe (Divides align (alignUp size align)) +alignUpCorrect size align = decDivides align (alignUp size align) -------------------------------------------------------------------------------- -- Ownership-Annotated Fields @@ -109,7 +126,7 @@ ownedFieldCount layout = length (filter requiresOwnershipTracking (toList layout ||| Calculate total struct size with padding public export -calcStructSize : Vect n Field -> Nat -> Nat +calcStructSize : Vect len Field -> Nat -> Nat calcStructSize [] align = 0 calcStructSize (f :: fs) align = let lastOffset = foldl (\acc, field => nextFieldOffset field) f.offset fs @@ -118,23 +135,30 @@ calcStructSize (f :: fs) align = ||| Proof that field offsets are correctly aligned public export -data FieldsAligned : Vect n Field -> Type where +data FieldsAligned : Vect len Field -> Type where NoFields : FieldsAligned [] ConsField : (f : Field) -> - (rest : Vect n Field) -> + (rest : Vect len Field) -> Divides f.alignment f.offset -> FieldsAligned rest -> FieldsAligned (f :: rest) -||| Verify a struct layout is valid +||| Verify a struct layout is valid. +||| Both erased obligations of `MkStructLayout` are discharged with genuine +||| witnesses: the size bound via `choose`, and `Divides align size` via +||| `decDivides`. If either fails to hold for the computed size, we report an +||| error instead of fabricating a proof. public export -verifyLayout : (name : String) -> (fields : Vect n Field) -> (align : Nat) -> Either String StructLayout +verifyLayout : (name : String) -> (fields : Vect len Field) -> (align : Nat) -> Either String StructLayout verifyLayout name fields align = - let size = calcStructSize fields align - in case decSo (size >= sum (map (\f => f.size) fields)) of - Yes prf => Right (MkStructLayout name fields size align) - No _ => Left "Invalid struct size for \{name}" + let size = calcStructSize fields align in + case choose (size >= sum (map (\f => f.size) fields)) of + Right _ => Left "Invalid struct size for \{name}" + Left szOk => case decDivides align size of + Nothing => Left "Total size of \{name} is not aligned to \{show align}" + Just dvd => Right (MkStructLayout name fields size align + {sizeCorrect = szOk} {aligned = dvd}) -------------------------------------------------------------------------------- -- Platform-Specific Layouts @@ -165,11 +189,25 @@ data CABICompliant : StructLayout -> Type where FieldsAligned layout.fields -> CABICompliant layout +||| Decide whether every field's offset is aligned to its alignment, +||| building a FieldsAligned witness over the whole vector. +public export +decFieldsAligned : (fields : Vect len Field) -> Maybe (FieldsAligned fields) +decFieldsAligned [] = Just NoFields +decFieldsAligned (f :: rest) = + case decDivides f.alignment f.offset of + Nothing => Nothing + Just dvd => case decFieldsAligned rest of + Nothing => Nothing + Just restPrf => Just (ConsField f rest dvd restPrf) + ||| Check if layout follows C ABI public export checkCABI : (layout : StructLayout) -> Either String (CABICompliant layout) checkCABI layout = - Right (CABIOk layout ?fieldsAlignedProof) + case decFieldsAligned layout.fields of + Just prf => Right (CABIOk layout prf) + Nothing => Left "Struct \{layout.structName} has misaligned fields" -------------------------------------------------------------------------------- -- Ownership Graph for Structs @@ -216,6 +254,8 @@ exampleOwnedLayout = ] 16 -- Total size: 16 bytes 8 -- Alignment: 8 bytes + {sizeCorrect = Oh} + {aligned = DivideBy 2 Refl} -- 16 = 2 * 8 ||| Example: Layout for a struct with a borrowed pointer. ||| This is what atsiser generates when it finds: @@ -231,6 +271,8 @@ exampleBorrowedLayout = ] 16 -- Total size: 16 bytes (with padding) 8 -- Alignment: 8 bytes + {sizeCorrect = Oh} + {aligned = DivideBy 2 Refl} -- 16 = 2 * 8 -------------------------------------------------------------------------------- -- Offset Calculation @@ -244,7 +286,11 @@ 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's offset+size fits within the struct's total size. +||| Returns a proof when the bound holds, Nothing otherwise (it does not hold +||| in general, so a universally-quantified return type would be unsound). 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/Atsiser/ABI/Proofs.idr b/src/interface/abi/Atsiser/ABI/Proofs.idr new file mode 100644 index 0000000..a971ad7 --- /dev/null +++ b/src/interface/abi/Atsiser/ABI/Proofs.idr @@ -0,0 +1,65 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Machine-checked theorems about the Atsiser ABI. +||| +||| These theorems pin down properties that the rest of the ABI relies on: +||| * the example struct layouts are genuinely C-ABI compliant +||| (every field offset is a multiple of its alignment), and +||| * the result-code encoding agrees with the C contract. +||| +||| Each compliance witness is built DIRECTLY (one `DivideBy` per field), +||| because multiplication reduces during typechecking while division does +||| not — so these are checked, not asserted. + +module Atsiser.ABI.Proofs + +import Atsiser.ABI.Types +import Atsiser.ABI.Layout +import Data.Vect + +%default total + +-------------------------------------------------------------------------------- +-- Struct Layout Compliance +-------------------------------------------------------------------------------- + +||| `exampleOwnedLayout` follows the C ABI: field `data` at offset 0 (= 0 * 8) +||| and field `len` at offset 8 (= 1 * 8) are both aligned to 8. +export +exampleOwnedCompliant : CABICompliant Layout.exampleOwnedLayout +exampleOwnedCompliant = + CABIOk Layout.exampleOwnedLayout + (ConsField _ _ (DivideBy 0 Refl) -- data: offset 0 = 0 * 8 + (ConsField _ _ (DivideBy 1 Refl) -- len: offset 8 = 1 * 8 + NoFields)) + +||| `exampleBorrowedLayout` follows the C ABI: field `name` at offset 0 (= 0 * 8) +||| aligned to 8, and field `flags` at offset 8 (= 2 * 4) aligned to 4. +export +exampleBorrowedCompliant : CABICompliant Layout.exampleBorrowedLayout +exampleBorrowedCompliant = + CABIOk Layout.exampleBorrowedLayout + (ConsField _ _ (DivideBy 0 Refl) -- name: offset 0 = 0 * 8 + (ConsField _ _ (DivideBy 2 Refl) -- flags: offset 8 = 2 * 4 + NoFields)) + +-------------------------------------------------------------------------------- +-- Result-Code Encoding +-------------------------------------------------------------------------------- + +||| The success code encodes to 0, as the C FFI contract requires. +export +okIsZero : resultToInt Ok = 0 +okIsZero = Refl + +||| The generic-error code encodes to 1, distinct from success. +export +errorIsOne : resultToInt Error = 1 +errorIsOne = Refl + +||| The result encoding is injective on the two codes that the FFI layer +||| branches on most: success and bounds violation map to different integers. +export +okNotBounds : Not (resultToInt Ok = resultToInt BoundsViolation) +okNotBounds = \case Refl impossible diff --git a/src/interface/abi/Types.idr b/src/interface/abi/Atsiser/ABI/Types.idr similarity index 77% rename from src/interface/abi/Types.idr rename to src/interface/abi/Atsiser/ABI/Types.idr index 8401e4b..4c6fd17 100644 --- a/src/interface/abi/Types.idr +++ b/src/interface/abi/Atsiser/ABI/Types.idr @@ -17,6 +17,7 @@ module Atsiser.ABI.Types import Data.Bits import Data.So import Data.Vect +import Decidable.Equality %default total @@ -29,13 +30,10 @@ public export data Platform = Linux | Windows | MacOS | BSD | WASM ||| Compile-time platform detection -||| This will be set during compilation based on target +||| This is the default target; override with compiler flags as needed. public export thisPlatform : Platform -thisPlatform = - %runElab do - -- Platform detection logic - pure Linux -- Default, override with compiler flags +thisPlatform = Linux -------------------------------------------------------------------------------- -- Result Codes @@ -81,7 +79,48 @@ DecEq Result where decEq NullPointer NullPointer = Yes Refl decEq OwnershipViolation OwnershipViolation = Yes Refl decEq BoundsViolation BoundsViolation = 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 OwnershipViolation = No (\case Refl impossible) + decEq Ok BoundsViolation = 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 OwnershipViolation = No (\case Refl impossible) + decEq Error BoundsViolation = 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 OwnershipViolation = No (\case Refl impossible) + decEq InvalidParam BoundsViolation = 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 OwnershipViolation = No (\case Refl impossible) + decEq OutOfMemory BoundsViolation = 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 OwnershipViolation = No (\case Refl impossible) + decEq NullPointer BoundsViolation = No (\case Refl impossible) + decEq OwnershipViolation Ok = No (\case Refl impossible) + decEq OwnershipViolation Error = No (\case Refl impossible) + decEq OwnershipViolation InvalidParam = No (\case Refl impossible) + decEq OwnershipViolation OutOfMemory = No (\case Refl impossible) + decEq OwnershipViolation NullPointer = No (\case Refl impossible) + decEq OwnershipViolation BoundsViolation = No (\case Refl impossible) + decEq BoundsViolation Ok = No (\case Refl impossible) + decEq BoundsViolation Error = No (\case Refl impossible) + decEq BoundsViolation InvalidParam = No (\case Refl impossible) + decEq BoundsViolation OutOfMemory = No (\case Refl impossible) + decEq BoundsViolation NullPointer = No (\case Refl impossible) + decEq BoundsViolation OwnershipViolation = No (\case Refl impossible) -------------------------------------------------------------------------------- -- Ownership State Machine @@ -165,8 +204,9 @@ data Handle : Type where ||| Returns Nothing if pointer is null 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 @@ -281,9 +321,10 @@ data HasAlignment : Type -> Nat -> Type where ||| Size of C types (platform-specific) public export +||| Note: `CInt p` / `CSize p` are type synonyms that reduce to `Bits32`/`Bits64`, +||| so they are covered by the `Bits32`/`Bits64` cases below rather than matched +||| as constructors (Idris2 cannot pattern-match on a type-level function). cSizeOf : (p : Platform) -> (t : Type) -> Nat -cSizeOf p (CInt _) = 4 -cSizeOf p (CSize _) = if ptrSize p == 64 then 8 else 4 cSizeOf p Bits32 = 4 cSizeOf p Bits64 = 8 cSizeOf p Double = 8 @@ -291,9 +332,9 @@ cSizeOf p _ = ptrSize p `div` 8 ||| Alignment of C types (platform-specific) public export +||| As with `cSizeOf`, `CInt`/`CSize` reduce to `Bits32`/`Bits64` and are +||| handled by those cases rather than matched as constructors. cAlignOf : (p : Platform) -> (t : Type) -> Nat -cAlignOf p (CInt _) = 4 -cAlignOf p (CSize _) = if ptrSize p == 64 then 8 else 4 cAlignOf p Bits32 = 4 cAlignOf p Bits64 = 8 cAlignOf p Double = 8 diff --git a/src/interface/abi/atsiser-abi.ipkg b/src/interface/abi/atsiser-abi.ipkg new file mode 100644 index 0000000..3c3df1e --- /dev/null +++ b/src/interface/abi/atsiser-abi.ipkg @@ -0,0 +1,9 @@ +-- SPDX-License-Identifier: MPL-2.0 +package atsiser-abi + +sourcedir = "." + +modules = Atsiser.ABI.Types + , Atsiser.ABI.Layout + , Atsiser.ABI.Foreign + , Atsiser.ABI.Proofs