part II · halo 2

The simulator on `halo2_proofs`.

Three runs of the same circuit through halo2_proofs::plonk::create_proof: an honest prover, a witness-indistinguishable simulator, and the strict ROM-programmable zero-knowledge simulator that satisfies the textbook ZK definition in the random-oracle model. The verifier in every case is the upstream halo2_proofs::plonk::verify_proof; the third row is the cryptographically load-bearing one.

The circuit is small on purpose. MulCircuit asserts a single multiplication gate q_mul · (a · b − c) = 0 on three advice columns and one instance column carrying c. There are no lookups, no rotations beyond the current row, and one selector. The witness is the pair (a, b); the public statement is the single scalar c. The relation R = { ((a, b), c) : a · b = c } admits every nonzero a as half of a valid witness, so the witness set is parameterised by a single field element. This multi-witness structure is what lets the WI simulator on the next slide work without forcing any value.

All three runs below pass through the same upstream prover and verifier. The only thing the simulator changes is which transcript implementation create_proof drives, and which witness it samples along the way.

Run it

Keygen runs once. After that, each click takes well under a second on a desktop. The two seeds are exposed in the URL hash; same pair, same byte-identical output.

c seed witness seed WASM loading…

The honest prover

A standard halo2_proofs::plonk::create_proof call. Sample a witness (a, b) with b = c · a⁻¹ for a uniformly sampled nonzero a; commit, vanish, evaluate, and open. The Fiat-Shamir transcript is Blake2bWrite. The verifier accepts under Blake2bRead; nothing surprising.

head (64 B) -

tail (64 B) -

The witness-indistinguishable simulator

Same circuit, same public c, but the simulator samples a different nonzero a from the witness set and runs the honest prover with it. Both honest and simulator drive the same upstream create_proof; the output bytes verify under Blake2bRead just like the honest run. The WI claim is: a verifier with access only to the proof bytes and the public statement cannot distinguish the two witnesses.

head (64 B) -

tail (64 B) -

The ROM-programmable zero-knowledge simulator

Same circuit, same c. The simulator chooses a sequence of Fiat-Shamir challenges uniformly at random in advance, then runs create_proof with the programmable transcript wrapper ProgrammableHalo2Write so the prover sees those challenges instead of hashing. The byte output verifies under the matching ProgrammableHalo2Read and is rejected by Blake2bRead. Acceptance under the programmable transcript is the zero-knowledge claim; rejection under Blake2b is the soundness side of the same coin.

head (64 B) -

tail (64 B) -

Programmed challenges

The 32-element list the simulator pre-committed to before running create_proof. The Pasta scalar field has ~254 bits, so these are 32-byte hex strings. The prover never hashes anything; it reads the next one off the queue every time it would have squeezed a Blake2b output.

What this shows

Three runs of the same circuit, three different transcripts, one upstream prover and verifier. The acceptance pattern determines what each run proves:

Run	Witness	Transcript	Blake2b verify	Programmable verify
honest	real (sampled)	Blake2bWrite	accept	n/a
WI simulator	different sample	Blake2bWrite	accept	n/a
ZK simulator	different sample	ProgrammableHalo2Write	reject	accept

The WI simulator's acceptance under Blake2b proves witness-indistinguishability: the verifier had to accept the proof of a different witness, with the same public statement, indistinguishably. The ZK simulator's pattern (acceptance under programmable, rejection under Blake2b) proves zero-knowledge in the random-oracle model: the simulator constructed an accepting transcript using only the public statement and the programmability power of the abstract oracle, with no leakage back to the witness.

Page III, Orchard, lifts both ideas to the production Action circuit. Same WI sampling argument, same programmable transcript trick, vastly larger circuit.

The Zcash protocol specification defines the concrete Halo 2 instantiation in §5.4.10.3 and the Pasta curves (Pallas and Vesta) in §5.4.9.6.