diff --git a/.github/workflows/abi-ffi-gate.yml b/.github/workflows/abi-ffi-gate.yml new file mode 100644 index 0000000..269464d --- /dev/null +++ b/.github/workflows/abi-ffi-gate.yml @@ -0,0 +1,38 @@ +# SPDX-License-Identifier: MPL-2.0 +# abi-ffi-gate.yml — enforce that the Zig FFI conforms to the Idris2 ABI. +# +# The Idris2 ABI (src/interface/abi) is the source of truth. This gate fails if +# the Zig FFI (src/interface/ffi) drifts from it: a declared C function with no +# export, a mismatched result-code map, or an unrendered template token. A +# second job builds + tests the Zig FFI under the pinned Zig 0.14.0. +name: ABI-FFI Gate + +on: + pull_request: + push: + branches: [main, master] + +permissions: + contents: read + +jobs: + conformance: + name: ABI ↔ FFI structural conformance + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - name: Run ABI-FFI gate + run: python3 scripts/abi-ffi-gate.py + + zig-build: + name: Zig FFI builds + tests (Zig 0.14.0) + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v4 + - name: Install Zig 0.14.0 + run: | + curl -fsSL https://ziglang.org/download/0.14.0/zig-linux-x86_64-0.14.0.tar.xz -o /tmp/zig.tar.xz + tar -xf /tmp/zig.tar.xz -C /tmp + echo "/tmp/zig-linux-x86_64-0.14.0" >> "$GITHUB_PATH" + - name: zig test FFI + run: zig test src/interface/ffi/src/main.zig -lc diff --git a/scripts/abi-ffi-gate.py b/scripts/abi-ffi-gate.py new file mode 100755 index 0000000..9ee96db --- /dev/null +++ b/scripts/abi-ffi-gate.py @@ -0,0 +1,103 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# abi-ffi-gate.py — fail (exit 1) if the Zig FFI does not conform to the Idris2 +# ABI. The Idris2 ABI is the source of truth. Checks, with no toolchain needed: +# +# 1. the Zig FFI carries no unrendered `{{...}}` template tokens; +# 2. every `%foreign "C:"` symbol declared anywhere in the ABI .idr +# sources is exported by the Zig FFI (`export fn `); +# 3. the Zig `Result = enum(c_int)` and the Idris `resultToInt` agree on BOTH +# names and integer values (the `Error`/`err` spelling is treated as one). +# +# Usage: python3 scripts/abi-ffi-gate.py [repo_root] (defaults to cwd) + +import os +import re +import sys +import glob + + +def camel_to_snake(s): + return re.sub(r"(? len(best): + best = variants + return best + + +def main(): + root = sys.argv[1] if len(sys.argv) > 1 else "." + name = os.path.basename(os.path.abspath(root)) + abi_dir = os.path.join(root, "src/interface/abi") + zig_path = os.path.join(root, "src/interface/ffi/src/main.zig") + errs = [] + + idr_files = [ + p for p in glob.glob(os.path.join(abi_dir, "**", "*.idr"), recursive=True) + if os.sep + "build" + os.sep not in p + ] + if not idr_files: + print(f"ABI-FFI GATE: SKIP ({name}) — no Idris2 ABI .idr files under {abi_dir}") + return 0 + if not os.path.exists(zig_path): + print(f"ABI-FFI GATE: FAIL ({name}) — no Zig FFI at {zig_path}") + return 1 + + idr = "\n".join(open(p, encoding="utf-8").read() for p in idr_files) + zig = open(zig_path, encoding="utf-8").read() + + # 1. unrendered template tokens + toks = sorted(set(re.findall(r"\{\{[A-Za-z0-9_]+\}\}", zig))) + if toks: + errs.append(f"Zig FFI has unrendered template tokens: {toks}") + + # 2. foreign C symbols must be exported + csyms = sorted(set(re.findall(r"C:([A-Za-z0-9_]+)", idr))) + exports = set(re.findall(r"export fn ([A-Za-z0-9_]+)", zig)) + missing = [s for s in csyms if s not in exports] + if missing: + errs.append(f"{len(missing)} ABI function(s) not exported by the Zig FFI: {missing}") + + # 3. result-code map (names + values) must agree + idr_rc = {} + for m in re.finditer(r"resultToInt\s+([A-Za-z0-9]+)\s*=\s*(\d+)", idr): + idr_rc[canon_rc(camel_to_snake(m.group(1)))] = int(m.group(2)) + zig_rc = find_result_enum(zig) + if idr_rc and not zig_rc: + errs.append("no Zig `enum(c_int)` Result block (with `ok = 0`) found to compare result codes") + elif idr_rc and zig_rc and idr_rc != zig_rc: + errs.append( + "Result-code map differs (name or value):\n" + f" Idris resultToInt: {dict(sorted(idr_rc.items()))}\n" + f" Zig Result enum: {dict(sorted(zig_rc.items()))}" + ) + + if errs: + print(f"ABI-FFI GATE: FAIL ({name})") + for e in errs: + print(" - " + e) + return 1 + print(f"ABI-FFI GATE: OK ({name}) — {len(csyms)} ABI functions exported, " + f"{len(idr_rc)} result codes match") + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/src/interface/abi/Chapeliser/ABI/Partition.idr b/src/interface/abi/Chapeliser/ABI/Partition.idr new file mode 100644 index 0000000..917f399 --- /dev/null +++ b/src/interface/abi/Chapeliser/ABI/Partition.idr @@ -0,0 +1,178 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| General partition-correctness proofs for Chapeliser. +||| +||| `Proofs.idr` verifies completeness/disjointness on a handful of *explicit* +||| slice vectors. This module proves the same invariants **for the whole +||| contiguous-partition family at once** — quantified over an arbitrary vector +||| of per-locale counts — and applies that result to the actual block-partition +||| strategy (the `div`/`mod` counts of `perItemSlices`) for **all** `n` items +||| and `k` locales. +||| +||| The key idea: contiguity is *structural*. A contiguous layout places each +||| slice exactly where the previous one ended, independently of the count +||| values, so the non-overlap guarantee needs no reasoning about `div`/`mod` +||| (which do not reduce at the type level). We capture non-overlap as a +||| `Tiling` — a gapless, overlap-free cover, strictly stronger than the pairwise +||| `disjoint` Bool check — and prove the real block partition is one for all +||| `n`, `k`. The only residual is the completeness identity +||| `sumNat (perItemCounts n k) = n`, which is isolated below. + +module Chapeliser.ABI.Partition + +import Chapeliser.ABI.Types +import Data.Vect +import Data.Vect.Quantifiers +import Data.Nat + +%default total + +-------------------------------------------------------------------------------- +-- The contiguous layout builder (a reducible, top-level form of perItemSlices) +-------------------------------------------------------------------------------- + +||| Lay out `k` slices contiguously from `start`, one per count: slice i begins +||| where slice i-1 ended. This is exactly the shape of `perItemSlices`' inner +||| `go`, lifted to top level so proofs can reduce through it. +public export +contiguousFrom : (start : Nat) -> Vect k Nat -> Vect k Slice +contiguousFrom _ [] = [] +contiguousFrom start (c :: cs) = MkSlice start c :: contiguousFrom (start + c) cs + +||| Sum of a vector of counts. +public export +sumNat : Vect k Nat -> Nat +sumNat [] = 0 +sumNat (c :: cs) = c + sumNat cs + +-------------------------------------------------------------------------------- +-- Completeness, generalised over ALL count vectors +-------------------------------------------------------------------------------- + +||| For ANY start offset and ANY vector of counts, the contiguous layout's slice +||| counts sum to exactly the total of the counts — no items dropped or +||| duplicated. (`Proofs.idr` only checked this for fixed vectors.) +export +contiguousComplete : (start : Nat) -> (counts : Vect k Nat) -> + sliceSum (contiguousFrom start counts) = sumNat counts +contiguousComplete _ [] = Refl +contiguousComplete start (c :: cs) = + rewrite contiguousComplete (start + c) cs in Refl + +-------------------------------------------------------------------------------- +-- Tiny LTE lemmas (propositional; these reduce, unlike the compare-based `<=`) +-------------------------------------------------------------------------------- + +lteReflexive : (n : Nat) -> LTE n n +lteReflexive Z = LTEZero +lteReflexive (S k) = LTESucc (lteReflexive k) + +lteAddR : (n, m : Nat) -> LTE n (n + m) +lteAddR Z m = LTEZero +lteAddR (S k) m = LTESucc (lteAddR k m) + +lteTrans' : LTE a b -> LTE b c -> LTE a c +lteTrans' LTEZero _ = LTEZero +lteTrans' (LTESucc p) (LTESucc q) = LTESucc (lteTrans' p q) + +-------------------------------------------------------------------------------- +-- Non-overlap as a structural tiling (gapless AND overlap-free by construction) +-------------------------------------------------------------------------------- + +||| `Tiling lo ss` witnesses that `ss` tiles `[lo, …)` with no gaps and no +||| overlaps: the first slice begins at `lo`, and the rest tile from exactly +||| where it ends. Strictly stronger than pairwise disjointness. +public export +data Tiling : Nat -> Vect k Slice -> Type where + TNil : Tiling lo [] + TCons : (c : Nat) -> Tiling (lo + c) rest -> + Tiling lo (MkSlice lo c :: rest) + +||| The contiguous layout is a perfect tiling for ANY start and ANY counts. +export +contiguousTiles : (lo : Nat) -> (counts : Vect k Nat) -> + Tiling lo (contiguousFrom lo counts) +contiguousTiles _ [] = TNil +contiguousTiles lo (c :: cs) = TCons c (contiguousTiles (lo + c) cs) + +-------------------------------------------------------------------------------- +-- Tiling ⇒ propositional pairwise non-overlap (no Bool `<=`/`all`) +-------------------------------------------------------------------------------- + +||| Every slice of a tiling based at `lo` starts at `lo` or later. +export +tilingStartsGE : {ss : Vect k Slice} -> Tiling lo ss -> + All (\s => LTE lo s.start) ss +tilingStartsGE TNil = [] +tilingStartsGE (TCons {lo} c t) = + lteReflexive lo + :: mapProperty (\le => lteTrans' (lteAddR lo c) le) (tilingStartsGE t) + +||| Propositional non-overlap of two slices: `a` ends at or before `b` starts. +public export +NoOverlap : Slice -> Slice -> Type +NoOverlap a b = LTE (a.start + a.count) b.start + +||| In a tiling, the head slice does not overlap any later slice — its end is +||| `lo + c`, and every later slice starts there or later. Genuine pairwise +||| disjointness, proven generically (not per concrete vector). +export +tilingHeadNoOverlap : {lo : Nat} -> (c : Nat) -> {rest : Vect k Slice} -> + Tiling (lo + c) rest -> + All (\s => NoOverlap (MkSlice lo c) s) rest +tilingHeadNoOverlap c t = tilingStartsGE t + +-------------------------------------------------------------------------------- +-- The actual block-partition strategy is correct for ALL n and k +-------------------------------------------------------------------------------- + +||| Per-locale counts for the even (block) partition: every locale gets `base` +||| items and the first `rem` locales get one extra. `idx` is the running locale +||| index. (This is the `div`/`mod` content of `perItemSlices`, isolated; the +||| proofs below do not depend on its values.) +public export +countsFrom : (idx, base, rem : Nat) -> (k : Nat) -> Vect k Nat +countsFrom _ _ _ Z = [] +countsFrom idx base rem (S j) = + (base + (if idx < rem then 1 else 0)) :: countsFrom (S idx) base rem j + +||| The block partition's per-locale counts for `n` items over `k` locales. +public export +perItemCounts : (n : Nat) -> (k : Nat) -> Vect k Nat +perItemCounts n k = countsFrom 0 (n `div` k) (n `mod` k) k + +||| The block partition laid out contiguously. +public export +blockSlices : (n : Nat) -> (k : Nat) -> Vect k Slice +blockSlices n k = contiguousFrom 0 (perItemCounts n k) + +||| MAIN RESULT: for every item count `n` and every locale count `k`, the block +||| partition is a gapless, non-overlapping tiling — no item is assigned to two +||| locales and the assigned ranges abut perfectly. Holds for ALL n, k with no +||| appeal to how `div`/`mod` evaluate. +export +blockPartitionTiles : (n : Nat) -> (k : Nat) -> Tiling 0 (blockSlices n k) +blockPartitionTiles n k = contiguousTiles 0 (perItemCounts n k) + +||| Corollary: completeness of the block partition reduces to the residual +||| arithmetic identity `sumNat (perItemCounts n k) = n` — the only `div`/`mod` +||| obligation, which the type checker cannot discharge by reduction (tracked as +||| future proof work). The structural half (slice counts sum to the count +||| total) is proven here for all n, k. +export +blockPartitionComplete : (n : Nat) -> (k : Nat) -> + sliceSum (blockSlices n k) = sumNat (perItemCounts n k) +blockPartitionComplete n k = contiguousComplete 0 (perItemCounts n k) + +-------------------------------------------------------------------------------- +-- Negative control: a wrong-sum partition is genuinely NOT complete +-------------------------------------------------------------------------------- + +||| A 3-locale layout whose counts sum to 9 cannot be a complete partition of 10 +||| items: `PartitionComplete` for `Partition 10 3` demands `sliceSum = 10`, but +||| this layout sums to 9. Witnessing the negation keeps completeness honest. +export +shortPartitionNotComplete : + Not (PartitionComplete (MkPartition {n = 10} {k = 3} (contiguousFrom 0 [3, 3, 3]))) +shortPartitionNotComplete (IsComplete Refl) impossible diff --git a/src/interface/abi/chapeliser-abi.ipkg b/src/interface/abi/chapeliser-abi.ipkg index 4dbfe94..ebad5e0 100644 --- a/src/interface/abi/chapeliser-abi.ipkg +++ b/src/interface/abi/chapeliser-abi.ipkg @@ -9,3 +9,4 @@ modules = Chapeliser.ABI.Types , Chapeliser.ABI.Layout , Chapeliser.ABI.Foreign , Chapeliser.ABI.Proofs + , Chapeliser.ABI.Partition