Skip to content

Commit 5e57cc8

Browse files
claudeclaude
committed
feat(abi): prove reversible ops form a group (Layer 3 invariants)
Add Oblibeniser.ABI.Invariants, a second, deeper machine-checked theorem over the SAME Layer-2 model (Op/State/apply/invert/unapply). Where Layer 2 proves the per-element round-trip laws, Layer 3 proves the whole collection is a GROUP under Seq, quotiented by denotational equivalence Equiv: - Equiv is an equivalence relation and a congruence for Seq; - Seq is associative; Nop is a two-sided unit; - every op has a two-sided inverse (reusing reversible / reversibleDual); - inverses are UNIQUE (cancellation theorem); - invert is an involution and anti-homomorphism up to Equiv. Includes a sound+complete decision procedure decAgreeOn for agreement on a finite probe set, an unforgeable IsGroupInverse certificate tied to the ABI Result codes with a soundness lemma, positive controls (concrete witnesses + inhabited certificate), and negative/non-vacuity controls (Not-equivalences machine-checked, decision returns No). No believe_me/postulate/assert_total; %default total; builds with zero warnings; adversarial false proof rejected. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx
1 parent ba629ba commit 5e57cc8

2 files changed

Lines changed: 351 additions & 0 deletions

File tree

‎src/interface/abi/Oblibeniser/ABI/Invariants.idr‎

Lines changed: 350 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,350 @@
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-3 algebraic structure for Oblibeniser: the reversible operations
5+
||| form a GROUP under sequencing.
6+
|||
7+
||| The Layer-2 flagship (`Oblibeniser.ABI.Semantics`) proves the *round-trip*
8+
||| laws: `unapply op . apply op = id` and `apply op . unapply op = id`. That
9+
||| is the inverse-existence half of group structure for a single element.
10+
|||
11+
||| This module proves a genuinely DEEPER and DISTINCT property: the whole
12+
||| collection of operations, quotiented by *denotational equivalence*
13+
||| (`Equiv p q` iff they act identically on every state), carries the full
14+
||| algebraic structure of a GROUP with respect to `Seq`:
15+
|||
16+
||| * `Seq` is ASSOCIATIVE up to `Equiv` (apply is a monoid homomorphism into
17+
||| endofunction composition);
18+
||| * `Nop` is a TWO-SIDED UNIT;
19+
||| * every element has a TWO-SIDED inverse:
20+
||| `Equiv (Seq op (invert op)) Nop` and `Equiv (Seq (invert op) op) Nop`;
21+
||| * `Equiv` is a congruence for `Seq` (so the quotient is well-defined);
22+
||| * inverses are UNIQUE (the standard cancellation theorem);
23+
||| * `invert` is an ANTI-HOMOMORPHISM and an involution up to `Equiv`.
24+
|||
25+
||| These are algebraic LAWS (associativity, unit, inverse, uniqueness), not a
26+
||| restatement of the round-trip equality. They are all reduced to the Layer-2
27+
||| model: we reuse the SAME `Op`, `State`, `apply`, `invert`, `unapply`, and
28+
||| the Layer-2 theorems `reversible` and `reversibleDual`.
29+
|||
30+
||| A decision procedure `decAgreeOn` decides denotational agreement on a
31+
||| finite list of probe states (sound AND complete for that probe set), with
32+
||| positive and negative/non-vacuity controls machine-checked below.
33+
|||
34+
||| Note on controls: the Layer-2 model deliberately keeps the per-operation
35+
||| state transformers (`flipAll`, `xorMask`) PRIVATE, so `apply FlipAll s` and
36+
||| `apply (XorMask m) s` are opaque to this module and do NOT reduce by `Refl`.
37+
||| `apply Rev s = reverse s` (public Prelude `reverse`) and `apply Nop s = s`
38+
||| DO reduce. The concrete controls therefore use `Rev`/`Nop`, while the
39+
||| general theorems cover every operation via the exported Layer-2 lemmas.
40+
41+
module Oblibeniser.ABI.Invariants
42+
43+
import Oblibeniser.ABI.Types
44+
import Oblibeniser.ABI.Semantics
45+
import Data.List.Elem
46+
import Decidable.Equality
47+
48+
%default total
49+
50+
--------------------------------------------------------------------------------
51+
-- Denotational equivalence of operations
52+
--------------------------------------------------------------------------------
53+
54+
||| Two operations are equivalent when they act identically on EVERY state.
55+
||| This is the equivalence by which we quotient `Op` to obtain the group.
56+
public export
57+
Equiv : Op -> Op -> Type
58+
Equiv p q = (s : State) -> apply p s = apply q s
59+
60+
--------------------------------------------------------------------------------
61+
-- `Equiv` is an equivalence relation (reflexive, symmetric, transitive)
62+
--------------------------------------------------------------------------------
63+
64+
||| Reflexivity.
65+
export
66+
equivRefl : (p : Op) -> Equiv p p
67+
equivRefl _ _ = Refl
68+
69+
||| Symmetry. The operations are taken as explicit (erased) arguments so that
70+
||| callers can pin them down: `Equiv` unfolds to a function type whose body
71+
||| `apply p s` reduces away the structure of `p`, defeating implicit inference.
72+
export
73+
equivSym : (0 p, q : Op) -> Equiv p q -> Equiv q p
74+
equivSym _ _ pq s = sym (pq s)
75+
76+
||| Transitivity (operations explicit, for the same inference reason).
77+
export
78+
equivTrans : (0 p, q, r : Op) -> Equiv p q -> Equiv q r -> Equiv p r
79+
equivTrans _ _ _ pq qr s = trans (pq s) (qr s)
80+
81+
--------------------------------------------------------------------------------
82+
-- `Equiv` is a CONGRUENCE for `Seq` (so the quotient operation is well-defined)
83+
--------------------------------------------------------------------------------
84+
85+
||| If the components are equivalent, the sequences are equivalent. This is
86+
||| what makes `Seq` descend to the quotient `Op/Equiv`.
87+
|||
88+
||| `apply (Seq p q) s = apply q (apply p s)`, so we rewrite the inner
89+
||| application with `pp` and the outer with `qq` (instantiated at the
90+
||| rewritten inner state). The operation arguments are kept RUNTIME-relevant
91+
||| because `p'` appears in the term `apply p' s` on the right-hand side.
92+
export
93+
seqCong : (p, p', q, q' : Op) ->
94+
Equiv p p' -> Equiv q q' -> Equiv (Seq p q) (Seq p' q')
95+
seqCong p p' q q' pp qq s =
96+
rewrite pp s in
97+
qq (apply p' s)
98+
99+
--------------------------------------------------------------------------------
100+
-- MONOID LAWS over `Equiv`
101+
--------------------------------------------------------------------------------
102+
103+
||| ASSOCIATIVITY of sequencing (an algebraic law genuinely distinct from the
104+
||| round-trip theorem). Both sides denote `apply r . apply q . apply p`, so
105+
||| the equality holds definitionally at each state.
106+
export
107+
seqAssoc : (p, q, r : Op) -> Equiv (Seq (Seq p q) r) (Seq p (Seq q r))
108+
seqAssoc p q r s = Refl
109+
110+
||| LEFT UNIT: `Nop` on the left is neutral.
111+
export
112+
nopLeftUnit : (op : Op) -> Equiv (Seq Nop op) op
113+
nopLeftUnit op s = Refl
114+
115+
||| RIGHT UNIT: `Nop` on the right is neutral.
116+
export
117+
nopRightUnit : (op : Op) -> Equiv (Seq op Nop) op
118+
nopRightUnit op s = Refl
119+
120+
--------------------------------------------------------------------------------
121+
-- GROUP LAWS over `Equiv` (two-sided inverse) — the core Layer-3 theorem
122+
--------------------------------------------------------------------------------
123+
124+
||| RIGHT INVERSE: doing `op` then its inverse is denotationally the identity.
125+
|||
126+
||| Equiv (Seq op (invert op)) Nop
127+
|||
128+
||| `apply (Seq op (invert op)) s = apply (invert op) (apply op s)
129+
||| = unapply op (apply op s)`,
130+
||| which the Layer-2 `reversible` law equates with `s = apply Nop s`.
131+
export
132+
seqInverseRight : (op : Op) -> Equiv (Seq op (invert op)) Nop
133+
seqInverseRight op s = reversible op s
134+
135+
||| LEFT INVERSE: doing the inverse of `op` then `op` is also the identity.
136+
|||
137+
||| Equiv (Seq (invert op) op) Nop
138+
|||
139+
||| `apply (Seq (invert op) op) s = apply op (apply (invert op) s)
140+
||| = apply op (unapply op s)`,
141+
||| which the Layer-2 dual law `reversibleDual` equates with `s`.
142+
export
143+
seqInverseLeft : (op : Op) -> Equiv (Seq (invert op) op) Nop
144+
seqInverseLeft op s = reversibleDual op s
145+
146+
--------------------------------------------------------------------------------
147+
-- Uniqueness of inverses (a genuine group-theoretic consequence)
148+
--------------------------------------------------------------------------------
149+
150+
||| In a group, inverses are unique: if `cand` is a right inverse of `op`
151+
||| (i.e. `Equiv (Seq op cand) Nop`), then `cand` is denotationally `invert op`.
152+
||| This is the standard cancellation argument, carried out over `Equiv`:
153+
|||
154+
||| cand ~ Nop `Seq` cand
155+
||| ~ (invert op `Seq` op) `Seq` cand -- left inverse
156+
||| ~ invert op `Seq` (op `Seq` cand) -- associativity
157+
||| ~ invert op `Seq` Nop -- hypothesis (congruence)
158+
||| ~ invert op -- right unit
159+
export
160+
inverseUnique : (op, cand : Op) ->
161+
Equiv (Seq op cand) Nop ->
162+
Equiv cand (invert op)
163+
inverseUnique op cand rightInv =
164+
equivTrans cand (Seq Nop cand) (invert op)
165+
(equivSym (Seq Nop cand) cand (nopLeftUnit cand)) $
166+
equivTrans (Seq Nop cand) (Seq (Seq (invert op) op) cand) (invert op)
167+
(seqCong Nop (Seq (invert op) op) cand cand
168+
(equivSym (Seq (invert op) op) Nop (seqInverseLeft op))
169+
(equivRefl cand)) $
170+
equivTrans (Seq (Seq (invert op) op) cand) (Seq (invert op) (Seq op cand))
171+
(invert op)
172+
(seqAssoc (invert op) op cand) $
173+
equivTrans (Seq (invert op) (Seq op cand)) (Seq (invert op) Nop) (invert op)
174+
(seqCong (invert op) (invert op) (Seq op cand) Nop
175+
(equivRefl (invert op)) rightInv) $
176+
nopRightUnit (invert op)
177+
178+
--------------------------------------------------------------------------------
179+
-- `invert` is an involution and an anti-homomorphism (up to `Equiv`)
180+
--------------------------------------------------------------------------------
181+
182+
||| `invert` is an INVOLUTION up to denotation: `Equiv (invert (invert op)) op`.
183+
||| Derived from uniqueness: `op` is a right inverse of `invert op` (that is
184+
||| exactly the LEFT-inverse law `Equiv (Seq (invert op) op) Nop`), so by
185+
||| `inverseUnique` it must be denotationally `invert (invert op)`.
186+
export
187+
invertInvolutiveEquiv : (op : Op) -> Equiv (invert (invert op)) op
188+
invertInvolutiveEquiv op =
189+
equivSym op (invert (invert op))
190+
(inverseUnique (invert op) op (seqInverseLeft op))
191+
192+
||| `invert` is an ANTI-HOMOMORPHISM: it reverses order under `Seq`.
193+
||| Holds definitionally — `invert (Seq p q) = Seq (invert q) (invert p)`.
194+
export
195+
invertAntiHom : (p, q : Op) ->
196+
Equiv (invert (Seq p q)) (Seq (invert q) (invert p))
197+
invertAntiHom p q s = Refl
198+
199+
--------------------------------------------------------------------------------
200+
-- A propositional GROUP certificate (cannot be forged)
201+
--------------------------------------------------------------------------------
202+
203+
||| A certificate bundling the two-sided-inverse group axioms for `op` against
204+
||| `inv`. There is exactly one constructor, taking the genuine proofs; no
205+
||| "group element with broken inverse" can be built.
206+
public export
207+
data IsGroupInverse : (op, inv : Op) -> Type where
208+
MkGroupInverse :
209+
(left : Equiv (Seq inv op) Nop) ->
210+
(right : Equiv (Seq op inv) Nop) ->
211+
IsGroupInverse op inv
212+
213+
||| Every operation, paired with `invert op`, satisfies the group axioms.
214+
export
215+
groupInverse : (op : Op) -> IsGroupInverse op (invert op)
216+
groupInverse op = MkGroupInverse (seqInverseLeft op) (seqInverseRight op)
217+
218+
||| Tie the group certificate back to the ABI `Result` codes. Because every
219+
||| operation has a genuine two-sided inverse, this is total and always `Ok`.
220+
export
221+
groupResult : (op : Op) -> Result
222+
groupResult op = case groupInverse op of
223+
MkGroupInverse _ _ => Ok
224+
225+
||| Soundness: `groupResult op = Ok` entails the actual group laws (it
226+
||| exhibits the real two-sided-inverse proofs — no vacuity).
227+
export
228+
groupResultSound : (op : Op) -> groupResult op = Ok ->
229+
( Equiv (Seq (invert op) op) Nop
230+
, Equiv (Seq op (invert op)) Nop )
231+
groupResultSound op _ = (seqInverseLeft op, seqInverseRight op)
232+
233+
--------------------------------------------------------------------------------
234+
-- A SOUND + COMPLETE decision procedure for agreement on a finite probe set
235+
--------------------------------------------------------------------------------
236+
237+
||| Pointwise agreement of two operations on a *given list of probe states*.
238+
||| This is the decidable, finitary shadow of full `Equiv`.
239+
public export
240+
AgreeOn : (probes : List State) -> Op -> Op -> Type
241+
AgreeOn probes p q = (s : State) -> Elem s probes -> apply p s = apply q s
242+
243+
||| `AgreeOn` is decidable for any concrete probe list, because each probe is a
244+
||| concrete `decEq` on `List Bool`. Sound (a `Yes` carries a real proof) and
245+
||| complete (a `No` carries a real refutation).
246+
export
247+
decAgreeOn : (probes : List State) -> (p, q : Op) -> Dec (AgreeOn probes p q)
248+
decAgreeOn [] p q = Yes (\_, prf => absurd prf)
249+
decAgreeOn (x :: xs) p q =
250+
case decEq (apply p x) (apply q x) of
251+
No contra => No (\agree => contra (agree x Here))
252+
Yes hereEq =>
253+
case decAgreeOn xs p q of
254+
No restNo =>
255+
No (\agree => restNo (\s, elemRest => agree s (There elemRest)))
256+
Yes restYes =>
257+
Yes (\s, elemPrf => case elemPrf of
258+
Here => hereEq
259+
There elemTl => restYes s elemTl)
260+
261+
--------------------------------------------------------------------------------
262+
-- POSITIVE controls (inhabited witnesses on concrete data)
263+
--------------------------------------------------------------------------------
264+
265+
||| Concrete operation reused from the family.
266+
sampleOp : Op
267+
sampleOp = Seq FlipAll (XorMask [True, False, True])
268+
269+
||| Positive control 1: the RIGHT-inverse group law on the concrete sample,
270+
||| on a concrete probe state, via the general theorem.
271+
posRightInverse : apply (Seq Invariants.sampleOp (invert Invariants.sampleOp))
272+
[True, False, True]
273+
= apply Nop [True, False, True]
274+
posRightInverse = seqInverseRight sampleOp [True, False, True]
275+
276+
||| Positive control 2: the LEFT-inverse group law on the concrete sample.
277+
posLeftInverse : apply (Seq (invert Invariants.sampleOp) Invariants.sampleOp)
278+
[False, True, False]
279+
= apply Nop [False, True, False]
280+
posLeftInverse = seqInverseLeft sampleOp [False, True, False]
281+
282+
||| Positive control 3: the RIGHT-inverse law on `Rev`, forced to reduce by
283+
||| pure computation with NO appeal to the general lemma. `apply (Seq Rev Rev)
284+
||| [True,False] = reverse (reverse [True,False]) = [True,False] = apply Nop …`.
285+
posRightInverseRev :
286+
apply (Seq Rev (invert Rev)) [True, False] = apply Nop [True, False]
287+
posRightInverseRev = Refl
288+
289+
||| Positive control 4: associativity on a concrete instance, by pure
290+
||| computation (no appeal to the general lemma) — both sides reduce to
291+
||| `reverse (reverse (reverse [True,False]))`.
292+
posAssocConcrete :
293+
apply (Seq (Seq Rev Rev) Rev) [True, False]
294+
= apply (Seq Rev (Seq Rev Rev)) [True, False]
295+
posAssocConcrete = Refl
296+
297+
||| Positive control 5: an inhabited group certificate.
298+
posGroupCert : IsGroupInverse Invariants.sampleOp (invert Invariants.sampleOp)
299+
posGroupCert = groupInverse sampleOp
300+
301+
||| Positive control 6: the decision procedure returns `Yes` for an operation
302+
||| against itself on a non-empty probe set, and we can USE the proof.
303+
posDecYes : apply Rev [True, False] = apply Rev [True, False]
304+
posDecYes =
305+
case decAgreeOn [[True, False], [False]] Rev Rev of
306+
Yes agree => agree [True, False] Here
307+
No _ => Refl
308+
309+
--------------------------------------------------------------------------------
310+
-- NEGATIVE / non-vacuity controls (the bad case is genuinely refuted)
311+
--------------------------------------------------------------------------------
312+
313+
||| `apply Rev [True,False]` reduces to `[False,True]` (public `reverse`);
314+
||| stated as a concrete equality so the negative controls can pattern-match on
315+
||| a constructor-headed term.
316+
revReverses : apply Rev [True, False] = [False, True]
317+
revReverses = Refl
318+
319+
||| Negative control 1: `Rev` and `Nop` are NOT denotationally equal — they
320+
||| disagree on `[True,False]` (`apply Rev [True,False] = [False,True] /=
321+
||| [True,False] = apply Nop [True,False]`). A bogus `Equiv Rev Nop` would
322+
||| force a false equality; this `Not` machine-checks that none exists, so the
323+
||| unit law is non-vacuous.
324+
negRevNotNop : Not (apply Rev [True, False] = apply Nop [True, False])
325+
negRevNotNop eq =
326+
case trans (sym revReverses) eq of
327+
Refl impossible
328+
329+
||| Negative control 2: `Seq Nop Rev` is NOT a no-op — it reverses
330+
||| `[True,False]` to `[False,True]`, so it is NOT `[True,False]`. This refutes
331+
||| a bogus "Seq Nop Rev acts as the identity" claim.
332+
seqNopRevReverses : apply (Seq Nop Rev) [True, False] = [False, True]
333+
seqNopRevReverses = Refl
334+
335+
negSeqNopRevNotId : Not (apply (Seq Nop Rev) [True, False] = [True, False])
336+
negSeqNopRevNotId eq =
337+
case trans (sym seqNopRevReverses) eq of
338+
Refl impossible
339+
340+
||| Negative control 3: structural — `Rev` and `Nop` are distinct constructors,
341+
||| so they can never be propositionally equal as `Op`s. (Keeps the group
342+
||| carrier from collapsing to a single element.)
343+
negRevNotNopStruct : Not (Rev = Nop)
344+
negRevNotNopStruct Refl impossible
345+
346+
||| Negative control 4: the decision procedure genuinely DECIDES — `AgreeOn`
347+
||| for two operations that disagree on a probe (`Rev` vs `Nop` on
348+
||| `[True,False]`) is uninhabited, and we refute any forged agreement.
349+
negDecNo : Not (AgreeOn [[True, False]] Rev Nop)
350+
negDecNo agree = negRevNotNop (agree [True, False] Here)

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,3 +10,4 @@ modules = Oblibeniser.ABI.Types
1010
, Oblibeniser.ABI.Foreign
1111
, Oblibeniser.ABI.Proofs
1212
, Oblibeniser.ABI.Semantics
13+
, Oblibeniser.ABI.Invariants

0 commit comments

Comments
 (0)