From 9c117ed9470244363eda535bd8c34d01f684fbf5 Mon Sep 17 00:00:00 2001 From: djmorel <35698075+djmorel@users.noreply.github.com> Date: Fri, 3 Jun 2022 13:21:12 -0400 Subject: [PATCH 1/4] Began initial rework on GameDLC Updating GameDLC.md to provide better documentation for the functions included in the directory. --- labs/SAW/Game/DLC/GameDLC.md | 50 ++++++++++++++++++++++-------------- 1 file changed, 31 insertions(+), 19 deletions(-) diff --git a/labs/SAW/Game/DLC/GameDLC.md b/labs/SAW/Game/DLC/GameDLC.md index 0783f5a7..72e91594 100644 --- a/labs/SAW/Game/DLC/GameDLC.md +++ b/labs/SAW/Game/DLC/GameDLC.md @@ -2,36 +2,27 @@ 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/. +Below is a list of functions included in src/. -## levelUp(uint32_t level) -**Goal:** Determine how to set up and verify a very simple function in a SAW contract. +## `uint32_t levelUp(uint32_t level)` -**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) - - -## getDefaultLevel() -**Goal:** Determine how to handle global variables in a SAW contract. +**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 declare a fresh `uint32_t` variable 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) + +## `uint32_t initDefaultPlayer(player_t* player)` -## initDefaultPlayer(player_t* player) -**Goal:** Determine how to setup a struct variable in a SAW contract. +**Goal:** Set up a struct variable in a SAW contract. **Lessons Learned:** - How and when to use `alias_ty` @@ -46,6 +37,27 @@ 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 + + + + + + + +## 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` + + + + + ## checkStats(character_t* character) **Goal:** Determine how to use parameterized contracts to set preconditions and postconditions. From 3a6f48ce7cea2f3138c6020af553fcc2ecf73701 Mon Sep 17 00:00:00 2001 From: djmorel <35698075+djmorel@users.noreply.github.com> Date: Fri, 3 Jun 2022 13:57:15 -0400 Subject: [PATCH 2/4] Added all current functions from src/ & reorganized them accordingly in GameDLC.md --- labs/SAW/Game/DLC/GameDLC.md | 63 +++++++++++++++++------------------- 1 file changed, 30 insertions(+), 33 deletions(-) diff --git a/labs/SAW/Game/DLC/GameDLC.md b/labs/SAW/Game/DLC/GameDLC.md index 72e91594..233e44a3 100644 --- a/labs/SAW/Game/DLC/GameDLC.md +++ b/labs/SAW/Game/DLC/GameDLC.md @@ -15,21 +15,21 @@ Below is a list of functions included in src/. **Goal:** Set up a SAW contract to verify a simple function. **Lessons Learned:** -- How to declare a fresh `uint32_t` variable in a contract +- 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) ## `uint32_t initDefaultPlayer(player_t* player)` -**Goal:** Set up a struct variable in a SAW contract. +**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` @@ -37,25 +37,10 @@ Below is a list of functions included in src/. - Compiling clang with the `-g` flag provides debug symbols, so you can reference fields names rather than just indices +// TODO: Update this section +## `uint32_t initDefaultSprite(character_t* character, sprite_t* sprite)` - - - - - - -## 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` - - - +**Goal:** Set up a struct ## checkStats(character_t* character) @@ -91,15 +76,31 @@ Below is a list of functions included in src/. - Goes back to the caller vs callee tradeoffs mentioned in `checkStats` **Additional Notes** +// TODO: Expand & discuss background with SAWscripts ## selfDamage(player_t* player) **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. -## resetInventoryItems(inventory_t* inventory) -**Goal:** To show the problems SAW faces when verifying structs with pointer fields. +## quickBattle(player_t* player, character_t* opponent) +**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) @@ -117,13 +118,9 @@ Below is a list of functions included in src/. - 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. +// TODO: Reevaluate position based on work done with initDefaultSprite() +## resetInventoryItems(inventory_t* inventory) +**Goal:** To show the problems SAW faces when verifying structs with pointer fields. **Lessons Learned:** -- 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 - +- Consider rewriting the source code to avoid unallocated pointers as it makes SAW happy and reduces assumptions code makes (improves security) From 1d751eb1b12648e66ed1c485c33536543ed34834 Mon Sep 17 00:00:00 2001 From: djmorel <35698075+djmorel@users.noreply.github.com> Date: Fri, 3 Jun 2022 14:13:34 -0400 Subject: [PATCH 3/4] Simplified function section naming convention & style --- labs/SAW/Game/DLC/GameDLC.md | 34 +++++++++++++++++++++------------- 1 file changed, 21 insertions(+), 13 deletions(-) diff --git a/labs/SAW/Game/DLC/GameDLC.md b/labs/SAW/Game/DLC/GameDLC.md index 233e44a3..394eb364 100644 --- a/labs/SAW/Game/DLC/GameDLC.md +++ b/labs/SAW/Game/DLC/GameDLC.md @@ -6,12 +6,13 @@ This directory contains additional Game functions and SAW contracts for you to r - `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 src/. -## `uint32_t levelUp(uint32_t level)` +## `levelUp()` **Goal:** Set up a SAW contract to verify a simple function. **Lessons Learned:** @@ -20,8 +21,7 @@ Below is a list of functions included in src/. - How to pass variables defined in the SAW contract to a Cryptol function (curly braces) -## `uint32_t initDefaultPlayer(player_t* player)` - +## `initDefaultPlayer()` **Goal:** Represent and initialize C structs in a SAW contract. **Lessons Learned:** @@ -37,13 +37,15 @@ Below is a list of functions included in src/. - Compiling clang with the `-g` flag provides debug symbols, so you can reference fields names rather than just indices +## `initDefaultSprite()` // TODO: Update this section -## `uint32_t initDefaultSprite(character_t* character, sprite_t* sprite)` **Goal:** Set up a struct +**Lessons Learned:** + -## checkStats(character_t* character) +## `checkStats()` **Goal:** Determine how to use parameterized contracts to set preconditions and postconditions. **Lessons Learned:** @@ -57,7 +59,7 @@ Below is a list of functions included in src/. - 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. @@ -66,7 +68,7 @@ Below is a list of functions included in src/. - 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:** @@ -76,12 +78,15 @@ Below is a list of functions included in src/. - Goes back to the caller vs callee tradeoffs mentioned in `checkStats` **Additional Notes** +## `selfDamage()` // TODO: Expand & discuss background with SAWscripts -## selfDamage(player_t* player) + **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:** + -## quickBattle(player_t* player, character_t* opponent) +## `quickBattle()` **Goal:** To show how to pass overrides (lemmas) to a Unit test. **Lessons Learned:** @@ -92,7 +97,7 @@ Below is a list of functions included in src/. - Explains why the `> 0` preconditions exist -## getDefaultLevel() +## `getDefaultLevel()` **Goal:** Determine how to handle global variables in a SAW contract. **Lessons Learned:** @@ -103,11 +108,13 @@ Below is a list of functions included in src/. - 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:** @@ -118,8 +125,9 @@ Below is a list of functions included in src/. - Repointing a pointer to a SAW variable (`screen_post`) in order to use that variable for postconditions +## `resetInventoryItems()` // TODO: Reevaluate position based on work done with initDefaultSprite() -## resetInventoryItems(inventory_t* inventory) + **Goal:** To show the problems SAW faces when verifying structs with pointer fields. **Lessons Learned:** From 9a1aac4948e62db6bcb4b752ba2fef5714d31ac6 Mon Sep 17 00:00:00 2001 From: djmorel <35698075+djmorel@users.noreply.github.com> Date: Fri, 3 Jun 2022 15:48:23 -0400 Subject: [PATCH 4/4] Added initial initDefaultSprite() documentation --- labs/SAW/Game/DLC/GameDLC.md | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/labs/SAW/Game/DLC/GameDLC.md b/labs/SAW/Game/DLC/GameDLC.md index 394eb364..9536b83b 100644 --- a/labs/SAW/Game/DLC/GameDLC.md +++ b/labs/SAW/Game/DLC/GameDLC.md @@ -38,11 +38,18 @@ Below is a list of functions included in src/. ## `initDefaultSprite()` -// TODO: Update this section - -**Goal:** Set up a struct +**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()`