Remove free choice of circuits

[naure]

See thread: #521. cc: @hero78119 @dreamATD

tl;dr: There should be some commitment to the choice of circuits in the transcript.

For example, write the numbers of instances (including number 0). Or some circuit ID. Or a bitmask of chosen circuits.

Or maybe it’s not a real problem.

[hero78119]

Some follow ups, haven't review carefully, just recording first as some heads up

num_instance

we need to add num_instance in transcript for soundness after discussed with Sphere.

comment from @hero78119 : we can add num_instance, but my sense is w/o it probably same sound. On the other hands, as we miss it in first place (and it seems ok), we probably also need to sort out the reasoning. E.g. do we need to follow re-design transcript (relevant #201) to assure everything come from proof will be included in transcript in more bug-free way.

Free-input in transcript

Free input also means unconstrained input. The impact of free input is as those data can be any value without affect the integrity of proof. A malicious prover can modify free-input to manipulate the desire challenge distribution and break random oracle model.

Notes of few place of suspicious vulnerability (yet exhaustive list)

case 1: strictly num_instance > 0 check in verify_xxxx_proof

commitment of witness is writing here

ceno/ceno_zkvm/src/scheme/verifier.rs

Lines 102 to 104 in ffd5773

	for (_, (_, proof)) in vm_proof.opcode_proofs.iter() {
	PCS::write_commitment(&proof.wits_commit, &mut transcript)
	.map_err(ZKVMError::PCSError)?;

If an opcode/table proof is non-empty, then proof.wits_commit.root() digest will be write to transcripts.

Then it make sense for add assertion inside to assure non-empty proof -> num_instane > 0 in verify_opcode_proof and verify_table_proof for assert!(num_instance > 0) to assure mpcs opening check is enable.

case 2: mpcs trustless from data from proof

@yczhangsjtu we might need to review carefully in basefold simple_batch_verify
There are few length check are derive from proof
e.g. commitment from "proof.wits_commit", evals from "proof.wits_in_evals". We might need to carefully review is there possible for a malicious prover to commit more data, but set less batch size, so possible for orphan commitment involved in transcript but skip verified.
I didnt review carefully, just bring an heads up, as I think probably we should define "verifier key" and retrieving, e.g. poly batch size from there as it should be settled from key setup phase