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.

The probability is not proved on machine states. contractDownTo simulates Karger's algorithm as a client of the contraction structure Cslib.Algorithms.Lean.Karger.spec: the graph the machine holds (heldGraph) has the law of Cslib.Algorithms.Lean.Karger.contractTimes (contractDownTo_law). Each step's rand call draws the offset uniformly below the total weight, as the client's coin does, and postRandStep_exec contracts the pair sampled there. The survival bound and the contraction invariant are the specification's (Cslib.Algorithms.Lean.Karger.survives_contractTimes, Cslib.Algorithms.Lean.Karger.isContractionOf_of_mem_support_contractTimes), carried through that law.

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.flattenMatrix: the row-major n ^ 2-word input layout of a weight matrix.
• 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.heldGraph: the graph a machine state holds, as a state of Cslib.Algorithms.Lean.Karger.spec.
• 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_law: contractDownTo simulates k - t contractions of the specification: ExecRandLaw with IsQueryBounded (k - t), worst-case step bound 36 * (k ^ 2 - t ^ 2) + 4, Modifies frame, and the law of heldGraph.
• Cslib.Algorithms.WordRAM.Karger.contractDownToAt_law: the same on any r ≥ 16 registers, preserving the caller's registers.
• Cslib.Algorithms.WordRAM.Karger.ContractState.mem_add_one: on two supervertices, the weight between them is half the total weight of the held graph.
• 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 cut-survival probability lower bound ((t * (t - 1) : ℕ) : ℝ≥0∞) / (k * (k - 1)), the last two from the specification.

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.

Row-major input layout of the matrix

def Cslib.Algorithms.WordRAM.Karger.flattenMatrix {n : ℕ} (W : Fin n → Fin n → ℕ) : List ℕ

Row-major n * n-element list encoding of W : Fin n → Fin n → ℕ.

@[simp]

theorem Cslib.Algorithms.WordRAM.Karger.length_flattenMatrix {n : ℕ} (W : Fin n → Fin n → ℕ) : (flattenMatrix W).length = n * n

theorem Cslib.Algorithms.WordRAM.Karger.getElem_flattenMatrix {n : ℕ} (W : Fin n → Fin n → ℕ) (u v : Fin n) : (flattenMatrix W)[↑u * n + ↑v] = W u v

theorem Cslib.Algorithms.WordRAM.Karger.mem_flattenMatrix_le_totalDoubledWeight {n : ℕ} (W : Fin n → Fin n → ℕ) {x : ℕ} (hx : x ∈ flattenMatrix W) : x ≤ WeightedCut.totalDoubledWeight W

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.

theorem Cslib.Algorithms.WordRAM.Karger.holdsMatrix_init_append {r n : ℕ} (pfx : List ℕ) (W : Fin n → Fin n → ℕ) : HoldsMatrix (WordRAM.Data.init (pfx ++ flattenMatrix W)).mem (1 + pfx.length) n W

In Data.init (pfx ++ flattenMatrix W), the flattened matrix occupies memory starting at 1 + pfx.length with stride n.

theorem Cslib.Algorithms.WordRAM.Karger.holdsMatrix_init_single {r n : ℕ} (W : Fin n → Fin n → ℕ) : HoldsMatrix (WordRAM.Data.init (n :: flattenMatrix W)).mem 2 n W

In Data.init (n :: flattenMatrix W), memory holds W at base 2 with stride n.

theorem Cslib.Algorithms.WordRAM.Karger.inputFits_cons_flattenMatrix {w a n B : ℕ} {W : Fin n → Fin n → ℕ} (hB : WordRAM.Fits w B) (hlen : 1 + n * n ≤ B) (ha : a ≤ B) (htot : WordRAM.Fits w (WeightedCut.totalDoubledWeight W)) : WordRAM.InputFits w (a :: flattenMatrix W)

The input a :: flattenMatrix W fits word size w when one fitting bound B covers both the input length 1 + n * n and the leading word a, and the matrix total fits.

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 = WeightedCut.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 (WeightedCut.totalDoubledWeight W)
• workspace : HoldsWorkspace x.mem wb db str W

def Cslib.Algorithms.WordRAM.Karger.heldGraph (wb str : ℕ) (x : WordRAM.Data 16) : Lean.Karger.Graph

The graph that a machine state holds in the workspace at wb with row stride str: activeK supervertices, with the weight matrix read from memory. It abstracts a ContractState to a state of the contraction structure Lean.Karger.spec.

theorem Cslib.Algorithms.WordRAM.Karger.ContractState.heldGraph_eq {w wb db str k t : ℕ} {W : Fin k → Fin k → ℕ} {x : WordRAM.Data 16} (hst : ContractState w wb db str k t W x) : heldGraph wb str x = { size := k, weight := W }

A state holding W on k supervertices holds the graph ⟨k, W⟩.

theorem Cslib.Algorithms.WordRAM.Karger.ContractState.mem_add_one {w wb db str t : ℕ} {W : Fin 2 → Fin 2 → ℕ} {x : WordRAM.Data 16} (hst : ContractState w wb db str 2 t W x) (hW : WeightedCut.IsMultigraph W) : x.mem (wb + 1) = WeightedCut.totalDoubledWeight (heldGraph wb str x).weight / 2

On two supervertices, the weight between them, at wb + 1, is half the total weight of the held graph.

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 (WeightedCut.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 = WeightedCut.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 : Karger.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 = WeightedCut.totalDoubledWeight W) (hrem : x.regs Reg.rem = r_val) (hdEnd : WordRAM.Fits w (db + k)) (htot : WordRAM.Fits w (WeightedCut.totalDoubledWeight W)) (hdeg : ∀ (i : Fin k), x.mem (db + ↑i) = WeightedCut.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 = WeightedCut.totalDoubledWeight W ∧ y.regs Reg.uReg = ↑u ∧ y.regs Reg.rem = r_val + 1 - Karger.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 : Karger.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 = WeightedCut.totalDoubledWeight W) (huReg : x.regs Reg.uReg = ↑u) (hrem : x.regs Reg.rem = r_val + 1 - Karger.degBefore W u) (hstr : k ≤ str) (hwEnd : WordRAM.Fits w (wb + str * k)) (hdEnd : WordRAM.Fits w (db + k)) (htot : WordRAM.Fits w (WeightedCut.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 = WeightedCut.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 : WeightedCut.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 = WeightedCut.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 (WeightedCut.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) = WeightedCut.rowDeg (WeightedCut.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 = WeightedCut.totalDoubledWeight (WeightedCut.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 : WeightedCut.IsMultigraph W) (hsamp : Karger.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 = WeightedCut.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 (WeightedCut.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 (WeightedCut.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.

Simulation of the contraction structure 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_law {w wb db str k t : ℕ} {W : Fin k → Fin k → ℕ} {x : WordRAM.Data 16} (ht : 2 ≤ t) (htk : t ≤ k) (hW : WeightedCut.IsMultigraph W) (hst : ContractState w wb db str k t W x) : WordRAM.ExecRandLaw w contractDownTo x (fun (y : WordRAM.Data 16) => WordRAM.Modifies (workspaceFootprint wb db str k) x.mem y.mem ∧ ∃ (W' : Fin t → Fin t → ℕ), WeightedCut.IsMultigraph W' ∧ ContractState w wb db str t t W' y) (36 * (k ^ 2 - t ^ 2) + 4) (k - t) (heldGraph wb str) (PMF.map Prod.snd (Lean.Karger.spec.toRandomized.withCoins.run (Lean.Karger.contractTimes (k - t)) { size := k, weight := W }))

contractDownTo refines the contraction structure. From a state holding a multigraph W on k ≥ t ≥ 2 supervertices, contractDownTo runs within 36 (k² - t²) + 4 instructions and k - t rand calls, writes only the workspace and ends holding a multigraph on t supervertices. The graph it holds (heldGraph) has the law of k - t contractions of ⟨k, W⟩ by the client Lean.Karger.contractTimes of Lean.Karger.spec.

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 : WeightedCut.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), WeightedCut.IsContractionOf W₀ part' W' ∧ ContractState w wb db str t t W' z.1) ∧ ∀ (B : Finset (Fin k)), 0 < WeightedCut.minCut W₀ → WeightedCut.IsNonTrivialCut B → WeightedCut.cutWeight W₀ (WeightedCut.pullbackCut part B) = WeightedCut.minCut W₀ → ↑(t * (t - 1)) / ↑(k * (k - 1)) ≤ m.eval.toOuterMeasure {z : WordRAM.Data 16 × ℕ | SurvivalPost W₀ wb db str t (WeightedCut.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)).

The first three parts and the law of the held graph are contractDownTo_law. The contraction in part 3 and the bound in part 4 are the specification's (Lean.Karger.isContractionOf_of_mem_support_contractTimes, Lean.Karger.survives_contractTimes), carried through that law.

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 : WeightedCut.IsNonTrivialCut C_star) (hmin : WeightedCut.cutWeight W₀ C_star = WeightedCut.minCut W₀) (hsurv : SurvivalPost W₀ wb db str 2 C_star y) : y.mem (wb + 1) = WeightedCut.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 (WeightedCut.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) = WeightedCut.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_law {r w wb db str k t : ℕ} (hr : 16 ≤ r) {W : Fin k → Fin k → ℕ} {x : WordRAM.Data r} (ht : 2 ≤ t) (htk : t ≤ k) (hW : WeightedCut.IsMultigraph W) (hst : ContractState w wb db str k t W (WordRAM.Data.comap (Fin.castLE hr) x)) : WordRAM.ExecRandLaw w (contractDownToAt hr) x (fun (y : WordRAM.Data r) => WordRAM.Modifies (workspaceFootprint wb db str k) x.mem y.mem ∧ (∀ (j : Fin r), 16 ≤ ↑j → y.regs j = x.regs j) ∧ ∃ (W' : Fin t → Fin t → ℕ), WeightedCut.IsMultigraph W' ∧ ContractState w wb db str t t W' (WordRAM.Data.comap (Fin.castLE hr) y)) (36 * (k ^ 2 - t ^ 2) + 4) (k - t) (fun (y : WordRAM.Data r) => heldGraph wb str (WordRAM.Data.comap (Fin.castLE hr) y)) (PMF.map Prod.snd (Lean.Karger.spec.toRandomized.withCoins.run (Lean.Karger.contractTimes (k - t)) { size := k, weight := W }))

contractDownToAt hr simulates k - t contractions of Lean.Karger.spec on any r-register file (16 ≤ r), as contractDownTo_law does, and preserves 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 : WeightedCut.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), WeightedCut.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 < WeightedCut.minCut W₀ → WeightedCut.IsNonTrivialCut B → WeightedCut.cutWeight W₀ (WeightedCut.pullbackCut part B) = WeightedCut.minCut W₀ → ↑(t * (t - 1)) / ↑(k * (k - 1)) ≤ m.eval.toOuterMeasure {z : WordRAM.Data r × ℕ | SurvivalPost W₀ wb db str t (WeightedCut.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.