Compositional while-loop segments for structured randomized word-RAM programs

Cslib.WordRAM.LoopSegment w cond body x m represents executing zero or more active iterations of Code.loop cond body starting at machine state x : Data r and producing the randomized state-time distribution m : ProbComp (Data r × ℕ), without yet performing the final loop-exit condition check.

Whereas ExecRand.loop_iter and ExecRand.loop_exit require each iteration to continue all the way to termination of the enclosing loop (¬cond.Holds), LoopSegment packages multi-iteration sub-runs that may finish in states where cond.Holds still holds. This allows explicit call-stack algorithms (such as Karger and Stein's recursive FastCut simulated inside a single while sp > 0 loop) to prove frame execution by structural induction on stack depth sp = b + 1 → b, compose sibling recursive subtrees via LoopSegment.trans, and discharge the outer while sp > 0 loop at depth b = 0 via LoopSegment.finish.

Main definitions

• Cslib.WordRAM.LoopSegment: multi-iteration execution segments of Code.loop cond body before loop exit.

Main results

• Cslib.WordRAM.LoopSegment.single, Cslib.WordRAM.LoopSegment.detSingle: single randomized or deterministic loop iteration (+ 2 loop-header instructions).
• Cslib.WordRAM.LoopSegment.trans, Cslib.WordRAM.LoopSegment.trans_exists, Cslib.WordRAM.LoopSegment.stepDet: transitive and deterministic-prefix sequential composition of loop segments.
• Cslib.WordRAM.LoopSegment.finish: closes a LoopSegment into ExecRand w (.loop cond body) once every supported output violates cond (+ 2 instructions for the final exit check).
• Cslib.WordRAM.LoopSegment.regs_eq, Cslib.WordRAM.LoopSegment.bounded: register preservation and word-bound invariance across a LoopSegment.
• Cslib.WordRAM.execRand_seq_det: appends a deterministic ExecWithin continuation onto a randomized ExecRand computation as a pure Functor.map.

References

• D. R. Karger and C. Stein, A New Approach to the Minimum Cut Problem

inductive Cslib.WordRAM.LoopSegment {B : Basis} {r : ℕ} (w : ℕ) (cond : Cond r) (body : Code B r) : Data r → ProbComp (Data r × ℕ) → Prop

LoopSegment w cond body x m: starting at data x, executing zero or more iterations of Code.loop cond body (each verifying cond.Holds, running body, and charging + 2 for the loop header test and back-jump) without yet taking the loop-exit check produces m.

Enables structural induction on explicit call-stack depth inside a single outer while sp > 0 loop, where popping a recursive frame lowers sp from b + 1 to b without exiting the loop when b > 0.

• nil {B : Basis} {r w : ℕ} {cond : Cond r} {body : Code B r} (x : Data r) : LoopSegment w cond body x (pure (x, 0))

  Zero iterations, charging 0 instructions.

• step {B : Basis} {r w : ℕ} {cond : Cond r} {body : Code B r} {x : Data r} {mb : ProbComp (Data r × ℕ)} {mr : Data r → ProbComp (Data r × ℕ)} (hc : cond.Holds x) (hb : ExecRand w body x mb) (hr : ∀ z ∈ OracleComp.support mb, LoopSegment w cond body z.1 (mr z.1)) : LoopSegment w cond body x do let z₁ ← mb let z₂ ← mr z₁.1 pure (z₂.1, z₁.2 + z₂.2 + 2)

  One active loop iteration followed by a continuation segment.

theorem Cslib.WordRAM.LoopSegment.single {B : Basis} {r w : ℕ} {cond : Cond r} {body : Code B r} {x : Data r} {mb : ProbComp (Data r × ℕ)} (hc : cond.Holds x) (hb : ExecRand w body x mb) : LoopSegment w cond body x ((fun (z : Data r × ℕ) => (z.1, z.2 + 2)) <$> mb)

A single randomized loop iteration (+ 2 loop-header instructions).

theorem Cslib.WordRAM.LoopSegment.detSingle {B : Basis} {r w : ℕ} {cond : Cond r} {body : Code B r} {x y : Data r} {n : ℕ} (hc : cond.Holds x) (hb : Exec w body x y n) : LoopSegment w cond body x (pure (y, n + 2))

A single deterministic loop iteration (+ 2 loop-header instructions).

theorem Cslib.WordRAM.LoopSegment.trans {B : Basis} {r w : ℕ} {cond : Cond r} {body : Code B r} {x : Data r} {m₁ : ProbComp (Data r × ℕ)} {m₂ : Data r → ProbComp (Data r × ℕ)} (h₁ : LoopSegment w cond body x m₁) (h₂ : ∀ z ∈ OracleComp.support m₁, LoopSegment w cond body z.1 (m₂ z.1)) : LoopSegment w cond body x do let z₁ ← m₁ let z₂ ← m₂ z₁.1 pure (z₂.1, z₁.2 + z₂.2)

Sequential composition of two loop segments.

theorem Cslib.WordRAM.LoopSegment.trans_exists {B : Basis} {r w : ℕ} {cond : Cond r} {body : Code B r} {x : Data r} {m₁ : ProbComp (Data r × ℕ)} {Q : Data r → ProbComp (Data r × ℕ) → Prop} (h₁ : LoopSegment w cond body x m₁) (h₂ : ∀ z ∈ OracleComp.support m₁, ∃ (m' : ProbComp (Data r × ℕ)), LoopSegment w cond body z.1 m' ∧ Q z.1 m') : ∃ (m₂ : Data r → ProbComp (Data r × ℕ)), (LoopSegment w cond body x do let z₁ ← m₁ let z₂ ← m₂ z₁.1 pure (z₂.1, z₁.2 + z₂.2)) ∧ ∀ z ∈ OracleComp.support m₁, LoopSegment w cond body z.1 (m₂ z.1) ∧ Q z.1 (m₂ z.1)

Existential sequential composition of two loop segments using Classical.choose.

theorem Cslib.WordRAM.LoopSegment.stepDet {B : Basis} {r w : ℕ} {cond : Cond r} {body : Code B r} {x y : Data r} {n₁ : ℕ} {m₂ : ProbComp (Data r × ℕ)} (hc : cond.Holds x) (hb : Exec w body x y n₁) (hr : LoopSegment w cond body y m₂) : LoopSegment w cond body x ((fun (z : Data r × ℕ) => (z.1, n₁ + 2 + z.2)) <$> m₂)

Prepending a deterministic single iteration onto a continuation LoopSegment.

theorem Cslib.WordRAM.LoopSegment.finish {B : Basis} {r w : ℕ} {cond : Cond r} {body : Code B r} {x : Data r} {m : ProbComp (Data r × ℕ)} (h : LoopSegment w cond body x m) (hexit : ∀ z ∈ OracleComp.support m, ¬cond.Holds z.1) : ExecRand w (Code.loop cond body) x ((fun (z : Data r × ℕ) => (z.1, z.2 + 2)) <$> m)

Closing a LoopSegment into ExecRand w (.loop cond body) once every supported state violates cond (+ 2 instructions for the final loop-exit check).

theorem Cslib.WordRAM.LoopSegment.regs_eq {B : Basis} {r w : ℕ} {cond : Cond r} {body : Code B r} {x : Data r} {m : ProbComp (Data r × ℕ)} {i : Fin r} (h : LoopSegment w cond body x m) (hi : Code.Preserves i body) {z : Data r × ℕ} (hz : z ∈ OracleComp.support m) : z.1.regs i = x.regs i

Any register preserved by body is preserved along every LoopSegment.

theorem Cslib.WordRAM.LoopSegment.bounded {B : Basis} {r w : ℕ} {cond : Cond r} {body : Code B r} {x : Data r} {m : ProbComp (Data r × ℕ)} (h : LoopSegment w cond body x m) (hx : Data.Bounded w x) {z : Data r × ℕ} (hz : z ∈ OracleComp.support m) : Data.Bounded w z.1

LoopSegment preserves Data.Bounded w on every supported path.

theorem Cslib.WordRAM.execRand_seq_det {B : Basis} {r w T : ℕ} {c₁ c₂ : Code B r} {x : Data r} {m₁ : ProbComp (Data r × ℕ)} {Q : Data r → Data r → Prop} (h₁ : ExecRand w c₁ x m₁) (h₂ : ∀ z ∈ OracleComp.support m₁, ∃ (y : Data r), ExecWithin w c₂ z.1 y T ∧ Q z.1 y) : ∃ (g : Data r → Data r × ℕ), ExecRand w (c₁.seq c₂) x ((fun (z : Data r × ℕ) => ((g z.1).1, z.2 + (g z.1).2)) <$> m₁) ∧ ∀ z ∈ OracleComp.support m₁, (g z.1).2 ≤ T ∧ Exec w c₂ z.1 (g z.1).1 (g z.1).2 ∧ Q z.1 (g z.1).1

Append a deterministic ExecWithin continuation onto a randomized ExecRand computation as a pure Functor.map.