Deterministic Word-RAM state-transition implementations

This file defines Cslib.DataStructure.WordRAM.StateTransitionImpl, the unified standalone and inline Word-RAM subroutine implementation and resource certificate for a relational state-transition specification D : Cslib.DataStructure.StateTransitionSpec.

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

1. Defined-evaluation basis lifting (StateTransitionImpl.mapSimulates, StateTransitionImpl.toStandard): Non-faulting executions over Basis.exact lift instruction-for-instruction to Basis.standard via Basis.Simulates.exactStandard.
2. Standalone DataStructure projections: toDynamicProgram, toCertificate, toAmortized, toBound, and adaptive-client corollaries (run_client_demonic_amortized, run_client_demonic_bound, run_client_amortized, run_client_bound).
3. Relocated inline calls (code_rename, call_rename, code_rename_ofFn, call_rename_ofFn): Inline execution on caller state space Data r_caller with amortized potential accounting and DS-to-caller Modifies framing.
4. Flat-program operation-sequence execution (RunsOps, run_ops_exact_fresh, run_ops_exact_reusable): Standalone flat-program sequence theorems over P.initFreshProg, P.initClearProg, and P.opProg.

Main definitions

• Cslib.DataStructure.WordRAM.StateTransitionImpl: unified standalone and inline Word-RAM implementation and resource certificate for D : StateTransitionSpec.
• Cslib.DataStructure.WordRAM.StateTransitionImpl.ofFn: constructor for deterministic specifications ([D.HasStepFn f]).
• Cslib.DataStructure.WordRAM.StateTransitionImpl.toCertificate: standalone .standard-basis DynamicCertificate projection.
• Cslib.DataStructure.WordRAM.StateTransitionImpl.RunsOps: sequential flat-program operation execution relation.

Main results

• Cslib.DataStructure.WordRAM.StateTransitionImpl.toAmortized, Cslib.DataStructure.WordRAM.StateTransitionImpl.toBound, Cslib.DataStructure.WordRAM.StateTransitionImpl.run_client_amortized, Cslib.DataStructure.WordRAM.StateTransitionImpl.run_client_bound: standalone amortized and worst-case instruction bounds over Basis.standard.
• Cslib.DataStructure.WordRAM.StateTransitionImpl.code_rename, Cslib.DataStructure.WordRAM.StateTransitionImpl.call_rename, Cslib.DataStructure.WordRAM.StateTransitionImpl.code_rename_ofFn, Cslib.DataStructure.WordRAM.StateTransitionImpl.call_rename_ofFn: relocated inline subroutine calls.
• Cslib.DataStructure.WordRAM.StateTransitionImpl.run_ops_exact_fresh, Cslib.DataStructure.WordRAM.StateTransitionImpl.run_ops_exact_reusable, Cslib.DataStructure.WordRAM.StateTransitionImpl.run_ops_exact_fresh_ofFn, Cslib.DataStructure.WordRAM.StateTransitionImpl.run_ops_exact_reusable_ofFn: standalone flat-program operation-sequence theorems.

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

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

Unified standalone and subroutine specification/resource certificate for P : SubroutineCode B r_ds k_init implementing a relational specification D : StateTransitionSpec at word width w, base address base, runtime parameters params, and initial state s₀.

Extends SubroutineBase P D.Result D.valid w base params s₀ (inheriting toDynamicProgram, initFresh_exec, initFresh_rename, initClear_exec, initClear_rename, frame_caller, and prepareRegs), and existentially quantifies over a permitted outcome (s', a) satisfying D.step s o s' a in step_exec.

• space : ℕ
• spanTime : ℕ
• setupTime : ℕ
• initPotential : ℕ
• charge : D.State → D.Op → ℕ
• rep : D.State → Data r_ds → Prop
• potential : Data r_ds → ℕ
• encode : D.Op → Fin r_ds → ℕ
• argMatch : D.Op → (Fin r_ds → ℕ) → Prop
• decode (o : D.Op) : (Fin r_ds → ℕ) → Option (D.Result o)
• bounded {s : D.State} {x : Data r_ds} : self.rep s x → Data.Bounded w x
• 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)
• 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
• 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'
• 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
• clear_nodup : [P.curReg, P.zeroReg, P.oneReg, P.baseReg, P.frontierReg].Nodup
• params_not_clear (j : Fin k_init) : P.initParams j ∉ [P.curReg, P.zeroReg, P.oneReg]
• 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))
• 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
• 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
• step_exec {s : D.State} {x : WordRAM.Data r_ds} (o : D.Op) : self.rep s x → D.valid s o → self.argMatch o x.regs → ∃ (y : WordRAM.Data r_ds) (s' : D.State) (a : D.Result o) (n : ℕ), WordRAM.Exec w P.code x y n ∧ D.step s o s' a ∧ self.decode o y.regs = some a ∧ self.rep s' y ∧ WordRAM.Modifies { base := base, length := self.space }.footprint x.mem y.mem ∧ n + self.potential y ≤ self.charge s o + self.potential x

  Angelic execution of P.code for any admissible operation o whose arguments match x.regs, witnessing some permitted outcome (s', a) with D.step s o s' a.

@[reducible, inline]

abbrev Cslib.DataStructure.WordRAM.StateTransitionImpl.ofFn {B : WordRAM.Basis} {r_ds k_init w base : ℕ} {P : WordRAM.SubroutineCode B r_ds k_init} {D : StateTransitionSpec} {params : Fin k_init → ℕ} {s₀ : D.State} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (space spanTime setupTime initPotential : ℕ) (charge : D.State → D.Op → ℕ) (rep : D.State → WordRAM.Data r_ds → Prop) (potential : WordRAM.Data r_ds → ℕ) (encode : D.Op → Fin r_ds → ℕ) (argMatch : D.Op → (Fin r_ds → ℕ) → Prop) (decode : (o : D.Op) → (Fin r_ds → ℕ) → Option (D.Result o)) (bounded : ∀ {s : D.State} {x : WordRAM.Data r_ds}, rep s x → WordRAM.Data.Bounded w x) (arguments_fit : ∀ {s : D.State} (o : D.Op), D.valid s o → ∀ (i : Fin r_ds), P.input i = true → WordRAM.Fits w (encode o i)) (encode_matches : ∀ (o : D.Op) (regs : Fin r_ds → ℕ), argMatch o fun (i : Fin r_ds) => if P.input i = true then encode o i else regs i) (rep_supported : ∀ {s : D.State} {x x' : WordRAM.Data r_ds}, (∀ (i : Fin r_ds), P.input i = false → x'.regs i = x.regs i) → (∀ a ∈ { base := base, length := space }.footprint, x'.mem a = x.mem a) → WordRAM.Data.Bounded w x' → rep s x → rep s x') (potential_supported : ∀ {s : D.State} {x x' : WordRAM.Data r_ds}, (∀ (i : Fin r_ds), P.input i = false → x'.regs i = x.regs i) → (∀ a ∈ { base := base, length := space }.footprint, x'.mem a = x.mem a) → rep s x → potential x' = potential x) (clear_nodup : [P.curReg, P.zeroReg, P.oneReg, P.baseReg, P.frontierReg].Nodup) (params_not_clear : ∀ (j : Fin k_init), P.initParams j ∉ [P.curReg, P.zeroReg, P.oneReg]) (incCur_eval : ∀ {x : WordRAM.Data r_ds}, x.regs P.oneReg = 1 → WordRAM.Fits w (x.regs P.curReg + 1) → WordRAM.Op.eval w P.incCur x = some (x.set P.curReg (x.regs P.curReg + 1))) (span_exec : ∀ {x : WordRAM.Data r_ds}, WordRAM.Data.Bounded w x → x.regs P.frontierReg = base → (∀ (j : Fin k_init), x.regs (P.initParams j) = params j) → ∃ (x₁ : WordRAM.Data r_ds), WordRAM.ExecWithin w P.allocSpan x x₁ spanTime ∧ x₁.mem = x.mem ∧ x₁.regs P.baseReg = base ∧ x₁.regs P.frontierReg = base + space ∧ ∀ (j : Fin k_init), x₁.regs (P.initParams j) = params j) (setup_exec : ∀ {x₁ : WordRAM.Data r_ds}, WordRAM.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) → ∃ (y : WordRAM.Data r_ds), WordRAM.ExecWithin w P.initSetup x₁ y setupTime ∧ y.regs P.frontierReg = base + space ∧ rep s₀ y ∧ potential y ≤ initPotential ∧ WordRAM.Modifies { base := base, length := space }.footprint x₁.mem y.mem) (step_exec : ∀ {s : D.State} {x : WordRAM.Data r_ds} (o : D.Op), rep s x → D.valid s o → argMatch o x.regs → ∃ (y : WordRAM.Data r_ds) (n : ℕ), WordRAM.Exec w P.code x y n ∧ decode o y.regs = some (D.stepFn s o).2 ∧ rep (D.stepFn s o).1 y ∧ WordRAM.Modifies { base := base, length := space }.footprint x.mem y.mem ∧ n + potential y ≤ charge s o + potential x) : StateTransitionImpl P D w base params s₀

Construct a StateTransitionImpl for a deterministic specification ([D.HasStepFn f]) from a functional step_exec proof at (D.stepFn s o).

Projection 1: Basis lifting and standalone DynamicProgram / DataStructure theorems

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

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

@[reducible, inline]

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

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

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

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

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

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

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

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

theorem Cslib.DataStructure.WordRAM.StateTransitionImpl.run_client_demonic_amortized {r_ds k_init w base : ℕ} {D : StateTransitionSpec} {params : Fin k_init → ℕ} {s₀ : D.State} {P_std : WordRAM.SubroutineCode WordRAM.Basis.standard r_ds k_init} (C : StateTransitionImpl P_std D w base params s₀) {α : Type u_1} (p : D.Client α) {s : D.State} {x : WordRAM.Data r_ds} (hr : C.rep s x) (hv : D.DemonicValid s p) : ∃ (a : α) (y : WordRAM.Data r_ds) (traces : List WordRAM.DynamicProgram.OperationTrace) (s' : D.State) (tr : D.Transcript), Executes (C.toDynamicProgram.ExecOp w) p x a y traces ∧ D.ClientRun s p a s' tr ∧ C.rep s' y ∧ traces.length = List.length tr ∧ total WordRAM.DynamicProgram.OperationTrace.instructions traces + C.potential y ≤ D.totalCostTranscript (fun (s : D.State) (o : D.Op) => C.charge s o + 1) s tr + C.potential x

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

theorem Cslib.DataStructure.WordRAM.StateTransitionImpl.run_client_demonic_bound {r_ds k_init w base : ℕ} {D : StateTransitionSpec} {params : Fin k_init → ℕ} {s₀ : D.State} {P_std : WordRAM.SubroutineCode WordRAM.Basis.standard r_ds k_init} (C : StateTransitionImpl P_std D w base params s₀) (hpot : ∀ (x : WordRAM.Data r_ds), C.potential x = 0) {α : Type u_1} (p : D.Client α) {s : D.State} {x : WordRAM.Data r_ds} (hr : C.rep s x) (hv : D.DemonicValid s p) : ∃ (a : α) (y : WordRAM.Data r_ds) (traces : List WordRAM.DynamicProgram.OperationTrace) (s' : D.State) (tr : D.Transcript), Executes (C.toDynamicProgram.ExecOp w) p x a y traces ∧ D.ClientRun s p a s' tr ∧ C.rep s' y ∧ traces.length = List.length tr ∧ total WordRAM.DynamicProgram.OperationTrace.instructions traces ≤ D.totalCostTranscript (fun (s : D.State) (o : D.Op) => C.charge s o + 1) s tr

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

theorem Cslib.DataStructure.WordRAM.StateTransitionImpl.run_client_amortized {r_ds k_init w base : ℕ} {D : StateTransitionSpec} {params : Fin k_init → ℕ} {s₀ : D.State} {P_std : WordRAM.SubroutineCode WordRAM.Basis.standard r_ds k_init} (C : StateTransitionImpl P_std D w base params s₀) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α : Type u_1} (p : D.Client α) {s : D.State} {x : WordRAM.Data r_ds} (hr : C.rep s x) (hv : D.ValidHistory s (D.clientHistory s p)) : ∃ (y : WordRAM.Data r_ds) (traces : List WordRAM.DynamicProgram.OperationTrace), Executes (C.toDynamicProgram.ExecOp w) p x (D.clientResult s p) y traces ∧ C.rep (D.clientState s p) y ∧ total WordRAM.DynamicProgram.OperationTrace.instructions traces + C.potential y ≤ D.totalCost (fun (s : D.State) (o : D.Op) => C.charge s o + 1) s (D.clientHistory s p) + C.potential x

Standalone adaptive-client amortized bound on a deterministic specification.

theorem Cslib.DataStructure.WordRAM.StateTransitionImpl.run_client_bound {r_ds k_init w base : ℕ} {D : StateTransitionSpec} {params : Fin k_init → ℕ} {s₀ : D.State} {P_std : WordRAM.SubroutineCode WordRAM.Basis.standard r_ds k_init} (C : StateTransitionImpl P_std D w base params s₀) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (hpot : ∀ (x : WordRAM.Data r_ds), C.potential x = 0) {α : Type u_1} (p : D.Client α) {s : D.State} {x : WordRAM.Data r_ds} (hr : C.rep s x) (hv : D.ValidHistory s (D.clientHistory s p)) : ∃ (y : WordRAM.Data r_ds) (traces : List WordRAM.DynamicProgram.OperationTrace), Executes (C.toDynamicProgram.ExecOp w) p x (D.clientResult s p) y traces ∧ C.rep (D.clientState s p) y ∧ total WordRAM.DynamicProgram.OperationTrace.instructions traces ≤ D.totalCost (fun (s : D.State) (o : D.Op) => C.charge s o + 1) s (D.clientHistory s p)

Standalone adaptive-client worst-case bound on a deterministic specification when C.potential is identically zero.

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

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

Execute P.code.rename f inline when arguments already match (x.comap f).regs, witnessing a permitted outcome (s', a) with D.step s o s' a.

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

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

Deterministic specialization of code_rename for [D.HasStepFn g].

theorem Cslib.DataStructure.WordRAM.StateTransitionImpl.call_rename_ofFn {B : WordRAM.Basis} {r_ds r_caller k_init w base : ℕ} {P : WordRAM.SubroutineCode B r_ds k_init} {D : StateTransitionSpec} {params : Fin k_init → ℕ} {s₀ : D.State} {g : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn g] (C : StateTransitionImpl P D w base params s₀) {f : Fin r_ds → Fin r_caller} (hf : Function.Injective f) {s : D.State} {x x' : WordRAM.Data r_caller} {prep : WordRAM.Code B r_caller} {t_prep : ℕ} (o : D.Op) (hr : C.rep s (WordRAM.Data.comap f x)) (hv : D.valid s o) (hprep : WordRAM.ExecWithin w prep x x' t_prep) (hb' : WordRAM.Data.Bounded w (WordRAM.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 (WordRAM.Data.comap f x').regs) : ∃ (z : WordRAM.Data r_caller) (t : ℕ), WordRAM.ExecWithin w (prep.seq (WordRAM.Code.rename f P.code)) x z t ∧ C.decode o (WordRAM.Data.comap f z).regs = some (D.stepFn s o).2 ∧ C.rep (D.stepFn s o).1 (WordRAM.Data.comap f z) ∧ WordRAM.Modifies { base := base, length := C.space }.footprint x'.mem z.mem ∧ (∀ j ∉ Set.range f, z.regs j = x'.regs j) ∧ t + C.potential (WordRAM.Data.comap f z) ≤ t_prep + C.charge s o + C.potential (WordRAM.Data.comap f x)

Deterministic specialization of call_rename for [D.HasStepFn g].

Projection 3: Flat-program operation-sequence execution (RunsOps, run_ops_exact_*)

inductive Cslib.DataStructure.WordRAM.StateTransitionImpl.RunsOps {B : WordRAM.Basis} {r_ds k_init w base : ℕ} {P : WordRAM.SubroutineCode B r_ds k_init} {D : StateTransitionSpec} {params : Fin k_init → ℕ} {s₀ : D.State} (C : StateTransitionImpl P D w base params s₀) (prepRegs : D.Op → (Fin r_ds → ℕ) → Fin r_ds → ℕ := C.prepareRegs) : D.State → WordRAM.Data r_ds → List D.Op → D.Transcript → D.State → WordRAM.Data r_ds → ℕ → Prop

Sequential flat-program execution of ops : List D.Op by repeated calls to P.opProg: each call prepares input registers via prepRegs, runs P.opProg from pc = 0 to halt, decodes a permitted outcome (s₁, a) with D.step s o s₁ a, modifies memory only within [base, base + C.space), records the resulting transcript tr : D.Transcript, and accumulates total instructions executed (including each trailing halt).

• nil {B : WordRAM.Basis} {r_ds k_init w base : ℕ} {P : WordRAM.SubroutineCode B r_ds k_init} {D : StateTransitionSpec} {params : Fin k_init → ℕ} {s₀ : D.State} {C : StateTransitionImpl P D w base params s₀} {prepRegs : optParam (D.Op → (Fin r_ds → ℕ) → Fin r_ds → ℕ) C.prepareRegs} {s : D.State} {x : WordRAM.Data r_ds} : C.RunsOps prepRegs s x [] [] s x 0
• cons {B : WordRAM.Basis} {r_ds k_init w base : ℕ} {P : WordRAM.SubroutineCode B r_ds k_init} {D : StateTransitionSpec} {params : Fin k_init → ℕ} {s₀ : D.State} {C : StateTransitionImpl P D w base params s₀} {prepRegs : optParam (D.Op → (Fin r_ds → ℕ) → Fin r_ds → ℕ) C.prepareRegs} {s s₁ s₂ : D.State} {x : WordRAM.Data r_ds} {o : D.Op} {a : D.Result o} {ops : List D.Op} {tr : D.Transcript} {pc : ℕ} {y z : WordRAM.Data r_ds} {steps rest : ℕ} : WordRAM.Runs w P.opProg { pc := 0, data := { regs := prepRegs o x.regs, mem := x.mem } } { pc := pc, data := y } steps → (∃ (out : ℕ), WordRAM.step w P.opProg { pc := pc, data := y } = WordRAM.Outcome.halt out) → D.step s o s₁ a → C.decode o y.regs = some a → WordRAM.Modifies { base := base, length := C.space }.footprint x.mem y.mem → C.RunsOps prepRegs s₁ y ops tr s₂ z rest → C.RunsOps prepRegs s x (o :: ops) ({ op := o, result := a, nextState := s₁ } :: tr) s₂ z (steps + 1 + rest)

theorem Cslib.DataStructure.WordRAM.StateTransitionImpl.seq_runsOps_of_prep {B : WordRAM.Basis} {r_ds k_init w base : ℕ} {P : WordRAM.SubroutineCode B r_ds k_init} {D : StateTransitionSpec} {params : Fin k_init → ℕ} {s₀ : D.State} (C : StateTransitionImpl P D w base params s₀) (prepRegs : D.Op → (Fin r_ds → ℕ) → Fin r_ds → ℕ) (hfit : ∀ {s : D.State} (o : D.Op) (regs : Fin r_ds → ℕ), D.valid s o → (∀ (i : Fin r_ds), WordRAM.Fits w (regs i)) → ∀ (i : Fin r_ds), WordRAM.Fits w (prepRegs o regs i)) (hnot_in : ∀ (o : D.Op) (regs : Fin r_ds → ℕ) (i : Fin r_ds), P.input i = false → prepRegs o regs i = regs i) (harg : ∀ (o : D.Op) (regs : Fin r_ds → ℕ), C.argMatch o (prepRegs o regs)) (ops : List D.Op) {s : D.State} {x : WordRAM.Data r_ds} : C.rep s x → D.ValidOpSeq s ops → ∃ (tr : D.Transcript) (s_fin : D.State) (z : WordRAM.Data r_ds) (t_ops : ℕ), C.RunsOps prepRegs s x ops tr s_fin z t_ops ∧ tr.ops = ops ∧ D.ValidTranscript s tr s_fin ∧ C.rep s_fin z ∧ t_ops + C.potential z ≤ D.totalCostTranscript (fun (st : D.State) (o : D.Op) => C.charge st o + 1) s tr + C.potential x

Flat-program sequence execution under a custom register-preparation function prepRegs.

theorem Cslib.DataStructure.WordRAM.StateTransitionImpl.seq_runsOps {B : WordRAM.Basis} {r_ds k_init w base : ℕ} {P : WordRAM.SubroutineCode B r_ds k_init} {D : StateTransitionSpec} {params : Fin k_init → ℕ} {s₀ : D.State} (C : StateTransitionImpl P D w base params s₀) (ops : List D.Op) {s : D.State} {x : WordRAM.Data r_ds} (hr : C.rep s x) (hv : D.ValidOpSeq s ops) : ∃ (tr : D.Transcript) (s_fin : D.State) (z : WordRAM.Data r_ds) (t_ops : ℕ), C.RunsOps C.prepareRegs s x ops tr s_fin z t_ops ∧ tr.ops = ops ∧ D.ValidTranscript s tr s_fin ∧ C.rep s_fin z ∧ t_ops + C.potential z ≤ D.totalCostTranscript (fun (st : D.State) (o : D.Op) => C.charge st o + 1) s tr + C.potential x

Flat-program sequence execution using C.prepareRegs.

theorem Cslib.DataStructure.WordRAM.StateTransitionImpl.run_ops_exact_fresh {B : WordRAM.Basis} {r_ds k_init w base : ℕ} {P : WordRAM.SubroutineCode B r_ds k_init} {D : StateTransitionSpec} {params : Fin k_init → ℕ} {s₀ : D.State} (C : StateTransitionImpl P D w base params s₀) {d₀ : WordRAM.Data r_ds} (hd₀ : WordRAM.Data.Bounded w d₀) (hfr : d₀.regs P.frontierReg = base) (hpar : ∀ (j : Fin k_init), d₀.regs (P.initParams j) = params j) (hzero : ∀ a ∈ { base := base, length := C.space }.footprint, d₀.mem a = 0) (ops : List D.Op) (hv : D.ValidOpSeq s₀ ops) : ∃ (pc₀ : ℕ) (x₀ : WordRAM.Data r_ds) (t_init : ℕ) (tr : D.Transcript) (s_fin : D.State) (z : WordRAM.Data r_ds) (t_ops : ℕ), WordRAM.Runs w P.initFreshProg { pc := 0, data := d₀ } { pc := pc₀, data := x₀ } t_init ∧ (∃ (out : ℕ), WordRAM.step w P.initFreshProg { pc := pc₀, data := x₀ } = WordRAM.Outcome.halt out) ∧ WordRAM.Modifies { base := base, length := C.space }.footprint d₀.mem x₀.mem ∧ C.RunsOps C.prepareRegs s₀ x₀ ops tr s_fin z t_ops ∧ tr.ops = ops ∧ D.ValidTranscript s₀ tr s_fin ∧ C.rep s_fin z ∧ t_init ≤ C.initTime ∧ t_ops + C.potential z ≤ D.totalCostTranscript (fun (st : D.State) (o : D.Op) => C.charge st o + 1) s₀ tr + C.initPotential

Standalone flat-program operation-sequence theorem with fresh initialization on zeroed [base, base + C.space): P.initFreshProg runs at most C.initTime steps before its halt.

theorem Cslib.DataStructure.WordRAM.StateTransitionImpl.run_ops_exact_reusable {B : WordRAM.Basis} {r_ds k_init w base : ℕ} {P : WordRAM.SubroutineCode B r_ds k_init} {D : StateTransitionSpec} {params : Fin k_init → ℕ} {s₀ : D.State} (C : StateTransitionImpl P D w base params s₀) {d₀ : WordRAM.Data r_ds} (hd₀ : WordRAM.Data.Bounded w d₀) (hfr : d₀.regs P.frontierReg = base) (hpar : ∀ (j : Fin k_init), d₀.regs (P.initParams j) = params j) (ops : List D.Op) (hv : D.ValidOpSeq s₀ ops) : ∃ (pc₀ : ℕ) (x₀ : WordRAM.Data r_ds) (t_init : ℕ) (tr : D.Transcript) (s_fin : D.State) (z : WordRAM.Data r_ds) (t_ops : ℕ), WordRAM.Runs w P.initClearProg { pc := 0, data := d₀ } { pc := pc₀, data := x₀ } t_init ∧ (∃ (out : ℕ), WordRAM.step w P.initClearProg { pc := pc₀, data := x₀ } = WordRAM.Outcome.halt out) ∧ WordRAM.Modifies { base := base, length := C.space }.footprint d₀.mem x₀.mem ∧ C.RunsOps C.prepareRegs s₀ x₀ ops tr s_fin z t_ops ∧ tr.ops = ops ∧ D.ValidTranscript s₀ tr s_fin ∧ C.rep s_fin z ∧ t_init ≤ C.initTime + 4 * C.space + 6 ∧ t_ops + C.potential z ≤ D.totalCostTranscript (fun (st : D.State) (o : D.Op) => C.charge st o + 1) s₀ tr + C.initPotential

Standalone flat-program operation-sequence theorem with reusable initialization on arbitrary w-bounded memory: P.initClearProg runs at most C.initTime + 4 * C.space + 6 steps before its halt.

theorem Cslib.DataStructure.WordRAM.StateTransitionImpl.run_ops_exact_fresh_ofFn {B : WordRAM.Basis} {r_ds k_init w base : ℕ} {P : WordRAM.SubroutineCode B r_ds k_init} {D : StateTransitionSpec} {params : Fin k_init → ℕ} {s₀ : D.State} {g : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn g] (C : StateTransitionImpl P D w base params s₀) {d₀ : WordRAM.Data r_ds} (hd₀ : WordRAM.Data.Bounded w d₀) (hfr : d₀.regs P.frontierReg = base) (hpar : ∀ (j : Fin k_init), d₀.regs (P.initParams j) = params j) (hzero : ∀ a ∈ { base := base, length := C.space }.footprint, d₀.mem a = 0) (ops : List D.Op) (hv : D.ValidHistory s₀ ops) : ∃ (pc₀ : ℕ) (x₀ : WordRAM.Data r_ds) (t_init : ℕ) (z : WordRAM.Data r_ds) (t_ops : ℕ), WordRAM.Runs w P.initFreshProg { pc := 0, data := d₀ } { pc := pc₀, data := x₀ } t_init ∧ (∃ (out : ℕ), WordRAM.step w P.initFreshProg { pc := pc₀, data := x₀ } = WordRAM.Outcome.halt out) ∧ WordRAM.Modifies { base := base, length := C.space }.footprint d₀.mem x₀.mem ∧ C.RunsOps C.prepareRegs s₀ x₀ ops (D.canonicalTranscript s₀ ops) (D.run s₀ ops).1 z t_ops ∧ C.rep (D.run s₀ ops).1 z ∧ t_init ≤ C.initTime ∧ t_ops + C.potential z ≤ D.totalCost (fun (st : D.State) (o : D.Op) => C.charge st o + 1) s₀ ops + C.initPotential

Deterministic specialization of run_ops_exact_fresh for [D.HasStepFn g], executing the canonical transcript D.canonicalTranscript s₀ ops to (D.run s₀ ops).1.

theorem Cslib.DataStructure.WordRAM.StateTransitionImpl.run_ops_exact_reusable_ofFn {B : WordRAM.Basis} {r_ds k_init w base : ℕ} {P : WordRAM.SubroutineCode B r_ds k_init} {D : StateTransitionSpec} {params : Fin k_init → ℕ} {s₀ : D.State} {g : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn g] (C : StateTransitionImpl P D w base params s₀) {d₀ : WordRAM.Data r_ds} (hd₀ : WordRAM.Data.Bounded w d₀) (hfr : d₀.regs P.frontierReg = base) (hpar : ∀ (j : Fin k_init), d₀.regs (P.initParams j) = params j) (ops : List D.Op) (hv : D.ValidHistory s₀ ops) : ∃ (pc₀ : ℕ) (x₀ : WordRAM.Data r_ds) (t_init : ℕ) (z : WordRAM.Data r_ds) (t_ops : ℕ), WordRAM.Runs w P.initClearProg { pc := 0, data := d₀ } { pc := pc₀, data := x₀ } t_init ∧ (∃ (out : ℕ), WordRAM.step w P.initClearProg { pc := pc₀, data := x₀ } = WordRAM.Outcome.halt out) ∧ WordRAM.Modifies { base := base, length := C.space }.footprint d₀.mem x₀.mem ∧ C.RunsOps C.prepareRegs s₀ x₀ ops (D.canonicalTranscript s₀ ops) (D.run s₀ ops).1 z t_ops ∧ C.rep (D.run s₀ ops).1 z ∧ t_init ≤ C.initTime + 4 * C.space + 6 ∧ t_ops + C.potential z ≤ D.totalCost (fun (st : D.State) (o : D.Op) => C.charge st o + 1) s₀ ops + C.initPotential

Deterministic specialization of run_ops_exact_reusable for [D.HasStepFn g], executing the canonical transcript D.canonicalTranscript s₀ ops to (D.run s₀ ops).1.