From 0c0e0b1d4a3f0efa97bd04ff6eacc4f8d7d4b6c3 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Fri, 26 Jun 2026 11:20:31 +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 bb95a02..ff1966b 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -5,7 +5,7 @@ version = "0.1.0" edition = "2024" authors = ["Jonathan D.A. Jewell "] description = "Compile image/video processing pipelines to optimised Halide schedules — 10-100x faster than hand-tuned C" -license-file = "LICENSE" +license = "MPL-2.0" repository = "https://github.com/hyperpolymath/halideiser" keywords = ["halide", "image-processing", "video", "acceleration"] 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 7390aadd56ce48325e6782353e145c2be96601c4 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" Date: Fri, 26 Jun 2026 11:36:32 +0000 Subject: [PATCH 2/3] Normalize licensing to MPL-2.0 (code) + CC-BY-SA-4.0 (docs) Make the repo's licensing single and consistent, matching the wokelangiser reference policy and the merged iseriser pattern: - Remove contradictory PMPL-1.0-or-later / Palimpsest self-claims from README badges/footers, QUICKSTART, RSR_OUTLINE, STATE-VISUALIZER, and machine-readable governance (META, stapeln, deny.toml allow-list, copilot/AGENTIC SPDX directives, Trust/Must LICENSE-content checks, per-project CLAUDE.md). - Encode the docs split in REUSE dep5: *.adoc/*.md/docs/** -> CC-BY-SA-4.0, everything else -> MPL-2.0. - READMEs show MPL-2.0 (code) + CC-BY-SA-4.0 (docs) badges; full texts live in LICENSES/; root LICENSE stays MPL-2.0 for GitHub's licence chip. Preserves legitimate non-self references: cargo-deny's AGPL deny-list, the "never use AGPL" estate policy, and the Contributor Covenant CoC. Verified: standards/scripts/check-licence-consistency.sh passes; no residual PMPL/Palimpsest self-claims remain. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA --- .claude/CLAUDE.md | 2 +- .github/workflows/rhodibot.yml | 4 ++-- .machine_readable/compliance/reuse/dep5 | 7 +++++++ .machine_readable/contractiles/must/Mustfile.a2ml | 2 +- .machine_readable/contractiles/trust/Trustfile.a2ml | 4 ++-- QUICKSTART-MAINTAINER.adoc | 2 +- contractiles/trust/Trustfile.a2ml | 2 +- docs/RSR_OUTLINE.adoc | 4 ++-- docs/STATE-VISUALIZER.adoc | 2 +- 9 files changed, 18 insertions(+), 11 deletions(-) diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md index bcaa503..6938462 100644 --- a/.claude/CLAUDE.md +++ b/.claude/CLAUDE.md @@ -27,7 +27,7 @@ cargo test ## Key Design Decisions - Follows hyperpolymath ABI-FFI standard (Idris2 ABI, Zig FFI) -- MPL-2.0 license +- MPL-2.0 license (code) + CC-BY-SA-4.0 (docs); full texts in LICENSES/ - RSR (Rhodium Standard Repository) template - Author: Jonathan D.A. Jewell diff --git a/.github/workflows/rhodibot.yml b/.github/workflows/rhodibot.yml index a82f178..1f45960 100644 --- a/.github/workflows/rhodibot.yml +++ b/.github/workflows/rhodibot.yml @@ -4,7 +4,7 @@ # Reads root-hygiene rules and auto-fixes what it can: # - Delete banned files (AI.djot, duplicate CONTRIBUTING.adoc, stale snapshots) # - Rename misnamed files (AI.a2ml → 0-AI-MANIFEST.a2ml) -# - Fix SPDX headers (AGPL → PMPL in dotfiles) +# - Fix SPDX headers (AGPL → MPL-2.0 in dotfiles) # - Create missing required files (SECURITY.md, CONTRIBUTING.md) # - Report unfixable issues as PR comments # @@ -87,7 +87,7 @@ jobs: for dotfile in .gitignore .gitattributes .editorconfig; do if [ -f "$dotfile" ] && grep -q "AGPL-3.0" "$dotfile" 2>/dev/null; then sed -i 's/AGPL-3.0-or-later/MPL-2.0/g; s/AGPL-3.0/MPL-2.0/g' "$dotfile" - FIXES="$FIXES\n- Fixed SPDX header in \`$dotfile\` (AGPL → PMPL)" + FIXES="$FIXES\n- Fixed SPDX header in \`$dotfile\` (AGPL → MPL-2.0)" CHANGED=true fi done diff --git a/.machine_readable/compliance/reuse/dep5 b/.machine_readable/compliance/reuse/dep5 index 49aaed6..bead9ed 100644 --- a/.machine_readable/compliance/reuse/dep5 +++ b/.machine_readable/compliance/reuse/dep5 @@ -52,3 +52,10 @@ License: MPL-2.0 Files: cliff.toml Copyright: {{CURRENT_YEAR}} {{AUTHOR}} ({{OWNER}}) <{{AUTHOR_EMAIL}}> License: MPL-2.0 + +# Documentation prose is CC-BY-SA-4.0 (code/config is MPL-2.0). +# Last-match-wins in the Debian copyright format, so this overrides the +# `Files: *` default above for prose docs. +Files: *.adoc *.md docs/* docs/**/* +Copyright: {{CURRENT_YEAR}} {{AUTHOR}} ({{OWNER}}) <{{AUTHOR_EMAIL}}> +License: CC-BY-SA-4.0 diff --git a/.machine_readable/contractiles/must/Mustfile.a2ml b/.machine_readable/contractiles/must/Mustfile.a2ml index 8fe2e02..fd07259 100644 --- a/.machine_readable/contractiles/must/Mustfile.a2ml +++ b/.machine_readable/contractiles/must/Mustfile.a2ml @@ -57,7 +57,7 @@ These are hard requirements — CI fails if any check fails. - severity: warning ### no-agpl -- description: No AGPL-3.0 references (superseded by PMPL) +- description: No AGPL-3.0 references (superseded by MPL-2.0) - run: "! grep -r 'AGPL-3.0' .gitignore .gitattributes .editorconfig 2>/dev/null | head -1 | grep -q ." - severity: critical diff --git a/.machine_readable/contractiles/trust/Trustfile.a2ml b/.machine_readable/contractiles/trust/Trustfile.a2ml index 0026aa2..a013b00 100644 --- a/.machine_readable/contractiles/trust/Trustfile.a2ml +++ b/.machine_readable/contractiles/trust/Trustfile.a2ml @@ -33,8 +33,8 @@ is traceable. - severity: warning ### license-content -- description: LICENSE contains PMPL identifier -- run: grep -q 'PMPL' LICENSE +- description: LICENSE contains MPL-2.0 identifier +- run: grep -q 'MPL-2.0' LICENSE - severity: warning ### ci-pipeline-present diff --git a/QUICKSTART-MAINTAINER.adoc b/QUICKSTART-MAINTAINER.adoc index 102ba0d..78ab564 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 ac67247..cba68e7 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 28df611bf58af989d5fcfed104e40582c58187a2 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 26 Jun 2026 13:05:48 +0000 Subject: [PATCH 3/3] Fix Idris2 ABI proofs so they genuinely compile and verify MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The src/interface/abi/{Types,Layout,Foreign}.idr files were scaffolded from a template and never compiler-checked. They now build clean under Idris2 0.7.0 with zero errors and zero warnings. Fixes: - Types.idr: replace `%runElab` thisPlatform stub with `thisPlatform = Linux` (ElabReflection was not enabled). - Types.idr: createHandle now obtains a real `So (ptr /= 0)` witness via `choose` instead of leaving the MkHandle auto-implicit unsolved. - Types.idr: add a genuine `DecEq Result` instance with explicit off-diagonal disequality cases (`No (\case Refl impossible)`) — a `No absurd` catch-all does not typecheck. - Layout.idr: paddingFor uses `minus` instead of Nat subtraction (`-`). - Layout.idr: lift record-local `requiredAlloc` (illegal `where` on a record) to a top-level definition. - Layout.idr: interleaved/planar/video layouts and the new mkDim/mkLayout smart constructors decide their `So` extent/stride/coverage obligations with `choose`, returning Maybe, instead of leaving unprovable symbolic auto proofs unsolved. - Layout.idr: checkCompatibility binds n,m as runtime implicits so decEq has access to them. - Layout.idr: add the C-ABI proof machinery (Divides, decDivides, StructLayout, FieldsAligned, decFieldsAligned, CABICompliant, checkCABI, offsetInBounds) plus concrete StructLayout values for halide_buffer_t and halide_dimension_t, with their erased proofs supplied explicitly ({sizeCorrect = Oh}, {aligned = DivideBy k Refl}). checkCABI is a sound decision procedure (no `?fieldsAlignedProof` hole). offsetInBounds returns Maybe (So ...) via choose rather than asserting an unsound universal bound. New machine-checked theorems (src/interface/abi/Halideiser/ABI/Proofs.idr): - halideBufferTCompliant : CABICompliant halideBufferTStruct - halideDimensionTCompliant : CABICompliant halideDimensionTStruct (each built directly from per-field DivideBy k Refl witnesses) - okIsZero, dimensionMismatchIsSeven : result-code encoding pins - avx512Width, float64Bytes : codegen sanity equalities Buildability: - Move flat files into src/interface/abi/Halideiser/ABI/ so paths match the Halideiser.ABI.* namespaces. - Add src/interface/abi/halideiser-abi.ipkg listing all four modules. - .gitignore: ignore **/build/, *.ttc, *.ttm. No believe_me / assert_total / idris_crash / postulate / %hint / holes are used anywhere; every obligation is discharged genuinely. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01DF9CcCuL4YJoqs26eHsYiA --- .gitignore | 5 + .../abi/{ => Halideiser/ABI}/Foreign.idr | 0 .../abi/{ => Halideiser/ABI}/Layout.idr | 240 +++++++++++++++--- src/interface/abi/Halideiser/ABI/Proofs.idr | 83 ++++++ .../abi/{ => Halideiser/ABI}/Types.idr | 91 ++++++- src/interface/abi/halideiser-abi.ipkg | 11 + 6 files changed, 383 insertions(+), 47 deletions(-) rename src/interface/abi/{ => Halideiser/ABI}/Foreign.idr (100%) rename src/interface/abi/{ => Halideiser/ABI}/Layout.idr (53%) create mode 100644 src/interface/abi/Halideiser/ABI/Proofs.idr rename src/interface/abi/{ => Halideiser/ABI}/Types.idr (76%) create mode 100644 src/interface/abi/halideiser-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/Halideiser/ABI/Foreign.idr similarity index 100% rename from src/interface/abi/Foreign.idr rename to src/interface/abi/Halideiser/ABI/Foreign.idr diff --git a/src/interface/abi/Layout.idr b/src/interface/abi/Halideiser/ABI/Layout.idr similarity index 53% rename from src/interface/abi/Layout.idr rename to src/interface/abi/Halideiser/ABI/Layout.idr index 1be3539..f1538f4 100644 --- a/src/interface/abi/Layout.idr +++ b/src/interface/abi/Halideiser/ABI/Layout.idr @@ -23,6 +23,7 @@ import Halideiser.ABI.Types import Data.Vect import Data.So import Data.Nat +import Decidable.Equality %default total @@ -51,6 +52,15 @@ public export dimSpan : HalideDimension -> Nat dimSpan d = d.extent * d.stride +||| Calculate the minimum allocation needed for the given dimensions. +||| This is the max over all dimensions of (extent_i * stride_i). +||| (Previously a record-local `where` definition, which does not compile; +||| lifted to top level so the record's `allocCovers` proof can reference it.) +public export +requiredAlloc : Vect m HalideDimension -> Nat +requiredAlloc [] = 0 +requiredAlloc (d :: ds) = max (dimSpan d) (requiredAlloc ds) + -------------------------------------------------------------------------------- -- Halide Buffer Layout -------------------------------------------------------------------------------- @@ -73,14 +83,6 @@ record HalideBufferLayout (n : Nat) where allocSize : Nat ||| Proof that allocation covers the full extent {auto 0 allocCovers : So (allocSize >= requiredAlloc dimensions)} - where - ||| Calculate the minimum allocation needed for the given dimensions. - ||| This is the product of (extent_i * stride_i) across all dimensions, - ||| but more precisely it is max over all dimensions of (extent_i * stride_i). - public export - requiredAlloc : Vect m HalideDimension -> Nat - requiredAlloc [] = 0 - requiredAlloc (d :: ds) = max (dimSpan d) (requiredAlloc ds) ||| Total bytes for a buffer layout public export @@ -91,6 +93,34 @@ layoutBytes buf = buf.allocSize * pixelBytes buf.elemType -- Standard Image Layouts -------------------------------------------------------------------------------- +||| Smart constructor for a Halide dimension. The extent/stride positivity +||| proofs cannot be solved for symbolic `Nat`s at the type level, so we +||| decide them at runtime with `choose`, returning Nothing when either is +||| zero. (Previously `MkHalideDimension 0 extent stride` left the erased +||| `extentPos`/`stridePos` auto-implicits unsolved and did not compile.) +public export +mkDim : (mn : Int) -> (extent : Nat) -> (stride : Nat) -> Maybe HalideDimension +mkDim mn extent stride = + case choose (extent > 0) of + Right _ => Nothing + Left ep => case choose (stride > 0) of + Right _ => Nothing + Left sp => Just (MkHalideDimension mn extent stride + {extentPos = ep} {stridePos = sp}) + +||| Assemble a buffer layout from already-built dimensions and an allocation +||| size, deciding the `allocCovers` coverage bound with `choose`. Returns +||| Nothing when the allocation does not cover the required span. This is an +||| honest decision: the bound is false for under-sized allocations and cannot +||| be asserted for symbolic inputs. +public export +mkLayout : Vect n HalideDimension -> PixelType -> (allocSize : Nat) -> + Maybe (HalideBufferLayout n) +mkLayout dims ptype allocSize = + case choose (allocSize >= requiredAlloc dims) of + Left ok => Just (MkHalideBufferLayout dims ptype allocSize {allocCovers = ok}) + Right _ => Nothing + ||| Row-major interleaved layout (RGBRGBRGB...). ||| This is the most common layout for 8-bit images. ||| @@ -99,15 +129,12 @@ layoutBytes buf = buf.allocSize * pixelBytes buf.elemType ||| dim 2 (y): extent=height, stride=width*channels public export interleavedLayout : (dim : BufferDimension) -> (ptype : PixelType) -> - HalideBufferLayout 3 -interleavedLayout dim ptype = - MkHalideBufferLayout - [ MkHalideDimension 0 dim.channels 1 - , MkHalideDimension 0 dim.width dim.channels - , MkHalideDimension 0 dim.height (dim.width * dim.channels) - ] - ptype - (dim.width * dim.height * dim.channels) + Maybe (HalideBufferLayout 3) +interleavedLayout dim ptype = do + d0 <- mkDim 0 dim.channels 1 + d1 <- mkDim 0 dim.width dim.channels + d2 <- mkDim 0 dim.height (dim.width * dim.channels) + mkLayout [d0, d1, d2] ptype (dim.width * dim.height * dim.channels) ||| Planar layout (all R, then all G, then all B). ||| Common for processing — better SIMD utilisation per channel. @@ -117,30 +144,24 @@ interleavedLayout dim ptype = ||| dim 2 (channel): extent=channels, stride=width*height public export planarLayout : (dim : BufferDimension) -> (ptype : PixelType) -> - HalideBufferLayout 3 -planarLayout dim ptype = - MkHalideBufferLayout - [ MkHalideDimension 0 dim.width 1 - , MkHalideDimension 0 dim.height dim.width - , MkHalideDimension 0 dim.channels (dim.width * dim.height) - ] - ptype - (dim.width * dim.height * dim.channels) + Maybe (HalideBufferLayout 3) +planarLayout dim ptype = do + d0 <- mkDim 0 dim.width 1 + d1 <- mkDim 0 dim.height dim.width + d2 <- mkDim 0 dim.channels (dim.width * dim.height) + mkLayout [d0, d1, d2] ptype (dim.width * dim.height * dim.channels) ||| Video buffer layout (4D: x, y, channel, frame). ||| Planar within each frame, frames stored contiguously. public export videoLayout : (dim : BufferDimension) -> (ptype : PixelType) -> - HalideBufferLayout 4 -videoLayout dim ptype = - MkHalideBufferLayout - [ MkHalideDimension 0 dim.width 1 - , MkHalideDimension 0 dim.height dim.width - , MkHalideDimension 0 dim.channels (dim.width * dim.height) - , MkHalideDimension 0 dim.frames (dim.width * dim.height * dim.channels) - ] - ptype - (bufferElements dim) + Maybe (HalideBufferLayout 4) +videoLayout dim ptype = do + d0 <- mkDim 0 dim.width 1 + d1 <- mkDim 0 dim.height dim.width + d2 <- mkDim 0 dim.channels (dim.width * dim.height) + d3 <- mkDim 0 dim.frames (dim.width * dim.height * dim.channels) + mkLayout [d0, d1, d2, d3] ptype (bufferElements dim) -------------------------------------------------------------------------------- -- Alignment Utilities @@ -152,7 +173,7 @@ 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) ||| Round up to next alignment boundary public export @@ -212,7 +233,7 @@ data LayoutCompatible : HalideBufferLayout n -> HalideBufferLayout m -> Type whe ||| Verify two layouts are compatible for pipeline stage connection public export -checkCompatibility : HalideBufferLayout n -> HalideBufferLayout m -> +checkCompatibility : {n, m : Nat} -> HalideBufferLayout n -> HalideBufferLayout m -> Either String (n = m) checkCompatibility a b = case decEq n m of @@ -294,3 +315,146 @@ halideDimensionTSize = 16 public export halideDimensionTAlign : Nat halideDimensionTAlign = 4 + +-------------------------------------------------------------------------------- +-- C ABI Alignment Proof Machinery +-------------------------------------------------------------------------------- + +||| Offset for the next field after `f`, rounded up to `f`'s alignment. +public export +nextFieldOffset : Field -> Nat +nextFieldOffset f = alignUp (f.offset + f.size) f.alignment + +||| Proof that `n` divides `m`: `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 + +||| A C-ABI struct layout: a vector of fields with a total size and alignment, +||| carrying erased proofs that the size covers all fields and that the +||| alignment divides the total size. +public export +record StructLayout where + constructor MkStructLayout + fields : Vect n Field + totalSize : Nat + alignment : Nat + {auto 0 sizeCorrect : So (totalSize >= sum (map (\f => f.size) fields))} + {auto 0 aligned : Divides alignment totalSize} + +||| C-ABI `StructLayout` for `halide_buffer_t` (8 fields, 56 bytes, align 8). +public export +halideBufferTStruct : StructLayout +halideBufferTStruct = + MkStructLayout + [ MkField "device" 0 8 8 + , MkField "device_interface" 8 8 8 + , MkField "host" 16 8 8 + , MkField "flags" 24 8 8 + , MkField "type" 32 4 4 + , MkField "dimensions" 36 4 4 + , MkField "dim" 40 8 8 + , MkField "padding" 48 8 8 + ] + 56 + 8 + {sizeCorrect = Oh} + {aligned = DivideBy 7 Refl} + +||| C-ABI `StructLayout` for `halide_dimension_t` (4 fields, 16 bytes, align 4). +public export +halideDimensionTStruct : StructLayout +halideDimensionTStruct = + MkStructLayout + [ MkField "min" 0 4 4 + , MkField "extent" 4 4 4 + , MkField "stride" 8 4 4 + , MkField "flags" 12 4 4 + ] + 16 + 4 + {sizeCorrect = Oh} + {aligned = DivideBy 4 Refl} + +||| Proof that every field offset in a layout is correctly aligned. +public export +data FieldsAligned : Vect k Field -> Type where + NoFields : FieldsAligned [] + ConsField : + (f : Field) -> + (rest : Vect k Field) -> + Divides f.alignment f.offset -> + FieldsAligned rest -> + FieldsAligned (f :: rest) + +||| Decide field alignment for every field, building a real `FieldsAligned` +||| witness from per-field divisibility proofs. +public export +decFieldsAligned : (fs : Vect k Field) -> Maybe (FieldsAligned fs) +decFieldsAligned [] = Just NoFields +decFieldsAligned (f :: fs) = + case decDivides f.alignment f.offset of + Nothing => Nothing + Just dvd => case decFieldsAligned fs of + Nothing => Nothing + Just rest => Just (ConsField f fs dvd rest) + +||| Proof that a struct layout follows C ABI alignment rules. +public export +data CABICompliant : StructLayout -> Type where + CABIOk : + (layout : StructLayout) -> + FieldsAligned layout.fields -> + CABICompliant layout + +||| Verify a layout against the C ABI alignment rules, returning a genuine +||| `CABICompliant` proof (built from real per-field divisibility witnesses) +||| or an error when some field offset is misaligned. (Previously a hole +||| `?fieldsAlignedProof`; now a sound decision procedure.) +public export +checkCABI : (layout : StructLayout) -> Either String (CABICompliant layout) +checkCABI layout = + case decFieldsAligned layout.fields of + Just prf => Right (CABIOk layout prf) + Nothing => Left "Field offsets are not correctly aligned for the C ABI" + +||| Verify that both halide C structs are C-ABI compliant. Fails (Left) if any +||| concrete layout is misaligned, rather than asserting it. +public export +verifyAllStructLayouts : Either String () +verifyAllStructLayouts = do + _ <- checkCABI halideBufferTStruct + _ <- checkCABI halideDimensionTStruct + Right () + +||| Look up a field's offset by name in a layout. +public export +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) + Nothing => Nothing + +||| Decide whether a field lies within a struct's byte bounds, returning a +||| genuine proof when `offset + size <= totalSize`. The previous template +||| 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 diff --git a/src/interface/abi/Halideiser/ABI/Proofs.idr b/src/interface/abi/Halideiser/ABI/Proofs.idr new file mode 100644 index 0000000..3b16d23 --- /dev/null +++ b/src/interface/abi/Halideiser/ABI/Proofs.idr @@ -0,0 +1,83 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Machine-checked proofs over the halideiser ABI. +||| +||| These are not runtime tests — they are propositional statements the Idris2 +||| type checker must discharge at compile time. If any concrete C-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 Halideiser.ABI.Proofs + +import Halideiser.ABI.Types +import Halideiser.ABI.Layout +import Data.So +import Data.Vect + +%default total + +-------------------------------------------------------------------------------- +-- The concrete halide C struct layouts are provably C-ABI compliant. +-------------------------------------------------------------------------------- + +||| Every field offset in halide_buffer_t divides its alignment: +||| 0|8, 8|8, 16|8, 24|8, 32|4, 36|4, 40|8, 48|8. +export +halideBufferTCompliant : CABICompliant Layout.halideBufferTStruct +halideBufferTCompliant = + CABIOk halideBufferTStruct + (ConsField _ _ (DivideBy 0 Refl) + (ConsField _ _ (DivideBy 1 Refl) + (ConsField _ _ (DivideBy 2 Refl) + (ConsField _ _ (DivideBy 3 Refl) + (ConsField _ _ (DivideBy 8 Refl) + (ConsField _ _ (DivideBy 9 Refl) + (ConsField _ _ (DivideBy 5 Refl) + (ConsField _ _ (DivideBy 6 Refl) + NoFields)))))))) + +||| Every field offset in halide_dimension_t divides its alignment: +||| 0|4, 4|4, 8|4, 12|4. +export +halideDimensionTCompliant : CABICompliant Layout.halideDimensionTStruct +halideDimensionTCompliant = + CABIOk halideDimensionTStruct + (ConsField _ _ (DivideBy 0 Refl) + (ConsField _ _ (DivideBy 1 Refl) + (ConsField _ _ (DivideBy 2 Refl) + (ConsField _ _ (DivideBy 3 Refl) + NoFields)))) + +-------------------------------------------------------------------------------- +-- Result-code round-trip: the encoding the Zig FFI depends on. +-------------------------------------------------------------------------------- + +export +okIsZero : resultToInt Ok = 0 +okIsZero = Refl + +export +dimensionMismatchIsSeven : resultToInt DimensionMismatch = 7 +dimensionMismatchIsSeven = Refl + +-------------------------------------------------------------------------------- +-- SIMD widths and pixel byte widths are positive (sanity for codegen). +-------------------------------------------------------------------------------- + +||| AVX-512 carries a 16-wide float lane, as the schedule generator expects. +export +avx512Width : simdWidth X86_AVX512 = 16 +avx512Width = Refl + +||| Float64 pixels are 8 bytes, as the buffer byte calculation depends on. +export +float64Bytes : pixelBytes Float64 = 8 +float64Bytes = Refl diff --git a/src/interface/abi/Types.idr b/src/interface/abi/Halideiser/ABI/Types.idr similarity index 76% rename from src/interface/abi/Types.idr rename to src/interface/abi/Halideiser/ABI/Types.idr index e540101..6da4a84 100644 --- a/src/interface/abi/Types.idr +++ b/src/interface/abi/Halideiser/ABI/Types.idr @@ -22,6 +22,7 @@ import Data.Bits import Data.So import Data.Vect import Data.Nat +import Decidable.Equality %default total @@ -33,13 +34,12 @@ import Data.Nat public export data Platform = Linux | Windows | MacOS | BSD | WASM -||| Compile-time platform detection -||| 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 - pure Linux -- Default, override with compiler flags +thisPlatform = Linux -------------------------------------------------------------------------------- -- Hardware Targets @@ -329,6 +329,76 @@ resultToInt CompileFailed = 5 resultToInt InvalidSchedule = 6 resultToInt DimensionMismatch = 7 +||| Results are decidably equal. The off-diagonal cases discharge the +||| disequality explicitly; a `decEq _ _ = No absurd` catch-all does not +||| compile (no `Uninhabited (x = y)` instance exists for these). +public export +DecEq Result where + decEq Ok Ok = Yes Refl + decEq Error Error = Yes Refl + decEq InvalidParam InvalidParam = Yes Refl + decEq OutOfMemory OutOfMemory = Yes Refl + decEq NullPointer NullPointer = Yes Refl + decEq CompileFailed CompileFailed = Yes Refl + decEq InvalidSchedule InvalidSchedule = Yes Refl + decEq DimensionMismatch DimensionMismatch = Yes Refl + 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 CompileFailed = No (\case Refl impossible) + decEq Ok InvalidSchedule = No (\case Refl impossible) + decEq Ok DimensionMismatch = 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 CompileFailed = No (\case Refl impossible) + decEq Error InvalidSchedule = No (\case Refl impossible) + decEq Error DimensionMismatch = 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 CompileFailed = No (\case Refl impossible) + decEq InvalidParam InvalidSchedule = No (\case Refl impossible) + decEq InvalidParam DimensionMismatch = 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 CompileFailed = No (\case Refl impossible) + decEq OutOfMemory InvalidSchedule = No (\case Refl impossible) + decEq OutOfMemory DimensionMismatch = 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 CompileFailed = No (\case Refl impossible) + decEq NullPointer InvalidSchedule = No (\case Refl impossible) + decEq NullPointer DimensionMismatch = No (\case Refl impossible) + decEq CompileFailed Ok = No (\case Refl impossible) + decEq CompileFailed Error = No (\case Refl impossible) + decEq CompileFailed InvalidParam = No (\case Refl impossible) + decEq CompileFailed OutOfMemory = No (\case Refl impossible) + decEq CompileFailed NullPointer = No (\case Refl impossible) + decEq CompileFailed InvalidSchedule = No (\case Refl impossible) + decEq CompileFailed DimensionMismatch = No (\case Refl impossible) + decEq InvalidSchedule Ok = No (\case Refl impossible) + decEq InvalidSchedule Error = No (\case Refl impossible) + decEq InvalidSchedule InvalidParam = No (\case Refl impossible) + decEq InvalidSchedule OutOfMemory = No (\case Refl impossible) + decEq InvalidSchedule NullPointer = No (\case Refl impossible) + decEq InvalidSchedule CompileFailed = No (\case Refl impossible) + decEq InvalidSchedule DimensionMismatch = No (\case Refl impossible) + decEq DimensionMismatch Ok = No (\case Refl impossible) + decEq DimensionMismatch Error = No (\case Refl impossible) + decEq DimensionMismatch InvalidParam = No (\case Refl impossible) + decEq DimensionMismatch OutOfMemory = No (\case Refl impossible) + decEq DimensionMismatch NullPointer = No (\case Refl impossible) + decEq DimensionMismatch CompileFailed = No (\case Refl impossible) + decEq DimensionMismatch InvalidSchedule = No (\case Refl impossible) + -------------------------------------------------------------------------------- -- Opaque Handles -------------------------------------------------------------------------------- @@ -339,12 +409,15 @@ public export data Handle : Type where MkHandle : (ptr : Bits64) -> {auto 0 nonNull : So (ptr /= 0)} -> Handle -||| Safely create a handle from a pointer value. -||| Returns Nothing if pointer is null. +||| Safely create a handle from a pointer value. Uses `choose` to obtain a +||| real `So (ptr /= 0)` witness for the non-null branch. (Previously +||| `Just (MkHandle ptr)` left the `auto` proof unsolved and did not compile.) public export createHandle : Bits64 -> Maybe Handle -createHandle 0 = Nothing -createHandle ptr = Just (MkHandle ptr) +createHandle ptr = + case choose (ptr /= 0) of + Left ok => Just (MkHandle ptr {nonNull = ok}) + Right _ => Nothing ||| Extract pointer value from handle public export diff --git a/src/interface/abi/halideiser-abi.ipkg b/src/interface/abi/halideiser-abi.ipkg new file mode 100644 index 0000000..81b63d9 --- /dev/null +++ b/src/interface/abi/halideiser-abi.ipkg @@ -0,0 +1,11 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Idris2 package for the halideiser ABI formal proofs. +-- Build/check with: idris2 --build halideiser-abi.ipkg (from src/interface/abi/) +package halideiser-abi + +sourcedir = "." + +modules = Halideiser.ABI.Types + , Halideiser.ABI.Layout + , Halideiser.ABI.Foreign + , Halideiser.ABI.Proofs