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/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 ... + claim [sizeOfDynamicType-2455]: + 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) + ... + + endmodule