You are an expert Lean4 and formal verification agent proving a Lean4 theorem. Your output **must** strictly adhere to the specified format.

### Input Information
You will receive the following components, relevant to the target theorem:
* <all_available_defs>: Definitions available from imported modules (either from the current Lean repository or from Mathlib)
* <all_available_lemmas>: Lemmas/theorems available that may assist the proof.
* <local_ctx>...</local_ctx>: The local file context (imports, namespaces, definitions, comments, etc.) from the top of the file up to—but not including—the target theorem or any previously defined local lemmas/theorems.
* <target_theorem>...</target_theorem>: The target theorem statement, ending with `:=`.

**Notes**
1. Definitions include their full bodies, but for definitions whose bodies contain proofs, the proof parts are replaced by `admit` (i.e., admit /- proof elided -/), while the rest of the definition is kept unchanged; lemmas include only their statements.
2. You may freely reference any definition or lemma contained in these tags without redefining them.
3. The tags for available definitions and lemmas (all_available_defs, all_available_lemmas) may be omitted if empty.

### Output Format & Requirements
Your output MUST contain a complete, syntactically correct Lean 4 proof for the target theorem.

**Strict Output Structure:**
<reasoning> 
...
</reasoning> 

<lean4_invented_lemmas>
-- each lemma is a full Lean 4 declaration with a complete proof
...
</lean4_invented_lemmas>

<lean4_proof>
-- Lean 4 proof body of the target theorem
...
</lean4_proof>

**Requirements:**
1. <reasoning> and <lean4_invented_lemmas> are OPTIONAL. Include them only if they aid proof construction.
2. <lean4_proof> MUST contain only the proof body (tactics/terms), starting by "by", NOT the theorem declaration.
3. <lean4_invented_lemmas> (if present) MUST contain syntactically correct lemma declarations that type checks AND complete proof bodies. Defining a lemma using `axiom` is NOT allowed.
4. <reasoning> contains high-level proof planning.
5. If you create a lemma under <lean4_invented_lemmas> whose name is namespaced (e.g., X.Y.Z), you MUST always refer to it using its fully qualified name. Do NOT rely on shortened names. For example, write rw [X.Y.Z], not rw [Z] for invented lemmas.
6. All Lean 4 code MUST be syntactically correct. No `sorry`, `admit`, or non-Lean text. Comments allowed using `--` or `/- ... -/`.
7. Follow the tags and structure EXACTLY. No extra text before, between, or after the sections.
8. Do NOT wrap invented lemmas in a `mutual` block unless they have genuine mutual recursion. Declare each lemma independently.

### Examples are provided here (example input are under "User Prompt", and example assistant response are under "Agent Response"):
Example 1 ------------------- 
User Prompt:
<all_available_defs>
structure BitVec (w : Nat) where
  /-- Construct a `BitVec w` from a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  ofFin ::

  /-- Interpret a bitvector as a number less than `2^w`.
  O(1), because we use `Fin` as the internal representation of a bitvector. -/
  toFin : Fin (hPow 2 w)
</all_available_defs>

<all_available_lemmas>
theorem List.getElem_append_left{α : Type u_1} {l₁ l₂ : List α} {i : Nat} (hn : i < l₁.length) : (l₁ ++ l₂)[i] = l₁[i]
theorem getElem_eq_testBit_toNat (x : BitVec w) (i : Nat) (h : i < w) :
  x[i] = x.toNat.testBit i := rfl
@[simp, grind =] theorem toNat_cons (b : Bool) (x : BitVec w) :
    (cons b x).toNat = (b.toNat <<< w) ||| x.toNat
@[simp, grind =] theorem getLsbD_of_ge (x : BitVec w) (i : Nat) (ge : w ≤ i) : getLsbD x i = false
theorem testBit_toNat (x : BitVec w) : x.toNat.testBit i = x.getLsbD i
</all_available_lemmas>

<local_ctx>
import Mathlib.Computability.NFA
import Mathlib.Data.FinEnum
import Mathlib.Data.Rel
import Mathlib.Data.Vector.Basic
import Blase.AutoStructs.ForLean

open Set
open Mathlib
open SetRel

-- this is better because card is defeq to n
instance (α : Type) : Inter (Language α) := ⟨Set.inter⟩
instance (α : Type) : Union (Language α) := ⟨Set.union⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width.
-/
structure BitVecs (n : Nat) where
  w : Nat
  bvs : List.Vector (BitVec w) n

def BitVecs.cast (bvs : BitVecs n) (h : n = n') : BitVecs n' :=
  { w := bvs.w, bvs := h ▸ bvs.bvs }

abbrev BitVecs.empty : BitVecs n := ⟨0, List.Vector.replicate n .nil⟩
abbrev BitVecs.singleton {w : Nat} (bv : BitVec w) : BitVecs 1 := ⟨w, bv ::ᵥ .nil⟩
abbrev BitVecs.pair {w : Nat} (bv1 bv2 : BitVec w) : BitVecs 2 := ⟨w, bv1 ::ᵥ bv2 ::ᵥ .nil⟩

/--
The set of `n`-tuples of bit vectors of an arbitrary width, encoded as a list of
bit vectors of width `n`. The width of the encoded bit vectors is the length of
the list.
-/
abbrev BitVecs' (n : Nat) := List (BitVec n)

@[simps]
def dec (bvs' : BitVecs' n) : BitVecs n where
  w := bvs'.length
  bvs := List.Vector.ofFn fun k => BitVec.ofFn fun i => bvs'[i].getLsbD k

@[simp]
</local_ctx>

<target_theorem>
lemma dec_snoc n (bvs' : BitVecs' n) (a : BitVec n) :
  dec (bvs' ++ [a]) =
    { w := bvs'.length + 1
      bvs := List.Vector.ofFn fun k =>
        BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k) } :=
</target_theorem>

Agent Response:
<reasoning> 
The goal is to understand what `dec` does after appending one more bitvector `a` to `bvs'`. By definition, `dec` builds a width `= length` and a vector of bitvectors whose `i`-th bit at position `k` is `bvs'[i].getLsbD k`. So for `bvs' ++ [a]`, we expect the width to increase by 1 and each resulting bitvector to be `BitVec.cons` of the new bit coming from `a`.

First, I use `ext` twice: once on the record to focus on the `bvs` field, and once on the resulting bitvector. This reduces everything to a pointwise statement:
for fixed `k` and `i` with `i < bvs'.length + 1`,
the bit `(bvs' ++ [a])[i].getLsbD k` should match the bit at index `i` of `BitVec.cons (a.getLsbD k) ((dec bvs').bvs.get k)`.

At this point I need a clean description of indexing into `BitVec.cons`: if we have `x : BitVec n`, then `(cons b x)[i]` should give `b` at the new “last” index `n` and `x[i]` otherwise. That motivates an auxiliary lemma `getElem_cons` expressing exactly this behavior, proved via the `testBit`/`toNat` characterization and a case split on `i < n`, `i = n`, `i > n`.

Using `getElem_cons`, the RHS becomes an `if` on whether `i = bvs'.length`. So I split into cases:
- If `i = bvs'.length`, then `(bvs' ++ [a])[i]` is the appended `a`, so both sides reduce to `a.getLsbD k`.
- If `i ≠ bvs'.length`, the bound `i < bvs'.length + 1` forces `i < bvs'.length`. Then `(bvs' ++ [a])[i] = bvs'[i]` by `List.getElem_append_left`, and the RHS takes the “else” branch and likewise gives the bit from `bvs'[i]`. In both subcases, `simp` (plus the definition of `dec`) finishes.

So the whole proof is: `ext` to bit level, unfold `dec` with `simp_all`, rewrite with `getElem_cons`, split on the boundary index `i = length bvs'`, and in the “< length” branch use `List.getElem_append_left` and bounds to line up both sides.
</reasoning> 

<lean4_invented_lemmas>
@[grind =]
theorem getElem_cons {b : Bool} {n} {x : BitVec n} {i : Nat} (h : i < n + 1) :
    (cons b x)[i] = if h : i = n then b else x[i] := by
  simp only [BitVec.getElem_eq_testBit_toNat, BitVec.toNat_cons, Nat.testBit_or]
  rw [Nat.testBit_shiftLeft]
  rcases Nat.lt_trichotomy i n with i_lt_n | i_eq_n | n_lt_i
  · have p1 : ¬(n ≤ i) := by omega
    have p2 : i ≠ n := by omega
    simp [p1, p2]
  · simp only [i_eq_n, ge_iff_le, Nat.le_refl, decide_true, Nat.sub_self, Nat.testBit_zero,
    Bool.true_and, BitVec.testBit_toNat, BitVec.getLsbD_of_ge, Bool.or_false]
    cases b <;> trivial
  · have p1 : i ≠ n := by omega
    have p2 : i - n ≠ 0 := by omega
    simp [p1, p2, Nat.testBit_bool_toNat]
</lean4_invented_lemmas>

<lean4_proof>
by
  ext k i hi <;> simp_all
  rw [getElem_cons]
  split
  next heq => simp_all
  next h =>
    have hlt : i < List.length bvs' := by simp at hi; omega
    rw [List.getElem_append_left hlt]
    simp
</lean4_proof>

### Your task:
<all_available_defs>
inductive FreeMonad (f : Type u → Type v) (α : Type w) : Type (max (u + 1) v w)
  | protected pure (x : α) : FreeMonad f α
  | roll {β : Type u} (x : f β) (r : β → FreeMonad f α) : FreeMonad f α

@[elab_as_elim]
protected def inductionOn {C : FreeMonad f α → Prop}
    (pure : ∀ x, C (pure x))
    (roll : ∀ {β} (x : f β), (r : β → FreeMonad f α) →
      (∀ y, C (r y)) → C (x >>= r)) :
    (oa : FreeMonad f α) → C oa
  | FreeMonad.pure x => pure x
  | FreeMonad.roll x r => roll x _ (λ u ↦
      FreeMonad.inductionOn pure roll (r u))

@[elab_as_elim]
protected def construct {C : FreeMonad f α → Type*}
    (pure : (x : α) → C (pure x))
    (roll : {β : Type u} → (x : f β) → (r : β → FreeMonad f α) →
      ((y : β) → C (r y)) → C (x >>= r)) :
    (oa : FreeMonad f α) → C oa
  | .pure x => pure x
  | .roll x r => roll x _ (λ u ↦ FreeMonad.construct pure roll (r u))

class HasEvalDist (m : Type u → Type v) [Monad m] where
  evalDist {α : Type u} (mx : m α) : SPMF α
  evalDist_pure {α : Type u} (x : α) : evalDist (pure x : m α) = pure x
  evalDist_bind {α β : Type u} (mx : m α) (my : α → m β) :
    evalDist (mx >>= my) = evalDist mx >>= fun x => evalDist (my x)

def supportWhen (oa : OracleComp spec α)
    (possible_outputs : {α : Type v} → OracleQuery spec α → Set α) : Set α :=

def support (oa : OracleComp spec α) : Set α :=
  oa.supportWhen fun _ => Set.univ

inductive OracleQuery {ι : Type u} (spec : OracleSpec.{u,v} ι) : Type v → Type (max u v)
  | query (i : ι) (t : spec.domain i) : OracleQuery spec (spec.range i)

def OracleComp {ι : Type u} (spec : OracleSpec.{u,v} ι) :
    Type w → Type (max u (v + 1) w) :=
  OptionT (FreeMonad (OracleQuery.{u,v} spec))

@[elab_as_elim]
protected def induction {C : OracleComp spec α → Prop}
    (oa : OracleComp spec α) (pure : (a : α) → C (pure a))
    (query_bind : (i : ι) → (t : spec.domain i) →
      (oa : spec.range i → OracleComp spec α) → (∀ u, C (oa u)) → C (query i t >>= oa))
    (failure : C failure) : C oa :=
  FreeMonad.inductionOn (Option.rec failure pure) (λ (query i t) ↦ query_bind i t) oa

@[elab_as_elim]
protected def construct {C : OracleComp spec α → Type*}
    (pure : (a : α) → C (pure a))
    (query_bind : {β : Type v} → (q : OracleQuery spec β) →
      (oa : β → OracleComp spec α) → ((u : β) → C (oa u)) → C (q >>= oa))
    (failure : C failure) (oa : OracleComp spec α) : C oa :=
  FreeMonad.construct (Option.rec failure pure) query_bind oa

def cases {α} {motive : {n : ℕ} → Vector α n → Sort*} (v_empty : motive #v[])
  (v_insert : {n : ℕ} → (hd : α) → (tl : Vector α n) → motive (tl.insertIdx 0 hd)) {m : ℕ} :
    (v : Vector α m) → motive v := match hm : m with
  | 0 => fun v => match v with | ⟨⟨[]⟩, rfl⟩ => v_empty
  | n + 1 => fun v => match hv : v with
    | ⟨⟨hd :: tl⟩, hSize⟩ => by admit /- proof elided -/

def OracleSpec (ι : Type u) : Type (max u (v + 1)) :=
  (i : ι) → Type v × Type v

@[inline, reducible]
protected def domain (spec : OracleSpec ι) (i : ι) : Type v := (spec i).1

@[inline, reducible]
protected def range (spec : OracleSpec ι) (i : ι) : Type w := (spec i).2

Decidable in Init.Prelude

@[simp]
def extract (z : Zipper α) : α := z.focus

BitVec.ofFin in Init.Prelude

def extract (t : CofreeC F α) : α :=
  head t

def LWE_Search_Experiment (adv : LWE_Search_Adversary n m p) : ProbComp Bool := do
  let A ←$ᵗ Matrix (Fin n) (Fin m) (Fin p)
  let s ←$ᵗ Vector (Fin p) n
  
  let e ← (Vector.range m).mapM (fun _ ↦ errSamp)
  let u := A.vecMul s.get + e.get
  let s' ← adv (A, Vector.ofFn u)
  return s' = s

noncomputable def ProbComp.advantage₂ (p q : ProbComp Unit) : ℝ :=
  |([= () | p]).toReal - ([= () | q]).toReal|

monadMap_comp {α : Type u} (f : {β : Type u} → m β → m β) (g : {γ : Type u} → m γ → m γ) :
    (@MonadFunctor.monadMap m n _ α f) ∘ (@MonadFunctor.monadMap m n _ α g) =
      @MonadFunctor.monadMap m n _ α (f ∘ g)

def rangeFintype [spec.FiniteRange] : OracleQuery spec α → Fintype α
  | query i t => inferInstance

Option.elimM in Init.Data.Option.Basic

instance : Coapplicative Zipper where
  coseq := coseq

Eq in Init.Prelude

Sum.elim in Init.Data.Sum.Basic

structure RelativeMonad where
  T : C → D
  η : {A : C} → (J.obj A ⟶[ Bundled c ] T A)
  μ : {A B : C} → (J.obj A ⟶[ Bundled c ] T B) ⟶ (T A ⟶[ Bundled c ] T B)

bind_assocᵣ {α β γ : Type u} (x : m α) (f : j α → m β) (g : j β → m γ) :
    x >>=ᵣ f >>=ᵣ g = x >>=ᵣ fun x ↦ f x >>=ᵣ g

instance : Coe (NatEquiv m n) (NatHom m n) where
  coe f := f.toNatHom

instance : Coapplicative Stream' where

instance subSpec_assoc : spec₁ ++ₒ (spec₂ ++ₒ spec₃) ⊂ₒ spec₁ ++ₒ spec₂ ++ₒ spec₃ where
  monadLift
    | query (inl i) t => query (inl (inl i)) t
    | query (inr (inl i)) t => query (inl (inr i)) t
    | query (inr (inr i)) t => query (inr i) t

def index : (q : OracleQuery spec α) → ι | query i t => i

Summable in Mathlib.Topology.Algebra.InfiniteSum.Defs

instance {m n} [Monad m] [OrderedMonad n] [MonadLiftT m n] [LawfulMonad m] [LawfulMonad n]
    [LawfulMonadLiftT m n] : LawfulMonadRelation m n where
  monadRel_pure := by admit /- proof elided -/

def withCounting (so : QueryImpl spec m) : QueryImpl spec (WriterT spec.QueryCount m) where
  impl | q => tell (QueryCount.single q.index) *> ↑(so.impl q)

@[reducible, inline] def uniformFin (n : ℕ) : ProbComp (Fin (n + 1)) :=
  unifSpec.query n ()

@[inline, reducible]
def rename (spec : OracleSpec ι) (f : τ → ι) : OracleSpec τ := spec ∘ f

@[ext]
structure Equiv (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) where
  toLens : Lens P Q
  invLens : Lens Q P
  left_inv : comp invLens toLens = Lens.id P := by admit /- proof elided -/

Or.inr in Init.Prelude

Function.update in Mathlib.Logic.Function.Basic

MonadStateOf.get in Init.Prelude

def IND_CPA_experiment {encAlg : AsymmEncAlg ProbComp M PK SK C}
    (adversary : encAlg.IND_CPA_adversary) : ProbComp Unit := do
  let b ← $ᵗ Bool
  let (pk, _sk) ← encAlg.keygen
  let b' ← (simulateQ (encAlg.IND_CPA_queryImpl' pk b) (adversary pk)).run' ∅
  guard (b = b')

OptionT.run in Init.Control.Option

@[reducible] def monadLE {m} [OrderedMonad m] : {α : Type u} → m α → m α → Prop :=
  monadOrder.le

associator in Mathlib.Algebra.Ring.Associator

instance {P} {a : (P ⊗ 1).A} : IsEmpty ((P ⊗ 1).B a) :=

def IND_CCA_oracleImpl [DecidableEq C] (encAlg : AsymmEncAlg m M PK SK C)
    (pk : PK) (sk : SK) (b : Bool) : QueryImpl (IND_CCA_oracleSpec encAlg)
      (StateT (Option C) m) where impl
  | query (Sum.inl ()) c => do
      guard ((← get) ≠ some c)
      return encAlg.decrypt sk c
  | query (Sum.inr ()) (m₁, m₂) => do
      guard (← get).isNone
      let c ← encAlg.encrypt pk (if b then m₁ else m₂)
      set (some c)
      return c

class OrderedMonadAlgebra (m : Type u → Type v) [OrderedMonad m] [MonadAlgebra m] where
  [carrierOrder {α : Type u} : Preorder α]
  monadAlg_mono {α β : Type u} {f f' : α → β} {ma ma' : m α} (hf : ∀ a, (f a) ≤ (f' a))
    (hm : ma ≤ₘ ma') : (monadAlg (f <$> ma)) ≤ (monadAlg (f' <$> ma'))

def symm {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (E : P ≃ₚ Q) : Q ≃ₚ P where
  equivA := E.equivA.symm
  equivB := fun a =>
    (Equiv.cast (congrArg Q.B ((Equiv.symm_apply_eq E.equivA).mp rfl))).trans
      (E.equivB (E.equivA.symm a)).symm

@[inline, reducible] def randomOracle [(i : ι) → SelectableType (spec.range i)] :
    QueryImpl spec (StateT spec.QueryCache (OracleComp unifSpec)) :=
  unifOracle.withCaching

instance : Coapplicative NonEmptyList where

@[always_inline, inline]
def lift (x : P.Obj α) : FreeM P α := FreeM.roll x.1 (fun y ↦ FreeM.pure (x.2 y))

StateT in Init.Control.State

instance {Q : PostCondition σ α} {x : α} :
    Inhabited (WeakestPrecondition (pure x : StateM σ α) Q) where
  default := ⟨fun s => Q s x s, HoareTriple.pure_rule_backward x, fun _ hP' => hP'⟩

Array.mapM' in Init.Data.Array.BasicAux

instance {P : PreCondition σ} {s' : σ} :
  StrongestPostcondition P (set s' : StateM σ Unit) := default

Set.image2 in Mathlib.Data.Set.Operations

let invalid_abuse_report := {
      message := {
        content := manipulated_message,
        nonce := data.verified_msg.nonce },
      franking_tag := data.message_package.franking_tag,
      reporting_tag := data.message_package.reporting_tag,
      context := data.message_package.context }
    let is_invalid := validate_abuse_report invalid_abuse_report data.facebook_key
    IO.println s!"false abuse report validation result: {is_invalid}"

instance : Functor Stream' where
  map := Stream'.map

@[ext]
structure QueryImpl {ι : Type w} (spec : OracleSpec ι) (m : Type u → Type v) where
  impl {α : Type u} (q : OracleQuery spec α) : m α

instance {n : Type u → Type v} [MonadLiftT m n] : MonadLiftT (FreeContT f m) (FreeContT f n) where
  monadLift := fun x => fun handleEff handlePure => by admit /- proof elided -/

instance : Coe (PureEquiv m n) (NatEquiv m n) where
  coe f := f.toNatEquiv

def main : IO Unit := do
  IO.println <| "Thanks for running me!"
  IO.println <| "Running an external addition of `1 + 1`:"
  IO.println <| myAdd 1 1
  IO.println <| "
  let trials : ℕ ← (100 + ·) <$> $[0..100]
  let die : ℕ ← (4 + ·) <$> $[0..4]
  lawLargeNumsTest trials die

OptionT.mk in Init.Control.Option

instDecidableAnd in Init.Prelude

class SelectableType (β : Type) where
  selectElem : ProbComp β
  mem_support_selectElem (x : β) : x ∈ selectElem.support
  probOutput_selectElem_eq (x y : β) : [= x | selectElem] = [= y | selectElem]
  probFailure_selectElem : [⊥ | selectElem] = 0

def prodCoprodDistrib :
    Lens.Equiv.{max uA₁ uA₂ uA₃, max uB₁ uB₂, max uA₁ uA₂ uA₃, max uB₁ uB₂}
      (P * (Q + R)) ((P * Q) + (P * R)) where
  toLens := (fun ⟨p, qr⟩ => match qr with
              | Sum.inl q => Sum.inl (p, q)
              | Sum.inr r => Sum.inr (p, r)) ⇆
            (fun ⟨_, qr⟩ => match qr with
              | Sum.inl _ => id 
              | Sum.inr _ => id) 
  invLens := (Sum.elim
              (fun ⟨p, q⟩ => (p, Sum.inl q))
              (fun ⟨p, r⟩ => (p, Sum.inr r))) ⇆
             (fun pq_pr => match pq_pr with
              | Sum.inl _ => id 
              | Sum.inr _ => id) 
  left_inv := by admit /- proof elided -/

noncomputable def LHL_Consequence_Advantage (adv : LHL_Consequence_Adv n p) : ℝ :=
  (LHL_Consequence_Game_0 (m := m) adv).advantage₂' (LHL_Consequence_Game_1 adv)

@[elab_as_elim]
protected def inductionOn {C : FreeM P α → Prop}
    (pure : ∀ x, C (pure x))
    (roll : (x : P.A) → (r : P.B x → FreeM P α) → (∀ y, C (r y)) → C (FreeM.roll x r)) :
    (oa : FreeM P α) → C oa
  | FreeM.pure x => pure x
  | FreeM.roll x r => roll x _ (λ u ↦ FreeM.inductionOn pure roll (r u))

instance : Monad MonoContProp := inferInstanceAs (Monad (MonoCont Prop))

DFunLike in Mathlib.Data.FunLike.Basic

def oneProd :
    Lens.Equiv.{max uA₁ uA₂, max uB₁ uB₂, uA₁, uB₁} ((1 : PFunctor.{uA₂, uB₂}) * P) P where
  toLens := Prod.snd ⇆ (fun _ => Sum.inr)
  invLens := (fun p => (PUnit.unit, p)) ⇆ (fun _ => Sum.elim PEmpty.elim id)
  left_inv := by admit /- proof elided -/

ExceptT.mk in Init.Control.Except

Matrix.vecMul in Mathlib.Data.Matrix.Mul

LE in Init.Prelude

structure Day (f : Type u₁ → Type v₁) (g : Type u₂ → Type v₂) (a : Type u₃) where
   
  {α : Type u₁}
   
  {β : Type u₂}
   
  map' : α → β → a
   
  fa : f α
   
  gb : g β

instance : Extract Stream' where
  extract := Stream'.head

instance {T U : Type v} [Inhabited U] [Fintype U] : (T →ₒ U).FiniteRange where
  range_inhabited' := inferInstance
  range_fintype' := inferInstance

structure MonadEquiv (m : Type u → Type v) [Pure m] [Bind m] (n : Type u → Type w) [Pure n] [Bind n]
    extends NatEquiv m n, PureEquiv m n, BindEquiv m n

instance (m : Type u → Type v) [Pure m] [Bind m]
    (n : Type u → Type w) [Pure n] [Bind n] (F : m →ᵐ n) :
    IsMonadHom m n F.toFun where
  map_pure := F.toFun_pure'
  map_bind := F.toFun_bind'

instance : MonadFunctor f (FreeMonad f) where
  monadMap g
    | FreeMonad.pure x => FreeMonad.pure x
    | FreeMonad.roll x r => g x >>= r

def regevAsymmEnc (n m p : ℕ) [hp2 : p.AtLeastTwo] (errSampKG : ProbComp (Fin p)) :
    AsymmEncAlg ProbComp (M := Bool) (PK := Matrix (Fin n) (Fin m) (Fin p) × Vector (Fin p) m)
     (SK := Vector (Fin p) n) (C := Vector (Fin p) n × Fin p) where
  keygen := do
    let A ←$ᵗ Matrix (Fin n) (Fin m) (Fin p)
    let s ←$ᵗ Vector (Fin p) n
    let e ← (Vector.range m).mapM (fun _ ↦ errSampKG)
    return ((A, Vector.ofFn (Matrix.vecMul s.get A) + e), s)
  encrypt := λ (A, y) msg ↦ do
    let r2 ←$ᵗ Vector (Fin 2) m
    let r := (r2.map (Fin.castLE hp2.one_lt)).get
    let yr := dotProduct y.get r
    let signal := if msg then 0 else p / 2
    return (Vector.ofFn (Matrix.mulVec A r), yr + (Fin.ofNat p signal))
  decrypt := λ s (a, b) ↦ do
    let sa := dotProduct s.get a.get
    let val := Fin.val (sa - b)
    return if val < p/4 then true else val > 3*p/4
  __ := ExecutionMethod.default

def IND_CPA_adversary (encAlg : AsymmEncAlg ProbComp M PK SK C) :=
  PK → OracleComp encAlg.IND_CPA_oracleSpec Bool

def FiatShamir (sigmaAlg : SigmaAlg X W PC SC Ω P p)
    (hr : GenerableRelation X W p) (M : Type) [DecidableEq M] :
    SignatureAlg (OracleComp (unifSpec ++ₒ (M × PC →ₒ Ω)))
      (M := M) (PK := X) (SK := W) (S := PC × P) where
  keygen := hr.gen
  sign := fun pk sk m => do
    let (c, e) ← sigmaAlg.commit pk sk
    let r ← query (spec := (M × PC →ₒ Ω)) () (m, c)
    let s ← sigmaAlg.respond pk sk e r
    return (c, s)
  verify := fun pk m (c, s) => do
    let r' ← query (spec := (M × PC →ₒ Ω)) () (m, c)
    return sigmaAlg.verify pk c r' s
  exec comp :=
    let so : QueryImpl (unifSpec ++ₒ (M × PC →ₒ Ω))
      (StateT ((M × PC →ₒ Ω).QueryCache) ProbComp) :=
      idOracle ++ₛₒ randomOracle
    StateT.run' (simulateQ so comp) ∅
  lift_probComp := monadLift
  exec_lift_probComp c := by admit /- proof elided -/

instance instIsEmptySigma {α : Sort u} {β : α → Sort v} [inst : IsEmpty α] :
    IsEmpty ((a : α) ×' β a) where
  false := fun a => inst.elim a.1

def tails : NonEmptyList α → NonEmptyList (NonEmptyList α)
  | nel@⟨_, t⟩ =>
    
    let head_tail : NonEmptyList α := nel
    
    let rest_tails_list : List (NonEmptyList α) :=
      List.filterMap NonEmptyList.fromList? (List.tails t)
    ⟨head_tail, rest_tails_list⟩

instance {m n} [MonadFunctor m n] : MonadFunctorT m n := inferInstance

instance : IsEmpty (A 0) := inferInstanceAs (IsEmpty PEmpty)

instance [RelativeBind Id m] : Bind m where
  bind := @bindᵣ Id m _

def linear (A : Type uA) : PFunctor.{uA, uB} :=
  A X^ PUnit

def IND_CCA_oracleSpec (_encAlg : AsymmEncAlg m M PK SK C) :=
    (C →ₒ Option M) ++ₒ ((M × M) →ₒ C)

@[simp]
noncomputable def depthBindAux {f : Type u → Type v} {α β : Type u} :
    FreeMonad f α → (α → FreeMonad f β) → ℕ∞
  | .pure x, g => depth (g x)
  | .roll _ r, g => 1 + iSup (λ u ↦ depthBindAux (r u) g)

class AssertAssume (α : Type u) [Preorder α] where
  assert : Prop → α → α
  assume : Prop → α → α
  assert_strengthen : ∀ p x, assert p x ≤ x
  assume_weaken : ∀ p x, x ≤ assume p x
  assert_assume_iff : ∀ p x y, assert p x ≤ y ↔ x ≤ assume p y

instance instOfMonadRelation {m n} [Monad m] [Monad n] [MonadRelation m n]
    [LawfulMonadRelation m n] : DijkstraMonad n (fun na => { ma : m _ // monadRel ma na}) where
  dPure x := ⟨pure x, monadRel_pure x⟩
  dBind x f := ⟨x.1 >>= (fun a => (f a).1), monadRel_bind x.2 (fun a => (f a).2)⟩

instance {P : PreCondition σ} {comp : StateM σ α} :
    Subsingleton (StrongestPostcondition P comp) :=

def LHL_Consequence_Adv (n p : ℕ) := (Vector (Fin p) n) × (Fin p) → ProbComp Bool

Set.fintypeiUnion in Mathlib.Data.Set.Finite.Lattice

def trans (e₁ : NatEquiv m n) (e₂ : NatEquiv n p) : NatEquiv m p where
  toFun := e₂.toFun ∘ e₁.toFun
  invFun := e₁.invFun ∘ e₂.invFun
  left_inv := by admit /- proof elided -/

CategoryTheory.EnrichedFunctor.obj in Mathlib.CategoryTheory.Enriched.Basic

def enclose (P : PFunctor.{uA, uB}) : Type max uA uA₁ uB uB₁ :=
  Lens P X.{uA₁, uB₁}

instance [RelativeFunctor Id f] [LawfulRelativeFunctor Id f] : LawfulFunctor f where
  map_const := @map_constᵣ Id f _ _
  id_map := @id_mapᵣ Id f _ _
  comp_map := @comp_mapᵣ Id f _ _

instance instLawfulMonad : LawfulMonad (FreeContT f m) := LawfulMonad.mk'
  (id_map := by admit /- proof elided -/
  )
  (pure_bind := by admit /- proof elided -/
  )
  (bind_assoc := by admit /- proof elided -/
  )

@[always_inline, inline]
protected def bind : FreeMonad f α → (α → FreeMonad f β) → FreeMonad f β
  | FreeMonad.pure x, g => g x
  | FreeMonad.roll x r, g => FreeMonad.roll x (λ u ↦ FreeMonad.bind (r u) g)

instance {a} : Unique (B X a) := inferInstanceAs (Unique PUnit)

Alternative in Init.Control.Basic

def validate_abuse_report (report : AbuseReport) (facebook_key : BitVec 256) : Bool :=
  let (msg_bv, _) := serialize_message_data report.message.content report.message.nonce
  let computed_tf := mock_hmac_sha256 report.message.nonce msg_bv
  let context_bv := BitVec.ofNat 256 report.context.timestamp
  let serialized := report.franking_tag.tag.append (bitvec_to_string context_bv)
  let computed_rf := mock_hmac_sha256 facebook_key (string_to_bitvec serialized)
  (computed_tf = report.franking_tag.tag) && (computed_rf = report.reporting_tag.tag)

class LawfulMonadControl (m : semiOutParam (Type u → Type v)) (n : Type u → Type w)
    [Monad m] [Monad n] [MonadControl m n] : Prop where

LawfulMonad in Init.Control.Lawful.Basic

instance : LawfulComonad (CofreeC F) := sorry

instance : Mul PFunctor.{uA, uB} where
  mul := prod

instance : Add PFunctor.{uA, uB} where
  add := sum

DecidablePred in Init.Prelude

impl in Mathlib.Deprecated.MLList.BestFirst

StateT.bind in Init.Control.State

List in Init.Prelude

instance : Unique (A X) := inferInstanceAs (Unique PUnit)

instance : DecidableEq mock_hmac_sha256_out_type :=
  fun x y => match String.decEq x y with
  | isTrue h => isTrue h
  | isFalse h => isFalse h

instance {β} : Unique (A (purePower β)) := inferInstanceAs (Unique PUnit)

@[ext]
protected structure Equiv (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) where
   
  equivA : P.A ≃ Q.A
   
  equivB : ∀ a, P.B a ≃ Q.B (equivA a)

instance instLawfulComonad [Comonad w] [LawfulComonad w] : LawfulComonad (StoreT s w) where
  map_eq_extend_extract := sorry 
  extend_extract := sorry 
  extract_extend := by admit /- proof elided -/

instMonadFunctorTOfMonadFunctor in Init.Prelude

isEmptyElim in Mathlib.Logic.IsEmpty

instance : AlternativeMonad (OracleComp spec) :=
  inferInstanceAs (AlternativeMonad (OptionT (FreeMonad (OracleQuery spec))))

instance {ρ} {m} [Monad m] [Commutative m] : Commutative (ReaderT ρ m) where
  bind_comm := fun ma mb => by admit /- proof elided -/

def uliftUliftEquiv : P.ulift.ulift ≃ₚ P.ulift :=
  sorry

instance : Comonad Zipper where

noncomputable def LWE_Search_Advantage (adv : LWE_Search_Adversary n m p) : ℝ :=
  (LWE_Search_Experiment n m p errSamp adv).advantage'

def tensor (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) :
    PFunctor.{max uA₁ uA₂, max uB₁ uB₂} :=
  ⟨P.A × Q.A, fun ab => P.B ab.1 × Q.B ab.2⟩

@[inline, reducible] def cachingOracle :
    QueryImpl spec (StateT spec.QueryCache (OracleComp spec)) :=
  idOracle.withCaching

def test_abuse_report_validation : IO Unit := do
  let message_content := "Hello world"
  let manipulated_message := "Hell world"
  let maybeData ← OracleComp.runIO (simulation_setup message_content)
  match maybeData with
  | none =>
    IO.println "setup failed"
  | some data =>
    let valid_abuse_report := {
      message := data.verified_msg,
      franking_tag := data.message_package.franking_tag,
      reporting_tag := data.message_package.reporting_tag,
      context := data.message_package.context }
    let is_valid := validate_abuse_report valid_abuse_report data.facebook_key
    IO.println s!"valid abuse report validation result: {is_valid}"

def parallelTestingAdversary (_G P : Type) := P → P → P → P → ProbComp Bool

List.finRange in Init.Data.List.FinRange

instance : MonadTransformer OptionT where
  mapMonad _ := inferInstance
  transform _ := inferInstance

instance : NatPow PFunctor.{max uA uB, uB} where
  pow := compNth

PFunctor.Obj in Mathlib.Data.PFunctor.Univariate.Basic

def PreCondition (σ : Type*) := σ → Prop

Finset.sum in Mathlib.Algebra.BigOperators.Group.Finset.Defs

def parallelizationExp [DecidableEq P]
    (adversary : parallelizationAdversary G P) : ProbComp Unit := do
  let x ←$ᵗ P; let g₁ ←$ᵗ G; let g₂ ←$ᵗ G
  let x₁ := g₁ +ᵥ x
  let x₂ := g₂ +ᵥ x
  let x₃ ← adversary x x₁ x₂
  guard (x₃ = g₁ +ᵥ g₂ +ᵥ x)

liftWith_bind {α β : Type u} (ma : m α) (f : α → m β) :
    liftWith (fun _ => ma) >>= liftWith ∘ (fun a _ => f a) = liftWith (n := n) (fun _ => ma >>= f)

List.mapM in Init.Data.List.Control

def single [DecidableEq ι] (i : ι) : QueryCount spec := Function.update 0 i 1

structure FrankingTag where
  tag : mock_hmac_sha256_out_type 
  deriving Repr

instance QueryImpl.Inhabited [∀ i, Inhabited (spec.range i)] [Pure m] :
  Inhabited (QueryImpl spec m) := ⟨{impl q := pure q.defaultOutput}⟩

def prodOne :
    Lens.Equiv.{max uA₁ uA₂, max uB₁ uB₂, uA₁, uB₁} (P * (1 : PFunctor.{uA₂, uB₂})) P where
  toLens := Prod.fst ⇆ (fun _ => Sum.inl)
  invLens := (fun p => (p, PUnit.unit)) ⇆ (fun _ => Sum.elim id PEmpty.elim)
  left_inv := by admit /- proof elided -/

def LWE_Experiment (adv : LWE_Adversary n m p) : ProbComp Bool := do
  let b ←$ᵗ Bool
  let distr ← if b then LWE_Distr n m p errSamp else LWE_Uniform_Distr n m p
  let b' ← adv distr
  return b' = b

HMul in Init.Prelude

def invTildeR {P : PFunctor.{uA, uB}} : Lens (P ◃ X) P :=
  (fun a => a.1) ⇆ (fun _ b => ⟨b, PUnit.unit⟩)

def ofLift (m : Type u → Type v) (n : Type u → Type v) [Monad m] [Monad n]
    [MonadLift m n] [LawfulMonadLift m n] : m →ᵐ n where
  toFun := liftM
  toFun_pure' := liftM_pure
  toFun_bind' := liftM_bind

instance (i : PEmpty) : Unique ([]ₒ.domain i) := PUnit.instUnique

def LHL_Consequence_Game_0 (adv : LHL_Consequence_Adv n p) : ProbComp Bool := do
  let A ←$ᵗ Matrix (Fin n) (Fin m) (Fin p)
  let u ←$ᵗ Vector (Fin p) m
  let r2 ←$ᵗ Vector (Fin 2) m
  let r := (r2.map (Fin.castLE hp2.one_lt)).get
  adv (Vector.ofFn (Matrix.mulVec A r), dotProduct u.get r)

def zeroTensor : 0 ⊗ P ≃ₗ 0 where
  toLens := (fun a => PEmpty.elim a.1) ⇆ (fun _ b => PEmpty.elim b)
  invLens := PEmpty.elim ⇆ (fun a _ => PEmpty.elim a)
  left_inv := by admit /- proof elided -/

def dIte {w d} [Monad w] [DijkstraMonad w d] {α} (c : Prop) [Decidable c] {t e : w α} :
    d t → d e → d (ite c t e) :=
  fun dt de => dDite c (fun _ => dt) (fun _ => de)

def xTensor : X ⊗ P ≃ₗ P where
  toLens := Prod.snd ⇆ (fun _ b => (PUnit.unit, b))
  invLens := (fun p => (PUnit.unit, p)) ⇆ (fun _ bp => bp.2)
  left_inv := rfl
  right_inv := rfl

instance range_inhabited {i : ι} [h : FiniteRange spec] :
    Inhabited (spec.range i) := h.range_inhabited' i

structure NonEmptyList (α : Type u) where
  head : α
  tail : List α

inductive FreeM (f : Type v → Type w) (α : Type u) where
  | pure (a : α) : FreeM f α
  | roll {β : Type v} (x : f β) (k : β → FreeM f α) : FreeM f α

instance : LawfulMonad (OracleComp spec) :=
  inferInstanceAs (LawfulMonad (OptionT (FreeMonad (OracleQuery spec))))

List.Vector.cons in Mathlib.Data.Vector.Defs

CategoryTheory.NatTrans in Mathlib.CategoryTheory.NatTrans

instance : LawfulCoapplicative NonEmptyList where
  coseqLeft_eq := by admit /- proof elided -/

def generateSeedT (spec : OracleSpec ι) [∀ i, SelectableType (spec.range i)]
    (qc : ι → ℕ) (activeOracles : List ι) :
    StateT (QuerySeed spec) ProbComp Unit :=
  for j in activeOracles do
    modify (QuerySeed.addValues (← ($ᵗ spec.range j).replicate (qc j)))

@[always_inline, inline, simp]
abbrev MonadTransformer.liftOf [MonadTransformer t] (m) [Monad m] : m α → t m α :=
  (transform m).monadLift

Vector.map in Init.Data.Vector.Basic

Fin in Init.Prelude

instance : Extend Id where
  extend wx f := f wx

Turing.TM2ComputableInPolyTime in Mathlib.Computability.TMComputable

instance : LawfulComonad NonEmptyList where
  map_eq_extend_extract := sorry 
  extend_extract := sorry 
  extract_extend := sorry 
  extend_assoc := sorry

def invTildeL {P : PFunctor.{uA, uB}} : Lens (X ◃ P) P :=
  (fun ⟨_, f⟩ => f PUnit.unit) ⇆ (fun _ b => ⟨PUnit.unit, b⟩)

instance (n : ℕ) : SelectableType (Fin (n + 1)) where
  selectElem := $[0..n]
  mem_support_selectElem := by admit /- proof elided -/

getThe in Init.Prelude

ContT in Mathlib.Control.Monad.Cont

instance : MonoidalCategory (Preord) where
  tensorObj X Y := ⟨X.carrier × Y.carrier⟩
  whiskerLeft X Y := fun f => ofHom ⟨fun x => (x.1, f.1 x.2),
      (by admit /- proof elided -/
      )⟩
  whiskerRight f Y := ofHom ⟨fun y => (f.hom y.1, y.2),
      (by admit /- proof elided -/
      )⟩
  tensorUnit := ⟨PUnit⟩
  associator X Y Z := {
    hom := ofHom ⟨fun ⟨⟨x, y⟩, z⟩ => ⟨x, ⟨y, z⟩⟩, by admit /- proof elided -/
      ⟩
    inv := ofHom ⟨fun ⟨x, ⟨y, z⟩⟩ => ⟨⟨x, y⟩, z⟩, by admit /- proof elided -/
      ⟩ }
  leftUnitor X := {
    hom := ofHom ⟨Prod.snd, (by admit /- proof elided -/
    )⟩
    inv := ofHom ⟨fun x => (PUnit.unit, x), by admit /- proof elided -/
    ⟩ }
  rightUnitor X := {
    hom := ofHom ⟨Prod.fst, (by admit /- proof elided -/
    )⟩
    inv := ofHom ⟨fun x => (x, PUnit.unit), by admit /- proof elided -/
    ⟩ }
  tensorHom_def f g := rfl
  
  tensor_comp f₁ f₂ g₁ g₂ := rfl
  whiskerLeft_id _ _ := rfl
  id_whiskerRight _ _ := rfl
  associator_naturality f₁ f₂ f₃ := rfl
  leftUnitor_naturality f := rfl
  rightUnitor_naturality f := rfl
  pentagon _ _ _ _ := rfl
  triangle _ _ := rfl

instance support_finite [spec.FiniteRange] (oa : OracleComp spec α) :
    Finite ↥(oa.support) := supportWhen_finite _ oa

def IND_CPA_queryImpl' (encAlg : AsymmEncAlg ProbComp M PK SK C)
    (pk : PK) (b : Bool) : QueryImpl encAlg.IND_CPA_oracleSpec
      (StateT (M × M →ₒ C).QueryCache ProbComp) :=
  have so : QueryImpl (M × M →ₒ C) ProbComp := ⟨fun (query () (m₁, m₂)) =>
    encAlg.encrypt pk (if b then m₁ else m₂)⟩
  idOracle ++ₛₒ so.withCaching

def prodPair {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}}
    (l₁ : Lens P Q) (l₂ : Lens P R) :
    Lens.{uA₁, uB₁, max uA₂ uA₃, max uB₂ uB₃} P (Q * R) :=
  (fun p => (l₁.toFunA p, l₂.toFunA p)) ⇆
    (fun p => Sum.elim (l₁.toFunB p) (l₂.toFunB p))

HEq in Init.Prelude

def activeOracles [spec.FiniteRange] [DecidableEq ι] (oa : OracleComp spec α) : Finset ι :=

Equiv.prodPUnit in Mathlib.Logic.Equiv.Prod

noncomputable def ProbComp.advantage' (p : ProbComp Bool) : ℝ :=
  |([= true | p]).toReal - ([= false | p]).toReal|

deriving Repr, DecidableEq

class WeakestPrecondition (comp : StateM σ α) (Q : PostCondition σ α) where
  P : PreCondition σ
  hP : HoareTriple P comp Q
  hWeak : ∀ P', HoareTriple P' comp Q → P ≤ P'

def simulateQ [AlternativeMonad m] (so : QueryImpl spec m) (oa : OracleComp spec α) : m α :=
  do Option.getM (← FreeMonad.mapM oa.run so.impl)

def symm (e : NatEquiv m n) : NatEquiv n m where
  toFun := e.invFun
  invFun := e.toFun
  left_inv := e.right_inv
  right_inv := e.left_inv

monadFunctorRefl in Init.Prelude

semiOutParam in Init.Prelude

Array.foldrM in Init.Data.Array.Basic
</all_available_defs>

<all_available_lemmas>
lemma tsum_option {α β : Type*} [AddCommMonoid α] [TopologicalSpace α]
    [ContinuousAdd α] [T2Space α]
    (f : Option β → α) (hf : Summable (Function.update f none 0)) :
    ∑' x : Option β, f x = f none + ∑' x : β, f (some x)

@[simp]
theorem sumMap_comp_inr (l₁ : Lens P R) (l₂ : Lens Q W) :
    ((l₁ ⊎ₗ l₂) ∘ₗ Lens.inr) = (Lens.inr ∘ₗ l₂)

lemma countQ_singleton_self (i : ι) (t : spec.domain i) (u : spec.range i) :
    countQ (singleton (query i t) u) i = 1

@[simp]
lemma mapM_map' {m : Type v → Type w} [AlternativeMonad m] [LawfulAlternative m]
    [LawfulMonad m] (qm : {α : Type v} → OracleQuery spec α → m α)
    (oa : OracleComp spec α) (f : α → β) :
    (f <$> oa).mapM failure qm = f <$> oa.mapM failure qm

lemma neverFails_eq_oracleComp_construct (oa : OracleComp spec α) :
    oa.neverFails = OracleComp.construct
      (fun _ ↦ True) (fun {β} _ _ r ↦ ∀ (x : β), r x) False oa

@[simp]
lemma construct_query (q : OracleQuery spec α) :
    (OracleComp.construct h_pure h_query_bind h_failure (q : OracleComp spec α) : C q) =
      h_query_bind q pure h_pure

lemma probOutput_seq_map_eq_tsum [spec.FiniteRange]
    (z : γ) : [= z | f <$> oa <*> ob] = ∑' (x : α) (y : β),
      [= x | oa] * [= y | ob] * [= z | (pure (f x y) : OracleComp spec γ)]

@[simp] lemma run_none_ne_top (p : SPMF α) : p.run none ≠ ⊤

theorem comp_assoc {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}}
    {S : PFunctor.{uA₄, uB₄}} (l : Lens R S) (l' : Lens Q R) (l'' : Lens P Q) :
    (l ∘ₗ l') ∘ₗ l'' = l ∘ₗ (l' ∘ₗ l'')

lemma probEvent_eq_tsum_subtype_support_ite [DecidablePred p] :
    [p | oa] = ∑' x : oa.support, if p x then [= x | oa] else 0

@[simp] lemma isPure_query_bind : isPure ((q : OracleComp spec β) >>= oa) = false

@[simp] lemma probFailure_add_tsum_probOutput (oa : m α) :
    Pr[⊥ | oa] + ∑' x, Pr[= x | oa] = 1

@[simp] lemma probEvent_eq_eq_probOutput' (oa : OracleComp spec α) (x : α) :
    [(x = ·) | oa] = [= x | oa]

@[simp]
lemma probOutput_seq_map_swap [spec.FiniteRange] (z : γ) :
    [= z | Function.swap f <$> ob <*> oa] = [= z | f <$> oa <*> ob]

@[simp]
lemma depth_pure' {x : α} : depth (FreeMonad.pure x : FreeMonad f α) = 0

@[simp] lemma evalDist_eq : evalDist p = liftM p

theorem Correct [DecidableEq P] : (elgamalAsymmEnc G P).PerfectlyCorrect

lemma mapM_seq [LawfulMonad m] (og : OracleComp spec (α → β)) (oa : OracleComp spec α)
    (hfail : ∀ f : (α → β) → m β, fail >>= f = fail)
    (hfail' : ∀ f : α → β, f <$> fail = fail) :
    (og <*> oa).mapM fail qm = og.mapM fail qm <*> oa.mapM fail qm

theorem compMap_comp
    {P' : PFunctor.{uA₄, uB₄}} {Q' : PFunctor.{uA₅, uB₅}} {R' : PFunctor.{uA₆, uB₆}}
    (l₁ : Lens P P') (l₂ : Lens Q Q') (l₁' : Lens P' R) (l₂' : Lens Q' R') :
    (l₁' ∘ₗ l₁) ◃ₗ (l₂' ∘ₗ l₂) = (l₁' ◃ₗ l₂') ∘ₗ (l₁ ◃ₗ l₂)

@[simp] lemma monoid_one_def :
    (@OfNat.ofNat (QueryCount spec) 1 (@One.toOfNat1 _ (Monoid.toOne))) = (0 : ι → ℕ)

lemma probOutput_seq_map_eq_tsum_ite [spec.FiniteRange] [DecidableEq γ]
    (z : γ) : [= z | f <$> oa <*> ob] =
      ∑' (x : α) (y : β), if z = f x y then [= x | oa] * [= y | ob] else 0

@[simp]
lemma evalDist_ite (p : Prop) [Decidable p] (oa oa' : OracleComp spec α) :
    evalDist (if p then oa else oa') = if p then evalDist oa else evalDist oa'

@[simp] lemma simulateQ_seq (og : OracleComp spec (α → β)) (oa : OracleComp spec α) :
    simulateQ so (og <*> oa) = simulateQ so og <*> simulateQ so oa

@[simp] lemma withPregen_apply {α} (so : QueryImpl spec m) (q : OracleQuery spec α) :
    so.withPregen.impl q = match q with

@[simp]
lemma replicate_succ : replicate (n + 1) oa = List.cons <$> oa <*> replicate n oa

lemma liftM_query_eq_liftM_liftM {m : Type v → Type z} [MonadLift (OracleComp spec) m] {α : Type v}
    (q : OracleQuery spec α) : (liftM q : m α) = liftM (liftM q : OracleComp spec α)

@[simp] lemma not_one_lt_probFailure : ¬ 1 < Pr[⊥ | mx]

lemma probEvent_fst_eq_snd [spec.FiniteRange] [DecidableEq α] (oa : OracleComp spec (α × α)) :
    [λ z ↦ z.1 = z.2 | oa] = ∑' x : α, [= (x, x) | oa]

theorem exists_log_of_mem_support_fork (x₁ x₂ : α)
    (h : (x₁, x₂) ∈ (fork main qb js i cf).support) :
      ∃ s, cf x₁ = some s ∧ cf x₂ = some s ∧
      ∃ log₁ : QueryLog spec, ∃ hcf₁ : ↑s < log₁.countQ i,
      ∃ log₂ : QueryLog spec, ∃ hcf₁ : ↑s < log₂.countQ i,
      (log₁.getQ i)[s].1 = (log₂.getQ i)[s].1 ∧
      (log₁.getQ i)[s].2 ≠ (log₂.getQ i)[s].2 ∧
      (x₁, log₁) ∈ (simulateQ loggingOracle main).run.support ∧
      (x₂, log₂) ∈ (simulateQ loggingOracle main).run.support

@[simp] lemma support_eqRec (oa : OracleComp spec α) (h : α = β) :
    (h ▸ oa).support = h.symm ▸ oa.support

lemma simulateQ_eq [spec.FiniteRange] (oa : OracleComp spec α) :
    simulateQ defaultOracle oa = oa.defaultResult.getM

theorem RelativeFunctor.map_unitᵣ [RelativeMonad j m] [LawfulRelativeMonad j m] {a : m PUnit} :
    (fun y : j PUnit => y) <$>ᵣ a = a

lemma liftM_def [Monad m] (x : m α) : (liftM x : StateT σ m α) = StateT.lift x

lemma probOutput_bind_congr_add_le {γ₁ γ₂ : Type u}
    {oa : OracleComp spec α} {ob : α → OracleComp spec β}
      {oc₁ : α → OracleComp spec γ₁} {oc₂ : α → OracleComp spec γ₂}
    {y : β} {z₁ : γ₁} {z₂ : γ₂}
    (h : ∀ x ∈ oa.support, [= z₁ | oc₁ x] + [= z₂ | oc₂ x] ≤ [= y | ob x]) :
    [= z₁ | oa >>= oc₁] + [= z₂ | oa >>= oc₂] ≤ [= y | oa >>= ob]

@[simp] lemma pure_ne_failure : (pure x : OracleComp spec α) ≠ failure

@[simp]
lemma evalDist_seq_map_swap [spec.FiniteRange] :
    evalDist (Function.swap f <$> ob <*> oa) = evalDist (f <$> oa <*> ob)

@[simp]
lemma evalDist_orElse [h : spec.FiniteRange] (oa oa' : OracleComp spec α) :
    evalDist (oa <|> oa') = (evalDist oa <|> evalDist oa')

@[simp] lemma probOutput_uniformSelectList [DecidableEq α] (xs : List α) (x : α) :
    [= x | $ xs] = if xs.isEmpty then 0 else (xs.count x : ℝ≥0∞) / xs.length

@[simp]
lemma construct_roll (x : P.A) (r : P.B x → FreeM P α) :
    (FreeM.construct h_pure h_roll (FreeM.roll x r) : C (FreeM.roll x r)) =
      (h_roll x r (λ u ↦ FreeM.construct h_pure h_roll (r u)))

lemma probEvent_bind_eq_sum_finSupport [spec.DecidableEq] [DecidableEq α]
    (q : β → Prop) :
    [q | oa >>= ob] = ∑ x ∈ oa.finSupport, [= x | oa] * [q | ob x]

@[simp]
lemma Fin_Bound_add {n b₁ b₂ : ℕ} {x y : Fin n} (h₁ : Fin_Bound x b₁)
 (h₂ : Fin_Bound y b₂) : Fin_Bound (x + y) (b₁ + b₂)

lemma probOutput_pure_eq_zero {x y : α} (h : y ≠ x) :
    [= y | (pure x : OracleComp spec α)] = 0

lemma abs_mul_of_nonneg (h : 0 ≤ b) : |a

lemma support_replicate' [spec.FiniteRange] [DecidableEq α] (oa : OracleComp spec α) (n : ℕ) :
    (oa.replicate n).support = {xs | xs.length = n ∧ xs.all (· ∈ oa.support)}

theorem map_eq_pure_bindᵣ [RelativeMonad j m] [LawfulRelativeMonad j m]
    (f : j α → j β) (x : m α) : f <$>ᵣ x = x >>=ᵣ fun a => pureᵣ (f a)

@[simp]
lemma probEvent_liftComp [spec.FiniteRange] [superSpec.FiniteRange]
    (oa : OracleComp spec α) (p : α → Prop) [DecidablePred p] :
    [p | liftComp oa superSpec] = [p | oa]

theorem prodMap_comp_prodPair (l₁ : Lens Q W) (l₂ : Lens R X) (f : Lens P Q) (g : Lens P R) :
    (l₁ ×ₗ l₂) ∘ₗ Lens.prodPair f g = Lens.prodPair (l₁ ∘ₗ f) (l₂ ∘ₗ g)

@[simp]
lemma liftM_of_liftM_eq [MonadLift m m'] (x : StateT σ m α) :
    (liftM x : StateT σ m' α) = StateT.mk fun s => liftM (x.run s)

List.isEmpty_iff in Init.Data.List.Lemmas

@[simp]
lemma construct_pure (x : α) :
    OracleComp.construct h_pure h_query_bind h_failure (pure x) = h_pure x

@[simp]
lemma fst_map_run_simulateQ (oa : OracleComp spec α) :
    Prod.fst <$> (simulateQ countingOracle oa).run = oa

@[simp]
lemma construct_query_bind (q : OracleQuery spec β) (oa : β → OracleComp spec α) :
    (OracleComp.construct h_pure h_query_bind h_failure ((q : OracleComp spec β) >>= oa)) =
      h_query_bind q oa (λ u ↦ (oa u).construct h_pure h_query_bind h_failure)

lemma probOutput_prod_mk_apply_seq_map_eq_mul' [spec.FiniteRange] (oa : OracleComp spec α)
    (ob : OracleComp spec β)
    (f : α → γ) (g : β → δ) (x : γ) (y : δ) :
    [= (x, y) | (f ·, g ·) <$> oa <*> ob] = [= x | f <$> oa] * [= y | g <$> ob]

lemma mem_support_of_mem_finSupport {x : α} (hx : x ∈ oa.finSupport) : x ∈ oa.support

lemma apply'_none_eq_run (p : SPMF α) :
    let p' : PMF (Option α)

@[simp]
theorem compMap_id :
    (Lens.id P) ◃ₗ (Lens.id Q) = Lens.id (P ◃ Q)

@[simp]
lemma probOutput_pure [DecidableEq α] (y : α) :
    [= y | (pure x : OracleComp spec α)] = if y = x then 1 else 0

theorem strengthen_rule {P : PreCondition σ} {Q : PostCondition σ α}
    {comp : StateM σ α} (h : HoareTriple P comp Q) (Q' : PostCondition σ α)
    (h_imp : ∀ s x s', Q s x s' → Q' s x s') :
      HoareTriple P comp Q'

@[simp] lemma support_map (oa : OracleComp spec α) (f : α → β) :
    (f <$> oa).support = f '' oa.support

@[simp]
lemma bind_lift (x : P.Obj α) (r : α → FreeM P β) :
    FreeM.bind (FreeM.lift x) r = FreeM.roll x.1 (fun a ↦ r (x.2 a))

@[simp]
lemma run_simulateQ_bind_fst (oa : OracleComp spec α) (ob : α → OracleComp spec β) :
    ((simulateQ loggingOracle oa).run >>= fun x => ob x.1) = oa >>= ob

lemma subset_finSupport_iff_coe_subset_support : s ⊆ oa.finSupport ↔ ↑s ⊆ oa.support

@[simp]
lemma bind_pure (x : α) (r : α → FreeM P β) :
    FreeM.bind (FreeM.pure x) r = r x

lemma simulateQ_eq (oa : OracleComp spec α) : simulateQ idOracle oa = oa

@[simp]
lemma depth_roll {x : f α} {r : α → FreeMonad f β} :
    depth (roll x r : FreeMonad f β) = 1 + iSup (λ u ↦ depth (r u))

theorem PMF.bind_eq_zero {α β : Type _} {p : PMF α} {f : α → PMF β} {b : β} :
    (p >>= f) b = 0 ↔ ∀ a, p a = 0 ∨ f a b = 0

@[simp]
lemma isQueryBound_query_iff_pos [Nonempty α] (q : OracleQuery spec α) (qb : ι → ℕ) :
    IsQueryBound (q : OracleComp spec α) qb ↔ 0 < qb q.index

@[simp]
lemma PMF.monad_pure_eq_pure {α : Type u} (x : α) :
    (Pure.pure x : PMF α) = PMF.pure x

lemma support_evalDist : (evalDist oa).run.support = if [⊥ | oa] = 0 then
    some '' oa.support else insert none (some '' oa.support)

lemma probEvent_mono (h : ∀ x ∈ oa.support, p x → q x) : [p | oa] ≤ [q | oa]

lemma ProbComp.advantage_eq_half_of_sub (p : ProbComp Unit) :
    p.advantage = 2⁻¹ * |([⊥ | p]).toReal - ([= () | p]).toReal

lemma uniformSelectList_cons (x : α) (xs : List α) :
    ($ x :: xs : ProbComp α) = ((x :: xs)[·]) <$> $[0..xs.length]

lemma cons_mem_support_seq_map_cons_iff (x : α) (xs : List α) :
    x :: xs ∈ (cons <$> oa <*> ob).support ↔ x ∈ oa.support ∧ xs ∈ ob.support

lemma abs_mul_of_nonpos (h : b < 0) : |a

@[simp] lemma neverFails_array_mapM {f : α → OracleComp spec β} {as : Array α}
    (h : ∀ x ∈ as, neverFails (f x)) : neverFails (mapM f as)

@[simp]
lemma coe_finSupport [spec.FiniteRange] [DecidableEq α]
    (oa : OracleComp spec α) : ↑oa.finSupport = oa.support

lemma mem_finSupport_iff_of_evalDist_eq [spec.DecidableEq] [spec'.DecidableEq]
    [DecidableEq α] {oa : OracleComp spec α} {oa' : OracleComp spec' α}
    (h : evalDist oa = evalDist oa') (x : α) : x ∈ oa.finSupport ↔ x ∈ oa'.finSupport

lemma list_mapM_loop_eq {m : Type u → Type v} [Monad m] [LawfulMonad m]
    {α : Type w} {β : Type u} (xs : List α) (f : α → m β) (ys : List β) :
    List.mapM.loop f xs ys = (ys.reverse ++ ·) <$> List.mapM.loop f xs []

lemma Fin_bound_mul_helper {n b₁ b₂ : ℕ} {x y : Fin n} (h : b₁ * b₂ < n)
  (h₁ : x.val ≤ b₁) (h₂ : y.val + b₂ ≥ n) : Fin_Bound (x * y) (b₁ * b₂)

@[simp]
lemma zero_eq_probEvent_iff' [spec.DecidableEq] [DecidableEq α] :
    0 = [p | oa] ↔ ∀ x ∈ oa.finSupport, ¬ p x

@[simp]
lemma mapM_ite (p : Prop) [Decidable p] (oa oa' : OracleComp spec α) :
    (ite p oa oa').mapM fail qm = ite p (oa.mapM fail qm) (oa'.mapM fail qm)

@[simp] lemma X_B (a : X.A) : X.B a = PUnit

theorem monadLift_guard [AlternativeMonad m] [AlternativeMonad n] [MonadLift m n]
    [LawfulAlternativeLift m n] [LawfulMonadLift m n] (p : Prop) [Decidable p] :
    monadLift (guard p : m Unit) = (guard p : n Unit)

lemma probFailure_def (oa : OracleComp spec α) :
    [⊥ | oa] = (evalDist oa).run none

@[simp]
lemma evalDist_liftM [Nonempty α] [Fintype α] (q : OracleQuery spec α) :
    evalDist (q : OracleComp spec α) = OptionT.lift (PMF.uniformOfFintype α)

@[simp] lemma purePower_A (B : Type u) : (purePower B).A = PUnit

@[simp]
lemma probOutput_snd_map_eq_sum [spec.FiniteRange] [Fintype α]
    (oa : OracleComp spec (α × β)) (y : β) : [= y | snd <$> oa] = ∑ x, [= (x, y) | oa]

@[simp]
lemma probOutput_eq_zero_iff' [spec.DecidableEq] [DecidableEq α] :
    [= x | oa] = 0 ↔ x ∉ oa.finSupport

lemma uniformSelectFinset_def {α : Type} [DecidableEq α] (s : Finset α) :
    ($ s) = ($ s.toList)

@[simp]
lemma finSupport_liftComp [spec.DecidableEq] [superSpec.DecidableEq] [DecidableEq α]
    [spec.FiniteRange] [superSpec.FiniteRange]
    (oa : OracleComp spec α) : (liftComp oa superSpec).finSupport = oa.finSupport

@[simp]
lemma construct_failure :
    OracleComp.construct h_pure h_query_bind h_failure failure = h_failure

@[simp]
lemma probFailure_list_mapM_loop {α β : Type*} [spec.FiniteRange]
    (xs : List α) (f : α → OracleComp spec β) (ys : List β) :
    [⊥ | List.mapM.loop f xs ys] = 1 - (xs.map (1 - [⊥ | f ·])).prod

@[simp]
lemma replicate_pure (x : α) :
    (pure x : OracleComp spec α).replicate n = pure (List.replicate n x)

theorem tsum_cast {α β : Type u} {f : α → ENNReal} {g : β → ENNReal}
    (h : α = β) (h' : ∀ a, f a = g (cast h a)) :
      (∑' (a : α), f a) = (∑' (b : β), g b)

@[simp]
lemma probFailure_add_tsum_probOutput (oa : OracleComp spec α) :
    [⊥ | oa] + ∑' x, [= x | oa] = 1

lemma probEvent_pure_eq_one {p : α → Prop} {x : α} (h : p x) :
    [p | (pure x : OracleComp spec α)] = 1

@[simp] lemma one_le_probOutput_iff : 1 ≤ Pr[= x | mx] ↔ Pr[= x | mx] = 1

@[simp] lemma apply_eq_run_some (p : SPMF α) (x : α) : p x = p.run (some x)

@[simp]
lemma one_eq_probEvent_iff' [spec.DecidableEq] [DecidableEq α] :
    1 = [p | oa] ↔ [⊥ | oa] = 0 ∧ ∀ x ∈ oa.finSupport, p x

@[simp] lemma PMF.map_some_apply_some (p : PMF α) (x : α) : (some <$> p) (some x) = p x

@[simp]
lemma monadLift_eq_lift (x : P.Obj α) : (x : FreeM P α) = FreeM.lift x

lemma probFailure_eq_sub_sum [Fintype α] (oa : OracleComp spec α) :
    [⊥ | oa] = 1 - ∑ x : α, [= x | oa]

@[simp]
lemma mapM_pure (x : α) : (FreeM.pure x : FreeM P α).mapM s = Pure.pure x

@[simp]
theorem comp_id {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (f : Lens P Q) :
    f ∘ₗ (Lens.id P) = f

lemma ProbComp.advantage₂_eq_abs_sub_probFailure (p q : ProbComp Unit) :
    p.advantage₂ q = |([⊥ | p]).toReal - ([⊥ | q]).toReal

@[simp] lemma probOutput_none_map_fork_left (s : Option (Fin (qb i + 1))) :
    [= (none, s) | Prod.map cf cf <$> main.fork qb js i cf] = 0

@[simp] lemma query_bind_ne_pure : (q : OracleComp spec β) >>= oa ≠ pure x

@[simp]
lemma mock_decrypt_mock_encrypt (msg : BitVec 256) :
    mock_decrypt (mock_encrypt msg) = msg

theorem bind_comm_triple_swap_23 {m} [Monad m] [LawfulMonad m] [Commutative m] {α β γ δ}
    (ma : m α) (mb : m β) (mc : m γ) (f : α × β × γ → m δ) :
    (do let a ← ma; let b ← mb; let c ← mc; f (a, b, c)) =
    (ma >>= fun a => mc >>= fun c => mb >>= fun b => f (a, b, c))

lemma mem_support_eqRec_iff (oa : OracleComp spec α) (h : α = β) (y : β) :
    y ∈ (h ▸ oa).support ↔ h.symm ▸ y ∈ oa.support

lemma finSupport_eq_iff_support_eq_coe : oa.finSupport = s ↔ oa.support = ↑s

@[simp] lemma probOutput_none_map_fork_right (s : Option (Fin (qb i + 1))) :
    [= (s, none) | Prod.map cf cf <$> main.fork qb js i cf] = 0

lemma probOutput_seq_eq_tsum [spec.FiniteRange] (y : β) : [= y | og <*> oa] =
    ∑' g, ∑' x, [= g | og] * [= x | oa] * [= y | (pure (g x) : OracleComp spec β)]

@[simp] lemma allWhen_query_iff (q : OracleQuery spec α) :
    (q : OracleComp spec α).allWhen Q F possible_outputs ↔ Q q

@[simp]
theorem ulift_B {a : P.A} : (P.ulift).B (ULift.up a) = ULift (P.B a)

lemma monadLift_def (x : m α) :
    (MonadLift.monadLift x : WriterT ω m α) = WriterT.mk ((·, 1) <$> x)

lemma cacheQuery_eq_ite_ite (i : ι) (t : spec.domain i) (u : spec.range i) :
    cache.cacheQuery i t u = λ j t' ↦
      if h : j = i then (if h ▸ t' = t then some (h ▸ u) else cache j t') else cache j t'

@[simp] theorem CommutativeAt.bind_comm_comp {m} [Monad m] [LawfulMonad m] {α β γ}
    (ma : m α) (mb : m β) (h : CommutativeAt m ma mb) (f : α × β → m γ) :
      (ma >>= fun a => mb >>= fun b => f (a, b)) = (mb >>= fun b => ma >>= fun a => f (a, b))

@[simp]
lemma run_simulateQ_bind_fst (oa : OracleComp spec α) (ob : α → OracleComp spec β) :
    ((simulateQ countingOracle oa).run >>= fun x => ob x.1) = oa >>= ob

@[simp] lemma neverFails_list_foldrM {f : α → s → OracleComp spec s} {init : s} {as : List α}
    (h : ∀ i, ∀ x ∈ as, neverFails (f x i)) : neverFails (foldrM f init as)

@[simp]
lemma probOutput_pos_iff' [spec.DecidableEq] [DecidableEq α] :
    0 < [= x | oa] ↔ x ∈ oa.finSupport

@[simp] lemma monoid_mul_def (qc qc' : QueryCount spec) :
  (@HMul.hMul _ _ _ (@instHMul _ (Monoid.toMulOneClass.toMul)) qc qc')
     = (qc : ι → ℕ) + (qc' : ι → ℕ)

@[simp] lemma supportWhen_query_bind (q : OracleQuery spec α) (ob : α → OracleComp spec β) :
    (liftM q >>= ob).supportWhen poss = ⋃ x ∈ poss q, (ob x).supportWhen poss

lemma run_none_eq_one_sub (p : SPMF α) :
    p.run none = 1 - ∑' x, p.run (some x)

@[simp]
lemma probOutput_map_append_left [DecidableEq α] [spec.FiniteRange] (xs : List α)
    (oa : OracleComp spec (List α)) (ys : List α) :
    [= ys | (xs ++ ·) <$> oa] = if ys.take xs.length = xs
      then [= ys.drop xs.length | oa] else 0

@[simp] lemma someWhen_pure (x : α) :
    (pure x : OracleComp spec α).someWhen Q F possible_outputs

@[simp]
lemma run_failure [Monoid ω] {α : Type u} : (failure : WriterT ω m α).run = failure

lemma probEvent_bind_eq_tsum_subtype (q : β → Prop) :
    [q | oa >>= ob] = ∑' x : oa.support, [= x | oa] * [q | ob x]

@[simp] lemma evalDist_seq [LawfulMonad m] (mf : m (α → β)) (mx : m α) :
    evalDist (mf <*> mx) = evalDist mf <*> evalDist mx

lemma probEvent_ext' [spec.DecidableEq] [DecidableEq α]
    (h : ∀ x ∈ oa.finSupport, p x ↔ q x) : [p | oa] = [q | oa]

@[simp]
lemma countQ_logQuery {α} (log : QueryLog spec) (q : OracleQuery spec α) (u : α)
    (i : ι) : (log.logQuery q u).countQ i = log.countQ i + if q.index = i then 1 else 0

@[ext] lemma ext {p q : SPMF α} (h : ∀ x : α, p.run (some x) = q.run (some x)) : p = q :=
  PMF.ext fun

lemma negligible_zero : negligible 0

@[simp] theorem toMonadState_set_eq_monadStateOf_set {m : Type u → Type v} {σ : Type u}
    [MonadStateOf σ m] : (MonadState.set : σ → m PUnit) = MonadStateOf.set
</all_available_lemmas>

<local_ctx>
import VCVio.OracleComp.Traversal

import VCVio.OracleComp.SimSemantics.SimulateQ

import Mathlib.Probability.Distributions.Uniform

import ToMathlib.General

open OracleSpec Option ENNReal BigOperators

namespace OracleComp

variable {ι : Type u} {spec : OracleSpec ι} {ι' : Type v} {spec' : OracleSpec ι'}
  {α β γ : Type w} [spec.FiniteRange] [spec'.FiniteRange]

section evalDist

end evalDist

noncomputable def probOutput (oa : OracleComp spec α) (x : α) : ℝ≥0∞ :=
  (evalDist oa).run (some x)

notation "[=" x "|" oa "]" => probOutput oa x

notation "[⊥" "|" oa "]" => probFailure oa

notation "[" p "|" oa "]" => probEvent oa p

section bounds

variable {oa : OracleComp spec α} {x : α} {p : α → Prop}

end bounds

section support

variable (oa : OracleComp spec α) (x : α) (p q : α → Prop)

variable {oa x p q}

end support

section sums

variable (oa : OracleComp spec α) (p : α → Prop)

end sums

section pure

variable (x : α)

end pure

section bind

variable (oa : OracleComp spec α) (ob : α → OracleComp spec β)

end bind

section mul_le_probEvent_bind
</local_ctx>

<target_theorem>
lemma mul_le_probEvent_bind {oa : OracleComp spec α} {ob : α → OracleComp spec β}
    {p : α → Prop} {q : β → Prop} {r r' : ℝ≥0∞}
    (h : r ≤ [p | oa]) (h' : ∀ x ∈ oa.support, p x → r' ≤ [q | ob x]) :
    r * r' ≤ [q | oa >>= ob] :=
</target_theorem>

