|
| 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 CAPSTONE: the end-to-end ABI SOUNDNESS CERTIFICATE for iseriser. |
| 5 | +||| |
| 6 | +||| This module proves NO new domain theorem. Its sole job is to ASSEMBLE the |
| 7 | +||| already-discharged proof layers into ONE inhabited value, so that the full |
| 8 | +||| ABI contract is shown to hold *together*. The certificate ties the chain: |
| 9 | +||| |
| 10 | +||| manifest/doctrine model (Types: Component, Scaffold, Result) |
| 11 | +||| -> Layer-2 flagship (Semantics.completeIsConformant — the canonical |
| 12 | +||| positive control: the complete five-component |
| 13 | +||| scaffold IS Conformant) |
| 14 | +||| -> Layer-3 invariant (Invariants.extendedGeneratedConformant — the |
| 15 | +||| upward-closure / monotonicity witness: a |
| 16 | +||| generated-then-extended scaffold stays Conformant) |
| 17 | +||| -> Layer-4 FFI seam (FfiSeam.resultToIntInjective — distinct ABI |
| 18 | +||| outcomes never collide on the C wire) |
| 19 | +||| |
| 20 | +||| into a single end-to-end soundness statement. `abiContractDischarged` is the |
| 21 | +||| capstone value: it is constructed ENTIRELY from the existing exported |
| 22 | +||| witnesses/theorems of the prior layers. If ANY prior layer were unsound, |
| 23 | +||| this value would not typecheck. There is no fresh proof obligation here — |
| 24 | +||| only genuine composition. |
| 25 | + |
| 26 | +module Iseriser.ABI.Capstone |
| 27 | + |
| 28 | +import Iseriser.ABI.Types |
| 29 | +import Iseriser.ABI.Semantics |
| 30 | +import Iseriser.ABI.Invariants |
| 31 | +import Iseriser.ABI.FfiSeam |
| 32 | + |
| 33 | +%default total |
| 34 | + |
| 35 | +-------------------------------------------------------------------------------- |
| 36 | +-- The capstone certificate |
| 37 | +-------------------------------------------------------------------------------- |
| 38 | + |
| 39 | +||| `ABISound` bundles the KEY proven facts of the iseriser ABI into one record. |
| 40 | +||| Each field is the TYPE of an already-proven theorem from a prior layer; the |
| 41 | +||| only way to inhabit the record is to supply those real witnesses. |
| 42 | +||| |
| 43 | +||| * `flagship` : the Layer-2 flagship property holds on the canonical |
| 44 | +||| positive-control instance (`Semantics.completeScaffold` is |
| 45 | +||| `Conformant`). |
| 46 | +||| * `invariant` : the Layer-3 deeper invariant holds — conformance is |
| 47 | +||| upward-closed under extension, witnessed on the generated |
| 48 | +||| scaffold extended by one component. |
| 49 | +||| * `ffiInjective` : the Layer-4 FFI-seam guarantee — `resultToInt` is |
| 50 | +||| injective, so distinct ABI outcomes never collide on the |
| 51 | +||| wire. Stored as the full injectivity statement. |
| 52 | +public export |
| 53 | +record ABISound where |
| 54 | + constructor MkABISound |
| 55 | + flagship : Conformant Semantics.completeScaffold |
| 56 | + invariant : Conformant (extend [Manifest] Invariants.generatedScaffold) |
| 57 | + ffiInjective : (a, b : Result) -> resultToInt a = resultToInt b -> a = b |
| 58 | + |
| 59 | +||| THE CAPSTONE. A single inhabited value assembled purely from the existing |
| 60 | +||| exported witnesses of Layers 2-4. Its mere existence certifies that the |
| 61 | +||| flagship property, the deeper invariant, and the FFI-seam injectivity are |
| 62 | +||| ALL simultaneously discharged for this ABI — manifest model -> ABI proofs |
| 63 | +||| -> FFI seam, sealed end to end. |
| 64 | +public export |
| 65 | +abiContractDischarged : ABISound |
| 66 | +abiContractDischarged = |
| 67 | + MkABISound |
| 68 | + completeIsConformant -- Layer-2 flagship positive control |
| 69 | + extendedGeneratedConformant -- Layer-3 upward-closure invariant witness |
| 70 | + resultToIntInjective -- Layer-4 FFI-seam injectivity |
0 commit comments