|
| 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 — the end-to-end ABI SOUNDNESS CERTIFICATE. |
| 5 | +||| |
| 6 | +||| Each prior layer discharged one part of the Idrisiser ABI contract in |
| 7 | +||| isolation: |
| 8 | +||| |
| 9 | +||| * Layer 2 (`Idrisiser.ABI.Semantics`) — the FLAGSHIP property: a generated |
| 10 | +||| bounded-array accessor is in-bounds-total, out-of-range access being |
| 11 | +||| unrepresentable. Its canonical positive control is `idx2InBounds`, an |
| 12 | +||| inhabited `InBounds 2 3` witness. |
| 13 | +||| * Layer 3 (`Idrisiser.ABI.Invariants`) — the DEEPER store/select invariant |
| 14 | +||| relating a generated WRITE to a subsequent READ. Its concrete positive |
| 15 | +||| control is `writeThenReadDelta`: writing "delta" into slot 1 and reading |
| 16 | +||| slot 1 back returns "delta". |
| 17 | +||| * Layer 4 (`Idrisiser.ABI.FfiSeam`) — sealing the ABI<->FFI seam: the wire |
| 18 | +||| encoding `resultToInt` is injective, so distinct ABI outcomes never |
| 19 | +||| collide as they cross into Zig/C. The proof is `resultToIntInjective`. |
| 20 | +||| |
| 21 | +||| This capstone ties those three together into ONE inhabited value. The record |
| 22 | +||| `ABISound` has one field per layer, each field's TYPE being the precise |
| 23 | +||| proven fact of that layer; the single value `abiContractDischarged` fills |
| 24 | +||| every field with the REAL exported witness/theorem from the layer above. |
| 25 | +||| Because the record is constructed only from genuine proofs, the existence of |
| 26 | +||| `abiContractDischarged` is a machine-checked statement that the full ABI |
| 27 | +||| contract — manifest -> ABI proofs (flagship + invariant) -> FFI seam — is |
| 28 | +||| discharged together: if any prior layer were unsound, no field could be |
| 29 | +||| filled and this value would not typecheck. |
| 30 | +||| |
| 31 | +||| Non-vacuity is enforced by the adversarial control (see /tmp/Adv*.idr in the |
| 32 | +||| build procedure): a bogus certificate — e.g. claiming the flagship control is |
| 33 | +||| `InBounds 5 3`, or that the write-then-read returns "beta" — is REJECTED by |
| 34 | +||| the type checker, so `ABISound` cannot be inhabited by a false component. |
| 35 | + |
| 36 | +module Idrisiser.ABI.Capstone |
| 37 | + |
| 38 | +import Idrisiser.ABI.Types |
| 39 | +import Idrisiser.ABI.Semantics |
| 40 | +import Idrisiser.ABI.Invariants |
| 41 | +import Idrisiser.ABI.FfiSeam |
| 42 | +import Data.Fin |
| 43 | + |
| 44 | +%default total |
| 45 | + |
| 46 | +-------------------------------------------------------------------------------- |
| 47 | +-- The certificate record: one field per discharged ABI layer |
| 48 | +-------------------------------------------------------------------------------- |
| 49 | + |
| 50 | +||| An end-to-end soundness certificate for the Idrisiser ABI. Each field's |
| 51 | +||| type is the exact proven fact of one prior layer, so the record is |
| 52 | +||| inhabitable ONLY when all three layers are genuinely sound. |
| 53 | +public export |
| 54 | +record ABISound where |
| 55 | + constructor MkABISound |
| 56 | + ||| Layer 2 (flagship): the canonical positive control — raw index 2 is in |
| 57 | + ||| bounds of a 3-element array (an inhabited `InBounds 2 3`). |
| 58 | + flagshipControl : InBounds 2 3 |
| 59 | + ||| Layer 3 (deeper invariant): the concrete write-then-read law instance — |
| 60 | + ||| writing "delta" into slot 1 of the control array and reading slot 1 back |
| 61 | + ||| returns exactly "delta". |
| 62 | + layer3Invariant : safeIndex (safeWrite Invariants.ctrlArray 1 "delta") 1 = "delta" |
| 63 | + ||| Layer 4 (FFI seam): the wire encoding is injective — distinct ABI outcomes |
| 64 | + ||| never collide as they cross to Zig/C. |
| 65 | + ffiSeamInjective : (a, b : Result) -> resultToInt a = resultToInt b -> a = b |
| 66 | + |
| 67 | +-------------------------------------------------------------------------------- |
| 68 | +-- The capstone value: assembled from the real exported witnesses |
| 69 | +-------------------------------------------------------------------------------- |
| 70 | + |
| 71 | +||| THE CAPSTONE. A single inhabited `ABISound`, each field supplied by the |
| 72 | +||| genuine exported proof of the corresponding layer: |
| 73 | +||| |
| 74 | +||| * `flagshipControl` = `Semantics.idx2InBounds` (Layer 2) |
| 75 | +||| * `layer3Invariant` = `Invariants.writeThenReadDelta` (Layer 3) |
| 76 | +||| * `ffiSeamInjective` = `FfiSeam.resultToIntInjective` (Layer 4) |
| 77 | +||| |
| 78 | +||| Nothing is fabricated; every field is a name that already typechecked in its |
| 79 | +||| home module. This value's existence is the end-to-end soundness statement. |
| 80 | +public export |
| 81 | +abiContractDischarged : ABISound |
| 82 | +abiContractDischarged = |
| 83 | + MkABISound |
| 84 | + Semantics.idx2InBounds |
| 85 | + writeThenReadDelta |
| 86 | + resultToIntInjective |
0 commit comments