Assembly and Formal Verification - Horse Store

Metadata

A detailed walkthrough of Solidity’s Metadata - Learn how the compiler encodes meta data about the contract. This lesson will break down the compiler’s output and show you how this data can help with debugging, identifying the contract’s version, and understanding how it was optimized.

Course Overview

About the course

What you'll learn

Assembly

Writing smart contracts using Huff and Yul

Ethereum Virtual Machine OPCodes

Formal verification testing

Smart contract invariant testing

Halmos, Certora, Kontrol

Course Description

Who is this course for?

Smart contract security researchers
Advanced Smart contract engineers
Chief Security Officiers
Security professionals

Potential Careers

Security researcher

$49,999 - $120,000 (avg. salary)

Smart Contract Auditor

$100,000 - $200,000 (avg. salary)

Meet your instructors

Patrick Collins

Founder at Cyfrin

Web3 engineer, educator, and Cyfrin co-founder. Patrick's smart contract development and security courses have helped hundreds of thousands of engineers kickstarting their careers into web3.

Guest lecturers:

Josselin Feist

Head of Blockchain at Trail of Bits

Last updated on January 17, 2025

Thanks for checking us out

Start learning for free

Start for free

Solidity Developer

Assembly and Formal Verification

Section 1: Introduction

Duration: 30min

Section 2: Horse Store

Duration: 4h 38min

1. Huff Yul Opcode

A foundational guide to understanding EVM bytecode, opcodes, and contract disasembly. This lesson introduces you to tools like Huff and Yul, and walks you through how to interpret bytecode and opcodes for a simple Solidity contract using the Foundry framework. Duration: 4min

2. What are Opcodes

A comprehensive overview of opcodes, which are machine-readable instructions, as used in Ethereum. The lesson covers the basics of opcodes, their role in the Ethereum Virtual Machine (EVM), and how they are used to execute smart contracts. Duration: 6min

3. Introduction to Huff

A comprehensive introduction to Huff, a low-level language used for highly optimized smart contract development. The lesson covers how to install Huff, rewrite a Solidity smart contract in Huff, and how to use the docs to get started. Duration: 4min

4. Function Dispatching

A detailed explanation of function dispatching in the EVM - This lesson explains how Solidity natively handles function dispatching using the function selector and call data. The EVM uses the first four bytes of the call data to determine which function is being requested. This allows Solidity smart contracts to efficiently handle function calls without the need for explicit code to manage the process. Duration: 5min

5. Huff MAIN() Macro

A basic guide to defining a main function and entry point in Huff - This lesson covers what a main function does in Huff, defining a macro main and testing compilation with the huff command. Duration: 3min

6. Huff Syntax Highlighting

A helpful guide to Huff syntax highlighting in VS Code. The lesson covers how to find and install the Huff extension in VS Code, which enables syntax highlighting for the Huff programming language. Duration: 1min

7. Smart Contract Bytecode

A detailed look at the sections of a Solidity smart contract Bytecode. This lesson dives into the contract creation, runtime code, and metadata sections of the bytecode and provides practical examples to illustrate how these sections work. You'll learn about the purpose of each section and how they interact to create a functioning smart contract on the blockchain. Duration: 3min

8. Introduction to CODECOPY

A deep dive into the CODE COPY opcode for solidity smart contracts. This lesson breaks down what the CODE COPY opcode does, how it’s used in Solidity code, and why it’s a valuable tool for developers working on smart contracts. Duration: 1min

9. EVM: The Stack

A deep dive into the EVM - The Stack - This lesson explains that the EVM is a stack machine and how that impacts the way we store and interact with data. In addition, it explains that data structures within the EVM are structured in a way that allows us to store data on the stack, memory, and storage. Duration: 4min

10. Stack Memory and Storage

A detailed guide to understanding memory and storage within the EVM. This lesson covers how memory and storage operate within the Ethereum Virtual Machine and explains how these two features relate to the stack of pancakes. Duration: 2min

11. Push and Add Opcode

A simple explanation of how PUSH and ADD opcodes work in EVM - In this lesson, we discuss the role of the stack in Ethereum Virtual Machine (EVM) execution and the PUSH and ADD opcodes. We look at how to understand and interpret stack input and output, and we see how these two opcodes function in a practical application. Duration: 3min

12. Push Opcode

A simple guide to using the PUSH opcode in Huff - The lesson covers pushing data values onto the stack within a Huff smart contract using the PUSH opcode. This includes using the PUSH0 opcode, which pushes a zero onto the stack, and the PUSH1 opcode, which pushes a one onto the stack. Duration: 4min

13. Calldataload

A detailed guide to the Call Data Load OpCode - The lesson covers the basic concepts behind Call Data Load and how to implement it in Huff, a Solidity alternative, using the EVM.codes website as a reference. It also discusses how to visualize the stack in Huff code using comments to help with debugging. Duration: 4min

14. SHR

A practical guide to understanding Right Shift in Solidity - This lesson explains how the SHR opcode works and how it can be used to easily extract the function selector from the calldata. It shows you how to represent numbers in binary, hex, and decimal and uses these representations to demonstrate the effect of the SHR opcode on calldata. Duration: 4min

15. evm.codes Playground

A practical demonstration of EVM right shift operation using a playground. The lesson covers how to implement a right shift operation in a playground using various inputs and then checks the results by casting the value to base 10 decimal. Duration: 3min

16. SHR & CALLDATALOAD

A detailed explanation of the `SHR` opcode in Solidity. The lesson covers how to right shift a hexadecimal number in Solidity, how to determine the number of bits to shift by, and how to use the `SHR` opcode to perform a right shift of 224 bits. Duration: 4min

17. Op Codes Recap

A detailed introduction to EVM Opcodes and the Stack - The lesson covers the EVM's main data structure (the stack) and how opcodes are used to manipulate it. It shows how solidity compiles into opcodes to execute smart contract functions. Duration: 4min

18. Dispatching

A comprehensive guide to understanding how Solidity functions are routed using function selectors and EVM Bytecode - This lesson demonstrates how Solidity functions are routed to the correct bytecode based on the function selector, and it shows how this routing process can be accomplished when developing bytecode in the Huff language. Duration: 1min

19. Opcode EQ

A comprehensive guide to function selectors in Solidity smart contracts - This lesson covers how to compute a function selector in Solidity, how to check for function selector matches in assembly, and how to use the 'EQ' opcode to check for equality between the top two items on the stack. Duration: 1min

20. JUMP & JUMPI

A comprehensive guide to conditional jumping in Huff - Learn how to use the 'jump if' opcode to control the flow of execution in your Huff programs. You'll see how to use the 'jump' opcodes to create basic branching and conditional logic in your Huff programs. Duration: 4min

21. JUMPDEST

A detailed guide to the jumpdest opcode - This lesson dives into the jumpdest opcode, its functionality, and how it's used in conjunction with jump and jumpi. The lesson also illustrates real-world application by compiling and running a Huff contract. Duration: 4min

22. DUP1

A comprehensive guide to the DUP1 opcode in Huff. Learn how the DUP1 opcode duplicates the top item on the stack and why it's a valuable tool for function selector checking. Duration: 3min

23. readNumberOfHorses Function Dispatch

A beginner’s guide to understanding function dispatch in Huff - This lesson goes over function dispatch in Huff. In particular, it goes over what function dispatch is, how to use it, and how to create more efficient function dispatchers. Duration: 2min

24. Testing JUMPDEST

A deep dive into the JUMP and JUMPDEST Opcode. This lesson shows you how to use the JUMP and JUMPDEST opcodes to control the flow of execution in your Solidity code, giving you more control and flexibility. You'll learn what the JUMP and JUMPDEST opcodes do and how they can be used to create more complex smart contracts. The lesson also provides practical examples that you can try out for yourself to understand how these opcodes can be used in different scenarios. Duration: 2min

25. Revert

A simple guide to reverting a function call in an EVM smart contract. This lesson covers the REVERT opcode, including how it takes two parameters, 'offset' and 'size', how to revert the current context execution, and how to revert the state changes. Duration: 3min

26. Huff Interfaces

A comprehensive guide to using function signatures and interfaces in Huff. The lesson covers how to calculate function signatures using the __FUNC_SIG keyword, how to define interfaces to clearly define function structures for use in Huff, and how to use these interfaces with the __FUNC_SIG keyword to automatically calculate function signatures. Duration: 3min

27. Storage Refresher

A comprehensive guide to creating a Huff smart contract that stores and retrieves information using storage slots. This lesson covers the basics of Huff, including function dispatching, function selectors, and the mechanics of storage, and concludes with the creation of tests to confirm the Huff implementation aligns with a Solidity implementation. Duration: 3min

28. SSTORE

A detailed explanation of the SSTORE opcode. This video lesson covers how to store data in the Ethereum Virtual Machine (EVM) using the SSTORE opcode. It explains how the opcode takes input from the stack and how this input gets written to storage. The video lesson also discusses why this opcode is particularly useful for storing the number of horses in a contract and provides a demonstration of its usage in the code. Duration: 2min

29. FREE_STORAGE_POINTER()

A beginner’s guide to working with storage slots in Huff - This lesson covers how storage slots work in Huff, and how they relate to Solidity. It introduces the keyword `FREE_STORAGE_POINTER`, which helps manage storage slots in a more concise way. The lesson also shows a simple implementation of a storage variable in Huff, and explains how to use it to store the number of horses in a smart contract. Duration: 2min

30. Accessing Constant Variables

A comprehensive guide to accessing constant variables in Huff - This lesson covers how to define constant variables, assign them values and reference their values in your code using the `FREE_STORAGE_POINTER` keyword, and how to store a value into the storage slot that the constant variable represents. Duration: 1min

31. Function Parameters From Calldata

A detailed walkthrough to accessing function parameters from calldata & STOP opcode - This lesson is all about how we can access parameters passed to a function by using calldata. We then learn about the STOP opcode, which ends the execution of a function successfully without reversing. Duration: 3min

32. Testing Macro In evm.codes

A practical guide to building a function in Huff and understand how its bytecode functions - This lesson covers how to build a function using Huff to update the number of horses in a smart contract using raw EVM bytecode. It also demonstrates how to test the function using the EVM.codes playground. Duration: 3min

33. SLOAD MSTORE RETURN

A comprehensive guide to understanding the SLOAD and RETURN opcodes in the EVM. The lesson explores how to retrieve data from storage and memory to ultimately return a value to the user. This lesson includes detailed explanations of how the SLOAD and RETURN opcodes work, as well as visual examples illustrating data flow between the stack, memory, and storage. Duration: 2min

34. getNumberOfHorses Macro

A detailed guide to implementing a getter function in Huff - This lesson covers the basics of working with Huff's opcodes, including SLOAD and MSTORE, and how to use them in a simple getter function. We'll also demonstrate the RETURN keyword and how to use it to exit a function successfully. Duration: 3min

35. Testing in evm.codes

A detailed walkthrough of how the EVM processes opcodes - This lesson shows you a detailed step-by-step process of how the EVM executes opcodes in the context of reading data from storage. It shows you exactly how the opcodes interact with the stack and memory of the EVM. Duration: 2min

36. Huff and Opcodes Recap

A comprehensive guide to writing a HuFF Smart Contract. The lesson covers the fundamentals of HuFF, including writing your first HuFF contract, understanding OpCodes, and how to debug contracts using foundry. Duration: 2min

37. Differential Testing

A practical guide to writing differential tests for smart contracts - This lesson will show you how to write tests in Solidity and Huff that will check to make sure the two are working identically. You'll learn how to create a base test, inherit from that base test, and deploy contracts to ensure that they run on the same tests. Duration: 5min

38. Deploying Huff in Foundry

A practical guide to deploying Huff smart contracts in Foundry - This lesson teaches viewers how to utilize the Foundry-Huff extension to deploy Huff smart contracts in Foundry. We'll explore the steps of installing the extension and how to properly configure the Foundry.toml file. Then, viewers will learn how to import the Huff deployer, add a constant string to the contract, and finally deploy the smart contract. Duration: 4min

39. Foundry Opcode Debugger

A simple guide to understanding Foundry opcodes. In this lesson, we will learn how to use the Foundry debugger to step through opcodes and see what is happening under the hood of a Huff smart contract. We will be using a test case to illustrate how the debugger can be used to trace the execution of a Huff contract and analyze its behavior at the opcode level. Duration: 7min

40. Updating Tests To Fuzz Tests

A comprehensive guide to updating tests to Fuzz Tests. This lesson explores the process of implementing fuzz testing in Solidity projects, demonstrating how to leverage the power of fuzz testing to identify subtle vulnerabilities in low-level assembly code and ensure the consistency of your Huff and Solidity contracts. Duration: 2min

41. Introduction To Deconstructing a Solidity Smart Contract

A comprehensive breakdown of EVM opcodes by deconstructing a Solidity smart contract. The lesson shows you how to take Solidity code, break it down to its EVM opcodes, and understand what is going on at the binary level. This includes an example of how Remix interacts with EVM opcodes. Duration: 3min

42. Retrieving Solidity Op Codes From Bytecode

A deep dive into Solidity opcodes - This lesson covers extracting Solidity opcodes from a compiled smart contract, and then compares them to their Huff equivalents. Duration: 2min

43. Solidity's Free Memory Pointer

A detailed look into Solidity’s Free Memory Pointer - Solidity works with a special thing called the free memory pointer. This allows it to keep track of where in memory they can put new variables. Duration: 8min

44. msg.value Check In Opcodes

A deep dive into EVM Opcodes - A breakdown of the code that runs smart contracts. The lesson covers how to interpret EVM opcodes by looking at a simple Solidity contract and figuring out what each opcode does by going through a list of opcodes and seeing how they are used in the contract's compiled bytecode. Duration: 6min

45. CODECOPY

A comprehensive dive into the EVM Opcodes for contract creation. The lesson covers how the EVM interacts with contracts, examining the contract creation code by walking through different opcodes. It concludes by exploring the "Create" and "Create2" opcodes and the subtle distinctions between them, which determine the deployment process of a smart contract. Duration: 6min

46. Notes On Your New Found Powers

A mind-blowing look at your newfound opcode inspecting powers – the lesson covers why you would want to check for `msg.value` in a payable Solidity constructor and how to optimize a simple smart contract's code. You can now create more optimized Solidity code! Duration: 2min

47. Runtime code Introduction

A comprehensive breakdown of a Solidity Smart Contract's Runtime Code. The lesson covers the runtime code, which is the first part of the code executed on the blockchain, as well as the entry point to all calls made to the smart contract. Duration: 5min

48. Function Selector Size Check

A comprehensive breakdown of a Solidity smart contract - This lesson walks through a Solidity smart contract and explains its function selector size check. It also delves into the various opcodes and their functions as part of the smart contract's execution. Duration: 4min

49. Solidity's Function Dispatcher

A fascinating breakdown of Solidity's function dispatcher - This lesson takes a dive into the function dispatcher code produced by the Solidity compiler, and then compares that to a hand-written dispatcher in Huff. This is a great lesson if you want to understand how Solidity processes function calls. Duration: 6min

50. Setting Up JUMPDEST

A comprehensive guide to setting up Jumpdest program counters. This lesson covers the importance of Jumpdest program counters and how to identify them by looking at their byte size, as well as how they relate to function selectors. Duration: 2min

51. Checking If Call Data Is Big Enough

A detailed breakdown of the opcodes for `updateHorseNumber` in our Solidity smart contract - The lesson walks through the assembly opcodes line by line for the `updateHorseNumber` function in our simple Solidity horse counter smart contract, specifically highlighting how the EVM checks whether there is more calldata than just the function selector. Duration: 6min

52. SSTOREing Our Value

A deep dive into EVM bytecode breakdown for updating a horse number - This video lesson takes an in-depth look at the EVM bytecode generated by a Solidity smart contract, focusing on the specific instructions used to update a horse number value. Duration: 7min

53. updateHorseNumber Recap

A technical deep dive into Solidity bytecode and how it is generated. The lesson covers how to analyze the generated bytecode, understand how opcodes are executed, and see how Solidity uses jumps to control the flow of execution. Duration: 2min

54. readNumberOfHorses Op Codes

A thorough breakdown of the opcodes used by Solidity to execute a simple read operation - This video walks through the assembly code generated by Solidity when calling a function to read a value from storage. It then compares the code to its equivalent in Huff and identifies the differences. This lesson explains how to read a value from storage and how to update the free memory pointer to avoid wasting gas. Duration: 8min

55. Metadata

56. Decompilers - Disassembly

A comprehensive introduction to smart contract decompilation and disassembly, in which the user learns how to read and understand the underlying bytecode of a smart contract. The lesson covers topics such as opcodes, how opcodes function in Solidity, and demonstrates using the Dedub and Heimdall-rs tools to decompile bytecode back into Solidity. Duration: 4min

57. Compiled Solidity Opcode Recap

A comprehensive walkthrough of a Solidity opcode breakdown. This lesson covers how opcodes function, how they are assembled into a smart contract, and how Solidity sets up a free memory pointer. Duration: 4min

58. Precompiles

A comprehensive guide to precompiles in Ethereum - The lesson covers the basic understanding of precompiles in Ethereum, their uses and implementation. It also covers some of the most common precompiles. Duration: 1min

59. Introduction to Yul Inline Assembly

A comprehensive introduction to Yul/Inline Assembly - This lesson covers the basics of Yul, a low-level programming language that can be used to write Solidity contracts. It also explains how to use inline assembly to create more gas-efficient contracts and gain fine-grained control over contract execution. Duration: 3min

60. Inline Assembly

A comprehensive guide to Yul Inline Assembly. The lesson covers how to use Yul inline assembly with Solidity smart contracts, demonstrating how to set up your environment and implement a simple example of storing and reading data within a smart contract. Duration: 6min

61. Pure Yul

A comprehensive guide to Yul - A low-level programming language for Ethereum Virtual Machines. The lesson covers contract creation, deploying a contract and using helper functions to read a number and store a number in the blockchain, using Yul. Duration: 15min

62. HorseStoreV2 Introduction

A hands-on guide to writing a Solidity smart contract in Huff. The lesson focuses on understanding the lower-level concepts of EVM assembly language and using Huff to rewrite an ERC721 token smart contract. Duration: 7min

63. HorseStoreV2 Function Dispatch

A comprehensive guide to function dispatch in Huff. The lesson covers building a function dispatcher for a Solidity smart contract using Huff, going through the process of defining functions, using function signatures, and setting up jump destinations to call those functions. Duration: 5min

64. feedHorse() Macro

A comprehensive guide to creating a FeedHorse macro - The lesson covers using the FeedHorse op-codes, which are essentially pre-compiled EVM contracts to send data onto the EVM stack. We explore how the `CALLDATALOAD` opcode can be used to take the first four bytes of the call data, which is usually the function selector, and how to use the `TIMESTAMP` opcode to get the latest block timestamp. Duration: 2min

65. Mappings & Arrays in EVM - Huff

A comprehensive guide to using mappings and arrays in the EVM/Huff environment. The lesson covers how mappings and arrays work in the EVM/Huff environment, and also walks through how to use these concepts in practice by building out a simple horse-related smart contract. Duration: 5min

66. horseIdToFedTimeStamp

A comprehensive guide to creating a Solidity smart contract to store a horse's fed timestamp - In this lesson, we will create a Solidity smart contract to store the timestamp of when a horse was last fed. We will cover how to implement functions like "feedHorse", "horseIdToFedTimestamp", and "isHappy" to effectively track a horse's feeding history and its happiness. Duration: 3min

67. isHappyHorse

A detailed walkthrough of how to create a macro for 'isHappyHorse', a function that determines if a horse has been fed within a day in a Solidity smart contract. The lesson covers the implementation of this function in Huff, which includes utilizing call data, defining constants, making comparisons, and storing return values in memory. Duration: 7min

68. Quick Function - Then - HuffMate

A practical guide to implementing ERC-721 functionality in a Huff smart contract - This lesson covers the process of adding ERC-721 features to a Huff contract by importing and utilizing a library of pre-written ERC-721 functions, focusing on the core functions such as total supply, minting, and incrementing the total supply. Duration: 7min

69. Huff Constructor

A simple guide to adding an ERC721 function dispatcher to your Huff contract. This lesson teaches you how to add a function dispatcher for your ERC721 functions in Huff, allowing your contracts to have more flexibility and functionality. It covers setting up the ERC721 constructor, including copying and pasting the function dispatchers into your Huff file, and ensuring you have a total supply function dispatcher. Duration: 6min

70. Huff, Yul, and Solidity Gas Comparisons

A comprehensive guide to comparing gas costs in Solidity, Huff, and Yul - This lesson demonstrates the ability to compare the different gas costs of the same smart contract when coded in Solidity, Huff, and Yul. We learn how to leverage Foundry to run gas snapshots, and understand how to analyze the results. Duration: 2min

71. Section 1 Recap

A comprehensive guide to EVM assembly, opcodes, Yul, and Huff - In this lesson, we’ll explore some of the fundamental building blocks of the EVM (Ethereum Virtual Machine) through various languages like Yul and Huff, including how to write a simple smart contract with Huff. We’ll also cover the free memory pointer concept in Solidity and how to write gas-efficient code. Duration: 10min

Section 3: Math Masters

Duration: 3h 57min

Section 4: Gas Bad NFT Marketplace

Duration: 1h 56min