From d0d9bde3f91573d5239f325060f6f1555fa85977 Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 26 Jun 2026 22:03:35 +0000 Subject: [PATCH 1/3] P1: align Zig FFI symbol names to the Idris2 ABI The Idris2 ABI in src/interface/abi/Chapeliser/ABI/Foreign.idr is the source of truth for the C-ABI contract. It declares 12 foreign symbols via `%foreign "C:c_*, libchapeliser_ffi"`: c_init, c_shutdown, c_get_total_items, c_load_item, c_store_result, c_process_item, c_process_chunk, c_reduce, c_is_match, c_key_hash, c_checkpoint_save, c_checkpoint_load The Zig FFI reference implementation exported these as `chapeliser_ref_` instead. The functions correspond 1:1 by stem and the Result codes already match, but the symbol names diverged, so the ABI and FFI would not link (every `c_*` import would be undefined). Fix (Zig-only, ABI unchanged because it is the source of truth): - Rename the 12 ABI-declared exports from `chapeliser_ref_` to exactly `c_` in src/interface/ffi/src/main.zig. - The two extra utility functions (`version`, `build_info`) are NOT part of the ABI, so they are namespaced as `chapeliser_version` and `chapeliser_build_info` rather than given `c_` names. - Update all internal call sites in main.zig tests and the `extern fn` declarations in test/integration_test.zig accordingly. No behaviour or result-code values changed. Verification: - `zig build test` (main.zig unit tests): pass - `zig build test-integration` (links the lib, resolves externs): pass - `idris2 --build chapeliser-abi.ipkg`: exit 0 - Every `C:c_` in Foreign.idr now has a matching `export fn c_` in main.zig. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_019xMKB3T4Vo5FYC7Czx3JSH --- src/interface/ffi/src/main.zig | 52 +++++++------- src/interface/ffi/test/integration_test.zig | 76 ++++++++++----------- 2 files changed, 64 insertions(+), 64 deletions(-) diff --git a/src/interface/ffi/src/main.zig b/src/interface/ffi/src/main.zig index b1fcc7b..8b81bb6 100644 --- a/src/interface/ffi/src/main.zig +++ b/src/interface/ffi/src/main.zig @@ -72,14 +72,14 @@ var state: ?ReferenceState = null; //============================================================================== /// Initialise the reference workload. Returns 0 on success. -export fn chapeliser_ref_init() callconv(.C) c_int { +export fn c_init() callconv(.C) c_int { if (state != null) return @intFromEnum(Result.err); // already initialised state = ReferenceState.init(std.heap.c_allocator); return @intFromEnum(Result.ok); } /// Shut down the reference workload. Returns 0 on success. -export fn chapeliser_ref_shutdown() callconv(.C) c_int { +export fn c_shutdown() callconv(.C) c_int { if (state) |*s| { s.deinit(); state = null; @@ -93,7 +93,7 @@ export fn chapeliser_ref_shutdown() callconv(.C) c_int { //============================================================================== /// Return the total number of input items. -export fn chapeliser_ref_get_total_items() callconv(.C) c_int { +export fn c_get_total_items() callconv(.C) c_int { if (state) |s| { return @intCast(s.items.items.len); } @@ -101,7 +101,7 @@ export fn chapeliser_ref_get_total_items() callconv(.C) c_int { } /// Serialise input item `idx` into `buf`. Set `*len` to bytes written. -export fn chapeliser_ref_load_item(idx: c_int, buf: [*]u8, len: *usize) callconv(.C) c_int { +export fn c_load_item(idx: c_int, buf: [*]u8, len: *usize) callconv(.C) c_int { const s = &(state orelse return @intFromEnum(Result.err)); const i: usize = @intCast(idx); if (i >= s.items.items.len) return @intFromEnum(Result.invalid_param); @@ -115,7 +115,7 @@ export fn chapeliser_ref_load_item(idx: c_int, buf: [*]u8, len: *usize) callconv } /// Receive a processed result at index `idx`. -export fn chapeliser_ref_store_result(idx: c_int, buf: [*]const u8, len: usize) callconv(.C) c_int { +export fn c_store_result(idx: c_int, buf: [*]const u8, len: usize) callconv(.C) c_int { const s = &(state orelse return @intFromEnum(Result.err)); // Copy the result data @@ -139,7 +139,7 @@ export fn chapeliser_ref_store_result(idx: c_int, buf: [*]const u8, len: usize) //============================================================================== /// Process a single item: for the reference implementation, just echo it back. -export fn chapeliser_ref_process_item( +export fn c_process_item( in_buf: [*]const u8, in_len: usize, out_buf: [*]u8, @@ -152,7 +152,7 @@ export fn chapeliser_ref_process_item( } /// Process a chunk of items: for reference, process each individually. -export fn chapeliser_ref_process_chunk( +export fn c_process_chunk( items_buf: [*]const u8, item_count: c_int, item_offsets: [*]const c_int, @@ -178,7 +178,7 @@ export fn chapeliser_ref_process_chunk( //============================================================================== /// Combine two results: for reference, concatenate them. -export fn chapeliser_ref_reduce( +export fn c_reduce( a_buf: [*]const u8, a_len: usize, b_buf: [*]const u8, @@ -197,7 +197,7 @@ export fn chapeliser_ref_reduce( //============================================================================== /// Check if a result matches: for reference, match if first byte is non-zero. -export fn chapeliser_ref_is_match(buf: [*]const u8, len: usize) callconv(.C) c_int { +export fn c_is_match(buf: [*]const u8, len: usize) callconv(.C) c_int { if (len == 0) return 0; return if (buf[0] != 0) 1 else 0; } @@ -207,7 +207,7 @@ export fn chapeliser_ref_is_match(buf: [*]const u8, len: usize) callconv(.C) c_i //============================================================================== /// Hash an item's key: for reference, use FNV-1a on the first 8 bytes. -export fn chapeliser_ref_key_hash(buf: [*]const u8, len: usize) callconv(.C) c_uint { +export fn c_key_hash(buf: [*]const u8, len: usize) callconv(.C) c_uint { const hash_len = @min(len, 8); var h: u32 = 2166136261; // FNV offset basis for (buf[0..hash_len]) |b| { @@ -222,7 +222,7 @@ export fn chapeliser_ref_key_hash(buf: [*]const u8, len: usize) callconv(.C) c_u //============================================================================== /// Save checkpoint: reference implementation is a no-op. -export fn chapeliser_ref_checkpoint_save( +export fn c_checkpoint_save( _: [*]const u8, _: usize, _: [*:0]const u8, @@ -231,7 +231,7 @@ export fn chapeliser_ref_checkpoint_save( } /// Load checkpoint: reference implementation is a no-op. -export fn chapeliser_ref_checkpoint_load( +export fn c_checkpoint_load( _: [*]u8, _: *usize, _: [*:0]const u8, @@ -243,11 +243,11 @@ export fn chapeliser_ref_checkpoint_load( // Version //============================================================================== -export fn chapeliser_ref_version() callconv(.C) [*:0]const u8 { +export fn chapeliser_version() callconv(.C) [*:0]const u8 { return VERSION.ptr; } -export fn chapeliser_ref_build_info() callconv(.C) [*:0]const u8 { +export fn chapeliser_build_info() callconv(.C) [*:0]const u8 { return BUILD_INFO.ptr; } @@ -256,12 +256,12 @@ export fn chapeliser_ref_build_info() callconv(.C) [*:0]const u8 { //============================================================================== test "lifecycle" { - const rc_init = chapeliser_ref_init(); + const rc_init = c_init(); try std.testing.expectEqual(@as(c_int, 0), rc_init); - defer _ = chapeliser_ref_shutdown(); + defer _ = c_shutdown(); // Double init should fail - const rc_double = chapeliser_ref_init(); + const rc_double = c_init(); try std.testing.expectEqual(@as(c_int, 1), rc_double); } @@ -270,7 +270,7 @@ test "process_item echo" { var output: [256]u8 = undefined; var out_len: usize = 0; - const rc = chapeliser_ref_process_item(input.ptr, input.len, &output, &out_len); + const rc = c_process_item(input.ptr, input.len, &output, &out_len); try std.testing.expectEqual(@as(c_int, 0), rc); try std.testing.expectEqual(input.len, out_len); try std.testing.expectEqualStrings(input, output[0..out_len]); @@ -282,33 +282,33 @@ test "reduce concatenates" { var output: [256]u8 = undefined; var out_len: usize = 0; - const rc = chapeliser_ref_reduce(a.ptr, a.len, b.ptr, b.len, &output, &out_len); + const rc = c_reduce(a.ptr, a.len, b.ptr, b.len, &output, &out_len); try std.testing.expectEqual(@as(c_int, 0), rc); try std.testing.expectEqualStrings("foobar", output[0..out_len]); } test "key_hash deterministic" { const data = "testkey1"; - const h1 = chapeliser_ref_key_hash(data.ptr, data.len); - const h2 = chapeliser_ref_key_hash(data.ptr, data.len); + const h1 = c_key_hash(data.ptr, data.len); + const h2 = c_key_hash(data.ptr, data.len); try std.testing.expectEqual(h1, h2); } test "is_match" { const yes = [_]u8{ 0x42, 0x00 }; const no = [_]u8{ 0x00, 0x42 }; - try std.testing.expectEqual(@as(c_int, 1), chapeliser_ref_is_match(&yes, yes.len)); - try std.testing.expectEqual(@as(c_int, 0), chapeliser_ref_is_match(&no, no.len)); + try std.testing.expectEqual(@as(c_int, 1), c_is_match(&yes, yes.len)); + try std.testing.expectEqual(@as(c_int, 0), c_is_match(&no, no.len)); } test "checkpoint not implemented" { var buf: [64]u8 = undefined; var len: usize = buf.len; - try std.testing.expectEqual(@as(c_int, -1), chapeliser_ref_checkpoint_save(&buf, len, "test")); - try std.testing.expectEqual(@as(c_int, -1), chapeliser_ref_checkpoint_load(&buf, &len, "test")); + try std.testing.expectEqual(@as(c_int, -1), c_checkpoint_save(&buf, len, "test")); + try std.testing.expectEqual(@as(c_int, -1), c_checkpoint_load(&buf, &len, "test")); } test "version" { - const ver = std.mem.span(chapeliser_ref_version()); + const ver = std.mem.span(chapeliser_version()); try std.testing.expectEqualStrings("0.1.0", ver); } diff --git a/src/interface/ffi/test/integration_test.zig b/src/interface/ffi/test/integration_test.zig index 53e078b..5d5c30f 100644 --- a/src/interface/ffi/test/integration_test.zig +++ b/src/interface/ffi/test/integration_test.zig @@ -8,44 +8,44 @@ const std = @import("std"); const testing = std.testing; // Import reference FFI functions -extern fn chapeliser_ref_init() c_int; -extern fn chapeliser_ref_shutdown() c_int; -extern fn chapeliser_ref_get_total_items() c_int; -extern fn chapeliser_ref_load_item(c_int, [*]u8, *usize) c_int; -extern fn chapeliser_ref_store_result(c_int, [*]const u8, usize) c_int; -extern fn chapeliser_ref_process_item([*]const u8, usize, [*]u8, *usize) c_int; -extern fn chapeliser_ref_process_chunk([*]const u8, c_int, [*]const c_int, [*]const c_int, [*]u8, *usize) c_int; -extern fn chapeliser_ref_reduce([*]const u8, usize, [*]const u8, usize, [*]u8, *usize) c_int; -extern fn chapeliser_ref_is_match([*]const u8, usize) c_int; -extern fn chapeliser_ref_key_hash([*]const u8, usize) c_uint; -extern fn chapeliser_ref_checkpoint_save([*]const u8, usize, [*:0]const u8) c_int; -extern fn chapeliser_ref_checkpoint_load([*]u8, *usize, [*:0]const u8) c_int; -extern fn chapeliser_ref_version() [*:0]const u8; -extern fn chapeliser_ref_build_info() [*:0]const u8; +extern fn c_init() c_int; +extern fn c_shutdown() c_int; +extern fn c_get_total_items() c_int; +extern fn c_load_item(c_int, [*]u8, *usize) c_int; +extern fn c_store_result(c_int, [*]const u8, usize) c_int; +extern fn c_process_item([*]const u8, usize, [*]u8, *usize) c_int; +extern fn c_process_chunk([*]const u8, c_int, [*]const c_int, [*]const c_int, [*]u8, *usize) c_int; +extern fn c_reduce([*]const u8, usize, [*]const u8, usize, [*]u8, *usize) c_int; +extern fn c_is_match([*]const u8, usize) c_int; +extern fn c_key_hash([*]const u8, usize) c_uint; +extern fn c_checkpoint_save([*]const u8, usize, [*:0]const u8) c_int; +extern fn c_checkpoint_load([*]u8, *usize, [*:0]const u8) c_int; +extern fn chapeliser_version() [*:0]const u8; +extern fn chapeliser_build_info() [*:0]const u8; //============================================================================== // Lifecycle Tests //============================================================================== test "init and shutdown" { - const rc_init = chapeliser_ref_init(); + const rc_init = c_init(); try testing.expectEqual(@as(c_int, 0), rc_init); - const rc_shutdown = chapeliser_ref_shutdown(); + const rc_shutdown = c_shutdown(); try testing.expectEqual(@as(c_int, 0), rc_shutdown); } test "double init fails" { - const rc1 = chapeliser_ref_init(); + const rc1 = c_init(); try testing.expectEqual(@as(c_int, 0), rc1); - defer _ = chapeliser_ref_shutdown(); + defer _ = c_shutdown(); - const rc2 = chapeliser_ref_init(); + const rc2 = c_init(); try testing.expectEqual(@as(c_int, 1), rc2); // error: already initialised } test "shutdown without init fails" { - const rc = chapeliser_ref_shutdown(); + const rc = c_shutdown(); try testing.expectEqual(@as(c_int, 1), rc); // error: not initialised } @@ -58,7 +58,7 @@ test "process_item preserves data" { var output: [256]u8 = undefined; var out_len: usize = 0; - const rc = chapeliser_ref_process_item(input.ptr, input.len, &output, &out_len); + const rc = c_process_item(input.ptr, input.len, &output, &out_len); try testing.expectEqual(@as(c_int, 0), rc); try testing.expectEqual(input.len, out_len); try testing.expectEqualStrings(input, output[0..out_len]); @@ -69,7 +69,7 @@ test "process_item handles empty input" { var output: [256]u8 = undefined; var out_len: usize = 0; - const rc = chapeliser_ref_process_item(input.ptr, input.len, &output, &out_len); + const rc = c_process_item(input.ptr, input.len, &output, &out_len); try testing.expectEqual(@as(c_int, 0), rc); try testing.expectEqual(@as(usize, 0), out_len); } @@ -84,7 +84,7 @@ test "reduce combines two results" { var output: [256]u8 = undefined; var out_len: usize = 0; - const rc = chapeliser_ref_reduce(a.ptr, a.len, b.ptr, b.len, &output, &out_len); + const rc = c_reduce(a.ptr, a.len, b.ptr, b.len, &output, &out_len); try testing.expectEqual(@as(c_int, 0), rc); try testing.expectEqualStrings("hello world", output[0..out_len]); } @@ -104,12 +104,12 @@ test "reduce is associative for concatenation" { var final2: usize = 0; // (a + b) + c - _ = chapeliser_ref_reduce(a.ptr, a.len, b.ptr, b.len, &tmp1, &len1); - _ = chapeliser_ref_reduce(&tmp1, len1, c.ptr, c.len, &result1, &final1); + _ = c_reduce(a.ptr, a.len, b.ptr, b.len, &tmp1, &len1); + _ = c_reduce(&tmp1, len1, c.ptr, c.len, &result1, &final1); // a + (b + c) - _ = chapeliser_ref_reduce(b.ptr, b.len, c.ptr, c.len, &tmp2, &len2); - _ = chapeliser_ref_reduce(a.ptr, a.len, &tmp2, len2, &result2, &final2); + _ = c_reduce(b.ptr, b.len, c.ptr, c.len, &tmp2, &len2); + _ = c_reduce(a.ptr, a.len, &tmp2, len2, &result2, &final2); try testing.expectEqualStrings(result1[0..final1], result2[0..final2]); } @@ -120,17 +120,17 @@ test "reduce is associative for concatenation" { test "is_match returns 1 for non-zero first byte" { const data = [_]u8{ 0xFF, 0x00, 0x00 }; - try testing.expectEqual(@as(c_int, 1), chapeliser_ref_is_match(&data, data.len)); + try testing.expectEqual(@as(c_int, 1), c_is_match(&data, data.len)); } test "is_match returns 0 for zero first byte" { const data = [_]u8{ 0x00, 0xFF, 0xFF }; - try testing.expectEqual(@as(c_int, 0), chapeliser_ref_is_match(&data, data.len)); + try testing.expectEqual(@as(c_int, 0), c_is_match(&data, data.len)); } test "is_match returns 0 for empty buffer" { const data = [_]u8{}; - try testing.expectEqual(@as(c_int, 0), chapeliser_ref_is_match(&data, 0)); + try testing.expectEqual(@as(c_int, 0), c_is_match(&data, 0)); } //============================================================================== @@ -139,16 +139,16 @@ test "is_match returns 0 for empty buffer" { test "key_hash is deterministic" { const key = "partition-key"; - const h1 = chapeliser_ref_key_hash(key.ptr, key.len); - const h2 = chapeliser_ref_key_hash(key.ptr, key.len); + const h1 = c_key_hash(key.ptr, key.len); + const h2 = c_key_hash(key.ptr, key.len); try testing.expectEqual(h1, h2); } test "key_hash differs for different keys" { const k1 = "key-alpha"; const k2 = "key-bravo"; - const h1 = chapeliser_ref_key_hash(k1.ptr, k1.len); - const h2 = chapeliser_ref_key_hash(k2.ptr, k2.len); + const h1 = c_key_hash(k1.ptr, k1.len); + const h2 = c_key_hash(k2.ptr, k2.len); try testing.expect(h1 != h2); } @@ -158,14 +158,14 @@ test "key_hash differs for different keys" { test "checkpoint save returns not-implemented" { const data = "checkpoint data"; - const rc = chapeliser_ref_checkpoint_save(data.ptr, data.len, "locale-0"); + const rc = c_checkpoint_save(data.ptr, data.len, "locale-0"); try testing.expectEqual(@as(c_int, -1), rc); } test "checkpoint load returns not-implemented" { var buf: [256]u8 = undefined; var len: usize = buf.len; - const rc = chapeliser_ref_checkpoint_load(&buf, &len, "locale-0"); + const rc = c_checkpoint_load(&buf, &len, "locale-0"); try testing.expectEqual(@as(c_int, -1), rc); } @@ -174,13 +174,13 @@ test "checkpoint load returns not-implemented" { //============================================================================== test "version is semantic" { - const ver = std.mem.span(chapeliser_ref_version()); + const ver = std.mem.span(chapeliser_version()); try testing.expect(ver.len > 0); try testing.expect(std.mem.count(u8, ver, ".") >= 1); } test "build_info is not empty" { - const info = std.mem.span(chapeliser_ref_build_info()); + const info = std.mem.span(chapeliser_build_info()); try testing.expect(info.len > 0); try testing.expect(std.mem.indexOf(u8, info, "chapeliser") != null); } From 4210cfc38c58888a95c4787904d7968851b0ce4f Mon Sep 17 00:00:00 2001 From: Claude Date: Fri, 26 Jun 2026 22:59:38 +0000 Subject: [PATCH 2/3] =?UTF-8?q?ci:=20add=20ABI=E2=86=94FFI=20conformance?= =?UTF-8?q?=20gate?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds scripts/abi-ffi-gate.py + .github/workflows/abi-ffi-gate.yml enforcing that the Zig FFI matches the Idris2 ABI (source of truth), on top of this branch's FFI fix. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_019xMKB3T4Vo5FYC7Czx3JSH --- .github/workflows/abi-ffi-gate.yml | 38 +++++++++++ scripts/abi-ffi-gate.py | 103 +++++++++++++++++++++++++++++ 2 files changed, 141 insertions(+) create mode 100644 .github/workflows/abi-ffi-gate.yml create mode 100755 scripts/abi-ffi-gate.py 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()) From 797950fadce9edd9710c10b09187e13f6dfa84e4 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 04:44:32 +0000 Subject: [PATCH 3/3] P3: prove partition correctness generally (all n, k), not hand-picked vectors MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Proofs.idr verified completeness/disjointness only on explicit slice vectors (tenAcrossTwo, tenAcrossThree). This module, Chapeliser.ABI.Partition, lifts those invariants to the whole contiguous-partition family — quantified over an arbitrary vector of per-locale counts — and applies them to the actual block strategy (the div/mod counts of perItemSlices) for ALL n items and k locales. Key idea: contiguity is structural — a contiguous layout places each slice exactly where the previous one ended, independent of the count values — so the non-overlap guarantee needs no reasoning about div/mod (which do not reduce at the type level). - contiguousComplete: for any start and any counts, sliceSum (contiguousFrom start counts) = sumNat counts (general completeness, by induction). - Tiling + contiguousTiles: a gapless, overlap-free cover proven for any start and any counts; strictly stronger than the pairwise `disjoint` Bool check. - tilingStartsGE / tilingHeadNoOverlap: derive genuine propositional pairwise non-overlap (LTE) from a tiling, generically. - blockPartitionTiles: THE result — the real block partition is a tiling for ALL n, k. blockPartitionComplete isolates the sole residual, the div/mod identity sumNat (perItemCounts n k) = n. - shortPartitionNotComplete: negative control (a 3-locale layout summing to 9 is provably not a complete partition of 10). Adversarially verified under Idris2 0.7.0: full ABI builds clean (zero warnings, no believe_me/postulate/holes); a Tiling for deliberately overlapping slices is rejected by the type checker (start mismatch), so the non-overlap certificate is non-vacuous. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_019xMKB3T4Vo5FYC7Czx3JSH --- .../abi/Chapeliser/ABI/Partition.idr | 178 ++++++++++++++++++ src/interface/abi/chapeliser-abi.ipkg | 1 + 2 files changed, 179 insertions(+) create mode 100644 src/interface/abi/Chapeliser/ABI/Partition.idr 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