Distributional refinements of randomized specifications

A RandomizedSpec is a state-transition specification whose operations draw their outcome from a distribution: law o is a stateful PMF handler. A client runs against it by OracleComp.interpret, and RandomizedSpec.run is the joint distribution of its result and final state. Its support is a relational StateTransitionSpec (RandomizedSpec.toSpec), and a deterministic specification is a randomized one with point-mass outcomes (StateTransitionSpec.toRandomized). An implementation that flips coins calls E.withCoins, the interface E beside uniform sampling, whose clients are the ProbOracleComp E.Result programs.

A RandomizedRefinement D F extends a relational Refinement of the supports with one distributional obligation. From a state satisfying the invariant, each admissible method's joint distribution of answer and abstracted final state is the specified law (law). The relational part then supplies the implementation invariant, the admissibility of lower calls and pathwise amortized costs (Refinement.Amortized of toRefinement), and the law lifts to every adaptive client (RandomizedRefinement.run_link). All probability is then done on the specification. States, operations and answers live in Type, as for ProbOracleComp and OracleComp.IdenticalUntilBad.

Failure events take one more step. If the real methods agree with exact ones until a bad lower state (OracleComp.IdenticalUntilBad), any experiment on the real client accepts at most as often as on the specification, plus the probability of the bad event (RandomizedRefinement.bind_apply_le_of_identicalUntilBad). OracleComp.toOuterMeasure_bad_le bounds that probability by per-call charges.

Expected costs go through charges as well. RandomizedSpec.expectedCost is the expected total charge of a client. A RandomizedRefinement.ExpectedAmortized certificate bounds each method's expected lower cost plus expected final potential by the upper charge plus the initial potential; it telescopes along adaptive clients (ExpectedAmortized.client) and stacks across composition (ExpectedAmortized.comp). When charges do not depend on the state, a query budget (OracleComp.IsCostBounded) bounds the expected cost (expectedCost_le_of_isCostBounded).

Hops stack whether or not they flip coins. A deterministic refinement is a distributional one of the point-mass laws (Refinement.toRandomized), and its pathwise amortized costs are expected ones (Refinement.Amortized.toRandomized). Coins pass through a refinement unchanged (RandomizedRefinement.withCoins), and two layers of coins merge into one (RandomizedRefinement.mergeCoins). So a hop with coins of its own composes over a lower hop with coins (RandomizedRefinement.compCoins), and expected potentials stack across it (ExpectedAmortized.compCoins).

Main definitions

• RandomizedSpec, RandomizedSpec.run: randomized specifications and the law of a client run.
• RandomizedSpec.toSpec: the relational support.
• StateTransitionSpec.toRandomized: a deterministic specification as a randomized one.
• RandomizedSpec.withCoins: an interface together with private uniform coins.
• RandomizedSpec.obliviousClient: issue a fixed list of operations and record the transcript.
• RandomizedRefinement, RandomizedRefinement.ofLaw: distributional refinements, and the constructor that derives the relational step from the law.
• RandomizedRefinement.comp: composition.
• RandomizedRefinement.handler: the methods as a stateful handler on lower states.
• RandomizedSpec.expectedCost, RandomizedRefinement.ExpectedAmortized: expected charges and expected amortized cost refinements.
• RandomizedSpec.coinCharge: charges on an interface with coins.
• RandomizedRefinement.withCoins, RandomizedRefinement.mergeCoins, RandomizedRefinement.compCoins: coins through refinements, merged coin streams, and the composition of hops with coins.
• Refinement.toRandomized: a deterministic refinement as a distributional one.

Main results

• RandomizedSpec.mem_support_run_of_clientRun, RandomizedSpec.exists_clientRun_of_mem_support: the support of a run consists of the relational runs.
• StateTransitionSpec.run_toRandomized, StateTransitionSpec.toRandomized_step_iff, StateTransitionSpec.toRandomized_demonicValid_iff: a deterministic run is a point mass, and the support of a deterministic specification is itself, with the same admissible clients.
• RandomizedSpec.demonicValid_liftRight, RandomizedSpec.demonicValid_liftRight_iff, RandomizedSpec.demonicValid_sample_bind: coin calls are admissible, and programs over E keep their admissibility.
• RandomizedSpec.expectedCost_bind, RandomizedSpec.expectedCost_le_of_isCostBounded, RandomizedSpec.isCostBounded_obliviousClient: expected charges of sequenced programs, and query budgets.
• RandomizedRefinement.run_link: the law of a linked client, read through the abstraction, is the law of the client on the specification.
• RandomizedRefinement.inv_of_mem_support_link: the invariant holds on every outcome.
• RandomizedRefinement.bind_apply_le_of_identicalUntilBad, RandomizedRefinement.abs_sub_le_of_identicalUntilBad: the identical-until-bad step.
• RandomizedRefinement.ExpectedAmortized.client, RandomizedRefinement.ExpectedAmortized.comp, RandomizedRefinement.ExpectedAmortized.of_isCostBounded: expected amortized costs.
• StateTransitionSpec.expectedCost_toRandomized, Refinement.Amortized.toRandomized: expected charges of deterministic runs, and pathwise amortized costs as expected ones.
• RandomizedRefinement.ExpectedAmortized.withCoins, RandomizedRefinement.expectedAmortized_mergeCoins, RandomizedRefinement.ExpectedAmortized.compCoins: expected amortized costs through coins.

References

• D. Boneh, V. Shoup, A Graduate Course in Applied Cryptography, Version 0.6, Theorem 4.7.
• Cormen, Leiserson, Rivest and Stein, Introduction to Algorithms, Chapter 17.

structure Cslib.DataStructure.RandomizedSpec : Type 1

A randomized specification: from each state, an operation draws its answer and next state from the distribution law o. Admissibility valid constrains only refinement certificates.

• State : Type

  Mathematical states.

• Op : Type

  Operations available to clients.

• Result : self.Op → Type

  The answer type of each operation.

• law (o : self.Op) : StateT self.State PMF (self.Result o)

  The distribution of the answer and the next state of each operation.

• valid : self.State → self.Op → Prop

  Preconditions under which an implementation must realize an operation.

@[reducible, inline]

abbrev Cslib.DataStructure.RandomizedSpec.toSpec (D : RandomizedSpec) : StateTransitionSpec

The support of a randomized specification as a relational specification: a step is permitted when the law gives it positive probability.

@[reducible, inline]

noncomputable abbrev Cslib.DataStructure.RandomizedSpec.run (D : RandomizedSpec) {α : Type} (p : OracleComp D.Result α) (s : D.State) : PMF (α × D.State)

The joint distribution of the result and the final state of a client run from s.

@[simp]

theorem Cslib.DataStructure.RandomizedSpec.run_pure (D : RandomizedSpec) {α : Type} (a : α) (s : D.State) : D.run (pure a) s = PMF.pure (a, s)

theorem Cslib.DataStructure.RandomizedSpec.run_liftBind (D : RandomizedSpec) {α : Type} (o : D.Op) (k : D.Result o → OracleComp D.Result α) (s : D.State) : D.run (PFunctor.FreeM.liftBind o k) s = (D.law o s).bind fun (x : D.Result o × D.State) => match x with | (a, s') => D.run (k a) s'

A call followed by a continuation draws the call's outcome, then runs the continuation.

theorem Cslib.DataStructure.RandomizedSpec.run_bind (D : RandomizedSpec) {α β : Type} (p : OracleComp D.Result α) (k : α → OracleComp D.Result β) (s : D.State) : D.run (p >>= k) s = (D.run p s).bind fun (x : α × D.State) => match x with | (a, s') => D.run (k a) s'

Running p >>= k runs p, then k at its result from the state it reached.

theorem Cslib.DataStructure.RandomizedSpec.run_map (D : RandomizedSpec) {α β : Type} (f : α → β) (p : OracleComp D.Result α) (s : D.State) : D.run (f <$> p) s = PMF.map (fun (x : α × D.State) => match x with | (a, s') => (f a, s')) (D.run p s)

Mapping the result of a client maps the result of its run.

@[simp]

theorem Cslib.DataStructure.RandomizedSpec.run_query (D : RandomizedSpec) (o : D.Op) (s : D.State) : D.run (OracleComp.query o) s = D.law o s

A single call draws its answer and next state from the law.

theorem Cslib.DataStructure.RandomizedSpec.mem_support_run_of_clientRun (D : RandomizedSpec) {α : Type} {p : D.toSpec.Client α} {s s' : D.toSpec.State} {a : α} {tr : D.toSpec.Transcript} (h : D.toSpec.ClientRun s p a s' tr) : (a, s') ∈ (D.run p s).support

Every relational run of a client has positive probability.

theorem Cslib.DataStructure.RandomizedSpec.exists_clientRun_of_mem_support (D : RandomizedSpec) {α : Type} {p : D.toSpec.Client α} {s s' : D.toSpec.State} {a : α} (hv : D.toSpec.DemonicValid s p) (h : (a, s') ∈ (D.run p s).support) : ∃ (tr : D.toSpec.Transcript), D.toSpec.ClientRun s p a s' tr

On a demonically admissible client, every outcome of positive probability is a relational run.

noncomputable def Cslib.DataStructure.RandomizedSpec.expectedCost (D : RandomizedSpec) {α : Type} (charge : D.State → D.Op → ℕ) : OracleComp D.Result α → D.State → ENNReal

The expected total charge of a client run from s, where a call o from state s costs charge s o. Cslib.OracleComp.expectedCost is the stateless counterpart, for calls answered by fixed distributions.

@[simp]

theorem Cslib.DataStructure.RandomizedSpec.expectedCost_pure (D : RandomizedSpec) {α : Type} (charge : D.State → D.Op → ℕ) (a : α) (s : D.State) : D.expectedCost charge (pure a) s = 0

theorem Cslib.DataStructure.RandomizedSpec.expectedCost_liftBind (D : RandomizedSpec) {α : Type} (charge : D.State → D.Op → ℕ) (o : D.Op) (k : D.Result o → OracleComp D.Result α) (s : D.State) : D.expectedCost charge (PFunctor.FreeM.liftBind o k) s = ↑(charge s o) + ∑' (x : D.Result o × D.State), (D.law o s) x * D.expectedCost charge (k x.1) x.2

@[simp]

theorem Cslib.DataStructure.RandomizedSpec.expectedCost_query (D : RandomizedSpec) (charge : D.State → D.Op → ℕ) (o : D.Op) (s : D.State) : D.expectedCost charge (OracleComp.query o) s = ↑(charge s o)

The expected charge of a single call is its charge.

theorem Cslib.DataStructure.RandomizedSpec.expectedCost_bind (D : RandomizedSpec) {α β : Type} (charge : D.State → D.Op → ℕ) (p : OracleComp D.Result α) (k : α → OracleComp D.Result β) (s : D.State) : D.expectedCost charge (p >>= k) s = D.expectedCost charge p s + ∑' (x : α × D.State), (D.run p s) x * D.expectedCost charge (k x.1) x.2

The expected charge of p >>= k is that of p plus the expected charge of the continuation.

theorem Cslib.DataStructure.RandomizedSpec.expectedCost_le_of_isCostBounded (D : RandomizedSpec) {α : Type} {cost : D.Op → ℕ} {p : OracleComp D.Result α} {n : ℕ} (h : OracleComp.IsCostBounded cost p n) (s : D.State) : D.expectedCost (fun (x : D.State) (o : D.Op) => cost o) p s ≤ ↑n

With charges independent of the state, a query budget bounds the expected charge.

def Cslib.DataStructure.RandomizedSpec.obliviousClient (D : RandomizedSpec) : List D.Op → OracleComp D.Result (List (Sigma D.Result))

Issue a fixed list of operations and return the transcript of operations and answers.

@[simp]

theorem Cslib.DataStructure.RandomizedSpec.obliviousClient_nil (D : RandomizedSpec) : D.obliviousClient [] = pure []

theorem Cslib.DataStructure.RandomizedSpec.obliviousClient_cons (D : RandomizedSpec) (o : D.Op) (os : List D.Op) : D.obliviousClient (o :: os) = PFunctor.FreeM.liftBind o fun (a : { A := D.Op, B := D.Result }.B o) => (fun (x : List (Sigma D.Result)) => ⟨o, a⟩ :: x) <$> D.obliviousClient os

theorem Cslib.DataStructure.RandomizedSpec.isCostBounded_obliviousClient (D : RandomizedSpec) (cost : D.Op → ℕ) (ops : List D.Op) : OracleComp.IsCostBounded cost (D.obliviousClient ops) (List.map cost ops).sum

The calls of an oblivious client cost the sum of the costs of its operations.

Private coins

@[reducible, inline]

noncomputable abbrev Cslib.DataStructure.RandomizedSpec.withCoins (E : RandomizedSpec) : RandomizedSpec

The interface E together with private uniform coins: a call .inl n is answered uniformly from Fin (n + 1) and leaves the state unchanged, and a call .inr o is a call of E. Its clients are the ProbOracleComp E.Result programs.

@[simp]

theorem Cslib.DataStructure.RandomizedSpec.withCoins_run_liftRight {D : RandomizedSpec} {α : Type} (p : OracleComp D.Result α) (s : D.State) : D.withCoins.run p.liftRight s = D.run p s

A program over E alone runs as over E.

@[simp]

theorem Cslib.DataStructure.RandomizedSpec.withCoins_run_sample {D : RandomizedSpec} {α : Type} (q : ProbComp α) (s : D.State) : D.withCoins.run (ProbOracleComp.sample q) s = PMF.map (fun (x : α) => (x, s)) q.eval

A closed sampler draws its value and leaves the state unchanged.

theorem Cslib.DataStructure.RandomizedSpec.demonicValid_liftRight {D : RandomizedSpec} {α : Type} {p : D.toSpec.Client α} {s : D.toSpec.State} (h : D.toSpec.DemonicValid s p) : D.withCoins.toSpec.DemonicValid s (OracleComp.liftRight p)

Admissibility over E is admissibility of the embedded program.

theorem Cslib.DataStructure.RandomizedSpec.demonicValid_liftRight_iff {D : RandomizedSpec} {α : Type} {p : D.toSpec.Client α} {s : D.toSpec.State} : D.withCoins.toSpec.DemonicValid s (OracleComp.liftRight p) ↔ D.toSpec.DemonicValid s p

A program over E is admissible over E.withCoins exactly when it is admissible over E.

theorem Cslib.DataStructure.RandomizedSpec.demonicValid_sample_bind {D : RandomizedSpec} {α β : Type} {q : ProbComp β} {k : β → OracleComp D.withCoins.Result α} {s : D.State} (h : ∀ (b : β), D.withCoins.toSpec.DemonicValid s (k b)) : D.withCoins.toSpec.DemonicValid s (ProbOracleComp.sample q >>= k)

Coin calls are admissible, and leave the state unchanged.

theorem Cslib.DataStructure.RandomizedSpec.withCoins_run_sample_bind {D : RandomizedSpec} {α β : Type} (q : ProbComp β) (k : β → OracleComp D.withCoins.Result α) (s : D.State) : D.withCoins.run (ProbOracleComp.sample q >>= k) s = q.eval.bind fun (b : β) => D.withCoins.run (k b) s

A closed sampler followed by a continuation draws a value, then runs the continuation from the same state.

theorem Cslib.DataStructure.RandomizedSpec.withCoins_law_inl {D : RandomizedSpec} (n : ℕ) (s : D.State) : D.withCoins.law (Sum.inl n) s = PMF.map (fun (x : Fin (n + 1)) => (x, s)) (ProbComp.unifOracle n)

A coin call draws uniformly and leaves the state unchanged.

theorem Cslib.DataStructure.RandomizedSpec.demonicValid_coin {D : RandomizedSpec} (n : ℕ) (s : D.State) : D.withCoins.toSpec.DemonicValid s (OracleComp.query (Sum.inl n))

A single coin call is admissible.

theorem Cslib.DataStructure.RandomizedSpec.demonicValid_query_inr {D : RandomizedSpec} {o : D.Op} {s : D.State} (h : D.valid s o) : D.withCoins.toSpec.DemonicValid s (OracleComp.query (Sum.inr o))

A single admissible call of D, made over D.withCoins, is admissible.

def Cslib.DataStructure.RandomizedSpec.coinCharge (D : RandomizedSpec) (coin : ℕ → ℕ) (charge : D.State → D.Op → ℕ) : D.withCoins.State → D.withCoins.Op → ℕ

Charges on D.withCoins: a coin call .inl n costs coin n, and a call .inr o costs as in D.

@[simp]

theorem Cslib.DataStructure.RandomizedSpec.coinCharge_const {D : RandomizedSpec} (K : ℕ) : (D.coinCharge (fun (x : ℕ) => K) fun (x : D.State) (x_1 : D.Op) => K) = fun (x : D.withCoins.State) (x_1 : D.withCoins.Op) => K

A constant charge on coin calls and on calls of D is that constant on D.withCoins.

theorem Cslib.DataStructure.RandomizedSpec.expectedCost_liftRight {D : RandomizedSpec} {α : Type} (coin : ℕ → ℕ) (charge : D.State → D.Op → ℕ) (p : OracleComp D.Result α) (s : D.State) : D.withCoins.expectedCost (D.coinCharge coin charge) p.liftRight s = D.expectedCost charge p s

A program over D alone costs over D.withCoins what it costs over D.

Deterministic specifications

@[reducible, inline]

noncomputable abbrev Cslib.DataStructure.StateTransitionSpec.toRandomized (D : StateTransitionSpec) {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] : RandomizedSpec

A deterministic specification as a randomized one: each outcome is a point mass.

@[simp]

theorem Cslib.DataStructure.StateTransitionSpec.run_toRandomized {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α : Type} (p : D.Client α) (s : D.State) : D.toRandomized.run p s = PMF.pure (eval D p s)

A deterministic run is the point mass at the evaluated result and final state.

theorem Cslib.DataStructure.StateTransitionSpec.toRandomized_step_iff {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] (s s' : D.State) (o : D.Op) (a : D.Result o) : D.toRandomized.toSpec.step s o s' a ↔ D.step s o s' a

The support of a deterministic specification is the specification.

theorem Cslib.DataStructure.StateTransitionSpec.toRandomized_demonicValid {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α : Type} {p : D.Client α} {s : D.State} (h : D.DemonicValid s p) : D.toRandomized.toSpec.DemonicValid s p

Admissibility on a deterministic specification is admissibility on its support.

theorem Cslib.DataStructure.StateTransitionSpec.toRandomized_demonicValid_iff {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α : Type} {p : D.Client α} {s : D.State} : D.toRandomized.toSpec.DemonicValid s p ↔ D.DemonicValid s p

Admissibility on the support of a deterministic specification is admissibility on it.

theorem Cslib.DataStructure.StateTransitionSpec.toRandomized_demonicValid_of_validHistory {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α : Type} {p : D.Client α} {s : D.State} (h : D.ValidHistory s (D.clientHistory s p)) : D.toRandomized.toSpec.DemonicValid s p

Admissibility of a deterministic history is admissibility on the support.

theorem Cslib.DataStructure.StateTransitionSpec.run_withCoins_query_bind {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {β : Type} (o : D.Op) (k : D.Result o → ProbOracleComp D.Result β) (s : D.State) : D.toRandomized.withCoins.run (ProbOracleComp.query o >>= k) s = D.toRandomized.withCoins.run (k (D.stepFn s o).2) (D.stepFn s o).1

Over a deterministic specification with coins, a call steps the state and continues with its answer.

theorem Cslib.DataStructure.StateTransitionSpec.demonicValid_withCoins_query_bind {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {β : Type} {o : D.Op} {k : D.Result o → ProbOracleComp D.Result β} {s : D.State} (hv : D.valid s o) (hk : D.toRandomized.withCoins.toSpec.DemonicValid (D.stepFn s o).1 (k (D.stepFn s o).2)) : D.toRandomized.withCoins.toSpec.DemonicValid s (ProbOracleComp.query o >>= k)

Over a deterministic specification with coins, an admissible call whose continuation is admissible from the next state is admissible.

theorem Cslib.DataStructure.StateTransitionSpec.expectedCost_toRandomized {D : StateTransitionSpec} {f : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn f] {α : Type} (charge : D.State → D.Op → ℕ) (p : D.Client α) (s : D.State) : D.toRandomized.expectedCost charge p s = ↑(D.totalCost charge s (D.clientHistory s p))

The expected charge of a deterministic run is the total charge of its history.

Distributional refinements

structure Cslib.DataStructure.RandomizedRefinement (D F : RandomizedSpec) extends Cslib.DataStructure.Refinement D.toSpec F.toSpec : Type

A randomized refinement of D by methods over F: a relational refinement of the supports whose methods, from a state satisfying the invariant, realize the specified law through the abstraction function.

• methods : Methods D.toSpec F.toSpec
• inv : F.toSpec.State → Prop
• abs : F.toSpec.State → D.toSpec.State
• valid {e : F.toSpec.State} (o : D.toSpec.Op) : self.inv e → D.toSpec.valid (self.abs e) o → F.toSpec.DemonicValid e (self.methods o)
• correct {e : F.toSpec.State} (o : D.toSpec.Op) {a : D.toSpec.Result o} {e' : F.toSpec.State} {tr : F.toSpec.Transcript} : self.inv e → D.toSpec.valid (self.abs e) o → F.toSpec.ClientRun e (self.methods o) a e' tr → D.toSpec.step (self.abs e) o (self.abs e') a ∧ self.inv e'
• law {e : F.toSpec.State} (o : D.Op) : self.inv e → D.valid (self.abs e) o → PMF.map (fun (x : D.toSpec.Result o × F.State) => match x with | (a, e') => (a, self.abs e')) (F.run (self.methods o) e) = D.law o (self.abs e)

  The answer and the abstracted final state of each admissible method follow the law.

def Cslib.DataStructure.RandomizedRefinement.ofLaw {D F : RandomizedSpec} (methods : Methods D.toSpec F.toSpec) (inv : F.State → Prop) (abs : F.State → D.State) (valid : ∀ {e : F.State} (o : D.Op), inv e → D.valid (abs e) o → F.toSpec.DemonicValid e (methods o)) (inv_run : ∀ {e : F.State} (o : D.Op), inv e → D.valid (abs e) o → ∀ (a : D.toSpec.Result o) (e' : F.State), (a, e') ∈ (F.run (methods o) e).support → inv e') (law : ∀ {e : F.State} (o : D.Op), inv e → D.valid (abs e) o → PMF.map (fun (x : D.toSpec.Result o × F.State) => match x with | (a, e') => (a, abs e')) (F.run (methods o) e) = D.law o (abs e)) : RandomizedRefinement D F

The constructor from admissibility, preservation of the invariant on outcomes of positive probability, and the law. The relational step follows from the law.

theorem Cslib.DataStructure.RandomizedRefinement.inv_of_mem_support {D F : RandomizedSpec} (M : RandomizedRefinement D F) {e : F.State} (o : D.Op) (he : M.inv e) (hv : D.valid (M.abs e) o) {a : D.Result o} {e' : F.State} (h : (a, e') ∈ (F.run (M.methods o) e).support) : M.inv e'

The invariant holds after every outcome of positive probability of an admissible method.

theorem Cslib.DataStructure.RandomizedRefinement.step_of_mem_support {D F : RandomizedSpec} (M : RandomizedRefinement D F) {e : F.State} (o : D.Op) (he : M.inv e) (hv : D.valid (M.abs e) o) {a : D.Result o} {e' : F.State} (h : (a, e') ∈ (F.run (M.methods o) e).support) : (a, M.abs e') ∈ (D.law o (M.abs e)).support

An outcome of positive probability of an admissible method abstracts to a permitted step.

theorem Cslib.DataStructure.RandomizedRefinement.run_link {D F : RandomizedSpec} {α : Type} (M : RandomizedRefinement D F) (p : OracleComp D.Result α) {e : F.State} (he : M.inv e) (hv : D.toSpec.DemonicValid (M.abs e) p) : PMF.map (fun (x : α × F.State) => match x with | (a, e') => (a, M.abs e')) (F.run (link M.methods p) e) = D.run p (M.abs e)

The distributional hop. The law of an admissible client linked through the methods, read through the abstraction function, is the law of the client on the specification. This is OracleComp.run_interpret_map_state_of_invariant for the methods' handler (run_interpret_handler), with preconditions: the law need hold only for admissible operations, and the client must be admissible.

theorem Cslib.DataStructure.RandomizedRefinement.inv_of_mem_support_link {D F : RandomizedSpec} {α : Type} (M : RandomizedRefinement D F) (p : OracleComp D.Result α) {e : F.State} (he : M.inv e) (hv : D.toSpec.DemonicValid (M.abs e) p) {a : α} {e' : F.State} (h : (a, e') ∈ (F.run (link M.methods p) e).support) : M.inv e'

The invariant holds on every outcome of positive probability of an admissible linked client.

def Cslib.DataStructure.RandomizedRefinement.comp {D F G : RandomizedSpec} (M : RandomizedRefinement D F) (N : RandomizedRefinement F G) : RandomizedRefinement D G

Composition: the upper methods are linked through the lower ones, the invariants conjoin, and the abstraction functions compose.

Identical until bad

@[reducible, inline]

noncomputable abbrev Cslib.DataStructure.RandomizedRefinement.handler {D F : RandomizedSpec} (methods : Methods D.toSpec F.toSpec) (o : D.Op) : StateT F.State PMF (D.Result o)

The methods as a stateful handler of the upper operations on lower states.

theorem Cslib.DataStructure.RandomizedRefinement.run_interpret_handler {D F : RandomizedSpec} {α : Type} (methods : Methods D.toSpec F.toSpec) (p : OracleComp D.Result α) (e : F.State) : (OracleComp.interpret (handler methods) p).run e = F.run (link methods p) e

Interpreting a client through the methods' handler runs the linked client.

theorem Cslib.DataStructure.RandomizedRefinement.bind_apply_le_of_identicalUntilBad {D F : RandomizedSpec} {α : Type} (M : RandomizedRefinement D F) (real : Methods D.toSpec F.toSpec) {bad : F.State → Prop} (h : OracleComp.IdenticalUntilBad (handler real) (handler M.methods) bad) (p : OracleComp D.Result α) {e : F.State} (he : M.inv e) (hv : D.toSpec.DemonicValid (M.abs e) p) {β : Type} (next : α × D.State → PMF β) (b : β) : ((F.run (link real p) e).bind fun (x : α × F.State) => match x with | (a, e') => next (a, M.abs e')) b ≤ ((D.run p (M.abs e)).bind next) b + (F.run (link real p) e).toOuterMeasure {x : α × F.State | bad x.2}

The identical-until-bad step. Let real methods agree with the methods of an exact randomized refinement until a bad lower state. Then an experiment continuing the real client run accepts at most as often as on the specification, plus the probability that the real run reaches a bad state.

theorem Cslib.DataStructure.RandomizedRefinement.abs_sub_le_of_identicalUntilBad {D F : RandomizedSpec} {α : Type} (M : RandomizedRefinement D F) (real : Methods D.toSpec F.toSpec) {bad : F.State → Prop} (h : OracleComp.IdenticalUntilBad (handler real) (handler M.methods) bad) (p : OracleComp D.Result α) {e : F.State} (he : M.inv e) (hv : D.toSpec.DemonicValid (M.abs e) p) {β : Type} (next : α × D.State → PMF β) (b : β) : |(((F.run (link real p) e).bind fun (x : α × F.State) => match x with | (a, e') => next (a, M.abs e')) b).toReal - (((D.run p (M.abs e)).bind next) b).toReal| ≤ ((F.run (link real p) e).toOuterMeasure {x : α × F.State | bad x.2}).toReal

The identical-until-bad step, two-sided. The acceptance probabilities of the real client and of the specification differ by at most the probability that the real run reaches a bad state.

Expected amortized costs

structure Cslib.DataStructure.RandomizedRefinement.ExpectedAmortized {D F : RandomizedSpec} (M : RandomizedRefinement D F) (lower : F.State → F.Op → ℕ) (upper : D.State → D.Op → ℕ) (potential : F.State → ENNReal) : Prop

Expected amortized cost refinement: the expected lower charges of every admissible method, plus the expected potential after it, are at most the upper charge plus the potential before it.

• step {e : F.toSpec.State} (o : D.Op) : M.inv e → D.valid (M.abs e) o → F.expectedCost lower (M.methods o) e + ∑' (x : D.toSpec.Result o × F.State), (F.run (M.methods o) e) x * potential x.2 ≤ ↑(upper (M.abs e) o) + potential e

  The physicist's inequality in expectation, for one method.

theorem Cslib.DataStructure.RandomizedRefinement.ExpectedAmortized.client {D F : RandomizedSpec} {α : Type} {M : RandomizedRefinement D F} {lower : F.State → F.Op → ℕ} {upper : D.State → D.Op → ℕ} {potential : F.State → ENNReal} (A : M.ExpectedAmortized lower upper potential) (p : OracleComp D.Result α) {e : F.State} (he : M.inv e) (hv : D.toSpec.DemonicValid (M.abs e) p) : F.expectedCost lower (link M.methods p) e + ∑' (x : α × F.State), (F.run (link M.methods p) e) x * potential x.2 ≤ D.expectedCost upper p (M.abs e) + potential e

Expected potentials telescope along adaptive clients. The expected lower charges of an admissible linked client, plus the expected final potential, are at most the expected upper charges of the client on the specification plus the initial potential.

theorem Cslib.DataStructure.RandomizedRefinement.ExpectedAmortized.comp {D F G : RandomizedSpec} {M : RandomizedRefinement D F} {upper : D.State → D.Op → ℕ} {N : RandomizedRefinement F G} {lower : G.State → G.Op → ℕ} {middle : F.State → F.Op → ℕ} {Φ : F.State → ENNReal} {Ψ : G.State → ENNReal} (A : M.ExpectedAmortized middle upper Φ) (B : N.ExpectedAmortized lower middle Ψ) : (M.comp N).ExpectedAmortized lower upper fun (g : G.State) => Φ (N.abs g) + Ψ g

Expected potentials stack across composition. The composite is amortized in expectation with the upper potential, read through the lower abstraction, plus the lower potential.

theorem Cslib.DataStructure.RandomizedRefinement.ExpectedAmortized.of_isCostBounded {D F : RandomizedSpec} {M : RandomizedRefinement D F} {cost : F.Op → ℕ} {budget : D.Op → ℕ} (h : ∀ (o : D.toSpec.Op), OracleComp.IsCostBounded cost (M.methods o) (budget o)) : M.ExpectedAmortized (fun (x : F.State) (q : F.Op) => cost q) (fun (x : D.State) (o : D.Op) => budget o) fun (x : F.State) => 0

With charges independent of the state, query budgets of the methods give an expected amortized certificate with zero potential.

Private coins through refinements

def Cslib.DataStructure.RandomizedRefinement.coinMethods {D F : RandomizedSpec} (methods : Methods D.toSpec F.toSpec) : Methods D.withCoins.toSpec F.withCoins.toSpec

The methods with private coins forwarded: a coin call .inl n is the same coin call, and a call .inr o runs the method of o over F.

noncomputable def Cslib.DataStructure.RandomizedRefinement.withCoins {D F : RandomizedSpec} (M : RandomizedRefinement D F) : RandomizedRefinement D.withCoins F.withCoins

Coins pass through refinements. A refinement of D by F refines D.withCoins by F.withCoins, with the same invariant and abstraction: coin calls are forwarded unchanged, and calls of D run their methods.

@[simp]

theorem Cslib.DataStructure.RandomizedRefinement.withCoins_methods_inl {D F : RandomizedSpec} {M : RandomizedRefinement D F} (n : ℕ) : M.withCoins.methods (Sum.inl n) = OracleComp.query (Sum.inl n)

@[simp]

theorem Cslib.DataStructure.RandomizedRefinement.withCoins_methods_inr {D F : RandomizedSpec} {M : RandomizedRefinement D F} (o : D.Op) : M.withCoins.methods (Sum.inr o) = OracleComp.liftRight (M.methods o)

@[simp]

theorem Cslib.DataStructure.RandomizedRefinement.withCoins_inv {D F : RandomizedSpec} {M : RandomizedRefinement D F} (e : F.State) : M.withCoins.inv e ↔ M.inv e

@[simp]

theorem Cslib.DataStructure.RandomizedRefinement.withCoins_abs {D F : RandomizedSpec} {M : RandomizedRefinement D F} (e : F.State) : M.withCoins.abs e = M.abs e

def Cslib.DataStructure.RandomizedRefinement.mergeMethods (G : RandomizedSpec) : Methods G.withCoins.withCoins.toSpec G.withCoins.toSpec

The methods merging two layers of private coins: coin calls of either layer become coin calls, and calls of G are forwarded.

noncomputable def Cslib.DataStructure.RandomizedRefinement.mergeCoins (G : RandomizedSpec) : RandomizedRefinement G.withCoins.withCoins G.withCoins

Two layers of private coins are one. Every call of G.withCoins.withCoins is one call of G.withCoins with the same law, so the identity on states is a refinement.

theorem Cslib.DataStructure.RandomizedRefinement.mergeCoins_methods {G : RandomizedSpec} : (mergeCoins G).methods = mergeMethods G

noncomputable def Cslib.DataStructure.RandomizedRefinement.compCoins {D F G : RandomizedSpec} (M : RandomizedRefinement D F.withCoins) (N : RandomizedRefinement F G.withCoins) : RandomizedRefinement D G.withCoins

Coin-using hops compose. A refinement of D by F with coins, over a refinement of F by G with coins, refines D by G with one stream of coins.

@[simp]

theorem Cslib.DataStructure.RandomizedRefinement.compCoins_inv {D F G : RandomizedSpec} (M : RandomizedRefinement D F.withCoins) (N : RandomizedRefinement F G.withCoins) (g : G.State) : (M.compCoins N).inv g ↔ N.inv g ∧ M.inv (N.abs g)

@[simp]

theorem Cslib.DataStructure.RandomizedRefinement.compCoins_abs {D F G : RandomizedSpec} (M : RandomizedRefinement D F.withCoins) (N : RandomizedRefinement F G.withCoins) (g : G.State) : (M.compCoins N).abs g = M.abs (N.abs g)

theorem Cslib.DataStructure.RandomizedRefinement.ExpectedAmortized.withCoins {D F : RandomizedSpec} {M : RandomizedRefinement D F} {lower : F.State → F.Op → ℕ} {upper : D.State → D.Op → ℕ} {potential : F.State → ENNReal} {coin : ℕ → ℕ} (A : M.ExpectedAmortized lower upper potential) : M.withCoins.ExpectedAmortized (F.coinCharge coin lower) (D.coinCharge coin upper) potential

Expected amortized costs pass through coins: coin calls cost the same on both sides and leave the potential unchanged.

theorem Cslib.DataStructure.RandomizedRefinement.expectedAmortized_mergeCoins {G : RandomizedSpec} {coin : ℕ → ℕ} (charge : G.State → G.Op → ℕ) : (mergeCoins G).ExpectedAmortized (G.coinCharge coin charge) (G.withCoins.coinCharge coin (G.coinCharge coin charge)) fun (x : G.withCoins.State) => 0

Merging coin streams costs one call per call, with zero potential.

theorem Cslib.DataStructure.RandomizedRefinement.ExpectedAmortized.compCoins {D F G : RandomizedSpec} {upper : D.State → D.Op → ℕ} {coin : ℕ → ℕ} {M : RandomizedRefinement D F.withCoins} {N : RandomizedRefinement F G.withCoins} {lower : G.State → G.Op → ℕ} {middle : F.State → F.Op → ℕ} {Φ : F.State → ENNReal} {Ψ : G.State → ENNReal} (A : M.ExpectedAmortized (F.coinCharge coin middle) upper Φ) (B : N.ExpectedAmortized (G.coinCharge coin lower) middle Ψ) : (M.compCoins N).ExpectedAmortized (G.coinCharge coin lower) upper fun (g : G.withCoins.State) => Φ (N.abs g) + Ψ g

Expected potentials stack across coin-using hops.

Deterministic refinements

noncomputable def Cslib.DataStructure.Refinement.toRandomized {D E : StateTransitionSpec} {fD : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn fD] {fE : E.State → (o : E.Op) → E.State × E.Result o} [E.HasStepFn fE] (M : Refinement D E) : RandomizedRefinement D.toRandomized E.toRandomized

Deterministic hops are distributional hops. A refinement of deterministic specifications refines their point-mass laws, with the same methods, invariant and abstraction.

@[simp]

theorem Cslib.DataStructure.Refinement.toRandomized_methods {D E : StateTransitionSpec} {fD : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn fD] {fE : E.State → (o : E.Op) → E.State × E.Result o} [E.HasStepFn fE] (M : Refinement D E) : M.toRandomized.methods = M.methods

@[simp]

theorem Cslib.DataStructure.Refinement.toRandomized_inv {D E : StateTransitionSpec} {fD : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn fD] {fE : E.State → (o : E.Op) → E.State × E.Result o} [E.HasStepFn fE] (M : Refinement D E) (e : E.State) : M.toRandomized.inv e ↔ M.inv e

@[simp]

theorem Cslib.DataStructure.Refinement.toRandomized_abs {D E : StateTransitionSpec} {fD : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn fD] {fE : E.State → (o : E.Op) → E.State × E.Result o} [E.HasStepFn fE] (M : Refinement D E) (e : E.State) : M.toRandomized.abs e = M.abs e

theorem Cslib.DataStructure.Refinement.Amortized.toRandomized {D E : StateTransitionSpec} {fD : D.State → (o : D.Op) → D.State × D.Result o} [D.HasStepFn fD] {fE : E.State → (o : E.Op) → E.State × E.Result o} [E.HasStepFn fE] {M : Refinement D E} {lower : E.State → E.Op → ℕ} {upper : D.State → D.Op → ℕ} {potential : E.State → ℕ} (A : M.Amortized lower upper potential) : M.toRandomized.ExpectedAmortized lower upper fun (e : E.toRandomized.State) => ↑(potential e)

Pathwise amortized costs of a deterministic refinement are expected amortized costs of its distributional form.