Merge branch 'main' into multiencoded-cev

Pi-Squared-Inc · Sep 30, 2024 · 703c3a0 · 703c3a0
2 parents 5613c86 + 950fb75
commit 703c3a0
Show file tree

Hide file tree

Showing 12 changed files with 238 additions and 105 deletions.
diff --git a/Makefile b/Makefile
@@ -94,37 +94,37 @@ $(RUST_EXECUTION_TIMESTAMP): $(RUST_SEMANTICS_FILES)
 $(MX_TESTING_TIMESTAMP): $(MX_SEMANTICS_FILES)
 	# Workaround for https://github.com/runtimeverification/k/issues/4141
 	-rm -r $(MX_TESTING_KOMPILED)
-	$$(which kompile) mx-semantics/targets/testing/mx.md -o $(MX_TESTING_KOMPILED) --debug
+	$$(which kompile) mx-semantics/targets/testing/mx.md --emit-json -o $(MX_TESTING_KOMPILED) --debug
 
 $(MX_RUST_TIMESTAMP): $(MX_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) $(MX_RUST_SEMANTICS_FILES)
 	# Workaround for https://github.com/runtimeverification/k/issues/4141
 	-rm -r $(MX_RUST_KOMPILED)
 	$$(which kompile) mx-rust-semantics/targets/blockchain/mx-rust.md \
-			-o $(MX_RUST_KOMPILED) \
+			--emit-json -o $(MX_RUST_KOMPILED) \
 			-I . \
 			--debug
 
 $(MX_RUST_TESTING_TIMESTAMP): $(MX_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) $(MX_RUST_SEMANTICS_FILES)
 	# Workaround for https://github.com/runtimeverification/k/issues/4141
 	-rm -r $(MX_RUST_TESTING_KOMPILED)
 	$$(which kompile) mx-rust-semantics/targets/testing/mx-rust.md \
-			-o $(MX_RUST_TESTING_KOMPILED) \
+			--emit-json -o $(MX_RUST_TESTING_KOMPILED) \
 			-I . \
 			--debug
 
 $(MX_RUST_CONTRACT_TESTING_TIMESTAMP): $(MX_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) $(MX_RUST_SEMANTICS_FILES)
 	# Workaround for https://github.com/runtimeverification/k/issues/4141
 	-rm -r $(MX_RUST_CONTRACT_TESTING_KOMPILED)
 	$$(which kompile) mx-rust-semantics/targets/contract-testing/mx-rust.md \
-			-o $(MX_RUST_CONTRACT_TESTING_KOMPILED) \
+			--emit-json -o $(MX_RUST_CONTRACT_TESTING_KOMPILED) \
 			-I . \
 			--debug
 
 $(MX_RUST_TWO_CONTRACTS_TESTING_TIMESTAMP): $(MX_SEMANTICS_FILES) $(RUST_SEMANTICS_FILES) $(MX_RUST_SEMANTICS_FILES)
 	# Workaround for https://github.com/runtimeverification/k/issues/4141
 	-rm -r $(MX_RUST_TWO_CONTRACTS_TESTING_KOMPILED)
 	$$(which kompile) mx-rust-semantics/targets/two-contracts-testing/mx-rust.md \
-			-o $(MX_RUST_TWO_CONTRACTS_TESTING_KOMPILED) \
+			--emit-json -o $(MX_RUST_TWO_CONTRACTS_TESTING_KOMPILED) \
 			-I . \
 			--debug
 

diff --git a/mx-rust-semantics/main/modules.md b/mx-rust-semantics/main/modules.md
@@ -2,6 +2,7 @@
 
 requires "modules/address.md"
 requires "modules/biguint.md"
+requires "modules/blockchain.md"
 requires "modules/call-value.md"
 requires "modules/hooks.md"
 requires "modules/managed-vec.md"
@@ -14,6 +15,7 @@ requires "modules/token-identifier.md"
 module MX-RUST-MODULES
     imports private MX-RUST-MODULES-ADDRESS
     imports private MX-RUST-MODULES-BIGUINT
+    imports private MX-RUST-MODULES-BLOCKCHAIN
     imports private MX-RUST-MODULES-CALL-VALUE
     imports private MX-RUST-MODULES-HOOKS
     imports private MX-RUST-MODULES-MANAGED-VEC

diff --git a/mx-rust-semantics/main/modules/blockchain.md b/mx-rust-semantics/main/modules/blockchain.md
@@ -0,0 +1,55 @@
+```k
+
+module MX-RUST-MODULES-BLOCKCHAIN
+    imports private COMMON-K-CELL
+    imports private MX-COMMON-SYNTAX
+    imports private MX-RUST-REPRESENTATION
+    imports private MX-RUST-REPRESENTATION-CONVERSIONS
+    imports private RUST-EXECUTION-CONFIGURATION
+    imports private RUST-SHARED-SYNTAX
+
+    syntax Identifier ::= "MxRust#Blockchain"  [token]
+
+    syntax MxRustStructType ::= "blockchainType"  [function, total]
+    rule blockchainType
+        => rustStructType
+            ( MxRust#Blockchain
+            , .MxRustStructFields
+            )
+
+    rule
+        normalizedMethodCall
+            ( MxRust#Blockchain
+            , #token("new", "Identifier"):Identifier
+            , .PtrList
+            )
+        =>  mxRustNewStruct
+                ( blockchainType
+                , .CallParamsList
+                )
+
+    rule
+        normalizedMethodCall
+            ( MxRust#Blockchain
+            , #token("get_caller", "Identifier"):Identifier
+            ,   ( ptr(_SelfId:Int)
+                , .PtrList
+                )
+            )
+        => MX#getCaller ( .MxValueList )
+            ~> mxValueToRust(#token("ManagedAddress", "Identifier"):Identifier)
+
+    rule
+        normalizedMethodCall
+            ( MxRust#Blockchain
+            , #token("get_block_timestamp", "Identifier"):Identifier
+            ,   ( ptr(_SelfId:Int)
+                , .PtrList
+                )
+            )
+        => MX#getBlockTimestamp ( .MxValueList )
+            ~> mxValueToRust(u64)
+
+endmodule
+
+```
diff --git a/mx-rust-semantics/main/preprocessing/contract.md b/mx-rust-semantics/main/preprocessing/contract.md
@@ -7,6 +7,7 @@ module MX-RUST-PREPROCESSING-CONTRACT
 
     syntax MxRustInstruction  ::= rustMxAddContractSend(TypePath)
                                 | rustMxAddContractCallValue(TypePath)
+                                | rustMxAddContractBlockchain(TypePath)
                                 | rustMxAddContractGenericMethod
                                     ( trait: TypePath
                                     , method: Identifier
@@ -16,6 +17,7 @@ module MX-RUST-PREPROCESSING-CONTRACT
     rule rustMxAddContractMethods(Trait:TypePath)
         => rustMxAddContractSend(Trait:TypePath)
             ~> rustMxAddContractCallValue(Trait:TypePath)
+            ~> rustMxAddContractBlockchain(Trait:TypePath)
 
     rule rustMxAddContractSend(Trait:TypePath)
         => rustMxAddContractGenericMethod
@@ -31,6 +33,13 @@ module MX-RUST-PREPROCESSING-CONTRACT
             , struct: #token("MxRust#CallValue", "Identifier")
             )
 
+    rule rustMxAddContractBlockchain(Trait:TypePath)
+        => rustMxAddContractGenericMethod
+            (... trait: Trait
+            , method: #token("blockchain", "Identifier")
+            , struct: #token("MxRust#Blockchain", "Identifier")
+            )
+
     rule
         <k>
             rustMxAddContractGenericMethod