Archive Clock Recovery

Abstract

Finite synchronized executions characterize archive-clock recovery and bound its first ambiguity.

Definition 1.1 (Finite partial-action systems).

$$\begin{array}{r}\forall X,A,Y:Type,\\ \mathrm{System}\left(X,A,Y\right)=\{D:A\to X\to Prop,F:A\to X\to X,\\ ell:\forall a:A,\forall x:X,D\left(a,x\right)\to Y,c:A\to X\to \mathbb{Z},\\ \forall a,x,\mathrm{Decidable}\left(D\left(a,x\right)\right)\}.\end{array}$$

Formalization. D5/S3/ObserverMemory/Algorithms/ArchiveClockRecovery.System (✓ std3).

Source. Repository-derived.

Commentary.

A system assigns to each action a decidable domain, a total successor and integer cost, and a reading defined only on that action’s domain. Values outside the domain never enter a legal execution, so this preserves the source partial-map model, including empty reading types and empty domains.

Definition 1.2 (State after an action word).

$$\begin{array}{r}\forall X,A,Y:Type,\forall S:\mathrm{System}\left(X,A,Y\right),\forall x:X,\\ \mathrm{stateAfter}\left(S,x,[]\right)=x,\\ \forall a:A,\forall w:\mathrm{List}\left(A\right),\mathrm{stateAfter}\left(S,x,\mathrm{cons}\left(a,w\right)\right)=\mathrm{stateAfter}\left(S,\mathrm{successor}\left(S,a,x\right),w\right).\end{array}$$

Formalization. D5/S3/ObserverMemory/Algorithms/ArchiveClockRecovery.stateAfter (✓ std3).

Source. Repository-derived.

Commentary.

The state after the empty word is the initial state. For a nonempty word, the first action changes the state and the remaining actions are then evaluated.

Definition 1.3 (Legal executions).

$$\begin{array}{r}\forall X,A,Y:Type,\forall S:\mathrm{System}\left(X,A,Y\right),\forall x:X,\\ \mathrm{Legal}\left(S,x,[]\right),\\ \forall a:A,\forall w:\mathrm{List}\left(A\right),(\mathrm{Legal}\left(S,x,\mathrm{cons}\left(a,w\right)\right))⟺((\mathrm{domain}\left(S,a,x\right))\wedge (\mathrm{Legal}\left(S,\mathrm{successor}\left(S,a,x\right),w\right))).\end{array}$$

Formalization. D5/S3/ObserverMemory/Algorithms/ArchiveClockRecovery.Legal (✓ std3).

Source. Repository-derived.

Commentary.

The empty execution is legal. A nonempty execution is legal exactly when its first action is defined at the current state and its tail is legal from the successor.

Definition 1.4 (Visible archives).

$$\begin{array}{r}\forall X,A,Y:Type,\forall S:\mathrm{System}\left(X,A,Y\right),\forall x:X,\\ \mathrm{visibleArchive}\left(S,x,[]\right)=[],\\ \forall a:A,\forall w:\mathrm{List}\left(A\right),\mathrm{visibleArchive}\left(S,x,\mathrm{cons}\left(a,w\right)\right)=\mathrm{dite}\left(\mathrm{domain}\left(S,a,x\right),\lambda h\mapsto \mathrm{cons}\left(\mathrm{pair}\left(a,\mathrm{reading}\left(S,a,x,h\right)\right),\mathrm{visibleArchive}\left(S,\mathrm{successor}\left(S,a,x\right),w\right)\right),\lambda h\mapsto []\right).\end{array}$$

Formalization. D5/S3/ObserverMemory/Algorithms/ArchiveClockRecovery.visibleArchive (✓ std3).

Source. Repository-derived.

Commentary.

Each execution step records the chosen action together with the reading produced at the state where that action is taken.

Definition 1.5 (Accumulated clock).

$$\begin{array}{r}\forall X,A,Y:Type,\forall S:\mathrm{System}\left(X,A,Y\right),\forall x:X,\\ \mathrm{clock}\left(S,x,[]\right)=0,\\ \forall a:A,\forall w:\mathrm{List}\left(A\right),\mathrm{clock}\left(S,x,\mathrm{cons}\left(a,w\right)\right)=\mathrm{cost}\left(S,a,x\right)+\mathrm{clock}\left(S,\mathrm{successor}\left(S,a,x\right),w\right).\end{array}$$

Formalization. D5/S3/ObserverMemory/Algorithms/ArchiveClockRecovery.clock (✓ std3).

Source. Repository-derived.

Commentary.

The clock of an execution is the sum of the integer costs of its actions at their successive source states.

Definition 1.6 (Synchronized edges).

$$\forall X,A,Y:Type,\forall S:\mathrm{System}\left(X,A,Y\right),\forall p:\mathrm{Prod}\left(X,X\right),\forall a:A,(\mathrm{SynchronizedEdge}\left(S,p,a\right))⟺(\exists h:\mathrm{domain}\left(S,a,\mathrm{fst}\left(p\right)\right),\exists h^{\prime }:\mathrm{domain}\left(S,a,\mathrm{snd}\left(p\right)\right),\mathrm{reading}\left(S,a,\mathrm{fst}\left(p\right),h\right)=\mathrm{reading}\left(S,a,\mathrm{snd}\left(p\right),h^{\prime }\right)).$$

Formalization. D5/S3/ObserverMemory/Algorithms/ArchiveClockRecovery.SynchronizedEdge (✓ std3).

Source. Repository-derived.

Commentary.

A synchronized edge applies one action legally to two states and requires the two visible readings for that action to agree.

Definition 1.7 (Synchronized paths).

$$\begin{array}{r}\forall X,A,Y:Type,\forall S:\mathrm{System}\left(X,A,Y\right),\forall x,x^{\prime }:X,\\ \mathrm{SynchronizedPath}\left(S,x,x^{\prime },[]\right),\\ \forall a:A,\forall w:\mathrm{List}\left(A\right),(\mathrm{SynchronizedPath}\left(S,x,x^{\prime },\mathrm{cons}\left(a,w\right)\right))⟺((\mathrm{SynchronizedEdge}\left(S,\mathrm{pair}\left(x,x^{\prime }\right),a\right))\wedge (\mathrm{SynchronizedPath}\left(S,\mathrm{successor}\left(S,a,x\right),\mathrm{successor}\left(S,a,x^{\prime }\right),w\right))).\end{array}$$

Formalization. D5/S3/ObserverMemory/Algorithms/ArchiveClockRecovery.SynchronizedPath (✓ std3).

Source. Repository-derived.

Commentary.

A synchronized path follows the same action word from two states, with a synchronized edge at every step.

Definition 1.8 (Synchronized pair traces).

$$\begin{array}{r}\forall X,A,Y:Type,\forall S:\mathrm{System}\left(X,A,Y\right),\forall x,x^{\prime }:X,\\ \mathrm{pairTrace}\left(S,x,x^{\prime },[]\right)=\mathrm{singleton}\left(\mathrm{pair}\left(x,x^{\prime }\right)\right),\\ \forall a:A,\forall w:\mathrm{List}\left(A\right),\mathrm{pairTrace}\left(S,x,x^{\prime },\mathrm{cons}\left(a,w\right)\right)=\mathrm{cons}\left(\mathrm{pair}\left(x,x^{\prime }\right),\mathrm{pairTrace}\left(S,\mathrm{successor}\left(S,a,x\right),\mathrm{successor}\left(S,a,x^{\prime }\right),w\right)\right).\end{array}$$

Formalization. D5/S3/ObserverMemory/Algorithms/ArchiveClockRecovery.pairTrace (✓ std3).

Source. Repository-derived.

Commentary.

The pair trace contains the initial state pair and every successive pair reached by the common action word.

Definition 1.9 (Clock-difference sums).

$$\begin{array}{r}\forall X,A,Y:Type,\forall S:\mathrm{System}\left(X,A,Y\right),\forall x,x^{\prime }:X,\\ \mathrm{deltaSum}\left(S,x,x^{\prime },[]\right)=0,\\ \forall a:A,\forall w:\mathrm{List}\left(A\right),\mathrm{deltaSum}\left(S,x,x^{\prime },\mathrm{cons}\left(a,w\right)\right)=(\mathrm{cost}\left(S,a,x\right)-\mathrm{cost}\left(S,a,x^{\prime }\right))+\mathrm{deltaSum}\left(S,\mathrm{successor}\left(S,a,x\right),\mathrm{successor}\left(S,a,x^{\prime }\right),w\right).\end{array}$$

Formalization. D5/S3/ObserverMemory/Algorithms/ArchiveClockRecovery.deltaSum (✓ std3).

Source. Repository-derived.

Commentary.

The delta sum accumulates, edge by edge, the first execution’s cost minus the second execution’s cost.

Definition 1.10 (Synchronous reachability).

$$\begin{array}{r}\forall X,A,Y:Type,\forall S:\mathrm{System}\left(X,A,Y\right),\forall X0:\mathrm{Set}\left(X\right),\forall p:\mathrm{Prod}\left(X,X\right),\\ (\mathrm{SynchronouslyReachable}\left(S,X0,p\right))⟺(\exists x,x^{\prime }:X,\exists w:\mathrm{List}\left(A\right),(((x\in X0)\wedge (x^{\prime }\in X0))\wedge (\mathrm{SynchronizedPath}\left(S,x,x^{\prime },w\right)))\wedge (\mathrm{pair}\left(\mathrm{stateAfter}\left(S,x,w\right),\mathrm{stateAfter}\left(S,x^{\prime },w\right)\right)=p)).\end{array}$$

Formalization. D5/S3/ObserverMemory/Algorithms/ArchiveClockRecovery.SynchronouslyReachable (✓ std3).

Source. Repository-derived.

Commentary.

A pair is synchronously reachable when a common synchronized word carries two allowed initial states to that pair.

Definition 1.11 (Recovery from visible archives).

$$\begin{array}{r}\forall X,A,Y:Type,\forall S:\mathrm{System}\left(X,A,Y\right),\forall X0:\mathrm{Set}\left(X\right),\\ (\mathrm{ArchiveRecoverable}\left(S,X0\right))⟺(\exists Gamma:\mathrm{List}\left(\mathrm{Prod}\left(A,Y\right)\right)\to \mathbb{Z},\forall x:X,\forall w:\mathrm{List}\left(A\right),((x\in X0)\wedge (\mathrm{Legal}\left(S,x,w\right)))\Rightarrow (\mathrm{Gamma}\left(\mathrm{visibleArchive}\left(S,x,w\right)\right)=\mathrm{clock}\left(S,x,w\right))).\end{array}$$

Formalization. D5/S3/ObserverMemory/Algorithms/ArchiveClockRecovery.ArchiveRecoverable (✓ std3).

Source. Repository-derived.

Commentary.

Archive recoverability means that one integer-valued function of the visible archive equals the clock on every legal execution from every allowed initial state.

Theorem 1.12 (Archive recovery is equivalent to synchronized cost consistency).

$$\begin{array}{r}\forall X,A,Y:Type,\forall n:\mathbb{N},\\ \forall X0:\mathrm{Set}\left(X\right),\forall S:\mathrm{System}\left(X,A,Y\right),\\ (((\mathrm{Fintype}\left(X\right))\wedge ((\mathrm{Fintype}\left(A\right))\wedge (\mathrm{Fintype}\left(Y\right))))\wedge ((\mathrm{card}\left(X\right)=n)\wedge (\mathrm{Nonempty}\left(X0\right))))\Rightarrow ((((\mathrm{ArchiveRecoverable}\left(S,X0\right))⟺(\forall x,x^{\prime }:X,\forall w:\mathrm{List}\left(A\right),(((x\in X0)\wedge (x^{\prime }\in X0))\wedge (\mathrm{SynchronizedPath}\left(S,x,x^{\prime },w\right)))\Rightarrow (\mathrm{deltaSum}\left(S,x,x^{\prime },w\right)=0)))\wedge ((\forall x,x^{\prime }:X,\forall w:\mathrm{List}\left(A\right),(((x\in X0)\wedge (x^{\prime }\in X0))\wedge (\mathrm{SynchronizedPath}\left(S,x,x^{\prime },w\right)))\Rightarrow (\mathrm{deltaSum}\left(S,x,x^{\prime },w\right)=0))⟺(\forall p:\mathrm{Prod}\left(X,X\right),\forall a:A,((\mathrm{SynchronouslyReachable}\left(S,X0,p\right))\wedge (\mathrm{SynchronizedEdge}\left(S,p,a\right)))\Rightarrow (\mathrm{cost}\left(S,a,\mathrm{fst}\left(p\right)\right)-\mathrm{cost}\left(S,a,\mathrm{snd}\left(p\right)\right)=0))))\wedge ((\neg \mathrm{ArchiveRecoverable}\left(S,X0\right))\Rightarrow (\exists x,x^{\prime }:X,\exists w:\mathrm{List}\left(A\right),(((x\in X0)\wedge (x^{\prime }\in X0))\wedge ((\mathrm{Legal}\left(S,x,w\right))\wedge (\mathrm{Legal}\left(S,x^{\prime },w\right))))\wedge ((\mathrm{visibleArchive}\left(S,x,w\right)=\mathrm{visibleArchive}\left(S,x^{\prime },w\right))\wedge ((\mathrm{clock}\left(S,x,w\right)\ne \mathrm{clock}\left(S,x^{\prime },w\right))\wedge (\mathrm{length}\left(w\right)\le n^2)))))).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/ArchiveClockRecovery.archive_clock_recovery_and_finite_ambiguity (✓ std3). ∎

Source. Repository-derived.

Commentary.

For finite configuration, action, and reading types, with n configurations and a nonempty allowed initial set, three conditions are equivalent: a single archive decoder recovers every legal clock, every synchronized path from allowed initial states has zero delta sum, and every synchronized edge whose source pair is synchronously reachable has zero cost difference.

Two synchronized executions have the same visible archive, and their delta sum is exactly the difference of their clocks. Conversely, equality of visible archives synchronizes the two executions. Prefix subtraction turns zero path sums into zero reachable-edge differences.

If recovery fails, choose a shortest synchronized word reaching the source of a nonzero edge. A repeated state pair would allow the intervening loop to be removed while preserving legality, readings, and the endpoint, contradicting minimality. Thus its pair trace has at most n squared vertices. According to whether the prefix delta is already nonzero, the prefix or the prefix followed by the bad edge gives equal archives, unequal clocks, and common length at most n squared.

References

• Truth anchor: D5/S3/ObserverMemory/Algorithms/ArchiveClockRecovery.ArchiveRecoverable
• Truth anchor: D5/S3/ObserverMemory/Algorithms/ArchiveClockRecovery.Legal
• Truth anchor: D5/S3/ObserverMemory/Algorithms/ArchiveClockRecovery.SynchronizedEdge
• Truth anchor: D5/S3/ObserverMemory/Algorithms/ArchiveClockRecovery.SynchronizedPath
• Truth anchor: D5/S3/ObserverMemory/Algorithms/ArchiveClockRecovery.SynchronouslyReachable
• Truth anchor: D5/S3/ObserverMemory/Algorithms/ArchiveClockRecovery.System
• Truth anchor: D5/S3/ObserverMemory/Algorithms/ArchiveClockRecovery.archive_clock_recovery_and_finite_ambiguity
• Truth anchor: D5/S3/ObserverMemory/Algorithms/ArchiveClockRecovery.clock
• Truth anchor: D5/S3/ObserverMemory/Algorithms/ArchiveClockRecovery.deltaSum
• Truth anchor: D5/S3/ObserverMemory/Algorithms/ArchiveClockRecovery.pairTrace
• Truth anchor: D5/S3/ObserverMemory/Algorithms/ArchiveClockRecovery.stateAfter
• Truth anchor: D5/S3/ObserverMemory/Algorithms/ArchiveClockRecovery.visibleArchive