Composable Word-RAM data-structure subroutines

This file unifies standalone Word-RAM data-structure realizations (DynamicProgram, DynamicCertificate, Stateful.Amortized, Stateful.Bound) with inline subroutine composition inside structured outer algorithms (Code.rename, ExecWithin).

A data structure is packaged once as a SubroutineCode B r_ds k_init and certified by a SubroutineDS bundle. From that single proof, this file derives:

1. Defined-evaluation basis lifting (SubroutineCode.mapSimulates, SubroutineDS.mapSimulates, SubroutineDS.toStandard): Non-faulting executions over Basis.exact lift instruction-for-instruction to Basis.standard via Basis.Simulates.exactStandard from Complexity.Computability.WordRAM.MapOp, bridging exact-basis algorithms and standard-basis DynamicProgram realizations.
2. Standalone Stateful projections: toDynamicProgram, toCertificate, toAmortized, toBound, and adaptive-client corollaries.
3. Relocated initialization (initFresh_rename, initClear_rename): Both O(1) fresh initialization on zeroed Data.init memory and generic O(space) dirty-memory re-initialization along any injective register embedding f : Fin r_ds → Fin r_caller.
4. Relocated inline calls and bidirectional framing (call_rename, frame_caller): Inline execution with amortized potential accounting, DS-to-caller Modifies framing, and caller-to-DS representation/potential framing.
5. Potential-retaining loop rule (ExecWithin.loop_potential_retain): Retains exit potential + Φ z across inner loops so stored data-structure credit survives nested loops.

Main definitions

• Cslib.WordRAM.SubroutineCode, Cslib.WordRAM.SubroutineDS: uniform relocatable machine code and unified standalone / inline specification and resource certificate for a Word-RAM data structure.
• Cslib.WordRAM.SubroutineCode.initFresh, Cslib.WordRAM.SubroutineCode.initClear: O(1) fresh initialization on zeroed memory and generic O(space) dirty-memory re-initialization.
• Cslib.WordRAM.SubroutineDS.toDynamicProgram, Cslib.WordRAM.SubroutineDS.toCertificate: standalone .standard-basis DynamicProgram and DynamicCertificate projections.

Main results

• Cslib.WordRAM.ExecWithin.loop_potential_retain: potential-retaining loop rule for nested loops.
• Cslib.WordRAM.SubroutineDS.toAmortized, Cslib.WordRAM.SubroutineDS.toBound, Cslib.WordRAM.SubroutineDS.run_client_amortized, Cslib.WordRAM.SubroutineDS.run_client_bound: standalone amortized and worst-case instruction bounds over Basis.standard.
• Cslib.WordRAM.SubroutineDS.initFresh_rename, Cslib.WordRAM.SubroutineDS.initClear_rename, Cslib.WordRAM.SubroutineDS.call_rename, Cslib.WordRAM.SubroutineDS.frame_caller: relocated inline initialization, inline operation calls, 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.extend_regs_of_notMem {r r' : ℕ} {f : Fin r → Fin r'} (y : Data r) (x : Data r') {j : Fin r'} (hj : j ∉ Set.range f) : (extend f y x).regs j = x.regs j

Registers outside Set.range f retain their caller values under Data.extend.

@[simp]

theorem Cslib.WordRAM.Data.extend_mem {r r' : ℕ} (f : Fin r → Fin r') (y : Data r) (x : Data r') : (extend f y x).mem = y.mem

Data.extend preserves memory.

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 SubroutineDS

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

O(1) initializer when [frontier, frontier + space) is already zeroed (e.g. Data.init).

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 O(space) reusable initializer on arbitrary dirty memory (zeroFillCode + initSetup).

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.

structure Cslib.WordRAM.SubroutineDS {B : Basis} {r_ds k_init : ℕ} (P : SubroutineCode B r_ds k_init) (D : Stateful.Spec) (w base : ℕ) (params : Fin k_init → ℕ) (s₀ : D.State) : Type (max (max u v) z)

Unified standalone and subroutine specification/resource certificate for P realizing D at word width w, base address base, runtime parameters params, and initial state s₀.

• 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 : D.State → D.Op → ℕ

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

• rep : D.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 : D.Op → Fin r_ds → ℕ

  Standalone register encoding for DynamicProgram.prepare.

• argMatch : D.Op → (Fin r_ds → ℕ) → Prop

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

• decode (o : D.Op) : (Fin r_ds → ℕ) → Option (D.Result o)

  Output decoder reading typed operation observations from final registers.

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

  Represented configurations are word-bounded.

• rep_unique {s₁ s₂ : D.State} {x : Data r_ds} : self.rep s₁ x → self.rep s₂ x → s₁ = s₂

  Concrete machine data determines at most one represented abstract state.

• arguments_fit {s : D.State} (o : D.Op) : D.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 : D.Op) (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 : D.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 : D.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.

• step_exec {s : D.State} {x : Data r_ds} (o : D.Op) : self.rep s x → D.valid s o → self.argMatch o x.regs → ∃ (y : Data r_ds) (n : ℕ), Exec w P.code x y n ∧ self.decode o y.regs = some (D.step s o).2 ∧ self.rep (D.step s o).1 y ∧ Modifies { base := base, length := self.space }.footprint x.mem y.mem ∧ n + self.potential y ≤ self.charge s o + self.potential x

  Execution of P.code for any admissible operation o whose arguments match x.regs.

def Cslib.WordRAM.SubroutineDS.initTime {B : Basis} {r_ds k_init w base : ℕ} {P : SubroutineCode B r_ds k_init} {D : Stateful.Spec} {params : Fin k_init → ℕ} {s₀ : D.State} (C : SubroutineDS P D w base params s₀) : ℕ

Total instruction bound for P.initFresh.

Projection 1: Basis lifting and standalone DynamicProgram / Stateful theorems

def Cslib.WordRAM.SubroutineDS.mapSimulates {B B' : Basis} {r_ds k_init w base : ℕ} {P : SubroutineCode B r_ds k_init} {D : Stateful.Spec} {params : Fin k_init → ℕ} {s₀ : D.State} (φ : B.Simulates B') (C : SubroutineDS P D w base params s₀) : SubroutineDS (SubroutineCode.mapSimulates φ P) D w base params s₀

Lift a SubroutineDS certificate along any defined-evaluation basis simulation.

@[reducible, inline]

abbrev Cslib.WordRAM.SubroutineDS.toStandard {r_ds k_init w base : ℕ} {D : Stateful.Spec} {params : Fin k_init → ℕ} {s₀ : D.State} {P : SubroutineCode Basis.exact r_ds k_init} (C : SubroutineDS P D w base params s₀) : SubroutineDS P.toStandard D w base params s₀

Lift an exact-basis SubroutineDS certificate to Basis.standard.

def Cslib.WordRAM.SubroutineDS.toDynamicProgram {r_ds k_init w base : ℕ} {D : Stateful.Spec} {params : Fin k_init → ℕ} {s₀ : D.State} {P_std : SubroutineCode Basis.standard r_ds k_init} (C : SubroutineDS P_std D w base params s₀) : DynamicProgram D r_ds

Project a .standard-basis SubroutineDS to a standalone DynamicProgram.

def Cslib.WordRAM.SubroutineDS.toCertificate {r_ds k_init w base : ℕ} {D : Stateful.Spec} {params : Fin k_init → ℕ} {s₀ : D.State} {P_std : SubroutineCode Basis.standard r_ds k_init} (C : SubroutineDS P_std D w base params s₀) : DynamicCertificate C.toDynamicProgram w

Project a .standard-basis SubroutineDS to a standalone DynamicCertificate.

theorem Cslib.WordRAM.SubroutineDS.toAmortized {r_ds k_init w base : ℕ} {D : Stateful.Spec} {params : Fin k_init → ℕ} {s₀ : D.State} {P_std : SubroutineCode Basis.standard r_ds k_init} (C : SubroutineDS P_std D w base params s₀) : Stateful.Amortized C.toCertificate.realization DynamicProgram.OperationTrace.instructions (fun (x : D.State) (x_1 : Data r_ds) => C.potential x_1) fun (s : D.State) (o : D.Op) => C.charge s o + 1

Project a .standard-basis SubroutineDS to a standalone Stateful.Amortized certificate, charging + 1 per operation for DynamicProgram's trailing halt instruction.

theorem Cslib.WordRAM.SubroutineDS.toBound {r_ds k_init w base : ℕ} {D : Stateful.Spec} {params : Fin k_init → ℕ} {s₀ : D.State} {P_std : SubroutineCode Basis.standard r_ds k_init} (C : SubroutineDS P_std D w base params s₀) (hpot : ∀ (x : Data r_ds), C.potential x = 0) : Stateful.Bound C.toCertificate.realization DynamicProgram.OperationTrace.instructions fun (s : D.State) (o : D.Op) => C.charge s o + 1

When C.potential is identically zero, SubroutineDS projects directly to a worst-case Stateful.Bound certificate.

theorem Cslib.WordRAM.SubroutineDS.run_client_amortized {r_ds k_init w base : ℕ} {D : Stateful.Spec} {params : Fin k_init → ℕ} {s₀ : D.State} {P_std : SubroutineCode Basis.standard r_ds k_init} (C : SubroutineDS P_std D w base params s₀) {α : Type u_1} (p : D.Client α) {s : D.State} {x : Data r_ds} (hr : C.rep s x) (hv : D.ValidHistory s (D.runClient s p).2.2) : ∃ (y : Data r_ds) (traces : List DynamicProgram.OperationTrace), Stateful.Executes (C.toDynamicProgram.ExecOp w) p x (D.runClient s p).1 y traces ∧ C.rep (D.runClient s p).2.1 y ∧ Stateful.total DynamicProgram.OperationTrace.instructions traces + C.potential y ≤ D.totalCost (fun (s : D.State) (o : D.Op) => C.charge s o + 1) s (D.runClient s p).2.2 + C.potential x

Standalone adaptive-client amortized bound for any admissible client program p.

theorem Cslib.WordRAM.SubroutineDS.run_client_bound {r_ds k_init w base : ℕ} {D : Stateful.Spec} {params : Fin k_init → ℕ} {s₀ : D.State} {P_std : SubroutineCode Basis.standard r_ds k_init} (C : SubroutineDS P_std D w base params s₀) (hpot : ∀ (x : Data r_ds), C.potential x = 0) {α : Type u_1} (p : D.Client α) {s : D.State} {x : Data r_ds} (hr : C.rep s x) (hv : D.ValidHistory s (D.runClient s p).2.2) : ∃ (y : Data r_ds) (traces : List DynamicProgram.OperationTrace), Stateful.Executes (C.toDynamicProgram.ExecOp w) p x (D.runClient s p).1 y traces ∧ C.rep (D.runClient s p).2.1 y ∧ Stateful.total DynamicProgram.OperationTrace.instructions traces ≤ D.totalCost (fun (s : D.State) (o : D.Op) => C.charge s o + 1) s (D.runClient s p).2.2

Standalone adaptive-client worst-case bound when C.potential is identically zero.

Projection 2: Fresh O(1) initialization and register relocation

theorem Cslib.WordRAM.SubroutineDS.initFresh_exec {B : Basis} {r_ds k_init w base : ℕ} {P : SubroutineCode B r_ds k_init} {D : Stateful.Spec} {params : Fin k_init → ℕ} {s₀ : D.State} (C : SubroutineDS P D 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.SubroutineDS.initFresh_rename {B : Basis} {r_ds r_caller k_init w base : ℕ} {P : SubroutineCode B r_ds k_init} {D : Stateful.Spec} {params : Fin k_init → ℕ} {s₀ : D.State} (C : SubroutineDS P D 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 O(1) fresh initialization along any injective register embedding f.

Projection 3: Generic O(space) dirty-memory initialization (initClear)

theorem Cslib.WordRAM.SubroutineDS.zeroFillCode_exec {B : Basis} {r_ds k_init w base : ℕ} {P : SubroutineCode B r_ds k_init} {D : Stateful.Spec} {params : Fin k_init → ℕ} {s₀ : D.State} (C : SubroutineDS P D w base params s₀) {x₁ : Data r_ds} (hx₁ : Data.Bounded w x₁) (hb₁ : x₁.regs P.baseReg = base) (hfr₁ : x₁.regs P.frontierReg = base + C.space) (hpar₁ : ∀ (j : Fin k_init), x₁.regs (P.initParams j) = params j) : ∃ (x₂ : Data r_ds), ExecWithin w P.zeroFillCode x₁ x₂ (4 * C.space + 6) ∧ Data.Bounded w x₂ ∧ x₂.regs P.baseReg = base ∧ x₂.regs P.frontierReg = base + C.space ∧ (∀ (j : Fin k_init), x₂.regs (P.initParams j) = params j) ∧ (∀ a ∈ { base := base, length := C.space }.footprint, x₂.mem a = 0) ∧ Modifies { base := base, length := C.space }.footprint x₁.mem x₂.mem

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

theorem Cslib.WordRAM.SubroutineDS.initClear_exec {B : Basis} {r_ds k_init w base : ℕ} {P : SubroutineCode B r_ds k_init} {D : Stateful.Spec} {params : Fin k_init → ℕ} {s₀ : D.State} (C : SubroutineDS P D 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.SubroutineDS.initClear_rename {B : Basis} {r_ds r_caller k_init w base : ℕ} {P : SubroutineCode B r_ds k_init} {D : Stateful.Spec} {params : Fin k_init → ℕ} {s₀ : D.State} (C : SubroutineDS P D 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 O(space) dirty-memory initialization along any injective register embedding f.

Projection 4: Relocated inline subroutine calls (code_rename, call_rename)

theorem Cslib.WordRAM.SubroutineDS.code_rename {B : Basis} {r_ds r_caller k_init w base : ℕ} {P : SubroutineCode B r_ds k_init} {D : Stateful.Spec} {params : Fin k_init → ℕ} {s₀ : D.State} (C : SubroutineDS P D w base params s₀) {f : Fin r_ds → Fin r_caller} (hf : Function.Injective f) {s : D.State} {x : Data r_caller} (o : D.Op) (hr : C.rep s (Data.comap f x)) (hv : D.valid s o) (harg : C.argMatch o (Data.comap f x).regs) : ∃ (z : Data r_caller) (t : ℕ), ExecWithin w (Code.rename f P.code) x z t ∧ C.decode o (Data.comap f z).regs = some (D.step s o).2 ∧ C.rep (D.step s o).1 (Data.comap f z) ∧ Modifies { base := base, length := C.space }.footprint x.mem z.mem ∧ (∀ j ∉ Set.range f, z.regs j = x.regs j) ∧ t + C.potential (Data.comap f z) ≤ C.charge s o + C.potential (Data.comap f x)

Execute P.code.rename f inline when arguments already match (x.comap f).regs.

theorem Cslib.WordRAM.SubroutineDS.call_rename {B : Basis} {r_ds r_caller k_init w base : ℕ} {P : SubroutineCode B r_ds k_init} {D : Stateful.Spec} {params : Fin k_init → ℕ} {s₀ : D.State} (C : SubroutineDS P D w base params s₀) {f : Fin r_ds → Fin r_caller} (hf : Function.Injective f) {s : D.State} {x x' : Data r_caller} {prep : Code B r_caller} {t_prep : ℕ} (o : D.Op) (hr : C.rep s (Data.comap f x)) (hv : D.valid s o) (hprep : ExecWithin w prep x x' t_prep) (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)) (hmem : ∀ a ∈ { base := base, length := C.space }.footprint, x'.mem a = x.mem a) (harg : C.argMatch o (Data.comap f x').regs) : ∃ (z : Data r_caller) (t : ℕ), ExecWithin w (prep.seq (Code.rename f P.code)) x z t ∧ C.decode o (Data.comap f z).regs = some (D.step s o).2 ∧ C.rep (D.step s o).1 (Data.comap f z) ∧ Modifies { base := base, length := C.space }.footprint x'.mem z.mem ∧ (∀ j ∉ Set.range f, z.regs j = x'.regs j) ∧ t + C.potential (Data.comap f z) ≤ t_prep + C.charge s o + C.potential (Data.comap f x)

Execute .seq prep (P.code.rename f) inline after a caller argument-preparation block prep that preserves persistent DS registers and memory in [base, base + C.space).

Projection 5: Caller-to-DS bidirectional framing (frame_caller)

theorem Cslib.WordRAM.SubroutineDS.frame_caller {B : Basis} {r_ds r_caller k_init w base : ℕ} {P : SubroutineCode B r_ds k_init} {D : Stateful.Spec} {params : Fin k_init → ℕ} {s₀ : D.State} (C : SubroutineDS P D w base params s₀) {f : Fin r_ds → Fin r_caller} {s : D.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).