From 7cd071b1c2a84ba2af99d3e5583b97936e24c95a Mon Sep 17 00:00:00 2001
From: Virgil <virgil.serbanuta@runtimeverification.com>
Date: Thu, 17 Oct 2024 16:39:21 +0300
Subject: [PATCH] Empty implementation for events

---
 tests/ukm-with-contract/events.1.run        | 20 +++++++++++++++
 tests/ukm-with-contract/events.rs           | 18 +++++++++++++
 ukm-semantics/main/preprocessing.md         |  2 ++
 ukm-semantics/main/preprocessing/events.md  | 25 ++++++++++++++++++
 ukm-semantics/main/preprocessing/methods.md | 28 +++++++++++++++++++++
 ukm-semantics/main/preprocessing/syntax.md  |  4 +++
 6 files changed, 97 insertions(+)
 create mode 100644 tests/ukm-with-contract/events.1.run
 create mode 100644 tests/ukm-with-contract/events.rs
 create mode 100644 ukm-semantics/main/preprocessing/events.md

diff --git a/tests/ukm-with-contract/events.1.run b/tests/ukm-with-contract/events.1.run
new file mode 100644
index 0000000..8c0c04b
--- /dev/null
+++ b/tests/ukm-with-contract/events.1.run
@@ -0,0 +1,20 @@
+call :: bytes_hooks :: empty;
+return_value_to_arg;
+push "logEvent(Uint64,Uint64)";
+call :: bytes_hooks :: append_str;
+return_value_to_arg;
+push 123_u64;
+call :: bytes_hooks :: append_u64;
+return_value_to_arg;
+push 555_u64;
+call :: bytes_hooks :: append_u64;
+return_value;
+mock CallData;
+
+call_contract 12345;
+return_value;
+check_eq ();
+
+push_status;
+check_eq 2
+
diff --git a/tests/ukm-with-contract/events.rs b/tests/ukm-with-contract/events.rs
new file mode 100644
index 0000000..44d2b7a
--- /dev/null
+++ b/tests/ukm-with-contract/events.rs
@@ -0,0 +1,18 @@
+#![no_std]
+
+#[allow(unused_imports)]
+use ukm::*;
+
+#[ukm::contract]
+pub trait Events {
+  #[event("MyEvent")]
+  fn my_event(&self, #[indexed] from: u64, value: u64);
+
+  #[init]
+  fn init(&self) {}
+
+  #[endpoint(logEvent)]
+  fn log_event(&self, from:u64, value: u64) {
+      self.my_event(from, value)
+  }
+}
diff --git a/ukm-semantics/main/preprocessing.md b/ukm-semantics/main/preprocessing.md
index f28192a..ce5ee3c 100644
--- a/ukm-semantics/main/preprocessing.md
+++ b/ukm-semantics/main/preprocessing.md
@@ -2,6 +2,7 @@
 
 requires "preprocessing/crates.md"
 requires "preprocessing/endpoints.md"
+requires "preprocessing/events.md"
 requires "preprocessing/methods.md"
 requires "preprocessing/storage.md"
 requires "preprocessing/syntax.md"
@@ -13,6 +14,7 @@ module UKM-PREPROCESSING
     imports private UKM-COMMON-TOOLS
     imports private UKM-PREPROCESSING-CRATES
     imports private UKM-PREPROCESSING-ENDPOINTS
+    imports private UKM-PREPROCESSING-EVENTS
     imports private UKM-PREPROCESSING-METHODS
     imports private UKM-PREPROCESSING-STORAGE
     imports private UKM-PREPROCESSING-TRAITS
diff --git a/ukm-semantics/main/preprocessing/events.md b/ukm-semantics/main/preprocessing/events.md
new file mode 100644
index 0000000..e8f9f29
--- /dev/null
+++ b/ukm-semantics/main/preprocessing/events.md
@@ -0,0 +1,25 @@
+```k
+
+module UKM-PREPROCESSING-EVENTS
+    imports private COMMON-K-CELL
+    imports private RUST-PREPROCESSING-CONFIGURATION
+    imports private UKM-PREPROCESSING-SYNTAX-PRIVATE
+
+    rule 
+        <k>
+            ukmPreprocessEvent
+                (... fullMethodPath: Method:PathInExpression
+                , eventName: _EventName:String
+                )
+            => .K
+            ...
+        </k>
+        <method-name> Method </method-name>
+        <method-implementation>
+            empty => block({.InnerAttributes .NonEmptyStatements})
+        </method-implementation>
+        <method-return-type> () </method-return-type>
+
+endmodule
+
+```
diff --git a/ukm-semantics/main/preprocessing/methods.md b/ukm-semantics/main/preprocessing/methods.md
index c09ecf3..e820f4a 100644
--- a/ukm-semantics/main/preprocessing/methods.md
+++ b/ukm-semantics/main/preprocessing/methods.md
@@ -27,6 +27,7 @@ module UKM-PREPROCESSING-METHODS
         <method-outer-attributes> Atts:OuterAttributes </method-outer-attributes>
         requires getEndpointName(Atts, MethodIdentifier) =/=K ""
             andBool getStorageName(Atts) ==K ""
+            andBool getEventName(Atts) ==K ""
     rule
         <k>
             ukmPreprocessMethod(_Trait:TypePath, MethodIdentifier:Identifier, Method:PathInExpression)
@@ -40,6 +41,21 @@ module UKM-PREPROCESSING-METHODS
         <method-outer-attributes> Atts:OuterAttributes </method-outer-attributes>
         requires getStorageName(Atts) =/=K ""
             andBool getEndpointName(Atts, MethodIdentifier) ==K ""
+            andBool getEventName(Atts) ==K ""
+    rule
+        <k>
+            ukmPreprocessMethod(_Trait:TypePath, MethodIdentifier:Identifier, Method:PathInExpression)
+            => ukmPreprocessEvent
+                (... fullMethodPath: Method
+                , eventName: getEventName(Atts)
+                )
+            ...
+        </k>
+        <method-name> Method </method-name>
+        <method-outer-attributes> Atts:OuterAttributes </method-outer-attributes>
+        requires getEventName(Atts) =/=K ""
+            andBool getEndpointName(Atts, MethodIdentifier) ==K ""
+            andBool getStorageName(Atts) ==K ""
     rule ukmPreprocessMethod(_:TypePath, _:Identifier, _:PathInExpression) => .K
         [owise]
 
@@ -91,6 +107,18 @@ module UKM-PREPROCESSING-METHODS
         => getStorageName(Atts)
         [owise]
 
+    syntax String ::= getEventName(atts:OuterAttributes)  [function, total]
+    rule getEventName() => ""
+    rule getEventName(.NonEmptyOuterAttributes) => ""
+    rule getEventName
+            (   (#[ #token("event", "Identifier") :: .SimplePathList
+                    ( Name:String, .CallParamsList )
+                ])
+                _:NonEmptyOuterAttributes
+            ) => Name
+    rule getEventName(_:OuterAttribute Atts:NonEmptyOuterAttributes)
+        => getEventName(Atts)
+        [owise]
 endmodule
 
 ```
diff --git a/ukm-semantics/main/preprocessing/syntax.md b/ukm-semantics/main/preprocessing/syntax.md
index a4a4dcc..c186d6d 100644
--- a/ukm-semantics/main/preprocessing/syntax.md
+++ b/ukm-semantics/main/preprocessing/syntax.md
@@ -46,6 +46,10 @@ module UKM-PREPROCESSING-SYNTAX-PRIVATE
                                   , mapperValueType: Type
                                   , appendParamsInstructions: NonEmptyStatementsOrError
                                   )
+                            | ukmPreprocessEvent
+                                ( fullMethodPath: PathInExpression
+                                , eventName: String
+                                )
 
 endmodule