Workspace-relocatable randomized contraction on the word RAM

Implements Karger's edge-weight-proportional contraction loop (contractDownTo) and its companion row-degree initializer (computeDegreesAndTotal) as structured Cslib.WordRAM programs over Basis.standard with 16 registers.

All memory accesses are parameterized dynamically by register-held workspace pointers (wBase, dBase, stride, activeK, targetT, totS), with zero hardcoded memory addresses and a Modifies frame confined to Finset.Ico wBase (wBase + stride * k) ∪ Finset.Ico dBase (dBase + k). This allows both repeated-trial amplification (KargerMinCut) and recursive stack-allocated calls in Karger–Stein (FastCut) to invoke contractDownTo directly at arbitrary memory offsets.

Each contraction from m + 1 down to m active supervertices runs in O(m) worst-case instructions and issues at most 1 rand call (0 calls when total active weight totS = 0), yielding 36 * (k ^ 2 - t ^ 2) + 4 worst-case instructions and at most k - t rand calls from k down to t, with survival probability at least (t * (t - 1)) / (k * (k - 1)) for any fixed minimum cut of a connected multigraph.

Source statements and notation mapping

• Matrix contraction and survival bound (paraphrase):
  • [KargerStein1996], Section 2, Lemma 2.1, Theorem 2.2, and Corollary 2.3, and Section 2.1, Corollary 2.4 (paraphrase): contracting an n-vertex weighted multigraph from k down to t supervertices via edge-weight-proportional selection preserves any fixed minimum cut with probability at least C(t, 2) / C(k, 2) = t * (t - 1) / (k * (k - 1)) ([Karger1993], Section 2, Theorem 2.1 and [MitzenmacherUpfal2017], Section 1.5, Theorem 1.8 give the t = 2 case 2 / (n * (n - 1))).
  • [KargerStein1996], Section 3 ("Implementing the Contraction Algorithm"), Section 3.1, Lemma 3.1 and Section 3.2, Corollary 3.2 (paraphrase): maintaining an n × n weighted adjacency matrix W and row-degree array D[u] = ∑ v, W[u, v] selects each edge (u, v) with probability 2 * W[u, v] / ∑ w, D[w] and executes the Contraction Algorithm in O(n ^ 2) total time (O(n) per contraction step in [KargerStein1996], Section 3.2).
• Notation mapping and implementation variants:
  • C(t, 2) / C(k, 2) ↔ ((t * (t - 1) : ℕ) : ℝ≥0∞) / (k * (k - 1)) in contractDownTo_spec and contractDownToAt_spec;
  • whereas [KargerStein1996], Section 3.1 draws twice (u proportional to D[u] then v proportional to W[u, v] via two Random-Select calls), our contractDownTo uses an equivalent single-draw variant: one unit-cost word-RAM rand instruction drawing uniformly from {0, …, totS - 1} (totS = totalDoubledWeight W), resolved through linear prefix-sum scans uScan over D[0..k) and vScan over W[u, 0..k) to select each unordered pair {u, v} with the same probability 2 * W[u, v] / totS of Lemma 3.1;
  • whereas [KargerStein1996], Section 3.2 updates rows and columns in O(n) per contraction by zeroing the removed vertex in place, our contractDownTo swap-compacts active slot k - 1 into v so each contraction step on k active supervertices runs in O(k) instructions.

Main definitions

• Cslib.Algorithms.WordRAM.Karger.HoldsMatrix, Cslib.Algorithms.WordRAM.Karger.HoldsWorkspace, Cslib.Algorithms.WordRAM.Karger.workspaceFootprint, Cslib.Algorithms.WordRAM.Karger.ContractState: relocatable memory layout and word-bound invariants for an active k × k supervertex adjacency matrix with row stride stride and row degree array at dBase.
• Cslib.Algorithms.WordRAM.Karger.computeDegreesAndTotal, Cslib.Algorithms.WordRAM.Karger.computeDegreesAndTotalAt: deterministic O(k ^ 2) initializer populating D[0..k) and totS.
• Cslib.Algorithms.WordRAM.Karger.contractDownTo, Cslib.Algorithms.WordRAM.Karger.contractDownToAt: randomized contraction loop from activeK down to targetT.

Main results

• Cslib.Algorithms.WordRAM.Karger.computeDegreesAndTotal_exec: computeDegreesAndTotal populates HoldsWorkspace and totS = totalDoubledWeight W within 6 * k ^ 2 + 12 * k + 6 instructions, modifying only Finset.Ico dBase (dBase + k).
• Cslib.Algorithms.WordRAM.Karger.contractDownTo_spec: joint certificate of ExecRand, IsQueryBounded (k - t), worst-case step bound 36 * (k ^ 2 - t ^ 2) + 4, Modifies frame, contraction invariant IsContractionOf, and telescoping cut-survival probability lower bound ((t * (t - 1) : ℕ) : ℝ≥0∞) / (k * (k - 1)).

References

• D. R. Karger, Global Min-cuts in RNC, and Other Ramifications of a Simple Min-Cut Algorithm
• D. R. Karger and C. Stein, A New Approach to the Minimum Cut Problem

Register layout (r = 16)

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.Reg.zero : Fin 16

Constant 0.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.Reg.one : Fin 16

Constant 1.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.Reg.wBase : Fin 16

Base address of active adjacency matrix W.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.Reg.dBase : Fin 16

Base address of active row-degree array D.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.Reg.stride : Fin 16

Row stride (≥ activeK) of the matrix buffer at wBase.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.Reg.activeK : Fin 16

Current number k of active supervertices.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.Reg.targetT : Fin 16

Target number t of active supervertices (2 ≤ t ≤ k).

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.Reg.totS : Fin 16

Current doubled total weight S = totalDoubledWeight W.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.Reg.uReg : Fin 16

Sampled / outer row index u.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.Reg.vReg : Fin 16

Sampled / inner column index v.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.Reg.idx : Fin 16

Loop index for merge and compaction sweeps.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.Reg.rem : Fin 16

Sample remainder / scratch address register.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.Reg.addr1 : Fin 16

Scratch pointer 1.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.Reg.addr2 : Fin 16

Scratch pointer 2.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.Reg.val1 : Fin 16

Scratch value 1.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.Karger.Reg.val2 : Fin 16

Scratch value 2.

Relocatable workspace representation and address geometry

def Cslib.Algorithms.WordRAM.Karger.HoldsMatrix (mem : ℕ → ℕ) (wb str : ℕ) {k : ℕ} (W : Fin k → Fin k → ℕ) : Prop

Memory mem stores W : Fin k → Fin k → ℕ at base address wb with row stride str.

def Cslib.Algorithms.WordRAM.Karger.HoldsWorkspace (mem : ℕ → ℕ) (wb db str : ℕ) {k : ℕ} (W : Fin k → Fin k → ℕ) : Prop

Memory mem stores W : Fin k → Fin k → ℕ at (wb, str) and its row degrees rowDeg W at db.

def Cslib.Algorithms.WordRAM.Karger.workspaceFootprint (wb db str k : ℕ) : Finset ℕ

Permitted memory write footprint of an active k-supervertex workspace at (wb, db, str).

structure Cslib.Algorithms.WordRAM.Karger.ContractState (w wb db str k t : ℕ) (W : Fin k → Fin k → ℕ) (x : WordRAM.Data 16) : Prop

Machine-state precondition for contractDownTo on k active supervertices targeting t.

• regs_wBase : x.regs Reg.wBase = wb
• regs_dBase : x.regs Reg.dBase = db
• regs_stride : x.regs Reg.stride = str
• regs_activeK : x.regs Reg.activeK = k
• regs_targetT : x.regs Reg.targetT = t
• regs_totS : x.regs Reg.totS = totalDoubledWeight W
• le_stride : k ≤ str
• disjoint_blocks : wb + str * k ≤ db ∨ db + k ≤ wb
• fits_wEnd : WordRAM.Fits w (wb + str * k)
• fits_dEnd : WordRAM.Fits w (db + k)
• fits_totS : WordRAM.Fits w (totalDoubledWeight W)
• workspace : HoldsWorkspace x.mem wb db str W

theorem Cslib.Algorithms.WordRAM.Karger.matAddr_lt_end {wb str k : ℕ} (hstr : k ≤ str) (i j : Fin k) : wb + ↑i * str + ↑j < wb + str * k

theorem Cslib.Algorithms.WordRAM.Karger.matAddr_mem_Ico {wb str k : ℕ} (hstr : k ≤ str) (i j : Fin k) : wb + ↑i * str + ↑j ∈ Finset.Ico wb (wb + str * k)

theorem Cslib.Algorithms.WordRAM.Karger.degAddr_mem_Ico {db k : ℕ} (i : Fin k) : db + ↑i ∈ Finset.Ico db (db + k)

theorem Cslib.Algorithms.WordRAM.Karger.matAddr_inj {wb str k : ℕ} (hstr : k ≤ str) {i₁ j₁ i₂ j₂ : Fin k} (h : wb + ↑i₁ * str + ↑j₁ = wb + ↑i₂ * str + ↑j₂) : i₁ = i₂ ∧ j₁ = j₂

theorem Cslib.Algorithms.WordRAM.Karger.matAddr_ne_degAddr {wb db str k : ℕ} (hstr : k ≤ str) (hdisj : wb + str * k ≤ db ∨ db + k ≤ wb) (i j l : Fin k) : wb + ↑i * str + ↑j ≠ db + ↑l

theorem Cslib.Algorithms.WordRAM.Karger.workspaceFootprint_mono {wb db str k₁ k₂ : ℕ} (hle : k₁ ≤ k₂) : workspaceFootprint wb db str k₁ ⊆ workspaceFootprint wb db str k₂

theorem Cslib.Algorithms.WordRAM.Karger.modifies_trans_subset {F F₁ F₂ : Finset ℕ} {m₀ m₁ m₂ : ℕ → ℕ} (h₁ : WordRAM.Modifies F₁ m₀ m₁) (h₂ : WordRAM.Modifies F₂ m₁ m₂) (hs₁ : F₁ ⊆ F) (hs₂ : F₂ ⊆ F) : WordRAM.Modifies F m₀ m₂

theorem Cslib.Algorithms.WordRAM.Karger.modifies_update_of_mem {F : Finset ℕ} {a : ℕ} (ha : a ∈ F) (m : ℕ → ℕ) (v : ℕ) : WordRAM.Modifies F m (Function.update m a v)

Prefix-sum step identities for degBefore and weightBefore

Part 1: Deterministic O(k ^ 2) row-degree and total-weight initializer

def Cslib.Algorithms.WordRAM.Karger.degInnerBody : WordRAM.Code WordRAM.Basis.standard 16

Inner loop body accumulating W[u, v] into val1.

def Cslib.Algorithms.WordRAM.Karger.degOuterBody : WordRAM.Code WordRAM.Basis.standard 16

Outer loop body computing D[u] = rowDeg W u and adding it to totS.

def Cslib.Algorithms.WordRAM.Karger.computeDegreesAndTotal : WordRAM.Code WordRAM.Basis.standard 16

Compute all row degrees D[0..k) at dBase and totS = totalDoubledWeight W from W at (wBase, stride) in 6 * k ^ 2 + 12 * k + 6 instructions.

theorem Cslib.Algorithms.WordRAM.Karger.computeDegreesAndTotal_exec {w wb db str k : ℕ} {W : Fin k → Fin k → ℕ} {x : WordRAM.Data 16} (hwBase : x.regs Reg.wBase = wb) (hdBase : x.regs Reg.dBase = db) (hstride : x.regs Reg.stride = str) (hactiveK : x.regs Reg.activeK = k) (hstr : k ≤ str) (hdisj : wb + str * k ≤ db ∨ db + k ≤ wb) (h1 : WordRAM.Fits w 1) (hwEnd : WordRAM.Fits w (wb + str * k)) (hdEnd : WordRAM.Fits w (db + k)) (htot : WordRAM.Fits w (totalDoubledWeight W)) (hmat : HoldsMatrix x.mem wb str W) : ∃ (y : WordRAM.Data 16), WordRAM.ExecWithin w computeDegreesAndTotal x y (6 * k ^ 2 + 12 * k + 6) ∧ HoldsWorkspace y.mem wb db str W ∧ WordRAM.Modifies (Finset.Ico db (db + k)) x.mem y.mem ∧ y.regs Reg.zero = 0 ∧ y.regs Reg.one = 1 ∧ y.regs Reg.wBase = wb ∧ y.regs Reg.dBase = db ∧ y.regs Reg.stride = str ∧ y.regs Reg.activeK = k ∧ y.regs Reg.targetT = x.regs Reg.targetT ∧ y.regs Reg.totS = totalDoubledWeight W

computeDegreesAndTotal initializes D[0..k) and totS in 6 * k ^ 2 + 12 * k + 6 instructions while modifying only Finset.Ico db (db + k).

Part 2: Single contraction step and contractDownTo

def Cslib.Algorithms.WordRAM.Karger.uScanBody : WordRAM.Code WordRAM.Basis.standard 16

Loop body for scanning row degrees D[u] until rem ≤ D[u].

def Cslib.Algorithms.WordRAM.Karger.uScan : WordRAM.Code WordRAM.Basis.standard 16

Scan u = 0, 1, … from rem = r + 1 to locate the sampled row u and row offset.

def Cslib.Algorithms.WordRAM.Karger.vScanBody : WordRAM.Code WordRAM.Basis.standard 16

Loop body for scanning row W[u, v] until rem ≤ W[u, v].

def Cslib.Algorithms.WordRAM.Karger.vScan : WordRAM.Code WordRAM.Basis.standard 16

Scan v = 0, 1, … along row u to locate the sampled column v (u ≠ v) with val1 = W u v.

def Cslib.Algorithms.WordRAM.Karger.phaseADegrees : WordRAM.Code WordRAM.Basis.standard 16

Update totS, zero W[u, v], and update D[u] and D[v] for merging v into u.

def Cslib.Algorithms.WordRAM.Karger.phaseAPtrs : WordRAM.Code WordRAM.Basis.standard 16

Set addr1 = wBase + u * stride, addr2 = wBase + v * stride, zero W[v, u], and set idx = 0.

def Cslib.Algorithms.WordRAM.Karger.mergeUpdate : WordRAM.Code WordRAM.Basis.standard 16

Redirect edges between v and idx (idx ∉ {u, v}) into u and zero v's entries.

def Cslib.Algorithms.WordRAM.Karger.mergeBody : WordRAM.Code WordRAM.Basis.standard 16

Single iteration of the Phase A merge sweep over idx < activeK.

def Cslib.Algorithms.WordRAM.Karger.compactUpdate : WordRAM.Code WordRAM.Basis.standard 16

Copy (activeK, idx) and (idx, activeK) into (vReg, idx) and (idx, vReg) for idx ≠ v.

def Cslib.Algorithms.WordRAM.Karger.compactBody : WordRAM.Code WordRAM.Basis.standard 16

Single iteration of the Phase B swap-compaction sweep over idx < m.

def Cslib.Algorithms.WordRAM.Karger.compactSetup : WordRAM.Code WordRAM.Basis.standard 16

Setup for Phase B when v < m: copy D[m] to D[v] and compute row pointers for m and v.

def Cslib.Algorithms.WordRAM.Karger.postRandStep : WordRAM.Code WordRAM.Basis.standard 16

Deterministic continuation of a positive-weight contraction step once rem holds r < totS.

def Cslib.Algorithms.WordRAM.Karger.contractStep : WordRAM.Code WordRAM.Basis.standard 16

One supervertex contraction step: deterministic merge when totS = 0, and edge-proportional random contraction otherwise.

def Cslib.Algorithms.WordRAM.Karger.contractDownTo : WordRAM.Code WordRAM.Basis.standard 16

Workspace-relocatable randomized contraction loop from activeK down to targetT.

Intermediate matrix invariants for mergeLoop and compactLoop

Deterministic execution of uScan, vScan, and postRandStep

theorem Cslib.Algorithms.WordRAM.Karger.uScan_exec {w wb db str k r_val : ℕ} {W : Fin k → Fin k → ℕ} {u v : Fin k} {x : WordRAM.Data 16} (hsamp : IsSampledPair W r_val u v) (h0 : x.regs Reg.zero = 0) (h1 : x.regs Reg.one = 1) (hwBase : x.regs Reg.wBase = wb) (hdBase : x.regs Reg.dBase = db) (hstride : x.regs Reg.stride = str) (hactiveK : x.regs Reg.activeK = k) (htotS : x.regs Reg.totS = totalDoubledWeight W) (hrem : x.regs Reg.rem = r_val) (hdEnd : WordRAM.Fits w (db + k)) (htot : WordRAM.Fits w (totalDoubledWeight W)) (hdeg : ∀ (i : Fin k), x.mem (db + ↑i) = rowDeg W i) : ∃ (y : WordRAM.Data 16), WordRAM.ExecWithin w uScan x y (6 * k) ∧ y.mem = x.mem ∧ y.regs Reg.zero = 0 ∧ y.regs Reg.one = 1 ∧ y.regs Reg.wBase = wb ∧ y.regs Reg.dBase = db ∧ y.regs Reg.stride = str ∧ y.regs Reg.activeK = k ∧ y.regs Reg.targetT = x.regs Reg.targetT ∧ y.regs Reg.totS = totalDoubledWeight W ∧ y.regs Reg.uReg = ↑u ∧ y.regs Reg.rem = r_val + 1 - degBefore W u

Deterministic execution of uScan locating row u for a sampled offset r_val.

theorem Cslib.Algorithms.WordRAM.Karger.vScan_exec {w wb db str k r_val : ℕ} {W : Fin k → Fin k → ℕ} {u v : Fin k} {x : WordRAM.Data 16} (hsamp : IsSampledPair W r_val u v) (h0 : x.regs Reg.zero = 0) (h1 : x.regs Reg.one = 1) (hwBase : x.regs Reg.wBase = wb) (hdBase : x.regs Reg.dBase = db) (hstride : x.regs Reg.stride = str) (hactiveK : x.regs Reg.activeK = k) (htotS : x.regs Reg.totS = totalDoubledWeight W) (huReg : x.regs Reg.uReg = ↑u) (hrem : x.regs Reg.rem = r_val + 1 - degBefore W u) (hstr : k ≤ str) (hwEnd : WordRAM.Fits w (wb + str * k)) (hdEnd : WordRAM.Fits w (db + k)) (htot : WordRAM.Fits w (totalDoubledWeight W)) (hmat : HoldsMatrix x.mem wb str W) : ∃ (y : WordRAM.Data 16), WordRAM.ExecWithin w vScan x y (6 * k + 1) ∧ y.mem = x.mem ∧ y.regs Reg.zero = 0 ∧ y.regs Reg.one = 1 ∧ y.regs Reg.wBase = wb ∧ y.regs Reg.dBase = db ∧ y.regs Reg.stride = str ∧ y.regs Reg.activeK = k ∧ y.regs Reg.targetT = x.regs Reg.targetT ∧ y.regs Reg.totS = totalDoubledWeight W ∧ y.regs Reg.uReg = ↑u ∧ y.regs Reg.vReg = ↑v ∧ y.regs Reg.addr2 = wb + ↑u * str + ↑v ∧ y.regs Reg.val1 = W u v

Deterministic execution of vScan locating column v along row u.

Execution of phaseADegrees, phaseAPtrs, and mergeLoop

theorem Cslib.Algorithms.WordRAM.Karger.phaseADegrees_exec {w wb db str m : ℕ} {W : Fin (m + 1) → Fin (m + 1) → ℕ} {u v : Fin (m + 1)} {x : WordRAM.Data 16} (hW : IsMultigraph W) (huv : u ≠ v) (h0 : x.regs Reg.zero = 0) (h1 : x.regs Reg.one = 1) (hwBase : x.regs Reg.wBase = wb) (hdBase : x.regs Reg.dBase = db) (hstride : x.regs Reg.stride = str) (hactiveK : x.regs Reg.activeK = m + 1) (htotS : x.regs Reg.totS = totalDoubledWeight W) (huReg : x.regs Reg.uReg = ↑u) (hvReg : x.regs Reg.vReg = ↑v) (ha2 : x.regs Reg.addr2 = wb + ↑u * str + ↑v) (hv1 : x.regs Reg.val1 = W u v) (hstr : m + 1 ≤ str) (hdisj : wb + str * (m + 1) ≤ db ∨ db + (m + 1) ≤ wb) (hdEnd : WordRAM.Fits w (db + (m + 1))) (htot : WordRAM.Fits w (totalDoubledWeight W)) (hws : HoldsWorkspace x.mem wb db str W) : ∃ (y : WordRAM.Data 16), WordRAM.ExecWithin w phaseADegrees x y 12 ∧ WordRAM.Modifies (workspaceFootprint wb db str (m + 1)) x.mem y.mem ∧ (∀ (i : Fin (m + 1)), y.mem (db + ↑i) = rowDeg (mergePair W u v) i) ∧ (∀ (i j : Fin (m + 1)), y.mem (wb + ↑i * str + ↑j) = if i = u ∧ j = v then 0 else W i j) ∧ y.regs Reg.zero = 0 ∧ y.regs Reg.one = 1 ∧ y.regs Reg.wBase = wb ∧ y.regs Reg.dBase = db ∧ y.regs Reg.stride = str ∧ y.regs Reg.activeK = m + 1 ∧ y.regs Reg.targetT = x.regs Reg.targetT ∧ y.regs Reg.totS = totalDoubledWeight (contractMatrix W u v) ∧ y.regs Reg.uReg = ↑u ∧ y.regs Reg.vReg = ↑v

Deterministic execution of phaseADegrees updating totS, W[u, v], D[u], and D[v].

Execution of Phase B (compactSetup + compactLoop) and postRandStep

theorem Cslib.Algorithms.WordRAM.Karger.postRandStep_exec {w wb db str m t r_val : ℕ} {W : Fin (m + 1) → Fin (m + 1) → ℕ} {u v : Fin (m + 1)} {x : WordRAM.Data 16} (hm : 2 ≤ m) (hW : IsMultigraph W) (hsamp : IsSampledPair W r_val u v) (h0 : x.regs Reg.zero = 0) (h1 : x.regs Reg.one = 1) (hwBase : x.regs Reg.wBase = wb) (hdBase : x.regs Reg.dBase = db) (hstride : x.regs Reg.stride = str) (hactiveK : x.regs Reg.activeK = m + 1) (htargetT : x.regs Reg.targetT = t) (htotS : x.regs Reg.totS = totalDoubledWeight W) (hrem : x.regs Reg.rem = r_val) (hstr : m + 1 ≤ str) (hdisj : wb + str * (m + 1) ≤ db ∨ db + (m + 1) ≤ wb) (hwEnd : WordRAM.Fits w (wb + str * (m + 1))) (hdEnd : WordRAM.Fits w (db + (m + 1))) (htot : WordRAM.Fits w (totalDoubledWeight W)) (hws : HoldsWorkspace x.mem wb db str W) : ∃ (y : WordRAM.Data 16), WordRAM.ExecWithin w postRandStep x y (45 * (m + 1) + 22) ∧ WordRAM.Modifies (workspaceFootprint wb db str (m + 1)) x.mem y.mem ∧ ContractState w wb db str m t (contractMatrix W u v) y ∧ y.regs Reg.zero = 0 ∧ y.regs Reg.one = 1

Deterministic post-sampling execution: given x.regs rem = r_val with IsSampledPair W r_val u v, postRandStep contracts (u, v) and swap-compacts Fin.last m into slot v within 45 * (m + 1) + 22 instructions.

PMF.toOuterMeasure helpers for step-count maps and contractDownTo_spec

def Cslib.Algorithms.WordRAM.Karger.SurvivalPost {n : ℕ} (W₀ : Fin n → Fin n → ℕ) (wb db str t : ℕ) (C_star : Finset (Fin n)) (y : WordRAM.Data 16) : Prop

Target survival predicate on final Data 16: memory holds a contracted t-supervertex multigraph W' along part' where some active cut B' pulls back to C_star.

theorem Cslib.Algorithms.WordRAM.Karger.contractDownTo_spec {n w wb db str k t : ℕ} {W₀ : Fin n → Fin n → ℕ} {W : Fin k → Fin k → ℕ} {part : Fin n → Fin k} {x : WordRAM.Data 16} (ht : 2 ≤ t) (htk : t ≤ k) (hC : IsContractionOf W₀ part W) (hst : ContractState w wb db str k t W x) : ∃ (m : ProbComp (WordRAM.Data 16 × ℕ)), WordRAM.ExecRand w contractDownTo x m ∧ OracleComp.IsQueryBounded m (k - t) ∧ (∀ z ∈ OracleComp.support m, z.2 ≤ 36 * (k ^ 2 - t ^ 2) + 4 ∧ WordRAM.Modifies (workspaceFootprint wb db str k) x.mem z.1.mem ∧ ∃ (W' : Fin t → Fin t → ℕ) (part' : Fin n → Fin t), IsContractionOf W₀ part' W' ∧ ContractState w wb db str t t W' z.1) ∧ ∀ (B : Finset (Fin k)), 0 < minCut W₀ → IsNonTrivialCut B → cutWeight W₀ (pullbackCut part B) = minCut W₀ → ↑(t * (t - 1)) / ↑(k * (k - 1)) ≤ m.eval.toOuterMeasure {z : WordRAM.Data 16 × ℕ | SurvivalPost W₀ wb db str t (pullbackCut part B) z.1}

Master specification for contractDownTo (Code .standard 16). Starting from any ContractState w wb db str k t W x (2 ≤ t ≤ k) where W is a contraction of W₀ along part, contractDownTo:

1. terminates fault-free on every path (ExecRand),
2. issues at most k - t rand calls (IsQueryBounded (k - t)),
3. executes at most 36 * (k ^ 2 - t ^ 2) + 4 instructions on every path, modifying only workspaceFootprint wb db str k and leaving a valid t-supervertex ContractState that is a contraction of W₀, and
4. preserves any fixed minimum cut pullbackCut part B of a connected multigraph (0 < minCut W₀) with probability at least (t * (t - 1)) / (k * (k - 1)).

theorem Cslib.Algorithms.WordRAM.Karger.survivalPost_two_mem_eq {n : ℕ} {W₀ : Fin n → Fin n → ℕ} {wb db str : ℕ} {C_star : Finset (Fin n)} {y : WordRAM.Data 16} (hnt : IsNonTrivialCut C_star) (hmin : cutWeight W₀ C_star = minCut W₀) (hsurv : SurvivalPost W₀ wb db str 2 C_star y) : y.mem (wb + 1) = minCut W₀

At t = 2, any state satisfying SurvivalPost W₀ wb db str 2 C_star y where C_star is a non-trivial cut attaining minCut W₀ stores minCut W₀ in y.mem (wb + 1).

Register-embedding (Code.rename) wrappers for callers with r ≥ 16

def Cslib.Algorithms.WordRAM.Karger.computeDegreesAndTotalAt {r : ℕ} (hr : 16 ≤ r) : WordRAM.Code WordRAM.Basis.standard r

computeDegreesAndTotal embedded on registers 0..15 of any r-register file (16 ≤ r).

def Cslib.Algorithms.WordRAM.Karger.contractDownToAt {r : ℕ} (hr : 16 ≤ r) : WordRAM.Code WordRAM.Basis.standard r

contractDownTo embedded on registers 0..15 of any r-register file (16 ≤ r).

theorem Cslib.Algorithms.WordRAM.Karger.computeDegreesAndTotalAt_exec {r w wb db str k : ℕ} (hr : 16 ≤ r) {W : Fin k → Fin k → ℕ} {x : WordRAM.Data r} (hwBase : x.regs (Fin.castLE hr Reg.wBase) = wb) (hdBase : x.regs (Fin.castLE hr Reg.dBase) = db) (hstride : x.regs (Fin.castLE hr Reg.stride) = str) (hactiveK : x.regs (Fin.castLE hr Reg.activeK) = k) (hstr : k ≤ str) (hdisj : wb + str * k ≤ db ∨ db + k ≤ wb) (h1 : WordRAM.Fits w 1) (hwEnd : WordRAM.Fits w (wb + str * k)) (hdEnd : WordRAM.Fits w (db + k)) (htot : WordRAM.Fits w (totalDoubledWeight W)) (hmat : HoldsMatrix x.mem wb str W) : ∃ (y : WordRAM.Data r), WordRAM.ExecWithin w (computeDegreesAndTotalAt hr) x y (6 * k ^ 2 + 12 * k + 6) ∧ HoldsWorkspace y.mem wb db str W ∧ WordRAM.Modifies (Finset.Ico db (db + k)) x.mem y.mem ∧ y.regs (Fin.castLE hr Reg.wBase) = wb ∧ y.regs (Fin.castLE hr Reg.dBase) = db ∧ y.regs (Fin.castLE hr Reg.stride) = str ∧ y.regs (Fin.castLE hr Reg.activeK) = k ∧ y.regs (Fin.castLE hr Reg.targetT) = x.regs (Fin.castLE hr Reg.targetT) ∧ y.regs (Fin.castLE hr Reg.totS) = totalDoubledWeight W ∧ ∀ (j : Fin r), 16 ≤ ↑j → y.regs j = x.regs j

Specification of computeDegreesAndTotalAt hr on any r-register file (16 ≤ r), preserving all caller registers with index ≥ 16.

theorem Cslib.Algorithms.WordRAM.Karger.contractDownToAt_spec {r n w wb db str k t : ℕ} (hr : 16 ≤ r) {W₀ : Fin n → Fin n → ℕ} {W : Fin k → Fin k → ℕ} {part : Fin n → Fin k} {x : WordRAM.Data r} (ht : 2 ≤ t) (htk : t ≤ k) (hC : IsContractionOf W₀ part W) (hst : ContractState w wb db str k t W (WordRAM.Data.comap (Fin.castLE hr) x)) : ∃ (m : ProbComp (WordRAM.Data r × ℕ)), WordRAM.ExecRand w (contractDownToAt hr) x m ∧ OracleComp.IsQueryBounded m (k - t) ∧ (∀ z ∈ OracleComp.support m, z.2 ≤ 36 * (k ^ 2 - t ^ 2) + 4 ∧ WordRAM.Modifies (workspaceFootprint wb db str k) x.mem z.1.mem ∧ (∀ (j : Fin r), 16 ≤ ↑j → z.1.regs j = x.regs j) ∧ ∃ (W' : Fin t → Fin t → ℕ) (part' : Fin n → Fin t), IsContractionOf W₀ part' W' ∧ ContractState w wb db str t t W' (WordRAM.Data.comap (Fin.castLE hr) z.1)) ∧ ∀ (B : Finset (Fin k)), 0 < minCut W₀ → IsNonTrivialCut B → cutWeight W₀ (pullbackCut part B) = minCut W₀ → ↑(t * (t - 1)) / ↑(k * (k - 1)) ≤ m.eval.toOuterMeasure {z : WordRAM.Data r × ℕ | SurvivalPost W₀ wb db str t (pullbackCut part B) (WordRAM.Data.comap (Fin.castLE hr) z.1)}

Specification of contractDownToAt hr on any r-register file (16 ≤ r), preserving all caller registers with index ≥ 16.