Theorem: ToySnark.soundness (FormalSnarksProject/SNARKs/ToySnark.lean)

State before:
F : Type
inst✝ : Field F
⊢ AGMProofSystemInstantiation.soundness F ToySnark (WitEntries → F)
    (fun stmt wit =>
      wit WitEntries.A * stmt StmtEntries.y = stmt StmtEntries.z ∨
        wit WitEntries.B * stmt StmtEntries.x = stmt StmtEntries.z)
    fun prover i => prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β)
Tactic:
unfold AGMProofSystemInstantiation.soundness AGMProofSystemInstantiation.verify AGMProofSystemInstantiation.proof_element_G1_as_poly AGMProofSystemInstantiation.proof_element_G2_as_poly
State after:
F : Type
inst✝ : Field F
⊢ ∀ (stmt : ToySnark.Stmt) (prover : AGMProofSystemInstantiation.Prover F ToySnark),
    ((∀ (check_idx : ToySnark.EqualityChecks), ToySnark.check_poly prover stmt check_idx = 0) ∧
        ∀ pfs ∈ ToySnark.Identified_Proof_Elems,
          (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * ToySnark.SRSElementValue_G1 SRS_elem)
                ToySnark.ListSRSElements_G1).sum =
            (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * ToySnark.SRSElementValue_G2 SRS_elem)
                ToySnark.ListSRSElements_G2).sum) →
      (fun stmt wit =>
          wit WitEntries.A * stmt StmtEntries.y = stmt StmtEntries.z ∨
            wit WitEntries.B * stmt StmtEntries.x = stmt StmtEntries.z)
        stmt
        ((fun prover i =>
            prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover)

State before:
F : Type
inst✝ : Field F
⊢ ∀ (stmt : ToySnark.Stmt) (prover : AGMProofSystemInstantiation.Prover F ToySnark),
    ((∀ (check_idx : ToySnark.EqualityChecks), ToySnark.check_poly prover stmt check_idx = 0) ∧
        ∀ pfs ∈ ToySnark.Identified_Proof_Elems,
          (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * ToySnark.SRSElementValue_G1 SRS_elem)
                ToySnark.ListSRSElements_G1).sum =
            (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * ToySnark.SRSElementValue_G2 SRS_elem)
                ToySnark.ListSRSElements_G2).sum) →
      (fun stmt wit =>
          wit WitEntries.A * stmt StmtEntries.y = stmt StmtEntries.z ∨
            wit WitEntries.B * stmt StmtEntries.x = stmt StmtEntries.z)
        stmt
        ((fun prover i =>
            prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover)
Tactic:
intros stmt prover eqns'
State after:
F : Type
inst✝ : Field F
stmt : ToySnark.Stmt
prover : AGMProofSystemInstantiation.Prover F ToySnark
eqns' :
  (∀ (check_idx : ToySnark.EqualityChecks), ToySnark.check_poly prover stmt check_idx = 0) ∧
    ∀ pfs ∈ ToySnark.Identified_Proof_Elems,
      (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * ToySnark.SRSElementValue_G1 SRS_elem)
            ToySnark.ListSRSElements_G1).sum =
        (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * ToySnark.SRSElementValue_G2 SRS_elem)
            ToySnark.ListSRSElements_G2).sum
⊢ (fun prover i => prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.A *
        stmt StmtEntries.y =
      stmt StmtEntries.z ∨
    (fun prover i =>
            prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.B *
        stmt StmtEntries.x =
      stmt StmtEntries.z

State before:
F : Type
inst✝ : Field F
stmt : ToySnark.Stmt
prover : AGMProofSystemInstantiation.Prover F ToySnark
eqns' :
  (∀ (check_idx : ToySnark.EqualityChecks), ToySnark.check_poly prover stmt check_idx = 0) ∧
    ∀ pfs ∈ ToySnark.Identified_Proof_Elems,
      (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * ToySnark.SRSElementValue_G1 SRS_elem)
            ToySnark.ListSRSElements_G1).sum =
        (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * ToySnark.SRSElementValue_G2 SRS_elem)
            ToySnark.ListSRSElements_G2).sum
⊢ (fun prover i => prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.A *
        stmt StmtEntries.y =
      stmt StmtEntries.z ∨
    (fun prover i =>
            prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.B *
        stmt StmtEntries.x =
      stmt StmtEntries.z
Tactic:
rcases eqns' with ⟨eqns, null⟩
State after:
case intro
F : Type
inst✝ : Field F
stmt : ToySnark.Stmt
prover : AGMProofSystemInstantiation.Prover F ToySnark
eqns : ∀ (check_idx : ToySnark.EqualityChecks), ToySnark.check_poly prover stmt check_idx = 0
null :
  ∀ pfs ∈ ToySnark.Identified_Proof_Elems,
    (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * ToySnark.SRSElementValue_G1 SRS_elem)
          ToySnark.ListSRSElements_G1).sum =
      (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * ToySnark.SRSElementValue_G2 SRS_elem)
          ToySnark.ListSRSElements_G2).sum
⊢ (fun prover i => prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.A *
        stmt StmtEntries.y =
      stmt StmtEntries.z ∨
    (fun prover i =>
            prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.B *
        stmt StmtEntries.x =
      stmt StmtEntries.z

State before:
case intro
F : Type
inst✝ : Field F
stmt : ToySnark.Stmt
prover : AGMProofSystemInstantiation.Prover F ToySnark
eqns : ∀ (check_idx : ToySnark.EqualityChecks), ToySnark.check_poly prover stmt check_idx = 0
null :
  ∀ pfs ∈ ToySnark.Identified_Proof_Elems,
    (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * ToySnark.SRSElementValue_G1 SRS_elem)
          ToySnark.ListSRSElements_G1).sum =
      (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * ToySnark.SRSElementValue_G2 SRS_elem)
          ToySnark.ListSRSElements_G2).sum
⊢ (fun prover i => prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.A *
        stmt StmtEntries.y =
      stmt StmtEntries.z ∨
    (fun prover i =>
            prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.B *
        stmt StmtEntries.x =
      stmt StmtEntries.z
Tactic:
have eqn := eqns ()
State after:
case intro
F : Type
inst✝ : Field F
stmt : ToySnark.Stmt
prover : AGMProofSystemInstantiation.Prover F ToySnark
eqns : ∀ (check_idx : ToySnark.EqualityChecks), ToySnark.check_poly prover stmt check_idx = 0
null :
  ∀ pfs ∈ ToySnark.Identified_Proof_Elems,
    (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * ToySnark.SRSElementValue_G1 SRS_elem)
          ToySnark.ListSRSElements_G1).sum =
      (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * ToySnark.SRSElementValue_G2 SRS_elem)
          ToySnark.ListSRSElements_G2).sum
eqn : ToySnark.check_poly prover stmt () = 0
⊢ (fun prover i => prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.A *
        stmt StmtEntries.y =
      stmt StmtEntries.z ∨
    (fun prover i =>
            prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.B *
        stmt StmtEntries.x =
      stmt StmtEntries.z

State before:
case intro
F : Type
inst✝ : Field F
stmt : ToySnark.Stmt
prover : AGMProofSystemInstantiation.Prover F ToySnark
eqns : ∀ (check_idx : ToySnark.EqualityChecks), ToySnark.check_poly prover stmt check_idx = 0
null :
  ∀ pfs ∈ ToySnark.Identified_Proof_Elems,
    (List.map (fun SRS_elem => C (prover.1 pfs.1 SRS_elem) * ToySnark.SRSElementValue_G1 SRS_elem)
          ToySnark.ListSRSElements_G1).sum =
      (List.map (fun SRS_elem => C (prover.2 pfs.2 SRS_elem) * ToySnark.SRSElementValue_G2 SRS_elem)
          ToySnark.ListSRSElements_G2).sum
eqn : ToySnark.check_poly prover stmt () = 0
⊢ (fun prover i => prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.A *
        stmt StmtEntries.y =
      stmt StmtEntries.z ∨
    (fun prover i =>
            prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.B *
        stmt StmtEntries.x =
      stmt StmtEntries.z
Tactic:
clear eqns null
State after:
case intro
F : Type
inst✝ : Field F
stmt : ToySnark.Stmt
prover : AGMProofSystemInstantiation.Prover F ToySnark
eqn : ToySnark.check_poly prover stmt () = 0
⊢ (fun prover i => prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.A *
        stmt StmtEntries.y =
      stmt StmtEntries.z ∨
    (fun prover i =>
            prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.B *
        stmt StmtEntries.x =
      stmt StmtEntries.z

State before:
case intro
F : Type
inst✝ : Field F
stmt : ToySnark.Stmt
prover : AGMProofSystemInstantiation.Prover F ToySnark
eqn : ToySnark.check_poly prover stmt () = 0
⊢ (fun prover i => prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.A *
        stmt StmtEntries.y =
      stmt StmtEntries.z ∨
    (fun prover i =>
            prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.B *
        stmt StmtEntries.x =
      stmt StmtEntries.z
Tactic:
simp_rw [ToySnark] at eqn
State after:
case intro
F : Type
inst✝ : Field F
stmt : ToySnark.Stmt
prover : AGMProofSystemInstantiation.Prover F ToySnark
eqn :
  { Stmt := StmtEntries → F, Sample := Option Vars, SRSElements_G1 := SRS_Elements_G1_Idx,
          ListSRSElements_G1 := [SRS_Elements_G1_Idx.α, SRS_Elements_G1_Idx.β], SRSElements_G2 := SRS_Elements_G2_Idx,
          ListSRSElements_G2 := [SRS_Elements_G2_Idx.α, SRS_Elements_G2_Idx.β],
          SRSElementValue_G1 := fun SRS_idx =>
            match SRS_idx with
            | SRS_Elements_G1_Idx.α => X Vars_α
            | SRS_Elements_G1_Idx.β => X Vars_β,
          SRSElementValue_G2 := fun SRS_idx =>
            match SRS_idx with
            | SRS_Elements_G2_Idx.α => X Vars_α
            | SRS_Elements_G2_Idx.β => X Vars_β,
          Proof_G1 := Proof_G1_Idx, ListProof_G1 := [Proof_G1_Idx.Pf], Proof_G2 := Proof_G2_Idx, ListProof_G2 := [],
          EqualityChecks := Unit, Pairings := fun x => PairingsIdx,
          ListPairings := fun x => [PairingsIdx.lhs, PairingsIdx.rhs],
          verificationPairingSRS_G1 := fun stmt x 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 x 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 x i pf =>
            match i with
            | PairingsIdx.lhs => 1
            | PairingsIdx.rhs => 0,
          verificationPairingProof_G2 := fun stmt x i pf => 0, Identified_Proof_Elems := [] }.check_poly
      prover stmt () =
    0
⊢ (fun prover i => prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.A *
        stmt StmtEntries.y =
      stmt StmtEntries.z ∨
    (fun prover i =>
            prover.1 Proof_G1_Idx.Pf (if i = WitEntries.A then SRS_Elements_G1_Idx.α else SRS_Elements_G1_Idx.β))
          prover WitEntries.B *
        stmt StmtEntries.x =
      stmt StmtEntries.z