fix/0-instances

[naure]

Issue #433
Extracted from #368

[naure]

Test with 0 instances of JAL. Does nothing anyway.

[naure]

@hero78119 I'm not totally convinced by this solution because since the commitments are optional, that gives degrees of freedom for the prover and that's no good with Fiat-Shamir.

There should be some commitment to the choice of circuits in the transcript. For example, the numbers of instances (including number 0). Or some circuit ID.

Is there something like this?

[hero78119]

@hero78119 I'm not totally convinced by this solution because since the commitments are optional, that gives degrees of freedom for the prover and that's no good with Fiat-Shamir.

There should be some commitment to the choice of circuits in the transcript. For example, the numbers of instances (including number 0). Or some circuit ID.

Is there something like this?

@naure this raises an excellent point for discussion! Including the number of instances in the transcript could be beneficial, but I'd also like to explore the implications of leaving the number of instances out of the transcript. The number of instances holds a particularly significant role in our system, which makes this consideration especially interesting

Giving pc start/halt (+ error code) + public i/o, prover goal is to convince verifier, $\exists$ witnesses, a list of opcode sequences, such that the pc start can transit to halt successfully following the opcode sequences order. A malicious prover manipulation of num of instances, e.g. set to 0, is equivalent in functionality to claim a list of opcode absence in sequence. In a valid sequence, each consecutive opcodes are constrained via pc and next_pc, so a list of opcode absence shouldn't satisfy state transition if it suppose to be there. So degree of freedom of num-instance seem only categories into num = 0, or num > 0 case, which is not that much, and this value also not be called free-input.

However, it bring up a further examine, if prover set number of instance to 0 of an opcode, then the free-input candidate is the witness commitments of this opcode. Thus in verifier, if an opcode instance is set as 0, it commitment need to be excluded from transcript, otherwise the backdoor is there, since we dont verify mpcs on those commitment. So I think this PR also need to check verifier and assure those free-input are excluded.

[hero78119]

To ensure soundness, also consult @dreamATD’s opinion on whether its necessary to include the number of instances in the transcript :)

In other word, in Ceno paper (Asymmetric Sumcheck Protocol), does n suppose to be included in transcript in Fiat-Shamir heuristic?

[naure]

equivalent in functionality to claim a list of opcode absence

Indeed, no issues with the constraints. It’s about the IOP:

…degree of freedom of num-instance seem only categories into num = 0, or num > 0 case…
…the free-input candidate is the witness commitments…

Right! Or in other words:

1. The prover can choose the set of circuits while knowing the challenge.
2. The witness columns can be interpreted as belonging to different circuits. The prover aligns his free sequence of proofs (opcode_proofs) with the committed sequence of polynomials (transcript).

I’m tracking this question in #542. Let’s go with this PR to unblock e2e testing, and continue discussion there?

[matthiasgoergens]

@hero78119 I'm not totally convinced by this solution because since the commitments are optional, that gives degrees of freedom for the prover and that's no good with Fiat-Shamir.

In my previous VM we solved a similar problem by just always requiring people to commit to some positive number of instances, and didn't allow zero. (In our case, all our tables had to be padded to a power of two and for further technical reasons we needed at least four. So that's what we padded everything to.)

I'm not sure if any of this applies here.

In any case, I'm very in favour of making it possible to prove the execution of a program that has 0 occurrences of specific features or instructions.

[kunxian-xia]

In any case, I'm very in favour of making it possible to prove the execution of a program that has 0 occurrences of specific features or instructions.

If there is no instances of any particular instruction / opcode, why do we bother to prove them as the accumulated r_eval = 1, w_eval = 1, log_sum = 0?

[hero78119]

LGTM!

Checked with @dreamATD and also suggested add num_instance to transcript as well for more safety.
I think add stuff in transcript is easiler, but we need to ruling out behind the scene for what need to be added and what needless.
Thanks for raising separete issue #542 and we can move discussion there!