Oblivious-Sequence Data Structure Specifications

An oblivious-sequence specification (Cslib.DataStructure.ObliviousSequenceSpec) describes the input-output contract of a randomized or deterministic data structure against an oblivious (non-adaptive) caller that fixes a finite operation sequence ops : List Op in advance. Unlike a state-transition specification (Cslib.DataStructure.StateTransitionSpec), an oblivious-sequence specification has no abstract State field: it constrains the joint probability distribution μ : PMF (List (Sigma Result)) of the full input-output transcript directly via a predicate Contract ops μ.

Every relational state-transition specification D : Cslib.DataStructure.StateTransitionSpec at an initial state s₀ : D.State embeds canonically into ObliviousSequenceSpec via Cslib.DataStructure.StateTransitionSpec.toObliviousSequenceSpec, requiring every transcript in the support of μ to arise from a valid relational execution of D from s₀. On deterministic specifications ([D.HasStepFn f]), this contract reduces to concentration on the unique canonical output trace (D.run s₀ ops).2.

Main definitions

• Cslib.DataStructure.ObliviousSequenceSpec: state-free distributional specification over finite oblivious operation sequences.
• Cslib.DataStructure.TranscriptMatches: alignment predicate out.map Sigma.fst = ops between an operation sequence and an input-output transcript.
• Cslib.DataStructure.ObliviousSequenceSpec.weaken: replaces ValidOpSeq and Contract by arbitrary predicates, keeping Op and Result.
• Cslib.DataStructure.StateTransitionSpec.toObliviousSequenceSpec, Cslib.DataStructure.ObliviousSequenceSpec.ofFn: canonical embeddings of relational and deterministic state-transition specifications into ObliviousSequenceSpec.

Main results

• Cslib.DataStructure.ObliviousSequenceSpec.contract_weaken: a distribution satisfying S.Contract on S.ValidOpSeq satisfies the contract of S.weaken V C on V, when V implies S.ValidOpSeq and S.Contract implies C on S.ValidOpSeq.
• Cslib.DataStructure.StateTransitionSpec.toObliviousSequenceSpec_contract_matches: every transcript in the support of a distribution satisfying (D.toObliviousSequenceSpec s₀).Contract ops matches ops.
• Cslib.DataStructure.StateTransitionSpec.toObliviousSequenceSpec_contract_iff_of_hasStepFn: on a deterministic specification, (D.toObliviousSequenceSpec s₀).Contract ops μ holds under D.ValidHistory s₀ ops if and only if every out ∈ μ.support equals (D.run s₀ ops).2.
• Cslib.DataStructure.StateTransitionSpec.toObliviousSequenceSpec_contract_pure_run: the point mass PMF.pure (D.run s₀ ops).2 satisfies (D.toObliviousSequenceSpec s₀).Contract ops.

Oblivious-sequence specifications

structure Cslib.DataStructure.ObliviousSequenceSpec : Type (max (u + 1) (v + 1))

A state-free distributional specification for an oblivious (non-adaptive) caller. For each admissible operation sequence ops : List Op, Contract ops μ constrains the joint probability distribution μ : PMF (List (Sigma Result)) of the returned input-output transcript.

• Op : Type u

  Operations available to an oblivious caller.

• Result : self.Op → Type v

  Observation type returned by each operation.

• ValidOpSeq : List self.Op → Prop

  Admissibility predicate on finite oblivious operation sequences ops : List Op.

• Contract (ops : List self.Op) : PMF (List (Sigma self.Result)) → Prop

  Distributional correctness contract on the joint output transcript distribution μ induced by executing ops.

def Cslib.DataStructure.TranscriptMatches {Op : Type u} {Result : Op → Type v} (ops : List Op) (out : List (Sigma Result)) : Prop

An input-output transcript out : List (Sigma Result) matches the operation sequence ops : List Op when its first projections equal ops.

@[simp]

theorem Cslib.DataStructure.transcriptMatches_nil {Op : Type u} {Result : Op → Type v} (out : List (Sigma Result)) : TranscriptMatches [] out ↔ out = []

theorem Cslib.DataStructure.transcriptMatches_nil_right {Op : Type u} {Result : Op → Type v} : TranscriptMatches [] []

@[simp]

theorem Cslib.DataStructure.transcriptMatches_cons {Op : Type u} {Result : Op → Type v} (o : Op) (a : Result o) (ops : List Op) (out : List (Sigma Result)) : TranscriptMatches (o :: ops) (⟨o, a⟩ :: out) ↔ TranscriptMatches ops out

theorem Cslib.DataStructure.TranscriptMatches.append {Op : Type u} {Result : Op → Type v} {ops₁ ops₂ : List Op} {out₁ out₂ : List (Sigma Result)} (h₁ : TranscriptMatches ops₁ out₁) (h₂ : TranscriptMatches ops₂ out₂) : TranscriptMatches (ops₁ ++ ops₂) (out₁ ++ out₂)

theorem Cslib.DataStructure.TranscriptMatches.length_eq {Op : Type u} {Result : Op → Type v} {ops : List Op} {out : List (Sigma Result)} (h : TranscriptMatches ops out) : out.length = ops.length

@[reducible, inline]

abbrev Cslib.DataStructure.ObliviousSequenceSpec.Label (S : ObliviousSequenceSpec) : Type (max u v)

Input-output label pairing an operation with its observation.

def Cslib.DataStructure.ObliviousSequenceSpec.weaken (S : ObliviousSequenceSpec) (ValidOpSeq' : List S.Op → Prop) (Contract' : List S.Op → PMF (List (Sigma S.Result)) → Prop) : ObliviousSequenceSpec

Replace the admissible operation sequences of an ObliviousSequenceSpec by ValidOpSeq' and its distributional contract by Contract', keeping Op and Result. The new predicates need not be related to S; contract_weaken assumes that ValidOpSeq' implies S.ValidOpSeq and that S.Contract implies Contract' on S.ValidOpSeq.

@[simp]

theorem Cslib.DataStructure.ObliviousSequenceSpec.weaken_op (S : ObliviousSequenceSpec) (V : List S.Op → Prop) (C : List S.Op → PMF (List (Sigma S.Result)) → Prop) : (S.weaken V C).Op = S.Op

@[simp]

theorem Cslib.DataStructure.ObliviousSequenceSpec.weaken_result (S : ObliviousSequenceSpec) (V : List S.Op → Prop) (C : List S.Op → PMF (List (Sigma S.Result)) → Prop) : (S.weaken V C).Result = S.Result

@[simp]

theorem Cslib.DataStructure.ObliviousSequenceSpec.weaken_validOpSeq (S : ObliviousSequenceSpec) (V : List S.Op → Prop) (C : List S.Op → PMF (List (Sigma S.Result)) → Prop) (ops : List S.Op) : (S.weaken V C).ValidOpSeq ops ↔ V ops

@[simp]

theorem Cslib.DataStructure.ObliviousSequenceSpec.weaken_contract (S : ObliviousSequenceSpec) (V : List S.Op → Prop) (C : List S.Op → PMF (List (Sigma S.Result)) → Prop) (ops : List S.Op) (μ : PMF (List (Sigma S.Result))) : (S.weaken V C).Contract ops μ ↔ C ops μ

theorem Cslib.DataStructure.ObliviousSequenceSpec.contract_weaken {S : ObliviousSequenceSpec} {V : List S.Op → Prop} {C : List S.Op → PMF (List (Sigma S.Result)) → Prop} (hV : ∀ (ops : List S.Op), V ops → S.ValidOpSeq ops) (hC : ∀ (ops : List S.Op) (μ : PMF (List (Sigma S.Result))), S.ValidOpSeq ops → S.Contract ops μ → C ops μ) {ops : List S.Op} {μ : PMF (List (Sigma S.Result))} (hv : (S.weaken V C).ValidOpSeq ops) (hμ : S.ValidOpSeq ops → S.Contract ops μ) : (S.weaken V C).Contract ops μ

Monotonicity of ObliviousSequenceSpec.weaken: any distribution satisfying S.Contract on S.ValidOpSeq also satisfies (S.weaken V C).Contract on V when V implies S.ValidOpSeq and S.Contract implies C on S.ValidOpSeq.

Canonical embedding of StateTransitionSpec into ObliviousSequenceSpec

@[reducible, inline]

abbrev Cslib.DataStructure.StateTransitionSpec.toObliviousSequenceSpec (D : StateTransitionSpec) (s₀ : D.State) : ObliviousSequenceSpec

Embed a relational state-transition specification D : StateTransitionSpec at initial state s₀ : D.State into DataStructure.ObliviousSequenceSpec:

• ValidOpSeq is demonic operation-sequence admissibility D.ValidOpSeq s₀;
• Contract ops μ requires every transcript out ∈ μ.support to be the label sequence of some valid relational execution transcript tr : D.Transcript with tr.ops = ops.

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.toObliviousSequenceSpec_op (D : StateTransitionSpec) (s₀ : D.State) : (D.toObliviousSequenceSpec s₀).Op = D.Op

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.toObliviousSequenceSpec_result (D : StateTransitionSpec) (s₀ : D.State) : (D.toObliviousSequenceSpec s₀).Result = D.Result

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.toObliviousSequenceSpec_validOpSeq (D : StateTransitionSpec) (s₀ : D.State) (ops : List D.Op) : (D.toObliviousSequenceSpec s₀).ValidOpSeq ops ↔ D.ValidOpSeq s₀ ops

theorem Cslib.DataStructure.StateTransitionSpec.toObliviousSequenceSpec_contract (D : StateTransitionSpec) (s₀ : D.State) (ops : List D.Op) (μ : PMF (List (Sigma D.Result))) : (D.toObliviousSequenceSpec s₀).Contract ops μ ↔ ∀ out ∈ μ.support, ∃ (tr : D.Transcript) (s_fin : D.State), tr.ops = ops ∧ tr.labels = out ∧ D.ValidTranscript s₀ tr s_fin

theorem Cslib.DataStructure.StateTransitionSpec.toObliviousSequenceSpec_contract_matches {D : StateTransitionSpec} {s₀ : D.State} {ops : List D.Op} {μ : PMF (List (Sigma D.Result))} (h : (D.toObliviousSequenceSpec s₀).Contract ops μ) (out : List (Sigma D.Result)) : out ∈ μ.support → TranscriptMatches ops out

Every transcript in the support of a distribution satisfying (D.toObliviousSequenceSpec s₀).Contract ops μ matches ops.

theorem Cslib.DataStructure.StateTransitionSpec.toObliviousSequenceSpec_contract_iff_of_hasStepFn (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (s₀ : D.State) {ops : List D.Op} (hv : D.ValidHistory s₀ ops) (μ : PMF (List (Sigma D.Result))) : (D.toObliviousSequenceSpec s₀).Contract ops μ ↔ ∀ out ∈ μ.support, out = (D.run s₀ ops).2

On a deterministic specification ([D.HasStepFn f]) and an admissible operation sequence D.ValidHistory s₀ ops, (D.toObliviousSequenceSpec s₀).Contract ops μ holds if and only if every output trace in μ.support equals (D.run s₀ ops).2.

theorem Cslib.DataStructure.StateTransitionSpec.toObliviousSequenceSpec_contract_pure_run (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (s₀ : D.State) {ops : List D.Op} (hv : D.ValidHistory s₀ ops) : (D.toObliviousSequenceSpec s₀).Contract ops (PMF.pure (D.run s₀ ops).2)

The point mass PMF.pure (D.run s₀ ops).2 satisfies (D.toObliviousSequenceSpec s₀).Contract ops whenever D.ValidHistory s₀ ops.

@[reducible, inline]

abbrev Cslib.DataStructure.ObliviousSequenceSpec.ofFn {State : Type u} {Op : Type v} {Result : Op → Type w} (stepFn : State → (o : Op) → State × Result o) (s₀ : State) (valid : State → Op → Prop := fun (x : State) (x_1 : Op) => True) : ObliviousSequenceSpec

Construct an ObliviousSequenceSpec from a deterministic state-transition function stepFn : (s : State) → (o : Op) → State × Result o, an initial state s₀ : State, and an optional per-step admissibility predicate valid.