|
| 1 | +-- SPDX-License-Identifier: MPL-2.0 |
| 2 | +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <j.d.a.jewell@open.ac.uk> |
| 3 | +-- |
| 4 | +||| Layer 5 — the CAPSTONE ABI SOUNDNESS CERTIFICATE for halideiser. |
| 5 | +||| |
| 6 | +||| Every prior layer proves one slice of the ABI contract in isolation: |
| 7 | +||| |
| 8 | +||| * Layer 2 (`Halideiser.ABI.Semantics`) — the FLAGSHIP semantic property: |
| 9 | +||| a loop SPLIT schedule computes exactly what the flat run computes |
| 10 | +||| (`SplitEquivalent`), with the canonical positive control |
| 11 | +||| `doubleSplit3x4Equivalent`. |
| 12 | +||| * Layer 3 (`Halideiser.ABI.Invariants`) — the DEEPER invariant: schedule |
| 13 | +||| equivalence is a genuine equivalence relation, and TILING (split of an |
| 14 | +||| outer split) preserves the result by transitive composition, witnessed |
| 15 | +||| on the canonical positive control `doubleTile2x3x2Equivalent`. |
| 16 | +||| * Layer 4 (`Halideiser.ABI.FfiSeam`) — the FFI SEAM: the on-the-wire |
| 17 | +||| `resultToInt` encoding is INJECTIVE (`resultToIntInjective`), so the |
| 18 | +||| ABI's `Result` values never collide on their C integer codes. |
| 19 | +||| |
| 20 | +||| This module ties those three together into ONE inhabited value. The record |
| 21 | +||| `ABISound` has one field per layer, each typed as the EXACT proven fact |
| 22 | +||| exported by that layer. `abiContractDischarged : ABISound` is constructed |
| 23 | +||| solely from the existing exported witnesses/theorems — no new domain |
| 24 | +||| theorem is proved here. If ANY prior layer were unsound (its witness |
| 25 | +||| missing or its theorem ill-typed), this single value would fail to |
| 26 | +||| typecheck. Thus the capstone is an end-to-end statement: manifest -> ABI |
| 27 | +||| proofs (flagship semantic equivalence + deeper tiling invariant) -> FFI |
| 28 | +||| seam injectivity, all discharged simultaneously. |
| 29 | +||| |
| 30 | +||| Genuine composition only: no believe_me / idris_crash / assert_total / |
| 31 | +||| postulate / sorry / %hint hacks. Every field is a real exported value. |
| 32 | +module Halideiser.ABI.Capstone |
| 33 | + |
| 34 | +import Halideiser.ABI.Types |
| 35 | +import Halideiser.ABI.Semantics |
| 36 | +import Halideiser.ABI.Invariants |
| 37 | +import Halideiser.ABI.FfiSeam |
| 38 | + |
| 39 | +%default total |
| 40 | + |
| 41 | +-------------------------------------------------------------------------------- |
| 42 | +-- The capstone certificate |
| 43 | +-------------------------------------------------------------------------------- |
| 44 | + |
| 45 | +||| `ABISound` bundles the key proven facts of the halideiser ABI, one per |
| 46 | +||| layer. To inhabit it you must supply, simultaneously: |
| 47 | +||| |
| 48 | +||| * `flagship` — a Layer-2 `SplitEquivalent` witness on the canonical |
| 49 | +||| positive-control instance (the `double` stage, split 3x4). This is the |
| 50 | +||| exact type of `Semantics.doubleSplit3x4Equivalent`. |
| 51 | +||| |
| 52 | +||| * `invariant` — a Layer-3 `ScheduleEquiv` witness that the tiled run of |
| 53 | +||| the same stage equals the flat run. This is the exact type of |
| 54 | +||| `Invariants.doubleTile2x3x2Equivalent`. |
| 55 | +||| |
| 56 | +||| * `ffiInjective` — the Layer-4 seam theorem that `resultToInt` is |
| 57 | +||| injective, stored as the proven function value itself. This is the |
| 58 | +||| exact type of `FfiSeam.resultToIntInjective`. |
| 59 | +||| |
| 60 | +||| None of these can be faked: each field's type is precisely a prior layer's |
| 61 | +||| exported proof obligation. |
| 62 | +public export |
| 63 | +record ABISound where |
| 64 | + constructor MkABISound |
| 65 | + flagship : SplitEquivalent Semantics.double 3 4 |
| 66 | + invariant : ScheduleEquiv (runTile Semantics.double 2 3 2) |
| 67 | + (runFlat Semantics.double ((2 * 3) * 2)) |
| 68 | + ffiInjective : (a, b : Result) -> resultToInt a = resultToInt b -> a = b |
| 69 | + |
| 70 | +-------------------------------------------------------------------------------- |
| 71 | +-- The single inhabited capstone value |
| 72 | +-------------------------------------------------------------------------------- |
| 73 | + |
| 74 | +||| THE CAPSTONE. One inhabited certificate assembled entirely from the |
| 75 | +||| already-exported witnesses of Layers 2, 3 and 4. Its very existence is the |
| 76 | +||| end-to-end soundness statement: the full ABI contract — flagship semantic |
| 77 | +||| equivalence, deeper tiling invariant, and FFI-seam injectivity — is |
| 78 | +||| discharged together. If any prior layer regressed, this value would not |
| 79 | +||| typecheck. |
| 80 | +public export |
| 81 | +abiContractDischarged : ABISound |
| 82 | +abiContractDischarged = |
| 83 | + MkABISound |
| 84 | + doubleSplit3x4Equivalent -- Layer 2: flagship positive control |
| 85 | + doubleTile2x3x2Equivalent -- Layer 3: deeper tiling invariant |
| 86 | + resultToIntInjective -- Layer 4: FFI seam injectivity |
| 87 | + |
| 88 | +-------------------------------------------------------------------------------- |
| 89 | +-- Field projections (the certificate really exposes each proven fact) |
| 90 | +-------------------------------------------------------------------------------- |
| 91 | + |
| 92 | +||| Project the Layer-2 flagship witness out of the discharged certificate. |
| 93 | +public export |
| 94 | +capstoneFlagship : SplitEquivalent Semantics.double 3 4 |
| 95 | +capstoneFlagship = abiContractDischarged.flagship |
| 96 | + |
| 97 | +||| Project the Layer-3 invariant witness out of the discharged certificate. |
| 98 | +public export |
| 99 | +capstoneInvariant : ScheduleEquiv (runTile Semantics.double 2 3 2) |
| 100 | + (runFlat Semantics.double ((2 * 3) * 2)) |
| 101 | +capstoneInvariant = abiContractDischarged.invariant |
| 102 | + |
| 103 | +||| Use the certificate's FFI-seam field at a concrete pair: equal codes force |
| 104 | +||| equal results. Here the trivial `Refl` premise yields `Ok = Ok`, confirming |
| 105 | +||| the stored injectivity proof really reduces. |
| 106 | +public export |
| 107 | +capstoneFfiOkOk : Ok = Ok |
| 108 | +capstoneFfiOkOk = abiContractDischarged.ffiInjective Ok Ok Refl |
0 commit comments