Oblivious-Sequence Word-RAM Implementation Certificates

This file connects state-free oblivious-sequence specifications (Cslib.DataStructure.ObliviousSequenceSpec) to concrete randomized Word-RAM subroutines:

1. Cslib.DataStructure.WordRAM.Randomized.ObliviousSequenceImpl: A reusable Word-RAM subroutine certificate realizing an S : Cslib.DataStructure.ObliviousSequenceSpec at word width w, base address base, and runtime initialization parameters params. It provides:

   • fresh zeroed-memory initialization (initFresh_exec) and dirty-memory clearing initialization (initClear_exec);
   • multi-step distributional execution ExecSteps across any admissible oblivious sequence ops : List S.Op;
   • end-to-end expected-time and distributional correctness theorems seq_expected and seq_expected_clear certifying both S.Contract ops (ν_final.map SeqOutcome.transcript) and the total expected instruction bound;
   • basis simulation transport mapSimulates and exact-to-standard lifting toStandard.

2. Canonical embedding Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.toObliviousSequenceImpl: Every relational Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl P D w base params s₀ whose per-operation amortized charge is bounded by a state-independent opCharge : D.Op → ℕ on admissible inputs canonically induces an ObliviousSequenceImpl P (D.toObliviousSequenceSpec s₀) w base params.

ObliviousSequenceImpl bounds the instruction cost of initialization and of the subroutine operation bodies across an oblivious sequence ops, excluding external caller argument delivery and dispatch, with the word width w treated as an external admissible parameter.

Main definitions

• Cslib.DataStructure.WordRAM.Randomized.LatentState, Cslib.DataStructure.WordRAM.Randomized.StepOutcome, Cslib.DataStructure.WordRAM.Randomized.SeqOutcome: named state and transcript records for multi-step distributional execution.
• Cslib.DataStructure.WordRAM.Randomized.ExecSteps: multi-operation distributional execution relation across an oblivious sequence ops : List S.Op.
• Cslib.DataStructure.WordRAM.Randomized.ObliviousSequenceImpl: Word-RAM implementation certificate for an ObliviousSequenceSpec.
• Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.toObliviousSequenceImpl: canonical embedding of a relational StateTransitionImpl into ObliviousSequenceImpl.

Main results

• Cslib.DataStructure.WordRAM.Randomized.ExecSteps.bounded, Cslib.DataStructure.WordRAM.Randomized.ExecSteps.arguments_fit, Cslib.DataStructure.WordRAM.Randomized.ExecSteps.mapSimulates: preservation of Data.Bounded w, word-admissibility of encoded operation arguments, and basis simulation lifting for ExecSteps.
• Cslib.DataStructure.WordRAM.Randomized.ObliviousSequenceImpl.prepare_bounded, Cslib.DataStructure.WordRAM.Randomized.ObliviousSequenceImpl.initFresh_exec, Cslib.DataStructure.WordRAM.Randomized.ObliviousSequenceImpl.initClear_exec, Cslib.DataStructure.WordRAM.Randomized.ObliviousSequenceImpl.seq_expected, Cslib.DataStructure.WordRAM.Randomized.ObliviousSequenceImpl.seq_expected_clear: word-bounded preparation, initialization, and end-to-end expected-time and distributional-contract theorems.

Named state and transcript bundles for oblivious-sequence execution

structure Cslib.DataStructure.WordRAM.Randomized.LatentState (Latent : Type z) (r : ℕ) : Type z

Coupled latent state and concrete Word-RAM register/memory state.

• latent : Latent

  Internal latent state (such as a hash seed or coupled relational state).

• data : WordRAM.Data r

  Concrete Word-RAM register and memory state.

structure Cslib.DataStructure.WordRAM.Randomized.StepOutcome (Latent : Type z) (α : Type v) (r : ℕ) : Type (max v z)

Outcome of a single subroutine operation step: updated latent state, updated concrete Word-RAM state, and decoded operation observation.

• latent : Latent

  Updated internal latent state.

• data : WordRAM.Data r

  Updated concrete Word-RAM register and memory state.

• result : α

  Decoded observation returned by the operation.

structure Cslib.DataStructure.WordRAM.Randomized.SeqOutcome (Latent : Type z) {Op : Type u} (Result : Op → Type v) (r : ℕ) : Type (max u v z)

Outcome of a multi-operation oblivious sequence: current latent state, concrete Word-RAM state, and accumulated input-output transcript List (Sigma Result).

• latent : Latent

  Current internal latent state.

• data : WordRAM.Data r

  Current concrete Word-RAM register and memory state.

• transcript : List (Sigma Result)

  Accumulated input-output transcript of operations executed so far.

def Cslib.DataStructure.WordRAM.Randomized.SeqOutcome.ofLatentState {Latent : Type z} {Op : Type u} {Result : Op → Type v} {r : ℕ} (t : LatentState Latent r) : SeqOutcome Latent Result r

Initialize a SeqOutcome from a LatentState with an empty transcript [].

def Cslib.DataStructure.WordRAM.Randomized.SeqOutcome.appendStep {Latent : Type z} {Op : Type u} {Result : Op → Type v} {r : ℕ} (t : SeqOutcome Latent Result r) (o : Op) (q : StepOutcome Latent (Result o) r) : SeqOutcome Latent Result r

Append a single operation outcome q : StepOutcome Latent (Result o) r to t : SeqOutcome.

inductive Cslib.DataStructure.WordRAM.Randomized.ExecSteps {B : WordRAM.Basis} {r_ds k_init : ℕ} (P : WordRAM.SubroutineCode B r_ds k_init) (S : ObliviousSequenceSpec) (Latent : Type z) (w base space : ℕ) (encode : S.Op → Fin r_ds → ℕ) (decode : (o : S.Op) → (Fin r_ds → ℕ) → Option (S.Result o)) : List S.Op → PMF (SeqOutcome Latent S.Result r_ds) → PMF (SeqOutcome Latent S.Result r_ds) → ENNReal → Prop

Multi-operation distributional execution relation across an oblivious sequence ops : List S.Op. At each operation o, t.data and the encoded arguments are word-bounded (Fits w), arguments are delivered via (P.toDynamicProgram encode decode).prepare o, P.code executes under ExecCodeDist preserving Data.Bounded w, the observation q.result is decoded from q.data.regs, memory outside [base, base + space) is preserved, and ⟨o, q.result⟩ is appended to the accumulated transcript.

• nil {B : WordRAM.Basis} {r_ds k_init : ℕ} {P : WordRAM.SubroutineCode B r_ds k_init} {S : ObliviousSequenceSpec} {Latent : Type z} {w base space : ℕ} {encode : S.Op → Fin r_ds → ℕ} {decode : (o : S.Op) → (Fin r_ds → ℕ) → Option (S.Result o)} (ν : PMF (SeqOutcome Latent S.Result r_ds)) : ExecSteps P S Latent w base space encode decode [] ν ν 0
• cons {B : WordRAM.Basis} {r_ds k_init : ℕ} {P : WordRAM.SubroutineCode B r_ds k_init} {S : ObliviousSequenceSpec} {Latent : Type z} {w base space : ℕ} {encode : S.Op → Fin r_ds → ℕ} {decode : (o : S.Op) → (Fin r_ds → ℕ) → Option (S.Result o)} {o : S.Op} {ops : List S.Op} {ν ν_final : PMF (SeqOutcome Latent S.Result r_ds)} {μ_step : SeqOutcome Latent S.Result r_ds → PMF (StepOutcome Latent (S.Result o) r_ds)} {T_step : SeqOutcome Latent S.Result r_ds → ENNReal} {T_rest : ENNReal} : (∀ t ∈ ν.support, WordRAM.Data.Bounded w t.data ∧ (∀ (i : Fin r_ds), P.input i = true → WordRAM.Fits w (encode o i)) ∧ WordRAM.Data.Bounded w ((P.toDynamicProgram encode decode).prepare o t.data) ∧ WordRAM.ExecCodeDist w P.code ((P.toDynamicProgram encode decode).prepare o t.data) (PMF.map StepOutcome.data (μ_step t)) (T_step t) ∧ ∀ q ∈ (μ_step t).support, WordRAM.Data.Bounded w q.data ∧ decode o q.data.regs = some q.result ∧ WordRAM.Modifies { base := base, length := space }.footprint t.data.mem q.data.mem) → ExecSteps P S Latent w base space encode decode ops (ν.bind fun (t : SeqOutcome Latent S.Result r_ds) => PMF.map (t.appendStep o) (μ_step t)) ν_final T_rest → ExecSteps P S Latent w base space encode decode (o :: ops) ν ν_final (∑' (t : SeqOutcome Latent S.Result r_ds), ν t * T_step t + T_rest)

theorem Cslib.DataStructure.WordRAM.Randomized.ExecSteps.bounded {B : WordRAM.Basis} {r_ds k_init : ℕ} {P : WordRAM.SubroutineCode B r_ds k_init} {S : ObliviousSequenceSpec} {Latent : Type z} {w base space : ℕ} {encode : S.Op → Fin r_ds → ℕ} {decode : (o : S.Op) → (Fin r_ds → ℕ) → Option (S.Result o)} {ops : List S.Op} {ν ν_final : PMF (SeqOutcome Latent S.Result r_ds)} {T_ops : ENNReal} (h : ExecSteps P S Latent w base space encode decode ops ν ν_final T_ops) (hbdd : ∀ t ∈ ν.support, WordRAM.Data.Bounded w t.data) (t : SeqOutcome Latent S.Result r_ds) : t ∈ ν_final.support → WordRAM.Data.Bounded w t.data

ExecSteps preserves Data.Bounded w on every state in the support of ν_final whenever every state in the support of ν is word-bounded.

theorem Cslib.DataStructure.WordRAM.Randomized.ExecSteps.arguments_fit {B : WordRAM.Basis} {r_ds k_init : ℕ} {P : WordRAM.SubroutineCode B r_ds k_init} {S : ObliviousSequenceSpec} {Latent : Type z} {w base space : ℕ} {encode : S.Op → Fin r_ds → ℕ} {decode : (o : S.Op) → (Fin r_ds → ℕ) → Option (S.Result o)} {ops : List S.Op} {ν ν_final : PMF (SeqOutcome Latent S.Result r_ds)} {T_ops : ENNReal} (h : ExecSteps P S Latent w base space encode decode ops ν ν_final T_ops) (o : S.Op) : o ∈ ops → ∀ (i : Fin r_ds), P.input i = true → WordRAM.Fits w (encode o i)

Every operation o ∈ ops in an ExecSteps derivation has word-bounded encoded arguments on all input registers of P.

theorem Cslib.DataStructure.WordRAM.Randomized.ExecSteps.mapSimulates {B B' : WordRAM.Basis} {r_ds k_init : ℕ} (φ : B.Simulates B') {P : WordRAM.SubroutineCode B r_ds k_init} {S : ObliviousSequenceSpec} {Latent : Type z} {w base space : ℕ} {encode : S.Op → Fin r_ds → ℕ} {decode : (o : S.Op) → (Fin r_ds → ℕ) → Option (S.Result o)} {ops : List S.Op} {ν ν_final : PMF (SeqOutcome Latent S.Result r_ds)} {T_ops : ENNReal} (h : ExecSteps P S Latent w base space encode decode ops ν ν_final T_ops) : ExecSteps (WordRAM.SubroutineCode.mapSimulates φ P) S Latent w base space encode decode ops ν ν_final T_ops

Lift an ExecSteps derivation along a basis simulation φ : B.Simulates B'.

ObliviousSequenceImpl: Word-RAM implementation for an ObliviousSequenceSpec

structure Cslib.DataStructure.WordRAM.Randomized.ObliviousSequenceImpl {B : WordRAM.Basis} {r_ds k_init : ℕ} (P : WordRAM.SubroutineCode B r_ds k_init) (S : ObliviousSequenceSpec) (w base : ℕ) (params : Fin k_init → ℕ) : Type (max u v (z + 1))

Reusable Word-RAM subroutine implementation certificate for a randomized data structure P : SubroutineCode B r_ds k_init realizing an oblivious-sequence specification S : DataStructure.ObliviousSequenceSpec at word width w, base address base, and runtime parameters params.

• Latent : Type z

  Internal latent state type (e.g. a hash seed or coupled relational state).

• 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 (0 when unamortized).

• charge : S.Op → ℕ

  Per-operation instruction charge.

• initInv : PMF (LatentState self.Latent r_ds) → Prop

  Distributional invariant on the initial coupled state distribution produced by P.initSetup.

• validOp : self.Latent → S.Op → Prop

  Predicate on a latent state and an operation under which arguments_fit bounds the encoded arguments (fun _ _ => True when operation encoding is unconditionally word-bounded). No field relates it to S.ValidOpSeq, and steps_exec does not use it.

• encode : S.Op → Fin r_ds → ℕ

  Standalone register encoding for argument delivery.

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

  Output decoder reading typed operation observations from final registers.

• bounded {ν : PMF (LatentState self.Latent r_ds)} : self.initInv ν → ∀ t ∈ ν.support, WordRAM.Data.Bounded w t.data

  Initial distributions satisfying initInv are supported on word-bounded states.

• arguments_fit {z : self.Latent} (o : S.Op) : self.validOp z 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 operations satisfying validOp at some latent state.

• 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 (LatentState self.Latent r_ds)), WordRAM.ExecCodeDist w P.initSetup x₁ (PMF.map LatentState.data ν₀) self.setupTime ∧ self.initInv ν₀ ∧ ∀ t ∈ ν₀.support, WordRAM.Data.Bounded w t.data ∧ t.data.regs P.frontierReg = base + self.space ∧ WordRAM.Modifies { base := base, length := self.space }.footprint x₁.mem t.data.mem

  Execution of P.initSetup once [base, base + space) holds zeros, producing an initial coupled state distribution ν₀ : PMF (LatentState Latent r_ds) satisfying initInv ν₀.

• steps_exec (ops : List S.Op) (ν₀ : PMF (LatentState self.Latent r_ds)) : S.ValidOpSeq ops → self.initInv ν₀ → ∃ (ν_final : PMF (SeqOutcome self.Latent S.Result r_ds)) (T_ops : ENNReal), ExecSteps P S self.Latent w base self.space self.encode self.decode ops (PMF.map SeqOutcome.ofLatentState ν₀) ν_final T_ops ∧ S.Contract ops (PMF.map SeqOutcome.transcript ν_final) ∧ T_ops ≤ ↑self.initPotential + ↑(List.map self.charge ops).sum

  Multi-operation execution across any admissible oblivious sequence ops : List S.Op from any initial distribution ν₀ satisfying initInv ν₀, certifying both S.Contract ops on the joint output transcript distribution and the expected instruction bound.

theorem Cslib.DataStructure.WordRAM.Randomized.ObliviousSequenceImpl.prepare_bounded {B : WordRAM.Basis} {r_ds k_init w base : ℕ} {P : WordRAM.SubroutineCode B r_ds k_init} {S : ObliviousSequenceSpec} {params : Fin k_init → ℕ} (C : ObliviousSequenceImpl P S w base params) {z : C.Latent} {o : S.Op} {x : WordRAM.Data r_ds} (hx : WordRAM.Data.Bounded w x) (hv : C.validOp z o) : WordRAM.Data.Bounded w ((P.toDynamicProgram C.encode C.decode).prepare o x)

Argument preparation preserves Data.Bounded w on operations satisfying C.validOp.

def Cslib.DataStructure.WordRAM.Randomized.ObliviousSequenceImpl.initTime {B : WordRAM.Basis} {r_ds k_init w base : ℕ} {P : WordRAM.SubroutineCode B r_ds k_init} {S : ObliviousSequenceSpec} {params : Fin k_init → ℕ} (C : ObliviousSequenceImpl P S w base params) : ENNReal

Total expected instruction bound for P.initFresh (spanTime + setupTime).

def Cslib.DataStructure.WordRAM.Randomized.ObliviousSequenceImpl.initClearTime {B : WordRAM.Basis} {r_ds k_init w base : ℕ} {P : WordRAM.SubroutineCode B r_ds k_init} {S : ObliviousSequenceSpec} {params : Fin k_init → ℕ} (C : ObliviousSequenceImpl P S w base params) : ENNReal

Total expected instruction bound for P.initClear (spanTime + (4 * space + 6) + setupTime).

def Cslib.DataStructure.WordRAM.Randomized.ObliviousSequenceImpl.totalCharge {B : WordRAM.Basis} {r_ds k_init w base : ℕ} {P : WordRAM.SubroutineCode B r_ds k_init} {S : ObliviousSequenceSpec} {params : Fin k_init → ℕ} (C : ObliviousSequenceImpl P S w base params) (ops : List S.Op) : ℕ

Total operation charge summed across an operation sequence ops : List S.Op.

@[simp]

theorem Cslib.DataStructure.WordRAM.Randomized.ObliviousSequenceImpl.totalCharge_nil {B : WordRAM.Basis} {r_ds k_init w base : ℕ} {P : WordRAM.SubroutineCode B r_ds k_init} {S : ObliviousSequenceSpec} {params : Fin k_init → ℕ} (C : ObliviousSequenceImpl P S w base params) : C.totalCharge [] = 0

@[simp]

theorem Cslib.DataStructure.WordRAM.Randomized.ObliviousSequenceImpl.totalCharge_cons {B : WordRAM.Basis} {r_ds k_init w base : ℕ} {P : WordRAM.SubroutineCode B r_ds k_init} {S : ObliviousSequenceSpec} {params : Fin k_init → ℕ} (C : ObliviousSequenceImpl P S w base params) (o : S.Op) (ops : List S.Op) : C.totalCharge (o :: ops) = C.charge o + C.totalCharge ops

@[reducible, inline]

abbrev Cslib.DataStructure.WordRAM.Randomized.ObliviousSequenceImpl.Steps {B : WordRAM.Basis} {r_ds k_init w base : ℕ} {P : WordRAM.SubroutineCode B r_ds k_init} {S : ObliviousSequenceSpec} {params : Fin k_init → ℕ} (C : ObliviousSequenceImpl P S w base params) : List S.Op → PMF (SeqOutcome C.Latent S.Result r_ds) → PMF (SeqOutcome C.Latent S.Result r_ds) → ENNReal → Prop

Specialization of ExecSteps to an ObliviousSequenceImpl certificate C.

def Cslib.DataStructure.WordRAM.Randomized.ObliviousSequenceImpl.mapSimulates {B B' : WordRAM.Basis} {r_ds k_init w base : ℕ} {P : WordRAM.SubroutineCode B r_ds k_init} {S : ObliviousSequenceSpec} {params : Fin k_init → ℕ} (φ : B.Simulates B') (C : ObliviousSequenceImpl P S w base params) : ObliviousSequenceImpl (WordRAM.SubroutineCode.mapSimulates φ P) S w base params

Transport an ObliviousSequenceImpl certificate along a basis simulation φ : B.Simulates B'.

@[reducible, inline]

abbrev Cslib.DataStructure.WordRAM.Randomized.ObliviousSequenceImpl.toStandard {r_ds k_init w base : ℕ} {S : ObliviousSequenceSpec} {params : Fin k_init → ℕ} {P : WordRAM.SubroutineCode WordRAM.Basis.exact r_ds k_init} (C : ObliviousSequenceImpl P S w base params) : ObliviousSequenceImpl P.toStandard S w base params

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

theorem Cslib.DataStructure.WordRAM.Randomized.ObliviousSequenceImpl.initFresh_exec {B : WordRAM.Basis} {r_ds k_init w base : ℕ} {P : WordRAM.SubroutineCode B r_ds k_init} {S : ObliviousSequenceSpec} {params : Fin k_init → ℕ} (C : ObliviousSequenceImpl P S w base params) {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 (LatentState C.Latent r_ds)), WordRAM.ExecCodeDist w P.initFresh x (PMF.map LatentState.data ν₀) C.initTime ∧ C.initInv ν₀ ∧ ∀ t ∈ ν₀.support, WordRAM.Data.Bounded w t.data ∧ t.data.regs P.frontierReg = base + C.space ∧ WordRAM.Modifies { base := base, length := C.space }.footprint x.mem t.data.mem

Expected-time execution of P.initFresh when [base, base + C.space) already holds zeros.

theorem Cslib.DataStructure.WordRAM.Randomized.ObliviousSequenceImpl.initClear_exec {B : WordRAM.Basis} {r_ds k_init w base : ℕ} {P : WordRAM.SubroutineCode B r_ds k_init} {S : ObliviousSequenceSpec} {params : Fin k_init → ℕ} (C : ObliviousSequenceImpl P S w base params) {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 (LatentState C.Latent r_ds)), WordRAM.ExecCodeDist w P.initClear x (PMF.map LatentState.data ν₀) C.initClearTime ∧ C.initInv ν₀ ∧ ∀ t ∈ ν₀.support, WordRAM.Data.Bounded w t.data ∧ t.data.regs P.frontierReg = base + C.space ∧ WordRAM.Modifies { base := base, length := C.space }.footprint x.mem t.data.mem

Expected-time execution of P.initClear on arbitrary dirty memory.

theorem Cslib.DataStructure.WordRAM.Randomized.ObliviousSequenceImpl.seq_expected {B : WordRAM.Basis} {r_ds k_init w base : ℕ} {P : WordRAM.SubroutineCode B r_ds k_init} {S : ObliviousSequenceSpec} {params : Fin k_init → ℕ} (C : ObliviousSequenceImpl P S w base params) {x : WordRAM.Data r_ds} (ops : List S.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 : S.ValidOpSeq ops) : ∃ (ν₀ : PMF (LatentState C.Latent r_ds)) (ν_final : PMF (SeqOutcome C.Latent S.Result r_ds)) (T_ops : ENNReal), WordRAM.ExecCodeDist w P.initFresh x (PMF.map LatentState.data ν₀) C.initTime ∧ C.Steps ops (PMF.map SeqOutcome.ofLatentState ν₀) ν_final T_ops ∧ (∀ t ∈ ν_final.support, WordRAM.Data.Bounded w t.data) ∧ S.Contract ops (PMF.map SeqOutcome.transcript ν_final) ∧ C.initTime + T_ops ≤ C.initTime + ↑C.initPotential + ↑(C.totalCharge ops)

End-to-end expected-time and distributional correctness theorem from fresh initialization (seq_expected). Starting from zeroed [base, base + C.space), P.initFresh followed by any admissible oblivious operation sequence ops : List S.Op (S.ValidOpSeq ops) executes in expected time at most C.initTime + C.initPotential + C.totalCharge ops, preserves Data.Bounded w on ν_final.support, and induces an output transcript distribution ν_final.map SeqOutcome.transcript satisfying S.Contract ops.

theorem Cslib.DataStructure.WordRAM.Randomized.ObliviousSequenceImpl.seq_expected_clear {B : WordRAM.Basis} {r_ds k_init w base : ℕ} {P : WordRAM.SubroutineCode B r_ds k_init} {S : ObliviousSequenceSpec} {params : Fin k_init → ℕ} (C : ObliviousSequenceImpl P S w base params) {x : WordRAM.Data r_ds} (ops : List S.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) (hv : S.ValidOpSeq ops) : ∃ (ν₀ : PMF (LatentState C.Latent r_ds)) (ν_final : PMF (SeqOutcome C.Latent S.Result r_ds)) (T_ops : ENNReal), WordRAM.ExecCodeDist w P.initClear x (PMF.map LatentState.data ν₀) C.initClearTime ∧ C.Steps ops (PMF.map SeqOutcome.ofLatentState ν₀) ν_final T_ops ∧ (∀ t ∈ ν_final.support, WordRAM.Data.Bounded w t.data) ∧ S.Contract ops (PMF.map SeqOutcome.transcript ν_final) ∧ C.initClearTime + T_ops ≤ C.initClearTime + ↑C.initPotential + ↑(C.totalCharge ops)

End-to-end expected-time and distributional correctness theorem from dirty memory (seq_expected_clear).

structure Cslib.DataStructure.WordRAM.Randomized.TraceLatent (D : StateTransitionSpec) (Seed : Type) : Type (max u v z)

Coupled latent seed, current abstract state, and accumulated relational transcript prefix for embedding Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl into ObliviousSequenceImpl.

• seed : Seed

  Latent random seed from the underlying StateTransitionImpl.

• state : D.State

  Current abstract state of D.

• trace : D.Transcript

  Relational execution transcript accumulated since s₀.

Canonical Embedding of StateTransitionImpl into ObliviousSequenceImpl

noncomputable def Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.toObliviousSequenceImpl {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₀) (opCharge : D.Op → ℕ := C.charge s₀) (hcharge : ∀ (s : D.State) (o : D.Op), D.valid s o → C.charge s o ≤ opCharge o := by intros; exact le_rfl) : ObliviousSequenceImpl P (D.toObliviousSequenceSpec s₀) w base params

Canonical embedding of any relational Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl certificate into ObliviousSequenceImpl realizing D.toObliviousSequenceSpec s₀, given a state-independent operation charge bound opCharge : D.Op → ℕ such that ∀ s o, D.valid s o → C.charge s o ≤ opCharge o.

@[simp]

theorem Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.toObliviousSequenceImpl_space {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₀) (opCharge : D.Op → ℕ) (hcharge : ∀ (s : D.State) (o : D.Op), D.valid s o → C.charge s o ≤ opCharge o) : (C.toObliviousSequenceImpl opCharge hcharge).space = C.space

@[simp]

theorem Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.toObliviousSequenceImpl_initPotential {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₀) (opCharge : D.Op → ℕ) (hcharge : ∀ (s : D.State) (o : D.Op), D.valid s o → C.charge s o ≤ opCharge o) : (C.toObliviousSequenceImpl opCharge hcharge).initPotential = C.initPotential

@[simp]

theorem Cslib.DataStructure.WordRAM.Randomized.StateTransitionImpl.toObliviousSequenceImpl_charge {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₀) (opCharge : D.Op → ℕ) (hcharge : ∀ (s : D.State) (o : D.Op), D.valid s o → C.charge s o ≤ opCharge o) : (C.toObliviousSequenceImpl opCharge hcharge).charge = opCharge