Sums of oracle interfaces

A program may call two interfaces at once: a query of spec₁ ⊕ₒ spec₂ is a query of either, answered as there. A program with private coins is the main instance (probOracleSpec), with uniform sampling on the left; a forger calling a signer and a hash function, and the prover and verifier oracles of an interactive protocol, are others.

OracleComp.sumHandler left right answers the two kinds of call with handlers in the same monad, and OracleComp.liftLeft and OracleComp.liftRight embed a program over one side. Interpreting an embedded program uses only the corresponding handler (interpret_sumHandler_liftLeft).

Main definitions

• Cslib.OracleSpec.sum, notation spec₁ ⊕ₒ spec₂: the disjoint sum of two interfaces.
• Cslib.OracleSpec.empty: the interface without queries.
• Cslib.OracleComp.sumHandler: answer the two sides with separate handlers.
• Cslib.OracleComp.liftLeft, Cslib.OracleComp.liftRight: embed a program over one side.

Main results

• Cslib.OracleComp.interpret_sumHandler_liftLeft, .interpret_sumHandler_liftRight: an embedded program uses only its own side's handler.
• Cslib.OracleComp.interpret_sumHandler: interpretation distributes over the two sides.

@[reducible, inline]

abbrev Cslib.OracleSpec.sum {ι₁ ι₂ : Type u} (spec₁ : OracleSpec ι₁) (spec₂ : OracleSpec ι₂) : OracleSpec (ι₁ ⊕ ι₂)

The disjoint sum of two interfaces: a query of either, answered as there.

def Cslib.«term_⊕ₒ_» : Lean.TrailingParserDescr

The disjoint sum of two interfaces: a query of either, answered as there.

@[reducible, inline]

abbrev Cslib.OracleSpec.empty : OracleSpec Empty

The interface without queries, for a party that uses no oracle.

@[reducible, inline]

abbrev Cslib.OracleComp.sumHandler {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {m : Type v → Type w} (left : (q : ι₁) → m (spec₁ q)) (right : (q : ι₂) → m (spec₂ q)) (q : ι₁ ⊕ ι₂) : m (spec₁.sum spec₂ q)

Answer the calls of the left interface with left and those of the right with right.

theorem Cslib.OracleComp.sumHandler_inl {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {m : Type v → Type w} (left : (q : ι₁) → m (spec₁ q)) (right : (q : ι₂) → m (spec₂ q)) (q : ι₁) : sumHandler left right (Sum.inl q) = left q

theorem Cslib.OracleComp.sumHandler_inr {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {m : Type v → Type w} (left : (q : ι₁) → m (spec₁ q)) (right : (q : ι₂) → m (spec₂ q)) (q : ι₂) : sumHandler left right (Sum.inr q) = right q

def Cslib.OracleComp.liftLeft {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {α : Type v} (program : OracleComp spec₁ α) : OracleComp (spec₁.sum spec₂) α

A program over the left interface, as a program over the sum.

def Cslib.OracleComp.liftRight {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {α : Type v} (program : OracleComp spec₂ α) : OracleComp (spec₁.sum spec₂) α

A program over the right interface, as a program over the sum.

@[simp]

theorem Cslib.OracleComp.liftLeft_pure {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {α : Type v} (a : α) : (pure a).liftLeft = pure a

@[simp]

theorem Cslib.OracleComp.liftRight_pure {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {α : Type v} (a : α) : (pure a).liftRight = pure a

@[simp]

theorem Cslib.OracleComp.liftLeft_bind {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {α β : Type v} (program : OracleComp spec₁ α) (next : α → OracleComp spec₁ β) : (program >>= next).liftLeft = do let a ← program.liftLeft (next a).liftLeft

@[simp]

theorem Cslib.OracleComp.liftRight_bind {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {α β : Type v} (program : OracleComp spec₂ α) (next : α → OracleComp spec₂ β) : (program >>= next).liftRight = do let a ← program.liftRight (next a).liftRight

@[simp]

theorem Cslib.OracleComp.liftLeft_map {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {α β : Type v} (f : α → β) (program : OracleComp spec₁ α) : (f <$> program).liftLeft = f <$> program.liftLeft

@[simp]

theorem Cslib.OracleComp.liftRight_map {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {α β : Type v} (f : α → β) (program : OracleComp spec₂ α) : (f <$> program).liftRight = f <$> program.liftRight

@[simp]

theorem Cslib.OracleComp.liftLeft_query {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (q : ι₁) : (query q).liftLeft = query (Sum.inl q)

@[simp]

theorem Cslib.OracleComp.liftRight_query {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} (q : ι₂) : (query q).liftRight = query (Sum.inr q)

@[simp]

theorem Cslib.OracleComp.interpret_sumHandler_liftLeft {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {α : Type v} {m : Type v → Type w} [Monad m] [LawfulMonad m] (left : (q : ι₁) → m (spec₁ q)) (right : (q : ι₂) → m (spec₂ q)) (program : OracleComp spec₁ α) : interpret (sumHandler left right) program.liftLeft = interpret left program

An embedded left program uses only the left handler.

@[simp]

theorem Cslib.OracleComp.interpret_sumHandler_liftRight {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {α : Type v} {m : Type v → Type w} [Monad m] [LawfulMonad m] (left : (q : ι₁) → m (spec₁ q)) (right : (q : ι₂) → m (spec₂ q)) (program : OracleComp spec₂ α) : interpret (sumHandler left right) program.liftRight = interpret right program

An embedded right program uses only the right handler.

theorem Cslib.OracleComp.interpret_sumHandler {ι₁ ι₂ : Type u} {spec₁ : OracleSpec ι₁} {spec₂ : OracleSpec ι₂} {m : Type v → Type w} [Monad m] {κ : Type u} {target : OracleSpec κ} (oracle : (q : κ) → m (target q)) (left : (q : ι₁) → OracleComp target (spec₁ q)) (right : (q : ι₂) → OracleComp target (spec₂ q)) : (fun (q : ι₁ ⊕ ι₂) => interpret oracle (sumHandler left right q)) = sumHandler (fun (q : ι₁) => interpret oracle (left q)) fun (q : ι₂) => interpret oracle (right q)

Interpretation distributes over the two sides of a combined handler.