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

def finSupportWhen [DecidableEq α] (oa : OracleComp spec α)
    (possible_outputs : {α : Type v} → OracleQuery spec α → Finset α) : Finset α :=

def finSupport [∀ i, Fintype (spec.range i)] [DecidableEq α] (oa : OracleComp spec α) : Finset α :=
  oa.finSupportWhen fun | query _ _ => Finset.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))

abbrev ProbComp : Type z → Type (max z 1) := OracleComp unifSpec

@[reducible, inline] def coin : OracleComp coinSpec Bool :=
  coinSpec.query () ()

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

@[reducible, inline] def uniformFin' (n m : ℕ) : OracleComp probSpec (Fin (m + 1)) :=
  probSpec.query m n

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

protected class DecidableEq (spec : OracleSpec ι) where
  domain_decidableEq' (i : ι) : DecidableEq (spec.domain i)
  range_decidableEq' (i : ι) : DecidableEq (spec.range i)

class FiniteRange (spec : OracleSpec ι) where
    range_inhabited' (i : ι) : Inhabited (spec.range i)
    range_fintype' (i : ι) : Fintype (spec.range i)

@[inline, reducible] def coinSpec : OracleSpec.{0,0} Unit := Unit →ₒ Bool

@[inline, reducible] def unifSpec : OracleSpec.{0,0} ℕ :=
  λ n ↦ (Unit, Fin (n + 1))

def probSpec : OracleSpec.{0,0} ℕ :=
  fun n => (ℕ, Fin (n + 1))

def equivFreeM : FreeMonad f α ≃ FreeContM f α where
  toFun := FreeMonad.toFreeContM
  invFun := FreeContM.toFreeMonad
  left_inv := FreeMonad.toFreeMonad_toFreeContM
  right_inv := FreeContM.toFreeContM_toFreeMonad

@[simp] instance : EmptyCollection (QuerySeed spec) := ⟨λ _ ↦ []⟩

noncomputable def unforgeableAdv.advantage
    {sigAlg : SignatureAlg (OracleComp spec) M PK SK S}
    (adv : unforgeableAdv sigAlg) : ℝ≥0∞ := [= true | unforgeableExp adv]

def oneTensor : 1 ⊗ P ≃ₚ C P.A where
  equivA := Equiv.punitProd P.A
  equivB := fun _ => Equiv.equivPEmpty _

def zeroProd : 0 * P ≃ₚ 0 where
  equivA := Equiv.pemptyProd P.A
  equivB := fun a => a.1.elim

instance : Inhabited (OracleComp spec α) := ⟨failure⟩

Or.inl in Init.Prelude

structure SecAdv {ι : Type u} [DecidableEq ι]
    (spec : OracleSpec ι) (α β : Type u) where
  run : α → OracleComp spec β
  qb : ι → ℕ
  qb_isQueryBound (x : α) : IsQueryBound (run x) (qb)
  activeOracles : List ι
  mem_activeOracles_iff (i : ι) : i ∈ activeOracles ↔ qb i ≠ 0

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

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

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

def LWE_Adversary := Matrix (Fin n) (Fin m) (Fin p) × Vector (Fin p) m → ProbComp Bool

instance [IsEmpty I] {F : I → PFunctor.{u}} : IsEmpty (sigma F).A :=

instance : MonadTransformer (StateT σ) where
  mapMonad _ := inferInstance
  transform _ := inferInstance

Id in Init.Control.Id

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

instance [IsEmpty I] {F : I → PFunctor.{u}} {a : (sigma F).A} : IsEmpty ((sigma F).B a) :=
  isEmptyElim a

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

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

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

instance : Comonad Zipper where

structure NatEquiv (m : Type u → Type v) (n : Type u → Type w) where
  toFun : {α : Type u} → m α → n α
  invFun : {α : Type u} → n α → m α
  left_inv : ∀ {α}, Function.LeftInverse (@invFun α) (@toFun α) := by admit /- proof elided -/

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 }

Option.isSome in Init.Data.Option.Basic

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

@[inline, reducible]
def singletonSpec (T U : Type v) : OracleSpec.{u,v} PUnit :=
  λ _ ↦ (T, U)

instance : Coe (QueryLog spec₂) (QueryLog (spec₁ ++ₒ spec₂)) := ⟨QueryLog.inr⟩

def idOracle : QueryImpl spec (OracleComp spec) where impl q := OracleComp.lift q

@[inline, reducible] def seededOracle [DecidableEq ι] :
    QueryImpl spec (ReaderT (QuerySeed spec) (OracleComp spec)) :=
  idOracle.withPregen

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)

HMul in Init.Prelude

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

IO.rand in Init.Data.Random

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

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

HAdd in Init.Prelude

class IsCovariant (t : (Type u → Type v) → Type u → Type w) [MonadTransformer t] where
  functorMap {m n : Type u → Type v} [MonadLiftT m n] :
    MonadLiftT (t m) (t n)

Monoid in Mathlib.Algebra.Group.Defs

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

PFunctor.B in Mathlib.Data.PFunctor.Univariate.Basic

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

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

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

def Nat.seq : ℕ → ℕ → List ℕ
  | _, 0 => []
  | n, m + 1 => n :: Nat.seq (n + 1) m

instance : FunLike (SPMF α) (Option α) ENNReal :=
  inferInstanceAs (FunLike (PMF (Option α)) (Option α) ENNReal)

modify in Init.Prelude

Set in Mathlib.Data.Set.Defs

OptionT.run in Init.Control.Option

def sumCompDistrib {R : PFunctor.{uA₃, uB₂}} :
    Lens.Equiv.{max uA₁ uA₂ uA₃ uB₂, max uB₁ uB₂, max uA₁ uA₂ uA₃ uB₂, max uB₁ uB₂}
      ((Q + R : PFunctor.{max uA₂ uA₃, uB₂}) ◃ P) ((Q ◃ P) + (R ◃ P)) where
  toLens := (fun a => match a with
              | ⟨Sum.inl qa, pf⟩ => Sum.inl ⟨qa, pf⟩
              | ⟨Sum.inr ra, pf⟩ => Sum.inr ⟨ra, pf⟩) ⇆
            (fun ⟨qr, pf⟩ b => match qr with
              | Sum.inl _ => b
              | Sum.inr _ => b)
  invLens := (fun a => match a with
              | Sum.inl ⟨qa, pf⟩ => ⟨Sum.inl qa, pf⟩
              | Sum.inr ⟨ra, pf⟩ => ⟨Sum.inr ra, pf⟩) ⇆
            (fun qprp b => match qprp with
              | Sum.inl _ => b
              | Sum.inr _ => b)
  left_inv := by admit /- proof elided -/

instance : Coe (BindEquiv m n) (BindHom m n) where
  coe f := ⟨f.toNatEquiv, f.map_bind'⟩

def oneComp : (1 : PFunctor.{uA, uB}) ◃ P ≃ₚ 1 where
  equivA := (@_root_.Equiv.uniqueSigma _ (fun i => B 1 i → P.A)
    (instUniqueAOfNat_toMathlib.{uA, uB})).trans (Equiv.pemptyArrowEquivPUnit _)
  equivB := fun _ => Equiv.equivPEmpty _

class OrderedMonad (m : Type u → Type v) extends Monad m where
  [monadOrder {α : Type u} : Preorder (m α)]
  bind_mono {α β : Type u} {ma ma' : m α} {f f' : α → m β} (ha : ma ≤ ma') (hf : ∀ a, f a ≤ f' a) :
    ma >>= f ≤ ma' >>= f'

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

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

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

CategoryTheory.NatTrans.mk in Mathlib.CategoryTheory.NatTrans

Finset.filter in Mathlib.Data.Finset.Filter

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

structure GenerableRelation
    (X W : Type) (r : X → W → Bool)
    [SelectableType X] [SelectableType W] where
  gen : ProbComp (X × W)
  gen_sound (x : X) (w : W) : (x, w) ∈ gen.support → r x w
  gen_uniform_right (x : X) : [= x | Prod.fst <$> gen] = [= x | $ᵗ X]
  gen_uniform_left (w : W) : [= w | Prod.snd <$> gen] = [= w | $ᵗ W]

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

class IsUpperClosed (m : Type u → Type v) (n : Type u → Type w) [Monad m] [OrderedMonad n]
    [MonadRelation m n] where
  monadRel_upper_closed {α} {ma : m α} {na na' : n α} (hr : ma ∼ₘ na) (hn : na ≤ₘ na') : ma ∼ₘ na'

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

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

MonadLift.monadLift in Init.Prelude

inferInstanceAs in Init.Prelude

def duplicate [Comonad f] [Comonad g] {a : Type u₃} (day : Day f g a) : Day f g (Day f g a) :=
  sorry

Finset.card in Mathlib.Data.Finset.Card

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

Stream'.zip in Mathlib.Data.Stream.Defs

instance : LawfulComonad (CofreeC F) := sorry

instance : LawfulMonadTransformer (StateT σ) where
  monad_functor := inferInstance
  liftOf_pure _ := funext fun _ => pure_bind _ _
  liftOf_bind _ _ := by admit /- proof elided -/

MonadControl.restoreM in Init.Control.Basic

protected def fst (log : QueryLog (spec₁ ++ₒ spec₂)) : QueryLog spec₁ :=
  log.filterMap (fun | ⟨.inl i, t, u⟩ => some ⟨i, t, u⟩ | _ => none)

Vector.add in Init.Data.Vector.Algebra

CategoryTheory.Category in Mathlib.CategoryTheory.Category.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)

@[simps]
def prodSumDistrib (R : PFunctor.{uA₃, uB₂}):
    (P * (Q + R) : PFunctor.{max uA₁ uA₂ uA₃, max uB₁ uB₂}) ≃ₚ
    ((P * Q) + (P * R) : PFunctor.{max uA₁ uA₂ uA₃, max uB₁ uB₂}) where
  equivA := _root_.Equiv.prodSumDistrib P.A Q.A R.A
  equivB := fun ⟨_, a⟩ =>
    Sum.casesOn a (fun _ => _root_.Equiv.refl _) (fun _ => _root_.Equiv.refl _)

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

@[simps]
def tensorComm :
    (P ⊗ Q : PFunctor.{max uA₁ uA₂, max uB₁ uB₂}) ≃ₚ
    (Q ⊗ P : PFunctor.{max uA₁ uA₂, max uB₁ uB₂}) where
  equivA := _root_.Equiv.prodComm P.A Q.A
  equivB := fun a => _root_.Equiv.prodComm (P.B a.1) (Q.B a.2)

Filter.atTop in Mathlib.Order.Filter.AtTopBot.Defs

MonadControlT in Init.Control.Basic

Fintype.ofBijective in Mathlib.Data.Fintype.OfMap

def tensorCoprodDistrib :
    Lens.Equiv.{max uA₁ uA₂ uA₃, max uB₁ uB₂, max uA₁ uA₂ uA₃, max uB₁ uB₂}
      (P ⊗ (Q + R : PFunctor.{max uA₂ uA₃, uB₂})) ((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 ⟨p, qr⟩ b => match qr with
              | Sum.inl _ => b
              | Sum.inr _ => b)
  invLens := (fun pqpr => match pqpr with
              | Sum.inl (p, q) => (p, Sum.inl q)
              | Sum.inr (p, r) => (p, Sum.inr r)) ⇆
             (fun pqpr b => match pqpr with
              | Sum.inl _ => b
              | Sum.inr _ => b)
  left_inv := by admit /- proof elided -/

def exp (P Q : PFunctor.{uA, uB}) : PFunctor.{max uA uB, max uA uB} :=
  pi (fun a => P ◃ (X + C (Q.B a)))

instance : Append (QueryLog spec) := ⟨List.append⟩

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)

structure StoreT (s : Type u₂) (w : Type u₂ → Type v₂) (a : Type u₂) where
   
  runStoreT : w (s → a)
   
  pos : s

instance {α} (a : α) : IsEmpty (B (C α) a) := inferInstanceAs (IsEmpty PEmpty)

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

Char in Init.Prelude

List.all in Init.Data.List.Basic

Array.drop in Init.Data.Array.Basic

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

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

@[simps!] def elgamalAsymmEnc (G P : Type) [SelectableType G] [SelectableType P]
    [AddGroup G] [Group P] [AddTorsor G P] : AsymmEncAlg ProbComp
    (M := P) (PK := P × P) (SK := G) (C := P × P) where
  keygen := do
    let x₀ ←$ᵗ P; let sk ←$ᵗ G
    return ((x₀, sk +ᵥ x₀), sk)
  encrypt := fun (x₀, pk) msg => do
    let g ←$ᵗ G
    return (g +ᵥ x₀, msg * (g +ᵥ pk))
  decrypt := fun sk (c₁, c₂) => do
    return c₂ / (sk +ᵥ c₁)
  __ := ExecutionMethod.default

class LawfulMonadTransformer (t) [MonadTransformer t] : Prop where
  [monad_functor {m : Type u → Type v} [Monad m] [LawfulMonad m] : LawfulMonad (t m)]
  liftOf_pure {m : Type u → Type v} [Monad m] [LawfulMonad m] {α} (x : α) :
    liftOf m (pure x) = (pure x : t m α)
  liftOf_bind {m : Type u → Type v} [Monad m] [LawfulMonad m] {α β} (x : m α) (f : α → m β) :
    liftOf (t := t) m (x >>= f) = liftOf m x >>= (fun a => liftOf m (f a))

structure forkInput (spec : OracleSpec ι) (α : Type) where
   
  main : OracleComp spec α
   
  queryBound : ι → ℕ
   
  js : List ι

List.count in Init.Data.List.Basic

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

@[inline] def bind (x : FreeContT f m α) (g : α → FreeContT f m β) :
    FreeContT f m β :=
  fun handleEff handlePure => x handleEff (fun a => g a handleEff handlePure)

class OrderedMonadLift (m : semiOutParam (Type u → Type v)) (n : Type u → Type w)
    [OrderedMonad m] [OrderedMonad n] extends MonadLift m n where
  monadLift_mono {α} : Monotone (@monadLift α)

def prepare_encrypted_message (content : String) (nonce : BitVec 256) : EncryptedMessage :=
  let (msg_bv, _) := serialize_message_data content nonce
  { ciphertext := mock_encrypt msg_bv }

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

DecidableEq in Init.Prelude

IO.userError in Init.System.IOError

liftWith_pure {α : Type u} (a : α) :
    MonadControl.liftWith (m := m) (n := n) (fun _ => pure a) = pure a

def XComp : X ◃ P ≃ₗ P where
  toLens := invTildeL
  invLens := tildeL
  left_inv := rfl
  right_inv := rfl

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

Equiv.Perm in Mathlib.Logic.Equiv.Defs

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

map_constᵣ {α β : Type u} : (mapConstᵣ : j α → f β → _) = mapᵣ ∘ (Function.const _)

Function.comp in Init.Prelude

structure SimulationData where
  verified_msg : SecretMessage
  message_package : MessagePackage
  facebook_key : BitVec 256
  deriving Repr

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

List.zip in Init.Data.List.Basic

StateT.get in Init.Control.State

protected def id (P : PFunctor.{uA, uB}) : Lens P P where
  toFunA := id
  toFunB := fun _ => id

Fintype.decidableExistsFintype in Mathlib.Data.Fintype.Defs

associator in Mathlib.Algebra.Ring.Associator

Polynomial in Mathlib.Algebra.Polynomial.Basic

class LawfulMonadFunctorT (m : Type u → Type v) (n : Type u → Type w) [Monad m] [Monad n]
    [MonadFunctorT m n] : Prop where
   
  monadMap_id {α : Type u} :
    monadMap (fun {β} => (id : m β → _)) = (id : n α → _)

String.mk in Init.Data.String.Bootstrap

structure Chart (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) where
  toFunA : P.A → Q.A
  toFunB : ∀ a, P.B a → Q.B (toFunA a)

structure Lens (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) where
  toFunA : P.A → Q.A
  toFunB : ∀ a, Q.B (toFunA a) → P.B a

instance : CoeFun (NatHom m n) (λ _ ↦ {α : Type u} → m α → n α) where
  coe f {_} x := f.toFun x

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

Array.foldrM in Init.Data.Array.Basic

Prod.fst in Init.Prelude

@[always_inline, inline, simp]
abbrev MonadTransformer.lift [MonadTransformer t] {m} [Monad m] : m α → t m α :=
  liftOf m

Asymptotics.SuperpolynomialDecay in Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

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

def pure (x : α) : HoareState (PreCondition.top σ) α (fun s a s' => s = s' ∧ a = x)
  | ⟨s, h⟩ => ⟨(x, s), by admit /- proof elided -/
  ⟩

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

class OrderedMonadLiftT (m : Type u → Type v) (n : Type u → Type w)
    [OrderedMonad m] [OrderedMonad n] extends MonadLiftT m n where
  monadLift_mono {α} : Monotone (@monadLift α)

Option in Init.Prelude

def mayFailWhen (oa : OracleComp spec α)
    (possible_outputs : {α : Type v} → OracleQuery spec α → Set α) : Prop :=
  oa.someWhen (fun _ => False) True possible_outputs

abbrev SPMF : Type u → Type u := OptionT PMF

instance : MonadTransformer (ReaderT ρ) where
  mapMonad _ := inferInstance
  transform := inferInstance

PFunctor.W in Mathlib.Data.PFunctor.Univariate.Basic

Set.univ in Mathlib.Data.Set.Defs

Vector.range in Init.Data.Vector.Basic

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

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

Function.Injective2 in Mathlib.Logic.Function.Basic

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

def head (t : CofreeC F α) : α :=
  (M.head t).1

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

protected def mapM_aux [Pure m] [Bind m] (s : {α : Type u} → f α → m α) :
    (oa : FreeMonad f α) → m α
  | .pure x => pure x
  | .roll x r => s x >>= λ u ↦ (r u).mapM_aux s

Nat in Init.Prelude

iSup in Mathlib.Order.SetNotation

Unit in Init.Prelude

instance lensCategory : Category PFunctor.{uA, uB} where
  Hom P Q := Lens P Q
  id P := Lens.id P
  comp f g := Lens.comp g f 
  id_comp _ := rfl
  comp_id _ := rfl
  assoc _ _ _ := rfl

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

Fin.castLE in Init.Data.Fin.Basic

def prodComm (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}):
    Lens.Equiv.{max uA₁ uA₂, max uB₁ uB₂, max uA₁ uA₂, max uB₁ uB₂} (P * Q) (Q * P) where
  toLens := Prod.swap ⇆ (fun _ => Sum.elim Sum.inr Sum.inl)
  invLens := Prod.swap ⇆ (fun _ => Sum.elim Sum.inr Sum.inl)
  left_inv := by admit /- proof elided -/

IO.println in Init.System.IO

Bool in Init.Prelude

alias coprod := sum

def lift (q : OracleQuery spec α) : OracleComp spec α :=
  OptionT.lift (FreeMonad.lift q)

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)

StateT.run in Init.Control.State

WithTop in Mathlib.Order.TypeTags

def MonoCont (r : Type v) [Preorder r] : Type u → Type max u v
  | α => {m : Cont r α // ∀ p p' : α → r, (∀ a, p a ≤ p' a) → m p ≤ m p'}

Functor.map in Init.Prelude

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

def IND_CPA_oracleSpec (_encAlg : AsymmEncAlg ProbComp M PK SK C) :=
  unifSpec ++ₒ (M × M →ₒ C)

decidable_of_iff' in Init.PropLemmas

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

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

instance {w d} [Monad w] [DijkstraMonad w d] [h : LawfulMonad w] [LawfulDijkstraMonad w d] :
    LawfulMonad (fun α => (w : w α) × d w) :=
  LawfulMonad.mk' _
    (by admit /- proof elided -/
      )
      
      
      
      
    (by admit /- proof elided -/
        )
    (fun x f g => by admit /- proof elided -/
      )

ContinuousAdd in Mathlib.Topology.Algebra.Monoid.Defs

modifyGet_eq : {α : Type u} → (f : σ → α × σ) →
    MonadStateOf.modifyGet (m := m) f = do let (a, s) := f (← MonadStateOf.get); set s; pure a

Vector in Init.Data.Vector.Basic

Or in Init.Prelude

def terminal {P : PFunctor.{uA, uB}} : Lens P 1 :=
  (fun _ => PUnit.unit) ⇆ (fun _ => PEmpty.elim)

instance : coinSpec.DecidableEq where
  domain_decidableEq' := inferInstance
  range_decidableEq' := inferInstance

noncomputable def IND_CPA_OneTime_Advantage (encAlg : AsymmEncAlg (OracleComp spec) M PK SK C)
    (adv : IND_CPA_Adv encAlg) : ℝ :=
  (IND_CPA_OneTime_Game (encAlg := encAlg) adv).advantage'

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

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

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

def withLogging (so : QueryImpl spec m) :
    QueryImpl spec (WriterT (QueryLog spec) m) where
  impl | q => do
    let x ← liftM (so.impl q)
    tell (QueryLog.singleton q x)
    return x

instance instExtend [Comonad w] : Extend (StoreT s w) where
  extend storet k := { runStoreT := Extend.extend storet.runStoreT (fun w'sa s' => k { runStoreT := w'sa, pos := s' }), pos := storet.pos }

@[reducible, inline] def mayFail (oa : OracleComp spec α) : Prop :=
  mayFailWhen oa fun _ => Set.univ

Matrix in Mathlib.LinearAlgebra.Matrix.Defs

Sum.map in Init.Data.Sum.Basic
</all_available_defs>

<all_available_lemmas>
lemma finSupport_def [∀ i, Fintype (spec.range i)] [DecidableEq α] (oa : OracleComp spec α) :
    oa.finSupport = oa.finSupportWhen fun

@[simp] lemma finSupportWhen_query [DecidableEq α] (q : OracleQuery spec α) :
    (q : OracleComp spec α).finSupportWhen fin_poss = fin_poss q

lemma finSupport_query [spec.FiniteRange] [DecidableEq α] (q : OracleQuery spec α) :
    (q : OracleComp spec _).finSupport = match q with

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]
lemma mapM_pure (x : α) : (FreeM.pure x : FreeM P α).mapM s = Pure.pure x

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]

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 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 run_pure [LawfulMonad m] (x : α) :
    (pure x : WriterT ω m α).run = pure (x, 1)

@[simp] lemma probFailure_uniformOfFintype : [⊥ | $ᵗ α] = 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]
theorem comp_id {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (f : Lens P Q) :
    f ∘ₗ (Lens.id P) = f

@[simp]
lemma probFailure_run_simulateQ [spec.FiniteRange] (oa : OracleComp spec α) :
    [⊥ | (simulateQ countingOracle oa).run] = [⊥ | oa]

lemma probOutput_bind_congr {oa : OracleComp spec α} {ob₁ ob₂ : α → OracleComp spec β} {y : β}
    (h : ∀ x ∈ oa.support, [= y | ob₁ x] = [= y | ob₂ x]) :
    [= y | oa >>= ob₁] = [= y | oa >>= ob₂]

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

theorem PMF.heq_iff {α β : Type u} {pa : PMF α} {pb : PMF β} (h : α = β) :
    HEq pa pb ↔ ∀ x, pa x = pb (cast h x)

@[simp] lemma C_unit : C PUnit = 1

@[simp]
lemma run_monadLift (x : m α) : (monadLift x : WriterT ω m α).run = (·, 1) <$> x

@[simp] lemma finSupport_uniformOfFintype [Fintype α] [DecidableEq α] :
    ($ᵗ α).finSupport = Finset.univ

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

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

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

lemma evalDist_lift_query [superSpec.FiniteRange] [Fintype α] [Nonempty α]
    (q : OracleQuery spec α) :
    evalDist ((q : OracleQuery superSpec α) : OracleComp superSpec α) =
      OptionT.lift (PMF.uniformOfFintype α)

@[simp]
lemma simulate_coe_append_right [AlternativeMonad m₂] [LawfulMonad m₂] [LawfulAlternative m₂]
    [LawfulMonadLift m₂ n] [LawfulAlternativeLift m₂ n] (oa : OracleComp spec₂ α) :
    simulateQ (so ++ₛₒ so') (liftM oa) = (liftM (simulateQ so' oa) : n α)

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

lemma negligible_zero : negligible 0

theorem pure_rule_forward {P : PreCondition σ} (x : α) :
    HoareTriple P (pure x) (fun s a s' => s = s' ∧ a = x ∧ P s)

@[simp]
lemma probOutput_list_mapM {α β : Type*} [spec.FiniteRange] (xs : List α)
    (f : α → OracleComp spec β) (ys : List β) : [= ys | xs.mapM f] = if ys.length = xs.length
      then (List.zipWith (fun x y => [= y | f x]) xs ys).prod else 0

@[simp]
lemma probOutput_prod_mk_snd_map' [spec.FiniteRange] (ob : OracleComp spec β)
    (f : β → γ) (x : α) (z : α × γ) :
    [= z | (x, f ·) <$> ob] = [= z.1 | (pure x : OracleComp spec α)] * [= z.2 | f <$> ob]

@[simp]
lemma probEvent_all_replicate [spec.FiniteRange] (oa : OracleComp spec α) (n : ℕ) (p : α → Bool) :
    [λ xs ↦ List.all xs p | oa.replicate n] = [λ x ↦ p x | oa] ^ n

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'

theorem map_congrᵣ [RelativeFunctor j m] {x : m α} {f g : j α → j β} (h : ∀ a, f a = g a) :
    (f <$>ᵣ x : m β) = g <$>ᵣ x

lemma probOutput_true_eq_probEvent {α} {m : Type → Type u} [Monad m] [HasEvalDist m]
    (mx : m α) (p : α → Prop) : Pr{let x ← mx}[p x] = Pr[p | mx]

@[simp]
lemma probFailure_run_simulateQ [spec.FiniteRange] (oa : OracleComp spec α) :
    [⊥ | (simulateQ loggingOracle oa).run] = [⊥ | oa]

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

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

@[simp]
lemma Fin_bound_neg {n b : ℕ} {x : Fin n} (h : Fin_Bound x b) :
  Fin_Bound (-x) b

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

@[simp] lemma finSupportWhen_pure [DecidableEq α] (x : α) :
    (pure x : OracleComp spec α).finSupportWhen fin_poss = {x}

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

@[simp]
lemma equivState_apply (q : OracleQuery spec α) :
    (so.equivState e).impl q = λ s ↦ map id e <$> so.impl q (e.symm s)

@[simp]
lemma probOutput_prod_mk_fst_map [spec.FiniteRange] (oa : OracleComp spec α) (y : β) (z : α × β) :
    [= z | (·, y) <$> oa] = [= z.1 | oa] * [= z.2 | (pure y : OracleComp spec β)]

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 mmap_seqRight [LawfulMonad m] [LawfulMonad n]
    (F : m →ᵐ n) (x : m α) (y : m β) : F (x *> y) = F x *> F y

@[simp] lemma probOutput_eq : probOutput p = p

@[simp]
lemma probOutput_prod_mk_fst_map' [spec.FiniteRange] (oa : OracleComp spec α)
    (f : α → γ) (y : β) (z : γ × β) :
    [= z | (f ·, y) <$> oa] = [= z.1 | f <$> oa] * [= z.2 | (pure y : OracleComp spec β)]

@[simp] lemma liftM_query_eq_liftM_liftM (q : OracleQuery spec α) :
    (q : OracleComp superSpec α) = ((q : OracleQuery superSpec α) : OracleComp superSpec α)

lemma probOutput_IND_CPA_experiment_eq_add {encAlg : AsymmEncAlg ProbComp M PK SK C}
    (adversary : encAlg.IND_CPA_adversary) :
    [= () | IND_CPA_experiment adversary] =
      [= () | do
        let (pk, _sk) ← encAlg.keygen
        let b ← (simulateQ (encAlg.IND_CPA_queryImpl' pk true) (adversary pk)).run' ∅
        guard b] / 2 +
      [= () | do
        let (pk, _sk) ← encAlg.keygen
        let b ← (simulateQ (encAlg.IND_CPA_queryImpl' pk false) (adversary pk)).run' ∅
        guard ¬b] / 2

@[simp] lemma support_coin : coin.support = {true, false}

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

@[simp] lemma C_B (A : Type u) (a : (C A).A) : (C A).B a = PEmpty

theorem comp_fst_snd (h : Lens.{uA₁, uB₁, max uA₂ uA₃, max uB₂ uB₃} P (Q * R)) :
    Lens.prodPair (Lens.fst ∘ₗ h) (Lens.snd ∘ₗ h) = h

@[simp]
theorem set_rule_basic (s' : σ) :
    HoareTriple (fun _ => True) (set s' : StateM σ Unit) (fun _ _ s'' => s'' = s')

@[simp]
lemma liftM_query_writerT {ω : Type v} [Monoid ω] {α : Type v} (q : OracleQuery spec α) :
  (liftM q : WriterT ω (OracleComp spec) α) = liftM (liftM q : OracleComp spec α)

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 depth_pure' {x : α} : depth (FreeMonad.pure x : FreeMonad f α) = 0

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

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

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

@[simp] theorem comonad_id_map {α : Type u} (wa : w α) : Functor.map id wa = wa

lemma probOutput_bind_eq_tsum (y : β) :
    Pr[= y | mx >>= my] = ∑' x : α, Pr[= x | mx] * Pr[= y | my x]

@[simp] lemma query_bind_ne_failure : (q : OracleComp spec β) >>= oa ≠ failure

lemma mem_support_seq_map_cons_iff (xs : List α) (h : xs ≠ []) :
    xs ∈ (List.cons <$> oa <*> ob).support ↔
      xs.head h ∈ oa.support ∧ xs.tail ∈ ob.support

@[simp]
lemma apply_eq (q : OracleQuery spec α) :
    unifOracle.impl q = match q with

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

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

theorem probFailure_fork_le :
    let acc : ℝ≥0∞ := ∑ s, [= some s | cf <$> main]
    let h : ℝ≥0∞ := Fintype.card (spec.range i)
    let q := qb i + 1
    [⊥ | fork main qb js i cf] ≤ 1 - acc * (acc / q - h⁻¹)

lemma apply_eq {α} (q : OracleQuery spec α) : randomOracle.impl q =
    match q with

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

@[simp] lemma run_lift {m : Type u → Type v} [Monad m]
    {α : Type u} (x : m α) : (OptionT.lift x).run = x

@[simp]
theorem vectorAdd_get {α : Type} {n : ℕ} [Add α] [Zero α]
 (vx : Vector α n) (vy : Vector α n)
 : (vx + vy).get = vx.get + vy.get

@[simp] lemma toExecutionMethod_eq (n : ℕ) :
    (oneTimePad n).toExecutionMethod = ExecutionMethod.default

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

theorem monadLift_optional [AlternativeMonad m] [AlternativeMonad n]
    [LawfulMonad m] [LawfulMonad n] [MonadLift m n] [LawfulAlternativeLift m n]
    [LawfulMonadLift m n]
    (x : m α) : monadLift (optional x) = optional (monadLift x : n α)

@[simp]
lemma probEvent_seq_map_swap [spec.FiniteRange] (p : γ → Prop) :
    [p | Function.swap f <$> ob <*> oa] = [p | f <$> oa <*> ob]

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

@[simp]
lemma addValues_nil {i : ι} (seed : QuerySeed spec) : seed.addValues (i := i) [] = seed

@[simp]
lemma probOutput_generateSeed_bind_map_simulateQ {ι : Type _} {spec : OracleSpec ι}
    {α β : Type _} [DecidableEq ι]
    [∀ i, SelectableType (spec.range i)] [unifSpec ⊂ₒ spec] [spec.FiniteRange]
    (qc : ι → ℕ) (js : List ι)
    (oa : OracleComp spec α) (f : α → β) (y : β) :
    [= y | do
      let seed ← liftComp (generateSeed spec qc js) spec
      f <$> (simulateQ seededOracle oa).run seed] = [= y | f <$> oa]

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

lemma negligible_of_zero {f : ℕ → ℝ≥0∞} (hf : ∀ n, f n = 0) : negligible f

lemma isQueryBound_iff_probEvent [spec.FiniteRange] {oa : OracleComp spec α} {qb : ι → ℕ} :
    IsQueryBound oa qb ↔
      [(· ≤ qb) | snd <$> (simulateQ countingOracle oa).run <|> return 0] = 1

@[simp] -- mathlib?
lemma vector_eq_nil {α : Type*} (xs : List.Vector α 0) : xs = Vector.nil

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

@[simp] lemma monoid_one_def : (1 : QueryLog spec) = List.nil

@[simp]
lemma fst_map_prod_mk_of_subsingleton [Subsingleton β]
    (oa : OracleComp spec α) (y : β) : fst <$> (·, y) <$> oa = oa

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

theorem comp_inl_inr (h : Lens.{max uA₁ uA₂, uB₁, uA₃, uB₃} (P + Q) R) :
    Lens.sumPair (h ∘ₗ Lens.inl) (h ∘ₗ Lens.inr) = h

lemma Function.injective2_swap_iff {α β γ : Type*} (f : α → β → γ) :
    (Function.swap f).Injective2 ↔ f.Injective2

lemma probOutput_seq_eq_sum_finSupport_ite [spec.FiniteRange] [spec.DecidableEq]
    [DecidableEq α] [DecidableEq (α → β)] [DecidableEq β]
    (y : β) : [= y | og <*> oa] = ∑ g ∈ og.finSupport, ∑ x ∈ oa.finSupport,
      if y = g x then [= g | og] * [= x | oa] else 0

protected lemma pure_def (x : α) : (pure x : OracleComp spec α) = OptionT.pure x

@[simp]
lemma probFailure_orElse {ι : Type u} {spec : OracleSpec ι} {α : Type u} [h : spec.FiniteRange]
    (oa oa' : OracleComp spec α) : [⊥ | oa <|> oa'] = [⊥ | oa] * [⊥ | oa']

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

@[simp]
lemma neverFails_query_bind_iff {q : OracleQuery spec α} {oa : α → OracleComp spec β} :
    (liftM q >>= oa).neverFails ↔ ∀ x, neverFails (oa x)

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

@[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 probEvent_liftComp [spec.FiniteRange] [superSpec.FiniteRange]
    (oa : OracleComp spec α) (p : α → Prop) [DecidablePred p] :
    [p | liftComp oa superSpec] = [p | oa]

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

@[simp]
lemma bind_lift (x : f α) (r : α → FreeMonad f β) :
    FreeMonad.bind (FreeMonad.lift x) r = FreeMonad.roll x r

@[simp] lemma apply_eq (q : OracleQuery spec α) : idOracle.impl q = q

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

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

@[simp]
lemma mapM'_lift [Monad m] [LawfulMonad m]
    (s : {α : Type u} → f α → m α) (x : f α) :
    FreeMonad.mapM' m s (FreeMonad.lift x) = s x

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

@[simp] theorem monadLift_mono' {m n} [OrderedMonad m] [OrderedMonad n] [OrderedMonadLiftT m n]
    {α} {a b : m α} (h : a ≤ₘ b) : monadLift a ≤ₘ (monadLift b : n α)

lemma ProbComp.advantage₂_comm (p q : ProbComp Unit) : p.advantage₂ q = q.advantage₂ p

@[simp]
lemma finSupport_seq_map_swap [spec.FiniteRange] [spec.DecidableEq] [DecidableEq γ] :
    (Function.swap f <$> ob <*> oa).finSupport = (f <$> oa <*> ob).finSupport

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

@[simp] lemma failure_ne_query_bind : failure ≠ (q : OracleComp spec β) >>= oa

lemma map_ite (oa₁ oa₂ : OracleComp spec α) (f : α → β) (p : Prop) [Decidable p] :
    f <$> (if p then oa₁ else oa₂) = if p then (f <$> oa₁) else (f <$> oa₂)

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

@[simp]
lemma run_mk {ω : Type u} [LawfulMonad m] (x : m (α × ω)) :
  (WriterT.mk x).run = x

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

@[simp] lemma selfMonomial_unit : selfMonomial PUnit = X

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

noncomputable def probFailure (oa : OracleComp spec α) : ℝ≥0∞ :=
  (evalDist oa).run none

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

end mul_le_probEvent_bind

section bind_const

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

end bind_const

section query

variable (i : ι) (t : spec.domain i)

end query

section failure

end failure

section map

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

end map

section neverFails

end neverFails

section unit

end unit

section bool

end bool

section eqRec

variable (oa : OracleComp spec α) (h : α = β)

end eqRec

section ite

variable (p : Prop) [Decidable p] (oa oa' : OracleComp spec α)

end ite

section coin

end coin

section uniformFin

variable (n : ℕ)
</local_ctx>

<target_theorem>
@[simp]
lemma probEvent_uniformFin (p : Fin (n + 1) → Prop) [DecidablePred p] :
    [p | $[0..n]] = (Finset.univ.filter p).card * (n + 1 : ℝ≥0∞)⁻¹ :=
</target_theorem>

