Erc20 test (#155)

Makefile

@@ -446,6 +446,12 @@ $(UKM_WITH_CONTRACT_TESTING_OUTPUT_DIR)/%.run.executed.kore: \
 	mkdir -p $(UKM_WITH_CONTRACT_TESTING_OUTPUT_DIR)
 
 	echo "<(<" > [email protected]
+	echo "::address" >> [email protected]
+	echo "<|>" >> [email protected]
+	cat $(UKM_CONTRACTS_TESTING_INPUT_DIR)/address.rs >> [email protected]
+	echo ">)>" >> [email protected]
+
+	echo "<(<" >> [email protected]
 	echo "::bytes_hooks" >> [email protected]
 	echo "<|>" >> [email protected]
 	cat $(UKM_CONTRACTS_TESTING_INPUT_DIR)/bytes_hooks.rs >> [email protected]

rust-semantics/helpers.md

@@ -36,11 +36,10 @@ module RUST-HELPERS
 
     syntax Bool ::= isSignedInt(Type)  [function, total]
     rule isSignedInt(_) => false [owise]
-    rule isSignedInt(u8) => true
-    rule isSignedInt(u16) => true
-    rule isSignedInt(u32) => true
-    rule isSignedInt(u64) => true
-    rule isSignedInt(u128) => true
+    rule isSignedInt(i8) => true
+    rule isSignedInt(i16) => true
+    rule isSignedInt(i32) => true
+    rule isSignedInt(i64) => true
     rule isSignedInt(&T => T)
 
     rule concatNonEmptyStatements(.NonEmptyStatements, S:NonEmptyStatements) => S

rust-semantics/test/configuration.md

@@ -7,6 +7,7 @@ module RUST-EXECUTION-TEST-CONFIGURATION
         <rust-test>
             <test-stack> .List </test-stack>
             <mocks> .Map </mocks>
+            <mock-list> .List </mock-list>
         </rust-test>
 endmodule
 

rust-semantics/test/execution.md

@@ -14,7 +14,9 @@ module RUST-EXECUTION-TEST-PARSING-SYNTAX
                             | "check_eq" Expression  [strict]
                             | "push" Expression [strict]
                             | "push_value" Expression [strict]
-    syntax KItem ::= mock(KItem, K)
+    syntax Mockable
+    syntax KItem  ::= mock(Mockable, K)
+                    | listMock(Mockable, K)
 endmodule
 
 module RUST-EXECUTION-TEST
@@ -101,7 +103,6 @@ module RUST-EXECUTION-TEST
         <next-value-id> NVI:Int => NVI +Int 1 </next-value-id>
 
     syntax KItem ::= wrappedK(K)
-    syntax Mockable
 
     rule
         <k> mock(Mocked:Mockable, Result:K) => .K ... </k>
@@ -111,6 +112,18 @@ module RUST-EXECUTION-TEST
         <k> (Mocked:Mockable => Result) ...</k>
         <mocks> Mocked |-> wrappedK(Result:K) ...</mocks>
         [priority(10)]
+
+    rule
+        <k> listMock(Mocked:Mockable, Result:K) => .K ... </k>
+        <mock-list> L:List => L ListItem(listMock(Mocked, Result)) </mock-list>
+
+    rule
+        <k> (Mocked:Mockable => Result) ...</k>
+        <mock-list>
+            (ListItem(listMock(Mocked:Mockable, Result:K)) => .List)
+            ...
+        </mock-list>
+        [priority(9)]
 endmodule
 
 ```

tests/demos/erc_20_token.rs

@@ -15,23 +15,23 @@ use multiversx_sc::imports::*;
 
 #[multiversx_sc::contract]
 pub trait Erc20Token {
-    #[view(totalSupply)]
+    // #[view(totalSupply)]
     #[storage_mapper("total_supply")]
     fn s_total_supply(&self) -> SingleValueMapper<BigUint>;
 
-    #[view(getName)]
+    // #[view(getName)]
     #[storage_mapper("name")]
     fn s_name(&self) -> SingleValueMapper<ManagedBuffer>;
 
-    #[view(getSymbol)]
+    // #[view(getSymbol)]
     #[storage_mapper("symbol")]
     fn s_symbol(&self) -> SingleValueMapper<ManagedBuffer>;
 
-    #[view(getBalances)]
+    // #[view(getBalances)]
     #[storage_mapper("balances")]
     fn s_balances(&self, address: &ManagedAddress) -> SingleValueMapper<BigUint>;
 
-    #[view(getAllowances)]
+    // #[view(getAllowances)]
     #[storage_mapper("allowances")]
     fn s_allowances(&self, account: &ManagedAddress, spender: &ManagedAddress) -> SingleValueMapper<BigUint>;
 

tests/ukm-contracts/address.rs

@@ -0,0 +1,3 @@
+fn is_zero(address: u64) -> bool {
+  address == 0_u64
+}

tests/ukm-with-contract/erc_20_token.1.run

@@ -0,0 +1,279 @@
+list_mock GetAccountStorageHook ( 7809087261546347641 ) ukmInt64Result(0);
+list_mock SetAccountStorageHook ( 7809087261546347641 , 10000 ) ukmNoResult();
+list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmInt64Result(0);
+list_mock SetAccountStorageHook ( 7162266444907899391 , 10000 ) ukmNoResult();
+list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmInt64Result(10000);
+list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmInt64Result(10000);
+list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmInt64Result(10000);
+list_mock SetAccountStorageHook ( 7162266444907899391 , 9900 ) ukmNoResult();
+list_mock GetAccountStorageHook ( 7162266444908917614 ) ukmInt64Result(0);
+list_mock SetAccountStorageHook ( 7162266444908917614 , 100 ) ukmNoResult();
+list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmInt64Result(9900);
+list_mock GetAccountStorageHook ( 7162266444908917614 ) ukmInt64Result(100);
+list_mock SetAccountStorageHook ( 8028228613167873919 , 200 ) ukmNoResult();
+list_mock GetAccountStorageHook ( 8028228613167873919 ) ukmInt64Result(200);
+list_mock SetAccountStorageHook ( 8028228613167873919 , 0 ) ukmNoResult();
+list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmInt64Result(9900);
+list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmInt64Result(9900);
+list_mock SetAccountStorageHook ( 7162266444907899391 , 9700 ) ukmNoResult();
+list_mock GetAccountStorageHook ( 7162266444908917614 ) ukmInt64Result(100);
+list_mock SetAccountStorageHook ( 7162266444908917614 , 300 ) ukmNoResult();
+list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmInt64Result(9700);
+list_mock GetAccountStorageHook ( 7162266444908917614 ) ukmInt64Result(300);
+
+call :: bytes_hooks :: empty;
+return_value_to_arg;
+push "#init(Uint64)";
+call :: bytes_hooks :: append_str;
+return_value_to_arg;
+push 10000_u64;
+call :: bytes_hooks :: append_u64;
+return_value;
+mock CallData;
+
+push_value 1010101_u64;
+mock Caller;
+
+call_contract 12345;
+return_value;
+check_eq ();
+
+push_status;
+check_eq 2;
+
+output_to_arg;
+call :: bytes_hooks :: length;
+return_value;
+
+check_eq 0_u32;
+
+
+
+
+call :: bytes_hooks :: empty;
+return_value_to_arg;
+push "balanceOf(Uint64)";
+call :: bytes_hooks :: append_str;
+return_value_to_arg;
+push 1010101_u64;
+call :: bytes_hooks :: append_u64;
+return_value;
+mock CallData;
+
+call_contract 12345;
+return_value;
+check_eq ();
+
+push_status;
+check_eq 2;
+
+output_to_arg;
+call :: test_helpers :: decode_single_u64;
+return_value;
+
+check_eq 10000_u64;
+
+
+
+call :: bytes_hooks :: empty;
+return_value_to_arg;
+push "transfer(Uint64,Uint64)";
+call :: bytes_hooks :: append_str;
+return_value_to_arg;
+push 2020202_u64;
+call :: bytes_hooks :: append_u64;
+return_value_to_arg;
+push 100_u64;
+call :: bytes_hooks :: append_u64;
+return_value;
+mock CallData;
+
+push_value 1010101_u64;
+mock Caller;
+
+call_contract 12345;
+return_value;
+check_eq ();
+
+push_status;
+check_eq 2;
+
+output_to_arg;
+call :: test_helpers :: decode_single_u64;
+return_value;
+
+check_eq 1_u64;
+
+
+
+call :: bytes_hooks :: empty;
+return_value_to_arg;
+push "balanceOf(Uint64)";
+call :: bytes_hooks :: append_str;
+return_value_to_arg;
+push 1010101_u64;
+call :: bytes_hooks :: append_u64;
+return_value;
+mock CallData;
+
+call_contract 12345;
+return_value;
+check_eq ();
+
+push_status;
+check_eq 2;
+
+output_to_arg;
+call :: test_helpers :: decode_single_u64;
+return_value;
+
+check_eq 9900_u64;
+
+
+
+
+call :: bytes_hooks :: empty;
+return_value_to_arg;
+push "balanceOf(Uint64)";
+call :: bytes_hooks :: append_str;
+return_value_to_arg;
+push 2020202_u64;
+call :: bytes_hooks :: append_u64;
+return_value;
+mock CallData;
+
+call_contract 12345;
+return_value;
+check_eq ();
+
+push_status;
+check_eq 2;
+
+output_to_arg;
+call :: test_helpers :: decode_single_u64;
+return_value;
+
+check_eq 100_u64;
+
+
+
+
+
+
+call :: bytes_hooks :: empty;
+return_value_to_arg;
+push "approve(Uint64,Uint64)";
+call :: bytes_hooks :: append_str;
+return_value_to_arg;
+push 3030303_u64;
+call :: bytes_hooks :: append_u64;
+return_value_to_arg;
+push 200_u64;
+call :: bytes_hooks :: append_u64;
+return_value;
+mock CallData;
+
+push_value 1010101_u64;
+mock Caller;
+
+call_contract 12345;
+return_value;
+check_eq ();
+
+push_status;
+check_eq 2;
+
+output_to_arg;
+call :: test_helpers :: decode_single_u64;
+return_value;
+
+check_eq 1_u64;
+
+
+
+call :: bytes_hooks :: empty;
+return_value_to_arg;
+push "transferFrom(Uint64,Uint64,Uint64)";
+call :: bytes_hooks :: append_str;
+return_value_to_arg;
+push 1010101_u64;
+call :: bytes_hooks :: append_u64;
+return_value_to_arg;
+push 2020202_u64;
+call :: bytes_hooks :: append_u64;
+return_value_to_arg;
+push 200_u64;
+call :: bytes_hooks :: append_u64;
+return_value;
+mock CallData;
+
+push_value 3030303_u64;
+mock Caller;
+
+call_contract 12345;
+return_value;
+check_eq ();
+
+push_status;
+check_eq 2;
+
+output_to_arg;
+call :: test_helpers :: decode_single_u64;
+return_value;
+
+check_eq 1_u64;
+
+
+
+
+
+call :: bytes_hooks :: empty;
+return_value_to_arg;
+push "balanceOf(Uint64)";
+call :: bytes_hooks :: append_str;
+return_value_to_arg;
+push 1010101_u64;
+call :: bytes_hooks :: append_u64;
+return_value;
+mock CallData;
+
+call_contract 12345;
+return_value;
+check_eq ();
+
+push_status;
+check_eq 2;
+
+output_to_arg;
+call :: test_helpers :: decode_single_u64;
+return_value;
+
+check_eq 9700_u64;
+
+
+
+
+call :: bytes_hooks :: empty;
+return_value_to_arg;
+push "balanceOf(Uint64)";
+call :: bytes_hooks :: append_str;
+return_value_to_arg;
+push 2020202_u64;
+call :: bytes_hooks :: append_u64;
+return_value;
+mock CallData;
+
+call_contract 12345;
+return_value;
+check_eq ();
+
+push_status;
+check_eq 2;
+
+output_to_arg;
+call :: test_helpers :: decode_single_u64;
+return_value;
+
+check_eq 300_u64
+
+