Skip to content

Latest commit

 

History

History
77 lines (48 loc) · 4.27 KB

ARCHITECTURE.md

File metadata and controls

77 lines (48 loc) · 4.27 KB
Raw

Table of Contents

  1. Table of Contents
  2. Overview
  3. Architecture
  4. Source Files
    1. High Level
    2. Mid Level
    3. Low Level

Overview

The evm-dafny repository contains five directories and five stand-alone files the most remarkable of which are the following:

  • github/workflows consists of the build process of different modules and their dependencies,

  • fixtures contains the ethereum tests to generate, to test our system against,

  • resources contains the log of tests which have been generated and our system is tested against,

  • src comprises the backbone of our system including the formal semantics of the Dafny-EVM. It contains three subdirectories:

    • dafny consists of the Dafny-EVM Source Files as explained further below,
    • main includes the Java interface to the Dafny,
    • test contains simple tests implemented in dafny for checking the correctness of different opcodes

  • tests consists of the list of ethereum tests we are currently running,

  • build.gradle consists of build instructions with the gradle tool,

We organize the Source Files of the Dafny-EVM according to a three-layer architecture explained further below.

Architecture

The architecture of the Source Files comprises the three layers; top, middle and the bottom layer, as shown in the image below. The top of the stack image, shows the [High Level] modules containing bytecode semantics and top-level types. We locate in the middle of the image, modules of the Middle Level which contain abstractions of the main components. The bottom of the stack depicts the modules placed at the Low Level which specify fundamental primitives (e.g. for manipulating bytes and ints).

Dafny-EVM Architecture

Source Files

The source files including our formalisation of the EVM semantics, the state, gas calculations, and helper modules appear under the directory src/dafny. The architecture of the source files accords with the three layer model explained above.

High Level

  • evms contains modules each of which specify an extension of our EVM with a particular hardfork of users' choice, for example berlin.dfy.

  • opcodes.dfy encodes all of the EVM opcodes.

  • evm.dfy provides a generic mechanism for building extensions on our EVM based on a hardfork of users' choice.

  • evmstate.dfy specifies various EVM states and how to perform operations on them.

  • bytecode.dfy includes the implementation of the EVM opcodes' semantics.

  • gas.dfy specifies gas charging calculations.

Mid Level

  • code.dfy is an implementation of read-only code region of the EVM.
  • context.dfy implements the execution context of a transaction.
  • memory.dfy is a specification of the EVM's volatile memory.
  • precompiled.dfy implements precompiled contracts.
  • stack.dfy specifies the stack of EVM together with stack operations.
  • storage.dfy is an implementation of the EVM storage including functionalities for performing operations on the storage.
  • substate.dfy encodes the substate of the EVM.
  • worldstate.dfy specifies the world state of the ethereum.

Low Level

  • option.dfy
  • bytes.dfy implements an specification of machine bytes together with methods for performing operations on them.
  • int.dfy specifies machine words of various length both signed and unsigned.
  • extern.dfy interfaces Dafny with Java.