diff --git a/lean/kv/Kv.lean b/lean/kv/Kv.lean index 44c82c80b0f..82160b35689 100644 --- a/lean/kv/Kv.lean +++ b/lean/kv/Kv.lean @@ -3,11 +3,8 @@ module -- shake: keep-all --deprecated_module: ignore public import Kv.Model public import Kv.Model.Transitions public import Kv.Model.Types -public import Kv.Proofs.Execution -public import Kv.Proofs.Invariants -public import Kv.Proofs.Model -public import Kv.Proofs.Properties -public import Kv.Proofs.Trace +public import Kv.Proofs.Reachable +public import Kv.Proofs.Replay public import Kv.Proofs.Witnesses public import Kv.Properties public import Kv.Properties.Invariants diff --git a/lean/kv/Kv/Proofs/Execution.lean b/lean/kv/Kv/Proofs/Execution.lean deleted file mode 100644 index 73a6bf95a77..00000000000 --- a/lean/kv/Kv/Proofs/Execution.lean +++ /dev/null @@ -1,78 +0,0 @@ --- Copyright (c) Microsoft Corporation. All rights reserved. --- Licensed under the Apache 2.0 License. - -module - -public import Kv.Model - -@[expose] public section - -/-! Links the shared `CCF.Execution` vocabulary to the model's executable `step` and `replay`. -/ - -namespace Kv.Proofs.Execution - -open Kv.Model - -theorem step_iff_transition (w next : World) (r : Record) - : transitionSystem.step w r = some next ↔ step w r = .ok next := by - simp only [transitionSystem] - cases step w r <;> simp [Except.toOption] - -theorem replay_iff_run (w final : World) (rs : List Record) - : CCF.Execution.Run transitionSystem w rs final ↔ replay w rs = .ok final := by - induction rs generalizing w with - | nil => - constructor - · intro run - cases run using @CCF.Execution.Run.casesOn transitionSystem - rfl - · intro accepted - cases accepted - exact .nil _ - | cons r rs ih => - constructor - · intro run - cases run using @CCF.Execution.Run.casesOn transitionSystem with - | cons transition rest => - simp only [replay, (step_iff_transition _ _ _).mp transition, Except.bind] - exact (ih _).mp rest - · intro accepted - simp only [replay] at accepted - cases accepted' : step w r with - | error failure => simp [accepted', Except.bind] at accepted - | ok next => - simp only [accepted', Except.bind] at accepted - exact .cons ((step_iff_transition _ _ _).mpr accepted') ((ih _).mpr accepted) - -theorem run_snoc {start before after : World} {rs : List Record} {r : Record} - (run : CCF.Execution.Run transitionSystem start rs before) - (transition : transitionSystem.step before r = some after) - : CCF.Execution.Run transitionSystem start (rs ++ [r]) after := by - induction run using @CCF.Execution.Run.rec transitionSystem with - | nil => exact .cons transition (.nil _) - | cons first _ ih => exact .cons first (ih transition) - -theorem run_reachable {start final : World} {rs : List Record} - (reachable : transitionSystem.Reachable start) - (run : CCF.Execution.Run transitionSystem start rs final) - : transitionSystem.Reachable final := by - induction run using @CCF.Execution.Run.rec transitionSystem with - | nil => exact reachable - | cons transition _ ih => exact ih (.step reachable transition) - -theorem reachable_iff_replay (w : World) - : transitionSystem.Reachable w ↔ ∃ rs, replay {} rs = .ok w := by - constructor - · intro reachable - induction reachable using @CCF.TransitionSystem.Reachable.rec transitionSystem with - | initial initialized => - cases initialized - exact ⟨[], rfl⟩ - | @step before after r _ transition ih => - obtain ⟨rs, accepted⟩ := ih - exact ⟨rs ++ ([r] : List Record), - (replay_iff_run _ _ _).mp (run_snoc ((replay_iff_run _ _ _).mpr accepted) transition)⟩ - · intro ⟨rs, accepted⟩ - exact run_reachable (.initial rfl) ((replay_iff_run {} w rs).mpr accepted) - -end Kv.Proofs.Execution diff --git a/lean/kv/Kv/Proofs/Invariants.lean b/lean/kv/Kv/Proofs/Invariants.lean deleted file mode 100644 index 4e520fd6562..00000000000 --- a/lean/kv/Kv/Proofs/Invariants.lean +++ /dev/null @@ -1,908 +0,0 @@ --- Copyright (c) Microsoft Corporation. All rights reserved. --- Licensed under the Apache 2.0 License. - -module - -public import Kv.Properties.Invariants -public import Kv.Proofs.Execution - -@[expose] public section - -/-! Initialisation and preservation of the executable model's separate state invariants. -/ - -namespace Kv.Proofs.Invariants - -open Kv.Model Kv.Properties - -/-- Executes operations in order with `normalStep` to reconstruct the normal view. -/ -def normalRun {M K V : Type} [DecidableEq M] [DecidableEq K] [DecidableEq V] - (snapshot : DB M K V) (n : Normal M K V) (ops : List (NormalOp M K V)) - : Option (Normal M K V) := - ops.foldlM (normalStep snapshot) n - -/-- Store histories are contiguous, headed by the current frame, and contain the global cut. -/ -structure StoreInvariant (s : Store) : Prop where - /-- Every frame follows by publishing writes to its predecessor. -/ - historyShape : History s.history s.head.version - /-- The head is the newest frame. -/ - headFirst : s.history.head? = some s.head - /-- The global version does not exceed the head. -/ - globalBound : s.global ≤ s.head.version - -/-- A global view is empty or was captured at a well-formed store's global cut. -/ -def GlobalInvariant (view : GlobalView) : Prop := - view.frame = {} ∨ ∃ s : Store, StoreInvariant s ∧ view.frame = atCut s s.global - -/-- Replaying an attempt's log from its pinned data reproduces its normal view. -/ -def NormalInvariant (t : Tx) : Prop := - match t.snapshot with - | none => t.normal = {} - | some _ => normalRun t.data {} t.normal.log = some t.normal - -/-- Consistency of an attempt's operation log and captured views. -/ -structure TxInvariant (t : Tx) : Prop where - /-- The operation log reproduces the normal view. -/ - normal : NormalInvariant t - /-- Each snapshot was captured from a well-formed store's head. -/ - snapshot - : ∀ snap, - t.snapshot = some snap → ∃ s : Store, StoreInvariant s ∧ snap.current = s.head - /-- Each acquired global view has valid provenance. -/ - globals : ∀ map view, find t.globalViews map = some view → GlobalInvariant view - -/-- Internal consistency of every live store and attempt. -/ -structure WorldInvariant (w : World) : Prop where - /-- Live stores have well-formed histories. -/ - stores : ∀ sid s, find w.stores sid = some s → StoreInvariant s - /-- Live attempts have valid logs and captured views. -/ - txs : ∀ tid t, find w.txs tid = some t → TxInvariant t - -/-- An attempt keeps its snapshot, pinned data and global views, and its invariant. -/ -structure Frozen (t next : Tx) : Prop where - /-- The captured snapshot is unchanged. -/ - snapshot : next.snapshot = t.snapshot - /-- The pinned local data is unchanged. -/ - data : next.data = t.data - /-- The captured global views are unchanged. -/ - globals : next.globalViews = t.globalViews - /-- The attempt invariant is preserved. -/ - valid : TxInvariant t → TxInvariant next - -/-- How an accepted event changes the live stores and attempts. -/ -inductive StepEffect (w : World) : Event → World → Prop - /-- Stores and attempts are unchanged. -/ - | same {e : Event} {next : World} (stores : next.stores = w.stores) - (txs : next.txs = w.txs) (noApply : ∀ sid, projectedApplication w sid e = []) - : StepEffect w e next - /-- A fresh store is created. -/ - | storeCreate {sid : Nat} {next : World} (stores : next.stores = set w.stores sid {}) - (txs : next.txs = w.txs) - : StepEffect w (.storeCreate sid) next - /-- A store is ended. -/ - | storeEnd {sid : Nat} {next : World} (stores : next.stores = erase w.stores sid) - (txs : next.txs = w.txs) - : StepEffect w (.storeEnd sid) next - /-- A fresh attempt is created. -/ - | txCreate {sid tid : Nat} {next : World} (stores : next.stores = w.stores) - (txs : next.txs = set w.txs tid { store := sid }) - : StepEffect w (.txCreate sid tid) next - /-- An attempt is ended. -/ - | txEnd {sid tid : Nat} {next : World} (stores : next.stores = w.stores) - (txs : next.txs = erase w.txs tid) - : StepEffect w (.txEnd sid tid) next - /-- A store is compacted. -/ - | compact {sid version requested : Nat} {next : World} {s : Store} - (store : storeOf w sid = .ok s) - (stores : next.stores = set w.stores sid (compactStore s requested)) - (txs : next.txs = w.txs) - : StepEffect w (.compact sid version requested) next - /-- A store is rolled back. -/ - | rollback {sid version requested term : Nat} {next : World} {s : Store} - (store : storeOf w sid = .ok s) - (stores : next.stores = set w.stores sid (rollbackStore s version term)) - (txs : next.txs = w.txs) - : StepEffect w (.rollback sid version requested term) next - /-- An attempt captures its snapshot; the store may learn its term. -/ - | snapshot {sid tid version global term : Nat} {next : World} {s established : Store} - {t : Tx} (store : storeOf w sid = .ok s) (history : established.history = s.history) - (head : established.head = s.head) (globalCut : established.global = s.global) - (tx : find w.txs tid = some t) (fresh : t.snapshot = none) - (stores : next.stores = set w.stores sid established) - (txs - : next.txs = set w.txs tid { t with snapshot := some { current := s.head, term } }) - : StepEffect w (.snapshot sid tid version global term) next - /-- An attempt acquires a map. -/ - | acquire {sid tid version global : Nat} {m : String} {next : World} {s : Store} - {t t' : Tx} (store : storeOf w sid = .ok s) (tx : txOf w sid tid = .ok t) - (accepted : acquireMap s t m version global = .ok t') - (stores : next.stores = w.stores) (txs : next.txs = set w.txs tid t') - : StepEffect w (.acquire sid tid m version global) next - /-- An attempt is applied to its store. -/ - | apply {sid tid version term : Nat} {writes : Pending} {next : World} {s new : Store} - {t : Tx} (store : storeOf w sid = .ok s) (tx : txOf w sid tid = .ok t) - (applied : tryApply s t = some new) (stores : next.stores = set w.stores sid new) - (txs : next.txs = set w.txs tid { t with phase := .applied version }) - : StepEffect w (.apply sid tid version term writes) next - /-- An attempt changes without moving its snapshot, pinned data or global views. -/ - | update {e : Event} {sid tid : Nat} {next : World} {t t' : Tx} - (tx : txOf w sid tid = .ok t) (frozen : Frozen t t') - (stores : next.stores = w.stores) (txs : next.txs = set w.txs tid t') - (noApply : ∀ sid, projectedApplication w sid e = []) - : StepEffect w e next - -variable {M K V : Type} - -theorem find_set_same [DecidableEq K] (xs : Assoc K V) (k : K) (v : V) - : find (set xs k v) k = some v := by - simp [Model.set, find] - -theorem find_erase_same [DecidableEq K] (xs : Assoc K V) (k : K) - : find (erase xs k) k = none := by - induction xs with - | nil => rfl - | cons p xs ih => - rcases p with ⟨a, v⟩ - by_cases h : a = k <;> simp_all [erase, find] - -theorem find_erase_other [DecidableEq K] (xs : Assoc K V) (a k : K) (h : a ≠ k) - : find (erase xs a) k = find xs k := by - induction xs with - | nil => rfl - | cons p xs ih => - rcases p with ⟨b, v⟩ - by_cases hba : b = a <;> by_cases hbk : b = k <;> simp_all [erase, find] - -theorem find_set_other [DecidableEq K] (xs : Assoc K V) (a k : K) (v : V) (h : a ≠ k) - : find (set xs a v) k = find xs k := by - simp [Model.set, find, h, find_erase_other xs a k h] - -theorem find_set_cases [DecidableEq K] (xs : Assoc K V) (id key : K) (v : V) - : find (set xs id v) key = if id = key then some v else find xs key := by - by_cases h : id = key <;> simp [h, find_set_same, find_set_other] - -theorem find_erase_cases [DecidableEq K] (xs : Assoc K V) (id key : K) - : find (erase xs id) key = if id = key then none else find xs key := by - by_cases h : id = key <;> simp [h, find_erase_same, find_erase_other] - -theorem normalRun_append [DecidableEq M] [DecidableEq K] [DecidableEq V] - (db : DB M K V) (n : Normal M K V) (a b : List (NormalOp M K V)) - : normalRun db n (a ++ b) - = (normalRun db n a).bind (fun next => normalRun db next b) := by - unfold normalRun - simp - -theorem normalStep_log [DecidableEq M] [DecidableEq K] [DecidableEq V] - (db : DB M K V) (n n' : Normal M K V) (op : NormalOp M K V) - (h : normalStep db n op = some n') - : n'.log = n.log ++ [op] := by - unfold normalStep at h - split at h - next => cases h; rfl - next => simp at h - -theorem normalRun_extend [DecidableEq M] [DecidableEq K] [DecidableEq V] - (db : DB M K V) (n n' : Normal M K V) (op : NormalOp M K V) - (before : normalRun db {} n.log = some n) - (one : normalStep db n op = some n') - : normalRun db {} n'.log = some n' := by - rw [normalStep_log db n n' op one, normalRun_append, before] - simp [normalRun, one] - -theorem History.bounded (fs : List Frame) (n : Nat) (h : History fs n) - : ∀ f ∈ fs, f.version ≤ n := by - induction h with - | zero => - intro g hg - have he : g = {} := List.mem_singleton.mp hg - subst g - exact Nat.le_refl 0 - | succ f n fs hv _effect _tail ih => - intro g hg - rcases List.mem_cons.mp hg with he | hm - · subst g; omega - · exact Nat.le_trans (ih g hm) (Nat.le_succ n) - -theorem History.cut (fs : List Frame) (n : Nat) (h : History fs n) - (cut : Nat) (hc : cut ≤ n) - : ∃ f, - fs.find? (fun f => f.version ≤ cut) = some f - ∧ f.version = cut - ∧ History (fs.filter fun f => f.version ≤ cut) cut - ∧ (fs.filter fun f => f.version ≤ cut).head? = some f := by - induction h with - | zero => - have hz : cut = 0 := by omega - subst cut - refine ⟨{}, ?_, rfl, ?_, ?_⟩ - · rfl - · exact .zero - · rfl - | succ f n fs hv effect tail ih => - by_cases he : cut = n + 1 - · subst cut - have hall : (f :: fs).filter (fun f => decide (f.version ≤ n + 1)) = f :: fs := by - apply List.filter_eq_self.mpr - intro g hg - simp only [decide_eq_true_eq] - exact History.bounded _ _ (.succ f n fs hv effect tail) g hg - refine ⟨f, by simp [List.find?, hv], hv, ?_, by simp [hall]⟩ - rw [hall] - exact .succ f n fs hv effect tail - · have hlt : ¬n + 1 ≤ cut := by omega - have hc' : cut ≤ n := by omega - obtain ⟨g, found, gv, shape, first⟩ := ih hc' - refine ⟨g, ?_, gv, ?_, ?_⟩ - · simpa [List.find?, hv, hlt] using found - · simpa [hv, hlt] using shape - · simpa [hv, hlt] using first - -theorem atCut_spec (s : Store) (valid : StoreInvariant s) - (cut : Nat) (hc : cut ≤ s.head.version) - : (atCut s cut).version = cut - ∧ History (s.history.filter fun f => f.version ≤ cut) cut - ∧ (s.history.filter fun f => f.version ≤ cut).head? = some (atCut s cut) := by - obtain ⟨f, found, version, shape, first⟩ := - History.cut s.history s.head.version valid.historyShape cut hc - simpa [atCut, found] using And.intro version (And.intro shape first) - -theorem operation_normal (t : Tx) (valid : NormalInvariant t) (snap : Snapshot) - (n : Normal String String String) (op : NormalOp String String String) - (hs : t.snapshot = some snap) - (hn : normalStep t.data t.normal op = some n) - : match t.snapshot with - | none => n = {} - | some _ => normalRun t.data {} n.log = some n := by - have old : normalRun t.data {} t.normal.log = some t.normal := by - simpa [NormalInvariant, hs] using valid - simpa [hs] using normalRun_extend t.data t.normal n op old hn - -theorem image_append (a b : Data) (m : String) - : image (a ++ b) m = image a m ++ image b m := by - simp [image] - -private theorem image_cons (name key : String) (cell : Cell String) (db : Data) - (m : String) - : image (((name, key), cell) :: db) m - = if name = m then (key, cell) :: image db m else image db m := by - unfold image - by_cases h : name = m - · simp only [List.filterMap_cons, h, ↓reduceIte] - · simp only [List.filterMap_cons, h, ↓reduceIte] - -theorem image_filter (db : Data) (m : String) (p : String → Bool) - : image (db.filter fun (a, _) => p a.1) m = if p m then image db m else [] := by - induction db with - | nil => split <;> rfl - | cons entry db ih => - obtain ⟨⟨name, key⟩, cell⟩ := entry - rw [List.filter_cons, image_cons] - by_cases h : name = m - · subst h - cases hp : p name - · simpa only [hp, Bool.false_eq_true, ite_false] using ih - · simp only [hp, ite_true, image_cons] - rw [ih, hp] - rfl - · cases hp : p name - · simpa only [hp, Bool.false_eq_true, ite_false, h] using ih - · simp only [hp, ite_true, image_cons, h, ite_false] - exact ih - -theorem pinData_other (db acquired : Data) (m other : String) (h : other ≠ m) - : image (pinData db m acquired) other = image db other := by - rw [pinData, image_append, image_filter db other (fun name => name != m), - image_filter acquired other (fun name => name == m)] - simp [h] - -theorem find_image (db : Data) (m key : String) - : find (image db m) key = find db (m, key) := by - induction db with - | nil => rfl - | cons entry db ih => - rcases entry with ⟨⟨name, k⟩, cell⟩ - by_cases hm : name = m <;> by_cases hk : k = key <;> - simp_all [image, find, Prod.mk.injEq] - -theorem normalStep_pinData (db acquired : Data) (m : String) - (n : Normal String String String) (op : NormalOp String String String) - (h : op.map ≠ m) - : normalStep (pinData db m acquired) n op = normalStep db n op := by - have hi := pinData_other db acquired m op.map h - cases op with - | read a v | previous a v => - have hf := congrArg (fun entries => find entries a.2) hi - simp only [NormalOp.map, find_image] at hf - change find (pinData db m acquired) a = find db a at hf - simp only [normalStep, observes, valueAt, previousAt, needs, hf] - rfl - | scan name entries => - change image (pinData db m acquired) name = image db name at hi - simp only [normalStep, observes, scanAt, needs, hi] - rfl - | write => rfl - -theorem normalRun_pinData (db acquired : Data) (m : String) - (n : Normal String String String) (ops : List (NormalOp String String String)) - (unused : ops.all (fun op => op.map != m) = true) - : normalRun (pinData db m acquired) n ops = normalRun db n ops := by - induction ops generalizing n with - | nil => rfl - | cons op ops ih => - have h : (op.map != m) = true ∧ ops.all (fun op => op.map != m) = true := by - simpa only [List.all_cons, Bool.and_eq_true] using unused - have other : op.map ≠ m := by simpa using h.1 - simp only [normalRun, List.foldlM_cons, normalStep_pinData db acquired m n op other] - cases normalStep db n op with - | none => rfl - | some next => exact ih next h.2 - -theorem acquisition_normal (t : Tx) (valid : NormalInvariant t) (m : String) - (acquired : Data) (unused : t.normal.log.all (fun op => op.map != m) = true) - : match t.snapshot with - | none => t.normal = {} - | some _ => - normalRun (pinData t.data m acquired) {} t.normal.log = some t.normal := by - cases hs : t.snapshot with - | none => simpa [NormalInvariant, hs] using valid - | some snap => - simpa [NormalInvariant, hs, - normalRun_pinData t.data acquired m {} t.normal.log unused] - using valid - -theorem snapshot_normal (t : Tx) (valid : NormalInvariant t) (data : Data) - (hs : t.snapshot = none) - : normalRun data {} t.normal.log = some t.normal := by - have hzero : t.normal = {} := by simpa [NormalInvariant, hs] using valid - simp [hzero, normalRun] - -theorem history_extension (s : Store) (valid : StoreInvariant s) (f : Frame) - (writes : Pending) (version : f.version = s.head.version + 1) - (data : f.data = publish s.head.data (s.head.version + 1) writes) - : History (f :: s.history) (s.head.version + 1) := - .succ f s.head.version s.history version - ⟨writes, by simpa only [valid.headFirst, Option.getD_some] using data⟩ - valid.historyShape - -theorem cut_history (s : Store) (valid : StoreInvariant s) - (cut : Nat) (within : cut ≤ s.head.version) - : History (s.history.filter fun f => f.version ≤ cut) (atCut s cut).version := by - have spec := atCut_spec s valid cut within - rw [spec.1] - exact spec.2.1 - -theorem cut_global_bound (s : Store) (valid : StoreInvariant s) (cut : Nat) - (within : cut ≤ s.head.version) (boundary : s.global ≤ cut) - : s.global ≤ (atCut s cut).version := by - rw [(atCut_spec s valid cut within).1] - exact boundary - -theorem store_initial : StoreInvariant {} := - ⟨.zero, rfl, Nat.le_refl 0⟩ - -theorem advance_invariant (s : Store) (valid : StoreInvariant s) (writes : Pending) - : StoreInvariant (advance s writes) := - ⟨ - history_extension s valid _ writes rfl rfl, - rfl, - Nat.le_trans valid.globalBound (Nat.le_succ _) - ⟩ - -theorem compact_invariant (s : Store) (valid : StoreInvariant s) (v : Nat) - : StoreInvariant (compactStore s v) := by - unfold compactStore - split - next within => - exact ⟨valid.historyShape, valid.headFirst, Nat.max_le.mpr ⟨valid.globalBound, within⟩⟩ - next => exact valid - -theorem rollback_invariant (s : Store) (valid : StoreInvariant s) (v term : Nat) - : StoreInvariant (rollbackStore s v term) := by - have within : rollbackCut s v ≤ s.head.version := - Nat.max_le.mpr ⟨valid.globalBound, Nat.min_le_left _ _⟩ - exact ⟨cut_history s valid _ within, (atCut_spec s valid _ within).2.2, - cut_global_bound s valid _ within (Nat.le_max_left _ _)⟩ - -theorem tx_initial (sid : Nat) : TxInvariant { store := sid } := by - refine ⟨rfl, ?_, ?_⟩ <;> simp [find] - -theorem runOp_invariant (t next : Tx) (valid : TxInvariant t) - (op : NormalOp String String String) (accepted : runOp t op = .ok next) - : TxInvariant next := by - simp only [runOp, Pure.pure, Except.pure] at accepted - split at accepted - next => contradiction - next snap hs => - split at accepted - next n hn => - cases accepted - exact ⟨operation_normal t valid.normal snap n op hs hn, valid.snapshot, valid.globals⟩ - next => contradiction - -theorem foldlM_invariant {A : Type} (items : List A) (f : Tx → A → Except Failure Tx) - (preserve : ∀ t a next, TxInvariant t → f t a = .ok next → TxInvariant next) - (t next : Tx) (valid : TxInvariant t) (accepted : items.foldlM f t = .ok next) - : TxInvariant next := by - induction items generalizing t with - | nil => cases accepted; exact valid - | cons a items ih => - simp only [List.foldlM_cons, Bind.bind, Except.bind] at accepted - cases one : f t a with - | error err => simp [one] at accepted - | ok middle => - exact ih middle (preserve t a middle valid one) (by simpa [one] using accepted) - -theorem clearWrites_invariant (t next : Tx) (valid : TxInvariant t) - (map : String) (entries : Assoc String String) - (accepted : clearWrites t map entries = .ok next) - : TxInvariant next := - foldlM_invariant entries _ - (fun t (key, _) next ht h => - runOp_invariant t next ht (.write (map, key) none) h) - t next valid accepted - -theorem captureGlobal_invariant (s : Store) (valid : StoreInvariant s) - (snap : Snapshot) (map : String) - : GlobalInvariant (captureGlobal s snap map) := by - dsimp only [captureGlobal] - split - · exact Or.inl rfl - · exact Or.inr ⟨s, valid, rfl⟩ - -theorem bind_ok {α β : Type} {x : Except Failure α} {f : α → Except Failure β} {b : β} - (h : (x >>= f) = .ok b) - : ∃ a, x = .ok a ∧ f a = .ok b := by - cases x with - | error => cases h - | ok a => exact ⟨a, rfl, h⟩ - -theorem pure_ok {α : Type} {a b : α} (h : (pure a : Except Failure α) = .ok b) - : a = b := by - cases h; rfl - -theorem withTx_ok {w next : World} {sid tid : Nat} {f : Tx → Except Failure Tx} - (h : withTx w sid tid f = .ok next) - : ∃ t t', - txOf w sid tid = .ok t - ∧ f t = .ok t' - ∧ next = { w with txs := set w.txs tid t' } := by - obtain ⟨t, tx, h⟩ := bind_ok h - obtain ⟨t', f, h⟩ := bind_ok h - exact ⟨t, t', tx, f, (pure_ok h).symm⟩ - -theorem present_ok {α : Type} {value : Option α} {message : String} {a : α} - (h : present value message = .ok a) - : value = some a := by - cases value with - | none => cases h - | some => cases h; rfl - -theorem require_ok {condition : Bool} {message : String} {u : Unit} - (h : require condition message = .ok u) - : condition = true := by - cases condition - · cases h - · rfl - -theorem expect_ok {condition : Bool} {message : String} {u : Unit} - (h : expect condition message = .ok u) - : condition = true := by - cases condition - · cases h - · rfl - -theorem acquireMap_ok {s : Store} {t next : Tx} {map : String} {version global : Nat} - (accepted : acquireMap s t map version global = .ok next) - : ∃ snap, - t.snapshot = some snap - ∧ find t.globalViews map = none - ∧ (version = (revision (captureGlobal s snap map).current map).version - ∧ global = (revision (captureGlobal s snap map).frame map).version) - ∧ t.normal.log.all (fun op => op.map != map) = true - ∧ next - = { - t with - globalViews := set t.globalViews map (captureGlobal s snap map) - data := pinData t.data map (captureGlobal s snap map).current.data - } := by - obtain ⟨_, -, accepted⟩ := bind_ok accepted - obtain ⟨_, -, accepted⟩ := bind_ok accepted - obtain ⟨snap, captured, accepted⟩ := bind_ok accepted - obtain ⟨_, fresh, accepted⟩ := bind_ok accepted - obtain ⟨_, versions, accepted⟩ := bind_ok accepted - obtain ⟨_, -, accepted⟩ := bind_ok accepted - split at accepted - next unused => - cases pure_ok accepted - have versions := expect_ok versions - simp only [Bool.and_eq_true, beq_iff_eq] at versions - exact ⟨snap, present_ok captured, Option.isNone_iff_eq_none.mp (require_ok fresh), versions, - unused, rfl⟩ - next => cases accepted - -theorem acquireMap_invariant (s : Store) (store : StoreInvariant s) - (t next : Tx) (valid : TxInvariant t) (map : String) (version global : Nat) - (accepted : acquireMap s t map version global = .ok next) - : TxInvariant next := by - obtain ⟨_, _, _, _, unused, rfl⟩ := acquireMap_ok accepted - refine ⟨acquisition_normal t valid.normal map _ unused, valid.snapshot, ?_⟩ - intro name view found - rw [find_set_cases] at found - split at found - · cases found - exact captureGlobal_invariant s store _ map - · exact valid.globals name view found - -theorem snapshot_invariant (s : Store) (store : StoreInvariant s) (term : Nat) - (t : Tx) (valid : TxInvariant t) (fresh : t.snapshot = none) - : TxInvariant { t with snapshot := some { current := s.head, term } } := by - refine ⟨snapshot_normal t valid.normal t.data fresh, ?_, valid.globals⟩ - intro snap captured - cases captured - exact ⟨s, store, rfl⟩ - -theorem tx_fields_invariant (t next : Tx) (valid : TxInvariant t) - (snapshot : next.snapshot = t.snapshot) (data : next.data = t.data) - (normal : next.normal = t.normal) (globals : next.globalViews = t.globalViews) - : TxInvariant next := by - rcases valid with ⟨hn, hs, hg⟩ - constructor - · simpa [NormalInvariant, snapshot, data, normal] using hn - · simpa [snapshot] using hs - · simpa [globals] using hg - -theorem lookup_set_invariant [DecidableEq K] (P : V → Prop) (xs : Assoc K V) - (valid : ∀ key value, find xs key = some value → P value) - (id : K) (value : V) (holds : P value) - : ∀ key next, find (set xs id value) key = some next → P next := by - intro key next found - rw [find_set_cases] at found - split at found - · cases found; exact holds - · exact valid key next found - -theorem lookup_erase_invariant [DecidableEq K] (P : V → Prop) (xs : Assoc K V) - (valid : ∀ key value, find xs key = some value → P value) (id : K) - : ∀ key next, find (erase xs id) key = some next → P next := by - intro key next found - rw [find_erase_cases] at found - split at found - · contradiction - · exact valid key next found - -theorem storeOf_invariant (w : World) (valid : WorldInvariant w) (sid : Nat) (s : Store) - (found : storeOf w sid = .ok s) - : StoreInvariant s := by - cases h : find w.stores sid <;> simp [storeOf, present, invalid, h] at found - next => cases found; exact valid.stores sid _ h - -theorem txOf_found (w : World) (sid tid : Nat) (t : Tx) (found : txOf w sid tid = .ok t) - : find w.txs tid = some t := by - obtain ⟨_, -, found⟩ := bind_ok found - obtain ⟨_, lookup, found⟩ := bind_ok found - obtain ⟨_, -, found⟩ := bind_ok found - cases pure_ok found - exact present_ok lookup - -theorem txOf_invariant (w : World) (valid : WorldInvariant w) (sid tid : Nat) (t : Tx) - (found : txOf w sid tid = .ok t) - : TxInvariant t := - valid.txs tid t (txOf_found w sid tid t found) - -theorem tryApply_invariant (s next : Store) (valid : StoreInvariant s) (t : Tx) - (applied : tryApply s t = some next) - : StoreInvariant next := by - unfold tryApply at applied - split at applied - · cases applied; exact advance_invariant s valid t.normal.writes - · contradiction - -theorem world_initial : WorldInvariant {} := by - constructor <;> simp [find] - -theorem Frozen.refl (t : Tx) : Frozen t t := ⟨rfl, rfl, rfl, id⟩ - -theorem Frozen.trans {a b c : Tx} (ab : Frozen a b) (bc : Frozen b c) : Frozen a c := - ⟨ - bc.snapshot.trans ab.snapshot, - bc.data.trans ab.data, - bc.globals.trans ab.globals, - bc.valid ∘ ab.valid - ⟩ - -theorem Frozen.fields {t next : Tx} (snapshot : next.snapshot = t.snapshot) - (data : next.data = t.data) (normal : next.normal = t.normal) - (globals : next.globalViews = t.globalViews) - : Frozen t next := - ⟨ - snapshot, - data, - globals, - fun valid => tx_fields_invariant t next valid snapshot data normal globals - ⟩ - -theorem runOp_frozen {t next : Tx} {op : NormalOp String String String} - (accepted : runOp t op = .ok next) - : Frozen t next := by - simp only [runOp, Pure.pure, Except.pure] at accepted - split at accepted - next => contradiction - next snap hs => - split at accepted - next n hn => - cases accepted - exact ⟨rfl, rfl, rfl, fun valid => - ⟨operation_normal t valid.normal snap n op hs hn, valid.snapshot, valid.globals⟩⟩ - next => contradiction - -theorem clearWrites_frozen {t next : Tx} {map : String} {entries : Assoc String String} - (accepted : clearWrites t map entries = .ok next) - : Frozen t next := by - unfold clearWrites at accepted - induction entries generalizing t with - | nil => cases accepted; exact Frozen.refl _ - | cons entry entries ih => - obtain ⟨middle, one, rest⟩ := bind_ok accepted - exact (runOp_frozen one).trans (ih rest) - -theorem StepEffect.withTx {w next : World} {e : Event} {sid tid : Nat} - {f : Tx → Except Failure Tx} (noApply : ∀ sid, projectedApplication w sid e = []) - (frozen : ∀ t t', f t = .ok t' → Frozen t t') - (accepted : withTx w sid tid f = .ok next) - : StepEffect w e next := by - obtain ⟨t, t', tx, h, rfl⟩ := withTx_ok accepted - exact .update tx (frozen t t' h) rfl rfl noApply - -theorem stepEvent_effect (w next : World) (e : Event) - (accepted : stepEvent w e = .ok next) - : StepEffect w e next := by - cases e with - | traceStart | caseBegin | caseEnd | subcaseBegin | subcaseEnd | traceEnd => - repeat obtain ⟨_, -, accepted⟩ := bind_ok accepted - cases pure_ok accepted - exact .same rfl rfl fun _ => rfl - | rollbackRejected => - repeat obtain ⟨_, -, accepted⟩ := bind_ok accepted - cases pure_ok accepted - exact .same rfl rfl fun _ => rfl - | unsupported => cases accepted - | storeCreate => - repeat obtain ⟨_, -, accepted⟩ := bind_ok accepted - cases pure_ok accepted - exact .storeCreate rfl rfl - | storeEnd => - repeat obtain ⟨_, -, accepted⟩ := bind_ok accepted - cases pure_ok accepted - exact .storeEnd rfl rfl - | txCreate => - repeat obtain ⟨_, -, accepted⟩ := bind_ok accepted - cases pure_ok accepted - exact .txCreate rfl rfl - | txEnd => - repeat obtain ⟨_, -, accepted⟩ := bind_ok accepted - cases pure_ok accepted - exact .txEnd rfl rfl - | compact => - obtain ⟨s, store, accepted⟩ := bind_ok accepted - repeat obtain ⟨_, -, accepted⟩ := bind_ok accepted - cases pure_ok accepted - exact .compact store rfl rfl - | rollback => - obtain ⟨s, store, accepted⟩ := bind_ok accepted - repeat obtain ⟨_, -, accepted⟩ := bind_ok accepted - cases pure_ok accepted - exact .rollback store rfl rfl - | snapshot sid tid version global term => - obtain ⟨s, store, accepted⟩ := bind_ok accepted - obtain ⟨t, t', tx, h, rfl⟩ := withTx_ok accepted - obtain ⟨_, -, h⟩ := bind_ok h - split at h - next fresh => - obtain ⟨_, -, h⟩ := bind_ok h - cases pure_ok h - have live := txOf_found _ sid tid t tx - exact .snapshot store (by split <;> rfl) (by split <;> rfl) (by split <;> rfl) - live fresh rfl rfl - next => cases h - | acquire => - obtain ⟨s, store, accepted⟩ := bind_ok accepted - obtain ⟨t, t', tx, h, rfl⟩ := withTx_ok accepted - exact .acquire store tx h rfl rfl - | apply => - obtain ⟨s, store, accepted⟩ := bind_ok accepted - obtain ⟨t, tx, accepted⟩ := bind_ok accepted - obtain ⟨_, -, accepted⟩ := bind_ok accepted - obtain ⟨_, -, accepted⟩ := bind_ok accepted - obtain ⟨_, -, accepted⟩ := bind_ok accepted - obtain ⟨_, -, accepted⟩ := bind_ok accepted - split at accepted - next new applied => - obtain ⟨_, same, accepted⟩ := bind_ok accepted - cases pure_ok same - obtain ⟨_, -, accepted⟩ := bind_ok accepted - cases pure_ok accepted - exact .apply store tx applied rfl rfl - next => - obtain ⟨_, rejected, -⟩ := bind_ok accepted - cases rejected - | get | has => - refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted - obtain ⟨_, -, h⟩ := bind_ok h - split at h - · repeat obtain ⟨_, -, h⟩ := bind_ok h - cases pure_ok h - exact .refl _ - · repeat obtain ⟨_, -, h⟩ := bind_ok h - exact runOp_frozen h - | previous | put | remove | size => - refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted - repeat obtain ⟨_, -, h⟩ := bind_ok h - exact runOp_frozen h - | range => - refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted - obtain ⟨_, -, h⟩ := bind_ok h - split at h - · obtain ⟨_, -, h⟩ := bind_ok h - cases pure_ok h - exact .refl _ - · obtain ⟨_, -, h⟩ := bind_ok h - exact runOp_frozen h - | clear => - refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted - obtain ⟨_, -, h⟩ := bind_ok h - obtain ⟨_, one, h⟩ := bind_ok h - exact (runOp_frozen one).trans (clearWrites_frozen h) - | foreachBegin => - refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted - obtain ⟨_, -, h⟩ := bind_ok h - obtain ⟨_, -, h⟩ := bind_ok h - obtain ⟨_, one, h⟩ := bind_ok h - cases pure_ok h - exact (runOp_frozen one).trans (.fields rfl rfl rfl rfl) - | foreachEntry | foreachContinue | foreachEnd => - refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted - obtain ⟨⟨_, _⟩, -, h⟩ := bind_ok h - repeat obtain ⟨_, -, h⟩ := bind_ok h - cases pure_ok h - exact .fields rfl rfl rfl rfl - | unavailable => - obtain ⟨_, -, accepted⟩ := bind_ok accepted - refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted - repeat obtain ⟨_, -, h⟩ := bind_ok h - cases pure_ok h - exact .fields rfl rfl rfl rfl - | commitBegin => - refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted - repeat obtain ⟨_, -, h⟩ := bind_ok h - cases pure_ok h - exact .fields rfl rfl rfl rfl - | commitResult => - refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted - split at h - next => - obtain ⟨_, -, h⟩ := bind_ok h - cases pure_ok h - exact .fields rfl rfl rfl rfl - next => - obtain ⟨_, -, h⟩ := bind_ok h - split at h - · obtain ⟨_, -, h⟩ := bind_ok h - cases pure_ok h - exact .fields rfl rfl rfl rfl - · cases pure_ok h - exact .fields rfl rfl rfl rfl - next => - obtain ⟨_, -, h⟩ := bind_ok h - cases pure_ok h - exact .fields rfl rfl rfl rfl - -theorem stepEvent_invariant (w next : World) (valid : WorldInvariant w) (e : Event) - (accepted : stepEvent w e = .ok next) - : WorldInvariant next := by - cases stepEvent_effect w next e accepted with - | same stores txs => - exact ⟨by rw [stores]; exact valid.stores, by rw [txs]; exact valid.txs⟩ - | storeCreate stores txs => - exact ⟨ - by rw [stores]; exact lookup_set_invariant _ _ valid.stores _ _ store_initial, - by rw [txs]; exact valid.txs - ⟩ - | storeEnd stores txs => - exact ⟨ - by rw [stores]; exact lookup_erase_invariant _ _ valid.stores _, - by rw [txs]; exact valid.txs - ⟩ - | txCreate stores txs => - exact ⟨ - by rw [stores]; exact valid.stores, - by rw [txs]; exact lookup_set_invariant _ _ valid.txs _ _ (tx_initial _) - ⟩ - | txEnd stores txs => - exact ⟨ - by rw [stores]; exact valid.stores, - by rw [txs]; exact lookup_erase_invariant _ _ valid.txs _ - ⟩ - | compact store stores txs => - exact ⟨ - by - rw [stores] - exact lookup_set_invariant _ _ valid.stores _ _ - (compact_invariant _ (storeOf_invariant w valid _ _ store) _), - by rw [txs]; exact valid.txs - ⟩ - | rollback store stores txs => - exact ⟨ - by - rw [stores] - exact lookup_set_invariant _ _ valid.stores _ _ - (rollback_invariant _ (storeOf_invariant w valid _ _ store) _ _), - by rw [txs]; exact valid.txs - ⟩ - | snapshot store history head globalCut tx fresh stores txs => - have shape := storeOf_invariant w valid _ _ store - refine ⟨?_, ?_⟩ - · rw [stores] - refine lookup_set_invariant _ _ valid.stores _ _ ⟨?_, ?_, ?_⟩ - · rw [history, head]; exact shape.historyShape - · rw [history, head]; exact shape.headFirst - · rw [globalCut, head]; exact shape.globalBound - · rw [txs] - exact lookup_set_invariant _ _ valid.txs _ _ - (snapshot_invariant _ shape _ _ (valid.txs _ _ tx) fresh) - | acquire store tx acquired stores txs => - exact ⟨ - by rw [stores]; exact valid.stores, - by - rw [txs] - exact lookup_set_invariant _ _ valid.txs _ _ - (acquireMap_invariant _ (storeOf_invariant w valid _ _ store) _ _ - (txOf_invariant w valid _ _ _ tx) _ _ _ acquired) - ⟩ - | apply store tx applied stores txs => - exact ⟨ - by - rw [stores] - exact lookup_set_invariant _ _ valid.stores _ _ - (tryApply_invariant _ _ (storeOf_invariant w valid _ _ store) _ applied), - by - rw [txs] - exact lookup_set_invariant _ _ valid.txs _ _ - (tx_fields_invariant _ _ (txOf_invariant w valid _ _ _ tx) rfl rfl rfl rfl) - ⟩ - | update tx frozen stores txs => - exact ⟨ - by rw [stores]; exact valid.stores, - by - rw [txs] - exact lookup_set_invariant _ _ valid.txs _ _ - (frozen.valid (txOf_invariant w valid _ _ _ tx)) - ⟩ - -theorem step_ok {w next : World} {r : Record} (accepted : step w r = .ok next) - : ∃ eventNext, - stepEvent w r.event = .ok eventNext - ∧ next = { eventNext with lastSeq := some r.seq, count := w.count + 1 } := by - obtain ⟨_, -, accepted⟩ := bind_ok accepted - obtain ⟨_, -, accepted⟩ := bind_ok accepted - obtain ⟨seq, event⟩ := r - dsimp only at accepted ⊢ - split at accepted <;> try split at accepted - all_goals first - | obtain ⟨_, invalid, -⟩ := bind_ok accepted; cases invalid - | obtain ⟨eventNext, event, accepted⟩ := bind_ok accepted - exact ⟨eventNext, event, (pure_ok accepted).symm⟩ - -theorem step_invariant (w next : World) (valid : WorldInvariant w) (r : Record) - (accepted : step w r = .ok next) - : WorldInvariant next := by - obtain ⟨_, event, rfl⟩ := step_ok accepted - have eventValid := stepEvent_invariant w _ valid r.event event - exact ⟨eventValid.stores, eventValid.txs⟩ - -theorem reachable_invariant (w : World) (reachable : transitionSystem.Reachable w) - : WorldInvariant w := by - induction reachable using @CCF.TransitionSystem.Reachable.rec transitionSystem with - | initial initialized => cases initialized; exact world_initial - | step _ transition ih => - exact step_invariant _ _ ih _ ((Execution.step_iff_transition _ _ _).mp transition) - -end Kv.Proofs.Invariants diff --git a/lean/kv/Kv/Proofs/Model.lean b/lean/kv/Kv/Proofs/Model.lean deleted file mode 100644 index 3ec2ef6e3a6..00000000000 --- a/lean/kv/Kv/Proofs/Model.lean +++ /dev/null @@ -1,424 +0,0 @@ --- Copyright (c) Microsoft Corporation. All rights reserved. --- Licensed under the Apache 2.0 License. - -module - -public import Kv.Proofs.Invariants - -@[expose] public section - -/-! Supporting lemmas and proof implementations for the executable KV model. -/ - -namespace Kv.Proofs.Model - -open Kv.Model Kv.Proofs.Invariants Kv.Properties - -section Generic -variable {M K V : Type} [DecidableEq M] [DecidableEq K] - -theorem find_image (db : DB M K V) (m : M) (key : K) - : find (image db m) key = find db (m, key) := by - induction db with - | nil => rfl - | cons entry db ih => - rcases entry with ⟨⟨map, k⟩, cell⟩ - by_cases hm : map = m <;> by_cases hk : k = key <;> - simp_all [image, find, Prod.mk.injEq] - -theorem empty_map_has_no_values (db : DB M K V) (m : M) (key : K) - (empty : image db m = []) - : find db (m, key) = none := by - rw [← find_image, empty] - rfl - -theorem erase_keys (xs : Assoc K V) (k : K) - : (erase xs k).map Prod.fst = (xs.map Prod.fst).filter (· != k) := - (List.filter_map (f := Prod.fst) (p := (· != k)) (l := xs)).symm - -theorem erase_unique (xs : Assoc K V) (k : K) (h : Kv.Properties.Unique xs) - : Kv.Properties.Unique (erase xs k) := by - unfold Kv.Properties.Unique - rw [erase_keys] - exact List.Pairwise.filter _ h - -theorem set_unique (xs : Assoc K V) (k : K) (v : V) (h : Kv.Properties.Unique xs) - : Kv.Properties.Unique (set xs k v) := by - simp only [Kv.Properties.Unique, Model.set, List.map_cons, List.nodup_cons] - constructor - · simp [erase_keys, eq_comm] - · exact erase_unique xs k h - -theorem publish_lookup (db : DB M K V) (version : Nat) (ws : Writes M K V) (a : Addr M K) - : find (publish db version ws) a - = match find ws a with - | none => find db a - | some none => none - | some (some v) => some { value := v, version } := by - induction ws with - | nil => rfl - | cons p ws ih => - rcases p with ⟨b, value⟩ - by_cases h : b = a - · subst b - cases value <;> simp [publish, find, find_set_same, find_erase_same] - · cases value <;> simp [publish, find, h, find_set_other, find_erase_other, ← ih, publish] - -theorem publish_unique (db : DB M K V) (version : Nat) (ws : Writes M K V) - (h : Kv.Properties.Unique db) - : Kv.Properties.Unique (publish db version ws) := by - induction ws with - | nil => exact h - | cons p ws ih => - rcases p with ⟨a, v⟩ - cases v with - | none => exact erase_unique _ a ih - | some value => exact set_unique _ a ⟨value, version⟩ ih - -theorem publication_noninterference (db : DB M K V) (version : Nat) - (ws : Writes M K V) (a : Addr M K) (h : find ws a = none) - : find (publish db version ws) a = find db a := by - simp [publish_lookup, h] - -theorem read_your_write (db : DB M K V) (ws : Writes M K V) (a : Addr M K) (v : V) - : valueAt db (set ws a (some v)) a = some v := by - simp [valueAt, find_set_same] - -theorem read_your_deletion (db : DB M K V) (ws : Writes M K V) (a : Addr M K) - : valueAt db (set ws a none) a = none := by - simp [valueAt, find_set_same] - -theorem absent_read (db : DB M K V) (ws : Writes M K V) (a : Addr M K) - (hw : find ws a = none) (hd : find db a = none) - : valueAt db ws a = none := by - simp [valueAt, hw, hd] - -theorem staged_noninterference (db : DB M K V) (ws : Writes M K V) - (a b : Addr M K) (v : Option V) (h : a ≠ b) - : valueAt db (set ws a v) b = valueAt db ws b := by - simp [valueAt, find_set_other ws a b v h] - -theorem previous_ignores_pending (db : DB M K V) (a : Addr M K) - : previousAt db a = (find db a).map Cell.version := - rfl - -variable [DecidableEq V] - -theorem validates_append (db : DB M K V) (a b : List (Dependency M K V)) - : validates db (a ++ b) = (validates db a && validates db b) := by - simp [validates] - -theorem serialStep_eq (base : DB M K V) (ws : Writes M K V) (op : NormalOp M K V) - : serialStep base ws op - = if observes base ws op then some (stage ws op) else none := by - cases op <;> simp [serialStep, observes, stage] - -theorem dependency_rebase (snapshot current : DB M K V) (ws : Writes M K V) - (op : NormalOp M K V) - (hv : validates current (needs snapshot ws op) = true) - : observes snapshot ws op = observes current ws op := by - cases op with - | read a v => - cases hw : find ws a with - | none => - have heq : find current a = find snapshot a := by - simpa [needs, hw, validates, Dependency.holds] using hv - simp [observes, valueAt, hw, heq] - | some value => simp [observes, valueAt, hw] - | previous a v => - have heq : find current a = find snapshot a := by - simpa [needs, validates, Dependency.holds] using hv - apply decide_eq_decide.mpr - simp only [previousAt, heq] - | scan m vs => - have heq : image current m = image snapshot m := by - simpa [needs, validates, Dependency.holds] using hv - apply decide_eq_decide.mpr - simp only [scanAt, heq] - | write _ _ => rfl - -theorem normalStep_prefix_valid (snapshot current : DB M K V) - (n n' : Normal M K V) (op : NormalOp M K V) - (hs : normalStep snapshot n op = some n') - (hv : validates current n'.deps = true) - : validates current n.deps = true := by - unfold normalStep at hs - split at hs - next h => - cases hs - have hh : validates current (needs snapshot n.writes op) = true ∧ - validates current n.deps = true := by simpa [validates_append] using hv - exact hh.2 - next h => simp at hs - -theorem normalStep_rebase (snapshot current : DB M K V) - (n n' : Normal M K V) (op : NormalOp M K V) - (hs : normalStep snapshot n op = some n') - (hv : validates current n'.deps = true) - : serialStep current n.writes op = some n'.writes := by - unfold normalStep at hs - split at hs - next h => - cases hs - have hh : validates current (needs snapshot n.writes op) = true ∧ - validates current n.deps = true := by simpa [validates_append] using hv - have hneeds := hh.1 - have hobs := dependency_rebase snapshot current n.writes op hneeds - rw [serialStep_eq, ← hobs] - simp [h] - next h => simp at hs - -theorem normalRun_prefix_valid (snapshot current : DB M K V) - (ops : List (NormalOp M K V)) (n n' : Normal M K V) - (hr : normalRun snapshot n ops = some n') - (hv : validates current n'.deps = true) - : validates current n.deps = true := by - induction ops generalizing n with - | nil => simp [normalRun] at hr; subst n'; exact hv - | cons op ops ih => - cases hs : normalStep snapshot n op with - | none => simp [normalRun, hs] at hr - | some next => - have ht : normalRun snapshot next ops = some n' := by - simpa [normalRun, hs] using hr - exact normalStep_prefix_valid snapshot current n next op hs (ih next ht) - -/-- Arbitrary finite OCC programs, including cross-map/absent/scan reads, -replay with identical observations immediately before their application. -The only rebase premise is the executable dependency check, not a serial oracle. -/ -theorem normalRun_serial (snapshot current : DB M K V) - (ops : List (NormalOp M K V)) (n n' : Normal M K V) - (hr : normalRun snapshot n ops = some n') - (hv : validates current n'.deps = true) - : serialRun current n.writes ops = some n'.writes := by - induction ops generalizing n with - | nil => simp [normalRun] at hr; subst n'; rfl - | cons op ops ih => - cases hs : normalStep snapshot n op with - | none => simp [normalRun, hs] at hr - | some next => - have ht : normalRun snapshot next ops = some n' := by - simpa [normalRun, hs] using hr - have hp := normalRun_prefix_valid snapshot current ops next n' ht hv - have hstep := normalStep_rebase snapshot current n next op hs hp - simp [serialRun, hstep, ih next ht] - -theorem validates_self (snapshot : DB M K V) (ws : Writes M K V) (op : NormalOp M K V) - : validates snapshot (needs snapshot ws op) = true := by - cases op <;> simp [needs, validates, Dependency.holds] - -theorem normalRun_snapshot_valid (snapshot : DB M K V) (ops : List (NormalOp M K V)) - (n n' : Normal M K V) - (hn : validates snapshot n.deps = true) - (hr : normalRun snapshot n ops = some n') - : validates snapshot n'.deps = true := by - induction ops generalizing n with - | nil => simp [normalRun] at hr; subst n'; exact hn - | cons op ops ih => - cases hs : normalStep snapshot n op with - | none => simp [normalRun, hs] at hr - | some next => - apply ih next - · unfold normalStep at hs - split at hs - next h => - cases hs - simp [validates_append, validates_self, hn] - next h => simp at hs - · simpa [normalRun, hs] using hr - -theorem readonly_snapshot_serial (snapshot : DB M K V) (ops : List (NormalOp M K V)) - (n : Normal M K V) (hr : normalRun snapshot {} ops = some n) - : serialRun snapshot [] ops = some n.writes := - normalRun_serial snapshot snapshot ops {} n hr - (normalRun_snapshot_valid snapshot ops {} n (by rfl) hr) - -end Generic - -theorem apply_atomic (s : Store) (writes : Pending) - : (advance s writes).head.data = publish s.head.data (s.head.version + 1) writes := - rfl - -theorem compact_preserves_head (s : Store) (v : Nat) - : (compactStore s v).head = s.head := by - unfold compactStore - split <;> rfl - -theorem compact_above_head_noop (s : Store) (v : Nat) (h : s.head.version < v) - : compactStore s v = s := by - simp [compactStore, Nat.not_le.mpr h] - -theorem runOp_preserves_snapshot (t next : Tx) (op : NormalOp String String String) - (h : runOp t op = .ok next) - : next.snapshot = t.snapshot := by - unfold runOp at h - split at h - next => simp [invalid] at h - next snap _ => - split at h - next n _ => - simp [Pure.pure, Except.pure] at h - cases h - rfl - next => simp [reject] at h - -theorem rollback_preserves_earlier_cuts (s : Store) (v term cut : Nat) - (hcut : cut ≤ v) (hhead : cut ≤ s.head.version) - : atCut (rollbackStore s v term) cut = atCut s cut := by - have hmono : ∀ f : Frame, f.version ≤ cut → f.version ≤ rollbackCut s v := fun f h => - Nat.le_trans h (Nat.le_trans (Nat.le_min.mpr ⟨hhead, hcut⟩) (Nat.le_max_right _ _)) - unfold atCut rollbackStore - congr 1 - rw [List.find?_filter] - congr 1 - exact funext fun f => by by_cases h : f.version ≤ cut <;> simp [h, hmono f] - -theorem durable_cut_survives_rollback (s : Store) (v term cut : Nat) - (valid : StoreInvariant s) (hcut : cut ≤ s.global) (hboundary : s.global ≤ v) - : (atCut (rollbackStore s v term) cut).data = (atCut s cut).data := by - rw [rollback_preserves_earlier_cuts s v term cut (Nat.le_trans hcut hboundary) - (Nat.le_trans hcut valid.globalBound)] - -theorem compacted_map_unavailable (s : Store) (f : Frame) (m : String) - (birth : Stamp) (existing : find f.births m = some birth) - (h : (revision f m).version < (revision (atCut s s.global) m).version) - : mapAvailable s f m = false := by - simp [mapAvailable, existing, Nat.not_le.mpr h] - -theorem absent_map_available (s : Store) (f : Frame) (m : String) - (absent : find f.births m = none) (empty : image f.data m = []) - (unwritten : find f.revisions m = none) - : mapAvailable s f m = true := by - simp [mapAvailable, absent, empty, unwritten] - -theorem absent_placeholder_has_no_values (s : Store) (f : Frame) (m key : String) - (absent : find f.births m = none) (permitted : mapAvailable s f m = true) - : find f.data (m, key) = none := by - have empty : image f.data m = [] := by - have checked : image f.data m = [] ∧ find f.revisions m = none := by - simpa [mapAvailable, absent] using permitted - exact checked.1 - exact empty_map_has_no_values f.data m key empty - -theorem withTx_preserves_stores (w next : World) (sid tid : Nat) - (f : Tx → Except Failure Tx) (h : withTx w sid tid f = .ok next) - : next.stores = w.stores := by - simp only [withTx, Bind.bind, Pure.pure, Except.bind, Except.pure] at h - cases ht : txOf w sid tid with - | error err => simp [ht] at h - | ok t => - cases hf : f t with - | error err => simp [ht, hf] at h - | ok t' => - simp [ht, hf] at h - cases h - rfl - -theorem rollback_keeps_prefix (s : Store) (v term : Nat) (f : Frame) - (h : f ∈ s.history) (hv : f.version ≤ s.global) - : f ∈ (rollbackStore s v term).history := by - simp only [rollbackStore, List.mem_filter, decide_eq_true_eq] - exact ⟨h, Nat.le_trans hv (Nat.le_max_left _ _)⟩ - -theorem rollback_discards_suffix (s : Store) (v term : Nat) (f : Frame) - (h : v < f.version) (boundary : s.global ≤ v) - : f ∉ (rollbackStore s v term).history := by - have hbound : rollbackCut s v ≤ v := Nat.max_le.mpr ⟨boundary, Nat.min_le_right _ _⟩ - simp [rollbackStore, Nat.not_le.mpr (Nat.lt_of_le_of_lt hbound h)] - -theorem stale_term_cannot_apply (s : Store) (t : Tx) (snap : Snapshot) - (hs : t.snapshot = some snap) (ht : s.term ≠ snap.term) - : canApply s t = false := by - simp [canApply, validLineage, hs, ht] - -theorem discarded_handle_cannot_apply (s : Store) (t : Tx) (snap : Snapshot) - (hs : t.snapshot = some snap) (m : String) (view : GlobalView) - (hm : (m, view) ∈ t.globalViews) - (gone : ∀ f ∈ s.history, (revision f m == revision view.current m) = false) - : canApply s t = false := by - apply Bool.eq_false_iff.mpr - intro h - have hh : (!t.unavailable = true ∧ validLineage s t = true) ∧ - validates s.head.data t.normal.deps = true := by simpa [canApply] using h - have hp : (s.term == snap.term) = true ∧ - t.globalViews.all (fun (name, view) => mapLineage s view.current name) = true := by - simpa [validLineage, hs] using hh.1.2 - have hall := hp.2 - have hit := List.all_eq_true.mp hall (m, view) hm - obtain ⟨f, hf, he⟩ := List.any_eq_true.mp hit - simp [gone f hf] at he - -theorem discarded_birth_cannot_apply (s : Store) (t : Tx) (snap : Snapshot) - (hs : t.snapshot = some snap) (m : String) (view : GlobalView) - (hm : (m, view) ∈ t.globalViews) - (gone : ∀ f ∈ s.history, (find f.births m == find view.current.births m) = false) - : canApply s t = false := by - apply Bool.eq_false_iff.mpr - intro h - have hh : (!t.unavailable = true ∧ validLineage s t = true) ∧ - validates s.head.data t.normal.deps = true := by simpa [canApply] using h - have hp : (s.term == snap.term) = true ∧ - t.globalViews.all (fun (name, view) => mapLineage s view.current name) = true := by - simpa [validLineage, hs] using hh.1.2 - have hit := List.all_eq_true.mp hp.2 (m, view) hm - obtain ⟨f, hf, he⟩ := List.any_eq_true.mp hit - simp [gone f hf] at he - -theorem canApply_validates (s : Store) (t : Tx) (h : canApply s t = true) - : validates s.head.data t.normal.deps = true := by - have hh : (!t.unavailable && validLineage s t) = true ∧ - validates s.head.data t.normal.deps = true := by simpa [canApply] using h - exact hh.2 - -theorem transaction_snapshot_serial (t : Tx) (snap : Snapshot) (valid : NormalInvariant t) - (hs : t.snapshot = some snap) - : serialRun t.data [] t.normal.log = some t.normal.writes := by - have hc : normalRun t.data {} t.normal.log = some t.normal := by - simpa [NormalInvariant, hs] using valid - exact readonly_snapshot_serial t.data t.normal.log t.normal hc - -/-- A valid attempt that passes OCC agrees with serial execution on the current head. -/ -theorem transaction_application_serial (s : Store) (t : Tx) (snap : Snapshot) - (valid : NormalInvariant t) - (hs : t.snapshot = some snap) (hv : canApply s t = true) - : serialRun s.head.data [] t.normal.log = some t.normal.writes := by - have hc : normalRun t.data {} t.normal.log = some t.normal := by - simpa [NormalInvariant, hs] using valid - exact normalRun_serial t.data s.head.data t.normal.log {} t.normal hc - (canApply_validates s t hv) - -theorem tryApply_serial (s next : Store) (t : Tx) (valid : NormalInvariant t) - (ha : tryApply s t = some next) - : serialRun s.head.data [] t.normal.log = some t.normal.writes - ∧ next.head.data = publish s.head.data (s.head.version + 1) t.normal.writes := by - unfold tryApply at ha - split at ha - next hv => - cases ha - refine ⟨?_, rfl⟩ - cases hs : t.snapshot with - | none => - have hc : t.normal = {} := by simpa [NormalInvariant, hs] using valid - simp [hc, serialRun] - | some snap => exact transaction_application_serial s t snap valid hs hv - next => simp at ha - -theorem executable_branch_serializability (s final : Store) (ts : List Tx) - (valid : ∀ t ∈ ts, NormalInvariant t) - (h : AppliedBranch s ts final) - : serialTransactions s.head.data s.head.version ts = some final.head.data := by - induction h with - | nil s => rfl - | compact s final v ts _rest ih => - simpa only [compact_preserves_head] using ih valid - | cons s middle final t ts one rest ih => - have hw := tryApply_serial s middle t (valid t (by simp)) one - have hversion : middle.head.version = s.head.version + 1 := by - unfold tryApply at one - split at one - next => cases one; rfl - next => simp at one - simp only [serialTransactions, hw.1, Option.bind_some] - rw [← hw.2, ← hversion] - exact ih (fun tx member => valid tx (by simp [member])) - -end Kv.Proofs.Model diff --git a/lean/kv/Kv/Proofs/Properties.lean b/lean/kv/Kv/Proofs/Properties.lean deleted file mode 100644 index 79ab6120b8f..00000000000 --- a/lean/kv/Kv/Proofs/Properties.lean +++ /dev/null @@ -1,259 +0,0 @@ --- Copyright (c) Microsoft Corporation. All rights reserved. --- Licensed under the Apache 2.0 License. - -module - -public import Kv.Proofs.Execution -public import Kv.Proofs.Trace - -@[expose] public section - -namespace Kv.Proofs.Properties - -open Kv.Model Kv.Properties - -theorem transaction_snapshot_serial - : ∀ (w : World) (tid : Nat) (t : Tx) (snap : Snapshot), - Model.transitionSystem.Reachable w - → find w.txs tid = some t - → t.snapshot = some snap - → serialRun t.data [] t.normal.log = some t.normal.writes := by - intro w tid t snap reachable live captured - exact Proofs.Model.transaction_snapshot_serial t snap - ((Proofs.Invariants.reachable_invariant w reachable).txs tid t live).normal captured - -theorem transaction_application_serial - : ∀ (w : World) (sid tid : Nat) (s : Store) (t : Tx) (snap : Snapshot), - Model.transitionSystem.Reachable w - → storeOf w sid = .ok s - → txOf w sid tid = .ok t - → t.snapshot = some snap - → canApply s t = true - → serialRun s.head.data [] t.normal.log = some t.normal.writes := by - intro w sid tid s t snap reachable _store tx captured applies - exact Proofs.Model.transaction_application_serial s t snap - (Proofs.Invariants.txOf_invariant w - (Proofs.Invariants.reachable_invariant w reachable) sid tid t tx).normal - captured applies - -theorem executable_branch_serializability - : ∀ (s final : Store) (ts : List Tx), - (∀ t ∈ ts, - ∃ (w : World) (tid : Nat), - Model.transitionSystem.Reachable w ∧ find w.txs tid = some t) - → AppliedBranch s ts final - → serialTransactions s.head.data s.head.version ts = some final.head.data := by - intro s final ts reachable branch - apply Proofs.Model.executable_branch_serializability s final ts _ branch - intro t member - obtain ⟨w, tid, reached, live⟩ := reachable t member - exact ((Proofs.Invariants.reachable_invariant w reached).txs tid t live).normal - -theorem durable_cut_survives_rollback - : ∀ (w : World) (sid : Nat) (s : Store) (v term cut : Nat), - Model.transitionSystem.Reachable w - → find w.stores sid = some s - → cut ≤ s.global - → s.global ≤ v - → (atCut (rollbackStore s v term) cut).data = (atCut s cut).data := by - intro w sid s v term cut reachable live below boundary - exact Proofs.Model.durable_cut_survives_rollback s v term cut - ((Proofs.Invariants.reachable_invariant w reachable).stores sid s live) below boundary - -theorem replay_segment_serializability - : ∀ (w final : World) (sid : Nat) (s : Store) (rs : List Record), - Model.transitionSystem.Reachable w - → find w.stores sid = some s - → (∀ r ∈ rs, SegmentEvent sid r.event) - → CCF.Execution.Run Model.transitionSystem w rs final - → ∃ after txs, - find final.stores sid = some after - ∧ projectApplications w sid rs = .ok txs - ∧ serialTransactions s.head.data s.head.version txs = some after.head.data - ∧ after.head.version = s.head.version + txs.length := by - intro w final sid s rs reachable live segment accepted - exact Proofs.Trace.replay_segment_serializability w final sid s - (Invariants.reachable_invariant w reachable) rs live segment ((Proofs.Execution.replay_iff_run _ _ _).mp accepted) - -theorem reachable_store_invariants - : ∀ (w : World) (sid : Nat) (s : Store), - Model.transitionSystem.Reachable w - → find w.stores sid = some s - → History s.history s.head.version - ∧ s.history.head? = some s.head - ∧ s.global ≤ s.head.version - ∧ (atCut s s.global).version = s.global := by - intro w sid s reachable live - exact Proofs.Trace.reachable_store_invariants w (Invariants.reachable_invariant w reachable) sid s live - -theorem reachable_store_data_invariants - : ∀ (w : World) (sid : Nat) (s : Store), - Model.transitionSystem.Reachable w - → find w.stores sid = some s - → Kv.Properties.Unique s.head.data ∧ CellsBounded s.head.data s.head.version := by - intro w sid s reachable live - exact Proofs.Trace.reachable_store_data_invariants w (Invariants.reachable_invariant w reachable) sid s live - -theorem step_capture_metadata - : ∀ (w next : World) (sid tid version global term seq : Nat) (s : Store) (t : Tx), - storeOf w sid = .ok s - → Model.transitionSystem.step w ⟨seq, .snapshot sid tid version global term⟩ - = some next - → find next.txs tid = some t - → ∃ snap, t.snapshot = some snap ∧ snap.current = s.head ∧ snap.term = term := by - intro w next sid tid version global term seq s t source accepted capturedTx - exact Proofs.Trace.step_capture_metadata w next sid tid version global term seq s t source ((Proofs.Execution.step_iff_transition _ _ _).mp accepted) capturedTx - -theorem step_capture_cut_values - : ∀ (w next : World) (sid tid version global term seq : Nat) (s : Store), - storeOf w sid = .ok s - → Model.transitionSystem.step w ⟨seq, .snapshot sid tid version global term⟩ - = some next - → version = s.head.version ∧ global = s.global := by - intro w next sid tid version global term seq s source accepted - exact Proofs.Trace.step_capture_cut_values w next sid tid version global term seq s source ((Proofs.Execution.step_iff_transition _ _ _).mp accepted) - -theorem capture_replay_preserves_metadata - : ∀ (w capturedWorld final : World) (sid tid version global term seq : Nat) - (s : Store) (t : Tx) (tail : List Record), - storeOf w sid = .ok s - → Model.transitionSystem.step w ⟨seq, .snapshot sid tid version global term⟩ - = some capturedWorld - → find capturedWorld.txs tid = some t - → (∀ r ∈ tail, AttemptEvent tid r.event) - → CCF.Execution.Run Model.transitionSystem capturedWorld tail final - → ∃ after snap, - find final.txs tid = some after - ∧ after.snapshot = some snap - ∧ snap.current = s.head - ∧ snap.term = term := by - intro w capturedWorld final sid tid version global term seq s t tail source capture live segment accepted - exact Proofs.Trace.capture_replay_preserves_metadata w capturedWorld final sid tid version global term seq s t tail source ((Proofs.Execution.step_iff_transition _ _ _).mp capture) live segment ((Proofs.Execution.replay_iff_run _ _ _).mp accepted) - -theorem replay_snapshot_fixed - : ∀ (w final : World) (tid : Nat) (before : Tx) (snap : Snapshot) (rs : List Record), - find w.txs tid = some before - → before.snapshot = some snap - → (∀ r ∈ rs, AttemptEvent tid r.event) - → CCF.Execution.Run Model.transitionSystem w rs final - → ∃ after, find final.txs tid = some after ∧ after.snapshot = some snap := by - intro w final tid before snap rs live captured segment accepted - exact Proofs.Trace.replay_snapshot_fixed w final tid before snap rs live captured segment ((Proofs.Execution.replay_iff_run _ _ _).mp accepted) - -theorem step_map_capture - : ∀ (w next : World) (sid tid localVersion globalVersion seq : Nat) (map : String) - (s : Store) (before after : Tx) (snap : Snapshot), - storeOf w sid = .ok s - → txOf w sid tid = .ok before - → before.snapshot = some snap - → Model.transitionSystem.step w - ⟨seq, .acquire sid tid map localVersion globalVersion⟩ - = some next - → find next.txs tid = some after - → find after.globalViews map = some (captureGlobal s snap map) - ∧ localVersion = (revision (captureLocal s snap map) map).version - ∧ globalVersion = (revision (captureGlobal s snap map).frame map).version := by - intro w next sid tid localVersion globalVersion seq map s before after snap store tx snapshot accepted live - exact Proofs.Trace.step_map_capture w next sid tid localVersion globalVersion seq map s before after snap store tx snapshot ((Proofs.Execution.step_iff_transition _ _ _).mp accepted) live - -theorem replay_map_global_fixed - : ∀ (w final : World) (tid : Nat) (before : Tx) (map : String) (view : GlobalView) - (rs : List Record), - find w.txs tid = some before - → find before.globalViews map = some view - → (∀ r ∈ rs, AttemptEvent tid r.event) - → CCF.Execution.Run Model.transitionSystem w rs final - → ∃ after, - find final.txs tid = some after ∧ find after.globalViews map = some view := by - intro w final tid before map view rs live captured segment accepted - exact Proofs.Trace.replay_map_global_fixed w final tid before map view rs live captured segment ((Proofs.Execution.replay_iff_run _ _ _).mp accepted) - -theorem capture_replay_preserves_map - : ∀ (w capturedWorld final : World) (sid tid localVersion globalVersion seq : Nat) - (map : String) (s : Store) (before capturedTx : Tx) (snap : Snapshot) - (tail : List Record), - storeOf w sid = .ok s - → txOf w sid tid = .ok before - → before.snapshot = some snap - → Model.transitionSystem.step w - ⟨seq, .acquire sid tid map localVersion globalVersion⟩ - = some capturedWorld - → find capturedWorld.txs tid = some capturedTx - → (∀ r ∈ tail, AttemptEvent tid r.event) - → CCF.Execution.Run Model.transitionSystem capturedWorld tail final - → ∃ after, - find final.txs tid = some after - ∧ find after.globalViews map = some (captureGlobal s snap map) - ∧ localVersion = (revision (captureLocal s snap map) map).version - ∧ globalVersion - = (revision (captureGlobal s snap map).frame map).version := by - intro w capturedWorld final sid tid localVersion globalVersion seq map s before capturedTx snap tail store tx snapshot capture live segment accepted - exact Proofs.Trace.capture_replay_preserves_map w capturedWorld final sid tid localVersion globalVersion seq map s before capturedTx snap tail store tx snapshot ((Proofs.Execution.step_iff_transition _ _ _).mp capture) live segment ((Proofs.Execution.replay_iff_run _ _ _).mp accepted) - -theorem step_global_read_from_captured_map - : ∀ (w next : World) (sid tid seq : Nat) (map key : String) (value : Option String) - (t : Tx) (view : GlobalView), - Model.transitionSystem.Reachable w - → txOf w sid tid = .ok t - → find t.globalViews map = some view - → Model.transitionSystem.step w ⟨seq, .get sid tid map key value true⟩ = some next - → value = (find view.frame.data (map, key)).map Cell.value - ∧ (view.frame = {} - ∨ ∃ origin : Store, - view.frame = atCut origin origin.global - ∧ view.frame.version = origin.global - ∧ CellsBounded view.frame.data origin.global) := by - intro w next sid tid seq map key value t view reachable source captured accepted - exact Proofs.Trace.step_global_read_from_captured_map w next sid tid seq - (Invariants.reachable_invariant w reachable) map key value t view source captured ((Proofs.Execution.step_iff_transition _ _ _).mp accepted) - -theorem step_global_has_from_captured_map - : ∀ (w next : World) (sid tid seq : Nat) (map key : String) (value : Bool) (t : Tx) - (view : GlobalView), - Model.transitionSystem.Reachable w - → txOf w sid tid = .ok t - → find t.globalViews map = some view - → Model.transitionSystem.step w ⟨seq, .has sid tid map key value true⟩ = some next - → value = (find view.frame.data (map, key)).isSome - ∧ (view.frame = {} - ∨ ∃ origin : Store, - view.frame = atCut origin origin.global - ∧ view.frame.version = origin.global - ∧ CellsBounded view.frame.data origin.global) := by - intro w next sid tid seq map key value t view reachable source captured accepted - exact Proofs.Trace.step_global_has_from_captured_map w next sid tid seq - (Invariants.reachable_invariant w reachable) map key value t view source captured ((Proofs.Execution.step_iff_transition _ _ _).mp accepted) - -theorem discarded_handle_cannot_apply - : ∀ (s : Store) (t : Tx) (snap : Snapshot) (m : String) (view : GlobalView), - t.snapshot = some snap - → (m, view) ∈ t.globalViews - → (∀ f ∈ s.history, (revision f m == revision view.current m) = false) - → canApply s t = false := by - intro s t snap m view hs hm gone - exact Proofs.Model.discarded_handle_cannot_apply s t snap hs m view hm gone - -theorem replay_map_local_fixed - : ∀ (w final : World) (tid : Nat) (before : Tx) (map : String) (view : GlobalView) - (rs : List Record), - find w.txs tid = some before - → find before.globalViews map = some view - → (∀ r ∈ rs, AttemptEvent tid r.event) - → CCF.Execution.Run Model.transitionSystem w rs final - → ∃ after, - find final.txs tid = some after - ∧ image after.data map = image before.data map := by - intro w final tid before map view rs live captured segment accepted - exact Proofs.Trace.replay_map_local_fixed w final tid before map view rs live captured segment - ((Proofs.Execution.replay_iff_run _ _ _).mp accepted) - -theorem discarded_birth_cannot_apply - : ∀ (s : Store) (t : Tx) (snap : Snapshot) (m : String) (view : GlobalView), - t.snapshot = some snap - → (m, view) ∈ t.globalViews - → (∀ f ∈ s.history, (find f.births m == find view.current.births m) = false) - → canApply s t = false := by - intro s t snap m view hs hm gone - exact Proofs.Model.discarded_birth_cannot_apply s t snap hs m view hm gone - -end Kv.Proofs.Properties diff --git a/lean/kv/Kv/Proofs/Reachable.lean b/lean/kv/Kv/Proofs/Reachable.lean new file mode 100644 index 00000000000..b7a1882c216 --- /dev/null +++ b/lean/kv/Kv/Proofs/Reachable.lean @@ -0,0 +1,1782 @@ +-- Copyright (c) Microsoft Corporation. All rights reserved. +-- Licensed under the Apache 2.0 License. + +module + +public import Kv.Properties.Invariants + +/-! +The executable model's state invariants, their preservation by every accepted step, and the +claims that depend on them: store invariants, serializability of replayed segments, and global +reads from captured maps. + +This module is self-contained: shared lemmas are duplicated as private declarations in each +proof module so that the proof modules can be checked in parallel. +-/ + +@[expose] public section + +namespace Kv.Proofs.Execution +end Kv.Proofs.Execution + +namespace Kv.Proofs.Invariants +end Kv.Proofs.Invariants + +namespace Kv.Proofs.Model +end Kv.Proofs.Model + +namespace Kv.Proofs.Trace +end Kv.Proofs.Trace + +namespace Kv.Proofs.Properties +end Kv.Proofs.Properties + +namespace Kv.Proofs.Witnesses +end Kv.Proofs.Witnesses + +namespace Kv.Proofs.Execution + +open Kv.Model + +private theorem step_iff_transition (w next : World) (r : Record) + : transitionSystem.step w r = some next ↔ step w r = .ok next := by + simp only [transitionSystem] + cases step w r <;> simp [Except.toOption] + +private theorem replay_iff_run (w final : World) (rs : List Record) + : CCF.Execution.Run transitionSystem w rs final ↔ replay w rs = .ok final := by + induction rs generalizing w with + | nil => + constructor + · intro run + cases run using @CCF.Execution.Run.casesOn transitionSystem + rfl + · intro accepted + cases accepted + exact .nil _ + | cons r rs ih => + constructor + · intro run + cases run using @CCF.Execution.Run.casesOn transitionSystem with + | cons transition rest => + simp only [replay, (step_iff_transition _ _ _).mp transition, Except.bind] + exact (ih _).mp rest + · intro accepted + simp only [replay] at accepted + cases accepted' : step w r with + | error failure => simp [accepted', Except.bind] at accepted + | ok next => + simp only [accepted', Except.bind] at accepted + exact .cons ((step_iff_transition _ _ _).mpr accepted') ((ih _).mpr accepted) + +end Kv.Proofs.Execution + +namespace Kv.Proofs.Invariants + +open Kv.Model Kv.Properties + +/-- Executes operations in order with `normalStep` to reconstruct the normal view. -/ +private def normalRun {M K V : Type} [DecidableEq M] [DecidableEq K] [DecidableEq V] + (snapshot : DB M K V) (n : Normal M K V) (ops : List (NormalOp M K V)) + : Option (Normal M K V) := + ops.foldlM (normalStep snapshot) n + +/-- Store histories are contiguous, headed by the current frame, and contain the global cut. -/ +private structure StoreInvariant (s : Store) : Prop where + /-- Every frame follows by publishing writes to its predecessor. -/ + historyShape : History s.history s.head.version + /-- The head is the newest frame. -/ + headFirst : s.history.head? = some s.head + /-- The global version does not exceed the head. -/ + globalBound : s.global ≤ s.head.version + +/-- A global view is empty or was captured at a well-formed store's global cut. -/ +private def GlobalInvariant (view : GlobalView) : Prop := + view.frame = {} ∨ ∃ s : Store, StoreInvariant s ∧ view.frame = atCut s s.global + +/-- Replaying an attempt's log from its pinned data reproduces its normal view. -/ +private def NormalInvariant (t : Tx) : Prop := + match t.snapshot with + | none => t.normal = {} + | some _ => normalRun t.data {} t.normal.log = some t.normal + +/-- Consistency of an attempt's operation log and captured views. -/ +private structure TxInvariant (t : Tx) : Prop where + /-- The operation log reproduces the normal view. -/ + normal : NormalInvariant t + /-- Each snapshot was captured from a well-formed store's head. -/ + snapshot + : ∀ snap, + t.snapshot = some snap → ∃ s : Store, StoreInvariant s ∧ snap.current = s.head + /-- Each acquired global view has valid provenance. -/ + globals : ∀ map view, find t.globalViews map = some view → GlobalInvariant view + +/-- Internal consistency of every live store and attempt. -/ +private structure WorldInvariant (w : World) : Prop where + /-- Live stores have well-formed histories. -/ + stores : ∀ sid s, find w.stores sid = some s → StoreInvariant s + /-- Live attempts have valid logs and captured views. -/ + txs : ∀ tid t, find w.txs tid = some t → TxInvariant t + +/-- An attempt keeps its snapshot, pinned data and global views, and its invariant. -/ +private structure Frozen (t next : Tx) : Prop where + /-- The captured snapshot is unchanged. -/ + snapshot : next.snapshot = t.snapshot + /-- The pinned local data is unchanged. -/ + data : next.data = t.data + /-- The captured global views are unchanged. -/ + globals : next.globalViews = t.globalViews + /-- The attempt invariant is preserved. -/ + valid : TxInvariant t → TxInvariant next + +/-- How an accepted event changes the live stores and attempts. -/ +private inductive StepEffect (w : World) : Event → World → Prop + /-- Stores and attempts are unchanged. -/ + | same {e : Event} {next : World} (stores : next.stores = w.stores) + (txs : next.txs = w.txs) (noApply : ∀ sid, projectedApplication w sid e = []) + : StepEffect w e next + /-- A fresh store is created. -/ + | storeCreate {sid : Nat} {next : World} (stores : next.stores = set w.stores sid {}) + (txs : next.txs = w.txs) + : StepEffect w (.storeCreate sid) next + /-- A store is ended. -/ + | storeEnd {sid : Nat} {next : World} (stores : next.stores = erase w.stores sid) + (txs : next.txs = w.txs) + : StepEffect w (.storeEnd sid) next + /-- A fresh attempt is created. -/ + | txCreate {sid tid : Nat} {next : World} (stores : next.stores = w.stores) + (txs : next.txs = set w.txs tid { store := sid }) + : StepEffect w (.txCreate sid tid) next + /-- An attempt is ended. -/ + | txEnd {sid tid : Nat} {next : World} (stores : next.stores = w.stores) + (txs : next.txs = erase w.txs tid) + : StepEffect w (.txEnd sid tid) next + /-- A store is compacted. -/ + | compact {sid version requested : Nat} {next : World} {s : Store} + (store : storeOf w sid = .ok s) + (stores : next.stores = set w.stores sid (compactStore s requested)) + (txs : next.txs = w.txs) + : StepEffect w (.compact sid version requested) next + /-- A store is rolled back. -/ + | rollback {sid version requested term : Nat} {next : World} {s : Store} + (store : storeOf w sid = .ok s) + (stores : next.stores = set w.stores sid (rollbackStore s version term)) + (txs : next.txs = w.txs) + : StepEffect w (.rollback sid version requested term) next + /-- An attempt captures its snapshot; the store may learn its term. -/ + | snapshot {sid tid version global term : Nat} {next : World} {s established : Store} + {t : Tx} (store : storeOf w sid = .ok s) (history : established.history = s.history) + (head : established.head = s.head) (globalCut : established.global = s.global) + (tx : find w.txs tid = some t) (fresh : t.snapshot = none) + (stores : next.stores = set w.stores sid established) + (txs + : next.txs = set w.txs tid { t with snapshot := some { current := s.head, term } }) + : StepEffect w (.snapshot sid tid version global term) next + /-- An attempt acquires a map. -/ + | acquire {sid tid version global : Nat} {m : String} {next : World} {s : Store} + {t t' : Tx} (store : storeOf w sid = .ok s) (tx : txOf w sid tid = .ok t) + (accepted : acquireMap s t m version global = .ok t') + (stores : next.stores = w.stores) (txs : next.txs = set w.txs tid t') + : StepEffect w (.acquire sid tid m version global) next + /-- An attempt is applied to its store. -/ + | apply {sid tid version term : Nat} {writes : Pending} {next : World} {s new : Store} + {t : Tx} (store : storeOf w sid = .ok s) (tx : txOf w sid tid = .ok t) + (applied : tryApply s t = some new) (stores : next.stores = set w.stores sid new) + (txs : next.txs = set w.txs tid { t with phase := .applied version }) + : StepEffect w (.apply sid tid version term writes) next + /-- An attempt changes without moving its snapshot, pinned data or global views. -/ + | update {e : Event} {sid tid : Nat} {next : World} {t t' : Tx} + (tx : txOf w sid tid = .ok t) (frozen : Frozen t t') + (stores : next.stores = w.stores) (txs : next.txs = set w.txs tid t') + (noApply : ∀ sid, projectedApplication w sid e = []) + : StepEffect w e next + +end Kv.Proofs.Invariants + +namespace Kv.Proofs.Invariants + +open Kv.Model Kv.Properties +variable {M K V : Type} + +private theorem find_set_same [DecidableEq K] (xs : Assoc K V) (k : K) (v : V) + : find (set xs k v) k = some v := by + simp [Model.set, find] + +private theorem find_erase_same [DecidableEq K] (xs : Assoc K V) (k : K) + : find (erase xs k) k = none := by + induction xs with + | nil => rfl + | cons p xs ih => + rcases p with ⟨a, v⟩ + by_cases h : a = k <;> simp_all [erase, find] + +private theorem find_erase_other [DecidableEq K] (xs : Assoc K V) (a k : K) (h : a ≠ k) + : find (erase xs a) k = find xs k := by + induction xs with + | nil => rfl + | cons p xs ih => + rcases p with ⟨b, v⟩ + by_cases hba : b = a <;> by_cases hbk : b = k <;> simp_all [erase, find] + +private theorem find_set_other [DecidableEq K] (xs : Assoc K V) (a k : K) (v : V) + (h : a ≠ k) + : find (set xs a v) k = find xs k := by + simp [Model.set, find, h, find_erase_other xs a k h] + +private theorem find_set_cases [DecidableEq K] (xs : Assoc K V) (id key : K) (v : V) + : find (set xs id v) key = if id = key then some v else find xs key := by + by_cases h : id = key <;> simp [h, find_set_same, find_set_other] + +private theorem find_erase_cases [DecidableEq K] (xs : Assoc K V) (id key : K) + : find (erase xs id) key = if id = key then none else find xs key := by + by_cases h : id = key <;> simp [h, find_erase_same, find_erase_other] + +private theorem normalRun_append [DecidableEq M] [DecidableEq K] [DecidableEq V] + (db : DB M K V) (n : Normal M K V) (a b : List (NormalOp M K V)) + : normalRun db n (a ++ b) + = (normalRun db n a).bind (fun next => normalRun db next b) := by + unfold normalRun + simp + +private theorem normalStep_log [DecidableEq M] [DecidableEq K] [DecidableEq V] + (db : DB M K V) (n n' : Normal M K V) (op : NormalOp M K V) + (h : normalStep db n op = some n') + : n'.log = n.log ++ [op] := by + unfold normalStep at h + split at h + next => cases h; rfl + next => simp at h + +private theorem normalRun_extend [DecidableEq M] [DecidableEq K] [DecidableEq V] + (db : DB M K V) (n n' : Normal M K V) (op : NormalOp M K V) + (before : normalRun db {} n.log = some n) + (one : normalStep db n op = some n') + : normalRun db {} n'.log = some n' := by + rw [normalStep_log db n n' op one, normalRun_append, before] + simp [normalRun, one] + +private theorem History.bounded (fs : List Frame) (n : Nat) (h : History fs n) + : ∀ f ∈ fs, f.version ≤ n := by + induction h with + | zero => + intro g hg + have he : g = {} := List.mem_singleton.mp hg + subst g + exact Nat.le_refl 0 + | succ f n fs hv _effect _tail ih => + intro g hg + rcases List.mem_cons.mp hg with he | hm + · subst g; exact Nat.le_of_eq hv + · exact Nat.le_trans (ih g hm) (Nat.le_succ n) + +private theorem History.cut (fs : List Frame) (n : Nat) (h : History fs n) + (cut : Nat) (hc : cut ≤ n) + : ∃ f, + fs.find? (fun f => f.version ≤ cut) = some f + ∧ f.version = cut + ∧ History (fs.filter fun f => f.version ≤ cut) cut + ∧ (fs.filter fun f => f.version ≤ cut).head? = some f := by + induction h with + | zero => + have hz : cut = 0 := Nat.le_zero.mp hc + subst cut + refine ⟨{}, ?_, rfl, ?_, ?_⟩ + · rfl + · exact .zero + · rfl + | succ f n fs hv effect tail ih => + by_cases he : cut = n + 1 + · subst cut + have hall : (f :: fs).filter (fun f => decide (f.version ≤ n + 1)) = f :: fs := by + apply List.filter_eq_self.mpr + intro g hg + simp only [decide_eq_true_eq] + exact History.bounded _ _ (.succ f n fs hv effect tail) g hg + refine ⟨f, by simp [List.find?, hv], hv, ?_, by simp [hall]⟩ + rw [hall] + exact .succ f n fs hv effect tail + · have hlt : ¬n + 1 ≤ cut := fun h => he (Nat.le_antisymm hc h) + have hc' : cut ≤ n := Nat.le_of_lt_succ (Nat.lt_of_le_of_ne hc he) + obtain ⟨g, found, gv, shape, first⟩ := ih hc' + refine ⟨g, ?_, gv, ?_, ?_⟩ + · simpa [List.find?, hv, hlt] using found + · simpa [hv, hlt] using shape + · simpa [hv, hlt] using first + +private theorem atCut_spec (s : Store) (valid : StoreInvariant s) + (cut : Nat) (hc : cut ≤ s.head.version) + : (atCut s cut).version = cut + ∧ History (s.history.filter fun f => f.version ≤ cut) cut + ∧ (s.history.filter fun f => f.version ≤ cut).head? = some (atCut s cut) := by + obtain ⟨f, found, version, shape, first⟩ := + History.cut s.history s.head.version valid.historyShape cut hc + simpa [atCut, found] using And.intro version (And.intro shape first) + +private theorem operation_normal (t : Tx) (valid : NormalInvariant t) (snap : Snapshot) + (n : Normal String String String) (op : NormalOp String String String) + (hs : t.snapshot = some snap) + (hn : normalStep t.data t.normal op = some n) + : match t.snapshot with + | none => n = {} + | some _ => normalRun t.data {} n.log = some n := by + have old : normalRun t.data {} t.normal.log = some t.normal := by + simpa [NormalInvariant, hs] using valid + simpa [hs] using normalRun_extend t.data t.normal n op old hn + +private theorem image_append (a b : Data) (m : String) + : image (a ++ b) m = image a m ++ image b m := by + simp [image] + +private theorem image_cons (name key : String) (cell : Cell String) (db : Data) + (m : String) + : image (((name, key), cell) :: db) m + = if name = m then (key, cell) :: image db m else image db m := by + unfold image + by_cases h : name = m + · simp only [List.filterMap_cons, h, ↓reduceIte] + · simp only [List.filterMap_cons, h, ↓reduceIte] + +private theorem image_filter (db : Data) (m : String) (p : String → Bool) + : image (db.filter fun (a, _) => p a.1) m = if p m then image db m else [] := by + induction db with + | nil => split <;> rfl + | cons entry db ih => + obtain ⟨⟨name, key⟩, cell⟩ := entry + rw [List.filter_cons, image_cons] + by_cases h : name = m + · subst h + cases hp : p name + · simpa only [hp, Bool.false_eq_true, ite_false] using ih + · simp only [hp, ite_true, image_cons] + rw [ih, hp] + rfl + · cases hp : p name + · simpa only [hp, Bool.false_eq_true, ite_false, h] using ih + · simp only [hp, ite_true, image_cons, h, ite_false] + exact ih + +private theorem pinData_other (db acquired : Data) (m other : String) (h : other ≠ m) + : image (pinData db m acquired) other = image db other := by + rw [pinData, image_append, image_filter db other (fun name => name != m), + image_filter acquired other (fun name => name == m)] + simp [h] + +private theorem find_image (db : Data) (m key : String) + : find (image db m) key = find db (m, key) := by + induction db with + | nil => rfl + | cons entry db ih => + rcases entry with ⟨⟨name, k⟩, cell⟩ + by_cases hm : name = m <;> by_cases hk : k = key <;> + simp_all [image, find, Prod.mk.injEq] + +private theorem normalStep_pinData (db acquired : Data) (m : String) + (n : Normal String String String) (op : NormalOp String String String) + (h : op.map ≠ m) + : normalStep (pinData db m acquired) n op = normalStep db n op := by + have hi := pinData_other db acquired m op.map h + cases op with + | read a v | previous a v => + have hf := congrArg (fun entries => find entries a.2) hi + simp only [NormalOp.map, find_image] at hf + change find (pinData db m acquired) a = find db a at hf + simp only [normalStep, observes, valueAt, previousAt, needs, hf] + rfl + | scan name entries => + change image (pinData db m acquired) name = image db name at hi + simp only [normalStep, observes, scanAt, needs, hi] + rfl + | write => rfl + +private theorem normalRun_pinData (db acquired : Data) (m : String) + (n : Normal String String String) (ops : List (NormalOp String String String)) + (unused : ops.all (fun op => op.map != m) = true) + : normalRun (pinData db m acquired) n ops = normalRun db n ops := by + induction ops generalizing n with + | nil => rfl + | cons op ops ih => + have h : (op.map != m) = true ∧ ops.all (fun op => op.map != m) = true := by + simpa only [List.all_cons, Bool.and_eq_true] using unused + have other : op.map ≠ m := by simpa using h.1 + simp only [normalRun, List.foldlM_cons, normalStep_pinData db acquired m n op other] + cases normalStep db n op with + | none => rfl + | some next => exact ih next h.2 + +private theorem acquisition_normal (t : Tx) (valid : NormalInvariant t) (m : String) + (acquired : Data) (unused : t.normal.log.all (fun op => op.map != m) = true) + : match t.snapshot with + | none => t.normal = {} + | some _ => + normalRun (pinData t.data m acquired) {} t.normal.log = some t.normal := by + cases hs : t.snapshot with + | none => simpa [NormalInvariant, hs] using valid + | some snap => + simpa [NormalInvariant, hs, + normalRun_pinData t.data acquired m {} t.normal.log unused] + using valid + +private theorem snapshot_normal (t : Tx) (valid : NormalInvariant t) (data : Data) + (hs : t.snapshot = none) + : normalRun data {} t.normal.log = some t.normal := by + have hzero : t.normal = {} := by simpa [NormalInvariant, hs] using valid + simp [hzero, normalRun] + +private theorem history_extension (s : Store) (valid : StoreInvariant s) (f : Frame) + (writes : Pending) (version : f.version = s.head.version + 1) + (data : f.data = publish s.head.data (s.head.version + 1) writes) + : History (f :: s.history) (s.head.version + 1) := + .succ f s.head.version s.history version + ⟨writes, by simpa only [valid.headFirst, Option.getD_some] using data⟩ + valid.historyShape + +private theorem cut_history (s : Store) (valid : StoreInvariant s) + (cut : Nat) (within : cut ≤ s.head.version) + : History (s.history.filter fun f => f.version ≤ cut) (atCut s cut).version := by + have spec := atCut_spec s valid cut within + rw [spec.1] + exact spec.2.1 + +private theorem cut_global_bound (s : Store) (valid : StoreInvariant s) (cut : Nat) + (within : cut ≤ s.head.version) (boundary : s.global ≤ cut) + : s.global ≤ (atCut s cut).version := by + rw [(atCut_spec s valid cut within).1] + exact boundary + +private theorem store_initial : StoreInvariant {} := + ⟨.zero, rfl, Nat.le_refl 0⟩ + +private theorem advance_invariant (s : Store) (valid : StoreInvariant s) + (writes : Pending) + : StoreInvariant (advance s writes) := + ⟨ + history_extension s valid _ writes rfl rfl, + rfl, + Nat.le_trans valid.globalBound (Nat.le_succ _) + ⟩ + +private theorem compact_invariant (s : Store) (valid : StoreInvariant s) (v : Nat) + : StoreInvariant (compactStore s v) := by + unfold compactStore + split + next within => + exact ⟨valid.historyShape, valid.headFirst, Nat.max_le.mpr ⟨valid.globalBound, within⟩⟩ + next => exact valid + +private theorem rollback_invariant (s : Store) (valid : StoreInvariant s) (v term : Nat) + : StoreInvariant (rollbackStore s v term) := by + have within : rollbackCut s v ≤ s.head.version := + Nat.max_le.mpr ⟨valid.globalBound, Nat.min_le_left _ _⟩ + exact ⟨cut_history s valid _ within, (atCut_spec s valid _ within).2.2, + cut_global_bound s valid _ within (Nat.le_max_left _ _)⟩ + +private theorem tx_initial (sid : Nat) : TxInvariant { store := sid } := by + refine ⟨rfl, ?_, ?_⟩ <;> simp [find] + +private theorem captureGlobal_invariant (s : Store) (valid : StoreInvariant s) + (snap : Snapshot) (map : String) + : GlobalInvariant (captureGlobal s snap map) := by + dsimp only [captureGlobal] + split + · exact Or.inl rfl + · exact Or.inr ⟨s, valid, rfl⟩ + +private theorem bind_ok {α β : Type} {x : Except Failure α} {f : α → Except Failure β} + {b : β} (h : (x >>= f) = .ok b) + : ∃ a, x = .ok a ∧ f a = .ok b := by + cases x with + | error => cases h + | ok a => exact ⟨a, rfl, h⟩ + +private theorem pure_ok {α : Type} {a b : α} (h : (pure a : Except Failure α) = .ok b) + : a = b := by + cases h; rfl + +private theorem withTx_ok {w next : World} {sid tid : Nat} {f : Tx → Except Failure Tx} + (h : withTx w sid tid f = .ok next) + : ∃ t t', + txOf w sid tid = .ok t + ∧ f t = .ok t' + ∧ next = { w with txs := set w.txs tid t' } := by + obtain ⟨t, tx, h⟩ := bind_ok h + obtain ⟨t', f, h⟩ := bind_ok h + exact ⟨t, t', tx, f, (pure_ok h).symm⟩ + +private theorem present_ok {α : Type} {value : Option α} {message : String} {a : α} + (h : present value message = .ok a) + : value = some a := by + cases value with + | none => cases h + | some => cases h; rfl + +private theorem require_ok {condition : Bool} {message : String} {u : Unit} + (h : require condition message = .ok u) + : condition = true := by + cases condition + · cases h + · rfl + +private theorem expect_ok {condition : Bool} {message : String} {u : Unit} + (h : expect condition message = .ok u) + : condition = true := by + cases condition + · cases h + · rfl + +private theorem acquireMap_ok {s : Store} {t next : Tx} {map : String} + {version global : Nat} (accepted : acquireMap s t map version global = .ok next) + : ∃ snap, + t.snapshot = some snap + ∧ find t.globalViews map = none + ∧ (version = (revision (captureGlobal s snap map).current map).version + ∧ global = (revision (captureGlobal s snap map).frame map).version) + ∧ t.normal.log.all (fun op => op.map != map) = true + ∧ next + = { + t with + globalViews := set t.globalViews map (captureGlobal s snap map) + data := pinData t.data map (captureGlobal s snap map).current.data + } := by + obtain ⟨_, -, accepted⟩ := bind_ok accepted + obtain ⟨_, -, accepted⟩ := bind_ok accepted + obtain ⟨snap, captured, accepted⟩ := bind_ok accepted + obtain ⟨_, fresh, accepted⟩ := bind_ok accepted + obtain ⟨_, versions, accepted⟩ := bind_ok accepted + obtain ⟨_, -, accepted⟩ := bind_ok accepted + split at accepted + next unused => + cases pure_ok accepted + have versions := expect_ok versions + simp only [Bool.and_eq_true, beq_iff_eq] at versions + exact ⟨snap, present_ok captured, Option.isNone_iff_eq_none.mp (require_ok fresh), versions, + unused, rfl⟩ + next => cases accepted + +private theorem acquireMap_invariant (s : Store) (store : StoreInvariant s) + (t next : Tx) (valid : TxInvariant t) (map : String) (version global : Nat) + (accepted : acquireMap s t map version global = .ok next) + : TxInvariant next := by + obtain ⟨_, _, _, _, unused, rfl⟩ := acquireMap_ok accepted + refine ⟨acquisition_normal t valid.normal map _ unused, valid.snapshot, ?_⟩ + intro name view found + rw [find_set_cases] at found + split at found + · cases found + exact captureGlobal_invariant s store _ map + · exact valid.globals name view found + +private theorem snapshot_invariant (s : Store) (store : StoreInvariant s) (term : Nat) + (t : Tx) (valid : TxInvariant t) (fresh : t.snapshot = none) + : TxInvariant { t with snapshot := some { current := s.head, term } } := by + refine ⟨snapshot_normal t valid.normal t.data fresh, ?_, valid.globals⟩ + intro snap captured + cases captured + exact ⟨s, store, rfl⟩ + +private theorem tx_fields_invariant (t next : Tx) (valid : TxInvariant t) + (snapshot : next.snapshot = t.snapshot) (data : next.data = t.data) + (normal : next.normal = t.normal) (globals : next.globalViews = t.globalViews) + : TxInvariant next := by + rcases valid with ⟨hn, hs, hg⟩ + constructor + · simpa [NormalInvariant, snapshot, data, normal] using hn + · simpa [snapshot] using hs + · simpa [globals] using hg + +private theorem lookup_set_invariant [DecidableEq K] (P : V → Prop) (xs : Assoc K V) + (valid : ∀ key value, find xs key = some value → P value) + (id : K) (value : V) (holds : P value) + : ∀ key next, find (set xs id value) key = some next → P next := by + intro key next found + rw [find_set_cases] at found + split at found + · cases found; exact holds + · exact valid key next found + +private theorem lookup_erase_invariant [DecidableEq K] (P : V → Prop) (xs : Assoc K V) + (valid : ∀ key value, find xs key = some value → P value) (id : K) + : ∀ key next, find (erase xs id) key = some next → P next := by + intro key next found + rw [find_erase_cases] at found + split at found + · contradiction + · exact valid key next found + +private theorem storeOf_invariant (w : World) (valid : WorldInvariant w) (sid : Nat) + (s : Store) (found : storeOf w sid = .ok s) + : StoreInvariant s := by + cases h : find w.stores sid <;> simp [storeOf, present, invalid, h] at found + next => cases found; exact valid.stores sid _ h + +private theorem txOf_found (w : World) (sid tid : Nat) (t : Tx) + (found : txOf w sid tid = .ok t) + : find w.txs tid = some t := by + obtain ⟨_, -, found⟩ := bind_ok found + obtain ⟨_, lookup, found⟩ := bind_ok found + obtain ⟨_, -, found⟩ := bind_ok found + cases pure_ok found + exact present_ok lookup + +private theorem txOf_invariant (w : World) (valid : WorldInvariant w) (sid tid : Nat) + (t : Tx) (found : txOf w sid tid = .ok t) + : TxInvariant t := + valid.txs tid t (txOf_found w sid tid t found) + +private theorem tryApply_invariant (s next : Store) (valid : StoreInvariant s) (t : Tx) + (applied : tryApply s t = some next) + : StoreInvariant next := by + unfold tryApply at applied + split at applied + · cases applied; exact advance_invariant s valid t.normal.writes + · contradiction + +private theorem world_initial : WorldInvariant {} := by + constructor <;> simp [find] + +private theorem Frozen.refl (t : Tx) : Frozen t t := ⟨rfl, rfl, rfl, id⟩ + +private theorem Frozen.trans {a b c : Tx} (ab : Frozen a b) (bc : Frozen b c) + : Frozen a c := + ⟨ + bc.snapshot.trans ab.snapshot, + bc.data.trans ab.data, + bc.globals.trans ab.globals, + bc.valid ∘ ab.valid + ⟩ + +private theorem Frozen.fields {t next : Tx} (snapshot : next.snapshot = t.snapshot) + (data : next.data = t.data) (normal : next.normal = t.normal) + (globals : next.globalViews = t.globalViews) + : Frozen t next := + ⟨ + snapshot, + data, + globals, + fun valid => tx_fields_invariant t next valid snapshot data normal globals + ⟩ + +private theorem runOp_frozen {t next : Tx} {op : NormalOp String String String} + (accepted : runOp t op = .ok next) + : Frozen t next := by + simp only [runOp, Pure.pure, Except.pure] at accepted + split at accepted + next => contradiction + next snap hs => + split at accepted + next n hn => + cases accepted + exact ⟨rfl, rfl, rfl, fun valid => + ⟨operation_normal t valid.normal snap n op hs hn, valid.snapshot, valid.globals⟩⟩ + next => contradiction + +private theorem clearWrites_frozen {t next : Tx} {map : String} + {entries : Assoc String String} (accepted : clearWrites t map entries = .ok next) + : Frozen t next := by + unfold clearWrites at accepted + induction entries generalizing t with + | nil => cases accepted; exact Frozen.refl _ + | cons entry entries ih => + obtain ⟨middle, one, rest⟩ := bind_ok accepted + exact (runOp_frozen one).trans (ih rest) + +private theorem StepEffect.withTx {w next : World} {e : Event} {sid tid : Nat} + {f : Tx → Except Failure Tx} (noApply : ∀ sid, projectedApplication w sid e = []) + (frozen : ∀ t t', f t = .ok t' → Frozen t t') + (accepted : withTx w sid tid f = .ok next) + : StepEffect w e next := by + obtain ⟨t, t', tx, h, rfl⟩ := withTx_ok accepted + exact .update tx (frozen t t' h) rfl rfl noApply + +private theorem stepEvent_effect_rollbackRejected (w next : World) + (store requested term : Nat) + (accepted : stepEvent w (.rollbackRejected store requested term) = .ok next) + : StepEffect w (.rollbackRejected store requested term) next := by + repeat obtain ⟨_, -, accepted⟩ := bind_ok accepted + cases pure_ok accepted + exact .same rfl rfl fun _ => rfl + +private theorem stepEvent_effect_storeCreate (w next : World) (store : Nat) + (accepted : stepEvent w (.storeCreate store) = .ok next) + : StepEffect w (.storeCreate store) next := by + repeat obtain ⟨_, -, accepted⟩ := bind_ok accepted + cases pure_ok accepted + exact .storeCreate rfl rfl + +private theorem stepEvent_effect_storeEnd (w next : World) (store : Nat) + (accepted : stepEvent w (.storeEnd store) = .ok next) + : StepEffect w (.storeEnd store) next := by + repeat obtain ⟨_, -, accepted⟩ := bind_ok accepted + cases pure_ok accepted + exact .storeEnd rfl rfl + +private theorem stepEvent_effect_txCreate (w next : World) (store tx : Nat) + (accepted : stepEvent w (.txCreate store tx) = .ok next) + : StepEffect w (.txCreate store tx) next := by + repeat obtain ⟨_, -, accepted⟩ := bind_ok accepted + cases pure_ok accepted + exact .txCreate rfl rfl + +private theorem stepEvent_effect_txEnd (w next : World) (store tx : Nat) + (accepted : stepEvent w (.txEnd store tx) = .ok next) + : StepEffect w (.txEnd store tx) next := by + repeat obtain ⟨_, -, accepted⟩ := bind_ok accepted + cases pure_ok accepted + exact .txEnd rfl rfl + +private theorem stepEvent_effect_snapshot (w next : World) + (sid tid version global term : Nat) + (accepted : stepEvent w (.snapshot sid tid version global term) = .ok next) + : StepEffect w (.snapshot sid tid version global term) next := by + obtain ⟨s, store, accepted⟩ := bind_ok accepted + obtain ⟨t, t', tx, h, rfl⟩ := withTx_ok accepted + obtain ⟨_, -, h⟩ := bind_ok h + split at h + next fresh => + obtain ⟨_, -, h⟩ := bind_ok h + cases pure_ok h + have live := txOf_found _ sid tid t tx + exact .snapshot store (by split <;> rfl) (by split <;> rfl) (by split <;> rfl) + live fresh rfl rfl + next => cases h + +private theorem stepEvent_effect_apply (w next : World) (store tx version term : Nat) + (writes : Pending) + (accepted : stepEvent w (.apply store tx version term writes) = .ok next) + : StepEffect w (.apply store tx version term writes) next := by + obtain ⟨s, store, accepted⟩ := bind_ok accepted + obtain ⟨t, tx, accepted⟩ := bind_ok accepted + obtain ⟨_, -, accepted⟩ := bind_ok accepted + obtain ⟨_, -, accepted⟩ := bind_ok accepted + obtain ⟨_, -, accepted⟩ := bind_ok accepted + obtain ⟨_, -, accepted⟩ := bind_ok accepted + split at accepted + next new applied => + obtain ⟨_, same, accepted⟩ := bind_ok accepted + cases pure_ok same + obtain ⟨_, -, accepted⟩ := bind_ok accepted + cases pure_ok accepted + exact .apply store tx applied rfl rfl + next => + obtain ⟨_, rejected, -⟩ := bind_ok accepted + cases rejected + +private theorem stepEvent_effect_get (w next : World) (store tx : Nat) (map key : String) + (value : Option String) (global : Bool) + (accepted : stepEvent w (.get store tx map key value global) = .ok next) + : StepEffect w (.get store tx map key value global) next := by + refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted + obtain ⟨_, -, h⟩ := bind_ok h + split at h + · repeat obtain ⟨_, -, h⟩ := bind_ok h + cases pure_ok h + exact .refl _ + · exact runOp_frozen h + +private theorem stepEvent_effect_has (w next : World) (store tx : Nat) (map key : String) + (value : Bool) (global : Bool) + (accepted : stepEvent w (.has store tx map key value global) = .ok next) + : StepEffect w (.has store tx map key value global) next := by + refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted + obtain ⟨_, -, h⟩ := bind_ok h + split at h + · repeat obtain ⟨_, -, h⟩ := bind_ok h + cases pure_ok h + exact .refl _ + · repeat obtain ⟨_, -, h⟩ := bind_ok h + exact runOp_frozen h + +private theorem stepEvent_effect_previous (w next : World) (store tx : Nat) + (map key : String) (value : Option Nat) + (accepted : stepEvent w (.previous store tx map key value) = .ok next) + : StepEffect w (.previous store tx map key value) next := by + refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted + repeat obtain ⟨_, -, h⟩ := bind_ok h + exact runOp_frozen h + +private theorem stepEvent_effect_put (w next : World) (store tx : Nat) + (map key value : String) + (accepted : stepEvent w (.put store tx map key value) = .ok next) + : StepEffect w (.put store tx map key value) next := by + refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted + repeat obtain ⟨_, -, h⟩ := bind_ok h + exact runOp_frozen h + +private theorem stepEvent_effect_remove (w next : World) (store tx : Nat) + (map key : String) (accepted : stepEvent w (.remove store tx map key) = .ok next) + : StepEffect w (.remove store tx map key) next := by + refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted + repeat obtain ⟨_, -, h⟩ := bind_ok h + exact runOp_frozen h + +private theorem stepEvent_effect_size (w next : World) (store tx : Nat) (map : String) + (value : Nat) (accepted : stepEvent w (.size store tx map value) = .ok next) + : StepEffect w (.size store tx map value) next := by + refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted + repeat obtain ⟨_, -, h⟩ := bind_ok h + exact runOp_frozen h + +private theorem stepEvent_effect_range (w next : World) (store tx : Nat) (map : String) + (lower upper : Option String) (entries : Assoc String String) + (accepted : stepEvent w (.range store tx map lower upper entries) = .ok next) + : StepEffect w (.range store tx map lower upper entries) next := by + refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted + obtain ⟨_, -, h⟩ := bind_ok h + split at h + · obtain ⟨_, -, h⟩ := bind_ok h + cases pure_ok h + exact .refl _ + · obtain ⟨_, -, h⟩ := bind_ok h + exact runOp_frozen h + +private theorem stepEvent_effect_clear (w next : World) (store tx : Nat) (map : String) + (accepted : stepEvent w (.clear store tx map) = .ok next) + : StepEffect w (.clear store tx map) next := by + refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted + obtain ⟨_, -, h⟩ := bind_ok h + obtain ⟨_, one, h⟩ := bind_ok h + exact (runOp_frozen one).trans (clearWrites_frozen h) + +private theorem stepEvent_effect_foreachBegin (w next : World) (store tx : Nat) + (map : String) (iteration : Nat) + (accepted : stepEvent w (.foreachBegin store tx map iteration) = .ok next) + : StepEffect w (.foreachBegin store tx map iteration) next := by + refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted + obtain ⟨_, -, h⟩ := bind_ok h + obtain ⟨_, -, h⟩ := bind_ok h + obtain ⟨_, one, h⟩ := bind_ok h + cases pure_ok h + exact (runOp_frozen one).trans (.fields rfl rfl rfl rfl) + +private theorem stepEvent_effect_unavailable (w next : World) (store tx : Nat) + (map : String) (accepted : stepEvent w (.unavailable store tx map) = .ok next) + : StepEffect w (.unavailable store tx map) next := by + obtain ⟨_, -, accepted⟩ := bind_ok accepted + refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted + repeat obtain ⟨_, -, h⟩ := bind_ok h + cases pure_ok h + exact .fields rfl rfl rfl rfl + +private theorem stepEvent_effect_commitResult (w next : World) (store tx : Nat) + (result : Outcome) (version : Nat) + (accepted : stepEvent w (.commitResult store tx result version) = .ok next) + : StepEffect w (.commitResult store tx result version) next := by + refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted + split at h + next => + obtain ⟨_, -, h⟩ := bind_ok h + cases pure_ok h + exact .fields rfl rfl rfl rfl + next => + obtain ⟨_, -, h⟩ := bind_ok h + split at h + · obtain ⟨_, -, h⟩ := bind_ok h + cases pure_ok h + exact .fields rfl rfl rfl rfl + · cases pure_ok h + exact .fields rfl rfl rfl rfl + next => + obtain ⟨_, -, h⟩ := bind_ok h + cases pure_ok h + exact .fields rfl rfl rfl rfl + +private theorem stepEvent_effect (w next : World) (e : Event) + (accepted : stepEvent w e = .ok next) + : StepEffect w e next := by + cases e with + | traceStart | caseBegin | caseEnd | subcaseBegin | subcaseEnd | traceEnd => + repeat obtain ⟨_, -, accepted⟩ := bind_ok accepted + cases pure_ok accepted + exact .same rfl rfl fun _ => rfl + | rollbackRejected => exact stepEvent_effect_rollbackRejected w next _ _ _ accepted + | unsupported => cases accepted + | storeCreate => exact stepEvent_effect_storeCreate w next _ accepted + | storeEnd => exact stepEvent_effect_storeEnd w next _ accepted + | txCreate => exact stepEvent_effect_txCreate w next _ _ accepted + | txEnd => exact stepEvent_effect_txEnd w next _ _ accepted + | compact => + obtain ⟨s, store, accepted⟩ := bind_ok accepted + repeat obtain ⟨_, -, accepted⟩ := bind_ok accepted + cases pure_ok accepted + exact .compact store rfl rfl + | rollback => + obtain ⟨s, store, accepted⟩ := bind_ok accepted + repeat obtain ⟨_, -, accepted⟩ := bind_ok accepted + cases pure_ok accepted + exact .rollback store rfl rfl + | snapshot => exact stepEvent_effect_snapshot w next _ _ _ _ _ accepted + | acquire => + obtain ⟨s, store, accepted⟩ := bind_ok accepted + obtain ⟨t, t', tx, h, rfl⟩ := withTx_ok accepted + exact .acquire store tx h rfl rfl + | apply => exact stepEvent_effect_apply w next _ _ _ _ _ accepted + | get => exact stepEvent_effect_get w next _ _ _ _ _ _ accepted + | has => exact stepEvent_effect_has w next _ _ _ _ _ _ accepted + | previous => exact stepEvent_effect_previous w next _ _ _ _ _ accepted + | put => exact stepEvent_effect_put w next _ _ _ _ _ accepted + | remove => exact stepEvent_effect_remove w next _ _ _ _ accepted + | size => exact stepEvent_effect_size w next _ _ _ _ accepted + | range => exact stepEvent_effect_range w next _ _ _ _ _ _ accepted + | clear => exact stepEvent_effect_clear w next _ _ _ accepted + | foreachBegin => exact stepEvent_effect_foreachBegin w next _ _ _ _ accepted + | foreachEntry | foreachContinue | foreachEnd => + refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted + obtain ⟨⟨_, _⟩, -, h⟩ := bind_ok h + repeat obtain ⟨_, -, h⟩ := bind_ok h + cases pure_ok h + exact .fields rfl rfl rfl rfl + | unavailable => exact stepEvent_effect_unavailable w next _ _ _ accepted + | commitBegin => + refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted + repeat obtain ⟨_, -, h⟩ := bind_ok h + cases pure_ok h + exact .fields rfl rfl rfl rfl + | commitResult => exact stepEvent_effect_commitResult w next _ _ _ _ accepted + +private theorem stepEvent_invariant (w next : World) (valid : WorldInvariant w) + (e : Event) (accepted : stepEvent w e = .ok next) + : WorldInvariant next := by + cases stepEvent_effect w next e accepted with + | same stores txs => + exact ⟨by rw [stores]; exact valid.stores, by rw [txs]; exact valid.txs⟩ + | storeCreate stores txs => + exact ⟨ + by rw [stores]; exact lookup_set_invariant _ _ valid.stores _ _ store_initial, + by rw [txs]; exact valid.txs + ⟩ + | storeEnd stores txs => + exact ⟨ + by rw [stores]; exact lookup_erase_invariant _ _ valid.stores _, + by rw [txs]; exact valid.txs + ⟩ + | txCreate stores txs => + exact ⟨ + by rw [stores]; exact valid.stores, + by rw [txs]; exact lookup_set_invariant _ _ valid.txs _ _ (tx_initial _) + ⟩ + | txEnd stores txs => + exact ⟨ + by rw [stores]; exact valid.stores, + by rw [txs]; exact lookup_erase_invariant _ _ valid.txs _ + ⟩ + | compact store stores txs => + exact ⟨ + by + rw [stores] + exact lookup_set_invariant _ _ valid.stores _ _ + (compact_invariant _ (storeOf_invariant w valid _ _ store) _), + by rw [txs]; exact valid.txs + ⟩ + | rollback store stores txs => + exact ⟨ + by + rw [stores] + exact lookup_set_invariant _ _ valid.stores _ _ + (rollback_invariant _ (storeOf_invariant w valid _ _ store) _ _), + by rw [txs]; exact valid.txs + ⟩ + | snapshot store history head globalCut tx fresh stores txs => + have shape := storeOf_invariant w valid _ _ store + refine ⟨?_, ?_⟩ + · rw [stores] + refine lookup_set_invariant _ _ valid.stores _ _ ⟨?_, ?_, ?_⟩ + · rw [history, head]; exact shape.historyShape + · rw [history, head]; exact shape.headFirst + · rw [globalCut, head]; exact shape.globalBound + · rw [txs] + exact lookup_set_invariant _ _ valid.txs _ _ + (snapshot_invariant _ shape _ _ (valid.txs _ _ tx) fresh) + | acquire store tx acquired stores txs => + exact ⟨ + by rw [stores]; exact valid.stores, + by + rw [txs] + exact lookup_set_invariant _ _ valid.txs _ _ + (acquireMap_invariant _ (storeOf_invariant w valid _ _ store) _ _ + (txOf_invariant w valid _ _ _ tx) _ _ _ acquired) + ⟩ + | apply store tx applied stores txs => + exact ⟨ + by + rw [stores] + exact lookup_set_invariant _ _ valid.stores _ _ + (tryApply_invariant _ _ (storeOf_invariant w valid _ _ store) _ applied), + by + rw [txs] + exact lookup_set_invariant _ _ valid.txs _ _ + (tx_fields_invariant _ _ (txOf_invariant w valid _ _ _ tx) rfl rfl rfl rfl) + ⟩ + | update tx frozen stores txs => + exact ⟨ + by rw [stores]; exact valid.stores, + by + rw [txs] + exact lookup_set_invariant _ _ valid.txs _ _ + (frozen.valid (txOf_invariant w valid _ _ _ tx)) + ⟩ + +private theorem step_ok {w next : World} {r : Record} (accepted : step w r = .ok next) + : ∃ eventNext, + stepEvent w r.event = .ok eventNext + ∧ next = { eventNext with lastSeq := some r.seq, count := w.count + 1 } := by + obtain ⟨_, -, accepted⟩ := bind_ok accepted + obtain ⟨_, -, accepted⟩ := bind_ok accepted + obtain ⟨seq, event⟩ := r + dsimp only at accepted ⊢ + split at accepted <;> try split at accepted + all_goals first + | obtain ⟨_, invalid, -⟩ := bind_ok accepted; cases invalid + | obtain ⟨eventNext, event, accepted⟩ := bind_ok accepted + exact ⟨eventNext, event, (pure_ok accepted).symm⟩ + +private theorem step_invariant (w next : World) (valid : WorldInvariant w) (r : Record) + (accepted : step w r = .ok next) + : WorldInvariant next := by + obtain ⟨_, event, rfl⟩ := step_ok accepted + have eventValid := stepEvent_invariant w _ valid r.event event + exact ⟨eventValid.stores, eventValid.txs⟩ + +private theorem reachable_invariant (w : World) (reachable : transitionSystem.Reachable w) + : WorldInvariant w := by + induction reachable using @CCF.TransitionSystem.Reachable.rec transitionSystem with + | initial initialized => cases initialized; exact world_initial + | step _ transition ih => + exact step_invariant _ _ ih _ ((Execution.step_iff_transition _ _ _).mp transition) + +end Kv.Proofs.Invariants + +namespace Kv.Proofs.Model + +open Kv.Model Kv.Proofs.Invariants Kv.Properties +section Generic +variable {M K V : Type} [DecidableEq M] [DecidableEq K] + +private theorem erase_keys (xs : Assoc K V) (k : K) + : (erase xs k).map Prod.fst = (xs.map Prod.fst).filter (· != k) := + (List.filter_map (f := Prod.fst) (p := (· != k)) (l := xs)).symm + +private theorem erase_unique (xs : Assoc K V) (k : K) (h : Kv.Properties.Unique xs) + : Kv.Properties.Unique (erase xs k) := by + unfold Kv.Properties.Unique + rw [erase_keys] + exact List.Pairwise.filter _ h + +private theorem set_unique (xs : Assoc K V) (k : K) (v : V) (h : Kv.Properties.Unique xs) + : Kv.Properties.Unique (set xs k v) := by + simp only [Kv.Properties.Unique, Model.set, List.map_cons, List.nodup_cons] + constructor + · simp [erase_keys, eq_comm] + · exact erase_unique xs k h + +private theorem publish_lookup (db : DB M K V) (version : Nat) (ws : Writes M K V) + (a : Addr M K) + : find (publish db version ws) a + = match find ws a with + | none => find db a + | some none => none + | some (some v) => some { value := v, version } := by + induction ws with + | nil => rfl + | cons p ws ih => + rcases p with ⟨b, value⟩ + by_cases h : b = a + · subst b + cases value <;> simp [publish, find, find_set_same, find_erase_same] + · cases value <;> simp [publish, find, h, find_set_other, find_erase_other, ← ih, publish] + +private theorem publish_unique (db : DB M K V) (version : Nat) (ws : Writes M K V) + (h : Kv.Properties.Unique db) + : Kv.Properties.Unique (publish db version ws) := by + induction ws with + | nil => exact h + | cons p ws ih => + rcases p with ⟨a, v⟩ + cases v with + | none => exact erase_unique _ a ih + | some value => exact set_unique _ a ⟨value, version⟩ ih + +end Generic +end Kv.Proofs.Model + +namespace Kv.Proofs.Model + +open Kv.Model Kv.Proofs.Invariants Kv.Properties +section Generic +variable {M K V : Type} [DecidableEq M] [DecidableEq K] +variable [DecidableEq V] + +private theorem validates_append (db : DB M K V) (a b : List (Dependency M K V)) + : validates db (a ++ b) = (validates db a && validates db b) := by + simp [validates] + +private theorem serialStep_eq (base : DB M K V) (ws : Writes M K V) (op : NormalOp M K V) + : serialStep base ws op + = if observes base ws op then some (stage ws op) else none := by + cases op <;> simp [serialStep, observes, stage] + +private theorem dependency_rebase (snapshot current : DB M K V) (ws : Writes M K V) + (op : NormalOp M K V) + (hv : validates current (needs snapshot ws op) = true) + : observes snapshot ws op = observes current ws op := by + cases op with + | read a v => + cases hw : find ws a with + | none => + have heq : find current a = find snapshot a := by + simpa [needs, hw, validates, Dependency.holds] using hv + simp [observes, valueAt, hw, heq] + | some value => simp [observes, valueAt, hw] + | previous a v => + have heq : find current a = find snapshot a := by + simpa [needs, validates, Dependency.holds] using hv + apply decide_eq_decide.mpr + simp only [previousAt, heq] + | scan m vs => + have heq : image current m = image snapshot m := by + simpa [needs, validates, Dependency.holds] using hv + apply decide_eq_decide.mpr + simp only [scanAt, heq] + | write _ _ => rfl + +private theorem normalStep_prefix_valid (snapshot current : DB M K V) + (n n' : Normal M K V) (op : NormalOp M K V) + (hs : normalStep snapshot n op = some n') + (hv : validates current n'.deps = true) + : validates current n.deps = true := by + unfold normalStep at hs + split at hs + next h => + cases hs + have hh : validates current (needs snapshot n.writes op) = true ∧ + validates current n.deps = true := by simpa [validates_append] using hv + exact hh.2 + next h => simp at hs + +private theorem normalStep_rebase (snapshot current : DB M K V) + (n n' : Normal M K V) (op : NormalOp M K V) + (hs : normalStep snapshot n op = some n') + (hv : validates current n'.deps = true) + : serialStep current n.writes op = some n'.writes := by + unfold normalStep at hs + split at hs + next h => + cases hs + have hh : validates current (needs snapshot n.writes op) = true ∧ + validates current n.deps = true := by simpa [validates_append] using hv + have hneeds := hh.1 + have hobs := dependency_rebase snapshot current n.writes op hneeds + rw [serialStep_eq, ← hobs] + simp [h] + next h => simp at hs + +private theorem normalRun_prefix_valid (snapshot current : DB M K V) + (ops : List (NormalOp M K V)) (n n' : Normal M K V) + (hr : normalRun snapshot n ops = some n') + (hv : validates current n'.deps = true) + : validates current n.deps = true := by + induction ops generalizing n with + | nil => simp [normalRun] at hr; subst n'; exact hv + | cons op ops ih => + cases hs : normalStep snapshot n op with + | none => simp [normalRun, hs] at hr + | some next => + have ht : normalRun snapshot next ops = some n' := by + simpa [normalRun, hs] using hr + exact normalStep_prefix_valid snapshot current n next op hs (ih next ht) + +/-- Arbitrary finite OCC programs, including cross-map/absent/scan reads, +replay with identical observations immediately before their application. +The only rebase premise is the executable dependency check, not a serial oracle. -/ +private theorem normalRun_serial (snapshot current : DB M K V) + (ops : List (NormalOp M K V)) (n n' : Normal M K V) + (hr : normalRun snapshot n ops = some n') + (hv : validates current n'.deps = true) + : serialRun current n.writes ops = some n'.writes := by + induction ops generalizing n with + | nil => simp [normalRun] at hr; subst n'; rfl + | cons op ops ih => + cases hs : normalStep snapshot n op with + | none => simp [normalRun, hs] at hr + | some next => + have ht : normalRun snapshot next ops = some n' := by + simpa [normalRun, hs] using hr + have hp := normalRun_prefix_valid snapshot current ops next n' ht hv + have hstep := normalStep_rebase snapshot current n next op hs hp + simp [serialRun, hstep, ih next ht] + +private theorem validates_self (snapshot : DB M K V) (ws : Writes M K V) + (op : NormalOp M K V) + : validates snapshot (needs snapshot ws op) = true := by + cases op <;> simp [needs, validates, Dependency.holds] + +private theorem normalRun_snapshot_valid (snapshot : DB M K V) + (ops : List (NormalOp M K V)) (n n' : Normal M K V) + (hn : validates snapshot n.deps = true) (hr : normalRun snapshot n ops = some n') + : validates snapshot n'.deps = true := by + induction ops generalizing n with + | nil => simp [normalRun] at hr; subst n'; exact hn + | cons op ops ih => + cases hs : normalStep snapshot n op with + | none => simp [normalRun, hs] at hr + | some next => + apply ih next + · unfold normalStep at hs + split at hs + next h => + cases hs + simp [validates_append, validates_self, hn] + next h => simp at hs + · simpa [normalRun, hs] using hr + +private theorem readonly_snapshot_serial (snapshot : DB M K V) + (ops : List (NormalOp M K V)) (n : Normal M K V) + (hr : normalRun snapshot {} ops = some n) + : serialRun snapshot [] ops = some n.writes := + normalRun_serial snapshot snapshot ops {} n hr + (normalRun_snapshot_valid snapshot ops {} n (by rfl) hr) + +end Generic +end Kv.Proofs.Model + +namespace Kv.Proofs.Model + +open Kv.Model Kv.Proofs.Invariants Kv.Properties + +private theorem compact_preserves_head (s : Store) (v : Nat) + : (compactStore s v).head = s.head := by + unfold compactStore + split <;> rfl + +private theorem rollback_preserves_earlier_cuts (s : Store) (v term cut : Nat) + (hcut : cut ≤ v) (hhead : cut ≤ s.head.version) + : atCut (rollbackStore s v term) cut = atCut s cut := by + have hmono : ∀ f : Frame, f.version ≤ cut → f.version ≤ rollbackCut s v := fun f h => + Nat.le_trans h (Nat.le_trans (Nat.le_min.mpr ⟨hhead, hcut⟩) (Nat.le_max_right _ _)) + unfold atCut rollbackStore + congr 1 + rw [List.find?_filter] + congr 1 + exact funext fun f => by by_cases h : f.version ≤ cut <;> simp [h, hmono f] + +private theorem durable_cut_survives_rollback (s : Store) (v term cut : Nat) + (valid : StoreInvariant s) (hcut : cut ≤ s.global) (hboundary : s.global ≤ v) + : (atCut (rollbackStore s v term) cut).data = (atCut s cut).data := by + rw [rollback_preserves_earlier_cuts s v term cut (Nat.le_trans hcut hboundary) + (Nat.le_trans hcut valid.globalBound)] + +private theorem transaction_snapshot_serial (t : Tx) (snap : Snapshot) + (valid : NormalInvariant t) (hs : t.snapshot = some snap) + : serialRun t.data [] t.normal.log = some t.normal.writes := by + have hc : normalRun t.data {} t.normal.log = some t.normal := by + simpa [NormalInvariant, hs] using valid + exact readonly_snapshot_serial t.data t.normal.log t.normal hc + +/-- A valid attempt that passes OCC agrees with serial execution on the current head. -/ +private theorem transaction_application_serial (s : Store) (t : Tx) (snap : Snapshot) + (valid : NormalInvariant t) + (hs : t.snapshot = some snap) (hv : canApply s t = true) + : serialRun s.head.data [] t.normal.log = some t.normal.writes := by + have canApply_validates (s : Store) (t : Tx) (h : canApply s t = true) + : validates s.head.data t.normal.deps = true := by + have hh : (!t.unavailable && validLineage s t) = true ∧ + validates s.head.data t.normal.deps = true := by simpa [canApply] using h + exact hh.2 + have hc : normalRun t.data {} t.normal.log = some t.normal := by + simpa [NormalInvariant, hs] using valid + exact normalRun_serial t.data s.head.data t.normal.log {} t.normal hc + (canApply_validates s t hv) + +private theorem tryApply_serial (s next : Store) (t : Tx) (valid : NormalInvariant t) + (ha : tryApply s t = some next) + : serialRun s.head.data [] t.normal.log = some t.normal.writes + ∧ next.head.data = publish s.head.data (s.head.version + 1) t.normal.writes := by + unfold tryApply at ha + split at ha + next hv => + cases ha + refine ⟨?_, rfl⟩ + cases hs : t.snapshot with + | none => + have hc : t.normal = {} := by simpa [NormalInvariant, hs] using valid + simp [hc, serialRun] + | some snap => exact transaction_application_serial s t snap valid hs hv + next => simp at ha + +private theorem executable_branch_serializability (s final : Store) (ts : List Tx) + (valid : ∀ t ∈ ts, NormalInvariant t) + (h : AppliedBranch s ts final) + : serialTransactions s.head.data s.head.version ts = some final.head.data := by + induction h with + | nil s => rfl + | compact s final v ts _rest ih => + simpa only [compact_preserves_head] using ih valid + | cons s middle final t ts one rest ih => + have hw := tryApply_serial s middle t (valid t (by simp)) one + have hversion : middle.head.version = s.head.version + 1 := by + unfold tryApply at one + split at one + next => cases one; rfl + next => simp at one + simp only [serialTransactions, hw.1, Option.bind_some] + rw [← hw.2, ← hversion] + exact ih (fun tx member => valid tx (by simp [member])) + +end Kv.Proofs.Model + +namespace Kv.Proofs.Trace + +open Kv.Model Kv.Proofs.Invariants Kv.Properties Kv.Proofs.Model + +/-- The head of `after` is that of `before`, or follows from it by applying the listed attempt. -/ +private inductive HeadEffect (before after : Store) : List Tx → Prop + /-- The head data and version are unchanged. -/ + | stutter (data : after.head.data = before.head.data) + (version : after.head.version = before.head.version) + : HeadEffect before after [] + /-- One attempt is applied. -/ + | apply (tx : Tx) (one : tryApply before tx = some after) : HeadEffect before after [tx] + +private theorem storeOf_ok (w : World) (sid : Nat) (s : Store) + : storeOf w sid = .ok s ↔ find w.stores sid = some s := by + cases h : find w.stores sid <;> simp [storeOf, present, invalid, h] + +private theorem stable_update_store_effect (w next : World) (sid id : Nat) + (s old new : Store) (hs : find w.stores sid = some s) + (hold : find w.stores id = some old) (same : next.stores = set w.stores id new) + (head : new.head = old.head) + : ∃ after, find next.stores sid = some after ∧ HeadEffect s after [] := by + by_cases h : id = sid + · subst id + have ho : old = s := Option.some.inj (hold.symm.trans hs) + subst old + exact ⟨new, by simp [same, find_set_same], .stutter (congrArg Frame.data head) + (congrArg Frame.version head)⟩ + · exact ⟨s, by simpa [same, find_set_other _ id sid new h] using hs, .stutter rfl rfl⟩ + +private theorem stepEvent_store_effect (w next : World) (sid : Nat) (s : Store) + (e : Event) (hs : find w.stores sid = some s) (segment : SegmentEvent sid e) + (accepted : stepEvent w e = .ok next) + : ∃ after, + find next.stores sid = some after + ∧ HeadEffect s after (projectedApplication w sid e) := by + have unchanged_store_effect (w next : World) (sid : Nat) (s : Store) (e : Event) + (hs : find w.stores sid = some s) (same : next.stores = w.stores) + (noApply : projectedApplication w sid e = []) + : ∃ after, + find next.stores sid = some after + ∧ HeadEffect s after (projectedApplication w sid e) := by + refine ⟨s, ?_, ?_⟩ + · simpa [same] using hs + · rw [noApply] + exact .stutter rfl rfl + have applied_update_store_effect (w next : World) (sid id tid : Nat) + (s old new : Store) (t : Tx) + (hs : find w.stores sid = some s) (hold : storeOf w id = .ok old) + (htx : txOf w id tid = .ok t) (ha : tryApply old t = some new) + (same : next.stores = set w.stores id new) + : ∃ after, + find next.stores sid = some after + ∧ HeadEffect s after + (if id = sid then (txOf w id tid).toOption.toList else []) := by + have hf := (storeOf_ok w id old).mp hold + by_cases h : id = sid + · subst id + have ho : old = s := Option.some.inj (hf.symm.trans hs) + subst old + refine ⟨new, by simp [same, find_set_same], ?_⟩ + simpa [htx, Except.toOption, Option.toList] using HeadEffect.apply t ha + · refine ⟨s, by simpa [same, find_set_other _ id sid new h] using hs, ?_⟩ + simpa [h] using HeadEffect.stutter (before := s) rfl rfl + cases stepEvent_effect w next e accepted with + | same stores _ noApply => + exact unchanged_store_effect w next sid s _ hs stores (noApply sid) + | storeCreate stores _ | rollback _ stores _ => + exact ⟨ + s, + by rw [stores, find_set_other _ _ _ _ segment]; exact hs, + .stutter rfl rfl + ⟩ + | storeEnd stores _ => + exact ⟨ + s, + by rw [stores, find_erase_other _ _ _ segment]; exact hs, + .stutter rfl rfl + ⟩ + | txCreate stores _ | txEnd stores _ | acquire _ _ _ stores _ => + exact unchanged_store_effect w next sid s _ hs stores rfl + | compact store stores _ => + exact stable_update_store_effect w next sid _ s _ _ hs ((storeOf_ok _ _ _).mp store) stores + (compact_preserves_head _ _) + | snapshot store _ head _ _ _ stores _ => + exact stable_update_store_effect w next sid _ s _ _ hs ((storeOf_ok _ _ _).mp store) stores + head + | apply store tx applied stores _ => + exact applied_update_store_effect w next sid _ _ s _ _ _ hs store tx applied stores + | update _ _ stores _ noApply => + exact unchanged_store_effect w next sid s _ hs stores (noApply sid) + +private theorem step_event_result (w next : World) (r : Record) + (accepted : step w r = .ok next) + : ∃ eventNext, + stepEvent w r.event = .ok eventNext + ∧ next.stores = eventNext.stores + ∧ next.txs = eventNext.txs := by + obtain ⟨eventNext, event, rfl⟩ := step_ok accepted + exact ⟨eventNext, event, rfl, rfl⟩ + +private theorem HeadEffect.serial_witness (before after : Store) (txs : List Tx) + (valid : ∀ t ∈ txs, NormalInvariant t) + (effect : HeadEffect before after txs) + : serialTransactions before.head.data before.head.version txs = some after.head.data + ∧ after.head.version = before.head.version + txs.length := by + cases effect with + | stutter data version => simp [serialTransactions, data, version] + | apply tx one => + have h := tryApply_serial before after tx (valid tx (by simp)) one + constructor + · simpa [serialTransactions, h.1] using congrArg some h.2.symm + · unfold tryApply at one + split at one + next => cases one; rfl + next => simp at one + +private theorem serialTransactions_append (db : Data) (version : Nat) (xs ys : List Tx) + : serialTransactions db version (xs ++ ys) + = (serialTransactions db version xs).bind + (fun next => serialTransactions next (version + xs.length) ys) := by + induction xs generalizing db version with + | nil => rfl + | cons tx xs ih => + cases h : serialRun db [] tx.normal.log with + | none => simp [serialTransactions, h] + | some writes => + simp [serialTransactions, h, ih, Nat.add_comm, Nat.add_left_comm] + +private theorem projectedApplication_normal (w : World) (valid : WorldInvariant w) + (sid : Nat) (e : Event) + : ∀ t ∈ projectedApplication w sid e, NormalInvariant t := by + cases e <;> simp only [projectedApplication] + all_goals try exact fun _ member => False.elim (List.not_mem_nil member) + rename_i id tid version term writes + intro t member + by_cases same : id = sid + · subst id + simp only [ite_true] at member + cases lookup : txOf w sid tid with + | error err => simp [lookup, Except.toOption] at member + | ok tx => + have equal : t = tx := by + simpa [lookup, Except.toOption, Option.toList] using member + subst t + exact (txOf_invariant w valid sid tid tx lookup).normal + · simp [same] at member + +/-- A selected store stays live throughout the segment. Its rollback/create/end +events partition segments; all other-store events are permitted. The projected +attempts are obtained from the real pre-event txOf, not supplied as a premise. -/ +private theorem replay_segment_serializability (w final : World) (sid : Nat) (s : Store) + (valid : WorldInvariant w) + (rs : List Record) (live : find w.stores sid = some s) + (segment : ∀ r ∈ rs, SegmentEvent sid r.event) + (accepted : replay w rs = .ok final) + : ∃ after txs, + find final.stores sid = some after + ∧ projectApplications w sid rs = .ok txs + ∧ serialTransactions s.head.data s.head.version txs = some after.head.data + ∧ after.head.version = s.head.version + txs.length := by + have step_store_effect (w next : World) (sid : Nat) (s : Store) (r : Record) + (hs : find w.stores sid = some s) (segment : SegmentEvent sid r.event) + (accepted : step w r = .ok next) + : ∃ after, + find next.stores sid = some after + ∧ HeadEffect s after (projectedApplication w sid r.event) := by + obtain ⟨eventNext, he, stores, _⟩ := step_event_result w next r accepted + obtain ⟨after, found, effect⟩ := stepEvent_store_effect w eventNext sid s r.event hs segment he + exact ⟨after, by simpa [stores] using found, effect⟩ + induction rs generalizing w s with + | nil => + cases accepted + exact ⟨s, [], live, rfl, rfl, by simp⟩ + | cons r rs ih => + cases first : step w r with + | error err => simp [replay, first, Except.bind] at accepted + | ok middle => + have rest : replay middle rs = .ok final := by + simpa [replay, first, Except.bind] using accepted + obtain ⟨nextStore, nextLive, effect⟩ := step_store_effect w middle sid s r live + (segment r (by simp)) first + obtain ⟨after, tailTxs, afterLive, projected, tailSerial, tailVersion⟩ := + ih middle nextStore (step_invariant w middle valid r first) nextLive + (fun e he => segment e (by simp [he])) rest + have applications := projectedApplication_normal w valid sid r.event + have one := HeadEffect.serial_witness s nextStore _ applications effect + refine ⟨ + after, + projectedApplication w sid r.event ++ tailTxs, + afterLive, + ?_, + ?_, + ?_ + ⟩ + · simp [projectApplications, first, projected, Bind.bind, Except.bind, Pure.pure, Except.pure] + · rw [serialTransactions_append, one.1] + simpa [← one.2] using tailSerial + · simp only [List.length_append] + rw [tailVersion, one.2] + exact Nat.add_assoc _ _ _ + +private theorem History.head_cells_bounded (fs : List Frame) (n : Nat) + (shape : History fs n) + : CellsBounded (fs.head?.getD {}).data n := by + have publish_cells_bounded (db : Data) (version : Nat) (writes : Pending) + (before : CellsBounded db version) + : CellsBounded (publish db version writes) version := by + intro key cell found + rw [publish_lookup] at found + cases hw : find writes key with + | none => exact before key cell (by simpa [hw] using found) + | some value => + cases value with + | none => simp [hw] at found + | some v => + simp [hw] at found + cases found + exact Nat.le_refl _ + induction shape with + | zero => + intro key cell found + simp [find] at found + | succ f n fs _version effect _tail ih => + obtain ⟨writes, published⟩ := effect + simp only [List.head?_cons, Option.getD_some] + rw [published] + apply publish_cells_bounded + intro key cell found + exact Nat.le_trans (ih key cell found) (Nat.le_succ n) + +private theorem History.head_unique (fs : List Frame) (n : Nat) (shape : History fs n) + : Kv.Properties.Unique (fs.head?.getD {}).data := by + induction shape with + | zero => simp [Kv.Properties.Unique] + | succ f n fs _version effect _tail ih => + obtain ⟨writes, published⟩ := effect + simp only [List.head?_cons, Option.getD_some] + rw [published] + exact publish_unique _ _ _ ih + +private theorem map_global_view_safety (view : GlobalView) (valid : GlobalInvariant view) + : view.frame = {} + ∨ ∃ origin : Store, + view.frame = atCut origin origin.global + ∧ view.frame.version = origin.global + ∧ CellsBounded view.frame.data origin.global := by + have atCut_cells_bounded (s : Store) (valid : StoreInvariant s) + (cut : Nat) (within : cut ≤ s.head.version) + : CellsBounded (atCut s cut).data cut := by + have spec := atCut_spec s valid cut within + have h := History.head_cells_bounded _ cut spec.2.1 + simpa only [spec.2.2, Option.getD_some] using h + rcases valid with placeholder | ⟨origin, store, committed⟩ + · exact Or.inl placeholder + · refine Or.inr ⟨origin, committed, ?_, ?_⟩ + · rw [committed]; exact (atCut_spec origin store origin.global store.globalBound).1 + · rw [committed]; exact atCut_cells_bounded origin store origin.global store.globalBound + +theorem replay_segment_serializability_claim + : ∀ (w final : World) (sid : Nat) (s : Store) (rs : List Record), + Model.transitionSystem.Reachable w + → find w.stores sid = some s + → (∀ r ∈ rs, SegmentEvent sid r.event) + → CCF.Execution.Run Model.transitionSystem w rs final + → ∃ after txs, + find final.stores sid = some after + ∧ projectApplications w sid rs = .ok txs + ∧ serialTransactions s.head.data s.head.version txs = some after.head.data + ∧ after.head.version = s.head.version + txs.length := by + intro w final sid s rs reachable live segment accepted + exact Proofs.Trace.replay_segment_serializability w final sid s + (Invariants.reachable_invariant w reachable) rs live segment ((Proofs.Execution.replay_iff_run _ _ _).mp accepted) + +theorem reachable_store_invariants_claim + : ∀ (w : World) (sid : Nat) (s : Store), + Model.transitionSystem.Reachable w + → find w.stores sid = some s + → History s.history s.head.version + ∧ s.history.head? = some s.head + ∧ s.global ≤ s.head.version + ∧ (atCut s s.global).version = s.global := by + have reachable_store_invariants (w : World) + (valid : WorldInvariant w) + (sid : Nat) (s : Store) (_live : find w.stores sid = some s) + : History s.history s.head.version + ∧ s.history.head? = some s.head + ∧ s.global ≤ s.head.version + ∧ (atCut s s.global).version = s.global := by + have store := valid.stores sid s _live + exact ⟨store.historyShape, store.headFirst, store.globalBound, + (atCut_spec s store s.global store.globalBound).1⟩ + intro w sid s reachable live + exact reachable_store_invariants w (Invariants.reachable_invariant w reachable) sid s + live + +theorem reachable_store_data_invariants_claim + : ∀ (w : World) (sid : Nat) (s : Store), + Model.transitionSystem.Reachable w + → find w.stores sid = some s + → Kv.Properties.Unique s.head.data ∧ CellsBounded s.head.data s.head.version := by + have reachable_store_data_invariants (w : World) + (valid : WorldInvariant w) + (sid : Nat) (s : Store) (_live : find w.stores sid = some s) + : Kv.Properties.Unique s.head.data ∧ CellsBounded s.head.data s.head.version := by + have store := valid.stores sid s _live + have unique := History.head_unique s.history s.head.version store.historyShape + have bounded := History.head_cells_bounded s.history s.head.version store.historyShape + simpa only [store.headFirst, Option.getD_some] using And.intro unique bounded + intro w sid s reachable live + exact reachable_store_data_invariants w (Invariants.reachable_invariant w reachable) sid + s live + +theorem step_global_read_from_captured_map_claim + : ∀ (w next : World) (sid tid seq : Nat) (map key : String) (value : Option String) + (t : Tx) (view : GlobalView), + Model.transitionSystem.Reachable w + → txOf w sid tid = .ok t + → find t.globalViews map = some view + → Model.transitionSystem.step w ⟨seq, .get sid tid map key value true⟩ = some next + → value = (find view.frame.data (map, key)).map Cell.value + ∧ (view.frame = {} + ∨ ∃ origin : Store, + view.frame = atCut origin origin.global + ∧ view.frame.version = origin.global + ∧ CellsBounded view.frame.data origin.global) := by + have stepEvent_get_global (w next : World) (sid tid : Nat) (map key : String) + (value : Option String) (t : Tx) (view : GlobalView) + (source : txOf w sid tid = .ok t) (captured : find t.globalViews map = some view) + (accepted : stepEvent w (.get sid tid map key value true) = .ok next) + : value = (find view.frame.data (map, key)).map Cell.value := by + obtain ⟨_, _, tx, h, -⟩ := withTx_ok accepted + cases source.symm.trans tx + obtain ⟨_, -, h⟩ := bind_ok h + obtain ⟨_, found, h⟩ := bind_ok h + cases captured.symm.trans (present_ok found) + obtain ⟨_, observed, -⟩ := bind_ok h + exact (beq_iff_eq.mp (expect_ok observed)).symm + have step_global_read_from_captured_map (w next : World) (sid tid seq : Nat) + (valid : WorldInvariant w) + (map key : String) (value : Option String) (t : Tx) (view : GlobalView) + (source : txOf w sid tid = .ok t) (captured : find t.globalViews map = some view) + (accepted : step w ⟨seq, .get sid tid map key value true⟩ = .ok next) + : value = (find view.frame.data (map, key)).map Cell.value + ∧ (view.frame = {} + ∨ ∃ origin : Store, + view.frame = atCut origin origin.global + ∧ view.frame.version = origin.global + ∧ CellsBounded view.frame.data origin.global) := by + obtain ⟨eventNext, eventStep, _, _⟩ := step_event_result w next _ accepted + exact ⟨stepEvent_get_global w eventNext sid tid map key value t view source captured eventStep, + map_global_view_safety view + ((txOf_invariant w valid sid tid t source).globals map view captured)⟩ + intro w next sid tid seq map key value t view reachable source captured accepted + exact step_global_read_from_captured_map w next sid tid seq + (Invariants.reachable_invariant w reachable) map key value t view source captured + ((Proofs.Execution.step_iff_transition _ _ _).mp accepted) + +theorem step_global_has_from_captured_map_claim + : ∀ (w next : World) (sid tid seq : Nat) (map key : String) (value : Bool) (t : Tx) + (view : GlobalView), + Model.transitionSystem.Reachable w + → txOf w sid tid = .ok t + → find t.globalViews map = some view + → Model.transitionSystem.step w ⟨seq, .has sid tid map key value true⟩ = some next + → value = (find view.frame.data (map, key)).isSome + ∧ (view.frame = {} + ∨ ∃ origin : Store, + view.frame = atCut origin origin.global + ∧ view.frame.version = origin.global + ∧ CellsBounded view.frame.data origin.global) := by + have stepEvent_has_global (w next : World) (sid tid : Nat) (map key : String) + (value : Bool) (t : Tx) (view : GlobalView) + (source : txOf w sid tid = .ok t) (captured : find t.globalViews map = some view) + (accepted : stepEvent w (.has sid tid map key value true) = .ok next) + : value = (find view.frame.data (map, key)).isSome := by + obtain ⟨_, _, tx, h, -⟩ := withTx_ok accepted + cases source.symm.trans tx + obtain ⟨_, -, h⟩ := bind_ok h + obtain ⟨_, found, h⟩ := bind_ok h + cases captured.symm.trans (present_ok found) + obtain ⟨_, observed, -⟩ := bind_ok h + exact (beq_iff_eq.mp (expect_ok observed)).symm + have step_global_has_from_captured_map (w next : World) (sid tid seq : Nat) + (valid : WorldInvariant w) + (map key : String) (value : Bool) (t : Tx) (view : GlobalView) + (source : txOf w sid tid = .ok t) (captured : find t.globalViews map = some view) + (accepted : step w ⟨seq, .has sid tid map key value true⟩ = .ok next) + : value = (find view.frame.data (map, key)).isSome + ∧ (view.frame = {} + ∨ ∃ origin : Store, + view.frame = atCut origin origin.global + ∧ view.frame.version = origin.global + ∧ CellsBounded view.frame.data origin.global) := by + obtain ⟨eventNext, eventStep, _, _⟩ := step_event_result w next _ accepted + exact ⟨stepEvent_has_global w eventNext sid tid map key value t view source captured eventStep, + map_global_view_safety view + ((txOf_invariant w valid sid tid t source).globals map view captured)⟩ + intro w next sid tid seq map key value t view reachable source captured accepted + exact step_global_has_from_captured_map w next sid tid seq + (Invariants.reachable_invariant w reachable) map key value t view source captured + ((Proofs.Execution.step_iff_transition _ _ _).mp accepted) + +end Kv.Proofs.Trace + +namespace Kv.Proofs.Properties + +open Kv.Model Kv.Properties + +theorem transaction_snapshot_serial + : ∀ (w : World) (tid : Nat) (t : Tx) (snap : Snapshot), + Model.transitionSystem.Reachable w + → find w.txs tid = some t + → t.snapshot = some snap + → serialRun t.data [] t.normal.log = some t.normal.writes := by + intro w tid t snap reachable live captured + exact Proofs.Model.transaction_snapshot_serial t snap + ((Proofs.Invariants.reachable_invariant w reachable).txs tid t live).normal captured + +theorem transaction_application_serial + : ∀ (w : World) (sid tid : Nat) (s : Store) (t : Tx) (snap : Snapshot), + Model.transitionSystem.Reachable w + → storeOf w sid = .ok s + → txOf w sid tid = .ok t + → t.snapshot = some snap + → canApply s t = true + → serialRun s.head.data [] t.normal.log = some t.normal.writes := by + intro w sid tid s t snap reachable _store tx captured applies + exact Proofs.Model.transaction_application_serial s t snap + (Proofs.Invariants.txOf_invariant w + (Proofs.Invariants.reachable_invariant w reachable) sid tid t tx).normal + captured applies + +theorem executable_branch_serializability + : ∀ (s final : Store) (ts : List Tx), + (∀ t ∈ ts, + ∃ (w : World) (tid : Nat), + Model.transitionSystem.Reachable w ∧ find w.txs tid = some t) + → AppliedBranch s ts final + → serialTransactions s.head.data s.head.version ts = some final.head.data := by + intro s final ts reachable branch + apply Proofs.Model.executable_branch_serializability s final ts _ branch + intro t member + obtain ⟨w, tid, reached, live⟩ := reachable t member + exact ((Proofs.Invariants.reachable_invariant w reached).txs tid t live).normal + +theorem durable_cut_survives_rollback + : ∀ (w : World) (sid : Nat) (s : Store) (v term cut : Nat), + Model.transitionSystem.Reachable w + → find w.stores sid = some s + → cut ≤ s.global + → s.global ≤ v + → (atCut (rollbackStore s v term) cut).data = (atCut s cut).data := by + intro w sid s v term cut reachable live below boundary + exact Proofs.Model.durable_cut_survives_rollback s v term cut + ((Proofs.Invariants.reachable_invariant w reachable).stores sid s live) below boundary + +end Kv.Proofs.Properties diff --git a/lean/kv/Kv/Proofs/Replay.lean b/lean/kv/Kv/Proofs/Replay.lean new file mode 100644 index 00000000000..b898c8cff9f --- /dev/null +++ b/lean/kv/Kv/Proofs/Replay.lean @@ -0,0 +1,1093 @@ +-- Copyright (c) Microsoft Corporation. All rights reserved. +-- Licensed under the Apache 2.0 License. + +module + +public import Kv.Properties.Invariants + +/-! +Snapshot, map-capture and attempt-replay claims for accepted traces. + +This module is self-contained: shared lemmas are duplicated as private declarations in each +proof module so that the proof modules can be checked in parallel. +-/ + +@[expose] public section + +namespace Kv.Proofs.Execution +end Kv.Proofs.Execution + +namespace Kv.Proofs.Invariants +end Kv.Proofs.Invariants + +namespace Kv.Proofs.Model +end Kv.Proofs.Model + +namespace Kv.Proofs.Trace +end Kv.Proofs.Trace + +namespace Kv.Proofs.Properties +end Kv.Proofs.Properties + +namespace Kv.Proofs.Witnesses +end Kv.Proofs.Witnesses + +namespace Kv.Proofs.Execution + +open Kv.Model + +private theorem step_iff_transition (w next : World) (r : Record) + : transitionSystem.step w r = some next ↔ step w r = .ok next := by + simp only [transitionSystem] + cases step w r <;> simp [Except.toOption] + +private theorem replay_iff_run (w final : World) (rs : List Record) + : CCF.Execution.Run transitionSystem w rs final ↔ replay w rs = .ok final := by + induction rs generalizing w with + | nil => + constructor + · intro run + cases run using @CCF.Execution.Run.casesOn transitionSystem + rfl + · intro accepted + cases accepted + exact .nil _ + | cons r rs ih => + constructor + · intro run + cases run using @CCF.Execution.Run.casesOn transitionSystem with + | cons transition rest => + simp only [replay, (step_iff_transition _ _ _).mp transition, Except.bind] + exact (ih _).mp rest + · intro accepted + simp only [replay] at accepted + cases accepted' : step w r with + | error failure => simp [accepted', Except.bind] at accepted + | ok next => + simp only [accepted', Except.bind] at accepted + exact .cons ((step_iff_transition _ _ _).mpr accepted') ((ih _).mpr accepted) + +end Kv.Proofs.Execution + +namespace Kv.Proofs.Invariants + +open Kv.Model Kv.Properties + +/-- Executes operations in order with `normalStep` to reconstruct the normal view. -/ +private def normalRun {M K V : Type} [DecidableEq M] [DecidableEq K] [DecidableEq V] + (snapshot : DB M K V) (n : Normal M K V) (ops : List (NormalOp M K V)) + : Option (Normal M K V) := + ops.foldlM (normalStep snapshot) n + +/-- Store histories are contiguous, headed by the current frame, and contain the global cut. -/ +private structure StoreInvariant (s : Store) : Prop where + /-- Every frame follows by publishing writes to its predecessor. -/ + historyShape : History s.history s.head.version + /-- The head is the newest frame. -/ + headFirst : s.history.head? = some s.head + /-- The global version does not exceed the head. -/ + globalBound : s.global ≤ s.head.version + +/-- A global view is empty or was captured at a well-formed store's global cut. -/ +private def GlobalInvariant (view : GlobalView) : Prop := + view.frame = {} ∨ ∃ s : Store, StoreInvariant s ∧ view.frame = atCut s s.global + +/-- Replaying an attempt's log from its pinned data reproduces its normal view. -/ +private def NormalInvariant (t : Tx) : Prop := + match t.snapshot with + | none => t.normal = {} + | some _ => normalRun t.data {} t.normal.log = some t.normal + +/-- Consistency of an attempt's operation log and captured views. -/ +private structure TxInvariant (t : Tx) : Prop where + /-- The operation log reproduces the normal view. -/ + normal : NormalInvariant t + /-- Each snapshot was captured from a well-formed store's head. -/ + snapshot + : ∀ snap, + t.snapshot = some snap → ∃ s : Store, StoreInvariant s ∧ snap.current = s.head + /-- Each acquired global view has valid provenance. -/ + globals : ∀ map view, find t.globalViews map = some view → GlobalInvariant view + +/-- An attempt keeps its snapshot, pinned data and global views, and its invariant. -/ +private structure Frozen (t next : Tx) : Prop where + /-- The captured snapshot is unchanged. -/ + snapshot : next.snapshot = t.snapshot + /-- The pinned local data is unchanged. -/ + data : next.data = t.data + /-- The captured global views are unchanged. -/ + globals : next.globalViews = t.globalViews + /-- The attempt invariant is preserved. -/ + valid : TxInvariant t → TxInvariant next + +/-- How an accepted event changes the live stores and attempts. -/ +private inductive StepEffect (w : World) : Event → World → Prop + /-- Stores and attempts are unchanged. -/ + | same {e : Event} {next : World} (stores : next.stores = w.stores) + (txs : next.txs = w.txs) (noApply : ∀ sid, projectedApplication w sid e = []) + : StepEffect w e next + /-- A fresh store is created. -/ + | storeCreate {sid : Nat} {next : World} (stores : next.stores = set w.stores sid {}) + (txs : next.txs = w.txs) + : StepEffect w (.storeCreate sid) next + /-- A store is ended. -/ + | storeEnd {sid : Nat} {next : World} (stores : next.stores = erase w.stores sid) + (txs : next.txs = w.txs) + : StepEffect w (.storeEnd sid) next + /-- A fresh attempt is created. -/ + | txCreate {sid tid : Nat} {next : World} (stores : next.stores = w.stores) + (txs : next.txs = set w.txs tid { store := sid }) + : StepEffect w (.txCreate sid tid) next + /-- An attempt is ended. -/ + | txEnd {sid tid : Nat} {next : World} (stores : next.stores = w.stores) + (txs : next.txs = erase w.txs tid) + : StepEffect w (.txEnd sid tid) next + /-- A store is compacted. -/ + | compact {sid version requested : Nat} {next : World} {s : Store} + (store : storeOf w sid = .ok s) + (stores : next.stores = set w.stores sid (compactStore s requested)) + (txs : next.txs = w.txs) + : StepEffect w (.compact sid version requested) next + /-- A store is rolled back. -/ + | rollback {sid version requested term : Nat} {next : World} {s : Store} + (store : storeOf w sid = .ok s) + (stores : next.stores = set w.stores sid (rollbackStore s version term)) + (txs : next.txs = w.txs) + : StepEffect w (.rollback sid version requested term) next + /-- An attempt captures its snapshot; the store may learn its term. -/ + | snapshot {sid tid version global term : Nat} {next : World} {s established : Store} + {t : Tx} (store : storeOf w sid = .ok s) (history : established.history = s.history) + (head : established.head = s.head) (globalCut : established.global = s.global) + (tx : find w.txs tid = some t) (fresh : t.snapshot = none) + (stores : next.stores = set w.stores sid established) + (txs + : next.txs = set w.txs tid { t with snapshot := some { current := s.head, term } }) + : StepEffect w (.snapshot sid tid version global term) next + /-- An attempt acquires a map. -/ + | acquire {sid tid version global : Nat} {m : String} {next : World} {s : Store} + {t t' : Tx} (store : storeOf w sid = .ok s) (tx : txOf w sid tid = .ok t) + (accepted : acquireMap s t m version global = .ok t') + (stores : next.stores = w.stores) (txs : next.txs = set w.txs tid t') + : StepEffect w (.acquire sid tid m version global) next + /-- An attempt is applied to its store. -/ + | apply {sid tid version term : Nat} {writes : Pending} {next : World} {s new : Store} + {t : Tx} (store : storeOf w sid = .ok s) (tx : txOf w sid tid = .ok t) + (applied : tryApply s t = some new) (stores : next.stores = set w.stores sid new) + (txs : next.txs = set w.txs tid { t with phase := .applied version }) + : StepEffect w (.apply sid tid version term writes) next + /-- An attempt changes without moving its snapshot, pinned data or global views. -/ + | update {e : Event} {sid tid : Nat} {next : World} {t t' : Tx} + (tx : txOf w sid tid = .ok t) (frozen : Frozen t t') + (stores : next.stores = w.stores) (txs : next.txs = set w.txs tid t') + (noApply : ∀ sid, projectedApplication w sid e = []) + : StepEffect w e next + +end Kv.Proofs.Invariants + +namespace Kv.Proofs.Invariants + +open Kv.Model Kv.Properties +variable {M K V : Type} + +private theorem find_set_same [DecidableEq K] (xs : Assoc K V) (k : K) (v : V) + : find (set xs k v) k = some v := by + simp [Model.set, find] + +private theorem find_erase_other [DecidableEq K] (xs : Assoc K V) (a k : K) (h : a ≠ k) + : find (erase xs a) k = find xs k := by + induction xs with + | nil => rfl + | cons p xs ih => + rcases p with ⟨b, v⟩ + by_cases hba : b = a <;> by_cases hbk : b = k <;> simp_all [erase, find] + +private theorem find_set_other [DecidableEq K] (xs : Assoc K V) (a k : K) (v : V) + (h : a ≠ k) + : find (set xs a v) k = find xs k := by + simp [Model.set, find, h, find_erase_other xs a k h] + +private theorem normalRun_append [DecidableEq M] [DecidableEq K] [DecidableEq V] + (db : DB M K V) (n : Normal M K V) (a b : List (NormalOp M K V)) + : normalRun db n (a ++ b) + = (normalRun db n a).bind (fun next => normalRun db next b) := by + unfold normalRun + simp + +private theorem normalStep_log [DecidableEq M] [DecidableEq K] [DecidableEq V] + (db : DB M K V) (n n' : Normal M K V) (op : NormalOp M K V) + (h : normalStep db n op = some n') + : n'.log = n.log ++ [op] := by + unfold normalStep at h + split at h + next => cases h; rfl + next => simp at h + +private theorem normalRun_extend [DecidableEq M] [DecidableEq K] [DecidableEq V] + (db : DB M K V) (n n' : Normal M K V) (op : NormalOp M K V) + (before : normalRun db {} n.log = some n) + (one : normalStep db n op = some n') + : normalRun db {} n'.log = some n' := by + rw [normalStep_log db n n' op one, normalRun_append, before] + simp [normalRun, one] + +private theorem operation_normal (t : Tx) (valid : NormalInvariant t) (snap : Snapshot) + (n : Normal String String String) (op : NormalOp String String String) + (hs : t.snapshot = some snap) + (hn : normalStep t.data t.normal op = some n) + : match t.snapshot with + | none => n = {} + | some _ => normalRun t.data {} n.log = some n := by + have old : normalRun t.data {} t.normal.log = some t.normal := by + simpa [NormalInvariant, hs] using valid + simpa [hs] using normalRun_extend t.data t.normal n op old hn + +private theorem image_append (a b : Data) (m : String) + : image (a ++ b) m = image a m ++ image b m := by + simp [image] + +private theorem image_cons (name key : String) (cell : Cell String) (db : Data) + (m : String) + : image (((name, key), cell) :: db) m + = if name = m then (key, cell) :: image db m else image db m := by + unfold image + by_cases h : name = m + · simp only [List.filterMap_cons, h, ↓reduceIte] + · simp only [List.filterMap_cons, h, ↓reduceIte] + +private theorem image_filter (db : Data) (m : String) (p : String → Bool) + : image (db.filter fun (a, _) => p a.1) m = if p m then image db m else [] := by + induction db with + | nil => split <;> rfl + | cons entry db ih => + obtain ⟨⟨name, key⟩, cell⟩ := entry + rw [List.filter_cons, image_cons] + by_cases h : name = m + · subst h + cases hp : p name + · simpa only [hp, Bool.false_eq_true, ite_false] using ih + · simp only [hp, ite_true, image_cons] + rw [ih, hp] + rfl + · cases hp : p name + · simpa only [hp, Bool.false_eq_true, ite_false, h] using ih + · simp only [hp, ite_true, image_cons, h, ite_false] + exact ih + +private theorem pinData_other (db acquired : Data) (m other : String) (h : other ≠ m) + : image (pinData db m acquired) other = image db other := by + rw [pinData, image_append, image_filter db other (fun name => name != m), + image_filter acquired other (fun name => name == m)] + simp [h] + +private theorem bind_ok {α β : Type} {x : Except Failure α} {f : α → Except Failure β} + {b : β} (h : (x >>= f) = .ok b) + : ∃ a, x = .ok a ∧ f a = .ok b := by + cases x with + | error => cases h + | ok a => exact ⟨a, rfl, h⟩ + +private theorem pure_ok {α : Type} {a b : α} (h : (pure a : Except Failure α) = .ok b) + : a = b := by + cases h; rfl + +private theorem withTx_ok {w next : World} {sid tid : Nat} {f : Tx → Except Failure Tx} + (h : withTx w sid tid f = .ok next) + : ∃ t t', + txOf w sid tid = .ok t + ∧ f t = .ok t' + ∧ next = { w with txs := set w.txs tid t' } := by + obtain ⟨t, tx, h⟩ := bind_ok h + obtain ⟨t', f, h⟩ := bind_ok h + exact ⟨t, t', tx, f, (pure_ok h).symm⟩ + +private theorem present_ok {α : Type} {value : Option α} {message : String} {a : α} + (h : present value message = .ok a) + : value = some a := by + cases value with + | none => cases h + | some => cases h; rfl + +private theorem require_ok {condition : Bool} {message : String} {u : Unit} + (h : require condition message = .ok u) + : condition = true := by + cases condition + · cases h + · rfl + +private theorem expect_ok {condition : Bool} {message : String} {u : Unit} + (h : expect condition message = .ok u) + : condition = true := by + cases condition + · cases h + · rfl + +private theorem acquireMap_ok {s : Store} {t next : Tx} {map : String} + {version global : Nat} (accepted : acquireMap s t map version global = .ok next) + : ∃ snap, + t.snapshot = some snap + ∧ find t.globalViews map = none + ∧ (version = (revision (captureGlobal s snap map).current map).version + ∧ global = (revision (captureGlobal s snap map).frame map).version) + ∧ t.normal.log.all (fun op => op.map != map) = true + ∧ next + = { + t with + globalViews := set t.globalViews map (captureGlobal s snap map) + data := pinData t.data map (captureGlobal s snap map).current.data + } := by + obtain ⟨_, -, accepted⟩ := bind_ok accepted + obtain ⟨_, -, accepted⟩ := bind_ok accepted + obtain ⟨snap, captured, accepted⟩ := bind_ok accepted + obtain ⟨_, fresh, accepted⟩ := bind_ok accepted + obtain ⟨_, versions, accepted⟩ := bind_ok accepted + obtain ⟨_, -, accepted⟩ := bind_ok accepted + split at accepted + next unused => + cases pure_ok accepted + have versions := expect_ok versions + simp only [Bool.and_eq_true, beq_iff_eq] at versions + exact ⟨snap, present_ok captured, Option.isNone_iff_eq_none.mp (require_ok fresh), versions, + unused, rfl⟩ + next => cases accepted + +private theorem tx_fields_invariant (t next : Tx) (valid : TxInvariant t) + (snapshot : next.snapshot = t.snapshot) (data : next.data = t.data) + (normal : next.normal = t.normal) (globals : next.globalViews = t.globalViews) + : TxInvariant next := by + rcases valid with ⟨hn, hs, hg⟩ + constructor + · simpa [NormalInvariant, snapshot, data, normal] using hn + · simpa [snapshot] using hs + · simpa [globals] using hg + +private theorem txOf_found (w : World) (sid tid : Nat) (t : Tx) + (found : txOf w sid tid = .ok t) + : find w.txs tid = some t := by + obtain ⟨_, -, found⟩ := bind_ok found + obtain ⟨_, lookup, found⟩ := bind_ok found + obtain ⟨_, -, found⟩ := bind_ok found + cases pure_ok found + exact present_ok lookup + +private theorem Frozen.refl (t : Tx) : Frozen t t := ⟨rfl, rfl, rfl, id⟩ + +private theorem Frozen.trans {a b c : Tx} (ab : Frozen a b) (bc : Frozen b c) + : Frozen a c := + ⟨ + bc.snapshot.trans ab.snapshot, + bc.data.trans ab.data, + bc.globals.trans ab.globals, + bc.valid ∘ ab.valid + ⟩ + +private theorem Frozen.fields {t next : Tx} (snapshot : next.snapshot = t.snapshot) + (data : next.data = t.data) (normal : next.normal = t.normal) + (globals : next.globalViews = t.globalViews) + : Frozen t next := + ⟨ + snapshot, + data, + globals, + fun valid => tx_fields_invariant t next valid snapshot data normal globals + ⟩ + +private theorem runOp_frozen {t next : Tx} {op : NormalOp String String String} + (accepted : runOp t op = .ok next) + : Frozen t next := by + simp only [runOp, Pure.pure, Except.pure] at accepted + split at accepted + next => contradiction + next snap hs => + split at accepted + next n hn => + cases accepted + exact ⟨rfl, rfl, rfl, fun valid => + ⟨operation_normal t valid.normal snap n op hs hn, valid.snapshot, valid.globals⟩⟩ + next => contradiction + +private theorem clearWrites_frozen {t next : Tx} {map : String} + {entries : Assoc String String} (accepted : clearWrites t map entries = .ok next) + : Frozen t next := by + unfold clearWrites at accepted + induction entries generalizing t with + | nil => cases accepted; exact Frozen.refl _ + | cons entry entries ih => + obtain ⟨middle, one, rest⟩ := bind_ok accepted + exact (runOp_frozen one).trans (ih rest) + +private theorem StepEffect.withTx {w next : World} {e : Event} {sid tid : Nat} + {f : Tx → Except Failure Tx} (noApply : ∀ sid, projectedApplication w sid e = []) + (frozen : ∀ t t', f t = .ok t' → Frozen t t') + (accepted : withTx w sid tid f = .ok next) + : StepEffect w e next := by + obtain ⟨t, t', tx, h, rfl⟩ := withTx_ok accepted + exact .update tx (frozen t t' h) rfl rfl noApply + +private theorem stepEvent_effect_rollbackRejected (w next : World) + (store requested term : Nat) + (accepted : stepEvent w (.rollbackRejected store requested term) = .ok next) + : StepEffect w (.rollbackRejected store requested term) next := by + repeat obtain ⟨_, -, accepted⟩ := bind_ok accepted + cases pure_ok accepted + exact .same rfl rfl fun _ => rfl + +private theorem stepEvent_effect_storeCreate (w next : World) (store : Nat) + (accepted : stepEvent w (.storeCreate store) = .ok next) + : StepEffect w (.storeCreate store) next := by + repeat obtain ⟨_, -, accepted⟩ := bind_ok accepted + cases pure_ok accepted + exact .storeCreate rfl rfl + +private theorem stepEvent_effect_storeEnd (w next : World) (store : Nat) + (accepted : stepEvent w (.storeEnd store) = .ok next) + : StepEffect w (.storeEnd store) next := by + repeat obtain ⟨_, -, accepted⟩ := bind_ok accepted + cases pure_ok accepted + exact .storeEnd rfl rfl + +private theorem stepEvent_effect_txCreate (w next : World) (store tx : Nat) + (accepted : stepEvent w (.txCreate store tx) = .ok next) + : StepEffect w (.txCreate store tx) next := by + repeat obtain ⟨_, -, accepted⟩ := bind_ok accepted + cases pure_ok accepted + exact .txCreate rfl rfl + +private theorem stepEvent_effect_txEnd (w next : World) (store tx : Nat) + (accepted : stepEvent w (.txEnd store tx) = .ok next) + : StepEffect w (.txEnd store tx) next := by + repeat obtain ⟨_, -, accepted⟩ := bind_ok accepted + cases pure_ok accepted + exact .txEnd rfl rfl + +private theorem stepEvent_effect_snapshot (w next : World) + (sid tid version global term : Nat) + (accepted : stepEvent w (.snapshot sid tid version global term) = .ok next) + : StepEffect w (.snapshot sid tid version global term) next := by + obtain ⟨s, store, accepted⟩ := bind_ok accepted + obtain ⟨t, t', tx, h, rfl⟩ := withTx_ok accepted + obtain ⟨_, -, h⟩ := bind_ok h + split at h + next fresh => + obtain ⟨_, -, h⟩ := bind_ok h + cases pure_ok h + have live := txOf_found _ sid tid t tx + exact .snapshot store (by split <;> rfl) (by split <;> rfl) (by split <;> rfl) + live fresh rfl rfl + next => cases h + +private theorem stepEvent_effect_apply (w next : World) (store tx version term : Nat) + (writes : Pending) + (accepted : stepEvent w (.apply store tx version term writes) = .ok next) + : StepEffect w (.apply store tx version term writes) next := by + obtain ⟨s, store, accepted⟩ := bind_ok accepted + obtain ⟨t, tx, accepted⟩ := bind_ok accepted + obtain ⟨_, -, accepted⟩ := bind_ok accepted + obtain ⟨_, -, accepted⟩ := bind_ok accepted + obtain ⟨_, -, accepted⟩ := bind_ok accepted + obtain ⟨_, -, accepted⟩ := bind_ok accepted + split at accepted + next new applied => + obtain ⟨_, same, accepted⟩ := bind_ok accepted + cases pure_ok same + obtain ⟨_, -, accepted⟩ := bind_ok accepted + cases pure_ok accepted + exact .apply store tx applied rfl rfl + next => + obtain ⟨_, rejected, -⟩ := bind_ok accepted + cases rejected + +private theorem stepEvent_effect_get (w next : World) (store tx : Nat) (map key : String) + (value : Option String) (global : Bool) + (accepted : stepEvent w (.get store tx map key value global) = .ok next) + : StepEffect w (.get store tx map key value global) next := by + refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted + obtain ⟨_, -, h⟩ := bind_ok h + split at h + · repeat obtain ⟨_, -, h⟩ := bind_ok h + cases pure_ok h + exact .refl _ + · exact runOp_frozen h + +private theorem stepEvent_effect_has (w next : World) (store tx : Nat) (map key : String) + (value : Bool) (global : Bool) + (accepted : stepEvent w (.has store tx map key value global) = .ok next) + : StepEffect w (.has store tx map key value global) next := by + refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted + obtain ⟨_, -, h⟩ := bind_ok h + split at h + · repeat obtain ⟨_, -, h⟩ := bind_ok h + cases pure_ok h + exact .refl _ + · repeat obtain ⟨_, -, h⟩ := bind_ok h + exact runOp_frozen h + +private theorem stepEvent_effect_previous (w next : World) (store tx : Nat) + (map key : String) (value : Option Nat) + (accepted : stepEvent w (.previous store tx map key value) = .ok next) + : StepEffect w (.previous store tx map key value) next := by + refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted + repeat obtain ⟨_, -, h⟩ := bind_ok h + exact runOp_frozen h + +private theorem stepEvent_effect_put (w next : World) (store tx : Nat) + (map key value : String) + (accepted : stepEvent w (.put store tx map key value) = .ok next) + : StepEffect w (.put store tx map key value) next := by + refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted + repeat obtain ⟨_, -, h⟩ := bind_ok h + exact runOp_frozen h + +private theorem stepEvent_effect_remove (w next : World) (store tx : Nat) + (map key : String) (accepted : stepEvent w (.remove store tx map key) = .ok next) + : StepEffect w (.remove store tx map key) next := by + refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted + repeat obtain ⟨_, -, h⟩ := bind_ok h + exact runOp_frozen h + +private theorem stepEvent_effect_size (w next : World) (store tx : Nat) (map : String) + (value : Nat) (accepted : stepEvent w (.size store tx map value) = .ok next) + : StepEffect w (.size store tx map value) next := by + refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted + repeat obtain ⟨_, -, h⟩ := bind_ok h + exact runOp_frozen h + +private theorem stepEvent_effect_range (w next : World) (store tx : Nat) (map : String) + (lower upper : Option String) (entries : Assoc String String) + (accepted : stepEvent w (.range store tx map lower upper entries) = .ok next) + : StepEffect w (.range store tx map lower upper entries) next := by + refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted + obtain ⟨_, -, h⟩ := bind_ok h + split at h + · obtain ⟨_, -, h⟩ := bind_ok h + cases pure_ok h + exact .refl _ + · obtain ⟨_, -, h⟩ := bind_ok h + exact runOp_frozen h + +private theorem stepEvent_effect_clear (w next : World) (store tx : Nat) (map : String) + (accepted : stepEvent w (.clear store tx map) = .ok next) + : StepEffect w (.clear store tx map) next := by + refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted + obtain ⟨_, -, h⟩ := bind_ok h + obtain ⟨_, one, h⟩ := bind_ok h + exact (runOp_frozen one).trans (clearWrites_frozen h) + +private theorem stepEvent_effect_foreachBegin (w next : World) (store tx : Nat) + (map : String) (iteration : Nat) + (accepted : stepEvent w (.foreachBegin store tx map iteration) = .ok next) + : StepEffect w (.foreachBegin store tx map iteration) next := by + refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted + obtain ⟨_, -, h⟩ := bind_ok h + obtain ⟨_, -, h⟩ := bind_ok h + obtain ⟨_, one, h⟩ := bind_ok h + cases pure_ok h + exact (runOp_frozen one).trans (.fields rfl rfl rfl rfl) + +private theorem stepEvent_effect_unavailable (w next : World) (store tx : Nat) + (map : String) (accepted : stepEvent w (.unavailable store tx map) = .ok next) + : StepEffect w (.unavailable store tx map) next := by + obtain ⟨_, -, accepted⟩ := bind_ok accepted + refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted + repeat obtain ⟨_, -, h⟩ := bind_ok h + cases pure_ok h + exact .fields rfl rfl rfl rfl + +private theorem stepEvent_effect_commitResult (w next : World) (store tx : Nat) + (result : Outcome) (version : Nat) + (accepted : stepEvent w (.commitResult store tx result version) = .ok next) + : StepEffect w (.commitResult store tx result version) next := by + refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted + split at h + next => + obtain ⟨_, -, h⟩ := bind_ok h + cases pure_ok h + exact .fields rfl rfl rfl rfl + next => + obtain ⟨_, -, h⟩ := bind_ok h + split at h + · obtain ⟨_, -, h⟩ := bind_ok h + cases pure_ok h + exact .fields rfl rfl rfl rfl + · cases pure_ok h + exact .fields rfl rfl rfl rfl + next => + obtain ⟨_, -, h⟩ := bind_ok h + cases pure_ok h + exact .fields rfl rfl rfl rfl + +private theorem stepEvent_effect (w next : World) (e : Event) + (accepted : stepEvent w e = .ok next) + : StepEffect w e next := by + cases e with + | traceStart | caseBegin | caseEnd | subcaseBegin | subcaseEnd | traceEnd => + repeat obtain ⟨_, -, accepted⟩ := bind_ok accepted + cases pure_ok accepted + exact .same rfl rfl fun _ => rfl + | rollbackRejected => exact stepEvent_effect_rollbackRejected w next _ _ _ accepted + | unsupported => cases accepted + | storeCreate => exact stepEvent_effect_storeCreate w next _ accepted + | storeEnd => exact stepEvent_effect_storeEnd w next _ accepted + | txCreate => exact stepEvent_effect_txCreate w next _ _ accepted + | txEnd => exact stepEvent_effect_txEnd w next _ _ accepted + | compact => + obtain ⟨s, store, accepted⟩ := bind_ok accepted + repeat obtain ⟨_, -, accepted⟩ := bind_ok accepted + cases pure_ok accepted + exact .compact store rfl rfl + | rollback => + obtain ⟨s, store, accepted⟩ := bind_ok accepted + repeat obtain ⟨_, -, accepted⟩ := bind_ok accepted + cases pure_ok accepted + exact .rollback store rfl rfl + | snapshot => exact stepEvent_effect_snapshot w next _ _ _ _ _ accepted + | acquire => + obtain ⟨s, store, accepted⟩ := bind_ok accepted + obtain ⟨t, t', tx, h, rfl⟩ := withTx_ok accepted + exact .acquire store tx h rfl rfl + | apply => exact stepEvent_effect_apply w next _ _ _ _ _ accepted + | get => exact stepEvent_effect_get w next _ _ _ _ _ _ accepted + | has => exact stepEvent_effect_has w next _ _ _ _ _ _ accepted + | previous => exact stepEvent_effect_previous w next _ _ _ _ _ accepted + | put => exact stepEvent_effect_put w next _ _ _ _ _ accepted + | remove => exact stepEvent_effect_remove w next _ _ _ _ accepted + | size => exact stepEvent_effect_size w next _ _ _ _ accepted + | range => exact stepEvent_effect_range w next _ _ _ _ _ _ accepted + | clear => exact stepEvent_effect_clear w next _ _ _ accepted + | foreachBegin => exact stepEvent_effect_foreachBegin w next _ _ _ _ accepted + | foreachEntry | foreachContinue | foreachEnd => + refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted + obtain ⟨⟨_, _⟩, -, h⟩ := bind_ok h + repeat obtain ⟨_, -, h⟩ := bind_ok h + cases pure_ok h + exact .fields rfl rfl rfl rfl + | unavailable => exact stepEvent_effect_unavailable w next _ _ _ accepted + | commitBegin => + refine StepEffect.withTx (fun _ => rfl) (fun t t' h => ?_) accepted + repeat obtain ⟨_, -, h⟩ := bind_ok h + cases pure_ok h + exact .fields rfl rfl rfl rfl + | commitResult => exact stepEvent_effect_commitResult w next _ _ _ _ accepted + +private theorem step_ok {w next : World} {r : Record} (accepted : step w r = .ok next) + : ∃ eventNext, + stepEvent w r.event = .ok eventNext + ∧ next = { eventNext with lastSeq := some r.seq, count := w.count + 1 } := by + obtain ⟨_, -, accepted⟩ := bind_ok accepted + obtain ⟨_, -, accepted⟩ := bind_ok accepted + obtain ⟨seq, event⟩ := r + dsimp only at accepted ⊢ + split at accepted <;> try split at accepted + all_goals first + | obtain ⟨_, invalid, -⟩ := bind_ok accepted; cases invalid + | obtain ⟨eventNext, event, accepted⟩ := bind_ok accepted + exact ⟨eventNext, event, (pure_ok accepted).symm⟩ + +end Kv.Proofs.Invariants + +namespace Kv.Proofs.Trace + +open Kv.Model Kv.Proofs.Invariants Kv.Properties Kv.Proofs.Model + +private theorem step_event_result (w next : World) (r : Record) + (accepted : step w r = .ok next) + : ∃ eventNext, + stepEvent w r.event = .ok eventNext + ∧ next.stores = eventNext.stores + ∧ next.txs = eventNext.txs := by + obtain ⟨eventNext, event, rfl⟩ := step_ok accepted + exact ⟨eventNext, event, rfl, rfl⟩ + +private theorem absent_ne {xs : Assoc String GlobalView} {map wanted : String} + {view : GlobalView} (absent : find xs map = none) (found : find xs wanted = some view) + : map ≠ wanted := + fun same => by + rw [same, found] at absent + cases absent + +/-- The attempt keeps its captured snapshot, global views and pinned map data. -/ +private def Kept (before after : Tx) : Prop := + (∀ snap, before.snapshot = some snap → after.snapshot = some snap) + ∧ ∀ map view, + find before.globalViews map = some view + → find after.globalViews map = some view + ∧ image after.data map = image before.data map + +private theorem Kept.refl (t : Tx) : Kept t t := ⟨fun _ h => h, fun _ _ h => ⟨h, rfl⟩⟩ + +private theorem Kept.frozen {t next : Tx} (frozen : Frozen t next) : Kept t next := + ⟨ + fun _ h => frozen.snapshot.trans h, + fun _ _ h => by + rw [frozen.globals, frozen.data] + exact ⟨h, rfl⟩ + ⟩ + +private theorem stepEvent_attempt_kept (w next : World) (tid : Nat) (before : Tx) + (e : Event) (live : find w.txs tid = some before) (segment : AttemptEvent tid e) + (accepted : stepEvent w e = .ok next) + : ∃ after, find next.txs tid = some after ∧ Kept before after := by + have set_kept {xs : Assoc Nat Tx} {tid id : Nat} {before next : Tx} + (live : find xs tid = some before) (kept : id = tid → Kept before next) + : ∃ after, find (set xs id next) tid = some after ∧ Kept before after := by + by_cases h : id = tid + · subst h + exact ⟨next, find_set_same _ _ _, kept rfl⟩ + · exact ⟨before, by rw [find_set_other _ _ _ _ h]; exact live, Kept.refl before⟩ + cases stepEvent_effect w next e accepted with + | same _ txs | storeCreate _ txs | storeEnd _ txs | compact _ _ txs | rollback _ _ txs + => + exact ⟨before, by rw [txs]; exact live, Kept.refl before⟩ + | txCreate _ txs => + exact ⟨ + before, + by rw [txs, find_set_other _ _ _ _ segment]; exact live, + Kept.refl before + ⟩ + | txEnd _ txs => + exact ⟨ + before, + by rw [txs, find_erase_other _ _ _ segment]; exact live, + Kept.refl before + ⟩ + | snapshot _ _ _ _ tx fresh _ txs => + rw [txs] + refine set_kept live fun same => ?_ + subst same + cases tx.symm.trans live + exact ⟨fun _ h => (by rw [fresh] at h; cases h), fun _ _ h => ⟨h, rfl⟩⟩ + | acquire _ tx acquired _ txs => + rw [txs] + refine set_kept live fun same => ?_ + subst same + cases (txOf_found _ _ _ _ tx).symm.trans live + obtain ⟨snap, _, fresh, _, _, rfl⟩ := acquireMap_ok acquired + refine ⟨fun _ h => h, fun map view h => ?_⟩ + have other := absent_ne fresh h + exact ⟨ + by rw [find_set_other _ _ _ _ other]; exact h, + Invariants.pinData_other _ _ _ _ (Ne.symm other) + ⟩ + | apply _ tx _ _ txs => + rw [txs] + refine set_kept live fun same => ?_ + subst same + cases (txOf_found _ _ _ _ tx).symm.trans live + exact Kept.refl _ + | update tx frozen _ txs => + rw [txs] + refine set_kept live fun same => ?_ + subst same + cases (txOf_found _ _ _ _ tx).symm.trans live + exact Kept.frozen frozen + +private theorem replay_attempt_invariant (tid : Nat) (P : Tx → Prop) + (preserve + : ∀ (w next : World) (before after : Tx) (r : Record), + find w.txs tid = some before + → find next.txs tid = some after + → P before + → AttemptEvent tid r.event + → step w r = .ok next + → P after) + (w final : World) (before : Tx) + (rs : List Record) (live : find w.txs tid = some before) + (holds : P before) + (segment : ∀ r ∈ rs, AttemptEvent tid r.event) + (accepted : replay w rs = .ok final) + : ∃ after, find final.txs tid = some after ∧ P after := by + have stepEvent_attempt_live (w next : World) (tid : Nat) (before : Tx) (e : Event) + (live : find w.txs tid = some before) (segment : AttemptEvent tid e) + (accepted : stepEvent w e = .ok next) + : ∃ after, find next.txs tid = some after := by + obtain ⟨after, found, -⟩ := stepEvent_attempt_kept w next tid before e live segment accepted + exact ⟨after, found⟩ + induction rs generalizing w before with + | nil => cases accepted; exact ⟨before, live, holds⟩ + | cons r rs ih => + cases one : step w r with + | error err => simp [replay, one, Except.bind] at accepted + | ok middle => + obtain ⟨eventNext, eventStep, _, txs⟩ := step_event_result w middle r one + have thisSegment := segment r (by simp) + obtain ⟨midTx, midLive⟩ := stepEvent_attempt_live w eventNext tid before r.event + live thisSegment eventStep + have midLive' : find middle.txs tid = some midTx := by simpa [txs] using midLive + have midProperty := + preserve w middle before midTx r live midLive' holds thisSegment one + apply ih middle midTx midLive' midProperty + · intro e he; exact segment e (by simp [he]) + · simpa [replay, one, Except.bind] using accepted + +private theorem replay_snapshot_fixed (w final : World) (tid : Nat) (before : Tx) + (snap : Snapshot) (rs : List Record) (live : find w.txs tid = some before) + (captured : before.snapshot = some snap) + (segment : ∀ r ∈ rs, AttemptEvent tid r.event) (accepted : replay w rs = .ok final) + : ∃ after, find final.txs tid = some after ∧ after.snapshot = some snap := by + have stepEvent_snapshot_fixed (w next : World) (tid : Nat) (before after : Tx) + (snap : Snapshot) (e : Event) + (live : find w.txs tid = some before) (stillLive : find next.txs tid = some after) + (captured : before.snapshot = some snap) (segment : AttemptEvent tid e) + (accepted : stepEvent w e = .ok next) + : after.snapshot = some snap := by + obtain ⟨found, live', kept⟩ := + stepEvent_attempt_kept w next tid before e live segment accepted + cases stillLive.symm.trans live' + exact kept.1 snap captured + have step_snapshot_fixed (w next : World) (tid : Nat) (before after : Tx) + (snap : Snapshot) (r : Record) + (live : find w.txs tid = some before) (stillLive : find next.txs tid = some after) + (captured : before.snapshot = some snap) (segment : AttemptEvent tid r.event) + (accepted : step w r = .ok next) + : after.snapshot = some snap := by + obtain ⟨eventNext, eventStep, _, txs⟩ := step_event_result w next r accepted + apply stepEvent_snapshot_fixed w eventNext tid before after snap r.event live + (by simpa [txs] using stillLive) captured segment eventStep + exact replay_attempt_invariant tid (fun t => t.snapshot = some snap) + (fun w next before after r => step_snapshot_fixed w next tid before after snap r) + w final before rs live captured segment accepted + +private theorem stepEvent_capture_metadata (w next : World) + (sid tid version global term : Nat) (s : Store) (t : Tx) + (source : storeOf w sid = .ok s) + (accepted : stepEvent w (.snapshot sid tid version global term) = .ok next) + (capturedTx : find next.txs tid = some t) + : ∃ snap, t.snapshot = some snap ∧ snap.current = s.head ∧ snap.term = term := by + refine ⟨{ current := s.head, term }, ?_, rfl, rfl⟩ + obtain ⟨_, store, accepted⟩ := bind_ok accepted + cases source.symm.trans store + obtain ⟨_, _, -, h, rfl⟩ := withTx_ok accepted + obtain ⟨_, -, h⟩ := bind_ok h + split at h + · obtain ⟨_, -, h⟩ := bind_ok h + cases pure_ok h + simp only [find_set_same, Option.some.injEq] at capturedTx + subst capturedTx + rfl + · cases h + +private theorem step_capture_metadata (w next : World) + (sid tid version global term seq : Nat) (s : Store) (t : Tx) + (source : storeOf w sid = .ok s) + (accepted : step w ⟨seq, .snapshot sid tid version global term⟩ = .ok next) + (capturedTx : find next.txs tid = some t) + : ∃ snap, t.snapshot = some snap ∧ snap.current = s.head ∧ snap.term = term := by + obtain ⟨eventNext, eventStep, _, txs⟩ := step_event_result w next _ accepted + exact stepEvent_capture_metadata w eventNext sid tid version global term s t source + eventStep (by simpa [txs] using capturedTx) + +private theorem stepEvent_map_capture (w next : World) + (sid tid localVersion globalVersion : Nat) (map : String) (s : Store) + (before after : Tx) (snap : Snapshot) (store : storeOf w sid = .ok s) + (tx : txOf w sid tid = .ok before) (snapshot : before.snapshot = some snap) + (accepted : stepEvent w (.acquire sid tid map localVersion globalVersion) = .ok next) + (live : find next.txs tid = some after) + : find after.globalViews map = some (captureGlobal s snap map) + ∧ localVersion = (revision (captureLocal s snap map) map).version + ∧ globalVersion = (revision (captureGlobal s snap map).frame map).version := by + have captureGlobal_current (s : Store) (snap : Snapshot) (map : String) + : (captureGlobal s snap map).current = captureLocal s snap map := by + dsimp only [captureGlobal] + split <;> rfl + obtain ⟨_, store', accepted⟩ := bind_ok accepted + cases store.symm.trans store' + obtain ⟨_, _, tx', h, rfl⟩ := withTx_ok accepted + cases tx.symm.trans tx' + obtain ⟨_, captured, -, versions, _, rfl⟩ := acquireMap_ok h + cases snapshot.symm.trans captured + simp only [find_set_same, Option.some.injEq] at live + subst live + rw [captureGlobal_current] at versions + exact ⟨find_set_same _ _ _, versions⟩ + +private theorem step_map_capture (w next : World) + (sid tid localVersion globalVersion seq : Nat) (map : String) (s : Store) + (before after : Tx) (snap : Snapshot) (store : storeOf w sid = .ok s) + (tx : txOf w sid tid = .ok before) (snapshot : before.snapshot = some snap) + (accepted : step w ⟨seq, .acquire sid tid map localVersion globalVersion⟩ = .ok next) + (live : find next.txs tid = some after) + : find after.globalViews map = some (captureGlobal s snap map) + ∧ localVersion = (revision (captureLocal s snap map) map).version + ∧ globalVersion = (revision (captureGlobal s snap map).frame map).version := by + obtain ⟨eventNext, eventStep, _, txs⟩ := step_event_result w next _ accepted + exact stepEvent_map_capture w eventNext sid tid localVersion globalVersion map s before + after snap store tx snapshot eventStep (by simpa [txs] using live) + +private theorem step_map_global_fixed (w next : World) (tid : Nat) (before after : Tx) + (map : String) (view : GlobalView) (r : Record) (live : find w.txs tid = some before) + (stillLive : find next.txs tid = some after) + (captured : find before.globalViews map = some view) + (segment : AttemptEvent tid r.event) (accepted : step w r = .ok next) + : find after.globalViews map = some view := by + have stepEvent_map_global_fixed (w next : World) (tid : Nat) (before after : Tx) + (map : String) (view : GlobalView) (e : Event) + (live : find w.txs tid = some before) (stillLive : find next.txs tid = some after) + (captured : find before.globalViews map = some view) (segment : AttemptEvent tid e) + (accepted : stepEvent w e = .ok next) + : find after.globalViews map = some view := by + obtain ⟨found, live', kept⟩ := + stepEvent_attempt_kept w next tid before e live segment accepted + cases stillLive.symm.trans live' + exact (kept.2 map view captured).1 + obtain ⟨eventNext, eventStep, _, txs⟩ := step_event_result w next r accepted + exact stepEvent_map_global_fixed w eventNext tid before after map view r.event live + (by simpa [txs] using stillLive) captured segment eventStep + +private theorem replay_map_global_fixed (w final : World) (tid : Nat) (before : Tx) + (map : String) (view : GlobalView) (rs : List Record) + (live : find w.txs tid = some before) + (captured : find before.globalViews map = some view) + (segment : ∀ r ∈ rs, AttemptEvent tid r.event) (accepted : replay w rs = .ok final) + : ∃ after, find final.txs tid = some after ∧ find after.globalViews map = some view := + replay_attempt_invariant tid (fun t => find t.globalViews map = some view) + (fun w next before after r => + step_map_global_fixed w next tid before after map view r) + w final before rs live captured segment accepted + +theorem capture_replay_preserves_metadata_claim + : ∀ (w capturedWorld final : World) (sid tid version global term seq : Nat) + (s : Store) (t : Tx) (tail : List Record), + storeOf w sid = .ok s + → Model.transitionSystem.step w ⟨seq, .snapshot sid tid version global term⟩ + = some capturedWorld + → find capturedWorld.txs tid = some t + → (∀ r ∈ tail, AttemptEvent tid r.event) + → CCF.Execution.Run Model.transitionSystem capturedWorld tail final + → ∃ after snap, + find final.txs tid = some after + ∧ after.snapshot = some snap + ∧ snap.current = s.head + ∧ snap.term = term := by + have capture_replay_preserves_metadata (w capturedWorld final : World) + (sid tid version global term seq : Nat) (s : Store) (t : Tx) (tail : List Record) + (source : storeOf w sid = .ok s) + (capture : step w ⟨seq, .snapshot sid tid version global term⟩ = .ok capturedWorld) + (live : find capturedWorld.txs tid = some t) + (segment : ∀ r ∈ tail, AttemptEvent tid r.event) + (accepted : replay capturedWorld tail = .ok final) + : ∃ after snap, + find final.txs tid = some after + ∧ after.snapshot = some snap + ∧ snap.current = s.head + ∧ snap.term = term := by + obtain ⟨snap, captured, current, snapshotTerm⟩ := + step_capture_metadata w capturedWorld sid tid version global term seq s t source capture live + obtain ⟨after, afterLive, same⟩ := replay_snapshot_fixed capturedWorld final tid t snap + tail live captured segment accepted + exact ⟨after, snap, afterLive, same, current, snapshotTerm⟩ + intro w capturedWorld final sid tid version global term seq s t tail source capture live segment accepted + exact capture_replay_preserves_metadata w capturedWorld final sid tid version global + term seq s t tail source ((Proofs.Execution.step_iff_transition _ _ _).mp capture) + live segment ((Proofs.Execution.replay_iff_run _ _ _).mp accepted) + +theorem replay_snapshot_fixed_claim + : ∀ (w final : World) (tid : Nat) (before : Tx) (snap : Snapshot) (rs : List Record), + find w.txs tid = some before + → before.snapshot = some snap + → (∀ r ∈ rs, AttemptEvent tid r.event) + → CCF.Execution.Run Model.transitionSystem w rs final + → ∃ after, find final.txs tid = some after ∧ after.snapshot = some snap := by + intro w final tid before snap rs live captured segment accepted + exact Proofs.Trace.replay_snapshot_fixed w final tid before snap rs live captured segment ((Proofs.Execution.replay_iff_run _ _ _).mp accepted) + +theorem replay_map_global_fixed_claim + : ∀ (w final : World) (tid : Nat) (before : Tx) (map : String) (view : GlobalView) + (rs : List Record), + find w.txs tid = some before + → find before.globalViews map = some view + → (∀ r ∈ rs, AttemptEvent tid r.event) + → CCF.Execution.Run Model.transitionSystem w rs final + → ∃ after, + find final.txs tid = some after ∧ find after.globalViews map = some view := by + intro w final tid before map view rs live captured segment accepted + exact Proofs.Trace.replay_map_global_fixed w final tid before map view rs live captured segment ((Proofs.Execution.replay_iff_run _ _ _).mp accepted) + +theorem capture_replay_preserves_map_claim + : ∀ (w capturedWorld final : World) (sid tid localVersion globalVersion seq : Nat) + (map : String) (s : Store) (before capturedTx : Tx) (snap : Snapshot) + (tail : List Record), + storeOf w sid = .ok s + → txOf w sid tid = .ok before + → before.snapshot = some snap + → Model.transitionSystem.step w + ⟨seq, .acquire sid tid map localVersion globalVersion⟩ + = some capturedWorld + → find capturedWorld.txs tid = some capturedTx + → (∀ r ∈ tail, AttemptEvent tid r.event) + → CCF.Execution.Run Model.transitionSystem capturedWorld tail final + → ∃ after, + find final.txs tid = some after + ∧ find after.globalViews map = some (captureGlobal s snap map) + ∧ localVersion = (revision (captureLocal s snap map) map).version + ∧ globalVersion + = (revision (captureGlobal s snap map).frame map).version := by + have capture_replay_preserves_map (w capturedWorld final : World) + (sid tid localVersion globalVersion seq : Nat) (map : String) + (s : Store) (before capturedTx : Tx) (snap : Snapshot) (tail : List Record) + (store : storeOf w sid = .ok s) (tx : txOf w sid tid = .ok before) + (snapshot : before.snapshot = some snap) + (capture + : step w ⟨seq, .acquire sid tid map localVersion globalVersion⟩ = .ok capturedWorld) + (live : find capturedWorld.txs tid = some capturedTx) + (segment : ∀ r ∈ tail, AttemptEvent tid r.event) + (accepted : replay capturedWorld tail = .ok final) + : ∃ after, + find final.txs tid = some after + ∧ find after.globalViews map = some (captureGlobal s snap map) + ∧ localVersion = (revision (captureLocal s snap map) map).version + ∧ globalVersion = (revision (captureGlobal s snap map).frame map).version := by + obtain ⟨view, localRevision, globalRevision⟩ := + step_map_capture w capturedWorld sid tid localVersion globalVersion seq map s before capturedTx snap + store tx snapshot capture live + obtain ⟨after, afterLive, fixed⟩ := + replay_map_global_fixed capturedWorld final tid capturedTx map (captureGlobal s snap map) + tail live view segment accepted + exact ⟨after, afterLive, fixed, localRevision, globalRevision⟩ + intro w capturedWorld final sid tid localVersion globalVersion seq map s before capturedTx snap tail store tx snapshot capture live segment accepted + exact capture_replay_preserves_map w capturedWorld final sid tid localVersion + globalVersion seq map s before capturedTx snap tail store tx snapshot + ((Proofs.Execution.step_iff_transition _ _ _).mp capture) live segment + ((Proofs.Execution.replay_iff_run _ _ _).mp accepted) + +theorem replay_map_local_fixed_claim + : ∀ (w final : World) (tid : Nat) (before : Tx) (map : String) (view : GlobalView) + (rs : List Record), + find w.txs tid = some before + → find before.globalViews map = some view + → (∀ r ∈ rs, AttemptEvent tid r.event) + → CCF.Execution.Run Model.transitionSystem w rs final + → ∃ after, + find final.txs tid = some after + ∧ image after.data map = image before.data map := by + have stepEvent_map_local_fixed (w next : World) (tid : Nat) (before after : Tx) + (map : String) (view : GlobalView) (e : Event) + (live : find w.txs tid = some before) (stillLive : find next.txs tid = some after) + (captured : find before.globalViews map = some view) (segment : AttemptEvent tid e) + (accepted : stepEvent w e = .ok next) + : image after.data map = image before.data map := by + obtain ⟨found, live', kept⟩ := + stepEvent_attempt_kept w next tid before e live segment accepted + cases stillLive.symm.trans live' + exact (kept.2 map view captured).2 + have replay_map_local_fixed (w final : World) (tid : Nat) (before : Tx) (map : String) + (view : GlobalView) (rs : List Record) (live : find w.txs tid = some before) + (captured : find before.globalViews map = some view) + (segment : ∀ r ∈ rs, AttemptEvent tid r.event) (accepted : replay w rs = .ok final) + : ∃ after, + find final.txs tid = some after + ∧ image after.data map = image before.data map := by + obtain ⟨after, afterLive, _, fixed⟩ := + replay_attempt_invariant tid + (fun t => find t.globalViews map = some view ∧ image t.data map = image before.data map) + (fun w next start finish r live stillLive holds segment accepted => by + refine ⟨step_map_global_fixed w next tid start finish map view r live stillLive + holds.1 segment accepted, ?_⟩ + obtain ⟨eventNext, eventStep, _, txs⟩ := step_event_result w next r accepted + exact (stepEvent_map_local_fixed w eventNext tid start finish map view r.event live + (by simpa [txs] using stillLive) holds.1 segment eventStep).trans holds.2) + w final before rs live ⟨captured, rfl⟩ segment accepted + exact ⟨after, afterLive, fixed⟩ + intro w final tid before map view rs live captured segment accepted + exact replay_map_local_fixed w final tid before map view rs live captured segment + ((Proofs.Execution.replay_iff_run _ _ _).mp accepted) + +end Kv.Proofs.Trace diff --git a/lean/kv/Kv/Proofs/Trace.lean b/lean/kv/Kv/Proofs/Trace.lean deleted file mode 100644 index b5f042a54a5..00000000000 --- a/lean/kv/Kv/Proofs/Trace.lean +++ /dev/null @@ -1,813 +0,0 @@ --- Copyright (c) Microsoft Corporation. All rights reserved. --- Licensed under the Apache 2.0 License. - -module - -public import Kv.Properties.Invariants -public import Kv.Proofs.Model - -@[expose] public section - -/-! Supporting lemmas and proof implementations connecting accepted replay to its contracts. -/ - -namespace Kv.Proofs.Trace - -open Kv.Model Kv.Proofs.Invariants Kv.Properties Kv.Proofs.Model - -/-- The head of `after` is that of `before`, or follows from it by applying the listed attempt. -/ -inductive HeadEffect (before after : Store) : List Tx → Prop - /-- The head data and version are unchanged. -/ - | stutter (data : after.head.data = before.head.data) - (version : after.head.version = before.head.version) - : HeadEffect before after [] - /-- One attempt is applied. -/ - | apply (tx : Tx) (one : tryApply before tx = some after) : HeadEffect before after [tx] - -theorem storeOf_ok (w : World) (sid : Nat) (s : Store) - : storeOf w sid = .ok s ↔ find w.stores sid = some s := by - cases h : find w.stores sid <;> simp [storeOf, present, invalid, h] - -theorem unchanged_store_effect (w next : World) (sid : Nat) (s : Store) (e : Event) - (hs : find w.stores sid = some s) (same : next.stores = w.stores) - (noApply : projectedApplication w sid e = []) - : ∃ after, - find next.stores sid = some after - ∧ HeadEffect s after (projectedApplication w sid e) := by - refine ⟨s, ?_, ?_⟩ - · simpa [same] using hs - · rw [noApply] - exact .stutter rfl rfl - -theorem stable_update_store_effect (w next : World) (sid id : Nat) (s old new : Store) - (hs : find w.stores sid = some s) (hold : find w.stores id = some old) - (same : next.stores = set w.stores id new) (head : new.head = old.head) - : ∃ after, find next.stores sid = some after ∧ HeadEffect s after [] := by - by_cases h : id = sid - · subst id - have ho : old = s := Option.some.inj (hold.symm.trans hs) - subst old - exact ⟨new, by simp [same, find_set_same], .stutter (congrArg Frame.data head) - (congrArg Frame.version head)⟩ - · exact ⟨s, by simpa [same, find_set_other _ id sid new h] using hs, .stutter rfl rfl⟩ - -theorem applied_update_store_effect (w next : World) (sid id tid : Nat) - (s old new : Store) (t : Tx) - (hs : find w.stores sid = some s) (hold : storeOf w id = .ok old) - (htx : txOf w id tid = .ok t) (ha : tryApply old t = some new) - (same : next.stores = set w.stores id new) - : ∃ after, - find next.stores sid = some after - ∧ HeadEffect s after - (if id = sid then (txOf w id tid).toOption.toList else []) := by - have hf := (storeOf_ok w id old).mp hold - by_cases h : id = sid - · subst id - have ho : old = s := Option.some.inj (hf.symm.trans hs) - subst old - refine ⟨new, by simp [same, find_set_same], ?_⟩ - simpa [htx, Except.toOption, Option.toList] using HeadEffect.apply t ha - · refine ⟨s, by simpa [same, find_set_other _ id sid new h] using hs, ?_⟩ - simpa [h] using HeadEffect.stutter (before := s) rfl rfl - -theorem snapshot_store_effect (w next : World) (sid : Nat) (s : Store) - (id tid version global term : Nat) (hs : find w.stores sid = some s) - (accepted : stepEvent w (.snapshot id tid version global term) = .ok next) - : ∃ after, find next.stores sid = some after ∧ HeadEffect s after [] := by - cases stepEvent_effect w next _ accepted with - | same stores _ _ | update _ _ stores _ _ => - exact ⟨s, by rw [stores]; exact hs, .stutter rfl rfl⟩ - | snapshot store _ head _ _ _ stores _ => - exact stable_update_store_effect w next sid _ s _ _ hs ((storeOf_ok _ _ _).mp store) stores - head - -theorem stepEvent_store_effect (w next : World) (sid : Nat) (s : Store) (e : Event) - (hs : find w.stores sid = some s) (segment : SegmentEvent sid e) - (accepted : stepEvent w e = .ok next) - : ∃ after, - find next.stores sid = some after - ∧ HeadEffect s after (projectedApplication w sid e) := by - cases stepEvent_effect w next e accepted with - | same stores _ noApply => - exact unchanged_store_effect w next sid s _ hs stores (noApply sid) - | storeCreate stores _ | rollback _ stores _ => - exact ⟨ - s, - by rw [stores, find_set_other _ _ _ _ segment]; exact hs, - .stutter rfl rfl - ⟩ - | storeEnd stores _ => - exact ⟨ - s, - by rw [stores, find_erase_other _ _ _ segment]; exact hs, - .stutter rfl rfl - ⟩ - | txCreate stores _ | txEnd stores _ | acquire _ _ _ stores _ => - exact unchanged_store_effect w next sid s _ hs stores rfl - | compact store stores _ => - exact stable_update_store_effect w next sid _ s _ _ hs ((storeOf_ok _ _ _).mp store) stores - (compact_preserves_head _ _) - | snapshot store _ head _ _ _ stores _ => - exact stable_update_store_effect w next sid _ s _ _ hs ((storeOf_ok _ _ _).mp store) stores - head - | apply store tx applied stores _ => - exact applied_update_store_effect w next sid _ _ s _ _ _ hs store tx applied stores - | update _ _ stores _ noApply => - exact unchanged_store_effect w next sid s _ hs stores (noApply sid) - -theorem step_event_result (w next : World) (r : Record) (accepted : step w r = .ok next) - : ∃ eventNext, - stepEvent w r.event = .ok eventNext - ∧ next.stores = eventNext.stores - ∧ next.txs = eventNext.txs := by - obtain ⟨eventNext, event, rfl⟩ := step_ok accepted - exact ⟨eventNext, event, rfl, rfl⟩ - -theorem step_store_effect (w next : World) (sid : Nat) (s : Store) (r : Record) - (hs : find w.stores sid = some s) (segment : SegmentEvent sid r.event) - (accepted : step w r = .ok next) - : ∃ after, - find next.stores sid = some after - ∧ HeadEffect s after (projectedApplication w sid r.event) := by - obtain ⟨eventNext, he, stores, _⟩ := step_event_result w next r accepted - obtain ⟨after, found, effect⟩ := stepEvent_store_effect w eventNext sid s r.event hs segment he - exact ⟨after, by simpa [stores] using found, effect⟩ - -theorem HeadEffect.serial_witness (before after : Store) (txs : List Tx) - (valid : ∀ t ∈ txs, NormalInvariant t) - (effect : HeadEffect before after txs) - : serialTransactions before.head.data before.head.version txs = some after.head.data - ∧ after.head.version = before.head.version + txs.length := by - cases effect with - | stutter data version => simp [serialTransactions, data, version] - | apply tx one => - have h := tryApply_serial before after tx (valid tx (by simp)) one - constructor - · simpa [serialTransactions, h.1] using congrArg some h.2.symm - · unfold tryApply at one - split at one - next => cases one; rfl - next => simp at one - -theorem serialTransactions_append (db : Data) (version : Nat) (xs ys : List Tx) - : serialTransactions db version (xs ++ ys) - = (serialTransactions db version xs).bind - (fun next => serialTransactions next (version + xs.length) ys) := by - induction xs generalizing db version with - | nil => rfl - | cons tx xs ih => - cases h : serialRun db [] tx.normal.log with - | none => simp [serialTransactions, h] - | some writes => - simp [serialTransactions, h, ih, Nat.add_comm, Nat.add_left_comm] - -theorem projectedApplication_normal (w : World) (valid : WorldInvariant w) - (sid : Nat) (e : Event) - : ∀ t ∈ projectedApplication w sid e, NormalInvariant t := by - cases e <;> simp only [projectedApplication] - all_goals try exact fun _ member => False.elim (List.not_mem_nil member) - rename_i id tid version term writes - intro t member - by_cases same : id = sid - · subst id - simp only [ite_true] at member - cases lookup : txOf w sid tid with - | error err => simp [lookup, Except.toOption] at member - | ok tx => - have equal : t = tx := by - simpa [lookup, Except.toOption, Option.toList] using member - subst t - exact (txOf_invariant w valid sid tid tx lookup).normal - · simp [same] at member - -/-- A selected store stays live throughout the segment. Its rollback/create/end -events partition segments; all other-store events are permitted. The projected -attempts are obtained from the real pre-event txOf, not supplied as a premise. -/ -theorem replay_segment_serializability (w final : World) (sid : Nat) (s : Store) - (valid : WorldInvariant w) - (rs : List Record) (live : find w.stores sid = some s) - (segment : ∀ r ∈ rs, SegmentEvent sid r.event) - (accepted : replay w rs = .ok final) - : ∃ after txs, - find final.stores sid = some after - ∧ projectApplications w sid rs = .ok txs - ∧ serialTransactions s.head.data s.head.version txs = some after.head.data - ∧ after.head.version = s.head.version + txs.length := by - induction rs generalizing w s with - | nil => - cases accepted - exact ⟨s, [], live, rfl, rfl, by simp⟩ - | cons r rs ih => - cases first : step w r with - | error err => simp [replay, first, Except.bind] at accepted - | ok middle => - have rest : replay middle rs = .ok final := by - simpa [replay, first, Except.bind] using accepted - obtain ⟨nextStore, nextLive, effect⟩ := step_store_effect w middle sid s r live - (segment r (by simp)) first - obtain ⟨after, tailTxs, afterLive, projected, tailSerial, tailVersion⟩ := - ih middle nextStore (step_invariant w middle valid r first) nextLive - (fun e he => segment e (by simp [he])) rest - have applications := projectedApplication_normal w valid sid r.event - have one := HeadEffect.serial_witness s nextStore _ applications effect - refine ⟨ - after, - projectedApplication w sid r.event ++ tailTxs, - afterLive, - ?_, - ?_, - ?_ - ⟩ - · simp [projectApplications, first, projected, Bind.bind, Except.bind, Pure.pure, Except.pure] - · rw [serialTransactions_append, one.1] - simpa [← one.2] using tailSerial - · simp only [List.length_append] - rw [tailVersion, one.2] - omega - -theorem reachable_store_invariants (w : World) - (valid : WorldInvariant w) - (sid : Nat) (s : Store) (_live : find w.stores sid = some s) - : History s.history s.head.version - ∧ s.history.head? = some s.head - ∧ s.global ≤ s.head.version - ∧ (atCut s s.global).version = s.global := by - have store := valid.stores sid s _live - exact ⟨store.historyShape, store.headFirst, store.globalBound, - (atCut_spec s store s.global store.globalBound).1⟩ - -theorem foldlM_tx_fixed {A B : Type} (g : Tx → B) (items : List A) - (f : Tx → A → Except Failure Tx) - (fixed : ∀ t a next, f t a = .ok next → g next = g t) - (t next : Tx) (accepted : items.foldlM f t = .ok next) - : g next = g t := by - induction items generalizing t with - | nil => cases accepted; rfl - | cons a items ih => - simp only [List.foldlM_cons, Bind.bind, Except.bind] at accepted - cases one : f t a with - | error err => simp [one] at accepted - | ok middle => - have rest : items.foldlM f middle = .ok next := by simpa [one] using accepted - exact (ih middle rest).trans (fixed t a middle one) - -private theorem absent_ne {xs : Assoc String GlobalView} {map wanted : String} - {view : GlobalView} (absent : find xs map = none) (found : find xs wanted = some view) - : map ≠ wanted := - fun same => by - rw [same, found] at absent - cases absent - -theorem clearWrites_snapshot_fixed (entries : Assoc String String) (map : String) - (t next : Tx) (accepted : clearWrites t map entries = .ok next) - : next.snapshot = t.snapshot := - foldlM_tx_fixed Tx.snapshot entries _ - (fun t (key, _) next h => - runOp_preserves_snapshot t next (.write (map, key) none) h) - t next accepted - -theorem acquireMap_snapshot_fixed (s : Store) (t next : Tx) (map : String) - (version global : Nat) (accepted : acquireMap s t map version global = .ok next) - : next.snapshot = t.snapshot := by - obtain ⟨_, _, _, _, _, rfl⟩ := acquireMap_ok accepted - rfl - -/-- The attempt keeps its captured snapshot, global views and pinned map data. -/ -private def Kept (before after : Tx) : Prop := - (∀ snap, before.snapshot = some snap → after.snapshot = some snap) - ∧ ∀ map view, - find before.globalViews map = some view - → find after.globalViews map = some view - ∧ image after.data map = image before.data map - -private theorem Kept.refl (t : Tx) : Kept t t := ⟨fun _ h => h, fun _ _ h => ⟨h, rfl⟩⟩ - -private theorem Kept.frozen {t next : Tx} (frozen : Frozen t next) : Kept t next := - ⟨ - fun _ h => frozen.snapshot.trans h, - fun _ _ h => by - rw [frozen.globals, frozen.data] - exact ⟨h, rfl⟩ - ⟩ - -private theorem set_kept {xs : Assoc Nat Tx} {tid id : Nat} {before next : Tx} - (live : find xs tid = some before) (kept : id = tid → Kept before next) - : ∃ after, find (set xs id next) tid = some after ∧ Kept before after := by - by_cases h : id = tid - · subst h - exact ⟨next, find_set_same _ _ _, kept rfl⟩ - · exact ⟨before, by rw [find_set_other _ _ _ _ h]; exact live, Kept.refl before⟩ - -private theorem stepEvent_attempt_kept (w next : World) (tid : Nat) (before : Tx) - (e : Event) (live : find w.txs tid = some before) (segment : AttemptEvent tid e) - (accepted : stepEvent w e = .ok next) - : ∃ after, find next.txs tid = some after ∧ Kept before after := by - cases stepEvent_effect w next e accepted with - | same _ txs | storeCreate _ txs | storeEnd _ txs | compact _ _ txs | rollback _ _ txs - => - exact ⟨before, by rw [txs]; exact live, Kept.refl before⟩ - | txCreate _ txs => - exact ⟨ - before, - by rw [txs, find_set_other _ _ _ _ segment]; exact live, - Kept.refl before - ⟩ - | txEnd _ txs => - exact ⟨ - before, - by rw [txs, find_erase_other _ _ _ segment]; exact live, - Kept.refl before - ⟩ - | snapshot _ _ _ _ tx fresh _ txs => - rw [txs] - refine set_kept live fun same => ?_ - subst same - cases tx.symm.trans live - exact ⟨fun _ h => (by rw [fresh] at h; cases h), fun _ _ h => ⟨h, rfl⟩⟩ - | acquire _ tx acquired _ txs => - rw [txs] - refine set_kept live fun same => ?_ - subst same - cases (txOf_found _ _ _ _ tx).symm.trans live - obtain ⟨snap, _, fresh, _, _, rfl⟩ := acquireMap_ok acquired - refine ⟨fun _ h => h, fun map view h => ?_⟩ - have other := absent_ne fresh h - exact ⟨ - by rw [find_set_other _ _ _ _ other]; exact h, - Invariants.pinData_other _ _ _ _ (Ne.symm other) - ⟩ - | apply _ tx _ _ txs => - rw [txs] - refine set_kept live fun same => ?_ - subst same - cases (txOf_found _ _ _ _ tx).symm.trans live - exact Kept.refl _ - | update tx frozen _ txs => - rw [txs] - refine set_kept live fun same => ?_ - subst same - cases (txOf_found _ _ _ _ tx).symm.trans live - exact Kept.frozen frozen - -theorem stepEvent_snapshot_fixed (w next : World) (tid : Nat) (before after : Tx) - (snap : Snapshot) (e : Event) - (live : find w.txs tid = some before) (stillLive : find next.txs tid = some after) - (captured : before.snapshot = some snap) (segment : AttemptEvent tid e) - (accepted : stepEvent w e = .ok next) - : after.snapshot = some snap := by - obtain ⟨found, live', kept⟩ := - stepEvent_attempt_kept w next tid before e live segment accepted - cases stillLive.symm.trans live' - exact kept.1 snap captured - -theorem step_snapshot_fixed (w next : World) (tid : Nat) (before after : Tx) - (snap : Snapshot) (r : Record) - (live : find w.txs tid = some before) (stillLive : find next.txs tid = some after) - (captured : before.snapshot = some snap) (segment : AttemptEvent tid r.event) - (accepted : step w r = .ok next) - : after.snapshot = some snap := by - obtain ⟨eventNext, eventStep, _, txs⟩ := step_event_result w next r accepted - apply stepEvent_snapshot_fixed w eventNext tid before after snap r.event live - (by simpa [txs] using stillLive) captured segment eventStep - -theorem find_set_live {K V : Type} [DecidableEq K] (xs : Assoc K V) (key : K) (before : V) - (id : K) (value : V) (live : find xs key = some before) - : ∃ after, find (set xs id value) key = some after := by - by_cases h : id = key - · exact ⟨value, by simp [h, find_set_same]⟩ - · exact ⟨before, by simpa [find_set_other, h] using live⟩ - -theorem stepEvent_attempt_live (w next : World) (tid : Nat) (before : Tx) (e : Event) - (live : find w.txs tid = some before) (segment : AttemptEvent tid e) - (accepted : stepEvent w e = .ok next) - : ∃ after, find next.txs tid = some after := by - obtain ⟨after, found, -⟩ := stepEvent_attempt_kept w next tid before e live segment accepted - exact ⟨after, found⟩ - -theorem replay_attempt_invariant (tid : Nat) (P : Tx → Prop) - (preserve - : ∀ (w next : World) (before after : Tx) (r : Record), - find w.txs tid = some before - → find next.txs tid = some after - → P before - → AttemptEvent tid r.event - → step w r = .ok next - → P after) - (w final : World) (before : Tx) - (rs : List Record) (live : find w.txs tid = some before) - (holds : P before) - (segment : ∀ r ∈ rs, AttemptEvent tid r.event) - (accepted : replay w rs = .ok final) - : ∃ after, find final.txs tid = some after ∧ P after := by - induction rs generalizing w before with - | nil => cases accepted; exact ⟨before, live, holds⟩ - | cons r rs ih => - cases one : step w r with - | error err => simp [replay, one, Except.bind] at accepted - | ok middle => - obtain ⟨eventNext, eventStep, _, txs⟩ := step_event_result w middle r one - have thisSegment := segment r (by simp) - obtain ⟨midTx, midLive⟩ := stepEvent_attempt_live w eventNext tid before r.event - live thisSegment eventStep - have midLive' : find middle.txs tid = some midTx := by simpa [txs] using midLive - have midProperty := - preserve w middle before midTx r live midLive' holds thisSegment one - apply ih middle midTx midLive' midProperty - · intro e he; exact segment e (by simp [he]) - · simpa [replay, one, Except.bind] using accepted - -theorem replay_snapshot_fixed (w final : World) (tid : Nat) (before : Tx) - (snap : Snapshot) (rs : List Record) (live : find w.txs tid = some before) - (captured : before.snapshot = some snap) - (segment : ∀ r ∈ rs, AttemptEvent tid r.event) (accepted : replay w rs = .ok final) - : ∃ after, find final.txs tid = some after ∧ after.snapshot = some snap := - replay_attempt_invariant tid (fun t => t.snapshot = some snap) - (fun w next before after r => step_snapshot_fixed w next tid before after snap r) - w final before rs live captured segment accepted - -theorem stepEvent_capture_metadata (w next : World) (sid tid version global term : Nat) - (s : Store) (t : Tx) (source : storeOf w sid = .ok s) - (accepted : stepEvent w (.snapshot sid tid version global term) = .ok next) - (capturedTx : find next.txs tid = some t) - : ∃ snap, t.snapshot = some snap ∧ snap.current = s.head ∧ snap.term = term := by - refine ⟨{ current := s.head, term }, ?_, rfl, rfl⟩ - obtain ⟨_, store, accepted⟩ := bind_ok accepted - cases source.symm.trans store - obtain ⟨_, _, -, h, rfl⟩ := withTx_ok accepted - obtain ⟨_, -, h⟩ := bind_ok h - split at h - · obtain ⟨_, -, h⟩ := bind_ok h - cases pure_ok h - simp only [find_set_same, Option.some.injEq] at capturedTx - subst capturedTx - rfl - · cases h - -theorem step_capture_metadata (w next : World) (sid tid version global term seq : Nat) - (s : Store) (t : Tx) (source : storeOf w sid = .ok s) - (accepted : step w ⟨seq, .snapshot sid tid version global term⟩ = .ok next) - (capturedTx : find next.txs tid = some t) - : ∃ snap, t.snapshot = some snap ∧ snap.current = s.head ∧ snap.term = term := by - obtain ⟨eventNext, eventStep, _, txs⟩ := step_event_result w next _ accepted - exact stepEvent_capture_metadata w eventNext sid tid version global term s t source - eventStep (by simpa [txs] using capturedTx) - -theorem stepEvent_capture_cut_values (w next : World) (sid tid version global term : Nat) - (s : Store) (source : storeOf w sid = .ok s) - (accepted : stepEvent w (.snapshot sid tid version global term) = .ok next) - : version = s.head.version ∧ global = s.global := by - obtain ⟨_, store, accepted⟩ := bind_ok accepted - cases source.symm.trans store - obtain ⟨_, _, -, h, -⟩ := withTx_ok accepted - obtain ⟨_, -, h⟩ := bind_ok h - split at h - · obtain ⟨_, metadata, -⟩ := bind_ok h - have metadata := expect_ok metadata - simp only [Bool.and_eq_true, beq_iff_eq] at metadata - exact metadata.1 - · cases h - -theorem step_capture_cut_values (w next : World) (sid tid version global term seq : Nat) - (s : Store) (source : storeOf w sid = .ok s) - (accepted : step w ⟨seq, .snapshot sid tid version global term⟩ = .ok next) - : version = s.head.version ∧ global = s.global := by - obtain ⟨eventNext, eventStep, _, _⟩ := step_event_result w next _ accepted - exact stepEvent_capture_cut_values w eventNext sid tid version global term s source eventStep - -theorem capture_replay_preserves_metadata (w capturedWorld final : World) - (sid tid version global term seq : Nat) (s : Store) (t : Tx) (tail : List Record) - (source : storeOf w sid = .ok s) - (capture : step w ⟨seq, .snapshot sid tid version global term⟩ = .ok capturedWorld) - (live : find capturedWorld.txs tid = some t) - (segment : ∀ r ∈ tail, AttemptEvent tid r.event) - (accepted : replay capturedWorld tail = .ok final) - : ∃ after snap, - find final.txs tid = some after - ∧ after.snapshot = some snap - ∧ snap.current = s.head - ∧ snap.term = term := by - obtain ⟨snap, captured, current, snapshotTerm⟩ := - step_capture_metadata w capturedWorld sid tid version global term seq s t source capture live - obtain ⟨after, afterLive, same⟩ := replay_snapshot_fixed capturedWorld final tid t snap - tail live captured segment accepted - exact ⟨after, snap, afterLive, same, current, snapshotTerm⟩ - -theorem publish_cells_bounded (db : Data) (version : Nat) (writes : Pending) - (before : CellsBounded db version) - : CellsBounded (publish db version writes) version := by - intro key cell found - rw [publish_lookup] at found - cases hw : find writes key with - | none => exact before key cell (by simpa [hw] using found) - | some value => - cases value with - | none => simp [hw] at found - | some v => - simp [hw] at found - cases found - exact Nat.le_refl _ - -theorem History.head_cells_bounded (fs : List Frame) (n : Nat) (shape : History fs n) - : CellsBounded (fs.head?.getD {}).data n := by - induction shape with - | zero => - intro key cell found - simp [find] at found - | succ f n fs _version effect _tail ih => - obtain ⟨writes, published⟩ := effect - simp only [List.head?_cons, Option.getD_some] - rw [published] - apply publish_cells_bounded - intro key cell found - exact Nat.le_trans (ih key cell found) (Nat.le_succ n) - -theorem atCut_cells_bounded (s : Store) (valid : StoreInvariant s) - (cut : Nat) (within : cut ≤ s.head.version) - : CellsBounded (atCut s cut).data cut := by - have spec := atCut_spec s valid cut within - have h := History.head_cells_bounded _ cut spec.2.1 - simpa only [spec.2.2, Option.getD_some] using h - -theorem History.head_unique (fs : List Frame) (n : Nat) (shape : History fs n) - : Kv.Properties.Unique (fs.head?.getD {}).data := by - induction shape with - | zero => simp [Kv.Properties.Unique] - | succ f n fs _version effect _tail ih => - obtain ⟨writes, published⟩ := effect - simp only [List.head?_cons, Option.getD_some] - rw [published] - exact publish_unique _ _ _ ih - -theorem reachable_store_data_invariants (w : World) - (valid : WorldInvariant w) - (sid : Nat) (s : Store) (_live : find w.stores sid = some s) - : Kv.Properties.Unique s.head.data ∧ CellsBounded s.head.data s.head.version := by - have store := valid.stores sid s _live - have unique := History.head_unique s.history s.head.version store.historyShape - have bounded := History.head_cells_bounded s.history s.head.version store.historyShape - simpa only [store.headFirst, Option.getD_some] using And.intro unique bounded - -theorem stepEvent_get_global (w next : World) (sid tid : Nat) (map key : String) - (value : Option String) (t : Tx) (view : GlobalView) - (source : txOf w sid tid = .ok t) (captured : find t.globalViews map = some view) - (accepted : stepEvent w (.get sid tid map key value true) = .ok next) - : value = (find view.frame.data (map, key)).map Cell.value := by - obtain ⟨_, _, tx, h, -⟩ := withTx_ok accepted - cases source.symm.trans tx - obtain ⟨_, -, h⟩ := bind_ok h - obtain ⟨_, found, h⟩ := bind_ok h - cases captured.symm.trans (present_ok found) - obtain ⟨_, observed, -⟩ := bind_ok h - exact (beq_iff_eq.mp (expect_ok observed)).symm - -theorem map_global_view_safety (view : GlobalView) (valid : GlobalInvariant view) - : view.frame = {} - ∨ ∃ origin : Store, - view.frame = atCut origin origin.global - ∧ view.frame.version = origin.global - ∧ CellsBounded view.frame.data origin.global := by - rcases valid with placeholder | ⟨origin, store, committed⟩ - · exact Or.inl placeholder - · refine Or.inr ⟨origin, committed, ?_, ?_⟩ - · rw [committed]; exact (atCut_spec origin store origin.global store.globalBound).1 - · rw [committed]; exact atCut_cells_bounded origin store origin.global store.globalBound - -theorem step_global_read_from_captured_map (w next : World) (sid tid seq : Nat) - (valid : WorldInvariant w) - (map key : String) (value : Option String) (t : Tx) (view : GlobalView) - (source : txOf w sid tid = .ok t) (captured : find t.globalViews map = some view) - (accepted : step w ⟨seq, .get sid tid map key value true⟩ = .ok next) - : value = (find view.frame.data (map, key)).map Cell.value - ∧ (view.frame = {} - ∨ ∃ origin : Store, - view.frame = atCut origin origin.global - ∧ view.frame.version = origin.global - ∧ CellsBounded view.frame.data origin.global) := by - obtain ⟨eventNext, eventStep, _, _⟩ := step_event_result w next _ accepted - exact ⟨stepEvent_get_global w eventNext sid tid map key value t view source captured eventStep, - map_global_view_safety view - ((txOf_invariant w valid sid tid t source).globals map view captured)⟩ - -theorem stepEvent_has_global (w next : World) (sid tid : Nat) (map key : String) - (value : Bool) (t : Tx) (view : GlobalView) - (source : txOf w sid tid = .ok t) (captured : find t.globalViews map = some view) - (accepted : stepEvent w (.has sid tid map key value true) = .ok next) - : value = (find view.frame.data (map, key)).isSome := by - obtain ⟨_, _, tx, h, -⟩ := withTx_ok accepted - cases source.symm.trans tx - obtain ⟨_, -, h⟩ := bind_ok h - obtain ⟨_, found, h⟩ := bind_ok h - cases captured.symm.trans (present_ok found) - obtain ⟨_, observed, -⟩ := bind_ok h - exact (beq_iff_eq.mp (expect_ok observed)).symm - -theorem step_global_has_from_captured_map (w next : World) (sid tid seq : Nat) - (valid : WorldInvariant w) - (map key : String) (value : Bool) (t : Tx) (view : GlobalView) - (source : txOf w sid tid = .ok t) (captured : find t.globalViews map = some view) - (accepted : step w ⟨seq, .has sid tid map key value true⟩ = .ok next) - : value = (find view.frame.data (map, key)).isSome - ∧ (view.frame = {} - ∨ ∃ origin : Store, - view.frame = atCut origin origin.global - ∧ view.frame.version = origin.global - ∧ CellsBounded view.frame.data origin.global) := by - obtain ⟨eventNext, eventStep, _, _⟩ := step_event_result w next _ accepted - exact ⟨stepEvent_has_global w eventNext sid tid map key value t view source captured eventStep, - map_global_view_safety view - ((txOf_invariant w valid sid tid t source).globals map view captured)⟩ - -theorem captureGlobal_placeholder (s : Store) (snap : Snapshot) (map : String) - (absent : find (captureLocal s snap map).births map = none) - : (captureGlobal s snap map).frame = {} := by - simp [captureGlobal, absent] - -theorem captureGlobal_committed (s : Store) (snap : Snapshot) (map : String) - (birth : Stamp) (existing : find (captureLocal s snap map).births map = some birth) - : (captureGlobal s snap map).frame = atCut s s.global := by - simp [captureGlobal, existing] - -theorem captureGlobal_current (s : Store) (snap : Snapshot) (map : String) - : (captureGlobal s snap map).current = captureLocal s snap map := by - dsimp only [captureGlobal] - split <;> rfl - -theorem stepEvent_map_capture (w next : World) (sid tid localVersion globalVersion : Nat) - (map : String) (s : Store) (before after : Tx) (snap : Snapshot) - (store : storeOf w sid = .ok s) (tx : txOf w sid tid = .ok before) - (snapshot : before.snapshot = some snap) - (accepted : stepEvent w (.acquire sid tid map localVersion globalVersion) = .ok next) - (live : find next.txs tid = some after) - : find after.globalViews map = some (captureGlobal s snap map) - ∧ localVersion = (revision (captureLocal s snap map) map).version - ∧ globalVersion = (revision (captureGlobal s snap map).frame map).version := by - obtain ⟨_, store', accepted⟩ := bind_ok accepted - cases store.symm.trans store' - obtain ⟨_, _, tx', h, rfl⟩ := withTx_ok accepted - cases tx.symm.trans tx' - obtain ⟨_, captured, -, versions, _, rfl⟩ := acquireMap_ok h - cases snapshot.symm.trans captured - simp only [find_set_same, Option.some.injEq] at live - subst live - rw [captureGlobal_current] at versions - exact ⟨find_set_same _ _ _, versions⟩ - -theorem step_map_capture (w next : World) (sid tid localVersion globalVersion seq : Nat) - (map : String) (s : Store) (before after : Tx) (snap : Snapshot) - (store : storeOf w sid = .ok s) (tx : txOf w sid tid = .ok before) - (snapshot : before.snapshot = some snap) - (accepted : step w ⟨seq, .acquire sid tid map localVersion globalVersion⟩ = .ok next) - (live : find next.txs tid = some after) - : find after.globalViews map = some (captureGlobal s snap map) - ∧ localVersion = (revision (captureLocal s snap map) map).version - ∧ globalVersion = (revision (captureGlobal s snap map).frame map).version := by - obtain ⟨eventNext, eventStep, _, txs⟩ := step_event_result w next _ accepted - exact stepEvent_map_capture w eventNext sid tid localVersion globalVersion map s before - after snap store tx snapshot eventStep (by simpa [txs] using live) - -theorem runOp_globalViews_fixed (t next : Tx) (op : NormalOp String String String) - (accepted : runOp t op = .ok next) - : next.globalViews = t.globalViews := by - unfold runOp at accepted - split at accepted - next => simp [invalid] at accepted - next snap _ => - split at accepted - next n _ => - simp [Pure.pure, Except.pure] at accepted - cases accepted - rfl - next => simp [reject] at accepted - -theorem clearWrites_globalViews_fixed (entries : Assoc String String) (map : String) - (t next : Tx) (accepted : clearWrites t map entries = .ok next) - : next.globalViews = t.globalViews := - foldlM_tx_fixed Tx.globalViews entries _ - (fun t (key, _) next h => - runOp_globalViews_fixed t next (.write (map, key) none) h) - t next accepted - -theorem acquireMap_global_fixed (s : Store) (t next : Tx) (map wanted : String) - (version global : Nat) (view : GlobalView) - (captured : find t.globalViews wanted = some view) - (accepted : acquireMap s t map version global = .ok next) - : find next.globalViews wanted = some view := by - obtain ⟨_, _, fresh, _, _, rfl⟩ := acquireMap_ok accepted - have other := absent_ne fresh captured - rw [find_set_other _ _ _ _ other] - exact captured - -theorem stepEvent_map_global_fixed (w next : World) (tid : Nat) (before after : Tx) - (map : String) (view : GlobalView) (e : Event) - (live : find w.txs tid = some before) (stillLive : find next.txs tid = some after) - (captured : find before.globalViews map = some view) (segment : AttemptEvent tid e) - (accepted : stepEvent w e = .ok next) - : find after.globalViews map = some view := by - obtain ⟨found, live', kept⟩ := - stepEvent_attempt_kept w next tid before e live segment accepted - cases stillLive.symm.trans live' - exact (kept.2 map view captured).1 - -theorem step_map_global_fixed (w next : World) (tid : Nat) (before after : Tx) - (map : String) (view : GlobalView) (r : Record) (live : find w.txs tid = some before) - (stillLive : find next.txs tid = some after) - (captured : find before.globalViews map = some view) - (segment : AttemptEvent tid r.event) (accepted : step w r = .ok next) - : find after.globalViews map = some view := by - obtain ⟨eventNext, eventStep, _, txs⟩ := step_event_result w next r accepted - exact stepEvent_map_global_fixed w eventNext tid before after map view r.event live - (by simpa [txs] using stillLive) captured segment eventStep - -theorem replay_map_global_fixed (w final : World) (tid : Nat) (before : Tx) (map : String) - (view : GlobalView) (rs : List Record) (live : find w.txs tid = some before) - (captured : find before.globalViews map = some view) - (segment : ∀ r ∈ rs, AttemptEvent tid r.event) (accepted : replay w rs = .ok final) - : ∃ after, find final.txs tid = some after ∧ find after.globalViews map = some view := - replay_attempt_invariant tid (fun t => find t.globalViews map = some view) - (fun w next before after r => - step_map_global_fixed w next tid before after map view r) - w final before rs live captured segment accepted - -theorem runOp_data_fixed (t next : Tx) (op : NormalOp String String String) - (accepted : runOp t op = .ok next) - : next.data = t.data := by - unfold runOp at accepted - split at accepted - next => simp [invalid] at accepted - next snap _ => - split at accepted - next n _ => - simp [Pure.pure, Except.pure] at accepted - cases accepted - rfl - next => simp [reject] at accepted - -theorem clearWrites_data_fixed (entries : Assoc String String) (map : String) - (t next : Tx) (accepted : clearWrites t map entries = .ok next) - : next.data = t.data := - foldlM_tx_fixed Tx.data entries _ - (fun t (key, _) next h => runOp_data_fixed t next (.write (map, key) none) h) - t next accepted - -theorem acquireMap_data_fixed (s : Store) (t next : Tx) (map wanted : String) - (version global : Nat) (view : GlobalView) - (captured : find t.globalViews wanted = some view) - (accepted : acquireMap s t map version global = .ok next) - : image next.data wanted = image t.data wanted := by - obtain ⟨_, _, fresh, _, _, rfl⟩ := acquireMap_ok accepted - have other := absent_ne fresh captured - exact Invariants.pinData_other _ _ _ _ (Ne.symm other) - -theorem stepEvent_map_local_fixed (w next : World) (tid : Nat) (before after : Tx) - (map : String) (view : GlobalView) (e : Event) - (live : find w.txs tid = some before) (stillLive : find next.txs tid = some after) - (captured : find before.globalViews map = some view) (segment : AttemptEvent tid e) - (accepted : stepEvent w e = .ok next) - : image after.data map = image before.data map := by - obtain ⟨found, live', kept⟩ := - stepEvent_attempt_kept w next tid before e live segment accepted - cases stillLive.symm.trans live' - exact (kept.2 map view captured).2 - -theorem replay_map_local_fixed (w final : World) (tid : Nat) (before : Tx) (map : String) - (view : GlobalView) (rs : List Record) (live : find w.txs tid = some before) - (captured : find before.globalViews map = some view) - (segment : ∀ r ∈ rs, AttemptEvent tid r.event) (accepted : replay w rs = .ok final) - : ∃ after, - find final.txs tid = some after - ∧ image after.data map = image before.data map := by - obtain ⟨after, afterLive, _, fixed⟩ := - replay_attempt_invariant tid - (fun t => find t.globalViews map = some view ∧ image t.data map = image before.data map) - (fun w next start finish r live stillLive holds segment accepted => by - refine ⟨step_map_global_fixed w next tid start finish map view r live stillLive - holds.1 segment accepted, ?_⟩ - obtain ⟨eventNext, eventStep, _, txs⟩ := step_event_result w next r accepted - exact (stepEvent_map_local_fixed w eventNext tid start finish map view r.event live - (by simpa [txs] using stillLive) holds.1 segment eventStep).trans holds.2) - w final before rs live ⟨captured, rfl⟩ segment accepted - exact ⟨after, afterLive, fixed⟩ - -theorem capture_replay_preserves_map (w capturedWorld final : World) - (sid tid localVersion globalVersion seq : Nat) (map : String) - (s : Store) (before capturedTx : Tx) (snap : Snapshot) (tail : List Record) - (store : storeOf w sid = .ok s) (tx : txOf w sid tid = .ok before) - (snapshot : before.snapshot = some snap) - (capture - : step w ⟨seq, .acquire sid tid map localVersion globalVersion⟩ = .ok capturedWorld) - (live : find capturedWorld.txs tid = some capturedTx) - (segment : ∀ r ∈ tail, AttemptEvent tid r.event) - (accepted : replay capturedWorld tail = .ok final) - : ∃ after, - find final.txs tid = some after - ∧ find after.globalViews map = some (captureGlobal s snap map) - ∧ localVersion = (revision (captureLocal s snap map) map).version - ∧ globalVersion = (revision (captureGlobal s snap map).frame map).version := by - obtain ⟨view, localRevision, globalRevision⟩ := - step_map_capture w capturedWorld sid tid localVersion globalVersion seq map s before capturedTx snap - store tx snapshot capture live - obtain ⟨after, afterLive, fixed⟩ := - replay_map_global_fixed capturedWorld final tid capturedTx map (captureGlobal s snap map) - tail live view segment accepted - exact ⟨after, afterLive, fixed, localRevision, globalRevision⟩ - -end Kv.Proofs.Trace diff --git a/lean/kv/Kv/Proofs/Witnesses.lean b/lean/kv/Kv/Proofs/Witnesses.lean index ac619badf03..b76709aacf7 100644 --- a/lean/kv/Kv/Proofs/Witnesses.lean +++ b/lean/kv/Kv/Proofs/Witnesses.lean @@ -4,17 +4,552 @@ module public import Kv.Properties.Invariants -public import Kv.Proofs.Execution -public import Kv.Proofs.Invariants - -@[expose] public section /-! -Non-vacuity witnesses for the claims in `Kv.Properties`. Trace claims are witnessed by prefixes -and segments of one accepted trace, evaluated by the kernel; store claims by directly -constructed stores; read and publication claims by small concrete association lists. +Non-vacuity witnesses for the claims in `Kv.Properties`, together with the executable model's +read, publication and store claims. Trace claims are witnessed by prefixes and segments of one +accepted trace, evaluated by the kernel; store claims by directly constructed stores; read and +publication claims by small concrete association lists. + +Each proof module under `Kv/Proofs/` is self-contained: lemmas needed by more than one module are +duplicated as private declarations, so the proof modules do not import each other and Lake can +check them in parallel. This layout is chosen to minimize verification wall-clock time. -/ +@[expose] public section + +namespace Kv.Proofs.Execution +end Kv.Proofs.Execution + +namespace Kv.Proofs.Invariants +end Kv.Proofs.Invariants + +namespace Kv.Proofs.Model +end Kv.Proofs.Model + +namespace Kv.Proofs.Trace +end Kv.Proofs.Trace + +namespace Kv.Proofs.Properties +end Kv.Proofs.Properties + +namespace Kv.Proofs.Witnesses +end Kv.Proofs.Witnesses + +namespace Kv.Proofs.Execution + +open Kv.Model + +private theorem step_iff_transition (w next : World) (r : Record) + : transitionSystem.step w r = some next ↔ step w r = .ok next := by + simp only [transitionSystem] + cases step w r <;> simp [Except.toOption] + +end Kv.Proofs.Execution + +namespace Kv.Proofs.Invariants + +open Kv.Model Kv.Properties + +/-- Store histories are contiguous, headed by the current frame, and contain the global cut. -/ +private structure StoreInvariant (s : Store) : Prop where + /-- Every frame follows by publishing writes to its predecessor. -/ + historyShape : History s.history s.head.version + /-- The head is the newest frame. -/ + headFirst : s.history.head? = some s.head + /-- The global version does not exceed the head. -/ + globalBound : s.global ≤ s.head.version + +end Kv.Proofs.Invariants + +namespace Kv.Proofs.Invariants + +open Kv.Model Kv.Properties +variable {M K V : Type} + +private theorem find_set_same [DecidableEq K] (xs : Assoc K V) (k : K) (v : V) + : find (set xs k v) k = some v := by + simp [Model.set, find] + +private theorem find_erase_same [DecidableEq K] (xs : Assoc K V) (k : K) + : find (erase xs k) k = none := by + induction xs with + | nil => rfl + | cons p xs ih => + rcases p with ⟨a, v⟩ + by_cases h : a = k <;> simp_all [erase, find] + +private theorem find_erase_other [DecidableEq K] (xs : Assoc K V) (a k : K) (h : a ≠ k) + : find (erase xs a) k = find xs k := by + induction xs with + | nil => rfl + | cons p xs ih => + rcases p with ⟨b, v⟩ + by_cases hba : b = a <;> by_cases hbk : b = k <;> simp_all [erase, find] + +private theorem find_set_other [DecidableEq K] (xs : Assoc K V) (a k : K) (v : V) + (h : a ≠ k) + : find (set xs a v) k = find xs k := by + simp [Model.set, find, h, find_erase_other xs a k h] + +private theorem history_extension (s : Store) (valid : StoreInvariant s) (f : Frame) + (writes : Pending) (version : f.version = s.head.version + 1) + (data : f.data = publish s.head.data (s.head.version + 1) writes) + : History (f :: s.history) (s.head.version + 1) := + .succ f s.head.version s.history version + ⟨writes, by simpa only [valid.headFirst, Option.getD_some] using data⟩ + valid.historyShape + +private theorem store_initial : StoreInvariant {} := + ⟨.zero, rfl, Nat.le_refl 0⟩ + +private theorem advance_invariant (s : Store) (valid : StoreInvariant s) + (writes : Pending) + : StoreInvariant (advance s writes) := + ⟨ + history_extension s valid _ writes rfl rfl, + rfl, + Nat.le_trans valid.globalBound (Nat.le_succ _) + ⟩ + +private theorem bind_ok {α β : Type} {x : Except Failure α} {f : α → Except Failure β} + {b : β} (h : (x >>= f) = .ok b) + : ∃ a, x = .ok a ∧ f a = .ok b := by + cases x with + | error => cases h + | ok a => exact ⟨a, rfl, h⟩ + +private theorem pure_ok {α : Type} {a b : α} (h : (pure a : Except Failure α) = .ok b) + : a = b := by + cases h; rfl + +private theorem withTx_ok {w next : World} {sid tid : Nat} {f : Tx → Except Failure Tx} + (h : withTx w sid tid f = .ok next) + : ∃ t t', + txOf w sid tid = .ok t + ∧ f t = .ok t' + ∧ next = { w with txs := set w.txs tid t' } := by + obtain ⟨t, tx, h⟩ := bind_ok h + obtain ⟨t', f, h⟩ := bind_ok h + exact ⟨t, t', tx, f, (pure_ok h).symm⟩ + +private theorem present_ok {α : Type} {value : Option α} {message : String} {a : α} + (h : present value message = .ok a) + : value = some a := by + cases value with + | none => cases h + | some => cases h; rfl + +private theorem require_ok {condition : Bool} {message : String} {u : Unit} + (h : require condition message = .ok u) + : condition = true := by + cases condition + · cases h + · rfl + +private theorem expect_ok {condition : Bool} {message : String} {u : Unit} + (h : expect condition message = .ok u) + : condition = true := by + cases condition + · cases h + · rfl + +private theorem acquireMap_ok {s : Store} {t next : Tx} {map : String} + {version global : Nat} (accepted : acquireMap s t map version global = .ok next) + : ∃ snap, + t.snapshot = some snap + ∧ find t.globalViews map = none + ∧ (version = (revision (captureGlobal s snap map).current map).version + ∧ global = (revision (captureGlobal s snap map).frame map).version) + ∧ t.normal.log.all (fun op => op.map != map) = true + ∧ next + = { + t with + globalViews := set t.globalViews map (captureGlobal s snap map) + data := pinData t.data map (captureGlobal s snap map).current.data + } := by + obtain ⟨_, -, accepted⟩ := bind_ok accepted + obtain ⟨_, -, accepted⟩ := bind_ok accepted + obtain ⟨snap, captured, accepted⟩ := bind_ok accepted + obtain ⟨_, fresh, accepted⟩ := bind_ok accepted + obtain ⟨_, versions, accepted⟩ := bind_ok accepted + obtain ⟨_, -, accepted⟩ := bind_ok accepted + split at accepted + next unused => + cases pure_ok accepted + have versions := expect_ok versions + simp only [Bool.and_eq_true, beq_iff_eq] at versions + exact ⟨snap, present_ok captured, Option.isNone_iff_eq_none.mp (require_ok fresh), versions, + unused, rfl⟩ + next => cases accepted + +private theorem step_ok {w next : World} {r : Record} (accepted : step w r = .ok next) + : ∃ eventNext, + stepEvent w r.event = .ok eventNext + ∧ next = { eventNext with lastSeq := some r.seq, count := w.count + 1 } := by + obtain ⟨_, -, accepted⟩ := bind_ok accepted + obtain ⟨_, -, accepted⟩ := bind_ok accepted + obtain ⟨seq, event⟩ := r + dsimp only at accepted ⊢ + split at accepted <;> try split at accepted + all_goals first + | obtain ⟨_, invalid, -⟩ := bind_ok accepted; cases invalid + | obtain ⟨eventNext, event, accepted⟩ := bind_ok accepted + exact ⟨eventNext, event, (pure_ok accepted).symm⟩ + +end Kv.Proofs.Invariants + +namespace Kv.Proofs.Model + +open Kv.Model Kv.Proofs.Invariants Kv.Properties +section Generic +variable {M K V : Type} [DecidableEq M] [DecidableEq K] + +private theorem find_image (db : DB M K V) (m : M) (key : K) + : find (image db m) key = find db (m, key) := by + induction db with + | nil => rfl + | cons entry db ih => + rcases entry with ⟨⟨map, k⟩, cell⟩ + by_cases hm : map = m <;> by_cases hk : k = key <;> + simp_all [image, find, Prod.mk.injEq] + +private theorem empty_map_has_no_values (db : DB M K V) (m : M) (key : K) + (empty : image db m = []) + : find db (m, key) = none := by + rw [← find_image, empty] + rfl + +private theorem erase_keys (xs : Assoc K V) (k : K) + : (erase xs k).map Prod.fst = (xs.map Prod.fst).filter (· != k) := + (List.filter_map (f := Prod.fst) (p := (· != k)) (l := xs)).symm + +private theorem erase_unique (xs : Assoc K V) (k : K) (h : Kv.Properties.Unique xs) + : Kv.Properties.Unique (erase xs k) := by + unfold Kv.Properties.Unique + rw [erase_keys] + exact List.Pairwise.filter _ h + +private theorem set_unique (xs : Assoc K V) (k : K) (v : V) (h : Kv.Properties.Unique xs) + : Kv.Properties.Unique (set xs k v) := by + simp only [Kv.Properties.Unique, Model.set, List.map_cons, List.nodup_cons] + constructor + · simp [erase_keys, eq_comm] + · exact erase_unique xs k h + +theorem publish_lookup (db : DB M K V) (version : Nat) (ws : Writes M K V) (a : Addr M K) + : find (publish db version ws) a + = match find ws a with + | none => find db a + | some none => none + | some (some v) => some { value := v, version } := by + induction ws with + | nil => rfl + | cons p ws ih => + rcases p with ⟨b, value⟩ + by_cases h : b = a + · subst b + cases value <;> simp [publish, find, find_set_same, find_erase_same] + · cases value <;> simp [publish, find, h, find_set_other, find_erase_other, ← ih, publish] + +theorem publish_unique (db : DB M K V) (version : Nat) (ws : Writes M K V) + (h : Kv.Properties.Unique db) + : Kv.Properties.Unique (publish db version ws) := by + induction ws with + | nil => exact h + | cons p ws ih => + rcases p with ⟨a, v⟩ + cases v with + | none => exact erase_unique _ a ih + | some value => exact set_unique _ a ⟨value, version⟩ ih + +theorem publication_noninterference (db : DB M K V) (version : Nat) + (ws : Writes M K V) (a : Addr M K) (h : find ws a = none) + : find (publish db version ws) a = find db a := by + simp [publish_lookup, h] + +theorem read_your_write (db : DB M K V) (ws : Writes M K V) (a : Addr M K) (v : V) + : valueAt db (set ws a (some v)) a = some v := by + simp [valueAt, find_set_same] + +theorem read_your_deletion (db : DB M K V) (ws : Writes M K V) (a : Addr M K) + : valueAt db (set ws a none) a = none := by + simp [valueAt, find_set_same] + +theorem absent_read (db : DB M K V) (ws : Writes M K V) (a : Addr M K) + (hw : find ws a = none) (hd : find db a = none) + : valueAt db ws a = none := by + simp [valueAt, hw, hd] + +theorem staged_noninterference (db : DB M K V) (ws : Writes M K V) + (a b : Addr M K) (v : Option V) (h : a ≠ b) + : valueAt db (set ws a v) b = valueAt db ws b := by + simp [valueAt, find_set_other ws a b v h] + +theorem previous_ignores_pending (db : DB M K V) (a : Addr M K) + : previousAt db a = (find db a).map Cell.version := + rfl + +end Generic +end Kv.Proofs.Model + +namespace Kv.Proofs.Model + +open Kv.Model Kv.Proofs.Invariants Kv.Properties + +theorem apply_atomic (s : Store) (writes : Pending) + : (advance s writes).head.data = publish s.head.data (s.head.version + 1) writes := + rfl + +theorem compact_above_head_noop (s : Store) (v : Nat) (h : s.head.version < v) + : compactStore s v = s := by + simp [compactStore, Nat.not_le.mpr h] + +theorem compacted_map_unavailable (s : Store) (f : Frame) (m : String) + (birth : Stamp) (existing : find f.births m = some birth) + (h : (revision f m).version < (revision (atCut s s.global) m).version) + : mapAvailable s f m = false := by + simp [mapAvailable, existing, Nat.not_le.mpr h] + +theorem absent_map_available (s : Store) (f : Frame) (m : String) + (absent : find f.births m = none) (empty : image f.data m = []) + (unwritten : find f.revisions m = none) + : mapAvailable s f m = true := by + simp [mapAvailable, absent, empty, unwritten] + +theorem absent_placeholder_has_no_values (s : Store) (f : Frame) (m key : String) + (absent : find f.births m = none) (permitted : mapAvailable s f m = true) + : find f.data (m, key) = none := by + have empty : image f.data m = [] := by + have checked : image f.data m = [] ∧ find f.revisions m = none := by + simpa [mapAvailable, absent] using permitted + exact checked.1 + exact empty_map_has_no_values f.data m key empty + +theorem rollback_keeps_prefix (s : Store) (v term : Nat) (f : Frame) + (h : f ∈ s.history) (hv : f.version ≤ s.global) + : f ∈ (rollbackStore s v term).history := by + simp only [rollbackStore, List.mem_filter, decide_eq_true_eq] + exact ⟨h, Nat.le_trans hv (Nat.le_max_left _ _)⟩ + +theorem rollback_discards_suffix (s : Store) (v term : Nat) (f : Frame) + (h : v < f.version) (boundary : s.global ≤ v) + : f ∉ (rollbackStore s v term).history := by + have hbound : rollbackCut s v ≤ v := Nat.max_le.mpr ⟨boundary, Nat.min_le_right _ _⟩ + simp [rollbackStore, Nat.not_le.mpr (Nat.lt_of_le_of_lt hbound h)] + +theorem stale_term_cannot_apply (s : Store) (t : Tx) (snap : Snapshot) + (hs : t.snapshot = some snap) (ht : s.term ≠ snap.term) + : canApply s t = false := by + simp [canApply, validLineage, hs, ht] + +private theorem discarded_handle_cannot_apply (s : Store) (t : Tx) (snap : Snapshot) + (hs : t.snapshot = some snap) (m : String) (view : GlobalView) + (hm : (m, view) ∈ t.globalViews) + (gone : ∀ f ∈ s.history, (revision f m == revision view.current m) = false) + : canApply s t = false := by + apply Bool.eq_false_iff.mpr + intro h + have hh : (!t.unavailable = true ∧ validLineage s t = true) ∧ + validates s.head.data t.normal.deps = true := by simpa [canApply] using h + have hp : (s.term == snap.term) = true ∧ + t.globalViews.all (fun (name, view) => mapLineage s view.current name) = true := by + simpa [validLineage, hs] using hh.1.2 + have hall := hp.2 + have hit := List.all_eq_true.mp hall (m, view) hm + obtain ⟨f, hf, he⟩ := List.any_eq_true.mp hit + simp [gone f hf] at he + +private theorem discarded_birth_cannot_apply (s : Store) (t : Tx) (snap : Snapshot) + (hs : t.snapshot = some snap) (m : String) (view : GlobalView) + (hm : (m, view) ∈ t.globalViews) + (gone : ∀ f ∈ s.history, (find f.births m == find view.current.births m) = false) + : canApply s t = false := by + apply Bool.eq_false_iff.mpr + intro h + have hh : (!t.unavailable = true ∧ validLineage s t = true) ∧ + validates s.head.data t.normal.deps = true := by simpa [canApply] using h + have hp : (s.term == snap.term) = true ∧ + t.globalViews.all (fun (name, view) => mapLineage s view.current name) = true := by + simpa [validLineage, hs] using hh.1.2 + have hit := List.all_eq_true.mp hp.2 (m, view) hm + obtain ⟨f, hf, he⟩ := List.any_eq_true.mp hit + simp [gone f hf] at he + +end Kv.Proofs.Model + +namespace Kv.Proofs.Trace + +open Kv.Model Kv.Proofs.Invariants Kv.Properties Kv.Proofs.Model + +private theorem step_event_result (w next : World) (r : Record) + (accepted : step w r = .ok next) + : ∃ eventNext, + stepEvent w r.event = .ok eventNext + ∧ next.stores = eventNext.stores + ∧ next.txs = eventNext.txs := by + obtain ⟨eventNext, event, rfl⟩ := step_ok accepted + exact ⟨eventNext, event, rfl, rfl⟩ + +private theorem stepEvent_capture_metadata (w next : World) + (sid tid version global term : Nat) (s : Store) (t : Tx) + (source : storeOf w sid = .ok s) + (accepted : stepEvent w (.snapshot sid tid version global term) = .ok next) + (capturedTx : find next.txs tid = some t) + : ∃ snap, t.snapshot = some snap ∧ snap.current = s.head ∧ snap.term = term := by + refine ⟨{ current := s.head, term }, ?_, rfl, rfl⟩ + obtain ⟨_, store, accepted⟩ := bind_ok accepted + cases source.symm.trans store + obtain ⟨_, _, -, h, rfl⟩ := withTx_ok accepted + obtain ⟨_, -, h⟩ := bind_ok h + split at h + · obtain ⟨_, -, h⟩ := bind_ok h + cases pure_ok h + simp only [find_set_same, Option.some.injEq] at capturedTx + subst capturedTx + rfl + · cases h + +private theorem step_capture_metadata (w next : World) + (sid tid version global term seq : Nat) (s : Store) (t : Tx) + (source : storeOf w sid = .ok s) + (accepted : step w ⟨seq, .snapshot sid tid version global term⟩ = .ok next) + (capturedTx : find next.txs tid = some t) + : ∃ snap, t.snapshot = some snap ∧ snap.current = s.head ∧ snap.term = term := by + obtain ⟨eventNext, eventStep, _, txs⟩ := step_event_result w next _ accepted + exact stepEvent_capture_metadata w eventNext sid tid version global term s t source + eventStep (by simpa [txs] using capturedTx) + +private theorem stepEvent_capture_cut_values (w next : World) + (sid tid version global term : Nat) (s : Store) (source : storeOf w sid = .ok s) + (accepted : stepEvent w (.snapshot sid tid version global term) = .ok next) + : version = s.head.version ∧ global = s.global := by + obtain ⟨_, store, accepted⟩ := bind_ok accepted + cases source.symm.trans store + obtain ⟨_, _, -, h, -⟩ := withTx_ok accepted + obtain ⟨_, -, h⟩ := bind_ok h + split at h + · obtain ⟨_, metadata, -⟩ := bind_ok h + have metadata := expect_ok metadata + simp only [Bool.and_eq_true, beq_iff_eq] at metadata + exact metadata.1 + · cases h + +theorem captureGlobal_placeholder (s : Store) (snap : Snapshot) (map : String) + (absent : find (captureLocal s snap map).births map = none) + : (captureGlobal s snap map).frame = {} := by + simp [captureGlobal, absent] + +theorem captureGlobal_committed (s : Store) (snap : Snapshot) (map : String) + (birth : Stamp) (existing : find (captureLocal s snap map).births map = some birth) + : (captureGlobal s snap map).frame = atCut s s.global := by + simp [captureGlobal, existing] + +private theorem stepEvent_map_capture (w next : World) + (sid tid localVersion globalVersion : Nat) (map : String) (s : Store) + (before after : Tx) (snap : Snapshot) (store : storeOf w sid = .ok s) + (tx : txOf w sid tid = .ok before) (snapshot : before.snapshot = some snap) + (accepted : stepEvent w (.acquire sid tid map localVersion globalVersion) = .ok next) + (live : find next.txs tid = some after) + : find after.globalViews map = some (captureGlobal s snap map) + ∧ localVersion = (revision (captureLocal s snap map) map).version + ∧ globalVersion = (revision (captureGlobal s snap map).frame map).version := by + have captureGlobal_current (s : Store) (snap : Snapshot) (map : String) + : (captureGlobal s snap map).current = captureLocal s snap map := by + dsimp only [captureGlobal] + split <;> rfl + obtain ⟨_, store', accepted⟩ := bind_ok accepted + cases store.symm.trans store' + obtain ⟨_, _, tx', h, rfl⟩ := withTx_ok accepted + cases tx.symm.trans tx' + obtain ⟨_, captured, -, versions, _, rfl⟩ := acquireMap_ok h + cases snapshot.symm.trans captured + simp only [find_set_same, Option.some.injEq] at live + subst live + rw [captureGlobal_current] at versions + exact ⟨find_set_same _ _ _, versions⟩ + +private theorem step_map_capture (w next : World) + (sid tid localVersion globalVersion seq : Nat) (map : String) (s : Store) + (before after : Tx) (snap : Snapshot) (store : storeOf w sid = .ok s) + (tx : txOf w sid tid = .ok before) (snapshot : before.snapshot = some snap) + (accepted : step w ⟨seq, .acquire sid tid map localVersion globalVersion⟩ = .ok next) + (live : find next.txs tid = some after) + : find after.globalViews map = some (captureGlobal s snap map) + ∧ localVersion = (revision (captureLocal s snap map) map).version + ∧ globalVersion = (revision (captureGlobal s snap map).frame map).version := by + obtain ⟨eventNext, eventStep, _, txs⟩ := step_event_result w next _ accepted + exact stepEvent_map_capture w eventNext sid tid localVersion globalVersion map s before + after snap store tx snapshot eventStep (by simpa [txs] using live) + +theorem step_capture_metadata_claim + : ∀ (w next : World) (sid tid version global term seq : Nat) (s : Store) (t : Tx), + storeOf w sid = .ok s + → Model.transitionSystem.step w ⟨seq, .snapshot sid tid version global term⟩ + = some next + → find next.txs tid = some t + → ∃ snap, t.snapshot = some snap ∧ snap.current = s.head ∧ snap.term = term := by + intro w next sid tid version global term seq s t source accepted capturedTx + exact Proofs.Trace.step_capture_metadata w next sid tid version global term seq s t source ((Proofs.Execution.step_iff_transition _ _ _).mp accepted) capturedTx + +theorem step_capture_cut_values_claim + : ∀ (w next : World) (sid tid version global term seq : Nat) (s : Store), + storeOf w sid = .ok s + → Model.transitionSystem.step w ⟨seq, .snapshot sid tid version global term⟩ + = some next + → version = s.head.version ∧ global = s.global := by + have step_capture_cut_values (w next : World) (sid tid version global term seq : Nat) + (s : Store) (source : storeOf w sid = .ok s) + (accepted : step w ⟨seq, .snapshot sid tid version global term⟩ = .ok next) + : version = s.head.version ∧ global = s.global := by + obtain ⟨eventNext, eventStep, _, _⟩ := step_event_result w next _ accepted + exact stepEvent_capture_cut_values w eventNext sid tid version global term s source eventStep + intro w next sid tid version global term seq s source accepted + exact step_capture_cut_values w next sid tid version global term seq s source + ((Proofs.Execution.step_iff_transition _ _ _).mp accepted) + +theorem step_map_capture_claim + : ∀ (w next : World) (sid tid localVersion globalVersion seq : Nat) (map : String) + (s : Store) (before after : Tx) (snap : Snapshot), + storeOf w sid = .ok s + → txOf w sid tid = .ok before + → before.snapshot = some snap + → Model.transitionSystem.step w + ⟨seq, .acquire sid tid map localVersion globalVersion⟩ + = some next + → find next.txs tid = some after + → find after.globalViews map = some (captureGlobal s snap map) + ∧ localVersion = (revision (captureLocal s snap map) map).version + ∧ globalVersion = (revision (captureGlobal s snap map).frame map).version := by + intro w next sid tid localVersion globalVersion seq map s before after snap store tx snapshot accepted live + exact Proofs.Trace.step_map_capture w next sid tid localVersion globalVersion seq map s before after snap store tx snapshot ((Proofs.Execution.step_iff_transition _ _ _).mp accepted) live + +end Kv.Proofs.Trace + +namespace Kv.Proofs.Properties + +open Kv.Model Kv.Properties + +theorem discarded_handle_cannot_apply + : ∀ (s : Store) (t : Tx) (snap : Snapshot) (m : String) (view : GlobalView), + t.snapshot = some snap + → (m, view) ∈ t.globalViews + → (∀ f ∈ s.history, (revision f m == revision view.current m) = false) + → canApply s t = false := by + intro s t snap m view hs hm gone + exact Proofs.Model.discarded_handle_cannot_apply s t snap hs m view hm gone + +theorem discarded_birth_cannot_apply + : ∀ (s : Store) (t : Tx) (snap : Snapshot) (m : String) (view : GlobalView), + t.snapshot = some snap + → (m, view) ∈ t.globalViews + → (∀ f ∈ s.history, (find f.births m == find view.current.births m) = false) + → canApply s t = false := by + intro s t snap m view hs hm gone + exact Proofs.Model.discarded_birth_cannot_apply s t snap hs m view hm gone + +end Kv.Proofs.Properties + namespace Kv.Proofs.Witnesses open Kv.Model Kv.Properties Kv.Proofs.Invariants @@ -160,16 +695,15 @@ private instance (A F R : Prop) [Decidable A] [rest : Checks F R] : Checks (A private theorem facts : Facts := Checks.sound (by decide +kernel) Facts.mk -private theorem accepted_le {m n : Nat} (le : m ≤ n) (h : accepted n = true) - : accepted m = true := by - induction le with - | refl => exact h - | step _ ih => - simp only [accepted, Bool.and_eq_true] at h - exact ih h.1 - private theorem step_world {n : Nat} (all : accepted 17 = true) (lt : n < 17) : transitionSystem.step (world n) (record n) = some (world (n + 1)) := by + have accepted_le {m n : Nat} (le : m ≤ n) (h : accepted n = true) + : accepted m = true := by + induction le with + | refl => exact h + | step _ ih => + simp only [accepted, Bool.and_eq_true] at h + exact ih h.1 have h := accepted_le lt all simp only [accepted, Bool.and_eq_true] at h simp only [transitionSystem, world] @@ -189,8 +723,11 @@ private theorem run_world {i k : Nat} (all : accepted 17 = true) (le : i + k ≤ induction k generalizing i with | zero => exact .nil _ | succ k ih => - rw [show i + (k + 1) = i + 1 + k by omega] - exact .cons (step_world all (by omega)) (ih (by omega)) + have same : i + (k + 1) = i + 1 + k := + (Nat.add_assoc i k 1).symm.trans (Nat.add_right_comm i k 1) + rw [same] + exact .cons (step_world all (Nat.lt_of_lt_of_le (Nat.lt_add_of_pos_right (Nat.succ_pos k)) le)) + (ih (same ▸ le)) private theorem some_get {α : Type} {o : Option α} (h : o.isSome = true) : o = some (o.get h) := @@ -222,9 +759,6 @@ private theorem txOf_world {n sid tid : Nat} simp [txOf, storeOf_world store, find_tx tx, present, require, owner, bind, Except.bind] rfl -private theorem written_valid : StoreInvariant written := - advance_invariant {} store_initial _ - private def committedCell : DB String String String := [(("a", "00"), ⟨"11", 1⟩)] lemma read_your_write_witness @@ -634,21 +1168,24 @@ lemma rollback_keeps_prefix_witness ⟨ compactStore written 1, _, - List.mem_of_mem_head? (compact_invariant written written_valid 1).headFirst, + List.mem_of_mem_head? (rfl : (compactStore written 1).history.head? = some _), facts.compactedHead, facts.compactedData ⟩ lemma rollback_discards_suffix_witness - : ∃ (s : Store) (v : Nat) (f : Frame), f ∈ s.history ∧ v < f.version ∧ s.global ≤ v := - ⟨ - written, - 0, - _, - List.mem_of_mem_head? written_valid.headFirst, - facts.writtenHead, - facts.writtenGlobal - ⟩ + : ∃ (s : Store) (v : Nat) (f : Frame), + f ∈ s.history ∧ v < f.version ∧ s.global ≤ v := by + have written_valid : StoreInvariant written := + advance_invariant {} store_initial _ + exact ⟨ + written, + 0, + _, + List.mem_of_mem_head? written_valid.headFirst, + facts.writtenHead, + facts.writtenGlobal + ⟩ lemma durable_cut_survives_rollback_witness : ∃ (w : World) (sid : Nat) (s : Store) (v cut : Nat), diff --git a/lean/kv/Kv/Properties.lean b/lean/kv/Kv/Properties.lean index 8e4b38e0af1..065170c7d84 100644 --- a/lean/kv/Kv/Properties.lean +++ b/lean/kv/Kv/Properties.lean @@ -5,7 +5,8 @@ module public import Kv.Properties.Invariants -import Kv.Proofs.Properties +import Kv.Proofs.Reachable +import Kv.Proofs.Replay import Kv.Proofs.Witnesses @[expose] public section @@ -222,7 +223,7 @@ theorem replay_segment_serializability ∧ projectApplications w sid rs = .ok txs ∧ serialTransactions s.head.data s.head.version txs = some after.head.data ∧ after.head.version = s.head.version + txs.length := by - exact Proofs.Properties.replay_segment_serializability + exact Proofs.Trace.replay_segment_serializability_claim /-- Witness: an accepted nonempty segment can keep a store alive. -/ lemma replay_segment_serializability_witness @@ -246,7 +247,7 @@ theorem reachable_store_invariants ∧ s.history.head? = some s.head ∧ s.global ≤ s.head.version ∧ (atCut s s.global).version = s.global := by - exact Proofs.Properties.reachable_store_invariants + exact Proofs.Trace.reachable_store_invariants_claim /-- Witness: a reachable world can have a live store. -/ lemma reachable_store_invariants_witness @@ -261,7 +262,7 @@ theorem reachable_store_data_invariants Model.transitionSystem.Reachable w → find w.stores sid = some s → Unique s.head.data ∧ CellsBounded s.head.data s.head.version := by - exact Proofs.Properties.reachable_store_data_invariants + exact Proofs.Trace.reachable_store_data_invariants_claim /-- Witness: a reachable world can have a live store. -/ lemma reachable_store_data_invariants_witness @@ -279,7 +280,7 @@ theorem step_capture_metadata = some next → find next.txs tid = some t → ∃ snap, t.snapshot = some snap ∧ snap.current = s.head ∧ snap.term = term := by - exact Proofs.Properties.step_capture_metadata + exact Proofs.Trace.step_capture_metadata_claim /-- Witness: a snapshot capture can be accepted. -/ lemma step_capture_metadata_witness @@ -297,7 +298,7 @@ theorem step_capture_cut_values → Model.transitionSystem.step w ⟨seq, .snapshot sid tid version global term⟩ = some next → version = s.head.version ∧ global = s.global := by - exact Proofs.Properties.step_capture_cut_values + exact Proofs.Trace.step_capture_cut_values_claim /-- Witness: a snapshot capture can be accepted. -/ lemma step_capture_cut_values_witness @@ -323,7 +324,7 @@ theorem capture_replay_preserves_metadata ∧ after.snapshot = some snap ∧ snap.current = s.head ∧ snap.term = term := by - exact Proofs.Properties.capture_replay_preserves_metadata + exact Proofs.Trace.capture_replay_preserves_metadata_claim /-- Witness: a snapshot capture can be followed by an accepted nonempty run that keeps the attempt. -/ lemma capture_replay_preserves_metadata_witness @@ -346,7 +347,7 @@ theorem replay_snapshot_fixed → (∀ r ∈ rs, AttemptEvent tid r.event) → CCF.Execution.Run Model.transitionSystem w rs final → ∃ after, find final.txs tid = some after ∧ after.snapshot = some snap := by - exact Proofs.Properties.replay_snapshot_fixed + exact Proofs.Trace.replay_snapshot_fixed_claim /-- Witness: an attempt with a snapshot can be followed by an accepted nonempty run that keeps it. -/ lemma replay_snapshot_fixed_witness @@ -374,7 +375,7 @@ theorem step_map_capture → find after.globalViews map = some (captureGlobal s snap map) ∧ localVersion = (revision (captureLocal s snap map) map).version ∧ globalVersion = (revision (captureGlobal s snap map).frame map).version := by - exact Proofs.Properties.step_map_capture + exact Proofs.Trace.step_map_capture_claim /-- Witness: a map acquisition can be accepted. -/ lemma step_map_capture_witness @@ -399,7 +400,7 @@ theorem replay_map_global_fixed → CCF.Execution.Run Model.transitionSystem w rs final → ∃ after, find final.txs tid = some after ∧ find after.globalViews map = some view := by - exact Proofs.Properties.replay_map_global_fixed + exact Proofs.Trace.replay_map_global_fixed_claim /-- Witness: an attempt with an acquired map can be followed by an accepted nonempty run that keeps it. -/ lemma replay_map_global_fixed_witness @@ -423,7 +424,7 @@ theorem replay_map_local_fixed → ∃ after, find final.txs tid = some after ∧ image after.data map = image before.data map := by - exact Proofs.Properties.replay_map_local_fixed + exact Proofs.Trace.replay_map_local_fixed_claim /-- Witness: an acquired map can survive a nonempty accepted segment. -/ lemma replay_map_local_fixed_witness @@ -457,7 +458,7 @@ theorem capture_replay_preserves_map ∧ localVersion = (revision (captureLocal s snap map) map).version ∧ globalVersion = (revision (captureGlobal s snap map).frame map).version := by - exact Proofs.Properties.capture_replay_preserves_map + exact Proofs.Trace.capture_replay_preserves_map_claim /-- Witness: a map acquisition can be followed by an accepted nonempty run that keeps the attempt. -/ lemma capture_replay_preserves_map_witness @@ -517,7 +518,7 @@ theorem step_global_read_from_captured_map view.frame = atCut origin origin.global ∧ view.frame.version = origin.global ∧ CellsBounded view.frame.data origin.global) := by - exact Proofs.Properties.step_global_read_from_captured_map + exact Proofs.Trace.step_global_read_from_captured_map_claim /-- Witness: a global read of a committed value can be accepted. -/ lemma step_global_read_from_captured_map_witness @@ -545,7 +546,7 @@ theorem step_global_has_from_captured_map view.frame = atCut origin origin.global ∧ view.frame.version = origin.global ∧ CellsBounded view.frame.data origin.global) := by - exact Proofs.Properties.step_global_has_from_captured_map + exact Proofs.Trace.step_global_has_from_captured_map_claim /-- Witness: a global presence test of a committed key can be accepted. -/ lemma step_global_has_from_captured_map_witness diff --git a/lean/kv/README.md b/lean/kv/README.md index 3c8a9bf08fa..0977a08f166 100644 --- a/lean/kv/README.md +++ b/lean/kv/README.md @@ -24,9 +24,10 @@ This profile follows the implementation's **per-map globally committed views**. Human review covers the model, the full theorem statements in `Properties.lean`, the definitions they use, and their one-line references to proof implementations. The proof implementations under `Proofs/` are verified by the build and `lake check` and are marked `linguist-generated` in `.gitattributes`. +The proof modules do not import each other, so Lake checks them in parallel; lemmas needed by more than one module are duplicated as private declarations to minimise verification wall-clock time. `Model.transitionSystem` presents `step` as a [`CCF.TransitionSystem`](../common/CCF/TransitionSystem.lean) from the empty world. -Properties of executions use the shared `CCF.Execution.Run` and `TransitionSystem.Reachable`, and `Proofs/Execution.lean` shows that they coincide with successful `replay`. +Properties of executions use the shared `CCF.Execution.Run` and `TransitionSystem.Reachable`, and the proof modules show that they coincide with successful `replay`. ## Model @@ -54,7 +55,7 @@ The first acquisition of a map selects the newest surviving frame at or below th `Tx.globalViews` stores one `GlobalView` per acquired map: the pinned local frame and the globally committed frame. Once acquired, neither frame changes for the rest of the attempt, and `Tx.data` combines the pinned local data used by normal observations. -The invariants used by the proofs are stated separately, in `Proofs/Invariants.lean`, and proved for every state reachable from the empty world. +The invariants used by the proofs are stated separately, in `Proofs/Reachable.lean`, and proved for every state reachable from the empty world. Store histories start with the empty version-zero frame, contain every descending version through the current head, and each successor frame results from publishing a finite write set over its predecessor; the head is the first history frame and the global cut never exceeds it. Each live attempt's operation log, replayed against its pinned data, reproduces its normal view. Each snapshot comes from a store head, and each global view is either an empty placeholder or a store's frame at its global cut. @@ -65,7 +66,7 @@ The normal-view reconstruction function `normalRun` and the per-step head-effect `Kv/Properties.lean` states each claim as a proved theorem in `Kv.Properties`, whose one-line proof refers to an implementation in `Kv/Proofs/`. No `sorry`, custom axioms, unsafe declarations, or external solver are used; `lake check` accepts only Lean's standard `propext`, `Quot.sound` and `Classical.choice`. -Claims that depend on the model's state invariants assume `Model.transitionSystem.Reachable`; `Proofs/Invariants.lean` proves those invariants hold initially and are preserved by every step. +Claims that depend on the model's state invariants assume `Model.transitionSystem.Reachable`; `Proofs/Reachable.lean` proves those invariants hold initially and are preserved by every step. Each claim is followed by a `_witness` lemma, so no claim is vacuous. For a claim with premises, the witness asserts that some concrete state, trace or program satisfies them.