Exploration of rearranging the step errors and to avoid soundness

[hero78119]

Describe the feature you would like

Background

Right now the execution state transition, (current state -> next state) witness filling is happened in bus mapping. Prover get the valid geth execution trace and rely on bus-mapping to fill the witness. If next_state cause an exec error, bus mapping will put error op in right place, then the respective constraints on error_op will be activated and assure the condition to cause this error is truly captured. Reverything work perfectly.

Potential Soundness

However, if a maliculous prover just change bus-mapping code/ or manually manipulating the next state to let it skip error op with normal op on purpose. Then based on it to manipulate stack/mem/address carefully and respectively running through all the opcodes to assume transaction reach the end successfully. The issue is, if the condition is only contraints in error op, if error op is disable purposely, will it be an potiential soundness issue?

Solution on framework design

1. combine normal state op & error state op constraints in one place, like what call op do (call op also check there is no insufficnet balance).
2. If an state in execution trace is possible be replace by others error state, need to make sure state constraints cover selector (not e1 & not e2 & not e3 & not e4), …) where in respective error state it’s error_selector (e1 or e2 or e3 ,…), eX means constraints

Feedback from @ed255 The idea of combining successful state and error state into one for each opcode pros and cons: pros:

• It makes the analysis of not forgetting error checks easier
• Reduction of execution states cons:
• Could lead to more complex constraints. For example, we have a single error state for all the opcodes that consume a constant amount of gas, and this state uses a lookup table to map the opcode to the gas cost. If we merge error and successful case, then we have to implement the same logic in all opcodes with constant gas
• What about opcodes that have many possible error situations? The execution state constraints may grow a lot with complex selectors to activate each of the possible states.

From this discussions there are 2 actions:

1. one is a must: create a framework to write negative tests for the EVM Circuit, and add many negative tests
2. Explore combining successful execution states with error situations. Proceeding with this would mean a significant refactor . So we should be very convinced of its benefits before implementing such a change

Additional context

No response

[hero78119]

similar issue also discussed with @han0110 maybe Han have other thoughts

[hero78119]

negative test on circuit is proposed in another issue https://github.com/privacy-scaling-explorations/zkevm-circuits/issues/400.