diff --git a/kmultiversx/pyproject.toml b/kmultiversx/pyproject.toml index a69f6311..ccf9e579 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.95" +version = "0.1.96" description = "Python tools for Elrond semantics" authors = [ "Runtime Verification, Inc. ", 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 f1de7b94..619e3ea1 100644 --- 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 rangeTotal(L, Front, 0) requires 0 <=Int Front andBool Back .ListBytes requires 0 <=Int Front - andBool 0 <=Int Back + andBool 0 <=Int Back andBool size(L)