Fix fallback on bigIntSign (#289)

* `bigIntSign`: pattern match to lookup * Set Version: 0.1.81 * Set Version: 0.1.82 --------- Co-authored-by: devops <[email protected]>
runtimeverification · Jun 20, 2024 · d531b4d · d531b4d
1 parent 65628e8
commit d531b4d
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 6 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.81"
+version = "0.1.82"
 description = "Python tools for Elrond semantics"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/bigIntOps.md b/kmultiversx/src/kmultiversx/kdist/mx-semantics/vmhooks/bigIntOps.md
@@ -341,16 +341,17 @@ module BIGINTOPS
 
     // extern int32_t bigIntSign(void* context, int32_t op);
     rule <instrs> hostCall("env", "bigIntSign", [ i32 .ValTypes ] -> [ i32 .ValTypes ])
-               => i32.const #bigIntSign(V)
+               => i32.const #bigIntSign(HEAP{{IDX}} orDefault 0)
                   ...
          </instrs>
          <locals> 0 |-> <i32> IDX </locals>
-         <bigIntHeap> ... wrap(IDX) Int2Int|-> wrap(V) </bigIntHeap>
-      [preserves-definedness]
+         <bigIntHeap> HEAP </bigIntHeap>
+      requires IDX in_keys{{HEAP}}
+      [preserves-definedness] // TODO maybe we don't need this anymore since everything is total
       // Preserving definedness:
       //  - #bigIntSign is total
       //  - in_keys is total
-      //  - _{{_ <- _}} is total
+      //  - _{{_}} orDefault _ is total
 
     rule <instrs> hostCall("env", "bigIntSign", [ i32 .ValTypes ] -> [ i32 .ValTypes ])
                => #throwException(ExecutionFailed, "no bigInt under the given handle")

diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.81
+0.1.82