diff --git a/labs/SAW/Game/DLC/GameDLC.md b/labs/SAW/Game/DLC/GameDLC.md
index 0783f5a7..9536b83b 100644
--- a/labs/SAW/Game/DLC/GameDLC.md
+++ b/labs/SAW/Game/DLC/GameDLC.md
@@ -2,43 +2,34 @@
 
 This directory contains additional Game functions and SAW contracts for you to reference. You will notice:
 - `Makefile`: Provides the necessary steps to generate our bitcode and run our SAW Python scripts.
-- `src/`: Contains the source code we'll be analyzing
+- `src/`: Contains the source code we'll be analyzing.
 - `proof/`: Contains our Python scripts to run our SAW contracts.
 - `specs/`: Contains our Cryptol specs that our SAW contracts can call.
 
-# DLC Functions
-
-Below is a list of functions included in Game/.
 
-## levelUp(uint32_t level)
-**Goal:** Determine how to set up and verify a very simple function in a SAW contract.
+# DLC Functions
 
-**Lessons Learned**
-- How to declare a fresh variable in SAW
-- How to call a Cryptol function
-- How to pass SAW types to Cryptol function (curly braces)
+Below is a list of functions included in src/.
 
 
-## getDefaultLevel()
-**Goal:** Determine how to handle global variables in a SAW contract.
+## `levelUp()`
+**Goal:** Set up a SAW contract to verify a simple function.
 
 **Lessons Learned:**
-- How and when to use `global_initializer`
-  - When the source code already initializes the value and SAW should just use that value
-- How to declare a global variable in SAW (`global_var`)
-- How to set a global variable to an initialized value in a SAW contract (`points_to`)
-- When to pass no inputs to `execute_func`
+- How to use `fresh_var` to represent `uint32_t` variables in a contract
+- How to call a Cryptol function in a contract
+- How to pass variables defined in the SAW contract to a Cryptol function (curly braces)
 
 
-## initDefaultPlayer(player_t* player)
-**Goal:** Determine how to setup a struct variable in a SAW contract.
+## `initDefaultPlayer()`
+**Goal:** Represent and initialize C structs in a SAW contract.
 
 **Lessons Learned:**
-- How and when to use `alias_ty`
+- How to use `alias_ty` to represent structs in a contract
+- Understand that SAW only recognizes the base struct name (`player_t` vs `character_t`)
 - How and when to use `alloc`
   - Use `alloc` when you only consider the pointer
   - Use `ptr_to_fresh` when you care about the values being referenced (i.e. for pre/postconditions) and the pointer
-- SAW only recognizes the base struct name (`player_t` vs `character_t`)
 - Passing global variables/parameters/defines defined in SAW to contracts
   - Values copied from the source code's defines
   - Examples: `MAX_NAME_LENGTH`, `SUCCESS`
@@ -46,7 +37,22 @@ Below is a list of functions included in Game/.
 - Compiling clang with the `-g` flag provides debug symbols, so you can reference fields names rather than just indices
 
 
-## checkStats(character_t* character)
+## `initDefaultSprite()`
+**Goal:** Use SAW's explicit structs to represent C structs that have pointer fields.
+
+**Lessons Learned:**
+- How to use `struct` to combine SAW variables into a struct representation
+- How to represent struct pointers either through `alloc` or through `fresh_var` and `ptr_ty`
+- How to represent multidimensional arrays in contracts
+- How to use Cryptol tuples to represent C structs in `points_to` postconditions
+- How to use 3 double quotes `"""` to spread Cryptol behaviors across multiple lines
+
+**Additional Notes:**
+- Notice that the contract includes two ways to assert struct postconditions holistically
+  - Each option has its way to declare `character`
+
+
+## `checkStats()`
 **Goal:** Determine how to use parameterized contracts to set preconditions and postconditions.
 
 **Lessons Learned:**
@@ -60,7 +66,7 @@ Below is a list of functions included in Game/.
 - How to use contract parameters to assert two possible postconditions
 - How to represent multiple Unit Tests on the same contract with different input parameters
 
-**Additional Notes:**
+**Additional Notes:**  
 - Note that the `checkStats` function would be used in the Game library to check character stats every instance before such stats would be referenced/used for gameplay.
 - In terms of the example, `checkStats` provides gameplay balancing by limiting how well characters can perform.
 - Given this policy, all other functions included in the library assume that `checkStats` is called before them.
@@ -69,7 +75,7 @@ Below is a list of functions included in Game/.
 - Discuss the coding & security tradeoffs between checks made in callers vs callees
 
 
-## resolveAttack(character_t* target, uint32_t atk)
+## `resolveAttack()`
 **Goal:** Expand upon the lessons learned with `checkStats` to get a contract ready for overrides/lemmas.
 
 **Lessons Learned:**
@@ -79,22 +85,43 @@ Below is a list of functions included in Game/.
   - Goes back to the caller vs callee tradeoffs mentioned in `checkStats` **Additional Notes**
 
 
-## selfDamage(player_t* player)
+## `selfDamage()`
+// TODO: Expand & discuss background with SAWscripts
+
 **Goal:** To provide a case study where SAW should have complained about its memory disjoint assertion being violated. Note that SAW's Python API silently resolves this issue.
 
+**Lessons Learned:**
 
-## resetInventoryItems(inventory_t* inventory)
-**Goal:** To show the problems SAW faces when verifying structs with pointer fields.
+
+## `quickBattle()`
+**Goal:** To show how to pass overrides (lemmas) to a Unit test.
 
 **Lessons Learned:**
-- Consider rewriting the source code to avoid unallocated pointers as it makes SAW happy and reduces assumptions code makes (improves security)
+- Must pass preconditions that match the preconditions included in the passed overrides
+
+**Additional Notes:**
+- The function assumes that both the player and opponent have non-zero HP values, otherwise there wouldn't be a battle!
+  - Explains why the `> 0` preconditions exist
+
+
+## `getDefaultLevel()`
+**Goal:** Determine how to handle global variables in a SAW contract.
+
+**Lessons Learned:**
+- How and when to use `global_initializer`
+  - When the source code already initializes the value and SAW should just use that value
+- How to declare a global variable in SAW (`global_var`)
+- How to set a global variable to an initialized value in a SAW contract (`points_to`)
+- When to pass no inputs to `execute_func`
 
 
-## initScreen(screen_t* screen, uint8_t assetID)
+## `initScreen()`
 **Goal:** To provide a case study where SAW should have complained about not knowing what nested defines resolve to. Note that SAW's Python API silently resolves this issue.
 
+**Lessons Learned:**
+
 
-## setScreenTile(screen_t* screen, uint32_t screenIdx, uint32_t tableIdx)
+## `setScreenTile()`
 **Goal:** Demonstrate how to initialize an extern global array.
 
 **Lessons Learned:**
@@ -105,13 +132,10 @@ Below is a list of functions included in Game/.
 - Repointing a pointer to a SAW variable (`screen_post`) in order to use that variable for postconditions
 
 
-## quickBattle(player_t* player, character_t* opponent)
-**Goal:** To show how to pass overrides (lemmas) to a Unit test.
-
-**Lessons Learned:**
-- Must pass preconditions that match the preconditions included in the passed overrides
+## `resetInventoryItems()`
+// TODO: Reevaluate position based on work done with initDefaultSprite()
 
-**Additional Notes:**
-- The function assumes that both the player and opponent have non-zero HP values, otherwise there wouldn't be a battle!
-  - Explains why the `> 0` preconditions exist
+**Goal:** To show the problems SAW faces when verifying structs with pointer fields.
 
+**Lessons Learned:**
+- Consider rewriting the source code to avoid unallocated pointers as it makes SAW happy and reduces assumptions code makes (improves security)