From c2082375ca0cffd3f22fecab277a52bef017c80c Mon Sep 17 00:00:00 2001
From: Virgil <virgil.serbanuta@runtimeverification.com>
Date: Wed, 28 Aug 2024 20:06:31 +0300
Subject: [PATCH] MX getBlockTimestamp hook

---
 mx-semantics/main/blocks/configuration.md  | 15 +++++++++++++++
 mx-semantics/main/blocks/hooks.md          | 14 ++++++++++++++
 mx-semantics/main/configuration.md         |  3 +++
 mx-semantics/main/mx-common.md             |  2 ++
 mx-semantics/test/execution.md             | 13 +++++++++++++
 tests/mx/blockchain/get-block-timestamp.mx |  3 +++
 6 files changed, 50 insertions(+)
 create mode 100644 mx-semantics/main/blocks/configuration.md
 create mode 100644 mx-semantics/main/blocks/hooks.md
 create mode 100644 tests/mx/blockchain/get-block-timestamp.mx

diff --git a/mx-semantics/main/blocks/configuration.md b/mx-semantics/main/blocks/configuration.md
new file mode 100644
index 0000000..e41e471
--- /dev/null
+++ b/mx-semantics/main/blocks/configuration.md
@@ -0,0 +1,15 @@
+```k
+
+module MX-BLOCKS-CONFIGURATION
+    imports INT-SYNTAX
+
+    configuration
+        <mx-blocks>
+            <mx-current-block>
+                <mx-current-block-timestamp> 0 </mx-current-block-timestamp>
+            </mx-current-block>
+        </mx-blocks>
+
+endmodule
+
+```
diff --git a/mx-semantics/main/blocks/hooks.md b/mx-semantics/main/blocks/hooks.md
new file mode 100644
index 0000000..22c0362
--- /dev/null
+++ b/mx-semantics/main/blocks/hooks.md
@@ -0,0 +1,14 @@
+```k
+
+module MX-BLOCKS-HOOKS
+    imports private COMMON-K-CELL
+    imports private MX-BLOCKS-CONFIGURATION
+    imports private MX-COMMON-SYNTAX
+
+    rule
+        <k> MX#getBlockTimestamp ( .MxHookArgs ) => mxIntValue(T) ... </k>
+        <mx-current-block-timestamp> T </mx-current-block-timestamp>
+
+endmodule
+
+```
diff --git a/mx-semantics/main/configuration.md b/mx-semantics/main/configuration.md
index 668158a..c6f0195 100644
--- a/mx-semantics/main/configuration.md
+++ b/mx-semantics/main/configuration.md
@@ -2,17 +2,20 @@
 
 requires "accounts/configuration.md"
 requires "biguint/configuration.md"
+requires "blocks/configuration.md"
 requires "calls/configuration.md"
 
 module MX-COMMON-CONFIGURATION
     imports MX-ACCOUNTS-CONFIGURATION
     imports MX-BIGUINT-CONFIGURATION
+    imports MX-BLOCKS-CONFIGURATION
     imports MX-CALL-CONFIGURATION
 
     configuration
         <mx-common>
             <mx-call-data/>
             <mx-biguint/>
+            <mx-blocks/>
             <mx-accounts/>
         </mx-common>
 endmodule
diff --git a/mx-semantics/main/mx-common.md b/mx-semantics/main/mx-common.md
index 275e749..27bb479 100644
--- a/mx-semantics/main/mx-common.md
+++ b/mx-semantics/main/mx-common.md
@@ -2,11 +2,13 @@
 
 requires "accounts/hooks.md"
 requires "biguint/hooks.md"
+requires "blocks/hooks.md"
 requires "calls/hooks.md"
 
 module MX-COMMON
     imports private MX-ACCOUNTS-HOOKS
     imports private MX-BIGUINT-HOOKS
+    imports private MX-BLOCKS-HOOKS
     imports private MX-CALLS-HOOKS
 endmodule
 
diff --git a/mx-semantics/test/execution.md b/mx-semantics/test/execution.md
index 42546cc..cef680c 100644
--- a/mx-semantics/test/execution.md
+++ b/mx-semantics/test/execution.md
@@ -13,6 +13,7 @@ module MX-TEST-EXECUTION-PARSING-SYNTAX
                               | setCaller(String)
                               | addAccount(String)
                               | setBalance(account:String, token:String, nonce:Int, value:Int)
+                              | setBlockTimestamp(Int)
 
     syntax MxTest ::= NeList{TestInstruction, ";"}
 
@@ -24,6 +25,7 @@ module MX-TEST-EXECUTION
     imports private INT
     imports private MX-ACCOUNTS-TEST
     imports private MX-BIGUINT-TEST
+    imports private MX-BLOCKS-TEST
     imports private MX-CALL-TEST
     imports private MX-TEST-CONFIGURATION
     imports private MX-TEST-EXECUTION-PARSING-SYNTAX
@@ -151,4 +153,15 @@ module MX-ACCOUNTS-TEST
 
 endmodule
 
+module MX-BLOCKS-TEST
+    imports private COMMON-K-CELL
+    imports private MX-BLOCKS-CONFIGURATION
+    imports private MX-TEST-EXECUTION-PARSING-SYNTAX
+
+    rule
+        <k> setBlockTimestamp(T:Int) => .K ... </k>
+        <mx-current-block-timestamp> _ => T </mx-current-block-timestamp>
+
+endmodule
+
 ```
diff --git a/tests/mx/blockchain/get-block-timestamp.mx b/tests/mx/blockchain/get-block-timestamp.mx
new file mode 100644
index 0000000..fc9a5c7
--- /dev/null
+++ b/tests/mx/blockchain/get-block-timestamp.mx
@@ -0,0 +1,3 @@
+setBlockTimestamp(1234);
+call 0 MX#getBlockTimestamp;
+check_eq mxIntValue(1234)