Let's begin with Wittgenstein's famous statement, "What can be said at all can be said clearly, and whereof one cannot speak, thereof one must be silent." Now it's our turn to thoroughly examine Halo2, so that the zero-knowledge proof stack can be explained clearly and concisely.

From the view of engineering, it is also fascinating that how a statement, could be transformed to a succinct argument, which further might be verified with minimal effort. As a compiler, Halo2 helps users to think in a certain way, then carving a narrow but sufficient path to generate the final proof. How does this happen? How does Halo2 force you to think in a certain way? How is the magic inside happening when you synthesize a circuit?

Today we will go through all topics about Halo2.

Screen Shot 2023-10-19 at 9.08.20 PM.png

fig 1: https://zkiap.com/#34e5b6cf6e1d4dd3901940d4be2edb0b Session 7 Ying Tong Dai

ZK Prove System Stack

From the above figure, we could find some analogy between a zk prove system and a compiler for general purpose.

  1. Frontend: What scope can ‘Halo2 compiler’ cover? How is a gate constraint converted to polynomial, then being evaluated on domain? What is the ‘IR’? In this session we will demonstrate a common job that syntax parser does: parse a certain format then transform it to a canonical expression, here, is SAT problem.
  2. Backend: Commitment Scheme, we have KZG10 or IPA. What’s the common API they are based on? Is there possibility to extend to other scheme (Ponky3: Yes, but any room for Nova-alike scheme?) Here we will check how an IOP being implemented, especially focusing on the trait — what kind of properties they are describing? Is the module is flexible enough to extend to other schemes?
  3. Plugin: What other library is working with halo2? Here we will examine Halo2 ecosystem including but not limited to halo2wrong, gadgets(poseidon, ec), code-gen tool like snark-verifier, or even a full project like Scroll.
  4. Towards higher order: zkWASM. In zkWASM, WASM code is input, a real code parse and stack machine simulator become frontend, and now, Halo2 itself is a giant backend. Here we will go through how a WASM op could be translated to a circuit, thus filling in the what Halo2 is capable.
  5. Optimization: hardware acceleration. May include, EC-GPU, GPU caching, parallel evaluation, an so on.