Composable Word-RAM subroutine infrastructure

This file provides the step-independent Word-RAM machine infrastructure for relocatable bounded-span subroutines (SubroutineCode, SubroutineBase), along with general structured-code helpers (appendCode, execWithin_append, ExecWithin.loop_potential_retain, Data.*).

State-transition data-structure implementations built on SubroutineBase live in CslibFrontier/DataStructure/WordRAM/StateTransition.lean (Cslib.DataStructure.WordRAM.StateTransitionImpl), and oblivious sequence implementations live in CslibFrontier/DataStructure/WordRAM/Randomized/ObliviousSequence.lean (Cslib.DataStructure.WordRAM.Randomized.ObliviousSequenceImpl).

Main definitions

• Cslib.WordRAM.SubroutineCode, Cslib.WordRAM.SubroutineBase: uniform relocatable machine code and step-independent initialization/framing bundle for a Word-RAM subroutine.
• Cslib.WordRAM.SubroutineCode.initFresh, Cslib.WordRAM.SubroutineCode.initClear: fresh initialization on zeroed memory, with no zero-fill pass, and generic dirty-memory re-initialization, which zero-fills the block before setup.
• Cslib.WordRAM.SubroutineCode.toDynamicProgram: standalone DynamicProgram projection.
• Cslib.WordRAM.SubroutineCode.initFreshProg, Cslib.WordRAM.SubroutineCode.initClearProg, Cslib.WordRAM.SubroutineCode.opProg: compiled flat programs.

Main results

• Cslib.WordRAM.ExecWithin.loop_potential_retain: potential-retaining loop rule for nested loops.
• Cslib.WordRAM.SubroutineCode.zeroFillCode_exec: generic 4 * space + 6 zero-fill execution.
• Cslib.WordRAM.SubroutineBase.initFresh_exec, Cslib.WordRAM.SubroutineBase.initFresh_rename, Cslib.WordRAM.SubroutineBase.initClear_exec, Cslib.WordRAM.SubroutineBase.initClear_rename, Cslib.WordRAM.SubroutineBase.frame_caller: relocated inline initialization and bidirectional register/memory framing.

References

• T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, Introduction to Algorithms, Chapter 17
• J. C. Reynolds, Separation Logic: A Logic for Shared Mutable Data Structures

Potential-retaining loop rule and general helpers

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

Right-nested sequential composition matching ram[…] block expansion.

theorem Cslib.WordRAM.execWithin_append {B : Basis} {r w T₁ T₂ : ℕ} {c d : Code B r} {x y z : Data r} (h₁ : ExecWithin w c x y T₁) (h₂ : ExecWithin w d y z T₂) : ExecWithin w (appendCode c d) x z (T₁ + T₂)

Bounded-step execution rule for appendCode.

theorem Cslib.WordRAM.ExecWithin.loop_potential_retain {B : Basis} {r w : ℕ} {cond : Cond r} {body : Code B r} (I : Data r → Prop) (Φ : Data r → ℕ) (hbody : ∀ (x : Data r), I x → cond.Holds x → ∃ (y : Data r) (T : ℕ), ExecWithin w body x y T ∧ I y ∧ T + 2 + Φ y ≤ Φ x) {x : Data r} (hx : I x) : ∃ (z : Data r) (T : ℕ), ExecWithin w (Code.loop cond body) x z T ∧ I z ∧ ¬cond.Holds z ∧ T + Φ z ≤ Φ x + 2

Potential-retaining loop rule. Like ExecWithin.loop_potential, but retains the remaining exit potential Φ z on the left of T + Φ z ≤ Φ x + 2 so that amortized data-structure credit survives inner loops inside nested loops.

theorem Cslib.WordRAM.Data.Bounded.comap {r r' w : ℕ} {x : Data r'} (hx : Bounded w x) (f : Fin r → Fin r') : Bounded w (Data.comap f x)

Data.comap preserves Bounded w.

theorem Cslib.WordRAM.Data.Bounded.extend {r r' w : ℕ} {f : Fin r → Fin r'} (hf : Function.Injective f) {y : Data r} {x : Data r'} (hy : Bounded w y) (hx : Bounded w x) : Bounded w (Data.extend f y x)

Data.extend preserves Bounded w when both y and x are bounded.

SubroutineCode and SubroutineBase

structure Cslib.WordRAM.SubroutineCode (B : Basis) (r_ds k_init : ℕ) : Type

Uniform machine code for a relocatable bounded-footprint data-structure subroutine over B, independent of runtime problem size, base address, and word size w.

• allocSpan : Code B r_ds

  Computes baseReg ← frontierReg and frontierReg ← frontierReg + space without writes.

• initSetup : Code B r_ds

  Scalar/register initialization assuming [base, base + space) already holds zeros.

• code : Code B r_ds

  Unified operation dispatcher serving all ADT operations.

• frontierReg : Fin r_ds

  Bump-pointer frontier register passed in and updated on initialization.

• baseReg : Fin r_ds

  Persistent base-address register of the allocated block.

• initParams : Fin k_init → Fin r_ds

  Registers carrying runtime dimension parameters (params) into initialization.

• curReg : Fin r_ds

  Scratch pointer register used by generic initClear to zero [base, base + space).

• zeroReg : Fin r_ds

  Constant-0 scratch register used by generic initClear.

• oneReg : Fin r_ds

  Constant-1 scratch register used by generic initClear.

• incCur : Op B r_ds

  Single-instruction increment curReg ← curReg + oneReg over B for initClear.

• input : Fin r_ds → Bool

  true on caller-overwritable argument/scratch registers; false on persistent registers.

• output : Fin r_ds

  Primary output register returned on halt in DynamicProgram.

def Cslib.WordRAM.SubroutineCode.initFresh {B : Basis} {r_ds k_init : ℕ} (P : SubroutineCode B r_ds k_init) : Code B r_ds

Initializer when [frontier, frontier + space) is already zeroed (e.g. Data.init): runs allocSpan then initSetup, with no zero-fill pass. SubroutineBase.initFresh_exec bounds it by SubroutineBase.initTime instructions (spanTime + setupTime).

def Cslib.WordRAM.SubroutineCode.zeroFillCode {B : Basis} {r_ds k_init : ℕ} (P : SubroutineCode B r_ds k_init) : Code B r_ds

Generic zeroing block over B clearing [baseReg, frontierReg) using incCur.

def Cslib.WordRAM.SubroutineCode.initClear {B : Basis} {r_ds k_init : ℕ} (P : SubroutineCode B r_ds k_init) : Code B r_ds

Generic reusable initializer on arbitrary dirty memory (allocSpan, then zeroFillCode, then initSetup). SubroutineBase.initClear_exec bounds it by initTime + 4 * space + 6 instructions.

def Cslib.WordRAM.SubroutineCode.mapSimulates {B B' : Basis} {r_ds k_init : ℕ} (φ : B.Simulates B') (P : SubroutineCode B r_ds k_init) : SubroutineCode B' r_ds k_init

Translate a SubroutineCode bundle along a basis simulation.

@[reducible, inline]

abbrev Cslib.WordRAM.SubroutineCode.toStandard {r_ds k_init : ℕ} (P : SubroutineCode Basis.exact r_ds k_init) : SubroutineCode Basis.standard r_ds k_init

Lift an exact-basis SubroutineCode to Basis.standard.

def Cslib.WordRAM.SubroutineCode.toDynamicProgram {B : Basis} {r_ds k_init : ℕ} (P : SubroutineCode B r_ds k_init) {O : Type u_1} {Result : O → Type u_2} (encode : O → Fin r_ds → ℕ) (decode : (o : O) → (Fin r_ds → ℕ) → Option (Result o)) : DynamicProgram { A := O, B := Result } r_ds B

Project subroutine code and its calling convention to the same operation signature. The basis is retained, so this projection does not translate instructions or resource claims.

theorem Cslib.WordRAM.SubroutineCode.zeroFillCode_exec {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 : ∀ {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), ExecWithin w 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

Generic execution of P.zeroFillCode clearing [base, base + space) in 4 * space + 6 instructions over any basis B.

structure Cslib.WordRAM.SubroutineBase {B : Basis} {r_ds k_init : ℕ} (P : SubroutineCode B r_ds k_init) {State : Type u} {O : Type v} (Result : O → Type z) (valid : State → O → Prop) (w base : ℕ) (params : Fin k_init → ℕ) (s₀ : State) : Type (max (max u v) z)

Step-independent specification, representation, calling-convention, and initialization bundle for P : SubroutineCode B r_ds k_init over a state type State, operation type Op, observation family Result, and admissibility predicate valid at word width w, base address base, runtime parameters params, and initial state s₀.

Extended by StateTransitionImpl so that initialization (initFresh, zeroFillCode, initClear), register relocation, standalone toDynamicProgram, and bidirectional framing (frame_caller) are stated and proved once.

• space : ℕ

  Contiguous memory footprint length [base, base + space).

• spanTime : ℕ

  Instruction bound for P.allocSpan.

• setupTime : ℕ

  Instruction bound for P.initSetup.

• initPotential : ℕ

  Upper bound on initial concrete potential after initialization.

• charge : State → O → ℕ

  Amortized instruction charge per operation (excluding trailing standalone halt).

• rep : State → Data r_ds → Prop

  Representation invariant linking mathematical state s to concrete Data r_ds.

• potential : Data r_ds → ℕ

  Concrete integer potential depending only on Data r_ds.

• encode : O → Fin r_ds → ℕ

  Standalone register encoding for DynamicProgram.prepare.

• argMatch : O → (Fin r_ds → ℕ) → Prop

  Partial argument-matching predicate for inline callers (refined by encode).

• decode (o : O) : (Fin r_ds → ℕ) → Option (Result o)

  Output decoder reading typed operation observations from final registers.

• bounded {s : State} {x : Data r_ds} : self.rep s x → Data.Bounded w x

  Represented configurations are word-bounded.

• arguments_fit {s : State} (o : O) : valid s o → ∀ (i : Fin r_ds), P.input i = true → Fits w (self.encode o i)

  Standalone encoded arguments fit in w-bit words on admissible calls.

• encode_matches (o : O) (regs : Fin r_ds → ℕ) : self.argMatch o fun (i : Fin r_ds) => if P.input i = true then self.encode o i else regs i

  Full standalone prepare delivery satisfies argMatch.

• rep_supported {s : State} {x x' : Data r_ds} : (∀ (i : Fin r_ds), P.input i = false → x'.regs i = x.regs i) → (∀ a ∈ { base := base, length := self.space }.footprint, x'.mem a = x.mem a) → Data.Bounded w x' → self.rep s x → self.rep s x'

  rep depends only on persistent registers (P.input i = false) and [base, base + space).

• potential_supported {s : State} {x x' : Data r_ds} : (∀ (i : Fin r_ds), P.input i = false → x'.regs i = x.regs i) → (∀ a ∈ { base := base, length := self.space }.footprint, x'.mem a = x.mem a) → self.rep s x → self.potential x' = self.potential x

  potential depends only on persistent registers and [base, base + space) under rep.

• clear_nodup : [P.curReg, P.zeroReg, P.oneReg, P.baseReg, P.frontierReg].Nodup

  Distinctness of registers used by zeroFillCode relative to baseReg and frontierReg.

• params_not_clear (j : Fin k_init) : P.initParams j ∉ [P.curReg, P.zeroReg, P.oneReg]

  Initialization parameter registers are not overwritten by zeroFillCode.

• incCur_eval {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))

  P.incCur increments P.curReg by 1 when P.oneReg = 1 and the sum fits in w bits.

• span_exec {x : Data r_ds} : Data.Bounded w x → x.regs P.frontierReg = base → (∀ (j : Fin k_init), x.regs (P.initParams j) = params j) → ∃ (x₁ : Data r_ds), ExecWithin w P.allocSpan x x₁ self.spanTime ∧ x₁.mem = x.mem ∧ x₁.regs P.baseReg = base ∧ x₁.regs P.frontierReg = base + self.space ∧ ∀ (j : Fin k_init), x₁.regs (P.initParams j) = params j

  Execution of P.allocSpan: records baseReg = base and advances frontierReg.

• setup_exec {x₁ : Data r_ds} : Data.Bounded w x₁ → x₁.regs P.baseReg = base → x₁.regs P.frontierReg = base + self.space → (∀ (j : Fin k_init), x₁.regs (P.initParams j) = params j) → (∀ a ∈ { base := base, length := self.space }.footprint, x₁.mem a = 0) → ∃ (y : Data r_ds), ExecWithin w P.initSetup x₁ y self.setupTime ∧ y.regs P.frontierReg = base + self.space ∧ self.rep s₀ y ∧ self.potential y ≤ self.initPotential ∧ Modifies { base := base, length := self.space }.footprint x₁.mem y.mem

  Execution of P.initSetup once [base, base + space) holds zeros.

def Cslib.WordRAM.SubroutineBase.initTime {B : Basis} {r_ds k_init w base : ℕ} {P : SubroutineCode B r_ds k_init} {State : Type u} {O : Type v} {Result : O → Type z} {valid : State → O → Prop} {params : Fin k_init → ℕ} {s₀ : State} (C : SubroutineBase P Result valid w base params s₀) : ℕ

Total instruction bound for P.initFresh.

def Cslib.WordRAM.SubroutineBase.prepareRegs {B : Basis} {r_ds k_init w base : ℕ} {P : SubroutineCode B r_ds k_init} {State : Type u} {O : Type v} {Result : O → Type z} {valid : State → O → Prop} {params : Fin k_init → ℕ} {s₀ : State} (C : SubroutineBase P Result valid w base params s₀) (o : O) (regs : Fin r_ds → ℕ) : Fin r_ds → ℕ

Default register-preparation function overwriting P.input registers with C.encode o.

def Cslib.WordRAM.SubroutineBase.mapSimulates {B B' : Basis} {r_ds k_init w base : ℕ} {P : SubroutineCode B r_ds k_init} {State : Type u} {O : Type v} {Result : O → Type z} {valid : State → O → Prop} {params : Fin k_init → ℕ} {s₀ : State} (φ : B.Simulates B') (C : SubroutineBase P Result valid w base params s₀) : SubroutineBase (SubroutineCode.mapSimulates φ P) Result valid w base params s₀

Lift a SubroutineBase bundle along any defined-evaluation basis simulation.

def Cslib.WordRAM.SubroutineBase.toDynamicProgram {B : Basis} {r_ds k_init w base : ℕ} {P : SubroutineCode B r_ds k_init} {State : Type u} {O : Type v} {Result : O → Type z} {valid : State → O → Prop} {params : Fin k_init → ℕ} {s₀ : State} (C : SubroutineBase P Result valid w base params s₀) : DynamicProgram { A := O, B := Result } r_ds B

Project a subroutine bundle to its signature-level program, retaining the instruction basis.

theorem Cslib.WordRAM.SubroutineBase.initFresh_exec {B : Basis} {r_ds k_init w base : ℕ} {P : SubroutineCode B r_ds k_init} {State : Type u} {O : Type v} {Result : O → Type z} {valid : State → O → Prop} {params : Fin k_init → ℕ} {s₀ : State} (C : SubroutineBase P Result valid w base params s₀) {x : Data r_ds} (hx : Data.Bounded w x) (hfr : x.regs P.frontierReg = base) (hpar : ∀ (j : Fin k_init), x.regs (P.initParams j) = params j) (hz : ∀ a ∈ { base := base, length := C.space }.footprint, x.mem a = 0) : ∃ (y : Data r_ds), ExecWithin w P.initFresh x y C.initTime ∧ y.regs P.frontierReg = base + C.space ∧ C.rep s₀ y ∧ C.potential y ≤ C.initPotential ∧ Modifies { base := base, length := C.space }.footprint x.mem y.mem

Execute P.initFresh on zeroed [base, base + C.space) in C.initTime instructions.

theorem Cslib.WordRAM.SubroutineBase.initFresh_rename {B : Basis} {r_ds r_caller k_init w base : ℕ} {P : SubroutineCode B r_ds k_init} {State : Type u} {O : Type v} {Result : O → Type z} {valid : State → O → Prop} {params : Fin k_init → ℕ} {s₀ : State} (C : SubroutineBase P Result valid w base params s₀) {f : Fin r_ds → Fin r_caller} (hf : Function.Injective f) {x : Data r_caller} (hx : Data.Bounded w (Data.comap f x)) (hfr : x.regs (f P.frontierReg) = base) (hpar : ∀ (j : Fin k_init), x.regs (f (P.initParams j)) = params j) (hz : ∀ a ∈ { base := base, length := C.space }.footprint, x.mem a = 0) : ∃ (z : Data r_caller), ExecWithin w (Code.rename f P.initFresh) x z C.initTime ∧ z.regs (f P.frontierReg) = base + C.space ∧ C.rep s₀ (Data.comap f z) ∧ C.potential (Data.comap f z) ≤ C.initPotential ∧ Modifies { base := base, length := C.space }.footprint x.mem z.mem ∧ ∀ j ∉ Set.range f, z.regs j = x.regs j

Relocated fresh initialization along any injective register embedding f, in C.initTime instructions.

theorem Cslib.WordRAM.SubroutineBase.initClear_exec {B : Basis} {r_ds k_init w base : ℕ} {P : SubroutineCode B r_ds k_init} {State : Type u} {O : Type v} {Result : O → Type z} {valid : State → O → Prop} {params : Fin k_init → ℕ} {s₀ : State} (C : SubroutineBase P Result valid w base params s₀) {x : Data r_ds} (hx : Data.Bounded w x) (hfr : x.regs P.frontierReg = base) (hpar : ∀ (j : Fin k_init), x.regs (P.initParams j) = params j) : ∃ (y : Data r_ds), ExecWithin w P.initClear x y (C.initTime + 4 * C.space + 6) ∧ y.regs P.frontierReg = base + C.space ∧ C.rep s₀ y ∧ C.potential y ≤ C.initPotential ∧ Modifies { base := base, length := C.space }.footprint x.mem y.mem

Execute P.initClear on arbitrary dirty memory in C.initTime + 4 * C.space + 6 instructions.

theorem Cslib.WordRAM.SubroutineBase.initClear_rename {B : Basis} {r_ds r_caller k_init w base : ℕ} {P : SubroutineCode B r_ds k_init} {State : Type u} {O : Type v} {Result : O → Type z} {valid : State → O → Prop} {params : Fin k_init → ℕ} {s₀ : State} (C : SubroutineBase P Result valid w base params s₀) {f : Fin r_ds → Fin r_caller} (hf : Function.Injective f) {x : Data r_caller} (hx : Data.Bounded w (Data.comap f x)) (hfr : x.regs (f P.frontierReg) = base) (hpar : ∀ (j : Fin k_init), x.regs (f (P.initParams j)) = params j) : ∃ (z : Data r_caller), ExecWithin w (Code.rename f P.initClear) x z (C.initTime + 4 * C.space + 6) ∧ z.regs (f P.frontierReg) = base + C.space ∧ C.rep s₀ (Data.comap f z) ∧ C.potential (Data.comap f z) ≤ C.initPotential ∧ Modifies { base := base, length := C.space }.footprint x.mem z.mem ∧ ∀ j ∉ Set.range f, z.regs j = x.regs j

Relocated dirty-memory initialization along any injective register embedding f, in C.initTime + 4 * C.space + 6 instructions.

theorem Cslib.WordRAM.SubroutineBase.frame_caller {B : Basis} {r_ds r_caller k_init w base : ℕ} {P : SubroutineCode B r_ds k_init} {State : Type u} {O : Type v} {Result : O → Type z} {valid : State → O → Prop} {params : Fin k_init → ℕ} {s₀ : State} (C : SubroutineBase P Result valid w base params s₀) {f : Fin r_ds → Fin r_caller} {s : State} {x x' : Data r_caller} {F : Finset ℕ} (hr : C.rep s (Data.comap f x)) (hb' : Data.Bounded w (Data.comap f x')) (hreg : ∀ (i : Fin r_ds), P.input i = false → x'.regs (f i) = x.regs (f i)) (hdisj : Disjoint { base := base, length := C.space }.footprint F) (hmem : Modifies F x.mem x'.mem) : C.rep s (Data.comap f x') ∧ C.potential (Data.comap f x') = C.potential (Data.comap f x)

Any caller state transition that preserves (x'.comap f).Bounded w, leaves persistent DS registers (P.input i = false) unchanged, and writes only to a set F disjoint from [base, base + C.space) preserves both C.rep s (x'.comap f) and C.potential (x'.comap f).

def Cslib.WordRAM.SubroutineCode.initFreshProg {B : Basis} {r_ds k_init : ℕ} (P : SubroutineCode B r_ds k_init) : Program B r_ds

Compiled flat Program B r_ds for fresh zeroed-memory initialization (initFresh).

def Cslib.WordRAM.SubroutineCode.initClearProg {B : Basis} {r_ds k_init : ℕ} (P : SubroutineCode B r_ds k_init) : Program B r_ds

Compiled flat Program B r_ds for dirty-memory reusable initialization (initClear).

def Cslib.WordRAM.SubroutineCode.opProg {B : Basis} {r_ds k_init : ℕ} (P : SubroutineCode B r_ds k_init) : Program B r_ds

Compiled flat Program B r_ds serving all operations of the data structure.