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

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

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

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

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

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

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

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

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

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

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

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

open Set
open Mathlib
open SetRel

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

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

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

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

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

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

@[simp]
</local_ctx>

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[elab_as_elim]
protected def inductionOn {C : OracleComp spec α → Prop}
    (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) (oa : OracleComp spec α) : C oa :=
  FreeMonad.inductionOn (Option.rec failure pure) (λ (query i t) ↦ query_bind i t) oa

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

set_get : (do let s ← get; set s) = pure ⟨⟩

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

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

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

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

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

noncomputable def LWE_Advantage (adv : LWE_Adversary n m p) : ℝ :=
  (LWE_Experiment n m p errSamp adv).advantage'

def speedup {S : Type u} {P : PFunctor.{uA, uB}} (l : Lens (selfMonomial S) P) :
    Lens (selfMonomial S) (P ◃ P) :=
  (l ◃ₗ l) ∘ₗ fixState

inductive Tree' (a : Type*) where
  | leaf : a → Tree' a
  | node : Tree' a → Tree' a → Tree' a

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

StateT in Init.Control.State

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

instance : LawfulComonad (CofreeC F) := sorry

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

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

noncomputable def IND_CPA_advantage {encAlg : AsymmEncAlg ProbComp M PK SK C}
    (adversary : encAlg.IND_CPA_adversary) : ℝ≥0∞ :=
  [= () | IND_CPA_experiment adversary] - 1 / 2

def trans {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}}
    (E : P ≃ₚ Q) (F : Q ≃ₚ R) : P ≃ₚ R where
  equivA := E.equivA.trans F.equivA
  equivB := fun a => (E.equivB a).trans (F.equivB (E.equivA a))

class StrongestPostcondition (P : PreCondition σ) (comp : StateM σ α) where
  Q : PostCondition σ α
  hQ : HoareTriple P comp Q
  hStrong : ∀ Q', HoareTriple P comp Q' → Q' ≤ Q

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

PEmpty in Init.Prelude

associator in Mathlib.Algebra.Ring.Associator

ExceptT.mk in Init.Control.Except

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

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

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

Vector in Init.Data.Vector.Basic

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

structure IND_CCA_Adversary (encAlg : AsymmEncAlg m M PK SK C) where
    main : PK → OracleComp encAlg.IND_CCA_oracleSpec Bool

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

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

def tensorAssoc : (P ⊗ Q) ⊗ R ≃ₗ P ⊗ (Q ⊗ R) where
  toLens := (_root_.Equiv.prodAssoc _ _ _).toFun ⇆
            (fun _ => (_root_.Equiv.prodAssoc _ _ _).invFun)
  invLens := (_root_.Equiv.prodAssoc _ _ _).invFun ⇆
            (fun _ => (_root_.Equiv.prodAssoc _ _ _).toFun)
  left_inv := rfl
  right_inv := rfl

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

iSup in Mathlib.Order.SetNotation

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

List.zipWith in Init.Data.List.Basic

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

liftWith_restoreM {α : Type u} (t : n α) :
    liftWith (m := m) (fun run => run t) >>= restoreM = t

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

class OrderedMonadTransformer (t : (Type u → Type v) → Type u → Type w)
    extends MonadTransformer t where
  mapOrderedMonad {m} [OrderedMonad m] : OrderedMonad (t m)
  liftOf_mono {m n} [OrderedMonad m] [OrderedMonad n] [OrderedMonadLiftT m n] :
    OrderedMonadLiftT (t m) (t n)

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

Sum in Init.Core

One.one in Init.Prelude

DecidableEq in Init.Prelude

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

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

def withPregen (so : QueryImpl spec m) : QueryImpl spec (ReaderT spec.QuerySeed m) where
  impl | query i t => do
    let seed ← read
    do match seed i with
      | u :: us => ReaderT.adapt (fun seed => seed.update i us) (return u)
      | [] => so.impl (query i t)

StateT.instMonad in Init.Control.State

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

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

ExceptT in Init.Control.Except

AlternativeMonad in Batteries.Control.AlternativeMonad

instance : Coapplicative Zipper where
  coseq := coseq

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⟩

PUnit.instUnique in Mathlib.Logic.Unique

BitVec in Init.Prelude

ExceptT.bind in Init.Control.Except

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

alias fromZero := initial
alias toOne := terminal

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

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

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

PEmpty.instIsEmpty in Mathlib.Logic.IsEmpty

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

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

Preord in Mathlib.Order.Category.Preord

instance : Coapplicative Stream' where

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

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

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

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

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

instance instFunctor [Functor f] [Functor g] : Functor (Day f g) where
  map {a b : Type u₃} (k : a → b) (day : Day f g a) : Day f g b :=
    
    ⟨fun (x : day.α) (y : day.β) => k (day.map' x y), day.fa, day.gb⟩

OptionT.mk in Init.Control.Option

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

BitVec.toFin in Init.Prelude

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

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

def zeroTensor : 0 ⊗ P ≃ₚ 0 where
  equivA := Equiv.pemptyProd P.A
  equivB := fun a => Equiv.pemptyProd (P.B a.2)

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

decidable_of_iff' in Init.PropLemmas

outParam in Init.Prelude

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

Set.image in Mathlib.Data.Set.Defs

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

def pointwiseRelation {α β : Type u} (r : β → β → Prop) (f g : α → β) : α → α → Prop :=
  fun a b => r (f a) (g b)

structure PolyQueries {ι : Type} [DecidableEq ι] {spec : ℕ → OracleSpec ι}
  {α β : ℕ → Type} (oa : (n : ℕ) → α n → OracleComp (spec n) (β n)) where
   
  qb : ι → Polynomial ℕ
   
  qb_isQueryBound (n : ℕ) (x : α n) :
    IsQueryBound (oa n x) (λ i ↦ (qb i).eval n)

Fintype.card in Mathlib.Data.Fintype.Card

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

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 α → _)

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

def sumPair {P : PFunctor.{uA₁, uB}} {Q : PFunctor.{uA₂, uB}} {R : PFunctor.{uA₃, uB₃}}
    (l₁ : Lens P R) (l₂ : Lens Q R) :
    Lens.{max uA₁ uA₂, uB, uA₃, uB₃} (P + Q) R :=
  (Sum.elim l₁.toFunA l₂.toFunA) ⇆
    (fun a d => match a with
      | Sum.inl pa => l₁.toFunB pa d
      | Sum.inr qa => l₂.toFunB qa d)

Array.flatMapM in Init.Data.Array.Basic

AddTorsor in Mathlib.Algebra.AddTorsor.Defs

instance : Comonad Zipper where

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

Functor.mapConst in Init.Prelude

scoped instance (priority := low) instDiscreteMonad (m) [Monad m] : OrderedMonad m where
  monadOrder := {
    le := (· = ·)
    le_refl _ := rfl
    le_trans _ _ _ _ _ := by admit /- proof elided -/

Vector.zipWith in Init.Data.Vector.Basic

def uliftSumEquiv (Q : PFunctor.{uA₂, uB₁}) :
    (PFunctor.ulift.{_, _, u, v} (P + Q : PFunctor.{max uA₁ uA₂, uB₁})) ≃ₚ
    ((PFunctor.ulift.{_, _, uA, uB} P : PFunctor.{max uA₁ uA, max uB₁ uB}) +
      (Q.ulift : PFunctor.{max uA₂ uA', max uB₁ uB}) : PFunctor.{max uA₁ uA uA₂ uA', max uB₁ uB}) :=
  sorry

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

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

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

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

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

List.map in Init.Prelude

Option.isSome in Init.Data.Option.Basic

instance {ε} [Subsingleton ε] : Commutative (Except ε) where
  bind_comm := fun ma mb => by admit /- proof elided -/

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)

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

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

Vector.ofFn in Init.Data.Vector.Basic

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

structure ReportingTag where
  tag : mock_hmac_sha256_out_type 
  deriving Repr

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

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

Vector.push in Init.Data.Vector.Basic

Turing.TM2ComputableInPolyTime in Mathlib.Computability.TMComputable

structure SignatureAlg (m : Type → Type v) (M PK SK S : Type)
    extends ExecutionMethod m where
  keygen : m (PK × SK)
  sign (pk : PK) (sk : SK) (msg : M) : m S
  verify (pk : PK) (msg : M) (σ : S) : m Bool

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

CategoryTheory.Functor.prod in Mathlib.CategoryTheory.Products.Basic

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

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

class MonadLift.LE (m : Type u → Type v) (n : Type u → Type w) [Monad m] [OrderedMonad n]
    [φ : MonadLift m n] [ψ : MonadLift m n] where
  monadLift_le {α} (a : m α) : φ.monadLift a ≤ₘ ψ.monadLift a

PFunctor.comp in Mathlib.Data.PFunctor.Univariate.Basic

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

ReaderT in Init.Prelude

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

abbrev PreCondition.top (σ : Type*) : PreCondition σ := fun _ => True

Prod.snd in Init.Prelude

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

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

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

def sum (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) :
    PFunctor.{max uA₁ uA₂, uB} :=
  ⟨P.A ⊕ Q.A, Sum.elim P.B Q.B⟩

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

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

List.filterMap in Init.Data.List.Basic

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

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

CharP in Mathlib.Algebra.CharP.Defs

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

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

monadFunctorRefl in Init.Prelude

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 : Extend Id where
  extend wx f := f wx

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

List.all in Init.Data.List.Basic

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

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

class Monad.AssertAssume (m : Type u → Type v) [∀ α, Preorder (m α)] where
  assert_assume {α} : _root_.AssertAssume (m α)

structure AbuseReport where
  message : SecretMessage
  franking_tag : FrankingTag
  reporting_tag : ReportingTag
  context : Context
  deriving Repr

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

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

@[simps]
def tensorAssoc :
    ((P ⊗ Q) ⊗ R : PFunctor.{max uA₁ uA₂ uA₃, max uB₁ uB₂ uB₃}) ≃ₚ
    (P ⊗ (Q ⊗ R) : PFunctor.{max uA₁ uA₂ uA₃, max uB₁ uB₂ uB₃}) where
  equivA := _root_.Equiv.prodAssoc P.A Q.A R.A
  equivB := fun a => _root_.Equiv.prodAssoc (P.B a.1.1) (Q.B a.1.2) (R.B a.2)

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

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

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

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

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

def fixState {S : Type u} : Lens (selfMonomial S) (selfMonomial S ◃ selfMonomial S) :=
  (fun s₀ => ⟨s₀, fun s₁ => s₁⟩) ⇆ (fun _s₀ => fun ⟨_s₁, s₂⟩ => s₂)

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

Summable in Mathlib.Topology.Algebra.InfiniteSum.Defs

ULift.up in Init.Prelude

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

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

alias coprod := sum

instance {Q : PostCondition σ σ} {x : σ} : WeakestPrecondition (pure x : StateM σ σ) Q := default

MonadStateOf.get in Init.Prelude

PMF.instMonad in Mathlib.Probability.ProbabilityMassFunction.Monad

Function.Injective2 in Mathlib.Logic.Function.Basic

LawfulMonad in Init.Control.Lawful.Basic

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

Bind.bind in Init.Prelude
</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]
lemma probOutput_seq_map_cons_eq_mul [spec.FiniteRange] [spec.DecidableEq] (xs : List α) :
    [= xs | cons <$> oa <*> ob] = if h : xs.isEmpty then 0 else
      [= xs.head (h ∘ List.isEmpty_iff.2) | oa] * [= xs.tail | ob]

@[simp low]
lemma probEvent_eq_one_iff : [p | oa] = 1 ↔ [⊥ | oa] = 0 ∧ ∀ x ∈ oa.support, p x

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

@[simp]
lemma getQ_append (log log' : QueryLog spec) (i : ι) :
    (log ++ log').getQ i = log.getQ i ++ log'.getQ i

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

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 pure_ne_query_bind : pure x ≠ (q : OracleComp spec β) >>= oa

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

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

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

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

@[simp]
lemma liftComp_failure : liftComp (failure : OracleComp spec α) superSpec = failure

@[simp]
lemma Fin_Bound_ge {n b₁ b₂ : ℕ} {x : Fin n} (h : Fin_Bound x b₁)
 (g : b₁ ≤ b₂) : Fin_Bound x b₂

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

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

@[simp]
lemma run_map (x : WriterT ω m α) (f : α → β) : (f <$> x).run = Prod.map f id <$> x.run

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

@[simp] lemma evalDist_ite (p : Prop) [Decidable p] (mx mx' : m α) :
    evalDist (if p then mx else mx') = if p then evalDist mx else evalDist mx'

@[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 generateSeed_nil : generateSeed spec qc [] = return ∅

lemma LWE_Experiment_eq_LWE_Game_01 {n m p : ℕ} [NeZero p] {errSamp : ProbComp (Fin p)}
    {adv : LWE_Adversary n m p} :
    2 * (LWE_Experiment n m p errSamp adv).advantage' =
      (LWE_Game_0 n m p errSamp adv).advantage₂' (LWE_Game_1 n m p adv)

@[simp]
lemma neverFails_run_simulateQ_iff (oa : OracleComp spec α) :
    neverFails (simulateQ loggingOracle oa).run ↔ neverFails oa

@[simp low + 1]
lemma finSupport_seq_map_eq_image2 [spec.FiniteRange] [spec.DecidableEq]
    [DecidableEq α] [DecidableEq β] [DecidableEq γ] :
    (f <$> oa <*> ob).finSupport = Finset.image₂ f oa.finSupport ob.finSupport

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

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

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

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 evalDist_simulateQ [spec.FiniteRange] (oa : OracleComp spec α) :
    evalDist (simulateQ unifOracle oa) = evalDist oa

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

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

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

theorem perfectSecrecy_iff_of_card_eq [Fintype M] [Fintype K] [Fintype C]
    (encAlg : SymmEncAlg m M K C) [encAlg.Complete] (h1 : Fintype.card M = Fintype.card K)
    (h2 : Fintype.card K = Fintype.card C) : encAlg.perfectSecrecy ↔
      (∀ k, [= k | encAlg.exec encAlg.keygen] = (Fintype.card K : ℝ≥0∞)⁻¹) ∧
      (∀ m c, ∃! k, k ∈ (encAlg.exec encAlg.keygen).support ∧ encAlg.encrypt k m = c)

@[simp] lemma probEvent_lt_top : Pr[p | mx] < ∞

lemma bind_def (x : WriterT ω m α) (f : α → WriterT ω m β) :
    x >>= f = WriterT.mk (x.run >>= fun (a, w₁) ↦
      (Prod.map id (w₁ * ·)) <$> (f a))

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

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

@[simp]
lemma queryBind_inj (q q' : OracleQuery spec α) (ob ob' : α → OracleComp spec β) :
    (q : OracleComp spec α) >>= ob = (q' : OracleComp spec α) >>= ob' ↔ q = q' ∧ ob = ob'

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

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

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

@[simp] lemma not_one_lt_probEvent : ¬ 1 < [p | oa]

@[simp] theorem id_mapᵣ' [RelativeFunctor j f] [LawfulRelativeFunctor j f] (x : f α) :
    (fun a : j α => a) <$>ᵣ x = x

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

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

@[simp]
lemma evalDist_comp_some (oa : OracleComp spec α) :
    (evalDist oa).run ∘ some = ([= · | oa])

@[simp] lemma selfMonomial_A (S : Type u) : (selfMonomial S).A = S

@[simp]
lemma getQ_cons (log : QueryLog spec) (q : (i : ι) × spec.domain i × spec.range i) (i : ι) :
    getQ (q :: log) i =
      if h : q.1 = i then h ▸ (q.2.1, q.2.2) :: getQ log i else getQ log i

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

@[simp]
lemma bind_eq_pure_iff (oa : OracleComp spec α) (ob : α → OracleComp spec β) (y : β) :
    oa >>= ob = pure y ↔ ∃ x : α, oa = pure x ∧ ob x = pure y

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

lemma apply_eq_apply_of_mem_support_fork (x₁ x₂ : α)
    (h : (x₁, x₂) ∈ (fork main qb js i cf).support) : cf x₁ = cf x₂

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

@[simp] lemma probOutput_eq : probOutput p = p

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

@[simp]
lemma function_support_probOutput : Function.support ([= · | oa]) = oa.support

@[simp] lemma supportWhen_failure : (failure : OracleComp spec α).supportWhen poss = ∅

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

@[simp]
lemma evalDist_map (oa : OracleComp spec α) (f : α → β) :
    evalDist (f <$> oa) = f <$> (evalDist oa)

@[simp] -- NOTE: shouldn't actually need finiteness here.
lemma support_liftComp [spec.FiniteRange] [superSpec.FiniteRange]
    (oa : OracleComp spec α) : (liftComp oa superSpec).support = oa.support

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

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

@[simp]
lemma probFailure_replicate [spec.FiniteRange] :
    [⊥ | oa.replicate n] = 1 - (1 - [⊥ | oa]) ^ n

theorem pure_eq_pmf_pure {a : α} : (pure a : SPMF α) = PMF.pure a

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

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

@[simp] lemma support_uniformOfFintype : ($ᵗ α).support = Set.univ

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

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

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

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

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

@[simp] lemma query_ne_pure : (q : OracleComp spec β) ≠ pure y

@[simp]
lemma support_orElse {ι : Type u} {spec : OracleSpec ι} {α : Type u}
    (oa oa' : OracleComp spec α) [Decidable oa.neverFails] : (oa <|> oa').support =
      if oa.neverFails then oa.support else oa.support ∪ oa'.support

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

@[simp]
lemma equivState_equivState : (so.equivState e).equivState e.symm = so

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

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

lemma simulation_setup_succeeds (message_content : String) :
    [⊥ | do
      let maybeData ← simulation_setup message_content
      match maybeData with
      | none => return true
      | some _ => return false] = 0

@[simp]
lemma getQ_singleton_self (i : ι) (t : spec.domain i) (u : spec.range i) :
    getQ (singleton (query i t) u) i = [(t, u)]

theorem Hybrid_0_ind_Hybrid_1 :
    (Hybrid_0 adv).advantage' ≤ (Hybrid_1 adv).advantage'
      + (LWE_Advantage n m p (uniformErrSamp χ (relax_p_bound he)) (Hybrid_01_Reduction adv))

@[simp]
lemma takeAtIndex_apply (j : ι) : seed.takeAtIndex i n j =
    (Function.update seed i ((seed i).take n) j)

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

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

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

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

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

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 purePower_unit : purePower PUnit = X

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

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

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

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

protected lemma liftM_def (q : OracleQuery spec α) :
    (q : OracleComp spec α) = OptionT.lift (FreeMonad.lift q)

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

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

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

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

lemma mem_support_bind_iff (oa : OracleComp spec α) (ob : α → OracleComp spec β) (y : β) :
    y ∈ (oa >>= ob).support ↔ ∃ x ∈ oa.support, y ∈ (ob x).support

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

lemma probFailure_bind_eq_sum_probFailure [spec.FiniteRange] (oa : OracleComp spec α)
    {ob : α → OracleComp spec β} {σ : Type u} {s : Finset σ}
    {oc : σ → α → OracleComp spec γ} :
    [⊥ | oa >>= ob] = ∑ x ∈ s, [⊥ | oa >>= oc x]

@[simp] lemma supportWhen_pure (x : α) :
    (pure x : OracleComp spec α).supportWhen poss = {x}

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

@[simp] lemma evalDist_uniformOfFintype [Fintype α] [Inhabited α] :
    evalDist ($ᵗ α) = OptionT.lift (PMF.uniformOfFintype α)

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]
lemma liftM_left_append_left_append_eq [h : spec₁ ⊂ₒ spec₃]
    (q : OracleQuery (spec₁ ++ₒ spec₂) α) : (liftM q : OracleQuery (spec₃ ++ₒ spec₂) α) =
    match q with

@[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] theorem RelativeFunctor.map_map [RelativeFunctor j f] [LawfulRelativeFunctor j f]
    (h : j α → j β) (g : j β → j γ) (x : f α) :
      g <$>ᵣ h <$>ᵣ x = (fun a => g (h a)) <$>ᵣ x

@[simp] lemma finSupport_uniformFin (n : ℕ) : ($[0..n]).finSupport = Finset.univ :=
  finSupport_query _

@[simp] lemma X_A : X.A = PUnit

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

@[simp]
lemma neverFails_map_iff (oa : OracleComp spec α) (f : α → β) :
    neverFails (f <$> oa) ↔ neverFails oa

@[simp]
theorem PreCondition.top_def {σ : Type _} : PreCondition.top σ = fun _ => True

@[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 not_one_lt_probOutput : ¬ 1 < [= x | oa]

lemma probOutput_prod_mk_seq_map_eq_mul [spec.FiniteRange] (oa : OracleComp spec α)
    (ob : OracleComp spec β) (z : α × β) :
    [= z | ((·, ·) <$> oa <*> ob : OracleComp spec (α × β))] = [= z.1 | oa] * [= z.2 | ob]

lemma getQ_singleton_of_ne {α} {q : OracleQuery spec α} {u : α} {i : ι}
    (h : q.index ≠ i) : getQ (singleton q u) i = []

@[simp]
lemma not_neverFails_failure : ¬ neverFails (failure : OracleComp spec α)

lemma eq_addValues_iff [DecidableEq ι] (seed seed' : QuerySeed spec)
    {i : ι} (xs : List (spec.range i)) :
    seed = seed'.addValues xs ↔ seed' = seed.takeAtIndex i (seed' i).length ∧
      xs = (seed i).drop (seed' i).length

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

lemma neverFailsWhen_simulate {ι' : Type*} {spec' : OracleSpec ι'}
    (oa : OracleComp spec α)
    (possible_outputs : {α : Type v} → OracleQuery spec α → Set α)
    (h : neverFailsWhen oa possible_outputs)
    -- {m : Type v → Type _} [Monad m]
    (so : QueryImpl spec (OracleComp spec'))
    (h' : ∀ {α}, ∀ q : OracleQuery spec α, (so.impl q).support ⊆ possible_outputs q)
    (hso : ∀ {α}, ∀ q : OracleQuery spec α, neverFails (so.impl q)) :
    neverFails (simulateQ so oa)

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

lemma mem_support_vector_mapM {n} {f : α → OracleComp spec β} {as : Vector α n} {x : Vector β n} :
    x ∈ (Vector.mapM f as).support ↔ ∀ i : Fin n, x[i] ∈ (f as[i]).support

@[simp] lemma finSupport_coin : coin.finSupport = {true, false}

lemma monad_bind_def [Monad m] (x : StateT σ m α) (f : α → StateT σ m β) :
    x >>= f = StateT.bind x f

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

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

lemma probOutput_map_eq_single [spec.FiniteRange] {oa : OracleComp spec α} {f : α → β} {y : β}
    (x : α) (h : ∀ x' ∈ oa.support, y = f x' → x = x') (h' : f x = y) :
    [= y | f <$> oa] = [= x | oa]

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

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

lemma probOutput_ne_zero (h : x ∈ oa.support) : [= x | oa] ≠ 0

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

@[simp] lemma selfMonomial_B (S : Type u) (a : (selfMonomial S).A) : (selfMonomial S).B a = S

lemma probOutput_seq_map_prod_mk_eq_mul :
    [= (x, y) | Prod.mk <$> oa <*> ob] = [= x | oa] * [= y | ob]

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

theorem IND_CPA_advantage_le :
  IND_CPA_OneTime_Advantage (encAlg := uniformRegevAsymmEnc n m p χ he) adv ≤
    (LWE_Advantage n m p (uniformErrSamp χ (relax_p_bound he)) (Hybrid_01_Reduction adv))
      + (LHL_Consequence_Advantage (m := m) (Hybrid_12_Reduction adv))

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

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

@[simp] lemma evalDist_eq : evalDist p = p

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

<local_ctx>
import VCVio.OracleComp.Traversal

import VCVio.OracleComp.SimSemantics.SimulateQ

import Mathlib.Probability.Distributions.Uniform

import ToMathlib.General

open OracleSpec Option ENNReal BigOperators

namespace OracleComp

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

section evalDist

end evalDist

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

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

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

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

section bounds

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

end bounds

section support

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

variable {oa x p q}

end support

section sums

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

end sums
</local_ctx>

<target_theorem>
lemma probEvent_congr' {p q : α → Prop} {oa : OracleComp spec α} {oa' : OracleComp spec' α}
    (h1 : ∀ x, x ∈ oa.support → x ∈ oa'.support → (p x ↔ q x))
    (h2 : evalDist oa = evalDist oa') : [p | oa] = [q | oa'] :=
</target_theorem>

