adding most of the pending chapters

courses/formal-verification/1-horse-store/26-huff-interfaces/+page.md

@@ -0,0 +1,37 @@
+---
+title: Huff - __FUNC_SIF & INterfaces
+---
+
+---
+
+# Understanding Function Dispatchers in Solidity and Viper
+
+Hello, fellow blockchain enthusiasts! If you've tinkered with writing smart contracts or if you're just curious about how they operate under the hood, you might have heard about something called a 'function dispatcher'. This little gem is central to the functionality of smart contracts and here's why.
+
+Whenever a smart contract receives a transaction or call data, the very first task it performs is a trip through the function dispatcher. This is not unique to Solidity – its cousin Viper does it too, and indeed, this is standard across our smart contracts. It's the dispatcher's job to figure out what function we intend to call and then, well, dispatch to that function. It's like the switchboard operator of the contract.
+
+Now, if you've got a keen eye for detail, you'll appreciate the importance of clean code. While we delve into writing our smart contracts, comments can get a bit overwhelming, making it difficult to sift through what's code and what's just a note to self.
+
+![Code cleanup](https://cdn.videotap.com/618/screenshots/fU2Wxa8rVkzcaweuNuJm-82.76.png)
+
+I like to keep my codebase lean for readability, so I'll usually sweep away most of the non-essential comments and align the jumps to make everything look nice and tidy. But hey, it's your code, and if you love comments, by all means, keep them coming! Remember, the goal is to maintain the code as readable and maintainable as you can.
+
+## Syntactic Sugar in Huff for Better Readability
+
+Moving into the sweet stuff, there's something about Huff that makes those function signatures a breeze to handle. Ever heard of `__FUNC_SIG`? This keyword in Huff does the heavy lifting for you, calculating those pesky function signatures behind the scenes.
+
+So if you're sick of manually setting up those selectors, here's a trick: define an interface at the top of your Huff code. Sketch out those functions just like you would in Solidity and let Huff work its magic to translate them into function selectors.
+
+## From Interface to Implementation: Compiling in Huff
+
+Let's take our newfound syntactic sweetness for a spin, shall we? By mimicking the interface definitions from Solidity into Huff, we open up a world of efficiency. And when we compile, it's the same robust code but without the manual slog.
+
+You might be wondering, why all the fuss with syntactic sugar and interfaces? It's simple, really. By using these techniques, we make our code neater, more readable, and let's face it, a whole lot cooler to write. It's taking the best practices from the Solidity world and applying them smartly in Huff to streamline our smart contract development process.
+
+And don't worry, when it's time to delve into the nitty-gritty of Solidity bytecode later on, you'll see the method to the madness. You'll get why a few extra opcodes actually matter and how they fit into this bigger picture of smart contract orchestration.
+
+So remember, whether you're a Solidity savant, a Viper virtuoso, or just starting on your blockchain journey, understanding the function dispatcher is key to mastering smart contract functionality.
+
+By stripping away the excess and employing a bit of coding finesse with tools like `__FUNC_SIG`, we not only make our lives easier, but we also pave the path for more maintainable, clear, and efficient contract code.
+
+So, go forth, optimize those contracts, and may your function dispatching be smoother than ever!

courses/formal-verification/1-horse-store/27-storage-refresher/+page.md

@@ -0,0 +1,46 @@
+---
+title: Storage Refresher
+---
+
+---
+
+## Understanding Function Dispatching
+
+So, picture this: we've got these two main functions, like launchpads ready for blastoff. They're our beacon, the destination our opcode has been eager to work with. Let's tackle `setNumberOfHorses` or as I like to call it, the horse-power update, first up on our coding playlist. Why this, you ask? Well, it's the whole storage shebang that makes it the prime candidate.
+
+### The Storage Saga—Array of Possibilities
+
+Now, hold up, let's take a sec for a quick refresher on _storage_. Think of it as this colossal array, an eternal vault that immortalizes the outcome of our transactions. Our beloved variables in Solidity contracts are mapped to storage slots that stick around for the long haul—they're there to stay. Everything from good ol' booleans to your cherished digits gets a cozy bytes32 structured home.
+
+![Mapping Magic and Hashing Hocus Pocus](https://cdn.videotap.com/618/screenshots/vf8rw9vA3Gg1oA7Gd6ik-53.67.png)
+
+Now, mappings, oh, they're a crafty bunch. They don't just claim any slot; instead, they've got this hash wizardry that stashes their values in slots based on the assortment of the array. Take my setup here: if my array's got dibs on slot two in storage, the opening act, aka the value in slot zero of said array, lands at `keccak256(slot, index)`. This sorcery ensures each bit of data finds its unique spot in the storage cosmos—no trespassers!
+
+### Constants and Memories—The Unstorageables
+
+Before I forget, let's clear the air—constants and memory variables, they don't set up camp in storage, no sir.
+
+## Upgrading Horsepower: `setNumberOfHorses`
+
+Alright, enough with the side quests; back to boosting those numbers of horses. To update our stable strength in storage, we gotta roll up our sleeves and:
+
+1. Assign a VIP storage slot
+2. Summon the `SSTORE` opcode to save the value
+
+Simple as that. We'll bookmark a spot in the eternal storage ledger for `numOfHorses`.
+
+Once we've carved out its place in the blockchain realm, we'll forever have `numOfHorses` safe and sound at its designated slot. How cool is that?
+
+### Testing the Code—Huff vs. Solidity Showdown
+
+Here’s where the rubber meets the road. Once we've coded our hearts out, it's test time. We'll pit our Huff masterpiece against the Solidity counterpart to see if they're two peas in a pod, doing the exact same magic. Spoiler alert: they will, and we’ll be doing victory laps before you know it.
+
+![Testing the Code—Huff vs. Solidity Showdown](https://cdn.videotap.com/618/screenshots/G7lCV1MCl8BcHIRSbW4N-126.5.png)
+
+### Closing In—A Huff Journey Nears Its End
+
+Guess what? We're zooming towards the finish line with our Huff codebase. Crafting `setNumberOfHorses` brings us just a heartbeat away from the grand finale. So let's power through and update those horses' stats, shall we?
+
+---
+
+Well, that's a wrap for now, code wranglers! Stay tuned for more smart contract escapades and remember—each line of code is a step closer to blockchain mastery. Happy coding!

courses/formal-verification/1-horse-store/28-sstore/+page.md

@@ -0,0 +1,88 @@
+---
+title: SSTORE
+---
+
+---
+
+# Demystifying the S STORE Opcode in Smart Contract Data Storage
+
+Hey everyone! Today we're diving into the interesting world of data storage in smart contracts, and specifically, we're going to focus on a mysterious little thing called the `S STORE` opcode. If you've dabbled in smart contract development or are simply curious about the intricacies of Ethereum's functionality, then you've come to the right place!
+
+## What is the S STORE Opcode?
+
+Alright, let's get straight to the point. The `S STORE` opcode is our go-to guy when we need to store data in a smart contract's storage. Think of it as a handyman whose job is to take your data and tuck it away securely in the storage unit. This opcode is all about action; it grabs the first two items from the stack, pops them right off, and voilà, they’re stored.
+
+The process is quite straightforward. The top of the stack holds a 32-byte key that represents a unique location in storage and directly below it lies the value you want to store. Essentially, it's about matching a 'where' with a 'what'—where you want to place your data and what that data actually is.
+
+## Understanding Stack Inputs and Outputs
+
+To better grasp how `S STORE` operates, think of a stack of plates. You take the top plate (your 32-byte key) and the one below it (your data value), and you put them in their respective places in the cupboard (that's your storage). Now, an interesting part about `S STORE` is that it doesn’t bother returning anything to the stack—no output. It's a one-way trip for those two values.
+
+## Storage Slots and Values
+
+Let's get practical for a moment. Imagine we're keeping track of something fun like the number of horses in a digital stable. Where do we store this piece of information? In slot one, two, three? In the world of bytes and binaries, these slots are distinct locations ready to keep your data safe and sound.
+
+```js
+uint256 numberOfHorses = 2;
+// Storing the number '2' in the predetermined storage slot for number of horses.
+```
+
+In order to actually store the number of horses, we first need to designate a storage slot to hold that value. This slot acts as a key that maps to the value we want to store. We could arbitrarily pick slot 1, slot 2 etc., but it's better practice to keep related data together in adjacent slots.
+
+For example, if we were also storing number of donkeys, number of cows, and number livestock in total, we may structure it like:
+
+```
+Slot 1: Number of horses (key: 0x01)
+Slot 2: Number of donkeys  (key: 0x02)
+Slot 3: Number of cows (key: 0x03)
+Slot 4: Total number of livestock (key: 0x04)
+```
+
+This keeps all the animal counts neatly organized in adjacent slots, with the total livestock count next in line at slot 4. The keys (0x01, 0x02 etc.) are unique identifiers that let us easily retrieve the corresponding values later.
+
+When it comes time to actually run the `SSTORE` opcode, it simply takes the slot key from the top of the stack, and the value to store from the next item down the stack, and handles the rest.
+
+## Retrieving Values Before Storing
+
+Hold your horses (pun intended)! Before we can store anything, we need the actual value to store. Usually, this value is part of what we call `call data`—data sent along with a function call to a smart contract. We need to fetch the value from this call data, determine the right storage slot, and then proceed with `S STORE`.
+
+> **Pro Tip:** Always make sure to retrieve the latest value from call data before attempting to store it.
+
+## Updating Stored Values
+
+What happens if we try to store a value in an already occupied slot? This is where things get a bit nuanced.
+
+If the slot contains a non-zero value and we store a non-zero value, it costs 20,000 gas to overwrite. However, if we store zero in a non-zero slot, it refunds 15,000 gas as a sort of "cleanup" operation. Additionally, if we store a non-zero value in a slot that's currently zero, it only costs 5,000 gas.
+
+These intricate gas mechanics incentivize efficient usage of storage by encouraging developers to reuse slots instead of continually expanding storage.
+
+Let's look at an example flow for updating the number of horses:
+
+```
+Current status:
+    Slot 1 (Horses key) = 5 (five horses initially)
+    1. User calls updateHorses(uint256 newNumHorses)
+    2. newNumHorses comes in from call data as 2
+    3. Contract checks slot 1, sees non-zero value (5)
+    4. Contract overwrites slot 1 with 2
+    5. 20,000 gas charged for writing non-zero (2) over non-zero (5)
+    6. Slot 1 now contains 2 horses
+```
+
+And that's the gist of updating stored values! By considering these gas stipulations, we can optimize our contracts to stay lean and mean.
+
+## Wrapping Up
+
+So that, my friends, is a basic rundown of the `S STORE` opcode. It's not as daunting as it seems at first glance, right? Remember that when you are programming smart contracts, handling data storage with care is crucial. The `S STORE` opcode is your silent partner in this endeavor—efficiently putting away those valuable bytes where they need to go.
+
+Now, before we part ways, a friendly reminder—using `S STORE` costs gas, so optimize your contract's storage patterns whenever possible to keep those gas fees in check. Efficiency is key in the blockchain realm, after all.
+
+I hope this explanation helps demystify data storage in smart contracts, and gives you a better understanding of how `S STORE` operates under the hood. Go forth and code with confidence, knowing that you've got another snippet of smart contract knowledge in your developer toolkit.
+
+And with that, I wish you happy coding! If you've got thoughts or questions, drop them in the comments. Keep exploring, and keep building those killer dApps!
+
+Stay tuned for more deep dives, and until next time, may your transactions always confirm swiftly, and your contracts be free of bugs!
+
+![screenshot](https://cdn.videotap.com/618/screenshots/IwQWS3EO6FEueC2NTmp8-85.03.png)
+
+Remember to always do your own research and happy developing!

courses/formal-verification/1-horse-store/29-free-storage-pointer/+page.md

@@ -0,0 +1,112 @@
+---
+title: Huff - FREE_STORAGE_POINTER
+---
+
+---
+
+## Maximizing Smart Contract Storage with Huff: The Simplified Approach to Storage Slots
+
+### Understanding Storage Slots
+
+Hey there, crypto enthusiasts and coders! Have you ever struggled with the logistics of assigning storage slots in smart contract development? Well, take a seat and let's talk shop. We're diving into the world of storage allocation and how using the Huff language can simplify our lives.
+
+When we're talking about smart contracts, particularly in blockchain environments, knowing where to store your data is crucial. Take, for example, a smart contract that manages a virtual stable of horses (I know, just go with it). We need to determine the number of horses and where to store that piece of data in our contract. Now, we could go old school and hard code it, setting our value at “0x80,” or wherever else we fancy—but is that our smartest move?
+
+### Enter Huff's Free Storage Pointer
+
+Fortunately, we've got Huff in our corner, which shakes things up a bit. Huff gives us the neat abstraction called `free storage pointer`. Imagine it as your friendly neighborhood counter, keeping tabs on available storage slots just for you.
+
+Here's a neat trick: If we start at the top of our code and declare a constant variable, let's name it `number_of_horses_storage_slot` and set it equal to `free storage pointer`. This little line of code assigns the `number_of_horses_storage_slot` to whichever slot is currently open.
+
+```huff
+#define constant NUMBER_OF_HORSES_STORAGE_SLOT free_storage_pointer()
+```
+
+And if we decide to add another slot, say `number_of_horses_storage_slot_two`, Huff is going to increment and assign this to the next slot in line, keeping everything organized and sequential.
+
+```huff
+#define constant NUMBER_OF_HORSES_STORAGE_SLOT_TWO free_storage_pointer()
+```
+
+This free storage pointer isn’t just handy; it’s crucial, keeping our data neatly stored in 32-byte slots and ensuring we’re not overwriting or losing track of our precious contract variables.
+
+> “Using Huff's free storage pointer abstracts away the manual tracking of our smart contract storage slots.”
+
+Now, you might still be tempted to hard code your slots. It's tempting, I get it. But let me tell you—embrace the Huff way. It will save you from future headaches and make maintaining your code that much easier.
+
+### Let's Get Practical
+
+So, in practice, what does this look like? Here's the down-low: when we're dealing with storage in Huff, and we say `number_of_horses_storage_slot`, it starts at slot zero. It's not in some random slot or way down the line at slot 576; it's right there at the starting gate at slot zero.
+
+![](https://cdn.videotap.com/618/screenshots/1teb0R4oDjCXsluR09DI-86.87.png)
+
+Anyone peeking at our smart contract will see that if they look at storage slot zero, they’ll find exactly how many horses are in our stable. It keeps things transparent and efficient. This is the same principle Solidity uses—first variable, first slot.
+
+```solidity
+uint256 number_of_horses; // In Solidity, this would be assigned to storage slot 0
+```
+
+The beauty of this system is that it aligns with how Solidity operates. Seeing our first variable, it knows what to do—straight to slot number zero.
+
+### Conclusion: The Huff Difference
+
+In wrapping up, what we've learned today is more than just how to use a storage slot—it’s about writing smarter, cleaner code with the tools that make our developer lives easier. Huff doesn't just give us a different way to code smart contracts; it gives us methodologies that align closely with the practices we already know and appreciate in languages like Solidity.
+
+So next time you’re about to hard code that storage slot, remember the power of Huff and its free storage pointer. Take advantage of the abstractions that make coding less of a chore and more of a breeze.
+
+Keep coding, keep learning, and let's make our storage slots the Huff way. Catch you on the blockchain!
+
+---
+
+I hope you found this deep dive into Huff’s storage pointers enlightening and practical. If you’re curious about more tips and tricks or want to further your understanding of smart contract development, leave a comment, and let's get the conversation going. Until next time, happy coding!
+
+### Additional Concepts to Explore
+
+While we covered the basics of Huff's free storage pointer, there are some additional nuances that are worth exploring further. Here are a few concepts that can help take your Huff storage slot skills to the next level:
+
+#### Packed Storage
+
+Huff provides a way to optimize storage usage even more through something called packed storage. This allows you to store multiple values in a single storage slot.
+
+For example:
+
+```huff
+#packed(uint128 number_of_horses;uint128 number_of_stables;) horses_data = free_storage_pointer()
+```
+
+This packs both the number of horses and stables into one slot instead of using two separate slots. Pretty nifty!
+
+#### Mappings
+
+Huff supports mappings which allow you to essentially create a lookup table for your data.
+
+Think of it like an address book that lets you access values by a "key". For example:
+
+```huff
+mapping(address => uint) public horse_balances;
+```
+
+This creates a mapping where you can lookup a horse balance by passing in the owner's wallet address. Very handy for certain use cases!
+
+#### Incrementing/Decrementing
+
+You can also increment or decrement slot values directly in Huff:
+
+```js
+horses_data++;
+// increments number of horses by 1
+horses_data--;
+// decrements number of horses by 1
+```
+
+This makes updating state variables a breeze.
+
+### Expanding Your Huff Horizons
+
+We've really just scratched the surface of what's possible with Huff storage. As you continue your blockchain journey, don't be afraid to experiment and push the boundaries of what you can build.
+
+The Huff team is also continuously improving and optimizing the language. Stay tuned for new features and updates that make writing gas-efficient smart contracts even simpler.
+
+In the famous words of Sarah Jessica Parker, "when it comes to Huff, there's always room for sequels!" Alright, maybe I took some creative liberty there. But the sentiment remains - there's so much more to uncover.
+
+Hope you enjoyed this introductory tour of Huff storage. Until next time, keep calm and code on!

courses/formal-verification/1-horse-store/30-accessing-constant-variables/+page.md

@@ -0,0 +1,5 @@
+---
+title: Huff - Accessing Constant Variables
+---
+
+---