Define a stable serialization format for VerifyingKey

[str4d]

in https://github.com/appliedzkp/zkevm-circuits/blob/main/circuit-benchmarks/src/evm_circuit.rs#L84 using the vk in memory works fine, but saving&reloading the VK (not PK mentioned in this issue) doesn't work. (and https://github.com/zcash/halo2/blob/main/examples/sha256/benches.rs works good)
Would you happen to have a chance to know any clue?

Originally posted by @HAOYUatHZ in #443 (comment)

[0xmountaintop]

a bit more of the context:

1. we switch to pairing bn256 instead of using pasta
2. the reported error is virtual selectors are removed during optimization

[ursi]

the following code can be added to the end of the main function in simple-circuit.rs to demonstrate this error.

use halo2_proofs::{
    plonk::{create_proof, keygen_pk, keygen_vk, VerifyingKey},
    poly::commitment::Params,
    transcript::Blake2bWrite,
};
use pasta_curves::{vesta, EqAffine};
use rand_core::OsRng;

let params: Params<EqAffine> = halo2_proofs::poly::commitment::Params::new(k);

let vk = keygen_vk(&params, &circuit).unwrap();

let mut vk_buffer = vec![];
vk.write(&mut vk_buffer).unwrap();
let vk =
    VerifyingKey::<EqAffine>::read::<_, MyCircuit<Fp>>(&mut &vk_buffer[..], &params).unwrap();

let pk = keygen_pk(&params, vk, &circuit).unwrap();
let mut transcript = Blake2bWrite::<_, vesta::Affine, _>::init(vec![]);

create_proof(
    &params,
    &pk,
    &[circuit],
    &[&[&[c]]],
    &mut OsRng,
    &mut transcript,
);

[ursi]

Possible helpful info:
If you change this line to vec![(lhs * rhs - out)] (and comment out the assertions from the MockProver section), you will no longer get any errors.

[ursi]

The code that is supposed to test this is used on a circuit that has no selectors

[str4d]

I've figured out the problem.

ViewingKey::read reads two components from the encoding (commitments to fixed columns, and the permutation verifying key), and reconstructs the ConstraintSystem from the provided Params:

halo2/halo2_proofs/src/plonk.rs

Lines 64 to 70 in 9617336

	let (domain, cs, _) = keygen::create_domain::<C, ConcreteCircuit>(params);
	let fixed_commitments: Vec<_> = (0..cs.num_fixed_columns)
	.map(|_| C::read(reader))
	.collect::<Result<_, _>>()?;
	let permutation = permutation::VerifyingKey::read(reader, &cs.permutation)?;

During keygen, we generate both the fixed column commitments and the permutation verifying key. However, we also mutate the ConstraintSystem:

halo2/halo2_proofs/src/plonk/keygen.rs

Lines 207 to 221 in 9617336

	// Synthesize the circuit to obtain URS
	ConcreteCircuit::FloorPlanner::synthesize(
	&mut assembly,
	circuit,
	config,
	cs.constants.clone(),
	)?;
	let mut fixed = batch_invert_assigned(assembly.fixed);
	let (cs, selector_polys) = cs.compress_selectors(assembly.selectors);
	fixed.extend(
	selector_polys
	.into_iter()
	.map(|poly| domain.lagrange_from_vec(poly)),
	);

The problem is that the effect of ConstraintSystem::compress_selectors is not being persisted in the VerifyingKey. That function mutates the following fields of ConstraintSystem:

• selector_map is set (replacing the default vec![]). This is only used to render the graphical layout.
• gates and lookups have the selectors in their expressions replaced with the real fixed columns.

We don't want to re-synthesize the circuit in VerifyingKey::read; otherwise there's no point in serializing the VerifyingKey in the first place. So we need to serialize one of the following:

• The input to ConstraintSystem::compress_selectors
  • The enabled selectors, a Vec<Vec<bool>> of size 2^k * num_selectors.
• The data needed to recreate its effects:
  • selector_map, a Vec<Column<Fixed>> of size num_selectors.
  • selector_replacements, a Vec<Expression<F>> of length num_selectors.

I suspect it will be easier to serialize the inputs. k is known from params, num_selectors is known in VerifyingKey::read due to re-running circuit configuration, and the serialization requires max(num_selectors << (k - 8), 1) bytes. We could probably use the bitvec crate to make this easier. By contrast, we currently don't have a serialization for either Column or Expression, and I'd prefer we don't try to define one, even if it would help us to avoid re-running selector compression (and maybe save some bytes in the VerifyingKey encoding).

[daira]

I would prefer that we not rerun selector compression, just for simplicity of analysis. Selector compression is supposed to be expressible as an optimization that transforms PLONKish circuits to PLONKish circuits. That is, it should be possible to serialize the transformed gates.

[ebfull]

Note that changing the serialization of the verification key to resolve this issue will be incompatible with older proofs, because the verification key is serialized in order to initialize the common inputs for Fiat-Shamir.

[str4d]

In a pairing, @ebfull and I decided that for halo2_proofs 0.1.0 we will remove the VerifyingKey::write and VerifyingKey::read APIs as we do not have time to fix this before then. We are instead making the necessary modifications internally to ensure that when a serialization format is defined, it doesn't cause proofs to become invalid. This issue can now be about defining that format.

[L-as]

Related: Currently you need the circuit to read the VerifyingKey, which seems counterintuitive to me. Is there any chance this limitation could be lifted, such that you don't need the code for creating the circuit to verify a proof?

[ebfull]

@L-as You do need the Circuit though note that you don't need an instance of the circuit. This is because the Circuit implementation instructs the verifier about how it should behave (the gates, columns, etc.) unlike in many other SNARKs where this stuff is constant size and the verification behavior is the same regardless of the circuit. In theory we could encode all of this data into the verification key too, we haven't done so yet because it's very complicated. (Related: #117)

[daira]

The verification key serialization should include the number of public input elements.