|
| 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 Betlangiser. |
| 5 | +||| |
| 6 | +||| Every prior layer proved one slice of the ABI contract in isolation: |
| 7 | +||| |
| 8 | +||| * Layer 2 (`Betlangiser.ABI.Semantics`) — the flagship semantic property: |
| 9 | +||| the Kleene substrate's `and3` preserves classical truth (`Designated`), |
| 10 | +||| witnessed on the canonical positive control `andTTDesignated`. |
| 11 | +||| * Layer 3 (`Betlangiser.ABI.Invariants`) — the deeper structural invariant: |
| 12 | +||| `and3` is the meet (greatest lower bound) of the Kleene information |
| 13 | +||| order, witnessed on the positive control `meetTU_belowU`. |
| 14 | +||| * Layer 4 (`Betlangiser.ABI.FfiSeam`) — the ABI<->FFI seam soundness: |
| 15 | +||| `resultToIntInjective`, distinct ABI outcomes never collide on the wire. |
| 16 | +||| |
| 17 | +||| This module ties them together into ONE inhabited value. The record |
| 18 | +||| `ABISound` bundles the three key proven facts as fields; the single value |
| 19 | +||| `abiContractDischarged` constructs it from the *actual exported witnesses* |
| 20 | +||| of those three modules. Because the record's field types name the genuine |
| 21 | +||| theorems, `abiContractDischarged` only typechecks if all three prior layers |
| 22 | +||| are themselves sound: the manifest's promised behaviour (ternary semantics) |
| 23 | +||| flows through the ABI proofs (flagship + invariant) and across the FFI seam |
| 24 | +||| (injective encoding) as a single, machine-checked end-to-end statement. |
| 25 | +||| |
| 26 | +||| No `believe_me`, `idris_crash`, `assert_total`, `postulate`, or `sorry`: |
| 27 | +||| this is genuine composition of already-proven facts only. |
| 28 | + |
| 29 | +module Betlangiser.ABI.Capstone |
| 30 | + |
| 31 | +import Betlangiser.ABI.Types |
| 32 | +import Betlangiser.ABI.Semantics |
| 33 | +import Betlangiser.ABI.Invariants |
| 34 | +import Betlangiser.ABI.FfiSeam |
| 35 | + |
| 36 | +%default total |
| 37 | + |
| 38 | +-------------------------------------------------------------------------------- |
| 39 | +-- The capstone certificate |
| 40 | +-------------------------------------------------------------------------------- |
| 41 | + |
| 42 | +||| `ABISound` is the end-to-end soundness certificate. Each field is a key |
| 43 | +||| proven fact of the Betlangiser ABI; an inhabitant exists only if every |
| 44 | +||| layer it references is sound. |
| 45 | +public export |
| 46 | +record ABISound where |
| 47 | + constructor MkABISound |
| 48 | + ||| Layer 2 flagship: `and3` preserves classical truth on the canonical |
| 49 | + ||| positive control `T and3 T`. (Reuses `Semantics.andTTDesignated`.) |
| 50 | + flagshipDesignated : Designated (and3 T T) |
| 51 | + ||| Layer 3 invariant: the meet of `T` and `U` is below `U` in the Kleene |
| 52 | + ||| order — `and3` is the genuine GLB. (Reuses `Invariants.meetTU_belowU`.) |
| 53 | + meetInvariant : Leq3 (and3 T U) U |
| 54 | + ||| Layer 4 FFI seam: the C-integer encoding of `Result` is injective, so |
| 55 | + ||| distinct ABI outcomes never collide on the wire. (Reuses |
| 56 | + ||| `FfiSeam.resultToIntInjective`.) |
| 57 | + seamInjective : (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/theorems of Layers 2, 3 and 4. If any of those layers |
| 61 | +||| were unsound, this value would fail to typecheck — so its mere existence |
| 62 | +||| certifies the whole ABI contract is discharged together. |
| 63 | +public export |
| 64 | +abiContractDischarged : ABISound |
| 65 | +abiContractDischarged = MkABISound andTTDesignated meetTU_belowU resultToIntInjective |
0 commit comments