Skip to content

Commit c2fba07

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
abi: prove single-use linear token semantics (Layer 2) (#42)
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. Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx Co-authored-by: Claude <noreply@anthropic.com>
1 parent ecb4711 commit c2fba07

2 files changed

Lines changed: 173 additions & 0 deletions

File tree

‎src/interface/abi/Ephapaxiser/ABI/Semantics.idr‎

Lines changed: 172 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,172 @@
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+
||| Flagship semantic proof for ephapaxiser: single-use (linear) token
5+
||| semantics.
6+
|||
7+
||| ephapaxiser's headline promise is "enforce single-use linear type
8+
||| semantics". This module gives that promise a faithful, machine-checked
9+
||| operational meaning:
10+
|||
11+
||| * A `Token` carries an explicit `consumed` flag (a `TokenState`).
12+
||| * `Consumable t` is the proposition "token `t` may legally be consumed".
13+
||| It has EXACTLY ONE constructor, and that constructor only applies to a
14+
||| `Fresh` token. There is NO constructor for a `Spent` token — so a proof
15+
||| that an already-consumed token may be consumed simply cannot be built.
16+
||| * `consume` advances a `Fresh` token to `Spent`, witnessed by a
17+
||| `Consumable` proof, and returns the resulting `Spent` token together
18+
||| with a `Consumed` certificate recording the single legal transition.
19+
|||
20+
||| The "no proof for the bad case" shape is the linear-logic content: a value
21+
||| of an affine/linear type can be consumed at most once, and after that no
22+
||| further consumption is well-typed. Here that is enforced at the level of
23+
||| Idris2 propositions, independently of any FFI implementation.
24+
|||
25+
||| This raises the ephapaxiser ABI to "Layer 2": beyond structural layout
26+
||| proofs, it proves the repo's domain invariant.
27+
28+
module Ephapaxiser.ABI.Semantics
29+
30+
import Ephapaxiser.ABI.Types
31+
import Data.So
32+
import Decidable.Equality
33+
34+
%default total
35+
36+
--------------------------------------------------------------------------------
37+
-- A faithful model of single-use token state
38+
--------------------------------------------------------------------------------
39+
40+
||| The two states a single-use token can be in.
41+
public export
42+
data TokenState : Type where
43+
||| Freshly issued, never consumed. May be consumed exactly once.
44+
Fresh : TokenState
45+
||| Already consumed (spent). Consuming again is a use-after-consume error.
46+
Spent : TokenState
47+
48+
||| A single-use token. The `id` distinguishes distinct tokens; the `state`
49+
||| index records whether it is still consumable. We keep the state as a type
50+
||| index so the linearity invariant is visible in the type of every token.
51+
public export
52+
data Token : TokenState -> Type where
53+
||| Construct a token in a given state, carrying an identity tag.
54+
MkToken : (id : Nat) -> Token st
55+
56+
||| The identity tag of a token (state-erased projection).
57+
public export
58+
tokenId : Token st -> Nat
59+
tokenId (MkToken i) = i
60+
61+
--------------------------------------------------------------------------------
62+
-- The headline proposition: a token may be consumed ONLY when Fresh.
63+
--------------------------------------------------------------------------------
64+
65+
||| `Consumable t` is the evidence that token `t` is in a state where consuming
66+
||| it is legal. Crucially there is NO constructor mentioning `Spent`: the bad
67+
||| case (consuming a spent token) is unrepresentable.
68+
public export
69+
data Consumable : Token st -> Type where
70+
||| A fresh token is consumable.
71+
FreshConsumable : Consumable (MkToken {st = Fresh} i)
72+
73+
||| There is no evidence that a spent token is consumable. This is the core
74+
||| linearity guarantee, stated as an `Uninhabited` instance and discharged by
75+
||| a top-level impossible clause (per Idris2 0.7.0 idiom: refute via a
76+
||| top-level function clause, not a nested case).
77+
public export
78+
Uninhabited (Consumable (MkToken {st = Spent} i)) where
79+
uninhabited FreshConsumable impossible
80+
81+
--------------------------------------------------------------------------------
82+
-- The single legal transition, recorded as a certificate.
83+
--------------------------------------------------------------------------------
84+
85+
||| A certificate that the one and only legal consumption transition happened:
86+
||| from a `Fresh` token of identity `i` to a `Spent` token of the same
87+
||| identity. The `Consumable` premise guarantees the source was fresh.
88+
public export
89+
data Consumed : (before : Token Fresh) -> (after : Token Spent) -> Type where
90+
||| The unique Fresh -> Spent transition for a given identity.
91+
MkConsumed : (i : Nat) -> Consumed (MkToken {st = Fresh} i) (MkToken {st = Spent} i)
92+
93+
--------------------------------------------------------------------------------
94+
-- The operation: consume a fresh token, producing a spent token + certificate.
95+
--------------------------------------------------------------------------------
96+
97+
||| Consume a fresh token. Requires `Consumable` evidence (only obtainable for
98+
||| a fresh token), and returns the resulting spent token together with the
99+
||| transition certificate. The result identity is preserved.
100+
public export
101+
consume : (t : Token Fresh) -> Consumable t -> (t' : Token Spent ** Consumed t t')
102+
consume (MkToken i) FreshConsumable = (MkToken i ** MkConsumed i)
103+
104+
--------------------------------------------------------------------------------
105+
-- Sound + complete decision procedure for consumability.
106+
--------------------------------------------------------------------------------
107+
108+
||| Decide whether a token is consumable. This is total, sound (a `Yes` carries
109+
||| a real `Consumable` proof) and complete (a `Spent` token gets a `No` backed
110+
||| by the `Uninhabited` instance — it never spuriously refuses a fresh token).
111+
||| The state is taken as an explicit argument because it is an erased index of
112+
||| `Token` and so cannot be recovered from the value alone.
113+
public export
114+
decConsumable : (st : TokenState) -> (t : Token st) -> Dec (Consumable t)
115+
decConsumable Fresh (MkToken i) = Yes FreshConsumable
116+
decConsumable Spent (MkToken i) = No absurd
117+
118+
--------------------------------------------------------------------------------
119+
-- A certifier mapping into the ABI's Result codes, plus its soundness proof.
120+
--------------------------------------------------------------------------------
121+
122+
||| Certify a token for consumption, reporting via the shared ABI `Result`:
123+
||| * `Ok` if the token may be consumed (it is fresh);
124+
||| * `AlreadyConsumed` if it may not (it is spent).
125+
||| This reuses the existing `Result` type from `Ephapaxiser.ABI.Types`.
126+
public export
127+
certifyConsume : (st : TokenState) -> (t : Token st) -> Result
128+
certifyConsume st t = case decConsumable st t of
129+
Yes _ => Ok
130+
No _ => AlreadyConsumed
131+
132+
||| Soundness of the certifier: whenever `certifyConsume` reports `Ok`, a real
133+
||| `Consumable` proof exists for that token. (No `believe_me` — the witness is
134+
||| recovered from the decision procedure.)
135+
public export
136+
certifyConsumeSound : (st : TokenState) -> (t : Token st) -> certifyConsume st t = Ok -> Consumable t
137+
certifyConsumeSound st t prf with (decConsumable st t)
138+
certifyConsumeSound st t prf | Yes ok = ok
139+
certifyConsumeSound st t Refl | No _ impossible
140+
141+
||| Completeness in the other direction: a spent token is always reported
142+
||| `AlreadyConsumed`. This is definitional, but stating it makes the
143+
||| use-after-consume guarantee explicit and machine-checked.
144+
public export
145+
certifySpentRejected : (i : Nat) -> certifyConsume Spent (MkToken {st = Spent} i) = AlreadyConsumed
146+
certifySpentRejected i = Refl
147+
148+
--------------------------------------------------------------------------------
149+
-- Positive control: an inhabited witness (a real fresh token is consumable).
150+
--------------------------------------------------------------------------------
151+
152+
||| POSITIVE CONTROL: a concrete fresh token is consumable, and consuming it
153+
||| yields a spent token of the same identity with a transition certificate.
154+
public export
155+
freshTokenConsumable : Consumable (MkToken {st = Fresh} 7)
156+
freshTokenConsumable = FreshConsumable
157+
158+
||| POSITIVE CONTROL (operation): the full consume step on a concrete token.
159+
public export
160+
consumeFreshSeven : (t' : Token Spent ** Consumed (MkToken {st = Fresh} 7) t')
161+
consumeFreshSeven = consume (MkToken 7) FreshConsumable
162+
163+
--------------------------------------------------------------------------------
164+
-- Negative control: the bad case has NO proof (machine-checked).
165+
--------------------------------------------------------------------------------
166+
167+
||| NEGATIVE CONTROL: a spent (already-consumed) token is NOT consumable. This
168+
||| is the linearity guarantee — no second consumption is well-typed. Proven by
169+
||| the `Uninhabited` instance, with no axioms.
170+
public export
171+
spentTokenNotConsumable : Not (Consumable (MkToken {st = Spent} 7))
172+
spentTokenNotConsumable = absurd

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,3 +9,4 @@ modules = Ephapaxiser.ABI.Types
99
, Ephapaxiser.ABI.Layout
1010
, Ephapaxiser.ABI.Foreign
1111
, Ephapaxiser.ABI.Proofs
12+
, Ephapaxiser.ABI.Semantics

0 commit comments

Comments
 (0)