Pi-Squared-Inc · virgil-serbanuta · Oct 25, 2024 · Oct 25, 2024
diff --git a/tests/ukm-with-contract/erc_20_token.1.run b/tests/ukm-with-contract/erc_20_token.1.run
@@ -21,13 +21,11 @@ list_mock SetAccountStorageHook ( 7089066454179379067 , 300 ) ukmNoResult();
 list_mock GetAccountStorageHook ( 7089066454178295295 ) ukmIntResult(9700, u256);
 list_mock GetAccountStorageHook ( 7089066454179379067 ) ukmIntResult(300, u256);
 
-push "#init";
-hold_string_from_test_stack; 
 push "uint256";
 hold_list_values_from_test_stack; 
 push 10000_u256;
 hold_list_values_from_test_stack; 
-encode_call_data; 
+encode_constructor_data; 
 
 
 return_value;
@@ -36,7 +34,8 @@ mock CallData;
 push_value 1010101_u160;
 mock Caller;
 
-call_contract 12345;
+init_contract 12345;
+clear_pgm;
 return_value;
 check_eq ();
 

diff --git a/ukm-semantics/main/encoding/encoder.md b/ukm-semantics/main/encoding/encoder.md
@@ -67,6 +67,8 @@ module UKM-CALLDATA-ENCODER
     // 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) => 

diff --git a/ukm-semantics/main/encoding/syntax.md b/ukm-semantics/main/encoding/syntax.md
@@ -10,6 +10,7 @@ module UKM-ENCODING-SYNTAX
 
     // 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]

diff --git a/ukm-semantics/main/execution/dispatch.md b/ukm-semantics/main/execution/dispatch.md
@@ -1,29 +1,38 @@
 ```k
 
 module UKM-EXECUTION-DISPATCH
+    imports private BYTES-SYNTAX
     imports private COMMON-K-CELL
+    imports private K-EQUAL-SYNTAX
     imports private RUST-REPRESENTATION
     imports private RUST-VALUE-SYNTAX
     imports private RUST-EXECUTION-CONFIGURATION
     imports private UKM-COMMON-TOOLS-SYNTAX
     imports private UKM-EXECUTION-SYNTAX
     imports private UKM-PREPROCESSING-CONFIGURATION
 
-    syntax UkmInstruction ::= ukmExecute(contract:Value, gas: ValueOrError)
+    syntax UkmInstruction ::= ukmExecute(create: Bool, contract:Value, gas: ValueOrError)
 
     rule
         <k>
-            ukmExecute(_AccountId:Int, Gas:Int)
-            => ukmExecute(struct(ContractTrait, .Map), integerToValue(Gas, u64))
+            // TODO: For some reason, kompile rejects 'Create' as a variabler name below.
+            // Figure out why.
+            ukmExecute(Createy:Bool, Pgm:Bytes, _AccountId:Int, Gas:Int)
+            => ukmExecute(Createy, struct(ContractTrait, .Map), integerToValue(Gas, u64))
+              ~> #if Createy #then Pgm #else .K #fi
             ...
         </k>
         <ukm-contract-trait>
             ContractTrait:TypePath
         </ukm-contract-trait>
     rule
         <k>
-            ukmExecute(... contract: Contract:Value, gas: Gas:Value)
-            => ptr(NVI) . dispatcherMethodIdentifier ( ptrValue(null, Gas), .CallParamsList )
+            ukmExecute(... create: Createy:Bool, contract: Contract:Value, gas: Gas:Value)
+            => ptr(NVI) . dispatcherMethodIdentifier
+                  ( ptrValue(null, Createy)
+                  , ptrValue(null, Gas)
+                  , .CallParamsList
+                  )
             ...
         </k>
         <values> Values:Map => Values[NVI <- Contract] </values>

diff --git a/ukm-semantics/main/execution/syntax.md b/ukm-semantics/main/execution/syntax.md
@@ -1,9 +1,11 @@
 ```k
 
 module UKM-EXECUTION-SYNTAX
+    imports BOOL-SYNTAX
+    imports BYTES-SYNTAX
     imports INT-SYNTAX
 
-    syntax UKMInstruction ::= ukmExecute(accountId: Int, gas: Int)
+    syntax UKMInstruction ::= ukmExecute(create: Bool, pgm:Bytes, accountId: Int, gas: Int)
 
 endmodule
 

diff --git a/ukm-semantics/main/preprocessing/endpoints.md b/ukm-semantics/main/preprocessing/endpoints.md
@@ -117,22 +117,27 @@ module UKM-PREPROCESSING-ENDPOINTS
                         typePathToPathInExpression(append(TypePath, dispatcherMethodIdentifier))
                     </method-name>
                     <method-params>
-                        self : $selftype , gas : u64, .NormalizedFunctionParameterList
+                        self : $selftype , create : bool , gas : u64 , .NormalizedFunctionParameterList
                     </method-params>
                     <method-return-type> ():Type </method-return-type>
                     <method-implementation>
                         block({
                             .InnerAttributes
-                            concatNonEmptyStatements
-                                (   let buffer_id = :: ukm :: CallData();
-                                    let ( buffer_id | .PatternNoTopAlts
-                                        , signature | .PatternNoTopAlts
-                                        , .Patterns
-                                        ) = decodeSignature(buffer_id);
-                                    .NonEmptyStatements
-                                ,   signatureToCall(signature, keys_list(Signatures), Signatures, buffer_id, gas)
-                                    .NonEmptyStatements
-                                )
+                            let buffer_id = :: ukm :: CallData();
+                            if create {
+                                .InnerAttributes
+                                self . ukmWrap##init ( buffer_id , gas , .CallParamsList );
+                                .NonEmptyStatements
+                            } else {
+                                .InnerAttributes
+                                let ( buffer_id | .PatternNoTopAlts
+                                    , signature | .PatternNoTopAlts
+                                    , .Patterns
+                                    ) = decodeSignature(buffer_id);
+                                signatureToCall(signature, keys_list(Signatures), Signatures, buffer_id, gas)
+                                .NonEmptyStatements
+                            };
+                            .NonEmptyStatements
                         })
                     </method-implementation>
                     <method-outer-attributes> `emptyOuterAttributes`(.KList) </method-outer-attributes>
@@ -142,6 +147,7 @@ module UKM-PREPROCESSING-ENDPOINTS
         </methods>
 
     syntax Identifier ::= "buffer_id"  [token]
+                        | "create"  [token]
                         | "signature"  [token]
                         | "gas"  [token]
                         | "state_hooks"  [token]
@@ -170,6 +176,7 @@ module UKM-PREPROCESSING-ENDPOINTS
                         | "empty"  [token]
                         | "equals"  [token]
                         | "ukm"  [token]
+                        | "ukmWrap##init"  [token]
                         | "CallData"  [token]
                         | "EVMC_BAD_JUMP_DESTINATION"  [token]
                         | "EVMC_SUCCESS"  [token]

diff --git a/ukm-semantics/targets/execution/configuration.md b/ukm-semantics/targets/execution/configuration.md
@@ -13,7 +13,7 @@ module COMMON-K-CELL
     configuration
         <k>
             ukmDecodePreprocessedCell($PGM:Bytes)
-            ~> ukmExecute($ACCTCODE:Int, $GAS:Int)
+            ~> ukmExecute($CREATE:Bool, $PGM:Bytes, $ACCTCODE:Int, $GAS:Int)
         </k>
 endmodule
 

diff --git a/ukm-semantics/test/execution.md b/ukm-semantics/test/execution.md
@@ -25,7 +25,10 @@ module UKM-TEST-SYNTAX
                             | "list_mock" UkmHook UkmHookResult
                             | "encode_call_data"
                             | "encode_call_data_to_string"
+                            | "encode_constructor_data"
                             | "call_contract" Int
+                            | "init_contract" Int
+                            | "clear_pgm"
                             | "hold" KItem 
                             | "output_to_arg"
                             | "push_status"
@@ -56,7 +59,7 @@ module UKM-TEST-EXECUTION
     imports private UKM-HOOKS-UKM-SYNTAX
     imports private UKM-REPRESENTATION
     imports private UKM-TEST-SYNTAX
-    imports RUST-SHARED-SYNTAX
+    imports private RUST-SHARED-SYNTAX
     imports private BYTES
 
     syntax Mockable ::= UkmHook
@@ -111,6 +114,17 @@ module UKM-TEST-EXECUTION
             ...
          </k> [owise]
 
+    rule <k> encode_constructor_data
+             ~> list_values_holder ARGS , list_values_holder PTYPES , .UKMTestTypeHolderList
+             => ukmBytesNew(encodeConstructorData(PTYPES, ARGS)) 
+            ...
+         </k> 
+
+    rule <k> encode_constructor_data
+             => ukmBytesNew(encodeConstructorData(.List, .List)) 
+            ...
+         </k> [owise]
+
     rule
         <k> mock CallData => mock(CallDataHook(), V) ... </k>
         <test-stack>
@@ -128,7 +142,11 @@ 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)
+    rule call_contract Account => ukmExecute(false, .Bytes, Account, 100)
+
+    rule init_contract Account => ukmExecute(true, b"init", Account, 100)
+
+    rule (V:PtrValue ~> b"init" ~> clear_pgm) => V
 
     rule
         <k>