From 3b0a7fad4b3dcaec383ff741480942b669a772e4 Mon Sep 17 00:00:00 2001
From: Virgil <25692529+virgil-serbanuta@users.noreply.github.com>
Date: Fri, 20 Dec 2024 20:11:48 +0200
Subject: [PATCH] ERC20 transfer test (#53)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* ERC20 transfer test

Co-authored-by: Traian Florin Șerbănuță <traian.serbanuta@pi2.network>
Co-authored-by: Virgil Șerbănuță <virgil.serbanuta@pi2.network>

* Cleanup

---------

Co-authored-by: Stephen Skeirik <stephen.skeirik@runtimeverification.com>
Co-authored-by: Traian Florin Șerbănuță <traian.serbanuta@pi2.network>
---
 .../pykwasm/kdist/wasm-semantics/ulm-wasm.md  | 139 ++++--
 tests/ulm/erc20/erc20_test.sh                 | 423 +++++++++++++++++-
 2 files changed, 528 insertions(+), 34 deletions(-)

diff --git a/pykwasm/src/pykwasm/kdist/wasm-semantics/ulm-wasm.md b/pykwasm/src/pykwasm/kdist/wasm-semantics/ulm-wasm.md
index 97b69b875..9582f9cc6 100644
--- a/pykwasm/src/pykwasm/kdist/wasm-semantics/ulm-wasm.md
+++ b/pykwasm/src/pykwasm/kdist/wasm-semantics/ulm-wasm.md
@@ -469,7 +469,7 @@ Helpers: loading bytes from memory.
 
 ```remote
 
-    syntax InternalInstr ::= #memLoad ( offset: Int , length: Int )
+    syntax UlmExpr ::= #memLoad ( offset: Int , length: Int )
  // ---------------------------------------------------------------
 
     rule [memLoad-wrong-index]:
@@ -535,10 +535,16 @@ Helpers: loading bytes from memory.
             )
 
     rule [memLoad]:
-        <instrs> #memLoad(OFFSET, LENGTH) => #getBytesRange(
-            #let memInst(_MAX, _SIZE, DATA) = MEMS[ADDR]
-            #in DATA,
-            OFFSET, LENGTH)
+        <instrs>
+            #memLoad(OFFSET, LENGTH)
+            =>
+            ulmBytes(
+                #getBytesRange(
+                    #let memInst(_MAX, _SIZE, DATA) = MEMS[ADDR]
+                    #in DATA,
+                    OFFSET, LENGTH
+                )
+            )
             ...
         </instrs>
         <contractModIdx> MODIDX:Int </contractModIdx>
@@ -583,18 +589,21 @@ Handle the actual hook calls.
     rule
         <instrs>
             hostCall("env", "setOutput", [ i32 i32 .ValTypes ] -> [ .ValTypes ])
-            => #memLoad(OFFSET, LENGTH) ~> #setOutput
+            => #setOutput(#memLoad(OFFSET, LENGTH))
             ...
         </instrs>
         <locals>
             ListItem(<i32> OFFSET:Int) ListItem(<i32> LENGTH:Int)
         </locals>
 
-    syntax InternalInstr ::= "#setOutput"
+    syntax InternalInstr ::= #setOutput(UlmExpr) // [strict]
+
+    rule <instrs> (.K => HOLE) ~> #setOutput(HOLE:UlmExpr) ... </instrs> [heat]
+    rule <instrs> (HOLE:UlmVal => .K) ~> #setOutput(_ => HOLE) ... </instrs> [cool]
 
     rule
         <instrs>
-            BYTES:Bytes ~> #setOutput => .K
+            #setOutput(ulmBytes(BYTES:Bytes)) => .K
             ...
         </instrs>
         <output>
@@ -605,7 +614,7 @@ Handle the actual hook calls.
     rule
         <instrs>
             hostCall("env", "fail", [ i32 i32 .ValTypes ] -> [ .ValTypes ])
-            => #memLoad(OFFSET, LENGTH) ~> #fail
+            => #fail(#memLoad(OFFSET, LENGTH))
             ...
         </instrs>
         <locals>
@@ -613,11 +622,14 @@ Handle the actual hook calls.
         </locals>
 
 
-    syntax InternalInstr ::= "#fail"
+    syntax InternalInstr ::= #fail(UlmExpr) // [strict]
+
+    rule <instrs> (.K => HOLE) ~> #fail(HOLE:UlmExpr) ... </instrs> [heat]
+    rule <instrs> (HOLE:UlmVal => .K) ~> #fail(_ => HOLE) ... </instrs> [cool]
 
     rule
         <instrs>
-            BYTES:Bytes ~> #fail => #throwException(EVMC_FAILURE, Bytes2String(BYTES))
+            #fail(ulmBytes(BYTES:Bytes)) => #throwException(EVMC_FAILURE, Bytes2String(BYTES))
             ...
         </instrs>
 
@@ -625,18 +637,21 @@ Handle the actual hook calls.
     rule
         <instrs>
             hostCall("env", "keccakHash", [ i32 i32 i32 .ValTypes ] -> [ .ValTypes ])
-            => #memLoad(OFFSET, LENGTH) ~> #keccakHash(RESULT_OFFSET)
+            => #keccakHash(#memLoad(OFFSET, LENGTH), RESULT_OFFSET)
             ...
         </instrs>
         <locals>
             ListItem(<i32> OFFSET:Int) ListItem(<i32> LENGTH:Int) ListItem(<i32> RESULT_OFFSET:Int)
         </locals>
 
-    syntax InternalInstr ::= #keccakHash(Int)
+    syntax InternalInstr ::= #keccakHash(UlmExpr, Int) // [strict(1)]
+
+    rule <instrs> (.K => HOLE) ~> #keccakHash(HOLE:UlmExpr, _) ... </instrs> [heat]
+    rule <instrs> (HOLE:UlmVal => .K) ~> #keccakHash(_ => HOLE, _) ... </instrs> [cool]
 
     rule
         <instrs>
-            BYTES:Bytes ~> #keccakHash(RESULT_OFFSET:Int)
+            #keccakHash(ulmBytes(BYTES:Bytes), RESULT_OFFSET:Int)
             => #memStore(RESULT_OFFSET, Keccak256raw(BYTES))
             ...
         </instrs>
@@ -645,21 +660,24 @@ Handle the actual hook calls.
     rule
         <instrs>
             hostCall("env", "GetAccountStorage", [ i32 i32 .ValTypes ] -> [ .ValTypes ])
-            => #memLoad(IN_OFFSET, 32) ~> #getAccountStorage(RESULT_OFFSET)
+            => #getAccountStorage(#memLoadInt(IN_OFFSET), RESULT_OFFSET)
             ...
         </instrs>
         <locals>
             ListItem(<i32> IN_OFFSET:Int) ListItem(<i32> RESULT_OFFSET:Int)
         </locals>
 
-    syntax InternalInstr ::= #getAccountStorage(Int)
+    syntax InternalInstr ::= #getAccountStorage(UlmExpr, Int) // [strict(1)]
+
+    rule <instrs> (.K => HOLE) ~> #getAccountStorage(HOLE:UlmExpr, _) ... </instrs> [heat]
+    rule <instrs> (HOLE:UlmVal => .K) ~> #getAccountStorage(_ => HOLE, _) ... </instrs> [cool]
 
     rule
         <instrs>
-            BYTES:Bytes ~> #getAccountStorage(RESULT_OFFSET:Int)
+            #getAccountStorage(ulmInt(KEY:Int), RESULT_OFFSET:Int)
             => #memStore
                 ( RESULT_OFFSET
-                , Int2Bytes(32, GetAccountStorage(Bytes2Int(BYTES, LE, Unsigned)), LE)
+                , Int2Bytes(32, GetAccountStorage(KEY), LE)
                 )
             ...
         </instrs>
@@ -668,27 +686,98 @@ Handle the actual hook calls.
     rule
         <instrs>
             hostCall("env", "SetAccountStorage", [ i32 i32 .ValTypes ] -> [ .ValTypes ])
-            => #memLoad(KEY_OFFSET, 32) ~> #setAccountStorageValue(VALUE_OFFSET)
+            => #setAccountStorageValue(#memLoadInt(KEY_OFFSET), #memLoadInt(VALUE_OFFSET))
             ...
         </instrs>
         <locals>
             ListItem(<i32> KEY_OFFSET:Int) ListItem(<i32> VALUE_OFFSET:Int)
         </locals>
 
-    syntax InternalInstr  ::= #setAccountStorageValue(Int)
-                            | #setAccountStorage(Bytes)
+    syntax InternalInstr  ::= #setAccountStorageValue(UlmExpr, UlmExpr) // [seqstrict]
+
+    rule <instrs> (.K => HOLE) ~> #setAccountStorageValue(HOLE:UlmExpr, _) ... </instrs> [heat]
+    rule <instrs> (HOLE => .K) ~> #setAccountStorageValue(NV => HOLE, _) ... </instrs>
+        requires notBool isUlmVal(NV)
+        [cool]
+
+    rule <instrs> (.K => HOLE) ~> #setAccountStorageValue(_:UlmVal, HOLE:UlmExpr) ... </instrs> [heat]
+    rule <instrs> (HOLE => .K) ~> #setAccountStorageValue(_:UlmVal, NV => HOLE) ... </instrs>
+        requires notBool isUlmVal(NV)
+        [cool]
+
+    rule
+        <instrs>
+            #setAccountStorageValue(ulmInt(KEY:Int), ulmInt(VALUE:Int))
+            => SetAccountStorage(KEY, VALUE)
+            ...
+        </instrs>
+
+
+    rule
+        <instrs>
+            hostCall("env", "Caller", [ i32 .ValTypes ] -> [ .ValTypes ])
+            => #memStore(RESULT_OFFSET, Int2Bytes(20, Caller(), LE))
+            ...
+        </instrs>
+        <locals>
+            ListItem(<i32> RESULT_OFFSET:Int)
+        </locals>
+        requires 0 <=Int Caller() andBool Caller() <Int 1 <<Int 160
 
     rule
         <instrs>
-            KEY:Bytes ~> #setAccountStorageValue(VALUE_OFFSET:Int)
-            => #memLoad(VALUE_OFFSET, 32) ~> #setAccountStorage(KEY)
+            hostCall("env", "Log3", [ i32 i32 i32 i32 i32 .ValTypes ] -> [ .ValTypes ])
+            => #log3(#memLoadInt(DATA1_OFFSET), #memLoadInt(DATA2_OFFSET), #memLoadInt(DATA3_OFFSET), #memLoad(BYTES_OFFSET, BYTES_LENGTH))
             ...
         </instrs>
+        <locals>
+            ListItem(<i32> DATA1_OFFSET:Int)
+            ListItem(<i32> DATA2_OFFSET:Int)
+            ListItem(<i32> DATA3_OFFSET:Int)
+            ListItem(<i32> BYTES_OFFSET:Int)
+            ListItem(<i32> BYTES_LENGTH:Int)
+        </locals>
+
+    syntax UlmVal ::= ulmBytes(Bytes) | ulmInt(Int)
+    syntax KResult ::= UlmVal
+    syntax UlmExpr ::= UlmVal
+
+    syntax InternalInstr ::= #log3(UlmExpr, UlmExpr, UlmExpr, UlmExpr) // [seqstrict]
+
+    rule <instrs> (.K => HOLE) ~> #log3(HOLE:UlmExpr, _, _, _) ... </instrs> [heat]
+    rule <instrs> (HOLE => .K) ~> #log3(NV => HOLE, _, _, _) ... </instrs>
+        requires notBool isUlmVal(NV)
+        [cool]
+
+    rule <instrs> (.K => HOLE) ~> #log3(_:UlmVal, HOLE:UlmExpr, _, _) ... </instrs> [heat]
+    rule <instrs> (HOLE:UlmVal => .K) ~> #log3(_:UlmVal, NV => HOLE, _, _) ... </instrs>
+        requires notBool isUlmVal(NV)
+        [cool]
+
+    rule <instrs> (.K => HOLE) ~> #log3(_:UlmVal, _:UlmVal, HOLE:UlmExpr, _) ... </instrs> [heat]
+    rule <instrs> (HOLE:UlmVal => .K) ~> #log3(_:UlmVal, _:UlmVal, NV => HOLE, _) ... </instrs>
+        requires notBool isUlmVal(NV)
+        [cool]
+
+    rule <instrs> (.K => HOLE) ~> #log3(_:UlmVal, _:UlmVal, _:UlmVal, HOLE:UlmExpr) ... </instrs> [heat]
+    rule <instrs> (HOLE:UlmVal => .K) ~> #log3(_:UlmVal, _:UlmVal, _:UlmVal, NV => HOLE) ... </instrs>
+        requires notBool isUlmVal(NV)
+        [cool]
+
+    syntax UlmExpr ::= #memLoadInt(Int)
+    rule <instrs> #memLoadInt(OFFSET) => #toInt(#memLoad(OFFSET, 32)) ... </instrs>
+
+    syntax UlmExpr ::= #toInt(UlmExpr) // [strict]
+
+    rule <instrs> (.K => HOLE) ~> #toInt(HOLE:UlmExpr) ... </instrs> [heat]
+    rule <instrs> (HOLE:UlmVal => .K) ~> #toInt(_ => HOLE) ... </instrs> [cool]
+
+    rule <instrs> #toInt(ulmBytes(BYTES:Bytes)) => ulmInt(Bytes2Int(BYTES, LE, Unsigned)) ...</instrs>
 
     rule
         <instrs>
-            VALUE:Bytes ~> #setAccountStorage(KEY:Bytes)
-            => SetAccountStorage(Bytes2Int(KEY, LE, Unsigned), Bytes2Int(VALUE, LE, Unsigned))
+            #log3(ulmInt(DATA1:Int), ulmInt(DATA2:Int), ulmInt(DATA3:Int), ulmBytes(BYTES:Bytes)) =>
+            Log3(DATA1, DATA2, DATA3, BYTES)
             ...
         </instrs>
 
diff --git a/tests/ulm/erc20/erc20_test.sh b/tests/ulm/erc20/erc20_test.sh
index 674a2a706..9781127e0 100755
--- a/tests/ulm/erc20/erc20_test.sh
+++ b/tests/ulm/erc20/erc20_test.sh
@@ -56,6 +56,14 @@ function erc20_balanceOf {
   call http://localhost:8545 erc20 $contract /dev/stdin 0 balanceOf $account <<< $key
 }
 
+function erc20_allowance {
+  local key=$1
+  local contract=$2
+  local from_account=$3
+  local allowed_account=$4
+  call http://localhost:8545 erc20 $contract /dev/stdin 0 allowance $from_account $allowed_account <<< $key
+}
+
 function erc20_mint {
   local key=$1
   local contract=$2
@@ -64,91 +72,488 @@ function erc20_mint {
   call http://localhost:8545 erc20 $contract /dev/stdin 0 mint $account $amount <<< $key
 }
 
+function erc20_transfer {
+  local key=$1
+  local contract=$2
+  local account=$3
+  local amount=$4
+  call http://localhost:8545 erc20 $contract /dev/stdin 0 transfer $account $amount <<< $key
+}
+
+function erc20_approve {
+  local key=$1
+  local contract=$2
+  local account=$3
+  local amount=$4
+  call http://localhost:8545 erc20 $contract /dev/stdin 0 approve $account $amount <<< $key
+}
+
+function erc20_transfer_from {
+  local key=$1
+  local contract=$2
+  local from_account=$3
+  local to_account=$4
+  local amount=$5
+  call http://localhost:8545 erc20 $contract /dev/stdin 0 transferFrom $from_account $to_account $amount <<< $key
+}
+
 function test_decimals {
-  echo "Decimals test"
+  echo -n "Decimals test "
 
   # generate some accounts
   account1=($(mkacct))
   a1=${account1[0]}
   k1=${account1[1]}
-  echo "Account 1. address: $a1; key: $k1"
+  echo -n "."
 
   # fund accounts
   fund /dev/stdin <<< $k1
+  echo -n "."
 
   # deploy contract
   contract=$(erc20_deploy $k1)
-  echo "Contract deployed. Contract address: $contract"
+  echo -n "."
 
   decimals=$(erc20_decimals $k1 $contract)
+  echo -n "."
   assert_eq "18" "$decimals" "Decimals"
+
+  echo -e " ${GREEN}passed${NC}"
 }
 
 function test_mint {
-  echo "Mint test"
+  echo -n "Mint test "
 
   # generate some accounts
   account1=($(mkacct))
   a1=${account1[0]}
   k1=${account1[1]}
-  echo "Account 1. address: $a1; key: $k1"
+  echo -n "."
 
   account2=($(mkacct))
   a2=${account2[0]}
   k2=${account2[1]}
-  echo "Account 2. address: $a2; key: $k2"
+  echo -n "."
 
   account3=($(mkacct))
   a3=${account3[0]}
   k3=${account3[1]}
-  echo "Account 3. address: $a3; key: $k3"
+  echo -n "."
 
   # fund accounts
   fund /dev/stdin <<< $k1
+  echo -n "."
   fund /dev/stdin <<< $k2
+  echo -n "."
   fund /dev/stdin <<< $k3
+  echo -n "."
 
   # deploy contract
   contract=$(erc20_deploy $k1)
-  echo "Contract deployed. Contract address: $contract"
+  echo -n "."
 
   balance2=$(erc20_balanceOf $k1 $contract $a2)
+  echo -n "."
   assert_eq "0" "$balance2" "Balance of Account 2"
 
   balance3=$(erc20_balanceOf $k1 $contract $a3)
+  echo -n "."
   assert_eq "0" "$balance3" "Balance of Account 3"
 
   # check total supply
   supply=$(erc20_totalSupply $k1 $contract)
+  echo -n "."
   assert_eq "0" "$supply" "Total Supply"
 
   erc20_mint $k1 $contract $a2 $(to_hex 1000)
+  echo -n "."
 
   balance2=$(erc20_balanceOf $k1 $contract $a2)
+  echo -n "."
   assert_eq "1000" "$balance2" "Balance of Account 2"
 
   balance3=$(erc20_balanceOf $k1 $contract $a3)
+  echo -n "."
   assert_eq "0" "$balance3" "Balance of Account 3"
 
   # check total supply
   supply=$(erc20_totalSupply $k1 $contract)
+  echo -n "."
   assert_eq "1000" "$supply" "Total Supply"
 
   erc20_mint $k1 $contract $a3 $(to_hex 2000)
+  echo -n "."
 
   balance2=$(erc20_balanceOf $k1 $contract $a2)
+  echo -n "."
   assert_eq "1000" "$balance2" "Balance of Account 2"
 
   balance3=$(erc20_balanceOf $k1 $contract $a3)
+  echo -n "."
   assert_eq "2000" "$balance3" "Balance of Account 3"
 
   # check total supply
   supply=$(erc20_totalSupply $k1 $contract)
+  echo -n "."
   assert_eq "3000" "$supply" "Total Supply"
+
+  echo -e " ${GREEN}passed${NC}"
 }
 
-test_decimals
+function test_transfer {
+  echo -n "Transfer test "
+
+  # generate some accounts
+  account1=($(mkacct))
+  a1=${account1[0]}
+  k1=${account1[1]}
+  echo -n "."
+
+  account2=($(mkacct))
+  a2=${account2[0]}
+  k2=${account2[1]}
+  echo -n "."
+
+  account3=($(mkacct))
+  a3=${account3[0]}
+  k3=${account3[1]}
+  echo -n "."
+
+  # fund accounts
+  fund /dev/stdin <<< $k1
+  echo -n "."
+  fund /dev/stdin <<< $k2
+  echo -n "."
+  fund /dev/stdin <<< $k3
+  echo -n "."
+
+  # deploy contract
+  contract=$(erc20_deploy $k1)
+  echo -n "."
+
+  balance2=$(erc20_balanceOf $k1 $contract $a2)
+  echo -n "."
+  assert_eq "0" "$balance2" "Balance of Account 2"
+
+  balance3=$(erc20_balanceOf $k1 $contract $a3)
+  echo -n "."
+  assert_eq "0" "$balance3" "Balance of Account 3"
+
+  # check total supply
+  supply=$(erc20_totalSupply $k1 $contract)
+  echo -n "."
+  assert_eq "0" "$supply" "Total Supply"
+
+  erc20_mint $k1 $contract $a2 $(to_hex 1000)
+  echo -n "."
+
+  balance2=$(erc20_balanceOf $k1 $contract $a2)
+  echo -n "."
+  assert_eq "1000" "$balance2" "Balance of Account 2"
+
+  balance3=$(erc20_balanceOf $k1 $contract $a3)
+  echo -n "."
+  assert_eq "0" "$balance3" "Balance of Account 3"
+
+  # check total supply
+  supply=$(erc20_totalSupply $k1 $contract)
+  echo -n "."
+  assert_eq "1000" "$supply" "Total Supply"
+
+  erc20_transfer $k2 $contract $a3 $(to_hex 200)
+  echo -n "."
+
+  balance2=$(erc20_balanceOf $k1 $contract $a2)
+  echo -n "."
+  assert_eq "800" "$balance2" "Balance of Account 2"
+
+  balance3=$(erc20_balanceOf $k1 $contract $a3)
+  echo -n "."
+  assert_eq "200" "$balance3" "Balance of Account 3"
+
+  # check total supply
+  supply=$(erc20_totalSupply $k1 $contract)
+  echo -n "."
+  assert_eq "1000" "$supply" "Total Supply"
+
+  echo -e " ${GREEN}passed${NC}"
+}
+
+function test_transfer_from {
+  echo -n "Transfer from test "
+
+  # generate some accounts
+  account1=($(mkacct))
+  a1=${account1[0]}
+  k1=${account1[1]}
+  echo -n "."
+
+  account2=($(mkacct))
+  a2=${account2[0]}
+  k2=${account2[1]}
+  echo -n "."
+
+  account3=($(mkacct))
+  a3=${account3[0]}
+  k3=${account3[1]}
+  echo -n "."
+
+  account4=($(mkacct))
+  a4=${account4[0]}
+  k4=${account4[1]}
+  echo -n "."
+
+  # fund accounts
+  fund /dev/stdin <<< $k1
+  echo -n "."
+  fund /dev/stdin <<< $k2
+  echo -n "."
+  fund /dev/stdin <<< $k3
+  echo -n "."
+  fund /dev/stdin <<< $k4
+  echo -n "."
+
+  # deploy contract
+  contract=$(erc20_deploy $k1)
+  echo -n "."
+
+  # ***** Check initial state
+
+  balance=$(erc20_balanceOf $k1 $contract $a2)
+  echo -n "."
+  assert_eq "0" "$balance" "Balance of Account 2"
+
+  balance=$(erc20_balanceOf $k1 $contract $a3)
+  echo -n "."
+  assert_eq "0" "$balance" "Balance of Account 3"
+
+  balance=$(erc20_balanceOf $k1 $contract $a4)
+  echo -n "."
+  assert_eq "0" "$balance" "Balance of Account 4"
+
+  supply=$(erc20_totalSupply $k1 $contract)
+  echo -n "."
+  assert_eq "0" "$supply" "Total Supply"
+
+  allowance=$(erc20_allowance $k1 $contract $a2 $a3)
+  echo -n "."
+  assert_eq "0" "$allowance" "Allowance from Account 2 to Account 3"
+
+  allowance=$(erc20_allowance $k1 $contract $a2 $a4)
+  echo -n "."
+  assert_eq "0" "$allowance" "Allowance from Account 2 to Account 4"
+
+  allowance=$(erc20_allowance $k1 $contract $a3 $a2)
+  echo -n "."
+  assert_eq "0" "$allowance" "Allowance from Account 3 to Account 2"
+
+  allowance=$(erc20_allowance $k1 $contract $a3 $a4)
+  echo -n "."
+  assert_eq "0" "$allowance" "Allowance from Account 3 to Account 4"
+
+  allowance=$(erc20_allowance $k1 $contract $a4 $a2)
+  echo -n "."
+  assert_eq "0" "$allowance" "Allowance from Account 4 to Account 2"
+
+  allowance=$(erc20_allowance $k1 $contract $a4 $a3)
+  echo -n "."
+  assert_eq "0" "$allowance" "Allowance from Account 4 to Account 3"
+
+  # ***** Mint tokens
+
+  erc20_mint $k1 $contract $a2 $(to_hex 1000)
+  echo -n "."
+
+  # ***** Check state after mint
+
+  balance=$(erc20_balanceOf $k1 $contract $a2)
+  echo -n "."
+  assert_eq "1000" "$balance" "Balance of Account 2"
+
+  balance=$(erc20_balanceOf $k1 $contract $a3)
+  echo -n "."
+  assert_eq "0" "$balance" "Balance of Account 3"
+
+  balance=$(erc20_balanceOf $k1 $contract $a4)
+  echo -n "."
+  assert_eq "0" "$balance" "Balance of Account 4"
+
+  supply=$(erc20_totalSupply $k1 $contract)
+  echo -n "."
+  assert_eq "1000" "$supply" "Total Supply"
+
+  allowance=$(erc20_allowance $k1 $contract $a2 $a3)
+  echo -n "."
+  assert_eq "0" "$allowance" "Allowance from Account 2 to Account 3"
+
+  allowance=$(erc20_allowance $k1 $contract $a2 $a4)
+  echo -n "."
+  assert_eq "0" "$allowance" "Allowance from Account 2 to Account 4"
+
+  allowance=$(erc20_allowance $k1 $contract $a3 $a2)
+  echo -n "."
+  assert_eq "0" "$allowance" "Allowance from Account 3 to Account 2"
+
+  allowance=$(erc20_allowance $k1 $contract $a3 $a4)
+  echo -n "."
+  assert_eq "0" "$allowance" "Allowance from Account 3 to Account 4"
+
+  allowance=$(erc20_allowance $k1 $contract $a4 $a2)
+  echo -n "."
+  assert_eq "0" "$allowance" "Allowance from Account 4 to Account 2"
+
+  allowance=$(erc20_allowance $k1 $contract $a4 $a3)
+  echo -n "."
+  assert_eq "0" "$allowance" "Allowance from Account 4 to Account 3"
+
+  # ***** Account 2 approves Account 3 to transfer 300 tokens
+
+  erc20_approve $k2 $contract $a3 $(to_hex 300)
+  echo -n "."
+
+  # ***** Check state after approve
+
+  balance=$(erc20_balanceOf $k1 $contract $a2)
+  echo -n "."
+  assert_eq "1000" "$balance" "Balance of Account 2"
+
+  balance=$(erc20_balanceOf $k1 $contract $a3)
+  echo -n "."
+  assert_eq "0" "$balance" "Balance of Account 3"
 
+  balance=$(erc20_balanceOf $k1 $contract $a4)
+  echo -n "."
+  assert_eq "0" "$balance" "Balance of Account 4"
+
+  supply=$(erc20_totalSupply $k1 $contract)
+  echo -n "."
+  assert_eq "1000" "$supply" "Total Supply"
+
+  allowance=$(erc20_allowance $k1 $contract $a2 $a3)
+  echo -n "."
+  assert_eq "300" "$allowance" "Allowance from Account 2 to Account 3"
+
+  allowance=$(erc20_allowance $k1 $contract $a2 $a4)
+  echo -n "."
+  assert_eq "0" "$allowance" "Allowance from Account 2 to Account 4"
+
+  allowance=$(erc20_allowance $k1 $contract $a3 $a2)
+  echo -n "."
+  assert_eq "0" "$allowance" "Allowance from Account 3 to Account 2"
+
+  allowance=$(erc20_allowance $k1 $contract $a3 $a4)
+  echo -n "."
+  assert_eq "0" "$allowance" "Allowance from Account 3 to Account 4"
+
+  allowance=$(erc20_allowance $k1 $contract $a4 $a2)
+  echo -n "."
+  assert_eq "0" "$allowance" "Allowance from Account 4 to Account 2"
+
+  allowance=$(erc20_allowance $k1 $contract $a4 $a3)
+  echo -n "."
+  assert_eq "0" "$allowance" "Allowance from Account 4 to Account 3"
+
+  # ***** Account 3 transfers 200 tokens from Account 2 to Account 4
+
+  erc20_transfer_from $k3 $contract $a2 $a4 $(to_hex 200)
+  echo -n "."
+
+  # ***** Check state after transfer
+
+  balance=$(erc20_balanceOf $k1 $contract $a2)
+  echo -n "."
+  assert_eq "800" "$balance" "Balance of Account 2"
+
+  balance=$(erc20_balanceOf $k1 $contract $a3)
+  echo -n "."
+  assert_eq "0" "$balance" "Balance of Account 3"
+
+  balance=$(erc20_balanceOf $k1 $contract $a4)
+  echo -n "."
+  assert_eq "200" "$balance" "Balance of Account 4"
+
+  supply=$(erc20_totalSupply $k1 $contract)
+  echo -n "."
+  assert_eq "1000" "$supply" "Total Supply"
+
+  allowance=$(erc20_allowance $k1 $contract $a2 $a3)
+  echo -n "."
+  assert_eq "100" "$allowance" "Allowance from Account 2 to Account 3"
+
+  allowance=$(erc20_allowance $k1 $contract $a2 $a4)
+  echo -n "."
+  assert_eq "0" "$allowance" "Allowance from Account 2 to Account 4"
+
+  allowance=$(erc20_allowance $k1 $contract $a3 $a2)
+  echo -n "."
+  assert_eq "0" "$allowance" "Allowance from Account 3 to Account 2"
+
+  allowance=$(erc20_allowance $k1 $contract $a3 $a4)
+  echo -n "."
+  assert_eq "0" "$allowance" "Allowance from Account 3 to Account 4"
+
+  allowance=$(erc20_allowance $k1 $contract $a4 $a2)
+  echo -n "."
+  assert_eq "0" "$allowance" "Allowance from Account 4 to Account 2"
+
+  allowance=$(erc20_allowance $k1 $contract $a4 $a3)
+  echo -n "."
+  assert_eq "0" "$allowance" "Allowance from Account 4 to Account 3"
+
+  # ***** Account 3 transfers 100 tokens from Account 2 to Account 3
+
+  erc20_transfer_from $k3 $contract $a2 $a3 $(to_hex 100)
+  echo -n "."
+
+  # ***** Check state after transfer
+
+  balance=$(erc20_balanceOf $k1 $contract $a2)
+  echo -n "."
+  assert_eq "700" "$balance" "Balance of Account 2"
+
+  balance=$(erc20_balanceOf $k1 $contract $a3)
+  echo -n "."
+  assert_eq "100" "$balance" "Balance of Account 3"
+
+  balance=$(erc20_balanceOf $k1 $contract $a4)
+  echo -n "."
+  assert_eq "200" "$balance" "Balance of Account 4"
+
+  supply=$(erc20_totalSupply $k1 $contract)
+  echo -n "."
+  assert_eq "1000" "$supply" "Total Supply"
+
+  allowance=$(erc20_allowance $k1 $contract $a2 $a3)
+  echo -n "."
+  assert_eq "0" "$allowance" "Allowance from Account 2 to Account 3"
+
+  allowance=$(erc20_allowance $k1 $contract $a2 $a4)
+  echo -n "."
+  assert_eq "0" "$allowance" "Allowance from Account 2 to Account 4"
+
+  allowance=$(erc20_allowance $k1 $contract $a3 $a2)
+  echo -n "."
+  assert_eq "0" "$allowance" "Allowance from Account 3 to Account 2"
+
+  allowance=$(erc20_allowance $k1 $contract $a3 $a4)
+  echo -n "."
+  assert_eq "0" "$allowance" "Allowance from Account 3 to Account 4"
+
+  allowance=$(erc20_allowance $k1 $contract $a4 $a2)
+  echo -n "."
+  assert_eq "0" "$allowance" "Allowance from Account 4 to Account 2"
+
+  allowance=$(erc20_allowance $k1 $contract $a4 $a3)
+  echo -n "."
+  assert_eq "0" "$allowance" "Allowance from Account 4 to Account 3"
+
+  echo -e " ${GREEN}passed${NC}"
+}
+
+
+test_decimals
 test_mint
+test_transfer
+test_transfer_from
 
 echo -e "${GREEN}All tests passed${NC}"