Merge pull request #79 from Cyfrin/formal-verification

Formal verification

content/authors/nader-dabit.json

@@ -2,6 +2,6 @@
   "authorId": "95eddbc5-e8be-4e52-92bc-531ced06dd59",
   "name": "Nader Dabit",
   "role": "Director of developer relations",
-  "avatarUrl": "https://pbs.twimg.com/profile_images/1683249222534025216/-AksKsna_400x400.jpg",
+  "avatarUrl": "https://res.cloudinary.com/droqoz7lg/image/upload/v1708620482/authors/auth2_yriysu.jpg",
   "company": "Avara"
 }

content/authors/richard-gottleber.json

@@ -2,6 +2,6 @@
   "authorId": "ed8b10d7-cd01-465b-85a5-28a13ea2422a",
   "name": "Richard Gottleber",
   "role": "Developer relations",
-  "avatarUrl": "https://pbs.twimg.com/profile_images/1575811580419350528/YDFtORxH_400x400.jpg",
+  "avatarUrl": "https://res.cloudinary.com/droqoz7lg/image/upload/v1708620479/authors/auth1_rwkb2f.jpg",
   "company": "Chainlink"
 }

courses/formal-verification/1-horse-store/1-huff-yul-opcode/+page.md

@@ -0,0 +1,61 @@
+---
+title: Huff, Yul, and Contract Opcode Disassembly
+---
+
+_Follow along with this video:_
+
+---
+
+Today, I'm excited to take you through the paces of creating a simple storage contract, which we're endearingly nicknaming our "one horse store" venture. Indeed, we're saddling up in our trusty Visual Studio Code (VS Code), and I'm going to share a trick that'll gallop your coding speed into the next-level: coding with an AI extension or AI buddy by your side.
+
+If you haven't yet, say a digital hello to GitHub Copilot—I've got it turned on and ready to code. AI tools like this are incredible time-savers, and I can't recommend them enough. While Microsoft's AI prowess is steering the ship at the moment, there are other AI-friendly extensions out there too. It's a playground of innovation, but let's not dwell on the tech politics for now.
+
+> "Embrace the AI extensions—not just for their speed, but for their ability to transform coding into a collaborative endeavor with the future."
+
+Let's get down to business and create a new project environment:
+
+```
+# Open up your terminal and run:mkdir one_horse_storecd one_horse_store# This creates your project directory and navigates you into it.
+```
+
+![](https://cdn.videotap.com/618/screenshots/4xk0alpmUeX5Q5g85Wng-134.4.png)
+
+Now, let's initiate our project by setting up Foundry, an awesome tool for smart contract development:
+
+```
+forge init
+```
+
+Ready? Hit the command and... Voilà! Your Foundry project is ready to roll.
+
+![](https://cdn.videotap.com/618/screenshots/lxxB0cs9eQo4oAnglwWL-158.4.png)With our scene all set up, it's time to script our first act. Dive into your README, clear the stage, and let's craft a basic, simple storage smart contract. It's easier than it sounds—I promise.
+
+If you're inclined to peek at the playbook, venture over to the GitHub repository associated with this walkthrough. You'll find our hero file `Horsestore.sol` under the `src/horse_store_v1` directory—there for the taking (or copying)!
+
+Here's where things get really interesting. As we explore the codebase, you'll stumble upon `horsestore_symbolic_t.sol`, which might seem like a riddle in code form. Don't stress about it now; it's part of our next adventure involving minimalistic symbolic execution or formal verification. We'll circle back to it in what I'd like to call the "Math Masters" section later on.
+
+If the code's looking alien, it's your cue to brush up on the Advanced Foundry or even the Basic Solidity skills. Everything we're doing here should resonate like a familiar chord.
+
+![](https://cdn.videotap.com/618/screenshots/vLrMPkPGuE8nuP01Nuon-182.4.png)
+
+Our smart contract? It's minimalism at its finest. We've got our `numberOfHorses` variable, an `update` function to change its value, and a `read` function to peek at it.
+
+Ready to see this baby run? Fire up your terminal and let's compile:
+
+```bash
+forge build
+```
+
+Success should grace your screen, and with it, confirmation of a job well done.
+
+![](https://cdn.videotap.com/618/screenshots/IRScPR5Kx7OL2J90pzyW-211.2.png)
+
+A quick command-shift-p brings up the command palette (handy tip: you can always google how to do this for your setup), and we're going to format our JSON output from the compiler and toggle the word wrap—it may not look pretty, but functionality is our first date, not aesthetics.
+
+![](https://cdn.videotap.com/618/screenshots/ge99ueN4MYHHbzplAWRz-220.8.png)
+
+Within the output—particularly the JSON—we find the ABI and bytecode, both critical for our smart contract to interact with the blockchain. They tell the tale of the deployed contract and its capabilities.
+
+And that's where we'll leave off for now. By following along, you've set the stage for more complex and thrilling coding adventures that lie ahead. Remember, coding doesn't have to be a solitary journey. With the right AI accomplices and a dash of collaborative spirit, you're well on your way to becoming a coding sorcerer in this electric era of smart contract development.
+
+---

courses/formal-verification/1-horse-store/10-stack-memory-and-storage/+page.md

@@ -0,0 +1,154 @@
+---
+title: EVM A Stack Machine Memory & Storage
+---
+
+---
+
+# Understanding Memory and Storage in Code: Making Sense of Where Data Goes
+
+Hey there, fellow code enthusiasts! Today, we're diving into the captivating world of data handling. Specifically, we're talking about the difference between memory and storage when you're whipping up some code magic 🧙‍♂️.
+
+## A Pancake Stack of Operations: Meet The Stack
+
+Before we talk memory and storage, let's get the basics down pat. Imagine a stack of pancakes—delicious, right? But in our case, it's a stack where our code does its cool tricks, like adding or subtracting values. Every time we want to perform an operation, we're piling it onto the stack, or pulling it off, one syrupy piece at a time.
+
+## Memory: The Temporary Art Gallery
+
+Now, let's chat about memory. Unlike the orderly stack, memory is the free-spirit of data storage. It's like an art gallery where you can hang variables all willy-nilly on any wall you fancy. Do your thing—add, change, and remove them as you please.
+
+But here's the catch—once your code's done running, everything in memory vanishes. _Poof!_ It's a clean slate the next time around.
+
+## Storage: The Library of Data Persistence
+
+Moving on to storage; think of it as a gigantic library where once the data is shelved—it stays put. Whether your program is running, paused, or done for the day, that data will stick around for as long as you need it. Archiving and retrieving, all handled with impeccable reliability.
+
+But here's the twist: interacting with storage is like ordering a luxury item—pricey! In the world of code, this means using way more computational resources.
+
+## OpCode Economics: Memory vs. Storage Costs
+
+Now, if we talk cost in opcode land, `S store` (saving to storage) demands a hefty price compared to `M store` (saving to memory). Think of it like a fine dining experience vs. a quick bite. You know which one's gonna hit your wallet harder.
+
+```js
+// Solidity example illustrating storage cost
+uint256 public storageCostly;
+function saveToStorage(uint256 newValue) public {storageCostly = newValue;
+// This is where things get expensive!
+}
+```
+
+Memory is like grabbing a quick burger, with a minimal fee of three units, while storage is like a five-course meal, starting at a steep hundred units. So whenever possible, try to keep things light and use memory. But remember, for data that needs to stick around, storage is your go-to.
+
+## The Bottom Line: Where Should Your Data Live?
+
+In summary, your data's home can be in the stack, memory, or storage. Each has its perks and quirks. Most of your operations will hang out in the stack. For temporary data shenanigans, hit up memory. And for the long-term stuff? Storage is your data's forever home.
+
+So keep these insights in your coder's toolkit:
+
+- Use the stack for quick calculations and operations.
+- Stick fleeting data in memory for a speedy yet temporary hold.
+- Leverage storage for persistent data that outlives your program's execution, but brace yourself for the higher cost.
+
+![screenshot](https://cdn.videotap.com/618/screenshots/sUIjunRhG763yEG9t2r6-96.46.png)
+
+As you dive back into crafting code, armed with this fresh knowledge, take a moment to appreciate the sophistication behind these data handling concepts. They may seem straightforward, but mastering their use is what elevates good code to great code.
+
+And, hey, wasn't that as satisfying as a perfectly stacked pile of pancakes? Keep these tips in mind, and you'll be flipping code breakfasts like a champ.
+
+---
+
+And there you have it—a detailed breakdown of memory and storage in the world of coding. If you enjoyed this tech-flavored foray, stay tuned for more! Next time, we might even delve into optimizing our usage of these concepts to whip up some truly efficient code. Until then, happy coding, and remember: in the digital realm, where you put your data is just as important as what you put in it.
+
+## Diving Deeper into Memory Management
+
+Now that we've covered the basics of memory, storage and the stack, let's go a little deeper on memory specifically. As a reminder, memory is used for temporary storage during code execution. When the transaction completes, everything in memory is wiped clean.
+
+So when should you use memory over the other options? Here are some key pointers:
+
+### Use Memory for Intermediate Results
+
+If you need to store some interim values in the midst of calculations or operations, memory is perfect. No need to persist the data, so save your precious storage resources. Memory offers speedy, temporary scratch space.
+
+### Opt for Memory with Iterative Algorithms
+
+For algorithms that repeat or loop through a sequence, memory allows storing iteration-specific values without accumulation. This prevents variables from piling up and cluttering your storage.
+
+### Memory Minimizes External State Changes
+
+Using memory minimizes interactions with external state like storage, network calls, etc. This makes memory-intensive code easier to test, reason about, and reuse since it avoids side effects.
+
+### Beware Memory Leaks!
+
+However, memory isn't infinite. If you over-allocate without freeing unneeded memory, you can leak away all your available memory! Structure your code to free memory once you're done with it.
+
+## Choosing between Heap and Stack Memory
+
+There are two types of memory in many languages - heap and stack. What's the difference, and when should you use each one?
+
+### Stack Memory
+
+Stack memory is fast, limited, and managed automatically. Variables stored here are given space as your program executes line by line. Once the function where the variable was declared finishes running, _poof!_ - stack memory for that variable is freed up.
+
+**Use stack memory for:**
+
+- Local function variables
+- Primitive datatypes
+- Smaller data sizes
+
+### Heap Memory
+
+Unlike the stack, the heap is a big, open memory pool that lets you manually allocate and free blocks yourself. Heap allocation is flexible, allowing much more custom control.
+
+**Use heap memory for:**
+
+- Larger data objects
+- When data lifetimes are less predictable
+- Reference types like arrays
+
+### Stack vs Heap: Striking a Balance
+
+The stack is fast and automatic but limited, while the heap is flexible with more space. A balanced program uses both:
+
+- Stack for transient values
+- Heap for larger, long-lived allocations
+
+Getting this mix right and minimizing waste takes experience - but now you know where to start tinkering!
+
+## Advanced Memory Techniques for Optimized Code
+
+As you level up your coding skills, optimizing memory usage should be a top priority. Here are some advanced tactics to squeeze the most out of memory:
+
+### 1. Reset Instead of Recreate
+
+Instead of freeing memory then reallocating later, reuse existing allocations when possible:
+
+### 2. Use Pooling for Frequency Allocated Objects
+
+For objects you instantiate often, use an object pool to reuse existing ones instead of unnecessary allocations:
+
+### 3. Compact Data Structures
+
+Opt for compact data structures like arrays over fragment-prone linked lists when feasible. Defragmenting memory improves locality.
+
+### 4. Profile, Profile, Profile!
+
+Use memory profiling tools to pinpoint waste. Guide optimization efforts with real usage data, not guesses!
+
+Following these best practices separates the truly efficient coders from the rest. How memory-mazed can you make your next program? Game on!
+
+## Striking the Ideal Balance Across the Data Realms
+
+We've journeyed far in our tour from stack to storage, with plenty of memory marvels along the way. To recap, here is how to make the best use of each data handling domain:
+
+**The Stack:** Use for transient values and calculations operating on them. Keep it light.
+
+**Memory:** Perfect for temporary storage during execution. Use heuristics to allocate/free just enough.
+
+**Storage:** Ideal for persisting data across transactions. Balance performance vs. storage needs.
+
+While conceptually straightforward, excelling at data handling requires experience. But now you have a strong starting framework as you build up those coding callouses!
+
+The deeper your understanding goes, the more adept you become at striking the right balance, reducing waste, and crafting optimized software that sings. And there is beauty in efficiency!
+
+Keep pushing your coding skills and curiosity ever forward. Our strange yet delightful digital world always has more wonders to uncover, if you know where to look.
+
+Now go let your creativity flow - those bits aren't going to push themselves!

courses/formal-verification/1-horse-store/11-push-and-add-opcode/+page.md

@@ -0,0 +1,63 @@
+---
+title: PUSH1 and ADD Opcode Example
+---
+
+---
+
+# Understanding Opcodes: Diving into Stack Operations in Programming
+
+Opcodes—short for operation codes—are the cornerstone of programming, especially when it comes to the manipulation of stack memory and storage. In this blog post, we'll unravel how these vital components function, illustrate their role in computation, and demystify the processes they govern within your code.
+
+## The Vital Role of the Stack
+
+At the very heart of opcode mechanics lies the stack—an area of memory reserved for executing instructions and managing data flow. Think of it as a literal stack of items where you can only add (push) or remove (pull) items from the top. It's this last-in, first-out (LIFO) method that allows us to maintain order in the execution process: the last item pushed onto the stack is the first item we can access.
+
+Most opcode instructions involve two essential activities: pushing data onto the stack and then executing an operation on this data. For instance, take the `ADD` opcode, which does precisely what it hints at—it adds numbers together. But how does it achieve this feat?
+
+### The Push and Add Opcodes
+
+Here's a scenario that's as common in the assembly language as a `print()` function in Python:
+
+1. We have two values, denoted as `a` and `b`.
+2. `a` sits comfortably at the top of our stack, while `b` is right beneath it.
+3. We execute the `ADD` opcode.
+
+What `ADD` does is beautiful in its simplicity—it takes `a`, adds it to `b`, and returns the result to the top of the stack. So if you push the hexadecimal values `0x1` and `0x3` onto the stack, and then call `ADD`, it crunches those numbers to push `0x4` as the new top-value of the stack.
+
+```
+PUSH 0x1 (Stack now has 1)PUSH 0x3 (Stack now has 1, 3)ADD      (Stack now has 4)
+```
+
+Before we can add them together, we need to get these values onto the stack using the `PUSH` opcode. There's a selection of `PUSH` opcodes available to us, each allowing for a different size of data to be placed onto the stack. The `PUSH1` opcode, for example, pushes a single byte onto the stack.
+
+To further illustrate the process:
+
+```markdown
+- Call `PUSH1 0x1`. Now `1` sits atop our stack.- Call `PUSH1 0x3`. Our stack now has a `3` on top, and `1` just below it.- Execute `ADD`. Our stack now shows `4`, the sum of `3` and `1`.
+```
+
+Bear in mind we're always dealing with hexadecimal data—`0x` preceding our numbers is a constant reminder of this.
+
+![Stack diagram](https://cdn.videotap.com/618/screenshots/plLHpyaWjeDR0FtTmn3K-57.68.png)
+
+### Stacking Up with Push
+
+To dive a bit deeper, let's examine the mechanics behind the `PUSH` opcode. Using `PUSH0` will always result in a `0` being placed at the current top of the stack—handy when zeroing out is necessary.
+
+But say we execute `PUSH1 0x1`, and then `PUSH1 0x3`. We've now lined our stack with two values, primed and ready for manipulation.
+
+> "The beauty of opcodes lies in their ability to perform complex tasks through simple, stack-based operations."
+
+By pushing values onto the stack, we're essentially loading up our computational 'gun' with the 'bullets'—or data—that we'll soon fire through the barrel of our opcode instructions.
+
+![Stack diagram](https://cdn.videotap.com/618/screenshots/ULPWQN6OHzUvj8hLYZf2-166.25.png)
+
+## A Peek at Memory Operations
+
+Aside from toying with our stack values, certain opcodes take it a step further. They reach into the stack, pull out values, and store them in memory, or even storage. Ever heard of the `MSTORE` or `SSTORE` opcodes? These guys are prime examples of stack interaction that ends up affecting the memory and storage of your system.
+
+Stay tuned as we delve deeper into these commands and explore the intricacies of opcode operations in subsequent posts. Understanding these foundations is crucial for anyone looking to get a firm grasp on the nuts and bolts of low-level programming and smart contract development.
+
+By the end of your journey with opcodes, you'll not just comprehend how to use them but also appreciate their elegance and efficiency. So, whether you're a seasoned developer or someone just starting out, grasping the fundamentals of opcodes and their relationship with the stack can truly elevate your coding game.
+
+Remember, practice makes perfect. Get comfortable with these basics, experiment with `PUSH` and `ADD`, and before you know it, you'll be stacking up your programming skills to new heights!