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>
structure NatHom (m : Type u → Type v) (n : Type u → Type w) where
  toFun : {α : Type u} → m α → n α

example : Hybrid_0 adv = IND_CPA_OneTime_Game adv :=

def sumMap {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₂, uB₁, max uA₃ uA₄, uB₃} (P + Q) (R + W) :=
  (Sum.map l₁.toFunA l₂.toFunA) ⇆
    (fun psum => match psum with
      | Sum.inl pa => l₁.toFunB pa
      | Sum.inr qa => l₂.toFunB qa)

PMF.toOuterMeasure in Mathlib.Probability.ProbabilityMassFunction.Basic

Monotone in Mathlib.Order.Monotone.Defs

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

def DijkstraMonad.dMap {w d} [Monad w] [DijkstraMonad w d] {α β} {a : w α} (f : α → β) :
    d a → d (a >>= fun b => pure (f b)) := fun x => x >>=ᵈ (fun a => dPure (f a))

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

monadFunctorRefl in Init.Prelude

@[simp] protected def default : ExecutionMethod ProbComp where
  exec := id
  lift_probComp := id
  exec_lift_probComp _ := rfl

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

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

def comp {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}}
    (l : Lens Q R) (l' : Lens P Q) : Lens P R where
  toFunA := l.toFunA ∘ l'.toFunA
  toFunB := fun i => (l'.toFunB i) ∘ l.toFunB (l'.toFunA i)

instance : Functor NonEmptyList where
  map := NonEmptyList.map

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

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

Computation in Mathlib.Data.Seq.Computation

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

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

Vector in Init.Data.Vector.Basic

Finset.card in Mathlib.Data.Finset.Card

inferInstanceAs in Init.Prelude

PFunctor.A in Mathlib.Data.PFunctor.Univariate.Basic

List.zip in Init.Data.List.Basic

Function.const in Init.Prelude

dotProduct in Mathlib.Data.Matrix.Mul

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

def punitSigma {F : PUnit → PFunctor.{uA, uB}} : sigma F ≃ₚ F PUnit.unit where
  equivA := _root_.Equiv.uniqueSigma _
  equivB := sorry

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

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

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

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

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

class LawfulMonadState (σ : outParam (Type u)) (m : Type u → Type v) [Monad m] :
    Type (max (u+1) v) extends MonadState σ m where

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

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

protected def mapM {m : Type v → Type w} [Monad m]
    (fail : {α : Type v} → m α)
    (query_map : {α : Type v} → OracleQuery spec α → m α)
    (oa : OracleComp spec α) : m α :=
  OracleComp.construct pure (λ q _ r ↦ query_map q >>= r) fail oa

Num in Mathlib.Data.Num.Basic

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

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

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

def bitvec_to_string (bv : BitVec 256) : String :=
  let rec chars (n : Nat) (acc : List Char) :=
    if n = 0 then acc
    else chars (n / 256) (Char.ofNat (n % 256) :: acc)
  String.mk (chars bv.toNat [])

Set.univ in Mathlib.Data.Set.Defs

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

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

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

def append {ι₁ : Type u} {ι₂ : Type u'} (spec₁ : OracleSpec ι₁) (spec₂ : OracleSpec ι₂) :
    OracleSpec (ι₁ ⊕ ι₂) := 
  fun | .inl i => spec₁ i | .inr i => spec₂ i

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

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

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

Option in Init.Prelude

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 trans (e₁ : NatEquiv m n) (e₂ : NatEquiv n p) : NatEquiv m p where
  toFun := e₂.toFun ∘ e₁.toFun
  invFun := e₁.invFun ∘ e₂.invFun
  left_inv := by admit /- proof elided -/

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

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

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

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

Array.drop in Init.Data.Array.Basic

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

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

associator in Mathlib.Algebra.Ring.Associator

ExceptT in Init.Control.Except

private def lawLargeNumsTest (trials : ℕ) (die : ℕ) : IO Unit := do
  let n : ℕ := trials * die
  let xs ← OracleComp.replicateTR n $[0..die - 1]
  IO.println ("Rolling " ++ toString n ++ " " ++ toString die ++ "-sided dice:")
  for i in List.range die do
    IO.println <| "▸Num " ++ toString (i + 1) ++ "s: " ++ toString (xs.count i)

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

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

class Comonad (w : Type u → Type v) extends Coapplicative w, Extend w where
   
  map f wa := extend wa (f ∘ extract)
   
  coseq wa wb := extend wa (fun wa' => (extract wa', extract wb))

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

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

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

instance (m : Type u → Type v) [Pure m] [Bind m] (n : Type u → Type w) [Pure n] [Bind n] :
    CoeFun (m →ᵐ n) (λ _ ↦ {α : Type u} → m α → n α) where
  coe f {_} x := f.toFun x

instance : Comonad (Prod ε) where

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

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

String in Init.Prelude

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

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

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

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

def generate_reporting_tag (franking_tag : FrankingTag) (context : Context)
    (facebook_key : BitVec 256) : ReportingTag :=
  
  let context_bv := BitVec.ofNat 256 context.timestamp
  let serialized := franking_tag.tag.append (bitvec_to_string context_bv)
  let rf_tag := mock_hmac_sha256 facebook_key (string_to_bitvec serialized)
  { tag := rf_tag }

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

Fintype.ofBijective in Mathlib.Data.Fintype.OfMap

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

instance : HAdd PFunctor.{uA₁, uB} PFunctor.{uA₂, uB} PFunctor.{max uA₁ uA₂, uB} where
  hAdd := sum

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

def compMap {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₂ uB₁, max uB₁ uB₂, max uA₃ uA₄ uB₃, max uB₃ uB₄} (P ◃ Q) (R ◃ W) :=
  (fun ⟨pa, pq⟩ => ⟨l₁.toFunA pa, fun rb' => l₂.toFunA (pq (l₁.toFunB pa rb'))⟩) ⇆
    (fun ⟨pa, pq⟩ ⟨rb, wc⟩ =>
      let pb := l₁.toFunB pa rb
      let qc := l₂.toFunB (pq pb) wc
      ⟨pb, qc⟩)

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

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

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

FunLike in Mathlib.Data.FunLike.Basic

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

structure SymmEncAlg (m : Type u → Type v)
    (M K C : Type u) extends ExecutionMethod m where
  keygen : m K
  encrypt (k : K) (msg : M) : m C
  decrypt (k : K) (c : C) : Option M

instance : Repr mock_hmac_sha256_out_type := instReprString

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 probSpec : OracleSpec.{0,0} ℕ :=
  fun n => (ℕ, Fin (n + 1))

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

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

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

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

Pure in Init.Prelude

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

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

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

List.mapM in Init.Data.List.Control

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'

List.map in Init.Prelude

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

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

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

CategoryTheory.NatTrans in Mathlib.CategoryTheory.NatTrans

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

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

Unit in Init.Prelude

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

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

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

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

OptionT.instMonadFunctor in Init.Control.Option

Function.uncurry in Init.Data.Function

MonadLift.monadLift in Init.Prelude

def MonoStateContProp (σ : Type u) := MonoCont (σ → Prop)

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

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

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

PUnit in Init.Prelude

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

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 instCoapplicative [Comonad w] : Coapplicative (StoreT s w) where

structure EncryptedMessage where
  ciphertext : BitVec 256
  deriving Repr

Decidable.isTrue in Init.Prelude

instance instMonadSigma {w d} [Monad w] [DijkstraMonad w d] :
    Monad (fun α => (w : w α) × d w) where
  pure x := ⟨pure x, dPure x⟩
  bind x f := ⟨x.1 >>= (fun a => (f a).1), x.2 >>=ᵈ (fun a => (f a).2)⟩

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

Equiv.prodPEmpty in Mathlib.Logic.Equiv.Prod

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

id in Init.Prelude

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

instance : Functor Zipper where
  map := map

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

Or.inr in Init.Prelude

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 }

StateM in Init.Control.State

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 invTildeL {P : PFunctor.{uA, uB}} : Lens (X ◃ P) P :=
  (fun ⟨_, f⟩ => f PUnit.unit) ⇆ (fun _ b => ⟨PUnit.unit, b⟩)

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

EmptyCollection in Init.Core

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

class Commutative (m : Type u → Type v) [Monad m] where
  bind_comm {α β} (ma : m α) (mb : m β) : CommutativeAt m ma mb

Vector.zero in Init.Data.Vector.Algebra

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

structure ReportingTag where
  tag : mock_hmac_sha256_out_type 
  deriving Repr

instance : Commutative Id where
  bind_comm := fun _ _ => rfl

LE in Init.Prelude

PEmpty.elim in Init.Core

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

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

instance [Monad m] [LawfulMonad m] : LawfulMonadLift m (FreeContT f m) where
  monadLift_pure := by admit /- proof elided -/

@[trans]
def trans {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}}
    (e₁ : P ≃ₗ Q) (e₂ : Q ≃ₗ R) : P ≃ₗ R :=
  ⟨e₂.toLens ∘ₗ e₁.toLens, e₁.invLens ∘ₗ e₂.invLens,
    by admit /- proof elided -/
      ⟩

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

NatPow in Init.Prelude

AddGroup in Mathlib.Algebra.Group.Defs

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

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

Fin.sub in Init.Data.Fin.Basic

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

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

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

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

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

def append {m₁ m₂ n : Type u → Type v} [MonadLiftT m₁ n] [MonadLiftT m₂ n]
    (so : QueryImpl spec₁ m₁) (so' : QueryImpl spec₂ m₂) :
    QueryImpl (spec₁ ++ₒ spec₂) n where impl
  | query (inl i) t => so.impl (query i t)
  | query (inr i) t => so'.impl (query i t)

instance : Coseq NonEmptyList where
  coseq := NonEmptyList.zip

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

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

def XComp : X ◃ P ≃ₚ P where
  equivA := (_root_.Equiv.uniqueSigma _).trans (Equiv.punitArrowEquiv P.A)
  equivB := fun _ => by admit /- proof elided -/

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

def toChart (e : P ≃ₚ Q) : Chart P Q where
  toFunA := e.equivA
  toFunB := fun a => e.equivB a

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

liftM in Init.Prelude

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

StateT.mk in Init.Control.State

instance : Coapplicative NonEmptyList where

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

CategoryTheory.aesop_cat in Mathlib.CategoryTheory.Category.Basic

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)

Char.ofNat in Init.Prelude

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

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

class LawfulMonadAlgebra (m : Type u → Type v) [Monad m] [MonadAlgebra m] where
  monadAlg_pure {α : Type u} (a : α) : monadAlg (pure a : m α) = a
  monadAlg_bind {α β : Type u} (ma : m α) (mb : α → m β) :
    monadAlg (mb (monadAlg ma)) = monadAlg (ma >>= mb)

LawfulAlternativeLift in Batteries.Control.AlternativeMonad

Zero in Init.Prelude

Array.foldrM in Init.Data.Array.Basic

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

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

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

MonadControlT in Init.Control.Basic

Prod in Init.Prelude

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

Subsingleton in Init.Core

instance : LawfulFunctor NonEmptyList where
  id_map := by admit /- proof elided -/

Function.comp in Init.Prelude
</all_available_defs>

<all_available_lemmas>
@[simp]
lemma probEvent_map (q : β → Prop) : [q | f <$> oa] = [q ∘ f | oa]

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

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

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 id_comp {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (f : Lens P Q) :
    (Lens.id Q) ∘ₗ f = f

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

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

@[simp]
lemma probFailure_ite : [⊥ | if p then oa else oa'] =
    if p then [⊥ | oa] else [⊥ | oa']

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

@[simp] lemma finSupportWhen_query_bind [DecidableEq β]
    (q : OracleQuery spec α) (ob : α → OracleComp spec β) :
    (liftM q >>= ob).finSupportWhen fin_poss =
      (fin_poss q).biUnion fun x => (ob x).finSupportWhen fin_poss

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

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

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

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

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

@[simp] lemma supportWhen_monadLift (q : OracleQuery spec α)
    (poss : {α : Type w} → OracleQuery superSpec α → Set α) :
    supportWhen (q : OracleComp superSpec α) poss = poss q

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

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

lemma monad_pure_def [Monad m] (x : α) :
    (pure x : StateT σ m α) = StateT.pure x

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

@[simp]
lemma support_generateSeed : (generateSeed spec qc js).support =
    {seed | ∀ i, (seed i).length = qc i * js.count i}

@[simp]
lemma probOutput_failure (x : α) : [= x | (failure : OracleComp spec α)] = 0

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

lemma probEvent_bind_eq_sum_fintype [Fintype α] (q : β → Prop) :
    [q | oa >>= ob] = ∑ x : α, [= x | oa] * [q | ob x]

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

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

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

@[simp]
theorem prodMap_id :
    Lens.prodMap (Lens.id P) (Lens.id Q) = Lens.id.{max uA₁ uA₂, max uB₁ uB₂} (P * Q)

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

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

@[simp]
lemma liftComp_map (oa : OracleComp spec α) (f : α → β) :
    liftComp (f <$> oa) superSpec = f <$> liftComp oa superSpec

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

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

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

lemma probEvent_query_eq_div [spec.DecidableEq] (p : spec.range i → Prop) [DecidablePred p] :
    [p | (query i t : OracleComp spec _)] =
      (Finset.univ.filter p).card / (Fintype.card (spec.range i))

@[simp]
lemma run_bind [LawfulMonad m] (x : WriterT ω m α) (f : α → WriterT ω m β) :
    (x >>= f).run = x.run >>= fun (a, w₁) => Prod.map id (w₁ * ·) <$> (f a).run

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

@[simp]
lemma mem_support_evalDist_iff' [spec.DecidableEq] [DecidableEq α]
    (oa : OracleComp spec α) (x : α) :
    some x ∈ (evalDist oa).run.support ↔ x ∈ oa.finSupport

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

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

@[simp]
lemma mmap_ofLift (m : Type u → Type v) (n : Type u → Type v) [Monad m] [Monad n]
    [MonadLift m n] [LawfulMonadLift m n] {α : Type u}
    (x : m α) : ofLift m n x = liftM x

lemma probEvent_seq_map_eq_probEvent_comp_uncurry [spec.FiniteRange]
    (p : γ → Prop) : [p | f <$> oa <*> ob] =
      [p ∘ f.uncurry | Prod.mk <$> oa <*> ob]

@[simp]
lemma heq_of_toArray_eq_of_size_eq {α} {m n : ℕ} {a : Vector α m} {b : Vector α n}
    (h : a.toArray = b.toArray) (h' : m = n) : HEq a b

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

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

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

@[simp] lemma tsum_run_some_ne_top (p : SPMF α) :
    ∑' x, p.run (some x) ≠ ⊤

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]
lemma bind_roll (a : P.A) (r : P.B a → FreeM P β) (g : β → FreeM P γ) :
    FreeM.bind (FreeM.roll a r) g = FreeM.roll a (λ u ↦ FreeM.bind (r u) g)

@[simp]
lemma probFailure_uniformFin : [⊥ | $[0..n]] = 0

lemma fst_map_writerT_run_simulateQ
    {so : QueryImpl spec (WriterT ω (OracleComp spec))}
    (hso : ∀ {α}, ∀ q : OracleQuery spec α, fst <$> (so.impl q).run = q)
    (oa : OracleComp spec α) : fst <$> (simulateQ so oa).run = oa

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

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 query_bind_ne_failure : (q : OracleComp spec β) >>= oa ≠ failure

theorem IsCoupling.bind {α₁ α₂ β₁ β₂ : Type u}
    {p : SPMF α₁} {q : SPMF α₂} {f : α₁ → SPMF β₁} {g : α₂ → SPMF β₂}
    (c : Coupling p q) (d : (a₁ : α₁) → (a₂ : α₂) → SPMF (β₁ × β₂))
    (h : ∀ (a₁ : α₁) (a₂ : α₂), c.1.1 (some (a₁, a₂)) ≠ 0 → IsCoupling (d a₁ a₂) (f a₁) (g a₂)) :
    IsCoupling (c.1 >>= λ (p : α₁ × α₂) => d p.1 p.2) (p >>= f) (q >>= g)

@[simp] lemma probEvent_uniformSelectList (xs : List α) (p : α → Prop) [DecidablePred p] :
    [p | $ xs] = if xs.isEmpty then 0 else (xs.countP p : ℝ≥0∞) / xs.length

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

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

theorem get_rule_forward (P : PreCondition σ) :
    HoareTriple P (get : StateM σ σ) (fun s x s' => P s ∧ s = x ∧ s = s')

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

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

lemma probOutput_uniformSelect_bool_bind_eq_add {α : Type}
    (oa : Bool → ProbComp α) (x : α) : -- should be anything $ᵗ Bool can lift to
    [= x | ($ᵗ Bool) >>= oa] = [= x | oa true] / 2 + [= x | oa false] / 2

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

@[simp]
lemma 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 query_ne_failure : (q : OracleComp spec β) ≠ failure

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

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)

@[simp] theorem toMonadState_get_eq_monadStateOf_get {m : Type u → Type v} {σ : Type u}
    [MonadStateOf σ m] : (MonadState.get : m σ) = MonadStateOf.get

lemma mul_abs_of_nonneg (h : 0 ≤ a) : a * |b

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

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

@[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 uniformSelectFinset_def {α : Type} [DecidableEq α] (s : Finset α) :
    ($ s) = ($ s.toList)

@[simp]
lemma probFailure_failure : [⊥ | (failure : OracleComp spec α)] = 1

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

@[simp]
lemma probOutput_liftM [Fintype α] (q : OracleQuery spec α) (u : α) :
    [= u | (q : OracleComp spec α)] = (Fintype.card α : ℝ≥0∞)⁻¹

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

@[simp]
lemma finSupport_generateSeed_ne_empty [DecidableEq spec.QuerySeed] :
    (generateSeed spec qc js).finSupport ≠ ∅

lemma probOutput_guard_eq_sub_probOutput_guard_not {α : Type} {oa : OracleComp spec α}
    (h : oa.neverFails) {p : α → Prop} [DecidablePred p] :
    [= () | do let a ← oa; guard (p a)] = 1 - [= () | do let a ← oa; guard (¬ p a)]

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 BitVec.xor_xor_cancel_right {n : ℕ} (bv1 bv2 : BitVec n) :
    bv1 ^^^ bv2 ^^^ bv2 = bv1

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

@[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 ProbComp.advantage₂_self (p : ProbComp Unit) : p.advantage₂ p = 0

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

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

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

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

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

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

@[simp]
lemma isQueryBound_pure (a : α) (qb : ι → ℕ) : IsQueryBound (pure a : OracleComp spec α) qb

@[simp] lemma finSupport_failure [spec.FiniteRange] [DecidableEq α] :
    (failure : OracleComp spec α).finSupport = ∅

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

@[simp] lemma not_one_lt_probOutput : ¬ 1 < Pr[= x | mx]

@[simp] lemma tsum_probOutput_le_one : ∑' x : α, Pr[= x | mx] ≤ 1

@[simp]
lemma Finset.count_toList {α} [DecidableEq α] (x : α) (s : Finset α) :
    s.toList.count x = if x ∈ s then 1 else 0

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

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

@[simp]
lemma probEvent_failure (p : α → Prop) :
    [p | (failure : OracleComp spec α)] = 0

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

lemma probEvent_comp (q : β → Prop) : [q ∘ f | oa] = [q | f <$> oa]

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

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

@[simp]
lemma generateSeed_zero : generateSeed spec 0 js = return ∅

lemma probOutput_map_eq_tsum_subtype (y : β) :
    [= y | f <$> oa] = ∑' x : {x ∈ oa.support | y = f x}, [= x | oa]

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

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

theorem bind_rule {P₁ : PreCondition σ} {Q₁ : PostCondition σ α}
    {P₂ : α → PreCondition σ} {Q₂ : α → PostCondition σ β}
    {comp₁ : StateM σ α} {comp₂ : α → StateM σ β}
    (h₁ : HoareTriple P₁ comp₁ Q₁) (h₂ : ∀ x, HoareTriple (P₂ x) (comp₂ x) (Q₂ x)) :
    HoareTriple (fun s => P₁ s ∧ ∀ x s', Q₁ s x s' → P₂ x s')
                (comp₁ >>= comp₂)
                (fun s y s'' => ∃ x s', Q₁ s x s' ∧ Q₂ x s' y s'')

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

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

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

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

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

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

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

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

@[simp]
theorem modifyThe_eq (f : σ → σ) :
    modifyThe σ (m := m) f = (do set (f (← MonadStateOf.get)))

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

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

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

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

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

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

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

@[simp] lemma probFailure_le_one : Pr[⊥ | mx] ≤ 1

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

lemma List.injective2_cons {α : Type*} : Function.Injective2 (List.cons (α := α))

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

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

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

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 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 CommutativeAt.bind_comm_comp {m} [Monad m] [LawfulMonad m] {α β γ}
    (ma : m α) (mb : m β) (h : CommutativeAt m ma mb) (f : α × β → m γ) :
      (ma >>= fun a => mb >>= fun b => f (a, b)) = (mb >>= fun b => ma >>= fun a => f (a, b))

@[simp] theorem liftM_orElse [Alternative m] [Alternative n] [MonadLift m n]
    [LawfulAlternativeLift m n] (x y : m α) : liftM (x <|> y) = (liftM x <|> liftM y : n α)

lemma probEvent_query_eq_mul_inv (p : spec.range i → Prop) [DecidablePred p] :
    [p | (query i t : OracleComp spec _)] =
      (Finset.univ.filter p).card * (↑(Fintype.card (spec.range i)))⁻¹

@[simp] lemma probFailure_eqRec : [⊥ | h ▸ oa] = [⊥ | oa]

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

@[simp]
lemma query_inj (i : ι) (t t' : spec.domain i) :
    (query i t : OracleComp spec (spec.range i)) = query i t' ↔ t = t'

@[simp] -- NOTE: debatable if this should be simp
lemma guard_eq {ι : Type} {spec : OracleSpec ι} (p : Prop) [Decidable p] :
    (guard p : OracleComp spec Unit) = if p then pure () else failure

@[simp]
lemma map_pure (f : PureEquiv m n) {α : Type u} (x : α) :
    f.toFun (pure x) = (pure x : n α)

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

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

<local_ctx>
import ToMathlib.Control.Monad.Hom

import Mathlib.Logic.Function.Defs

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

namespace NatEquiv

variable {m : Type u → Type v} {n : Type u → Type w} {p : Type u → Type z}

end NatEquiv

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

namespace PureEquiv

variable {m : Type u → Type v} [Pure m] {n : Type u → Type w} [Pure n]
</local_ctx>

<target_theorem>
@[simp]
lemma map_pure_inv (f : PureEquiv m n) {α : Type u} (x : α) :
    f.invFun (pure x) = (pure x : m α) :=
</target_theorem>

