Introducing halo2-repl: A Browser-based REPL for halo2 in Javascript

Roshan, Yi Sun

• 4 min read
Introducing halo2-repl: A Browser-based REPL for halo2 in Javascript

Today we are releasing halo2-repl, a browser-based REPL for halo2 in Javascript. This allows developers to write ZK circuits using only standard Javascript and without the need to learn new languages like Rust, install proving libraries, or wrangle dependencies. ZK circuits written in halo2-repl can be compiled and proven directly in the browser, meaning you can get started with ZK right away. We've included a small circuit puzzle as the default circuit in this release – try writing a circuit to solve the puzzle and tweet your solution to us at @axiom_xyz!

Under the hood, halo2-repl uses WebAssembly bindings to allow your Javascript code to call into ZK circuit primitives in our halo2-lib library written in Rust. This gives developers access to the power of Rust in a familiar Javascript format. We've packaged these bindings into halo2-browser, a suite of tools to make in-browser proof generation with halo2 easier, which we've open-sourced in conjunction with this release. We are taking PRs on these repos and hope to work with the community to make deploying ZK circuits in the browser easier.

This release owes a debt to substantial prior work. Thanks to the amazing developers at Electric Coin Co. and the Privacy & Scaling Explorations team at the Ethereum Foundation for building halo2. For the REPL interface, we drew obvious inspiration from zkREPL, and we learned about compiling halo2 to WASM from Nalin Bhardwaj's guide.

Using halo2-repl

To write a ZK circuit with halo2-repl, you can use standard Javascript syntax and bindings to halo2-lib documented here. Once you've written a circuit, you can perform the following operations:

  • Test Circuit: Run a "mock proof" which fills in the constants and witnesses in your ZK circuit and generates the public input/outputs without actually generating a ZK proof. This should be used for testing purposes only.
  • Generate Keys: Generate proving and verification keys for your ZK circuit. Once generated, you can export the verification key under the Export tab.
  • Generate Proof: Actually generate the ZK proof. This requires Generate Keys to have been run. Once generated, you can download the proof under the Export tab.
  • Verify Proof: Verify the generated ZK proof against the verification key. At present, this step should always pass if both the proof and verification key have been generated.

We'd love to merge any features or tooling to enhance the halo2-repl experience. A few things we have in mind are: exporting an in-browser prover or on-chain verifier, allowing verification of external proofs, and adding additional circuit bindings. Check out the halo2-browser repo for good first issues!

Building halo2-repl with halo2-browser

The halo2-browser repo has 3 modules: halo2-wasm, halo2-lib-js, and halo2-repl. The first two are used as a toolkit to build halo2-repl, and we hope they will be helpful for building other applications which generate halo2 proofs in the browser.

halo2-wasm

halo2-wasm uses wasm-bindgen to create JavaScript bindings for all the common circuit operations like proving, key generation, and verification. halo2-wasm handles all the serialization and parsing of values passed between Rust and JavaScript and is easily extensible for your own circuit needs. It also includes the halo2-lib-wasm class, which wraps all the common halo2-lib functions like add and mul so that you can directly write a circuit in JavaScript without having to deal with halo2-lib and Rust. halo2-wasm also includes a TypeScript scaffold, CircuitScaffold, to facilitate using the JavaScript bindings without having to worry about setting up and using the WASM binaries.

halo2-lib-js

halo2-lib-js is a strongly-typed eDSL for halo2-lib built on top of halo2-wasm in TypeScript. It wraps all the halo2-lib-wasm functions with TypeScript definitions and introduces the CircuitValue class to clearly delineate between in-circuit values and JS values. Circuits are TypeScript functions that take as input halo2-lib/halo2-lib-wasm context objects, and witnesses are assigned by calling halo2-lib-wasm functions. Once the circuit function is run, you can then run key generation, proving, or any of the other functions in halo2-wasm.

halo2-repl

halo2-repl contains the frontend Next.js app of our REPL, built using halo2-lib-js and halo2-wasm.

Benchmarks

We ran some simple benchmarks for the ECDSA signature verification circuit from halo2-ecc in halo2-repl. In certain settings, we are seeing in-browser proving times below 10 seconds for this benchmark task.

These benchmarks were done on a M2 MacBook Air with 24GB RAM in Safari.

What's Next?

We're excited to have you play around with halo2-repl and would love to see what you build with it. The underlying code is open-source with an MIT license at halo2-browser, and we welcome contributions! We've also created a Telegram group here for technical discussion and collaboration.

Finally, in the coming weeks, we'll share how halo2-repl plays a role in future releases of Axiom. Follow us on Twitter or join our technical Telegram discussion group to stay updated.