Revert "Merge branch 'main' into constant-lookup"

This reverts commit 5f1f5d9, reversing changes made to 5390063.
Pi-Squared-Inc · Sep 3, 2024 · 804d9d9 · 804d9d9
1 parent 5f1f5d9
commit 804d9d9
Show file tree

Hide file tree

Showing 24 changed files with 20 additions and 707 deletions.
diff --git a/Makefile b/Makefile
@@ -45,18 +45,12 @@ execution-test: $(EXECUTION_OUTPUTS)
 mx-test: $(MX_TESTING_OUTPUTS)
 
 $(RUST_PREPROCESSING_TIMESTAMP): $(RUST_SEMANTICS_FILES)
-	# Workaround for https://github.com/runtimeverification/k/issues/4141
-	-rm -r $(RUST_PREPROCESSING_KOMPILED)
-	$$(which kompile) rust-semantics/targets/preprocessing/rust.md --emit-json -o $(RUST_PREPROCESSING_KOMPILED) --debug
+	$$(which kompile) rust-semantics/targets/preprocessing/rust.md --emit-json -o $(RUST_PREPROCESSING_KOMPILED)
 
 $(RUST_EXECUTION_TIMESTAMP): $(RUST_SEMANTICS_FILES)
-	# Workaround for https://github.com/runtimeverification/k/issues/4141
-	-rm -r $(RUST_EXECUTION_KOMPILED)
-	$$(which kompile) rust-semantics/targets/execution/rust.md --emit-json -o $(RUST_EXECUTION_KOMPILED) --debug
+	$$(which kompile) rust-semantics/targets/execution/rust.md --emit-json -o $(RUST_EXECUTION_KOMPILED)
 
 $(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
 
 $(RUST_SYNTAX_OUTPUT_DIR)/%.rs-parsed: $(RUST_SYNTAX_INPUT_DIR)/%.rs $(RUST_PREPROCESSING_TIMESTAMP)

diff --git a/mx-semantics/main/accounts/configuration.md b/mx-semantics/main/accounts/configuration.md
@@ -24,11 +24,4 @@ module MX-ACCOUNTS-CONFIGURATION
 
 endmodule
 
-module MX-ACCOUNTS-STACK-CONFIGURATION
-    imports LIST
-
-    configuration
-        <mx-world-stack> .List </mx-world-stack>
-endmodule
-
 ```
diff --git a/mx-semantics/main/accounts/hooks.md b/mx-semantics/main/accounts/hooks.md
@@ -10,7 +10,7 @@ module MX-ACCOUNTS-HOOKS
                 ( mxStringValue(Owner:String)
                 , mxStringValue(TokenId:String)
                 , mxIntValue(Nonce:Int)
-                , .MxValueList
+                , .MxHookArgs
                 ) => MX#bigIntNew(mxIntValue(Balance)) ... </k>
         <mx-account-address> Owner </mx-account-address>
         <mx-esdt-id>
@@ -23,9 +23,9 @@ module MX-ACCOUNTS-HOOKS
     rule
         <k> MX#bigIntGetESDTExternalBalance
                 ( mxStringValue(Owner:String)
-                , mxStringValue(_TokenId:String)
-                , mxIntValue(_Nonce:Int)
-                , .MxValueList
+                , mxStringValue(TokenId:String)
+                , mxIntValue(Nonce:Int)
+                , .MxHookArgs
                 ) => MX#bigIntNew(mxIntValue(0)) ... </k>
         <mx-account-address> Owner </mx-account-address>
         [priority(100)]

diff --git a/mx-semantics/main/accounts/tools.md b/mx-semantics/main/accounts/tools.md
diff --git a/mx-semantics/main/blocks/hooks.md b/mx-semantics/main/blocks/hooks.md
@@ -6,7 +6,7 @@ module MX-BLOCKS-HOOKS
     imports private MX-COMMON-SYNTAX
 
     rule
-        <k> MX#getBlockTimestamp ( .MxValueList ) => mxIntValue(T) ... </k>
+        <k> MX#getBlockTimestamp ( .MxHookArgs ) => mxIntValue(T) ... </k>
         <mx-current-block-timestamp> T </mx-current-block-timestamp>
 
 endmodule

diff --git a/mx-semantics/main/calls/configuration.md b/mx-semantics/main/calls/configuration.md
@@ -1,27 +1,12 @@
 ```k
 
 module MX-CALL-CONFIGURATION
-    imports INT-SYNTAX
-    imports MX-COMMON-SYNTAX
-    imports STRING-SYNTAX
+    imports STRING
 
     configuration
         <mx-call-data>
-            <mx-callee> "" </mx-callee>
             <mx-caller> "" </mx-caller>
-            <mx-call-args> .MxValueList </mx-call-args>
-            <mx-egld-value> 0 </mx-egld-value>
-            <mx-esdt-transfers> .MxEsdtTransferList </mx-esdt-transfers>
-            <mx-gas-provided> 0 </mx-gas-provided>
-            <mx-gas-price> 0 </mx-gas-price>
         </mx-call-data>
 endmodule
 
-module MX-CALL-RESULT-CONFIGURATION
-    imports MX-COMMON-SYNTAX
-
-    configuration
-        <mx-call-result> .MxCallResult </mx-call-result>
-endmodule
-
 ```
diff --git a/mx-semantics/main/calls/hooks.md b/mx-semantics/main/calls/hooks.md
@@ -2,40 +2,13 @@
 
 module MX-CALLS-HOOKS
     imports private COMMON-K-CELL
-    imports private INT
     imports private MX-CALL-CONFIGURATION
-    imports private MX-CALL-TOOLS-SYNTAX
     imports private MX-COMMON-SYNTAX
-    imports private STRING
 
     rule
-        <k> MX#getCaller ( .MxValueList ) => mxStringValue(Caller) ... </k>
+        <k> MX#getCaller ( .MxHookArgs ) => mxStringValue(Caller) ... </k>
         <mx-caller> Caller:String </mx-caller>
 
-    rule
-        <k>
-            MX#managedMultiTransferESDTNFTExecute
-                ( mxStringValue(Destination:String)
-                , mxTransfersValue(Transfers:MxEsdtTransferList)
-                , mxIntValue(_Gas:Int)
-                , mxStringValue("")  // Function name
-                , mxListValue(.MxValueList)  // Other arguments
-                )
-            => (transferESDTs(Callee, Destination, Transfers) ~> mxIntValue(0))
-            ...
-        </k>
-        <mx-callee> Callee:String </mx-callee>
-
-    rule
-        MX#managedMultiTransferESDTNFTExecute
-            ( mxStringValue(Destination:String)
-            , mxTransfersValue(Transfers:MxEsdtTransferList)
-            , mxIntValue(GasLimit:Int)
-            , mxStringValue(FunctionName:String)
-            , mxListValue(Args:MxValueList)
-            )
-        => executeOnDestContext(Destination, 0, Transfers, GasLimit, FunctionName, Args)
-        requires 0 <Int lengthString(FunctionName)
 endmodule
 
 ```