Timeline editing by reset and replay

This is the elementary rebuilding transformation motivated by retroactive data structures Demaine, Iacono, and Langerman. A timeline edit is followed by an explicit reset and replay of the edited history. It is not an efficient rollback algorithm or a historical-query interface. Editing an admissible timeline can make later operations invalid, so admissibility checks the entire edited history.

Main definitions

• TimelineEdit: insertion and deletion by position.
• Retroactive.spec: the abstract timeline-editing specification.
• Retroactive.backend: an interface exposing edit, reset, and ordinary operations.
• Retroactive.implementation: the reusable rebuilding module.

Main results

• Retroactive.replay_run: replay has exactly the ordinary history's state and operations.
• Retroactive.operation_charge: costs include editing, reset, and the entire replay.
• Retroactive.realized_bound: the same bound transports to every backend realization.
• Retroactive.realized_linear_bound: an ordinary-operation bound gives linear replay overhead.

The edit primitive includes storing the timeline and exposing the edited list to its caller. A backend must certify this primitive's resource weight; list copying is not assumed constant time. Like all Spec.Client results, the resource claims count explicit backend operations and leave pure Lean controller computation uncharged. There is no fixed Word-RAM compiler here.

References

• E. D. Demaine, J. Iacono, and S. Langerman, Retroactive Data Structures

inductive Cslib.Algorithms.Lean.TimelineEdit (Op : Type) : Type

An edit position names a gap for insertion and an existing entry for deletion.

• insert {Op : Type} (position : ℕ) (operation : Op) : TimelineEdit Op
• erase {Op : Type} (position : ℕ) : TimelineEdit Op

def Cslib.Algorithms.Lean.TimelineEdit.apply {Op : Type} (e : TimelineEdit Op) (os : List Op) : List Op

Edit the operation sequence. Valid excludes out-of-range positions.

def Cslib.Algorithms.Lean.TimelineEdit.Valid {Op : Type} (e : TimelineEdit Op) (os : List Op) : Prop

Insertion allows the final gap; deletion requires an existing entry.

theorem Cslib.Algorithms.Lean.TimelineEdit.length_insert {Op : Type} (os : List Op) (i : ℕ) (o : Op) (hi : i ≤ os.length) : ((insert i o).apply os).length = os.length + 1

A valid insertion increases the timeline length by one.

theorem Cslib.Algorithms.Lean.TimelineEdit.length_erase {Op : Type} (os : List Op) (i : ℕ) (hi : i < os.length) : ((erase i).apply os).length + 1 = os.length

A valid deletion removes exactly one operation.

@[reducible, inline]

abbrev Cslib.Algorithms.Lean.Retroactive.spec (D : Stateful.Spec) (initial : D.State) : Stateful.Spec

A dynamic specification of admissible timeline edits.

inductive Cslib.Algorithms.Lean.Retroactive.BackendOp (Op : Type) : Type

Primitive operations required by rebuilding; editing returns the entire new timeline.

• edit {Op : Type} (change : TimelineEdit Op) : BackendOp Op
• reset {Op : Type} : BackendOp Op
• execute {Op : Type} (operation : Op) : BackendOp Op

@[reducible, inline]

abbrev Cslib.Algorithms.Lean.Retroactive.backend (D : Stateful.Spec) (initial : D.State) : Stateful.Spec

The rebuilding backend tracks the stored timeline and current ordinary state separately.

def Cslib.Algorithms.Lean.Retroactive.replay (D : Stateful.Spec) (initial : D.State) : List D.Op → (backend D initial).Client Unit

Replay ordinary operations through explicitly charged backend calls.

def Cslib.Algorithms.Lean.Retroactive.methods (D : Stateful.Spec) (initial : D.State) : Stateful.Methods (spec D initial) (backend D initial)

Editing, reset, and replay are distinct calls in the interface client.

theorem Cslib.Algorithms.Lean.Retroactive.replay_run (D : Stateful.Spec) (initial : D.State) (timeline os : List D.Op) (s : D.State) : (backend D initial).runClient (timeline, s) (replay D initial os) = ((), (timeline, (D.run s os).1), List.map BackendOp.execute os)

Replay preserves the stored timeline and has precisely the original operation trace.

theorem Cslib.Algorithms.Lean.Retroactive.replay_valid (D : Stateful.Spec) (initial : D.State) (timeline os : List D.Op) (s : D.State) (h : D.ValidHistory s os) : (backend D initial).ValidHistory (timeline, s) (List.map BackendOp.execute os)

Every admissible ordinary history is admissible when executed through the backend.

def Cslib.Algorithms.Lean.Retroactive.implementation (D : Stateful.Spec) (initial : D.State) : Stateful.Module (spec D initial) (backend D initial)

Rebuilding correctness is independent of the implementation of reset, edit, and execution.

def Cslib.Algorithms.Lean.Retroactive.primitiveCharge (D : Stateful.Spec) (initial : D.State) (editCharge : List D.Op → TimelineEdit D.Op → ℕ) (resetCharge : ℕ) (ordinaryCharge : D.State → D.Op → ℕ) (s : (backend D initial).State) : (backend D initial).Op → ℕ

Separate charges for timeline editing, resetting, and ordinary operations.

theorem Cslib.Algorithms.Lean.Retroactive.replay_charge (D : Stateful.Spec) (initial : D.State) (editCharge : List D.Op → TimelineEdit D.Op → ℕ) (resetCharge : ℕ) (ordinaryCharge : D.State → D.Op → ℕ) (timeline os : List D.Op) (s : D.State) : (backend D initial).totalCost (primitiveCharge D initial editCharge resetCharge ordinaryCharge) (timeline, s) (List.map BackendOp.execute os) = D.totalCost ordinaryCharge s os

Charges for replay are exactly the charges for the ordinary history.

theorem Cslib.Algorithms.Lean.Retroactive.operation_charge (D : Stateful.Spec) (initial : D.State) (editCharge : List D.Op → TimelineEdit D.Op → ℕ) (resetCharge : ℕ) (ordinaryCharge : D.State → D.Op → ℕ) (timeline : List D.Op) (state : D.State) (e : TimelineEdit D.Op) : (backend D initial).totalCost (primitiveCharge D initial editCharge resetCharge ordinaryCharge) (timeline, state) ((backend D initial).runClient (timeline, state) (methods D initial e)).2.2 = editCharge timeline e + resetCharge + D.totalCost ordinaryCharge initial (e.apply timeline)

The full operation charge retains both editing and resetting overhead.

theorem Cslib.Algorithms.Lean.Retroactive.realized_bound (D : Stateful.Spec) (initial : D.State) {C Trace : Type} {exec : Stateful.Execution (backend D initial) C Trace} (R : Stateful.Realization (backend D initial) exec) (weight : Trace → ℕ) (editCharge : List D.Op → TimelineEdit D.Op → ℕ) (resetCharge : ℕ) (ordinaryCharge : D.State → D.Op → ℕ) (B : Stateful.Bound R weight (primitiveCharge D initial editCharge resetCharge ordinaryCharge)) : Stateful.Bound ((implementation D initial).realize R) (Stateful.total weight) fun (os : (spec D initial).State) (e : (spec D initial).Op) => editCharge os e + resetCharge + D.totalCost ordinaryCharge initial (TimelineEdit.apply e os)

Resource bounds transport to any realization of the backend interface. This certificate then composes across arbitrary admissible timeline edits via Bound.client.

theorem Cslib.Algorithms.Lean.Retroactive.realized_linear_bound (D : Stateful.Spec) (initial : D.State) {C Trace : Type} {exec : Stateful.Execution (backend D initial) C Trace} (R : Stateful.Realization (backend D initial) exec) (weight : Trace → ℕ) (editCharge : List D.Op → TimelineEdit D.Op → ℕ) (resetCharge : ℕ) (ordinaryCharge : D.State → D.Op → ℕ) (B : Stateful.Bound R weight (primitiveCharge D initial editCharge resetCharge ordinaryCharge)) (T : ℕ) (hT : ∀ (s : D.State) (o : D.Op), D.valid s o → ordinaryCharge s o ≤ T) : Stateful.Bound ((implementation D initial).realize R) (Stateful.total weight) fun (os : (spec D initial).State) (e : (spec D initial).Op) => editCharge os e + resetCharge + (TimelineEdit.apply e os).length * T

A uniform ordinary-operation bound gives linear replay overhead. Editing and resetting remain explicit, and the resulting certificate applies to every concrete operation execution.