diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md index c76a2cd..71f706f 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/.gitignore b/.gitignore index 73f5db0..e7d1b5f 100644 --- a/.gitignore +++ b/.gitignore @@ -18,6 +18,11 @@ Thumbs.db /dist/ /out/ +# Idris2 ABI build artefacts +**/build/ +*.ttc +*.ttm + # Dependencies /node_modules/ /vendor/ 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 75188d5..6373fbb 100644 --- a/.machine_readable/contractiles/must/Mustfile.a2ml +++ b/.machine_readable/contractiles/must/Mustfile.a2ml @@ -47,7 +47,7 @@ These are hard requirements — CI fails if any check fails. - severity: warning ### no-agpl -- description: No AGPL-3.0 references (replaced by PMPL) +- description: No AGPL-3.0 references (replaced 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 976ee52..2346d0e 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 ### signed-by-ci diff --git a/Cargo.toml b/Cargo.toml index 2762022..63c7be1 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -5,7 +5,7 @@ version = "0.1.0" edition = "2024" authors = ["Jonathan D.A. Jewell "] description = "Generate OTP supervision trees, GenServers, and fault-tolerance scaffolding from service descriptions" -license-file = "LICENSE" +license = "MPL-2.0" repository = "https://github.com/hyperpolymath/otpiser" keywords = ["erlang", "otp", "elixir", "fault-tolerance", "supervision"] 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 ================================== diff --git a/QUICKSTART-MAINTAINER.adoc b/QUICKSTART-MAINTAINER.adoc index 881f28e..4553f93 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 95e7377..b188798 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 ───────────────────────────────────────────────────────────────────────────── diff --git a/src/interface/abi/Foreign.idr b/src/interface/abi/Otpiser/ABI/Foreign.idr similarity index 95% rename from src/interface/abi/Foreign.idr rename to src/interface/abi/Otpiser/ABI/Foreign.idr index e9625b9..d494443 100644 --- a/src/interface/abi/Foreign.idr +++ b/src/interface/abi/Otpiser/ABI/Foreign.idr @@ -17,6 +17,18 @@ import Otpiser.ABI.Layout %default total +-------------------------------------------------------------------------------- +-- String Operations (shared FFI utilities) +-------------------------------------------------------------------------------- +-- Declared first so its type is in scope for every use below. Without this, +-- a forward reference lets the elaborator pick up the support `Ptr String` +-- variant and the call sites fail to unify against our `Bits64` pointers. + +||| Convert C string to Idris String +export +%foreign "support:idris2_getString, libidris2_support" +prim__getString : Bits64 -> String + -------------------------------------------------------------------------------- -- Library Lifecycle -------------------------------------------------------------------------------- @@ -236,11 +248,8 @@ prim__serializedSize : Bits64 -> Bits64 -> PrimIO Bits32 -------------------------------------------------------------------------------- -- String Operations (shared FFI utilities) -------------------------------------------------------------------------------- - -||| Convert C string to Idris String -export -%foreign "support:idris2_getString, libidris2_support" -prim__getString : Bits64 -> String +-- (prim__getString is declared near the top of this module so its type is in +-- scope for all callers above.) ||| Free C string allocated by otpiser export diff --git a/src/interface/abi/Layout.idr b/src/interface/abi/Otpiser/ABI/Layout.idr similarity index 70% rename from src/interface/abi/Layout.idr rename to src/interface/abi/Otpiser/ABI/Layout.idr index 5f473aa..b14d40a 100644 --- a/src/interface/abi/Layout.idr +++ b/src/interface/abi/Otpiser/ABI/Layout.idr @@ -15,6 +15,8 @@ module Otpiser.ABI.Layout import Otpiser.ABI.Types import Data.Vect import Data.So +import Data.Nat +import Decidable.Equality %default total @@ -28,24 +30,41 @@ 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 for divisibility. +||| Returns a genuine `Divides d v` witness when `d` divides `v`, else Nothing. +||| For `d = S j`, compute the candidate quotient `q = v `div` (S j)` and check +||| `v = q * (S j)` decidably; the equality proof IS the divisibility witness. +||| Division never reduces under Refl, so we go through `decEq`, never a hole. +public export +decDivides : (d : Nat) -> (v : Nat) -> Maybe (Divides d v) +decDivides Z _ = Nothing +decDivides (S j) v = + let q = v `div` (S j) in + case decEq v (q * (S j)) 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 +||| Decision: is the rounded-up size actually a multiple of the alignment? +||| `alignUp` uses `div`/`mod`, which do not reduce under `Refl`, so the +||| divisibility witness is produced by the sound `decDivides` decision +||| procedure rather than asserted. Returns Nothing only if the (decidable) +||| check fails for the given 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 @@ -77,7 +96,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 +105,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. +||| Both record obligations are discharged by sound decisions: `choose` for the +||| size bound (`So`) and `decDivides` for the alignment witness. No assertions. 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 sizeOk => + case decDivides align size of + Nothing => Left "Total size is not a multiple of alignment" + Just alignProof => + Right (MkStructLayout fields size align + {sizeCorrect = sizeOk} {aligned = alignProof}) -------------------------------------------------------------------------------- -- Supervision Tree Node Layout @@ -133,6 +159,8 @@ supervisorNodeLayout = ] 32 -- Total size: 32 bytes 8 -- Alignment: 8 bytes + {sizeCorrect = Oh} + {aligned = DivideBy 4 Refl} -- 32 = 4 * 8 ||| Layout of a serialised ChildSpec for FFI transport. ||| @@ -157,6 +185,8 @@ childSpecLayout = ] 32 -- Total size: 32 bytes 8 -- Alignment: 8 bytes + {sizeCorrect = Oh} + {aligned = DivideBy 4 Refl} -- 32 = 4 * 8 ||| Layout of a GenServerCallback specification for FFI transport. ||| @@ -185,6 +215,8 @@ genServerCallbackLayout = ] 40 -- Total size: 40 bytes 8 -- Alignment: 8 bytes + {sizeCorrect = Oh} + {aligned = DivideBy 5 Refl} -- 40 = 5 * 8 -------------------------------------------------------------------------------- -- Platform-Specific Layouts @@ -215,21 +247,25 @@ data CABICompliant : StructLayout -> Type where FieldsAligned layout.fields -> CABICompliant layout -||| Check if layout follows C ABI +||| Decide alignment of every field in a vector, building a FieldsAligned witness. +public export +decFieldsAligned : (fields : Vect k Field) -> Maybe (FieldsAligned fields) +decFieldsAligned [] = Just NoFields +decFieldsAligned (f :: fs) = + case decDivides f.alignment f.offset of + Nothing => Nothing + Just dv => + case decFieldsAligned fs of + Nothing => Nothing + Just rest => Just (ConsField f fs dv rest) + +||| Check if layout follows C ABI by deciding field alignment soundly. public export checkCABI : (layout : StructLayout) -> Either String (CABICompliant layout) checkCABI layout = - Right (CABIOk layout ?fieldsAlignedProof) - -||| Proof that supervisor node layout is C ABI compliant -export -supervisorNodeCABI : CABICompliant supervisorNodeLayout -supervisorNodeCABI = CABIOk supervisorNodeLayout ?supervisorFieldsAligned - -||| Proof that child spec layout is C ABI compliant -export -childSpecCABI : CABICompliant childSpecLayout -childSpecCABI = CABIOk childSpecLayout ?childSpecFieldsAligned + case decFieldsAligned layout.fields of + Just prf => Right (CABIOk layout prf) + Nothing => Left "Struct fields are not C-ABI aligned" -------------------------------------------------------------------------------- -- Offset Calculation @@ -243,7 +279,12 @@ 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 the struct's total size. +||| This is genuinely partial (a field may lie outside an arbitrary layout), +||| so it returns `Maybe` of the bound proof rather than asserting it. 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/Otpiser/ABI/Proofs.idr b/src/interface/abi/Otpiser/ABI/Proofs.idr new file mode 100644 index 0000000..807c6d9 --- /dev/null +++ b/src/interface/abi/Otpiser/ABI/Proofs.idr @@ -0,0 +1,108 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Machine-Checked ABI Theorems for Otpiser +||| +||| This module collects the genuine, compiler-verified theorems about the +||| Otpiser C-ABI surface. Each `*Compliant` theorem exhibits a DIRECT +||| `FieldsAligned` witness for a concrete `StructLayout`: one `DivideBy` +||| per field, where `field.offset = k * field.alignment`. Multiplication +||| reduces during type-checking (so `Refl` discharges each equation), whereas +||| division does NOT — hence these witnesses are built by hand rather than via +||| the `decFieldsAligned` decision procedure. +||| +||| The result-code lemmas pin the wire encoding of the FFI `Result` enum. +||| +||| @see Otpiser.ABI.Layout for the layouts and the `CABICompliant` relation +||| @see Otpiser.ABI.Types for the `Result` encoding + +module Otpiser.ABI.Proofs + +import Otpiser.ABI.Types +import Otpiser.ABI.Layout +import Data.Vect + +%default total + +-------------------------------------------------------------------------------- +-- C-ABI compliance of the concrete struct layouts +-------------------------------------------------------------------------------- + +||| The serialised supervisor-node layout is C-ABI compliant: every field's +||| offset is an exact multiple of its alignment. +||| nodeType@0/4, strategy@4/4, maxRestarts@8/4, maxSeconds@12/4, +||| childCount@16/4, nameLen@20/4, namePtr@24/8. +export +supervisorNodeCompliant : CABICompliant Layout.supervisorNodeLayout +supervisorNodeCompliant = + CABIOk Layout.supervisorNodeLayout + (ConsField _ _ (DivideBy 0 Refl) -- offset 0 = 0 * 4 + (ConsField _ _ (DivideBy 1 Refl) -- offset 4 = 1 * 4 + (ConsField _ _ (DivideBy 2 Refl) -- offset 8 = 2 * 4 + (ConsField _ _ (DivideBy 3 Refl) -- offset 12 = 3 * 4 + (ConsField _ _ (DivideBy 4 Refl) -- offset 16 = 4 * 4 + (ConsField _ _ (DivideBy 5 Refl) -- offset 20 = 5 * 4 + (ConsField _ _ (DivideBy 3 Refl) -- offset 24 = 3 * 8 + NoFields))))))) + +||| The serialised child-spec layout is C-ABI compliant. +||| childIdLen@0/4, restartType@4/4, shutdownMs@8/4, childType@12/4, +||| childIdPtr@16/8, modulePtr@24/8. +export +childSpecCompliant : CABICompliant Layout.childSpecLayout +childSpecCompliant = + CABIOk Layout.childSpecLayout + (ConsField _ _ (DivideBy 0 Refl) -- offset 0 = 0 * 4 + (ConsField _ _ (DivideBy 1 Refl) -- offset 4 = 1 * 4 + (ConsField _ _ (DivideBy 2 Refl) -- offset 8 = 2 * 4 + (ConsField _ _ (DivideBy 3 Refl) -- offset 12 = 3 * 4 + (ConsField _ _ (DivideBy 2 Refl) -- offset 16 = 2 * 8 + (ConsField _ _ (DivideBy 3 Refl) -- offset 24 = 3 * 8 + NoFields)))))) + +||| The serialised GenServer-callback layout is C-ABI compliant. +||| moduleNameLen@0/4, stateTypeLen@4/4, callTypeCount@8/4, castTypeCount@12/4, +||| infoTypeCount@16/4, padding@20/4, moduleNamePtr@24/8, stateTypePtr@32/8. +export +genServerCallbackCompliant : CABICompliant Layout.genServerCallbackLayout +genServerCallbackCompliant = + CABIOk Layout.genServerCallbackLayout + (ConsField _ _ (DivideBy 0 Refl) -- offset 0 = 0 * 4 + (ConsField _ _ (DivideBy 1 Refl) -- offset 4 = 1 * 4 + (ConsField _ _ (DivideBy 2 Refl) -- offset 8 = 2 * 4 + (ConsField _ _ (DivideBy 3 Refl) -- offset 12 = 3 * 4 + (ConsField _ _ (DivideBy 4 Refl) -- offset 16 = 4 * 4 + (ConsField _ _ (DivideBy 5 Refl) -- offset 20 = 5 * 4 + (ConsField _ _ (DivideBy 3 Refl) -- offset 24 = 3 * 8 + (ConsField _ _ (DivideBy 4 Refl) -- offset 32 = 4 * 8 + NoFields)))))))) + +-------------------------------------------------------------------------------- +-- Result-code wire-encoding lemmas +-------------------------------------------------------------------------------- + +||| The success code encodes to 0 (the C convention for "no error"). +export +okIsZero : resultToInt Ok = 0 +okIsZero = Refl + +||| The null-pointer error encodes to 4, distinct from success. +export +nullPointerIsFour : resultToInt NullPointer = 4 +nullPointerIsFour = Refl + +||| Encoding is injective on the two endpoints we care about most: success and +||| the malformed-tree error never collide. Pins that 0 /= 6 under the encoding. +export +okDistinctFromMalformed : Not (resultToInt Ok = resultToInt MalformedTree) +okDistinctFromMalformed = \case Refl impossible + +-------------------------------------------------------------------------------- +-- Supervision-strategy round-trip (re-export as a named theorem) +-------------------------------------------------------------------------------- + +||| Strategy encode/decode is a genuine round trip for every strategy. +export +strategyEncodingRoundTrips : + (s : SupervisorStrategy) -> intToStrategy (strategyToInt s) = Just s +strategyEncodingRoundTrips = strategyRoundTrip diff --git a/src/interface/abi/Types.idr b/src/interface/abi/Otpiser/ABI/Types.idr similarity index 75% rename from src/interface/abi/Types.idr rename to src/interface/abi/Otpiser/ABI/Types.idr index b54f55c..ea45bf8 100644 --- a/src/interface/abi/Types.idr +++ b/src/interface/abi/Otpiser/ABI/Types.idr @@ -15,6 +15,7 @@ module Otpiser.ABI.Types import Data.Bits import Data.So import Data.Vect +import Decidable.Equality %default total @@ -30,10 +31,7 @@ data Platform = Linux | Windows | MacOS | BSD | WASM ||| This will be set during compilation based on target public export thisPlatform : Platform -thisPlatform = - %runElab do - -- Platform detection logic - pure Linux -- Default, override with compiler flags +thisPlatform = Linux -- Default platform; override with compiler flags -------------------------------------------------------------------------------- -- OTP Supervision Strategy Types @@ -60,7 +58,12 @@ DecEq SupervisorStrategy where decEq OneForOne OneForOne = Yes Refl decEq OneForAll OneForAll = Yes Refl decEq RestForOne RestForOne = Yes Refl - decEq _ _ = No absurd + decEq OneForOne OneForAll = No (\case Refl impossible) + decEq OneForOne RestForOne = No (\case Refl impossible) + decEq OneForAll OneForOne = No (\case Refl impossible) + decEq OneForAll RestForOne = No (\case Refl impossible) + decEq RestForOne OneForOne = No (\case Refl impossible) + decEq RestForOne OneForAll = No (\case Refl impossible) ||| Convert SupervisorStrategy to C-compatible integer for FFI public export @@ -179,6 +182,13 @@ data ValidCallback : GenServerCallback -> Type where ||| A child specification defines how a supervisor starts, monitors, ||| and restarts a child process. ||| @see https://www.erlang.org/doc/man/supervisor#type-child_spec + +||| Whether a child is a worker process or a supervisor. +public export +data ChildType : Type where + Worker : ChildType + Supervisor : ChildType + public export record ChildSpec where constructor MkChildSpec @@ -189,12 +199,6 @@ record ChildSpec where shutdown : ShutdownType childType : ChildType -||| Whether a child is a worker process or a supervisor. -public export -data ChildType : Type where - Worker : ChildType - Supervisor : ChildType - ||| Proof that a child spec has a non-empty ID public export data ValidChildSpec : ChildSpec -> Type where @@ -220,29 +224,47 @@ data ProcessTree : Type where (spec : ChildSpec) -> ProcessTree -||| Count total nodes in a process tree +||| Count total nodes in a process tree. +||| Uses an explicit structural fold over the child vector so the totality +||| checker can see the recursion descend into proper subterms. public export treeSize : ProcessTree -> Nat treeSize (WorkerNode _) = 1 -treeSize (SupervisorNode _ _ _ children) = 1 + sum (map treeSize children) +treeSize (SupervisorNode _ _ _ children) = 1 + sumChildSizes children + where + sumChildSizes : Vect k ProcessTree -> Nat + sumChildSizes [] = 0 + sumChildSizes (c :: cs) = treeSize c + sumChildSizes cs ||| Count worker nodes only public export workerCount : ProcessTree -> Nat workerCount (WorkerNode _) = 1 -workerCount (SupervisorNode _ _ _ children) = sum (map workerCount children) +workerCount (SupervisorNode _ _ _ children) = sumChildWorkers children + where + sumChildWorkers : Vect k ProcessTree -> Nat + sumChildWorkers [] = 0 + sumChildWorkers (c :: cs) = workerCount c + sumChildWorkers cs ||| Depth of the supervision tree public export treeDepth : ProcessTree -> Nat treeDepth (WorkerNode _) = 0 -treeDepth (SupervisorNode _ _ _ children) = 1 + foldr max 0 (map treeDepth children) +treeDepth (SupervisorNode _ _ _ children) = 1 + maxChildDepth children + where + maxChildDepth : Vect k ProcessTree -> Nat + maxChildDepth [] = 0 + maxChildDepth (c :: cs) = max (treeDepth c) (maxChildDepth cs) ||| Proof that a tree has at least one worker public export data HasWorkers : ProcessTree -> Type where - IsWorker : HasWorkers (WorkerNode _) - HasChildWorker : HasWorkers child -> HasWorkers (SupervisorNode _ _ _ (child :: _)) + IsWorker : HasWorkers (WorkerNode spec) + HasChildWorker : + {0 n : Nat} -> + {0 rest : Vect n ProcessTree} -> + HasWorkers child -> + HasWorkers (SupervisorNode name strategy intensity (child :: rest)) -------------------------------------------------------------------------------- -- FFI Result Codes @@ -288,7 +310,48 @@ DecEq Result where decEq NullPointer NullPointer = Yes Refl decEq InvalidStrategy InvalidStrategy = Yes Refl decEq MalformedTree MalformedTree = 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 InvalidStrategy = No (\case Refl impossible) + decEq Ok MalformedTree = 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 InvalidStrategy = No (\case Refl impossible) + decEq Error MalformedTree = 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 InvalidStrategy = No (\case Refl impossible) + decEq InvalidParam MalformedTree = 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 InvalidStrategy = No (\case Refl impossible) + decEq OutOfMemory MalformedTree = 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 InvalidStrategy = No (\case Refl impossible) + decEq NullPointer MalformedTree = No (\case Refl impossible) + decEq InvalidStrategy Ok = No (\case Refl impossible) + decEq InvalidStrategy Error = No (\case Refl impossible) + decEq InvalidStrategy InvalidParam = No (\case Refl impossible) + decEq InvalidStrategy OutOfMemory = No (\case Refl impossible) + decEq InvalidStrategy NullPointer = No (\case Refl impossible) + decEq InvalidStrategy MalformedTree = No (\case Refl impossible) + decEq MalformedTree Ok = No (\case Refl impossible) + decEq MalformedTree Error = No (\case Refl impossible) + decEq MalformedTree InvalidParam = No (\case Refl impossible) + decEq MalformedTree OutOfMemory = No (\case Refl impossible) + decEq MalformedTree NullPointer = No (\case Refl impossible) + decEq MalformedTree InvalidStrategy = No (\case Refl impossible) -------------------------------------------------------------------------------- -- Opaque Handles @@ -304,8 +367,10 @@ 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 @@ -343,10 +408,15 @@ ptrSize MacOS = 64 ptrSize BSD = 64 ptrSize WASM = 32 -||| Pointer type for platform +||| Pointer type for platform: a pointer-width unsigned integer. +||| 64-bit on native platforms, 32-bit on WASM. public export CPtr : Platform -> Type -> Type -CPtr p _ = Bits (ptrSize p) +CPtr Linux _ = Bits64 +CPtr Windows _ = Bits64 +CPtr MacOS _ = Bits64 +CPtr BSD _ = Bits64 +CPtr WASM _ = Bits32 -------------------------------------------------------------------------------- -- Memory Layout Proofs diff --git a/src/interface/abi/otpiser-abi.ipkg b/src/interface/abi/otpiser-abi.ipkg new file mode 100644 index 0000000..ba2a27a --- /dev/null +++ b/src/interface/abi/otpiser-abi.ipkg @@ -0,0 +1,9 @@ +-- SPDX-License-Identifier: MPL-2.0 +package otpiser-abi + +sourcedir = "." + +modules = Otpiser.ABI.Types + , Otpiser.ABI.Layout + , Otpiser.ABI.Foreign + , Otpiser.ABI.Proofs