Pi-Squared-Inc · ACassimiro · Oct 23, 2024 · Oct 17, 2024 · Oct 18, 2024 · Oct 19, 2024
diff --git a/.gitignore b/.gitignore
@@ -1,4 +1,5 @@
 .build
 .DS_store
+blockchain-k-plugin
 tmp
 tmp.*
diff --git a/.gitmodules b/.gitmodules
@@ -0,0 +1,3 @@
+[submodule "blockchain-k-plugin"]
+	path = blockchain-k-plugin
+	url = https://github.com/runtimeverification/blockchain-k-plugin
diff --git a/Makefile b/Makefile
@@ -184,23 +184,29 @@ $(MX_RUST_TWO_CONTRACTS_TESTING_TIMESTAMP): $(MX_SEMANTICS_FILES) $(RUST_SEMANTI
 $(UKM_EXECUTION_TIMESTAMP): $(UKM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES)
 	# Workaround for https://github.com/runtimeverification/k/issues/4141
 	-rm -r $(UKM_EXECUTION_KOMPILED)
-	$$(which kompile) ukm-semantics/targets/execution/ukm-target.md \
+	$$(which kompile) ukm-semantics/targets/execution/ukm-target.md  \
+			--hook-namespaces KRYPTO -ccopt -g -ccopt -std=c++17 -ccopt -lcrypto \
+			-ccopt -lsecp256k1 -ccopt -lssl -ccopt 'blockchain-k-plugin/build/krypto/lib/krypto.a' \
 			--emit-json -o $(UKM_EXECUTION_KOMPILED) \
 			-I . \
 			--debug
 
 $(UKM_PREPROCESSING_TIMESTAMP): $(UKM_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES)
 	# Workaround for https://github.com/runtimeverification/k/issues/4141
 	-rm -r $(UKM_PREPROCESSING_KOMPILED)
-	$$(which kompile) ukm-semantics/targets/preprocessing/ukm-target.md \
+	$$(which kompile) ukm-semantics/targets/preprocessing/ukm-target.md  \
+			--hook-namespaces KRYPTO -ccopt -g -ccopt -std=c++17 -ccopt -lcrypto \
+			-ccopt -lsecp256k1 -ccopt -lssl -ccopt 'blockchain-k-plugin/build/krypto/lib/krypto.a' \
 			--emit-json -o $(UKM_PREPROCESSING_KOMPILED) \
 			-I . \
 			--debug
 
 $(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 \
+	$$(which kompile) ukm-semantics/targets/testing/ukm-target.md  \
+			--hook-namespaces KRYPTO -ccopt -g -ccopt -std=c++17 -ccopt -lcrypto \
+			-ccopt -lsecp256k1 -ccopt -lssl -ccopt 'blockchain-k-plugin/build/krypto/lib/krypto.a' \
 			--emit-json -o $(UKM_TESTING_KOMPILED) \
 			-I . \
 			--debug

diff --git a/blockchain-k-plugin b/blockchain-k-plugin
diff --git a/tests/ukm-with-contract/endpoints.1.run b/tests/ukm-with-contract/endpoints.1.run
@@ -1,6 +1,6 @@
 call :: bytes_hooks :: empty;
 return_value_to_arg;
-push "myEndpoint(Uint64)";
+push "myEndpoint(uint64)";
 call :: bytes_hooks :: append_str;
 return_value_to_arg;
 push 123_u64;

diff --git a/tests/ukm-with-contract/endpoints.2.run b/tests/ukm-with-contract/endpoints.2.run
@@ -0,0 +1,9 @@
+push "myEndpoint";
+hold_string_from_test_stack;
+push "uint64";
+hold_list_values_from_test_stack;
+push 1_u64;
+hold_list_values_from_test_stack;
+mock EncodeOp;
+return_value;
+check_eq "81922854\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\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\x00\x01"
diff --git a/tests/ukm-with-contract/endpoints.3.run b/tests/ukm-with-contract/endpoints.3.run
@@ -0,0 +1,5 @@
+hold b"c6b6e179\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\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\x00\x01";
+mock DecodeOp;
+return_value;
+
+check_eq 3_u64
diff --git a/ukm-semantics/main/decoding.md b/ukm-semantics/main/decoding.md
@@ -1,8 +1,10 @@
 ```k
 
 requires "decoding/syntax.md"
+requires "decoding/decoder.md"
 
 module UKM-DECODING
+    imports UKM-CALLDATA-DECODER
 endmodule
 
 ```
diff --git a/ukm-semantics/main/decoding/decoder.md b/ukm-semantics/main/decoding/decoder.md
@@ -0,0 +1,75 @@
+```k
+
+module UKM-CALLDATA-DECODER
+    imports RUST-VALUE-SYNTAX
+    imports UKM-DECODING-SYNTAX
+    imports BYTES-HOOKED
+    imports BYTES-SYNTAX
+    imports private COMMON-K-CELL
+    imports private RUST-PREPROCESSING-CONFIGURATION
+    imports private UKM-PREPROCESSING-CONFIGURATION
+    imports private RUST-EXECUTION-CONFIGURATION
+    imports private RUST-REPRESENTATION
+    imports private RUST-CONVERSIONS-SYNTAX
+    imports INT
+
+    rule decodeCallData(D:Bytes) => 
+            UKMDecodedCallData1(decodeFunctionSignature(substrBytes(D, 0, 8)), decodeArguments(loadArgumentsFromHash(substrBytes(D, 0, 8)), substrBytes(D, 8, lengthBytes(D)), .List) )
+
+    // TODO: Self is being assigned to an integer 0. This should be fixed in case we need
+    // to make references to self within rust contracts
+    rule <k> UKMDecodedCallData1(P:PathInExpression, L:List)
+                => UKMDecodedCallData1(P, L)
+                    ~> UKMDecodedCallData2(P, ListItem(NextId)) 
+        ... </k> 
+        <next-value-id> NextId:Int => NextId +Int 1 </next-value-id>
+        <values> Values:Map => Values[NextId <- u64(Int2MInt(0))] </values> [priority(80)] 
+
+
+    rule <k> UKMDecodedCallData1(P:PathInExpression, L:List ListItem(ptrValue(_, V)))
+            ~> UKMDecodedCallData2(P:PathInExpression, PL:List)
+                => UKMDecodedCallData1(P, L)
+                    ~> UKMDecodedCallData2(P, ListItem(NextId) PL)  
+        ... </k> 
+        <next-value-id> NextId:Int => NextId +Int 1 </next-value-id>
+        <values> Values:Map => Values[NextId <- V] </values> [priority(70)]
+
+    rule <k> UKMDecodedCallData1(P:PathInExpression, .List)
+                => .K ... </k>         
+
+    rule <k> UKMDecodedCallData2(P:PathInExpression, L:List)
+                => UKMDecodedCallData(P:PathInExpression, listToPtrList(L)) ... </k>         
+
+    rule [[ decodeFunctionSignature(FuncSigHash:Bytes) => P ]]
+        <ukm-method-hash-to-signatures>
+            ... FuncSigHash |-> P:PathInExpression ...
+        </ukm-method-hash-to-signatures>
+
+    rule [[ loadArgumentsFromHash(FuncSigHash:Bytes) => loadArgumentsFromHash(P) ]]
+        <ukm-method-hash-to-signatures>
+            ... FuncSigHash |-> P:PathInExpression ...
+        </ukm-method-hash-to-signatures>
+
+    rule [[ loadArgumentsFromHash(Method:PathInExpression) => L ]]
+        <method-name> Method </method-name>
+        <method-params> (self : $selftype), L:NormalizedFunctionParameterList </method-params>
+
+    rule decodeArguments(((_ : T:Type), R):NormalizedFunctionParameterList, D:Bytes, L:List) => 
+        decodeArguments(R, substrBytes(D, 0, sizeOfType(T)), 
+            ListItem( convertKBytesToPtrValue (T, Bytes2Int ( substrBytes(D, 0, sizeOfType(T)), BE, Unsigned ) ) ) L ) 
+
+    rule decodeArguments(.NormalizedFunctionParameterList, _, L:List) => L
+
+    rule convertKBytesToPtrValue(u32, I:Int) => ptrValue(null, u32(Int2MInt(I)))
+    rule convertKBytesToPtrValue(i32, I:Int) => ptrValue(null, i32(Int2MInt(I)))
+    rule convertKBytesToPtrValue(i64, I:Int) => ptrValue(null, i64(Int2MInt(I)))
+    rule convertKBytesToPtrValue(u64, I:Int) => ptrValue(null, u64(Int2MInt(I)))
+    rule convertKBytesToPtrValue(u128, I:Int) => ptrValue(null, u128(Int2MInt(I)))
+
+    rule sizeOfType(i32)  => 32
+    rule sizeOfType(u32)  => 32
+    rule sizeOfType(u64)  => 64
+    rule sizeOfType(i64)  => 64
+    rule sizeOfType(u128) => 128    
+endmodule
+```
diff --git a/ukm-semantics/main/decoding/syntax.md b/ukm-semantics/main/decoding/syntax.md
@@ -2,9 +2,33 @@
 
 module UKM-DECODING-SYNTAX
     imports BYTES-SYNTAX
+    imports INT-SYNTAX
+    imports LIST
+    imports RUST-VALUE-SYNTAX
+    imports private RUST-REPRESENTATION
+
+    syntax UKMDecodedCallDataWrapper ::= UKMDecodedCallData1( PathInExpression , List ) 
+                                       | UKMDecodedCallData2( PathInExpression , List )
+                                       | UKMDecodedCallData ( PathInExpression , PtrListOrError) 
+                                       | decodeCallData(Bytes) [function] 
 
     syntax UKMInstruction ::= ukmDecodePreprocessedCell(Bytes)
 
+    syntax NormalizedFunctionParameterList ::= loadArgumentsFromHash(Bytes) [function]
+                                             | loadArgumentsFromHash(PathInExpression) [function]
+
+    syntax List ::= decodeCallDataArguments(Bytes) [function] 
+                   | decodeArguments(NormalizedFunctionParameterList, Bytes, List) [function]
+
+
+
+    syntax PathInExpression ::= decodeFunctionSignature(Bytes) [function] 
+
+    syntax PtrValue ::= convertKBytesToPtrValue(Type, Int) [function]
+
+    syntax Int ::= sizeOfType(Type) [function]
+
+
 endmodule
 
-```
+```
diff --git a/ukm-semantics/main/encoding.md b/ukm-semantics/main/encoding.md
@@ -1,8 +1,10 @@
 ```k
 
 requires "encoding/syntax.md"
+requires "encoding/encoder.md"
 
 module UKM-ENCODING
+    imports UKM-CALLDATA-ENCODER
 endmodule
 
 ```
diff --git a/ukm-semantics/main/encoding/encoder.md b/ukm-semantics/main/encoding/encoder.md
@@ -0,0 +1,75 @@
+```k
+requires "blockchain-k-plugin/plugin/krypto.md"
+
+module UKM-CALLDATA-ENCODER
+    imports private COMMON-K-CELL
+    imports private UKM-ENCODING-SYNTAX
+    imports private UKM-PREPROCESSING-ENDPOINTS
+    imports STRING
+    imports BYTES
+    imports INT
+    imports KRYPTO
+
+    syntax String ::= Identifier2String(Identifier)  [function, total, hook(STRING.token2string)]
+                    | Type2String(Type)  [function, total, hook(STRING.token2string)]
+
+    rule encodeFunctionSignature (P:PathInExpression, N:NormalizedFunctionParameterList) => 
+                encodeFunctionSignature(convertPathInExprToString(P), convertFuncParamListToStrList(N, .List), "")
+
+    rule convertPathInExprToString(( :: I:Identifier :: R:PathExprSegments):PathInExpression ) =>
+            convertPathInExprToString(R) [priority(80)]
+    rule convertPathInExprToString(( I:Identifier :: R:PathExprSegments):PathInExpression ) =>
+            convertPathInExprToString(R) [priority(80)]
+    rule convertPathInExprToString(( I:Identifier :: .PathExprSegments):PathInExpression ) =>
+            Identifier2String(I) [priority(70)]
+
+    rule convertFuncParamListToStrList(((self : _), N:NormalizedFunctionParameterList), .List) => 
+        convertFuncParamListToStrList( N, .List) [priority(60)]
+    rule convertFuncParamListToStrList(((_ : T:Type), N:NormalizedFunctionParameterList), L:List) =>
+        convertFuncParamListToStrList(N, L ListItem(signatureType(T))) [priority(70)]
+    rule convertFuncParamListToStrList(.NormalizedFunctionParameterList, L:List) => L
+
+    rule encodeCallData(FN:String, FAT:List, FAL:List) => 
+            encodeFunctionSignature(FN, FAT, "") +Bytes encodeFunctionParams(FAL, FAT, b"")  
+
+    // Function signature encoding
+    rule encodeFunctionSignature(FuncName:String, RL:List, "") => 
+            encodeFunctionSignature("", RL:List, FuncName +String "(") 
+
+    rule encodeFunctionSignature("", ListItem(FuncParam:String) RL:List, FS) => 
+                encodeFunctionSignature("", RL, FS +String FuncParam +String ",") [owise]
+
+    // The last param does not have a follow up comma
+    rule encodeFunctionSignature("", ListItem(FuncParam:String) .List, FS) => 
+                encodeFunctionSignature("", .List, FS +String FuncParam ) 
+
+    rule encodeFunctionSignature("", .List, FS) => String2Bytes(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
+
+
+    // Encoding of individual types
+
+    rule convertToKBytes(i8(V) , "int8") => Int2Bytes(8, MInt2Signed(V), BE:Endianness) 
+    rule convertToKBytes(u8(V) , "uint8") => Int2Bytes(8, MInt2Unsigned(V), BE:Endianness) 
+    rule convertToKBytes(i16(V), "int16") => Int2Bytes(16, MInt2Signed(V), BE:Endianness) 
+    rule convertToKBytes(u16(V), "uint16") => Int2Bytes(16, 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(64, MInt2Signed(V), BE:Endianness) 
+    rule convertToKBytes(u64(V), "uint64") => Int2Bytes(64, MInt2Unsigned(V), BE:Endianness) 
+    rule convertToKBytes(u128(V), "uint128") => Int2Bytes(128, MInt2Unsigned(V), BE:Endianness) 
+    rule convertToKBytes(true,  "bool") => Int2Bytes(8, 1, BE:Endianness) 
+    rule convertToKBytes(false, "bool") => Int2Bytes(8, 0, BE:Endianness)
+    // TODO: as we currently do not support u160 (addresses) or u256, we're converting them to u64 for now
+    rule convertToKBytes(u64(V), "uint256") => Int2Bytes(256, MInt2Unsigned(V), BE:Endianness) 
+    rule convertToKBytes(u64(V), "uint160") => Int2Bytes(160, MInt2Unsigned(V), BE:Endianness)  
+    rule convertToKBytes(u64(V), "address") => Int2Bytes(160, MInt2Unsigned(V), BE:Endianness)  
+
+endmodule
+
+```
diff --git a/ukm-semantics/main/encoding/syntax.md b/ukm-semantics/main/encoding/syntax.md
@@ -2,8 +2,20 @@
 
 module UKM-ENCODING-SYNTAX
     imports BYTES-SYNTAX
+    imports LIST
+    imports RUST-REPRESENTATION
 
     syntax UKMInstruction ::= "ukmEncodePreprocessedCell"
+
+    syntax Bytes ::= encodeFunctionSignature (PathInExpression, NormalizedFunctionParameterList) [function]
+
+    syntax String ::= convertPathInExprToString(PathInExpression) [function]
+    syntax List ::= convertFuncParamListToStrList(NormalizedFunctionParameterList, List) [function]
+
+    syntax Bytes ::= encodeCallData (String, List, List) [function] //Function name, argument types, argument list
+                   | encodeFunctionSignature (String, List, String) [function]
+                   | encodeFunctionParams (List, List, Bytes) [function]
+                   | convertToKBytes ( Value , String ) [function]
 
 endmodule
 

diff --git a/ukm-semantics/main/preprocessing/configuration.md b/ukm-semantics/main/preprocessing/configuration.md
@@ -8,6 +8,9 @@ module UKM-PREPROCESSING-CONFIGURATION
             <ukm-contract-trait>
                 (#token("not#initialized", "Identifier"):Identifier):TypePath
             </ukm-contract-trait>
+            <ukm-method-hash-to-signatures>
+                .Map
+            </ukm-method-hash-to-signatures>
         </ukm-preprocessed>
 endmodule
 

diff --git a/ukm-semantics/main/preprocessing/endpoints.md b/ukm-semantics/main/preprocessing/endpoints.md
@@ -180,10 +180,10 @@ module UKM-PREPROCESSING-ENDPOINTS
             )
         => concat(signatureType(T), concat(",", signatureTypes(Ps)))
 
-    rule signatureType(u8) => "Uint8"
-    rule signatureType(u16) => "Uint16"
-    rule signatureType(u32) => "Uint32"
-    rule signatureType(u64) => "Uint64"
+    rule signatureType(u8) => "uint8"
+    rule signatureType(u16) => "uint16"
+    rule signatureType(u32) => "uint32"
+    rule signatureType(u64) => "uint64"
     rule signatureType(T) => error("Unknown type in signatureType:", ListItem(T))
         [owise]
 

diff --git a/ukm-semantics/main/preprocessing/methods.md b/ukm-semantics/main/preprocessing/methods.md
@@ -5,7 +5,22 @@ module UKM-PREPROCESSING-METHODS
     imports private K-EQUAL-SYNTAX
     imports private RUST-CONVERSIONS-SYNTAX
     imports private RUST-PREPROCESSING-CONFIGURATION
+    imports private UKM-PREPROCESSING-CONFIGURATION
     imports private UKM-PREPROCESSING-SYNTAX-PRIVATE
+    imports private UKM-ENCODING-SYNTAX
+
+    rule <k>
+            ukmPreprocessMethodSignature(Method) => ukmPreprocessingStoreMethodSignature(encodeFunctionSignature(Method, L), Method) 
+            ...
+        </k>
+        <method-name> Method </method-name>
+        <method-params> L:NormalizedFunctionParameterList </method-params>
+
+    rule <k> ukmPreprocessingStoreMethodSignature(B:Bytes, P:PathInExpression) => .K ... </k> 
+        <ukm-method-hash-to-signatures>
+            STATE => STATE [ B <- P ]
+        </ukm-method-hash-to-signatures>
+
 
     rule ukmPreprocessMethods(_:TypePath, .List) => .K
     rule ukmPreprocessMethods(Trait:TypePath, ListItem(Name:Identifier) Methods:List)
@@ -20,7 +35,7 @@ module UKM-PREPROCESSING-METHODS
                 , method: MethodIdentifier
                 , fullMethodPath: Method
                 , endpointName: getEndpointName(Atts, MethodIdentifier)
-                )
+                ) ~> ukmPreprocessMethodSignature(Method)
             ...
         </k>
         <method-name> Method </method-name>

diff --git a/ukm-semantics/main/preprocessing/syntax.md b/ukm-semantics/main/preprocessing/syntax.md
@@ -10,11 +10,14 @@ module UKM-PREPROCESSING-SYNTAX-PRIVATE
     imports LIST
     imports RUST-REPRESENTATION
     imports RUST-SHARED-SYNTAX
+    imports private BYTES-SYNTAX
 
     syntax UKMInstruction ::= ukmPreprocessTraits(List)
                             | ukmPreprocessTrait(TypePath)
                             | ukmPreprocessMethods(trait: TypePath, List)
                             | ukmPreprocessMethod(trait: TypePath, methodId: Identifier, fullMethodPath: PathInExpression)
+                            | ukmPreprocessMethodSignature(PathInExpression)
+                            | ukmPreprocessingStoreMethodSignature(Bytes, PathInExpression)
                             | ukmPreprocessEndpoint
                                 ( trait: TypePath
                                 , method: Identifier

diff --git a/ukm-semantics/targets/testing/ukm-target.md b/ukm-semantics/targets/testing/ukm-target.md
@@ -1,5 +1,7 @@
 ```k
 
+requires "../../main/encoding.md"
+requires "../../main/decoding.md"
 requires "../../main/execution.md"
 requires "../../main/preprocessing.md"
 requires "../../test/execution.md"
@@ -19,6 +21,8 @@ module UKM-TARGET
     imports private RUST-FULL-PREPROCESSING
     imports private RUST-EXECUTION-TEST
     imports private UKM-EXECUTION
+    imports private UKM-ENCODING
+    imports private UKM-DECODING
     imports private UKM-PREPROCESSING
     imports private UKM-TARGET-CONFIGURATION
     imports private UKM-TEST-EXECUTION