Keccak circuit

The keccak circuit is specified in detail in spec/circuits/var_len_keccak.md.

Nebra uses a fork of Axiom's halo2-lib. Changes are made to the keccak circuit in Nebra's halo2-lib fork to complete all constraints without the need for a second phase. The proofs generated by keccak circuit are verified alongside batch verification proofs in the outer circuit. All inputs to the Keccak Circuit and their corresponding hash images are constrained as instances. Outer verifier ensures consistency by constraining the keccak instances of bath verify and keccak proofs to be equal.

Entry points

The SafeCircuit implementation for KeccakCircuit offers the main entry points keygen and prover to generate the verification keys and to prove the keccak circuit. They handle the appropriate settings and otherwise act as a wrapper around KeccakChip.

Inputs to the circuit are formatted as KeccakVarLenInput as KeccakFixedInput which are wrapped in the KeccakCircuitInputs enum. KeccakCircuit::new serves as the main entrypoint on the prover side

Step 1: Assignment and byte decomposition of keccak inputs

KeccakCircuit::new is called with a keccak config and inputs as KeccakPaddedCircuitInputs. This function handles witness assignment and byte decomposition as specified in step 1 of the spec before passing the inputs to KeccakChip

Step 2, 3 and 4: Compute length in bytes, compute variable length keccak queries and compute fixed length keccak queries

KeccakChip provides the functions keccak_fixed_len and keccak_var_len as entrypoints. These perform step 2 3 and 4 of the spec

Step 5: Compose into field elements

Outputs computed in KeccakChip are composed into field elements

Precomputation for Step 6

KeccakChip::produce_keccak_row_data is used to compute the witness values for zkevm keccak config, which is used to constrain the actual keccak computation.

Step 6: Assign Keccak Cells

Keccak computation is assigned inside the zkevm KeccakCircuitConfig using the witness values generated in precomputation and constrained. Appropriate cells are exposed as instances.

Step 7 and 8: Constrained Queries

The inputs and outputs are constrained to be equal between the zkevm KeccakCircuitConfig and KeccakCircuit in KeccakChip::constrain_fixed_queries and KeccakChip::constrain_var_queries