From a973a08e5ff85c5bfc5c8343212f3b438e41490b Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Mon, 29 Jul 2024 11:40:46 +1000
Subject: [PATCH] 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 d8868937759cb51b0b8de22ff70c364770537607.

* Set Version: 0.1.106

---------

Co-authored-by: devops <devops@runtimeverification.com>
---
 kmultiversx/pyproject.toml                    |  2 +-
 .../kdist/mx-semantics/data/list-bytes.k      | 23 +++++--------------
 package/version                               |  2 +-
 3 files changed, 8 insertions(+), 19 deletions(-)

diff --git a/kmultiversx/pyproject.toml b/kmultiversx/pyproject.toml
index 47238412..d5b61e28 100644
--- 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.105"
+version = "0.1.106"
 description = "Python tools for Elrond semantics"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
diff --git a/kmultiversx/src/kmultiversx/kdist/mx-semantics/data/list-bytes.k b/kmultiversx/src/kmultiversx/kdist/mx-semantics/data/list-bytes.k
index 619e3ea1..ef0697ee 100644
--- a/kmultiversx/src/kmultiversx/kdist/mx-semantics/data/list-bytes.k
+++ b/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))
diff --git a/package/version b/package/version
index 23175873..9e3db2aa 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.1.105
+0.1.106