|
| 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 ABI SOUNDNESS CERTIFICATE for Nimiser. |
| 5 | +||| |
| 6 | +||| This capstone proves nothing new. Instead it ASSEMBLES the four prior |
| 7 | +||| proof layers of the Nimiser ABI into a single inhabited value, so that |
| 8 | +||| "the whole ABI contract is discharged" becomes one typechecked fact: |
| 9 | +||| |
| 10 | +||| * Layer 2 (flagship semantics) — `Semantics.samplePreserved`, the |
| 11 | +||| positive-control witness that the code generator's output for the |
| 12 | +||| canonical `proc add(a,b: int): int` provably PRESERVES the source |
| 13 | +||| signature (arity + per-argument/return Nim->C lowering). |
| 14 | +||| * Layer 3 (deeper invariant) — `Invariants.composedArgsWitness`, a |
| 15 | +||| concrete `ArgsLower` witness BUILT by composing two sub-witnesses |
| 16 | +||| through the distributivity/composition lemma (`argsLowerAppend`), |
| 17 | +||| i.e. the generator is a monoid homomorphism on argument lists. |
| 18 | +||| * Layer 3 (whole-signature injectivity) — `Invariants.genBindingInjective`, |
| 19 | +||| the theorem that distinct Nim signatures lower to distinct C bindings |
| 20 | +||| (no codegen-introduced symbol/ABI aliasing). |
| 21 | +||| * Layer 4 (FFI seam) — `FfiSeam.resultToIntInjective`, soundness of the |
| 22 | +||| ABI<->C `Result` encoding: distinct ABI outcomes never collide on the |
| 23 | +||| wire. |
| 24 | +||| |
| 25 | +||| The certificate threads the chain manifest -> ABI proofs (flagship + |
| 26 | +||| invariant) -> FFI seam into one end-to-end soundness statement. The single |
| 27 | +||| inhabited value `abiContractDischarged` cannot be constructed unless EVERY |
| 28 | +||| referenced witness/theorem from the prior layers still typechecks; if any |
| 29 | +||| earlier layer regressed into unsoundness, this module would fail to build. |
| 30 | +||| That is the point of a capstone: one value that stands or falls with the |
| 31 | +||| entire stack. |
| 32 | + |
| 33 | +module Nimiser.ABI.Capstone |
| 34 | + |
| 35 | +import Nimiser.ABI.Types |
| 36 | +import Nimiser.ABI.Semantics |
| 37 | +import Nimiser.ABI.Invariants |
| 38 | +import Nimiser.ABI.FfiSeam |
| 39 | + |
| 40 | +%default total |
| 41 | + |
| 42 | +-------------------------------------------------------------------------------- |
| 43 | +-- The certificate record |
| 44 | +-------------------------------------------------------------------------------- |
| 45 | + |
| 46 | +||| `ABISound` bundles the key proven facts of the Nimiser ABI. Each field is a |
| 47 | +||| genuine proof object reused verbatim from the layer that established it — no |
| 48 | +||| field is re-proved here, and none can be faked. An inhabitant of this record |
| 49 | +||| is exactly a certificate that all four layers hold simultaneously. |
| 50 | +public export |
| 51 | +record ABISound where |
| 52 | + constructor MkABISound |
| 53 | + ||| Layer 2 (flagship): the generated C binding for the canonical sample |
| 54 | + ||| signature provably preserves it (name + arity + per-type lowering). |
| 55 | + flagshipPreserved : |
| 56 | + SigPreserved Semantics.sampleNimSig Semantics.sampleCSig |
| 57 | + ||| Layer 3 (composition invariant): a concrete composed `ArgsLower` witness |
| 58 | + ||| for an extended argument list, demonstrating lowering is a homomorphism |
| 59 | + ||| over list concatenation. |
| 60 | + invariantComposed : |
| 61 | + ArgsLower (Invariants.baseSig.sigArgs ++ Invariants.extraArgs) |
| 62 | + [CIntT, CDoubleT, CCharStarT] |
| 63 | + ||| Layer 3 (whole-signature injectivity): distinct Nim signatures lower to |
| 64 | + ||| distinct C bindings — the generator introduces no ABI aliasing. |
| 65 | + bindingInjective : |
| 66 | + (s1, s2 : NimSig) -> genBinding s1 = genBinding s2 -> s1 = s2 |
| 67 | + ||| Layer 4 (FFI seam): the ABI<->C `Result` encoding is injective, so |
| 68 | + ||| distinct ABI outcomes never collide on the wire. |
| 69 | + ffiSeamInjective : |
| 70 | + (a, b : Result) -> resultToInt a = resultToInt b -> a = b |
| 71 | + |
| 72 | +-------------------------------------------------------------------------------- |
| 73 | +-- The capstone value |
| 74 | +-------------------------------------------------------------------------------- |
| 75 | + |
| 76 | +||| THE CAPSTONE. A single inhabited `ABISound`, constructed entirely from the |
| 77 | +||| existing exported witnesses/theorems of Layers 2-4. This value is the |
| 78 | +||| end-to-end ABI soundness certificate for Nimiser: it typechecks iff the |
| 79 | +||| flagship semantic property, the deeper composition invariant, whole-signature |
| 80 | +||| injectivity, and the FFI-seam encoding soundness are ALL discharged together. |
| 81 | +public export |
| 82 | +abiContractDischarged : ABISound |
| 83 | +abiContractDischarged = |
| 84 | + MkABISound |
| 85 | + Semantics.samplePreserved |
| 86 | + Invariants.composedArgsWitness |
| 87 | + Invariants.genBindingInjective |
| 88 | + FfiSeam.resultToIntInjective |
0 commit comments