Expected running time for randomized word RAMs

Expected instruction counts for flat (Program) and structured (Code) randomized word RAM programs, valued in the extended nonnegative reals ℝ≥0∞ so expectations are total without summability side conditions; nonsummable running-probability tails have value ⊤.

For a flat program p starting at state s, the expected running time is defined via the discrete tail-sum formula over clocked horizons: expectedTime w p s = ∑' t : ℕ, (evalRand w p t s).toOuterMeasure {cfg | ∃ u, cfg = .running u}. Because .halted and .faulted are absorbing, each horizon t contributes the probability that execution is still running before either halt or fault after t steps. Summing over t : ℕ yields the exact 1-step Bellman equation expectedStepsFrom_running, connects directly to structured ExecRand trees via ExecRand.expectedTime_program, reduces to a finite sum under RandHaltsWithin (RandHaltsWithin.expectedTime_eq_sum, expectedTime_le_of_randHaltsWithin), and recovers exact deterministic step counts (Executes.expectedTime_eq).

For structured Code B r programs, expectedCodeTime measures the expected instruction count of codeComp w c x when a finite, fault-free ExecRand tree exists, and is ⊤ otherwise. Thus unbounded almost-surely terminating loops can receive a conservative infinite structured cost. It satisfies exact sequential additivity (expectedCodeTime_seq), branch laws (expectedCodeTime_branch_pos, expectedCodeTime_branch_neg, expectedCodeTime_branch_le), and a potential/drift bound for while loops (expectedCodeTime_loop_le_of_drift).

Main definitions

• Cslib.WordRAM.AlmostSurelyHalts: zero faults at all horizons and supremum halting probability equal to 1.
• Cslib.WordRAM.expectedStepsFrom, Cslib.WordRAM.expectedTime: ℝ≥0∞-valued expected remaining instructions from a RandCfg r or initial State r.
• Cslib.WordRAM.expectedCodeTime: ℝ≥0∞-valued expected instruction count of a structured Code B r.

Main results

• Cslib.WordRAM.expectedStepsFrom_running: 1-step Bellman equation for expectedStepsFrom.
• Cslib.WordRAM.RandHaltsWithin.almostSurelyHalts, Cslib.WordRAM.AlmostSurelyHalts.of_expectedTime_ne_top: sufficient conditions for almost-sure halting.
• Cslib.WordRAM.RandHaltsWithin.expectedTime_eq_sum, Cslib.WordRAM.expectedTime_le_of_randHaltsWithin: finite-horizon reduction under RandHaltsWithin.
• Cslib.WordRAM.Executes.expectedTime_eq: deterministic halting runs have expectedTime = n.
• Cslib.WordRAM.ExecRand.expectedTime_program: exact bridge between compiled c.program out and expectedCodeTime.
• Cslib.WordRAM.expectedCodeTime_seq, Cslib.WordRAM.expectedCodeTime_branch_le, Cslib.WordRAM.expectedCodeTime_loop_le_of_drift: compositional expected-time rules for structured Code.

Discrete and conditional expectation principles are classical background; see [MU17], Sections 2.1 and 2.3. The particular native tail-sum/Bellman definitions, finite structured-execution-tree bridge and ranked-loop expected-cost formalization are original library constructions in this module.

References

• M. Mitzenmacher and E. Upfal, Probability and Computing, Sections 2.1 and 2.3.

Almost-sure halting and ℝ≥0∞-valued expected running time

def Cslib.WordRAM.RandCfg.runningSet (r : ℕ) : Set (RandCfg r)

Set of active (.running) configurations.

def Cslib.WordRAM.RandCfg.haltedSet (r : ℕ) : Set (RandCfg r)

Set of cleanly halted (.halted) configurations.

@[simp]

theorem Cslib.WordRAM.RandCfg.mem_runningSet_iff {r : ℕ} {cfg : RandCfg r} : cfg ∈ runningSet r ↔ ∃ (u : State r), cfg = running u

@[simp]

theorem Cslib.WordRAM.RandCfg.mem_haltedSet_iff {r : ℕ} {cfg : RandCfg r} : cfg ∈ haltedSet r ↔ ∃ (v : ℕ) (d : Data r), cfg = halted v d

def Cslib.WordRAM.AlmostSurelyHalts {B : Basis} {r : ℕ} (w : ℕ) (p : Program B r) (s : State r) : Prop

Starting from s, p never faults and halts with probability tending to 1.

theorem Cslib.WordRAM.evalRand_haltedSet_mono {B : Basis} {r : ℕ} (w : ℕ) (p : Program B r) (s : State r) : Monotone fun (T : ℕ) => (evalRand w p T s).toOuterMeasure (RandCfg.haltedSet r)

Halting probability is monotone in the horizon T because .halted is absorbing.

theorem Cslib.WordRAM.RandHaltsWithin.almostSurelyHalts {B : Basis} {r w T : ℕ} {p : Program B r} {s : State r} (h : RandHaltsWithin w p s T) : AlmostSurelyHalts w p s

Any worst-case bounded execution halts almost surely.

noncomputable def Cslib.WordRAM.expectedStepsFrom {B : Basis} {r : ℕ} (w : ℕ) (p : Program B r) (cfg : RandCfg r) : ENNReal

Expected number of remaining instructions starting from configuration cfg, defined via the tail sum of active-configuration probabilities.

noncomputable def Cslib.WordRAM.expectedTime {B : Basis} {r : ℕ} (w : ℕ) (p : Program B r) (s : State r) : ENNReal

Expected running time of p at word size w from initial state s, valued in ℝ≥0∞.

theorem Cslib.WordRAM.expectedTime_eq_expectedStepsFrom {B : Basis} {r : ℕ} (w : ℕ) (p : Program B r) (s : State r) : expectedTime w p s = expectedStepsFrom w p (RandCfg.running s)

@[simp]

theorem Cslib.WordRAM.expectedStepsFrom_halted {B : Basis} {r : ℕ} (w : ℕ) (p : Program B r) (v : ℕ) (d : Data r) : expectedStepsFrom w p (RandCfg.halted v d) = 0

@[simp]

theorem Cslib.WordRAM.expectedStepsFrom_faulted {B : Basis} {r : ℕ} (w : ℕ) (p : Program B r) : expectedStepsFrom w p RandCfg.faulted = 0

theorem Cslib.WordRAM.expectedStepsFrom_running {B : Basis} {r : ℕ} (w : ℕ) (p : Program B r) (s : State r) : expectedStepsFrom w p (RandCfg.running s) = 1 + (stepRand w p (RandCfg.running s)).expect (expectedStepsFrom w p)

1-step Bellman equation: an active state s incurs 1 immediate step plus the expected remaining steps from stepRand w p (.running s).

theorem Cslib.WordRAM.RandFaultFree.running_add_halted_eq_one {B : Basis} {r w : ℕ} {p : Program B r} {s : State r} (hf : RandFaultFree w p s) (t : ℕ) : (evalRand w p t s).toOuterMeasure {cfg : RandCfg r | ∃ (u : State r), cfg = RandCfg.running u} + (evalRand w p t s).toOuterMeasure (RandCfg.haltedSet r) = 1

Under RandFaultFree, every horizon partitions probability 1 between .running and .halted.

theorem Cslib.WordRAM.AlmostSurelyHalts.of_expectedTime_ne_top {B : Basis} {r w : ℕ} {p : Program B r} {s : State r} (hf : RandFaultFree w p s) (htop : expectedTime w p s ≠ ⊤) : AlmostSurelyHalts w p s

A fault-free execution with finite expected running time halts almost surely.

theorem Cslib.WordRAM.RandHaltsWithin.expectedTime_eq_sum {B : Basis} {r w T : ℕ} {p : Program B r} {s : State r} (h : RandHaltsWithin w p s T) : expectedTime w p s = ∑ t ∈ Finset.range T, (evalRand w p t s).toOuterMeasure {cfg : RandCfg r | ∃ (u : State r), cfg = RandCfg.running u}

Under RandHaltsWithin w p s T, the active-configuration tail sum vanishes from T onward and reduces to a finite sum over Finset.range T.

theorem Cslib.WordRAM.expectedTime_le_of_randHaltsWithin {B : Basis} {r w T : ℕ} {p : Program B r} {s : State r} (h : RandHaltsWithin w p s T) : expectedTime w p s ≤ ↑T

A worst-case step bound RandHaltsWithin w p s T immediately bounds expectedTime by T.

theorem Cslib.WordRAM.Runs.expectedStepsFrom_eq {B : Basis} {r w m : ℕ} {p : Program B r} {s t : State r} (hrun : Runs w p s t m) : expectedStepsFrom w p (RandCfg.running s) = ↑m + expectedStepsFrom w p (RandCfg.running t)

Along any deterministic Runs of length m, expectedStepsFrom adds m to the expected remaining steps at the destination state.

theorem Cslib.WordRAM.Executes.expectedTime_eq {B : Basis} {r w n : ℕ} {p : Program B r} {s : State r} {v : ℕ} (h : Executes w p s v n) : expectedTime w p s = ↑n

Any deterministic halting execution Executes w p s v n has exact expected running time n.

Structured expectedCodeTime and compilation bridge

theorem Cslib.WordRAM.ExecRand.expectedStepsFrom_assemble {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} {m : ProbComp (Data r × ℕ)} (h : ExecRand w c x m) {p : Program B r} {pc : ℕ} (hp : p.Contains pc (c.assemble pc)) : expectedStepsFrom w p (RandCfg.running { pc := pc, data := x }) = m.expect fun (z : Data r × ℕ) => ↑z.2 + expectedStepsFrom w p (RandCfg.running { pc := pc + c.size, data := z.1 })

Along an assembled structured execution ExecRand w c x m inside p, the expected remaining steps from ⟨pc, x⟩ equal the expected step count of m plus the expected continuation steps from ⟨pc + c.size, y⟩.

theorem Cslib.WordRAM.ExecRand.expectedTime_program {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} {m : ProbComp (Data r × ℕ)} (h : ExecRand w c x m) (out : Fin r) : expectedTime w (c.program out) { pc := 0, data := x } = (m.expect fun (z : Data r × ℕ) => ↑z.2) + 1

Exact bridge: compiling c with c.program out adds 1 (for the final halt out instruction) to the expected step count of ExecRand w c x m.

theorem Cslib.WordRAM.codeComp_execRand {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} (hex : ∃ (m : ProbComp (Data r × ℕ)), ExecRand w c x m) : ExecRand w c x (codeComp w c x)

When some ExecRand w c x m exists, codeComp w c x satisfies ExecRand.

noncomputable def Cslib.WordRAM.expectedCodeTime {B : Basis} {r : ℕ} (w : ℕ) (c : Code B r) (x : Data r) : ENNReal

Expected instruction count of a structured program c from data x at word size w, or ⊤ if c can fault or diverge on some path from x.

theorem Cslib.WordRAM.ExecRand.expectedCodeTime_eq {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} {m : ProbComp (Data r × ℕ)} (h : ExecRand w c x m) : expectedCodeTime w c x = m.expect fun (z : Data r × ℕ) => ↑z.2

theorem Cslib.WordRAM.expectedCodeTime_eq_top {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} (h : ¬∃ (m : ProbComp (Data r × ℕ)), ExecRand w c x m) : expectedCodeTime w c x = ⊤

theorem Cslib.WordRAM.Exec.expectedCodeTime_eq {B : Basis} {r w n : ℕ} {c : Code B r} {x y : Data r} (h : Exec w c x y n) : expectedCodeTime w c x = ↑n

theorem Cslib.WordRAM.expectedCodeTime_program {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} {m : ProbComp (Data r × ℕ)} (h : ExecRand w c x m) (out : Fin r) : expectedTime w (c.program out) { pc := 0, data := x } = expectedCodeTime w c x + 1

@[simp]

theorem Cslib.WordRAM.expectedCodeTime_op {B : Basis} {r w : ℕ} {o : Op B r} {x y : Data r} (ho : Op.eval w o x = some y) : expectedCodeTime w (Code.op o) x = 1

@[simp]

theorem Cslib.WordRAM.expectedCodeTime_rand {B : Basis} {r w : ℕ} {dst src : Fin r} {x : Data r} (h : Fits w (x.regs src)) : expectedCodeTime w (Code.rand dst src) x = 1

theorem Cslib.WordRAM.expectedCodeTime_seq {B : Basis} {r w : ℕ} {c₁ c₂ : Code B r} {x : Data r} {m₁ : ProbComp (Data r × ℕ)} (h₁ : ExecRand w c₁ x m₁) : expectedCodeTime w (c₁.seq c₂) x = expectedCodeTime w c₁ x + m₁.expect fun (z : Data r × ℕ) => expectedCodeTime w c₂ z.1

Sequential additivity of expectedCodeTime: when c₁ executes via m₁, the expected time of Code.seq c₁ c₂ equals the expected time of c₁ plus the m₁-expected time of c₂.

theorem Cslib.WordRAM.expectedCodeTime_seq_of_exec {B : Basis} {r w n₁ : ℕ} {c₁ c₂ : Code B r} {x y : Data r} (h₁ : Exec w c₁ x y n₁) : expectedCodeTime w (c₁.seq c₂) x = ↑n₁ + expectedCodeTime w c₂ y

Sequential additivity after a deterministic prefix Exec w c₁ x y n₁.

theorem Cslib.WordRAM.expectedCodeTime_branch_pos {B : Basis} {r w : ℕ} {cond : Cond r} {pos neg : Code B r} {x : Data r} (hc : cond.Holds x) : expectedCodeTime w (Code.branch cond pos neg) x = expectedCodeTime w pos x + 1

theorem Cslib.WordRAM.expectedCodeTime_branch_neg {B : Basis} {r w : ℕ} {cond : Cond r} {pos neg : Code B r} {x : Data r} (hc : ¬cond.Holds x) : expectedCodeTime w (Code.branch cond pos neg) x = expectedCodeTime w neg x + 2

theorem Cslib.WordRAM.expectedCodeTime_branch_le {B : Basis} {r w : ℕ} {cond : Cond r} {pos neg : Code B r} {x : Data r} {B_steps : ENNReal} (hpos : cond.Holds x → expectedCodeTime w pos x + 1 ≤ B_steps) (hneg : ¬cond.Holds x → expectedCodeTime w neg x + 2 ≤ B_steps) : expectedCodeTime w (Code.branch cond pos neg) x ≤ B_steps

Branch convexity / uniform upper bound on expectedCodeTime (.branch cond pos neg).

theorem Cslib.WordRAM.expect_expectedCodeTime_branch {B : Basis} {r w : ℕ} {cond : Cond r} {pos neg : Code B r} (m : ProbComp (Data r)) : (m.expect fun (x : Data r) => expectedCodeTime w (Code.branch cond pos neg) x) = m.expect fun (x : Data r) => if cond.Holds x then expectedCodeTime w pos x + 1 else expectedCodeTime w neg x + 2

Convex combination of branch expected times under a random input distribution m.

theorem Cslib.WordRAM.expectedCodeTime_loop_exit {B : Basis} {r w : ℕ} {cond : Cond r} {body : Code B r} {x : Data r} (hc : ¬cond.Holds x) : expectedCodeTime w (Code.loop cond body) x = 2

theorem Cslib.WordRAM.expectedCodeTime_loop_iter {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) : expectedCodeTime w (Code.loop cond body) x = expectedCodeTime w body x + 2 + mb.expect fun (z : Data r × ℕ) => expectedCodeTime w (Code.loop cond body) z.1

theorem Cslib.WordRAM.expectedCodeTime_loop_le_of_drift {B : Basis} {r w : ℕ} {cond : Cond r} {body : Code B r} (I : Data r → Prop) (Φ : Data r → ℕ) (Ψ : Data r → ENNReal) {x : Data r} (hx : I x) (hstep : ∀ (s : Data r), I s → cond.Holds s → ∃ (mb : ProbComp (Data r × ℕ)), ExecRand w body s mb ∧ (∀ z ∈ OracleComp.support mb, I z.1 ∧ Φ z.1 < Φ s) ∧ (mb.expect fun (z : Data r × ℕ) => ↑z.2 + 2 + Ψ z.1) ≤ Ψ s) : (∃ (m : ProbComp (Data r × ℕ)), ExecRand w (Code.loop cond body) x m) ∧ expectedCodeTime w (Code.loop cond body) x ≤ Ψ x + 2

Potential/drift bound for Code.loop: if an invariant I holds, every iteration decreases a well-founded ℕ ranking Φ, and the expected single-iteration cost (z.2 : ℝ≥0∞) + 2 plus next potential Ψ z.1 is at most Ψ s, then the loop executes cleanly (∃ m, ExecRand ...) and its expectedCodeTime is at most Ψ x + 2 (accounting for the final 2-step loop exit).