EVM proof in appliedzkp zkevm (11)

1. introduction

EVM Proof Used to prove ：

• state trie root The change is correct , By verifying that the transactions contained in a block have correct execution results .

EVM circuit Will be re implemented EVM, But it is verified from the perspective of verification , That means ,Prover Can help provide clues , As long as these clues do not contradict the results . Such as ,Prover Can provide information about call Whether or not to revert A clue to , Or something opcode Will you encounter the wrong clue , And then the EVM circuit It can be verified that the execution result is correct .

Transactions contained within a block can be simple ether transfers、contraction creation or contract interactions, Because every transaction has variable execution trace, Cannot use fixed circuit layout To verify specific region Specific to logic, So , We need to a chip To verify all possible logics, The chip Repeat yourself to achieve the whole circuit.

2. Custom type

The following types are customized for clues ：

Name	Type	Description
GlobalCounter	int	Order of random access to BusMapping, which should be in sequence
BusMapping	List[Tuple[int, ...]]	List of random read-write access data in sequence with GlobalCounter as index

3. Random Accessible Data

EVM The parser can do any random access to data Similar to account balance、account storage、stack in current scope、memeory in current scope, But for EVM circuit Come on , It is difficult to track these data to ensure the real-time consistency of these data .
therefore ,EVM proof have State proof To provide a valid list of random read-write access records indexed by the GlobalCounter as a lookup table to do random access at any moment.

take random read-write access records list be called BusMapping, Because its function is similar to that in computers bus, Used to transmit data between different parts . Allied ,read-only The data to random access The way is from lookup table load .

Target	Index	Accessible By	Description
Block	{enum}	Read	Block constant decided before executing the block
BlockHash	{index}	Read	Previous 256 block hashes as a encoded word array
AccountNonce	{address}	Read, Write	Account’s nonce
AccountBalance	{address}	Read, Write	Account’s balance
AccountCodeHash	{address}	Read, Write	Account’s code hash
AccountStorage	{address}.{key}	Read, Write	Account’s storage as a key-value mapping
Code	{hash}.{index}	Read	Executed code as a byte array
Call	{id}.{enum}	Read	Call’s context decided by caller (includes EOA and internal calls)
CallCalldata	{id}.{index}	Read	Call’s calldata as a byte array (only for EOA calls)
CallSignature	{id}.{index}	Read	Call’s signature as a byte array (only for EOA calls)
CallState	{id}.{enum}	Read, Write	Call’s internal state
CallStateStack	{id}.{index}	Read, Write	Call’s stack as a encoded word array
CallStateMemory	{id}.{index}	Read, Write	Call’s memory as a byte array

3. Circuit Constraints

This repetition chip have 2 individual main states, A call initializes , Another one for bytecode execution.

Reference material

[1] EVM Proof