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>
Fin in Init.Prelude

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'

def IND_CPA_parallelTesting_reduction
    (adversary : (elgamalAsymmEnc G P).IND_CPA_adversary) :
    parallelTestingAdversary G P := fun x x₁ x₂ x₃ => do
  let so : QueryImpl (P × P →ₒ P × P) ProbComp := ⟨fun (query () (m₁, _m₂)) =>
    return (x₂, m₁ * x₃)⟩
  simulateQ (idOracle ++ₛₒ so) (adversary (x, x₁))

class DijkstraMonad (w : Type u → Type v) (d : {α : Type u} → w α → Type z) [Monad w] where
  
  dPure {α : Type u} : (x : α) → d (pure x)
  dBind {α β : Type u} {wa : w α} {wb : α → w β} : d wa → ((a : α) → d (wb a)) → d (wa >>= wb)

Function.RightInverse in Init.Data.Function

Monoid.toOne in Mathlib.Algebra.Group.Defs

instance subSpec_right_append_right_append_of_subSpec [h : spec₂ ⊂ₒ spec₃] :
    spec₁ ++ₒ spec₂ ⊂ₒ spec₁ ++ₒ spec₃ where
  monadLift
    | query (inl i) t => query (inl i) t
    | query (inr i) t => liftM (query i t)

@[inherit_doc] scoped[PFunctor] infixr:80 " X^ " => monomial

instance [Comonad f] [Comonad g] : Comonad (Day f g) where
  extract {a : Type u₃} := extract
  extend {a b : Type u₃} (day : Day f g a) (k : Day f g a → b) : Day f g b :=
    sorry 
    
  coseq {a b : Type u₃} := coseq

MonadFunctor.monadMap in Init.Prelude

Option.getM in Init.Data.Option.Basic

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

List.singleton in Init.Data.List.Basic

instance : Functor NonEmptyList where
  map := NonEmptyList.map

instance [h₁ : spec₁.DecidableEq] [h₂ : spec₂.DecidableEq] :
    (spec₁ ++ₒ spec₂).DecidableEq where
  domain_decidableEq' := Sum.rec h₁.domain_decidableEq' h₂.domain_decidableEq'
  range_decidableEq' := Sum.rec h₁.range_decidableEq' h₂.range_decidableEq'

MonadControl.restoreM in Init.Control.Basic

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

instance : LawfulMonad (FreeMonad f) :=
  LawfulMonad.mk' (FreeMonad f)
    (λ x ↦ by admit /- proof elided -/
      )
    (λ x f ↦ rfl)
    (λ x f g ↦ by admit /- proof elided -/
      )

def Hybrid_1 : ProbComp Bool := do
  let b ←$ᵗ Bool
  let A ←$ᵗ Matrix (Fin n) (Fin m) (Fin p)
  let u ←$ᵗ Vector (Fin p) m
  let ⟨m₁, m₂, st⟩ ← adv.chooseMessages (A, u)
  let c ← if b then (uniformRegevAsymmEnc n m p χ he).encrypt (A, u) m₁
    else (uniformRegevAsymmEnc n m p χ he).encrypt (A, u) m₂
  let b' ← adv.distinguish st c
  return b = b'

dite in Init.Prelude

def decryptionOracle (encAlg : AsymmEncAlg m M PK SK C)
    (sk : SK) : QueryImpl (C →ₒ M) m where
  impl | query () c => Option.getM (encAlg.decrypt sk c)

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

def verify_message_package
    (package : MessagePackage) : OracleComp unifSpec (Option SecretMessage) := do
  let content := decrypt_message package.encrypted_message package.nonce
  let (msg_bv, _) := serialize_message_data content package.nonce
  let computed_tf := mock_hmac_sha256 package.nonce msg_bv
  if computed_tf = package.franking_tag.tag then
    return some { content := content, nonce := package.nonce }
  else
    return none

def prodSigmaDistrib : (P * sigma F : PFunctor.{max uA₁ uA₂ v, max uB₁ uB₂}) ≃ₚ
    sigma (fun i => (P * F i : PFunctor.{max uA₁ uA₂, max uB₁ uB₂})) where
  equivA := sorry
  equivB := sorry

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

instance instOfMonadLiftT {m n} [MonadLiftT m n] : MonadRelation m n where
  monadRel := fun ma na => liftM ma = na

def CommutativeAt (m : Type u → Type v) [Monad m] {α β : Type u} (ma : m α) (mb : m β) : Prop :=
  (do let a ← ma; let b ← mb; pure (a, b)) = (do let b ← mb; let a ← ma; pure (a, b))

def uniqueSigma [Unique I] : sigma F ≃ₚ F default where
  equivA := _root_.Equiv.uniqueSigma _
  equivB := fun a => 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)))

MonadLift in Init.Prelude

instance {r} [h : Preorder r] : OrderedMonad (MonoCont r) where
  monadOrder := inferInstance
  bind_mono := fun _ _ => by admit /- proof elided -/

def coseq (za : Zipper α) (zb : Zipper β) : Zipper (α × β) :=
  sorry

@[simp] def head_nel (nel : NonEmptyList α) : α := nel.head

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

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 -/

StateT.set in Init.Control.State

def deserialize_message_data (data : BitVec 256 × BitVec 256) : String × BitVec 256 :=
  let (msg_bv, nonce) := data
  (bitvec_to_string msg_bv, nonce)

instance decidablePred_mem_support [spec.FiniteRange] [hα : DecidableEq α]
    (oa : OracleComp spec α) : DecidablePred (· ∈ oa.support) :=

instHMul in Init.Prelude

class LawfulMonadRelation (m : Type u → Type v) (n : Type u → Type w) [Monad m] [Monad n]
    [MonadRelation m n] where
  monadRel_pure {α : Type u} (a : α) : monadRel (pure a : m α) (pure a : n α)
  monadRel_bind {α β : Type u} {ma : m α} {mb : α → m β} {na : n α} {nb : α → n β}
    (ha : monadRel ma na) (hb : ∀ a, monadRel (mb a) (nb a)) : monadRel (ma >>= mb) (na >>= nb)

Classical.arbitrary in Mathlib.Logic.Nonempty

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

@[simp]
def compNth (P : PFunctor.{uA, uB}) : Nat → PFunctor.{max uA uB, uB}
  | 0 => X
  | Nat.succ n => P ◃ compNth P n

def generate_franking_tag (nonce : BitVec 256) (msg : String) : FrankingTag :=
  let (msg_bv, _) := serialize_message_data msg nonce
  let tf := mock_hmac_sha256 nonce msg_bv 
  { tag := tf }

List.foldlM in Init.Data.List.Control

Finite.Set.finite_biUnion'' in Mathlib.Data.Set.Finite.Lattice

example : Hybrid_0 adv = IND_CPA_OneTime_Game adv :=

def compAssoc : (P ◃ Q) ◃ R ≃ₚ P ◃ (Q ◃ R) where
  equivA := {
    toFun := fun ⟨⟨pa, qf⟩, rf⟩ => ⟨pa, fun pb => ⟨qf pb, fun qb => rf ⟨pb, qb⟩⟩⟩
    invFun := fun ⟨pa, g⟩ => ⟨⟨pa, fun pb => (g pb).1⟩, fun ⟨pb, qb⟩ => (g pb).2 qb⟩
    left_inv := by admit /- proof elided -/

def string_to_bitvec (s : String) : BitVec 256 :=
  s.foldl (λ acc c => (acc.shiftLeft 8) + BitVec.ofNat 256 c.toNat) 0

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)

ReaderT in Init.Prelude

@[simp] def negligible_iff (f : ℕ → ℝ≥0∞) :
    negligible f ↔ SuperpolynomialDecay atTop (λ x ↦ ↑x) f := Iff.rfl

def monomial (A : Type uA) (B : Type uB) : PFunctor.{uA, uB} :=
  ⟨A, fun _ => B⟩

def compX : P ◃ X ≃ₚ P where
  equivA := Equiv.sigmaUnique P.A (fun a => P.B a → PUnit.{_ + 1})
  equivB := fun _ => _root_.Equiv.sigmaPUnit _

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

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 _ _

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)

def takeAtIndex [DecidableEq ι] (seed : QuerySeed spec) (i : ι) (n : ℕ) : QuerySeed spec :=
  Function.update seed i ((seed i).take n)

ExceptT in Init.Control.Except

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

instance {a : (1 ◃ P).A} : IsEmpty ((1 ◃ P).B a) where
  false := fun a => a.1.elim

instance : EmptyCollection (QueryCache spec) := ⟨fun _ _ => none⟩

def prodMap {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}}
    {W : PFunctor.{uA₄, uB₄}} (l₁ : Lens P R) (l₂ : Lens Q W) :
    Lens.{max uA₁ uA₂, max uB₁ uB₂, max uA₃ uA₄, max uB₃ uB₄} (P * Q) (R * W) :=
  (fun pq => (l₁.toFunA pq.1, l₂.toFunA pq.2)) ⇆
    (fun pq => Sum.elim (Sum.inl ∘ l₁.toFunB pq.1) (Sum.inr ∘ l₂.toFunB pq.2))

Append in Init.Prelude

def map (f : α → β) : NonEmptyList α → NonEmptyList β
  | ⟨h, t⟩ => ⟨f h, List.map f t⟩

List.range in Init.Data.List.Basic

class RelativeMonad (j : Type u → Type w) (m : Type u → Type v)
    extends RelativePure j m, RelativeBind j m, RelativeFunctor j m where
  mapᵣ f x := bindᵣ x (pureᵣ ∘ f)

instance : MonadLift P (FreeM P) where
  monadLift x := FreeM.lift x

alias PKE_Alg := AsymmEncAlg

def rangeDecidableEq [spec.DecidableEq] : OracleQuery spec α → DecidableEq α
  | query i t => inferInstance

instance : Comonad (Prod ε) where

Set.image in Mathlib.Data.Set.Defs

instance hasEvalDist : HasEvalDist SPMF where
  evalDist := id
  evalDist_pure _ := rfl
  evalDist_bind _ _ := rfl

class LawfulRelativeMonad (j : Type u → Type w) (m : Type u → Type v)
    [RelativeMonad j m] extends LawfulRelativeFunctor j m where

def pi {I : Type v} (F : I → PFunctor.{uA, uB}) : PFunctor.{max uA v, max uB v} :=
  ⟨(i : I) → (F i).A, fun f => Σ i, (F i).B (f i)⟩

def Hybrid_2 : ProbComp Bool := do
  let b ←$ᵗ Bool
  let A ←$ᵗ Matrix (Fin n) (Fin m) (Fin p)
  let u ←$ᵗ Vector (Fin p) m
  let ⟨_, _, st⟩ ← adv.chooseMessages (A, u)
  
  let c₁ ←$ᵗ Vector (Fin p) n
  let c₂ ←$ᵗ Fin p
  let b' ← adv.distinguish st (c₁, c₂)
  return b = b'

MonadState in Init.Prelude

PMF.instMonad in Mathlib.Probability.ProbabilityMassFunction.Monad

structure BindHom (m : Type u → Type v) [Bind m] (n : Type u → Type w) [Bind n]
    extends NatHom m n where
  toFun_bind' {α β : Type u} (x : m α) (y : α → m β) :
    toFun (x >>= y) = toFun x >>= (fun a => toFun (y a))

Sum in Init.Core

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

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

structure FrankingTag where
  tag : mock_hmac_sha256_out_type 
  deriving Repr

class LawfulMonadStateOf (σ : outParam (Type u)) (m : Type u → Type v) [Monad m] [MonadStateOf σ m]
    : Prop where

inductive FreeDijkstra (m : Type u → Type v) [Monad m] : {α : Type u} → m α → Type _ where
  | protected pure {α} (x : α) : FreeDijkstra m (pure x)
  | roll {α β} (x : m α) {f : α → m β} (r : α → FreeDijkstra m (x >>= f)) : FreeDijkstra m (x >>= f)

def fst {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} :
    Lens.{max uA₁ uA₂, max uB₁ uB₂, uA₁, uB₁} (P * Q) P :=
  Prod.fst ⇆ (fun _ => Sum.inl)

def negligible (f : ℕ → ℝ≥0∞) : Prop :=
  SuperpolynomialDecay atTop (λ x ↦ ↑x) f

StateT.mk in Init.Control.State

Except in Init.Prelude

def decrypt_message (encrypted_msg : EncryptedMessage) (nonce : BitVec 256) : String :=
  let decrypted_bv := mock_decrypt encrypted_msg.ciphertext
  let (msg, _) := deserialize_message_data (decrypted_bv, nonce)
  msg

protected def mapM' (m : Type u → Type w) [Monad m] [LawfulMonad m]
    (s : {α : Type u} → f α → m α) : FreeMonad f →ᵐ m where
  toFun := FreeMonad.mapM_aux s
  toFun_pure' x := rfl
  toFun_bind' x y := by admit /- proof elided -/

def generateSeed (spec : OracleSpec ι) [∀ i, SelectableType (spec.range i)]
    (qc : ι → ℕ) (js : List ι) : ProbComp (QuerySeed spec) := do
  let mut seed : QuerySeed spec := ∅
  for j in js do
    seed := seed.addValues (← ($ᵗ spec.range j).replicate (qc j))
  return seed

Equiv.punitArrowEquiv in Mathlib.Logic.Equiv.Defs

instance [Monoid ω] [LawfulMonad m] : LawfulMonadLift m (WriterT ω m) where
  monadLift_pure x := map_pure (·, 1) x
  monadLift_bind {α β} x y := by admit /- proof elided -/

def zeroProd :
    Lens.Equiv.{max uA₁ uA₂, max uB₁ uB₂, uA₁, uB₁} ((0 : PFunctor.{uA₂, uB₂}) * P) 0 where
  toLens := (fun ⟨pa, _⟩ => PEmpty.elim pa) ⇆ (fun _ x => PEmpty.elim x)
  invLens := PEmpty.elim ⇆ (fun pe _ => PEmpty.elim pe)
  left_inv := by admit /- proof elided -/

class Coapplicative (w : Type u → Type v) extends
    Functor w, Extract w, Coseq w, CoseqLeft w, CoseqRight w where
   
  coseqLeft wa wb := Functor.map Prod.fst (coseq wa wb)
   
  coseqRight wa wb := Functor.map Prod.snd (coseq wa wb)

Equiv.pemptyArrowEquivPUnit in Mathlib.Logic.Equiv.Defs

class RelativePure (j : Type u → Type w) (f : Type u → Type v) where
   
  pureᵣ : {α : Type u} → j α → f α

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

List.zipWith in Init.Data.List.Basic

Fintype.card in Mathlib.Data.Fintype.Card

def sumSigmaDistrib (F : I → PFunctor.{uA₂, uB₁}) :
    (P + sigma F : PFunctor.{max uA₁ uA₂ v, uB₁}) ≃ₚ
    sigma (fun i => (P + F i : PFunctor.{max uA₁ uA₂, uB₁})) where
  equivA := by admit /- proof elided -/

structure ExecutionMethod (m : Type u → Type v) where
    exec {α : Type u} : m α → ProbComp α
    lift_probComp {α : Type u} : ProbComp α → m α
    exec_lift_probComp {α : Type u} (px : ProbComp α) :
      exec (lift_probComp px) = px

IO in Init.System.IO

class MonadAlgebra (m : Type u → Type v) where
  monadAlg {α : Type u} : m α → α

instance [Inhabited (f α)] : Inhabited (FreeMonad f α) := ⟨FreeMonad.lift default⟩

set_get : (do let s ← MonadStateOf.get (m := m); set (σ := σ) s) = pure ⟨⟩

instance {comp : StateM σ α} {Q : PostCondition σ α} :
    Subsingleton (WeakestPrecondition comp Q) :=

@[symm]
def symm {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (e : P ≃ₗ Q) : Q ≃ₗ P :=
  ⟨e.invLens, e.toLens, e.right_inv, e.left_inv⟩

structure SecretMessage where
  content : String
  nonce : BitVec 256
  deriving Repr

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

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

def tail (t : CofreeC F α) : F (CofreeC F α) :=
  let d := M.dest t       
  ⟨d.1.2, d.2⟩

def cast {P Q : PFunctor.{uA, uB}} (hA : P.A = Q.A) (hB : ∀ a, P.B a = Q.B (cast hA a)) :
    P ≃ₚ Q where
  equivA := _root_.Equiv.cast hA
  equivB := fun a => _root_.Equiv.cast (hB a)

structure MessagePackage where
  encrypted_message : EncryptedMessage
  franking_tag : FrankingTag
  reporting_tag : ReportingTag
  context : Context
  nonce : BitVec 256
  deriving Repr

guard in Init.Control.Basic

def addValues [DecidableEq ι] {i : ι}
    (us : List (spec.range i)) (seed : QuerySeed spec) : QuerySeed spec :=
  Function.update seed i (seed i ++ us)

Fin.foldlM in Init.Data.Fin.Fold

OptionT in Init.Control.Option

comp_mapᵣ {α β γ : Type u} (g : j α → j β) (h : j β → j γ) (x : f α) :
    (h ∘ g) <$>ᵣ x = h <$>ᵣ g <$>ᵣ x

instance instOfMonadMorphism {m n} [Monad m] [Monad n] [h : MonadLiftT m n]
    [h' : LawfulMonadLiftT m n] :
      DijkstraMonad n (fun na => { ma : m _ // monadLift ma = na }) :=
  @instOfMonadRelation m n _ _ (@instOfMonadLiftT m n h) (@instOfLawfulMonadLiftT m n _ _ h h')

One.one in Init.Prelude

instance [MonadTransformer t] [Monad m] : MonadLift m (t m) := MonadTransformer.transform m

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}"

protected def mapM {m : Type u → Type v} {n : Type u → Type w}
    [AlternativeMonad n] (f : {α : Type u} → m α → n α)
    {α : Type u} (x : OptionT m α) : n α :=
  do (← f x.run).getM

Functor in Init.Prelude

def fork (main : OracleComp spec α)
    (qb : ι → ℕ) (js : List ι) (i : ι)
    (cf : α → Option (Fin (qb i + 1))) :
    OracleComp spec (α × α) := do
  let seed ← generateSeed spec qb js
  let x₁ ← (simulateQ seededOracle main).run seed
  let s : Fin (qb i + 1) ← (cf x₁).getM
  let u ←$ᵗ spec.range i 
  guard ((seed i)[s + 1]? ≠ some u) 
  let seed' := (seed.takeAtIndex i s).addValue i u
  let x₂ ← (simulateQ seededOracle main).run seed'
  guard (cf x₂ = some s) 
  return (x₁, x₂)

instance instCoapplicative [Comonad w] : Coapplicative (StoreT s w) where

@[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

@[simps]
def zeroSum : 0 + P ≃ₚ P where
  equivA := Equiv.emptySum PEmpty P.A
  equivB := (Sum.casesOn · (fun a => a.elim) (fun _ => _root_.Equiv.refl _))

structure PureHom (m : Type u → Type v) [Pure m] (n : Type u → Type w) [Pure n]
    extends NatHom m n where
  toFun_pure' {α : Type u} (x : α) : toFun (pure x) = (pure x : n α)

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 -/

Except.bind in Init.Control.Except

LawfulAlternative in Batteries.Control.AlternativeMonad

instance : Functor Zipper where
  map := map

Inhabited in Init.Prelude

PMF.uniformOfFinset in Mathlib.Probability.Distributions.Uniform

instance : Coe (MonadEquiv m n) (MonadHom n m) where
  coe f := ⟨f.invNatHom, f.map_pure_inv, f.map_bind_inv⟩

ULift in Init.Prelude

class LawfulMonadControlT (m : Type u → Type v) (n : Type u → Type w)
    [Monad m] [Monad n] [MonadControlT m n] : Prop where

Equiv.sigmaUnique in Mathlib.Logic.Equiv.Prod

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

MonadControl in Init.Control.Basic

WithTop in Mathlib.Order.TypeTags

CategoryTheory.aesop_cat in Mathlib.CategoryTheory.Category.Basic

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

instance : unifSpec.FiniteRange where
  range_inhabited' := inferInstance
  range_fintype' := inferInstance

abbrev PreordEnrichedCategory (C : Type u) := EnrichedCategory Preord C

def FreeContM (f : Type z → Type y) (α : Type w) : Type (max (u + 1) w y (z + 1)) :=
  FreeContT f Id.{u} α

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

abbrev addValue (seed : QuerySeed spec) (i : ι) (u : spec.range i) : QuerySeed spec :=
  seed.addValues [u]

Sum.elim in Init.Data.Sum.Basic

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 -/
  )

LawfulMonad in Init.Control.Lawful.Basic

instance : Extend Stream' where
  extend s f := fun n => f (Stream'.drop n s)

Zero in Init.Prelude

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

MonadFunctor in Init.Prelude

instance {w d} [Monad w] [DijkstraMonad w d] : MonadLiftT (fun α => (w : w α) × d w) w where
  monadLift x := x.1

instance {w d} [Monad w] [DijkstraMonad w d] : MonadRelation (fun α => (w : w α) × d w) w :=
  instOfMonadLiftT

def FreeContM.toFreeMonad : FreeContM f α → FreeMonad f α :=
  fun x => x FreeMonad.roll FreeMonad.pure

instance : Coseq NonEmptyList where
  coseq := NonEmptyList.zip

instance instLawfulFunctor [Comonad w] [LawfulFunctor w] : LawfulFunctor (EnvT e w) where
  id_map := by admit /- proof elided -/

instance : Coe (PureEquiv m n) (PureHom n m) where
  coe f := ⟨f.toNatEquiv, f.map_pure_inv⟩

Vector.range in Init.Data.Vector.Basic

def unzipCommits (x₀ pk : P) (zs : Vector G n)
    (hash : Vector Bool n) : Vector P n :=
  Vector.zipWith (λ z b ↦ if b then z +ᵥ pk else z +ᵥ x₀) zs hash

Prod.map in Init.Core

instance : Coapplicative NonEmptyList where

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

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

def isFailure {α : Type v} : OracleComp spec α → Bool
  | FreeMonad.pure x => Option.isNone x
  | _ => false

Stream'.map in Mathlib.Data.Stream.Defs

def mock_hmac_sha256_out_type : Type := String

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

require "leanprover-community" / "mathlib" @ git "v4.24.0-rc1"

instance instMonadLift [Bind m] : MonadLift m (FreeContT f m) where
  monadLift := lift

AddGroup in Mathlib.Algebra.Group.Defs

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 -/

List.count in Init.Data.List.Basic

Vector.ofFn in Init.Data.Vector.Basic

structure NatHom (m : Type u → Type v) (n : Type u → Type w) where
  toFun : {α : Type u} → m α → n α
</all_available_defs>

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

@[simp]
lemma PMF.monad_bind_eq_bind {α β : Type u}
      (p : PMF α) (q : α → PMF β) : p >>= q = p.bind q

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 liftM_query_writerT {ω : Type v} [Monoid ω] {α : Type v} (q : OracleQuery spec α) :
  (liftM q : WriterT ω (OracleComp spec) α) = liftM (liftM q : OracleComp spec α)

@[simp]
lemma evalDist_seq (oa : OracleComp spec α) (og : OracleComp spec (α → β)) :
    evalDist (og <*> oa) = evalDist og <*> evalDist oa

@[simp]
lemma support_toFun (q : OracleQuery spec α) :
    support (h.monadLift q : OracleComp superSpec α) = Set.univ

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

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

lemma mem_support_iff_probOutput_pos : x ∈ oa.support ↔ 0 < [= x | oa]

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

@[simp]
lemma finSupport_simulateQ [spec.FiniteRange] [spec.DecidableEq] [DecidableEq α]
    (oa : OracleComp spec α) : (simulateQ unifOracle oa).finSupport = oa.finSupport

lemma evalDist_seq_map [spec.FiniteRange] :
    evalDist (f <$> oa <*> ob) = f <$> evalDist oa <*> evalDist ob

@[simp]
theorem liftM_elimM [Monad m] [Monad n] [LawfulMonad m] [LawfulMonad n]
    [MonadLift m n] [LawfulMonadLift m n] (x : m (Option α)) (y : m β) (z : α → m β) :
      liftM (Option.elimM x y z) = Option.elimM (x : n (Option α)) (y) (fun x => z x)

@[simp]
lemma evalDist_simulateQ [spec.FiniteRange] (oa : OracleComp spec α) :
    evalDist (simulateQ unifOracle oa) = evalDist oa

lemma probEvent_eq_tsum_indicator (oa : OracleComp spec α) (p : α → Prop) :
    [p | oa] = ∑' x : α, {x | p x}.indicator ([= · | oa]) x

@[simp] theorem RelativeFunctor.map_map [RelativeFunctor j f] [LawfulRelativeFunctor j f]
    (h : j α → j β) (g : j β → j γ) (x : f α) :
      g <$>ᵣ h <$>ᵣ x = (fun a => g (h a)) <$>ᵣ x

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

@[simp] lemma support_query_bind (q : OracleQuery spec α) (ob : α → OracleComp spec β) :
    (liftM q >>= ob).support = ⋃ x, (ob x).support

@[simp]
lemma probFailure_pure : [⊥ | (pure x : OracleComp spec α)] = 0

@[simp]
lemma replicateTR_zero : replicate 0 oa = return []

theorem Option.cast_eq_some_iff {α β : Type u} {x : Option α} {b : β} (h : α = β) :
    cast (congrArg Option h) x = some b ↔ x = some (cast h.symm b)

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

@[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)))

@[simp] lemma fin_support_map [spec.DecidableEq] [spec.FiniteRange]
    [DecidableEq α] [DecidableEq β] (oa : OracleComp spec α) (f : α → β) :
    (f <$> oa).finSupport = oa.finSupport.image f

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 generateSeed_zero : generateSeed spec 0 js = return ∅

@[simp] lemma withCounting_apply {α} (so : QueryImpl spec m) (q : OracleQuery spec α) :
    so.withCounting.impl q = tell (QueryCount.single q.index) *> ↑(so.impl q)

@[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

@[simp]
theorem symm_comp_self {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (e : P ≃ₚ Q) :
    e.symm.equivA ∘ e.equivA = id

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

lemma tsum_probOutput_eq_one (oa : OracleComp spec α) (h : [⊥ | oa] = 0) :
    ∑' x : α, [= x | oa] = 1

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

lemma probOutput_map_eq_tsum_subtype_ite [DecidableEq β] (y : β) :
    [= y | f <$> oa] = ∑' x : oa.support, if y = f x then [= x | oa] else 0

@[simp]
theorem MonoContProp_def :
  MonoContProp = fun α => {m : Cont Prop α // ∀ p p', (∀ a, p a → p' a) → m p → m p'}

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

@[simp]
lemma evalDist_bind (oa : OracleComp spec α) (ob : α → OracleComp spec β) :
    evalDist (oa >>= ob) = (evalDist oa) >>= (evalDist ∘ ob)

@[simp]
lemma evalDist_liftComp [spec.FiniteRange] [superSpec.FiniteRange]
    (oa : OracleComp spec α) : evalDist (liftComp oa superSpec) = evalDist oa

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

@[simp]
lemma takeAtIndex_addValues (seed : QuerySeed spec) {i : ι} (n : ℕ) (xs : List (spec.range i)) :
    (seed.addValues xs).takeAtIndex i n = if n ≤ (seed i).length
      then seed.takeAtIndex i n else seed.addValues (xs.take (n - (seed i).length))

@[simp] lemma one_le_probEvent_iff : 1 ≤ Pr[p | mx] ↔ Pr[p | mx] = 1

@[simp]
lemma probOutput_coin (b : Bool) : [= b | coin] = 2⁻¹

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)

lemma monad_failure_eq [Monad m] [Alternative m] :
    (failure : StateT σ m α) = StateT.failure

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

@[simp] lemma support_bind (oa : OracleComp spec α) (ob : α → OracleComp spec β) :
    (oa >>= ob).support = ⋃ x ∈ oa.support, (ob x).support

@[simp] lemma neverFails_vector_mapM {n} {f : α → OracleComp spec β} {as : Vector α n}
    (h : ∀ x ∈ as.toList, neverFails (f x)) : neverFails (Vector.mapM f as)

lemma List.countP_eq_sum_fin_ite {α : Type*} (xs : List α) (p : α → Bool) :
    (∑ i : Fin xs.length, if p xs[i] then 1 else 0) = xs.countP p

@[simp]
lemma card_bitVec (n : ℕ) : Fintype.card (BitVec n) = 2 ^ n

lemma probEvent_seq_map_eq_probEvent [spec.FiniteRange] (p : γ → Prop) :
    [p | f <$> oa <*> ob] = [λ z ↦ p (f z.1 z.2) | Prod.mk <$> oa <*> ob]

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

lemma eq_query_index_input : (q : OracleQuery spec α) →
    q = q.range_index ▸ OracleQuery.query q.index q.input

lemma X_eq_purePower_pUnit : X = purePower PUnit

lemma mapM_bind [LawfulMonad m] (oa : OracleComp spec α) (ob : α → OracleComp spec β)
    (hfail : ∀ f : α → m β, fail >>= f = fail) :
    (oa >>= ob).mapM fail qm =
      oa.mapM fail qm >>= λ x ↦ (ob x).mapM fail qm

@[simp]
lemma monad_pure_def (x : α) : (pure x : FreeM P α) = FreeM.pure x

@[simp]
lemma FreeContM.def_eq : FreeContM.{u, w, y, z} f α =
    ({r : Type u} → ({x : Type z} → f x → (x → r) → r) → (α → r) → r)

@[simp] theorem extract_map {α β : Type u} (f : α → β) (wa : w α) :
  extract (Functor.map f wa) = f (extract wa)

@[simp] lemma failure_ne_query : failure ≠ (q : OracleComp spec β)

lemma probOutput_seq_eq_tsum_ite [spec.FiniteRange] [DecidableEq β] (y : β) :
    [= y | og <*> oa] = ∑' g, ∑' x, if y = g x then [= g | og] * [= x | oa] else 0

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

@[simp] lemma support_uniformSelectList (xs : List α) :
    ($ xs).support = if xs.isEmpty then ∅ else {y | y ∈ (xs)}

lemma mem_finSupport_seq_map_cons_iff [spec.FiniteRange] [spec.DecidableEq] [DecidableEq α]
    (xs : List α) (h : xs ≠ []) : xs ∈ (cons <$> oa <*> ob).finSupport ↔
      xs.head h ∈ oa.finSupport ∧ xs.tail ∈ ob.finSupport

@[simp]
theorem pure_rule (x : α) :
    HoareTriple (PreCondition.top σ) (pure x) (fun s a s' => s = s' ∧ a = x)

@[simp]
lemma map_bind (f : BindEquiv m n) {α β : Type u} (x : m α) (y : α → m β) :
    f.toFun (x >>= y) = f.toFun x >>= (fun a => f.toFun (y a))

@[simp] lemma simulateQ_ite (p : Prop) [Decidable p] (oa oa' : OracleComp spec α) :
    simulateQ so (ite p oa oa') = ite p (simulateQ so oa) (simulateQ so oa')

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

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

@[simp] theorem liftM_guard [AlternativeMonad m] [AlternativeMonad n] [MonadLift m n]
    [LawfulAlternativeLift m n] [LawfulMonadLift m n] (p : Prop) [Decidable p] :
    liftM (guard p : m Unit) = (guard p : n Unit)

@[simp] lemma simulateQ_query (q : OracleQuery spec α) : simulateQ so q = so.impl q

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

@[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

@[simp]
theorem sumMap_id :
    Lens.sumMap (Lens.id P) (Lens.id Q) = Lens.id.{max uA₁ uA₂, uB₁} (P + Q)

@[simp] -- Automatically reduce "multiplication" of query logs to `List.append`
lemma monoid_mul_def (qc qc' : QueryLog spec) :
  (@HMul.hMul _ _ _ (@instHMul _ (Monoid.toMulOneClass.toMul)) qc qc')
     = (qc : List _) ++ (qc' : List _)

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

@[simp low]
lemma probEvent_eq_zero_iff : [p | oa] = 0 ↔ ∀ x ∈ oa.support, ¬ p x

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

lemma probEvent_eqRec (q : β → Prop) :
    [q | h ▸ oa] = [λ x ↦ q (h ▸ x) | oa]

@[simp]
theorem ulift_A : (P.ulift).A = ULift P.A

lemma probOutput_bind_ite_failure_eq_tsum [spec.FiniteRange] [DecidableEq β]
    (oa : OracleComp spec α) (f : α → β) (p : α → Prop) [DecidablePred p] (y : β) :
    [= y | oa >>= fun x => if p x then pure (f x) else failure] =
      ∑' x : α, if p x ∧ y = f x then [= x | oa] else 0

@[simp]
lemma mapM_lift [Monad m] [LawfulMonad m] (s : (a : P.A) → m (P.B a)) (x : P.Obj α) :
    FreeM.mapM s (FreeM.lift x) = s x.1 >>= (λ u ↦ (pure (x.2 u)).mapM s)

lemma not_noFailure_of_probFailure_pos {oa : OracleComp spec α} (h : 0 < [⊥ | oa]) :
    ¬ neverFails oa

lemma probOutput_eqRec (y : β) : [= y | h ▸ oa] = [= h ▸ y | oa]

@[simp]
lemma probOutput_ite (x : α) : [= x | if p then oa else oa'] =
    if p then [= x | oa] else [= x | oa']

lemma probOutput_map_eq_sum_filter_finSupport [spec.DecidableEq] [DecidableEq α] [DecidableEq β]
    (y : β) : [= y | f <$> oa] = ∑ x ∈ oa.finSupport.filter (y = f ·), [= x | oa]

example : support (do
    let b ← coin; let b' ← coin
    let x ← (if b && b' then return 0 else return 1);
    let z ← (if b && b' then return x else return 0);
    return (x * z)) = {0}

@[simp] lemma evalDist_map [LawfulMonad m] (mx : m α) (f : α → β) :
    evalDist (f <$> mx) = f <$> (evalDist mx)

lemma mem_support_seq_map_cons_iff' (xs : List α) : xs ∈ (List.cons <$> oa <*> ob).support ↔
    xs.recOn False (λ x xs _ ↦ x ∈ oa.support ∧ xs ∈ ob.support)

lemma pure_eq_query_iff_false : pure y = (q : OracleComp spec β) ↔ False

@[simp]
lemma construct_roll (x : f β) (r : β → FreeMonad f α) :
    (FreeMonad.construct h_pure h_roll (roll x r) : C (roll x r)) =
      (h_roll x r (λ u ↦ FreeMonad.construct h_pure h_roll (r u)))

@[simp] lemma simulateQ_failure : simulateQ so (failure : OracleComp spec α) = failure

@[simp] lemma finSupport_bind (oa : OracleComp spec α) (ob : α → OracleComp spec β)
    [hα : DecidableEq α] [hβ : DecidableEq β] [spec.FiniteRange] :
    (oa >>= ob).finSupport = oa.finSupport.biUnion (λ x ↦ (ob x).finSupport)

@[simp] lemma finSupportWhen_bind (oa : OracleComp spec α) (ob : α → OracleComp spec β)
    [DecidableEq α] [DecidableEq β] :
    (oa >>= ob).finSupportWhen fin_poss =
      (oa.finSupportWhen fin_poss).biUnion fun x => (ob x).finSupportWhen fin_poss

lemma FreeContM.toFreeContM_toFreeMonad (x : FreeContM f α):
    @FreeMonad.toFreeContM f α (FreeContM.toFreeMonad x) = @x

lemma probEvent_coin_eq_sum_subtype (p : Bool → Prop) :
    [p | coin] = ∑' _ : {x | p x}, 2⁻¹

@[simp]
lemma neverFails_pure (x : α) : neverFails (pure x : OracleComp spec α)

@[simp]
lemma single_le_iff_pos [DecidableEq ι] (i : ι) (qc : QueryCount spec) :
    single i ≤ qc ↔ 0 < qc i

@[simp] lemma one_le_probFailure_iff : 1 ≤ [⊥ | oa] ↔ [⊥ | oa] = 1

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

lemma probFailure_eq_sub_probEvent (oa : OracleComp spec α) :
    [⊥ | oa] = 1 - [λ _ ↦ true | oa]

@[simp] lemma isFailure_failure : isFailure (failure : OracleComp spec α) = true

lemma probEvent_seq_map_prod_mk_eq_mul' :
    [λ z ↦ p z.1 ∧ q z.2 | (λ x y ↦ (y, x) : β → α → α × β) <$> ob <*> oa] = [p | oa] * [q | ob]

@[simp] lemma probOutput_ne_top : Pr[= x | mx] ≠ ∞

@[simp]
lemma liftM_append_left_eq (q : OracleQuery spec₁ α) :
    (liftM q : OracleQuery (spec₁ ++ₒ spec₂) α) =
      match q with

lemma probEvent_eq_tsum_ite (mx : m α) (p : α → Prop) [DecidablePred p] :
    Pr[p | mx] = ∑' x : α, if p x then Pr[= x | mx] else 0

lemma ite_bind (p : Prop) [Decidable p] (oa oa' : OracleComp spec α)
    (ob : α → OracleComp spec β) : ite p oa oa' >>= ob = ite p (oa >>= ob) (oa' >>= ob)

@[simp] lemma withLogging_apply {α} (so : QueryImpl spec m) (q : OracleQuery spec α) :
    so.withLogging.impl q =
      do let x ← liftM (so.impl q); tell (QueryLog.singleton q x); return x

@[simp]
lemma probEvent_toFun [superSpec.FiniteRange] [Fintype α]
    (q : OracleQuery spec α) (p : α → Prop) [DecidablePred p] :
    [p | (h.monadLift q : OracleComp superSpec α)] =
      (Finset.univ.filter p).card / Fintype.card α

@[simp] lemma probOutput_uniformOfFintype [Fintype α] (x : α) :
    [= x | $ᵗ α] = (Fintype.card α : ℝ≥0∞)⁻¹

lemma probEvent_seq_map_eq_mul {ι : Type u} {spec : OracleSpec ι}
    {α β γ : Type v} (f : α → β → γ) [spec.FiniteRange]
    (oa : OracleComp spec α) (ob : OracleComp spec β)
    (p : γ → Prop) (q1 : α → Prop) (q2 : β → Prop)
    (h : ∀ x ∈ oa.support, ∀ y ∈ ob.support, p (f x y) ↔ q1 x ∧ q2 y) :
    [p | f <$> oa <*> ob] = [q1 | oa] * [q2 | ob]

lemma probFailure_bind_congr' (oa : OracleComp spec α)
    {ob : α → OracleComp spec β} {oc : α → OracleComp spec γ}
    (h : ∀ x, [⊥ | ob x] = [⊥ | oc x]) : [⊥ | oa >>= ob] = [⊥ | oa >>= oc]

lemma probEvent_pure_eq_zero {p : α → Prop} {x : α} (h : ¬ p x) :
    [p | (pure x : OracleComp spec α)] = 0

@[simp]
lemma bind_roll (x : f α) (r : α → FreeMonad f β) (g : β → FreeMonad f γ) :
    FreeMonad.bind (FreeMonad.roll x r) g = FreeMonad.roll x (λ u ↦ FreeMonad.bind (r u) g)

@[simp]
theorem sumComm_symm :
    (sumComm P Q).symm = sumComm Q P

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)

@[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)

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

@[ext (iff := false)]
theorem ext {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (c₁ c₂ : Chart P Q)
    (h₁ : ∀ a, c₁.toFunA a = c₂.toFunA a) (h₂ : ∀ a, c₁.toFunB a = (h₁ a) ▸ c₂.toFunB a) :
    c₁ = c₂

theorem IsCoupling.none_iff {α β : Type u} {c : SPMF (α × β)} :
    IsCoupling c (failure : SPMF α) (failure : SPMF β) ↔ c = failure

theorem set_rule_backward (s' : σ) (Q : σ → Unit → σ → Prop) :
    HoareTriple (fun s => Q s () s') (set s') Q

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

@[simp] lemma evalDist_uniformSelectFinset [DecidableEq α] (s : Finset α) :
    evalDist ($ s) = if hs : s.Nonempty then
      OptionT.lift (PMF.uniformOfFinset s hs) else failure

lemma mem_finSupport_seq_map_iff_of_injective2 [spec.FiniteRange] [spec.DecidableEq]
    [DecidableEq α] [DecidableEq β] [DecidableEq γ]
    (hf : f.Injective2) (x : α) (y : β) : f x y ∈ (f <$> oa <*> ob).finSupport ↔
      x ∈ oa.finSupport ∧ y ∈ ob.finSupport

@[simp] lemma Finset.sum_boole' {ι β : Type*} [AddCommMonoid β] (r : β)
    (p) [DecidablePred p] (s : Finset ι) :
    (∑ x ∈ s, if p x then r else 0 : β) = (s.filter p).card • r

theorem get_get {α : Type u} {a : σ → σ → StateT σ m α} :
    (do let s₁ ← StateT.get; let s₂ ← StateT.get; a s₁ s₂) = (do let s ← StateT.get; a s s)

@[simp] lemma apply_eq (q : OracleQuery spec α) : loggingOracle.impl q =
    do let u ← q; tell (QueryLog.singleton q u); return u

@[simp] lemma neverFails_list_filterMapM {f : α → OracleComp spec (Option β)} {as : List α}
    (h : ∀ x ∈ as, neverFails (f x)) : neverFails (filterMapM f as)

@[simp low]
lemma finSupport_seq [spec.DecidableEq] [spec.FiniteRange]
    [DecidableEq α] [DecidableEq β] [DecidableEq (α → β)] :
    (og <*> oa).finSupport = og.finSupport.biUnion (λ g ↦ oa.finSupport.image g)

@[simp] lemma probEvent_ne_top : [p | oa] ≠ ∞

@[simp] lemma finSupport_eqRec [spec.DecidableEq] [spec.FiniteRange]
    [hα : DecidableEq α] [hβ : DecidableEq β] (oa : OracleComp spec α) (h : α = β) :
    @finSupport _ _ _ _ hβ (h ▸ oa : OracleComp spec β) =
      h.symm ▸ @finSupport _ _ _ _ hα oa

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

@[simp]
lemma snd_map_prod_mk_of_subsingleton [Subsingleton α]
    (ob : OracleComp spec β) (x : α) : snd <$> (x, ·) <$> ob = ob

@[simp]
lemma isQueryBound_failure (qb : ι → ℕ) : IsQueryBound (failure : OracleComp spec α) qb

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

lemma probFailure_bind_of_neverFails {oa : OracleComp spec α}
    (h : neverFails oa) (ob : α → OracleComp spec β) :
    [⊥ | oa >>= ob] = ∑' x : α, [= x | oa] * [⊥ | ob x]

lemma probOutput_prod_mk_eq_probEvent [spec.FiniteRange] [DecidableEq α] [DecidableEq β]
    (oa : OracleComp spec (α × β)) (x : α) (y : β) :
    [= (x, y) | oa] = [λ z ↦ z.1 = x ∧ z.2 = y | oa]

@[simp]
lemma mapM_roll (x : f α) (r : α → FreeMonad f β) :
    (FreeMonad.roll x r).mapM s = s x >>= λ u ↦ (r u).mapM s

lemma probFailure_eq_sub_sum_probOutput_map [Fintype β] (oa : OracleComp spec α) (f : α → β) :
    [⊥ | oa] = 1 - ∑ y : β, [= y | f <$> oa]

lemma depth_eq_zero_iff {x : FreeMonad f α} : depth x = 0 ↔ ∃ y, x = pure y

lemma mul_abs_of_nonpos (h : a < 0) : a * |b

@[simp] lemma support_query (q : OracleQuery spec α) :
    (q : OracleComp spec α).support = Set.univ

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

lemma query_bind_eq_roll (q : OracleQuery spec α) (ob : α → OracleComp spec β) :
    (q : OracleComp spec α) >>= ob = OptionT.mk (FreeMonad.roll q ob)

lemma eq_takeAtIndex_length_iff (seed seed' : QuerySeed spec) (i : ι) :
    seed = seed'.takeAtIndex i (seed i).length ↔
      seed' = seed.addValues ((seed' i).drop (seed i).length)

@[simp] lemma support_uniformFin (n : ℕ) : ($[0..n]).support = Set.univ

@[simp low]
lemma probOutput_eq_zero_iff : [= x | oa] = 0 ↔ x ∉ oa.support

@[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]
theorem symm_symm {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (e : P ≃ₚ Q) :
    e.symm.symm = e

lemma probFailure_bind_le_of_forall {oa : OracleComp spec α} {s : ℝ≥0∞}
    -- TODO: this should be a general type of `uniformOutput` computations
    (h' : [⊥ | oa] = s) (ob : α → OracleComp spec β) {r : ℝ≥0∞}
    (hr : ∀ x ∈ oa.support, [⊥ | ob x] ≤ r) : [⊥ | oa >>= ob] ≤ s + (1 - s) * r

lemma probEvent_seq_eq_tsum [spec.FiniteRange] (p : β → Prop) :
    [p | og <*> oa] = ∑' (g : α → β), [= g | og] * [p ∘ g | oa]

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

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

lemma getQ_singleton {α} (q : OracleQuery spec α) (u : α) (i : ι) :
    getQ (singleton q u) i = match q with

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

@[simp] lemma finSupport_query_bind [spec.FiniteRange] [Fintype α] [DecidableEq β]
    (q : OracleQuery spec α) (ob : α → OracleComp spec β) :
    (liftM q >>= ob).finSupport = Finset.univ.biUnion fun x => (ob x).finSupport

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

theorem IsCoupling.exists_bind {α₁ α₂ β₁ β₂ : Type u}
    {p : SPMF α₁} {q : SPMF α₂} {f : α₁ → SPMF β₁} {g : α₂ → SPMF β₂}
    (c : Coupling p q)
    (h : ∀ (a₁ : α₁) (a₂ : α₂), ∃ (d : SPMF (β₁ × β₂)), IsCoupling d (f a₁) (g a₂)) :
    ∃ (d : SPMF (β₁ × β₂)), IsCoupling d (p >>= f) (q >>= g) :=
  let d : (a₁ : α₁) → (a₂ : α₂) → SPMF (β₁ × β₂)

@[simp] lemma probEvent_le_one : [p | oa] ≤ 1

@[simp] lemma PerfectlyCorrect_iff (encAlg : AsymmEncAlg m M PK SK C) :
    PerfectlyCorrect encAlg ↔ ∀ (msg : M),
      [⊥ | CorrectExp encAlg msg] = 0

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

<local_ctx>
import Mathlib.Probability.ProbabilityMassFunction.Monad

import ToMathlib.General

open ENNReal

variable {α β γ : Type u} {m : Type u → Type v} [Monad m]

@[reducible] def SPMF : Type u → Type u := OptionT PMF

namespace SPMF

end SPMF

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 probOutput [HasEvalDist m] (mx : m α) (x : α) : ℝ≥0∞ := evalDist mx x

noncomputable def probEvent [HasEvalDist m] (mx : m α) (p : α → Prop) : ℝ≥0∞ :=
  (evalDist mx).run.toOuterMeasure (some '' {x | p x})

notation "Pr[=" x "|" mx "]" => probOutput mx x

notation "Pr[" p "|" mx "]" => probEvent mx p

notation "Pr[⊥" "|" mx "]" => probFailure mx

variable [HasEvalDist m]

section sums

end sums

section bounds

variable {mx : m α} {mxe : OptionT m α} {x : α} {p : α → Prop}

end bounds

section bind

variable (mx : m α) (my : α → m β)

end bind

namespace SPMF

instance hasEvalDist : HasEvalDist SPMF where
  evalDist := id
  evalDist_pure _ := rfl
  evalDist_bind _ _ := rfl

variable (p : SPMF α) (x : α)

end SPMF

namespace PMF

noncomputable instance hasEvalDist : HasEvalDist PMF where
  evalDist p := OptionT.mk p
  evalDist_pure _ := by admit /- proof elided -/

variable (p : PMF α) (x : α)
</local_ctx>

<target_theorem>
@[simp] lemma probOutput_eq : probOutput p = p :=
</target_theorem>

