|
| 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 — END-TO-END ABI SOUNDNESS CERTIFICATE for Lustreiser. |
| 5 | +||| |
| 6 | +||| This module proves NO new domain theorem. It is the CAPSTONE: it |
| 7 | +||| ASSEMBLES the already-proven facts from every prior ABI layer into a |
| 8 | +||| single inhabited certificate value. The certificate ties the whole |
| 9 | +||| chain together — |
| 10 | +||| |
| 11 | +||| manifest (lustreiser.toml describes the node) |
| 12 | +||| -> ABI proofs: |
| 13 | +||| * Layer 2 (Semantics): the flagship per-tick / whole-run |
| 14 | +||| SAFETY BOUND — the saturating counter never exceeds its cap |
| 15 | +||| (reusing the exported positive control `safeWatchdogWithinBound` |
| 16 | +||| and the whole-run control `safeRunWithinBound`); |
| 17 | +||| * Layer 3 (Invariants): the deeper ALGEBRAIC invariant — `run` |
| 18 | +||| is a left monoid action of the input stream on node state |
| 19 | +||| (reusing the exported concrete witness `appendWitness` of the |
| 20 | +||| flagship `runAppend` law, and the `monotoneWitness` of |
| 21 | +||| `satInc` monotonicity); |
| 22 | +||| -> FFI seam (Layer 4): the result-code encoding is INJECTIVE, so the |
| 23 | +||| C integer crossing the Zig FFI unambiguously reconstructs the ABI |
| 24 | +||| `Result` (reusing the exported `resultToIntInjective`). |
| 25 | +||| |
| 26 | +||| The single value `abiContractDischarged : ABISound` below is constructed |
| 27 | +||| ENTIRELY from those existing exported witnesses/theorems. Because it |
| 28 | +||| typechecks, every prior layer is jointly sound: if any one of them were |
| 29 | +||| unsound (e.g. the bound proof, the action law, or the seam injectivity), |
| 30 | +||| this value would fail to elaborate. That is the end-to-end statement. |
| 31 | +module Lustreiser.ABI.Capstone |
| 32 | + |
| 33 | +import Data.Nat |
| 34 | + |
| 35 | +import Lustreiser.ABI.Types |
| 36 | +import Lustreiser.ABI.Semantics |
| 37 | +import Lustreiser.ABI.Invariants |
| 38 | +import Lustreiser.ABI.FfiSeam |
| 39 | + |
| 40 | +%default total |
| 41 | + |
| 42 | +-------------------------------------------------------------------------------- |
| 43 | +-- The capstone certificate record |
| 44 | +-------------------------------------------------------------------------------- |
| 45 | + |
| 46 | +||| `ABISound` bundles the KEY proven facts of the Lustreiser ABI, one field |
| 47 | +||| per layer. There is no constructor escape hatch: each field demands a real |
| 48 | +||| proof term, so the record is inhabited ONLY if every layer is genuinely |
| 49 | +||| discharged. |
| 50 | +public export |
| 51 | +record ABISound where |
| 52 | + constructor MkABISound |
| 53 | + |
| 54 | + ||| Layer 2 flagship (per-tick safety bound): the canonical watchdog node |
| 55 | + ||| (cap = 3, state = 2) provably stays within its static bound. Reuses the |
| 56 | + ||| exported positive control from `Semantics`. |
| 57 | + flagshipBound : WithinBound (MkCounter 3 2) |
| 58 | + |
| 59 | + ||| Layer 2 whole-run safety: running a real input stream (where saturation |
| 60 | + ||| actually fires) from a within-bound start stays within bound. Reuses the |
| 61 | + ||| exported `safeRunWithinBound`. |
| 62 | + flagshipRunBound : |
| 63 | + WithinBound (run [Tick,Tick,Tick,Tick,Reset,Tick] (MkCounter 3 0)) |
| 64 | + |
| 65 | + ||| Layer 3 deeper invariant (monoid-action / fold-fusion law on a concrete |
| 66 | + ||| split): replaying `[Tick,Tick]` then `[Reset,Tick]` equals replaying the |
| 67 | + ||| whole four-tick stream. Reuses the exported `appendWitness` instance of |
| 68 | + ||| the flagship `runAppend` theorem. |
| 69 | + layer3Action : |
| 70 | + run ([Tick,Tick] ++ [Reset,Tick]) (MkCounter 3 0) |
| 71 | + = run [Reset,Tick] (run [Tick,Tick] (MkCounter 3 0)) |
| 72 | + |
| 73 | + ||| Layer 3 orthogonal invariant (order-preservation): `satInc` is monotone |
| 74 | + ||| in its counter argument on a concrete instance. Reuses the exported |
| 75 | + ||| `monotoneWitness`. |
| 76 | + layer3Monotone : LTE (satInc 3 1) (satInc 3 2) |
| 77 | + |
| 78 | + ||| Layer 4 FFI-seam soundness: the result-code encoding is INJECTIVE — no |
| 79 | + ||| two ABI `Result`s collide on the wire. The full theorem `resultToIntInjective` |
| 80 | + ||| is carried as a field, so the seam guarantee is part of the certificate. |
| 81 | + ffiSeamInjective : |
| 82 | + (a, b : Result) -> resultToInt a = resultToInt b -> a = b |
| 83 | + |
| 84 | +-------------------------------------------------------------------------------- |
| 85 | +-- THE CAPSTONE: a single inhabited value built from prior-layer proofs |
| 86 | +-------------------------------------------------------------------------------- |
| 87 | + |
| 88 | +||| The end-to-end soundness certificate. Every field is one of the EXISTING |
| 89 | +||| exported witnesses/theorems from the layer modules — nothing is reproved, |
| 90 | +||| nothing is fabricated. If any prior layer were unsound, this value would |
| 91 | +||| not typecheck; its mere existence discharges the full ABI contract. |
| 92 | +public export |
| 93 | +abiContractDischarged : ABISound |
| 94 | +abiContractDischarged = MkABISound |
| 95 | + { flagshipBound = safeWatchdogWithinBound |
| 96 | + , flagshipRunBound = safeRunWithinBound |
| 97 | + , layer3Action = appendWitness |
| 98 | + , layer3Monotone = monotoneWitness |
| 99 | + , ffiSeamInjective = resultToIntInjective |
| 100 | + } |
0 commit comments