Skip to content

Commit de7135c

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
ABI Layer 3: consent withdrawal (revocation removes permission) (#54)
## Summary Layer 3 (second, deeper invariant): proves **consent withdrawal** — after revoking consent for an action, that action is no longer `Permitted` (revocation monotonicity). Complements (and is distinct from) the Layer-2 consent-grant theorem. New module `Wokelangiser.ABI.Invariants` (imports the Layer-2 `Semantics` model). Positive + non-vacuity controls. ## Testing Idris2 0.7.0 `--build` → exit 0, zero warnings. Adversarial rejection confirmed. `build/` removed. No `believe_me`/`postulate`/`sorry`. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --- _Generated by [Claude Code](https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx)_ --------- Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> Co-authored-by: Claude <noreply@anthropic.com>
1 parent f5025ed commit de7135c

2 files changed

Lines changed: 250 additions & 0 deletions

File tree

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

Lines changed: 249 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,249 @@
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 invariant proof for wokelangiser: consent *withdrawal*.
5+
|||
6+
||| Headline property (Layer 3 — distinct from and deeper than Layer 2):
7+
||| REVOCATION MONOTONICITY. The Layer-2 `Semantics` theorem is static — it
8+
||| says permission requires an `Active` record. This module reasons about a
9+
||| *state transition*: the `revoke` operation that withdraws consent (GDPR
10+
||| Article 7(3): "It shall be as easy to withdraw as to give consent"). We
11+
||| prove that AFTER revoking consent for an action, that action can never be
12+
||| `Permitted` — regardless of what the ledger said before, and regardless of
13+
||| how many prior (even Active) records exist for it. The withdrawal entry is
14+
||| authoritative because the resolver reads the most-recent record first.
15+
|||
16+
||| This is genuinely different from the grant theorem:
17+
||| * Layer 2: `Permitted env act` <=> `lookupConsent act env = Just Active`
18+
||| (a property of a *fixed* ledger).
19+
||| * Layer 3: for the *transformed* ledger `revoke act env`, permission is
20+
||| IMPOSSIBLE for `act`, and the transformation is monotone in the sense
21+
||| that it never re-enables a permission (a property of the *operation*).
22+
|||
23+
||| The module supplies, over the SAME model (`Action`, `Ledger`, `Permitted`,
24+
||| `lookupConsent` imported from `Semantics`):
25+
||| * `revoke` — the withdrawal operation (prepends a `Revoked` record);
26+
||| * `revokeResolvesRevoked` — after revoke, the lookup is `Just Revoked`;
27+
||| * `revokeDeniesPermission` — THE Layer-3 theorem: revoked => never Permitted;
28+
||| * `revokeOverridesActive` — even an explicit prior Active record is
29+
||| overridden (non-vacuity: the hard case really is handled);
30+
||| * `revokeIdempotent` — revoking twice resolves identically (algebraic law);
31+
||| * `revokePreservesOthers` — revoking `a` does not disturb a *different*
32+
||| action `b` (a non-interference / locality law, with a fresh-implicit-free
33+
||| signature);
34+
||| * a sound+complete `Dec` for "is this action revoked?";
35+
||| * a POSITIVE control (a concrete `IsRevoked` witness) and a NEGATIVE /
36+
||| non-vacuity control (`Not (Permitted (revoke ...) ...)` on a ledger that
37+
||| previously granted Active consent), both machine-checked.
38+
39+
module Wokelangiser.ABI.Invariants
40+
41+
import Wokelangiser.ABI.Types
42+
import Wokelangiser.ABI.Semantics
43+
import Decidable.Equality
44+
45+
%default total
46+
47+
--------------------------------------------------------------------------------
48+
-- decEq reflexivity helper (decEq on Action does not reduce definitionally)
49+
--------------------------------------------------------------------------------
50+
51+
||| For any action, `decEq act act` is a `Yes`. We need this because the resolver
52+
||| branches on `decEq`, which does not reduce for a symbolic `act` (idiom 4).
53+
||| Proven by exhaustive case analysis over the four constructors — no cheats.
54+
private
55+
decEqActSelf : (act : Action) -> (p : (act = act) ** decEq act act = Yes p)
56+
decEqActSelf Collect = (Refl ** Refl)
57+
decEqActSelf Process = (Refl ** Refl)
58+
decEqActSelf Share = (Refl ** Refl)
59+
decEqActSelf Store = (Refl ** Refl)
60+
61+
--------------------------------------------------------------------------------
62+
-- The withdrawal operation
63+
--------------------------------------------------------------------------------
64+
65+
||| Withdraw consent for `act`: record a fresh `Revoked` entry at the head of the
66+
||| ledger. Because `lookupConsent` returns the FIRST matching entry, this new
67+
||| record is authoritative and shadows every earlier record for `act`. This is
68+
||| the operational meaning of GDPR Art. 7(3) withdrawal in this model.
69+
public export
70+
revoke : Action -> Ledger -> Ledger
71+
revoke act env = MkEntry act Revoked :: env
72+
73+
--------------------------------------------------------------------------------
74+
-- Core resolution lemma after withdrawal
75+
--------------------------------------------------------------------------------
76+
77+
||| After withdrawing consent for `act`, the ledger resolves `act` to
78+
||| `Just Revoked`. Proven by forcing the head `decEq act act` branch via
79+
||| `decEqActSelf` and rewriting (idiom 4: cannot rely on `Refl` through decEq).
80+
public export
81+
revokeResolvesRevoked :
82+
(act : Action) -> (env : Ledger) ->
83+
lookupConsent act (revoke act env) = Just Revoked
84+
revokeResolvesRevoked act env =
85+
let (p ** eq) = decEqActSelf act in
86+
-- lookupConsent act (MkEntry act Revoked :: env)
87+
-- = case decEq act act of { Yes _ => Just Revoked; No _ => ... }
88+
rewrite eq in Refl
89+
90+
--------------------------------------------------------------------------------
91+
-- THE Layer-3 theorem: revocation monotonicity
92+
--------------------------------------------------------------------------------
93+
94+
||| Injectivity of `Just`, used to transport the stuck-lookup equality without a
95+
||| `case ... of Refl` on a stuck operand (idiom 3).
96+
private
97+
justInj' : {0 x, y : a} -> Just x = Just y -> x = y
98+
justInj' Refl = Refl
99+
100+
||| `Revoked = Active` is uninhabited; expose it as an explicit refutation.
101+
private
102+
revokedNotActive : Revoked = Active -> Void
103+
revokedNotActive Refl impossible
104+
105+
||| REVOCATION MONOTONICITY (headline). After consent for `act` is withdrawn,
106+
||| `act` is NOT `Permitted` under the resulting ledger — no matter what the
107+
||| prior ledger `env` recorded. A `Permitted` witness would force the resolved
108+
||| state to be `Active`, but withdrawal pins it to `Revoked`; the contradiction
109+
||| `Revoked = Active` discharges the case. This complements (does not restate)
110+
||| the Layer-2 grant theorem: that one characterised permission on a fixed
111+
||| ledger; this one proves the withdrawal *operation* removes permission.
112+
public export
113+
revokeDeniesPermission :
114+
(act : Action) -> (env : Ledger) ->
115+
Not (Permitted (revoke act env) act)
116+
revokeDeniesPermission act env (PermitActive prf) =
117+
-- prf : lookupConsent act (revoke act env) = Just Active
118+
-- revokeResolvesRevoked : lookupConsent act (revoke act env) = Just Revoked
119+
revokedNotActive
120+
(justInj' (trans (sym (revokeResolvesRevoked act env)) prf))
121+
122+
--------------------------------------------------------------------------------
123+
-- Non-vacuity: the HARD case (prior Active record) is genuinely overridden
124+
--------------------------------------------------------------------------------
125+
126+
||| Withdrawal overrides an explicit prior `Active` grant. This is the case that
127+
||| makes the theorem non-trivial: even if the data subject had previously
128+
||| activated consent, the fresh `Revoked` head shadows it. Demonstrates the
129+
||| resolver's "most-recent-wins" semantics actually does the work.
130+
public export
131+
revokeOverridesActive :
132+
(act : Action) -> (env : Ledger) ->
133+
lookupConsent act (revoke act (MkEntry act Active :: env)) = Just Revoked
134+
revokeOverridesActive act env = revokeResolvesRevoked act (MkEntry act Active :: env)
135+
136+
--------------------------------------------------------------------------------
137+
-- Algebraic law: withdrawal is idempotent at the resolution level
138+
--------------------------------------------------------------------------------
139+
140+
||| Withdrawing twice resolves the action exactly as withdrawing once does:
141+
||| both yield `Just Revoked`. (An idempotence law for the operation, distinct
142+
||| in shape from monotonicity.)
143+
public export
144+
revokeIdempotent :
145+
(act : Action) -> (env : Ledger) ->
146+
lookupConsent act (revoke act (revoke act env))
147+
= lookupConsent act (revoke act env)
148+
revokeIdempotent act env =
149+
trans (revokeResolvesRevoked act (revoke act env))
150+
(sym (revokeResolvesRevoked act env))
151+
152+
--------------------------------------------------------------------------------
153+
-- Locality / non-interference law
154+
--------------------------------------------------------------------------------
155+
156+
||| Withdrawing consent for one action does not disturb the resolution of a
157+
||| DIFFERENT action. If `a /= b`, then looking up `b` after revoking `a` gives
158+
||| the same answer as before. The head `MkEntry a Revoked` is skipped because
159+
||| `decEq b a = No _`. (`a`, `b` bound explicitly — no fresh-implicit warning,
160+
||| idiom 1.)
161+
public export
162+
revokePreservesOthers :
163+
(a : Action) -> (b : Action) -> (env : Ledger) ->
164+
Not (b = a) ->
165+
lookupConsent b (revoke a env) = lookupConsent b env
166+
revokePreservesOthers a b env neq with (decEq b a)
167+
revokePreservesOthers a b env neq | Yes prf = absurd (neq prf)
168+
revokePreservesOthers a b env neq | No _ = Refl
169+
170+
--------------------------------------------------------------------------------
171+
-- A decidable, sound+complete predicate: "is this action revoked here?"
172+
--------------------------------------------------------------------------------
173+
174+
||| `IsRevoked env act` witnesses that the ledger resolves `act` to `Revoked`.
175+
||| Sole constructor pins the lookup to `Just Revoked` (mirrors `Permitted`).
176+
public export
177+
data IsRevoked : (env : Ledger) -> (act : Action) -> Type where
178+
RevokedRecord :
179+
(prf : lookupConsent act env = Just Revoked) -> IsRevoked env act
180+
181+
||| Decide `IsRevoked env act`. Sound (`Yes` carries a real witness) and
182+
||| complete (`No` carries a refutation). The `with ... proof eq` pins the
183+
||| symbolic lookup so each branch can reason (idiom mirrors `decPermitted`).
184+
public export
185+
decIsRevoked : (env : Ledger) -> (act : Action) -> Dec (IsRevoked env act)
186+
decIsRevoked env act with (lookupConsent act env) proof eq
187+
_ | Just Revoked = Yes (RevokedRecord eq)
188+
_ | Just Active = No (\(RevokedRecord prf) =>
189+
case trans (sym prf) eq of Refl impossible)
190+
_ | Just Pending = No (\(RevokedRecord prf) =>
191+
case trans (sym prf) eq of Refl impossible)
192+
_ | Just Granted = No (\(RevokedRecord prf) =>
193+
case trans (sym prf) eq of Refl impossible)
194+
_ | Nothing = No (\(RevokedRecord prf) =>
195+
case trans (sym prf) eq of Refl impossible)
196+
197+
||| Bridge: a revoked action is never permitted (links the two predicates).
198+
||| If both held, the lookup would be `Just Revoked` and `Just Active` at once.
199+
public export
200+
revokedExcludesPermitted :
201+
(env : Ledger) -> (act : Action) ->
202+
IsRevoked env act -> Not (Permitted env act)
203+
revokedExcludesPermitted env act (RevokedRecord rprf) (PermitActive pprf) =
204+
revokedNotActive (justInj' (trans (sym rprf) pprf))
205+
206+
||| The withdrawal operation always produces an `IsRevoked` witness for its
207+
||| target — i.e. `revoke` is a constructor of revoked-state. Ties the operation
208+
||| to the decidable predicate.
209+
public export
210+
revokeProducesRevoked :
211+
(act : Action) -> (env : Ledger) -> IsRevoked (revoke act env) act
212+
revokeProducesRevoked act env = RevokedRecord (revokeResolvesRevoked act env)
213+
214+
--------------------------------------------------------------------------------
215+
-- POSITIVE control (inhabited witness)
216+
--------------------------------------------------------------------------------
217+
218+
||| A ledger that records ACTIVE consent for `Process` — the strongest possible
219+
||| prior state, so the controls exercise the override path.
220+
public export
221+
priorLedger : Ledger
222+
priorLedger = [ MkEntry Process Active ]
223+
224+
||| POSITIVE control: after withdrawal, `Process` is recorded `Revoked`, and we
225+
||| exhibit a concrete `IsRevoked` witness for it (lookup reduces on data).
226+
public export
227+
processRevoked : IsRevoked (revoke Process Invariants.priorLedger) Process
228+
processRevoked = RevokedRecord Refl
229+
230+
--------------------------------------------------------------------------------
231+
-- NEGATIVE / non-vacuity controls (machine-checked refutations)
232+
--------------------------------------------------------------------------------
233+
234+
||| NEGATIVE control (the crux): `Process` WAS Active in `priorLedger` (so the
235+
||| Layer-2 theorem would grant it there), yet after `revoke Process` it is NOT
236+
||| `Permitted`. This is the concrete instance of revocation monotonicity over
237+
||| the override case — proving the theorem is non-vacuous.
238+
public export
239+
processNotPermittedAfterRevoke :
240+
Not (Permitted (revoke Process Invariants.priorLedger) Process)
241+
processNotPermittedAfterRevoke = revokeDeniesPermission Process Invariants.priorLedger
242+
243+
||| Sanity / non-vacuity counter-check: BEFORE withdrawal the same action IS
244+
||| permitted in `priorLedger` (concrete `Permitted` witness). Together with the
245+
||| control above this shows `revoke` genuinely *changes* the verdict — it is not
246+
||| vacuously denying an already-denied action.
247+
public export
248+
processPermittedBeforeRevoke : Permitted Invariants.priorLedger Process
249+
processPermittedBeforeRevoke = PermitActive Refl

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

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

0 commit comments

Comments
 (0)