diff --git a/Makefile b/Makefile index 650c784..26e8e57 100644 --- a/Makefile +++ b/Makefile @@ -446,6 +446,12 @@ $(UKM_WITH_CONTRACT_TESTING_OUTPUT_DIR)/%.run.executed.kore: \ mkdir -p $(UKM_WITH_CONTRACT_TESTING_OUTPUT_DIR) echo "<(<" > $@.in.tmp + echo "::address" >> $@.in.tmp + echo "<|>" >> $@.in.tmp + cat $(UKM_CONTRACTS_TESTING_INPUT_DIR)/address.rs >> $@.in.tmp + echo ">)>" >> $@.in.tmp + + echo "<(<" >> $@.in.tmp echo "::bytes_hooks" >> $@.in.tmp echo "<|>" >> $@.in.tmp cat $(UKM_CONTRACTS_TESTING_INPUT_DIR)/bytes_hooks.rs >> $@.in.tmp diff --git a/rust-semantics/helpers.md b/rust-semantics/helpers.md index 2a13b17..6ebdcb5 100644 --- a/rust-semantics/helpers.md +++ b/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 diff --git a/rust-semantics/test/configuration.md b/rust-semantics/test/configuration.md index 8c469cb..4698e4e 100644 --- a/rust-semantics/test/configuration.md +++ b/rust-semantics/test/configuration.md @@ -7,6 +7,7 @@ module RUST-EXECUTION-TEST-CONFIGURATION .List .Map + .List endmodule diff --git a/rust-semantics/test/execution.md b/rust-semantics/test/execution.md index 621248f..1ba26a6 100644 --- a/rust-semantics/test/execution.md +++ b/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 NVI:Int => NVI +Int 1 syntax KItem ::= wrappedK(K) - syntax Mockable rule mock(Mocked:Mockable, Result:K) => .K ... @@ -111,6 +112,18 @@ module RUST-EXECUTION-TEST (Mocked:Mockable => Result) ... Mocked |-> wrappedK(Result:K) ... [priority(10)] + + rule + listMock(Mocked:Mockable, Result:K) => .K ... + L:List => L ListItem(listMock(Mocked, Result)) + + rule + (Mocked:Mockable => Result) ... + + (ListItem(listMock(Mocked:Mockable, Result:K)) => .List) + ... + + [priority(9)] endmodule ``` diff --git a/tests/demos/erc_20_token.rs b/tests/demos/erc_20_token.rs index c1c2ea2..cd935ce 100644 --- a/tests/demos/erc_20_token.rs +++ b/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; - #[view(getName)] + // #[view(getName)] #[storage_mapper("name")] fn s_name(&self) -> SingleValueMapper; - #[view(getSymbol)] + // #[view(getSymbol)] #[storage_mapper("symbol")] fn s_symbol(&self) -> SingleValueMapper; - #[view(getBalances)] + // #[view(getBalances)] #[storage_mapper("balances")] fn s_balances(&self, address: &ManagedAddress) -> SingleValueMapper; - #[view(getAllowances)] + // #[view(getAllowances)] #[storage_mapper("allowances")] fn s_allowances(&self, account: &ManagedAddress, spender: &ManagedAddress) -> SingleValueMapper; diff --git a/tests/ukm-contracts/address.rs b/tests/ukm-contracts/address.rs new file mode 100644 index 0000000..47d0329 --- /dev/null +++ b/tests/ukm-contracts/address.rs @@ -0,0 +1,3 @@ +fn is_zero(address: u64) -> bool { + address == 0_u64 +} \ No newline at end of file diff --git a/tests/ukm-with-contract/erc_20_token.1.run b/tests/ukm-with-contract/erc_20_token.1.run new file mode 100644 index 0000000..a87b559 --- /dev/null +++ b/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 + + diff --git a/tests/ukm-with-contract/erc_20_token.rs b/tests/ukm-with-contract/erc_20_token.rs new file mode 100644 index 0000000..77c01ab --- /dev/null +++ b/tests/ukm-with-contract/erc_20_token.rs @@ -0,0 +1,160 @@ +// This contract is a translation of +// https://github.com/Pi-Squared-Inc/pi2-examples/blob/b63d0a78922874a486be8a0395a627425fb5a052/solidity/src/tokens/SomeToken.sol +// +// The main change is that the contract does not issue specific error objects +// (e.g. ERC20InsufficientBalance), it just calls `::helpers::require` with various +// (string) explanations. +// +// Also, the `totalSupply` endpoint is declared implicitely as a view for +// `s_total_supply`. + +#![no_std] + +#[allow(unused_imports)] +use ukm::*; + +/* ---------------------------------------------------------------------------- + +TODOs: + - Integers are all u64 at the moment. Implement u256 and modify appropriately; + - Reuse the implementation of ManagedBuffer for strings, and the annotations for + the contract trait identification, as well as views, storage mappers, update, and + inits; + - Support some sort of struct for implementing MessageResult within the UKM module. + We also have to figure out the contents of MessageResult. + +Observations: + - ManagedAddress was replaced by an integer to fit the behaviors of UKM; + +---------------------------------------------------------------------------- */ + +#[ukm::contract] +pub trait Erc20Token { + // #[view(totalSupply)] + #[storage_mapper("total_supply")] + fn s_total_supply(&self) -> ::single_value_mapper::SingleValueMapper; + + // #[view(getName)] + #[storage_mapper("name")] + fn s_name(&self) -> ::single_value_mapper::SingleValueMapper; + + // #[view(getSymbol)] + #[storage_mapper("symbol")] + fn s_symbol(&self) -> ::single_value_mapper::SingleValueMapper; + + // #[view(getBalances)] + #[storage_mapper("balances")] + fn s_balances(&self, address: u64) -> ::single_value_mapper::SingleValueMapper; + + // #[view(getAllowances)] + #[storage_mapper("balances")] + fn s_allowances(&self, account: u64, spender: u64) -> ::single_value_mapper::SingleValueMapper; + + #[event("Transfer")] + fn transfer_event(&self, #[indexed] from: u64, #[indexed] to: u64, value: u64); + + #[event("Approval")] + fn approval_event(&self, #[indexed] owner: u64, #[indexed] spender: u64, value: u64); + + + #[init] + fn init(&self, /*name: &ManagedBuffer, symbol: &ManagedBuffer, */init_supply: u64) { + // self.s_name().set_if_empty(name); + // self.s_symbol().set_if_empty(symbol); + self._mint(::ukm::Caller(), init_supply); + } + + #[upgrade] + fn upgrade(&self) {} + + #[view(decimals)] + fn decimals(&self) -> u8 { + 18 + } + + // #[view(name)] + // fn name(&self) -> ManagedBuffer { + // self.s_name().get() + // } + + // #[view(symbol)] + // fn symbol(&self) -> ManagedBuffer { + // self.s_symbol().get() + // } + + #[view(balanceOf)] + fn balance_of(&self, account: u64) -> u64 { + self.s_balances(account).get() + } + + #[endpoint(transfer)] + fn transfer(&self, to: u64, value: u64) -> bool { + let owner = ::ukm::Caller(); + self._transfer(&owner, to, &value); + true + } + + #[view(allowance)] + fn allowance(&self, owner: u64, spender: u64) -> u64 { + self.s_allowances(owner, spender).get() + } + + #[endpoint(approve)] + fn approve(&self, spender: u64, value: u64) -> bool { + let owner = ::ukm::Caller(); + self._approve(&owner, spender, value, true); + true + } + + #[endpoint(transferFrom)] + fn transfer_from(&self, from: u64, to: u64, value: u64) -> bool { + let spender = ::ukm::Caller(); + self._spend_allowance(from, &spender, value); + self._transfer(from, to, value); + true + } + + fn _transfer(&self, from: u64, to: u64, value: u64) { + ::helpers::require(!::address::is_zero(from), "Invalid sender"); + ::helpers::require(!::address::is_zero(to), "Invalid receiver"); + self._update(from, to, value); + self.transfer_event(from, to, value); + } + + fn _update(&self, from: u64, to: u64, value: u64) { + if ::address::is_zero(from) { + self.s_total_supply().set(self.s_total_supply().get() + value); + } else { + let from_balance = self.s_balances(from).get(); + ::helpers::require(value <= &from_balance, "Insufficient balance"); + self.s_balances(from).set(self.s_balances(from).get() - value); + }; + + if ::address::is_zero(to) { + self.s_total_supply().set(self.s_total_supply().get() - value); + } else { + self.s_balances(to).set(self.s_balances(to).get() + value); + } + } + + fn _mint(&self, account: u64, value: u64) { + ::helpers::require(!::address::is_zero(account), "Zero address"); + self._update(0_u64, account, value); + } + + fn _approve(&self, owner: u64, spender: u64, value: u64, emit_event: bool) { + ::helpers::require(!::address::is_zero(owner), "Invalid approver"); + ::helpers::require(!::address::is_zero(spender), "Invalid spender"); + self.s_allowances(owner, spender).set(value); + if emit_event { + self.approval_event(owner, spender, value); + } + } + + fn _spend_allowance(&self, owner: u64, spender: u64, value: u64) { + let current_allowance = self.allowance(owner, spender); + ::helpers::require(value <= ¤t_allowance, "Insuficient allowance"); + self._approve(owner, spender, &(current_allowance - value), false); + } + +} diff --git a/ukm-semantics/test/execution.md b/ukm-semantics/test/execution.md index 7b1c968..fef9839 100644 --- a/ukm-semantics/test/execution.md +++ b/ukm-semantics/test/execution.md @@ -8,6 +8,7 @@ module UKM-TEST-SYNTAX syntax ExecutionItem ::= "mock" "CallData" | "mock" "Caller" | "mock" UkmHook UkmHookResult + | "list_mock" UkmHook UkmHookResult | "call_contract" Int | "output_to_arg" | "push_status" @@ -43,6 +44,7 @@ module UKM-TEST-EXECUTION rule mock Hook:UkmHook Result:UkmHookResult => mock(Hook, Result) + rule list_mock Hook:UkmHook Result:UkmHookResult => listMock(Hook, Result) rule call_contract Account => ukmExecute(Account, 100)