Define primitive ListBytes lookup using the hooked function (#306)

* Rewrite ListBytes:primitiveLookup to a hooked operation when defined * remove rule side conditions * Set Version: 0.1.96 --------- Co-authored-by: devops <[email protected]>
runtimeverification · Jul 16, 2024 · bf76305 · bf76305
1 parent 1a2c815
commit bf76305
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.95"
+version = "0.1.96"
 description = "Python tools for Elrond semantics"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/kmultiversx/src/kmultiversx/kdist/mx-semantics/data/list-bytes.k b/kmultiversx/src/kmultiversx/kdist/mx-semantics/data/list-bytes.k
@@ -52,6 +52,7 @@ module LIST-BYTES-EXTENSIONS
                  [function, symbol(ListBytes:primitiveLookup)]
 // -----------------------------------------------------------
   rule L:ListBytes {{ I:Int }} => unwrap( L[ I ] )
+       [preserves-definedness] // defined or undefined on both sides
 
   syntax Bytes ::= ListBytes "{{" Int "}}" "orDefault" Bytes
                  [ function, total, symbol(ListBytes:primitiveLookupOrDefault) ]
@@ -113,19 +114,19 @@ module LIST-BYTES-EXTENSIONS
 // ----------------------------------------------------------
   rule rangeTotal(L, Front, Back) => range(L, Front, Back)
     requires 0 <=Int Front
-     andBool 0 <=Int Back 
+     andBool 0 <=Int Back
      andBool size(L) >=Int Front +Int Back
 
   rule rangeTotal(L, Front, Back) => rangeTotal(L, 0, Back)
     requires Front <Int 0
-  
+
   rule rangeTotal(L, Front, Back) => rangeTotal(L, Front, 0)
     requires 0 <=Int Front
      andBool Back <Int 0
-  
+
   rule rangeTotal(L, Front, Back) => .ListBytes
     requires 0 <=Int Front
-     andBool 0 <=Int Back 
+     andBool 0 <=Int Back
      andBool size(L) <Int Front +Int Back
 
 endmodule
diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.95
+0.1.96