Spec ExecutionState::{EndTx,EndBlock}

[han0110]

This PR aims to spec ExecutionState::EndTx and ExecutionState::EndBlock, for enable EVM circuit to verify block consists of minimal transaction. With BeginTx, EndTx and EndBlock, the finite state machine diagram will look like:

The EndTx aims to handle tx refund to signer, and tx fee to coinbase.

The EndBlock aims to pad the EVM circuit to the fixed capacity, and checks tx_id and rw_counter at the last step.

Also it refactors random linear combination usage, to make things more straightforward. Regardless of the refactors, please refer to end_tx.py and end_block.py for spec itself.

TODO

• Testing ExecutionState::EndTx
• Testing ExecutionState::EndBlock

[CPerezz]

Should we also file issues for the TODOs that we will leave with this PR?

[CPerezz]

Question: Which is the purpose of applying the RLC to the keccak inputs? Hasn't it been done previously in assign_bytecode_circuit?

Also, why do we need to reversethe bytecodet?

[han0110]

Which is the purpose of applying the RLC to the keccak inputs? Hasn't it been done previously in assign_bytecode_circuit?

This is a mocking keccak_table, for lookup the hash by RLC of bytecode and length.

Also, why do we need to reversethe bytecodet?

Because in bytecode circuit, it accumulates the bytes in big-endian order, so we need to reverse it for RLC, which takes input as little-endian.

[CPerezz]

Makes complete sense!

[ed255]

LGTM!

[CPerezz]

LGTM!