Hotfix ListBytes:getOrDefault with List:get (#313)

* Use normal list indexing (`List[Idx]`, `LIST.get`) to define `ListBytes:getOrDefault`

To avoid recursion and element-wise list matching when we index into a `ListBytes`,
the hooked function for normal lists should be used.
We are already doing this for the `ListBytes:primitiveLookup` function.

For the case of `ListBytes:getOrDefault`, this means to either rewrite to an
expression backed by the `LIST.get` function, or to the default value when the
index is out of range.

* remove isBytes constraint from getBuffer rules (assume there are always bytes)

* Set Version: 0.1.102

* Revert "remove isBytes constraint from getBuffer rules (assume there are always bytes)"

This reverts commit d886893.

* Set Version: 0.1.106

---------

Co-authored-by: devops <[email protected]>

kmultiversx/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kmultiversx"
-version = "0.1.105"
+version = "0.1.106"
 description = "Python tools for Elrond semantics"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

kmultiversx/src/kmultiversx/kdist/mx-semantics/data/list-bytes.k

@@ -47,6 +47,12 @@ module LIST-BYTES-EXTENSIONS
 
   syntax WrappedBytes ::= ListBytes "[" Int "]" "orDefault" WrappedBytes
           [ function, total, symbol(ListBytes:getOrDefault) ]
+// ---------------------------------------------------------------------
+  rule L:ListBytes[I:Int] orDefault _:WrappedBytes => L[I]
+    requires 0 -Int size(L) <=Int I andBool I <Int size(L)
+
+  rule L:ListBytes[I:Int] orDefault D:WrappedBytes => D
+    requires notBool (0 -Int size(L) <=Int I andBool I <Int size(L))
 
   syntax Bytes ::= ListBytes "{{" Int "}}"
                  [function, symbol(ListBytes:primitiveLookup)]
@@ -60,23 +66,6 @@ module LIST-BYTES-EXTENSIONS
   rule L:ListBytes {{ I:Int }} orDefault Value:Bytes
       => unwrap( L [I] orDefault wrap(Value) )
 
-  rule ListItem(V:WrappedBytes) _:ListBytes [0] orDefault _:WrappedBytes
-      => V
-  rule _:ListBytes ListItem(V:WrappedBytes) [-1] orDefault _:WrappedBytes
-      => V
-  rule .ListBytes [_:Int] orDefault D:WrappedBytes => D
-
-  rule ListItem(_:WrappedBytes) L:ListBytes [I:Int] orDefault D:WrappedBytes
-      => L[I -Int 1] orDefault D
-    requires 0 <Int I
-  rule L:ListBytes ListItem(_:WrappedBytes) [I:Int] orDefault D:WrappedBytes
-      => L[I +Int 1] orDefault D
-    requires I <Int 0
-
-  rule L:ListBytes[I:Int] orDefault D:WrappedBytes => D
-    requires notBool (0 -Int size(L) <=Int I andBool I <Int size(L))
-    [simplification]
-
   syntax ListBytes ::= ListItemWrap( Bytes )
       [function, total, symbol(ListBytesItemWrap)]
   rule ListItemWrap( B:Bytes ) => ListItem(wrap(B))

package/version

@@ -1 +1 @@
-0.1.105
+0.1.106