Dependencies

Given \(p, p' \in S\), we have that \(p\rightarrow p'\) if

• \(p, p'\in S_{\text{KEVM}}\) and Rewrites \(p\) \(p'\) holds.

• \(p, p'\in S_{\text{EvmYul}}\) and executing the step[38] or X[39] function on \(p\) yields \(p'\).

zeroes len returns a byte array of size len where every byte is the zero byte.

some (n * m)

some (n + m)

some (n - m)

Empty bytes wrapper.

Truncated division.

Given a transition system \((S, \rightarrow )\), a binary relation \(R\) on \(S\) is a bisimulation if and only if for every pair of states \((p, q)\in R\) we have:

• if \(p \rightarrow p'\) then there is \(q \rightarrow q'\) with \((p', q') \in R\);

• if \(q \rightarrow q'\) then there is \(p \rightarrow p'\) with \((p', q') \in R\).

Bytes to integer conversion.

Warning: The Lean reference link is broken because the name of the definition contains commas, and this apparently results in a new line.

EVM.step orchestrates opcode execution, taking the following arguments.

• Amount of gas left: fuel

• Cost of executing the opcode: gasCost

• Opcode to be executed: instr

Given these arguments and an EVM.state, the step function will perform the correspondent updates on the provided state according to the semantics of instr.

Formalization of the yellow paper’s \(X\) function as defined in section 9.4.

Given the following arguments:

• Amount of gas left: fuel.

• Valid jumpdests: validJumps.

• An EVM.State: evmState.

The function X performs the following tasks:

• Decode the opcodes present in evmState’s execution environment.

• Perform sanity checks and halt execution if these are not met.

• Assign gas costs depending on the decoded opcode.

• Execute EVM.step with the current decoded opcode.

• Iterate if the conditions are right.

The function «_<<_>>_SCHEDULE_Bool_ScheduleFlag_Schedule» (or _<<_>> for short) takes as arguments a schedule flag (such as \(G_{\text{hascreate2}}\)) and a schedule and returns the corresponding boolean if the schedule has the schedule flag. This is used to discriminate which rules can be applied depending on the schedule we’re working with.

In this example, working on an schedule SCHED, any rule involving the CREATE2 opcode will have to satisfy \(G_{\text{hascreate2}}\)<< SCHED >> in order to be applied.

The «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» function (or _<_> for short) takes as arguments a gas constant (such as \(G_{\text{verylow}}\)) and a schedule (such as CANCUN) and returns how much is that gas constant in that schedule.

Integer to bytes conversion.

Warning: The Lean reference link is broken because the name of the definition contains commas, and this apparently results in a new line.

Given \(n\) of type SortInt, \(\text{intMap}\, n =\, \)UInt256.toSigned\(\, n\).

Get the length of a bytes array.

Euclidian modulus.

Class of opcodes consisting of DIV, SDIV, MOD, SMOD, SIGNEXT, SLT, SGT, AND, XOR, NOT, BYTE, SHL, SHR, SAR.

oneOpLHS is a symbolic state representing all KEVM states that rewrite to some other state by means of executing any opcode from the stackOps_op class. Viewed as a function,

oneOpRHS is a symbolic state representing all KEVM states that are a rewrite of some other state by means of executing any opcode from the stackOps_op class. Viewed as a function,

Pads to the right a bytes array with a specific value.

Warning: The Lean reference link is broken because the name of the definition contains commas, and this apparently results in a new line.

Pads to the right a bytes array with a specific value.

Warning: The Lean reference link is broken because the name of the definition contains commas, and this apparently results in a new line.

Replace contents inside a bytes array.

Warning: The Lean reference link is broken because the name of the definition contains commas, and this apparently results in a new line.

Rules extracted to Lean from K will be enconded as constructors of this type.

We have that Rewrites : SortGeneratedTopCell → SortGeneratedTopCell → Prop where SortGeneratedTopCell is the type for KEVM states.

Given p, p’ : SortGeneratedTopCell, Rewrites p p’ means that the KEVM state p rewrites to p’.

All of the requires clauses of a rule are encoded as the corresponding constructor’s arguments.

There’s an special transitivy rule that ensures the chaining of multiple rewrite rules:

| tran
  {s1 s2 s3 : SortGeneratedTopCell}
  (t1 : Rewrites s1 s2)
  (t2 : Rewrites s2 s3)
  : Rewrites s1 s3

Alias for Bool.

Alias for ByteArray.

Bytes endianness.

Alias for Int.

Bytes signedness for integer representations.

KEVM states are represented by the type SortGeneratedTopCell. Hence, we will be taking as input a SortGeneratedTopCell and converting it to an EVM.State.

The state mapping function will take an extra EVM.State argument to perform the identity mapping on the parts of the state that are not yet mapped.

Slice a bytes array up.

Warning: The Lean reference link is broken because the name of the definition contains commas, and this apparently results in a new line.

toBytes’ n converts a given natural number n to its little endian bytes representation.

Crucially, this definition is private.

toBytes’ n converts a given natural number n to its big endian bytes representation.

toBytesBigEndian = List.reverse ∘ toBytes’✝

zeroes len produces a byte array of size len where every byte is the zero byte.

This part of the EvmYul FFI.

Injection type class.

Every sort in K is a subsort of the KItem sort. This type class will enable the injections of arbitrary sorts into the KItem sort with ease.

Wrapper to Inj.inj to trigger type resolution.

\(log_2\) on positive integers.

Max operation.

Integer complement.

Warning: Leanblueprint has a problem with \(\backslash \)lean{} references that contain special symbols. In this case, the \(\backslash \)lean{} reference is « Int_». This will cause the reference to be broken.

Integer powmod.

Warning: Leanblueprint has a problem with \(\backslash \)lean{} references that contain special symbols. In this case, the \(\backslash \)lean{} reference is «_^%Int__». This will cause the reference to be broken.

Given const : SortScheduleConst, we equate «_<_>_SCHEDULE_Int_ScheduleConst_Schedule» const .CANCUN_EVM to a simple match statement on const.

Given flag : SortScheduleFlag, we equate «_<<_>>_SCHEDULE_Bool_ScheduleFlag_Schedule» flag .CANCUN_EVM to a simple match statement on flag.

This theorem allows for a clean rewrite of \(\text{stateMap}(\texttt{oneOpLHS})\).

This theorem allows for a clean rewrite of \(\text{stateMap}(\texttt{oneOpRHS})\). We typically go beyond just a pure rewrite of the stateMap function and also simplify some of the initial expressions present either in oneOpRHS or as a result of the stateMap computation.

Given the restrictions posed by the Rewrites constructors corresponding to the stackOps_op opcode class, \(\texttt{Rewrites}_{\texttt{stackOps_op}}\) oneOpLHS oneOpRHS.

Assume

• All the conditions needed to satisfy the summaries of \(\texttt{Rewrites}_{\texttt{stackOps_op}}\),

• A schedule set to CANCUN,

• Enough gas per opcode,

• Well formed gas and program counter parameters in oneOpLHS,

• Non-negative elements in the stack of oneOpLHS.

Then, evaluating the function EVM.step with any of the stackOps_op opcodes on \(\text{stateMap}(\texttt{oneOpLHS})\) results in \(\text{stateMap}(\texttt{oneOpRHS})\).

EvmYul.toBytesBigEndian n = (List.reverse ∘ toBytes’_ax) n

Given

• a single-opcode program \(P\),

• a gas amount greater than 1,

• the program counter set to 1,

• the symbolic and well constrained remaining inputs of \(X\).

Executing \(X\) on \(P\) with a fully symbolic state with the above conditions is successful and returns an empty output with the following modifications to the symbolic state:

• The parameter returnData is empty.

• The executionLength is increased by one.

Assume

• All the conditions needed to satisfy the summaries of \(\texttt{Rewrites}_{\texttt{stackOps_op}}\),

• A schedule set to CANCUN,

• Enough gas per opcode,

• Well formed gas parameter in oneOpLHS,

• The program counter of oneOpLHS set to zero,

• Non-negative elements in the stack of oneOpLHS,

• A well formed stack in oneOpLHS

• The program to be executed in oneOpLHS be a single-opcode program consisting of any opcode of the stackOps_op class.

Then, evaluating the function EVM.X with any of the stackOps_op opcodes on \(\text{stateMap}(\texttt{oneOpLHS})\) results in \(\text{stateMap}(\texttt{oneOpRHS})\).