Frontier-bounded structured word-RAM executions

Cslib.WordRAM.Exec and Cslib.WordRAM.ExecWithin evaluate memory loads and stores on an unbounded cell array ℕ → ℕ without checking an allocation frontier. On the Resizable Word RAM, by contrast, load and store succeed only at addresses strictly below the current hardware word frontier frontier.

This module refines Exec and ExecWithin to ExecBoundedExact and ExecBounded, recording on every load d a and store a s that the accessed word address x.regs a lies strictly below an explicit address bound L. Pairing Realization.Realizes with the frontier-bounded realization judgment Realization.RealizesBounded allows every non-allocating Memory.Prog client compiled by realize to lift directly to the Resizable Word RAM (RDemonicExec.of_execBounded) without duplicating the compiler or modifying CslibFrontier/Tactic/Realize.lean.

Main definitions

• Cslib.WordRAM.IsRegOnlyOp, Cslib.WordRAM.IsRegOnlyCode: predicates for data instructions and structured programs that perform no memory accesses (load or store) and no rand sampling.
• Cslib.WordRAM.Op.BoundedAccess: side condition requiring x.regs a < L on load and store.
• Cslib.WordRAM.ExecBoundedExact, Cslib.WordRAM.ExecBounded: exact-step and bounded-step structured executions whose memory accesses stay strictly below L.

Main results

• Cslib.WordRAM.ExecBounded.toExecWithin: forget the address bound L back to ExecWithin.
• Cslib.WordRAM.ExecBounded.mono_bound: enlarge the address bound L₁ ≤ L₂.
• Cslib.WordRAM.ExecBounded.of_execWithin_regOnly: lift any register-only ExecWithin execution to ExecBounded at an arbitrary bound L.
• Cslib.WordRAM.ExecBounded.mapSimulates: transport frontier-bounded executions along any defined-evaluation basis simulation Basis.Simulates.
• Cslib.WordRAM.SubroutineCode.zeroFillCode_execBounded: frontier-bounded execution of SubroutineCode.zeroFillCode.

References

• [Hag98] Torben Hagerup, Sorting and Searching on the Word RAM, STACS 1998 (standard word-RAM register and memory instruction semantics).
• [KLZ26] William Kuszmaul, Jingxun Liang, and Renfei Zhou, Succinct Dynamic Rank/Select: Bypassing the Tree-Structure Bottleneck, SODA 2026 (arXiv:2510.19175v1, Section 5.1, PDF p. 16 / printed p. 15: memory accesses restricted to the active word prefix).

Register-only instructions and bounded memory access

def Cslib.WordRAM.IsRegOnlyOp {B : Basis} {r : ℕ} : Op B r → Prop

Whether a data instruction accesses only registers (neither load nor store).

@[instance_reducible]

instance Cslib.WordRAM.decidableIsRegOnlyOp {B : Basis} {r : ℕ} (o : Op B r) : Decidable (IsRegOnlyOp o)

def Cslib.WordRAM.IsRegOnlyCode {B : Basis} {r : ℕ} : Code B r → Prop

Whether a structured Code B r uses only register instructions (no load, store, or rand).

@[instance_reducible]

instance Cslib.WordRAM.decidableIsRegOnlyCode {B : Basis} {r : ℕ} (c : Code B r) : Decidable (IsRegOnlyCode c)

theorem Cslib.WordRAM.Code.IsGlue.isRegOnlyCode {B : Basis} {r : ℕ} {c : Code B r} (h : c.IsGlue) : IsRegOnlyCode c

Every Code.IsGlue fragment is register-only.

theorem Cslib.WordRAM.copyBank_isRegOnlyCode {B : Basis} {r k : ℕ} (src dst : Fin k → Fin r) (idle : Fin r) : IsRegOnlyCode (copyBank src dst idle)

copyBank uses only register-copy instructions.

def Cslib.WordRAM.Op.BoundedAccess {B : Basis} {r : ℕ} (L : ℕ) : Op B r → Data r → Prop

Data instruction o accesses only memory addresses strictly below L when evaluated at x.

@[instance_reducible]

instance Cslib.WordRAM.decidableBoundedAccess {B : Basis} {r : ℕ} (L : ℕ) (o : Op B r) (x : Data r) : Decidable (Op.BoundedAccess L o x)

theorem Cslib.WordRAM.Op.BoundedAccess.mono {B : Basis} {r L₁ L₂ : ℕ} {o : Op B r} {x : Data r} (hL : L₁ ≤ L₂) (h : BoundedAccess L₁ o x) : BoundedAccess L₂ o x

theorem Cslib.WordRAM.Op.BoundedAccess.of_isRegOnly {B : Basis} {r L : ℕ} {o : Op B r} {x : Data r} (ho : IsRegOnlyOp o) : BoundedAccess L o x

theorem Cslib.WordRAM.Op.boundedAccess_mapSimulates_iff {B B' : Basis} {r : ℕ} (ψ : B.Simulates B') (L : ℕ) (o : Op B r) (x : Data r) : BoundedAccess L (mapSimulates ψ o) x ↔ BoundedAccess L o x

Exact and bounded executions with address bound L

inductive Cslib.WordRAM.ExecBoundedExact {B : Basis} {r : ℕ} (w L : ℕ) : Code B r → Data r → Data r → ℕ → Prop

ExecBoundedExact w L c x y n: at word size w, the structured program c leads from data x to data y in n instructions, and every load or store accesses an address < L.

• op {B : Basis} {r w L : ℕ} {o : Op B r} {x y : Data r} : Op.BoundedAccess L o x → Op.eval w o x = some y → ExecBoundedExact w L (Code.op o) x y 1

  A data instruction whose memory access (if any) is < L takes 1 instruction.

• seq {B : Basis} {r w L : ℕ} {c₁ c₂ : Code B r} {x y z : Data r} {m n : ℕ} : ExecBoundedExact w L c₁ x y m → ExecBoundedExact w L c₂ y z n → ExecBoundedExact w L (c₁.seq c₂) x z (m + n)

  Sequencing adds the instruction counts.

• branch_pos {B : Basis} {r w L : ℕ} {c : Cond r} {pos neg : Code B r} {x y : Data r} {n : ℕ} : c.Holds x → ExecBoundedExact w L pos x y n → ExecBoundedExact w L (Code.branch c pos neg) x y (n + 1)

  Positive branch of a conditional adds 1 instruction.

• branch_neg {B : Basis} {r w L : ℕ} {c : Cond r} {pos neg : Code B r} {x y : Data r} {n : ℕ} : ¬c.Holds x → ExecBoundedExact w L neg x y n → ExecBoundedExact w L (Code.branch c pos neg) x y (n + 2)

  Negative branch of a conditional adds 2 instructions.

• loop_exit {B : Basis} {r w L : ℕ} {c : Cond r} {body : Code B r} {x : Data r} : ¬c.Holds x → ExecBoundedExact w L (Code.loop c body) x x 2

  Exiting a while loop takes 2 instructions.

• loop_iter {B : Basis} {r w L : ℕ} {c : Cond r} {body : Code B r} {x y z : Data r} {m n : ℕ} : c.Holds x → ExecBoundedExact w L body x y m → ExecBoundedExact w L (Code.loop c body) y z n → ExecBoundedExact w L (Code.loop c body) x z (m + n + 2)

  One iteration of a while loop followed by the rest adds m + n + 2 instructions.

def Cslib.WordRAM.ExecBounded {B : Basis} {r : ℕ} (w L : ℕ) (c : Code B r) (x y : Data r) (T : ℕ) : Prop

ExecBounded w L c x y T: at word size w, the structured program c leads from data x to data y within T instructions while every load or store accesses an address < L.

theorem Cslib.WordRAM.ExecBoundedExact.toExec {B : Basis} {r w L n : ℕ} {c : Code B r} {x y : Data r} (h : ExecBoundedExact w L c x y n) : Exec w c x y n

Forget the address bound L to obtain an ordinary Exec.

theorem Cslib.WordRAM.ExecBoundedExact.mono_bound {B : Basis} {r w L₁ L₂ n : ℕ} {c : Code B r} {x y : Data r} (hL : L₁ ≤ L₂) (h : ExecBoundedExact w L₁ c x y n) : ExecBoundedExact w L₂ c x y n

Enlarge the address bound L₁ ≤ L₂.

theorem Cslib.WordRAM.ExecBoundedExact.of_exec_regOnly {B : Basis} {r w L n : ℕ} {c : Code B r} {x y : Data r} (hc : IsRegOnlyCode c) (h : Exec w c x y n) : ExecBoundedExact w L c x y n

Lift any register-only Exec to ExecBoundedExact at an arbitrary bound L.

theorem Cslib.WordRAM.ExecBoundedExact.mapSimulates {B B' : Basis} {r w L n : ℕ} {c : Code B r} {x y : Data r} (ψ : B.Simulates B') (h : ExecBoundedExact w L c x y n) : ExecBoundedExact w L (Code.mapSimulates ψ c) x y n

Transport ExecBoundedExact along a defined-evaluation basis simulation.

theorem Cslib.WordRAM.ExecBoundedExact.within {B : Basis} {r w L n : ℕ} {c : Code B r} {x y : Data r} (h : ExecBoundedExact w L c x y n) : ExecBounded w L c x y n

Every exact execution within n instructions is a bounded execution within n.

theorem Cslib.WordRAM.ExecBoundedExact.bounded {B : Basis} {r w L n : ℕ} {c : Code B r} {x y : Data r} (h : ExecBoundedExact w L c x y n) (hx : Data.Bounded w x) : Data.Bounded w y

Word-boundedness is preserved along ExecBoundedExact.

theorem Cslib.WordRAM.ExecBoundedExact.regs_eq {B : Basis} {r w L n : ℕ} {c : Code B r} {x y : Data r} {reg : Fin r} (h : ExecBoundedExact w L c x y n) (hp : Code.Preserves reg c) : y.regs reg = x.regs reg

Unwritten registers keep their values along ExecBoundedExact.

theorem Cslib.WordRAM.ExecBoundedExact.runs {B : Basis} {r w L n : ℕ} {c : Code B r} {x y : Data r} {p : Program B r} {pc : ℕ} (h : ExecBoundedExact w L c x y n) (hp : p.Contains pc (c.assemble pc)) : Runs w p { pc := pc, data := x } { pc := pc + c.size, data := y } n

A frontier-bounded structured execution is a run of any containing flat program.

theorem Cslib.WordRAM.ExecBoundedExact.executes {B : Basis} {r w L n : ℕ} {c : Code B r} {x y : Data r} (h : ExecBoundedExact w L c x y n) (out : Fin r) : Executes w (c.program out) { pc := 0, data := x } (y.regs out) (n + 1)

A frontier-bounded structured execution followed by halt out is a halting run.

theorem Cslib.WordRAM.ExecBounded.toExecWithin {B : Basis} {r w L T : ℕ} {c : Code B r} {x y : Data r} (h : ExecBounded w L c x y T) : ExecWithin w c x y T

Forget the address bound L to obtain ExecWithin.

@[instance_reducible]

instance Cslib.WordRAM.ExecBounded.instCoeOutExec {B : Basis} {r : ℕ} (w L : ℕ) (c : Code B r) (x y : Data r) (n : ℕ) : CoeOut (ExecBoundedExact w L c x y n) (Exec w c x y n)

@[instance_reducible]

instance Cslib.WordRAM.ExecBounded.instCoeOutExecWithin {B : Basis} {r : ℕ} (w L : ℕ) (c : Code B r) (x y : Data r) (T : ℕ) : CoeOut (ExecBounded w L c x y T) (ExecWithin w c x y T)

theorem Cslib.WordRAM.ExecBounded.mono {B : Basis} {r w L T T₂ : ℕ} {c : Code B r} {x y : Data r} (h : ExecBounded w L c x y T) (hT : T ≤ T₂) : ExecBounded w L c x y T₂

Enlarge the instruction budget T ≤ T₂.

theorem Cslib.WordRAM.ExecBounded.mono_bound {B : Basis} {r w L₁ L₂ T : ℕ} {c : Code B r} {x y : Data r} (hL : L₁ ≤ L₂) (h : ExecBounded w L₁ c x y T) : ExecBounded w L₂ c x y T

Enlarge the address bound L₁ ≤ L₂.

theorem Cslib.WordRAM.ExecBounded.of_execWithin_regOnly {B : Basis} {r w L T : ℕ} {c : Code B r} {x y : Data r} (hc : IsRegOnlyCode c) (h : ExecWithin w c x y T) : ExecBounded w L c x y T

Lift any register-only ExecWithin execution to ExecBounded at an arbitrary bound L.

theorem Cslib.WordRAM.ExecBounded.bounded {B : Basis} {r w L T : ℕ} {c : Code B r} {x y : Data r} (h : ExecBounded w L c x y T) (hx : Data.Bounded w x) : Data.Bounded w y

Word-boundedness is preserved along ExecBounded.

theorem Cslib.WordRAM.ExecBounded.regs_eq {B : Basis} {r w L T : ℕ} {c : Code B r} {x y : Data r} {reg : Fin r} (h : ExecBounded w L c x y T) (hp : Code.Preserves reg c) : y.regs reg = x.regs reg

Unwritten registers keep their values along ExecBounded.

theorem Cslib.WordRAM.ExecBounded.mapSimulates {B B' : Basis} {r w L T : ℕ} {c : Code B r} {x y : Data r} (ψ : B.Simulates B') (h : ExecBounded w L c x y T) : ExecBounded w L (Code.mapSimulates ψ c) x y T

Transport ExecBounded along a defined-evaluation basis simulation.

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

Single data instruction with bounded access.

theorem Cslib.WordRAM.ExecBounded.const {B : Basis} {r w L : ℕ} {x : Data r} {d : Fin r} {v : ℕ} (h : Fits w v) : ExecBounded w L (Code.op (Op.const d v)) x (x.set d v) 1

Constant load into register d.

theorem Cslib.WordRAM.ExecBounded.alu {B : Basis} {r w L : ℕ} {x : Data r} {d : Fin r} {f : B.Op} {args : Fin (B.Arity f) → Fin r} {v : ℕ} (hf : B.interp w f (x.regs ∘ args) = some v) (h : Fits w v) : ExecBounded w L (Code.op (Op.alu f d args)) x (x.set d v) 1

ALU operation into register d.

theorem Cslib.WordRAM.ExecBounded.copy {B : Basis} {r w L : ℕ} {x : Data r} {d s : Fin r} : ExecBounded w L (Code.op (Op.copy d s)) x (x.set d (x.regs s)) 1

Register copy into register d.

theorem Cslib.WordRAM.ExecBounded.load {B : Basis} {r w L : ℕ} {x : Data r} {d a : Fin r} (ha : x.regs a < L) : ExecBounded w L (Code.op (Op.load d a)) x (x.set d (x.mem (x.regs a))) 1

Memory load from an address x.regs a < L.

theorem Cslib.WordRAM.ExecBounded.store {B : Basis} {r w L : ℕ} {x : Data r} {a s : Fin r} (ha : x.regs a < L) : ExecBounded w L (Code.op (Op.store a s)) x (x.write (x.regs a) (x.regs s)) 1

Memory store to an address x.regs a < L.

theorem Cslib.WordRAM.ExecBounded.bin {r w L : ℕ} {x : Data r} {d i j : Fin r} {f : BinOp} (h : Fits w (f.eval (x.regs i) (x.regs j))) : ExecBounded w L (Code.op (Op.bin f d i j)) x (x.set d (f.eval (x.regs i) (x.regs j))) 1

Standard binary operation into register d.

theorem Cslib.WordRAM.ExecBounded.width {r w L : ℕ} {x : Data r} {d : Fin r} : ExecBounded w L (Code.op (Op.width d)) x (x.set d w) 1

Word-width read into register d.

theorem Cslib.WordRAM.ExecBounded.seq {B : Basis} {r w L T₁ T₂ : ℕ} {c₁ c₂ : Code B r} {x y z : Data r} (h₁ : ExecBounded w L c₁ x y T₁) (h₂ : ExecBounded w L c₂ y z T₂) : ExecBounded w L (c₁.seq c₂) x z (T₁ + T₂)

Sequential composition of frontier-bounded executions.

theorem Cslib.WordRAM.ExecBounded.branch_pos {B : Basis} {r w L T : ℕ} {pos neg : Code B r} {cond : Cond r} {x y : Data r} (hc : cond.Holds x) (h : ExecBounded w L pos x y T) : ExecBounded w L (Code.branch cond pos neg) x y (T + 1)

Positive branch of a conditional.

theorem Cslib.WordRAM.ExecBounded.branch_neg {B : Basis} {r w L T : ℕ} {pos neg : Code B r} {cond : Cond r} {x y : Data r} (hc : ¬cond.Holds x) (h : ExecBounded w L neg x y T) : ExecBounded w L (Code.branch cond pos neg) x y (T + 2)

Negative branch of a conditional.

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

Conditional with a shared bound on both alternatives.

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

Exiting a loop when the condition fails takes at most 2 instructions.

theorem Cslib.WordRAM.ExecBounded.loop_iter {B : Basis} {r w L T₁ T₂ : ℕ} {body : Code B r} {cond : Cond r} {x y z : Data r} (hc : cond.Holds x) (h₁ : ExecBounded w L body x y T₁) (h₂ : ExecBounded w L (Code.loop cond body) y z T₂) : ExecBounded w L (Code.loop cond body) x z (T₁ + T₂ + 2)

One loop iteration followed by the rest adds T₁ + 2 instructions to the bound.

theorem Cslib.WordRAM.ExecBounded.loop {B : Basis} {r w L : ℕ} {body : Code B r} {cond : Cond r} (xs : ℕ → Data r) (k T : ℕ) (hc : ∀ i < k, cond.Holds (xs i)) (hk : ¬cond.Holds (xs k)) (hbody : ∀ i < k, ExecBounded w L body (xs i) (xs (i + 1)) T) : ExecBounded w L (Code.loop cond body) (xs 0) (xs k) (k * (T + 2) + 2)

Loop through explicit states xs 0, …, xs k under address bound L.

theorem Cslib.WordRAM.ExecBounded.loop_invariant_state_additive {B : Basis} {r w L : ℕ} {cond : Cond r} {σ : Type u_1} {code : Code B r} {C D : ℕ} (I : ℕ → σ → Data r → Prop) (next : σ → σ) (charge : σ → ℕ) (hexit : ∀ (s : σ) (x : Data r), I 0 s x → ¬cond.Holds x) (hbody : ∀ (n : ℕ) (s : σ) (x : Data r), I (n + 1) s x → cond.Holds x ∧ ∃ (y : Data r), ExecBounded w L code x y (C * (charge s + 1) + D) ∧ I n (next s) y) {n : ℕ} {s : σ} {x : Data r} (hx : I n s x) : ∃ (y : Data r), ExecBounded w L (Code.loop cond code) x y (C * iterationSum next charge n s + (C + D + 2) * n + 2) ∧ I 0 (next^[n] s) y

Frontier-bounded counterpart of ExecWithin.loop_invariant_state_additive.

theorem Cslib.WordRAM.copyBank_execBounded {B : Basis} {r k : ℕ} (src dst : Fin k → Fin r) (idle : Fin r) (hi : Function.Injective dst) (hd : ∀ (i j : Fin k), src i ≠ dst j) (w L : ℕ) (x : Data r) : ∃ (y : Data r), ExecBounded w L (copyBank src dst idle) x y (k + 1) ∧ y.mem = x.mem ∧ (∀ (i : Fin k), y.regs (dst i) = x.regs (src i)) ∧ ∀ (j : Fin r), (∀ (i : Fin k), dst i ≠ j) → y.regs j = x.regs j

copyBank executes within k + 1 instructions under any address bound L.

theorem Cslib.WordRAM.SubroutineCode.zeroFillCode_execBounded {B : Basis} {r_ds k_init : ℕ} (P : SubroutineCode B r_ds k_init) {w base space : ℕ} {params : Fin k_init → ℕ} (hclear : [P.curReg, P.zeroReg, P.oneReg, P.baseReg, P.frontierReg].Nodup) (hparams : ∀ (j : Fin k_init), P.initParams j ∉ [P.curReg, P.zeroReg, P.oneReg]) (hinc_reg : IsRegOnlyOp P.incCur) (hinc : ∀ {x : Data r_ds}, x.regs P.oneReg = 1 → Fits w (x.regs P.curReg + 1) → Op.eval w P.incCur x = some (x.set P.curReg (x.regs P.curReg + 1))) {x₁ : Data r_ds} (hx₁ : Data.Bounded w x₁) (hb₁ : x₁.regs P.baseReg = base) (hfr₁ : x₁.regs P.frontierReg = base + space) (hpar₁ : ∀ (j : Fin k_init), x₁.regs (P.initParams j) = params j) : ∃ (x₂ : Data r_ds), ExecBounded w (base + space) P.zeroFillCode x₁ x₂ (4 * space + 6) ∧ Data.Bounded w x₂ ∧ x₂.regs P.baseReg = base ∧ x₂.regs P.frontierReg = base + space ∧ (∀ (j : Fin k_init), x₂.regs (P.initParams j) = params j) ∧ (∀ a ∈ { base := base, length := space }.footprint, x₂.mem a = 0) ∧ Modifies { base := base, length := space }.footprint x₁.mem x₂.mem

Frontier-bounded execution of P.zeroFillCode clearing [base, base + space) with all stores strictly below base + space.