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.
• Cslib.WordRAM.ExecCodeDist: compositional structured execution certificate pairing an output distribution μ : PMF (Data r) with an expected step bound T : ℝ≥0∞, closed under unbounded almost-surely terminating geometric while loops (ExecCodeDist.loop_geometric).

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.
• Cslib.WordRAM.ExecCodeDist.loop_geometric, Cslib.WordRAM.expectedStepsFrom_loop_le_of_geometric, Cslib.WordRAM.ExecCodeDist.program_halts: expected-time and almost-sure halting rules for geometric Las Vegas while loops and structured programs.

Discrete and conditional expectation principles are classical background; see [MU17], Sections 2.1, 2.3, and 2.4. 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, 2.3, and 2.4.

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).

Distributional structured execution (ExecCodeDist) and geometric Las Vegas loops

theorem Cslib.WordRAM.ExecRand.mapSimulates {B : Basis} {r : ℕ} {B' : Basis} (ψ : B.Simulates B') {w : ℕ} {c : Code B r} {x : Data r} {m : ProbComp (Data r × ℕ)} (h : ExecRand w c x m) : ExecRand w (Code.mapSimulates ψ c) x m

Non-faulting structured randomized executions transfer instruction-for-instruction along any defined-evaluation basis simulation ψ : B.Simulates B'.

theorem Cslib.WordRAM.evalRand_halted_mono {B : Basis} {r : ℕ} (w : ℕ) (p : Program B r) (s : State r) (v : ℕ) (d : Data r) : Monotone fun (T : ℕ) => (evalRand w p T s) (RandCfg.halted v d)

Pointwise halting probability at .halted v d is monotone in the horizon T.

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

Finite-horizon approximation of expectedStepsFrom: expected number of active (.running) steps within the first N steps starting from configuration cfg.

@[simp]

theorem Cslib.WordRAM.expectedStepsWithin_zero {B : Basis} {r : ℕ} (w : ℕ) (p : Program B r) (cfg : RandCfg r) : expectedStepsWithin w p 0 cfg = 0

@[simp]

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

@[simp]

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

theorem Cslib.WordRAM.expectedStepsWithin_mono {B : Basis} {r : ℕ} (w : ℕ) (p : Program B r) (cfg : RandCfg r) : Monotone fun (N : ℕ) => expectedStepsWithin w p N cfg

theorem Cslib.WordRAM.iSup_expectedStepsWithin {B : Basis} {r : ℕ} (w : ℕ) (p : Program B r) (cfg : RandCfg r) : ⨆ (N : ℕ), expectedStepsWithin w p N cfg = expectedStepsFrom w p cfg

theorem Cslib.WordRAM.expectedStepsWithin_le_expectedStepsFrom {B : Basis} {r : ℕ} (w : ℕ) (p : Program B r) (N : ℕ) (cfg : RandCfg r) : expectedStepsWithin w p N cfg ≤ expectedStepsFrom w p cfg

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

1-step horizon recursion for expectedStepsWithin: at horizon N + 1, an active state s incurs 1 step plus the N-step continuation expectation.

theorem Cslib.WordRAM.expectedStepsWithin_running_le {B : Basis} {r : ℕ} (w : ℕ) (p : Program B r) (N : ℕ) (s : State r) : expectedStepsWithin w p N (RandCfg.running s) ≤ 1 + (stepRand w p (RandCfg.running s)).expect (expectedStepsWithin w p N)

theorem Cslib.WordRAM.ExecRand.expectedStepsWithin_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)) (N : ℕ) : expectedStepsWithin w p N (RandCfg.running { pc := pc, data := x }) ≤ m.expect fun (z : Data r × ℕ) => ↑z.2 + expectedStepsWithin w p N (RandCfg.running { pc := pc + c.size, data := z.1 })

theorem Cslib.WordRAM.ExecRand.evalRand_faulted_eq_zero {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 T : ℕ} (hp : p.Contains pc (c.assemble pc)) (hcont : ∀ z ∈ OracleComp.support m, ∀ t ≤ T, (evalRand w p t { pc := pc + c.size, data := z.1 }) RandCfg.faulted = 0) (t : ℕ) : t ≤ T → (evalRand w p t { pc := pc, data := x }) RandCfg.faulted = 0

Along ExecRand w c x m, if no continuation from ⟨pc + c.size, y⟩ faults within T steps for any supported outcome y, then running p from ⟨pc, x⟩ does not fault within T steps.

theorem Cslib.WordRAM.ExecRand.le_iSup_evalRand_halted {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)) (v : ℕ) (d : Data r) : (m.expect fun (z : Data r × ℕ) => ⨆ (T : ℕ), (evalRand w p T { pc := pc + c.size, data := z.1 }) (RandCfg.halted v d)) ≤ ⨆ (T : ℕ), (evalRand w p T { pc := pc, data := x }) (RandCfg.halted v d)

Along ExecRand w c x m, the expected supremum halting probability from ⟨pc + c.size, y⟩ is a lower bound on the supremum halting probability from ⟨pc, x⟩.

Absorbing Markov chain for geometric Las Vegas loops

noncomputable def Cslib.WordRAM.loopStepPMF {r : ℕ} (cond : Cond r) (μ_body : Data r → PMF (Data r)) (x : Data r) : PMF (Data r)

One step of the stopped loop Markov kernel on Data r: active states (cond.Holds x) step according to μ_body x, while exiting states (¬cond.Holds x) are absorbing.

theorem Cslib.WordRAM.loopStepPMF_of_holds {r : ℕ} {cond : Cond r} {μ_body : Data r → PMF (Data r)} {x : Data r} (hc : cond.Holds x) : loopStepPMF cond μ_body x = μ_body x

theorem Cslib.WordRAM.loopStepPMF_of_not_holds {r : ℕ} {cond : Cond r} {μ_body : Data r → PMF (Data r)} {x : Data r} (hc : ¬cond.Holds x) : loopStepPMF cond μ_body x = PMF.pure x

noncomputable def Cslib.WordRAM.loopIterPMF {r : ℕ} (cond : Cond r) (μ_body : Data r → PMF (Data r)) : ℕ → Data r → PMF (Data r)

K-step iterate of loopStepPMF.

@[simp]

theorem Cslib.WordRAM.loopIterPMF_zero {r : ℕ} (cond : Cond r) (μ_body : Data r → PMF (Data r)) (x : Data r) : loopIterPMF cond μ_body 0 x = PMF.pure x

theorem Cslib.WordRAM.loopIterPMF_succ {r : ℕ} (cond : Cond r) (μ_body : Data r → PMF (Data r)) (K : ℕ) (x : Data r) : loopIterPMF cond μ_body (K + 1) x = (loopStepPMF cond μ_body x).bind (loopIterPMF cond μ_body K)

theorem Cslib.WordRAM.loopIterPMF_of_not_holds {r : ℕ} {cond : Cond r} {μ_body : Data r → PMF (Data r)} {x : Data r} (hc : ¬cond.Holds x) (K : ℕ) : loopIterPMF cond μ_body K x = PMF.pure x

theorem Cslib.WordRAM.loopIterPMF_succ_right {r : ℕ} (cond : Cond r) (μ_body : Data r → PMF (Data r)) (K : ℕ) (x : Data r) : loopIterPMF cond μ_body (K + 1) x = (loopIterPMF cond μ_body K x).bind (loopStepPMF cond μ_body)

theorem Cslib.WordRAM.loopIterPMF_mono_of_not_holds {r : ℕ} (cond : Cond r) (μ_body : Data r → PMF (Data r)) (x : Data r) {y : Data r} (hy : ¬cond.Holds y) : Monotone fun (K : ℕ) => (loopIterPMF cond μ_body K x) y

theorem Cslib.WordRAM.loopIterPMF_indicator_mono {r : ℕ} (cond : Cond r) (μ_body : Data r → PMF (Data r)) (x y : Data r) : Monotone fun (K : ℕ) => {z : Data r | ¬cond.Holds z}.indicator (⇑(loopIterPMF cond μ_body K x)) y

def Cslib.WordRAM.LoopStateInv {r : ℕ} (cond : Cond r) (I Q : Data r → Prop) (x : Data r) : Prop

Combined loop state invariant: either active (cond.Holds x ∧ I x) or exited (¬cond.Holds x ∧ Q x).

theorem Cslib.WordRAM.loopIterPMF_support_inv {r : ℕ} {cond : Cond r} {I Q : Data r → Prop} {μ_body : Data r → PMF (Data r)} (hinv : ∀ (x : Data r), I x → cond.Holds x → ∀ y ∈ (μ_body x).support, LoopStateInv cond I Q y) (K : ℕ) {x : Data r} (hx : LoopStateInv cond I Q x) (y : Data r) : y ∈ (loopIterPMF cond μ_body K x).support → LoopStateInv cond I Q y

theorem Cslib.WordRAM.hasSum_loopExitDensity {r : ℕ} {cond : Cond r} {I Q : Data r → Prop} {μ_body : Data r → PMF (Data r)} {p_exit : ENNReal} (hp_pos : 0 < p_exit) (hp_top : p_exit ≠ ⊤) (hinv : ∀ (x : Data r), I x → cond.Holds x → ∀ y ∈ (μ_body x).support, LoopStateInv cond I Q y) (hp_exit : ∀ (x : Data r), I x → cond.Holds x → p_exit ≤ (μ_body x).toOuterMeasure {y : Data r | ¬cond.Holds y}) {x : Data r} (hx : LoopStateInv cond I Q x) : HasSum (fun (y : Data r) => ⨆ (K : ℕ), {z : Data r | ¬cond.Holds z}.indicator (⇑(loopIterPMF cond μ_body K x)) y) 1

noncomputable def Cslib.WordRAM.loopExitPMF {r : ℕ} (cond : Cond r) (μ_body : Data r → PMF (Data r)) (x : Data r) : PMF (Data r)

Limiting exit distribution of Code.loop cond body starting from x under one-step body distribution family μ_body.

theorem Cslib.WordRAM.loopExitPMF_apply_of_hasSum {r : ℕ} {cond : Cond r} {μ_body : Data r → PMF (Data r)} {x : Data r} (h : HasSum (fun (y : Data r) => ⨆ (K : ℕ), {z : Data r | ¬cond.Holds z}.indicator (⇑(loopIterPMF cond μ_body K x)) y) 1) (y : Data r) : (loopExitPMF cond μ_body x) y = ⨆ (K : ℕ), {z : Data r | ¬cond.Holds z}.indicator (⇑(loopIterPMF cond μ_body K x)) y

theorem Cslib.WordRAM.loopExitPMF_of_not_holds {r : ℕ} {cond : Cond r} {μ_body : Data r → PMF (Data r)} {x : Data r} (hc : ¬cond.Holds x) : loopExitPMF cond μ_body x = PMF.pure x

theorem Cslib.WordRAM.loopExitPMF_of_holds {r : ℕ} {cond : Cond r} {I Q : Data r → Prop} {μ_body : Data r → PMF (Data r)} {p_exit : ENNReal} (hp_pos : 0 < p_exit) (hp_top : p_exit ≠ ⊤) (hinv : ∀ (x : Data r), I x → cond.Holds x → ∀ y ∈ (μ_body x).support, LoopStateInv cond I Q y) (hp_exit : ∀ (x : Data r), I x → cond.Holds x → p_exit ≤ (μ_body x).toOuterMeasure {y : Data r | ¬cond.Holds y}) {x : Data r} (hIx : I x) (hcx : cond.Holds x) : loopExitPMF cond μ_body x = (μ_body x).bind (loopExitPMF cond μ_body)

theorem Cslib.WordRAM.mem_support_loopExitPMF {r : ℕ} {cond : Cond r} {I Q : Data r → Prop} {μ_body : Data r → PMF (Data r)} {p_exit : ENNReal} (hp_pos : 0 < p_exit) (hp_top : p_exit ≠ ⊤) (hinv : ∀ (x : Data r), I x → cond.Holds x → ∀ y ∈ (μ_body x).support, LoopStateInv cond I Q y) (hp_exit : ∀ (x : Data r), I x → cond.Holds x → p_exit ≤ (μ_body x).toOuterMeasure {y : Data r | ¬cond.Holds y}) {x : Data r} (hx : LoopStateInv cond I Q x) {y : Data r} (hy : y ∈ (loopExitPMF cond μ_body x).support) : (¬cond.Holds y ∧ Q y) ∧ ∃ (K : ℕ), y ∈ (loopIterPMF cond μ_body K x).support

Compositional distributional execution (ExecCodeDist)

inductive Cslib.WordRAM.ExecCodeDist {B : Basis} {r : ℕ} (w : ℕ) : Code B r → Data r → PMF (Data r) → ENNReal → Prop

ExecCodeDist w c x μ T: at word size w, running structured program c from data x terminates almost surely without faulting, realizes exit distribution μ : PMF (Data r) at the fallthrough address pc + c.size of any containing flat program, and uses at most T : ℝ≥0∞ expected instructions.

Unlike ExecRand, which requires a finite-depth computation tree, ExecCodeDist includes unbounded Las Vegas while loops whose each active iteration exits with probability bounded below by p_exit > 0 (ExecCodeDist.loop_geometric).

• of_execRand {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} {m : ProbComp (Data r × ℕ)} : ExecRand w c x m → ExecCodeDist w c x (Prod.fst <$> m).eval (m.expect fun (z : Data r × ℕ) => ↑z.2)
• mono {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} {μ : PMF (Data r)} {T T' : ENNReal} : ExecCodeDist w c x μ T → T ≤ T' → ExecCodeDist w c x μ T'
• seq {B : Basis} {r w : ℕ} {c₁ c₂ : Code B r} {x : Data r} {μ₁ : PMF (Data r)} {μ₂ : Data r → PMF (Data r)} {T₁ : ENNReal} {T₂ : Data r → ENNReal} : ExecCodeDist w c₁ x μ₁ T₁ → (∀ y ∈ μ₁.support, ExecCodeDist w c₂ y (μ₂ y) (T₂ y)) → ExecCodeDist w (c₁.seq c₂) x (μ₁.bind μ₂) (T₁ + ∑' (y : Data r), μ₁ y * T₂ y)
• branch_pos {B : Basis} {r w : ℕ} {cond : Cond r} {pos neg : Code B r} {x : Data r} {μ : PMF (Data r)} {T : ENNReal} : cond.Holds x → ExecCodeDist w pos x μ T → ExecCodeDist w (Code.branch cond pos neg) x μ (T + 1)
• branch_neg {B : Basis} {r w : ℕ} {cond : Cond r} {pos neg : Code B r} {x : Data r} {μ : PMF (Data r)} {T : ENNReal} : ¬cond.Holds x → ExecCodeDist w neg x μ T → ExecCodeDist w (Code.branch cond pos neg) x μ (T + 2)
• loop_geometric {B : Basis} {r w : ℕ} {cond : Cond r} {body : Code B r} (I Q : Data r → Prop) {μ_body : Data r → PMF (Data r)} {T_body : Data r → ENNReal} {B_body p_exit : ENNReal} {x : Data r} : 0 < p_exit → p_exit ≠ ⊤ → (∀ (z : Data r), I z → cond.Holds z → ExecCodeDist w body z (μ_body z) (T_body z)) → (∀ (z : Data r), I z → cond.Holds z → T_body z ≤ B_body) → (∀ (z : Data r), I z → cond.Holds z → ∀ y ∈ (μ_body z).support, LoopStateInv cond I Q y) → (∀ (z : Data r), I z → cond.Holds z → p_exit ≤ (μ_body z).toOuterMeasure {y : Data r | ¬cond.Holds y}) → LoopStateInv cond I Q x → ExecCodeDist w (Code.loop cond body) x (loopExitPMF cond μ_body x) ((B_body + 2) / p_exit + 2)

theorem Cslib.WordRAM.ExecCodeDist.congr_dist {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} {μ μ' : PMF (Data r)} {T T' : ENNReal} (h : ExecCodeDist w c x μ T) (hμ : μ = μ') (hT : T ≤ T') : ExecCodeDist w c x μ' T'

theorem Cslib.WordRAM.ExecCodeDist.of_exec {B : Basis} {r w : ℕ} {c : Code B r} {x y : Data r} {n : ℕ} (h : Exec w c x y n) : ExecCodeDist w c x (PMF.pure y) ↑n

Every deterministic Exec w c x y n gives ExecCodeDist w c x (PMF.pure y) n.

theorem Cslib.WordRAM.ExecCodeDist.of_execWithin {B : Basis} {r w : ℕ} {c : Code B r} {x y : Data r} {n : ℕ} (h : ExecWithin w c x y n) : ExecCodeDist w c x (PMF.pure y) ↑n

Every deterministic ExecWithin w c x y n gives ExecCodeDist w c x (PMF.pure y) n.

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

Single deterministic operation instruction.

theorem Cslib.WordRAM.ExecCodeDist.rand {B : Basis} {r w : ℕ} {x : Data r} {dst src : Fin r} (hfit : Fits w (x.regs src)) : ExecCodeDist w (Code.rand dst src) x (PMF.map (fun (k : Fin (x.regs src + 1)) => x.set dst ↑k) (ProbComp.unifFin (x.regs src)).eval) 1

Single rand dst src instruction.

theorem Cslib.WordRAM.ExecCodeDist.loop_exit {B : Basis} {r w : ℕ} {body : Code B r} {cond : Cond r} {x : Data r} (hc : ¬cond.Holds x) : ExecCodeDist w (Code.loop cond body) x (PMF.pure x) 2

Exiting a loop immediately when ¬cond.Holds x takes 2 steps and leaves x unchanged.

theorem Cslib.WordRAM.ExecCodeDist.seq_const {B : Basis} {r w : ℕ} {c₁ c₂ : Code B r} {x : Data r} {μ₁ : PMF (Data r)} {T₁ : ENNReal} {μ₂ : Data r → PMF (Data r)} {T₂ : Data r → ENNReal} {B₂ : ENNReal} (h₁ : ExecCodeDist w c₁ x μ₁ T₁) (h₂ : ∀ y ∈ μ₁.support, ExecCodeDist w c₂ y (μ₂ y) (T₂ y)) (hB₂ : ∀ y ∈ μ₁.support, T₂ y ≤ B₂) : ExecCodeDist w (c₁.seq c₂) x (μ₁.bind μ₂) (T₁ + B₂)

Sequencing with a uniform continuation step bound T₂.

theorem Cslib.WordRAM.ExecCodeDist.seq_pure {B : Basis} {r w : ℕ} {c₁ c₂ : Code B r} {x y : Data r} {μ : PMF (Data r)} {T₁ T₂ : ENNReal} (h₁ : ExecCodeDist w c₁ x (PMF.pure y) T₁) (h₂ : ExecCodeDist w c₂ y μ T₂) : ExecCodeDist w (c₁.seq c₂) x μ (T₁ + T₂)

Sequencing after a deterministic first stage (PMF.pure y).

theorem Cslib.WordRAM.ExecCodeDist.bounded {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} {μ : PMF (Data r)} {T : ENNReal} (h : ExecCodeDist w c x μ T) (hx : Data.Bounded w x) (y : Data r) : y ∈ μ.support → Data.Bounded w y

Every state in the support of μ preserves Data.Bounded w when x.Bounded w.

theorem Cslib.WordRAM.ExecCodeDist.regs_eq {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} {μ : PMF (Data r)} {T : ENNReal} {i : Fin r} (h : ExecCodeDist w c x μ T) (hi : Code.Preserves i c) (y : Data r) : y ∈ μ.support → y.regs i = x.regs i

Any register i not written by c (c.Preserves i) is preserved across the support of μ.

theorem Cslib.WordRAM.ExecCodeDist.mapSimulates {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} {μ : PMF (Data r)} {T : ENNReal} {B' : Basis} (ψ : B.Simulates B') (h : ExecCodeDist w c x μ T) : ExecCodeDist w (Code.mapSimulates ψ c) x μ T

Distributional executions transfer along any defined-evaluation basis simulation ψ : B.Simulates B'.

theorem Cslib.WordRAM.ExecCodeDist.rename {B : Basis} {r w : ℕ} {c : Code B r} {μ : PMF (Data r)} {T : ENNReal} {r' : ℕ} {f : Fin r → Fin r'} (hf : Function.Injective f) {x : Data r'} (h : ExecCodeDist w c (Data.comap f x) μ T) : ExecCodeDist w (Code.rename f c) x (PMF.map (fun (y : Data r) => Data.extend f y x) μ) T

Renaming a distributional execution along an injective register map f : Fin r → Fin r' transforms the output distribution via Data.extend f x and preserves the expected step bound.

Compilation of ExecCodeDist to flat Program semantics

theorem Cslib.WordRAM.ExecCodeDist.expectedStepsWithin_assemble {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} {μ : PMF (Data r)} {T : ENNReal} (h : ExecCodeDist w c x μ T) {p : Program B r} {pc : ℕ} (hp : p.Contains pc (c.assemble pc)) (N : ℕ) : expectedStepsWithin w p N (RandCfg.running { pc := pc, data := x }) ≤ T + ∑' (y : Data r), μ y * expectedStepsWithin w p N (RandCfg.running { pc := pc + c.size, data := y })

Finite-horizon Bellman inequality for ExecCodeDist inside any containing flat program p.

theorem Cslib.WordRAM.ExecCodeDist.expectedStepsFrom_assemble {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} {μ : PMF (Data r)} {T : ENNReal} (h : ExecCodeDist w c x μ T) {p : Program B r} {pc : ℕ} (hp : p.Contains pc (c.assemble pc)) : expectedStepsFrom w p (RandCfg.running { pc := pc, data := x }) ≤ T + ∑' (y : Data r), μ y * expectedStepsFrom w p (RandCfg.running { pc := pc + c.size, data := y })

Full-horizon Bellman inequality for ExecCodeDist inside any containing flat program p.

theorem Cslib.WordRAM.ExecCodeDist.expectedStepsFrom_le {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} {μ : PMF (Data r)} {T : ENNReal} (h : ExecCodeDist w c x μ T) {p : Program B r} {pc : ℕ} (hp : p.Contains pc (c.assemble pc)) {k : Data r → ENNReal} (hk : ∀ y ∈ μ.support, expectedStepsFrom w p (RandCfg.running { pc := pc + c.size, data := y }) ≤ k y) : expectedStepsFrom w p (RandCfg.running { pc := pc, data := x }) ≤ T + ∑' (y : Data r), μ y * k y

Continuation upper-bound form of expectedStepsFrom_assemble.

theorem Cslib.WordRAM.ExecCodeDist.evalRand_faulted_eq_zero {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} {μ : PMF (Data r)} {T : ENNReal} (h : ExecCodeDist w c x μ T) {p : Program B r} {pc T_hor : ℕ} (hp : p.Contains pc (c.assemble pc)) (hcont : ∀ y ∈ μ.support, ∀ t ≤ T_hor, (evalRand w p t { pc := pc + c.size, data := y }) RandCfg.faulted = 0) (t : ℕ) : t ≤ T_hor → (evalRand w p t { pc := pc, data := x }) RandCfg.faulted = 0

Along ExecCodeDist w c x μ T, if no continuation from ⟨pc + c.size, y⟩ faults within T_hor steps for any supported y ∈ μ.support, then running p from ⟨pc, x⟩ does not fault within T_hor steps.

theorem Cslib.WordRAM.ExecCodeDist.randFaultFree_assemble {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} {μ : PMF (Data r)} {T : ENNReal} (h : ExecCodeDist w c x μ T) {p : Program B r} {pc : ℕ} (hp : p.Contains pc (c.assemble pc)) (hcont : ∀ y ∈ μ.support, RandFaultFree w p { pc := pc + c.size, data := y }) : RandFaultFree w p { pc := pc, data := x }

If every continuation from ⟨pc + c.size, y⟩ (y ∈ μ.support) is fault-free at all horizons, then running p from ⟨pc, x⟩ is fault-free at all horizons.

theorem Cslib.WordRAM.ExecCodeDist.le_iSup_evalRand_halted {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} {μ : PMF (Data r)} {T : ENNReal} (h : ExecCodeDist w c x μ T) {p : Program B r} {pc : ℕ} (hp : p.Contains pc (c.assemble pc)) (v : ℕ) (d : Data r) : ∑' (y : Data r), μ y * ⨆ (T_hor : ℕ), (evalRand w p T_hor { pc := pc + c.size, data := y }) (RandCfg.halted v d) ≤ ⨆ (T_hor : ℕ), (evalRand w p T_hor { pc := pc, data := x }) (RandCfg.halted v d)

Along ExecCodeDist w c x μ T, the μ-weighted supremum halting probability from ⟨pc + c.size, y⟩ is a lower bound on the supremum halting probability from ⟨pc, x⟩.

theorem Cslib.WordRAM.ExecCodeDist.program_halts {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} {μ : PMF (Data r)} {T : ENNReal} (h : ExecCodeDist w c x μ T) (out : Fin r) : expectedTime w (c.program out) { pc := 0, data := x } ≤ T + 1 ∧ RandFaultFree w (c.program out) { pc := 0, data := x } ∧ (T ≠ ⊤ → AlmostSurelyHalts w (c.program out) { pc := 0, data := x }) ∧ ∀ (y : Data r), μ y ≤ ⨆ (T_hor : ℕ), (evalRand w (c.program out) T_hor { pc := 0, data := x }) (RandCfg.halted (y.regs out) y)

Compiling ExecCodeDist w c x μ T with c.program out yields:

1. expectedTime w (c.program out) ⟨0, x⟩ ≤ T + 1,
2. RandFaultFree w (c.program out) ⟨0, x⟩,
3. AlmostSurelyHalts w (c.program out) ⟨0, x⟩ whenever T ≠ ⊤, and
4. for every y : Data r, μ y ≤ ⨆ T_hor : ℕ, evalRand w (c.program out) T_hor ⟨0, x⟩ (.halted (y.regs out) y).

theorem Cslib.WordRAM.expectedStepsFrom_loop_le_of_geometric {B : Basis} {r w : ℕ} {cond : Cond r} {body : Code B r} (I Q : Data r → Prop) {μ_body : Data r → PMF (Data r)} {T_body : Data r → ENNReal} {B_body p_exit : ENNReal} {x : Data r} (hp_pos : 0 < p_exit) (hp_top : p_exit ≠ ⊤) (hbody : ∀ (z : Data r), I z → cond.Holds z → ExecCodeDist w body z (μ_body z) (T_body z)) (hB : ∀ (z : Data r), I z → cond.Holds z → T_body z ≤ B_body) (hinv : ∀ (z : Data r), I z → cond.Holds z → ∀ y ∈ (μ_body z).support, LoopStateInv cond I Q y) (hp_exit : ∀ (z : Data r), I z → cond.Holds z → p_exit ≤ (μ_body z).toOuterMeasure {y : Data r | ¬cond.Holds y}) (hx_inv : LoopStateInv cond I Q x) {p : Program B r} {pc : ℕ} (hp : p.Contains pc ((Code.loop cond body).assemble pc)) {k : Data r → ENNReal} (hk : ∀ (y : Data r), ¬cond.Holds y → Q y → expectedStepsFrom w p (RandCfg.running { pc := pc + (Code.loop cond body).size, data := y }) ≤ k y) : expectedStepsFrom w p (RandCfg.running { pc := pc, data := x }) ≤ (B_body + 2) / p_exit + 2 + ∑' (y : Data r), (loopExitPMF cond μ_body x) y * k y

Geometric Las Vegas loop expected-step bound inside any flat program p containing (Code.loop cond body).assemble pc.