# EVM and the Ethereum Protocol

## Storage

The EVM can access four memory areas: storage, memory, calldata and stack. The storage layout of a Solidity contract directly maps to its EVM storage layout. In several cases, data locations of the variables need to be specified to the Solidity compiler using data location keywords. The storage is a word-addressable memory area that persists across contract calls. It is a key-value mapping with 256-bit slots. It stores all the state variables of a solidity contract, and every variable declared as a "storage" variable. It is allocated by the EVM when a contract is deployed and is part of Ethereum global state.

Account storage is governed by the code of the account and can eventually be written by other bytecode during a `DELEGATECALL` or a `CALLCODE`. The memory stores temporary values for the scope of a given call. However, it is wiped after each call. The calldata is a byte-addressable read-only memory. It is allocated by the caller and contains the input of the call, i.e., the function selector and the arguments passed to the function. Reading from this memory section requires specifying the exact number of bytes to read along with the position (offset) to start reading from.

The stack holds small local variables of size at most 256 bits. It is limited in size and cannot store complex structures. The EVM stack has a maximum depth of 1024 slots and is used for local computations. However, it can access directly only the top 16 slots.

[DIAGRAM_1]

## Library
Solidity introduces the concept of libraries. A library is similar to a contract, with the exception that it can be deployed only once at a specific address on the blockchain. Contracts can then `DELEGATECALL` into library functions, meaning the code of a function defined in the library is executed in the context of the caller contract. A library can thus modify the storage of the calling contract. Libraries can also contain internal functions meaning a contract calling these functions will follow the "internal" call paradigm, i.e., invoking the function using a `JUMP` instead of a `CALL`. To make this possible, the Solidity compiler inlines every internal library function in the contract at compilation time. Unlike contracts, libraries cannot have state variables (they must be executed in the context of the calling contract using `DELEGATECALL`), cannot receive Ether, cannot self-destruct, and do not support inheritance

## Interface
Interfaces instruct the Solidity compiler on how to invoke functions from external contracts. Solidity compiler assumes that all contracts will have the interface definitions of any Interface Interfaces instruct the Solidity compiler on how to invoke functions from external contracts. Solidity compiler assumes that all contracts will have the interface definitions of an

### Interface is Object-oriented programming

OOP also introduces the notion of an *interface*. An interface contains definitions for a set of related properties that a class must implement. It can be seen as a description of the actions an object must support, i.e., a contract that states what functionalities one can expect from a class implementing the interface. A class implementing an interface must provide an implementation for every method declared in the interface. Like classes, interfaces can also be extended by derived interfaces. Solidity also enables the defi- nition of interfaces that are very similar to general object-oriented program interfaces[^1]. The only difference is that Solidity interfaces can only declare external functions i.e., functions that can be called by external accounts. Interfaces in Solidity are important as they are required by contracts from different accounts to interact with each other.

[^1]: The careful reader will notice that typical Solidity naming patterns take after C++/C# as it relates to *Interface* naming and ilk.

> Thus, we can say state that Solidity contracts are very comparable to classes of object-oriented programs.

Solidity compiles every contract into a single bytecode executed on the EVM. When a contract is de- ployed, the EVM creates an instance of the contract and associates it with an address on the blockchain. This address can be used by EOAs or other contract accounts to interact with the contract. Any EOA or contract can deploy a new contract with a contract deployment transaction. A contract deployment transaction is a transaction whose recipient is the zero address, and the data contains the code needed to initialize the contract. This code, generated by the Solidity compiler, does two things: first, it runs the contract’s constructor to initialize the storage of the contract account. Second, it copies the rest of the bytecode (i.e., without the constructor) in the bytecode storage of the account. From an external point of view, a contract looks similar to an immutable class whose instance members are all private but with public getter methods defined for each public storage variable. However, this analogy breaks when contracts interact using `DELEGATECALL` or `CALLCODE` opcodes. Assume contract A maps to class A and contract B maps to class B, a `DELEGATECALL` from contract A to contract B can be seen as an unchecked typecast of class A to class B. The EVM delegates the control of A’s storage to B’s code. This is possible because of the slot-based storage mechanism of the EVM

## Call specifications

### Qualified call

A call into a contract is qualified for a property check if:

(1.) There is at least one contract invariant or call property defined for the corresponding function selector or special function (receive/fallback).

(2.) The call does not revert.

Theoretically, there should be no need to reestablish invariants when calling into the contract as long as they are reestablished before leaving the contract. When calling functions internally i.e., jumping, the contract is not in a visible state. Additionally, transaction execution is atomic: either it succeeds or reverts. No partial change to the world state is possible. The state is locked while the transaction is executing.[^2]

[^2]: This is similar to JML ( Java Modeling Language) way of handling helper functions: helper functions are authorized to violate invariants as long as they are re-established before leaving the contract in a visible state.

Unfortunately, the current EVM implementation breaks this semantic by enabling to transfer ETH into a contract without calling into it. It means that the balance of a contract account can change even if the account is not loaded inside the EVM context (i.e., without first calling into the contract[^3]). This is possible in the following case: one creates contract A, sends ETH to this contract, and makes this contract self-destruct. When self-destructing, the contract can be instructed to send all its funds to contract B without calling into B. Block creators can also directly reward ETH to any account without calling into the account. Consequently, we need to check every invariant referring to the balance of the account before every call into the contract. Otherwise, the caller may assume a violated invariant. This is also the reason we need to check balance invariants before deploying the contract.

[^3]: Transfer by Suicide, as this does not effect contract code.

### Call Pre and Post Conditions

> Call properties can only be specified for external and public functions of a contract that we generalize as the public functions of the contract. We start with functional specifications below.

#### Functional specifications

We focus on checking call specifications, more precisely, call post-conditions and call error pre- conditions by adding call properties. This differs from classical Hoare pre and post-conditions as we allow for evaluation of properties in case the program does not successfully terminate (if the transaction reverts) by using error pre-conditions. This also slightly differs from usual function properties and function pre/post-conditions found in most specification languages ( JML, Frama-C). That is because we focus on properties that can be expressed over the external interface of the contract. *Call properties can only be specified for external and public functions of a contract that we generalize as the public functions of the contract.* These are the only functions of the contract that can be called from external accounts. We provide two types of call property clauses to specify conditions

1.) if the call into the function *successfully terminates* (`if_succeeds`) or

(2.) if it *reverts* (`if_aborts`).

> Note that thanks to the EVM semantic, a call will always successfully return, or revert with an error.

### External Functions

External functions are part of the contract interface, which means they can be called from other contracts and via transactions. An external `function f` cannot be called internally (i.e. `f()` does not work, but `this.f()` works). External functions are sometimes more efficient when they receive large arrays of data, because the data is not copied from calldata to memory.