|
| 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 Oblibeniser. |
| 5 | +||| |
| 6 | +||| This module proves no new domain theorem. It ASSEMBLES the already-proven |
| 7 | +||| facts of every prior layer into a single inhabited record value. The point |
| 8 | +||| is composition: `abiContractDischarged` only typechecks if every layer it |
| 9 | +||| draws on is genuinely sound. If any underlying proof were vacuous or broken, |
| 10 | +||| this capstone value would fail to elaborate. |
| 11 | +||| |
| 12 | +||| It ties together the full ABI contract: |
| 13 | +||| |
| 14 | +||| manifest (Result codes, Op family in Types) |
| 15 | +||| -> Layer-2 flagship : reversibility round-trip (Semantics.certify / |
| 16 | +||| Semantics.reversible, packaged as `IsReversible`) |
| 17 | +||| -> Layer-3 invariant : the operations form a GROUP under sequencing, |
| 18 | +||| with a genuine two-sided inverse |
| 19 | +||| (Invariants.groupInverse, `IsGroupInverse`) |
| 20 | +||| -> Layer-4 FFI seam : the wire encoding is injective, so distinct ABI |
| 21 | +||| outcomes never collide on the C boundary |
| 22 | +||| (FfiSeam.resultToIntInjective) |
| 23 | +||| |
| 24 | +||| into ONE end-to-end soundness statement. The non-vacuity control at the |
| 25 | +||| bottom (`okErrorWireDistinct`) re-derives, through the very injectivity field |
| 26 | +||| stored in the certificate, that `Ok` and `Error` cannot share a wire code — |
| 27 | +||| so the FFI field is a real injection, not a constant. The adversarial harness |
| 28 | +||| (checked out of tree) confirms a bogus certificate cannot be constructed. |
| 29 | + |
| 30 | +module Oblibeniser.ABI.Capstone |
| 31 | + |
| 32 | +import Oblibeniser.ABI.Types |
| 33 | +import Oblibeniser.ABI.Semantics |
| 34 | +import Oblibeniser.ABI.Invariants |
| 35 | +import Oblibeniser.ABI.FfiSeam |
| 36 | + |
| 37 | +%default total |
| 38 | + |
| 39 | +-------------------------------------------------------------------------------- |
| 40 | +-- The canonical positive-control instance |
| 41 | +-------------------------------------------------------------------------------- |
| 42 | + |
| 43 | +||| The canonical operation the capstone certifies, built from the exported |
| 44 | +||| public `Op` constructors of the Layer-2 model: flip every bit, XOR a fixed |
| 45 | +||| mask, then reverse. This is a faithful reconstruction of the flagship |
| 46 | +||| positive control (the module-private `Semantics.sample` is not exported, so |
| 47 | +||| we rebuild the same shape here from public constructors rather than fake a |
| 48 | +||| reference to a private name). |
| 49 | +public export |
| 50 | +canonOp : Op |
| 51 | +canonOp = Seq FlipAll (Seq (XorMask [True, False, True]) Rev) |
| 52 | + |
| 53 | +-------------------------------------------------------------------------------- |
| 54 | +-- The certificate record |
| 55 | +-------------------------------------------------------------------------------- |
| 56 | + |
| 57 | +||| One bundled certificate that the whole ABI contract is discharged together. |
| 58 | +||| Each field is a real proven fact reused from a prior layer; there is no |
| 59 | +||| constructor that lets any field be skipped or forged. |
| 60 | +public export |
| 61 | +record ABISound where |
| 62 | + constructor MkABISound |
| 63 | + ||| Layer-2 flagship: the canonical operation is reversible (round-trip law), |
| 64 | + ||| as an `IsReversible` certificate built only via the exported `certify`. |
| 65 | + flagshipReversible : IsReversible Capstone.canonOp |
| 66 | + ||| Layer-3 invariant: the canonical operation and its inverse satisfy the |
| 67 | + ||| two-sided group-inverse axioms (deeper than the bare round-trip). |
| 68 | + groupStructured : IsGroupInverse Capstone.canonOp (invert Capstone.canonOp) |
| 69 | + ||| Layer-4 FFI seam: the wire encoding `resultToInt` is injective, so |
| 70 | + ||| distinct ABI Result codes never collide on the C boundary. |
| 71 | + ffiSeamInjective : (a, b : Result) -> resultToInt a = resultToInt b -> a = b |
| 72 | + |
| 73 | +-------------------------------------------------------------------------------- |
| 74 | +-- THE CAPSTONE VALUE: every layer discharged at once |
| 75 | +-------------------------------------------------------------------------------- |
| 76 | + |
| 77 | +||| The capstone. Constructed entirely from prior-layer exported theorems: |
| 78 | +||| * `certify` (Oblibeniser.ABI.Semantics) |
| 79 | +||| * `groupInverse` (Oblibeniser.ABI.Invariants) |
| 80 | +||| * `resultToIntInjective` (Oblibeniser.ABI.FfiSeam) |
| 81 | +||| If any of those proofs were unsound, this definition would not typecheck. |
| 82 | +public export |
| 83 | +abiContractDischarged : ABISound |
| 84 | +abiContractDischarged = |
| 85 | + MkABISound |
| 86 | + (certify canonOp) |
| 87 | + (groupInverse canonOp) |
| 88 | + resultToIntInjective |
| 89 | + |
| 90 | +-------------------------------------------------------------------------------- |
| 91 | +-- Non-vacuity control (the FFI field is a real injection, used live) |
| 92 | +-------------------------------------------------------------------------------- |
| 93 | + |
| 94 | +||| Re-derive, THROUGH the certificate's own injectivity field, that `Ok` and |
| 95 | +||| `Error` cannot share a wire code. If `resultToInt Ok = resultToInt Error`, |
| 96 | +||| injectivity would force `Ok = Error`, which is structurally impossible. This |
| 97 | +||| proves the stored injectivity is genuine (not a constant collapse), so the |
| 98 | +||| certificate is non-vacuous. |
| 99 | +export |
| 100 | +okErrorWireDistinct : Not (resultToInt Ok = resultToInt Error) |
| 101 | +okErrorWireDistinct eq = |
| 102 | + case abiContractDischarged.ffiSeamInjective Ok Error eq of |
| 103 | + Refl impossible |
0 commit comments