Pi-Squared-Inc · virgil-serbanuta · Oct 22, 2024 · Oct 21, 2024
diff --git a/.gitmodules b/.gitmodules
diff --git 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
@@ -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
@@ -116,6 +116,7 @@ module RUST-EXECUTION-TEST
     rule
         <k> listMock(Mocked:Mockable, Result:K) => .K ... </k>
         <mock-list> L:List => L ListItem(listMock(Mocked, Result)) </mock-list>
+        [priority(10)]
 
     rule
         <k> (Mocked:Mockable => Result) ...</k>

diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
+            (   <generatedTop>
+                    <ukm>
+                        <ukm-state>
+                            <ukm-output> Value:Bytes </ukm-output>
+                            ...
+                        </ukm-state>
+                        ...
+                    </ukm>
+                    ...
+                </generatedTop>
+            )
+        => Value
+
+    rule getStatus
+            (   <generatedTop>
+                    <ukm>
+                        <ukm-state>
+                            <ukm-status> Value:Int </ukm-status>
+                            ...
+                        </ukm-state>
+                        ...
+                    </ukm>
+                    ...
+                </generatedTop>
+            )
+        => Value
+
+    rule getGasLeft
+            (   <generatedTop>
+                    <ukm>
+                        <ukm-state>
+                            <ukm-gas> Value:Int </ukm-gas>
+                            ...
+                        </ukm-state>
+                        ...
+                    </ukm>
+                    ...
+                </generatedTop>
+            )
+        => Value
 
 endmodule
 

diff --git 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
-        <ukm-target>
-            <ukm-full-preprocessed/>
-            <ukm/>
-            <execution/>
-            <k/>
-        </ukm-target>
+        <ukm-full-preprocessed/>
+        <ukm/>
+        <execution/>
+        <k/>
 endmodule
 
 ```
diff --git 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
@@ -29,15 +29,13 @@ module UKM-TARGET-CONFIGURATION
     imports UKM-TEST-CONFIGURATION
 
     configuration
-        <ukm-target>
-            <ukm-full-preprocessed/>
-            <ukm-preprocessing-ephemeral/>
-            <ukm/>
-            <ukm-test/>
-            <rust-test/>
-            <execution/>
-            <k/>
-        </ukm-target>
+        <ukm-full-preprocessed/>
+        <ukm-preprocessing-ephemeral/>
+        <ukm/>
+        <ukm-test/>
+        <rust-test/>
+        <execution/>
+        <k/>
 endmodule
 
 ```