P3: prove partition correctness generally (all n, k), not hand-picked vectors

.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

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) <j.d.a.jewell@open.ac.uk>
+#
+# 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:<name>"` symbol declared anywhere in the ABI .idr
+#      sources is exported by the Zig FFI (`export fn <name>`);
+#   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"(?<!^)(?=[A-Z])", "_", s).lower()
+
+
+def canon_rc(name):
+    n = name.lower()
+    return "error" if n in ("err", "error") else n
+
+
+def find_result_enum(zig):
+    """Return {variant: value} for the C-ABI Result enum, or {}."""
+    best = {}
+    for m in re.finditer(r"enum\s*\(\s*c_int\s*\)\s*\{(.*?)\}", zig, re.S):
+        body = m.group(1)
+        variants = {}
+        for vm in re.finditer(r'@?"?([A-Za-z_][A-Za-z0-9_]*)"?\s*=\s*(\d+)', body):
+            variants[canon_rc(vm.group(1))] = int(vm.group(2))
+        # The Result enum is the one starting at ok = 0.
+        if variants.get("ok") == 0 and len(variants) > 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())

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) <j.d.a.jewell@open.ac.uk>
+--
+||| 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

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