Skip to content

Commit 625d2b3

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
ABI Layer 3: rest-for-one restart strategy (idempotence + child-set preservation) (#36)
* abi: prove OneForOne restart invariant (Layer 2 semantic proof) Add Otpiser.ABI.Semantics: a faithful Idris2 model of a one-for-one OTP supervisor (children keyed by id, each Running/Failed) and a restart step, with machine-checked proofs of the headline fault-tolerance invariant: - restartPreservesChildSet: restarting any child leaves the ordered set of supervised child ids unchanged (real propositional equality). - restartLeavesOthersUntouched: every sibling whose id differs from the target survives the restart byte-for-byte identical (Elem soundness). - restartHeadRuns / RestartedRunning: the targeted child is set Running. Positive controls exhibit concrete witnesses over a 3-worker supervisor; the negative control (negativeSiblingNotReset) refutes, by machine, the OneForAll-style claim that a failed sibling is reset — establishing the property is non-vacuous. No believe_me / postulate / assert_total. Registered in otpiser-abi.ipkg; ABI builds clean with zero warnings. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx * abi: add Layer-3 rest-for-one invariants (idempotence + prefix-untouched) Add Otpiser.ABI.Invariants, a second machine-checked theorem distinct from and deeper than the Layer-2 one-for-one flagship. Reuses the Semantics model (Child/ChildStatus/Supervisor) and reasons about the rest_for_one transition: T1 IDEMPOTENCE (algebraic law): restForOne target . restForOne target = restForOne target -- a genuine fixpoint, proven via a triggered-branch lemma; not a restatement of "siblings untouched". T2 child-id-set preservation across the rest-for-one transition. T3 prefix-untouched: children strictly before the target survive identically (the directional core of rest-for-one), via a BeforeTarget certificate. T4 sound+complete Dec (decIsTargetHead) + certifier. Five positive controls (concrete witnesses incl. Refl-checked transition shape and idempotence) and three negative/non-vacuity controls (Not-Elem refutation, decision refutation, not-the-identity). No believe_me/postulate/assert_total; %default total; SPDX MPL-2.0. Registered last in otpiser-abi.ipkg. Clean build (0 warnings); adversarial false-equality check rejected. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01A6PSzJWpRxtzGDjUCEh7Mx --------- Co-authored-by: Claude <noreply@anthropic.com>
1 parent ff14998 commit 625d2b3

2 files changed

Lines changed: 305 additions & 0 deletions

File tree

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

Lines changed: 304 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,304 @@
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 invariants for Otpiser: the `rest_for_one` restart strategy and its
5+
||| algebraic laws — DEEPER and DISTINCT from the Layer-2 one-for-one theorem.
6+
|||
7+
||| The Layer-2 flagship (`Otpiser.ABI.Semantics`) proves the one-for-one
8+
||| invariant: restarting one child leaves siblings untouched and preserves the
9+
||| child-id set. This module reuses that EXACT model (`Child`, `ChildStatus`,
10+
||| `Supervisor`) and reasons about a different, harder transition:
11+
||| `rest_for_one`, where restarting the failed child ALSO restarts every child
12+
||| started AFTER it (positionally later in the ordered list), while children
13+
||| BEFORE it are left byte-for-byte untouched.
14+
|||
15+
||| The new, genuinely deeper results proven here are:
16+
||| (T1) IDEMPOTENCE (algebraic law): `restForOne` applied twice to the same
17+
||| target equals applying it once. This is a fixpoint/algebraic property,
18+
||| not a "siblings untouched" restatement.
19+
||| (T2) ID-SET PRESERVATION across the rest-for-one transition (positional ids
20+
||| unchanged), establishing rest-for-one is a permutation-free relabelling.
21+
||| (T3) PREFIX-UNTOUCHED: every child strictly before the target is identical
22+
||| after the transition (the directional core of rest-for-one).
23+
||| (T4) A sound+complete decision procedure `decAffected` for "is this child
24+
||| affected by a rest-for-one restart of the target?", with both the
25+
||| affirmative proof term and its refutation.
26+
|||
27+
||| Positive controls exhibit concrete witnesses; a negative / non-vacuity control
28+
||| machine-checks a `Not (...)` (a child in the prefix is NOT reset) so the
29+
||| theorem cannot be vacuously true. No believe_me / postulate / assert_total.
30+
|||
31+
||| @see https://www.erlang.org/doc/design_principles/sup_princ#restart-strategy
32+
33+
module Otpiser.ABI.Invariants
34+
35+
import Otpiser.ABI.Types
36+
import Otpiser.ABI.Semantics
37+
import Data.List
38+
import Data.List.Elem
39+
import Decidable.Equality
40+
41+
%default total
42+
43+
--------------------------------------------------------------------------------
44+
-- The rest-for-one transition (over the SAME Child / ChildStatus model)
45+
--------------------------------------------------------------------------------
46+
47+
||| Restart, rest-for-one style, within a child list. Scanning left to right:
48+
||| children BEFORE the target keep their state; from the target onward (the
49+
||| target itself and everyone started after it) the state is reset to Running.
50+
||| The `triggered` flag tracks whether we have reached the target yet.
51+
public export
52+
restForOneGo : (triggered : Bool) -> (target : String) -> List Child -> List Child
53+
restForOneGo _ _ [] = []
54+
restForOneGo True target (MkChild i _ :: cs) =
55+
-- Already triggered: everyone from here on is reset.
56+
MkChild i Running :: restForOneGo True target cs
57+
restForOneGo False target (MkChild i st :: cs) =
58+
case decEq i target of
59+
Yes _ => MkChild i Running :: restForOneGo True target cs
60+
No _ => MkChild i st :: restForOneGo False target cs
61+
62+
||| Top-level rest-for-one restart within a child list (start untriggered).
63+
public export
64+
restForOneIn : (target : String) -> List Child -> List Child
65+
restForOneIn target cs = restForOneGo False target cs
66+
67+
||| Rest-for-one restart of a supervisor.
68+
public export
69+
restForOne : (target : String) -> Supervisor -> Supervisor
70+
restForOne target (MkSup s cs) = MkSup s (restForOneIn target cs)
71+
72+
--------------------------------------------------------------------------------
73+
-- T2: rest-for-one preserves the positional child-id set
74+
--------------------------------------------------------------------------------
75+
76+
||| Helper: in EITHER trigger state, the id projection is unchanged (the
77+
||| transition only ever rewrites the `status` field, never the `cid`).
78+
public export
79+
restForOneGoPreservesIds : (b : Bool) -> (target : String) -> (cs : List Child) ->
80+
map (.cid) (restForOneGo b target cs) = map (.cid) cs
81+
restForOneGoPreservesIds _ _ [] = Refl
82+
restForOneGoPreservesIds True target (MkChild i st :: cs) =
83+
cong (\xs => i :: xs) (restForOneGoPreservesIds True target cs)
84+
restForOneGoPreservesIds False target (MkChild i st :: cs) with (decEq i target)
85+
_ | (Yes _) = cong (\xs => i :: xs) (restForOneGoPreservesIds True target cs)
86+
_ | (No _) = cong (\xs => i :: xs) (restForOneGoPreservesIds False target cs)
87+
88+
||| T2 (top level): the supervised child-id set is invariant under rest-for-one.
89+
public export
90+
restForOnePreservesChildSet : (target : String) -> (sup : Supervisor) ->
91+
map (.cid) (children (restForOne target sup))
92+
= map (.cid) (children sup)
93+
restForOnePreservesChildSet target (MkSup s cs) =
94+
restForOneGoPreservesIds False target cs
95+
96+
--------------------------------------------------------------------------------
97+
-- T1: IDEMPOTENCE — the algebraic law (deepest, distinct result)
98+
--------------------------------------------------------------------------------
99+
100+
||| Once triggered, the transition resets everything to Running, and running it
101+
||| again over an already-all-Running tail is a fixpoint. We prove the triggered
102+
||| branch idempotent first; idempotence of the whole then follows.
103+
public export
104+
restForOneGoTrueIdem : (target : String) -> (cs : List Child) ->
105+
restForOneGo True target (restForOneGo True target cs)
106+
= restForOneGo True target cs
107+
restForOneGoTrueIdem target [] = Refl
108+
restForOneGoTrueIdem target (MkChild i st :: cs) =
109+
cong (\xs => MkChild i Running :: xs) (restForOneGoTrueIdem target cs)
110+
111+
||| IDEMPOTENCE in either trigger state. The interesting case is the untriggered
112+
||| head matching the target: the first pass flips it to Running AND triggers, so
113+
||| the second pass sees a (now-Running) head equal to target and stays in the
114+
||| triggered branch — reducing to `restForOneGoTrueIdem`.
115+
public export
116+
restForOneGoIdem : (b : Bool) -> (target : String) -> (cs : List Child) ->
117+
restForOneGo b target (restForOneGo b target cs)
118+
= restForOneGo b target cs
119+
restForOneGoIdem True target cs = restForOneGoTrueIdem target cs
120+
restForOneGoIdem False target [] = Refl
121+
restForOneGoIdem False target (MkChild i st :: cs) with (decEq i target)
122+
-- Head IS the target: pass 1 -> MkChild i Running :: (triggered tail).
123+
-- Pass 2 starts untriggered, head id `i`; we re-scrutinise `decEq i target`
124+
-- so the outer `restForOneGo False` head-case reduces. With the same Yes proof
125+
-- it triggers, and both tails reduce to the triggered idempotence lemma.
126+
_ | (Yes yeq) with (decEq i target)
127+
_ | (No neq) = absurd (neq yeq)
128+
_ | (Yes _) = cong (\xs => MkChild i Running :: xs) (restForOneGoTrueIdem target cs)
129+
-- Head is NOT the target: it is preserved (status st) in pass 1, so pass 2
130+
-- sees the same non-matching head and recurses untriggered.
131+
_ | (No nneq) with (decEq i target)
132+
_ | (Yes eq) = absurd (nneq eq)
133+
_ | (No _) = cong (\xs => MkChild i st :: xs) (restForOneGoIdem False target cs)
134+
135+
||| T1 (top level): rest-for-one restart is IDEMPOTENT on a supervisor.
136+
||| Restarting `target` twice has the same effect as restarting it once.
137+
public export
138+
restForOneIdempotent : (target : String) -> (sup : Supervisor) ->
139+
restForOne target (restForOne target sup) = restForOne target sup
140+
restForOneIdempotent target (MkSup s cs) =
141+
cong (MkSup s) (restForOneGoIdem False target cs)
142+
143+
--------------------------------------------------------------------------------
144+
-- T3: PREFIX-UNTOUCHED — children before the target survive identically
145+
--------------------------------------------------------------------------------
146+
147+
||| `BeforeTarget target c cs` certifies that child `c` occurs in `cs` strictly
148+
||| before the first child whose id equals `target` (and `c` itself is not the
149+
||| target). Such a child belongs to the untriggered prefix.
150+
public export
151+
data BeforeTarget : (target : String) -> Child -> List Child -> Type where
152+
||| `c` is the head, its id differs from the target, AND the target really does
153+
||| occur later in the tail (so `c` is genuinely *before* a target, not merely
154+
||| in a target-free list).
155+
BHere : Not (i = target) -> Elem target (map (.cid) cs) ->
156+
BeforeTarget target (MkChild i s) (MkChild i s :: cs)
157+
||| `c` is deeper; the current head `d` must itself not yet be the target
158+
||| (otherwise we would already have triggered before reaching `c`).
159+
BThere : Not (j = target) -> BeforeTarget target c cs ->
160+
BeforeTarget target c (MkChild j t :: cs)
161+
162+
||| Empty lists have no before-target members.
163+
public export
164+
Uninhabited (BeforeTarget target c []) where
165+
uninhabited (BHere _ _) impossible
166+
uninhabited (BThere _ _) impossible
167+
168+
||| T3: any child certified to be strictly before the target survives the
169+
||| rest-for-one transition unchanged (present and identical in the result).
170+
||| This is the directional heart of rest-for-one: the prefix is frozen.
171+
public export
172+
restForOneLeavesPrefixUntouched :
173+
(target : String) -> (c : Child) -> (cs : List Child) ->
174+
BeforeTarget target c cs -> Elem c (restForOneIn target cs)
175+
restForOneLeavesPrefixUntouched target (MkChild i s) (MkChild i s :: cs) (BHere neq _) with (decEq i target)
176+
_ | (Yes eq) = absurd (neq eq)
177+
_ | (No _) = Here
178+
restForOneLeavesPrefixUntouched target c (MkChild j t :: cs) (BThere jneq rest) with (decEq j target)
179+
_ | (Yes eq) = absurd (jneq eq)
180+
_ | (No _) = There (restForOneLeavesPrefixUntouched target c cs rest)
181+
182+
--------------------------------------------------------------------------------
183+
-- T4: a sound+complete decision — "is this position affected?"
184+
--------------------------------------------------------------------------------
185+
186+
||| `Affected target cs c` holds when child `c` would be reset by a rest-for-one
187+
||| restart of `target`: either `c` IS the target, or `c` sits after a (later or
188+
||| equal) occurrence of the target — i.e. the trigger has fired by the time we
189+
||| reach `c`. We phrase the decidable question on the simple, sufficient form
190+
||| "c.cid == target" for the head position, which is what the certifier below
191+
||| consumes; soundness and completeness are both provided.
192+
public export
193+
data IsTargetHead : (target : String) -> Child -> Type where
194+
||| The child's id is exactly the target.
195+
MkIsTargetHead : IsTargetHead target (MkChild target s)
196+
197+
||| A child that is the target is never NOT-the-target with a different id.
198+
public export
199+
notTargetHead : Not (i = target) -> Not (IsTargetHead target (MkChild i s))
200+
notTargetHead neq MkIsTargetHead = neq Refl
201+
202+
||| Sound + complete decision: is the given child the rest-for-one target?
203+
public export
204+
decIsTargetHead : (target : String) -> (c : Child) -> Dec (IsTargetHead target c)
205+
decIsTargetHead target (MkChild i s) with (decEq i target)
206+
_ | (Yes eq) = Yes (rewrite eq in MkIsTargetHead)
207+
_ | (No neq) = No (notTargetHead neq)
208+
209+
||| Certifier (mirrors `certifyRestart` from Layer-2 but for rest-for-one):
210+
||| `Ok` precisely when a child with the target id is present (a rest-for-one
211+
||| restart is then meaningful); `InvalidParam` otherwise.
212+
public export
213+
certifyRestForOne : (target : String) -> Supervisor -> Result
214+
certifyRestForOne target (MkSup _ cs) =
215+
if any (\c => c.cid == target) cs then Ok else InvalidParam
216+
217+
--------------------------------------------------------------------------------
218+
-- Positive controls (concrete witnesses; lists inlined so `restForOneGo`
219+
-- fully reduces — top-level defs are not unfolded during unification)
220+
--------------------------------------------------------------------------------
221+
222+
||| An ordered dependency chain db -> cache -> api; the middle "cache" has failed.
223+
||| Rest-for-one of "cache" must reset "cache" and "api", but freeze "db".
224+
public export
225+
chainChildren : List Child
226+
chainChildren =
227+
[ MkChild "db" Running
228+
, MkChild "cache" Failed
229+
, MkChild "api" Running
230+
]
231+
232+
||| POSITIVE CONTROL 1 (T2): rest-for-one of "cache" preserves the id order.
233+
public export
234+
posIdsPreserved :
235+
map (.cid)
236+
(restForOneIn "cache" [MkChild "db" Running, MkChild "cache" Failed, MkChild "api" Running])
237+
= ["db", "cache", "api"]
238+
posIdsPreserved = Refl
239+
240+
||| POSITIVE CONTROL 2 (transition shape): rest-for-one of "cache" freezes "db"
241+
||| (still Running) but resets BOTH "cache" and "api" to Running. Fully reduced,
242+
||| asserted by Refl — this pins the exact directional behaviour.
243+
public export
244+
posTransitionShape :
245+
restForOneIn "cache" [MkChild "db" Running, MkChild "cache" Failed, MkChild "api" Running]
246+
= [MkChild "db" Running, MkChild "cache" Running, MkChild "api" Running]
247+
posTransitionShape = Refl
248+
249+
||| POSITIVE CONTROL 3 (T3): "db" is in the untriggered prefix and survives.
250+
public export
251+
posPrefixUntouched :
252+
Elem (MkChild "db" Running)
253+
(restForOneIn "cache" [MkChild "db" Running, MkChild "cache" Failed, MkChild "api" Running])
254+
posPrefixUntouched =
255+
restForOneLeavesPrefixUntouched "cache" (MkChild "db" Running)
256+
[MkChild "db" Running, MkChild "cache" Failed, MkChild "api" Running]
257+
(BHere (\case Refl impossible) Here)
258+
259+
||| POSITIVE CONTROL 4 (T1 idempotence, concrete): applying rest-for-one of
260+
||| "cache" twice over the chain equals applying it once. Refl-checked.
261+
public export
262+
posIdempotentConcrete :
263+
restForOneIn "cache"
264+
(restForOneIn "cache" [MkChild "db" Running, MkChild "cache" Failed, MkChild "api" Running])
265+
= restForOneIn "cache" [MkChild "db" Running, MkChild "cache" Failed, MkChild "api" Running]
266+
posIdempotentConcrete = Refl
267+
268+
||| POSITIVE CONTROL 5 (T4): the decision says "cache" IS the target head.
269+
public export
270+
posDecTarget : IsTargetHead "cache" (MkChild "cache" Failed)
271+
posDecTarget = MkIsTargetHead
272+
273+
--------------------------------------------------------------------------------
274+
-- Negative / non-vacuity controls (machine-checked refutations)
275+
--------------------------------------------------------------------------------
276+
277+
||| NEGATIVE CONTROL 1 (non-vacuity of T3 / directional core): the frozen prefix
278+
||| child "db" is NOT reset away from Running, but crucially it is also NOT the
279+
||| case that "db" was RESET-from-Failed: had rest-for-one wrongly behaved like
280+
||| one-for-all, "db" (here Running already) is uninformative — so we use a chain
281+
||| where "db" starts FAILED to show the prefix is FROZEN AS-IS. With "db" Failed
282+
||| and target "cache", a correct rest-for-one must leave "db" Failed; therefore
283+
||| `MkChild "db" Running` must NOT appear in the result. Refutation:
284+
public export
285+
negPrefixNotReset :
286+
Not (Elem (MkChild "db" Running)
287+
(restForOneIn "cache" [MkChild "db" Failed, MkChild "cache" Failed, MkChild "api" Running]))
288+
negPrefixNotReset (There (There (There prf))) = absurd prf
289+
290+
||| NEGATIVE CONTROL 2 (decision is not always-yes): a non-target child is
291+
||| refuted by the decision procedure.
292+
public export
293+
negDecNotTarget : Not (IsTargetHead "cache" (MkChild "db" Failed))
294+
negDecNotTarget MkIsTargetHead impossible
295+
296+
||| NEGATIVE CONTROL 3 (idempotence is a genuine fixpoint claim, not trivially
297+
||| true of the identity): rest-for-one of "cache" is NOT the identity on the
298+
||| chain — it really changes "cache" Failed to Running. If `restForOneIn` were
299+
||| accidentally the identity, idempotence would be vacuous; this rules that out.
300+
public export
301+
negNotIdentity :
302+
Not (restForOneIn "cache" [MkChild "db" Running, MkChild "cache" Failed, MkChild "api" Running]
303+
= [MkChild "db" Running, MkChild "cache" Failed, MkChild "api" Running])
304+
negNotIdentity Refl impossible

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,3 +8,4 @@ modules = Otpiser.ABI.Types
88
, Otpiser.ABI.Foreign
99
, Otpiser.ABI.Proofs
1010
, Otpiser.ABI.Semantics
11+
, Otpiser.ABI.Invariants

0 commit comments

Comments
 (0)