refactor(Algorithms/WordRAM/Karger): derive contraction survival from Karger.spec through a simulation lemma

Complexity.lean

@@ -1372,6 +1372,7 @@ public import Complexity.Computability.Complexity.Classes.Promise.Probabilistic
 public import Complexity.Computability.Complexity.Classes.Promise.Randomized
 public import Complexity.Computability.Complexity.Classes.Promise.Reduction
 public import Complexity.Computability.Complexity.Classes.Promise.Time
+public import Complexity.Computability.Complexity.Classes.Promise.Time.Verifier
 public import Complexity.Computability.Complexity.Classes.RP
 public import Complexity.Computability.Complexity.Classes.RP.Closure
 public import Complexity.Computability.Complexity.Classes.RepeatedTrials
@@ -1434,6 +1435,7 @@ public import Complexity.Computability.Complexity.Classes.Time
 public import Complexity.Computability.Complexity.Classes.Time.AcceptCount
 public import Complexity.Computability.Complexity.Classes.Time.BoundedExists
 public import Complexity.Computability.Complexity.Classes.Time.Polynomial
+public import Complexity.Computability.Complexity.Classes.Time.SampleVerify
 public import Complexity.Computability.Complexity.Classes.Time.Verifier
 public import Complexity.Computability.Complexity.Classes.Time.WordRAM
 public import Complexity.Computability.Complexity.Classes.TimeSpace.Williams
@@ -2951,6 +2953,7 @@ public import Complexity.DataStructure.HashFamily.WordRAM.DoubleTabulation
 public import Complexity.DataStructure.HashFamily.WordRAM.KWise
 public import Complexity.DataStructure.HashFamily.WordRAM.MultiplyShift
 public import Complexity.DataStructure.HashFamily.WordRAM.Tabulation
+public import Complexity.DataStructure.Memory.Alloc
 public import Complexity.DataStructure.Memory.Field
 public import Complexity.DataStructure.Memory.Frame
 public import Complexity.DataStructure.Memory.Record
@@ -2971,6 +2974,7 @@ public import Complexity.DataStructure.PrefixSums.WordRAM.Update
 public import Complexity.DataStructure.PriorityQueue.BinaryHeap.Memory
 public import Complexity.DataStructure.PriorityQueue.BinaryHeap.Order
 public import Complexity.DataStructure.PriorityQueue.FibonacciHeap.Basic
+public import Complexity.DataStructure.PriorityQueue.FibonacciHeap.DecreaseKey
 public import Complexity.DataStructure.PriorityQueue.Spec
 public import Complexity.DataStructure.PriorityQueue.WordRAM.Basic
 public import Complexity.DataStructure.PriorityQueue.WordRAM.BinaryHeap
@@ -3040,6 +3044,7 @@ public import Complexity.Foundations.Algebra.Shear
 public import Complexity.Foundations.Analysis.Asymptotics.CostBound
 public import Complexity.Foundations.Analysis.Asymptotics.Exponential
 public import Complexity.Foundations.Analysis.BernoulliInequality
+public import Complexity.Foundations.Analysis.ENNRealFraction
 public import Complexity.Foundations.Analysis.ENNRealTsum
 public import Complexity.Foundations.Analysis.Fourier.ZModProd
 public import Complexity.Foundations.Analysis.HarmonicMean

Complexity/Algorithms/Lean/Dijkstra/Memory.lean

@@ -176,12 +176,14 @@ theorem holds_inputGraph (G : ListInstance) :
 /-- **The structures after allocation.** Past the input of `G`, a distance table and then a heap,
 allocated without clearing, together with the adjacency arrays of the input, represent the
 initial state of Dijkstra's algorithm on `G`: an empty queue, an empty distance map and the
-graph. -/
+graph. The structures share memory only while its frontier fits a word (`Memory.Framed.Apart`). -/
 theorem inv_input (G : ListInstance) {w K V : ℕ}
     (hH : (BinaryHeap.Memory.allocated G.n ((Memory.State.init G.encode).frontier + G.n)).Valid
       w K)
     (hT : Dictionary.Memory.Valid ⟨(Memory.State.init G.encode).frontier, G.n⟩ w G.n V)
-    (hA : (inputGraph G.n G.m).Valid G.n) :
+    (hA : (inputGraph G.n G.m).Valid G.n)
+    (hfit : Fits w ((Memory.State.init G.encode).frontier + G.n + 1 +
+      PriorityQueue.WordRAM.BinaryHeap.space G.n)) :
     (framed hH hT hA G.adj).inv ⟨(Memory.State.init G.encode).mem,
         (Memory.State.init G.encode).frontier + G.n + 1 +
           PriorityQueue.WordRAM.BinaryHeap.space G.n⟩ ∧
@@ -202,13 +204,15 @@ theorem inv_input (G : ListInstance) {w K V : ℕ}
     ⟨by simp only [inputGraph, Block.Allocated]; omega,
       by simp only [inputGraph, Block.Allocated]; omega, holds_inputGraph G⟩, ?_⟩, ?_⟩,
     Prod.ext hHabs (Prod.ext hTabs rfl)⟩
-  · simp only [Dictionary.Memory.framed_footprint, AdjacencyList.Memory.framed_footprint]
+  · refine ⟨?_, hfit⟩
+    simp only [Dictionary.Memory.framed_footprint, AdjacencyList.Memory.framed_footprint]
     rw [Finset.disjoint_left]
     intro a ha hb
     simp only [Block.mem_footprint, Block.Owns, AdjacencyList.Memory.Layout.footprint,
       inputGraph, Finset.mem_union] at ha hb
     omega
-  · simp only [Memory.Framed.prod_footprint, BinaryHeap.Memory.framed_footprint,
+  · refine ⟨?_, hfit⟩
+    simp only [Memory.Framed.prod_footprint, BinaryHeap.Memory.framed_footprint,
       Dictionary.Memory.framed_footprint, AdjacencyList.Memory.framed_footprint]
     rw [Finset.disjoint_left]
     intro a ha hb
@@ -300,6 +304,7 @@ theorem run_triple (G : ListInstance) {w : ℕ}
   have hA : (inputGraph G.n G.m).Valid G.n := ⟨rfl⟩
   set M := framed hH hT hA G.adj with hM
   obtain ⟨hinv, habs⟩ := inv_input G hH hT hA
+    (hfit.of_le (by simp only [PriorityQueue.WordRAM.BinaryHeap.space]; nlinarith))
   obtain ⟨hvalid, hdist⟩ := dijkstra_correct (K := K) (V := K + 1) G le_rfl (by omega)
   rw [← habs] at hvalid hdist
   obtain ⟨hvE, -, hstate, -⟩ := M.simulates_client (dijkstra G.source) hinv hvalid

Complexity/Algorithms/Lean/Karger/Contraction.lean

@@ -41,11 +41,12 @@ less than it (`minCut_le_of_mem_support_karger`). Every call it makes is admissi
 `telescope_survival_step`), used unchanged, and the composition of the stages is
 `Probability.PMF.toOuterMeasure_bind_ge_mul_ennreal`.
 
-The word-RAM implementation proves the same bound on machine states, interleaved with register
-steps (`Cslib.Algorithms.WordRAM.Karger.contractDownTo_spec`). Here no register, address or
-instruction count appears. An implementation of `spec` over the memory oracle is a separate,
-deterministic hop, and `Refinement.toRandomized` with `RandomizedRefinement.withCoins` carries the
-law of the client through it.
+No register, address or instruction count appears here. The word-RAM loop
+`Cslib.Algorithms.WordRAM.Karger.contractDownTo` simulates `contractTimes`: the graph it holds has
+the law of the client's final state (`Cslib.Algorithms.WordRAM.Karger.contractDownTo_law`), so its
+survival bound is `survives_contractTimes`. An implementation of `spec` over the memory oracle is a
+separate, deterministic hop, and `Refinement.toRandomized` with `RandomizedRefinement.withCoins`
+carries the law of the client through it.
 
 ## Main definitions
 
@@ -56,6 +57,8 @@ law of the client through it.
 
 ## Main results
 
+* `run_contractStep_bind`, `run_contractStep_bind_of_eq_zero`: the run of one contraction, the
+  step that an implementation simulates.
 * `survives_contractTimes`: the survival bound.
 * `two_div_le_toOuterMeasure_karger`: Karger's success probability.
 * `isContractionOf_of_mem_support_contractTimes`, `minCut_le_of_mem_support_karger`: every
@@ -181,7 +184,7 @@ noncomputable def karger : ProbOracleComp Op.Result ℕ := do
 
 /-- One contraction of a graph of positive weight draws a uniform offset below the weight and
 contracts the pair sampled there. -/
-private theorem run_contractStep_bind {α : Type} (p : ProbOracleComp Op.Result α) {m : ℕ}
+theorem run_contractStep_bind {α : Type} (p : ProbOracleComp Op.Result α) {m : ℕ}
     (W : Fin (m + 1) → Fin (m + 1) → ℕ) (hS : totalDoubledWeight W ≠ 0) :
     spec.toRandomized.withCoins.run (contractStep >>= fun _ => p) ⟨m + 1, W⟩ =
       (ProbComp.unifOracle (totalDoubledWeight W - 1)).bind fun r =>
@@ -197,7 +200,7 @@ private theorem run_contractStep_bind {α : Type} (p : ProbOracleComp Op.Result
   rfl
 
 /-- One contraction of a weightless graph contracts its first and last supervertices. -/
-private theorem run_contractStep_bind_of_eq_zero {α : Type} (p : ProbOracleComp Op.Result α)
+theorem run_contractStep_bind_of_eq_zero {α : Type} (p : ProbOracleComp Op.Result α)
     {m : ℕ} (W : Fin (m + 1) → Fin (m + 1) → ℕ) (hS : totalDoubledWeight W = 0) :
     spec.toRandomized.withCoins.run (contractStep >>= fun _ => p) ⟨m + 1, W⟩ =
       spec.toRandomized.withCoins.run p ⟨m, contractMatrix W 0 (Fin.last m)⟩ := by