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>
noncomputable def proof_element_G1_as_poly {F : Type} [Field F]
    (𝓟 : AGMProofSystemInstantiation F) (prover : 𝓟.Prover) (pf_elem : 𝓟.Proof_G1) :
    MvPolynomial (𝓟.Sample) F :=
  (𝓟.ListSRSElements_G1.map fun SRS_elem =>
          MvPolynomial.C (prover.fst pf_elem SRS_elem) * (𝓟.SRSElementValue_G1 SRS_elem)).sum

noncomputable def proof_element_G2_as_poly {F : Type} [Field F]
    (𝓟 : AGMProofSystemInstantiation F) (prover : 𝓟.Prover) (pf_elem : 𝓟.Proof_G2) :
    MvPolynomial (𝓟.Sample) F :=
  (𝓟.ListSRSElements_G2.map fun SRS_elem =>
          MvPolynomial.C (prover.snd pf_elem SRS_elem) * (𝓟.SRSElementValue_G2 SRS_elem)).sum

noncomputable def check_poly {F : Type} [Field F]
    (𝓟 : AGMProofSystemInstantiation F) (prover : 𝓟.Prover) (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) :
    MvPolynomial 𝓟.Sample F :=
  (
  (𝓟.ListPairings check_idx).map fun pairing =>
    𝓟.pairing_poly prover stmt check_idx pairing
  ).sum

def soundness (F : Type) [Field F]
    (𝓟 : AGMProofSystemInstantiation F)
    (Wit : Type) (relation : 𝓟.Stmt -> Wit -> Prop)
    (extractor : 𝓟.Prover -> Wit) : Prop :=
   ∀ stmt : 𝓟.Stmt,
    ∀ prover : 𝓟.Prover,
      𝓟.verify prover stmt -> relation stmt (extractor prover)

inductive Vars : Type where
  | r_v : Vars
  | r_w : Vars
  | α_v : Vars
  | α_w : Vars
  | α_y : Vars
  | β : Vars
  | γ : Vars
deriving Repr, BEq

local notation "poly_r_v" => X (some Vars.r_v)
local notation "poly_r_w" => X (some Vars.r_w)
local notation "poly_α_v" => X (some Vars.α_v)
local notation "poly_α_w" => X (some Vars.α_w)
local notation "poly_α_y" => X (some Vars.α_y)
local notation "poly_β" => X (some Vars.β)
local notation "poly_γ" => X (some Vars.γ)
local notation "poly_s" => X (none)

inductive Vars : Type where
  | α : Vars
  | β_v : Vars
  | β_w : Vars
  | β_y : Vars
  | γ : Vars
deriving Repr, BEq

local notation "poly_α" => X (some Vars.α)
local notation "poly_β_v" => X (some Vars.β_v)
local notation "poly_β_w" => X (some Vars.β_w)
local notation "poly_β_y" => X (some Vars.β_y)
local notation "poly_γ" => X (some Vars.γ)
local notation "poly_s" => X (none)

inductive SRS_Elements_G1_Idx {n_stmt n_wit n_var : ℕ} : Type where
  | α : SRS_Elements_G1_Idx
  | β : SRS_Elements_G1_Idx
  | δ : SRS_Elements_G1_Idx
  | x_pow : Fin n_var → SRS_Elements_G1_Idx
  | x_pow_times_t : Fin (n_var - 1) → SRS_Elements_G1_Idx
  | y : Fin n_stmt → SRS_Elements_G1_Idx
  | q : Fin n_wit → SRS_Elements_G1_Idx

inductive SRS_Elements_G2_Idx {n_stmt n_wit n_var : ℕ} : Type where
  | β : SRS_Elements_G2_Idx
  | γ : SRS_Elements_G2_Idx
  | δ : SRS_Elements_G2_Idx
  | x_pow : Fin n_var → SRS_Elements_G2_Idx

inductive SRS_Elements_G1_Idx {n_stmt n_wit n_var : ℕ} : Type where
  | α : SRS_Elements_G1_Idx
  | β : SRS_Elements_G1_Idx
  | δ : SRS_Elements_G1_Idx
  | x_pow : Fin n_var → SRS_Elements_G1_Idx
  | x_pow_times_t : Fin (n_var - 1) → SRS_Elements_G1_Idx
  | y : Fin n_stmt → SRS_Elements_G1_Idx
  | q : Fin n_wit → SRS_Elements_G1_Idx

inductive SRS_Elements_G2_Idx {n_stmt n_wit n_var : ℕ} : Type where
  | β : SRS_Elements_G2_Idx
  | γ : SRS_Elements_G2_Idx
  | δ : SRS_Elements_G2_Idx
  | x_pow : Fin n_var → SRS_Elements_G2_Idx

noncomputable def to_MvPolynomial_Option {F : Type} [Field F] (V : Type) :
    Polynomial F →+* MvPolynomial (Option V) F
  where
    toFun p := Polynomial.eval₂ (MvPolynomial.C) (MvPolynomial.X none) p
    map_one' := by admit /- proof elided -/

inductive SRS_Elements_G1_Idx {n_stmt n_wit n_var : ℕ} : Type where
  | α : SRS_Elements_G1_Idx
  | β : SRS_Elements_G1_Idx
  | δ : SRS_Elements_G1_Idx
  | x_pow : Fin n_var → SRS_Elements_G1_Idx
  | x_pow_times_t : Fin (n_var - 1) → SRS_Elements_G1_Idx
  | y : Fin n_stmt → SRS_Elements_G1_Idx
  | q : Fin n_wit → SRS_Elements_G1_Idx

inductive SRS_Elements_G2_Idx {n_stmt n_wit n_var : ℕ} : Type where
  | β : SRS_Elements_G2_Idx
  | γ : SRS_Elements_G2_Idx
  | δ : SRS_Elements_G2_Idx
  | x_pow : Fin n_var → SRS_Elements_G2_Idx

def Prover (F : Type) [Field F]
    (𝓟 : AGMProofSystemInstantiation F) : Type :=
  (𝓟.Proof -> 𝓟.SRSElements -> F) × (𝓟.Proof -> 𝓟.SRSElements -> F)

noncomputable def proof_element_as_poly {F : Type} [Field F]
    (𝓟 : AGMProofSystemInstantiation F) (prover : 𝓟.Prover) (pf_elem : 𝓟.Proof) :
    MvPolynomial (𝓟.Sample) F :=
  (𝓟.ListSRSElements.map fun SRS_elem =>
          MvPolynomial.C (prover.fst pf_elem SRS_elem) * (𝓟.SRSElementValue SRS_elem)).sum

noncomputable def pairing_poly {F : Type} [Field F]
    (𝓟 : AGMProofSystemInstantiation F) (prover : 𝓟.Prover) (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx) :
    MvPolynomial 𝓟.Sample F :=
  (
    ( 
      
      (
        (𝓟.ListProof.map fun pf_elem => 
          C (𝓟.verificationPairingProof stmt check_idx pairing pf_elem) 
            *
            
            𝓟.proof_element_as_poly prover pf_elem).sum
      )
      +
      ( 
        (𝓟.ListSRSElements.map fun SRS_elem =>
          C (𝓟.verificationPairingSRS stmt check_idx pairing SRS_elem) * (𝓟.SRSElementValue SRS_elem)).sum
      )
    )
    *
    ( 
      
      (
        (𝓟.ListProof.map fun pf_elem => 
          C (𝓟.verificationPairingProof stmt check_idx pairing pf_elem) 
            *
            
            𝓟.proof_element_as_poly prover pf_elem).sum
      )
      +
      ( 
        (𝓟.ListSRSElements.map fun SRS_elem =>
          C (𝓟.verificationPairingSRS stmt check_idx pairing SRS_elem) * (𝓟.SRSElementValue SRS_elem)).sum
      )
    )
  )

noncomputable def check_poly {F : Type} [Field F]
    (𝓟 : AGMProofSystemInstantiation F) (prover : 𝓟.Prover) (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) :
    MvPolynomial 𝓟.Sample F :=
  (
  (𝓟.ListPairings check_idx).map fun pairing =>
    𝓟.pairing_poly prover stmt check_idx pairing
  ).sum

def verify {F : Type} [Field F]
    (𝓟 : AGMProofSystemInstantiation F) (prover : 𝓟.Prover) (stmt : 𝓟.Stmt) : Prop :=
  (
    ∀ check_idx : 𝓟.EqualityChecks, 𝓟.check_poly prover stmt check_idx = 0
  )
  ∧
  ∀ pfs ∈ 𝓟.Identified_Proof_Elems,
    𝓟.proof_element_as_poly prover pfs.fst = 𝓟.proof_element_as_poly prover pfs.snd

def soundness (F : Type) [Field F]
    (𝓟 : AGMProofSystemInstantiation F)
    (Wit : Type) (relation : 𝓟.Stmt -> Wit -> Prop)
    (extractor : 𝓟.Prover -> Wit) : Prop :=
   ∀ stmt : 𝓟.Stmt,
    ∀ prover : 𝓟.Prover,
      𝓟.verify prover stmt -> relation stmt (extractor prover)

structure AGMProofSystemInstantiation (F : Type) [Field F] where
  Stmt Sample SRSElements Proof EqualityChecks : Type

ListSRSElements : List SRSElements
  SRSElementValue : SRSElements → MvPolynomial Sample F
  ListProof : List Proof
  Pairings : EqualityChecks → Type
  ListPairings : (k : EqualityChecks) → List (Pairings k)
  verificationPairingSRS_G1 : Stmt -> (k : EqualityChecks) → Pairings k → SRSElements → F
  verificationPairingSRS_G2 : Stmt -> (k : EqualityChecks) → Pairings k → SRSElements → F
  verificationPairingProof_G1 : Stmt -> (k : EqualityChecks) → Pairings k → Proof → F
  verificationPairingProof_G2 : Stmt -> (k : EqualityChecks) → Pairings k → Proof → F

def Prover (F : Type) [Field F]
    (𝓟 : AGMProofSystemInstantiation F) : Type :=
  (𝓟.Proof -> 𝓟.SRSElements -> F) × (𝓟.Proof -> 𝓟.SRSElements -> F)

def soundness (F : Type) [Field F]
    (𝓟 : AGMProofSystemInstantiation F)
    (Wit : Type) (relation : 𝓟.Stmt -> Wit -> Prop)
    (extractor : 𝓟.Prover -> Wit) : Prop :=
   ∀ stmt : 𝓟.Stmt,
    ∀ prover : 𝓟.Prover,
      𝓟.verify prover stmt -> relation stmt (extractor prover)

noncomputable def pairing_poly {F : Type} [Field F]
    (𝓟 : AGMProofSystemInstantiation F) (prover : 𝓟.Prover) (stmt : 𝓟.Stmt) (check_idx : 𝓟.EqualityChecks) (pairing : 𝓟.Pairings check_idx) :
    MvPolynomial 𝓟.Sample F :=
  (
    ( 
      
      (
        (𝓟.ListProof_G1.map fun pf_elem => 
          C (𝓟.verificationPairingProof_G1 stmt check_idx pairing pf_elem) 
            *
            
            𝓟.proof_element_G1_as_poly prover pf_elem).sum
      )
      +
      ( 
        (𝓟.ListSRSElements_G1.map fun SRS_elem =>
          C (𝓟.verificationPairingSRS_G1 stmt check_idx pairing SRS_elem) * (𝓟.SRSElementValue_G1 SRS_elem)).sum
      )
    )
    *
    ( 
      
      (
        (𝓟.ListProof_G2.map fun pf_elem => 
          C (𝓟.verificationPairingProof_G2 stmt check_idx pairing pf_elem) 
            *
            
            𝓟.proof_element_G2_as_poly prover pf_elem).sum
      )
      +
      ( 
        (𝓟.ListSRSElements_G2.map fun SRS_elem =>
          C (𝓟.verificationPairingSRS_G2 stmt check_idx pairing SRS_elem) * (𝓟.SRSElementValue_G2 SRS_elem)).sum
      )
    )
  )

def elabPatterns_Or (pats : Array Term) : TermElabM (Array AbstractMVarsResult) :=
  withTheReader Term.Context (fun ctx ↦ { ctx with ignoreTCFailures := true }) <|
  Term.withoutErrToSorry <|
  pats.mapM fun p ↦ Term.withoutModifyingElabMetaStateWithInfo do
    withRef p <| abstractMVars (← Term.elabTerm p none)

inductive Proof_G2_Idx : Type where
  | B : Proof_G2_Idx

ListPairings : (k : EqualityChecks) → List (Pairings k)

inductive Vars : Type where
  | α : Vars
  | β : Vars
  | γ : Vars
  | δ : Vars
deriving Repr, BEq

Lean.Elab.Term.Context in Lean.Elab.Term.TermElabM

inductive Proof_G1_Idx : Type where
  | A : Proof_G1_Idx
  | C : Proof_G1_Idx

noncomputable def v_sum {F : Type} [Field F] {n_stmt n_wit : ℕ}
    (v_stmt : Fin n_stmt → (Polynomial F))
    (v_wit : Fin n_wit → (Polynomial F))
    (stmt : Fin n_stmt -> F)
    (wit : Fin n_wit -> F)
    : Polynomial F :=
  List.sum (List.map (fun j => Polynomial.C (stmt j) * (v_stmt j)) (List.finRange n_stmt))
  + List.sum (List.map (fun j => Polynomial.C (wit j) * (v_wit j)) (List.finRange n_wit))

structure AGMProofSystemInstantiation (F : Type) [Field F] where
   
  Stmt : Type
   
  Sample : Type
   
  SRSElements : Type
  ListSRSElements : List SRSElements

EqualityChecks : Type

MvPolynomial.eval₂ in Mathlib.Algebra.MvPolynomial.Eval

inductive Proof_G1_Idx : Type where
  | V_mid : Proof_G1_Idx
  | V_mid' : Proof_G1_Idx
  | W' : Proof_G1_Idx
  | Y : Proof_G1_Idx
  | H' : Proof_G1_Idx

Finset.univ in Mathlib.Data.Fintype.Defs

noncomputable def changeExponent_G1 (𝓟 : AGMProofSystemInstantiation F) (sample : 𝓟.Sample)
    (d : ℕ) :
    AGMProofSystemInstantiation F where
      Stmt := 𝓟.Stmt
      Sample := 𝓟.Sample
      SRSElements_G1 := 𝓟.SRSElements_G1
      ListSRSElements_G1 := 𝓟.ListSRSElements_G1
      SRSElements_G2 := 𝓟.SRSElements_G2
      ListSRSElements_G2 := 𝓟.ListSRSElements_G2
      SRSElementValue_G1 := fun i => MvPolynomial.X sample ^ d * 𝓟.SRSElementValue_G1 i
      SRSElementValue_G2 := 𝓟.SRSElementValue_G2
      Proof_G1 := 𝓟.Proof_G1
      ListProof_G1 := 𝓟.ListProof_G1
      Proof_G2 := 𝓟.Proof_G2
      ListProof_G2 := 𝓟.ListProof_G2
      EqualityChecks := 𝓟.EqualityChecks
      Pairings := 𝓟.Pairings
      ListPairings := 𝓟.ListPairings
      verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1
      verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2
      verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1
      verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2
      Identified_Proof_Elems := 𝓟.Identified_Proof_Elems

verificationPairingSRS_G1 : Stmt -> (k : EqualityChecks) → Pairings k → SRSElements → F
   
  verificationPairingSRS_G2 : Stmt -> (k : EqualityChecks) → Pairings k → SRSElements → F
   
  verificationPairingProof_G1 : Stmt -> (k : EqualityChecks) → Pairings k → Proof → F
   
  verificationPairingProof_G2 : Stmt -> (k : EqualityChecks) → Pairings k → Proof → F

inductive PairingsII_Idx : Type where
  | bγ : PairingsII_Idx
  | γβv : PairingsII_Idx

EquivLike in Mathlib.Data.FunLike.Equiv

Lean.FVarId in Lean.Expr

Lean.instantiateMVars in Lean.MetavarContext

def AGMProofSystemInstantiation.soundness (F : Type) [Field F]
    (𝓟 : AGMProofSystemInstantiation F)
    (Wit : Type) (relation : 𝓟.Stmt -> Wit -> Prop)
    (extractor : 𝓟.Prover -> Wit) : Prop :=
   ∀ stmt : 𝓟.Stmt,
    ∀ prover : 𝓟.Prover,
      𝓟.verify prover stmt -> relation stmt (extractor prover)

nProof_G1 : ℕ
  nProof_G2 : ℕ

EqualityChecks : Type

Function.comp in Init.Prelude

Lean.Meta.MetaM in Lean.Meta.Basic

def Proof_G2_Idx : Type := Empty

Lean.Syntax in Init.Prelude

Fin in Init.Prelude

Polynomial.eval₂ in Mathlib.Algebra.Polynomial.Eval.Defs

EqualityChecks : Type

noncomputable def Pinocchio
     
    {F : Type} [Field F]
     
    {n_stmt n_wit d : ℕ}
    
    
    
    
    
     
    {v_stmt : Fin n_stmt → Polynomial F }
    {w_stmt : Fin n_stmt → Polynomial F }
    {y_stmt : Fin n_stmt → Polynomial F }
    {v_wit : Fin n_wit → Polynomial F }
    {w_wit : Fin n_wit → Polynomial F }
    {y_wit : Fin n_wit → Polynomial F }
    {v_0 : Polynomial F }
    {w_0 : Polynomial F }
    {y_0 : Polynomial F }
     
    {t : Polynomial F}
    
    
    
    :
    AGMProofSystemInstantiation F :=
  { Stmt := Fin n_stmt → F
    Sample := Option Vars
    SRSElements_G1 := @SRS_Elements_Idx n_stmt n_wit d
    ListSRSElements_G1 :=
      ((List.finRange n_wit).map fun i => SRS_Elements_Idx.EK_v i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_Idx.EK_w i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_Idx.EK_y i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_Idx.EK_α_v i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_Idx.EK_α_w i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_Idx.EK_α_y i)
      ++ ((List.finRange d).map fun i => SRS_Elements_Idx.EK_s_pow i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_Idx.EK_β_v_w_y i)
      ++ [SRS_Elements_Idx.VK_1, SRS_Elements_Idx.VK_α_v, SRS_Elements_Idx.VK_α_w, SRS_Elements_Idx.VK_α_y, SRS_Elements_Idx.VK_γ, SRS_Elements_Idx.VK_βγ, SRS_Elements_Idx.VK_t, SRS_Elements_Idx.VK_v_0, SRS_Elements_Idx.VK_w_0, SRS_Elements_Idx.VK_y_0]
      ++ ((List.finRange n_stmt).map fun i => SRS_Elements_Idx.VK_v_stmt i)
      ++ ((List.finRange n_stmt).map fun i => SRS_Elements_Idx.VK_w_stmt i)
      ++ ((List.finRange n_stmt).map fun i => SRS_Elements_Idx.VK_y_stmt i)
    
    SRSElements_G2 := @SRS_Elements_Idx n_stmt n_wit d
    ListSRSElements_G2 :=
      ((List.finRange n_wit).map fun i => SRS_Elements_Idx.EK_v i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_Idx.EK_w i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_Idx.EK_y i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_Idx.EK_α_v i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_Idx.EK_α_w i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_Idx.EK_α_y i)
      ++ ((List.finRange d).map fun i => SRS_Elements_Idx.EK_s_pow i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_Idx.EK_β_v_w_y i)
      ++ [SRS_Elements_Idx.VK_1, SRS_Elements_Idx.VK_α_v, SRS_Elements_Idx.VK_α_w, SRS_Elements_Idx.VK_α_y, SRS_Elements_Idx.VK_γ, SRS_Elements_Idx.VK_βγ, SRS_Elements_Idx.VK_t, SRS_Elements_Idx.VK_v_0, SRS_Elements_Idx.VK_w_0, SRS_Elements_Idx.VK_y_0]
      ++ ((List.finRange n_stmt).map fun i => SRS_Elements_Idx.VK_v_stmt i)
      ++ ((List.finRange n_stmt).map fun i => SRS_Elements_Idx.VK_w_stmt i)
      ++ ((List.finRange n_stmt).map fun i => SRS_Elements_Idx.VK_y_stmt i)

instance : Fintype Proof_G2_Idx :=
  ⟨⟨[Proof_G2_Idx.B], by admit /- proof elided -/
  ⟩, fun x => by admit /- proof elided -/
  ⟩

Sum in Init.Core

inductive PairingsI_Idx : Type where
  | lhs : PairingsI_Idx
  | rhs1 : PairingsI_Idx
  | rhs2 : PairingsI_Idx

noncomputable def collapseSRSElement_G1 (𝓟 : AGMProofSystemInstantiation F)
    [DecidableEq 𝓟.SRSElements_G1] (twin1 twin2 : 𝓟.SRSElements_G1) :
    AGMProofSystemInstantiation F where
      Stmt := 𝓟.Stmt
      Sample := 𝓟.Sample
      SRSElements_G1 := 𝓟.SRSElements_G1
      ListSRSElements_G1 := 𝓟.ListSRSElements_G1
      SRSElements_G2 := 𝓟.SRSElements_G2
      ListSRSElements_G2 := 𝓟.ListSRSElements_G2
      SRSElementValue_G1 := fun srs => if srs = twin1
                                        then 𝓟.SRSElementValue_G1 twin1 + 𝓟.SRSElementValue_G1 twin2
                                        else if srs = twin2 then 0 else 𝓟.SRSElementValue_G1 srs
      SRSElementValue_G2 := 𝓟.SRSElementValue_G2
      Proof_G1 := 𝓟.Proof_G1
      ListProof_G1 := 𝓟.ListProof_G1
      Proof_G2 := 𝓟.Proof_G2
      ListProof_G2 := 𝓟.ListProof_G2
      EqualityChecks := 𝓟.EqualityChecks
      Pairings := 𝓟.Pairings
      ListPairings := 𝓟.ListPairings
      verificationPairingSRS_G1 := 𝓟.verificationPairingSRS_G1
      verificationPairingSRS_G2 := 𝓟.verificationPairingSRS_G2
      verificationPairingProof_G1 := 𝓟.verificationPairingProof_G1
      verificationPairingProof_G2 := 𝓟.verificationPairingProof_G2
      Identified_Proof_Elems := 𝓟.Identified_Proof_Elems

elab tk:"##" tac:(tacticSeq)? : command => do
  let state :: rest := proofStateExt.getState (← getEnv)
    | throwError "proof mode not started, use `start_proof`"
  Elab.Command.liftTermElabM do
    state.with do
      Elab.Tactic.withTacticInfoContext tk do
        if let some tac := tac then
          Elab.Tactic.evalTactic tac
      if (← Elab.Tactic.getUnsolvedGoals).isEmpty then
        logInfoAt tk "Goals accomplished 🎉"
        modifyEnv (proofStateExt.setState · rest)
      else
        modifyEnv (proofStateExt.setState · ((← ProofState.get) :: rest))

inductive Proof_Idx : Type where
  | A : Proof_Idx
  | B : Proof_Idx
  | C : Proof_Idx

inductive PairingsIdx : Type where
  | ab : PairingsIdx
  | αβ : PairingsIdx
  | stmtγ : PairingsIdx
  | cδ : PairingsIdx

Lean.Name.str in Init.Prelude

Nat in Init.Prelude

local notation "Vars_α" => some Vars.α
local notation "Vars_β" => some Vars.β
local notation "Vars_γ" => some Vars.γ
local notation "Vars_δ" => some Vars.δ
local notation "Vars_x" => none

inductive Vars : Type where
  | α : Vars
  | β : Vars
deriving Repr, BEq

inductive Vars : Type where
  | β : Vars
  | γ : Vars
deriving Repr, BEq

def ProofState.with : ProofState → Elab.Tactic.TacticM α → CoreM α :=
  fun { tacCtx, tacState, termCtx, termState, metaCtx, metaState } x => do
    let tacState ← IO.mkRef tacState
    let termState ← IO.mkRef termState
    let metaState ← IO.mkRef metaState
    x tacCtx tacState termCtx termState metaCtx metaState

noncomputable def Groth16TypeIII
     
    {F : Type} [Field F]
     
    {n_stmt n_wit n_var : ℕ}
     
    {u_stmt : Fin n_stmt → (Polynomial F) }
    {u_wit : Fin n_wit → (Polynomial F) }
    {v_stmt : Fin n_stmt → (Polynomial F) }
    {v_wit : Fin n_wit → (Polynomial F) }
    {w_stmt : Fin n_stmt → (Polynomial F) }
    {w_wit : Fin n_wit → (Polynomial F) }
     
    {t : Polynomial F} :
    AGMProofSystemInstantiation F :=
  {
    Stmt := Fin n_stmt -> F
    Sample := Option Vars
    SRSElements_G1 := @SRS_Elements_G1_Idx n_stmt n_wit n_var
    ListSRSElements_G1 :=
      [SRS_Elements_G1_Idx.α]
      ++ [SRS_Elements_G1_Idx.β]
      ++ [SRS_Elements_G1_Idx.δ]
      ++ ((List.finRange n_var).map fun i => SRS_Elements_G1_Idx.x_pow i)
      ++ ((List.finRange (n_var - 1)).map fun i => SRS_Elements_G1_Idx.x_pow_times_t i)
      ++ ((List.finRange n_stmt).map fun i => SRS_Elements_G1_Idx.y i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_G1_Idx.q i)
    SRSElements_G2 := @SRS_Elements_G2_Idx n_stmt n_wit n_var
    ListSRSElements_G2 :=
      [SRS_Elements_G2_Idx.β]
      ++ [SRS_Elements_G2_Idx.γ]
      ++ [SRS_Elements_G2_Idx.δ]
      ++ ((List.finRange n_var).map fun i => SRS_Elements_G2_Idx.x_pow i)
    SRSElementValue_G1 := fun SRS_idx => match SRS_idx with
      | SRS_Elements_G1_Idx.α => X Vars_γ * X Vars_δ * X Vars_α
      | SRS_Elements_G1_Idx.β => X Vars_γ * X Vars_δ * X Vars_β
      | SRS_Elements_G1_Idx.δ => X Vars_γ * X Vars_δ * X Vars_δ
      | SRS_Elements_G1_Idx.x_pow i => X Vars_γ * X Vars_δ * X Vars_x ^ (i : ℕ)
      | SRS_Elements_G1_Idx.x_pow_times_t i => X Vars_γ
                                                  * X Vars_x ^ (i : ℕ)
                                                  * to_MvPolynomial_Option Vars t
      | SRS_Elements_G1_Idx.y i => ((X Vars_β * X Vars_δ) * ( (to_MvPolynomial_Option Vars (u_stmt i))))
                                      +
                                      (X Vars_α * X Vars_δ) * (to_MvPolynomial_Option Vars (v_stmt i))
                                      +
                                      X Vars_δ * (to_MvPolynomial_Option Vars (w_stmt i))
      | SRS_Elements_G1_Idx.q i => (X Vars_β * X Vars_γ) * ( to_MvPolynomial_Option Vars (u_wit i))
                                      +
                                      (X Vars_α * X Vars_γ) * (to_MvPolynomial_Option Vars (v_wit i))
                                      +
                                      X Vars_γ * to_MvPolynomial_Option Vars (w_wit i)
      
    SRSElementValue_G2 := fun SRS_idx => match SRS_idx with
      | SRS_Elements_G2_Idx.β => X Vars_γ * X Vars_δ * X Vars_β
      | SRS_Elements_G2_Idx.γ => X Vars_γ * X Vars_δ * X Vars_γ
      | SRS_Elements_G2_Idx.δ => X Vars_γ * X Vars_δ * X Vars_δ
      | SRS_Elements_G2_Idx.x_pow i => X Vars_γ * X Vars_δ * X Vars_x ^ (i : ℕ)
    Proof_G1 := Proof_G1_Idx
    ListProof_G1 := [Proof_G1_Idx.A, Proof_G1_Idx.C]
    Proof_G2 := Proof_G2_Idx
    ListProof_G2 := [Proof_G2_Idx.B]
    EqualityChecks := Unit
    Pairings := fun _ => PairingsIdx
    ListPairings := fun _ => [PairingsIdx.ab, PairingsIdx.αβ, PairingsIdx.stmtγ, PairingsIdx.cδ]
    verificationPairingSRS_G1 := fun stmt _ i SRS_idx => match i with
      | PairingsIdx.ab => match SRS_idx with
        | SRS_Elements_G1_Idx.α => 0
        | SRS_Elements_G1_Idx.β => 0
        | SRS_Elements_G1_Idx.δ => 0
        | SRS_Elements_G1_Idx.x_pow _ => 0
        | SRS_Elements_G1_Idx.x_pow_times_t _ => 0
        | SRS_Elements_G1_Idx.y _ => 0
        | SRS_Elements_G1_Idx.q _ => 0
      | PairingsIdx.αβ => match SRS_idx with
        | SRS_Elements_G1_Idx.α => 1
        | SRS_Elements_G1_Idx.β => 0
        | SRS_Elements_G1_Idx.δ => 0
        | SRS_Elements_G1_Idx.x_pow _ => 0
        | SRS_Elements_G1_Idx.x_pow_times_t _ => 0
        | SRS_Elements_G1_Idx.y _ => 0
        | SRS_Elements_G1_Idx.q _ => 0
      | PairingsIdx.stmtγ => match SRS_idx with
        | SRS_Elements_G1_Idx.α => 0
        | SRS_Elements_G1_Idx.β => 0
        | SRS_Elements_G1_Idx.δ => 0
        | SRS_Elements_G1_Idx.x_pow _ => 0
        | SRS_Elements_G1_Idx.x_pow_times_t _ => 0
        | SRS_Elements_G1_Idx.y i => stmt i
        | SRS_Elements_G1_Idx.q _ => 0
      | PairingsIdx.cδ => match SRS_idx with
        | SRS_Elements_G1_Idx.α => 0
        | SRS_Elements_G1_Idx.β => 0
        | SRS_Elements_G1_Idx.δ => 0
        | SRS_Elements_G1_Idx.x_pow _ => 0
        | SRS_Elements_G1_Idx.x_pow_times_t _ => 0
        | SRS_Elements_G1_Idx.y _ => 0
        | SRS_Elements_G1_Idx.q i => 0
    verificationPairingSRS_G2 := fun stmt _ i SRS_idx => match i with
      | PairingsIdx.ab => match SRS_idx with
        | SRS_Elements_G2_Idx.β => 0
        | SRS_Elements_G2_Idx.γ => 0
        | SRS_Elements_G2_Idx.δ => 0
        | SRS_Elements_G2_Idx.x_pow _ => 0
      | PairingsIdx.αβ => match SRS_idx with
        | SRS_Elements_G2_Idx.β => 1
        | SRS_Elements_G2_Idx.γ => 0
        | SRS_Elements_G2_Idx.δ => 0
        | SRS_Elements_G2_Idx.x_pow _ => 0
      | PairingsIdx.stmtγ => match SRS_idx with
        | SRS_Elements_G2_Idx.β => 0
        | SRS_Elements_G2_Idx.γ => 1
        | SRS_Elements_G2_Idx.δ => 0
        | SRS_Elements_G2_Idx.x_pow _ => 0
      | PairingsIdx.cδ => match SRS_idx with
        | SRS_Elements_G2_Idx.β => 0
        | SRS_Elements_G2_Idx.γ => 0
        | SRS_Elements_G2_Idx.δ => 1
        | SRS_Elements_G2_Idx.x_pow _ => 0
    verificationPairingProof_G1 := fun stmt _ i pf => match i with
      | PairingsIdx.ab => match pf with
        | Proof_G1_Idx.A => 1
        | Proof_G1_Idx.C => 0
      | PairingsIdx.αβ => match pf with
        | Proof_G1_Idx.A => 0
        | Proof_G1_Idx.C => 0
      | PairingsIdx.stmtγ => match pf with
        | Proof_G1_Idx.A => 0
        | Proof_G1_Idx.C => 0
      | PairingsIdx.cδ => match pf with
        | Proof_G1_Idx.A => 0
        | Proof_G1_Idx.C => 1
    verificationPairingProof_G2 := fun stmt _ i pf => match i with
      | PairingsIdx.ab => match pf with
        | Proof_G2_Idx.B => -1
      | PairingsIdx.αβ => match pf with
        | Proof_G2_Idx.B => 0
      | PairingsIdx.stmtγ => match pf with
        | Proof_G2_Idx.B => 0
      | PairingsIdx.cδ => match pf with
        | Proof_G2_Idx.B => 0
  }

inferInstanceAs in Init.Prelude

Finsupp in Mathlib.Data.Finsupp.Defs

Finset.prod in Mathlib.Algebra.BigOperators.Group.Finset.Defs

noncomputable def Groth16TypeI
     
    {F : Type} [Field F]
     
    {n_stmt n_wit n_var : ℕ}
     
    {u_stmt : Fin n_stmt → (Polynomial F) }
    {u_wit : Fin n_wit → (Polynomial F) }
    {v_stmt : Fin n_stmt → (Polynomial F) }
    {v_wit : Fin n_wit → (Polynomial F) }
    {w_stmt : Fin n_stmt → (Polynomial F) }
    {w_wit : Fin n_wit → (Polynomial F) }
     
    {r : Fin n_wit → F} :
    AGMProofSystemInstantiation F :=
  let t : Polynomial F :=
    ∏ i in (Finset.univ : Finset (Fin n_wit)), (Polynomial.X - Polynomial.C (r i));
  {
    Stmt := Fin n_stmt -> F
    Sample := Option Vars
    SRSElements_G1 := @SRS_Elements_Idx n_stmt n_wit n_var
    ListSRSElements_G1 :=
      [SRS_Elements_Idx.α]
      ++ [SRS_Elements_Idx.β]
      ++ [SRS_Elements_Idx.δ]
      ++ ((List.finRange n_var).map fun i => SRS_Elements_Idx.x_pow i)
      ++ ((List.finRange (n_var - 1)).map fun i => SRS_Elements_Idx.x_pow_times_t i)
      ++ ((List.finRange n_stmt).map fun i => SRS_Elements_Idx.y i)
      ++ ((List.finRange n_wit).map fun i => SRS_Elements_Idx.q i)
    SRSElements_G2 := @SRS_Elements_Idx n_stmt n_wit n_var
    ListSRSElements_G2 :=
      [SRS_Elements_Idx.β]
      ++ [SRS_Elements_Idx.γ]
      ++ [SRS_Elements_Idx.δ]
      ++ ((List.finRange n_var).map fun i => SRS_Elements_Idx.x_pow i)
    SRSElementValue_G1 := fun SRS_idx => match SRS_idx with
      | SRS_Elements_Idx.α => X Vars_γ * X Vars_δ * X Vars_α
      | SRS_Elements_Idx.β => X Vars_γ * X Vars_δ * X Vars_β
      | SRS_Elements_Idx.γ => X Vars_γ * X Vars_δ * X Vars_γ
      | SRS_Elements_Idx.δ => X Vars_γ * X Vars_δ * X Vars_δ
      | SRS_Elements_Idx.x_pow i => X Vars_γ * X Vars_δ * X Vars_x ^ (i : ℕ)
      | SRS_Elements_Idx.x_pow_times_t i => X Vars_γ
                                                  * X Vars_x ^ (i : ℕ)
                                                  * to_MvPolynomial_Option Vars t
      | SRS_Elements_Idx.y i => ((X Vars_β * X Vars_δ) * ( (to_MvPolynomial_Option Vars (u_stmt i))))
                                      +
                                      (X Vars_α * X Vars_δ) * (to_MvPolynomial_Option Vars (v_stmt i))
                                      +
                                      X Vars_δ * (to_MvPolynomial_Option Vars (w_stmt i))
      | SRS_Elements_Idx.q i => (X Vars_β * X Vars_γ) * ( to_MvPolynomial_Option Vars (u_wit i))
                                      +
                                      (X Vars_α * X Vars_γ) * (to_MvPolynomial_Option Vars (v_wit i))
                                      +
                                      X Vars_γ * to_MvPolynomial_Option Vars (w_wit i)
      
    SRSElementValue_G2 := fun SRS_idx => match SRS_idx with
      | SRS_Elements_Idx.α => X Vars_γ * X Vars_δ * X Vars_α
      | SRS_Elements_Idx.β => X Vars_γ * X Vars_δ * X Vars_β
      | SRS_Elements_Idx.γ => X Vars_γ * X Vars_δ * X Vars_γ
      | SRS_Elements_Idx.δ => X Vars_γ * X Vars_δ * X Vars_δ
      | SRS_Elements_Idx.x_pow i => X Vars_γ * X Vars_δ * X Vars_x ^ (i : ℕ)
      | SRS_Elements_Idx.x_pow_times_t i => X Vars_γ
                                                  * X Vars_x ^ (i : ℕ)
                                                  * to_MvPolynomial_Option Vars t
      | SRS_Elements_Idx.y i => ((X Vars_β * X Vars_δ) * ( (to_MvPolynomial_Option Vars (u_stmt i))))
                                      +
                                      (X Vars_α * X Vars_δ) * (to_MvPolynomial_Option Vars (v_stmt i))
                                      +
                                      X Vars_δ * (to_MvPolynomial_Option Vars (w_stmt i))
      | SRS_Elements_Idx.q i => (X Vars_β * X Vars_γ) * ( to_MvPolynomial_Option Vars (u_wit i))
                                      +
                                      (X Vars_α * X Vars_γ) * (to_MvPolynomial_Option Vars (v_wit i))
                                      +
                                      X Vars_γ * to_MvPolynomial_Option Vars (w_wit i)
      
    Proof_G1 := Proof_Idx
    ListProof_G1 := [Proof_Idx.A, Proof_Idx.B, Proof_Idx.C]
    Proof_G2 := Proof_Idx
    ListProof_G2 := [Proof_Idx.A, Proof_Idx.B, Proof_Idx.C]
    EqualityChecks := Unit
    Pairings := fun _ => PairingsIdx
    ListPairings := fun _ => [PairingsIdx.ab, PairingsIdx.αβ, PairingsIdx.stmtγ, PairingsIdx.cδ]
    verificationPairingSRS_G1 := fun stmt _ i SRS_idx => match i with
      | PairingsIdx.ab => match SRS_idx with
        | SRS_Elements_Idx.α => 0
        | SRS_Elements_Idx.β => 0
        | SRS_Elements_Idx.γ => 0
        | SRS_Elements_Idx.δ => 0
        | SRS_Elements_Idx.x_pow _ => 0
        | SRS_Elements_Idx.x_pow_times_t _ => 0
        | SRS_Elements_Idx.y _ => 0
        | SRS_Elements_Idx.q _ => 0
      | PairingsIdx.αβ => match SRS_idx with
        | SRS_Elements_Idx.α => 1
        | SRS_Elements_Idx.β => 0
        | SRS_Elements_Idx.γ => 0
        | SRS_Elements_Idx.δ => 0
        | SRS_Elements_Idx.x_pow _ => 0
        | SRS_Elements_Idx.x_pow_times_t _ => 0
        | SRS_Elements_Idx.y _ => 0
        | SRS_Elements_Idx.q _ => 0
      | PairingsIdx.stmtγ => match SRS_idx with
        | SRS_Elements_Idx.α => 0
        | SRS_Elements_Idx.β => 0
        | SRS_Elements_Idx.γ => 0
        | SRS_Elements_Idx.δ => 0
        | SRS_Elements_Idx.x_pow _ => 0
        | SRS_Elements_Idx.x_pow_times_t _ => 0
        | SRS_Elements_Idx.y i => stmt i
        | SRS_Elements_Idx.q _ => 0
      | PairingsIdx.cδ => match SRS_idx with
        | SRS_Elements_Idx.α => 0
        | SRS_Elements_Idx.β => 0
        | SRS_Elements_Idx.γ => 0
        | SRS_Elements_Idx.δ => 0
        | SRS_Elements_Idx.x_pow _ => 0
        | SRS_Elements_Idx.x_pow_times_t _ => 0
        | SRS_Elements_Idx.y _ => 0
        | SRS_Elements_Idx.q i => 0
    verificationPairingSRS_G2 := fun stmt _ i SRS_idx => match i with
      | PairingsIdx.ab => match SRS_idx with
        | SRS_Elements_Idx.β => 0
        | SRS_Elements_Idx.γ => 0
        | SRS_Elements_Idx.δ => 0
        | SRS_Elements_Idx.x_pow _ => 0
        | _ => 0
      | PairingsIdx.αβ => match SRS_idx with
        | SRS_Elements_Idx.β => 1
        | SRS_Elements_Idx.γ => 0
        | SRS_Elements_Idx.δ => 0
        | SRS_Elements_Idx.x_pow _ => 0
        | _ => 0
      | PairingsIdx.stmtγ => match SRS_idx with
        | SRS_Elements_Idx.β => 0
        | SRS_Elements_Idx.γ => 1
        | SRS_Elements_Idx.δ => 0
        | SRS_Elements_Idx.x_pow _ => 0
        | _ => 0
      | PairingsIdx.cδ => match SRS_idx with
        | SRS_Elements_Idx.β => 0
        | SRS_Elements_Idx.γ => 0
        | SRS_Elements_Idx.δ => 1
        | SRS_Elements_Idx.x_pow _ => 0
        | _ => 0
    verificationPairingProof_G1 := fun stmt _ i pf => match i with
      | PairingsIdx.ab => match pf with
        | Proof_Idx.A => 1
        | Proof_Idx.B => 0
        | Proof_Idx.C => 0
      | PairingsIdx.αβ => match pf with
        | Proof_Idx.A => 0
        | Proof_Idx.B => 0
        | Proof_Idx.C => 0
      | PairingsIdx.stmtγ => match pf with
        | Proof_Idx.A => 0
        | Proof_Idx.B => 0
        | Proof_Idx.C => 0
      | PairingsIdx.cδ => match pf with
        | Proof_Idx.A => 0
        | Proof_Idx.B => 0
        | Proof_Idx.C => 1
    verificationPairingProof_G2 := fun stmt _ i pf => match i with
      | PairingsIdx.ab => match pf with
        | Proof_Idx.A => 0
        | Proof_Idx.B => -1
        | Proof_Idx.C => 0
      | PairingsIdx.αβ => match pf with
        | Proof_Idx.A => 0
        | Proof_Idx.B => 0
        | Proof_Idx.C => 0
      | PairingsIdx.stmtγ => match pf with
        | Proof_Idx.A => 0
        | Proof_Idx.B => 0
        | Proof_Idx.C => 0
      | PairingsIdx.cδ => match pf with
        | Proof_Idx.A => 0
        | Proof_Idx.B => 0
        | Proof_Idx.C => 0
    Identified_Proof_Elems := [(Proof_Idx.A, Proof_Idx.A), (Proof_Idx.B, Proof_Idx.B), (Proof_Idx.C, Proof_Idx.C)]
  }

def compile_Fin_list (l : List ℕ) : List (Fin (l.length)) := sorry

Proof_G1 := Proof_G1_Idx
    ListProof_G1 := [Proof_G1_Idx.V_mid, Proof_G1_Idx.V_mid', Proof_G1_Idx.W', Proof_G1_Idx.Y, Proof_G1_Idx.H']
    Proof_G2 := Proof_G2_Idx
    ListProof_G2 := [Proof_G2_Idx.W, Proof_G2_Idx.H]
    EqualityChecks := ChecksIdx
    Pairings := fun check_idx => match check_idx with
      | ChecksIdx.CheckI => PairingsI_Idx
      | ChecksIdx.CheckII => PairingsII_Idx
      | ChecksIdx.CheckIII => PairingsIII_Idx
      | ChecksIdx.CheckIV => PairingsIV_Idx
      | ChecksIdx.CheckV => PairingsV_Idx
    ListPairings := fun check_idx => match check_idx with
      | ChecksIdx.CheckI => [PairingsI_Idx.lhs, PairingsI_Idx.rhs]
      | ChecksIdx.CheckII => [PairingsII_Idx.lhs, PairingsII_Idx.rhs]
      | ChecksIdx.CheckIII => [PairingsIII_Idx.lhs, PairingsIII_Idx.rhs]
      | ChecksIdx.CheckIV => [PairingsIV_Idx.lhs, PairingsIV_Idx.rhs]
      | ChecksIdx.CheckV => [PairingsV_Idx.lhs, PairingsV_Idx.rhs1, PairingsV_Idx.rhs2]
    
    
    
    
    
    
    verificationPairingSRS_G1 := fun stmt check_idx i SRS_idx => match check_idx with
      | ChecksIdx.CheckI => match i with
        | PairingsI_Idx.lhs => match SRS_idx with
          | SRS_Elements_Idx.VK_v_0 => 1
          | SRS_Elements_Idx.VK_v_stmt k => stmt k
          | _ => 0
        | PairingsI_Idx.rhs => match SRS_idx with
          | SRS_Elements_Idx.VK_t => 1
          | _ => 0
      | ChecksIdx.CheckII => match i with
        | PairingsII_Idx.lhs => match SRS_idx with
          | _ => 0
        | PairingsII_Idx.rhs => match SRS_idx with
          | _ => 0
      | ChecksIdx.CheckIII => match i with
        | PairingsIII_Idx.lhs => match SRS_idx with
          | _ => 0
        | PairingsIII_Idx.rhs => match SRS_idx with
          | SRS_Elements_Idx.VK_α => 1
          | _ => 0
      | ChecksIdx.CheckIV => match i with
        | PairingsIV_Idx.lhs => match SRS_idx with
          | _ => 0
        | PairingsIV_Idx.rhs => match SRS_idx with
          | SRS_Elements_Idx.VK_α => 1
          | _ => 0
      | ChecksIdx.CheckV => match i with
        | PairingsV_Idx.lhs => match SRS_idx with
          | _ => 0
        | PairingsV_Idx.rhs1 => match SRS_idx with
          | _ => 0
        | PairingsV_Idx.rhs2 => match SRS_idx with
          | SRS_Elements_Idx.VK_βw_γ => 1
          | _ => 0
    
    
    
    
    
    verificationPairingSRS_G2 := fun stmt check_idx i SRS_idx => match check_idx with
      | ChecksIdx.CheckI => match i with
        | PairingsI_Idx.lhs => match SRS_idx with
          | SRS_Elements_Idx.VK_w_0 => 1
          | _ => 0
        | PairingsI_Idx.rhs => 0
      | ChecksIdx.CheckII => match i with
        | PairingsII_Idx.lhs => match SRS_idx with
          | SRS_Elements_Idx.VK_1 => 1
          | _ => 0
        | PairingsII_Idx.rhs => match SRS_idx with
          | SRS_Elements_Idx.VK_α => -1 
          | _ => 0
      | ChecksIdx.CheckIII => match i with
        | PairingsIII_Idx.lhs => match SRS_idx with
          | SRS_Elements_Idx.VK_1 => 1
          | _ => 0
        | PairingsIII_Idx.rhs => match SRS_idx with
          | _ => 0
      | ChecksIdx.CheckIV => match i with
        | PairingsIV_Idx.lhs => match SRS_idx with
          | SRS_Elements_Idx.VK_1 => 1
          | _ => 0
        | PairingsIV_Idx.rhs => match SRS_idx with
          | _ => 0
      | ChecksIdx.CheckV => match i with
        | PairingsV_Idx.lhs => match SRS_idx with
          | SRS_Elements_Idx.VK_γ => 1
          | _ => 0
        | PairingsV_Idx.rhs1 => match SRS_idx with
          | SRS_Elements_Idx.VK_βv_γ => -1 
          | _ => 0
        | PairingsV_Idx.rhs2 => match SRS_idx with
          | _ => 0
    
    
    
    
    
    verificationPairingProof_G1 := fun stmt check_idx i pf_idx => match check_idx with
      | ChecksIdx.CheckI => match i with
        | PairingsI_Idx.lhs => match pf_idx with
          | Proof_G1_Idx.V_mid => 1
          | _ => 0
        | PairingsI_Idx.rhs => match pf_idx with
          | _ => 0
      | ChecksIdx.CheckII => match i with
        | PairingsII_Idx.lhs => match pf_idx with
          | Proof_G1_Idx.V_mid' => 1
          | _ => 0
        | PairingsII_Idx.rhs => match pf_idx with
          | Proof_G1_Idx.V_mid => 1
          | _ => 0
      | ChecksIdx.CheckIII => match i with
        | PairingsIII_Idx.lhs => match pf_idx with
          | Proof_G1_Idx.W' => 1
          | _ => 0
        | PairingsIII_Idx.rhs => match pf_idx with
          | _ => 0
      | ChecksIdx.CheckIV => match i with
        | PairingsIV_Idx.lhs => match pf_idx with
          | Proof_G1_Idx.H' => 1
          | _ => 0
        | PairingsIV_Idx.rhs => match pf_idx with
          | _ => 0
      | ChecksIdx.CheckV => match i with
        | PairingsV_Idx.lhs => match pf_idx with
          | Proof_G1_Idx.Y => 1
          | _ => 0
        | PairingsV_Idx.rhs1 => match pf_idx with
          | Proof_G1_Idx.V_mid => 1
          | _ => 0
        | PairingsV_Idx.rhs2 => match pf_idx with
          | _ => 0
    
    
    
    
    
    verificationPairingProof_G2 := fun stmt check_idx i pf_idx => match check_idx with
      | ChecksIdx.CheckI => match i with
        | PairingsI_Idx.lhs => match pf_idx with
          | Proof_G2_Idx.W => 1
          | _ => 0
        | PairingsI_Idx.rhs => match pf_idx with
          | Proof_G2_Idx.H => -1 
          | _ => 0
      | ChecksIdx.CheckII => 0
      | ChecksIdx.CheckIII => match i with
        | PairingsIII_Idx.lhs => match pf_idx with
          | _ => 0
        | PairingsIII_Idx.rhs => match pf_idx with
          | Proof_G2_Idx.W => -1 
          | _ => 0
      | ChecksIdx.CheckIV => match i with
        | PairingsIV_Idx.lhs => match pf_idx with
          | _ => 0
        | PairingsIV_Idx.rhs => match pf_idx with
          | Proof_G2_Idx.H => -1 
          | _ => 0
      | ChecksIdx.CheckV => match i with
        | PairingsV_Idx.lhs => match pf_idx with
          | _ => 0
        | PairingsV_Idx.rhs1 => match pf_idx with
          | _ => 0
        | PairingsV_Idx.rhs2 => match pf_idx with
          | Proof_G2_Idx.W => -1 
          | _ => 0
    Identified_Proof_Elems := []
  }

Lean.MVarId in Lean.Expr

MvPolynomial.optionEquivRight in Mathlib.Algebra.MvPolynomial.Equiv

Proof : Type
  ListProof : List Proof

inductive WitEntries : Type where
  | A : WitEntries
  | B : WitEntries
deriving Repr, BEq

Pairings : EqualityChecks → Type

noncomputable def w_sum {F : Type} [Field F] {n_stmt n_wit : ℕ}
    (w_stmt : Fin n_stmt → (Polynomial F))
    (w_wit : Fin n_wit → (Polynomial F))
    (stmt : Fin n_stmt -> F)
    (wit : Fin n_wit -> F)
    : Polynomial F :=
  List.sum (List.map (fun j => Polynomial.C (stmt j) * (w_stmt j)) (List.finRange n_stmt))
  + List.sum (List.map (fun j => Polynomial.C (wit j) * (w_wit j)) (List.finRange n_wit))

Pairings : EqualityChecks → Type

nSRSComponents_G1 : ℕ
   
  SRSElements_G1_Lengths : Fin nSRSComponents_G1 -> ℕ -> ℕ -> Aux -> ℕ
   
  nSRSComponents_G2 : ℕ
  SRSElements_G2_Lengths : Fin nSRSComponents_G2 -> ℕ -> ℕ -> Aux -> ℕ

def verify {F : Type} [Field F]
    (𝓟 : AGMProofSystemInstantiation F) (prover : 𝓟.Prover) (stmt : 𝓟.Stmt) : Prop :=
  (
    ∀ check_idx : 𝓟.EqualityChecks, 𝓟.check_poly prover stmt check_idx = 0
  )
  ∧
  ∀ pfs ∈ 𝓟.Identified_Proof_Elems,
    𝓟.proof_element_G1_as_poly prover pfs.fst = 𝓟.proof_element_G2_as_poly prover pfs.snd

def matchPatterns_Or (pats : Array AbstractMVarsResult) (e : Expr) : MetaM Bool := do
  let e ← instantiateMVars e
  pats.anyM fun p ↦ return (← Conv.matchPattern? p e) matches some (_, #[])

inductive Proof_G2_Idx : Type where
  | W : Proof_G2_Idx
  | H : Proof_G2_Idx

liftM in Init.Prelude

inductive Proof_G2_Idx : Type where
  | B : Proof_G2_Idx

inductive PairingsIdx : Type where
  | lhs : PairingsIdx
  | rhs : PairingsIdx

Proof_G1 : Type
  ListProof_G1 : List Proof_G1
  Proof_G2 : Type
  ListProof_G2 : List Proof_G2

List.sum in Init.Data.List.Basic

DFunLike in Mathlib.Data.FunLike.Basic

AlgHom in Mathlib.Algebra.Algebra.Hom

Proof_G1 : Type
  Proof_G2 : Type

instance : Fintype Proof_G2_Idx :=
  ⟨⟨[Proof_G2_Idx.B], by admit /- proof elided -/
  ⟩, fun x => by admit /- proof elided -/
  ⟩

inductive SRS_Elements_G2_Idx : Type where
  | α : SRS_Elements_G2_Idx
  | β : SRS_Elements_G2_Idx

Lean.Elab.Tactic.TacticM in Lean.Elab.Tactic.Basic

inductive Proof_G1_Idx : Type where
  | A : Proof_G1_Idx
  | C : Proof_G1_Idx

Lean.Expr in Lean.Expr
</all_available_defs>

<all_available_lemmas>
lemma to_MvPolynomial_Option_X {F V : Type} [Field F] :
    to_MvPolynomial_Option V (Polynomial.X) = MvPolynomial.X (R := F) none

lemma to_MvPolynomial_Option_C {F V : Type} [Field F] (r : F) :
    to_MvPolynomial_Option V (Polynomial.C r) = MvPolynomial.C r

theorem Polynomial.hom_congr_vars {R : Type u} {S : Type v}
    [CommSemiring R] [CommSemiring S]
    {f₁ : Polynomial R →+* S} {f₂ : Polynomial R →+* S}
    (hC : RingHom.comp f₁ Polynomial.C = RingHom.comp f₂ Polynomial.C)
    (hv : f₁ (Polynomial.X) = f₂ (Polynomial.X)) :
    f₁ = f₂

lemma optionEquivRight_comp_to_MvPolynomial_Option {F V : Type} [Field F] :
    RingHom.comp (MvPolynomial.optionEquivRight F V).toRingEquiv.toRingHom (to_MvPolynomial_Option (F := F) V) = C

lemma optionEquivRight_to_MvPolynomial_Option {F V : Type} [Field F] (p : Polynomial F) :
    (MvPolynomial.optionEquivRight F V) (to_MvPolynomial_Option V p) = C p

lemma MvPolynomial.sum_map_C {σ A R : Type} [CommSemiring R] (l : List A) (f : A → R) :
    (l.map (fun (x : A) => C (σ := σ) (f x))).sum = C ((l.map f).sum)

theorem AlgEquiv.list_map_sum {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂}
    [CommSemiring R] [Semiring A₁] [Semiring A₂] [Algebra R A₁] [Algebra R A₂]
    (e : A₁ ≃ₐ[R] A₂) {ι : Type u_1} (f : ι → A₁) (l : List ι) :
    e (l.map (fun (x : ι) => f x)).sum = (l.map fun (x : ι) => e (f x)).sum

lemma Int.near_mods (a b c d : ℤ) (ha' : 0 ≤ a) (hb' : 0 ≤ b)
    (ha : a < d) (hb : b < d) (habcd : a = b + c * d) :
    c = 0

@[simp]
lemma MvPolynomial.coeff_zero_of_not_mem_support {σ F : Type} [Field F]
    (p : MvPolynomial σ F)
    (m : σ →₀ ℕ)
    (h : m ∉ p.support) :
    coeff m p = 0

lemma identified_proof_elems_def
    {F : Type} [Field F]
    {n_stmt n_wit n_var : ℕ}
    {u_stmt : Fin n_stmt → (Polynomial F) }
    {u_wit : Fin n_wit → (Polynomial F) }
    {t : Polynomial F} :
    (BabySNARK
        (F := F) (n_stmt := n_stmt) (n_wit := n_wit) (n_var := n_var)
        (u_stmt := u_stmt) (u_wit := u_wit) (t := t)).Identified_Proof_Elems = [(Proof_Idx.H, Proof_Idx.H), (Proof_Idx.V, Proof_Idx.V), (Proof_Idx.B, Proof_Idx.B)]

lemma soundness
    {F : Type} [Field F]
    {n_stmt n_wit d : ℕ}
    {v_stmt : Fin n_stmt → Polynomial F }
    {w_stmt : Fin n_stmt → Polynomial F }
    {y_stmt : Fin n_stmt → Polynomial F }
    {v_wit : Fin n_wit → Polynomial F }
    {w_wit : Fin n_wit → Polynomial F }
    {y_wit : Fin n_wit → Polynomial F }
    {v_0 : Polynomial F }
    {w_0 : Polynomial F }
    {y_0 : Polynomial F }
    /- t is the polynomial divisibility by which is used to verify satisfaction of the QAP -/
    {t : Polynomial F}
    (tMonic : t.Monic)
    -- t can also be expressed as follows, but this structure is not important for soundness
    -- {r : Fin (n_wit) → F}
    -- let t : Polynomial F

theorem MvPolynomial.degreeOf_C_mul {σ R : Type} [Field R] (j : σ)
    (c : R) (hc : c ≠ 0) (f : MvPolynomial σ R) :
    MvPolynomial.degreeOf j (MvPolynomial.C c * f) = MvPolynomial.degreeOf j f

lemma soundness
    {F : Type} [Field F]
    {n_stmt n_wit n_var : ℕ}
    {u_stmt : Fin n_stmt → (Polynomial F) }
    {u_wit : Fin n_wit → (Polynomial F) }
    {v_stmt : Fin n_stmt → (Polynomial F) }
    {v_wit : Fin n_wit → (Polynomial F) }
    {w_stmt : Fin n_stmt → (Polynomial F) }
    {w_wit : Fin n_wit → (Polynomial F) }
    {r : Fin n_wit → F} :
    (AGMProofSystemInstantiation.soundness
      F
      (Lipmaa
        (F := F) (n_stmt := n_stmt) (n_wit := n_wit) (n_var := n_var)
        (u_stmt := u_stmt) (u_wit := u_wit) (v_stmt := v_stmt)
        (v_wit := v_wit) (w_stmt := w_stmt) (w_wit := w_wit) (r := r))
      (Fin n_wit -> F)
      (fun (stmt : Fin n_stmt → F) (wit : Fin n_wit -> F) =>
        let t : Polynomial F :=
          ∏ i in (Finset.univ : Finset (Fin n_wit)), (Polynomial.X - Polynomial.C (r i));
        (((List.sum (List.map (fun i => Polynomial.C (stmt i) * u_stmt i) (List.finRange n_stmt)))
            + (List.sum (List.map (fun i => Polynomial.C (wit i) * u_wit i) (List.finRange n_wit))))
            *
          ((List.sum (List.map (fun i => Polynomial.C (stmt i) * v_stmt i) (List.finRange n_stmt)))
            + (List.sum (List.map (fun i => Polynomial.C (wit i) * v_wit i) (List.finRange n_wit))))
            -
          ((List.sum (List.map (fun i => Polynomial.C (stmt i) * w_stmt i) (List.finRange n_stmt)))
            + (List.sum (List.map (fun i => Polynomial.C (wit i) * w_wit i) (List.finRange n_wit)))))
            %ₘ t = 0
      )
      (fun prover i => prover.fst Proof_G1_Idx.C (SRS_Elements_G1_Idx.q i))
    )

lemma is_sound
    {F : Type} [Field F]
    {n_stmt n_wit n_var : ℕ}
    {u_stmt : Fin n_stmt → (Polynomial F) }
    {u_wit : Fin n_wit → (Polynomial F) }
    {v_stmt : Fin n_stmt → (Polynomial F) }
    {v_wit : Fin n_wit → (Polynomial F) }
    {w_stmt : Fin n_stmt → (Polynomial F) }
    {w_wit : Fin n_wit → (Polynomial F) }
    {r : Fin n_wit → F} :
    (soundness
      F
      (Groth16TypeI
        (F := F) (n_stmt := n_stmt) (n_wit := n_wit) (n_var := n_var)
        (u_stmt := u_stmt) (u_wit := u_wit) (v_stmt := v_stmt)
        (v_wit := v_wit) (w_stmt := w_stmt) (w_wit := w_wit) (r := r))
      (Fin n_wit -> F)
      (fun (stmt : Fin n_stmt → F) (wit : Fin n_wit -> F) =>
        let t : Polynomial F :=
          ∏ i in (Finset.univ : Finset (Fin n_wit)), (Polynomial.X - Polynomial.C (r i));
        (((List.sum (List.map (fun i => Polynomial.C (stmt i) * u_stmt i) (List.finRange n_stmt)))
            + (List.sum (List.map (fun i => Polynomial.C (wit i) * u_wit i) (List.finRange n_wit))))
            *
          ((List.sum (List.map (fun i => Polynomial.C (stmt i) * v_stmt i) (List.finRange n_stmt)))
            + (List.sum (List.map (fun i => Polynomial.C (wit i) * v_wit i) (List.finRange n_wit))))
            -
          ((List.sum (List.map (fun i => Polynomial.C (stmt i) * w_stmt i) (List.finRange n_stmt)))
            + (List.sum (List.map (fun i => Polynomial.C (wit i) * w_wit i) (List.finRange n_wit)))))
            %ₘ t = 0
      )
      (fun prover i => prover.fst Proof_Idx.C (SRS_Elements_Idx.q i))
    )

lemma MvPolynomial.bind₁_ite_pow_eq_zero_of {σ F : Type} [Field F] [DecidableEq σ]
    (p : MvPolynomial σ F)
    (d : ℕ)  (hd : 0 < d)
    (sample_removed sample_target : σ)
    (hsa : sample_target ≠ sample_removed)
    (h : MvPolynomial.bind₁
          ((fun x => (if x = sample_removed then MvPolynomial.X sample_target ^ d else MvPolynomial.X x)))
          p = 0)
    (hdegree : p.degreeOf sample_target < d) :
    p = 0

lemma Polynomial.mul_self_modByMonic {F : Type} [Field F] (t p : Polynomial F) (mt : t.Monic) : (t * p) %ₘ t = 0

)
</all_available_lemmas>

<local_ctx>
import FormalSnarksProject.Models.AGMProofSystemInstantiation

import Mathlib.Algebra.Polynomial.Div

import FormalSnarksProject.ToMathlib.OptionEquivRight

import Mathlib.Algebra.MvPolynomial.Equiv

import FormalSnarksProject.SoundnessTactic.SoundnessProver

open scoped BigOperators Classical

section ToySnark

open MvPolynomial Option List

namespace ToySnark

inductive Vars : Type where
  | α : Vars
  | β : Vars
deriving Repr, BEq

inductive StmtEntries : Type where
  | x : StmtEntries
  | y : StmtEntries
  | z : StmtEntries
deriving Repr, BEq

inductive WitEntries : Type where
  | A : WitEntries
  | B : WitEntries
deriving Repr, BEq

local notation "Vars_α" => some Vars.α
local notation "Vars_β" => some Vars.β
local notation "Vars_x" => none

inductive Proof_G1_Idx : Type where
  | Pf : Proof_G1_Idx

def Proof_G2_Idx : Type := Empty

inductive PairingsIdx : Type where
  | lhs : PairingsIdx
  | rhs : PairingsIdx

inductive SRS_Elements_G2_Idx : Type where
  | α : SRS_Elements_G2_Idx
  | β : SRS_Elements_G2_Idx

noncomputable def ToySnark
     
    {F : Type} [Field F] :
    AGMProofSystemInstantiation F :=
  {
    Stmt := StmtEntries -> F
    Sample := Option Vars
    SRSElements_G1 := SRS_Elements_G1_Idx
    ListSRSElements_G1 :=
      [.α, .β]
    SRSElements_G2 := SRS_Elements_G2_Idx
    ListSRSElements_G2 :=
      [.α, .β]
    SRSElementValue_G1 := fun SRS_idx => match SRS_idx with
      | SRS_Elements_G1_Idx.α => MvPolynomial.X Vars_α
      | SRS_Elements_G1_Idx.β => MvPolynomial.X Vars_β
    SRSElementValue_G2 := fun SRS_idx => match SRS_idx with
      | SRS_Elements_G2_Idx.α => MvPolynomial.X Vars_α
      | SRS_Elements_G2_Idx.β => MvPolynomial.X Vars_β
    Proof_G1 := Proof_G1_Idx
    ListProof_G1 := [Proof_G1_Idx.Pf]
    Proof_G2 := Proof_G2_Idx
    ListProof_G2 := []
    EqualityChecks := Unit
    Pairings := fun _ => PairingsIdx
    ListPairings := fun _ => [PairingsIdx.lhs, PairingsIdx.rhs]
    verificationPairingSRS_G1 := fun stmt _ i SRS_idx => match i with
      | PairingsIdx.lhs => 0
      | PairingsIdx.rhs => match SRS_idx with
        | SRS_Elements_G1_Idx.α => stmt StmtEntries.z
        | SRS_Elements_G1_Idx.β => 0
    verificationPairingSRS_G2 := fun stmt _ i SRS_idx => match i with
      | PairingsIdx.lhs => match SRS_idx with
        | SRS_Elements_G2_Idx.α => stmt StmtEntries.x
        | SRS_Elements_G2_Idx.β => stmt StmtEntries.y
      | PairingsIdx.rhs => match SRS_idx with
        | SRS_Elements_G2_Idx.α => 0
        | SRS_Elements_G2_Idx.β => -1
    verificationPairingProof_G1 := fun stmt _ i pf => match i with
      | PairingsIdx.lhs => match pf with
        | Proof_G1_Idx.Pf => 1
      | PairingsIdx.rhs => match pf with
        | Proof_G1_Idx.Pf => 0
    verificationPairingProof_G2 := fun stmt _ i pf => 0
  }

section soundness
</local_ctx>

<target_theorem>
lemma soundness
    {F : Type} [Field F] :
    (AGMProofSystemInstantiation.soundness
      F
      (ToySnark
        (F := F))
      (WitEntries -> F)
      (fun (stmt : StmtEntries → F) (wit : WitEntries -> F) =>
        wit WitEntries.A * stmt StmtEntries.y = stmt StmtEntries.z -- - wit WitEntries.I
        ∨
        wit WitEntries.B * stmt StmtEntries.x = stmt StmtEntries.z -- - wit WitEntries.I
      )
      (fun prover i => prover.fst Proof_G1_Idx.Pf (if i = WitEntries.A then .α else .β))

    ) :=
</target_theorem>

