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 α

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

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

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

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

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

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

def cases {α} {motive : {n : ℕ} → Vector α n → Sort*} (v_empty : motive #v[])
  (v_insert : {n : ℕ} → (hd : α) → (tl : Vector α n) → motive (tl.insertIdx 0 hd)) {m : ℕ} :
    (v : Vector α m) → motive v := match hm : m with
  | 0 => fun v => match v with | ⟨⟨[]⟩, rfl⟩ => v_empty
  | n + 1 => fun v => match hv : v with
    | ⟨⟨hd :: tl⟩, hSize⟩ => by admit /- proof elided -/

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

@[inline, reducible]
protected def domain (spec : OracleSpec ι) (i : ι) : Type v := (spec i).1

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

ExceptT.lift in Init.Control.Except

instance : Coseq NonEmptyList where
  coseq := NonEmptyList.zip

Fintype in Mathlib.Data.Fintype.Defs

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

String.decEq in Init.Prelude

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

Except in Init.Prelude

structure Context where
  sender_id : BitVec 256
  recipient_id : BitVec 256
  timestamp : Nat
  message_id : Nat
  deriving Repr

instHMul 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

@[simp]
def map (f : α → β) (z : Zipper α) : Zipper β :=
  ⟨ List.map f z.left, f z.focus, List.map f z.right ⟩

Option in Init.Prelude

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

MonadStateOf.get in Init.Prelude

def initial {P : PFunctor.{uA, uB}} : Lens 0 P :=
  PEmpty.elim ⇆ fun a => PEmpty.elim a

def uliftEquiv : P ≃ₚ (P.ulift : PFunctor.{max uA₁ u, max uB₁ v}) :=
  sorry

PMF.uniformOfFinset in Mathlib.Probability.Distributions.Uniform

def uniformErrSamp {p : ℕ} (χ : ℕ) (hχ : p > 2*χ) : ProbComp (Fin p) := do
  let e ←$ᵗ Fin (2*χ + 1)
  haveI : NeZero p := ⟨by admit /- proof elided -/
  ⟩
  return (Fin.castLE hχ e) - ⟨χ, by admit /- proof elided -/
  ⟩

Option.isNone in Init.Data.Option.Basic

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'

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

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

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

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

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

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

Equiv in Mathlib.Logic.Equiv.Defs

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

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

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

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

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 }

OptionT in Init.Control.Option

def LHL_Consequence_Game_1 (adv : LHL_Consequence_Adv n p) : ProbComp Bool := do
  let x ←$ᵗ Vector (Fin p) n
  let y ←$ᵗ Fin p
  adv (x, y)

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

instance [Monoid ω] [LawfulMonad m] [LawfulAlternative m] :
    LawfulAlternative (WriterT ω m) := sorry

@[inline] def pure (a : α) : FreeContT f m α :=
  fun _ handlePure => handlePure a

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

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

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

def effectObserve (m : Type u → Type v) (α : Type u) := m α → (m α → Prop) → Prop

instDecidableAnd in Init.Prelude

instance domain_decidableEq {i : ι} [h : spec.DecidableEq] :
    DecidableEq (spec.domain i) := h.domain_decidableEq' i

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

Vector.push in Init.Data.Vector.Basic

Function.RightInverse in Init.Data.Function

instance : LawfulComonad (Prod ε) where
  
  map_eq_extend_extract := by admit /- proof elided -/

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

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

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

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

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

noncomputable def ProbComp.advantage (p : ProbComp Unit) : ℝ := |1 / 2 - ([= () | p]).toReal|

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

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

ContT in Mathlib.Control.Monad.Cont

List.cons in Init.Prelude

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

IO.println in Init.System.IO

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

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

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

instance : Coe (MonadEquiv m n) (MonadHom m n) where
  coe f := ⟨f.toNatHom, f.map_pure, f.map_bind⟩

@[always_inline, inline]
def liftPos (a : P.A) : FreeM P (P.B a) := FreeM.roll a FreeM.pure

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

class IsMonadHom (m : Type u → Type v) [Pure m] [Bind m]
    (n : Type u → Type w) [Pure n] [Bind n]
    (f : {α : Type u} → m α → n α) where
  map_pure {α} (x : α) : f (pure x) = pure x
  map_bind {α β} (x : m α) (y : α → m β) : f (x >>= y) = f x >>= f ∘ y

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

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

ExceptT.mk in Init.Control.Except

ContinuousAdd in Mathlib.Topology.Algebra.Monoid.Defs

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

class LawfulDijkstraMonadLift (w₁ : Type u → Type v) (w₂ : Type u → Type w)
    (d₁ : {α : Type u} → w₁ α → Type z) (d₂ : {α : Type u} → w₂ α → Type z)
    [Monad w₁] [Monad w₂] [MonadLiftT w₁ w₂] [DijkstraMonad w₁ d₁] [DijkstraMonad w₂ d₂]
    [inst : DijkstraMonadMorphism w₁ w₂ d₁ d₂]
    [LawfulMonad w₁] [LawfulMonad w₂] [LawfulMonadLiftT w₁ w₂] where
  dMorphism_dPure {α : Type u} (a : α) :
    (monadLift_pure (m := w₁) (n := w₂) a) ▸ (dMorphism (dPure a : d₁ _)) = (dPure a : d₂ _)
  dMorphism_dBind {α β : Type u} {a : w₁ α} {f : α → w₁ β} (x : d₁ a) (g : (a : α) → d₁ (f a)) :
    (monadLift_bind (m := w₁) (n := w₂) a f) ▸ (dMorphism x >>=ᵈ (fun a => dMorphism (g a))) =
      inst.dMorphism (x >>=ᵈ g)

@[inline, reducible]
def rename (spec : OracleSpec ι) (f : τ → ι) : OracleSpec τ := spec ∘ f

instance : Inhabited (OracleSpec ι) := ⟨λ _ ↦ (PUnit, PUnit)⟩

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

Finset in Mathlib.Data.Finset.Defs

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

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

OfNat in Init.Prelude

Function.uncurry in Init.Data.Function

def totalQueries [FiniteRange spec] {α : Type v} (oa : OracleComp spec α) : ℕ :=

noncomputable def depth : FreeMonad f α → ℕ∞
  | .pure _ => 0
  | .roll _ r => 1 + iSup (λ u ↦ depth (r u))

def tensorComm (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) : P ⊗ Q ≃ₗ Q ⊗ P where
  toLens := Prod.swap ⇆ (fun _ => Prod.swap)
  invLens := Prod.swap ⇆ (fun _ => Prod.swap)
  left_inv := rfl
  right_inv := rfl

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)

LawfulMonadLiftT in Init.Control.Lawful.MonadLift.Basic

List.replicate in Init.Data.List.Basic

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

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

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

StateT.run in Init.Control.State

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

Preorder in Mathlib.Order.Defs.PartialOrder

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

def rightKanExtension {α β : Type u} (f : w β) (p : w α) :=
  { ext : β → w α // f >>= ext ≤ₘ p ∧ (∀ w', f >>= w' ≤ₘ p → ∀ a, w' a ≤ₘ ext a) }

NeZero in Init.Data.NeZero

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 : Comonad (CofreeC F) where
  extract := extract
  extend := sorry
  coseq := sorry

instance [RelativePure Id f] : Pure f where
  pure := @pureᵣ Id f _

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

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

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

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

@[reducible] def monadLE {m} [OrderedMonad m] : {α : Type u} → m α → m α → Prop :=
  monadOrder.le

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

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

def generateSingleSeed (spec : OracleSpec ι) (i : ι) [SelectableType (spec.range i)]
    (n : ℕ) : ProbComp (QuerySeed spec) :=
  QuerySeed.ofList <$> ($ᵗ spec.range i).replicate n

HEq in Init.Prelude

def refl (m : Type u → Type v) : NatEquiv m m where
  toFun := id
  invFun := id
  left_inv := by admit /- proof elided -/

instReprString in Init.Data.Repr

instance : Coapplicative Zipper where
  coseq := coseq

instance {m} [Monad m] [Commutative m] {α β} (ma : m α) (mb : m β) :
    CommutativeAt m ma mb := bind_comm ma mb

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

Classical.arbitrary in Mathlib.Logic.Nonempty

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

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

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

iSup in Mathlib.Order.SetNotation

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

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

instance {m n} [Monad m] [OrderedMonad n] [MonadLiftT m n] : MonadRelation m n where
  monadRel := fun a b => monadLift a ≤ₘ b

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 unforgeableExp {sigAlg : SignatureAlg (OracleComp spec) M PK SK S}
    (adv : unforgeableAdv sigAlg) : ProbComp Bool :=
  sigAlg.exec do
    let (pk, sk) ← sigAlg.keygen
    
    let sim_adv : WriterT (QueryLog (M →ₒ S)) (OracleComp spec) (M × S) :=
      simulateQ (idOracle ++ₛₒ sigAlg.signingOracle pk sk) (adv.main pk)
    
    let ((m, σ), log) ← sim_adv.run
    return !(log.wasQueried () m) && (← sigAlg.verify pk m σ)

def zeroCoprod :
    Lens.Equiv.{max uA uA₁, uB, uA₁, uB} ((0 : PFunctor.{uA, uB}) + P) P where
  toLens := Lens.sumPair Lens.initial (Lens.id P)
  invLens := Lens.inr
  left_inv := by admit /- proof elided -/

BitVec in Init.Prelude

instance {P : PFunctor.{uA, uB}} [inst : P.Fintype] : PFunctor.Fintype (PFunctor.ulift P) where
  fintype_B := fun a => by admit /- proof elided -/

def cacheQuery  (i : ι) (t : spec.domain i) (u : spec.range i) :
    QueryCache spec := Function.update cache i (Function.update (cache i) t u)

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

List.count in Init.Data.List.Basic

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

CategoryTheory.inv in Mathlib.CategoryTheory.Iso

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

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

def tensorMap {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}}
    {W : PFunctor.{uA₄, uB₄}} (l₁ : Lens P R) (l₂ : Lens Q W) :
    Lens.{max uA₁ uA₂, max uB₁ uB₂, max uA₃ uA₄, max uB₃ uB₄} (P ⊗ Q) (R ⊗ W) :=
  (fun ⟨pa, qa⟩ => (l₁.toFunA pa, l₂.toFunA qa)) ⇆
    (fun ⟨_pa, qa⟩ ⟨rb, wb⟩ => (l₁.toFunB _pa rb, l₂.toFunB qa wb))

def dIte {w d} [Monad w] [DijkstraMonad w d] {α} (c : Prop) [Decidable c] {t e : w α} :
    d t → d e → d (ite c t e) :=
  fun dt de => dDite c (fun _ => dt) (fun _ => de)

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

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

def unifSpec' : OracleSpec.{u+1,u} (Type u) :=
  λ α : Type u ↦ (PUnit, α)

modifyThe in Init.Prelude

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

instance : CoseqRight Stream' where
  coseqRight _ s₂ := s₂

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

List.Vector in Mathlib.Data.Vector.Defs

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

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

def withCaching (so : QueryImpl spec m) : QueryImpl spec (StateT spec.QueryCache m) where
  impl | query i t => do match (← get) i t with
    | Option.some u => return u
    | Option.none =>
        let u ← so.impl (query i t)
        modifyGet fun cache => (u, cache.cacheQuery i t u)

def LWE_Game_1 (adv : LWE_Adversary n m p) : ProbComp Bool := do
  let distr ← LWE_Uniform_Distr n m p
  let b ← adv distr
  return b

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

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

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

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

Monoid.toOne in Mathlib.Algebra.Group.Defs

Subsingleton in Init.Core

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

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

StateT.mk in Init.Control.State

Fin.val in Init.Prelude

instance : Extract Id where
  extract := id

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

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

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

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

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

instance decidablePred_mem_finSupport [spec.DecidableEq] [spec.FiniteRange] [DecidableEq α]
    (oa : OracleComp spec α) : DecidablePred (· ∈ oa.finSupport) :=

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

StateT in Init.Control.State

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

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

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

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

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

def sigmaCompDistrib {I : Type v} (F : I → PFunctor.{uA₁, uB₁}) (P : PFunctor.{uA₂, uB₂}) :
    sigma F ◃ P ≃ₚ sigma (fun i => F i ◃ P) where
  equivA := sorry
  equivB := sorry

PEmpty.instIsEmpty in Mathlib.Logic.IsEmpty

structure List.Zipper (α : Type u) where
  left   : List α 
  focus  : α      
  right  : List α

liftM in Init.Prelude

instance [MonadLift (OracleQuery spec) (OracleQuery superSpec)] :
    MonadLift (OracleComp spec) (OracleComp superSpec) where
  monadLift oa := liftComp oa superSpec

def FreeContT (f : Type z → Type y) (m : Type u → Type v) (α : Type w) :
    Type (max (u + 1) v w y (z + 1)) :=
  {r : Type u} → ({x : Type z} → f x → ContT r m x) → ContT r m α

OfNat.ofNat in Init.Prelude

Finite in Mathlib.Data.Finite.Defs

Finset.biUnion in Mathlib.Data.Finset.Union

Sum.inr in Init.Core

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

class LawfulRelativeFunctor (j : Type u → Type w) (f : Type u → Type v)
    [RelativeFunctor j f] where

MonadFunctorT in Init.Prelude
</all_available_defs>

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

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

@[simp]
lemma depth_roll {x : f α} {r : α → FreeMonad f β} :
    depth (roll x r : FreeMonad f β) = 1 + iSup (λ u ↦ depth (r u))

@[simp]
lemma probOutput_pure_self (x : α) : [= x | (pure x : OracleComp spec α)] = 1

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

@[simp]
theorem getThe_eq [MonadStateOf σ m] : getThe σ (m := m) = MonadStateOf.get

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

lemma cons_mem_finSupport_seq_map_cons_iff [spec.FiniteRange] [spec.DecidableEq] [DecidableEq α]
    (x : α) (xs : List α) : x :: xs ∈ (cons <$> oa <*> ob).finSupport ↔
      x ∈ oa.finSupport ∧ xs ∈ ob.finSupport

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

lemma probEvent_eq_sum_fintype_ite [DecidablePred p] [Fintype α] :
    [p | oa] = ∑ x : α, if p x then [= x | oa] else 0

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

@[simp]
lemma evalDist_apply_eq_zero_iff (x : Option α) :
    (evalDist oa).run x = 0 ↔ x.rec ([⊥ | oa] = 0) (· ∉ oa.support)

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

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

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

lemma probOutput_seq_map_eq_tsum [spec.FiniteRange]
    (z : γ) : [= z | f <$> oa <*> ob] = ∑' (x : α) (y : β),
      [= x | oa] * [= y | ob] * [= z | (pure (f x y) : OracleComp spec γ)]

lemma mem_finSupport_iff_probOutput_ne_zero [spec.DecidableEq] [DecidableEq α] :
    x ∈ oa.finSupport ↔ [= x | oa] ≠ 0

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

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

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

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

lemma probEvent_eq_sum_filter_finSupport [spec.DecidableEq] [DecidablePred p] [DecidableEq α] :
    [p | oa] = ∑ x ∈ oa.finSupport.filter p, [= x | oa]

lemma probFailure_bind_eq_tsum :
    [⊥ | oa >>= ob] = [⊥ | oa] + ∑' x : α, [= x | oa] * [⊥ | ob x]

lemma Fin_bound_shift_cast_vec {p χ m : ℕ} {v : Vector (Fin (2*χ + 1)) m} [NeZero p] (h : p > 2*χ) :
    Fin_Bound_vec (v.map (fun t ↦ (Fin.castLE h t) - (Fin.ofNat p χ))) χ

lemma probOutput_bind_of_const (y : β) (r : ℝ≥0∞) (h : ∀ x, [= y | ob x] = r) :
    [= y | oa >>= ob] = (1 - [⊥ | oa]) * r

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

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

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

theorem bind_eq_pmf_bind {p : SPMF α} {f : α → SPMF β} :
    (p >>= f) = PMF.bind p (fun a => match a with | some a' => f a' | none => PMF.pure none)

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

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

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

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

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

theorem bind_comm_triple_swap_23 {m} [Monad m] [LawfulMonad m] [Commutative m] {α β γ δ}
    (ma : m α) (mb : m β) (mc : m γ) (f : α × β × γ → m δ) :
    (do let a ← ma; let b ← mb; let c ← mc; f (a, b, c)) =
    (ma >>= fun a => mc >>= fun c => mb >>= fun b => f (a, b, c))

@[simp]
lemma 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]

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

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

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

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

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

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

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

@[simp]
lemma pure_inj (x y : α) : (pure x : OracleComp spec α) = pure y ↔ x = y

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 probFailure_list_mapM {α β : Type*} [spec.FiniteRange] (xs : List α)
    (f : α → OracleComp spec β) : [⊥ | xs.mapM f] = 1 - (xs.map (1 - [⊥ | f ·])).prod

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

theorem map_eq_pure_bindᵣ [RelativeMonad j m] [LawfulRelativeMonad j m]
    (f : j α → j β) (x : m α) : f <$>ᵣ x = x >>=ᵣ fun a => pureᵣ (f a)

@[simp]
lemma liftComp_query (q : OracleQuery spec α) :
    liftComp (q : OracleComp spec _) superSpec = liftM q

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

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

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

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

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

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

protected lemma orElse_def (oa oa' : OracleComp spec α) : (oa <|> oa') = OptionT.mk
      (do match ← OptionT.run oa with | some a => pure (some a) | _  => OptionT.run oa')

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 fst_map_run_simulateQ (oa : OracleComp spec α) :
    (Prod.fst <$> (simulateQ loggingOracle oa).run) = oa

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

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

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

@[simp]
lemma countQ_logQuery {α} (log : QueryLog spec) (q : OracleQuery spec α) (u : α)
    (i : ι) : (log.logQuery q u).countQ i = log.countQ i + if q.index = i then 1 else 0

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

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

@[simp] theorem map_extract_duplicate_eq_id : Functor.map extract (duplicate wa) = wa

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

@[simp]
lemma probOutput_seq_map_vector_cons_eq_mul [spec.FiniteRange] [spec.DecidableEq]
    (xs : List.Vector α (n + 1)) :
    [= xs | (· ::ᵥ ·) <$> oa <*> ob] = [= xs.head | oa] * [= xs.tail | ob]

lemma eq_failure_of_isFailure {oa : OracleComp spec α} (h : isFailure oa) : oa = failure

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

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

@[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 probFailure_orElse {ι : Type u} {spec : OracleSpec ι} {α : Type u} [h : spec.FiniteRange]
    (oa oa' : OracleComp spec α) : [⊥ | oa <|> oa'] = [⊥ | oa] * [⊥ | oa']

@[simp]
theorem ulift_B {a : P.A} : (P.ulift).B (ULift.up a) = ULift (P.B a)

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

@[simp]
lemma Fin_Bound_add {n b₁ b₂ : ℕ} {x y : Fin n} (h₁ : Fin_Bound x b₁)
 (h₂ : Fin_Bound y b₂) : Fin_Bound (x + y) (b₁ + b₂)

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

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

theorem validateAbuseReport_is_sound (message_content : String) :
    [= true | do
      -- basically simulation_setup
      let facebook_key := BitVec.ofNat 256 123456789
      let context : Context := {
        sender_id := BitVec.ofNat 256 1001,
        recipient_id := BitVec.ofNat 256 1002,
        timestamp := 1730230302,
        message_id := 123 }
      -- simulation data
      let maybeData ← simulation_setup message_content
      match maybeData with
      | none => return false
      | some data =>
        let valid_abuse_report := {
          message := data.verified_msg,
          franking_tag := data.message_package.franking_tag,
          reporting_tag := data.message_package.reporting_tag,
          context := data.message_package.context }
        -- validation result
        return validate_abuse_report valid_abuse_report data.facebook_key] = 1

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

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

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

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

@[simp] lemma C_unit : C PUnit = 1

lemma list_mapM_loop_eq {m : Type u → Type v} [Monad m] [LawfulMonad m]
    {α : Type w} {β : Type u} (xs : List α) (f : α → m β) (ys : List β) :
    List.mapM.loop f xs ys = (ys.reverse ++ ·) <$> List.mapM.loop f xs []

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

@[simp]
lemma countQ_singleton {α} (q : OracleQuery spec α) (u : α) (i : ι) :
    countQ (singleton q u) i = if q.index = i then 1 else 0

@[simp] lemma probFailure_uniformSelectList (xs : List α) :
    [⊥ | $ xs] = if xs.isEmpty then 1 else 0

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

lemma probOutput_pure_eq_one {x y : α} (h : y = x) :
    [= y | (pure x : OracleComp spec α)] = 1

@[simp] lemma probEvent_lt_top : [p | oa] < ∞

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

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

@[simp]
lemma probOutput_pos_iff' [spec.DecidableEq] [DecidableEq α] :
    0 < [= x | oa] ↔ x ∈ oa.finSupport

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

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

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

lemma probFailure_bind_eq_sum_fintype [Fintype α] :
    [⊥ | oa >>= ob] = [⊥ | oa] + ∑ x : α, [= x | oa] * [⊥ | ob x]

@[simp] lemma probFailure_eq : probFailure p = 0

@[simp] lemma support_uniformSelectFinset [DecidableEq α] (s : Finset α) :
    ($ s).support = if s.Nonempty then ↑s else ∅

@[simp]
lemma probOutput_eq_zero_iff' [spec.DecidableEq] [DecidableEq α] :
    [= x | oa] = 0 ↔ x ∉ oa.finSupport

@[simp] lemma probOutput_uniformSelectFinset [DecidableEq α] (s : Finset α) (x : α) :
    [= x | $ s] = if x ∈ s then (s.card : ℝ≥0∞)⁻¹ else 0

theorem set_set {s₁ s₂ : σ} : (do StateT.set s₁; StateT.set s₂) = StateT.set (m := m) s₂

theorem monadLift_guard [AlternativeMonad m] [AlternativeMonad n] [MonadLift m n]
    [LawfulAlternativeLift m n] [LawfulMonadLift m n] (p : Prop) [Decidable p] :
    monadLift (guard p : m Unit) = (guard p : n Unit)

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

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

lemma probEvent_congr {oa : OracleComp spec α} {oa' : OracleComp spec' α}
    (h1 : ∀ x, p x ↔ q x) (h2 : evalDist oa = evalDist oa') : [p | oa] = [q | oa']

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

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

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

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

lemma Fin_bound_shift_cast {p χ} {a : Fin (2*χ + 1)} [NeZero p] (h : p > 2*χ) :
    Fin_Bound (Fin.castLE h a - (Fin.ofNat p χ)) χ

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

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

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

@[simp] lemma finSupportWhen_failure [DecidableEq α] :
    (failure : OracleComp spec α).finSupportWhen fin_poss = ∅

lemma not_mem_support_iff_probOutput_eq_zero : x ∉ oa.support ↔ [= x | oa] = 0

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

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

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

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

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

@[simp] theorem 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 one_le_probOutput_iff : 1 ≤ [= x | oa] ↔ [= x | oa] = 1

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

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

@[simp] lemma probFailure_ne_top : Pr[⊥ | mx] ≠ ∞

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 allWhen_failure_iff :
    (failure : OracleComp spec α).allWhen Q F possible_outputs ↔ F

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

@[simp]
lemma bind_lift (x : P.Obj α) (r : α → FreeM P β) :
    FreeM.bind (FreeM.lift x) r = FreeM.roll x.1 (fun a ↦ r (x.2 a))

lemma probOutput_seq_map_prod_mk_eq_mul' :
    [= (x, y) | (λ x y ↦ (y, x) : β → α → α × β) <$> ob <*> oa] = [= x | oa] * [= y | ob]

@[simp] lemma allWhen_query_bind (q : OracleQuery spec α) (oa : α → OracleComp spec β) :
    ((q : OracleComp spec α) >>= oa).allWhen Q F possible_outputs ↔
      Q q ∧ ∀ x ∈ possible_outputs q, (oa x).allWhen Q F possible_outputs

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

lemma probFailure_def (mx : m α) : Pr[⊥ | mx] = (evalDist mx).run none

protected lemma bind_congr' {oa oa' : OracleComp spec α} {ob ob' : α → OracleComp spec β}
    (h : oa = oa') (h' : ∀ x, ob x = ob' x) : oa >>= ob = oa' >>= ob'

theorem bind_comm_quad_swap_23 {m} [Monad m] [LawfulMonad m] [Commutative m] {α β γ δ ε}
    (ma : m α) (mb : m β) (mc : m γ) (md : m δ) (f : α × β × γ × δ → m ε) :
    (ma >>= fun a => mb >>= fun b => mc >>= fun c => md >>= fun d => f (a, b, c, d)) =
    (ma >>= fun a => mc >>= fun c => mb >>= fun b => md >>= fun d => f (a, b, c, d))

@[simp]
lemma run_failure [Monoid ω] {α : Type u} : (failure : WriterT ω m α).run = failure

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

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

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

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

@[simp]
lemma support_replicate [spec.FiniteRange] (oa : OracleComp spec α) (n : ℕ) :
    (oa.replicate n).support = {xs | xs.length = n ∧ ∀ x ∈ xs, x ∈ oa.support}

@[simp] lemma linear_A (A : Type u) : (linear A).A = A

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

@[simp] lemma support_uniformOfFintype : ($ᵗ α).support = Set.univ
</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

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

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

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

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

section bounds

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

end bounds

section support

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

variable {oa x p q}

end support

section sums

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

end sums

section pure

variable (x : α)

end pure

section bind

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

end bind

section mul_le_probEvent_bind

end mul_le_probEvent_bind

section bind_const

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

end bind_const

section query

variable (i : ι) (t : spec.domain i)
</local_ctx>

<target_theorem>
@[simp]
lemma probFailure_liftM (q : OracleQuery spec α) :
    [⊥ | (q : OracleComp spec _)] = 0 :=
</target_theorem>

