# Groth16 Theorem 1 Walkthroughs

Interactive, single-file HTML walkthroughs of the knowledge-soundness proof of Groth's 2016 zk-SNARK ("On the Size of Pairing-Based Non-interactive Arguments"). Each page steps through the coefficient-matching reduction that extracts a QAP witness from any accepting proof, with the CRS pinned at the top, the verifier equation highlighted per step, and the forms of `A, B, C` updated in place as coefficients are zeroed or substituted.

## Files

- **[ggm.html](ggm.html)** — the proof in the **affine prover / Generic Group Model** framing (Groth's original). The adversary is modeled as one who can only combine CRS group elements linearly; the proof treats `A, B, C` as Laurent polynomials in the trapdoor indeterminates and pattern-matches monomials against the verifier equation.
- **[agm.html](agm.html)** — the same reduction re-framed in the **Algebraic Group Model** (Fuchsbauer–Kiltz–Loss). The AGM axiom hands us the adversary's representations of `A, B, C` directly, the *q*-DLOG assumption lifts point-wise equality to formal polynomial identity, and the extractor reads the witness straight off the adversary's representation of `C`.
- **[weak-se.html](weak-se.html)** — walkthrough of a related result on weak simulation-extractability of Groth16.

The GGM and AGM walkthroughs share the same 12-step coefficient reduction; they differ only in the intro card, step 0, step 7a (extraction framing), and the capstone. The mathematical core is identical — what changes is the surrounding story about *why* the polynomial identity holds and *what* the extractor outputs.

## Walkthrough structure (ggm.html / agm.html)

| Step | Coefficient | What happens |
|------|-------------|--------------|
| 0    | —           | General affine / algebraic representation |
| 1    | α²          | `B_α = 0` (WLOG by relabeling) |
| 2    | αβ          | rescale: `A_α = B_β = 1` |
| 3    | β²          | `A_β = 0` |
| 4a   | δ⁻²         | WLOG `B`'s `1/δ` part vanishes (integral-domain argument) |
| 4b   | δ⁻¹         | `A`'s `1/δ` part vanishes — using β from step 2 in `B_{δ⁰}` |
| 5a   | γ⁻²         | WLOG `B`'s `1/γ` part vanishes |
| 5b   | γ⁻¹         | `A`'s `1/γ` part vanishes |
| 6    | βγ, αγ      | `A_γ = B_γ = 0` |
| 7a   | α           | witness extraction: `a_i := C_i` for `i > ℓ`; `B(x) = Σ a_i v_i(x)` |
| 7b   | β           | symmetric: `A(x) = Σ a_i u_i(x)` |
| 8    | pure x-poly | derives the QAP divisibility identity `(Σ a_i u_i)(Σ a_i v_i) = Σ a_i w_i + h(x) t(x)` |

Residual coefficients (`A_δ, B_δ, C_α, C_β, C_δ, C(x), C_h(x)`) stay free — they're slack variables that adjust to keep the verifier equation consistent; the walkthrough doesn't force them to zero because honest provers need `A_δ = r, B_δ = s` for zero-knowledge. See the note on step 8 for details.

## Viewing

No build step. Open any `.html` file directly:

```sh
open ggm.html   # or agm.html, weak-se.html
```

KaTeX is loaded from a CDN (`cdn.jsdelivr.net`), so an internet connection is needed the first time.

## Controls

- `←` / `→` — previous/next step
- `Home` / `End` — jump to first/last step
- Click any chip in the bottom step-navigator to jump directly
- `#step-N` URL hash deep-links to a specific step (right-click any chip to copy)

## References

- Jens Groth, [*On the Size of Pairing-Based Non-interactive Arguments*](https://eprint.iacr.org/2016/260), EUROCRYPT 2016.
- Fuchsbauer, Kiltz, Loss, [*The Algebraic Group Model and its Applications*](https://eprint.iacr.org/2017/620), CRYPTO 2018.
- Baghery, Kohlweiss, Siim, Volkhov, [*Another Look at Extraction and Randomization of Groth's zk-SNARK*](https://eprint.iacr.org/2020/811), ePrint 2020/811.