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 α

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)

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

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

deriving Repr, DecidableEq

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

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

LawfulMonad in Init.Control.Lawful.Basic

def LWE_Uniform_Distr : ProbComp (Matrix (Fin n) (Fin m) (Fin p) × Vector (Fin p) m) := do
  let A ←$ᵗ Matrix (Fin n) (Fin m) (Fin p)
  let u ←$ᵗ Vector (Fin p) m
  return (A, u)

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

def defaultOutput [∀ i, Inhabited (spec.range i)] : (q : OracleQuery spec α) → α
  | query i t => default

instance : Extract Zipper where
  extract := extract

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

def replicate {ι : Type u} {spec : OracleSpec ι} {α : Type v}
    (n : ℕ) (oa : OracleComp spec α) : OracleComp spec (List α) :=
  (List.replicate n ()).mapM fun () => oa

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

pure_bindᵣ {α β : Type u} (x : j α) (f : j α → m β) :
    (pureᵣ x) >>=ᵣ f = f x

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

instance : CoseqLeft Stream' where
  coseqLeft s₁ _ := s₁

instance : OracleSpec.DecidableEq []ₒ where
  domain_decidableEq' := inferInstance
  range_decidableEq' := inferInstance

class LawfulCoapplicative (w : Type u → Type v) [Coapplicative w] extends LawfulFunctor w where
   
  coseqLeft_eq : ∀ {α β : Type u} (wa : w α) (wb : w β),
    @coseqLeft w _ α β wa wb = Functor.map (@Prod.fst α β) (coseq wa wb)
   
  coseqRight_eq : ∀ {α β : Type u} (wa : w α) (wb : w β),
    coseqRight wa wb = Functor.map (@Prod.snd α β) (coseq wa wb)
   
  coseq_assoc : ∀ {α β γ : Type u} (wa : w α) (wb : w β) (wc : w γ),
    Functor.map (Equiv.prodAssoc α β γ) (coseq (coseq wa wb) wc) = coseq wa (coseq wb wc)

Vector.zero in Init.Data.Vector.Algebra

def zipCommits (sk : G) (gs : Vector G n)
    (bs : Vector Bool n) : Vector G n :=
  Vector.zipWith (λ c b ↦ if b then c else c + sk) gs bs

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

Seq in Init.Prelude

def FreeMonad.toFreeContM : FreeMonad f α → FreeContM f α :=
  fun x => match x with
    | FreeMonad.pure a => fun _ handlePure => handlePure a
    | FreeMonad.roll x k => fun handleEff handlePure =>
      handleEff x (fun a => FreeMonad.toFreeContM (k a) handleEff handlePure)

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)

FunLike in Mathlib.Data.FunLike.Basic

instance {m} [OrderedMonad m] : OrderedMonadLiftT m m where
  monadLift_mono h := by admit /- proof elided -/

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

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

Monotone in Mathlib.Order.Monotone.Defs

instance : FiniteRange []ₒ where
  range_inhabited' := inferInstance
  range_fintype' := inferInstance

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

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

class MonadRelationHom (m₁ : Type u → Type v₁) (n₁ : Type u → Type w₁)
    (m₂ : Type u → Type v₂) (n₂ : Type u → Type w₂) where
  monadRelHomFst {α : Type u} : m₁ α → m₂ α
  monadRelHomSnd {α : Type u} : n₁ α → n₂ α

instance : Extend NonEmptyList where
  extend s f := NonEmptyList.map f (NonEmptyList.tails s)

inductive FreeM (P : PFunctor.{uA, uB}) : Type v → Type (max uA uB v)
  | pure {α} (x : α) : FreeM P α
  | roll {α} (a : P.A) (r : P.B a → FreeM P α) : FreeM P α
deriving Inhabited

OptionT.mk in Init.Control.Option

MonadLiftT in Init.Prelude

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

PMF.instMonad in Mathlib.Probability.ProbabilityMassFunction.Monad

def signingOracle (sigAlg : SignatureAlg m M PK SK S) (pk : PK) (sk : SK) :
    QueryImpl (M →ₒ S) (WriterT (QueryLog (M →ₒ S)) m) :=
  QueryImpl.withLogging ⟨fun | query () msg => sigAlg.sign pk sk msg⟩

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

def zip : NonEmptyList α → NonEmptyList β → NonEmptyList (α × β)
  | ⟨h₁, t₁⟩, ⟨h₂, t₂⟩ => ⟨(h₁, h₂), List.zip t₁ t₂⟩

def ofList [DecidableEq ι] {i : ι} (xs : List (spec.range i)) : QuerySeed spec :=
  fun j => if h : i = j then h ▸ xs else []

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

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

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

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

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

instance : Monad (FreeM P) where
  pure := FreeM.pure
  bind := FreeM.bind

def sumComm (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) :
    Lens.Equiv.{max uA₁ uA₂, uB, max uA₁ uA₂, uB} (P + Q) (Q + P) where
  toLens := Lens.sumPair Lens.inr Lens.inl
  invLens := Lens.sumPair Lens.inr Lens.inl
  left_inv := by admit /- proof elided -/

Stream'.drop in Mathlib.Data.Stream.Defs

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

instance instLawfulCoapplicative [Comonad w] [LawfulCoapplicative w] : LawfulCoapplicative (StoreT s w) where
  coseqLeft_eq := sorry 
  coseqRight_eq := sorry 
  coseq_assoc := sorry

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

def HoareState (P : PreCondition σ) (α : Type*) (Q : PostCondition σ α) :=
  ∀ s : {s : σ // P s}, {result : α × σ // Q s result.1 result.2}

MonadFunctor.monadMap in Init.Prelude

IO in Init.System.IO

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

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

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

class RelativeMonadMorphism (r₁ : Type u → Type v₁) (m₁ : Type u → Type v₁)
    (r₂ : Type u → Type v₂) (m₂ : Type u → Type v₂)
    [RelativeMonad r₁ m₁] [RelativeMonad r₂ m₂] where
  r₁₂ : Type v₁ → Type v₂
  [instFunctor : Functor r₁₂]
  φ : MonadIso r₂ (r₁₂ ∘ r₁)
  mmapᵣ {α : Type u} : r₁₂ (m₁ α) → m₂ α
  mmapᵣ_pureᵣ {α} :
    mmapᵣ ∘ (Functor.map (f := r₁₂) (@pureᵣ r₁ m₁ _ α)) = pureᵣ ∘ φ.invLift.monadLift
  mmapᵣ_bindᵣ {α β : Type u} (f : r₁ α → m₁ β) :
    mmapᵣ ∘ (Functor.map (f := r₁₂) (bindᵣ · f)) =
      (· >>=ᵣ mmapᵣ ∘ Functor.map (f := r₁₂) f ∘ φ.toLift.monadLift) ∘ mmapᵣ

@[reducible, inline]
def CorrectExp (encAlg : AsymmEncAlg m M PK SK C) (msg : M) :
    ProbComp Unit := encAlg.exec do
  let (pk, sk) ← encAlg.keygen
  guard (encAlg.decrypt sk (← encAlg.encrypt pk msg) = msg)

alias coprod := sum

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

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

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

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

def instSeqOfRelativeMonadOfSeq {j : Type u → Type w} [Seq j] {m : Type u → Type v}
    [RelativeMonad j m] : Seq m where
  seq f x := bindᵣ (j := j) (m := m) f (fun y => mapᵣ (y <*> ·) (x ()))

instance {P : PreCondition σ} {x : α} :
    Inhabited (StrongestPostcondition P (pure x : StateM σ α)) where
  default := ⟨fun s a s' => s = s' ∧ a = x ∧ P s, HoareTriple.pure_rule_forward x,
    fun y hP hy => by admit /- proof elided -/
    ⟩

structure unforgeableAdv (_sigAlg : SignatureAlg (OracleComp spec) M PK SK S) where
  main (pk : PK) : OracleComp (spec ++ₒ (M →ₒ S)) (M × S)

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

class LawfulDijkstraMonad (w : Type u → Type v) (d : {α : Type u} → w α → Type z) [Monad w]
    [LawfulMonad w] [DijkstraMonad w d] where
  dPure_dBind {α β} {f : α → w β} (x : α) (g : (a : α) → d (f a)) :
    (pure_bind x f) ▸ (dPure x >>=ᵈ g) = g x
  dBind_dPure {α} {a : w α} (x : d a) :
    (bind_pure a) ▸ (x >>=ᵈ dPure) = x
  dBind_assoc {α β γ} {a} {f : α → w β} {g : β → w γ} (x : d a)
    (f' : (a : α) → d (f a)) (g' : (b : β) → d (g b)) :
      (bind_assoc a f g) ▸ ((x >>=ᵈ f') >>=ᵈ g') = x >>=ᵈ (fun a => f' a >>=ᵈ g')

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

def Hybrid_01_Reduction : LWE_Adversary n m p := fun Au => do
  let b ←$ᵗ Bool
  let ⟨m₁, m₂, st⟩ ← adv.chooseMessages Au
  let c ← if b then (uniformRegevAsymmEnc n m p χ he).encrypt Au m₁
  else (uniformRegevAsymmEnc n m p χ he).encrypt Au m₂
  let b' ← adv.distinguish st c
  return b'

EmptyCollection in Init.Core

Append in Init.Prelude

def toNatHom (e : NatEquiv m n) : NatHom m n where
  toFun := e.toFun

@[refl]
def refl (P : PFunctor.{uA, uB}) : P ≃ₗ P :=
  ⟨Lens.id P, Lens.id P, rfl, rfl⟩

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

def compX : P ◃ X ≃ₗ P where
  toLens := invTildeR
  invLens := tildeR
  left_inv := rfl
  right_inv := rfl

bind_pure_compᵣ {α β : Type u} (f : j α → j β) (x : m α) :
    x >>=ᵣ (fun y => pureᵣ (f y)) = f <$>ᵣ x

def PFunctor.FreeContT (P : PFunctor.{z, y}) (m : Type u → Type v) (α : Type w) :
    Type (max (u + 1) v w y z) :=
  {r : Type u} → ((a : P.A) → ContT r m (P.B a)) → ContT r m α

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

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

def selfMonomial (S : Type uA) : PFunctor.{uA, uA} :=
  S X^ S

List.zip in Init.Data.List.Basic

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 }

TopologicalSpace in Mathlib.Topology.Defs.Basic

def extend (f : CofreeC F α → α) (t : CofreeC F α) : α :=
  f t

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

modifyThe in Init.Prelude

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

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

CategoryTheory.inv in Mathlib.CategoryTheory.Iso

def serialize_message_data (msg : String) (nonce : BitVec 256) : BitVec 256 × BitVec 256 :=
  let msg_bv := string_to_bitvec msg
  (msg_bv, nonce)

Computation in Mathlib.Data.Seq.Computation

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

CategoryTheory.NatTrans.mk in Mathlib.CategoryTheory.NatTrans

def piUnit {P : PFunctor.{u}} : pi (fun (_ : PUnit) => P) ≃ₗ P where
  toLens := (fun f => f PUnit.unit) ⇆ (fun _ pb => ⟨PUnit.unit, pb⟩)
  invLens := (fun pa _ => pa) ⇆ (fun _ spb => spb.2)
  left_inv := rfl
  right_inv := rfl

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

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

instance : Extend Zipper where
  extend z f := map f (duplicate z)

Decidable.isFalse in Init.Prelude

instance {T U : Type v} [DecidableEq T] [DecidableEq U] : (T →ₒ U).DecidableEq where
  domain_decidableEq' := inferInstance
  range_decidableEq' := inferInstance

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

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

def toLensEquiv (e : P ≃ₚ Q) : P ≃ₗ Q where
  toLens := e.equivA ⇆ (fun a => (e.equivB a).symm)
  invLens := e.symm.equivA ⇆ (fun a => (e.symm.equivB a).symm)
  left_inv := by admit /- proof elided -/

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

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

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

PMF in Mathlib.Probability.ProbabilityMassFunction.Basic

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

HMul.hMul in Init.Prelude

Fin.castLE in Init.Data.Fin.Basic

Vector.ofFn in Init.Data.Vector.Basic

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)

PMF.uniformOfFintype in Mathlib.Probability.Distributions.Uniform

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

def tensorMap {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 ⟨pa, qa⟩ => (l₁.toFunA pa, l₂.toFunA qa)) ⇆
    (fun ⟨_pa, qa⟩ ⟨rb, wb⟩ => (l₁.toFunB _pa rb, l₂.toFunB qa wb))

def mock_hmac_sha256 (key : BitVec 256) (data : BitVec 256) : mock_hmac_sha256_out_type :=
  "HMAC_SHA256_OUT(" ++ bitvec_to_string key  ++ "," ++ bitvec_to_string data ++ ")"

class SubSpec (spec : OracleSpec.{u,w} ι) (superSpec : OracleSpec τ)
  extends MonadLift (OracleQuery spec) (OracleQuery superSpec) where

ULift.down in Init.Prelude

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

structure MonadHom (m : Type u → Type v) [Pure m] [Bind m]
    (n : Type u → Type w) [Pure n] [Bind n] extends NatHom m n, PureHom m n, BindHom m n

CategoryTheory.Bundled in Mathlib.CategoryTheory.ConcreteCategory.Bundled

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

Monoid in Mathlib.Algebra.Group.Defs

MonadControl.liftWith in Init.Control.Basic

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

One.one in Init.Prelude

NeZero in Init.Data.NeZero

instance [MonadTransformer t] [Monad m] [LawfulMonad m] [LawfulMonadTransformer t]
    : LawfulMonadLift m (t m) where
  monadLift_pure := LawfulMonadTransformer.liftOf_pure
  monadLift_bind := LawfulMonadTransformer.liftOf_bind

def compAssoc : (P ◃ Q) ◃ R ≃ₗ P ◃ (Q ◃ R) where
  toLens := (fun ⟨⟨pa, qf⟩, rf⟩ => ⟨pa, fun pb => ⟨qf pb, fun qb => rf ⟨pb, qb⟩⟩⟩) ⇆
            (fun _ ⟨pb, ⟨qb, rb⟩⟩ => ⟨⟨pb, qb⟩, rb⟩)
  invLens := (fun ⟨pa, g⟩ => ⟨⟨pa, fun pb => (g pb).1⟩, fun ⟨pb, qb⟩ => (g pb).2 qb⟩) ⇆
             (fun _ ⟨⟨pb, qb⟩, rb⟩ => ⟨pb, ⟨qb, rb⟩⟩)
  left_inv := rfl
  right_inv := rfl

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

instance : Zero PFunctor.{uA, uB} where
  zero := ⟨PEmpty, fun _ => PEmpty⟩

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

instance : LawfulCoapplicative (Prod ε) where
  
  coseqLeft_eq := by admit /- proof elided -/

CharP in Mathlib.Algebra.CharP.Defs

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

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

instance isEmpty : IsEmpty (OracleQuery []ₒ α) where false | query i t => i.elim

def piPUnit (P : PFunctor.{uA, uB}) :
    pi (fun (_ : PUnit) => P) ≃ₚ P where
  equivA := sorry
  equivB := sorry

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

Fintype.card in Mathlib.Data.Fintype.Card

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

instance : Comonad NonEmptyList where

Nonempty in Init.Prelude

alias PKE_Alg := AsymmEncAlg

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

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

Fin.val in Init.Prelude

def countingOracle : QueryImpl spec (WriterT (QueryCount spec) (OracleComp spec)) :=
  idOracle.withCounting

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

instance : LawfulFunctor NonEmptyList where
  id_map := 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 (n : ℕ) : SelectableType (Fin (n + 1)) where
  selectElem := $[0..n]
  mem_support_selectElem := by admit /- proof elided -/

MonadLift.monadLift in Init.Prelude

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

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

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

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

def sumCompDistrib (Q : PFunctor.{uA₂, uB₁}) :
    (P + Q : PFunctor.{max uA₁ uA₂, uB₁}) ◃ R ≃ₚ
    ((P ◃ R) + (Q ◃ R) : PFunctor.{max uA₁ uA₂ uA₃ uB₁, max uB₁ uB₃}) where
  equivA := sorry
  equivB := sorry

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

protected class Fintype (P : PFunctor.{uA, uB}) where
  fintype_B : ∀ a, Fintype (P.B a)

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

Array.filterMapM in Init.Data.Array.Basic

get_set : {s : σ} → (do set (m := m) s; MonadStateOf.get) = do set s; pure s

String.mk in Init.Data.String.Bootstrap

Classical.decPred in Mathlib.Logic.Basic

guard in Init.Control.Basic

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

def liftComp (oa : OracleComp spec α) (superSpec : OracleSpec τ)
      [h : MonadLift (OracleQuery spec) (OracleQuery superSpec)] :
      OracleComp superSpec α := simulateQ ⟨liftM⟩ oa

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

Alternative in Init.Control.Basic

Function.const in Init.Prelude

ExceptT in Init.Control.Except

DFunLike in Mathlib.Data.FunLike.Basic
</all_available_defs>

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

@[simp]
theorem modifyGetThe_eq [MonadStateOf σ m] {α : Type u} (f : σ → α × σ) :
    modifyGetThe σ (m := m) f = MonadStateOf.modifyGet f

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

@[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 probFailure_writerT_run_simulateQ [spec.FiniteRange]
    {so : QueryImpl spec (WriterT ω (OracleComp spec))}
    (hso : ∀ {α}, ∀ q : OracleQuery spec α, fst <$> (so.impl q).run = q)
    (hso' : ∀ {α}, ∀ q : OracleQuery spec α, [⊥ | (so.impl q).run] = 0)
    (oa : OracleComp spec α) : [⊥ | (simulateQ so oa).run] = [⊥ | oa]

@[simp]
lemma takeAtIndex_length (seed : QuerySeed spec) (i : ι) :
    seed.takeAtIndex i (seed i).length = seed

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

@[simp] lemma probEvent_eq : probEvent p = p.run.toOuterMeasure ∘ Set.image some

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

lemma depth_eq_one_iff {x : FreeMonad f α} : depth x = 1 ↔
    (∃ (β : Type u) (y : f β) (r : β → FreeMonad f α), x = roll y r ∧ ∀ u, depth (r u) = 0)

@[simp] lemma probOutput_lt_top : [= x | oa] < ∞

@[simp]
lemma mapM_query_bind (q : OracleQuery spec α) (ob : α → OracleComp spec β) :
    ((q : OracleComp spec α) >>= ob).mapM fail qm =
      (do let x ← qm q; (ob x).mapM fail qm)

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

@[simp] lemma simulateQ_comp_pure_comp (f : α → β) : simulateQ so ∘ pure ∘ f = pure ∘ f

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

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

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

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

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

@[simp]
lemma liftComp_bind (oa : OracleComp spec α) (ob : α → OracleComp spec β) :
    liftComp (oa >>= ob) superSpec =
      liftComp oa superSpec >>= λ x ↦ liftComp (ob x) superSpec

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

theorem 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 supportWhen_query (q : OracleQuery spec α) :
    (q : OracleComp spec α).supportWhen poss = poss q

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

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

@[simp]
lemma mapM_roll (x : P.A) (r : P.B x → FreeM P α) :
    (FreeM.roll x r).mapM s = s x >>= λ u ↦ (r u).mapM s

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

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

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

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

@[simp] lemma probEvent_le_one : Pr[p | mx] ≤ 1

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

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

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

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

lemma mem_finSupport_iff_mem_support (x : α) : x ∈ oa.finSupport ↔ x ∈ oa.support

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

@[simp]
lemma probOutput_bitVec_ofFin_map {n : ℕ} (oa : OracleComp spec (Fin (2 ^ n)))
    (x : BitVec n) : [= x | ofFin <$> oa] = [= toFin x | oa]

@[simp]
theorem head_tails_eq (s : NonEmptyList α) : (tails s).head = s

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 monad_bind_def (x : FreeM P α) (g : α → FreeM P β) :
    x >>= g = FreeM.bind x g

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

@[simp] lemma isFailure_pure : isFailure (pure x : OracleComp spec α) = false

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

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

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

@[simp] lemma probOutput_eq : probOutput p = p

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

lemma probOutput_bind_eq_sum_fintype [Fintype α] (y : β) :
    [= y | oa >>= ob] = ∑ x : α, [= x | oa] * [= y | ob x]

@[simp]
lemma monad_pure_def (x : α) : (pure x : FreeMonad f α) = FreeMonad.pure x

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

@[simp] lemma probOutput_lt_top : Pr[= x | mx] < ∞

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

theorem bind_congrᵣ [RelativeBind j m] {x : m α} {f g : j α → m β} (h : ∀ a, f a = g a) :
    x >>=ᵣ f = x >>=ᵣ g

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 liftM_of_liftM_eq [MonadLift m m'] (x : StateT σ m α) :
    (liftM x : StateT σ m' α) = StateT.mk fun s => liftM (x.run s)

lemma List.card_filter_getElem_eq {α : Type*} [DecidableEq α]
    (xs : List α) (x : α) :
    (Finset.filter (λ i : Fin (xs.length) ↦ xs[i] = x) Finset.univ).card =
      xs.count x

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

@[simp]
lemma bitvec_to_string_to_bitvec (bv : BitVec 256) :
    string_to_bitvec (bitvec_to_string bv) = bv

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

@[simp]
lemma construct_roll (q : OracleQuery spec β) (oa : β → OracleComp spec α) :
    (OracleComp.construct h_pure h_query_bind h_failure (OptionT.mk (FreeMonad.roll q oa)) :
      C (OptionT.mk (FreeMonad.roll q oa))) = h_query_bind q oa
        (λ u ↦ (oa u).construct h_pure h_query_bind h_failure)

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

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

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

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

@[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 probEvent_congr {oa : OracleComp spec α} {oa' : OracleComp spec' α}
    (h1 : ∀ x, p x ↔ q x) (h2 : evalDist oa = evalDist oa') : [p | oa] = [q | oa']

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

@[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 low]
lemma probOutput_eq_zero_iff : [= x | oa] = 0 ↔ x ∉ oa.support

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

lemma probEvent_def (mx : m α) (p : α → Prop) :
    Pr[p | mx] = (evalDist mx).run.toOuterMeasure (some '' {x | p x})

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

@[simp]
lemma construct_pure (y : α) : FreeMonad.construct h_pure h_roll (pure y) = h_pure y

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

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

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

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

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

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

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

@[simp]
theorem fst_comp_prodPair (f : Lens P Q) (g : Lens P R) :
    Lens.fst ∘ₗ Lens.prodPair f g = f

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

@[simp]
lemma liftM_query_stateT {σ : Type v} {α : Type v} (q : OracleQuery spec α) :
  (liftM q : StateT σ (OracleComp spec) α) = liftM (liftM q : OracleComp spec α)

@[simp]
lemma evalDist_query (i : ι) (t : spec.domain i) : evalDist (query i t : OracleComp spec _) =
    OptionT.lift (PMF.uniformOfFintype (spec.range i))

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)

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 Fin_Bound_mul {n b₁ b₂ : ℕ} {x y : Fin n} (h₁ : Fin_Bound x b₁)
 (h₂ : Fin_Bound y b₂) : Fin_Bound (x * y) (b₁ * b₂)

lemma neverFails_eq_freeMonad_construct (oa : OracleComp spec α) :
    oa.neverFails = FreeMonad.construct
      (fun t ↦ Option.rec False (fun _ ↦ True) t) (fun _ _ r ↦ ∀ x, r x) oa

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

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

@[simp]
lemma mem_finSupport_replicate [spec.FiniteRange] [spec.DecidableEq] [DecidableEq α]
    (oa : OracleComp spec α) (n : ℕ)
    (xs : List α) : xs ∈ (oa.replicate n).finSupport ↔
      xs.length = n ∧ xs.all (· ∈ oa.finSupport)

@[simp] lemma evalDist_uniformSelectList (xs : List α) : evalDist ($ xs) =
    match xs with

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

@[simp]
lemma probOutput_liftComp [spec.FiniteRange] [superSpec.FiniteRange]
    (oa : OracleComp spec α) (x : α) : [= x | liftComp oa superSpec] = [= x | oa]

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

theorem bind_comm_triple_swap_12 {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)) =
    (do let b ← mb; let a ← ma; let c ← mc; f (a, b, c))

lemma probFailure_seq [spec.FiniteRange] :
    [⊥ | og <*> oa] = [⊥ | og] + [⊥ | oa] - [⊥ | og] * [⊥ | oa]

@[simp] lemma isPure_failure : isPure (failure : OracleComp spec α) = false

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

lemma relax_p_bound {p χ m: ℕ} [hm : NeZero m] (h : p > 4 * (χ * m + 1)) : p > 2 * χ

@[simp low]
lemma support_seq : (og <*> oa).support = ⋃ g ∈ og.support, g '' oa.support

theorem Hybrid_1_ind_Hybrid_2 :
    (Hybrid_1 adv).advantage' ≤ (Hybrid_2 adv).advantage'
      + (LHL_Consequence_Advantage (m := m) (Hybrid_12_Reduction adv))

@[simp] lemma neverFails_lift_comp_iff (oa : OracleComp spec α) :
    (liftComp oa superSpec).neverFails ↔ oa.neverFails

theorem pure_rule_backward {Q : PostCondition σ α} (x : α) :
    HoareTriple (fun s => Q s x s) (pure x) Q

@[simp]
lemma snd_map_prod_map (oa : OracleComp spec (α × β)) (f : α → γ) (g : β → δ) :
    snd <$> map f g <$> oa = (g ∘ Prod.snd) <$> oa

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

@[simp]
lemma probOutput_bind_bind_prod_mk_eq_mul' [spec.FiniteRange] (oa : OracleComp spec α)
    (ob : OracleComp spec β) (f : α → γ) (g : β → δ) (x : γ) (y : δ) :
    [= (x, y) | do let x ← oa; let y ← ob; return (f x, g y)] =
      [= x | f <$> oa] * [= y | g <$> ob]

@[simp]
lemma probOutput_list_mapM_loop {α β : Type*} [DecidableEq β] [spec.FiniteRange]
    (xs : List α) (f : α → OracleComp spec β) (ys : List β)
    (zs : List β) : [= zs | List.mapM.loop f xs ys] =
      if zs.length = xs.length + ys.length ∧ zs.take ys.length = ys.reverse
      then (List.zipWith (λ x z ↦ [= z | f x]) xs (zs.drop ys.length)).prod else 0

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

lemma Fintype.sum_inv_card (α : Type*) [Fintype α] [Nonempty α] :
  Finset.sum Finset.univ (λ _ ↦ (Fintype.card α)⁻¹ : α → ℝ≥0∞) = 1

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

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]
theorem ulift_B {a : P.A} : (P.ulift).B (ULift.up a) = ULift (P.B a)

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

lemma probOutput_bind_eq_tsum (y : β) :
    [= y | oa >>= ob] = ∑' x : α, [= x | oa] * [= y | ob x]

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

@[simp] lemma tsum_probOutput_ne_top : ∑' x : α, Pr[= x | mx] ≠ ⊤

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

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

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

@[simp] lemma support_map_prod_map_fork : (Prod.map cf cf <$> main.fork qb js i cf).support =
    (fun s => (s, s)) '' (cf <$> main).support

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

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

@[simp]
theorem get_rule_basic :
    HoareTriple (fun _ => True) (get : StateM σ σ) (fun s x s' => s = x ∧ s = s')

@[ext]
protected lemma ext (seed₁ seed₂ : QuerySeed spec) (h : ∀ i, seed₁ i = seed₂ i) : seed₁ = seed₂

@[simp]
lemma BitVec.xor_xor_cancel_right {n : ℕ} (bv1 bv2 : BitVec n) :
    bv1 ^^^ bv2 ^^^ bv2 = bv1

@[simp] lemma C_unit : C PUnit = 1
</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 β)
</local_ctx>

<target_theorem>
lemma probFailure_bind_eq_sub_mul {oa : OracleComp spec α} {ob : α → OracleComp spec β}
    (r : ℝ≥0∞) (h : ∀ x, [⊥ | ob x] = r) :
    [⊥ | oa >>= ob] = 1 - (1 - [⊥ | oa]) * (1 - r) :=
</target_theorem>

