1  """
  2  End-to-end example: Groth16 proof for r = x * y * z * u
  3  
  4  This example demonstrates the complete workflow:
  5  1. Create R1CS for the computation
  6  2. Convert R1CS to QAP
  7  3. Generate trusted setup
  8  4. Create a proof
  9  5. Verify the proof
 10  """
 11  
 12  # Add the parent directory to the load path
 13  push!(LOAD_PATH, dirname(@__DIR__))
 14  
 15  using GrothAlgebra
 16  using GrothCurves
 17  using GrothProofs
 18  
 19  function main()
 20      println("=" ^ 60)
 21      println("Groth16 Proof System Example: r = x * y * z * u")
 22      println("=" ^ 60)
 23      
 24      # Step 1: Create the R1CS
 25      println("\n1. Creating R1CS for r = x * y * z * u")
 26      println("   Variables: [1, r, x, y, z, u, v1, v2]")
 27      println("   Constraints:")
 28      println("   - v1 = x * y")
 29      println("   - v2 = z * u")
 30      println("   - r = v1 * v2")
 31      
 32      r1cs = create_r1cs_example_multiplication()
 33      println("   ✓ R1CS created with $(r1cs.num_constraints) constraints and $(r1cs.num_vars) variables")
 34      
 35      # Step 2: Create a witness with specific values
 36      x, y, z, u = 3, 5, 7, 11
 37      println("\n2. Creating witness with values:")
 38      println("   x = $x, y = $y, z = $z, u = $u")
 39      
 40      witness = create_witness_multiplication(x, y, z, u)
 41      r = x * y * z * u
 42      println("   Expected result: r = $r")
 43      
 44      # Verify the witness satisfies the R1CS
 45      if is_satisfied(r1cs, witness)
 46          println("   ✓ Witness satisfies R1CS constraints")
 47      else
 48          println("   ✗ Witness does NOT satisfy R1CS constraints")
 49          return
 50      end
 51      
 52      # Step 3: Convert R1CS to QAP
 53      println("\n3. Converting R1CS to QAP")
 54      qap = r1cs_to_qap(r1cs)
 55      println("   ✓ QAP created with degree-$(degree(qap.t)) target polynomial")
 56      println("   Evaluation domain points: $(qap.points)")
 57      println("   Coset offset for FFTs: $(coset_offset(qap.coset_domain))")
 58      
 59      # Step 4: Generate production-style keys (CRS)
 60      println("\n4. Generating Groth16 keys (CRS)")
 61      keypair = setup_full(qap)
 62      println("   ✓ Keys generated (ProvingKey + VerificationKey)")
 63      
 64      # Step 5: Generate proof
 65      println("\n5. Generating Groth16 proof")
 66      proof = prove_full(keypair.pk, qap, witness)
 67      println("   ✓ Proof generated:")
 68      println("   - [A]₁ ∈ G1")
 69      println("   - [B]₂ ∈ G2")
 70      println("   - [C]₁ ∈ G1")
 71      
 72      # Show proof elements in affine coordinates
 73      A_affine = to_affine(proof.A)
 74      C_affine = to_affine(proof.C)
 75      println("\n   Proof elements (affine coordinates):")
 76      println("   A.x = $(A_affine[1].value)")
 77      println("   A.y = $(A_affine[2].value)")
 78      println("   C.x = $(C_affine[1].value)")
 79      println("   C.y = $(C_affine[2].value)")
 80      
 81      # Step 6: Verify proof
 82      println("\n6. Verifying proof")
 83      
 84      # Extract public inputs (first 6 elements of witness: 1, r, x, y, z, u)
 85      public_inputs = witness.values[1:r1cs.num_public]
 86      
 87      # Verify using pairing check
 88      println("   Checking pairing equation: e(A,B) = e(α,β) · e(vk_x,γ) · e(C,δ)")
 89      is_valid = verify_full(keypair.vk, proof, public_inputs)
 90      
 91      if is_valid
 92          println("   ✓ Proof is VALID!")
 93      else
 94          println("   ✗ Proof is INVALID!")
 95      end
 96      
 97      # Additional verification details
 98      println("\n7. Verification Summary")
 99      println("   Public inputs verified:")
100      println("   - r = $(witness.values[2].value)")
101      println("   - x = $(witness.values[3].value)")
102      println("   - y = $(witness.values[4].value)")
103      println("   - z = $(witness.values[5].value)")
104      println("   - u = $(witness.values[6].value)")
105      println("   Private witnesses (not revealed to verifier):")
106      println("   - v1 = $(witness.values[7].value) (= x*y)")
107      println("   - v2 = $(witness.values[8].value) (= z*u)")
108      
109      println("\n" * "=" ^ 60)
110      println("Example completed successfully!")
111      println("=" ^ 60)
112  end
113  
114  # Run the example
115  main()