Skip to content

Draft: GameDLC Improvements #205

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
djmorel wants to merge 4 commits into
base: master
Choose a base branch
from
Draft

Draft: GameDLC Improvements #205

Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
9c117ed
Began initial rework on GameDLC
djmorel Jun 3, 2022
3a6f48c
Added all current functions from src/ & reorganized them accordingly …
djmorel Jun 3, 2022
1d751eb
Simplified function section naming convention & style
djmorel Jun 3, 2022
9a1aac4
Added initial initDefaultSprite() documentation
djmorel Jun 3, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
100 changes: 62 additions & 38 deletions labs/SAW/Game/DLC/GameDLC.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,51 +2,57 @@

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`
- How to assert postconditions using `points_to`
- 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:**
Expand All @@ -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.
Expand All @@ -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:**
Expand All @@ -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:**
Expand All @@ -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)