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
+
+ ukmPreprocessEvent
+ (... fullMethodPath: Method:PathInExpression
+ , eventName: _EventName:String
+ )
+ => .K
+ ...
+
+ Method
+
+ empty => block({.InnerAttributes .NonEmptyStatements})
+
+ ()
+
+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
Atts:OuterAttributes
requires getEndpointName(Atts, MethodIdentifier) =/=K ""
andBool getStorageName(Atts) ==K ""
+ andBool getEventName(Atts) ==K ""
rule
ukmPreprocessMethod(_Trait:TypePath, MethodIdentifier:Identifier, Method:PathInExpression)
@@ -40,6 +41,21 @@ module UKM-PREPROCESSING-METHODS
Atts:OuterAttributes
requires getStorageName(Atts) =/=K ""
andBool getEndpointName(Atts, MethodIdentifier) ==K ""
+ andBool getEventName(Atts) ==K ""
+ rule
+
+ ukmPreprocessMethod(_Trait:TypePath, MethodIdentifier:Identifier, Method:PathInExpression)
+ => ukmPreprocessEvent
+ (... fullMethodPath: Method
+ , eventName: getEventName(Atts)
+ )
+ ...
+
+ Method
+ Atts:OuterAttributes
+ 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