Merge pull request #1015 from informalsystems/th/examples-erc20

Update ERC20 example
informalsystems · Jul 7, 2023 · 451a70a · 451a70a
2 parents f1b674a + d3d3252
commit 451a70a
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 2 deletions.
diff --git a/examples/.scripts/run-example.sh b/examples/.scripts/run-example.sh
@@ -23,6 +23,8 @@ get_main () {
   local main=""
   if [[ "$file" == "classic/distributed/LamportMutex/LamportMutex.qnt" ]] ; then
     main="--main=LamportMutex_3_10"
+  elif [[ "$file" == "solidity/ERC20/erc20.qnt" ]] ; then
+    main="--main=erc20Tests"
   elif [[ "$file" == "solidity/SimplePonzi/simplePonzi.qnt" ]] ; then
     main="--main=simplePonziTest"
   elif [[ "$file" == "solidity/GradualPonzi/gradualPonzi.qnt" ]] ; then

diff --git a/examples/README.md b/examples/README.md
@@ -76,7 +76,7 @@ listed without any additional command line arguments.
 | [puzzles/river/river.qnt](./puzzles/river/river.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [puzzles/tictactoe/tictactoe.qnt](./puzzles/tictactoe/tictactoe.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [solidity/Coin/coin.qnt](./solidity/Coin/coin.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
-| [solidity/ERC20/erc20.qnt](./solidity/ERC20/erc20.qnt) | :white_check_mark: | :white_check_mark: | :x: | :x: |
+| [solidity/ERC20/erc20.qnt](./solidity/ERC20/erc20.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [solidity/GradualPonzi/gradualPonzi.qnt](./solidity/GradualPonzi/gradualPonzi.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :white_check_mark: |
 | [solidity/icse23-fig7/lottery.qnt](./solidity/icse23-fig7/lottery.qnt) | :white_check_mark: | :white_check_mark: | :white_check_mark: | :x: |
 | [solidity/SimpleAuction/SimpleAuctionNonComposable.qnt](./solidity/SimpleAuction/SimpleAuctionNonComposable.qnt) | :white_check_mark: | :white_check_mark: | :x: | :x: |

diff --git a/examples/solidity/ERC20/erc20.qnt b/examples/solidity/ERC20/erc20.qnt
@@ -98,7 +98,8 @@ module erc20 {
     // https://github.com/OpenZeppelin/openzeppelin-contracts/blob/ca822213f2275a14c26167bd387ac3522da67fe9/contracts/token/ERC20/ERC20.sol#L222
     pure def _transfer(state: Erc20State,
             fromAddr: Address, toAddr: Address, amount: Uint): Erc20Result = {
-        val fromBalance = state.balanceOf.get(fromAddr)
+        // FIXME(#693): type annotation below is a workaround, inferred type is too general
+        val fromBalance: int = state.balanceOf.get(fromAddr)
         val err = require(fromAddr != ZERO_ADDRESS, "ERC20: transfer from the zero address")
             .andRequire(toAddr != ZERO_ADDRESS, "ERC20: transfer to the zero address")
             .andRequire(fromBalance >= amount, "ERC20: transfer amount exceeds balance")