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. ", 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 D + requires notBool (0 -Int size(L) <=Int I andBool I 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 L[I +Int 1] orDefault D - requires I D - requires notBool (0 -Int size(L) <=Int I andBool I 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