From 97c33ebfb732d668cdaf1c69983d87cc88431bd9 Mon Sep 17 00:00:00 2001
From: Maria Kotsifakou <kotsifakou.maria@gmail.com>
Date: Tue, 5 Nov 2024 06:23:42 -0600
Subject: [PATCH] New module execute, in order to import expression.

---
 src/solidity.md | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/src/solidity.md b/src/solidity.md
index 7443c15..cf17b75 100644
--- a/src/solidity.md
+++ b/src/solidity.md
@@ -13,6 +13,7 @@ requires "plugin/krypto.md"
 module SOLIDITY-CONFIGURATION
   imports SOLIDITY-DATA
   imports SOLIDITY-SYNTAX
+  imports SOLIDITY-ULM-EXECUTE-SYNTAX
   imports BYTES
   imports K-EQUAL
   imports ULM
@@ -81,8 +82,28 @@ module SOLIDITY-CONFIGURATION
         <gas> $GAS:Int </gas>
       </exec>
 
+endmodule
+```
+
+```k
+module SOLIDITY-ULM-EXECUTE-SYNTAX
+  imports BOOL
+  imports BYTES
+
     syntax KItem ::= execute(Bool, Bytes)
 
+endmodule
+```
+
+```k
+module SOLIDITY-ULM-EXECUTE
+  imports SOLIDITY-CONFIGURATION
+  imports SOLIDITY-DATA
+  imports SOLIDITY-SYNTAX
+  imports SOLIDITY-EXPRESSION
+  imports BYTES
+  imports K-EQUAL
+
     // The active contract should be the last one in the list of contracts as
     // decoded by the provided $PGM.
     rule <k> execute(true, B) => List2Statements(INIT) ~> B </k>
@@ -289,6 +310,7 @@ module SOLIDITY
   imports SOLIDITY-STATEMENT
   imports SOLIDITY-FUNCTION-SELECTORS
   imports SOLIDITY-ULM-SIGNATURE-IMPLEMENTATION
+  imports SOLIDITY-ULM-EXECUTE
 
   rule <k> _:PragmaDefinition Ss:SourceUnits => Ss ...</k>
   rule S:SourceUnit Ss:SourceUnits => S ~> Ss