Booster improvements (#288)

* `startPrank` match: `getbuffer` => `#getBuffer` * `memLoad-zero-length` match * `appendToOutAccount` definedness of `_Map_` * add `preserves-definedness` * Set Version: 0.1.80 --------- Co-authored-by: devops <[email protected]>
runtimeverification · Jun 17, 2024 · a8a0d5d · a8a0d5d
1 parent 261cbeb
commit a8a0d5d
Show file tree

Hide file tree

Showing 7 changed files with 30 additions and 24 deletions.
diff --git a/kmultiversx/pyproject.toml b/kmultiversx/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kmultiversx"
-version = "0.1.79"
+version = "0.1.80"
 description = "Python tools for Elrond semantics"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/kmultiversx/src/kmultiversx/kdist/mx-semantics/elrond-config.md b/kmultiversx/src/kmultiversx/kdist/mx-semantics/elrond-config.md
@@ -117,8 +117,9 @@ module ELROND-CONFIG
       requires #signed(i32 , LENGTH) <Int 0
 
     rule [memLoad-zero-length]:
-        <instrs> #memLoad(_, 0) => .K ... </instrs>
+        <instrs> #memLoad(_, LENGTH) => .K ... </instrs>
         <bytesStack> STACK => .Bytes : STACK </bytesStack>
+      requires LENGTH ==Int 0
 
     rule [memLoad-bad-bounds]:
          <instrs> #memLoad(OFFSET, LENGTH) => #throwException(ExecutionFailed, "mem load: bad bounds") ... </instrs>

diff --git a/kmultiversx/src/kmultiversx/kdist/mx-semantics/elrond-node.md b/kmultiversx/src/kmultiversx/kdist/mx-semantics/elrond-node.md
@@ -156,23 +156,22 @@ Storage maps byte arrays to byte arrays.
     rule [appendToOutAccount]:
         <commands> appendToOutAccount(ACC, T) => .K ... </commands>
         <outputAccounts>
-          ...
-          ACC |-> (OA => appendToOutTransfers(OA, T))
-          ...
+          OAs => OAs [ ACC <- appendToOutTransfers(
+                                { OAs [ ACC ] orDefault OutputAccount(ACC, .List) }:>OutputAccount,
+                                T
+                              ) ]
         </outputAccounts>
       requires nonZeroOutputTransfer(T)
-      [priority(60)]
-
-    rule [appendToOutAccount-new-item]:
-        <commands> appendToOutAccount(ACC, T) => .K ... </commands>
-        <outputAccounts> OAs => OAs [ ACC <- OutputAccount(ACC, ListItem(T))] </outputAccounts>
-      requires nonZeroOutputTransfer(T)
-      [priority(61)]
+       andBool isOutputAccount( OAs [ ACC ] orDefault OutputAccount(ACC, .List) ) 
+      [priority(60), preserves-definedness]
+      // Preserving definedness
+      // - Map[_<-_], Map[_]orDefault_ and appendToOutTransfers are total
+      // - {_}:>OutputAccount is checked
 
     rule [appendToOutAccount-zero]:
         <commands> appendToOutAccount(_, T) => .K ... </commands>
       requires notBool nonZeroOutputTransfer(T)
-      [priority(61)]
+      [priority(60)]
 
     syntax TransferValue ::= Int            // EGLD transfer
                            | List

diff --git a/kmultiversx/src/kmultiversx/kdist/mx-semantics/kasmer.md b/kmultiversx/src/kmultiversx/kdist/mx-semantics/kasmer.md
@@ -588,36 +588,33 @@ Only the `#kasmerRunner` account can execute these commands/host functions.
 ```k
     rule [testapi-startPrank]:
         <instrs> hostCall ( "env" , "startPrank" , [ i32  .ValTypes ] -> [ .ValTypes ] )
-              => #startPrank(getBuffer(ADDR_HANDLE)) ...
+              => #getBuffer(ADDR_HANDLE)
+              ~> #startPrank ...
         </instrs>
         <locals>
           0 |-> <i32> ADDR_HANDLE
         </locals>
         <callee> #kasmerRunner </callee>
 
-    syntax InternalInstr ::= #startPrank(BytesResult)
+    syntax InternalInstr ::= "#startPrank"
  // -------------------------------------------------
     rule [startPrank]:
-        <instrs> #startPrank(ADDR:Bytes) => .K ... </instrs>
+        <instrs> #startPrank => .K ... </instrs>
+        <bytesStack> ADDR:Bytes : S => S </bytesStack>
         <callee> #kasmerRunner => ADDR </callee>
         <prank> false => true </prank>
 
     rule [startPrank-not-allowed]:
-        <instrs> #startPrank(_:Bytes)
+        <instrs> #startPrank
               => #throwException(ExecutionFailed, "Only the test contract can start a prank and the test contract can't start a prank while already pranking")
                  ...
         </instrs>
+        <bytesStack> _:Bytes : S => S </bytesStack>
         <callee> ADDR </callee>
         <prank> PRANK </prank>
       requires ADDR =/=K #kasmerRunner
         orBool PRANK
 
-    rule [startPrank-err]:
-        <instrs> #startPrank(Err(MSG))
-              => #throwException(ExecutionFailed, MSG)
-                 ...
-        </instrs>
-
     rule [testapi-stopPrank]:
         <instrs> hostCall ( "env" , "stopPrank" , [ .ValTypes ] -> [ .ValTypes ] )
               => .K ...

diff --git a/kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/manBufOps.md b/kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/manBufOps.md
@@ -169,6 +169,8 @@ module MANBUFOPS
          <locals> 0 |-> <i32> ARG_IDX  1 |-> <i32> DEST_IDX </locals>
          <callArgs> ARGS </callArgs>
       requires #validArgIdx(ARG_IDX, ARGS)
+      [preserves-definedness]
+      // Preserving definedness: #validArgIdx(_) ensures Map {{ }} is defined
 
  // extern int32_t   mBufferAppend(void* context, int32_t accumulatorHandle, int32_t dataHandle);
     rule <instrs> hostCall("env", "mBufferAppend", [ i32 i32 .ValTypes ] -> [ i32 .ValTypes ] ) 

diff --git a/kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/smallIntOps.md b/kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/smallIntOps.md
@@ -57,13 +57,20 @@ module SMALLINTOPS
                   ...
          </instrs>
          <locals> 0 |-> <i64> VALUE </locals>
+      requires definedUnsigned(i64, VALUE)
+      [preserves-definedness]
+      // Preserving definedness: definedUnsigned(_) ensures #unsigned(_) is defined
 
     // extern void smallIntFinishSigned(void* context, long long value);
     rule <instrs> hostCall("env", "smallIntFinishSigned", [ i64 .ValTypes ] -> [ .ValTypes ])
                => #appendToOut(Int2Bytes(#signed(i64, VALUE), BE, Signed))
                   ...
          </instrs>
          <locals> 0 |-> <i64> VALUE </locals>
+      requires definedSigned(i64, VALUE)
+      [preserves-definedness]
+      // Preserving definedness: definedSigned(_) ensures #signed(_) is defined
+
 
     // extern int32_t smallIntStorageStoreUnsigned(void *context, int32_t keyOffset, int32_t keyLength, long long value);
     rule <instrs> hostCall("env", "smallIntStorageStoreUnsigned", [ i32 i32 i64 .ValTypes ] -> [ i32 .ValTypes ])

diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.79
+0.1.80