|
| 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 Anvomidaviser. |
| 5 | +||| |
| 6 | +||| Every prior proof layer establishes one facet of the ABI contract: |
| 7 | +||| |
| 8 | +||| * Layer 2 (`Anvomidaviser.ABI.Semantics`) — the FLAGSHIP property: the ISU |
| 9 | +||| short-program element-count rule (`WellFormed`), with `goodWellFormed` |
| 10 | +||| witnessing it on the canonical positive-control program. |
| 11 | +||| * Layer 3 (`Anvomidaviser.ABI.Invariants`) — a DEEPER invariant: |
| 12 | +||| downward-closure of well-formedness under deletion, with |
| 13 | +||| `trimmedWellFormed` transporting the Layer-2 witness through the |
| 14 | +||| Layer-3 theorem on a concrete instance. |
| 15 | +||| * Layer 4 (`Anvomidaviser.ABI.FfiSeam`) — the ABI<->FFI seam: |
| 16 | +||| `resultToIntInjective` proves the result-code encoding never collides, |
| 17 | +||| so an FFI integer carries exactly one ABI meaning. |
| 18 | +||| |
| 19 | +||| This module ASSEMBLES those already-proven facts into a single record |
| 20 | +||| `ABISound` and inhabits it once as `abiContractDischarged`. That value ties |
| 21 | +||| the chain together: manifest (the ISU rules the user asked for) -> ABI proofs |
| 22 | +||| (flagship element-count + the deeper downward-closure invariant) -> FFI seam |
| 23 | +||| (injective wire encoding) into one end-to-end soundness statement. If ANY |
| 24 | +||| prior layer were unsound, `abiContractDischarged` would fail to typecheck — |
| 25 | +||| so a clean build of this module is the certificate. |
| 26 | +||| |
| 27 | +||| Genuine composition only: every field below is filled from a real exported |
| 28 | +||| witness of a prior module. No believe_me / idris_crash / assert_total / |
| 29 | +||| postulate / sorry / %hint appears anywhere. |
| 30 | + |
| 31 | +module Anvomidaviser.ABI.Capstone |
| 32 | + |
| 33 | +import Anvomidaviser.ABI.Types |
| 34 | +import Anvomidaviser.ABI.Semantics |
| 35 | +import Anvomidaviser.ABI.Invariants |
| 36 | +import Anvomidaviser.ABI.FfiSeam |
| 37 | + |
| 38 | +%default total |
| 39 | + |
| 40 | +-------------------------------------------------------------------------------- |
| 41 | +-- The capstone certificate type |
| 42 | +-------------------------------------------------------------------------------- |
| 43 | + |
| 44 | +||| `ABISound` bundles the key proven facts of the Anvomidaviser ABI. Inhabiting |
| 45 | +||| it requires a real proof of each layer simultaneously. |
| 46 | +public export |
| 47 | +record ABISound where |
| 48 | + constructor MkABISound |
| 49 | + ||| Layer 2 — flagship property holds on the canonical positive control. |
| 50 | + flagship : WellFormed Semantics.goodProgram |
| 51 | + ||| Layer 3 — the deeper downward-closure invariant holds on a concrete |
| 52 | + ||| transformed instance (Layer-2 witness transported through Layer-3). |
| 53 | + invariant : WellFormed Invariants.trimmedProgram |
| 54 | + ||| Layer 4 — the FFI result-code encoding is injective (the seam is sealed). |
| 55 | + ffiSeam : (a : Result) -> (b : Result) -> resultToInt a = resultToInt b -> a = b |
| 56 | + |
| 57 | +-------------------------------------------------------------------------------- |
| 58 | +-- The capstone value: the contract, discharged |
| 59 | +-------------------------------------------------------------------------------- |
| 60 | + |
| 61 | +||| The single inhabited capstone. Each field is supplied by the genuine |
| 62 | +||| exported witness/theorem of the corresponding layer; nothing is fabricated. |
| 63 | +||| A successful typecheck of this value is the end-to-end ABI soundness proof. |
| 64 | +export |
| 65 | +abiContractDischarged : ABISound |
| 66 | +abiContractDischarged = MkABISound |
| 67 | + goodWellFormed -- Layer 2 (Semantics) |
| 68 | + trimmedWellFormed -- Layer 3 (Invariants) |
| 69 | + resultToIntInjective -- Layer 4 (FfiSeam) |
| 70 | + |
| 71 | +-------------------------------------------------------------------------------- |
| 72 | +-- Projections (each layer recoverable from the one certificate) |
| 73 | +-------------------------------------------------------------------------------- |
| 74 | + |
| 75 | +||| The flagship Layer-2 fact, recovered from the capstone. |
| 76 | +export |
| 77 | +capstoneFlagship : WellFormed Semantics.goodProgram |
| 78 | +capstoneFlagship = abiContractDischarged.flagship |
| 79 | + |
| 80 | +||| The Layer-3 invariant, recovered from the capstone. |
| 81 | +export |
| 82 | +capstoneInvariant : WellFormed Invariants.trimmedProgram |
| 83 | +capstoneInvariant = abiContractDischarged.invariant |
| 84 | + |
| 85 | +||| The Layer-4 seam injectivity, recovered from the capstone, applied here to |
| 86 | +||| a concrete pair to show it really reduces (non-vacuity at use site). |
| 87 | +export |
| 88 | +capstoneSeamOkOk : the Result Ok = the Result Ok |
| 89 | +capstoneSeamOkOk = abiContractDischarged.ffiSeam Ok Ok Refl |
0 commit comments