|
| 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 for a2mliser: a single end-to-end ABI SOUNDNESS |
| 5 | +||| CERTIFICATE that ties the whole stack together into one inhabited value. |
| 6 | +||| |
| 7 | +||| This certificate ties the chain together: |
| 8 | +||| manifest -> ABI proofs (flagship + invariant) -> FFI seam |
| 9 | +||| into a single end-to-end soundness statement. It assembles, in one record, |
| 10 | +||| the KEY proven facts already discharged by the prior layers: |
| 11 | +||| |
| 12 | +||| * flagship (Layer 2) — `Semantics.goodVerifies` : the canonical |
| 13 | +||| positive-control attestation really `Verifies` the document |
| 14 | +||| it was issued over (attestation-binding soundness). |
| 15 | +||| * roundTrip (Layer 3) — `Invariants.goodRoundTrips` : the ABI certifier |
| 16 | +||| returns `Ok` for that honest attestation (issue->verify |
| 17 | +||| round-trip / process correctness over the SAME control). |
| 18 | +||| * seamInj (Layer 4) — `FfiSeam.resultToIntInjective` : the ABI->C |
| 19 | +||| result-code encoder is injective, so distinct ABI outcomes |
| 20 | +||| never collide on the wire (FFI-seam soundness). |
| 21 | +||| |
| 22 | +||| The single inhabited value `abiContractDischarged` is constructed ENTIRELY |
| 23 | +||| from those existing exported witnesses. It is the capstone: if any prior |
| 24 | +||| layer were unsound, this value would not typecheck. Genuine composition — |
| 25 | +||| no `believe_me`, `postulate`, `assert_total`, `idris_crash`, or fabricated |
| 26 | +||| witnesses anywhere. |
| 27 | + |
| 28 | +module A2mliser.ABI.Capstone |
| 29 | + |
| 30 | +import A2mliser.ABI.Types |
| 31 | +import A2mliser.ABI.Semantics |
| 32 | +import A2mliser.ABI.Invariants |
| 33 | +import A2mliser.ABI.FfiSeam |
| 34 | + |
| 35 | +%default total |
| 36 | + |
| 37 | +-------------------------------------------------------------------------------- |
| 38 | +-- The capstone certificate type |
| 39 | +-------------------------------------------------------------------------------- |
| 40 | + |
| 41 | +||| `ABISound` collects, as fields, the load-bearing proven facts of the a2mliser |
| 42 | +||| ABI contract. Each field's TYPE is the proposition a prior layer discharged; |
| 43 | +||| inhabiting the record therefore demands a real proof of every one at once. |
| 44 | +public export |
| 45 | +record ABISound where |
| 46 | + constructor MkABISound |
| 47 | + ||| Layer 2 (flagship): the canonical positive-control attestation verifies |
| 48 | + ||| the exact document it was issued over. |
| 49 | + flagship : Verifies Semantics.goodAtt Semantics.goodDoc |
| 50 | + ||| Layer 3 (invariant): the ABI certifier round-trips that honest attestation |
| 51 | + ||| to an `Ok` result code through the real `certify`/`decVerifies` pipeline. |
| 52 | + roundTrip : certify Semantics.goodAtt Semantics.goodDoc = Ok |
| 53 | + ||| Layer 4 (FFI seam): the ABI->C result-code encoder is injective, so |
| 54 | + ||| distinct ABI outcomes never collide on the wire. |
| 55 | + seamInj : (a, b : AttestationResult) -> resultToInt a = resultToInt b -> a = b |
| 56 | + |
| 57 | +-------------------------------------------------------------------------------- |
| 58 | +-- The capstone value: the full ABI contract, discharged together |
| 59 | +-------------------------------------------------------------------------------- |
| 60 | + |
| 61 | +||| THE CAPSTONE. One inhabited value assembled solely from prior-layer exports. |
| 62 | +||| Its existence is the end-to-end soundness certificate for the a2mliser ABI: |
| 63 | +||| flagship binding soundness, the issue->verify round-trip, and FFI-seam |
| 64 | +||| injectivity all hold simultaneously over the canonical control. |
| 65 | +public export |
| 66 | +abiContractDischarged : ABISound |
| 67 | +abiContractDischarged = |
| 68 | + MkABISound |
| 69 | + Semantics.goodVerifies -- Layer 2 flagship positive control |
| 70 | + Invariants.goodRoundTrips -- Layer 3 round-trip invariant |
| 71 | + resultToIntInjective -- Layer 4 FFI-seam injectivity |
0 commit comments