Documentation

VCVio.OracleComp.Coercions.Append

Coercing Computations to Larger Oracle Sets #

This file defines an append operation on OracleSpec to combine different sets of oracles. We use Sum to combine the indexing sets, so this operation is "ordered" in the sense that the two oracle sets correspond to Sum.inl and Sum.inr. Note that this operation is never associative, as Sum is not associative

We also define a number of coercions involving append. These instances allow an OracleSpec of the form spec₁ ++ₒ ... ++ₒ spec₂ to coerce to one of the form spec'₁ ++ₒ ... ++ₒ spec'₂, assuming that the set of oracles in the first is a sub-sequence of the oracles in the second. We also include associativity instances, so parenthisization of the sequence is irrelevant.

Note that this requires the ordering of oracles in each to match, and so we generally adopt a standard ordering of OracleSpec for computations in order to make this apply as often as possible. We specifically adopt the following convention: {coin_oracle} ++ₒ {unif_spec} ++ₒ {random oracle} ++ₒ {adversary oracles} ++ₒ ..., where any of the individual parts may be ommited. The adversary oracles are for things like a signing oracle in unforgeability experiments of a signature scheme.

TODO!: This is still not as powerful as what could be done in Lean3 ** Maybe just manually add a ton of these, simp should mostly help that**

The typelcasses are applied in an order defined by specific priorities:

  1. Try applying the associativity instance to remove parenthesization.
  2. If both the subspec and superspec are an append, try to independently coerce both sides.
  3. Try to coerce the subspec to the left side of the superspec append.
  4. Try to coerce the subspec to the right side of the superspec append.
  5. Try appending a single oracle to the left side of the subspec.
  6. Try appending a single oracle to the right side of the subspec.
  7. Try coercing the subspec to itself. This ordering is chosen to both give a generally applicable instance tree, and avoid an infinite typeclass search whether or not an instance exists.
source
instance OracleSpec.subSpec_append_left {ι₁ : Type u_1} {ι₂ : Type u_2} (spec₁ : OracleSpec ι₁) (spec₂ : OracleSpec ι₂) :
spec₁ ⊂ₒ spec₁ ++ₒ spec₂

Add additional oracles to the right side of the existing ones.

Equations
source
@[simp]
theorem OracleSpec.liftM_append_left_eq {ι₁ : Type u_1} {ι₂ : Type u_2} (spec₁ : OracleSpec ι₁) (spec₂ : OracleSpec ι₂) {α : Type u} (q : spec₁.OracleQuery α) :
liftM q = match α, q with | .(spec₁.range i), query i t => query (Sum.inl i) t
source
instance OracleSpec.subSpec_append_right {ι₁ : Type u_1} {ι₂ : Type u_2} (spec₁ : OracleSpec ι₁) (spec₂ : OracleSpec ι₂) :
spec₂ ⊂ₒ spec₁ ++ₒ spec₂

Add additional oracles to the left side of the exiting ones

Equations
source
@[simp]
theorem OracleSpec.liftM_append_right_eq {ι₁ : Type u_1} {ι₂ : Type u_2} (spec₁ : OracleSpec ι₁) (spec₂ : OracleSpec ι₂) {α : Type u} (q : spec₂.OracleQuery α) :
liftM q = match α, q with | .(spec₂.range i), query i t => query (Sum.inr i) t
source
instance OracleSpec.subSpec_left_append_left_append_of_subSpec {ι₁ : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} (spec₁ : OracleSpec ι₁) (spec₂ : OracleSpec ι₂) (spec₃ : OracleSpec ι₃) [h : spec₁ ⊂ₒ spec₃] :
spec₁ ++ₒ spec₂ ⊂ₒ spec₃ ++ₒ spec₂
Equations
source
@[simp]
theorem OracleSpec.liftM_left_append_left_append_eq {ι₁ : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} (spec₁ : OracleSpec ι₁) (spec₂ : OracleSpec ι₂) (spec₃ : OracleSpec ι₃) {α : Type u} [h : spec₁ ⊂ₒ spec₃] (q : (spec₁ ++ₒ spec₂).OracleQuery α) :
liftM q = match α, q with | .((spec₁ ++ₒ spec₂).range (Sum.inl i)), query (Sum.inl i) t => liftM (query i t) | .((spec₁ ++ₒ spec₂).range (Sum.inr i)), query (Sum.inr i) t => query (Sum.inr i) t
source
instance OracleSpec.subSpec_right_append_right_append_of_subSpec {ι₁ : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} (spec₁ : OracleSpec ι₁) (spec₂ : OracleSpec ι₂) (spec₃ : OracleSpec ι₃) [h : spec₂ ⊂ₒ spec₃] :
spec₁ ++ₒ spec₂ ⊂ₒ spec₁ ++ₒ spec₃
Equations
source
@[simp]
theorem OracleSpec.liftM_right_append_right_append_eq {ι₁ : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} (spec₁ : OracleSpec ι₁) (spec₂ : OracleSpec ι₂) (spec₃ : OracleSpec ι₃) {α : Type u} [h : spec₂ ⊂ₒ spec₃] (q : (spec₁ ++ₒ spec₂).OracleQuery α) :
liftM q = match α, q with | .((spec₁ ++ₒ spec₂).range (Sum.inl i)), query (Sum.inl i) t => liftM (query i t) | .((spec₁ ++ₒ spec₂).range (Sum.inr i)), query (Sum.inr i) t => liftM (query (Sum.inr i) t)
source
instance OracleSpec.subSpec_assoc {ι₁ : Type u_1} {ι₂ : Type u_2} {ι₃ : Type u_3} (spec₁ : OracleSpec ι₁) (spec₂ : OracleSpec ι₂) (spec₃ : OracleSpec ι₃) :
spec₁ ++ₒ (spec₂ ++ₒ spec₃) ⊂ₒ spec₁ ++ₒ spec₂ ++ₒ spec₃
Equations