• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Community
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • Apt
        • Error-checking
        • Fty-extensions
        • Isar
        • Kestrel-utilities
        • Set
        • Soft
        • C
        • Bv
        • Imp-language
        • Event-macros
        • Java
        • Riscv
        • Ethereum
          • Mmp-trees
          • Semaphore
          • Database
          • Cryptography
          • Rlp
          • Transactions
          • Hex-prefix
          • Basics
          • Addresses
        • Bitcoin
        • Zcash
        • Yul
        • ACL2-programming-language
        • Prime-fields
        • Json
        • Syntheto
        • File-io-light
        • Cryptography
        • Number-theory
        • Lists-light
        • Axe
        • Builtins
        • Solidity
        • Helpers
        • Htclient
        • Typed-lists-light
        • Arithmetic-light
      • X86isa
      • Axe
      • Execloader
    • Math
    • Testing-utilities
  • Kestrel-books
  • Projects

Ethereum

A library for Ethereum.

Currently this library contains a formal model of some aspects of the Ethereum ``world computer''. It is expected that this library will be extended with more Ethereum-related formalizations and tools.

This library is based on the following sources:

  • The Ethereum Wiki, referenced as `[Wiki]' in the documentation of this library. This Ethereum Wiki can no longer be found at the URL it had at the time, but presumably its contents have been migrated (and likely updated) to the Ethereum development documentation.
  • The BYZANTIUM VERSION 3e36772 of the Ethereum Yellow Paper, referenced as `[YP]' in the documentation of this library. Sections, appendices, and equations are referenced by appending their designations separated by colon, e.g. `[YP:3]' references Section 3, `[YP:6.1]' references Section 6.1, `[YP:B]' references Appendix B, and `[YP:(4)]' references Equation (4).
  • The Ethereum Improvement Proposal (EIP) 155, referenced as `[EIP155]' in the documentation of this library.

These square-bracketed references may be used as nouns or parenthentically.

Subtopics

Mmp-trees
Modified Merkle Patricia trees.
Semaphore
Ethereum's Semaphore.
Database
Database.
Cryptography
Cryptography in Ethereum.
Rlp
Recursive Length Prefix (RLP).
Transactions
Transactions.
Hex-prefix
Hex-prefix encoding.
Basics
Some basic Ethereum notions and utilities.
Addresses
Addresses.