From b33aa520e5a189f264fa84adf0176e03d83e4d93 Mon Sep 17 00:00:00 2001 From: Virgil <25692529+virgil-serbanuta@users.noreply.github.com> Date: Tue, 22 Oct 2024 23:28:45 +0300 Subject: [PATCH] Implement ULM hooks; Implement ULM callbacks and fixes (#169) --- .gitmodules | 0 Makefile | 3 + kllvm/ulm.k | 156 ++++++++++++++++++ rust-semantics/test/execution.md | 1 + tests/ukm-with-contract/erc_20_token.1.run | 28 ++-- tests/ukm-with-contract/storage.key.run | 2 +- tests/ukm-with-contract/storage.simple.run | 2 +- ukm-semantics/main/hooks.md | 1 + ukm-semantics/main/hooks/ukm.md | 78 ++++++++- .../targets/execution/configuration.md | 10 +- ukm-semantics/targets/execution/ukm-target.md | 1 + .../targets/testing/configuration.md | 16 +- ukm-semantics/test/execution.md | 8 + 13 files changed, 267 insertions(+), 39 deletions(-) create mode 100644 .gitmodules create mode 100644 kllvm/ulm.k diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 0000000..e69de29 diff --git a/Makefile b/Makefile index 26e8e57..ac83c27 100644 --- a/Makefile +++ b/Makefile @@ -186,6 +186,7 @@ $(UKM_EXECUTION_TIMESTAMP): $(UKM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) -rm -r $(UKM_EXECUTION_KOMPILED) $$(which kompile) ukm-semantics/targets/execution/ukm-target.md \ --emit-json -o $(UKM_EXECUTION_KOMPILED) \ + -I kllvm \ -I . \ --debug @@ -201,8 +202,10 @@ $(UKM_TESTING_TIMESTAMP): $(UKM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) # Workaround for https://github.com/runtimeverification/k/issues/4141 -rm -r $(UKM_TESTING_KOMPILED) $$(which kompile) ukm-semantics/targets/testing/ukm-target.md \ + ${PLUGIN_FLAGS} \ --emit-json -o $(UKM_TESTING_KOMPILED) \ -I . \ + -I kllvm \ --debug $(RUST_SYNTAX_OUTPUT_DIR)/%.rs-parsed: $(RUST_SYNTAX_INPUT_DIR)/%.rs $(RUST_PREPROCESSING_TIMESTAMP) diff --git a/kllvm/ulm.k b/kllvm/ulm.k new file mode 100644 index 0000000..5070423 --- /dev/null +++ b/kllvm/ulm.k @@ -0,0 +1,156 @@ +// The hooks in this module can be called by the semantics. +// Currently the semantics is required to keep track of the gas costs for these +// operations. This will change in the final version after October. +module ULM-HOOKS + imports private BASIC-K + imports private BOOL + imports private INT + imports private BYTES + + // block parameters + syntax Int ::= GasLimit() [function, hook(ULM.gasLimit)] + | BaseFee() [function, hook(ULM.baseFee)] + | Coinbase() [function, hook(ULM.coinbase)] + | BlockTimestamp() [function, hook(ULM.timestamp)] + | BlockNumber() [function, hook(ULM.number)] + | BlockDifficulty() [function, hook(ULM.difficulty)] + | PrevRandao() [function, hook(ULM.prevRandao)] + syntax Int ::= BlockHash(index: Int) [function, hook(ULM.blockHash), total] + + // transaction parameters + syntax Int ::= GasPrice() [function, hook(ULM.gasPrice)] + | Origin() [function, hook(ULM.origin)] + + // message parameters + syntax Int ::= Address() [function, hook(ULM.address)] + | Caller() [function, hook(ULM.caller)] + | CallValue() [function, hook(ULM.callValue)] + syntax Bytes ::= CallData() [function, hook(ULM.callData)] + + // chain parameters + syntax Int ::= ChainId() [function, hook(ULM.chainId)] + + // account getters + syntax Int ::= GetAccountBalance(acct: Int) [function, hook(ULM.getBalance), total] + syntax Bytes ::= GetAccountCode(acct: Int) [function, hook(ULM.getCode), total] + syntax Int ::= GetAccountStorage(key: Int) [function, hook(ULM.getStorage), total] + | GetAccountOrigStorage(key: Int) [function, hook(ULM.getOrigStorage), total] + | GetAccountTransientStorage(key: Int) [function, hook(ULM.getTransientStorage), total] + syntax Bool ::= IsAccountEmpty(acct: Int) [function, hook(ULM.isAccountEmpty), total] + + // to be removed in final version + syntax Bool ::= AccessedStorage(key: Int) [function, hook(ULM.accessedStorage), total] + syntax Bool ::= AccessedAccount(acct: Int) [function, hook(ULM.accessedAccount), total] + + // account modifiers + syntax Bool ::= Transfer(to: Int, value: Int) [function, hook(ULM.transfer), impure] + syntax K ::= SelfDestruct(to: Int) [function, hook(ULM.selfdestruct), impure] + syntax K ::= SetAccountStorage(key: Int, value: Int) [function, hook(ULM.setStorage)] + | SetAccountTransientStorage(key: Int, value: Int) [function, hook(ULM.setTransientStorage)] + + // log emitters + syntax K ::= Log0(data: Bytes) [function, hook(ULM.log0)] + | Log1(topic0: Int, data: Bytes) [function, hook(ULM.log1)] + | Log2(topic0: Int, topic1: Int, data: Bytes) [function, hook(ULM.log2)] + | Log3(topic0: Int, topic1: Int, topic2: Int, data: Bytes) [function, hook(ULM.log3)] + | Log4(topic0: Int, topic1: Int, topic2: Int, topic3: Int, data: Bytes) [function, hook(ULM.log4)] + + syntax Int ::= "EVMC_REJECTED" [function] + | "EVMC_INTERNAL_ERROR" [function] + | "EVMC_SUCCESS" [function] + | "EVMC_REVERT" [function] + | "EVMC_FAILURE" [function] + | "EVMC_INVALID_INSTRUCTION" [function] + | "EVMC_UNDEFINED_INSTRUCTION" [function] + | "EVMC_OUT_OF_GAS" [function] + | "EVMC_BAD_JUMP_DESTINATION" [function] + | "EVMC_STACK_OVERFLOW" [function] + | "EVMC_STACK_UNDERFLOW" [function] + | "EVMC_CALL_DEPTH_EXCEEDED" [function] + | "EVMC_INVALID_MEMORY_ACCESS" [function] + | "EVMC_STATIC_MODE_VIOLATION" [function] + | "EVMC_PRECOMPILE_FAILURE" [function] + | "EVMC_NONCE_EXCEEDED" [function] + + rule EVMC_REJECTED => 0 + rule EVMC_INTERNAL_ERROR => 1 + rule EVMC_SUCCESS => 2 + rule EVMC_REVERT => 3 + rule EVMC_FAILURE => 4 + rule EVMC_INVALID_INSTRUCTION => 5 + rule EVMC_UNDEFINED_INSTRUCTION => 6 + rule EVMC_OUT_OF_GAS => 7 + rule EVMC_BAD_JUMP_DESTINATION => 8 + rule EVMC_STACK_OVERFLOW => 9 + rule EVMC_STACK_UNDERFLOW => 10 + rule EVMC_CALL_DEPTH_EXCEEDED => 11 + rule EVMC_INVALID_MEMORY_ACCESS => 12 + rule EVMC_STATIC_MODE_VIOLATION => 13 + rule EVMC_PRECOMPILE_FAILURE => 14 + rule EVMC_NONCE_EXCEEDED => 15 + + // external account calls and creation + syntax MessageResult ::= MessageResult(gas: Int, data: Bytes, status: Int, target: Int) [symbol(MessageResult)] + | Create(value: Int, data: Bytes, gas: Int) [function, hook(ULM.create), impure] + | Create2(value: Int, data: Bytes, salt: Bytes, gas: Int) [function, hook(ULM.create2), impure] + | Call(gas: Int, to: Int, value: Int, data: Bytes) [function, hook(ULM.call), impure] + | CallCode(gas: Int, to: Int, value: Int, data: Bytes) [function, hook(ULM.callCode), impure] + | DelegateCall(gas: Int, to: Int, data: Bytes) [function, hook(ULM.delegateCall), impure] + | StaticCall(gas: Int, to: Int, data: Bytes) [function, hook(ULM.staticCall), impure] + +endmodule + +// The functions in this module must be implemented by the semantics. They +// represent the way the integration layer understands the output of the call +// frame (i.e., return data buffer, status code, gas remaining) +module ULM-SIGNATURE + imports ULM-HOOKS + imports private BYTES + imports private INT + + syntax GeneratedTopCell + + syntax Bytes ::= getOutput(GeneratedTopCell) [function, symbol(getOutput), total] + rule getOutput(_) => .Bytes [owise] + + syntax Int ::= getStatus(GeneratedTopCell) [function, symbol(getStatus), total] + rule getStatus(_) => EVMC_INTERNAL_ERROR [owise] + + syntax Int ::= getGasLeft(GeneratedTopCell) [function, symbol(getGasLeft), total] + rule getGasLeft(_) => 0 [owise] + +endmodule + +module ULM + imports ULM-SIGNATURE + + // Additionally, the semantics must declare the following configuration + // variables only. It is allowed for some of these variables to be ommitted + // if the semantics does not need them. + // + // $PGM:Bytes - This is the value of the contract's code as stored by the + // StateDB. The semantics is responsible for deserializing this into a + // format it is able to execute. + // + // $ACCTCODE:Int - This is the 160-bit integer address of the account that + // corresponds to the $PGM. + // + // $SCHEDULE:Int - This is the value of the schedule_t from ulm_kllvm.h that + // corresponds to the EVM execution layer hard fork active on the current + // block. It can be ignored for non-EVM semantics; a different mechanism for + // handling layer upgrades will likely be developed post-October. + // + // $GAS:Int - This is the amount of gas provided to the contract. Eventually + // gas calculations will be handled a different way instead of being tracked + // by the semantics. For now nothing prevents a semantics from ignoring this + // value, which leaves the chain open to denial-of-service attacks. + // + // $STATIC:Bool - This indicates whether the current contract is allowed + // to modify the block state. Currently this is not enforced; nothing stops + // the semantics from choosing to ignore it. This will change in the final + // version. + // + // $CREATE:Bool - This indicates whether this is a contract creation message. + // Non-EVM languages may need this information to decide how to decode the + // $PGM variable +endmodule diff --git a/rust-semantics/test/execution.md b/rust-semantics/test/execution.md index 1ba26a6..b8929f0 100644 --- a/rust-semantics/test/execution.md +++ b/rust-semantics/test/execution.md @@ -116,6 +116,7 @@ module RUST-EXECUTION-TEST rule listMock(Mocked:Mockable, Result:K) => .K ... L:List => L ListItem(listMock(Mocked, Result)) + [priority(10)] rule (Mocked:Mockable => Result) ... diff --git a/tests/ukm-with-contract/erc_20_token.1.run b/tests/ukm-with-contract/erc_20_token.1.run index e477965..21b01e3 100644 --- a/tests/ukm-with-contract/erc_20_token.1.run +++ b/tests/ukm-with-contract/erc_20_token.1.run @@ -1,25 +1,25 @@ -list_mock GetAccountStorageHook ( 7809087261546347641 ) ukmInt256Result(0); +list_mock GetAccountStorageHook ( 7809087261546347641 ) ukmIntResult(0, u256); list_mock SetAccountStorageHook ( 7809087261546347641 , 10000 ) ukmNoResult(); -list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmInt256Result(0); +list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmIntResult(0, u256); list_mock SetAccountStorageHook ( 7162266444907899391 , 10000 ) ukmNoResult(); -list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmInt256Result(10000); -list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmInt256Result(10000); -list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmInt256Result(10000); +list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmIntResult(10000, u256); +list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmIntResult(10000, u256); +list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmIntResult(10000, u256); list_mock SetAccountStorageHook ( 7162266444907899391 , 9900 ) ukmNoResult(); -list_mock GetAccountStorageHook ( 7162266444908917614 ) ukmInt256Result(0); +list_mock GetAccountStorageHook ( 7162266444908917614 ) ukmIntResult(0, u256); list_mock SetAccountStorageHook ( 7162266444908917614 , 100 ) ukmNoResult(); -list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmInt256Result(9900); -list_mock GetAccountStorageHook ( 7162266444908917614 ) ukmInt256Result(100); +list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmIntResult(9900, u256); +list_mock GetAccountStorageHook ( 7162266444908917614 ) ukmIntResult(100, u256); list_mock SetAccountStorageHook ( 8028228613167873919 , 200 ) ukmNoResult(); -list_mock GetAccountStorageHook ( 8028228613167873919 ) ukmInt256Result(200); +list_mock GetAccountStorageHook ( 8028228613167873919 ) ukmIntResult(200, u256); list_mock SetAccountStorageHook ( 8028228613167873919 , 0 ) ukmNoResult(); -list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmInt256Result(9900); -list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmInt256Result(9900); +list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmIntResult(9900, u256); +list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmIntResult(9900, u256); list_mock SetAccountStorageHook ( 7162266444907899391 , 9700 ) ukmNoResult(); -list_mock GetAccountStorageHook ( 7162266444908917614 ) ukmInt256Result(100); +list_mock GetAccountStorageHook ( 7162266444908917614 ) ukmIntResult(100, u256); list_mock SetAccountStorageHook ( 7162266444908917614 , 300 ) ukmNoResult(); -list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmInt256Result(9700); -list_mock GetAccountStorageHook ( 7162266444908917614 ) ukmInt256Result(300); +list_mock GetAccountStorageHook ( 7162266444907899391 ) ukmIntResult(9700, u256); +list_mock GetAccountStorageHook ( 7162266444908917614 ) ukmIntResult(300, u256); call :: bytes_hooks :: empty; return_value_to_arg; diff --git a/tests/ukm-with-contract/storage.key.run b/tests/ukm-with-contract/storage.key.run index 129a218..a2e618d 100644 --- a/tests/ukm-with-contract/storage.key.run +++ b/tests/ukm-with-contract/storage.key.run @@ -1,5 +1,5 @@ mock SetAccountStorageHook ( 7010817630605304703 , 123 ) ukmNoResult(); -mock GetAccountStorageHook ( 7010817630605304703 ) ukmInt64Result(123); +mock GetAccountStorageHook ( 7010817630605304703 ) ukmIntResult(123, u64); call :: bytes_hooks :: empty; return_value_to_arg; diff --git a/tests/ukm-with-contract/storage.simple.run b/tests/ukm-with-contract/storage.simple.run index 72b139a..4648776 100644 --- a/tests/ukm-with-contract/storage.simple.run +++ b/tests/ukm-with-contract/storage.simple.run @@ -1,5 +1,5 @@ mock SetAccountStorageHook ( 1809217465971809 , 123 ) ukmNoResult(); -mock GetAccountStorageHook ( 1809217465971809 ) ukmInt64Result(123); +mock GetAccountStorageHook ( 1809217465971809 ) ukmIntResult(123, u64); call :: bytes_hooks :: empty; return_value_to_arg; diff --git a/ukm-semantics/main/hooks.md b/ukm-semantics/main/hooks.md index 934e5c0..1e930b3 100644 --- a/ukm-semantics/main/hooks.md +++ b/ukm-semantics/main/hooks.md @@ -4,6 +4,7 @@ requires "hooks/bytes.md" requires "hooks/helpers.md" requires "hooks/state.md" requires "hooks/ukm.md" +requires "ulm.k" module UKM-HOOKS imports private UKM-HOOKS-BYTES diff --git a/ukm-semantics/main/hooks/ukm.md b/ukm-semantics/main/hooks/ukm.md index fa02046..5246aba 100644 --- a/ukm-semantics/main/hooks/ukm.md +++ b/ukm-semantics/main/hooks/ukm.md @@ -8,15 +8,18 @@ module UKM-HOOKS-UKM-SYNTAX | SetAccountStorageHook(Int, Int) | GetAccountStorageHook(Int) + syntax K + syntax Type syntax UkmHookResult ::= ukmNoResult() - | ukmInt64Result(Int) - | ukmInt256Result(Int) + | ukmIntResult(Int, Type) endmodule module UKM-HOOKS-UKM imports private RUST-REPRESENTATION imports private RUST-SHARED-SYNTAX + imports private UKM-HOOKS-BYTES-SYNTAX + imports private UKM-HOOKS-SIGNATURE imports private UKM-HOOKS-UKM-SYNTAX syntax Identifier ::= "ukm" [token] @@ -53,14 +56,73 @@ module UKM-HOOKS-UKM => GetAccountStorageHook(MInt2Unsigned(Key)) rule ukmNoResult() => ptrValue(null, tuple(.ValueList)) + rule ukmIntResult(Value:Int, T:Type) => ukmValueResult(integerToValue(Value, T)) - syntax UkmHook ::= #ukmInt64Result(ValueOrError) - rule ukmInt64Result(Value:Int) => #ukmInt64Result(integerToValue(Value, u64)) - rule #ukmInt64Result(V:Value) => ptrValue(null, V) + syntax UkmHook ::= ukmValueResult(ValueOrError) + rule ukmValueResult(V:Value) => ptrValue(null, V) - syntax UkmHook ::= #ukmInt256Result(ValueOrError) - rule ukmInt256Result(Value:Int) => #ukmInt256Result(integerToValue(Value, u256)) - rule #ukmInt256Result(V:Value) => ptrValue(null, V) +endmodule + +// This module should be used only in kompilation targets which have implementations +// for the ULM hooks. +module UKM-HOOKS-TO-ULM-FUNCTIONS + imports private RUST-REPRESENTATION + imports private UKM-HOOKS-BYTES-SYNTAX + imports private UKM-HOOKS-UKM-SYNTAX + imports private ULM-HOOKS + + rule CallDataHook() => ukmBytesNew(CallData()) + rule CallerHook() => ukmIntResult(Caller(), u160) + rule SetAccountStorageHook(Key:Int, Value:Int) => SetAccountStorage(Key, Value) ~> ukmNoResult() + rule GetAccountStorageHook(Key:Int) => ukmIntResult(GetAccountStorage(Key), u256) +endmodule + +module UKM-HOOKS-SIGNATURE + imports private ULM-SIGNATURE + imports private UKM-HOOKS-STATE-CONFIGURATION + imports private UKM-TARGET-CONFIGURATION + + rule getOutput + ( + + + Value:Bytes + ... + + ... + + ... + + ) + => Value + + rule getStatus + ( + + + Value:Int + ... + + ... + + ... + + ) + => Value + + rule getGasLeft + ( + + + Value:Int + ... + + ... + + ... + + ) + => Value endmodule diff --git a/ukm-semantics/targets/execution/configuration.md b/ukm-semantics/targets/execution/configuration.md index c5d7b08..fd6f427 100644 --- a/ukm-semantics/targets/execution/configuration.md +++ b/ukm-semantics/targets/execution/configuration.md @@ -24,12 +24,10 @@ module UKM-TARGET-CONFIGURATION imports UKM-FULL-PREPROCESSED-CONFIGURATION configuration - - - - - - + + + + endmodule ``` diff --git a/ukm-semantics/targets/execution/ukm-target.md b/ukm-semantics/targets/execution/ukm-target.md index 819fc79..e0ad3d4 100644 --- a/ukm-semantics/targets/execution/ukm-target.md +++ b/ukm-semantics/targets/execution/ukm-target.md @@ -13,6 +13,7 @@ module UKM-TARGET imports private RUST-COMMON imports private UKM-DECODING imports private UKM-EXECUTION + imports private UKM-HOOKS-TO-ULM-FUNCTIONS imports private UKM-TARGET-CONFIGURATION endmodule diff --git a/ukm-semantics/targets/testing/configuration.md b/ukm-semantics/targets/testing/configuration.md index 7d3a7c8..37cc2ab 100644 --- a/ukm-semantics/targets/testing/configuration.md +++ b/ukm-semantics/targets/testing/configuration.md @@ -29,15 +29,13 @@ module UKM-TARGET-CONFIGURATION imports UKM-TEST-CONFIGURATION configuration - - - - - - - - - + + + + + + + endmodule ``` diff --git a/ukm-semantics/test/execution.md b/ukm-semantics/test/execution.md index 20f1a61..77956e4 100644 --- a/ukm-semantics/test/execution.md +++ b/ukm-semantics/test/execution.md @@ -14,6 +14,14 @@ module UKM-TEST-SYNTAX | "push_status" | "check_eq" Int | "expect_cancel" + + syntax Identifier ::= "u8" [token] + | "u16" [token] + | "u32" [token] + | "u64" [token] + | "u128" [token] + | "u160" [token] + | "u256" [token] endmodule module UKM-TEST-EXECUTION