Skip to content

Commit bf9ec0e

Browse files
claudeclaude
committed
Add Layer-5 ABI soundness capstone certificate
Assemble the existing per-layer proofs into one inhabited value `abiContractDischarged : ABISound`, wiring the flagship semantic preservation (Semantics.sampleAgreesGeneric), the Layer-3 invariants (Invariants.compositeAgrees compositionality + translateInjective deterministic codegen), and the Layer-4 FFI seam injectivity (FfiSeam.resultToIntInjective) into a single end-to-end soundness statement. No new domain theorem; genuine composition only. Builds with zero warnings; a false-certificate adversarial probe is rejected. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx
1 parent f058fca commit bf9ec0e

2 files changed

Lines changed: 121 additions & 0 deletions

File tree

‎src/interface/abi/Julianiser/ABI/Capstone.idr‎

Lines changed: 120 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,120 @@
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: a single end-to-end ABI soundness certificate.
5+
|||
6+
||| This module proves NO new domain theorem. Its sole job is to ASSEMBLE the
7+
||| already-proven facts from every prior proof layer into ONE inhabited value,
8+
||| `abiContractDischarged : ABISound`. Because that value is constructed only
9+
||| from genuine exported witnesses/theorems, it typechecks IF AND ONLY IF every
10+
||| layer it depends on is itself sound — collapsing the whole ABI contract into
11+
||| a single yes/no compile event.
12+
|||
13+
||| The certificate ties the manifest's correctness promise through the ABI
14+
||| proofs into the FFI seam:
15+
|||
16+
||| * Layer 2 (flagship) — `Julianiser.ABI.Semantics.sampleAgreesGeneric`:
17+
||| on the canonical positive-control pipeline (`sampleExpr` over `sampleEnv`)
18+
||| the generated Julia code computes exactly the same value as the source.
19+
||| This is the headline manifest promise: translation preserves semantics.
20+
|||
21+
||| * Layer 3 (deeper invariant) — two distinct facts reused verbatim:
22+
||| - `Julianiser.ABI.Invariants.compositeAgrees`: correctness is CLOSED
23+
||| UNDER COMPOSITION (the modular/compositional theorem, witnessed on a
24+
||| concrete linked program), and
25+
||| - `Julianiser.ABI.Invariants.translateInjective`: the codegen is
26+
||| INJECTIVE (distinct source ASTs never collapse) — the structural
27+
||| backbone of deterministic, information-preserving translation.
28+
|||
29+
||| * Layer 4 (FFI seam) — `Julianiser.ABI.FfiSeam.resultToIntInjective`:
30+
||| the C-ABI wire encoding of `Result` is unambiguous, so the boundary back
31+
||| out to Zig/C is sound.
32+
|||
33+
||| Together these say: manifest promise -> ABI proofs (flagship + invariant +
34+
||| injective codegen) -> FFI seam, all discharged in one place. If ANY prior
35+
||| layer were unsound, the field supplying its witness would fail to resolve and
36+
||| this module would not build. The adversarial control (in /tmp during CI)
37+
||| confirms the certificate is non-vacuous: a FALSE field value is rejected.
38+
39+
module Julianiser.ABI.Capstone
40+
41+
import Julianiser.ABI.Types
42+
import Julianiser.ABI.Semantics
43+
import Julianiser.ABI.Invariants
44+
import Julianiser.ABI.FfiSeam
45+
import Data.Vect
46+
import Data.Fin
47+
48+
%default total
49+
50+
--------------------------------------------------------------------------------
51+
-- The end-to-end ABI soundness certificate
52+
--------------------------------------------------------------------------------
53+
54+
||| `ABISound` is a conjunction of the KEY proven facts of this ABI, one field
55+
||| per layer. Each field's TYPE is the exact proposition proved in the layer it
56+
||| names; an inhabitant therefore certifies all layers simultaneously.
57+
public export
58+
record ABISound where
59+
constructor MkABISound
60+
61+
||| Layer 2 flagship, on the canonical positive control: source and generated
62+
||| Julia agree on the sample pipeline. (= `Semantics.sampleAgreesGeneric`.)
63+
flagshipControl :
64+
evalSrc Semantics.sampleEnv Semantics.sampleExpr
65+
= evalJulia Semantics.sampleEnv (translate Semantics.sampleExpr)
66+
67+
||| Layer 3 invariant (compositionality): correctness is closed under
68+
||| composition, witnessed on the concrete composite program.
69+
||| (= `Invariants.compositeAgrees`.)
70+
invariantCompose :
71+
evalSrc Semantics.sampleEnv Invariants.compositeExpr
72+
= evalJulia Semantics.sampleEnv (translate Invariants.compositeExpr)
73+
74+
||| Layer 3 invariant (deterministic, information-preserving codegen):
75+
||| `translate` is injective for every array length. (=
76+
||| `Invariants.translateInjective`, held as a function field so the full
77+
||| universally-quantified theorem is carried; `n` is bound explicitly here so
78+
||| the field type is closed.)
79+
invariantInjective :
80+
(n : Nat) -> (e1, e2 : Expr n) -> translate e1 = translate e2 -> e1 = e2
81+
82+
||| Layer 4 FFI seam: the `Result` wire encoding is injective / unambiguous.
83+
||| (= `FfiSeam.resultToIntInjective`.)
84+
ffiSeamInjective :
85+
(a, b : Result) -> resultToInt a = resultToInt b -> a = b
86+
87+
--------------------------------------------------------------------------------
88+
-- THE CAPSTONE: one inhabited value assembled from the real witnesses
89+
--------------------------------------------------------------------------------
90+
91+
||| The capstone certificate. Every field is an existing exported theorem/witness
92+
||| — nothing is re-proved here, only composed. If any layer were unsound, the
93+
||| corresponding witness would not resolve and this definition would not build.
94+
public export
95+
abiContractDischarged : ABISound
96+
abiContractDischarged = MkABISound
97+
Semantics.sampleAgreesGeneric
98+
Invariants.compositeAgrees
99+
(\n, e1, e2, prf => Invariants.translateInjective e1 e2 prf)
100+
FfiSeam.resultToIntInjective
101+
102+
--------------------------------------------------------------------------------
103+
-- Positive control: the certificate's facts are usable end-to-end
104+
--------------------------------------------------------------------------------
105+
106+
||| Positive control: project the flagship field back out of the assembled
107+
||| certificate and confirm it is the genuine sample-agreement equality.
108+
||| Demonstrates the capstone is not an opaque token but carries real proofs.
109+
public export
110+
capstoneFlagship :
111+
evalSrc Semantics.sampleEnv Semantics.sampleExpr
112+
= evalJulia Semantics.sampleEnv (translate Semantics.sampleExpr)
113+
capstoneFlagship = flagshipControl abiContractDischarged
114+
115+
||| Positive control: the carried FFI-seam injectivity, applied to a concrete
116+
||| pair (`Ok`, `Ok`) with `Refl`, yields the expected `Ok = Ok`. Exercises the
117+
||| function-valued field of the assembled certificate.
118+
public export
119+
capstoneSeamOnOk : Ok = Ok
120+
capstoneSeamOnOk = ffiSeamInjective abiContractDischarged Ok Ok Refl

‎src/interface/abi/julianiser-abi.ipkg‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -12,3 +12,4 @@ modules = Julianiser.ABI.Types
1212
, Julianiser.ABI.Semantics
1313
, Julianiser.ABI.Invariants
1414
, Julianiser.ABI.FfiSeam
15+
, Julianiser.ABI.Capstone

0 commit comments

Comments
 (0)