Composable Randomized Word-RAM State-Transition Implementations

This file extends the relational Cslib.DataStructure.WordRAM.StateTransitionImpl interface to randomized data structures and Las Vegas subroutines on the Word-RAM — covering both structures initialized from a random seed (such as universal hash tables, 2-choice hash tables, and cuckoo hash tables) and structures whose operations make random choices via Instr.rand (such as treaps, skip lists, reservoir samplers, or randomized rehashing); see [MU17], Sections 2.1, 2.3, and 2.4.

Core design

A Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl P D w base params s₀ couples machine execution with a latent seed type Seed : Type, the relational abstract state D.State, and a reference distribution seedLaw : PMF Seed up to a bounded density factor seedSlack : ℝ≥0∞:

1. Seed-coupled representation (rep θ s x) and potential (potential θ x):

   • Data structures without a persistent random seed set Seed := Unit, seedLaw := PMF.pure (), and seedSlack := 1 (in particular, Cslib.DataStructure.WordRAM.StateTransitionImpl.toRandomized embeds every relational Cslib.DataStructure.WordRAM.StateTransitionImpl directly).
   • Hash tables that resample their hash family on rare table-full events maintain a joint distribution whose marginal on Seed satisfies (ν.map Prod.fst) θ ≤ seedSlack * seedLaw θ.

2. Distributional execution (ExecCodeDist):

   • setup_exec and step_exec use ExecCodeDist from CslibFrontier.Computability.WordRAM.Randomized.Expected, which supports both bounded randomized code (ExecRand) and unbounded almost-surely terminating Las Vegas while loops (ExecCodeDist.loop_geometric).

3. Addition-only ℝ≥0∞ amortized-in-expectation bound:

   • Every operation o : D.Op from a coupled state distribution ν : PMF (CoupledState Seed D.State r_ds) whose support states satisfy D.valid t.state o (and are concentrated on a single abstract state when C.singleState holds) produces a transition kernel μ_step : CoupledState Seed D.State r_ds → PMF (CoupledState Seed D.State r_ds) and expected step count T_step : CoupledState Seed D.State r_ds → ℝ≥0∞ angelically realizing D.step t.state o q.state a on every branch, preserving single-state support (when C.singleState holds) and the seed-marginal bound, and satisfying (for Φ(t) := potential t.seed t.data) ∑' t, ν t * (T_step t + ∑' q, μ_step t q * Φ(q)) ≤ ∑' t, ν t * (charge t.state o + Φ(t)).
   • General relational certificates (singleState := False, the default, including Cslib.DataStructure.WordRAM.StateTransitionImpl.toRandomized) apply to arbitrary branch-dependent state distributions ν : PMF (CoupledState Seed D.State r_ds), whether D is deterministic or nondeterministic.
   • For functional specifications ([D.HasStepFn f]), StateTransitionImpl.ofFn (singleState := True), step_exec_ofFn, frame_caller_dist_ofFn, code_rename_ofFn, call_rename_ofFn, ExecStepsOfFn, steps_expected_amortized_ofFn, and seq_expected_amortized_ofFn specialize the interface to a single deterministic abstract state s : D.State and distribution ν : PMF (Seed × Data r_ds) (preventing adaptive correlation between s and the latent seed θ in oblivious-adversary structures).

The sequence theorems charge initialization and subroutine bodies for a fixed operation list. prepare delivers each operation's arguments by a semantic register replacement; its encoding and delivery, caller dispatch and a whole-client driver are not charged. Callers requiring native argument preparation can use call_rename / call_rename_ofFn, whose B_prep explicitly charges the preparation code. Compiling a standalone body adds the final halt separately via ExecCodeDist.program_halts.

Main definitions

• Cslib.DataStructure.WordRAM.Randomized.CoupledState: coupled latent seed, abstract specification state, and concrete Word-RAM state for relational randomized subroutine analysis.
• Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl: reusable randomized Word-RAM subroutine certificate for a relational specification D : StateTransitionSpec.
• Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.ofFn: constructor for functional specifications [D.HasStepFn f].
• Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.ExecSteps, ExecStepsOfFn: multi-operation distributional execution traces across ops : List D.Op.
• Cslib.DataStructure.WordRAM.StateTransitionImpl.toRandomized: canonical embedding of any relational Cslib.DataStructure.WordRAM.StateTransitionImpl into Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.
• Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.mapSimulates, toStandard: basis transport from Basis.exact to Basis.standard.

Main results

• Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.initFresh_exec, initFresh_rename: expected-time initialization on fresh zeroed memory.
• Cslib.WordRAM.SubroutineCode.zeroFillCode_exec, Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.initClear_exec, initClear_rename: expected-time initialization on arbitrary dirty memory.
• Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.code_rename, call_rename, code_rename_ofFn, call_rename_ofFn: inline subroutine invocation on caller state space Data r_caller via register injection f : Fin r_ds → Fin r_caller.
• Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.frame_caller, frame_caller_dist, frame_caller_dist_ofFn: preservation of rep, potential, and the coupled caller distribution across arbitrary deterministic or randomized caller steps that do not modify persistent DS registers (P.input i = false) or [base, base + space).
• Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.steps_expected_amortized, seq_expected_amortized, steps_expected_amortized_ofFn, seq_expected_amortized_ofFn: telescope theorems bounding initialization and expected body time across any admissible operation sequence ops : List D.Op.

References

• T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, Introduction to Algorithms, Chapter 17
• M. Mitzenmacher and E. Upfal, Probability and Computing: Randomization and Probabilistic Techniques in Algorithms and Data Analysis, Sections 2.1, 2.3, and 2.4.

structure Cslib.DataStructure.WordRAM.Randomized.CoupledState (Seed : Type) (State : Type u) (r : ℕ) : Type u

Coupled latent seed, abstract specification state, and concrete Word-RAM state for relational randomized subroutine analysis.

• seed : Seed

  Latent random seed.

• state : State

  Abstract specification state.

• data : WordRAM.Data r

  Concrete Word-RAM register and memory state.

structure Cslib.DataStructure.WordRAM.Randomized.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) : Type (max u v z 1)

Unified standalone and inline subroutine specification/resource certificate for a randomized Word-RAM data structure P realizing a relational specification D at word width w, base address base, runtime parameters params, and initial abstract state s₀.

• Seed : Type

  Latent random seed type (use Unit when no persistent seed is needed).

• seedLaw : PMF self.Seed

  Reference distribution over latent seeds.

• seedSlack : ENNReal

  Marginal density slack factor (1 when the seed distribution is exact).

• seedSlack_ne_top : self.seedSlack ≠ ⊤

  The marginal density slack factor is finite.

• space : ℕ

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

• spanTime : ℕ

  Worst-case instruction bound for P.allocSpan.

• setupTime : ENNReal

  Expected instruction bound for P.initSetup.

• initPotential : ℕ

  Upper bound on initial concrete potential after initialization.

• charge : D.State → D.Op → ℕ

  Amortized instruction charge per operation.

• rep : self.Seed → D.State → WordRAM.Data r_ds → Prop

  Seed-indexed representation invariant linking Seed, D.State, and Data r_ds.

• potential : self.Seed → WordRAM.Data r_ds → ℕ

  Seed-indexed nonnegative integer potential.

• encode : D.Op → Fin r_ds → ℕ

  Standalone register encoding for argument delivery.

• 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 {θ : self.Seed} {s : D.State} {x : WordRAM.Data r_ds} : self.rep θ s x → WordRAM.Data.Bounded w x

  Represented configurations are word-bounded.

• arguments_fit {s : D.State} (o : D.Op) : D.valid s o → ∀ (i : Fin r_ds), P.input i = true → WordRAM.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 argument delivery satisfies argMatch.

• rep_supported {θ : self.Seed} {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 := self.space }.footprint, x'.mem a = x.mem a) → WordRAM.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 {θ : self.Seed} {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 := 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 : 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))

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

• 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₁ 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₁ : WordRAM.Data r_ds} : WordRAM.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) → ∃ (ν₀ : PMF (self.Seed × WordRAM.Data r_ds)), WordRAM.ExecCodeDist w P.initSetup x₁ (PMF.map Prod.snd ν₀) self.setupTime ∧ (∀ (θ : self.Seed), (PMF.map Prod.fst ν₀) θ ≤ self.seedSlack * self.seedLaw θ) ∧ ∀ p ∈ ν₀.support, p.2.regs P.frontierReg = base + self.space ∧ self.rep p.1 s₀ p.2 ∧ self.potential p.1 p.2 ≤ self.initPotential ∧ WordRAM.Modifies { base := base, length := self.space }.footprint x₁.mem p.2.mem

  Execution of P.initSetup once [base, base + space) holds zeros, producing a coupled distribution ν₀ : PMF (Seed × Data r_ds) whose seed marginal is bounded by seedSlack * seedLaw.

• singleState : Prop

  Whether step_exec requires the pre-state distribution ν to be concentrated on a single abstract state s : D.State (False by default for general relational certificates, allowing branch-dependent state distributions even when D is deterministic; True for single-state functional certificates constructed via StateTransitionImpl.ofFn, where the oblivious adversary fixes a single abstract state s independent of the latent seed θ and every branch transitions to (D.stepFn s o).1).

• step_exec (o : D.Op) (ν : PMF (CoupledState self.Seed D.State r_ds)) : (self.singleState → ∃ (s : D.State), ∀ t ∈ ν.support, t.state = s) → (∀ (θ : self.Seed), (PMF.map CoupledState.seed ν) θ ≤ self.seedSlack * self.seedLaw θ) → (∀ t ∈ ν.support, D.valid t.state o ∧ self.rep t.seed t.state t.data ∧ self.argMatch o t.data.regs) → ∃ (μ_step : CoupledState self.Seed D.State r_ds → PMF (CoupledState self.Seed D.State r_ds)) (T_step : CoupledState self.Seed D.State r_ds → ENNReal), (∀ t ∈ ν.support, WordRAM.ExecCodeDist w P.code t.data (PMF.map CoupledState.data (μ_step t)) (T_step t) ∧ ∀ q ∈ (μ_step t).support, ∃ (a : D.Result o), D.step t.state o q.state a ∧ self.decode o q.data.regs = some a ∧ self.rep q.seed q.state q.data ∧ WordRAM.Modifies { base := base, length := self.space }.footprint t.data.mem q.data.mem) ∧ (∀ (θ' : self.Seed), (PMF.map CoupledState.seed (ν.bind μ_step)) θ' ≤ self.seedSlack * self.seedLaw θ') ∧ (self.singleState → ∃ (s' : D.State), ∀ q ∈ (ν.bind μ_step).support, q.state = s') ∧ ∑' (t : CoupledState self.Seed D.State r_ds), ν t * (T_step t + ∑' (q : CoupledState self.Seed D.State r_ds), (μ_step t) q * ↑(self.potential q.seed q.data)) ≤ ∑' (t : CoupledState self.Seed D.State r_ds), ν t * (↑(self.charge t.state o) + ↑(self.potential t.seed t.data))

  Coupled one-step execution of P.code for any operation o from a coupled distribution ν : PMF (CoupledState Seed D.State r_ds) (supported on a single abstract state when singleState holds) with seed marginal bounded by seedSlack * seedLaw: produces a transition kernel μ_step and expected step count T_step preserving single-state support (when singleState holds) and the seed-marginal bound, angelically realizing D.step t.state o q.state a, modifying only [base, base + space), and satisfying the addition-only ℝ≥0∞ amortized-in-expectation inequality.

noncomputable def Cslib.DataStructure.WordRAM.StateTransitionImpl.toRandomized {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₀) : Randomized.StateTransitionImpl P D w base params s₀

Canonical embedding of any relational Cslib.DataStructure.WordRAM.StateTransitionImpl certificate into Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl (Seed := Unit, seedLaw := PMF.pure (), seedSlack := 1).

def Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.initTime {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₀) : ENNReal

Total expected instruction bound for P.initFresh.

@[reducible, inline]

noncomputable abbrev Cslib.DataStructure.WordRAM.Randomized.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} {stepFn : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn stepFn] (Seed : Type) (seedLaw : PMF Seed) (seedSlack : ENNReal := 1) (seedSlack_ne_top : seedSlack ≠ ⊤ := by simp) (space spanTime : ℕ) (setupTime : ENNReal) (initPotential : ℕ) (charge : D.State → D.Op → ℕ) (rep : Seed → D.State → WordRAM.Data r_ds → Prop) (potential : Seed → 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 : ∀ {θ : Seed} {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 : ∀ {θ : Seed} {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 : ∀ {θ : Seed} {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) → ∃ (ν₀ : PMF (Seed × WordRAM.Data r_ds)), WordRAM.ExecCodeDist w P.initSetup x₁ (PMF.map Prod.snd ν₀) setupTime ∧ (∀ (θ : Seed), (PMF.map Prod.fst ν₀) θ ≤ seedSlack * seedLaw θ) ∧ ∀ p ∈ ν₀.support, p.2.regs P.frontierReg = base + space ∧ rep p.1 s₀ p.2 ∧ potential p.1 p.2 ≤ initPotential ∧ WordRAM.Modifies { base := base, length := space }.footprint x₁.mem p.2.mem) (step_exec : ∀ {s : D.State} (o : D.Op) (ν : PMF (Seed × WordRAM.Data r_ds)), D.valid s o → (∀ (θ : Seed), (PMF.map Prod.fst ν) θ ≤ seedSlack * seedLaw θ) → (∀ p ∈ ν.support, rep p.1 s p.2 ∧ argMatch o p.2.regs) → ∃ (μ_step : Seed × WordRAM.Data r_ds → PMF (Seed × WordRAM.Data r_ds)) (T_step : Seed × WordRAM.Data r_ds → ENNReal), (∀ p ∈ ν.support, WordRAM.ExecCodeDist w P.code p.2 (PMF.map Prod.snd (μ_step p)) (T_step p) ∧ ∀ q ∈ (μ_step p).support, decode o q.2.regs = some (D.stepFn s o).2 ∧ rep q.1 (D.stepFn s o).1 q.2 ∧ WordRAM.Modifies { base := base, length := space }.footprint p.2.mem q.2.mem) ∧ (∀ (θ' : Seed), (PMF.map Prod.fst (ν.bind μ_step)) θ' ≤ seedSlack * seedLaw θ') ∧ ∑' (p : Seed × WordRAM.Data r_ds), ν p * (T_step p + ∑' (q : Seed × WordRAM.Data r_ds), (μ_step p) q * ↑(potential q.1 q.2)) ≤ ↑(charge s o) + ∑' (p : Seed × WordRAM.Data r_ds), ν p * ↑(potential p.1 p.2)) : StateTransitionImpl P D w base params s₀

Construct a randomized StateTransitionImpl certificate for a functional specification [D.HasStepFn stepFn].

theorem Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.step_exec_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} (C : StateTransitionImpl P D w base params s₀) {stepFn : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn stepFn] {s : D.State} (o : D.Op) (ν : PMF (C.Seed × WordRAM.Data r_ds)) (hv : D.valid s o) (hseed : ∀ (θ : C.Seed), (PMF.map Prod.fst ν) θ ≤ C.seedSlack * C.seedLaw θ) (hsupp : ∀ p ∈ ν.support, C.rep p.1 s p.2 ∧ C.argMatch o p.2.regs) : ∃ (μ_step : C.Seed × WordRAM.Data r_ds → PMF (C.Seed × WordRAM.Data r_ds)) (T_step : C.Seed × WordRAM.Data r_ds → ENNReal), (∀ p ∈ ν.support, WordRAM.ExecCodeDist w P.code p.2 (PMF.map Prod.snd (μ_step p)) (T_step p) ∧ ∀ q ∈ (μ_step p).support, C.decode o q.2.regs = some (D.stepFn s o).2 ∧ C.rep q.1 (D.stepFn s o).1 q.2 ∧ WordRAM.Modifies { base := base, length := C.space }.footprint p.2.mem q.2.mem) ∧ (∀ (θ' : C.Seed), (PMF.map Prod.fst (ν.bind μ_step)) θ' ≤ C.seedSlack * C.seedLaw θ') ∧ ∑' (p : C.Seed × WordRAM.Data r_ds), ν p * (T_step p + ∑' (q : C.Seed × WordRAM.Data r_ds), (μ_step p) q * ↑(C.potential q.1 q.2)) ≤ ↑(C.charge s o) + ∑' (p : C.Seed × WordRAM.Data r_ds), ν p * ↑(C.potential p.1 p.2)

Deterministic one-step execution of P.code when [D.HasStepFn stepFn].

Projection 1: Basis lifting (mapSimulates, toStandard)

def Cslib.DataStructure.WordRAM.Randomized.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 randomized StateTransitionImpl certificate along any defined-evaluation basis simulation.

@[reducible, inline]

abbrev Cslib.DataStructure.WordRAM.Randomized.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 randomized StateTransitionImpl certificate to Basis.standard.

Projection 2: Fresh initialization and register relocation (initFresh_exec,

initFresh_rename)

theorem Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.initFresh_exec {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₀) {x : WordRAM.Data r_ds} (hx : WordRAM.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) : ∃ (ν₀ : PMF (C.Seed × WordRAM.Data r_ds)), WordRAM.ExecCodeDist w P.initFresh x (PMF.map Prod.snd ν₀) C.initTime ∧ (∀ (θ : C.Seed), (PMF.map Prod.fst ν₀) θ ≤ C.seedSlack * C.seedLaw θ) ∧ ∀ p ∈ ν₀.support, p.2.regs P.frontierReg = base + C.space ∧ C.rep p.1 s₀ p.2 ∧ C.potential p.1 p.2 ≤ C.initPotential ∧ WordRAM.Modifies { base := base, length := C.space }.footprint x.mem p.2.mem

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

theorem Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.initFresh_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) {x : WordRAM.Data r_caller} (hx : WordRAM.Data.Bounded w (WordRAM.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) : ∃ (ν₀ : PMF (C.Seed × WordRAM.Data r_caller)), WordRAM.ExecCodeDist w (WordRAM.Code.rename f P.initFresh) x (PMF.map Prod.snd ν₀) C.initTime ∧ (∀ (θ : C.Seed), (PMF.map Prod.fst ν₀) θ ≤ C.seedSlack * C.seedLaw θ) ∧ ∀ p ∈ ν₀.support, p.2.regs (f P.frontierReg) = base + C.space ∧ C.rep p.1 s₀ (WordRAM.Data.comap f p.2) ∧ C.potential p.1 (WordRAM.Data.comap f p.2) ≤ C.initPotential ∧ WordRAM.Modifies { base := base, length := C.space }.footprint x.mem p.2.mem ∧ ∀ j ∉ Set.range f, p.2.regs j = x.regs j

Relocated fresh initialization along any injective register embedding f.

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

initClear_exec, initClear_rename)

theorem Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.initClear_exec {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₀) {x : WordRAM.Data r_ds} (hx : WordRAM.Data.Bounded w x) (hfr : x.regs P.frontierReg = base) (hpar : ∀ (j : Fin k_init), x.regs (P.initParams j) = params j) : ∃ (ν₀ : PMF (C.Seed × WordRAM.Data r_ds)), WordRAM.ExecCodeDist w P.initClear x (PMF.map Prod.snd ν₀) (C.initTime + ↑(4 * C.space + 6)) ∧ (∀ (θ : C.Seed), (PMF.map Prod.fst ν₀) θ ≤ C.seedSlack * C.seedLaw θ) ∧ ∀ p ∈ ν₀.support, p.2.regs P.frontierReg = base + C.space ∧ C.rep p.1 s₀ p.2 ∧ C.potential p.1 p.2 ≤ C.initPotential ∧ WordRAM.Modifies { base := base, length := C.space }.footprint x.mem p.2.mem

Execute P.initClear on arbitrary dirty memory in C.initTime + (4 * C.space + 6 : ℕ) expected instructions.

theorem Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.initClear_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) {x : WordRAM.Data r_caller} (hx : WordRAM.Data.Bounded w (WordRAM.Data.comap f x)) (hfr : x.regs (f P.frontierReg) = base) (hpar : ∀ (j : Fin k_init), x.regs (f (P.initParams j)) = params j) : ∃ (ν₀ : PMF (C.Seed × WordRAM.Data r_caller)), WordRAM.ExecCodeDist w (WordRAM.Code.rename f P.initClear) x (PMF.map Prod.snd ν₀) (C.initTime + ↑(4 * C.space + 6)) ∧ (∀ (θ : C.Seed), (PMF.map Prod.fst ν₀) θ ≤ C.seedSlack * C.seedLaw θ) ∧ ∀ p ∈ ν₀.support, p.2.regs (f P.frontierReg) = base + C.space ∧ C.rep p.1 s₀ (WordRAM.Data.comap f p.2) ∧ C.potential p.1 (WordRAM.Data.comap f p.2) ≤ C.initPotential ∧ WordRAM.Modifies { base := base, length := C.space }.footprint x.mem p.2.mem ∧ ∀ j ∉ Set.range f, p.2.regs j = x.regs j

Relocated O(space) dirty-memory initialization along any injective register embedding f.

Projection 4: Caller-to-DS bidirectional framing (frame_caller, frame_caller_dist,

frame_caller_dist_ofFn)

theorem Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.frame_caller {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} {θ : C.Seed} {s : D.State} {x x' : WordRAM.Data r_caller} {F : Finset ℕ} (hr : C.rep θ s (WordRAM.Data.comap f x)) (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)) (hdisj : Disjoint { base := base, length := C.space }.footprint F) (hmem : WordRAM.Modifies F x.mem x'.mem) : C.rep θ s (WordRAM.Data.comap f x') ∧ C.potential θ (WordRAM.Data.comap f x') = C.potential θ (WordRAM.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).

noncomputable def Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.frameStateDist {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₀) (ν : PMF (CoupledState C.Seed D.State r_caller)) (μ_caller : CoupledState C.Seed D.State r_caller → PMF (WordRAM.Data r_caller)) : PMF (CoupledState C.Seed D.State r_caller)

Coupled caller distribution on CoupledState C.Seed D.State r_caller after a caller transition kernel μ_caller that does not resample the DS seed or change the abstract DS state.

@[simp]

theorem Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.frameStateDist_map_seed {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₀) (ν : PMF (CoupledState C.Seed D.State r_caller)) (μ_caller : CoupledState C.Seed D.State r_caller → PMF (WordRAM.Data r_caller)) : PMF.map CoupledState.seed (C.frameStateDist ν μ_caller) = PMF.map CoupledState.seed ν

theorem Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.frame_caller_dist {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} {ν : PMF (CoupledState C.Seed D.State r_caller)} {μ_caller : CoupledState C.Seed D.State r_caller → PMF (WordRAM.Data r_caller)} {F : Finset ℕ} (hseed : ∀ (θ : C.Seed), (PMF.map CoupledState.seed ν) θ ≤ C.seedSlack * C.seedLaw θ) (hrep : ∀ t ∈ ν.support, C.rep t.seed t.state (WordRAM.Data.comap f t.data)) (hdisj : Disjoint { base := base, length := C.space }.footprint F) (hframe : ∀ t ∈ ν.support, ∀ x' ∈ (μ_caller t).support, WordRAM.Data.Bounded w (WordRAM.Data.comap f x') ∧ (∀ (i : Fin r_ds), P.input i = false → x'.regs (f i) = t.data.regs (f i)) ∧ WordRAM.Modifies F t.data.mem x'.mem) : (∀ (θ : C.Seed), (PMF.map CoupledState.seed (C.frameStateDist ν μ_caller)) θ ≤ C.seedSlack * C.seedLaw θ) ∧ (∀ q ∈ (C.frameStateDist ν μ_caller).support, C.rep q.seed q.state (WordRAM.Data.comap f q.data)) ∧ ∑' (q : CoupledState C.Seed D.State r_caller), (C.frameStateDist ν μ_caller) q * ↑(C.potential q.seed (WordRAM.Data.comap f q.data)) = ∑' (t : CoupledState C.Seed D.State r_caller), ν t * ↑(C.potential t.seed (WordRAM.Data.comap f t.data))

Distributional caller framing: any deterministic or randomized caller transition kernel μ_caller (including caller steps that execute Instr.rand) 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 the coupled seed marginal bound, C.rep, and expected potential under C.frameStateDist ν μ_caller.

noncomputable def Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.frameDist {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₀) (ν : PMF (C.Seed × WordRAM.Data r_caller)) (μ_caller : C.Seed × WordRAM.Data r_caller → PMF (WordRAM.Data r_caller)) : PMF (C.Seed × WordRAM.Data r_caller)

Coupled caller distribution after a caller transition kernel μ_caller that does not resample the DS seed θ.

@[simp]

theorem Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.frameDist_map_fst {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₀) (ν : PMF (C.Seed × WordRAM.Data r_caller)) (μ_caller : C.Seed × WordRAM.Data r_caller → PMF (WordRAM.Data r_caller)) : PMF.map Prod.fst (C.frameDist ν μ_caller) = PMF.map Prod.fst ν

theorem Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.frame_caller_dist_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} (C : StateTransitionImpl P D w base params s₀) {f : Fin r_ds → Fin r_caller} {s : D.State} {ν : PMF (C.Seed × WordRAM.Data r_caller)} {μ_caller : C.Seed × WordRAM.Data r_caller → PMF (WordRAM.Data r_caller)} {F : Finset ℕ} (hseed : ∀ (θ : C.Seed), (PMF.map Prod.fst ν) θ ≤ C.seedSlack * C.seedLaw θ) (hrep : ∀ p ∈ ν.support, C.rep p.1 s (WordRAM.Data.comap f p.2)) (hdisj : Disjoint { base := base, length := C.space }.footprint F) (hframe : ∀ p ∈ ν.support, ∀ x' ∈ (μ_caller p).support, WordRAM.Data.Bounded w (WordRAM.Data.comap f x') ∧ (∀ (i : Fin r_ds), P.input i = false → x'.regs (f i) = p.2.regs (f i)) ∧ WordRAM.Modifies F p.2.mem x'.mem) : (∀ (θ : C.Seed), (PMF.map Prod.fst (C.frameDist ν μ_caller)) θ ≤ C.seedSlack * C.seedLaw θ) ∧ (∀ q ∈ (C.frameDist ν μ_caller).support, C.rep q.1 s (WordRAM.Data.comap f q.2)) ∧ ∑' (q : C.Seed × WordRAM.Data r_caller), (C.frameDist ν μ_caller) q * ↑(C.potential q.1 (WordRAM.Data.comap f q.2)) = ∑' (p : C.Seed × WordRAM.Data r_caller), ν p * ↑(C.potential p.1 (WordRAM.Data.comap f p.2))

Single-state distributional caller framing: any deterministic or randomized caller transition kernel μ_caller 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 the coupled seed marginal bound, C.rep, and expected potential under C.frameDist ν μ_caller.

Projection 5: Relocated inline subroutine calls (code_rename, call_rename,

code_rename_ofFn, call_rename_ofFn)

theorem Cslib.DataStructure.WordRAM.Randomized.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) (o : D.Op) (ν : PMF (CoupledState C.Seed D.State r_caller)) (hseed : ∀ (θ : C.Seed), (PMF.map CoupledState.seed ν) θ ≤ C.seedSlack * C.seedLaw θ) (hsupp : ∀ t ∈ ν.support, D.valid t.state o ∧ C.rep t.seed t.state (WordRAM.Data.comap f t.data) ∧ C.argMatch o (WordRAM.Data.comap f t.data).regs) (hsingle : C.singleState → ∃ (s : D.State), ∀ t ∈ ν.support, t.state = s := by intro h; cases h) : ∃ (μ_caller : CoupledState C.Seed D.State r_caller → PMF (CoupledState C.Seed D.State r_caller)) (T_caller : CoupledState C.Seed D.State r_caller → ENNReal), (∀ t ∈ ν.support, WordRAM.ExecCodeDist w (WordRAM.Code.rename f P.code) t.data (PMF.map CoupledState.data (μ_caller t)) (T_caller t) ∧ ∀ q ∈ (μ_caller t).support, ∃ (a : D.Result o), D.step t.state o q.state a ∧ C.decode o (WordRAM.Data.comap f q.data).regs = some a ∧ C.rep q.seed q.state (WordRAM.Data.comap f q.data) ∧ WordRAM.Modifies { base := base, length := C.space }.footprint t.data.mem q.data.mem ∧ ∀ j ∉ Set.range f, q.data.regs j = t.data.regs j) ∧ (∀ (θ' : C.Seed), (PMF.map CoupledState.seed (ν.bind μ_caller)) θ' ≤ C.seedSlack * C.seedLaw θ') ∧ ∑' (t : CoupledState C.Seed D.State r_caller), ν t * (T_caller t + ∑' (q : CoupledState C.Seed D.State r_caller), (μ_caller t) q * ↑(C.potential q.seed (WordRAM.Data.comap f q.data))) ≤ ∑' (t : CoupledState C.Seed D.State r_caller), ν t * (↑(C.charge t.state o) + ↑(C.potential t.seed (WordRAM.Data.comap f t.data)))

Execute P.code.rename f inline when arguments already match (t.data.comap f).regs on the support of a coupled caller distribution ν : PMF (CoupledState C.Seed D.State r_caller).

theorem Cslib.DataStructure.WordRAM.Randomized.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} (C : StateTransitionImpl P D w base params s₀) {stepFn : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn stepFn] {f : Fin r_ds → Fin r_caller} (hf : Function.Injective f) {s : D.State} (o : D.Op) (ν : PMF (C.Seed × WordRAM.Data r_caller)) (hv : D.valid s o) (hseed : ∀ (θ : C.Seed), (PMF.map Prod.fst ν) θ ≤ C.seedSlack * C.seedLaw θ) (hsupp : ∀ p ∈ ν.support, C.rep p.1 s (WordRAM.Data.comap f p.2) ∧ C.argMatch o (WordRAM.Data.comap f p.2).regs) : ∃ (μ_caller : C.Seed × WordRAM.Data r_caller → PMF (C.Seed × WordRAM.Data r_caller)) (T_caller : C.Seed × WordRAM.Data r_caller → ENNReal), (∀ p ∈ ν.support, WordRAM.ExecCodeDist w (WordRAM.Code.rename f P.code) p.2 (PMF.map Prod.snd (μ_caller p)) (T_caller p) ∧ ∀ q ∈ (μ_caller p).support, C.decode o (WordRAM.Data.comap f q.2).regs = some (D.stepFn s o).2 ∧ C.rep q.1 (D.stepFn s o).1 (WordRAM.Data.comap f q.2) ∧ WordRAM.Modifies { base := base, length := C.space }.footprint p.2.mem q.2.mem ∧ ∀ j ∉ Set.range f, q.2.regs j = p.2.regs j) ∧ (∀ (θ' : C.Seed), (PMF.map Prod.fst (ν.bind μ_caller)) θ' ≤ C.seedSlack * C.seedLaw θ') ∧ ∑' (p : C.Seed × WordRAM.Data r_caller), ν p * (T_caller p + ∑' (q : C.Seed × WordRAM.Data r_caller), (μ_caller p) q * ↑(C.potential q.1 (WordRAM.Data.comap f q.2))) ≤ ↑(C.charge s o) + ∑' (p : C.Seed × WordRAM.Data r_caller), ν p * ↑(C.potential p.1 (WordRAM.Data.comap f p.2))

Execute P.code.rename f inline for a functional specification [D.HasStepFn stepFn] when arguments already match (p.2.comap f).regs on the support of a coupled caller distribution ν : PMF (C.Seed × Data r_caller).

theorem Cslib.DataStructure.WordRAM.Randomized.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) {prep : WordRAM.Code B r_caller} {B_prep : ENNReal} (o : D.Op) (ν : PMF (CoupledState C.Seed D.State r_caller)) {μ_prep : CoupledState C.Seed D.State r_caller → PMF (WordRAM.Data r_caller)} {T_prep : CoupledState C.Seed D.State r_caller → ENNReal} (hseed : ∀ (θ : C.Seed), (PMF.map CoupledState.seed ν) θ ≤ C.seedSlack * C.seedLaw θ) (hrep : ∀ t ∈ ν.support, D.valid t.state o ∧ C.rep t.seed t.state (WordRAM.Data.comap f t.data)) (hprep : ∀ t ∈ ν.support, WordRAM.ExecCodeDist w prep t.data (μ_prep t) (T_prep t) ∧ T_prep t ≤ B_prep ∧ ∀ x' ∈ (μ_prep t).support, WordRAM.Data.Bounded w (WordRAM.Data.comap f x') ∧ (∀ (i : Fin r_ds), P.input i = false → x'.regs (f i) = t.data.regs (f i)) ∧ (∀ a ∈ { base := base, length := C.space }.footprint, x'.mem a = t.data.mem a) ∧ C.argMatch o (WordRAM.Data.comap f x').regs) (hsingle : C.singleState → ∃ (s : D.State), ∀ t ∈ ν.support, t.state = s := by intro h; cases h) : ∃ (μ_call : CoupledState C.Seed D.State r_caller → PMF (CoupledState C.Seed D.State r_caller)) (T_call : CoupledState C.Seed D.State r_caller → ENNReal), (∀ t ∈ ν.support, WordRAM.ExecCodeDist w (prep.seq (WordRAM.Code.rename f P.code)) t.data (PMF.map CoupledState.data (μ_call t)) (T_call t) ∧ ∀ q ∈ (μ_call t).support, ∃ (a : D.Result o), D.step t.state o q.state a ∧ C.decode o (WordRAM.Data.comap f q.data).regs = some a ∧ C.rep q.seed q.state (WordRAM.Data.comap f q.data) ∧ ∃ x' ∈ (μ_prep t).support, WordRAM.Modifies { base := base, length := C.space }.footprint x'.mem q.data.mem ∧ ∀ j ∉ Set.range f, q.data.regs j = x'.regs j) ∧ (∀ (θ' : C.Seed), (PMF.map CoupledState.seed (ν.bind μ_call)) θ' ≤ C.seedSlack * C.seedLaw θ') ∧ ∑' (t : CoupledState C.Seed D.State r_caller), ν t * (T_call t + ∑' (q : CoupledState C.Seed D.State r_caller), (μ_call t) q * ↑(C.potential q.seed (WordRAM.Data.comap f q.data))) ≤ B_prep + ∑' (t : CoupledState C.Seed D.State r_caller), ν t * (↑(C.charge t.state o) + ↑(C.potential t.seed (WordRAM.Data.comap f t.data)))

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

theorem Cslib.DataStructure.WordRAM.Randomized.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} (C : StateTransitionImpl P D w base params s₀) {stepFn : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn stepFn] {f : Fin r_ds → Fin r_caller} (hf : Function.Injective f) {s : D.State} {prep : WordRAM.Code B r_caller} {B_prep : ENNReal} (o : D.Op) (ν : PMF (C.Seed × WordRAM.Data r_caller)) {μ_prep : C.Seed × WordRAM.Data r_caller → PMF (WordRAM.Data r_caller)} {T_prep : C.Seed × WordRAM.Data r_caller → ENNReal} (hv : D.valid s o) (hseed : ∀ (θ : C.Seed), (PMF.map Prod.fst ν) θ ≤ C.seedSlack * C.seedLaw θ) (hrep : ∀ p ∈ ν.support, C.rep p.1 s (WordRAM.Data.comap f p.2)) (hprep : ∀ p ∈ ν.support, WordRAM.ExecCodeDist w prep p.2 (μ_prep p) (T_prep p) ∧ T_prep p ≤ B_prep ∧ ∀ x' ∈ (μ_prep p).support, WordRAM.Data.Bounded w (WordRAM.Data.comap f x') ∧ (∀ (i : Fin r_ds), P.input i = false → x'.regs (f i) = p.2.regs (f i)) ∧ (∀ a ∈ { base := base, length := C.space }.footprint, x'.mem a = p.2.mem a) ∧ C.argMatch o (WordRAM.Data.comap f x').regs) : ∃ (μ_call : C.Seed × WordRAM.Data r_caller → PMF (C.Seed × WordRAM.Data r_caller)) (T_call : C.Seed × WordRAM.Data r_caller → ENNReal), (∀ p ∈ ν.support, WordRAM.ExecCodeDist w (prep.seq (WordRAM.Code.rename f P.code)) p.2 (PMF.map Prod.snd (μ_call p)) (T_call p) ∧ ∀ q ∈ (μ_call p).support, C.decode o (WordRAM.Data.comap f q.2).regs = some (D.stepFn s o).2 ∧ C.rep q.1 (D.stepFn s o).1 (WordRAM.Data.comap f q.2) ∧ ∃ x' ∈ (μ_prep p).support, WordRAM.Modifies { base := base, length := C.space }.footprint x'.mem q.2.mem ∧ ∀ j ∉ Set.range f, q.2.regs j = x'.regs j) ∧ (∀ (θ' : C.Seed), (PMF.map Prod.fst (ν.bind μ_call)) θ' ≤ C.seedSlack * C.seedLaw θ') ∧ ∑' (p : C.Seed × WordRAM.Data r_caller), ν p * (T_call p + ∑' (q : C.Seed × WordRAM.Data r_caller), (μ_call p) q * ↑(C.potential q.1 (WordRAM.Data.comap f q.2))) ≤ B_prep + ↑(C.charge s o) + ∑' (p : C.Seed × WordRAM.Data r_caller), ν p * ↑(C.potential p.1 (WordRAM.Data.comap f p.2))

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

Projection 6: End-to-end expected-amortized sequence telescope (steps_expected_amortized,

seq_expected_amortized, steps_expected_amortized_ofFn, seq_expected_amortized_ofFn)

def Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.toDynamicProgram {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₀) : WordRAM.DynamicProgram D.signature r_ds B

Reuse the signature-level program and argument-delivery API with the actual instruction basis. This projection carries code and the calling convention, without a deterministic certificate.

theorem Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.prepare_rep {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₀) {θ : C.Seed} {s : D.State} {o : D.Op} {x : WordRAM.Data r_ds} (hr : C.rep θ s x) (hv : D.valid s o) : C.rep θ s (C.toDynamicProgram.prepare o x)

theorem Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.prepare_potential {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₀) {θ : C.Seed} {s : D.State} {o : D.Op} {x : WordRAM.Data r_ds} (hr : C.rep θ s x) : C.potential θ (C.toDynamicProgram.prepare o x) = C.potential θ x

theorem Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.prepare_argMatch {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₀) (o : D.Op) (x : WordRAM.Data r_ds) : C.argMatch o (C.toDynamicProgram.prepare o x).regs

inductive Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.ExecSteps {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₀) : List D.Op → PMF (CoupledState C.Seed D.State r_ds) → PMF (CoupledState C.Seed D.State r_ds) → ENNReal → ENNReal → Prop

Inductive multi-operation distributional execution relation for a randomized subroutine C over a relational specification D. C.ExecSteps ops ν ν_final T_ops C_ops witnesses that starting from coupled distribution ν : PMF (CoupledState C.Seed D.State r_ds), executing each operation o in ops by delivering arguments via C.toDynamicProgram.prepare o and running P.code under ExecCodeDist produces the final coupled distribution ν_final, angelically witnesses a valid transition D.step s o s' a and decoded observation C.decode o q.data.regs = some a at every step, modifies memory only within [base, base + C.space), incurs total expected operation body cost T_ops, and accumulates total expected operation charge C_ops.

• 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₀} (ν : PMF (CoupledState C.Seed D.State r_ds)) : C.ExecSteps [] ν ν 0 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₀} {o : D.Op} {ops : List D.Op} {ν ν_final : PMF (CoupledState C.Seed D.State r_ds)} {μ_step : CoupledState C.Seed D.State r_ds → PMF (CoupledState C.Seed D.State r_ds)} {T_step : CoupledState C.Seed D.State r_ds → ENNReal} {T_rest C_rest : ENNReal} : (∀ t ∈ ν.support, WordRAM.ExecCodeDist w P.code (C.toDynamicProgram.prepare o t.data) (PMF.map CoupledState.data (μ_step t)) (T_step t) ∧ ∀ q ∈ (μ_step t).support, ∃ (a : D.Result o), D.step t.state o q.state a ∧ C.decode o q.data.regs = some a ∧ C.rep q.seed q.state q.data ∧ WordRAM.Modifies { base := base, length := C.space }.footprint t.data.mem q.data.mem) → C.ExecSteps ops (ν.bind μ_step) ν_final T_rest C_rest → C.ExecSteps (o :: ops) ν ν_final (∑' (t : CoupledState C.Seed D.State r_ds), ν t * T_step t + T_rest) (∑' (t : CoupledState C.Seed D.State r_ds), ν t * ↑(C.charge t.state o) + C_rest)

theorem Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.steps_expected_amortized {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) (ν : PMF (CoupledState C.Seed D.State r_ds)) (hv : ∀ t ∈ ν.support, D.ValidOpSeq t.state ops) (hseed : ∀ (θ : C.Seed), (PMF.map CoupledState.seed ν) θ ≤ C.seedSlack * C.seedLaw θ) (hrep : ∀ t ∈ ν.support, C.rep t.seed t.state t.data) (hsingle : C.singleState → ∃ (s : D.State), ∀ t ∈ ν.support, t.state = s := by intro h; cases h) : ∃ (ν_final : PMF (CoupledState C.Seed D.State r_ds)) (T_ops : ENNReal) (C_ops : ENNReal), C.ExecSteps ops ν ν_final T_ops C_ops ∧ (∀ (θ : C.Seed), (PMF.map CoupledState.seed ν_final) θ ≤ C.seedSlack * C.seedLaw θ) ∧ (∀ t ∈ ν_final.support, C.rep t.seed t.state t.data) ∧ T_ops + ∑' (q : CoupledState C.Seed D.State r_ds), ν_final q * ↑(C.potential q.seed q.data) ≤ C_ops + ∑' (t : CoupledState C.Seed D.State r_ds), ν t * ↑(C.potential t.seed t.data)

Multi-operation expected-amortized telescope (steps_expected_amortized). From any coupled state distribution ν : PMF (CoupledState C.Seed D.State r_ds) satisfying the seed-marginal bound, C.rep t.seed t.state t.data, and demonic admissibility D.ValidOpSeq t.state ops on ν.support, executing ops : List D.Op produces a final coupled distribution ν_final, total expected operation step count T_ops : ℝ≥0∞, and total expected operation charge C_ops : ℝ≥0∞ witnessing C.ExecSteps ops ν ν_final T_ops C_ops and satisfying the addition-only ℝ≥0∞ telescope inequality T_ops + ∑' q, ν_final q * Φ(q) ≤ C_ops + ∑' t, ν t * Φ(t).

theorem Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.seq_expected_amortized {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₀) {x : WordRAM.Data r_ds} (ops : List D.Op) (hx : WordRAM.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) (hv : D.ValidOpSeq s₀ ops) : ∃ (ν₀ : PMF (C.Seed × WordRAM.Data r_ds)) (ν_final : PMF (CoupledState C.Seed D.State r_ds)) (T_ops : ENNReal) (C_ops : ENNReal), WordRAM.ExecCodeDist w P.initFresh x (PMF.map Prod.snd ν₀) C.initTime ∧ C.ExecSteps ops (PMF.map (fun (p : C.Seed × WordRAM.Data r_ds) => { seed := p.1, state := s₀, data := p.2 }) ν₀) ν_final T_ops C_ops ∧ (∀ (θ : C.Seed), (PMF.map CoupledState.seed ν_final) θ ≤ C.seedSlack * C.seedLaw θ) ∧ (∀ t ∈ ν_final.support, C.rep t.seed t.state t.data) ∧ C.initTime + T_ops + ∑' (q : CoupledState C.Seed D.State r_ds), ν_final q * ↑(C.potential q.seed q.data) ≤ C.initTime + ↑C.initPotential + C_ops

End-to-end expected-amortized theorem from fresh initialization (seq_expected_amortized). Starting from zeroed [base, base + C.space), P.initFresh followed by any demonically admissible operation sequence ops : List D.Op (D.ValidOpSeq s₀ ops) has total expected instruction cost C.initTime + T_ops bounded by C.initTime + C.initPotential + C_ops.

inductive Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.ExecStepsOfFn {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₀) {stepFn : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn stepFn] : D.State → List D.Op → PMF (C.Seed × WordRAM.Data r_ds) → PMF (C.Seed × WordRAM.Data r_ds) → ENNReal → Prop

Inductive multi-operation distributional execution relation for a randomized subroutine C over a functional specification [D.HasStepFn stepFn].

• 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₀} {stepFn : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn stepFn] (s : D.State) (ν : PMF (C.Seed × WordRAM.Data r_ds)) : C.ExecStepsOfFn s [] ν ν 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₀} {stepFn : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn stepFn] {s : D.State} {o : D.Op} {ops : List D.Op} {ν ν_final : PMF (C.Seed × WordRAM.Data r_ds)} {μ_step : C.Seed × WordRAM.Data r_ds → PMF (C.Seed × WordRAM.Data r_ds)} {T_step : C.Seed × WordRAM.Data r_ds → ENNReal} {T_rest : ENNReal} : (∀ p ∈ ν.support, WordRAM.ExecCodeDist w P.code (C.toDynamicProgram.prepare o p.2) (PMF.map Prod.snd (μ_step p)) (T_step p) ∧ ∀ q ∈ (μ_step p).support, C.decode o q.2.regs = some (D.stepFn s o).2 ∧ C.rep q.1 (D.stepFn s o).1 q.2 ∧ WordRAM.Modifies { base := base, length := C.space }.footprint p.2.mem q.2.mem) → C.ExecStepsOfFn (D.stepFn s o).1 ops (ν.bind μ_step) ν_final T_rest → C.ExecStepsOfFn s (o :: ops) ν ν_final (∑' (p : C.Seed × WordRAM.Data r_ds), ν p * T_step p + T_rest)

theorem Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.ExecSteps.toOfFn {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₀} {stepFn : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn stepFn] {s : D.State} {ops : List D.Op} {ν_rel ν_final : PMF (CoupledState C.Seed D.State r_ds)} {T_ops C_ops : ENNReal} (hex : C.ExecSteps ops ν_rel ν_final T_ops C_ops) (hs : ∀ t ∈ ν_rel.support, t.state = s) : C.ExecStepsOfFn s ops (PMF.map (fun (t : CoupledState C.Seed D.State r_ds) => (t.seed, t.data)) ν_rel) (PMF.map (fun (t : CoupledState C.Seed D.State r_ds) => (t.seed, t.data)) ν_final) T_ops ∧ C_ops = ↑(D.totalCost C.charge s ops) ∧ ∀ q ∈ ν_final.support, q.state = (D.run s ops).1

Project a relational ExecSteps derivation to ExecStepsOfFn when [D.HasStepFn stepFn] and the initial coupled distribution is supported on a single abstract state s.

theorem Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.steps_expected_amortized_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} (C : StateTransitionImpl P D w base params s₀) {stepFn : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn stepFn] {s : D.State} (ops : List D.Op) (ν : PMF (C.Seed × WordRAM.Data r_ds)) (hv : D.ValidHistory s ops) (hseed : ∀ (θ : C.Seed), (PMF.map Prod.fst ν) θ ≤ C.seedSlack * C.seedLaw θ) (hrep : ∀ p ∈ ν.support, C.rep p.1 s p.2) : ∃ (ν_final : PMF (C.Seed × WordRAM.Data r_ds)) (T_ops : ENNReal), C.ExecStepsOfFn s ops ν ν_final T_ops ∧ (∀ (θ : C.Seed), (PMF.map Prod.fst ν_final) θ ≤ C.seedSlack * C.seedLaw θ) ∧ (∀ p ∈ ν_final.support, C.rep p.1 (D.run s ops).1 p.2) ∧ T_ops + ∑' (q : C.Seed × WordRAM.Data r_ds), ν_final q * ↑(C.potential q.1 q.2) ≤ ↑(D.totalCost C.charge s ops) + ∑' (p : C.Seed × WordRAM.Data r_ds), ν p * ↑(C.potential p.1 p.2)

Multi-operation expected-amortized telescope for functional specifications (steps_expected_amortized_ofFn).

theorem Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.seq_expected_amortized_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} (C : StateTransitionImpl P D w base params s₀) {stepFn : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn stepFn] {x : WordRAM.Data r_ds} (ops : List D.Op) (hx : WordRAM.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) (hv : D.ValidHistory s₀ ops) : ∃ (ν₀ : PMF (C.Seed × WordRAM.Data r_ds)) (ν_final : PMF (C.Seed × WordRAM.Data r_ds)) (T_ops : ENNReal), WordRAM.ExecCodeDist w P.initFresh x (PMF.map Prod.snd ν₀) C.initTime ∧ C.ExecStepsOfFn s₀ ops ν₀ ν_final T_ops ∧ (∀ (θ : C.Seed), (PMF.map Prod.fst ν_final) θ ≤ C.seedSlack * C.seedLaw θ) ∧ (∀ p ∈ ν_final.support, C.rep p.1 (D.run s₀ ops).1 p.2) ∧ C.initTime + T_ops + ∑' (q : C.Seed × WordRAM.Data r_ds), ν_final q * ↑(C.potential q.1 q.2) ≤ C.initTime + ↑C.initPotential + ↑(D.totalCost C.charge s₀ ops)

End-to-end expected-amortized theorem from fresh initialization for functional specifications (seq_expected_amortized_ofFn).