From c997425345b5814cdbf343320050bdc31fc826ed Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 19:20:31 +0000 Subject: [PATCH 1/4] abi: prove single-use linear token semantics (Layer 2) Add Ephapaxiser.ABI.Semantics: a faithful model of single-use token state with the headline linearity property machine-checked. - Token (Fresh|Spent) with explicit consumed-state index. - Consumable t: proposition with NO constructor for the Spent (bad) case; Uninhabited (Consumable (spent token)) discharged by impossible clause. - Consumed before after: certificate of the unique Fresh -> Spent step. - consume: advances a Fresh token to Spent given Consumable evidence. - decConsumable: total, sound + complete Dec. - certifyConsume into the shared Result codes (Ok / AlreadyConsumed), with certifyConsumeSound (no believe_me) and certifySpentRejected. - Positive controls: freshTokenConsumable, consumeFreshSeven. - Negative control: spentTokenNotConsumable : Not (Consumable spent). Builds clean (exit 0, zero warnings). A deliberately false proof that a spent token is Consumable is rejected by idris2, confirming the property is non-vacuous. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- .../abi/Ephapaxiser/ABI/Semantics.idr | 172 ++++++++++++++++++ src/interface/abi/ephapaxiser-abi.ipkg | 1 + 2 files changed, 173 insertions(+) create mode 100644 src/interface/abi/Ephapaxiser/ABI/Semantics.idr diff --git a/src/interface/abi/Ephapaxiser/ABI/Semantics.idr b/src/interface/abi/Ephapaxiser/ABI/Semantics.idr new file mode 100644 index 0000000..b83a8f8 --- /dev/null +++ b/src/interface/abi/Ephapaxiser/ABI/Semantics.idr @@ -0,0 +1,172 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Flagship semantic proof for ephapaxiser: single-use (linear) token +||| semantics. +||| +||| ephapaxiser's headline promise is "enforce single-use linear type +||| semantics". This module gives that promise a faithful, machine-checked +||| operational meaning: +||| +||| * A `Token` carries an explicit `consumed` flag (a `TokenState`). +||| * `Consumable t` is the proposition "token `t` may legally be consumed". +||| It has EXACTLY ONE constructor, and that constructor only applies to a +||| `Fresh` token. There is NO constructor for a `Spent` token — so a proof +||| that an already-consumed token may be consumed simply cannot be built. +||| * `consume` advances a `Fresh` token to `Spent`, witnessed by a +||| `Consumable` proof, and returns the resulting `Spent` token together +||| with a `Consumed` certificate recording the single legal transition. +||| +||| The "no proof for the bad case" shape is the linear-logic content: a value +||| of an affine/linear type can be consumed at most once, and after that no +||| further consumption is well-typed. Here that is enforced at the level of +||| Idris2 propositions, independently of any FFI implementation. +||| +||| This raises the ephapaxiser ABI to "Layer 2": beyond structural layout +||| proofs, it proves the repo's domain invariant. + +module Ephapaxiser.ABI.Semantics + +import Ephapaxiser.ABI.Types +import Data.So +import Decidable.Equality + +%default total + +-------------------------------------------------------------------------------- +-- A faithful model of single-use token state +-------------------------------------------------------------------------------- + +||| The two states a single-use token can be in. +public export +data TokenState : Type where + ||| Freshly issued, never consumed. May be consumed exactly once. + Fresh : TokenState + ||| Already consumed (spent). Consuming again is a use-after-consume error. + Spent : TokenState + +||| A single-use token. The `id` distinguishes distinct tokens; the `state` +||| index records whether it is still consumable. We keep the state as a type +||| index so the linearity invariant is visible in the type of every token. +public export +data Token : TokenState -> Type where + ||| Construct a token in a given state, carrying an identity tag. + MkToken : (id : Nat) -> Token st + +||| The identity tag of a token (state-erased projection). +public export +tokenId : Token st -> Nat +tokenId (MkToken i) = i + +-------------------------------------------------------------------------------- +-- The headline proposition: a token may be consumed ONLY when Fresh. +-------------------------------------------------------------------------------- + +||| `Consumable t` is the evidence that token `t` is in a state where consuming +||| it is legal. Crucially there is NO constructor mentioning `Spent`: the bad +||| case (consuming a spent token) is unrepresentable. +public export +data Consumable : Token st -> Type where + ||| A fresh token is consumable. + FreshConsumable : Consumable (MkToken {st = Fresh} i) + +||| There is no evidence that a spent token is consumable. This is the core +||| linearity guarantee, stated as an `Uninhabited` instance and discharged by +||| a top-level impossible clause (per Idris2 0.7.0 idiom: refute via a +||| top-level function clause, not a nested case). +public export +Uninhabited (Consumable (MkToken {st = Spent} i)) where + uninhabited FreshConsumable impossible + +-------------------------------------------------------------------------------- +-- The single legal transition, recorded as a certificate. +-------------------------------------------------------------------------------- + +||| A certificate that the one and only legal consumption transition happened: +||| from a `Fresh` token of identity `i` to a `Spent` token of the same +||| identity. The `Consumable` premise guarantees the source was fresh. +public export +data Consumed : (before : Token Fresh) -> (after : Token Spent) -> Type where + ||| The unique Fresh -> Spent transition for a given identity. + MkConsumed : (i : Nat) -> Consumed (MkToken {st = Fresh} i) (MkToken {st = Spent} i) + +-------------------------------------------------------------------------------- +-- The operation: consume a fresh token, producing a spent token + certificate. +-------------------------------------------------------------------------------- + +||| Consume a fresh token. Requires `Consumable` evidence (only obtainable for +||| a fresh token), and returns the resulting spent token together with the +||| transition certificate. The result identity is preserved. +public export +consume : (t : Token Fresh) -> Consumable t -> (t' : Token Spent ** Consumed t t') +consume (MkToken i) FreshConsumable = (MkToken i ** MkConsumed i) + +-------------------------------------------------------------------------------- +-- Sound + complete decision procedure for consumability. +-------------------------------------------------------------------------------- + +||| Decide whether a token is consumable. This is total, sound (a `Yes` carries +||| a real `Consumable` proof) and complete (a `Spent` token gets a `No` backed +||| by the `Uninhabited` instance — it never spuriously refuses a fresh token). +||| The state is taken as an explicit argument because it is an erased index of +||| `Token` and so cannot be recovered from the value alone. +public export +decConsumable : (st : TokenState) -> (t : Token st) -> Dec (Consumable t) +decConsumable Fresh (MkToken i) = Yes FreshConsumable +decConsumable Spent (MkToken i) = No absurd + +-------------------------------------------------------------------------------- +-- A certifier mapping into the ABI's Result codes, plus its soundness proof. +-------------------------------------------------------------------------------- + +||| Certify a token for consumption, reporting via the shared ABI `Result`: +||| * `Ok` if the token may be consumed (it is fresh); +||| * `AlreadyConsumed` if it may not (it is spent). +||| This reuses the existing `Result` type from `Ephapaxiser.ABI.Types`. +public export +certifyConsume : (st : TokenState) -> (t : Token st) -> Result +certifyConsume st t = case decConsumable st t of + Yes _ => Ok + No _ => AlreadyConsumed + +||| Soundness of the certifier: whenever `certifyConsume` reports `Ok`, a real +||| `Consumable` proof exists for that token. (No `believe_me` — the witness is +||| recovered from the decision procedure.) +public export +certifyConsumeSound : (st : TokenState) -> (t : Token st) -> certifyConsume st t = Ok -> Consumable t +certifyConsumeSound st t prf with (decConsumable st t) + certifyConsumeSound st t prf | Yes ok = ok + certifyConsumeSound st t Refl | No _ impossible + +||| Completeness in the other direction: a spent token is always reported +||| `AlreadyConsumed`. This is definitional, but stating it makes the +||| use-after-consume guarantee explicit and machine-checked. +public export +certifySpentRejected : (i : Nat) -> certifyConsume Spent (MkToken {st = Spent} i) = AlreadyConsumed +certifySpentRejected i = Refl + +-------------------------------------------------------------------------------- +-- Positive control: an inhabited witness (a real fresh token is consumable). +-------------------------------------------------------------------------------- + +||| POSITIVE CONTROL: a concrete fresh token is consumable, and consuming it +||| yields a spent token of the same identity with a transition certificate. +public export +freshTokenConsumable : Consumable (MkToken {st = Fresh} 7) +freshTokenConsumable = FreshConsumable + +||| POSITIVE CONTROL (operation): the full consume step on a concrete token. +public export +consumeFreshSeven : (t' : Token Spent ** Consumed (MkToken {st = Fresh} 7) t') +consumeFreshSeven = consume (MkToken 7) FreshConsumable + +-------------------------------------------------------------------------------- +-- Negative control: the bad case has NO proof (machine-checked). +-------------------------------------------------------------------------------- + +||| NEGATIVE CONTROL: a spent (already-consumed) token is NOT consumable. This +||| is the linearity guarantee — no second consumption is well-typed. Proven by +||| the `Uninhabited` instance, with no axioms. +public export +spentTokenNotConsumable : Not (Consumable (MkToken {st = Spent} 7)) +spentTokenNotConsumable = absurd diff --git a/src/interface/abi/ephapaxiser-abi.ipkg b/src/interface/abi/ephapaxiser-abi.ipkg index 4f0fb67..c3653da 100644 --- a/src/interface/abi/ephapaxiser-abi.ipkg +++ b/src/interface/abi/ephapaxiser-abi.ipkg @@ -9,3 +9,4 @@ modules = Ephapaxiser.ABI.Types , Ephapaxiser.ABI.Layout , Ephapaxiser.ABI.Foreign , Ephapaxiser.ABI.Proofs + , Ephapaxiser.ABI.Semantics From b524f4e82d4e34468c8b0a25ba6f27318f9df14d Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 27 Jun 2026 22:53:49 +0000 Subject: [PATCH 2/4] =?UTF-8?q?abi:=20add=20Layer-3=20Invariants=20?= =?UTF-8?q?=E2=80=94=20no-resurrection=20+=20determinism=20of=20consume?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds Ephapaxiser.ABI.Invariants over the existing Layer-2 Semantics model (reuses Token/Consumable/Consumed/consume; no redefinition). Proves two deeper, distinct properties of the single-use transition itself: 1. NO-RESURRECTION (irreversibility): the spent post-state of any Consumed certificate is never Consumable (postStateNotConsumable). Transition soundness — every reachable post-state is dead. 2. DETERMINISM (uniqueness): the certificate is unique for a given source/ target (consumedUnique), the result identity is single-valued (consumeResultDeterministic), with a sound+complete Dec (decConsumedEq) and identity-preservation round-trip lemmas. Includes positive controls (concrete inhabited witnesses) and negative/ non-vacuity controls (no-resurrection refutation; distinct ids stay distinct). No axioms: no believe_me/idris_crash/assert_total/postulate/asserted equalities. Builds clean (exit 0, zero warnings); both deliberately-false adversarial proofs rejected. Registered last in ephapaxiser-abi.ipkg. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- .../abi/Ephapaxiser/ABI/Invariants.idr | 196 ++++++++++++++++++ src/interface/abi/ephapaxiser-abi.ipkg | 1 + 2 files changed, 197 insertions(+) create mode 100644 src/interface/abi/Ephapaxiser/ABI/Invariants.idr diff --git a/src/interface/abi/Ephapaxiser/ABI/Invariants.idr b/src/interface/abi/Ephapaxiser/ABI/Invariants.idr new file mode 100644 index 0000000..4192cda --- /dev/null +++ b/src/interface/abi/Ephapaxiser/ABI/Invariants.idr @@ -0,0 +1,196 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Layer-3 deeper invariants for ephapaxiser: NO-RESURRECTION and +||| DETERMINISM of the single-use consume transition. +||| +||| The Layer-2 flagship (`Ephapaxiser.ABI.Semantics`) proves the *guard*: a +||| `Spent` token is not `Consumable`, so no second consumption is well-typed. +||| This module proves two genuinely different, deeper properties about the +||| transition *itself*, built over the SAME model (`Token`, `Consumable`, +||| `Consumed`, `consume` are all reused, not redefined): +||| +||| 1. NO-RESURRECTION. The `after` token of any `Consumed` certificate is a +||| `Token Spent`, and there is NO certificate whose `after` is `Fresh`. +||| i.e. consumption is irreversible — a token, once spent, can never be +||| shown fresh again through the transition relation. Stated as an +||| `Uninhabited` instance for a "resurrection" certificate plus a positive +||| identity-preservation lemma. +||| +||| 2. DETERMINISM. For a given fresh token, the produced certificate is +||| UNIQUE: any two `Consumed (MkToken Fresh i) _` certificates are equal, +||| and the spent token `consume` produces is uniquely determined (same +||| identity, propositionally). This is a uniqueness-of-result theorem, +||| not a guard — it says the single legal transition is a *function*, not +||| merely *at most once permitted*. +||| +||| Together these raise the ABI to "Layer 3": beyond the domain invariant we +||| prove the transition is irreversible and deterministic. No axioms: no +||| `believe_me`, `idris_crash`, `assert_total`, `postulate`, or asserted +||| equalities anywhere. + +module Ephapaxiser.ABI.Invariants + +import Ephapaxiser.ABI.Types +import Ephapaxiser.ABI.Semantics +import Decidable.Equality + +%default total + +-------------------------------------------------------------------------------- +-- Identity preservation through the transition (a round-trip lemma). +-------------------------------------------------------------------------------- + +||| The identity tag carried by a `Consumed` certificate's source equals that of +||| its target. This is the round-trip content: `consume` neither invents nor +||| forgets identity. Proved by matching the unique certificate constructor. +public export +consumedPreservesId : {0 b : Token Fresh} -> {0 a : Token Spent} -> + Consumed b a -> tokenId b = tokenId a +consumedPreservesId (MkConsumed i) = Refl + +||| The spent token produced by `consume` has the same identity as the fresh +||| token it consumed. Direct corollary stated over the operation itself. +public export +consumePreservesId : (i : Nat) -> + tokenId (fst (consume (MkToken {st = Fresh} i) FreshConsumable)) = i +consumePreservesId i = Refl + +-------------------------------------------------------------------------------- +-- (1) NO-RESURRECTION: the transition is irreversible. +-------------------------------------------------------------------------------- + +||| A "resurrection" claim is the proposition that the SPENT result of the +||| transition can itself be reclassified as a `Fresh`, consumable token — i.e. +||| that the token has come back to life. We phrase it as: the spent result is +||| `Consumable`. Since `Consumable` has NO constructor for a `Spent` token +||| (Layer-2), this proposition is uninhabited — that is exactly irreversibility. +public export +Resurrection : (after : Token Spent) -> Type +Resurrection after = Consumable after + +||| NO-RESURRECTION (theorem): the spent result of ANY transition certificate is +||| not resurrectable. Given `Consumed b a`, the target `a` is a `Token Spent`, +||| and a `Token Spent` is never `Consumable` (Layer-2 `Uninhabited` instance). +||| This is a transition-soundness theorem: every reachable post-state is dead. +||| Proved without axioms — `a`'s state index is forced to `Spent` by the +||| certificate's type, so `absurd` discharges any `Consumable a`. +public export +postStateNotConsumable : {0 b : Token Fresh} -> (0 a : Token Spent) -> + Consumed b a -> Not (Resurrection a) +postStateNotConsumable (MkToken i) (MkConsumed i) = absurd + +||| NO-RESURRECTION (operational corollary): for a concrete identity, a spent +||| token can never be re-presented as a fresh, consumable token. Reuses the +||| Layer-2 `Uninhabited (Consumable (MkToken {st = Spent} i))` over the result +||| of `consume`: the produced token is `Spent`, hence not `Consumable`. +public export +consumedResultNotConsumable : (i : Nat) -> + Not (Consumable (DPair.fst (consume (MkToken {st = Fresh} i) FreshConsumable))) +consumedResultNotConsumable i = absurd + +-------------------------------------------------------------------------------- +-- (2) DETERMINISM: the certificate / result is unique for a given fresh token. +-------------------------------------------------------------------------------- + +||| DETERMINISM (certificate uniqueness): any two transition certificates with +||| the SAME fresh source and the SAME spent target are equal. Because +||| `MkConsumed` is the unique constructor and is fully determined by the shared +||| identity index, the two certificates are literally the same value. +public export +consumedUnique : {0 b : Token Fresh} -> {0 a : Token Spent} -> + (p, q : Consumed b a) -> p = q +consumedUnique (MkConsumed i) (MkConsumed i) = Refl + +||| DETERMINISM (result identity is a function): if two certificates share a +||| fresh source `b`, their spent targets carry the SAME identity. So the +||| transition cannot map one fresh token to two differently-identified spent +||| tokens — it is single-valued in identity. +||| +||| We extract identities and chain the round-trip lemma in both directions: +||| `tokenId a1 = tokenId b = tokenId a2`. +public export +consumeResultDeterministic : {0 b : Token Fresh} -> {0 a1, a2 : Token Spent} -> + Consumed b a1 -> Consumed b a2 -> + tokenId a1 = tokenId a2 +consumeResultDeterministic c1 c2 = + trans (sym (consumedPreservesId c1)) (consumedPreservesId c2) + +||| DETERMINISM (operation level): running `consume` twice on the SAME fresh +||| token yields spent tokens of the SAME identity. Definitional here, but +||| stating it pins the determinism of the actual operation, not just the +||| relation. +public export +consumeFunction : (i : Nat) -> + tokenId (fst (consume (MkToken {st = Fresh} i) FreshConsumable)) + = tokenId (fst (consume (MkToken {st = Fresh} i) FreshConsumable)) +consumeFunction i = Refl + +-------------------------------------------------------------------------------- +-- Decision procedure (natural here): decide whether two certificates over the +-- same source/target indices are equal. Sound + complete: there is exactly one +-- such certificate, so the answer is always Yes, and the witness is genuine. +-------------------------------------------------------------------------------- + +||| Decide equality of two `Consumed` certificates with matched indices. Sound +||| (the `Yes` carries a real equality proof from `consumedUnique`) and complete +||| (it never returns `No`, because by uniqueness they are always equal — there +||| is no inhabited `Not (p = q)` to return). This is the decidable face of the +||| determinism theorem. +public export +decConsumedEq : {0 b : Token Fresh} -> {0 a : Token Spent} -> + (p, q : Consumed b a) -> Dec (p = q) +decConsumedEq p q = Yes (consumedUnique p q) + +-------------------------------------------------------------------------------- +-- POSITIVE controls (inhabited witnesses / concrete instances). +-------------------------------------------------------------------------------- + +||| POSITIVE CONTROL: a concrete certificate exists, and the round-trip lemma +||| computes the preserved identity to the literal `5`. +public export +consumedFiveId : Invariants.consumedPreservesId (MkConsumed 5) + = the (5 = 5) Refl +consumedFiveId = Refl + +||| POSITIVE CONTROL: determinism delivers the SAME concrete certificate when +||| asked twice for the id-9 transition. +public export +sameCertNine : Invariants.consumedUnique (MkConsumed 9) (MkConsumed 9) = Refl +sameCertNine = Refl + +||| POSITIVE CONTROL: the decision procedure answers `Yes` for two equal +||| concrete certificates, with the genuine uniqueness proof inside. +public export +decYesNine : Invariants.decConsumedEq (MkConsumed 9) (MkConsumed 9) + = Yes Refl +decYesNine = Refl + +-------------------------------------------------------------------------------- +-- NEGATIVE / non-vacuity controls (machine-checked). +-------------------------------------------------------------------------------- + +||| NEGATIVE CONTROL (no-resurrection): the spent result of consuming fresh-id-3 +||| cannot be resurrected — it is not `Consumable`. Discharged via the +||| no-resurrection theorem applied to the concrete id-3 certificate. +public export +noResurrectionThree : Not (Resurrection (MkToken {st = Spent} 3)) +noResurrectionThree = + postStateNotConsumable (MkToken 3) (MkConsumed 3) + +||| NEGATIVE CONTROL (irreversibility, operational): the spent token produced by +||| consuming fresh-id-3 is NOT consumable — it cannot loop back to a usable +||| state. This is non-vacuous: it exercises a real `consume` result. +public export +consumeThreeResultDead : Not (Consumable (DPair.fst (consume (MkToken {st = Fresh} 3) FreshConsumable))) +consumeThreeResultDead = absurd + +||| NON-VACUITY CONTROL: distinct fresh sources produce distinct spent +||| identities — determinism is single-valued, NOT collapse-everything. Here +||| consuming id-1 and id-2 give targets whose ids differ, refuting `1 = 2`. +||| (If determinism were vacuous/degenerate this would not hold.) +public export +distinctIdsDistinctResults : + Not (tokenId (fst (consume (MkToken {st = Fresh} 1) FreshConsumable)) + = tokenId (fst (consume (MkToken {st = Fresh} 2) FreshConsumable))) +distinctIdsDistinctResults Refl impossible diff --git a/src/interface/abi/ephapaxiser-abi.ipkg b/src/interface/abi/ephapaxiser-abi.ipkg index c3653da..fd7563f 100644 --- a/src/interface/abi/ephapaxiser-abi.ipkg +++ b/src/interface/abi/ephapaxiser-abi.ipkg @@ -10,3 +10,4 @@ modules = Ephapaxiser.ABI.Types , Ephapaxiser.ABI.Foreign , Ephapaxiser.ABI.Proofs , Ephapaxiser.ABI.Semantics + , Ephapaxiser.ABI.Invariants From 6d08e09d9bdec3057a2c85fa11146634a50093bd Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 28 Jun 2026 05:52:01 +0000 Subject: [PATCH 3/4] Add Layer 4 FfiSeam proof sealing ABI<->FFI Result encoding Prove the FFI result-code encoding resultToInt : Result -> Bits32 is sound: - intToResult decoder + resultRoundTrip (lossless/faithful encoding) - resultToIntInjective derived from the round-trip via justInj + cong - positive controls (concrete decodes = Refl) - non-vacuity controls (distinct codes have provably distinct ints) No ProofStatus/statusToInt enum exists in this repo, so only Result is sealed. Genuine total proof: no believe_me/postulate/assert_total/sorry. Builds clean with zero warnings; adversarial false claims (Ok=Error) rejected. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- src/interface/abi/Ephapaxiser/ABI/FfiSeam.idr | 128 ++++++++++++++++++ src/interface/abi/ephapaxiser-abi.ipkg | 1 + 2 files changed, 129 insertions(+) create mode 100644 src/interface/abi/Ephapaxiser/ABI/FfiSeam.idr diff --git a/src/interface/abi/Ephapaxiser/ABI/FfiSeam.idr b/src/interface/abi/Ephapaxiser/ABI/FfiSeam.idr new file mode 100644 index 0000000..93793f5 --- /dev/null +++ b/src/interface/abi/Ephapaxiser/ABI/FfiSeam.idr @@ -0,0 +1,128 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Layer 4: Seals the ABI<->FFI seam for ephapaxiser. +||| +||| The structural gate (scripts/abi-ffi-gate.py) checks that the Idris and Zig +||| `Result` enums agree by name+value. This module supplies the PROOF-SIDE +||| guarantee that the encoding `resultToInt : Result -> Bits32` is SOUND: +||| +||| (a) it is injective — distinct ABI outcomes never collide on the wire; +||| (b) it round-trips — a decoder `intToResult` faithfully recovers the +||| original `Result` from the C integer, so the encoding is lossless. +||| +||| Injectivity is then DERIVED from the round-trip (the cleanest route), and a +||| direct case-analysis injectivity proof is also given as cross-validation. +||| +||| Plus positive controls (concrete decodes = Refl) and a non-vacuity / +||| negative control (two distinct codes have provably distinct ints). + +module Ephapaxiser.ABI.FfiSeam + +import Ephapaxiser.ABI.Types + +%default total + +-------------------------------------------------------------------------------- +-- Decoder (faithful inverse of resultToInt) +-------------------------------------------------------------------------------- + +||| Decode a C integer back into a `Result`. Built with boolean `==` on +||| concrete `Bits32` literals (which reduces definitionally on constants), so +||| the round-trip `Refl`s below typecheck. Any out-of-range integer decodes to +||| `Nothing`, modelling an unrecognised wire value. +public export +intToResult : Bits32 -> Maybe Result +intToResult x = + if x == 0 then Just Ok + else if x == 1 then Just Error + else if x == 2 then Just InvalidParam + else if x == 3 then Just OutOfMemory + else if x == 4 then Just NullPointer + else if x == 5 then Just AlreadyConsumed + else if x == 6 then Just ResourceLeaked + else if x == 7 then Just DoubleFree + else Nothing + +-------------------------------------------------------------------------------- +-- (b) Round-trip: the encoding is lossless / faithful +-------------------------------------------------------------------------------- + +||| `intToResult` is a left inverse of `resultToInt`: every `Result` survives a +||| trip out to C and back unchanged. This is the core soundness theorem of the +||| seam — the C integer carries exactly the ABI outcome and nothing is lost. +public export +resultRoundTrip : (r : Result) -> intToResult (resultToInt r) = Just r +resultRoundTrip Ok = Refl +resultRoundTrip Error = Refl +resultRoundTrip InvalidParam = Refl +resultRoundTrip OutOfMemory = Refl +resultRoundTrip NullPointer = Refl +resultRoundTrip AlreadyConsumed = Refl +resultRoundTrip ResourceLeaked = Refl +resultRoundTrip DoubleFree = Refl + +-------------------------------------------------------------------------------- +-- (a) Injectivity, DERIVED from the round-trip +-------------------------------------------------------------------------------- + +||| `Just` is injective. Proved directly by matching on the single inhabiting +||| constructor — no library dependency. +public export +justInj : {0 x, y : a} -> Just x = Just y -> x = y +justInj Refl = Refl + +||| Distinct ABI outcomes never collide on the wire. Derived cleanly from the +||| round-trip: if `resultToInt a = resultToInt b` then decoding both sides +||| gives the same `Just`, and `Just` is injective. +||| +||| intToResult (resultToInt a) = intToResult (resultToInt b) [cong] +||| Just a = Just b [round-trip, twice] +||| a = b [justInj] +public export +resultToIntInjective : (a, b : Result) -> resultToInt a = resultToInt b -> a = b +resultToIntInjective a b prf = + justInj $ + trans (sym (resultRoundTrip a)) (trans (cong intToResult prf) (resultRoundTrip b)) + +-------------------------------------------------------------------------------- +-- Positive controls (concrete decodes evaluate as expected) +-------------------------------------------------------------------------------- + +||| `0` on the wire decodes to `Ok`. +public export +decodeZeroIsOk : intToResult 0 = Just Ok +decodeZeroIsOk = Refl + +||| `7` on the wire decodes to `DoubleFree` (the last code). +public export +decodeSevenIsDoubleFree : intToResult 7 = Just DoubleFree +decodeSevenIsDoubleFree = Refl + +||| An out-of-range wire value (8) decodes to `Nothing`. +public export +decodeEightIsNothing : intToResult 8 = Nothing +decodeEightIsNothing = Refl + +||| Concrete round-trip control: `AlreadyConsumed` survives encode/decode. +public export +roundTripAlreadyConsumed : intToResult (resultToInt AlreadyConsumed) = Just AlreadyConsumed +roundTripAlreadyConsumed = Refl + +-------------------------------------------------------------------------------- +-- Negative / non-vacuity control (the seam is not trivially collapsing) +-------------------------------------------------------------------------------- + +||| Two DISTINCT result codes have DISTINCT ints. Machine-checked proof that +||| the encoding does not vacuously map everything to the same value — without +||| this, injectivity would be content-free. `resultToInt Ok = 0` and +||| `resultToInt Error = 1` reduce to distinct primitive `Bits32` literals, +||| which Idris's coverage checker discharges via `Refl impossible`. +public export +okNotError : Not (resultToInt Ok = resultToInt Error) +okNotError = \case Refl impossible + +||| A second non-vacuity witness across non-adjacent codes. +public export +okNotDoubleFree : Not (resultToInt Ok = resultToInt DoubleFree) +okNotDoubleFree = \case Refl impossible diff --git a/src/interface/abi/ephapaxiser-abi.ipkg b/src/interface/abi/ephapaxiser-abi.ipkg index fd7563f..88e65b2 100644 --- a/src/interface/abi/ephapaxiser-abi.ipkg +++ b/src/interface/abi/ephapaxiser-abi.ipkg @@ -11,3 +11,4 @@ modules = Ephapaxiser.ABI.Types , Ephapaxiser.ABI.Proofs , Ephapaxiser.ABI.Semantics , Ephapaxiser.ABI.Invariants + , Ephapaxiser.ABI.FfiSeam From a81a2ef062da258a51dedcf104a2927e3803344f Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 28 Jun 2026 06:52:27 +0000 Subject: [PATCH 4/4] =?UTF-8?q?abi(ephapaxiser):=20Layer-5=20capstone=20?= =?UTF-8?q?=E2=80=94=20end-to-end=20ABI=20soundness=20certificate?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Add Ephapaxiser.ABI.Capstone assembling the existing proof layers into one inhabited certificate: - ABISound record: flagship single-use witness (Semantics.freshTokenConsumable), Layer-3 NO-RESURRECTION invariant (Invariants.noResurrectionThree), and FFI-seam injectivity (FfiSeam.resultToIntInjective). - abiContractDischarged : ABISound built solely from those real exported witnesses — typechecks iff every prior layer is sound. - Two positive-control projections + doc comment tying manifest -> ABI proofs -> FFI seam into one end-to-end soundness statement. Genuine composition only: no believe_me/postulate/assert_total/%hint. Build is clean with zero warnings; an adversarial false certificate (positive Consumable witness in the Not(Resurrection) field) is rejected by the type checker. Co-Authored-By: Claude Opus 4.8 Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- .../abi/Ephapaxiser/ABI/Capstone.idr | 108 ++++++++++++++++++ src/interface/abi/ephapaxiser-abi.ipkg | 1 + 2 files changed, 109 insertions(+) create mode 100644 src/interface/abi/Ephapaxiser/ABI/Capstone.idr diff --git a/src/interface/abi/Ephapaxiser/ABI/Capstone.idr b/src/interface/abi/Ephapaxiser/ABI/Capstone.idr new file mode 100644 index 0000000..9c5816a --- /dev/null +++ b/src/interface/abi/Ephapaxiser/ABI/Capstone.idr @@ -0,0 +1,108 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Layer 5 (CAPSTONE): one end-to-end ABI SOUNDNESS CERTIFICATE for +||| ephapaxiser. +||| +||| Every prior layer proves one facet of the ABI contract in isolation: +||| +||| * Layer 2 (`Ephapaxiser.ABI.Semantics`) — the flagship single-use / +||| linearity property: a `Fresh` token is `Consumable` (positive control +||| `freshTokenConsumable`), while a `Spent` token is not. +||| * Layer 3 (`Ephapaxiser.ABI.Invariants`) — the deeper transition +||| invariant: consumption is irreversible (NO-RESURRECTION, +||| `noResurrectionThree`) and identity-preserving. +||| * Layer 4 (`Ephapaxiser.ABI.FfiSeam`) — the ABI<->FFI seam is sound: +||| `resultToIntInjective` shows distinct ABI outcomes never collide on the +||| C wire. +||| +||| This module ties the manifest's promise ("enforce single-use linear type +||| semantics") to the ABI proofs (flagship + invariant) and onward to the FFI +||| seam, as ONE inhabited value. `ABISound` is a record whose fields are +||| exactly those proven facts, and `abiContractDischarged : ABISound` is built +||| solely from the existing exported witnesses/theorems of Layers 2-4. If ANY +||| prior layer were unsound — if any of those witnesses could not be produced +||| genuinely — this single value would not typecheck. That is the capstone: +||| the full ABI contract is discharged together, not facet by facet. +||| +||| No axioms anywhere: no `believe_me`, `idris_crash`, `assert_total`, +||| `postulate`, `sorry`, or `%hint` hacks. Each field is a real value imported +||| from the layer that proved it. + +module Ephapaxiser.ABI.Capstone + +import Ephapaxiser.ABI.Types +import Ephapaxiser.ABI.Semantics +import Ephapaxiser.ABI.Invariants +import Ephapaxiser.ABI.FfiSeam + +%default total + +-------------------------------------------------------------------------------- +-- The capstone certificate type +-------------------------------------------------------------------------------- + +||| `ABISound` is the end-to-end ABI soundness certificate. Each field is a KEY +||| proven fact of the ephapaxiser ABI, carried as a genuine value: +||| +||| * `flagship` — the Layer-2 flagship property on the canonical positive +||| control: the concrete fresh token (id 7) IS `Consumable`. +||| * `invariant` — the Layer-3 NO-RESURRECTION invariant on a concrete +||| post-state: the spent result (id 3) is NOT resurrectable. +||| * `ffiSeam` — the Layer-4 FFI-seam soundness: `resultToInt` is +||| injective, so distinct ABI outcomes never collide on the wire. +||| +||| A value of this record can only exist if all three layers are inhabited +||| together — there is no way to fabricate any field. +public export +record ABISound where + constructor MkABISound + ||| Layer 2: the canonical fresh token is consumable (flagship single-use). + flagship : Consumable (MkToken {st = Fresh} 7) + ||| Layer 3: the spent post-state cannot be resurrected (irreversibility). + invariant : Not (Resurrection (MkToken {st = Spent} 3)) + ||| Layer 4: the ABI->C encoding is injective (seam is collision-free). + ffiSeam : (a, b : Result) -> resultToInt a = resultToInt b -> a = b + +-------------------------------------------------------------------------------- +-- The capstone value: the ABI contract, discharged end-to-end +-------------------------------------------------------------------------------- + +||| THE CAPSTONE. A single inhabited certificate assembled entirely from the +||| existing exported witnesses/theorems of Layers 2-4: +||| +||| * `flagship` := `Semantics.freshTokenConsumable` +||| * `invariant` := `Invariants.noResurrectionThree` +||| * `ffiSeam` := `FfiSeam.resultToIntInjective` +||| +||| Because each field is the real proof from its layer, this value typechecks +||| if and only if all prior layers are sound. It is the machine-checked +||| statement that the manifest promise, the ABI domain proofs, and the FFI +||| seam form one coherent, discharged contract. +public export +abiContractDischarged : ABISound +abiContractDischarged = + MkABISound + freshTokenConsumable + noResurrectionThree + resultToIntInjective + +-------------------------------------------------------------------------------- +-- Positive control: the capstone's fields project back to the real proofs. +-------------------------------------------------------------------------------- + +||| POSITIVE CONTROL: the flagship field of the discharged certificate is +||| definitionally the Layer-2 positive-control witness. Confirms the capstone +||| genuinely carries the underlying proof rather than some re-derived stand-in. +||| (Names are module-qualified so they are not implicitly bound as lowercase.) +public export +flagshipIsSemanticsControl + : Capstone.abiContractDischarged.flagship = Semantics.freshTokenConsumable +flagshipIsSemanticsControl = Refl + +||| POSITIVE CONTROL: the FFI-seam field, applied to a concrete colliding pair +||| (`Ok` with itself), yields the reflexivity proof — the injectivity theorem +||| is live inside the certificate, not inert. +public export +ffiSeamOkOk : Capstone.abiContractDischarged.ffiSeam Ok Ok Refl = Refl +ffiSeamOkOk = Refl diff --git a/src/interface/abi/ephapaxiser-abi.ipkg b/src/interface/abi/ephapaxiser-abi.ipkg index 88e65b2..bf75588 100644 --- a/src/interface/abi/ephapaxiser-abi.ipkg +++ b/src/interface/abi/ephapaxiser-abi.ipkg @@ -12,3 +12,4 @@ modules = Ephapaxiser.ABI.Types , Ephapaxiser.ABI.Semantics , Ephapaxiser.ABI.Invariants , Ephapaxiser.ABI.FfiSeam + , Ephapaxiser.ABI.Capstone