Summarize all the EVM opcodes

[Stevengre]

What is an opcode summary

For this opcode, the backend can rewrite one step to execute it. It could be several rules.

Why we need summaries

It's important to provide summaries for all EVM opcodes, because:

1. prove semantics equivalence between different implementations.
2. improve the performance for both interpretation and verification.

[Stevengre]

Remaining TODOs

• summarize all the unpassed opcodes
• refine specifications for better summary
• provide a way to generate optimization.md automatically
• evaluate the effectiveness of the summary

[Stevengre]

Remaining Issues in the summary rules

• The stack overflow check is in the ensures clause which will lead to ndbranches or unexpected branches.
• We don't need the revert summary rules like EVMC_STACK_OVERFLOW.
• We need a better rule name for the summary rules, like XX-SUMMARY-USEGAS and XX-SUMMARY-NOGAS.