Randomized word RAMs

A randomized word RAM executes a Cslib.WordRAM.Program B r at word size w, interpreting Instr.rand dst src as drawing a uniform integer in [0, regs src] (ProbComp.unifFin) when regs src < 2 ^ w (Fits w (regs src)), writing the sample to dst, advancing pc by 1, and charging one instruction and one rand call. When regs src ≥ 2 ^ w on an unbounded raw state, Instr.rand faults; on any word-bounded state (Data.Bounded w), regs src < 2 ^ w holds automatically and Instr.rand preserves Data.Bounded w. Note that rand(0) succeeds without faulting, writes 0, and still charges one instruction and one rand call (unifBitCost 0 = 0 entropy bits).

Following Cslib.OracleComp, clocked T-step execution runRand is defined as a terminating program in ProbComp (RandCfg r) (= OracleComp unifSpec (RandCfg r)), and its configuration distribution evalRand in PMF (RandCfg r) is obtained via the monad morphism ProbComp.eval. Unlike deterministic Outcome.halt (which carries only the scalar output), the absorbing randomized configuration RandCfg r records the final Data r alongside the scalar output (RandCfg.halted v data) so flat-program theorems can assert in-place memory postconditions directly.

On rand-free programs (Program.IsRandFree), runRand makes zero oracle calls and agrees in both directions with deterministic Runs/Executes (runRand_eq_pure_halted_iff_of_isRandFree, exists_data_runRand_eq_pure_halted_iff_executes_of_isRandFree). Conversely, any deterministic halting run lifts unconditionally to runRand without IsRandFree because a deterministic run never executes Instr.rand (runRand_eq_pure_halted_of_runs_halt).

Main definitions

• Cslib.WordRAM.RandCfg, Cslib.WordRAM.RandCfg.ofOutcome: absorbing randomized machine configuration (running, halted v data, faulted) and lifting from deterministic Outcome.
• Cslib.WordRAM.stepRand, Cslib.WordRAM.runRand, Cslib.WordRAM.evalRand: single-step and clocked T-step randomized execution in ProbComp and PMF.
• Cslib.WordRAM.RandFaultFree, Cslib.WordRAM.RandHaltsWithin: zero-fault invariant and worst-case step bound.
• Cslib.WordRAM.RandCallsBounded, Cslib.WordRAM.unifBitCost, Cslib.WordRAM.RandBitsBounded: worst-case rand-call and entropy-bit budgets via OracleComp.IsQueryBounded and OracleComp.IsCostBounded.

Main results

• Cslib.WordRAM.runRand_add: clocked runs compose additively in ProbComp.
• Cslib.WordRAM.runRand_bounded_init: from an input that fits w, every supported configuration remains word-bounded.
• Cslib.WordRAM.runRand_eq_pure_halted_of_runs_halt: deterministic halting runs lift unconditionally to runRand with the halting state's Data r.
• Cslib.WordRAM.runRand_isQueryBounded_zero_of_isRandFree: rand-free programs issue zero queries.
• Cslib.WordRAM.runRand_eq_pure_halted_iff_of_isRandFree, Cslib.WordRAM.exists_data_runRand_eq_pure_halted_iff_executes_of_isRandFree: two-way agreement with deterministic semantics on rand-free programs.
• Cslib.WordRAM.RandCallsBounded.randBitsBounded: R rand calls at word size w use at most R * w entropy bits.

References

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

Randomized configurations and single step

inductive Cslib.WordRAM.RandCfg (r : ℕ) : Type

Absorbing machine configuration for clocked randomized execution. Retains the halting Data r alongside the scalar output v so flat-program specifications can inspect final memory without changing deterministic Outcome.halt.

• running {r : ℕ} (s : State r) : RandCfg r

  Active execution at machine state s.

• halted {r : ℕ} (v : ℕ) (data : Data r) : RandCfg r

  Halted with output word v and final machine data data.

• faulted {r : ℕ} : RandCfg r

  Faulted on an invalid operation, out-of-range constant/sample, or out-of-bounds pc.

def Cslib.WordRAM.RandCfg.ofOutcome {r : ℕ} (x : Data r) : Outcome r → RandCfg r

Lift a deterministic Outcome from pre-step data x (halt i does not mutate x).

def Cslib.WordRAM.RandCfg.Bounded {r : ℕ} (w : ℕ) : RandCfg r → Prop

Word-boundedness lifted to randomized configurations.

def Cslib.WordRAM.stepRand {B : Basis} {r : ℕ} (w : ℕ) (p : Program B r) : RandCfg r → ProbComp (RandCfg r)

One step of randomized execution at word size w. Halted and faulted configurations are absorbing (pure, issuing zero queries), and every non-rand instruction delegates to deterministic step. Left unmarked by @[simp] because unfolding the program lookup and instruction dispatch at symbolic program counters blows up step-level goals; rewrite via the instruction-specific stepRand_* lemmas instead.

theorem Cslib.WordRAM.stepRand_halted {B : Basis} {r w : ℕ} {p : Program B r} (v : ℕ) (d : Data r) : stepRand w p (RandCfg.halted v d) = pure (RandCfg.halted v d)

theorem Cslib.WordRAM.stepRand_faulted {B : Basis} {r w : ℕ} {p : Program B r} : stepRand w p RandCfg.faulted = pure RandCfg.faulted

theorem Cslib.WordRAM.stepRand_none {B : Basis} {r w : ℕ} {p : Program B r} {s : State r} (hp : p[s.pc]? = none) : stepRand w p (RandCfg.running s) = pure RandCfg.faulted

theorem Cslib.WordRAM.stepRand_op {B : Basis} {r w : ℕ} {p : Program B r} {s : State r} {o : Op B r} {x : Data r} (hp : p[s.pc]? = some (Instr.op o)) (h : Op.eval w o s.data = some x) : stepRand w p (RandCfg.running s) = pure (RandCfg.running { pc := s.pc + 1, data := x })

theorem Cslib.WordRAM.stepRand_op_fault {B : Basis} {r w : ℕ} {p : Program B r} {s : State r} {o : Op B r} (hp : p[s.pc]? = some (Instr.op o)) (h : Op.eval w o s.data = none) : stepRand w p (RandCfg.running s) = pure RandCfg.faulted

theorem Cslib.WordRAM.stepRand_jump {B : Basis} {r w : ℕ} {p : Program B r} {s : State r} {t : ℕ} (hp : p[s.pc]? = some (Instr.jump t)) : stepRand w p (RandCfg.running s) = pure (RandCfg.running { pc := t, data := s.data })

theorem Cslib.WordRAM.stepRand_branch {B : Basis} {r w : ℕ} {p : Program B r} {s : State r} {c : Cond r} {t : ℕ} (hp : p[s.pc]? = some (Instr.branch c t)) : stepRand w p (RandCfg.running s) = pure (RandCfg.running { pc := if c.Holds s.data then t else s.pc + 1, data := s.data })

theorem Cslib.WordRAM.stepRand_halt {B : Basis} {r w : ℕ} {p : Program B r} {s : State r} {i : Fin r} (hp : p[s.pc]? = some (Instr.halt i)) : stepRand w p (RandCfg.running s) = pure (RandCfg.halted (s.data.regs i) s.data)

theorem Cslib.WordRAM.stepRand_rand_of_fits {B : Basis} {r w : ℕ} {p : Program B r} {s : State r} {dst src : Fin r} (hp : p[s.pc]? = some (Instr.rand dst src)) (hfit : Fits w (s.data.regs src)) : stepRand w p (RandCfg.running s) = do let k ← ProbComp.unifFin (s.data.regs src) pure (RandCfg.running { pc := s.pc + 1, data := s.data.set dst ↑k })

theorem Cslib.WordRAM.stepRand_rand_of_not_fits {B : Basis} {r w : ℕ} {p : Program B r} {s : State r} {dst src : Fin r} (hp : p[s.pc]? = some (Instr.rand dst src)) (hfit : ¬Fits w (s.data.regs src)) : stepRand w p (RandCfg.running s) = pure RandCfg.faulted

theorem Cslib.WordRAM.stepRand_of_step_eq_next {B : Basis} {r w : ℕ} {p : Program B r} {s t : State r} (h : step w p s = Outcome.next t) : stepRand w p (RandCfg.running s) = pure (RandCfg.running t)

A deterministic step (any non-faulting outcome of WordRAM.step) agrees unconditionally with stepRand.

theorem Cslib.WordRAM.stepRand_of_step_eq_halt {B : Basis} {r w : ℕ} {p : Program B r} {s : State r} {v : ℕ} (h : step w p s = Outcome.halt v) : stepRand w p (RandCfg.running s) = pure (RandCfg.halted v s.data)

A deterministic halt step agrees unconditionally with stepRand, retaining s.data.

Clocked randomized runs and output distribution

@[irreducible]

def Cslib.WordRAM.runRand {B : Basis} {r : ℕ} (w : ℕ) (p : Program B r) : ℕ → RandCfg r → ProbComp (RandCfg r)

Clocked T-step randomized execution from configuration cfg.

noncomputable def Cslib.WordRAM.evalRand {B : Basis} {r : ℕ} (w : ℕ) (p : Program B r) (T : ℕ) (s : State r) : PMF (RandCfg r)

T-step configuration distribution from initial machine state s.

@[simp]

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

theorem Cslib.WordRAM.runRand_succ {B : Basis} {r : ℕ} (w : ℕ) (p : Program B r) (T : ℕ) (cfg : RandCfg r) : runRand w p (T + 1) cfg = do let cfg' ← stepRand w p cfg runRand w p T cfg'

@[simp]

theorem Cslib.WordRAM.runRand_halted {B : Basis} {r : ℕ} (w : ℕ) (p : Program B r) (T v : ℕ) (d : Data r) : runRand w p T (RandCfg.halted v d) = pure (RandCfg.halted v d)

@[simp]

theorem Cslib.WordRAM.runRand_faulted {B : Basis} {r : ℕ} (w : ℕ) (p : Program B r) (T : ℕ) : runRand w p T RandCfg.faulted = pure RandCfg.faulted

theorem Cslib.WordRAM.runRand_add {B : Basis} {r : ℕ} (w : ℕ) (p : Program B r) (T₁ T₂ : ℕ) (cfg : RandCfg r) : runRand w p (T₁ + T₂) cfg = do let cfg' ← runRand w p T₁ cfg runRand w p T₂ cfg'

Clocked runs compose additively in ProbComp.

@[simp]

theorem Cslib.WordRAM.evalRand_zero {B : Basis} {r : ℕ} (w : ℕ) (p : Program B r) (s : State r) : evalRand w p 0 s = PMF.pure (RandCfg.running s)

theorem Cslib.WordRAM.evalRand_succ {B : Basis} {r : ℕ} (w : ℕ) (p : Program B r) (T : ℕ) (s : State r) : evalRand w p (T + 1) s = (stepRand w p (RandCfg.running s)).eval.bind fun (cfg : RandCfg r) => (runRand w p T cfg).eval

theorem Cslib.WordRAM.support_evalRand {B : Basis} {r : ℕ} (w : ℕ) (p : Program B r) (T : ℕ) (s : State r) : (evalRand w p T s).support = OracleComp.support (runRand w p T (RandCfg.running s))

Translation along basis homomorphisms

@[simp]

theorem Cslib.WordRAM.stepRand_mapOp {B B' : Basis} {r : ℕ} (φ : B.Hom B') (w : ℕ) (p : Program B r) (cfg : RandCfg r) : stepRand w (Program.mapOp φ p) cfg = stepRand w p cfg

@[simp]

theorem Cslib.WordRAM.runRand_mapOp {B B' : Basis} {r : ℕ} (φ : B.Hom B') (w : ℕ) (p : Program B r) (T : ℕ) (cfg : RandCfg r) : runRand w (Program.mapOp φ p) T cfg = runRand w p T cfg

@[simp]

theorem Cslib.WordRAM.evalRand_mapOp {B B' : Basis} {r : ℕ} (φ : B.Hom B') (w : ℕ) (p : Program B r) (T : ℕ) (s : State r) : evalRand w (Program.mapOp φ p) T s = evalRand w p T s

Word-bound preservation

theorem Cslib.WordRAM.stepRand_bounded {B : Basis} {r w : ℕ} {p : Program B r} {cfg cfg' : RandCfg r} (hcfg : RandCfg.Bounded w cfg) (hmem : cfg' ∈ OracleComp.support (stepRand w p cfg)) : RandCfg.Bounded w cfg'

One randomized step preserves RandCfg.Bounded w.

theorem Cslib.WordRAM.runRand_bounded {B : Basis} {r w : ℕ} {p : Program B r} {T : ℕ} {cfg cfg' : RandCfg r} (hcfg : RandCfg.Bounded w cfg) (hmem : cfg' ∈ OracleComp.support (runRand w p T cfg)) : RandCfg.Bounded w cfg'

Clocked randomized execution preserves RandCfg.Bounded w.

theorem Cslib.WordRAM.runRand_bounded_init {B : Basis} {r w : ℕ} {p : Program B r} {input : List ℕ} {T : ℕ} {cfg : RandCfg r} (hi : InputFits w input) (hmem : cfg ∈ OracleComp.support (runRand w p T (RandCfg.running (State.init input)))) : RandCfg.Bounded w cfg

Every configuration reachable under runRand from an input that fits w holds only w-bit words.

Agreement with deterministic semantics

theorem Cslib.WordRAM.stepRand_eq_of_isRandFree {B : Basis} {r w : ℕ} {p : Program B r} (hp : p.IsRandFree) (s : State r) : stepRand w p (RandCfg.running s) = pure (RandCfg.ofOutcome s.data (step w p s))

On a rand-free program, stepRand agrees with deterministic WordRAM.step.

theorem Cslib.WordRAM.runRand_eq_pure_running_of_runs {B : Basis} {r w m : ℕ} {p : Program B r} {s t : State r} (hrun : Runs w p s t m) : runRand w p m (RandCfg.running s) = pure (RandCfg.running t)

A deterministic m-step Runs lifts unconditionally to runRand (no IsRandFree needed, as Runs never visits Instr.rand).

theorem Cslib.WordRAM.runRand_eq_pure_halted_of_runs_halt {B : Basis} {r w m T : ℕ} {p : Program B r} {s t : State r} {v : ℕ} (hrun : Runs w p s t m) (hhalt : step w p t = Outcome.halt v) (hT : m + 1 ≤ T) : runRand w p T (RandCfg.running s) = pure (RandCfg.halted v t.data)

Unconditional lifting (no IsRandFree needed): a deterministic Runs followed by halt gives pure (.halted v t.data) at every fuel T ≥ m + 1.

theorem Cslib.WordRAM.stepRand_isQueryBounded_zero_of_isRandFree {B : Basis} {r w : ℕ} {p : Program B r} (hp : p.IsRandFree) (cfg : RandCfg r) : OracleComp.IsQueryBounded (stepRand w p cfg) 0

On a rand-free program, a single step makes zero oracle calls.

theorem Cslib.WordRAM.runRand_isQueryBounded_zero_of_isRandFree {B : Basis} {r w T : ℕ} {p : Program B r} (hp : p.IsRandFree) (cfg : RandCfg r) : OracleComp.IsQueryBounded (runRand w p T cfg) 0

On a rand-free program, clocked execution makes zero oracle calls.

theorem Cslib.WordRAM.runRand_eq_pure_halted_iff_of_isRandFree {B : Basis} {r w T : ℕ} {p : Program B r} (hp : p.IsRandFree) {s : State r} {v : ℕ} {d : Data r} : runRand w p T (RandCfg.running s) = pure (RandCfg.halted v d) ↔ ∃ (t : State r) (m : ℕ), m + 1 ≤ T ∧ Runs w p s t m ∧ step w p t = Outcome.halt v ∧ t.data = d

Full state-and-memory agreement on IsRandFree programs, matching Executes.

theorem Cslib.WordRAM.exists_data_runRand_eq_pure_halted_iff_executes_of_isRandFree {B : Basis} {r w T : ℕ} {p : Program B r} (hp : p.IsRandFree) {s : State r} {v : ℕ} : (∃ (d : Data r), runRand w p T (RandCfg.running s) = pure (RandCfg.halted v d)) ↔ ∃ n ≤ T, Executes w p s v n

Scalar projection corollary matching Executes on IsRandFree programs.

Worst-case safety, step bounds, and randomness budgets

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

Starting from s, randomized runs of p never reach .faulted at any horizon T.

theorem Cslib.WordRAM.RandFaultFree.evalRand_faulted_eq_zero {B : Basis} {r w : ℕ} {p : Program B r} {s : State r} (h : RandFaultFree w p s) (T : ℕ) : (evalRand w p T s) RandCfg.faulted = 0

Under RandFaultFree, the fault probability vanishes at every horizon T.

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

Every supported randomized execution path from s has halted cleanly within T steps.

theorem Cslib.WordRAM.runRand_eq_of_randHaltsWithin {B : Basis} {r w T T' : ℕ} {p : Program B r} {s : State r} (h : RandHaltsWithin w p s T) (hT : T ≤ T') : runRand w p T' (RandCfg.running s) = runRand w p T (RandCfg.running s)

Once RandHaltsWithin w p s T holds, increasing the step budget T' ≥ T leaves the ProbComp computation identically unchanged (and charges zero additional oracle queries).

theorem Cslib.WordRAM.evalRand_eq_of_randHaltsWithin {B : Basis} {r w T T' : ℕ} {p : Program B r} {s : State r} (h : RandHaltsWithin w p s T) (hT : T ≤ T') : evalRand w p T' s = evalRand w p T s

Increasing fuel preserves the output distribution once RandHaltsWithin holds.

theorem Cslib.WordRAM.RandHaltsWithin.mono {B : Basis} {r w T T' : ℕ} {p : Program B r} {s : State r} (h : RandHaltsWithin w p s T) (hT : T ≤ T') : RandHaltsWithin w p s T'

RandHaltsWithin is monotone in the step bound.

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

Any program whose randomized runs halt within T steps is fault-free at all horizons.

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

Worst-case rand-call budget: at most R rand instructions are executed on every path within T steps (including rand(0)).

theorem Cslib.WordRAM.RandCallsBounded.mono {B : Basis} {r w T R R' : ℕ} {p : Program B r} {s : State r} (h : RandCallsBounded w p s T R) (hR : R ≤ R') : RandCallsBounded w p s T R'

RandCallsBounded is monotone in the call budget R.

theorem Cslib.WordRAM.RandCallsBounded.of_randHaltsWithin {B : Basis} {r w T T' R : ℕ} {p : Program B r} {s : State r} (hhalt : RandHaltsWithin w p s T) (hr : RandCallsBounded w p s T R) (hT : T ≤ T') : RandCallsBounded w p s T' R

Once RandHaltsWithin w p s T holds, running for T' ≥ T steps charges zero additional rand calls.

def Cslib.WordRAM.unifBitCost (n : ℕ) : ℕ

Nominal bit cost of a single ProbComp.unifFin n draw: ⌈log₂(n + 1)⌉ (0 bits for rand(0), w bits for rand(2 ^ w - 1)). Charging ⌈log₂(n + 1)⌉ bits per draw is an information-theoretic accounting convention, not the number of fair coins an exact rejection sampler consumes, which has no finite worst-case bound when n + 1 is not a power of two.

@[simp]

theorem Cslib.WordRAM.unifBitCost_zero : unifBitCost 0 = 0

@[simp]

theorem Cslib.WordRAM.unifBitCost_two_pow_sub_one (w : ℕ) : unifBitCost (2 ^ w - 1) = w

theorem Cslib.WordRAM.unifBitCost_le_of_fits {w n : ℕ} (h : Fits w n) : unifBitCost n ≤ w

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

Worst-case entropy-bit budget over T steps.

theorem Cslib.WordRAM.stepRand_queriesSatisfy_fits {B : Basis} {r : ℕ} (w : ℕ) (p : Program B r) (cfg : RandCfg r) : OracleComp.QueriesSatisfy (Fits w) (stepRand w p cfg)

Every ProbComp.unifFin n query issued by stepRand satisfies Fits w n.

theorem Cslib.WordRAM.runRand_queriesSatisfy_fits {B : Basis} {r : ℕ} (w : ℕ) (p : Program B r) (T : ℕ) (cfg : RandCfg r) : OracleComp.QueriesSatisfy (Fits w) (runRand w p T cfg)

Every ProbComp.unifFin n query issued by runRand satisfies Fits w n.

theorem Cslib.WordRAM.RandCallsBounded.randBitsBounded {B : Basis} {r w T R : ℕ} {p : Program B r} {s : State r} (h : RandCallsBounded w p s T R) : RandBitsBounded w p s T (R * w)

At word size w, R rand calls cost at most R * w entropy bits.