From 58e71cc6cd08bb5c4098cd151094cdcf68b25db1 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 22:31:54 +0000 Subject: [PATCH 1/6] abi: Layer-3 div/mod completeness proof for the block partition Adds Chapeliser.ABI.Invariants, a new machine-checked theorem deeper than and distinct from the Layer-2 Partition tiling proof. Partition.idr proved the block partition is a gapless, non-overlapping tiling for all n,k but explicitly left open the arithmetic residual `sumNat (perItemCounts n k) = n` ("the only div/mod obligation"). This module discharges exactly that. blockCountsComplete : (n,k') -> sumNat (blockCounts n k') = n proves every item is covered exactly once, for ALL n and all k>0, via the Euclidean division theorem (contrib Data.Nat.Division) plus a self-contained count of remainder slots. Counts are expressed with the public-export divNatNZ/modNatNZ (the reducing form of Prelude div/mod on a positive divisor) so the proof and its concrete controls reduce at the type level. Includes: a sound+complete Dec (decCoversExactly), positive controls (covers10over3, covers12over4 by Refl + via the general theorem), and non-vacuity/negative controls (notCovers10as9, dec10over3as9No, remainderCountMatters). Genuine proof: no believe_me/postulate/assert_total/ sorry/admitted. Builds clean (0 warnings); a deliberately false variant is rejected by the type checker. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- .../abi/Chapeliser/ABI/Invariants.idr | 294 ++++++++++++++++++ src/interface/abi/chapeliser-abi.ipkg | 3 + 2 files changed, 297 insertions(+) create mode 100644 src/interface/abi/Chapeliser/ABI/Invariants.idr diff --git a/src/interface/abi/Chapeliser/ABI/Invariants.idr b/src/interface/abi/Chapeliser/ABI/Invariants.idr new file mode 100644 index 0000000..7fad469 --- /dev/null +++ b/src/interface/abi/Chapeliser/ABI/Invariants.idr @@ -0,0 +1,294 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Layer-3 invariant for Chapeliser's block partition: DIV/MOD COMPLETENESS. +||| +||| `Partition.idr` (Layer 2) proves the partition is a gapless, non-overlapping +||| *tiling* for all `n`, `k`, and reduces full completeness to one residual +||| arithmetic identity it explicitly leaves open: +||| +||| sumNat (perItemCounts n k) = n -- "the only div/mod obligation" +||| +||| This module discharges exactly that residual — the deeper, genuinely +||| different theorem. Where the Layer-2 proof was *structural* (contiguity needs +||| no reasoning about how `div`/`mod` evaluate), THIS proof is *arithmetic*: it +||| pins down the values produced by integer division of `n` by `k` and shows +||| the per-locale counts sum to exactly `n` — every one of the `n` items is +||| covered exactly once. It rests on the Euclidean division theorem +||| `n = (n mod k) + (n div k) * k` (contrib `Data.Nat.Division`) plus a +||| self-contained count of how many locale indices receive the +1 remainder +||| slot. +||| +||| Division note (Idris2 0.7.0): the Prelude `div`/`mod` on `Nat` go through the +||| `Integral` interface to `divNat`/`modNat`, which are `export partial` and so +||| do NOT reduce at the type level (idiom: "Nat div/mod do not reduce for +||| symbolic operands"). The reducing, `public export` primitives are +||| `divNatNZ`/`modNatNZ`, and `contrib`'s `DivisionTheorem` is stated over those. +||| We therefore phrase the block counts with `divNatNZ`/`modNatNZ` — the SAME +||| values the block partition uses (Prelude `div`/`mod` on a positive `Nat` +||| literally call them), just written in the form that both reduces and matches +||| the division theorem. `blockCounts n (S k')` is thus `perItemCounts n (S k')` +||| with the division spelled in its reducing primitive. +||| +||| Combined with Layer 2 this yields, for ALL n and k>0, a partition that is +||| complete (`sliceSum = n`) AND a perfect tiling — a fully proven even +||| distribution with no items lost or duplicated. + +module Chapeliser.ABI.Invariants + +import Chapeliser.ABI.Types +import Chapeliser.ABI.Partition +import Data.Vect +import Data.Nat +import Data.Nat.Division +import Decidable.Equality + +%default total + +-------------------------------------------------------------------------------- +-- The block partition's per-locale counts, in reducing (NZ) form +-------------------------------------------------------------------------------- + +||| The block partition's per-locale counts for `n` items over `S k'` locales, +||| using the `public export` division primitives so the type checker can reduce +||| through them. This is exactly `perItemCounts n (S k')` from `Partition.idr` +||| (which calls Prelude `div`/`mod` = `divNatNZ`/`modNatNZ` on the positive +||| divisor `S k'`), reusing Partition's own `countsFrom`. +public export +blockCounts : (n, k' : Nat) -> Vect (S k') Nat +blockCounts n k' = + countsFrom 0 (divNatNZ n (S k') SIsNonZero) (modNatNZ n (S k') SIsNonZero) (S k') + +-------------------------------------------------------------------------------- +-- Tiny boolean comparison facts (the `<` inside countsFrom) +-------------------------------------------------------------------------------- + +||| Nothing is below zero. +ltZeroFalse : (idx : Nat) -> (idx < 0) = False +ltZeroFalse Z = Refl +ltZeroFalse (S _) = Refl + +||| `S a < S b` decides identically to `a < b` (the comparison steps S/S down). +ltSuccSucc : (a, b : Nat) -> (S a < S b) = (a < b) +ltSuccSucc _ _ = Refl + +-------------------------------------------------------------------------------- +-- Counting the remainder ("+1") slots +-------------------------------------------------------------------------------- + +||| `numBelow idx rem cnt` counts how many of the `cnt` consecutive locale +||| indices `idx, idx+1, ..., idx+cnt-1` are strictly below `rem` — i.e. how many +||| of those locales receive the extra remainder item. It mirrors EXACTLY the +||| `if localeIdx < remainder then 1 else 0` decision inside `countsFrom`, using +||| the same Prelude boolean `<`, so the sum lemma below reduces structurally. +public export +numBelow : (idx, rem, cnt : Nat) -> Nat +numBelow _ _ Z = Z +numBelow idx rem (S c) = (if idx < rem then 1 else 0) + numBelow (S idx) rem c + +||| (a + b) + (c + d) = (a + c) + (b + d) — the only shuffle the sum law needs. +rearrange : (a, b, c, d : Nat) -> (a + b) + (c + d) = (a + c) + (b + d) +rearrange a b c d = + rewrite plusAssociative (a + b) c d in + rewrite sym (plusAssociative a b c) in + rewrite plusCommutative b c in + rewrite plusAssociative a c b in + rewrite sym (plusAssociative (a + c) b d) in + Refl + +||| Structural sum law: a `countsFrom` block contributes `base` per locale plus +||| one extra for each locale index below `rem`. No div/mod facts used here — it +||| is pure bookkeeping over the `if` in `countsFrom`. +sumCountsFrom : (idx, base, rem, cnt : Nat) -> + sumNat (countsFrom idx base rem cnt) = base * cnt + numBelow idx rem cnt +sumCountsFrom idx base rem Z = + rewrite multZeroRightZero base in Refl +sumCountsFrom idx base rem (S c) = + rewrite sumCountsFrom (S idx) base rem c in + rewrite multRightSuccPlus base c in + rearrange base (if idx < rem then 1 else 0) (base * c) (numBelow (S idx) rem c) + +-------------------------------------------------------------------------------- +-- Evaluating the remainder count exactly +-------------------------------------------------------------------------------- + +||| If the threshold is zero, no index is below it: the window contributes no +||| extra items regardless of where it starts or how long it is. +numBelowRemZero : (idx, cnt : Nat) -> numBelow idx 0 cnt = 0 +numBelowRemZero idx Z = Refl +numBelowRemZero idx (S c) = + rewrite ltZeroFalse idx in + numBelowRemZero (S idx) c + +||| Shifting both the index and the threshold up by one leaves the count +||| unchanged: `S idx < S rem` holds exactly when `idx < rem`. +numBelowShift : (idx, rem, cnt : Nat) -> + numBelow (S idx) (S rem) cnt = numBelow idx rem cnt +numBelowShift idx rem Z = Refl +numBelowShift idx rem (S c) = + -- head: (if S idx < S rem ..) = (if idx < rem ..) by ltSuccSucc; + -- tail: numBelow (S (S idx)) (S rem) c = numBelow (S idx) rem c by IH. + -- Combine the two equalities additively with cong2 (+). + cong2 (+) + (cong (\b => if b then (the Nat 1) else 0) (ltSuccSucc idx rem)) + (numBelowShift (S idx) rem c) + +||| EXACT remainder count over the full locale range `[0, cnt)`: when the +||| remainder `rem` does not exceed the number of locales `cnt`, exactly `rem` +||| locales (indices 0 .. rem-1) receive the extra item. This is the heart of +||| the arithmetic argument and is where `rem <= cnt` (i.e. `n mod k < k`) is +||| consumed. +numBelowFull : (rem, cnt : Nat) -> LTE rem cnt -> numBelow 0 rem cnt = rem +numBelowFull Z cnt _ = numBelowRemZero 0 cnt +numBelowFull (S r) (S c) (LTESucc le) = + -- idx 0 < S r is True (0 < S r reduces to True), so head = 1; the tail is + -- numBelow 1 (S r) c = numBelow 0 r c (numBelowShift), then IH gives r. + rewrite numBelowShift 0 r c in + cong S (numBelowFull r c le) + +-------------------------------------------------------------------------------- +-- The remainder is below the locale count (n mod k < k) +-------------------------------------------------------------------------------- + +||| `n mod (S k')` (in reducing NZ form) is strictly less than `S k'`, hence +||| `<= S k'`. Strict bound from contrib's `boundModNatNZ`, then weakened. +modLEk : (n, k' : Nat) -> LTE (modNatNZ n (S k') SIsNonZero) (S k') +modLEk n k' = lteSuccLeft (boundModNatNZ n (S k') SIsNonZero) + +-------------------------------------------------------------------------------- +-- MAIN LAYER-3 THEOREM +-------------------------------------------------------------------------------- + +||| DIV/MOD COMPLETENESS, the residual left open by `Partition.idr`: +||| for every item count `n` and every POSITIVE locale count `S k'`, the block +||| partition's per-locale counts sum to exactly `n`. No item is dropped or +||| double-assigned. Quantified over ALL n, k'. +||| +||| Proof: the counts sum to `base * k + (remainder count)` (`sumCountsFrom`); +||| the remainder count is exactly `n mod k` because `n mod k <= k` +||| (`numBelowFull` + `modLEk`); and `base * k + n mod k = n div k * k + n mod k +||| = n` by the Euclidean division theorem. +export +blockCountsComplete : (n, k' : Nat) -> sumNat (blockCounts n k') = n +blockCountsComplete n k' = + let base : Nat + base = divNatNZ n (S k') SIsNonZero + rem : Nat + rem = modNatNZ n (S k') SIsNonZero + -- 1. structural sum law + step1 : sumNat (blockCounts n k') = base * (S k') + numBelow 0 rem (S k') + step1 = sumCountsFrom 0 base rem (S k') + -- 2. the remainder count collapses to rem, using n mod k <= k + step2 : numBelow 0 rem (S k') = rem + step2 = numBelowFull rem (S k') (modLEk n k') + -- 3. Euclidean division theorem: n = rem + base * (S k') + divThm : n = rem + base * (S k') + divThm = DivisionTheorem n (S k') SIsNonZero SIsNonZero + in rewrite step1 in + rewrite step2 in + -- goal: base * (S k') + rem = n + rewrite plusCommutative (base * (S k')) rem in + -- goal: rem + base * (S k') = n + sym divThm + +||| Corollary in the Layer-2 vocabulary: the block partition's `sliceSum` equals +||| `n` for all n and k>0. `blockPartitionComplete` (Layer 2) reduced sliceSum to +||| `sumNat (perItemCounts n k)`; `blockCounts n k'` is that very count vector in +||| reducing form, so this closes the completeness loop for the real strategy. +export +blockSlicesSumIsN : (n, k' : Nat) -> + sliceSum (contiguousFrom 0 (blockCounts n k')) = n +blockSlicesSumIsN n k' = + rewrite contiguousComplete 0 (blockCounts n k') in + blockCountsComplete n k' + +||| The full `PartitionComplete` proof OBJECT for the block partition, packaged +||| as a `Partition` (the Layer-2 invariant type `sliceSum p.slices = n`), now +||| DISCHARGED for the real block strategy at any n and k>0 — previously only +||| provable for hand-written fixed vectors in `Proofs.idr`. +export +blockPartitionIsComplete : (n, k' : Nat) -> + PartitionComplete + (MkPartition {n} {k = S k'} (contiguousFrom 0 (blockCounts n k'))) +blockPartitionIsComplete n k' = IsComplete (blockSlicesSumIsN n k') + +-------------------------------------------------------------------------------- +-- Sound + complete decision for "these counts cover exactly n" +-------------------------------------------------------------------------------- + +||| A natural decision: do a candidate count vector's slices sum to exactly the +||| declared item total? Decidable because `sumNat` is a concrete Nat and `Nat` +||| has `DecEq`. Sound (Yes carries the equality) and complete (No carries a +||| refutation), via `decEq`. +export +decCoversExactly : (target : Nat) -> (counts : Vect k Nat) -> + Dec (sumNat counts = target) +decCoversExactly target counts = decEq (sumNat counts) target + +||| Reduce a `Dec` to whether it is the `No` branch — a concrete projector that +||| evaluates, used by the negative-control below (the `No contra` term itself +||| does not reduce cheaply, but its tag does). +public export +decidedNo : Dec p -> Bool +decidedNo (Yes _) = False +decidedNo (No _) = True + +-------------------------------------------------------------------------------- +-- POSITIVE controls: concrete inhabited instances +-------------------------------------------------------------------------------- + +||| Positive witness: 10 items over 3 locales. base = 3, rem = 1, so counts are +||| [4,3,3] summing to 10. Machine-checked by `Refl` (the NZ primitives reduce on +||| concrete literals) AND re-derived by the general theorem below. +export +covers10over3 : sumNat (blockCounts 10 2) = 10 +covers10over3 = Refl + +||| The same fact via the general Layer-3 theorem, confirming the abstract proof +||| specialises to the concrete reduct. +export +covers10over3_general : sumNat (blockCounts 10 2) = 10 +covers10over3_general = blockCountsComplete 10 2 + +||| A second concrete instance where division is exact (rem = 0): 12 over 4 gives +||| [3,3,3,3] summing to 12. Exercises the `rem = 0` branch of the counting. +export +covers12over4 : sumNat (blockCounts 12 3) = 12 +covers12over4 = Refl + +||| A positive Dec witness: the decision says Yes for the [4,3,3] cover of 10. +||| `decCoversExactly` returns `Yes` here, and we project its proof. +export +dec10over3Yes : decCoversExactly 10 (blockCounts 10 2) = Yes Refl +dec10over3Yes = Refl + +-------------------------------------------------------------------------------- +-- NEGATIVE / non-vacuity controls +-------------------------------------------------------------------------------- + +||| Non-vacuity 1: the theorem is NOT trivially true for the wrong target. The +||| block cover of 10 does not sum to 9. We derive it from the real total (10): +||| if it were also 9 then 10 = 9, absurd. (A bare `Refl : ... = 9` would itself +||| be a type error, which is the point.) +export +notCovers10as9 : Not (sumNat (blockCounts 10 2) = 9) +notCovers10as9 prf = + -- blockCountsComplete 10 2 : sumNat (blockCounts 10 2) = 10 + uninhabited (trans (sym (blockCountsComplete 10 2)) prf) + +||| Non-vacuity 2: the decision procedure genuinely says No when the target is +||| wrong (9 vs the true 10). If `decCoversExactly` always said Yes the theorem +||| would be vacuous; this `Refl` (the No tag reduces concretely) rules it out. +||| Paired with `notCovers10as9`, this is the sound+complete negative side of the +||| decision (Yes side witnessed by `dec10over3Yes`). +export +dec10over3as9No : decidedNo (decCoversExactly 9 (blockCounts 10 2)) = True +dec10over3as9No = Refl + +||| Non-vacuity 3 (numBelow is real, not a constant): with threshold 0 nobody +||| gets the extra slot, but with a positive threshold somebody does — these are +||| DIFFERENT, so the remainder count truly depends on `rem`. A `Refl` here would +||| be ill-typed (0 vs 2), so the negation is the honest statement. +export +remainderCountMatters : Not (numBelow 0 0 5 = numBelow 0 2 5) +remainderCountMatters prf = uninhabited prf diff --git a/src/interface/abi/chapeliser-abi.ipkg b/src/interface/abi/chapeliser-abi.ipkg index ebad5e0..1e9cea9 100644 --- a/src/interface/abi/chapeliser-abi.ipkg +++ b/src/interface/abi/chapeliser-abi.ipkg @@ -5,8 +5,11 @@ package chapeliser-abi sourcedir = "." +depends = contrib + modules = Chapeliser.ABI.Types , Chapeliser.ABI.Layout , Chapeliser.ABI.Foreign , Chapeliser.ABI.Proofs , Chapeliser.ABI.Partition + , Chapeliser.ABI.Invariants From 613bae4fb33c6581853c4056c71ae7f1e2d02864 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 28 Jun 2026 05:48:15 +0000 Subject: [PATCH 2/6] abi: seal ABI<->FFI seam with Layer 4 soundness proofs (Chapeliser.ABI.FfiSeam) Add a new module proving the Result FFI encoding is sound: - intToResult decoder + resultRoundTrip: the C integer faithfully round-trips back to the ABI Result (lossless/faithful encoding). - resultToIntInjective: distinct ABI outcomes never collide on the wire, derived from the round-trip via justInj . cong intToResult. - Positive controls (concrete decode = Refl) and a machine-checked non-vacuity control: distinct codes have distinct ints. Genuine total proofs, no believe_me/postulate/assert_total/etc. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- src/interface/abi/Chapeliser/ABI/FfiSeam.idr | 132 +++++++++++++++++++ src/interface/abi/chapeliser-abi.ipkg | 1 + 2 files changed, 133 insertions(+) create mode 100644 src/interface/abi/Chapeliser/ABI/FfiSeam.idr diff --git a/src/interface/abi/Chapeliser/ABI/FfiSeam.idr b/src/interface/abi/Chapeliser/ABI/FfiSeam.idr new file mode 100644 index 0000000..a024c4e --- /dev/null +++ b/src/interface/abi/Chapeliser/ABI/FfiSeam.idr @@ -0,0 +1,132 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Chapeliser ABI <-> FFI Seam Soundness Proofs (Layer 4) +||| +||| The structural gate (scripts/abi-ffi-gate.py) checks that the Idris2 +||| `resultToInt` encoder and the Zig FFI enum agree by name+value. This +||| module supplies the PROOF-SIDE guarantee that the encoding itself is +||| SOUND, independent of any external comparison: +||| +||| 1. resultRoundTrip — the C integer faithfully ROUND-TRIPS back to the +||| ABI `Result` value (the encoding is lossless / faithful). A decoder +||| `intToResult : Bits32 -> Maybe Result` recovers exactly the encoded +||| constructor. +||| 2. resultToIntInjective — distinct ABI outcomes NEVER collide on the +||| wire (the encoding is unambiguous). This is DERIVED from the +||| round-trip via `justInj . cong intToResult`, so injectivity is +||| a corollary of faithfulness rather than a separate hand proof. +||| +||| Together these seal the ABI<->FFI seam: every `Result` maps to a unique +||| C integer, and that integer decodes back to the same `Result`. +||| +||| All proofs are genuine and machine-checked — no `believe_me`, +||| `idris_crash`, `assert_total`, `postulate`, `sorry`, or `%hint` hacks. + +module Chapeliser.ABI.FfiSeam + +import Chapeliser.ABI.Types + +%default total + +-------------------------------------------------------------------------------- +-- Local helper: Just is injective +-------------------------------------------------------------------------------- + +||| `Just` is injective. Proved locally (rather than relying on a Prelude name) +||| by matching the single `Refl` constructor of the hypothesis. +private +justInj : {0 x, y : a} -> Just x = Just y -> x = y +justInj Refl = Refl + +-------------------------------------------------------------------------------- +-- Decoder: C integer back to ABI Result +-------------------------------------------------------------------------------- + +||| Decode a C-compatible integer back to a `Result`. +||| +||| Built with boolean `==` on concrete `Bits32` literals (rather than a +||| `case`/pattern match on literals) precisely so the comparison REDUCES +||| definitionally on closed literals — this is what lets the `resultRoundTrip` +||| witnesses below check as plain `Refl`. Unknown codes decode to `Nothing`. +public export +intToResult : Bits32 -> Maybe Result +intToResult x = + if x == 0 then Just Ok + else if x == 1 then Just Error + else if x == 2 then Just InvalidParam + else if x == 3 then Just OutOfMemory + else if x == 4 then Just NullPointer + else if x == 5 then Just RetryExhausted + else if x == 6 then Just CheckpointError + else Nothing + +-------------------------------------------------------------------------------- +-- (b) Faithful / lossless encoding: round-trip +-------------------------------------------------------------------------------- + +||| The encoding is FAITHFUL: decoding the C integer produced by `resultToInt` +||| recovers exactly the original `Result`. One clause per constructor; each +||| reduces to `Refl` because the boolean `==` in `intToResult` evaluates on +||| the concrete `Bits32` literal that `resultToInt` emits. +public export +resultRoundTrip : (r : Result) -> intToResult (resultToInt r) = Just r +resultRoundTrip Ok = Refl +resultRoundTrip Error = Refl +resultRoundTrip InvalidParam = Refl +resultRoundTrip OutOfMemory = Refl +resultRoundTrip NullPointer = Refl +resultRoundTrip RetryExhausted = Refl +resultRoundTrip CheckpointError = Refl + +-------------------------------------------------------------------------------- +-- (a) Unambiguous encoding: injectivity (DERIVED from the round-trip) +-------------------------------------------------------------------------------- + +||| The encoding is INJECTIVE: distinct ABI outcomes never collide on the wire. +||| +||| Derived from `resultRoundTrip`: if `resultToInt a = resultToInt b` then +||| applying `intToResult` to both sides (via `cong`) gives +||| `Just a = Just b` (rewriting through the two round-trip equalities), and +||| `justInj` strips the `Just`. No constructor case analysis needed. +public export +resultToIntInjective : (a, b : Result) -> + resultToInt a = resultToInt b -> a = b +resultToIntInjective a b prf = + justInj $ + rewrite sym (resultRoundTrip a) in + rewrite sym (resultRoundTrip b) in + cong intToResult prf + +-------------------------------------------------------------------------------- +-- Positive controls (concrete decodes = Refl) +-------------------------------------------------------------------------------- + +||| Positive control: code 0 decodes to `Ok`. +decodeOk : intToResult 0 = Just Ok +decodeOk = Refl + +||| Positive control: code 6 (the largest) decodes to `CheckpointError`. +decodeCheckpointError : intToResult 6 = Just CheckpointError +decodeCheckpointError = Refl + +||| Positive control: an out-of-range code decodes to `Nothing` (the decoder +||| is total and rejects codes that no `Result` maps to). +decodeUnknown : intToResult 7 = Nothing +decodeUnknown = Refl + +-------------------------------------------------------------------------------- +-- Negative / non-vacuity control +-------------------------------------------------------------------------------- + +||| NON-VACUITY: two DISTINCT result codes have DISTINCT integers, machine +||| checked. `resultToInt Ok` reduces to the literal `0` and `resultToInt +||| Error` to `1`; distinct primitive `Bits32` literals are provably unequal, +||| so the coverage checker discharges the impossible `Refl`. This rules out +||| the trivial (vacuous) world in which the encoder is constant. +okErrorDistinct : Not (resultToInt Ok = resultToInt Error) +okErrorDistinct Refl impossible + +||| A second distinctness witness across a non-adjacent pair, for good measure. +nullCheckpointDistinct : Not (resultToInt NullPointer = resultToInt CheckpointError) +nullCheckpointDistinct Refl impossible diff --git a/src/interface/abi/chapeliser-abi.ipkg b/src/interface/abi/chapeliser-abi.ipkg index 1e9cea9..c043ae3 100644 --- a/src/interface/abi/chapeliser-abi.ipkg +++ b/src/interface/abi/chapeliser-abi.ipkg @@ -13,3 +13,4 @@ modules = Chapeliser.ABI.Types , Chapeliser.ABI.Proofs , Chapeliser.ABI.Partition , Chapeliser.ABI.Invariants + , Chapeliser.ABI.FfiSeam From 0ac7f00d8f58eddc6b96f340ff66425aa4ea517d Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 28 Jun 2026 06:48:27 +0000 Subject: [PATCH 3/6] Add Layer-5 ABI soundness capstone certificate MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Assemble the existing proof layers into one inhabited certificate value in Chapeliser.ABI.Capstone: - ABISound record whose fields reuse real exported witnesses: * flagshipValid -> Proofs.tenAcrossTwoValid (Layer 2, complete+disjoint) * blockComplete -> Invariants.blockPartitionIsComplete 10 2 (Layer 3) * blockCompleteAll -> Invariants.blockCountsComplete (Layer 3, general) * ffiInjective -> FfiSeam.resultToIntInjective (Layer 4 seam) - abiContractDischarged : ABISound — the single inhabited capstone value; ties manifest -> ABI proofs (flagship + invariant) -> FFI seam into one end-to-end soundness statement. Stops typechecking if any layer weakens. No believe_me/postulate/assert_total/sorry/%hint; %default total; SPDX line 1. Build clean (0 warnings); adversarial false-field certificate is rejected. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- src/interface/abi/Chapeliser/ABI/Capstone.idr | 102 ++++++++++++++++++ src/interface/abi/chapeliser-abi.ipkg | 1 + 2 files changed, 103 insertions(+) create mode 100644 src/interface/abi/Chapeliser/ABI/Capstone.idr diff --git a/src/interface/abi/Chapeliser/ABI/Capstone.idr b/src/interface/abi/Chapeliser/ABI/Capstone.idr new file mode 100644 index 0000000..2e1c8b4 --- /dev/null +++ b/src/interface/abi/Chapeliser/ABI/Capstone.idr @@ -0,0 +1,102 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Chapeliser ABI Soundness CAPSTONE (Layer 5) +||| +||| This module is the END-TO-END certificate: it ASSEMBLES the already-proven +||| facts of every prior ABI layer into a SINGLE inhabited value. It proves no +||| new domain theorem of its own — its entire content is that the prior layers +||| compose, and that one record can be built from their real exported witnesses. +||| If any earlier layer were unsound (its witness retracted or weakened), the +||| value `abiContractDischarged` below would simply fail to typecheck and the +||| proof build would go red. +||| +||| The contract it ties together, manifest -> ABI proofs -> FFI seam: +||| +||| * Layer 2 (flagship property, `Proofs.idr`): the canonical positive-control +||| partition `tenAcrossTwo` is a VALID partition — complete AND disjoint +||| (`Proofs.tenAcrossTwoValid : ValidPartition Proofs.tenAcrossTwo`). This is +||| the manifest-level "no item lost or double-placed" guarantee on a concrete +||| instance. +||| +||| * Layer 3 (deeper invariant, `Invariants.idr`): the REAL block-partition +||| strategy (the div/mod counts the codegen actually emits) is complete for +||| all n and k>0 — discharged here on the canonical 10-over-3 instance via +||| `Invariants.blockPartitionIsComplete`, the packaged `PartitionComplete` +||| object. We also carry the GENERAL theorem `blockCountsComplete` as a field +||| so the certificate witnesses universal, not merely pointwise, completeness. +||| +||| * Layer 4 (FFI seam, `FfiSeam.idr`): the `resultToInt` encoder crossing the +||| Zig/C boundary is INJECTIVE — distinct ABI outcomes never collide on the +||| wire (`FfiSeam.resultToIntInjective`). This is the seam soundness the FFI +||| wrappers depend on. +||| +||| One value below inhabits all of these at once: that is the soundness +||| certificate. A deliberately-FALSE field is rejected by the type checker (see +||| the adversarial control in /tmp during the build procedure), so the record is +||| non-vacuous: it cannot be built from a bogus component. +||| +||| All composition is genuine: no `believe_me`, `idris_crash`, `assert_total`, +||| `postulate`, `sorry`, or `%hint` hacks. Every field is filled with a name +||| actually exported by the module it comes from. + +module Chapeliser.ABI.Capstone + +import Chapeliser.ABI.Types +import Chapeliser.ABI.Proofs +import Chapeliser.ABI.Partition +import Chapeliser.ABI.Invariants +import Chapeliser.ABI.FfiSeam + +import Data.Vect + +%default total + +-------------------------------------------------------------------------------- +-- The capstone certificate type +-------------------------------------------------------------------------------- + +||| `ABISound` is the end-to-end ABI soundness certificate. Each field is a KEY +||| proven fact of a prior layer, reused verbatim — the record is inhabited iff +||| every layer it names is itself sound. +public export +record ABISound where + constructor MkABISound + ||| Layer 2 flagship: the canonical positive-control partition is VALID + ||| (complete and non-overlapping). Reuses `Proofs.tenAcrossTwoValid`. + flagshipValid : ValidPartition Proofs.tenAcrossTwo + + ||| Layer 3 invariant, concrete: the REAL block partition of 10 items over 3 + ||| locales is complete (`PartitionComplete` object). Reuses + ||| `Invariants.blockPartitionIsComplete`. + blockComplete : + PartitionComplete + (MkPartition {n = 10} {k = 3} (contiguousFrom 0 (blockCounts 10 2))) + + ||| Layer 3 invariant, GENERAL: the block partition's per-locale counts sum to + ||| exactly `n` for every item count `n` and every positive locale count + ||| `S k'`. Reuses `Invariants.blockCountsComplete` (universal, not pointwise). + blockCompleteAll : (n, k' : Nat) -> sumNat (blockCounts n k') = n + + ||| Layer 4 FFI seam: the `resultToInt` encoder is injective — distinct ABI + ||| outcomes never collide on the wire. Reuses `FfiSeam.resultToIntInjective`. + ffiInjective : (a, b : Result) -> resultToInt a = resultToInt b -> a = b + +-------------------------------------------------------------------------------- +-- The capstone value: the contract, discharged +-------------------------------------------------------------------------------- + +||| THE CAPSTONE. A single inhabited `ABISound`, assembled entirely from the +||| existing exported witnesses/theorems of Layers 2, 3 and 4. Its mere +||| typechecking is the proof that the full ABI contract — manifest-level +||| partition validity, real-strategy completeness, and FFI-seam injectivity — +||| is discharged together, end to end. Weaken any contributing proof and this +||| value stops typechecking. +export +abiContractDischarged : ABISound +abiContractDischarged = + MkABISound + Proofs.tenAcrossTwoValid + (Invariants.blockPartitionIsComplete 10 2) + Invariants.blockCountsComplete + FfiSeam.resultToIntInjective diff --git a/src/interface/abi/chapeliser-abi.ipkg b/src/interface/abi/chapeliser-abi.ipkg index c043ae3..e508ac0 100644 --- a/src/interface/abi/chapeliser-abi.ipkg +++ b/src/interface/abi/chapeliser-abi.ipkg @@ -14,3 +14,4 @@ modules = Chapeliser.ABI.Types , Chapeliser.ABI.Partition , Chapeliser.ABI.Invariants , Chapeliser.ABI.FfiSeam + , Chapeliser.ABI.Capstone From 100efb25ae8fcf39976423ba0ff178ea07b91cf8 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 28 Jun 2026 07:42:25 +0000 Subject: [PATCH 4/6] =?UTF-8?q?ci:=20make=20CI=20green=20=E2=80=94=20bump?= =?UTF-8?q?=20rust-ci=20to=20standards@8dc2bf0=20(toolchain:=20stable=20fi?= =?UTF-8?q?x);=20port=20ABI-FFI=20gate=20Python->Bash=20(Python=20is=20est?= =?UTF-8?q?ate-banned)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Resolves the standing baseline CI reds (rust-ci toolchain error, governance Language/anti-pattern, governance workflow-lint) without altering the proven ABI. The Bash gate reproduces the former Python gate's verdict verbatim (validated across all -iser repos) and catches the same drift classes. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- .github/workflows/abi-ffi-gate.yml | 2 +- .github/workflows/rust-ci.yml | 2 +- scripts/abi-ffi-gate.py | 103 -------------------------- scripts/abi-ffi-gate.sh | 113 +++++++++++++++++++++++++++++ 4 files changed, 115 insertions(+), 105 deletions(-) delete mode 100755 scripts/abi-ffi-gate.py create mode 100755 scripts/abi-ffi-gate.sh diff --git a/.github/workflows/abi-ffi-gate.yml b/.github/workflows/abi-ffi-gate.yml index 269464d..d88579a 100644 --- a/.github/workflows/abi-ffi-gate.yml +++ b/.github/workflows/abi-ffi-gate.yml @@ -22,7 +22,7 @@ jobs: steps: - uses: actions/checkout@v4 - name: Run ABI-FFI gate - run: python3 scripts/abi-ffi-gate.py + run: bash scripts/abi-ffi-gate.sh zig-build: name: Zig FFI builds + tests (Zig 0.14.0) diff --git a/.github/workflows/rust-ci.yml b/.github/workflows/rust-ci.yml index c60e60a..b1b86c6 100644 --- a/.github/workflows/rust-ci.yml +++ b/.github/workflows/rust-ci.yml @@ -14,4 +14,4 @@ permissions: jobs: rust-ci: - uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@d135b05bfc647d0c0fbfedc7e80f37ea50f49236 + uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@8dc2bf039d1ff0372d650895c46bea7fbaec68ff diff --git a/scripts/abi-ffi-gate.py b/scripts/abi-ffi-gate.py deleted file mode 100755 index 9ee96db..0000000 --- a/scripts/abi-ffi-gate.py +++ /dev/null @@ -1,103 +0,0 @@ -#!/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/scripts/abi-ffi-gate.sh b/scripts/abi-ffi-gate.sh new file mode 100755 index 0000000..3258af3 --- /dev/null +++ b/scripts/abi-ffi-gate.sh @@ -0,0 +1,113 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# abi-ffi-gate.sh — fail (exit 1) if the Zig FFI does not conform to the Idris2 +# ABI. The Idris2 ABI is the source of truth. Bash port of the former +# abi-ffi-gate.py (Python is banned estate-wide). No toolchain needed — only +# coreutils + grep/awk/sed. Checks: +# +# 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: bash scripts/abi-ffi-gate.sh [repo_root] (defaults to cwd) +set -uo pipefail + +root="${1:-.}" +name="$(basename "$(cd "$root" 2>/dev/null && pwd || echo "$root")")" +abi_dir="$root/src/interface/abi" +zig_path="$root/src/interface/ffi/src/main.zig" + +# canon(name): camelCase -> snake_case, lowercase, err -> error +canon() { + printf '%s' "$1" \ + | sed -E 's/([a-zA-Z0-9])([A-Z])/\1_\2/g' \ + | tr '[:upper:]' '[:lower:]' \ + | sed -E 's/^err$/error/' +} + +idr_files="$(find "$abi_dir" -name '*.idr' -not -path '*/build/*' 2>/dev/null | sort)" +if [ -z "$idr_files" ]; then + echo "ABI-FFI GATE: SKIP ($name) — no Idris2 ABI .idr files under $abi_dir" + exit 0 +fi +if [ ! -f "$zig_path" ]; then + echo "ABI-FFI GATE: FAIL ($name) — no Zig FFI at $zig_path" + exit 1 +fi + +idr="$(cat $idr_files)" +zig="$(cat "$zig_path")" +errs="" + +# 1. unrendered template tokens +toks="$(printf '%s\n' "$zig" | grep -oE '\{\{[A-Za-z0-9_]+\}\}' | sort -u | tr '\n' ' ')" +if [ -n "${toks// /}" ]; then + errs="${errs} - Zig FFI has unrendered template tokens: ${toks} +" +fi + +# 2. foreign C symbols must be exported +csyms="$(printf '%s\n' "$idr" | grep -oE 'C:[A-Za-z0-9_]+' | sed 's/^C://' | sort -u | grep -v '^$')" +exports="$(printf '%s\n' "$zig" | grep -oE 'export fn [A-Za-z0-9_]+' | awk '{print $3}' | sort -u | grep -v '^$')" +missing="$(comm -23 <(printf '%s\n' "$csyms") <(printf '%s\n' "$exports") | tr '\n' ' ')" +ncsyms="$(printf '%s\n' "$csyms" | grep -vc '^$' || true)" +if [ -n "${missing// /}" ]; then + errs="${errs} - ABI function(s) not exported by the Zig FFI: ${missing} +" +fi + +# 3. result-code map (names + values) must agree +idr_rc="$(printf '%s\n' "$idr" \ + | grep -oE 'resultToInt +[A-Za-z0-9]+ *= *[0-9]+' \ + | sed -E 's/resultToInt +([A-Za-z0-9]+) *= *([0-9]+)/\1 \2/' \ + | while read -r nm val; do echo "$(canon "$nm") $val"; done | sort -u)" +nrc="$(printf '%s\n' "$idr_rc" | grep -vc '^$' || true)" + +# Parse each `enum (c_int) { ... }` block separately (variants up to the first +# `}`), tagged by a block id. Then in shell, canonicalise each block and pick +# the one whose `ok == 0` with the most variants — mirrors Python find_result_enum. +zig_raw="$(printf '%s\n' "$zig" | awk ' + /enum[ \t]*\([ \t]*c_int[ \t]*\)/ { cap=1; bid++ } + cap { + s=$0 + while (match(s, /@?"?[A-Za-z_][A-Za-z0-9_]*"?[ \t]*=[ \t]*[0-9]+/)) { + seg=substr(s, RSTART, RLENGTH); s=substr(s, RSTART+RLENGTH) + gsub(/[@"\t ]/,"",seg) + eq=index(seg,"="); k=substr(seg,1,eq-1); v=substr(seg,eq+1) + print bid, k, v + } + if ($0 ~ /\}/) cap=0 + } +')" + +zig_rc_final=""; best_n=-1 +for bid in $(printf '%s\n' "$zig_raw" | awk 'NF{print $1}' | sort -un); do + cb="$(printf '%s\n' "$zig_raw" | awk -v b="$bid" '$1==b{print $2" "$3}' \ + | while read -r nm val; do [ -n "$nm" ] && echo "$(canon "$nm") $val"; done | sort -u)" + if printf '%s\n' "$cb" | grep -qx 'ok 0'; then + cnt="$(printf '%s\n' "$cb" | grep -vc '^$')" + if [ "$cnt" -gt "$best_n" ]; then best_n="$cnt"; zig_rc_final="$cb"; fi + fi +done + +if [ "$nrc" -gt 0 ] && [ -z "$zig_rc_final" ]; then + errs="${errs} - no Zig enum(c_int) Result block (with ok = 0) found to compare result codes +" +elif [ "$nrc" -gt 0 ] && [ -n "$zig_rc_final" ] && [ "$idr_rc" != "$zig_rc_final" ]; then + errs="${errs} - Result-code map differs (name or value): + Idris resultToInt: $(printf '%s' "$idr_rc" | tr '\n' ',') + Zig Result enum: $(printf '%s' "$zig_rc_final" | tr '\n' ',') +" +fi + +if [ -n "$errs" ]; then + echo "ABI-FFI GATE: FAIL ($name)" + printf '%s' "$errs" + exit 1 +fi +echo "ABI-FFI GATE: OK ($name) — ${ncsyms} ABI functions exported, ${nrc} result codes match" +exit 0 From 7fd2fbcfd6d72469e09568355e17c4efddffa52b Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 28 Jun 2026 08:01:25 +0000 Subject: [PATCH 5/6] ci: adopt canonical Julia ABI-FFI gate (estate standard, matches verisimiser) in place of the interim Bash port --- .github/workflows/abi-ffi-gate.yml | 9 ++- scripts/abi-ffi-gate.jl | 116 +++++++++++++++++++++++++++++ scripts/abi-ffi-gate.sh | 113 ---------------------------- 3 files changed, 124 insertions(+), 114 deletions(-) create mode 100644 scripts/abi-ffi-gate.jl delete mode 100755 scripts/abi-ffi-gate.sh diff --git a/.github/workflows/abi-ffi-gate.yml b/.github/workflows/abi-ffi-gate.yml index d88579a..f647ba6 100644 --- a/.github/workflows/abi-ffi-gate.yml +++ b/.github/workflows/abi-ffi-gate.yml @@ -21,8 +21,15 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 + - name: Install Julia 1.11.5 + run: | + curl -fsSL https://julialang-s3.julialang.org/bin/linux/x64/1.11/julia-1.11.5-linux-x86_64.tar.gz -o /tmp/julia.tar.gz + tar -xf /tmp/julia.tar.gz -C /tmp + echo "/tmp/julia-1.11.5/bin" >> "$GITHUB_PATH" - name: Run ABI-FFI gate - run: bash scripts/abi-ffi-gate.sh + run: | + julia --version # confirms the pinned 1.11.5 is on PATH, not the runner default + julia scripts/abi-ffi-gate.jl zig-build: name: Zig FFI builds + tests (Zig 0.14.0) diff --git a/scripts/abi-ffi-gate.jl b/scripts/abi-ffi-gate.jl new file mode 100644 index 0000000..540ce1a --- /dev/null +++ b/scripts/abi-ffi-gate.jl @@ -0,0 +1,116 @@ +#!/usr/bin/env julia +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# abi-ffi-gate.jl — 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 compile toolchain +# needed (pure base-Julia text analysis): +# +# 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: julia scripts/abi-ffi-gate.jl [repo_root] (defaults to cwd) +# +# Julia port of the former scripts/abi-ffi-gate.py (Python is banned estate-wide, +# RSR-H4); behaviour is identical. + +"camelCase / PascalCase → snake_case (insert `_` before each non-initial capital)." +camel_to_snake(s) = lowercase(replace(s, r"(? "_")) + +"Canonical result-code key: lowercased, with `err`/`error` unified to `error`." +function canon_rc(name) + n = lowercase(name) + (n == "err" || n == "error") ? "error" : n +end + +"Return {variant => value} for the C-ABI `Result` enum (the `enum(c_int)` block whose `ok = 0`), or empty." +function find_result_enum(zig::AbstractString) + best = Dict{String,Int}() + for m in eachmatch(r"enum\s*\(\s*c_int\s*\)\s*\{(.*?)\}"s, zig) + body = m.captures[1] + variants = Dict{String,Int}() + for vm in eachmatch(r"@?\"?([A-Za-z_][A-Za-z0-9_]*)\"?\s*=\s*(\d+)", body) + variants[canon_rc(vm.captures[1])] = parse(Int, vm.captures[2]) + end + # The Result enum is the one starting at ok = 0. + if get(variants, "ok", nothing) == 0 && length(variants) > length(best) + best = variants + end + end + return best +end + +"Collect every `*.idr` under `abi_dir`, skipping any `build/` output directory." +function idr_sources(abi_dir::AbstractString) + files = String[] + isdir(abi_dir) || return files + for (root, _dirs, fs) in walkdir(abi_dir) + occursin("/build/", root * "/") && continue + for f in fs + endswith(f, ".idr") && push!(files, joinpath(root, f)) + end + end + return files +end + +function main(root::AbstractString)::Int + name = basename(rstrip(abspath(root), '/')) + abi_dir = joinpath(root, "src/interface/abi") + zig_path = joinpath(root, "src/interface/ffi/src/main.zig") + errs = String[] + + idr_files = idr_sources(abi_dir) + if isempty(idr_files) + println("ABI-FFI GATE: SKIP ($name) — no Idris2 ABI .idr files under $abi_dir") + return 0 + end + if !isfile(zig_path) + println("ABI-FFI GATE: FAIL ($name) — no Zig FFI at $zig_path") + return 1 + end + + idr = join((read(p, String) for p in idr_files), "\n") + zig = read(zig_path, String) + + # 1. unrendered template tokens + toks = sort(unique(String(m.match) for m in eachmatch(r"\{\{[A-Za-z0-9_]+\}\}", zig))) + isempty(toks) || push!(errs, "Zig FFI has unrendered template tokens: $(toks)") + + # 2. foreign C symbols must be exported + csyms = sort(unique(String(m.captures[1]) for m in eachmatch(r"C:([A-Za-z0-9_]+)", idr))) + exports = Set(String(m.captures[1]) for m in eachmatch(r"export fn ([A-Za-z0-9_]+)", zig)) + missing_syms = [s for s in csyms if !(s in exports)] + isempty(missing_syms) || + push!(errs, "$(length(missing_syms)) ABI function(s) not exported by the Zig FFI: $(missing_syms)") + + # 3. result-code map (names + values) must agree + idr_rc = Dict{String,Int}() + for m in eachmatch(r"resultToInt\s+([A-Za-z0-9]+)\s*=\s*(\d+)", idr) + idr_rc[canon_rc(camel_to_snake(m.captures[1]))] = parse(Int, m.captures[2]) + end + zig_rc = find_result_enum(zig) + if !isempty(idr_rc) && isempty(zig_rc) + push!(errs, "no Zig `enum(c_int)` Result block (with `ok = 0`) found to compare result codes") + elseif !isempty(idr_rc) && !isempty(zig_rc) && idr_rc != zig_rc + push!(errs, "Result-code map differs (name or value):\n" * + " Idris resultToInt: $(sort(collect(idr_rc)))\n" * + " Zig Result enum: $(sort(collect(zig_rc)))") + end + + if !isempty(errs) + println("ABI-FFI GATE: FAIL ($name)") + for e in errs + println(" - " * e) + end + return 1 + end + println("ABI-FFI GATE: OK ($name) — $(length(csyms)) ABI functions exported, " * + "$(length(idr_rc)) result codes match") + return 0 +end + +root = length(ARGS) >= 1 ? ARGS[1] : "." +exit(main(root)) diff --git a/scripts/abi-ffi-gate.sh b/scripts/abi-ffi-gate.sh deleted file mode 100755 index 3258af3..0000000 --- a/scripts/abi-ffi-gate.sh +++ /dev/null @@ -1,113 +0,0 @@ -#!/usr/bin/env bash -# SPDX-License-Identifier: MPL-2.0 -# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) -# -# abi-ffi-gate.sh — fail (exit 1) if the Zig FFI does not conform to the Idris2 -# ABI. The Idris2 ABI is the source of truth. Bash port of the former -# abi-ffi-gate.py (Python is banned estate-wide). No toolchain needed — only -# coreutils + grep/awk/sed. Checks: -# -# 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: bash scripts/abi-ffi-gate.sh [repo_root] (defaults to cwd) -set -uo pipefail - -root="${1:-.}" -name="$(basename "$(cd "$root" 2>/dev/null && pwd || echo "$root")")" -abi_dir="$root/src/interface/abi" -zig_path="$root/src/interface/ffi/src/main.zig" - -# canon(name): camelCase -> snake_case, lowercase, err -> error -canon() { - printf '%s' "$1" \ - | sed -E 's/([a-zA-Z0-9])([A-Z])/\1_\2/g' \ - | tr '[:upper:]' '[:lower:]' \ - | sed -E 's/^err$/error/' -} - -idr_files="$(find "$abi_dir" -name '*.idr' -not -path '*/build/*' 2>/dev/null | sort)" -if [ -z "$idr_files" ]; then - echo "ABI-FFI GATE: SKIP ($name) — no Idris2 ABI .idr files under $abi_dir" - exit 0 -fi -if [ ! -f "$zig_path" ]; then - echo "ABI-FFI GATE: FAIL ($name) — no Zig FFI at $zig_path" - exit 1 -fi - -idr="$(cat $idr_files)" -zig="$(cat "$zig_path")" -errs="" - -# 1. unrendered template tokens -toks="$(printf '%s\n' "$zig" | grep -oE '\{\{[A-Za-z0-9_]+\}\}' | sort -u | tr '\n' ' ')" -if [ -n "${toks// /}" ]; then - errs="${errs} - Zig FFI has unrendered template tokens: ${toks} -" -fi - -# 2. foreign C symbols must be exported -csyms="$(printf '%s\n' "$idr" | grep -oE 'C:[A-Za-z0-9_]+' | sed 's/^C://' | sort -u | grep -v '^$')" -exports="$(printf '%s\n' "$zig" | grep -oE 'export fn [A-Za-z0-9_]+' | awk '{print $3}' | sort -u | grep -v '^$')" -missing="$(comm -23 <(printf '%s\n' "$csyms") <(printf '%s\n' "$exports") | tr '\n' ' ')" -ncsyms="$(printf '%s\n' "$csyms" | grep -vc '^$' || true)" -if [ -n "${missing// /}" ]; then - errs="${errs} - ABI function(s) not exported by the Zig FFI: ${missing} -" -fi - -# 3. result-code map (names + values) must agree -idr_rc="$(printf '%s\n' "$idr" \ - | grep -oE 'resultToInt +[A-Za-z0-9]+ *= *[0-9]+' \ - | sed -E 's/resultToInt +([A-Za-z0-9]+) *= *([0-9]+)/\1 \2/' \ - | while read -r nm val; do echo "$(canon "$nm") $val"; done | sort -u)" -nrc="$(printf '%s\n' "$idr_rc" | grep -vc '^$' || true)" - -# Parse each `enum (c_int) { ... }` block separately (variants up to the first -# `}`), tagged by a block id. Then in shell, canonicalise each block and pick -# the one whose `ok == 0` with the most variants — mirrors Python find_result_enum. -zig_raw="$(printf '%s\n' "$zig" | awk ' - /enum[ \t]*\([ \t]*c_int[ \t]*\)/ { cap=1; bid++ } - cap { - s=$0 - while (match(s, /@?"?[A-Za-z_][A-Za-z0-9_]*"?[ \t]*=[ \t]*[0-9]+/)) { - seg=substr(s, RSTART, RLENGTH); s=substr(s, RSTART+RLENGTH) - gsub(/[@"\t ]/,"",seg) - eq=index(seg,"="); k=substr(seg,1,eq-1); v=substr(seg,eq+1) - print bid, k, v - } - if ($0 ~ /\}/) cap=0 - } -')" - -zig_rc_final=""; best_n=-1 -for bid in $(printf '%s\n' "$zig_raw" | awk 'NF{print $1}' | sort -un); do - cb="$(printf '%s\n' "$zig_raw" | awk -v b="$bid" '$1==b{print $2" "$3}' \ - | while read -r nm val; do [ -n "$nm" ] && echo "$(canon "$nm") $val"; done | sort -u)" - if printf '%s\n' "$cb" | grep -qx 'ok 0'; then - cnt="$(printf '%s\n' "$cb" | grep -vc '^$')" - if [ "$cnt" -gt "$best_n" ]; then best_n="$cnt"; zig_rc_final="$cb"; fi - fi -done - -if [ "$nrc" -gt 0 ] && [ -z "$zig_rc_final" ]; then - errs="${errs} - no Zig enum(c_int) Result block (with ok = 0) found to compare result codes -" -elif [ "$nrc" -gt 0 ] && [ -n "$zig_rc_final" ] && [ "$idr_rc" != "$zig_rc_final" ]; then - errs="${errs} - Result-code map differs (name or value): - Idris resultToInt: $(printf '%s' "$idr_rc" | tr '\n' ',') - Zig Result enum: $(printf '%s' "$zig_rc_final" | tr '\n' ',') -" -fi - -if [ -n "$errs" ]; then - echo "ABI-FFI GATE: FAIL ($name)" - printf '%s' "$errs" - exit 1 -fi -echo "ABI-FFI GATE: OK ($name) — ${ncsyms} ABI functions exported, ${nrc} result codes match" -exit 0 From 796c024b037d778d31d0cc271ba8bbde7d9ba9ea Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 28 Jun 2026 08:41:49 +0000 Subject: [PATCH 6/6] =?UTF-8?q?style:=20cargo=20fmt=20+=20clippy=20--fix?= =?UTF-8?q?=20under=20stable=201.96=20(CI=20toolchain)=20=E2=80=94=20fmt?= =?UTF-8?q?=20--check=20+=20clippy=20-D=20warnings=20clean?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- src/codegen/header.rs | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/codegen/header.rs b/src/codegen/header.rs index 8f3b840..0ed2662 100644 --- a/src/codegen/header.rs +++ b/src/codegen/header.rs @@ -233,7 +233,10 @@ pub fn generate(manifest: &Manifest, output_dir: &Path) -> Result<()> { fn write_abi_header(output_dir: &Path, safe_name: &str, upper: &str) -> Result<()> { let mut h = String::with_capacity(2048); writeln!(h, "/* SPDX-License-Identifier: MPL-2.0 */")?; - writeln!(h, "/* Auto-generated by Chapeliser — do not edit manually. */")?; + writeln!( + h, + "/* Auto-generated by Chapeliser — do not edit manually. */" + )?; writeln!( h, "/* C-ABI prototypes for the c_* bridge the generated Chapel calls. */"