Add bus mapping lookup in POP

[han0110]

There is an issue in original POP's spec: it increases the global_counter even it doesn't do bus mapping lookup. This breaks the requirement that each global_counter corresponds to an expected read-write in state circuit. (Imagine that a malicious prover could use this non-used global_counter to insert unexpected write in state circuit)

However, if we don't do the bus mapping lookup, we can't ensure that 0 <= stack_pointer < 1024 at this step, since we assume the state circuit will verify that. (Imagine that a contract starts with POP and then STOP immediately, which would pass the verification)

So there are 2 approach to fix this:

1. Do the bus mapping lookup to verify stack_pointer is in range
2. Explicitly do range check on stack_pointer

After some consideration, I think since we are already outsourcing the effort of verify stack_pointer is in range, then we should just use approach 1. to reduce the overall validity check.

[ChihChengLiang]

The fix looks good.

[ChihChengLiang]

@DreamWuGit Can we update the circuit to reflect this change?

[CPerezz]

This is being implemented following the rationale exposed by @han0110 in privacy-scaling-explorations/zkevm-circuits#140 and I think it makes sense.

If we add the check and the Read operation in the bus-mapping I think makes everything more homogeneous over all opcodes so that the correctness checking is easier.

Should we proceed on this way and keep with the Stack read? @han0110 @ChihChengLiang ?

[DreamWuGit]

This is being implemented following the rationale exposed by @han0110 in appliedzkp/zkevm-circuits#140 and I think it makes sense.

If we add the check and the Read operation in the bus-mapping I think makes everything more homogeneous over all opcodes so that the correctness checking is easier.

Should we proceed on this way and keep with the Stack read? @han0110 @ChihChengLiang ?

I think CC means update in the evm circuit here, rather than bussmapping side ?

[CPerezz]

I think CC means update in the evm circuit here, rather than bus-mapping side ?

Sure, What I was referring to was to the fact that the bus-mapping has to create a Stack operation or not depending on the outcome of this discussion. And seems that it will be the case. This stack operation will be the one witnessed by the zkevm-circuits crate.

[CPerezz]

LGTM!

[DreamWuGit]

LGTM