diff --git a/compilation/prepare-rust-bundle.sh b/compilation/prepare-rust-bundle.sh index 3e696ec2..fb4dcc39 100755 --- a/compilation/prepare-rust-bundle.sh +++ b/compilation/prepare-rust-bundle.sh @@ -25,9 +25,9 @@ cat $ULM_CONTRACTS_TESTING_INPUT_DIR/bytes_hooks.rs >> $output_file echo ">)>" >> $output_file echo "<(<" >> $output_file -echo "::test_helpers" >> $output_file +echo "::debug" >> $output_file echo "<|>" >> $output_file -cat $ULM_CONTRACTS_TESTING_INPUT_DIR/test_helpers.rs >> $output_file +cat $ULM_CONTRACTS_TESTING_INPUT_DIR/debug.rs >> $output_file echo ">)>" >> $output_file echo "<(<" >> $output_file @@ -48,6 +48,12 @@ echo "<|>" >> $output_file cat $ULM_CONTRACTS_TESTING_INPUT_DIR/single_value_mapper.rs >> $output_file echo ">)>" >> $output_file +echo "<(<" >> $output_file +echo "::test_helpers" >> $output_file +echo "<|>" >> $output_file +cat $ULM_CONTRACTS_TESTING_INPUT_DIR/test_helpers.rs >> $output_file +echo ">)>" >> $output_file + echo "<(<" >> $output_file echo "::ulm" >> $output_file echo "<|>" >> $output_file diff --git a/tests/ulm-contracts/debug.rs b/tests/ulm-contracts/debug.rs new file mode 100644 index 00000000..98d1c703 --- /dev/null +++ b/tests/ulm-contracts/debug.rs @@ -0,0 +1,12 @@ +extern "C" { + fn debug_u256(value: u256); + fn debug_u160(value: u160); + fn debug_u128(value: u128); + fn debug_u64(value: u64); + fn debug_u32(value: u32); + fn debug_u16(value: u16); + fn debug_u8(value: u8); + fn debug_bool(value: bool); + fn debug_str(value: &str); + fn debug_unit(value: ()); +} diff --git a/tests/ulm-with-contract/endpoints.1.run b/tests/ulm-with-contract/endpoints.1.run index 01bec977..ecccccba 100644 --- a/tests/ulm-with-contract/endpoints.1.run +++ b/tests/ulm-with-contract/endpoints.1.run @@ -1,10 +1,4 @@ -push "myEndpoint"; -hold_string_from_test_stack; -push "uint64"; -hold_list_values_from_test_stack; -push 123_u64; -hold_list_values_from_test_stack; -encode_call_data; +encode_call_data myEndpoint(123_u64:u64); return_value; mock CallData; diff --git a/tests/ulm-with-contract/endpoints.2.run b/tests/ulm-with-contract/endpoints.2.run index a4dc92d4..a16b70ff 100644 --- a/tests/ulm-with-contract/endpoints.2.run +++ b/tests/ulm-with-contract/endpoints.2.run @@ -1,9 +1,3 @@ -push "myEndpoint"; -hold_string_from_test_stack; -push "uint64"; -hold_list_values_from_test_stack; -push 1_u64; -hold_list_values_from_test_stack; -encode_call_data_to_string; +encode_call_data myEndpoint(1_u64:u64); return_value; -check_eq "\x81\x92(T\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" \ No newline at end of file +check_eq_bytes b"\x81\x92(T\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" diff --git a/tests/ulm-with-contract/endpoints.notfound.run b/tests/ulm-with-contract/endpoints.notfound.run index 2fce4e94..9ad1e122 100644 --- a/tests/ulm-with-contract/endpoints.notfound.run +++ b/tests/ulm-with-contract/endpoints.notfound.run @@ -1,10 +1,4 @@ -push "noEndpoint"; -hold_string_from_test_stack; -push "uint64"; -hold_list_values_from_test_stack; -push 123_u64; -hold_list_values_from_test_stack; -encode_call_data; +encode_call_data noEndpoint(123_u64:u64); return_value; mock CallData; diff --git a/tests/ulm-with-contract/erc_20_token.1.run b/tests/ulm-with-contract/erc_20_token.1.run index 72953e0e..94e4dd0e 100644 --- a/tests/ulm-with-contract/erc_20_token.1.run +++ b/tests/ulm-with-contract/erc_20_token.1.run @@ -1,36 +1,30 @@ -list_mock GetAccountStorageHook ( 13032332009337290780939164280742955473285243463246449969298152790977293574652 ) ulmIntResult(0, u256); -list_mock SetAccountStorageHook ( 13032332009337290780939164280742955473285243463246449969298152790977293574652 , 10000 ) ulmNoResult(); -list_mock GetAccountStorageHook ( 61159765391625381932700807532824927387505868579121206115135228514320059425645 ) ulmIntResult(0, u256); -list_mock SetAccountStorageHook ( 61159765391625381932700807532824927387505868579121206115135228514320059425645 , 10000 ) ulmNoResult(); -list_mock GetAccountStorageHook ( 61159765391625381932700807532824927387505868579121206115135228514320059425645 ) ulmIntResult(10000, u256); -list_mock GetAccountStorageHook ( 61159765391625381932700807532824927387505868579121206115135228514320059425645 ) ulmIntResult(10000, u256); -list_mock GetAccountStorageHook ( 61159765391625381932700807532824927387505868579121206115135228514320059425645 ) ulmIntResult(10000, u256); -list_mock SetAccountStorageHook ( 61159765391625381932700807532824927387505868579121206115135228514320059425645 , 9900 ) ulmNoResult(); -list_mock GetAccountStorageHook ( 107935355587284645605585039702009686485686559005730386557515578263121021727641 ) ulmIntResult(0, u256); -list_mock SetAccountStorageHook ( 107935355587284645605585039702009686485686559005730386557515578263121021727641 , 100 ) ulmNoResult(); -list_mock Log3Hook ( 100389287136786176327247604509743168900146139575972864366142685224231313322991 , 1010101 , 2020202 , b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00d" ) ulmNoResult(); -list_mock GetAccountStorageHook ( 61159765391625381932700807532824927387505868579121206115135228514320059425645 ) ulmIntResult(9900, u256); -list_mock GetAccountStorageHook ( 107935355587284645605585039702009686485686559005730386557515578263121021727641 ) ulmIntResult(100, u256); -list_mock SetAccountStorageHook ( 6299478510657022222390882510197411465571447485061513230872540120223652878023 , 200 ) ulmNoResult(); -list_mock Log3Hook ( 63486140976153616755203102783360879283472101686154884697241723088393386309925 , 1010101 , 3030303 , b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xc8" ) ulmNoResult(); -list_mock GetAccountStorageHook ( 6299478510657022222390882510197411465571447485061513230872540120223652878023 ) ulmIntResult(200, u256); -list_mock SetAccountStorageHook ( 6299478510657022222390882510197411465571447485061513230872540120223652878023 , 0 ) ulmNoResult(); -list_mock GetAccountStorageHook ( 61159765391625381932700807532824927387505868579121206115135228514320059425645 ) ulmIntResult(9900, u256); -list_mock GetAccountStorageHook ( 61159765391625381932700807532824927387505868579121206115135228514320059425645 ) ulmIntResult(9900, u256); -list_mock SetAccountStorageHook ( 61159765391625381932700807532824927387505868579121206115135228514320059425645 , 9700 ) ulmNoResult(); -list_mock GetAccountStorageHook ( 107935355587284645605585039702009686485686559005730386557515578263121021727641 ) ulmIntResult(100, u256); -list_mock SetAccountStorageHook ( 107935355587284645605585039702009686485686559005730386557515578263121021727641 , 300 ) ulmNoResult(); -list_mock Log3Hook ( 100389287136786176327247604509743168900146139575972864366142685224231313322991 , 1010101 , 2020202 , b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xc8" ) ulmNoResult(); -list_mock GetAccountStorageHook ( 61159765391625381932700807532824927387505868579121206115135228514320059425645 ) ulmIntResult(9700, u256); -list_mock GetAccountStorageHook ( 107935355587284645605585039702009686485686559005730386557515578263121021727641 ) ulmIntResult(300, u256); - -push "uint256"; -hold_list_values_from_test_stack; -push 10000_u256; -hold_list_values_from_test_stack; -encode_constructor_data; - - +list_mock GetAccountStorageHook ( storageKey("total_supply", ) ) ulmIntResult(0, u256); +list_mock SetAccountStorageHook ( storageKey("total_supply", ) , 10000_u256 ) ulmNoResult(); +list_mock GetAccountStorageHook ( storageKey("balances", 1010101_u160:u160) ) ulmIntResult(0, u256); +list_mock SetAccountStorageHook ( storageKey("balances", 1010101_u160:u160) , 10000_u256 ) ulmNoResult(); +list_mock GetAccountStorageHook ( storageKey("balances", 1010101_u160:u160) ) ulmIntResult(10000, u256); +list_mock GetAccountStorageHook ( storageKey("balances", 1010101_u160:u160) ) ulmIntResult(10000, u256); +list_mock GetAccountStorageHook ( storageKey("balances", 1010101_u160:u160) ) ulmIntResult(10000, u256); +list_mock SetAccountStorageHook ( storageKey("balances", 1010101_u160:u160) , 9900_u256 ) ulmNoResult(); +list_mock GetAccountStorageHook ( storageKey("balances", 2020202_u160:u160) ) ulmIntResult(0, u256); +list_mock SetAccountStorageHook ( storageKey("balances", 2020202_u160:u160) , 100_u256 ) ulmNoResult(); +list_mock Log3Hook ( eventSignature("Transfer(address,address,uint256)") , 1010101 , 2020202 , encodeValues(100_u256:u256) ) ulmNoResult(); +list_mock GetAccountStorageHook ( storageKey("balances", 1010101_u160:u160) ) ulmIntResult(9900, u256); +list_mock GetAccountStorageHook ( storageKey("balances", 2020202_u160:u160) ) ulmIntResult(100, u256); +list_mock SetAccountStorageHook ( storageKey("allowances", 1010101_u160:u160, 3030303_u160:u160) , 200_u256 ) ulmNoResult(); +list_mock Log3Hook ( eventSignature("Approval(address,address,uint256)") , 1010101 , 3030303 , encodeValues(200_u256:u256) ) ulmNoResult(); +list_mock GetAccountStorageHook ( storageKey("allowances", 1010101_u160:u160, 3030303_u160:u160) ) ulmIntResult(200, u256); +list_mock SetAccountStorageHook ( storageKey("allowances", 1010101_u160:u160, 3030303_u160:u160) , 0_u256 ) ulmNoResult(); +list_mock GetAccountStorageHook ( storageKey("balances", 1010101_u160:u160) ) ulmIntResult(9900, u256); +list_mock GetAccountStorageHook ( storageKey("balances", 1010101_u160:u160) ) ulmIntResult(9900, u256); +list_mock SetAccountStorageHook ( storageKey("balances", 1010101_u160:u160) , 9700_u256 ) ulmNoResult(); +list_mock GetAccountStorageHook ( storageKey("balances", 2020202_u160:u160) ) ulmIntResult(100, u256); +list_mock SetAccountStorageHook ( storageKey("balances", 2020202_u160:u160) , 300_u256 ) ulmNoResult(); +list_mock Log3Hook ( eventSignature("Transfer(address,address,uint256)") , 1010101 , 2020202 , encodeValues(200_u256:u256) ) ulmNoResult(); +list_mock GetAccountStorageHook ( storageKey("balances", 1010101_u160:u160) ) ulmIntResult(9700, u256); +list_mock GetAccountStorageHook ( storageKey("balances", 2020202_u160:u160) ) ulmIntResult(300, u256); + +encode_constructor_data 10000_u256:u256; return_value; mock CallData; @@ -51,13 +45,7 @@ check_eq 0_u32; -push "balanceOf"; -hold_string_from_test_stack; -push "address"; -hold_list_values_from_test_stack; -push 1010101_u160; -hold_list_values_from_test_stack; -encode_call_data; +encode_call_data balanceOf(1010101_u160:u160); return_value; mock CallData; @@ -75,15 +63,7 @@ return_value; check_eq 10000_u256; -push "transfer"; -hold_string_from_test_stack; -push "address"; -push "uint256"; -hold_list_values_from_test_stack; -push 2020202_u160; -push 100_u256; -hold_list_values_from_test_stack; -encode_call_data; +encode_call_data transfer(2020202_u160:u160, 100_u256:u256); return_value; mock CallData; @@ -104,13 +84,7 @@ return_value; check_eq 1_u64; -push "balanceOf"; -hold_string_from_test_stack; -push "address"; -hold_list_values_from_test_stack; -push 1010101_u160; -hold_list_values_from_test_stack; -encode_call_data; +encode_call_data balanceOf(1010101_u160:u160); return_value; mock CallData; @@ -128,13 +102,7 @@ return_value; check_eq 9900_u256; -push "balanceOf"; -hold_string_from_test_stack; -push "address"; -hold_list_values_from_test_stack; -push 2020202_u160; -hold_list_values_from_test_stack; -encode_call_data; +encode_call_data balanceOf(2020202_u160:u160); return_value; mock CallData; @@ -152,15 +120,7 @@ return_value; check_eq 100_u256; -push "approve"; -hold_string_from_test_stack; -push "address"; -push "uint256"; -hold_list_values_from_test_stack; -push 3030303_u160; -push 200_u256; -hold_list_values_from_test_stack; -encode_call_data; +encode_call_data approve(3030303_u160:u160, 200_u256:u256); return_value; mock CallData; @@ -181,17 +141,7 @@ return_value; check_eq 1_u64; -push "transferFrom"; -hold_string_from_test_stack; -push "address"; -push "address"; -push "uint256"; -hold_list_values_from_test_stack; -push 1010101_u160; -push 2020202_u160; -push 200_u256; -hold_list_values_from_test_stack; -encode_call_data; +encode_call_data transferFrom(1010101_u160:u160, 2020202_u160:u160, 200_u256:u256); return_value; mock CallData; @@ -213,13 +163,7 @@ check_eq 1_u64; -push "balanceOf"; -hold_string_from_test_stack; -push "address"; -hold_list_values_from_test_stack; -push 1010101_u160; -hold_list_values_from_test_stack; -encode_call_data; +encode_call_data balanceOf(1010101_u160:u160); return_value; mock CallData; @@ -238,13 +182,7 @@ check_eq 9700_u256; -push "balanceOf"; -hold_string_from_test_stack; -push "address"; -hold_list_values_from_test_stack; -push 2020202_u160; -hold_list_values_from_test_stack; -encode_call_data; +encode_call_data balanceOf(2020202_u160:u160); return_value; mock CallData; diff --git a/tests/ulm-with-contract/erc_20_token.rs b/tests/ulm-with-contract/erc_20_token.rs index 6709262a..d5a25abc 100644 --- a/tests/ulm-with-contract/erc_20_token.rs +++ b/tests/ulm-with-contract/erc_20_token.rs @@ -47,7 +47,7 @@ pub trait Erc20Token { fn s_balances(&self, address: u160) -> ::single_value_mapper::SingleValueMapper; // #[view(getAllowances)] - #[storage_mapper("balances")] + #[storage_mapper("allowances")] fn s_allowances(&self, account: u160, spender: u160) -> ::single_value_mapper::SingleValueMapper; #[event("Transfer")] diff --git a/tests/ulm-with-contract/events.1.run b/tests/ulm-with-contract/events.1.run index 493b6ea5..a0b62cf2 100644 --- a/tests/ulm-with-contract/events.1.run +++ b/tests/ulm-with-contract/events.1.run @@ -1,14 +1,6 @@ list_mock Log2Hook ( 74657075023537209477280918141328480329188930599530356189395812678724488965561 , 123 , b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x02+" ) ulmNoResult(); -push "logEvent"; -hold_string_from_test_stack; -push "uint64"; -push "uint64"; -hold_list_values_from_test_stack; -push 123_u64; -push 555_u64; -hold_list_values_from_test_stack; -encode_call_data; +encode_call_data logEvent(123_u64:u64, 555_u64:u64); return_value; mock CallData; diff --git a/tests/ulm-with-contract/require.false.run b/tests/ulm-with-contract/require.false.run index 4e8a416a..1e463507 100644 --- a/tests/ulm-with-contract/require.false.run +++ b/tests/ulm-with-contract/require.false.run @@ -1,10 +1,4 @@ -push "myEndpoint"; -hold_string_from_test_stack; -push "uint64"; -hold_list_values_from_test_stack; -push 0_u64; -hold_list_values_from_test_stack; -encode_call_data; +encode_call_data myEndpoint(0_u64:u64); return_value; mock CallData; diff --git a/tests/ulm-with-contract/require.true.run b/tests/ulm-with-contract/require.true.run index 9ae345d2..6b20616f 100644 --- a/tests/ulm-with-contract/require.true.run +++ b/tests/ulm-with-contract/require.true.run @@ -1,10 +1,4 @@ -push "myEndpoint"; -hold_string_from_test_stack; -push "uint64"; -hold_list_values_from_test_stack; -push 123_u64; -hold_list_values_from_test_stack; -encode_call_data; +encode_call_data myEndpoint(123_u64:u64); return_value; mock CallData; diff --git a/tests/ulm-with-contract/storage.256.run b/tests/ulm-with-contract/storage.256.run index f20b63a9..52e8af47 100644 --- a/tests/ulm-with-contract/storage.256.run +++ b/tests/ulm-with-contract/storage.256.run @@ -1,13 +1,7 @@ -mock SetAccountStorageHook ( 81899343944223093934060911023235694134954301913235101281428181165721203435003 , 1000000000000000000000000000000000000000000000000000000000000 ) ulmNoResult(); -mock GetAccountStorageHook ( 81899343944223093934060911023235694134954301913235101281428181165721203435003 ) ulmIntResult(1000000000000000000000000000000000000000000000000000000000000, u256); - -push "setMyData256"; -hold_string_from_test_stack; -push "uint256"; -hold_list_values_from_test_stack; -push 1_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_u256; -hold_list_values_from_test_stack; -encode_call_data; +mock SetAccountStorageHook ( storageKey("myData256", ) , 1_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_u256 ) ulmNoResult(); +mock GetAccountStorageHook ( storageKey("myData256", ) ) ulmIntResult(1000000000000000000000000000000000000000000000000000000000000, u256); + +encode_call_data setMyData256(1_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_000_u256:u256); return_value; mock CallData; @@ -19,9 +13,7 @@ push_status; check_eq 2; -push "getMyData256"; -hold_string_from_test_stack; -encode_call_data; +encode_call_data getMyData256(); return_value; mock CallData; diff --git a/tests/ulm-with-contract/storage.key.run b/tests/ulm-with-contract/storage.key.run index 2f9d282f..1f2eb8a7 100644 --- a/tests/ulm-with-contract/storage.key.run +++ b/tests/ulm-with-contract/storage.key.run @@ -1,15 +1,7 @@ -mock SetAccountStorageHook ( 89307555350153532481150451243271458944170707741354029868021544305102042370102 , 123 ) ulmNoResult(); -mock GetAccountStorageHook ( 89307555350153532481150451243271458944170707741354029868021544305102042370102 ) ulmIntResult(123, u256); - -push "setMyDataKey"; -hold_string_from_test_stack; -push "uint64"; -push "uint64"; -hold_list_values_from_test_stack; -push 555_u64; -push 123_u64; -hold_list_values_from_test_stack; -encode_call_data; +mock SetAccountStorageHook ( storageKey("myDataKey", 555_u64:u64) , 123_u64 ) ulmNoResult(); +mock GetAccountStorageHook ( storageKey("myDataKey", 555_u64:u64) ) ulmIntResult(123, u256); + +encode_call_data setMyDataKey(555_u64:u64, 123_u64:u64); return_value; mock CallData; @@ -21,13 +13,7 @@ push_status; check_eq 2; -push "getMyDataKey"; -hold_string_from_test_stack; -push "uint64"; -hold_list_values_from_test_stack; -push 555_u64; -hold_list_values_from_test_stack; -encode_call_data; +encode_call_data getMyDataKey(555_u64:u64); return_value; mock CallData; diff --git a/tests/ulm-with-contract/storage.simple.run b/tests/ulm-with-contract/storage.simple.run index 67d06534..cd6f5647 100644 --- a/tests/ulm-with-contract/storage.simple.run +++ b/tests/ulm-with-contract/storage.simple.run @@ -1,13 +1,7 @@ -mock SetAccountStorageHook ( 2566766180763832229052383091904627608042490431692515280991237530682175269032 , 123 ) ulmNoResult(); -mock GetAccountStorageHook ( 2566766180763832229052383091904627608042490431692515280991237530682175269032 ) ulmIntResult(123, u256); - -push "setMyData"; -hold_string_from_test_stack; -push "uint64"; -hold_list_values_from_test_stack; -push 123_u64; -hold_list_values_from_test_stack; -encode_call_data; +mock SetAccountStorageHook ( storageKey("myData", ) , 123_u64 ) ulmNoResult(); +mock GetAccountStorageHook ( storageKey("myData", ) ) ulmIntResult(123, u256); + +encode_call_data setMyData(123_u64:u64); return_value; mock CallData; @@ -19,9 +13,7 @@ push_status; check_eq 2; -push "getMyData"; -hold_string_from_test_stack; -encode_call_data; +encode_call_data getMyData(); return_value; mock CallData; diff --git a/tests/ulm-with-contract/types.str-raw.run b/tests/ulm-with-contract/types.str-raw.run index a53a467c..4b79b65e 100644 --- a/tests/ulm-with-contract/types.str-raw.run +++ b/tests/ulm-with-contract/types.str-raw.run @@ -1,9 +1,4 @@ -push "strEndpoint"; -hold_string_from_test_stack; -hold_list_values_from_test_stack; -hold_list_values_from_test_stack; -encode_call_data; - +encode_call_data strEndpoint(); return_value; mock CallData; diff --git a/tests/ulm-with-contract/types.str.run b/tests/ulm-with-contract/types.str.run index 384e17ac..dc2a025a 100644 --- a/tests/ulm-with-contract/types.str.run +++ b/tests/ulm-with-contract/types.str.run @@ -1,9 +1,4 @@ -push "strEndpoint"; -hold_string_from_test_stack; -hold_list_values_from_test_stack; -hold_list_values_from_test_stack; -encode_call_data; - +encode_call_data strEndpoint(); return_value; mock CallData; @@ -14,6 +9,7 @@ check_eq (); push_status; check_eq 2; output_to_arg; + call :: test_helpers :: decode_single_str; return_value; check_eq "Hello" diff --git a/ulm-semantics/main/encoding/encoder.md b/ulm-semantics/main/encoding/encoder.md index fc37d305..2670d74c 100644 --- a/ulm-semantics/main/encoding/encoder.md +++ b/ulm-semantics/main/encoding/encoder.md @@ -31,20 +31,20 @@ module ULM-ENCODING-HELPER // Encoding of individual types - rule convertToKBytes(i8(V) , "int8") => Int2Bytes(32, MInt2Signed(V), BE:Endianness) - rule convertToKBytes(u8(V) , "uint8") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) - rule convertToKBytes(i16(V), "int16") => Int2Bytes(32, MInt2Signed(V), BE:Endianness) - rule convertToKBytes(u16(V), "uint16") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) - rule convertToKBytes(i32(V), "int32") => Int2Bytes(32, MInt2Signed(V), BE:Endianness) - rule convertToKBytes(u32(V), "uint32") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) - rule convertToKBytes(i64(V), "int64") => Int2Bytes(32, MInt2Signed(V), BE:Endianness) - rule convertToKBytes(u64(V), "uint64") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) - rule convertToKBytes(u128(V), "uint128") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) - rule convertToKBytes(true, "bool") => Int2Bytes(32, 1, BE:Endianness) + rule convertToKBytes(i8(V) , "int8") => Int2Bytes(32, MInt2Signed(V), BE:Endianness) + rule convertToKBytes(u8(V) , "uint8") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(i16(V), "int16") => Int2Bytes(32, MInt2Signed(V), BE:Endianness) + rule convertToKBytes(u16(V), "uint16") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(i32(V), "int32") => Int2Bytes(32, MInt2Signed(V), BE:Endianness) + rule convertToKBytes(u32(V), "uint32") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(i64(V), "int64") => Int2Bytes(32, MInt2Signed(V), BE:Endianness) + rule convertToKBytes(u64(V), "uint64") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(u128(V), "uint128") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(true, "bool") => Int2Bytes(32, 1, BE:Endianness) rule convertToKBytes(false, "bool") => Int2Bytes(32, 0, BE:Endianness) - rule convertToKBytes(u256(V), "uint256") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) - rule convertToKBytes(u160(V), "uint160") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) - rule convertToKBytes(u160(V), "address") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(u256(V), "uint256") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(u160(V), "uint160") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) + rule convertToKBytes(u160(V), "address") => Int2Bytes(32, MInt2Unsigned(V), BE:Endianness) endmodule @@ -69,6 +69,17 @@ module ULM-CALLDATA-ENCODER | "append_u256" [token] | "append_bool" [token] | "append_str" [token] + | "debug" [token] + | "debug_u8" [token] + | "debug_u16" [token] + | "debug_u32" [token] + | "debug_u64" [token] + | "debug_u128" [token] + | "debug_u160" [token] + | "debug_u256" [token] + | "debug_bool" [token] + | "debug_str" [token] + | "debug_unit" [token] | "empty" [token] | "length" [token] @@ -81,34 +92,6 @@ module ULM-CALLDATA-ENCODER => Bytes2Int(Keccak256raw(String2Bytes(FS)), BE, Unsigned) rule encodeEventSignatureAsInt(E:SemanticsError) => E - // TODO: it may be worth extracting the substrString(Keccak256(String2Bytes(FS)), 0, 8) - // thing to a function that takes a String and produces a String or Bytes (as opposed to - // taking a StringOrError as below) (perhaps with an encodeAsBytes(...) on top of it) and - // then use it here and in the rules below. - rule encodeCallData(FN:String, FAT:List, FAL:List) => - encodeFunctionSignature(FN, FAT) +Bytes encodeFunctionParams(FAL, FAT, b"") - rule encodeConstructorData(FAT:List, FAL:List) => - encodeFunctionParams(FAL, FAT, b"") - - // Function signature encoding - rule encodeFunctionSignature(FuncName:String, RL:List) => - encodeFunctionSignatureHelper(RL:List, FuncName +String "(") [priority(40)] - - rule encodeFunctionSignatureHelper(ListItem(FuncParam:String) RL:List, FS) => - encodeFunctionSignatureHelper(RL, FS +String FuncParam +String ",") [owise] - - // The last param does not have a follow up comma - rule encodeFunctionSignatureHelper(ListItem(FuncParam:String) .List, FS) => - encodeFunctionSignatureHelper(.List, FS +String FuncParam ) - - rule encodeFunctionSignatureHelper(.List, FS) => encodeHexBytes(substrString(Keccak256(String2Bytes(FS +String ")")), 0, 8)) - - // Function parameters encoding - rule encodeFunctionParams(ListItem(V:Value) ARGS:List, ListItem(T:String) PTYPES:List, B:Bytes) => - encodeFunctionParams(ARGS:List, PTYPES:List, B:Bytes +Bytes convertToKBytes(V, T)) - - rule encodeFunctionParams(.List, .List, B:Bytes) => B - syntax Identifier ::= "ulm#head_size" [token] | "ulm#head" [token] | "ulm#tail" [token] @@ -162,6 +145,7 @@ module ULM-CALLDATA-ENCODER , HeadSize , Head, Tail , appendType(T) + , debugType(T) ) , appendValues(Evs, HeadSize, Head, Tail) ) @@ -187,12 +171,30 @@ module ULM-CALLDATA-ENCODER => error("appendType: unrecognized type", ListItem(T)) [owise] + syntax PathInExpressionOrError ::= PathInExpression | SemanticsError + syntax PathInExpressionOrError ::= debugType(Type) [function, total] + + rule debugType(u8 ) => :: debug :: debug_u8 + rule debugType(u16 ) => :: debug :: debug_u16 + rule debugType(u32 ) => :: debug :: debug_u32 + rule debugType(u64 ) => :: debug :: debug_u64 + rule debugType(u128) => :: debug :: debug_u128 + rule debugType(u160) => :: debug :: debug_u160 + rule debugType(u256) => :: debug :: debug_u256 + + rule debugType(bool) => :: debug :: debug_bool + rule debugType(()) => :: debug :: debug_unit + rule debugType(str) => :: debug :: debug_str + rule debugType(T:Type) => error("debugType: unrecognized type", ListItem(T)) + [owise] + syntax NonEmptyStatementsOrError ::= appendValue ( value: Expression , headSize: Expression , head: Identifier , tail: Identifier , appendFn: AppendTypeOrError + , debugFn: PathInExpressionOrError ) [function, total] rule appendValue @@ -201,6 +203,16 @@ module ULM-CALLDATA-ENCODER , head: _Head:Identifier , tail: _Tail:Identifier , appendFn: E:SemanticsError + , debugFn: _Debug:PathInExpressionOrError + ) + => E + rule appendValue + (... value: _Value:Expression + , headSize: _HeadSize:Expression + , head: _Head:Identifier + , tail: _Tail:Identifier + , appendFn: _Append:AppendType + , debugFn: E:SemanticsError ) => E rule appendValue @@ -209,8 +221,10 @@ module ULM-CALLDATA-ENCODER , head: Head:Identifier , tail: _Tail:Identifier , appendFn: fixedSize(P:PathInExpression) + , debugFn: Debug:PathInExpression ) => let Head = P ( Head , Value , .CallParamsList ); + Debug ( Value, .CallParamsList ); .NonEmptyStatements rule appendValue (... value: Value:Expression @@ -218,6 +232,7 @@ module ULM-CALLDATA-ENCODER , head: Head:Identifier , tail: Tail:Identifier , appendFn: variableSize(P:PathInExpression) + , debugFn: Debug:PathInExpression ) => let Head = :: bytes_hooks :: append_u32 ( Head @@ -225,15 +240,18 @@ module ULM-CALLDATA-ENCODER , .CallParamsList ); let Tail = P ( Tail , Value , .CallParamsList ); + Debug ( Value, .CallParamsList ); .NonEmptyStatements rule appendValue - (... value: _Value:Expression + (... value: Value:Expression , headSize: _HeadSize:Expression , head: _Head:Identifier , tail: _Tail:Identifier , appendFn: empty + , debugFn: Debug:PathInExpression ) - => .NonEmptyStatements + => Debug ( Value, .CallParamsList ); + .NonEmptyStatements syntax ExpressionOrError ::= headSize(Type) [function, total] rule headSize(u8 ) => v(ptrValue(null, u32(32p32))) diff --git a/ulm-semantics/main/encoding/syntax.md b/ulm-semantics/main/encoding/syntax.md index 2e65f554..fbf3aca1 100644 --- a/ulm-semantics/main/encoding/syntax.md +++ b/ulm-semantics/main/encoding/syntax.md @@ -4,13 +4,7 @@ module ULM-ENCODING-SYNTAX imports BYTES-SYNTAX imports LIST imports RUST-REPRESENTATION - - // TODO: Make these functions total and returning BytesOrError - syntax Bytes ::= encodeCallData (String, List, List) [function] //Function name, argument types, argument list - | encodeConstructorData (List, List) [function] // argument types, argument list - | encodeFunctionSignature (String, List) [function] - | encodeFunctionSignatureHelper (List, String) [function] - | encodeFunctionParams (List, List, Bytes) [function] + imports ULM-ENCODING-ENCODE-VALUE-SYNTAX syntax BytesOrError ::= encodeFunctionSignatureAsBytes(StringOrError) [function, total] syntax IntOrError ::= encodeEventSignatureAsInt(StringOrError) [function, total] @@ -18,9 +12,6 @@ module ULM-ENCODING-SYNTAX syntax BytesOrError ::= methodSignature(String, NormalizedFunctionParameterList) [function, total] syntax ValueOrError ::= eventSignature(String, NormalizedFunctionParameterList) [function, total] - syntax EncodeValue ::= Expression ":" Type - syntax EncodeValues ::= List{EncodeValue, ","} - // assumes that bufferId points to an empty buffer. syntax NonEmptyStatementsOrError ::= codegenValuesEncoder(bufferId: Identifier, values: EncodeValues) [function, total] @@ -28,6 +19,13 @@ module ULM-ENCODING-SYNTAX syntax EncodeValues ::= paramsToEncodeValues(NormalizedFunctionParameterList) [function, total] endmodule +module ULM-ENCODING-ENCODE-VALUE-SYNTAX + imports RUST-SHARED-SYNTAX + + syntax EncodeValue ::= Expression ":" Type + syntax EncodeValues ::= List{EncodeValue, ","} +endmodule + module ULM-ENCODING-HELPER-SYNTAX imports BYTES-SYNTAX imports LIST diff --git a/ulm-semantics/main/hooks.md b/ulm-semantics/main/hooks.md index ad7f659c..0a077f3e 100644 --- a/ulm-semantics/main/hooks.md +++ b/ulm-semantics/main/hooks.md @@ -1,6 +1,7 @@ ```k requires "hooks/bytes.md" +requires "hooks/debug.md" requires "hooks/helpers.md" requires "hooks/state.md" requires "hooks/ulm.md" @@ -8,6 +9,8 @@ requires "ulm.k" module ULM-SEMANTICS-HOOKS imports private ULM-SEMANTICS-HOOKS-BYTES + // Not including ULM-SEMANTICS-HOOKS-NO-DEBUG or ULM-SEMANTICS-HOOKS-DEBUG + // here, they should be included directly in the target module. imports private ULM-SEMANTICS-HOOKS-HELPERS imports private ULM-SEMANTICS-HOOKS-STATE imports private ULM-SEMANTICS-HOOKS-ULM diff --git a/ulm-semantics/main/hooks/bytes.md b/ulm-semantics/main/hooks/bytes.md index 5111ea00..d11bdbae 100644 --- a/ulm-semantics/main/hooks/bytes.md +++ b/ulm-semantics/main/hooks/bytes.md @@ -303,7 +303,6 @@ module ULM-SEMANTICS-HOOKS-BYTES rule ulmBytesAppendBool(ptrValue(P, u64(BytesId)), ptrValue(_, true)) => ulmBytesAppendInt(ptrValue(P, u64(BytesId)), ptrValue(null, u8(1p8))) - // TODO: This can create key ambiguity for storage rule ulmBytesAppendStr(ptrValue(_, u64(BytesId)), ptrValue(_, Value:String)) => ulmBytesAppendLenAndBytes(ulmBytesId(BytesId), String2Bytes(Value)) diff --git a/ulm-semantics/main/hooks/debug.md b/ulm-semantics/main/hooks/debug.md new file mode 100644 index 00000000..7a6df087 --- /dev/null +++ b/ulm-semantics/main/hooks/debug.md @@ -0,0 +1,61 @@ +```k + +module ULM-SEMANTICS-HOOKS-DEBUG-CONFIGURATION + imports LIST + + configuration + + .List + +endmodule + +module ULM-SEMANTICS-HOOKS-DEBUG-SYNTAX + imports RUST-SHARED-SYNTAX + + syntax Instruction ::= debugExpression(Expression) +endmodule + +// Either ULM-SEMANTICS-HOOKS-NO-DEBUG or ULM-SEMANTICS-HOOKS-DEBUG should be +// included directly in the target module. +module ULM-SEMANTICS-HOOKS-NO-DEBUG + imports private ULM-SEMANTICS-HOOKS-DEBUG-FUNCTIONS + imports private ULM-SEMANTICS-HOOKS-DEBUG-SYNTAX + + rule debugExpression(_:Expression) => .K +endmodule + +module ULM-SEMANTICS-HOOKS-DEBUG + imports private COMMON-K-CELL + imports private RUST-REPRESENTATION + imports private ULM-SEMANTICS-HOOKS-DEBUG-CONFIGURATION + imports private ULM-SEMANTICS-HOOKS-DEBUG-FUNCTIONS + imports private ULM-SEMANTICS-HOOKS-DEBUG-SYNTAX + + rule debugExpression(E:Expression) => debugExpressionImpl(E) + + syntax Instruction ::= debugExpressionImpl(Expression) [strict(1)] + + rule + debugExpressionImpl(V:PtrValue) => .K ... + + ... + .List => ListItem(V) + +endmodule + +module ULM-SEMANTICS-HOOKS-DEBUG-FUNCTIONS + imports private RUST-REPRESENTATION + imports private ULM-SEMANTICS-HOOKS-DEBUG-SYNTAX + + syntax Identifier ::= "debug" [token] + + rule + normalizedFunctionCall + ( :: debug :: _:Identifier :: .PathExprSegments + , ValueId:Ptr, .PtrList + ) + => debugExpression(ValueId) + +endmodule + +``` diff --git a/ulm-semantics/main/hooks/ulm.md b/ulm-semantics/main/hooks/ulm.md index eeced224..c6b06f69 100644 --- a/ulm-semantics/main/hooks/ulm.md +++ b/ulm-semantics/main/hooks/ulm.md @@ -6,8 +6,6 @@ module ULM-SEMANTICS-HOOKS-ULM-SYNTAX syntax UlmHook ::= CallDataHook() | CallerHook() - // TODO: Build mocks for all the hooks below in a meaningful - // way in tests (right now we just use opaque values). | SetAccountStorageHook(Int, Int) | GetAccountStorageHook(Int) | Log0Hook(Bytes) diff --git a/ulm-semantics/main/preprocessing/storage.md b/ulm-semantics/main/preprocessing/storage.md index 72a313bf..3c46f768 100644 --- a/ulm-semantics/main/preprocessing/storage.md +++ b/ulm-semantics/main/preprocessing/storage.md @@ -5,6 +5,8 @@ module ULM-PREPROCESSING-STORAGE imports private COMMON-K-CELL imports private RUST-ERROR-SYNTAX imports private RUST-PREPROCESSING-CONFIGURATION + imports private RUST-REPRESENTATION + imports private ULM-ENCODING-SYNTAX imports private ULM-PREPROCESSING-SYNTAX-PRIVATE imports private ULM-REPRESENTATION @@ -16,9 +18,14 @@ module ULM-PREPROCESSING-STORAGE ) => ulmAddStorageMethodBody (... methodName: Method - , storageName: StorageName , mapperValueType: MapperValue - , appendParamsInstructions: encodeParams(Params) + , appendParamsInstructions: + codegenValuesEncoder + ( buffer_id + , ( ptrValue(null, StorageName) : str + , paramsToEncodeValues(Params) + ) + ) ) ... @@ -34,7 +41,6 @@ module ULM-PREPROCESSING-STORAGE ulmAddStorageMethodBody (... methodName: Method:PathInExpression - , storageName: StorageName:String , mapperValueType: MapperValueType:Type , appendParamsInstructions: Append:NonEmptyStatements ) => .K @@ -46,11 +52,6 @@ module ULM-PREPROCESSING-STORAGE concatNonEmptyStatements ( concatNonEmptyStatements ( let buffer_id = :: bytes_hooks :: empty(.CallParamsList); - let buffer_id = :: bytes_hooks :: append_str - ( buffer_id - , ptrValue(null, StorageName) - , .CallParamsList - ); .NonEmptyStatements , Append ) @@ -79,17 +80,9 @@ module ULM-PREPROCESSING-STORAGE | "single_value_mapper" [token] | "SingleValueMapper" [token] | "storage" [token] + | "str" [token] | "value_type" [token] - syntax NonEmptyStatementsOrError ::= encodeParams(NormalizedFunctionParameterList) - [function, total] - rule encodeParams(.NormalizedFunctionParameterList) => .NonEmptyStatements - rule encodeParams(Name:Identifier : T:Type , Ps:NormalizedFunctionParameterList) - => concat(encodeParam(Name, T), encodeParams(Ps)) - rule encodeParams(P:NormalizedFunctionParameter , Ps:NormalizedFunctionParameterList) - => error("encodeParams: unexpected", ListItem(P) ListItem(Ps)) - [owise] - syntax NonEmptyStatementsOrError ::= encodeParam(Identifier, Type) [function, total] syntax NonEmptyStatementsOrError ::= encodeParam(ExpressionOrError) [function, total] syntax ExpressionOrError ::= encodeForType(Identifier, Type) [function, total] diff --git a/ulm-semantics/main/preprocessing/syntax.md b/ulm-semantics/main/preprocessing/syntax.md index 5e80e05e..294e4f07 100644 --- a/ulm-semantics/main/preprocessing/syntax.md +++ b/ulm-semantics/main/preprocessing/syntax.md @@ -43,7 +43,6 @@ module ULM-PREPROCESSING-SYNTAX-PRIVATE ) | ulmAddStorageMethodBody ( methodName: PathInExpression - , storageName: String , mapperValueType: Type , appendParamsInstructions: NonEmptyStatementsOrError ) diff --git a/ulm-semantics/targets/execution/ulm-target.md b/ulm-semantics/targets/execution/ulm-target.md index 7b5e705f..1edcae80 100644 --- a/ulm-semantics/targets/execution/ulm-target.md +++ b/ulm-semantics/targets/execution/ulm-target.md @@ -21,6 +21,7 @@ module ULM-TARGET imports private ULM-ENCODING imports private ULM-EXECUTION imports private ULM-PREPROCESSING + imports private ULM-SEMANTICS-HOOKS-NO-DEBUG imports private ULM-SEMANTICS-HOOKS-TO-ULM-FUNCTIONS imports private ULM-TARGET-CONFIGURATION endmodule diff --git a/ulm-semantics/targets/testing/configuration.md b/ulm-semantics/targets/testing/configuration.md index e8627a9f..3474a479 100644 --- a/ulm-semantics/targets/testing/configuration.md +++ b/ulm-semantics/targets/testing/configuration.md @@ -25,6 +25,7 @@ module ULM-TARGET-CONFIGURATION imports RUST-EXECUTION-TEST-CONFIGURATION imports ULM-CONFIGURATION imports ULM-FULL-PREPROCESSED-CONFIGURATION + imports ULM-SEMANTICS-HOOKS-DEBUG-CONFIGURATION imports ULM-PREPROCESSING-EPHEMERAL-CONFIGURATION imports ULM-TEST-CONFIGURATION @@ -35,6 +36,7 @@ module ULM-TARGET-CONFIGURATION + endmodule diff --git a/ulm-semantics/targets/testing/ulm-target.md b/ulm-semantics/targets/testing/ulm-target.md index 36b874d0..b60f8438 100644 --- a/ulm-semantics/targets/testing/ulm-target.md +++ b/ulm-semantics/targets/testing/ulm-target.md @@ -23,6 +23,7 @@ module ULM-TARGET imports private ULM-EXECUTION imports private ULM-ENCODING imports private ULM-PREPROCESSING + imports private ULM-SEMANTICS-HOOKS-DEBUG imports private ULM-TARGET-CONFIGURATION imports private ULM-TEST-EXECUTION endmodule diff --git a/ulm-semantics/test/execution.md b/ulm-semantics/test/execution.md index 7f22cbb2..4fd2d74d 100644 --- a/ulm-semantics/test/execution.md +++ b/ulm-semantics/test/execution.md @@ -3,41 +3,34 @@ module ULM-TEST-SYNTAX imports BYTES-SYNTAX imports INT-SYNTAX - imports STRING-SYNTAX imports RUST-EXECUTION-TEST-PARSING-SYNTAX + imports STRING-SYNTAX + imports ULM-ENCODING-ENCODE-VALUE-SYNTAX imports ULM-SEMANTICS-HOOKS-ULM-SYNTAX - imports BYTES-SYNTAX - // TODO: Do not use KItem for ptr_holder and value_holder. This is - // too generic and can lead to problems. - // TODO: Replace the list_ptrs_holder and list_values_holder with - // PtrList and ValueList. - syntax ULMTestTypeHolder ::= "ptr_holder" KItem [strict] - | "value_holder" KItem - | "list_ptrs_holder" List - | "list_values_holder" List - - syntax ULMTestTypeHolderList ::= List{ULMTestTypeHolder, ","} syntax BytesList ::= NeList{Bytes, "+"} + syntax EncodeCall ::= Identifier "(" EncodeValues ")" + + syntax Expression ::= newBytes(Bytes) + syntax ExecutionItem ::= "mock" "CallData" | "mock" "Caller" | "mock" UlmHook UlmHookResult + | "mock" UlmTestHook UlmHookResult [strict(1), result(TestResult)] | "list_mock" UlmHook UlmHookResult - | "encode_call_data" - | "encode_call_data_to_string" - | "encode_constructor_data" + | "list_mock" UlmTestHook UlmHookResult [strict(1), result(TestResult)] + | "encode_call_data" EncodeCall + | "encode_constructor_data" EncodeValues | "call_contract" Int | "init_contract" Int | "clear_pgm" - | "hold" KItem | "output_to_arg" | "push_status" | "check_eq" Int - | "hold_string_from_test_stack" - | "hold_list_values_from_test_stack" | "expect_cancel" | "check_raw_output" BytesList + | "check_eq_bytes" Bytes syntax Identifier ::= "u8" [token] | "u16" [token] @@ -46,13 +39,24 @@ module ULM-TEST-SYNTAX | "u128" [token] | "u160" [token] | "u256" [token] + + syntax UlmTestHook ::= SetAccountStorageHook(StorageKey, Expression) [seqstrict, result(TestResult)] + | GetAccountStorageHook(StorageKey) [seqstrict, result(TestResult)] + | Log3Hook(EventSignature, Int, Int, EncodeValues) [seqstrict(1, 4), result(TestResult)] + + syntax StorageKey ::= storageKey(String, EncodeValues) + syntax EventSignature ::= eventSignature(String) + syntax EncodeValues ::= encodeValues(EncodeValues) endmodule module ULM-TEST-EXECUTION imports private BYTES imports private COMMON-K-CELL imports private K-EQUAL-SYNTAX + imports private KRYPTO + imports private RUST-ERROR-SYNTAX imports private RUST-EXECUTION-TEST-CONFIGURATION + imports private RUST-REPRESENTATION imports private RUST-SHARED-SYNTAX imports private ULM-ENCODING-SYNTAX imports private ULM-EXECUTION-SYNTAX @@ -63,68 +67,70 @@ module ULM-TEST-EXECUTION imports private ULM-REPRESENTATION imports private ULM-TEST-SYNTAX + syntax UlmTestHook ::= mockSetAccountStorageHook(Int, IntOrError) + | mockGetAccountStorageHook(Int) + | #Log3Hook(Int, Int, Int, Bytes) syntax Mockable ::= UlmHook - // The following constructions allows us to build more complex data structures - // for mocking tests - rule UTH:ULMTestTypeHolder ~> EI:ExecutionItem => EI ~> UTH ... - rule UTHL:ULMTestTypeHolderList ~> EI:ExecutionItem => EI ~> UTHL ... - rule UTH1:ULMTestTypeHolder ~> UTH2:ULMTestTypeHolder - => (UTH1, UTH2):ULMTestTypeHolderList ... - rule UTH:ULMTestTypeHolder ~> UTHL:ULMTestTypeHolderList - => (UTH, UTHL):ULMTestTypeHolderList ... - - rule hold_string_from_test_stack => ptr_holder P ... - ListItem(P) L:List => L - rule ptr_holder ptrValue(_, V) => value_holder V ... - - - // TODO: Rework the implementation of the productions related to list value holding - // Ref - https://github.com/Pi-Squared-Inc/rust-demo-semantics/pull/167#discussion_r1813386536 - rule hold_list_values_from_test_stack => list_ptrs_holder L ~> list_values_holder .List ... - L:List => .List - rule list_ptrs_holder ListItem(I) LPH ~> list_values_holder LLH - => I ~> list_ptrs_holder LPH ~> list_values_holder LLH ... - rule ptrValue(_, V) ~> list_ptrs_holder LPH ~> list_values_holder LLH - => list_ptrs_holder LPH ~> list_values_holder ListItem(V) LLH ... - rule list_ptrs_holder .List => .K ... - - rule hold I => value_holder I ... - - rule encode_call_data_to_string - ~> list_values_holder ARGS , list_values_holder PTYPES , value_holder FNAME , .ULMTestTypeHolderList - => Bytes2String(encodeCallData(FNAME, PTYPES, ARGS)) - ... - - - rule encode_call_data_to_string - ~> value_holder FNAME - => Bytes2String(encodeCallData(FNAME, .List, .List)) - ... - [owise] + syntax BytesOrError ::= extractCallSignature(EncodeCall) [function, total] + rule extractCallSignature(Fn:Identifier ( Args:EncodeValues )) + => methodSignature(IdentifierToString(Fn), encodeArgsToNormalizedParams(Args)) + syntax NormalizedFunctionParameterList ::= encodeArgsToNormalizedParams(EncodeValues) [function, total] + rule encodeArgsToNormalizedParams(.EncodeValues) => .NormalizedFunctionParameterList + rule encodeArgsToNormalizedParams(_:Expression : T:Type , Eas:EncodeValues ) + => #token("#unused", "Identifier"):T , encodeArgsToNormalizedParams(Eas) + + syntax Identifier ::= "append_bytes_raw" [token] + | "buffer_id" [token] + | "bytes_hooks" [token] + | "empty" [token] + | "str" [token] + + syntax NonEmptyStatementsOrError ::= encodeInstructions(EncodeCall) [function, total] + rule encodeInstructions( _:Identifier ( Args:EncodeValues ) ) + => encodeInstructions(Args) + syntax NonEmptyStatementsOrError ::= encodeInstructions(EncodeValues) [function, total] + rule encodeInstructions(Args:EncodeValues) + => concat + ( let buffer_id = :: bytes_hooks :: empty( .CallParamsList ); + .NonEmptyStatements + , codegenValuesEncoder(buffer_id, Args) + ) + + rule encode_call_data C:EncodeCall + => encodeCallData(extractCallSignature(C), encodeInstructions(C)) + + syntax ExecutionItem ::= encodeCallData(BytesOrError, NonEmptyStatementsOrError) + rule encodeCallData(Signature:Bytes, Statements:NonEmptyStatements) + => Statements + :: bytes_hooks :: append_bytes_raw + ( ulmBytesNew(Signature) , buffer_id , .CallParamsList ):Expression - rule encode_call_data - ~> list_values_holder ARGS , list_values_holder PTYPES , value_holder FNAME , .ULMTestTypeHolderList - => ulmBytesNew(encodeCallData(FNAME, PTYPES, ARGS)) - ... - - - rule encode_call_data - ~> value_holder FNAME - => ulmBytesNew(encodeCallData(FNAME, .List, .List)) - ... - [owise] - - rule encode_constructor_data - ~> list_values_holder ARGS , list_values_holder PTYPES , .ULMTestTypeHolderList - => ulmBytesNew(encodeConstructorData(PTYPES, ARGS)) + rule + + check_eq_bytes B:Bytes => .K ... - - - rule encode_constructor_data - => ulmBytesNew(encodeConstructorData(.List, .List)) + + + ListItem(ptrValue(_, u64(V))) => .List ... - [owise] + + + Buffers:Map + + // We expect that the item at the top of the stack points to the + // bytes provided to `check_eq_bytes`. This means that the + // equality below should evaluate to false on the "orDefault" case + // (i.e. the item at the top of the stack does not point to bytes). + requires B:Bytes:KItem ==K Buffers[MInt2Unsigned(V)] orDefault 0 + + syntax ExecutionItem ::= encodeConstructorData(NonEmptyStatementsOrError) + + rule encode_constructor_data Args:EncodeValues + => encodeConstructorData(encodeInstructions(Args)) + rule encodeConstructorData(Statements:NonEmptyStatements) + => Statements + buffer_id:Expression rule mock CallData => mock(CallDataHook(), V) ... @@ -199,6 +205,100 @@ module ULM-TEST-EXECUTION B:Bytes + syntax Bool ::= isTestResult(K) [symbol(isTestResult), function] + rule isTestResult(_:K) => false [owise] + rule isTestResult(evaluatedStorageKey(_:Bytes)) => true + rule isTestResult(evaluatedEventSignature(_:Int)) => true + rule isTestResult(encodedValues(_:Bytes)) => true + rule isTestResult(_:PtrValue) => true + rule isTestResult(mockSetAccountStorageHook(_:Int, _:Int)) => true + rule isTestResult(mockGetAccountStorageHook(_:Int)) => true + rule isTestResult(#Log3Hook(_:Int, _:Int, _:Int, _:Bytes)) => true + + syntax StorageKey ::= storageKey(NonEmptyStatementsOrError) + | storageKey(Expression) [strict(1)] + | storageKey(UlmExpression) [strict(1)] + | evaluatedStorageKey(Bytes) + rule storageKey(StorageName:String, Args:EncodeValues) + => storageKey + ( concat + ( let buffer_id = :: bytes_hooks :: empty( .CallParamsList ); + .NonEmptyStatements + , codegenValuesEncoder + ( buffer_id + , (StorageName : str , Args) + ) + ) + ) + rule storageKey(Statements:NonEmptyStatements) + => storageKey({.InnerAttributes Statements buffer_id }) + rule storageKey(ptrValue(_, u64(BytesId))) => storageKey(ulmBytesId(BytesId)) + rule storageKey(ulmBytesValue(B:Bytes)) => evaluatedStorageKey(B) + + syntax EventSignature ::= evaluatedEventSignature(Int) + rule eventSignature(Signature:String) + => evaluatedEventSignature(Bytes2Int(Keccak256raw(String2Bytes(Signature)), BE, Unsigned)) + + syntax EncodeValues ::= encodeValues(NonEmptyStatementsOrError) + | encodeValues(Expression) [strict(1)] + | encodeValues(UlmExpression) [strict(1)] + | encodedValues(Bytes) + rule encodeValues(Args:EncodeValues) + => encodeValues + ( concat + ( let buffer_id = :: bytes_hooks :: empty( .CallParamsList ); + .NonEmptyStatements + , codegenValuesEncoder + ( buffer_id + , Args + ) + ) + ) + rule encodeValues(Statements:NonEmptyStatements) + => encodeValues({.InnerAttributes Statements buffer_id }) + rule encodeValues(ptrValue(_, u64(BytesId))) => encodeValues(ulmBytesId(BytesId)) + rule encodeValues(ulmBytesValue(B:Bytes)) => encodedValues(B) + + rule SetAccountStorageHook(evaluatedStorageKey(B:Bytes), ptrValue(_, Value:Value)) + => mockSetAccountStorageHook + ( Bytes2Int(Keccak256raw(B), BE, Unsigned) + , valueToInteger(Value) + ) + rule mock mockSetAccountStorageHook(Key:Int, Value:Int) Result:UlmHookResult + => mock + SetAccountStorageHook(Key, Value) + Result + rule list_mock mockSetAccountStorageHook(Key:Int, Value:Int) Result:UlmHookResult + => list_mock + SetAccountStorageHook(Key, Value) + Result + + rule GetAccountStorageHook(evaluatedStorageKey(B:Bytes)) + => mockGetAccountStorageHook(Bytes2Int(Keccak256raw(B), BE, Unsigned)) + rule mock mockGetAccountStorageHook(Key:Int) Result:UlmHookResult + => mock + GetAccountStorageHook(Key) + Result + rule list_mock mockGetAccountStorageHook(Key:Int) Result:UlmHookResult + => list_mock + GetAccountStorageHook(Key) + Result + + rule Log3Hook(evaluatedEventSignature(I:Int), A:Int, C:Int, encodedValues(B2:Bytes)) + => #Log3Hook + ( I + , A + , C + , B2 + ) + rule list_mock #Log3Hook(V1:Int, V2:Int, V3:Int, B:Bytes) Result:UlmHookResult + => list_mock + Log3Hook(V1, V2, V3, B) + Result + + // This may seem stupid, but it's a workaround for + // https://github.com/runtimeverification/k/issues/4683 + rule isKResult(X) => true requires isTestResult(X) endmodule ```