fix prank in Stylus

package/version

@@ -1 +1 @@
-0.1.26
+0.1.27

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "hatchling.build"
 
 [project]
 name = "skribe"
-version = "0.1.26"
+version = "0.1.27"
 description = "Property testing for Stylus smart contracts"
 readme = "README.md"
 requires-python = "~=3.10"

src/skribe/kdist/stylus-semantics/hostfuns.md

@@ -449,17 +449,24 @@ This is just a tracing (no-op) function.
               => #waitCommands
                  ...
         </instrs>
-        <k> (.K => #accessAccounts ACCTTO
-                ~> #checkCall ACCTFROM VALUE
-                ~> #call ACCTFROM ACCTTO ACCTTO VALUE VALUE DATA false
-                ~> #returnStylus RET_LEN_PTR
-            ) 
+        <k> (.K => #callStylus ACCTTO ACCTTO VALUE VALUE DATA false RET_LEN_PTR ) 
           ~> #endWasm ... 
         </k>
         <stylusStack> ACCTTO : (DATA : VALUE : RET_LEN_PTR : S) => S </stylusStack>
-        <id> ACCTFROM </id>
 
 
+    syntax InternalCmd ::= "#callStylus" Int Int Int Int Bytes Bool Int
+ // ------------------------------------
+    rule [callStylus]:
+        <k> #callStylus ACCTTO ACCTCODE VALUE APPVALUE ARGS STATIC RET_LEN_PTR
+         => #accessAccounts ACCTTO
+         ~> #checkCall ACCTFROM VALUE
+         ~> #call ACCTFROM ACCTTO ACCTTO VALUE APPVALUE ARGS STATIC
+         ~> #returnStylus RET_LEN_PTR
+            ...
+        </k>
+        <id> ACCTFROM </id>
+
     syntax InternalCmd ::= "#returnStylus" Int
  // ------------------------------------------
     rule [halt-returnStylus.success]:
@@ -508,15 +515,10 @@ This is just a tracing (no-op) function.
               => #waitCommands
                  ...
         </instrs>
-        <k> (.K => #accessAccounts ACCTTO
-                ~> #checkCall ACCTFROM 0
-                ~> #call ACCTFROM ACCTTO ACCTTO 0 0 DATA false
-                ~> #returnStylus RET_LEN_PTR
-            ) 
+        <k> (.K => #callStylus ACCTTO ACCTTO 0 0 DATA true RET_LEN_PTR )
           ~> #endWasm ... 
         </k>
         <stylusStack> ACCTTO : (DATA : RET_LEN_PTR : S) => S </stylusStack>
-        <id> ACCTFROM </id>
 
 ```
 

src/skribe/kdist/stylus-semantics/skribe.md

@@ -159,6 +159,31 @@ module SKRIBE
         </instrs>
         <output> OUT </output>
 
+```
+
+### Pranks
+
+```k
+    rule [stylus.prank]:
+         <k> #callStylus ACCTTO ACCTCODE VALUE APPVALUE ARGS STATIC RET_LEN_PTR
+          => #injectPrank
+          ~> #callStylus ACCTTO ACCTCODE VALUE APPVALUE ARGS STATIC RET_LEN_PTR
+          ~> #endPrank
+             ...
+         </k>
+         <callDepth> CD </callDepth>
+         <id> ACCT </id>
+         <prank>
+           <active> true </active>
+           <newCaller> NCL </newCaller>
+           <depth> CD </depth>
+           ...
+         </prank>
+      requires ACCT =/=K NCL
+       andBool ACCTTO =/=K #address(FoundryCheat)
+      [priority(34)]
+
+
 endmodule
 ```