Welcome to elle’s documentation!

Contents:

• Overview
• Installation
  • Getting Elle
  • Installation as an End-User of Elle
  • Installation for Modifying and Examining Elle
• Usage of the LLL Frontend
  • Basic Usage
  • Supported LLL Constructs
  • Debugging Failed Compilation
  • Inspecting Bytecode
• Elle Syntax
  • Goal: Compiling Structured Code to EVM
  • De Bruijn Indices and Structured Programming
  • Elle-Core Syntax
  • Label Resolution in Elle
  • Resolving Jump Addresses
  • Conclusion
• Elle Semantics
  • Goal: A Formal Meaning for Elle Programs
  • Informal Description of Semantics
  • Interpreter (Pseudo)Code
• Implementation
  • Phase 1 - Generating Size Annotations
  • Phase 2 - Finding Labels
  • Phase 3 - Resolving Jumps
  • The Big Picture
• Correctness
  • The Corrcetness Theorem
  • Setting Up the Proof
  • Correctness of Elle: Proof Sketch

Indices and tables