From d8783c71058bed27afdab19468a8939ee4030eaf 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 f2c6a70..918cb06 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -5,7 +5,7 @@ version = "0.1.0" edition = "2024" authors = ["Jonathan D.A. Jewell "] description = "Make operations reversible and auditable in hostile environments via Oblíbený" -license-file = "LICENSE" +license = "MPL-2.0" repository = "https://github.com/hyperpolymath/oblibeniser" keywords = ["reversible-computing", "audit-trail", "undo", "oblibeny", "code-generation"] 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 297aca2d7845fb8db5fd6ed99e190cf082cc23a5 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Fri, 26 Jun 2026 11:36:40 +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 850780d..4cf2ff0 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 b5ed831..5f4f4c4 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 42d8daa..8731d33 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 69553d9182b5c9e746c821406ed56f753c2a7a83 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 26 Jun 2026 12:36:27 +0000 Subject: [PATCH 3/3] Fix Idris2 ABI proofs to genuinely compile and verify under 0.7.0 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The src/interface/abi/{Types,Layout,Foreign}.idr scaffold was never compiler-checked. This makes the oblibeniser ABI proofs typecheck cleanly (zero errors, zero warnings) under Idris2 0.7.0 with genuine proofs — no believe_me/postulate/holes. Types.idr: - DecEq Result: replace uncompilable `decEq _ _ = No absurd` with all 56 explicit off-diagonal `No (\case Refl impossible)` cases (8 constructors). - thisPlatform: drop the `%runElab` stub (needs ElabReflection) for `Linux`. - createHandle: solve the `So (ptr /= 0)` auto-proof via `choose` instead of leaving `Just (MkHandle ptr)` unsolved. - Remove the non-compiling CPtr (`Bits (ptrSize p)`) and the vacuous HasSize/HasAlignment/cSizeOf/cAlignOf block (it pattern-matched on Type and proved nothing); the real size/alignment guarantees live in Layout/Proofs. - Remove the duplicate `namespace Foreign` that collided with Foreign.idr. Layout.idr: - paddingFor: `minus` instead of Nat subtraction `-` (no Neg for Nat). - Add sound `decDivides`/`decFieldsAligned`; replace `alignUpCorrect`'s bogus `DivideBy ... Refl` with decidable `alignUpDivides`. - checkCABI: build a real CABICompliant witness via decFieldsAligned instead of the `?fieldsAlignedProof` hole. - offsetInBounds: honest `Maybe (So ...)` via `choose` (the universal `So` return type was unsound). - Concrete StructLayout values supply explicit `{sizeCorrect = Oh}` and `{aligned = DivideBy k Refl}` erased proofs. - *LayoutValid proofs: discharge the holes with explicit DivideBy witnesses; qualify layout names as `Layout.x` in types to avoid implicit-binding. Proofs.idr (new): machine-checked theorems — auditEntryCompliant / stateSnapshotCompliant / undoStackCompliant (built directly from per-field DivideBy witnesses), plus result-code pins okIsZero / notReversibleIsFive / inverseProofFailedIsSeven. Build layout: move flat files to src/interface/abi/Oblibeniser/ABI/ and add oblibeniser-abi.ipkg. `idris2 --build oblibeniser-abi.ipkg` exits 0 cleanly. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA --- .gitignore | 5 + .../abi/{ => Oblibeniser/ABI}/Foreign.idr | 0 .../abi/{ => Oblibeniser/ABI}/Layout.idr | 164 ++++++++++---- src/interface/abi/Oblibeniser/ABI/Proofs.idr | 91 ++++++++ .../abi/{ => Oblibeniser/ABI}/Types.idr | 204 ++++++++---------- src/interface/abi/oblibeniser-abi.ipkg | 11 + 6 files changed, 309 insertions(+), 166 deletions(-) rename src/interface/abi/{ => Oblibeniser/ABI}/Foreign.idr (100%) rename src/interface/abi/{ => Oblibeniser/ABI}/Layout.idr (57%) create mode 100644 src/interface/abi/Oblibeniser/ABI/Proofs.idr rename src/interface/abi/{ => Oblibeniser/ABI}/Types.idr (60%) create mode 100644 src/interface/abi/oblibeniser-abi.ipkg diff --git a/.gitignore b/.gitignore index 73f5db0..9bb544c 100644 --- a/.gitignore +++ b/.gitignore @@ -18,6 +18,11 @@ Thumbs.db /dist/ /out/ +# Idris2 build artefacts (nested ABI package build dirs) +**/build/ +*.ttc +*.ttm + # Dependencies /node_modules/ /vendor/ diff --git a/src/interface/abi/Foreign.idr b/src/interface/abi/Oblibeniser/ABI/Foreign.idr similarity index 100% rename from src/interface/abi/Foreign.idr rename to src/interface/abi/Oblibeniser/ABI/Foreign.idr diff --git a/src/interface/abi/Layout.idr b/src/interface/abi/Oblibeniser/ABI/Layout.idr similarity index 57% rename from src/interface/abi/Layout.idr rename to src/interface/abi/Oblibeniser/ABI/Layout.idr index 9d61f85..3630940 100644 --- a/src/interface/abi/Layout.idr +++ b/src/interface/abi/Oblibeniser/ABI/Layout.idr @@ -14,6 +14,8 @@ module Oblibeniser.ABI.Layout import Oblibeniser.ABI.Types import Data.Vect import Data.So +import Data.Nat +import Decidable.Equality %default total @@ -27,12 +29,7 @@ paddingFor : (offset : Nat) -> (alignment : Nat) -> Nat paddingFor offset alignment = if offset `mod` alignment == 0 then 0 - else 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 + else minus alignment (offset `mod` alignment) ||| Round up to next alignment boundary public export @@ -40,12 +37,34 @@ alignUp : (size : Nat) -> (alignment : Nat) -> Nat alignUp size alignment = size + paddingFor size alignment -||| Proof that alignUp produces aligned result +||| 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 + +||| 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 and is tracked as residual proof work; 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 = - -- Proof that (size + padding) is divisible by align - 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,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 @@ -113,14 +135,8 @@ public export PlatformLayout : Platform -> Type -> Type PlatformLayout p t = StructLayout -||| Verify layout is correct for all platforms -public export -verifyAllPlatforms : - (layouts : (p : Platform) -> PlatformLayout p t) -> - Either String () -verifyAllPlatforms layouts = - -- Check that layout is valid on all platforms - Right () +-- `verifyAllLayouts` is defined at the end of this module, after the concrete +-- layouts and `checkCABI` it depends on. -------------------------------------------------------------------------------- -- C ABI Compatibility @@ -134,12 +150,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 = - -- Verify C ABI rules - 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" -------------------------------------------------------------------------------- -- AuditEntry Layout (oblibeniser-specific) @@ -171,11 +190,24 @@ auditEntryLayout = ] 64 -- Total size: 64 bytes (with 4 bytes trailing padding) 8 -- Alignment: 8 bytes + {sizeCorrect = Oh} + {aligned = DivideBy 8 Refl} -||| Proof that AuditEntry layout is C-ABI compliant +||| Proof that AuditEntry layout is C-ABI compliant. Each field offset +||| divides its alignment: 0|8, 8|8, 16|8, 24|8, 32|8, 40|8, 48|8, 56|4. export -auditEntryLayoutValid : CABICompliant auditEntryLayout -auditEntryLayoutValid = CABIOk auditEntryLayout ?auditEntryFieldsAligned +auditEntryLayoutValid : CABICompliant Layout.auditEntryLayout +auditEntryLayoutValid = + CABIOk auditEntryLayout + (ConsField _ _ (DivideBy 0 Refl) + (ConsField _ _ (DivideBy 1 Refl) + (ConsField _ _ (DivideBy 2 Refl) + (ConsField _ _ (DivideBy 3 Refl) + (ConsField _ _ (DivideBy 4 Refl) + (ConsField _ _ (DivideBy 5 Refl) + (ConsField _ _ (DivideBy 6 Refl) + (ConsField _ _ (DivideBy 14 Refl) + NoFields)))))))) -------------------------------------------------------------------------------- -- StateSnapshot Layout (oblibeniser-specific) @@ -201,11 +233,21 @@ stateSnapshotLayout = ] 40 -- Total size: 40 bytes (with 4 bytes internal padding after stateSize) 8 -- Alignment: 8 bytes + {sizeCorrect = Oh} + {aligned = DivideBy 5 Refl} -||| Proof that StateSnapshot layout is C-ABI compliant +||| Proof that StateSnapshot layout is C-ABI compliant. Each field offset +||| divides its alignment: 0|8, 8|8, 16|8, 24|4, 32|8. export -stateSnapshotLayoutValid : CABICompliant stateSnapshotLayout -stateSnapshotLayoutValid = CABIOk stateSnapshotLayout ?snapshotFieldsAligned +stateSnapshotLayoutValid : CABICompliant Layout.stateSnapshotLayout +stateSnapshotLayoutValid = + CABIOk stateSnapshotLayout + (ConsField _ _ (DivideBy 0 Refl) + (ConsField _ _ (DivideBy 1 Refl) + (ConsField _ _ (DivideBy 2 Refl) + (ConsField _ _ (DivideBy 6 Refl) + (ConsField _ _ (DivideBy 4 Refl) + NoFields))))) -------------------------------------------------------------------------------- -- UndoStack Layout (oblibeniser-specific) @@ -228,25 +270,53 @@ undoStackLayout = ] 24 -- Total size: 24 bytes 8 -- Alignment: 8 bytes + {sizeCorrect = Oh} + {aligned = DivideBy 3 Refl} -||| Proof that UndoStack layout is C-ABI compliant +||| Proof that UndoStack layout is C-ABI compliant. Each field offset +||| divides its alignment: 0|8, 8|4, 12|4, 16|8. export -undoStackLayoutValid : CABICompliant undoStackLayout -undoStackLayoutValid = CABIOk undoStackLayout ?undoStackFieldsAligned +undoStackLayoutValid : CABICompliant Layout.undoStackLayout +undoStackLayoutValid = + CABIOk undoStackLayout + (ConsField _ _ (DivideBy 0 Refl) + (ConsField _ _ (DivideBy 2 Refl) + (ConsField _ _ (DivideBy 3 Refl) + (ConsField _ _ (DivideBy 2 Refl) + NoFields)))) -------------------------------------------------------------------------------- -- Offset Calculation -------------------------------------------------------------------------------- -||| Calculate field offset with proof of correctness +||| Look up a field's offset 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) -> + 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 + +||| Verify that all oblibeniser concrete layouts are C-ABI compliant. This +||| fails (Left) if any concrete layout is misaligned, rather than asserting +||| it. Each layout's `FieldsAligned` witness is built by `checkCABI`'s sound +||| `decFieldsAligned`. public export -offsetInBounds : (layout : StructLayout) -> (f : Field) -> So (f.offset + f.size <= layout.totalSize) -offsetInBounds layout f = ?offsetInBoundsProof +verifyAllLayouts : Either String () +verifyAllLayouts = do + _ <- checkCABI auditEntryLayout + _ <- checkCABI stateSnapshotLayout + _ <- checkCABI undoStackLayout + Right () diff --git a/src/interface/abi/Oblibeniser/ABI/Proofs.idr b/src/interface/abi/Oblibeniser/ABI/Proofs.idr new file mode 100644 index 0000000..f1ee9ff --- /dev/null +++ b/src/interface/abi/Oblibeniser/ABI/Proofs.idr @@ -0,0 +1,91 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Machine-checked proofs over the oblibeniser ABI. +||| +||| These are not runtime tests — they are propositional statements the Idris2 +||| type checker must discharge at compile time. If any concrete ABI struct +||| layout were misaligned, the result-code 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 avoid routing them through `Nat` division, which is a +||| primitive that does not reduce at the type level. + +module Oblibeniser.ABI.Proofs + +import Oblibeniser.ABI.Types +import Oblibeniser.ABI.Layout +import Data.So +import Data.Vect + +%default total + +-------------------------------------------------------------------------------- +-- The concrete reversible-computing FFI struct layouts are C-ABI compliant. +-------------------------------------------------------------------------------- + +||| Every field offset in the AuditEntry layout divides its alignment: +||| 0|8, 8|8, 16|8, 24|8, 32|8, 40|8, 48|8, 56|4. +export +auditEntryCompliant : CABICompliant Layout.auditEntryLayout +auditEntryCompliant = + CABIOk auditEntryLayout + (ConsField _ _ (DivideBy 0 Refl) + (ConsField _ _ (DivideBy 1 Refl) + (ConsField _ _ (DivideBy 2 Refl) + (ConsField _ _ (DivideBy 3 Refl) + (ConsField _ _ (DivideBy 4 Refl) + (ConsField _ _ (DivideBy 5 Refl) + (ConsField _ _ (DivideBy 6 Refl) + (ConsField _ _ (DivideBy 14 Refl) + NoFields)))))))) + +||| Every field offset in the StateSnapshot layout divides its alignment: +||| 0|8, 8|8, 16|8, 24|4, 32|8. +export +stateSnapshotCompliant : CABICompliant Layout.stateSnapshotLayout +stateSnapshotCompliant = + CABIOk stateSnapshotLayout + (ConsField _ _ (DivideBy 0 Refl) + (ConsField _ _ (DivideBy 1 Refl) + (ConsField _ _ (DivideBy 2 Refl) + (ConsField _ _ (DivideBy 6 Refl) + (ConsField _ _ (DivideBy 4 Refl) + NoFields))))) + +||| Every field offset in the UndoStack layout divides its alignment: +||| 0|8, 8|4, 12|4, 16|8. +export +undoStackCompliant : CABICompliant Layout.undoStackLayout +undoStackCompliant = + CABIOk undoStackLayout + (ConsField _ _ (DivideBy 0 Refl) + (ConsField _ _ (DivideBy 2 Refl) + (ConsField _ _ (DivideBy 3 Refl) + (ConsField _ _ (DivideBy 2 Refl) + NoFields)))) + +-------------------------------------------------------------------------------- +-- Result-code encoding: the integer contract the Zig FFI depends on. +-------------------------------------------------------------------------------- + +||| Success is encoded as 0, matching the C convention. +export +okIsZero : resultToInt Ok = 0 +okIsZero = Refl + +||| NotReversible is encoded as 5 — the inverse-computation FFI returns this +||| code and the safe wrappers decode it back to `NotReversible`. +export +notReversibleIsFive : resultToInt NotReversible = 5 +notReversibleIsFive = Refl + +||| InverseProofFailed is encoded as 7 — the central correctness failure code +||| for oblibeniser's reversibility guarantee. +export +inverseProofFailedIsSeven : resultToInt InverseProofFailed = 7 +inverseProofFailedIsSeven = Refl diff --git a/src/interface/abi/Types.idr b/src/interface/abi/Oblibeniser/ABI/Types.idr similarity index 60% rename from src/interface/abi/Types.idr rename to src/interface/abi/Oblibeniser/ABI/Types.idr index 08a1dd2..be45e7e 100644 --- a/src/interface/abi/Types.idr +++ b/src/interface/abi/Oblibeniser/ABI/Types.idr @@ -15,6 +15,7 @@ module Oblibeniser.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 the 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 -------------------------------------------------------------------------------- -- Core Result Codes @@ -72,7 +71,9 @@ resultToInt NotReversible = 5 resultToInt AuditViolation = 6 resultToInt InverseProofFailed = 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 @@ -83,7 +84,62 @@ DecEq Result where decEq NotReversible NotReversible = Yes Refl decEq AuditViolation AuditViolation = Yes Refl decEq InverseProofFailed InverseProofFailed = 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 NotReversible = No (\case Refl impossible) + decEq Ok AuditViolation = No (\case Refl impossible) + decEq Ok InverseProofFailed = 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 NotReversible = No (\case Refl impossible) + decEq Error AuditViolation = No (\case Refl impossible) + decEq Error InverseProofFailed = 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 NotReversible = No (\case Refl impossible) + decEq InvalidParam AuditViolation = No (\case Refl impossible) + decEq InvalidParam InverseProofFailed = 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 NotReversible = No (\case Refl impossible) + decEq OutOfMemory AuditViolation = No (\case Refl impossible) + decEq OutOfMemory InverseProofFailed = 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 NotReversible = No (\case Refl impossible) + decEq NullPointer AuditViolation = No (\case Refl impossible) + decEq NullPointer InverseProofFailed = No (\case Refl impossible) + decEq NotReversible Ok = No (\case Refl impossible) + decEq NotReversible Error = No (\case Refl impossible) + decEq NotReversible InvalidParam = No (\case Refl impossible) + decEq NotReversible OutOfMemory = No (\case Refl impossible) + decEq NotReversible NullPointer = No (\case Refl impossible) + decEq NotReversible AuditViolation = No (\case Refl impossible) + decEq NotReversible InverseProofFailed = No (\case Refl impossible) + decEq AuditViolation Ok = No (\case Refl impossible) + decEq AuditViolation Error = No (\case Refl impossible) + decEq AuditViolation InvalidParam = No (\case Refl impossible) + decEq AuditViolation OutOfMemory = No (\case Refl impossible) + decEq AuditViolation NullPointer = No (\case Refl impossible) + decEq AuditViolation NotReversible = No (\case Refl impossible) + decEq AuditViolation InverseProofFailed = No (\case Refl impossible) + decEq InverseProofFailed Ok = No (\case Refl impossible) + decEq InverseProofFailed Error = No (\case Refl impossible) + decEq InverseProofFailed InvalidParam = No (\case Refl impossible) + decEq InverseProofFailed OutOfMemory = No (\case Refl impossible) + decEq InverseProofFailed NullPointer = No (\case Refl impossible) + decEq InverseProofFailed NotReversible = No (\case Refl impossible) + decEq InverseProofFailed AuditViolation = No (\case Refl impossible) -------------------------------------------------------------------------------- -- Opaque Handles @@ -95,12 +151,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 @@ -233,113 +292,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 - --------------------------------------------------------------------------------- --- Reversible Operation Struct Layout Proofs --------------------------------------------------------------------------------- - -||| StateSnapshot has 5 fields: snapshotId(8) + timestamp(8) + stateHash(8) + -||| stateSize(4) + padding(4) + statePtr(8) = 40 bytes, aligned to 8 -public export -stateSnapshotSize : (p : Platform) -> HasSize StateSnapshot 40 -stateSnapshotSize p = SizeProof - -public export -stateSnapshotAlign : (p : Platform) -> HasAlignment StateSnapshot 8 -stateSnapshotAlign p = AlignProof - -||| AuditEntry has 8 fields laid out for C-ABI compatibility. -||| 7x Bits64 (56 bytes) + 1x Bits32 (4 bytes) + 4 padding = 64 bytes -public export -auditEntrySize : (p : Platform) -> HasSize AuditEntry 64 -auditEntrySize p = SizeProof - -public export -auditEntryAlign : (p : Platform) -> HasAlignment AuditEntry 8 -auditEntryAlign p = AlignProof - -||| UndoStack: stackPtr(8) + depth(4) + maxDepth(4) + topHash(8) = 24 bytes -public export -undoStackSize : (p : Platform) -> HasSize UndoStack 24 -undoStackSize p = SizeProof - -public export -undoStackAlign : (p : Platform) -> HasAlignment UndoStack 8 -undoStackAlign p = AlignProof - --------------------------------------------------------------------------------- --- FFI Declarations --------------------------------------------------------------------------------- - -||| Declare external C functions -||| These will be implemented in Zig FFI -namespace Foreign - - ||| Record a forward operation, returning its operation ID - export - %foreign "C:oblibeniser_record_operation, liboblibeniser" - prim__recordOperation : Bits64 -> Bits64 -> PrimIO Bits64 - - ||| Compute and apply the inverse of an operation - export - %foreign "C:oblibeniser_apply_inverse, liboblibeniser" - prim__applyInverse : Bits64 -> Bits64 -> PrimIO Bits32 - - ||| Safe wrapper around record operation - export - recordOperation : Handle -> Bits64 -> IO (Either Result Bits64) - recordOperation h namePtr = do - result <- primIO (prim__recordOperation (handlePtr h) namePtr) - if result == 0 - then pure (Left Error) - else pure (Right result) - - ||| Safe wrapper around apply inverse - export - applyInverse : Handle -> Bits64 -> IO (Either Result ()) - applyInverse h opId = do - result <- primIO (prim__applyInverse (handlePtr h) opId) - pure $ case result of - 0 => Right () - _ => Left Error +||| Note: the precise C size/alignment guarantees for the reversible-computing +||| structs (StateSnapshot, AuditEntry, UndoStack) are not asserted here via +||| vacuous `HasSize`/`HasAlignment` witnesses (the original scaffold did so +||| with constructors that proved nothing, and also pattern-matched on `Type`, +||| which Idris2 cannot do). Instead they are captured *genuinely* in +||| `Oblibeniser.ABI.Layout` as `StructLayout` values carrying real `Divides` +||| alignment proofs, and discharged as machine-checked theorems in +||| `Oblibeniser.ABI.Proofs` (`auditEntryCompliant`, `stateSnapshotCompliant`, +||| `undoStackCompliant`). + +-- The FFI primitive and safe-wrapper declarations live exclusively in +-- `Oblibeniser.ABI.Foreign`. A duplicate `namespace Foreign` here previously +-- redeclared `prim__applyInverse`/`recordOperation`, which collided with the +-- real declarations once `Foreign` imported `Types` (ambiguous elaboration). -------------------------------------------------------------------------------- -- Verification diff --git a/src/interface/abi/oblibeniser-abi.ipkg b/src/interface/abi/oblibeniser-abi.ipkg new file mode 100644 index 0000000..05368cd --- /dev/null +++ b/src/interface/abi/oblibeniser-abi.ipkg @@ -0,0 +1,11 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Idris2 package for the oblibeniser ABI formal proofs. +-- Build/check with: idris2 --build oblibeniser-abi.ipkg (from src/interface/abi/) +package oblibeniser-abi + +sourcedir = "." + +modules = Oblibeniser.ABI.Types + , Oblibeniser.ABI.Layout + , Oblibeniser.ABI.Foreign + , Oblibeniser.ABI.Proofs