P3: prove partition correctness generally (all n, k), not hand-picked vectors#40
Merged
Conversation
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_<stem>` 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_<stem>` to
exactly `c_<stem>` 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_<name>` in Foreign.idr now has a matching
`export fn c_<name>` in main.zig.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019xMKB3T4Vo5FYC7Czx3JSH
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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019xMKB3T4Vo5FYC7Czx3JSH
… vectors 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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019xMKB3T4Vo5FYC7Czx3JSH
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What & why
Proofs.idrverified partition completeness/disjointness only on a few explicit slice vectors (tenAcrossTwo,tenAcrossThree). The §5.6 frontier is partition correctness overperItemSlicesfor all inputs — which is hard becauseperItemSlicesusesdiv/mod, and those don't reduce at the type level.Insight
Contiguity is structural:
perItemSlices' innergo offset (S r) = MkSlice offset cnt :: go (offset+cnt) rplaces each slice exactly where the previous ended, independent of thecntvalues. So the non-overlap guarantee can be proven for all n, k without ever reducingdiv/mod.Change — new module
Chapeliser.ABI.PartitioncontiguousComplete— for any start and any count vector,sliceSum (contiguousFrom start counts) = sumNat counts(general completeness, by induction).Tiling+contiguousTiles— a gapless, overlap-free cover, proven for any counts. Strictly stronger than the pairwisedisjointBool check.tilingStartsGE/tilingHeadNoOverlap— derive genuine propositional pairwise non-overlap (LTE) from a tiling, generically (the compare-based Bool<=and foldl-basedalldon't reduce symbolically, so the proof uses propositionalLTE).blockPartitionTiles— the headline: the real block partition is a non-overlapping tiling for ALL n, k.blockPartitionCompleteisolates the sole residual — thediv/modidentitysumNat (perItemCounts n k) = n— flagged as future work.shortPartitionNotComplete— negative control (a 3-locale layout summing to 9 is provably not a complete partition of 10).Verification (Idris2 0.7.0)
believe_me/postulate/holes.Tilingfor deliberately overlapping slices[0,5)/[3,8)is rejected by the type checker (Mismatch between 2 and 0) — the non-overlap certificate is non-vacuous; and the general theorem instantiates at concreten,k.Second of the priority-repo P3 deepenings (chapeliser #2).
CI note
rust-ci / Hypatia / governance reds are pre-existing estate-infra unrelated to this change.
🤖 Generated with Claude Code
https://claude.ai/code/session_019xMKB3T4Vo5FYC7Czx3JSH
Generated by Claude Code