From 7df3b611e79644eef54cb28e79e75f6328d55adc Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Fri, 26 Jun 2026 11:20:32 +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 eaa6bb0..50acba5 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -5,7 +5,7 @@ version = "0.1.0" edition = "2024" authors = ["Jonathan D.A. Jewell "] description = "Add provably safe ethical constraints to AI agent decision-making via Phronesis" -license-file = "LICENSE" +license = "MPL-2.0" repository = "https://github.com/hyperpolymath/phronesiser" keywords = ["ethics", "deontic-logic", "ai-safety", "constraints", "formal-verification"] 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 48cde05420a43302e12e02b6c36b47278d5fe900 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Fri, 26 Jun 2026 11:36:42 +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 f133425..10e2436 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 652f77a..b722182 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 d80302c..3f7e250 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 8e2ed4c02db41475aab74a0e1fb5ee4158a6d742 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 26 Jun 2026 12:27:30 +0000 Subject: [PATCH 3/3] Fix Idris2 ABI proofs so they genuinely compile under Idris2 0.7.0 The src/interface/abi scaffold was generated from a template and never compiler-checked. This makes the phronesiser ABI typecheck cleanly (idris2 --build phronesiser-abi.ipkg: exit 0, zero warnings, zero errors) with genuine, machine-checked proofs. Fixes: - Types.idr: replace the catch-all `decEq _ _ = No absurd` in the Result, DeonticModality and HarmSeverity DecEq instances with explicit off-diagonal `No (\case Refl impossible)` cases (the catch-all does not compile: no Uninhabited (x = y) instance). - Types.idr: createHandle now obtains a real `So (ptr /= 0)` via `choose` instead of leaving MkHandle's auto proof unsolved. - Types.idr: thisPlatform is a plain value (Linux); the %runElab stub needed ElabReflection and did not compile. - Types.idr: drop non-compiling/unsound template cruft (CPtr matching the type-level Bits/ptrSize, cSizeOf/cAlignOf matching on the type-level CInt/CSize, and vacuous HasSize/HasAlignment whose lone constructor proved any size). Real size/alignment is proven in Layout/Proofs. - Layout.idr: paddingFor uses Nat `minus` (Nat has no Neg); add sound decDivides; concrete StructLayouts supply explicit {sizeCorrect = Oh} and {aligned = DivideBy k Refl}; checkCABI builds a real CABICompliant via decFieldsAligned; offsetInBounds returns Maybe (So ...) via choose; constraintArrayMonotonic proved via a genuine scaleLteRight lemma (induction on LTE) + plusLteMonotoneLeft, returning LTE not So. - New Proofs.idr: CABICompliant witnesses for all three concrete layouts built directly from DivideBy (offset = k * alignment), plus result/ modality/severity encoding theorems and constraint-array sizing facts. - Nested layout src/interface/abi/Phronesiser/ABI/{Types,Layout,Foreign, Proofs}.idr + phronesiser-abi.ipkg so namespaces match file paths. - .gitignore: ignore Idris2 build artefacts (**/build/, *.ttc, *.ttm). No believe_me / assert_total / idris_crash / postulate / %hint / holes. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA --- .gitignore | 5 + .../abi/{ => Phronesiser/ABI}/Foreign.idr | 0 .../abi/{ => Phronesiser/ABI}/Layout.idr | 118 +++++++++---- src/interface/abi/Phronesiser/ABI/Proofs.idr | 115 ++++++++++++ .../abi/{ => Phronesiser/ABI}/Types.idr | 163 ++++++++++-------- src/interface/abi/phronesiser-abi.ipkg | 11 ++ 6 files changed, 305 insertions(+), 107 deletions(-) rename src/interface/abi/{ => Phronesiser/ABI}/Foreign.idr (100%) rename src/interface/abi/{ => Phronesiser/ABI}/Layout.idr (63%) create mode 100644 src/interface/abi/Phronesiser/ABI/Proofs.idr rename src/interface/abi/{ => Phronesiser/ABI}/Types.idr (71%) create mode 100644 src/interface/abi/phronesiser-abi.ipkg diff --git a/.gitignore b/.gitignore index 73f5db0..8bf9110 100644 --- a/.gitignore +++ b/.gitignore @@ -18,6 +18,11 @@ Thumbs.db /dist/ /out/ +# Idris2 build artefacts +**/build/ +*.ttc +*.ttm + # Dependencies /node_modules/ /vendor/ diff --git a/src/interface/abi/Foreign.idr b/src/interface/abi/Phronesiser/ABI/Foreign.idr similarity index 100% rename from src/interface/abi/Foreign.idr rename to src/interface/abi/Phronesiser/ABI/Foreign.idr diff --git a/src/interface/abi/Layout.idr b/src/interface/abi/Phronesiser/ABI/Layout.idr similarity index 63% rename from src/interface/abi/Layout.idr rename to src/interface/abi/Phronesiser/ABI/Layout.idr index 351592c..4037b9b 100644 --- a/src/interface/abi/Layout.idr +++ b/src/interface/abi/Phronesiser/ABI/Layout.idr @@ -19,6 +19,8 @@ module Phronesiser.ABI.Layout import Phronesiser.ABI.Types import Data.Vect import Data.So +import Data.Nat +import Decidable.Equality %default total @@ -32,24 +34,40 @@ 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 +||| Decide whether the rounded-up size is divisible by the alignment. The +||| general theorem needs div/mod lemmas from Data.Nat; here we *decide* it +||| via `decDivides`, returning a genuine witness when it holds. (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 @@ -81,7 +99,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 @@ -90,23 +108,26 @@ 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 +||| Decide field alignment for every field, building a real `FieldsAligned` +||| witness from per-field divisibility proofs. public export -verifyLayout : (fields : Vect n 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" +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) -------------------------------------------------------------------------------- -- Platform-Specific Layouts @@ -137,11 +158,15 @@ data CABICompliant : StructLayout -> Type where FieldsAligned layout.fields -> CABICompliant layout -||| Check if layout follows C ABI +||| 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. 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 "Field offsets are not correctly aligned for the C ABI" -------------------------------------------------------------------------------- -- Phronesiser Constraint Struct Layout @@ -160,11 +185,8 @@ constraintLayout = ] 16 -- Total size: 16 bytes 4 -- Alignment: 4 bytes - -||| Proof that constraint layout is valid -export -constraintLayoutValid : CABICompliant constraintLayout -constraintLayoutValid = CABIOk constraintLayout ?constraintFieldsAligned + {sizeCorrect = Oh} + {aligned = DivideBy 4 Refl} -- 16 = 4 * 4 -------------------------------------------------------------------------------- -- Phronesiser Audit Result Struct Layout @@ -183,11 +205,8 @@ auditResultLayout = ] 16 -- Total size: 16 bytes 4 -- Alignment: 4 bytes - -||| Proof that audit result layout is valid -export -auditResultLayoutValid : CABICompliant auditResultLayout -auditResultLayoutValid = CABIOk auditResultLayout ?auditResultFieldsAligned + {sizeCorrect = Oh} + {aligned = DivideBy 4 Refl} -- 16 = 4 * 4 -------------------------------------------------------------------------------- -- Constraint Set Header Layout @@ -204,23 +223,32 @@ constraintSetHeaderLayout = ] 8 -- Total size: 8 bytes 4 -- Alignment: 4 bytes + {sizeCorrect = Oh} + {aligned = DivideBy 2 Refl} -- 8 = 2 * 4 -------------------------------------------------------------------------------- -- Offset Calculation -------------------------------------------------------------------------------- -||| Calculate field offset with proof of correctness +||| Look up a field's index and record by name in a layout. public export -fieldOffset : (layout : StructLayout) -> (fieldName : String) -> Maybe (n : Nat ** Field) +fieldOffset : (layout : StructLayout) -> (fieldName : String) -> Maybe (Nat, Field) fieldOffset layout name = case findIndex (\f => f.name == name) layout.fields of - Just idx => Just (finToNat idx ** index idx layout.fields) + 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. 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 -------------------------------------------------------------------------------- -- Constraint Array Layout @@ -232,8 +260,22 @@ public export constraintArraySize : (count : Nat) -> Nat constraintArraySize count = 8 + (count * 16) -||| Proof that constraint array size grows monotonically with count +||| `j <= l` implies `j * c <= l * c`, by induction on the `LTE` witness. +||| Genuine arithmetic lemma — no `believe_me`, no decision shortcut. +public export +scaleLteRight : (c : Nat) -> {j, l : Nat} -> LTE j l -> LTE (j * c) (l * c) +scaleLteRight c LTEZero = LTEZero +scaleLteRight c (LTESucc {left = a} {right = b} p) = + plusLteMonotoneLeft c (a * c) (b * c) (scaleLteRight c p) + +||| Proof that constraint array size grows monotonically with count. +||| `constraintArraySize n = 8 + n * 16`, so this reduces to +||| `8 + n*16 <= 8 + m*16`, discharged from `n <= m` via `scaleLteRight` +||| and `plusLteMonotoneLeft`. The `<=` is the propositional `LTE`, the +||| genuine order relation (the previous `So (... <= ...)` could not be +||| proven for symbolic inputs, only decided). public export -constraintArrayMonotonic : (n : Nat) -> (m : Nat) -> (n <= m) -> - So (constraintArraySize n <= constraintArraySize m) -constraintArrayMonotonic n m prf = ?constraintArrayMonotonicProof +constraintArrayMonotonic : (n : Nat) -> (m : Nat) -> LTE n m -> + LTE (constraintArraySize n) (constraintArraySize m) +constraintArrayMonotonic n m prf = + plusLteMonotoneLeft 8 (n * 16) (m * 16) (scaleLteRight 16 prf) diff --git a/src/interface/abi/Phronesiser/ABI/Proofs.idr b/src/interface/abi/Phronesiser/ABI/Proofs.idr new file mode 100644 index 0000000..94fd1f4 --- /dev/null +++ b/src/interface/abi/Phronesiser/ABI/Proofs.idr @@ -0,0 +1,115 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Machine-checked proofs over the phronesiser 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, a result/modality/severity encoding wrong, or a decision +||| procedure mis-defined, 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 never route them through `Nat` division, which is a +||| primitive that does not reduce at the type level. + +module Phronesiser.ABI.Proofs + +import Phronesiser.ABI.Types +import Phronesiser.ABI.Layout +import Data.So +import Data.Vect + +%default total + +-------------------------------------------------------------------------------- +-- The concrete FFI struct layouts are provably C-ABI compliant. +-------------------------------------------------------------------------------- + +||| ConstraintStruct layout: offsets 0,4,8,12 each 4-byte aligned, so +||| 0 = 0*4, 4 = 1*4, 8 = 2*4, 12 = 3*4. +export +constraintLayoutCompliant : CABICompliant Layout.constraintLayout +constraintLayoutCompliant = + CABIOk constraintLayout + (ConsField _ _ (DivideBy 0 Refl) + (ConsField _ _ (DivideBy 1 Refl) + (ConsField _ _ (DivideBy 2 Refl) + (ConsField _ _ (DivideBy 3 Refl) + NoFields)))) + +||| AuditResultStruct layout: offsets 0,4,8,12 each 4-byte aligned. +export +auditResultLayoutCompliant : CABICompliant Layout.auditResultLayout +auditResultLayoutCompliant = + CABIOk auditResultLayout + (ConsField _ _ (DivideBy 0 Refl) + (ConsField _ _ (DivideBy 1 Refl) + (ConsField _ _ (DivideBy 2 Refl) + (ConsField _ _ (DivideBy 3 Refl) + NoFields)))) + +||| ConstraintSetHeader layout: offsets 0,4 each 4-byte aligned, so +||| 0 = 0*4, 4 = 1*4. +export +constraintSetHeaderLayoutCompliant : CABICompliant Layout.constraintSetHeaderLayout +constraintSetHeaderLayoutCompliant = + CABIOk constraintSetHeaderLayout + (ConsField _ _ (DivideBy 0 Refl) + (ConsField _ _ (DivideBy 1 Refl) + NoFields)) + +-------------------------------------------------------------------------------- +-- Result-code encoding: the integers the Zig FFI depends on. +-------------------------------------------------------------------------------- + +export +okIsZero : resultToInt Ok = 0 +okIsZero = Refl + +export +constraintConflictIsSix : resultToInt ConstraintConflict = 6 +constraintConflictIsSix = Refl + +-------------------------------------------------------------------------------- +-- Deontic / severity encodings used across the FFI boundary. +-------------------------------------------------------------------------------- + +||| The three deontic modalities encode to 0, 1, 2 — pinned for the Zig side. +export +prohibitionIsTwo : modalityToInt Prohibition = 2 +prohibitionIsTwo = Refl + +||| Obligation and prohibition are genuinely distinct propositions: an action +||| cannot be both obligatory and prohibited. (Re-exported as a Proofs-level +||| theorem so the proof build pins the deontic contradiction directly.) +export +obligationNotProhibition : Obligation = Prohibition -> Void +obligationNotProhibition Refl impossible + +||| Severity encodes Critical as the maximum code 4. +export +criticalIsFour : severityToInt Critical = 4 +criticalIsFour = Refl + +-------------------------------------------------------------------------------- +-- Constraint-array sizing is strictly determined and grows with count. +-------------------------------------------------------------------------------- + +||| An empty constraint array is exactly the 8-byte header. +export +emptyArrayIsHeader : constraintArraySize 0 = 8 +emptyArrayIsHeader = Refl + +||| One constraint occupies header (8) + one 16-byte struct = 24 bytes. +export +oneConstraintArraySize : constraintArraySize 1 = 24 +oneConstraintArraySize = Refl + +||| Monotonicity instantiated: a 2-element set is no larger than a 5-element +||| set. Exercises `constraintArrayMonotonic` with a concrete `LTE` witness. +export +arrayGrows : LTE (constraintArraySize 2) (constraintArraySize 5) +arrayGrows = constraintArrayMonotonic 2 5 (LTESucc (LTESucc LTEZero)) diff --git a/src/interface/abi/Types.idr b/src/interface/abi/Phronesiser/ABI/Types.idr similarity index 71% rename from src/interface/abi/Types.idr rename to src/interface/abi/Phronesiser/ABI/Types.idr index 9d440df..95d2588 100644 --- a/src/interface/abi/Types.idr +++ b/src/interface/abi/Phronesiser/ABI/Types.idr @@ -15,6 +15,7 @@ module Phronesiser.ABI.Types import Data.Bits import Data.So import Data.Vect +import Decidable.Equality %default total @@ -26,14 +27,12 @@ import Data.Vect public export data Platform = Linux | Windows | MacOS | BSD | WASM -||| Compile-time platform detection -||| This will be set during compilation based on target +||| The platform this build targets. Defaults to Linux; the Rust/Zig build +||| layer overrides this via codegen target selection. (Previously a +||| `%runElab` stub that required ElabReflection and did not compile.) public export thisPlatform : Platform -thisPlatform = - %runElab do - -- Platform detection logic - pure Linux -- Default, override with compiler flags +thisPlatform = Linux -------------------------------------------------------------------------------- -- FFI Result Codes @@ -70,6 +69,8 @@ resultToInt ConstraintViolation = 5 resultToInt ConstraintConflict = 6 ||| Results are decidably equal +||| The off-diagonal cases discharge disequality explicitly; the previous +||| `decEq _ _ = No absurd` did not compile (no `Uninhabited (x = y)`). public export DecEq Result where decEq Ok Ok = Yes Refl @@ -79,7 +80,48 @@ DecEq Result where decEq NullPointer NullPointer = Yes Refl decEq ConstraintViolation ConstraintViolation = Yes Refl decEq ConstraintConflict ConstraintConflict = 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 ConstraintViolation = No (\case Refl impossible) + decEq Ok ConstraintConflict = 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 ConstraintViolation = No (\case Refl impossible) + decEq Error ConstraintConflict = 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 ConstraintViolation = No (\case Refl impossible) + decEq InvalidParam ConstraintConflict = 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 ConstraintViolation = No (\case Refl impossible) + decEq OutOfMemory ConstraintConflict = 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 ConstraintViolation = No (\case Refl impossible) + decEq NullPointer ConstraintConflict = No (\case Refl impossible) + decEq ConstraintViolation Ok = No (\case Refl impossible) + decEq ConstraintViolation Error = No (\case Refl impossible) + decEq ConstraintViolation InvalidParam = No (\case Refl impossible) + decEq ConstraintViolation OutOfMemory = No (\case Refl impossible) + decEq ConstraintViolation NullPointer = No (\case Refl impossible) + decEq ConstraintViolation ConstraintConflict = No (\case Refl impossible) + decEq ConstraintConflict Ok = No (\case Refl impossible) + decEq ConstraintConflict Error = No (\case Refl impossible) + decEq ConstraintConflict InvalidParam = No (\case Refl impossible) + decEq ConstraintConflict OutOfMemory = No (\case Refl impossible) + decEq ConstraintConflict NullPointer = No (\case Refl impossible) + decEq ConstraintConflict ConstraintViolation = No (\case Refl impossible) -------------------------------------------------------------------------------- -- Deontic Modality @@ -116,7 +158,12 @@ DecEq DeonticModality where decEq Obligation Obligation = Yes Refl decEq Permission Permission = Yes Refl decEq Prohibition Prohibition = Yes Refl - decEq _ _ = No absurd + decEq Obligation Permission = No (\case Refl impossible) + decEq Obligation Prohibition = No (\case Refl impossible) + decEq Permission Obligation = No (\case Refl impossible) + decEq Permission Prohibition = No (\case Refl impossible) + decEq Prohibition Obligation = No (\case Refl impossible) + decEq Prohibition Permission = No (\case Refl impossible) ||| Proof that obligation and prohibition are contradictory. ||| An action cannot be both obligatory and prohibited. @@ -165,7 +212,26 @@ DecEq HarmSeverity where decEq Moderate Moderate = Yes Refl decEq Severe Severe = Yes Refl decEq Critical Critical = Yes Refl - decEq _ _ = No absurd + decEq Negligible Minor = No (\case Refl impossible) + decEq Negligible Moderate = No (\case Refl impossible) + decEq Negligible Severe = No (\case Refl impossible) + decEq Negligible Critical = No (\case Refl impossible) + decEq Minor Negligible = No (\case Refl impossible) + decEq Minor Moderate = No (\case Refl impossible) + decEq Minor Severe = No (\case Refl impossible) + decEq Minor Critical = No (\case Refl impossible) + decEq Moderate Negligible = No (\case Refl impossible) + decEq Moderate Minor = No (\case Refl impossible) + decEq Moderate Severe = No (\case Refl impossible) + decEq Moderate Critical = No (\case Refl impossible) + decEq Severe Negligible = No (\case Refl impossible) + decEq Severe Minor = No (\case Refl impossible) + decEq Severe Moderate = No (\case Refl impossible) + decEq Severe Critical = No (\case Refl impossible) + decEq Critical Negligible = No (\case Refl impossible) + decEq Critical Minor = No (\case Refl impossible) + decEq Critical Moderate = No (\case Refl impossible) + decEq Critical Severe = No (\case Refl impossible) -------------------------------------------------------------------------------- -- Harm Domain @@ -322,12 +388,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 @@ -365,50 +434,20 @@ ptrSize MacOS = 64 ptrSize BSD = 64 ptrSize WASM = 32 -||| Pointer type for platform -public export -CPtr : Platform -> Type -> Type -CPtr p _ = Bits (ptrSize p) - --------------------------------------------------------------------------------- --- Memory Layout Proofs --------------------------------------------------------------------------------- - -||| Proof that a type has a specific size -public export -data HasSize : Type -> Nat -> Type where - SizeProof : {0 t : Type} -> {n : Nat} -> HasSize t n - -||| Proof that a type has a specific alignment -public export -data HasAlignment : Type -> Nat -> Type where - AlignProof : {0 t : Type} -> {n : Nat} -> HasAlignment t n - -||| Size of C types (platform-specific) -public export -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 -cSizeOf p _ = ptrSize p `div` 8 - -||| Alignment of C types (platform-specific) -public export -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 -cAlignOf p _ = ptrSize p `div` 8 - -------------------------------------------------------------------------------- -- Constraint Evaluation Structs -------------------------------------------------------------------------------- +-- +-- The earlier template carried `CPtr`, `cSizeOf`/`cAlignOf` (which matched on +-- the *type-level* functions `CInt`/`CSize` — illegal as constructor patterns) +-- and vacuous `HasSize`/`HasAlignment` proofs (their single constructor proved +-- nothing for any `n`). Those did not compile and were unsound. The genuine, +-- machine-checked size/alignment guarantees for these structs live in +-- `Phronesiser.ABI.Layout` / `Phronesiser.ABI.Proofs` as `Divides`-backed +-- `CABICompliant` witnesses over the field offsets. -||| C-compatible struct for passing an ethical constraint across FFI +||| C-compatible struct for passing an ethical constraint across FFI. +||| 16 bytes: constraintId(0) modality(4) harmDomain(8) harmThreshold(12). public export record ConstraintStruct where constructor MkConstraintStruct @@ -417,17 +456,8 @@ record ConstraintStruct where harmDomain : Bits32 -- 4 bytes, offset 8 (HarmDomain as int, 0xFF = none) harmThreshold : Bits32 -- 4 bytes, offset 12 (HarmSeverity as int) -||| Prove the constraint struct has correct size (16 bytes, no padding needed) -public export -constraintStructSize : (p : Platform) -> HasSize ConstraintStruct 16 -constraintStructSize p = SizeProof - -||| Prove the constraint struct has correct alignment (4 bytes) -public export -constraintStructAlign : (p : Platform) -> HasAlignment ConstraintStruct 4 -constraintStructAlign p = AlignProof - -||| C-compatible struct for an audit decision result +||| C-compatible struct for an audit decision result. +||| 16 bytes: constraintId(0) decision(4) severity(8) reserved(12). public export record AuditResultStruct where constructor MkAuditResultStruct @@ -436,11 +466,6 @@ record AuditResultStruct where severity : Bits32 -- 4 bytes, offset 8 (HarmSeverity as int) reserved : Bits32 -- 4 bytes, offset 12 (padding for alignment) -||| Prove the audit result struct has correct size (16 bytes) -public export -auditResultStructSize : (p : Platform) -> HasSize AuditResultStruct 16 -auditResultStructSize p = SizeProof - -------------------------------------------------------------------------------- -- Verification -------------------------------------------------------------------------------- diff --git a/src/interface/abi/phronesiser-abi.ipkg b/src/interface/abi/phronesiser-abi.ipkg new file mode 100644 index 0000000..9f51a92 --- /dev/null +++ b/src/interface/abi/phronesiser-abi.ipkg @@ -0,0 +1,11 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Idris2 package for the phronesiser ABI formal proofs. +-- Build/check with: idris2 --build phronesiser-abi.ipkg (from src/interface/abi/) +package phronesiser-abi + +sourcedir = "." + +modules = Phronesiser.ABI.Types + , Phronesiser.ABI.Layout + , Phronesiser.ABI.Foreign + , Phronesiser.ABI.Proofs