tmp

Pi-Squared-Inc · Oct 25, 2024 · 9efbde7 · 9efbde7
1 parent 8a356c6
commit 9efbde7
Show file tree

Hide file tree

Showing 4 changed files with 11 additions and 5 deletions.
diff --git a/ukm-semantics/main/execution/dispatch.md b/ukm-semantics/main/execution/dispatch.md
@@ -1,7 +1,9 @@
 ```k
 
 module UKM-EXECUTION-DISPATCH
+    imports private BYTES-SYNTAX
     imports private COMMON-K-CELL
+    imports private K-EQUAL-SYNTAX
     imports private RUST-REPRESENTATION
     imports private RUST-VALUE-SYNTAX
     imports private RUST-EXECUTION-CONFIGURATION
@@ -13,8 +15,11 @@ module UKM-EXECUTION-DISPATCH
 
     rule
         <k>
-            ukmExecute(Createy:Bool, _AccountId:Int, Gas:Int)
+            // TODO: For some reason, kompile rejects 'Create' as a variabler name below.
+            // Figure out why.
+            ukmExecute(Createy:Bool, Pgm:Bytes, _AccountId:Int, Gas:Int)
             => ukmExecute(Createy, struct(ContractTrait, .Map), integerToValue(Gas, u64))
+              ~> #if Createy #then Pgm #else .K #fi
             ...
         </k>
         <ukm-contract-trait>

diff --git a/ukm-semantics/main/execution/syntax.md b/ukm-semantics/main/execution/syntax.md
@@ -2,9 +2,10 @@
 
 module UKM-EXECUTION-SYNTAX
     imports BOOL-SYNTAX
+    imports BYTES-SYNTAX
     imports INT-SYNTAX
 
-    syntax UKMInstruction ::= ukmExecute(create: Bool, accountId: Int, gas: Int)
+    syntax UKMInstruction ::= ukmExecute(create: Bool, pgm:Bytes, accountId: Int, gas: Int)
 
 endmodule
 

diff --git a/ukm-semantics/targets/execution/configuration.md b/ukm-semantics/targets/execution/configuration.md
@@ -13,7 +13,7 @@ module COMMON-K-CELL
     configuration
         <k>
             ukmDecodePreprocessedCell($PGM:Bytes)
-            ~> ukmExecute($CREATE, $ACCTCODE:Int, $GAS:Int)
+            ~> ukmExecute($CREATE:Bool, $PGM:Bytes, $ACCTCODE:Int, $GAS:Int)
         </k>
 endmodule
 

diff --git a/ukm-semantics/test/execution.md b/ukm-semantics/test/execution.md
@@ -141,9 +141,9 @@ module UKM-TEST-EXECUTION
     rule mock Hook:UkmHook Result:UkmHookResult => mock(Hook, Result)
     rule list_mock Hook:UkmHook Result:UkmHookResult => listMock(Hook, Result)
 
-    rule call_contract Account => ukmExecute(false, Account, 100)
+    rule call_contract Account => ukmExecute(false, .Bytes, Account, 100)
 
-    rule init_contract Account => ukmExecute(true, Account, 100)
+    rule init_contract Account => ukmExecute(true, b"init", Account, 100)
 
     rule
         <k>