From 80b6e07a21669cbbaf236c15e9127911b0a75410 Mon Sep 17 00:00:00 2001
From: Noah Watson <107630091+nwatson22@users.noreply.github.com>
Date: Tue, 4 Jun 2024 05:01:54 -0500
Subject: [PATCH] Change formula for #sizeOfDynamicType(#array) (#2455)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* Change formula for #sizeOfDynamicType(#array)

* Set Version: 1.0.580

* Add test

* Set Version: 1.0.581

* Set Version: 1.0.584

* Set Version: 1.0.585

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: Andrei Văcaru <16517508+anvacaru@users.noreply.github.com>
---
 kevm-pyk/pyproject.toml                       |  2 +-
 kevm-pyk/src/kevm_pyk/__init__.py             |  2 +-
 .../src/kevm_pyk/kproj/evm-semantics/abi.md   |  4 ++--
 package/version                               |  2 +-
 tests/specs/functional/abi-spec.k             | 22 +++++++++++++++++++
 5 files changed, 27 insertions(+), 5 deletions(-)

diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml
index 352dbbc43e..c500be701e 100644
--- a/kevm-pyk/pyproject.toml
+++ b/kevm-pyk/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.584"
+version = "1.0.585"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py
index 5b21805eea..dbab82e2fd 100644
--- a/kevm-pyk/src/kevm_pyk/__init__.py
+++ b/kevm-pyk/src/kevm_pyk/__init__.py
@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '1.0.584'
+VERSION: Final = '1.0.585'
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/abi.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/abi.md
index 9db573e05b..420cd0548a 100644
--- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/abi.md
+++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/abi.md
@@ -321,7 +321,7 @@ For most types, this is a fixed 32 bytes, except for static tuples, for which th
  - for `#bytes(BS)` and `#string(BS)`, the size is 32 bytes for the length prefix plus the size of the actual byte sequence, rounded up to the nearest multiple of 32.
  - for `#tuple(ARGS)`, the size is 32 bytes for the length prefix plus the cumulative size of its elements.
  - for `#array(T, N, _)` that has elements of a static `TypedArg` `T`, the size is `32 * (1 + N)`,which accounts for 32 bytes for the length prefix and 32 bytes for each element.
- - for dynamic type arrays `#array(T, N, ELEMS)`, the size is `32 * (1 + N + #sizeOfDynamicTypeList(ELEMS))`.
+ - for dynamic type arrays `#array(T, N, ELEMS)`, the size is `32 * (1 + N) + #sizeOfDynamicTypeList(ELEMS)`.
 
 ```k
     syntax Int ::= #sizeOfDynamicType ( TypedArg ) [klabel(#sizeOfDynamicType), function]
@@ -332,7 +332,7 @@ For most types, this is a fixed 32 bytes, except for static tuples, for which th
     rule #sizeOfDynamicType(#array(T, N, _)) => 32 *Int (1 +Int N)
       requires #isStaticType(T)
 
-    rule #sizeOfDynamicType(#array(T, N, ELEMS)) => 32 *Int (1 +Int N +Int #sizeOfDynamicTypeList(ELEMS))
+    rule #sizeOfDynamicType(#array(T, N, ELEMS)) => (32 *Int (1 +Int N)) +Int #sizeOfDynamicTypeList(ELEMS)
       requires notBool #isStaticType(T)
 
     syntax Int ::= #sizeOfDynamicTypeList ( TypedArgs ) [klabel(#sizeOfDynamicTypeList), function, total]
diff --git a/package/version b/package/version
index c4fba1744f..4d1a4dc836 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-1.0.584
+1.0.585
diff --git a/tests/specs/functional/abi-spec.k b/tests/specs/functional/abi-spec.k
index 4b4d84bd5c..0d27b80096 100644
--- a/tests/specs/functional/abi-spec.k
+++ b/tests/specs/functional/abi-spec.k
@@ -39,4 +39,26 @@ module ABI-SPEC
           ...
       </k>
 
+    claim [sizeOfDynamicType-2455]:
+      <k> runLemma(
+        #sizeOfDynamicType(
+          #array(
+            #bytes(b"\x00"), 
+            3, 
+            #bytes(b"\xaa"), #bytes(b"\xbb\xbb"), #bytes(b"\xcc\xcc\xcc")
+          )
+        )
+        ==Int
+        lengthBytes(#enc(
+          #array(
+            #bytes(b"\x00"), 
+            3, 
+            #bytes(b"\xaa"), #bytes(b"\xbb\xbb"), #bytes(b"\xcc\xcc\xcc")
+          )
+        ))
+      ) 
+      => doneLemma(true) 
+      ... 
+      </k>
+
 endmodule