|
| 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 — END-TO-END ABI SOUNDNESS CERTIFICATE for Affinescriptiser. |
| 5 | +||| |
| 6 | +||| This capstone does NOT prove a new domain theorem. It ASSEMBLES the proofs |
| 7 | +||| already discharged in the lower layers into ONE inhabited record value. The |
| 8 | +||| certificate ties the whole ABI contract together: |
| 9 | +||| |
| 10 | +||| manifest (the affine-usage model: `Trace` / `AffineOk`) |
| 11 | +||| -> Layer 2 FLAGSHIP property : a single program fragment uses every |
| 12 | +||| variable at most once (`AffineOk`, witnessed on the canonical |
| 13 | +||| positive-control instance `safeTraceAffineOk : AffineOk [0,1,2]`). |
| 14 | +||| -> Layer 3 INVARIANT : the composition law — sequencing two affine, |
| 15 | +||| variable-disjoint fragments stays affine (`concatAffine`, witnessed |
| 16 | +||| on the canonical positive control `composedOk : AffineOk [0,1,2,3]`). |
| 17 | +||| -> Layer 4 FFI SEAM : the ABI<->C `Result` encoding is unambiguous, so |
| 18 | +||| distinct ABI outcomes never collide on the wire |
| 19 | +||| (`resultToIntInjective`). |
| 20 | +||| |
| 21 | +||| Each field below is filled ONLY from an already-`export`ed witness/theorem of |
| 22 | +||| the modules it imports — nothing is re-proved or fabricated here. The single |
| 23 | +||| value `abiContractDischarged : ABISound` is therefore the capstone: if ANY |
| 24 | +||| prior layer were unsound (the flagship witness, the invariant witness, or the |
| 25 | +||| seam injectivity), this value would fail to typecheck and the certificate |
| 26 | +||| could not be issued. Genuine composition only: no believe_me, no idris_crash, |
| 27 | +||| no assert_total, no postulate, no sorry, no %hint hacks, no asserted equality. |
| 28 | + |
| 29 | +module Affinescriptiser.ABI.Capstone |
| 30 | + |
| 31 | +import Affinescriptiser.ABI.Types |
| 32 | +import Affinescriptiser.ABI.Semantics |
| 33 | +import Affinescriptiser.ABI.Invariants |
| 34 | +import Affinescriptiser.ABI.FfiSeam |
| 35 | + |
| 36 | +%default total |
| 37 | + |
| 38 | +-------------------------------------------------------------------------------- |
| 39 | +-- The certificate type |
| 40 | +-------------------------------------------------------------------------------- |
| 41 | + |
| 42 | +||| `ABISound` records the KEY proven facts of the Affinescriptiser ABI, one |
| 43 | +||| field per proof layer. Inhabiting it requires a genuine witness of each. |
| 44 | +public export |
| 45 | +record ABISound where |
| 46 | + constructor MkABISound |
| 47 | + ||| Layer 2 (flagship): the canonical positive-control program fragment |
| 48 | + ||| [0,1,2] is affine-safe — every variable used at most once. |
| 49 | + flagship : AffineOk [0, 1, 2] |
| 50 | + ||| Layer 3 (invariant): the composition law applied to the canonical |
| 51 | + ||| disjoint fragments yields an affine-safe sequenced fragment [0,1,2,3]. |
| 52 | + invariant : AffineOk ([0, 1] ++ [2, 3]) |
| 53 | + ||| Layer 4 (FFI seam): the ABI<->C `Result` encoding is injective, i.e. |
| 54 | + ||| equal wire integers imply equal ABI outcomes (distinct outcomes never |
| 55 | + ||| collide). Carried as the full injectivity theorem. |
| 56 | + seamInjective : (a, b : Result) -> resultToInt a = resultToInt b -> a = b |
| 57 | + |
| 58 | +-------------------------------------------------------------------------------- |
| 59 | +-- The capstone value: the whole ABI contract, discharged together |
| 60 | +-------------------------------------------------------------------------------- |
| 61 | + |
| 62 | +||| THE CAPSTONE. A single inhabited certificate built entirely from the |
| 63 | +||| lower-layer exported witnesses: |
| 64 | +||| * `flagship` = `safeTraceAffineOk` (Layer 2 positive control) |
| 65 | +||| * `invariant` = `composedOk` (Layer 3 composition control) |
| 66 | +||| * `seamInjective` = `resultToIntInjective` (Layer 4 seam theorem) |
| 67 | +||| Typechecking this value is exactly the end-to-end soundness statement. |
| 68 | +public export |
| 69 | +abiContractDischarged : ABISound |
| 70 | +abiContractDischarged = |
| 71 | + MkABISound safeTraceAffineOk composedOk resultToIntInjective |
0 commit comments