Rollback

This module formalises rollback of an event on a configuration: a maximal sub-configuration omitting the chosen event. It shows the canonical rollback (removing the future of the event) is the unique rollback, proves redoability and causal safety, and—given a finite representation—correctness (the original configuration is reachable from the rollback) and minimality.

def EventStructures.Rollback.isRollback (es : EventStructure) (c : Conf es) (e : es.Event) (m : Conf es) : Prop

A rollback of event e on configuration c is a maximal configuration m with m ⊆ c and e ∉ m.

Equations

• EventStructures.Rollback.isRollback es c e m = (↑m ⊆ ↑c ∧ e ∉ ↑m ∧ ∀ (m' : EventStructures.Conf es), ↑m' ⊆ ↑c → e ∉ ↑m' → ↑m ⊆ ↑m' → ↑m' ⊆ ↑m)

def EventStructures.Rollback.Rollbacks (es : EventStructure) (c : Conf es) (e : es.Event) : Set (Conf es)

The set of all rollbacks of event e on configuration c.

Equations

• EventStructures.Rollback.Rollbacks es c e = {m : EventStructures.Conf es | EventStructures.Rollback.isRollback es c e m}

def EventStructures.Rollback.RollbackCandidates (es : EventStructure) (c : Conf es) (e : es.Event) : Set (Conf es)

Candidate configurations for rollback.

Equations

• EventStructures.Rollback.RollbackCandidates es c e = {m : EventStructures.Conf es | ↑m ⊆ ↑c ∧ e ∉ ↑m}

@[simp]

theorem EventStructures.Rollback.rollback_subset (es : EventStructure) {c : Conf es} {e : es.Event} {m : Conf es} (h : isRollback es c e m) : ↑m ⊆ ↑c

@[simp]

theorem EventStructures.Rollback.rollback_not_mem (es : EventStructure) {c : Conf es} {e : es.Event} {m : Conf es} (h : isRollback es c e m) : e ∉ ↑m

theorem EventStructures.Rollback.rollback_maximal (es : EventStructure) {c : Conf es} {e : es.Event} {m : Conf es} (h : isRollback es c e m) (m' : Conf es) : ↑m' ⊆ ↑c → e ∉ ↑m' → ↑m ⊆ ↑m' → ↑m' ⊆ ↑m

theorem EventStructures.Rollback.isRollback_iff_maximal (es : EventStructure) {c : Conf es} {e : es.Event} {m : Conf es} : isRollback es c e m ↔ m ∈ RollbackCandidates es c e ∧ ∀ m' ∈ RollbackCandidates es c e, ↑m ⊆ ↑m' → ↑m' ⊆ ↑m

theorem EventStructures.Rollback.rollback_subset_future (es : EventStructure) {c : Conf es} {e : es.Event} {m : Conf es} (h : isRollback es c e m) : ↑m ⊆ ↑c \ es.future e

theorem EventStructures.Rollback.rollback_future_isConf (es : EventStructure) {c : Conf es} {e : es.Event} : isConf es (↑c \ es.future e)

Removing the future of e from a configuration keeps it a configuration.

def EventStructures.Rollback.rollbackFuture (es : EventStructure) (c : Conf es) (e : es.Event) : Conf es

The canonical rollback configuration: remove all events causally after e.

Equations

• EventStructures.Rollback.rollbackFuture es c e = ⟨↑c \ es.future e, ⋯⟩

@[simp]

theorem EventStructures.Rollback.rollbackFuture_val (es : EventStructure) (c : Conf es) (e : es.Event) : ↑(rollbackFuture es c e) = ↑c \ es.future e

theorem EventStructures.Rollback.rollbackFuture_mem (es : EventStructure) {c : Conf es} {e x : es.Event} : x ∈ ↑(rollbackFuture es c e) ↔ x ∈ ↑c ∧ x ∉ es.future e

theorem EventStructures.Rollback.rollback_redoable (es : EventStructure) {c : Conf es} {e : es.Event} (he : e ∈ ↑c) : Configuration.enables es (↑(rollbackFuture es c e)) e

Redoability: e is enabled in rollback(c,e) when e ∈ c.

theorem EventStructures.Rollback.rollback_causal_safety (es : EventStructure) {c : Conf es} {e x : es.Event} : x ∈ ↑(rollbackFuture es c e) → x ∉ es.future e

Causal safety: Rollback removes exactly the causal consequences of e.

theorem EventStructures.Rollback.rollback_future (es : EventStructure) {c : Conf es} {e : es.Event} : isRollback es c e (rollbackFuture es c e)

The canonical rollback is a rollback for c and e.

@[simp]

theorem EventStructures.Rollback.rollback_eq_future (es : EventStructure) {c : Conf es} {e : es.Event} {m : Conf es} (h : isRollback es c e m) : ↑m = ↑c \ es.future e

Any rollback coincides with the canonical rollback.

theorem EventStructures.Rollback.rollback_unique (es : EventStructure) {c : Conf es} {e : es.Event} {m₁ m₂ : Conf es} (h₁ : isRollback es c e m₁) (h₂ : isRollback es c e m₂) : m₁ = m₂

Rollbacks are unique when they exist.

theorem EventStructures.Rollback.rollback_maximum (es : EventStructure) {c : Conf es} {e : es.Event} {m : Conf es} (h : isRollback es c e m) (m' : Conf es) : m' ∈ RollbackCandidates es c e → ↑m' ⊆ ↑m

The rollback is the maximum element among rollback candidates.

theorem EventStructures.Rollback.event_enabled_when_past_present (es : EventStructure) {c : Conf es} {e x : es.Event} (hx : x ∈ ↑c ∩ es.future e) (c' : Conf es) (hxnot : x ∉ ↑c') (hpast : ∀ y < x, y ∈ ↑c ∩ es.future e → y ∈ ↑c') (hbase : ↑(rollbackFuture es c e) ⊆ ↑c') (hconf : ↑c' ⊆ ↑c) : Configuration.enables es (↑c') x

Helper: An event in the future that is not yet in a partial configuration is enabled there, provided the partial configuration contains its strict past and is consistent.

theorem EventStructures.Rollback.execList_exists_finite (es : EventStructure) [DecidableEventStructure es] {c : Conf es} {e : es.Event} (cF : Finset es.Event) (hcF : ∀ (x : es.Event), x ∈ cF ↔ x ∈ ↑c) : Nonempty ((t : List es.Event) × Path.ExecList es (rollbackFuture es c e) t c)

Constructive: given a Finset representation cF of the underlying configuration c, there is an executable list from the rollback configuration to c. Uses decidable equality and decidable strict order on events.

theorem EventStructures.Rollback.rollback_correctness_finite (es : EventStructure) [DecidableEventStructure es] {c : Conf es} {e : es.Event} (cF : Finset es.Event) (hcF : ∀ (x : es.Event), x ∈ cF ↔ x ∈ ↑c) : Nonempty (Path es (rollbackFuture es c e) c)

Correctness: the original configuration c is reachable from rollback(c,e) when c.1 admits a Finset representation.

theorem EventStructures.Rollback.rollback_minimality (es : EventStructure) {c : Conf es} {e : es.Event} {c' : Conf es} (_hredo : Configuration.enables es (↑c') e) (hsafe : ∀ x ∈ ↑c', x ∉ es.future e) (p' : Path es c' c) : (↑c ∩ es.future e).ncard ≤ Path.length es p'

Minimality of Rollback - Any path from a redo-candidate configuration c' to c is at least as long as the number of events in c causally after e.