Structured randomized word-RAM programs

Cslib.WordRAM.ExecRand w c x m is the randomized counterpart of Cslib.WordRAM.Exec: at word size w, running the structured program c : Code B r from x : Data r terminates without faulting on every path and yields the ProbComp (Data r × ℕ) computation m, pairing each final machine data y with the exact number of compiled instructions n executed along that path.

Cslib.WordRAM.ExecRandWithin w c x P T R bundles ExecRand with a pathwise postcondition P, a worst-case instruction budget T, and a worst-case rand-call budget R (IsQueryBounded), supporting Hoare-style rules for data instructions, rand, sequencing, branches, and potential loops (ExecRandWithin.loop_potential).

Every structured randomized execution refines Code.assemble (ExecRand.runRand_assemble) and compiles via Code.program out to a flat Program B r establishing RandHaltsWithin, RandCallsBounded, and the memory postcondition P directly on RandCfg.halted (ExecRandWithin.program).

Main definitions

• Cslib.WordRAM.ExecRand: exact randomized execution of Code B r into ProbComp (Data r × ℕ).
• Cslib.WordRAM.codeComp: canonical ProbComp (Data r × ℕ) associated with (w, c, x).
• Cslib.WordRAM.ExecRandWithin: pathwise postcondition, worst-case instruction bound, and rand-call budget on Code B r.

Main results

• Cslib.WordRAM.ExecRand.unique: m is uniquely determined by (w, c, x).
• Cslib.WordRAM.Exec.execRand, Cslib.WordRAM.ExecWithin.execRandWithin: deterministic structured executions lift with zero rand calls.
• Cslib.WordRAM.ExecRandWithin.loop_potential: potential-based termination, worst-case time, and rand-call rule for randomized loops.
• Cslib.WordRAM.ExecRand.runRand_assemble, Cslib.WordRAM.ExecRand.runRand_program, Cslib.WordRAM.Exec.runRand_program, Cslib.WordRAM.ExecRandWithin.program: assembly refinement into flat runRand, RandHaltsWithin, and RandCallsBounded.

References

• T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, Introduction to Algorithms
• M. Mitzenmacher and E. Upfal, Probability and Computing

Structured randomized executions

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

ExecRand w c x m: at word size w, the structured program c runs from data x without faulting on any path and induces the ProbComp (Data r × ℕ) computation m of (finalData, steps) matching the exact instruction counts of Code.assemble.

• op {B : Basis} {r w : ℕ} {o : Op B r} {x y : Data r} (h : Op.eval w o x = some y) : ExecRand w (Code.op o) x (pure (y, 1))

  A data instruction executes in 1 instruction and issues 0 calls.

• rand {B : Basis} {r w : ℕ} {dst src : Fin r} {x : Data r} (h : Fits w (x.regs src)) : ExecRand w (Code.rand dst src) x do let k ← ProbComp.unifFin (x.regs src) pure (x.set dst ↑k, 1)

  Code.rand dst src draws uniformly from [0, x.regs src] in 1 instruction when the bound fits a word.

• seq {B : Basis} {r w : ℕ} {c₁ c₂ : Code B r} {x : Data r} {m₁ : ProbComp (Data r × ℕ)} {m₂ : Data r → ProbComp (Data r × ℕ)} (h₁ : ExecRand w c₁ x m₁) (h₂ : ∀ z ∈ OracleComp.support m₁, ExecRand w c₂ z.1 (m₂ z.1)) : ExecRand w (c₁.seq c₂) x do let z₁ ← m₁ let z₂ ← m₂ z₁.1 pure (z₂.1, z₁.2 + z₂.2)

  Sequencing composes the two computations and adds their instruction counts.

• branch_pos {B : Basis} {r w : ℕ} {c : Cond r} {pos neg : Code B r} {x : Data r} {m : ProbComp (Data r × ℕ)} (hc : c.Holds x) (h : ExecRand w pos x m) : ExecRand w (Code.branch c pos neg) x ((fun (z : Data r × ℕ) => (z.1, z.2 + 1)) <$> m)

  Taking the positive branch adds 1 instruction for the branch test.

• branch_neg {B : Basis} {r w : ℕ} {c : Cond r} {pos neg : Code B r} {x : Data r} {m : ProbComp (Data r × ℕ)} (hc : ¬c.Holds x) (h : ExecRand w neg x m) : ExecRand w (Code.branch c pos neg) x ((fun (z : Data r × ℕ) => (z.1, z.2 + 2)) <$> m)

  Taking the negative branch adds 2 instructions (branch test and jump past pos).

• loop_exit {B : Basis} {r w : ℕ} {c : Cond r} {body : Code B r} {x : Data r} (hc : ¬c.Holds x) : ExecRand w (Code.loop c body) x (pure (x, 2))

  Exiting a loop when the condition fails takes 2 instructions (branch test and exit jump).

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

  Entering a loop executes body, jumps back to the header, and continues the loop, adding 2 instructions for the branch test and back-jump.

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

The ProbComp tree of a structured execution is uniquely determined by (w, c, x).

theorem Cslib.WordRAM.ExecRand.pos {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} {m : ProbComp (Data r × ℕ)} (h : ExecRand w c x m) {z : Data r × ℕ} (hz : z ∈ OracleComp.support m) : 1 ≤ z.2

Every structured execution takes at least 1 instruction on every path.

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

Structured randomized executions preserve word-boundedness on every supported path.

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

A register that c does not write retains its value on every supported path.

noncomputable def Cslib.WordRAM.codeComp {B : Basis} {r : ℕ} (w : ℕ) (c : Code B r) (x : Data r) : ProbComp (Data r × ℕ)

Canonical ProbComp (Data r × ℕ) of a structured program c from x when ExecRand w c x m holds for some m (unique by ExecRand.unique), and pure (x, 0) otherwise.

theorem Cslib.WordRAM.ExecRand.codeComp_eq {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} {m : ProbComp (Data r × ℕ)} (h : ExecRand w c x m) : codeComp w c x = m

When ExecRand w c x m holds, codeComp w c x equals m.

theorem Cslib.WordRAM.Exec.execRand {B : Basis} {r w : ℕ} {c : Code B r} {x y : Data r} {n : ℕ} (h : Exec w c x y n) : ExecRand w c x (pure (y, n))

Every deterministic structured execution Exec w c x y n lifts to ExecRand w c x (pure (y, n)).

theorem Cslib.WordRAM.Exec.seqRand {B : Basis} {r w : ℕ} {c₁ c₂ : Code B r} {x y : Data r} {n₁ : ℕ} {m₂ : ProbComp (Data r × ℕ)} (h₁ : Exec w c₁ x y n₁) (h₂ : ExecRand w c₂ y m₂) : ExecRand w (c₁.seq c₂) x ((fun (z : Data r × ℕ) => (z.1, n₁ + z.2)) <$> m₂)

Prepending a deterministic Exec onto a randomized ExecRand shifts the instruction count by n₁.

Renaming registers in structured randomized executions

theorem Cslib.WordRAM.ExecRand.rename {B : Basis} {r r' : ℕ} {f : Fin r → Fin r'} (hf : Function.Injective f) {w : ℕ} {c : Code B r} {x : Data r'} {m : ProbComp (Data r × ℕ)} (h : ExecRand w c (Data.comap f x) m) : ExecRand w (Code.rename f c) x ((fun (z : Data r × ℕ) => (Data.extend f z.1 x, z.2)) <$> m)

Running a structured randomized program through an injective register map f transforms its outputs via Data.extend f x, preserving instruction counts and untouched registers.

Hoare-style bounded structured execution (ExecRandWithin)

def Cslib.WordRAM.ExecRandWithin {B : Basis} {r : ℕ} (w : ℕ) (c : Code B r) (x : Data r) (P : Data r → Prop) (T R : ℕ) : Prop

ExecRandWithin w c x P T R: at word size w, running c from x terminates cleanly on every path (ExecRand), makes at most R rand calls on every path, and every supported outcome (y, n) satisfies P y and n ≤ T.

theorem Cslib.WordRAM.ExecWithin.execRandWithin {B : Basis} {r w T : ℕ} {c : Code B r} {x y : Data r} {P : Data r → Prop} (h : ExecWithin w c x y T) (hy : P y) : ExecRandWithin w c x P T 0

Every deterministic ExecWithin lifts to ExecRandWithin with 0 rand calls.

theorem Cslib.WordRAM.ExecRandWithin.mono {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} {P Q : Data r → Prop} {T T' R R' : ℕ} (h : ExecRandWithin w c x P T R) (hPQ : ∀ (y : Data r), P y → Q y) (hT : T ≤ T') (hR : R ≤ R') : ExecRandWithin w c x Q T' R'

Monotonicity / consequence rule for ExecRandWithin.

theorem Cslib.WordRAM.ExecRandWithin.withBounded {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} {P : Data r → Prop} {T R : ℕ} (h : ExecRandWithin w c x P T R) (hx : Data.Bounded w x) : ExecRandWithin w c x (fun (y : Data r) => P y ∧ Data.Bounded w y) T R

Strengthening P with Data.Bounded w when x.Bounded w holds initially.

theorem Cslib.WordRAM.ExecRandWithin.withPreserves {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} {P : Data r → Prop} {T R : ℕ} {i : Fin r} (h : ExecRandWithin w c x P T R) (hi : Code.Preserves i c) : ExecRandWithin w c x (fun (y : Data r) => P y ∧ y.regs i = x.regs i) T R

Strengthening P with preservation of a register i not written by c.

theorem Cslib.WordRAM.ExecRandWithin.op {B : Basis} {r w : ℕ} {x : Data r} {P : Data r → Prop} {o : Op B r} {y : Data r} (ho : Op.eval w o x = some y) (hy : P y) : ExecRandWithin w (Code.op o) x P 1 0

A single op instruction runs in 1 step and 0 rand calls.

theorem Cslib.WordRAM.ExecRandWithin.rand {B : Basis} {r w : ℕ} {x : Data r} {P : Data r → Prop} {dst src : Fin r} (hfit : Fits w (x.regs src)) (hk : ∀ (k : Fin (x.regs src + 1)), P (x.set dst ↑k)) : ExecRandWithin w (Code.rand dst src) x P 1 1

Code.rand dst src runs in 1 step and 1 rand call when x.regs src fits a word.

theorem Cslib.WordRAM.ExecRandWithin.seq {B : Basis} {r w : ℕ} {c₁ c₂ : Code B r} {x : Data r} {P Q : Data r → Prop} {T₁ T₂ R₁ R₂ : ℕ} (h₁ : ExecRandWithin w c₁ x P T₁ R₁) (h₂ : ∀ (y : Data r), P y → ExecRandWithin w c₂ y Q T₂ R₂) : ExecRandWithin w (c₁.seq c₂) x Q (T₁ + T₂) (R₁ + R₂)

Sequencing rule: composes ExecRandWithin specs and sums both step and call budgets.

theorem Cslib.WordRAM.ExecRandWithin.branch_pos {B : Basis} {r w : ℕ} {pos neg : Code B r} {cond : Cond r} {x : Data r} {P : Data r → Prop} {T R : ℕ} (hc : cond.Holds x) (h : ExecRandWithin w pos x P T R) : ExecRandWithin w (Code.branch cond pos neg) x P (T + 1) R

Positive branch rule (+1 step, same call budget).

theorem Cslib.WordRAM.ExecRandWithin.branch_neg {B : Basis} {r w : ℕ} {pos neg : Code B r} {cond : Cond r} {x : Data r} {P : Data r → Prop} {T R : ℕ} (hc : ¬cond.Holds x) (h : ExecRandWithin w neg x P T R) : ExecRandWithin w (Code.branch cond pos neg) x P (T + 2) R

Negative branch rule (+2 steps, same call budget).

theorem Cslib.WordRAM.ExecRandWithin.branch {B : Basis} {r w : ℕ} {pos neg : Code B r} {cond : Cond r} {x : Data r} {P : Data r → Prop} {T R : ℕ} (hpos : cond.Holds x → ExecRandWithin w pos x P T R) (hneg : ¬cond.Holds x → ExecRandWithin w neg x P T R) : ExecRandWithin w (Code.branch cond pos neg) x P (T + 2) R

Combined branch rule with common budgets (T + 2, R).

theorem Cslib.WordRAM.ExecRandWithin.loop_exit {B : Basis} {r w : ℕ} {body : Code B r} {cond : Cond r} {x : Data r} {P : Data r → Prop} (hc : ¬cond.Holds x) (hx : P x) : ExecRandWithin w (Code.loop cond body) x P 2 0

Exiting a loop when the condition fails takes 2 steps and 0 rand calls.

theorem Cslib.WordRAM.ExecRandWithin.loop_iter {B : Basis} {r w : ℕ} {body : Code B r} {cond : Cond r} {x : Data r} {P Q : Data r → Prop} {T₁ T₂ R₁ R₂ : ℕ} (hc : cond.Holds x) (hb : ExecRandWithin w body x P T₁ R₁) (hl : ∀ (y : Data r), P y → ExecRandWithin w (Code.loop cond body) y Q T₂ R₂) : ExecRandWithin w (Code.loop cond body) x Q (T₁ + T₂ + 2) (R₁ + R₂)

One iteration of a loop followed by the rest adds T₁ + 2 steps and R₁ + R₂ calls.

theorem Cslib.WordRAM.ExecRandWithin.loop_potential {B : Basis} {r w : ℕ} {body : Code B r} {cond : Cond r} {x : Data r} (I : Data r → Prop) (Φ Ψ : Data r → ℕ) (hbody : ∀ (x : Data r), I x → cond.Holds x → ∃ (T_b : ℕ) (R_b : ℕ), ExecRandWithin w body x (fun (y : Data r) => I y ∧ T_b + 2 + Φ y ≤ Φ x ∧ R_b + Ψ y ≤ Ψ x) T_b R_b) (hx : I x) : ExecRandWithin w (Code.loop cond body) x (fun (y : Data r) => I y ∧ ¬cond.Holds y) (Φ x + 2) (Ψ x)

Potential rule for randomized loops. Suppose every state x satisfying I x and cond.Holds x runs body within some T_b instructions and R_b rand calls such that every supported successor y satisfies I y, T_b + 2 + Φ y ≤ Φ x, and R_b + Ψ y ≤ Ψ x. Then from any x satisfying I x, .loop cond body terminates within Φ x + 2 instructions and Ψ x rand calls, reaching a state y with I y ∧ ¬cond.Holds y.

theorem Cslib.WordRAM.ExecRandWithin.rename {B : Basis} {r r' w : ℕ} {c : Code B r} {P : Data r → Prop} {T R : ℕ} {f : Fin r → Fin r'} (hf : Function.Injective f) {x : Data r'} (h : ExecRandWithin w c (Data.comap f x) P T R) : ExecRandWithin w (Code.rename f c) x (fun (y' : Data r') => ∃ (y : Data r), P y ∧ y' = Data.extend f y x) T R

Renaming a ExecRandWithin specification along an injective register map f.

Compilation to flat runRand, RandHaltsWithin, and RandCallsBounded

theorem Cslib.WordRAM.ExecRand.runRand_assemble {B : Basis} {r w : ℕ} {p : Program B r} {c : Code B r} {x : Data r} {m : ProbComp (Data r × ℕ)} {pc T : ℕ} (h : ExecRand w c x m) (hp : p.Contains pc (c.assemble pc)) (hT : ∀ z ∈ OracleComp.support m, z.2 ≤ T) : runRand w p T (RandCfg.running { pc := pc, data := x }) = do let z ← m runRand w p (T - z.2) (RandCfg.running { pc := pc + c.size, data := z.1 })

Randomized assembly is exact. Running a flat program p containing c.assemble pc at pc for T steps (where every path of m uses at most T steps) is equal in ProbComp to sampling (y, n) ← m and continuing from ⟨pc + c.size, y⟩ for the remaining T - n steps.

theorem Cslib.WordRAM.ExecRand.runRand_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) {T : ℕ} (hT : ∀ z ∈ OracleComp.support m, z.2 + 1 ≤ T) : runRand w (c.program out) T (RandCfg.running { pc := 0, data := x }) = (fun (z : Data r × ℕ) => RandCfg.halted (z.1.regs out) z.1) <$> m

Compiling c with Code.program out maps every (y, n) of m to .halted (y.regs out) y once T ≥ n + 1 on every path.

theorem Cslib.WordRAM.Exec.runRand_program {B : Basis} {r w : ℕ} {c : Code B r} {x y : Data r} {n T : ℕ} (h : Exec w c x y n) (out : Fin r) (hT : n + 1 ≤ T) : runRand w (c.program out) T (RandCfg.running { pc := 0, data := x }) = pure (RandCfg.halted (y.regs out) y)

Structured deterministic corollary: a compiled Exec w c x y n halts cleanly under runRand with output y.regs out and final machine data y at any fuel T ≥ n + 1.

theorem Cslib.WordRAM.ExecRandWithin.program {B : Basis} {r w : ℕ} {c : Code B r} {x : Data r} {P : Data r → Prop} {T T' R : ℕ} (h : ExecRandWithin w c x P T R) (out : Fin r) (hT : T + 1 ≤ T') : RandHaltsWithin w (c.program out) { pc := 0, data := x } T' ∧ RandCallsBounded w (c.program out) { pc := 0, data := x } T' R ∧ ∀ cfg ∈ OracleComp.support (runRand w (c.program out) T' (RandCfg.running { pc := 0, data := x })), ∃ (y : Data r), cfg = RandCfg.halted (y.regs out) y ∧ P y

Compiling an ExecRandWithin w c x P T R certificate via c.program out yields RandHaltsWithin, RandCallsBounded, and pathwise P on the halting data at any fuel T' ≥ T + 1.