Avoid PUSH data when computing jumpdests (#2460)

* kevm.py: avoid PUSH data when computing jumpdests

* Set Version: 1.0.585

* fix typo

* update claim files

* kevm.py: add review suggestion

* Set Version: 1.0.586

---------

Co-authored-by: devops <[email protected]>

Author: anvacaru

kevm-pyk/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.585"
+version = "1.0.586"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

kevm-pyk/src/kevm_pyk/__init__.py

@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '1.0.585'
+VERSION: Final = '1.0.586'

kevm-pyk/src/kevm_pyk/kevm.py

@@ -690,7 +690,7 @@ def compute_jumpdests(sections: list[KInner]) -> KInner:
 
 
 def _process_jumpdests(bytecode: bytes, offset: int) -> list[KToken]:
-    """Computes the location of JUMPDEST opcodes from a given bytecode.
+    """Computes the location of JUMPDEST opcodes from a given bytecode while avoiding bytes from within the PUSH opcodes.
 
     :param bytecode: The bytecode of the contract as bytes.
     :type bytecode: bytes
@@ -699,4 +699,16 @@ def _process_jumpdests(bytecode: bytes, offset: int) -> list[KToken]:
     :return:  A list of intToken instances representing the positions of all found jump destinations in the bytecode adjusted by the offset.
     :rtype: list[KToken]
     """
-    return [intToken(offset + i) for i, byte in enumerate(bytecode) if byte == 0x5B]
+    push1 = 0x60
+    push32 = 0x7F
+    jumpdest = 0x5B
+    i = 0
+    jumpdests: list[KToken] = []
+    while i < len(bytecode):
+        if push1 <= bytecode[i] <= push32:
+            i += bytecode[i] - push1 + 2
+        else:
+            if bytecode[i] == jumpdest:
+                jumpdests.append(intToken(offset + i))
+            i += 1
+    return jumpdests

kevm-pyk/src/tests/unit/test_kevm.py

@@ -106,6 +106,7 @@ def test_kinner_to_hex(test_id: str, input: KInner, result: KInner) -> None:
         ],
         set_of([token(68), token(104), token(105), token(106), token(108)]),
     ),
+    ('jump_to_push', [token(bytes.fromhex('6001600055600A56605B5B'))], set_of([token(10)])),
 ]
 
 

package/version

@@ -1 +1 @@
-1.0.585
+1.0.586

tests/specs/kontrol/test-allowchangestest-testallow-0-spec.k

@@ -143,7 +143,7 @@ module TEST-ALLOWCHANGESTEST-TESTALLOW-0-SPEC
                  <jumpDests>
                      ( SetItem ( 1001 ) ( SetItem ( 102 ) ( SetItem ( 1097 ) ( SetItem ( 1117 ) ( SetItem ( 1163 ) ( SetItem ( 1189 ) ( SetItem ( 1209 ) ( SetItem ( 1217 ) ( SetItem ( 1231 ) ( SetItem ( 1259 ) ( SetItem ( 1276 ) ( SetItem ( 1304 ) ( SetItem ( 1393 ) ( SetItem ( 1413 ) ( SetItem ( 1509 ) ( SetItem ( 151 ) ( SetItem ( 1529 ) ( SetItem ( 1579 ) ( SetItem ( 16 ) ( SetItem ( 1615 ) ( SetItem ( 1723 ) ( SetItem ( 1785 ) ( SetItem ( 1809 ) ( SetItem ( 1818 ) ( SetItem ( 1854 ) ( SetItem ( 1885 ) ( SetItem ( 1929 ) ( SetItem ( 1963 ) ( SetItem ( 1977 ) ( SetItem ( 2006 ) ( SetItem ( 2026 ) ( SetItem ( 2062 ) ( SetItem ( 211 ) ( SetItem ( 2170 ) ( SetItem ( 2232 ) ( SetItem ( 2256 ) ( SetItem ( 2292 ) ( SetItem ( 2323 ) ( SetItem ( 2367 ) ( SetItem ( 2401 ) ( SetItem ( 2415 ) ( SetItem ( 2444 ) ( SetItem ( 2464 ) ( SetItem ( 2498 ) ( SetItem ( 256 ) ( SetItem ( 261 ) ( SetItem ( 2640 ) ( SetItem ( 2666 ) ( SetItem ( 269 ) ( SetItem ( 2727 ) ( SetItem ( 2732 ) ( SetItem ( 2756 ) ( SetItem ( 2760 ) ( SetItem ( 2765 ) ( SetItem ( 2779 ) ( SetItem ( 2807 ) ( SetItem ( 282 ) ( SetItem ( 2824 ) ( SetItem ( 2852 ) ( SetItem ( 291 ) ( SetItem ( 2941 ) ( SetItem ( 2961 ) ( SetItem ( 299 ) ( SetItem ( 3057 ) ( SetItem ( 307 ) ( SetItem ( 3077 ) ( SetItem ( 3126 ) ( SetItem ( 315 ) ( SetItem ( 317 ) ( SetItem ( 3222 ) ( SetItem ( 3236 ) ( SetItem ( 325 ) ( SetItem ( 3264 ) ( SetItem ( 3281 ) ( SetItem ( 3309 ) ( SetItem ( 333 ) ( SetItem ( 3398 ) ( SetItem ( 3418 ) ( SetItem ( 346 ) ( SetItem ( 3514 ) ( SetItem ( 3534 ) ( SetItem ( 354 ) ( SetItem ( 3585 ) ( SetItem ( 3595 ) ( SetItem ( 3597 ) ( SetItem ( 367 ) ( SetItem ( 3697 ) ( SetItem ( 3713 ) ( SetItem ( 3716 ) ( SetItem ( 375 ) ( SetItem ( 383 ) ( SetItem ( 3870 ) ( SetItem ( 3896 ) ( SetItem ( 391 ) ( SetItem ( 3957 ) ( SetItem ( 3962 ) ( SetItem ( 3967 ) ( SetItem ( 3984 ) ( SetItem ( 3996 ) ( SetItem ( 4024 ) ( SetItem ( 4061 ) ( SetItem ( 407 ) ( SetItem ( 4073 ) ( SetItem ( 4113 ) ( SetItem ( 4174 ) ( SetItem ( 4216 ) ( SetItem ( 4237 ) ( SetItem ( 4252 ) ( SetItem ( 4255 ) ( SetItem ( 4279 ) ( SetItem ( 4294 ) ( SetItem ( 4300 ) ( SetItem ( 4339 ) ( SetItem ( 4378 ) ( SetItem ( 4409 ) ( SetItem ( 4422 ) ( SetItem ( 4442 ) ( SetItem ( 446 ) ( SetItem ( 4474 ) ( SetItem ( 4480 ) ( SetItem ( 4515 ) ( SetItem ( 4529 ) ( SetItem ( 4547 ) ( SetItem ( 4557 ) ( SetItem ( 4575 ) ( SetItem ( 4591 ) ( SetItem ( 4615 ) ( SetItem ( 4645 ) ( SetItem ( 470 ) ( SetItem ( 4700 ) ( SetItem ( 4705 ) ( SetItem ( 4716 ) ( SetItem ( 4721 ) ( SetItem ( 4723 ) ( SetItem ( 4731 ) ( SetItem ( 4749 ) ( SetItem ( 4757 ) ( SetItem ( 4768 ) ( SetItem ( 4773 ) ( SetItem ( 478 ) ( SetItem ( 4790 ) ( SetItem ( 486 ) ( SetItem ( 494 ) ( SetItem ( 502 ) ( SetItem ( 515 ) ( SetItem ( 573 ) ( SetItem ( 603 ) ( SetItem ( 613 ) ( SetItem ( 709 ) ( SetItem ( 805 ) ( SetItem ( 819 ) ( SetItem ( 847 ) ( SetItem ( 864 ) ( SetItem ( 892 ) SetItem ( 981 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
                       =>
-                     ( SetItem ( 16 ) ( SetItem ( 46 ) ( SetItem ( 117 ) ( SetItem ( 108 ) ( SetItem ( 101 ) ( SetItem ( 106 ) ( SetItem ( 174 ) ( SetItem ( 169 ) ( SetItem ( 160 ) ( SetItem ( 132 ) ( SetItem ( 122 ) ( SetItem ( 124 ) ( SetItem ( 191 ) ( SetItem ( 150 ) SetItem ( 158 ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
+                     ( SetItem ( 16 ) ( SetItem ( 46 ) ( SetItem ( 117 ) ( SetItem ( 101 ) ( SetItem ( 106 ) ( SetItem ( 174 ) ( SetItem ( 169 ) ( SetItem ( 132 ) ( SetItem ( 122 ) ( SetItem ( 124 ) ( SetItem ( 191 ) ( SetItem ( 150 ) SetItem ( 158 ) ) ) ) ) ) ) ) ) ) ) ) )
                  </jumpDests>
                  <id>
                    ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 )

tests/specs/kontrol/test-allowchangestest-testallow_fail-0-spec.k

@@ -143,7 +143,7 @@ module TEST-ALLOWCHANGESTEST-TESTALLOW_FAIL-0-SPEC
                  <jumpDests>
                    ( SetItem ( 1001 ) ( SetItem ( 102 ) ( SetItem ( 1097 ) ( SetItem ( 1117 ) ( SetItem ( 1163 ) ( SetItem ( 1189 ) ( SetItem ( 1209 ) ( SetItem ( 1217 ) ( SetItem ( 1231 ) ( SetItem ( 1259 ) ( SetItem ( 1276 ) ( SetItem ( 1304 ) ( SetItem ( 1393 ) ( SetItem ( 1413 ) ( SetItem ( 1509 ) ( SetItem ( 151 ) ( SetItem ( 1529 ) ( SetItem ( 1579 ) ( SetItem ( 16 ) ( SetItem ( 1615 ) ( SetItem ( 1723 ) ( SetItem ( 1785 ) ( SetItem ( 1809 ) ( SetItem ( 1818 ) ( SetItem ( 1854 ) ( SetItem ( 1885 ) ( SetItem ( 1929 ) ( SetItem ( 1963 ) ( SetItem ( 1977 ) ( SetItem ( 2006 ) ( SetItem ( 2026 ) ( SetItem ( 2062 ) ( SetItem ( 211 ) ( SetItem ( 2170 ) ( SetItem ( 2232 ) ( SetItem ( 2256 ) ( SetItem ( 2292 ) ( SetItem ( 2323 ) ( SetItem ( 2367 ) ( SetItem ( 2401 ) ( SetItem ( 2415 ) ( SetItem ( 2444 ) ( SetItem ( 2464 ) ( SetItem ( 2498 ) ( SetItem ( 256 ) ( SetItem ( 261 ) ( SetItem ( 2640 ) ( SetItem ( 2666 ) ( SetItem ( 269 ) ( SetItem ( 2727 ) ( SetItem ( 2732 ) ( SetItem ( 2756 ) ( SetItem ( 2760 ) ( SetItem ( 2765 ) ( SetItem ( 2779 ) ( SetItem ( 2807 ) ( SetItem ( 282 ) ( SetItem ( 2824 ) ( SetItem ( 2852 ) ( SetItem ( 291 ) ( SetItem ( 2941 ) ( SetItem ( 2961 ) ( SetItem ( 299 ) ( SetItem ( 3057 ) ( SetItem ( 307 ) ( SetItem ( 3077 ) ( SetItem ( 3126 ) ( SetItem ( 315 ) ( SetItem ( 317 ) ( SetItem ( 3222 ) ( SetItem ( 3236 ) ( SetItem ( 325 ) ( SetItem ( 3264 ) ( SetItem ( 3281 ) ( SetItem ( 3309 ) ( SetItem ( 333 ) ( SetItem ( 3398 ) ( SetItem ( 3418 ) ( SetItem ( 346 ) ( SetItem ( 3514 ) ( SetItem ( 3534 ) ( SetItem ( 354 ) ( SetItem ( 3585 ) ( SetItem ( 3595 ) ( SetItem ( 3597 ) ( SetItem ( 367 ) ( SetItem ( 3697 ) ( SetItem ( 3713 ) ( SetItem ( 3716 ) ( SetItem ( 375 ) ( SetItem ( 383 ) ( SetItem ( 3870 ) ( SetItem ( 3896 ) ( SetItem ( 391 ) ( SetItem ( 3957 ) ( SetItem ( 3962 ) ( SetItem ( 3967 ) ( SetItem ( 3984 ) ( SetItem ( 3996 ) ( SetItem ( 4024 ) ( SetItem ( 4061 ) ( SetItem ( 407 ) ( SetItem ( 4073 ) ( SetItem ( 4113 ) ( SetItem ( 4174 ) ( SetItem ( 4216 ) ( SetItem ( 4237 ) ( SetItem ( 4252 ) ( SetItem ( 4255 ) ( SetItem ( 4279 ) ( SetItem ( 4294 ) ( SetItem ( 4300 ) ( SetItem ( 4339 ) ( SetItem ( 4378 ) ( SetItem ( 4409 ) ( SetItem ( 4422 ) ( SetItem ( 4442 ) ( SetItem ( 446 ) ( SetItem ( 4474 ) ( SetItem ( 4480 ) ( SetItem ( 4515 ) ( SetItem ( 4529 ) ( SetItem ( 4547 ) ( SetItem ( 4557 ) ( SetItem ( 4575 ) ( SetItem ( 4591 ) ( SetItem ( 4615 ) ( SetItem ( 4645 ) ( SetItem ( 470 ) ( SetItem ( 4700 ) ( SetItem ( 4705 ) ( SetItem ( 4716 ) ( SetItem ( 4721 ) ( SetItem ( 4723 ) ( SetItem ( 4731 ) ( SetItem ( 4749 ) ( SetItem ( 4757 ) ( SetItem ( 4768 ) ( SetItem ( 4773 ) ( SetItem ( 478 ) ( SetItem ( 4790 ) ( SetItem ( 486 ) ( SetItem ( 494 ) ( SetItem ( 502 ) ( SetItem ( 515 ) ( SetItem ( 573 ) ( SetItem ( 603 ) ( SetItem ( 613 ) ( SetItem ( 709 ) ( SetItem ( 805 ) ( SetItem ( 819 ) ( SetItem ( 847 ) ( SetItem ( 864 ) ( SetItem ( 892 ) SetItem ( 981 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
                      =>
-                   ( SetItem ( 16 ) ( SetItem ( 46 ) ( SetItem ( 117 ) ( SetItem ( 108 ) ( SetItem ( 101 ) ( SetItem ( 106 ) ( SetItem ( 174 ) ( SetItem ( 169 ) ( SetItem ( 160 ) ( SetItem ( 132 ) ( SetItem ( 122 ) ( SetItem ( 124 ) ( SetItem ( 191 ) ( SetItem ( 150 ) SetItem ( 158 ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
+                   ( SetItem ( 16 ) ( SetItem ( 46 ) ( SetItem ( 117 ) ( SetItem ( 101 ) ( SetItem ( 106 ) ( SetItem ( 174 ) ( SetItem ( 169 ) ( SetItem ( 132 ) ( SetItem ( 122 ) ( SetItem ( 124 ) ( SetItem ( 191 ) ( SetItem ( 150 ) SetItem ( 158 ) ) ) ) ) ) ) ) ) ) ) ) )
                  </jumpDests>
                  <id>
                    ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 )

tests/specs/kontrol/test-allowchangestest-testfailallowcallstoaddress-0-spec.k

@@ -143,7 +143,7 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCALLSTOADDRESS-0-SPEC
                  <jumpDests>
                    ( SetItem ( 1001 ) ( SetItem ( 102 ) ( SetItem ( 1097 ) ( SetItem ( 1117 ) ( SetItem ( 1163 ) ( SetItem ( 1189 ) ( SetItem ( 1209 ) ( SetItem ( 1217 ) ( SetItem ( 1231 ) ( SetItem ( 1259 ) ( SetItem ( 1276 ) ( SetItem ( 1304 ) ( SetItem ( 1393 ) ( SetItem ( 1413 ) ( SetItem ( 1509 ) ( SetItem ( 151 ) ( SetItem ( 1529 ) ( SetItem ( 1579 ) ( SetItem ( 16 ) ( SetItem ( 1615 ) ( SetItem ( 1723 ) ( SetItem ( 1785 ) ( SetItem ( 1809 ) ( SetItem ( 1818 ) ( SetItem ( 1854 ) ( SetItem ( 1885 ) ( SetItem ( 1929 ) ( SetItem ( 1963 ) ( SetItem ( 1977 ) ( SetItem ( 2006 ) ( SetItem ( 2026 ) ( SetItem ( 2062 ) ( SetItem ( 211 ) ( SetItem ( 2170 ) ( SetItem ( 2232 ) ( SetItem ( 2256 ) ( SetItem ( 2292 ) ( SetItem ( 2323 ) ( SetItem ( 2367 ) ( SetItem ( 2401 ) ( SetItem ( 2415 ) ( SetItem ( 2444 ) ( SetItem ( 2464 ) ( SetItem ( 2498 ) ( SetItem ( 256 ) ( SetItem ( 261 ) ( SetItem ( 2640 ) ( SetItem ( 2666 ) ( SetItem ( 269 ) ( SetItem ( 2727 ) ( SetItem ( 2732 ) ( SetItem ( 2756 ) ( SetItem ( 2760 ) ( SetItem ( 2765 ) ( SetItem ( 2779 ) ( SetItem ( 2807 ) ( SetItem ( 282 ) ( SetItem ( 2824 ) ( SetItem ( 2852 ) ( SetItem ( 291 ) ( SetItem ( 2941 ) ( SetItem ( 2961 ) ( SetItem ( 299 ) ( SetItem ( 3057 ) ( SetItem ( 307 ) ( SetItem ( 3077 ) ( SetItem ( 3126 ) ( SetItem ( 315 ) ( SetItem ( 317 ) ( SetItem ( 3222 ) ( SetItem ( 3236 ) ( SetItem ( 325 ) ( SetItem ( 3264 ) ( SetItem ( 3281 ) ( SetItem ( 3309 ) ( SetItem ( 333 ) ( SetItem ( 3398 ) ( SetItem ( 3418 ) ( SetItem ( 346 ) ( SetItem ( 3514 ) ( SetItem ( 3534 ) ( SetItem ( 354 ) ( SetItem ( 3585 ) ( SetItem ( 3595 ) ( SetItem ( 3597 ) ( SetItem ( 367 ) ( SetItem ( 3697 ) ( SetItem ( 3713 ) ( SetItem ( 3716 ) ( SetItem ( 375 ) ( SetItem ( 383 ) ( SetItem ( 3870 ) ( SetItem ( 3896 ) ( SetItem ( 391 ) ( SetItem ( 3957 ) ( SetItem ( 3962 ) ( SetItem ( 3967 ) ( SetItem ( 3984 ) ( SetItem ( 3996 ) ( SetItem ( 4024 ) ( SetItem ( 4061 ) ( SetItem ( 407 ) ( SetItem ( 4073 ) ( SetItem ( 4113 ) ( SetItem ( 4174 ) ( SetItem ( 4216 ) ( SetItem ( 4237 ) ( SetItem ( 4252 ) ( SetItem ( 4255 ) ( SetItem ( 4279 ) ( SetItem ( 4294 ) ( SetItem ( 4300 ) ( SetItem ( 4339 ) ( SetItem ( 4378 ) ( SetItem ( 4409 ) ( SetItem ( 4422 ) ( SetItem ( 4442 ) ( SetItem ( 446 ) ( SetItem ( 4474 ) ( SetItem ( 4480 ) ( SetItem ( 4515 ) ( SetItem ( 4529 ) ( SetItem ( 4547 ) ( SetItem ( 4557 ) ( SetItem ( 4575 ) ( SetItem ( 4591 ) ( SetItem ( 4615 ) ( SetItem ( 4645 ) ( SetItem ( 470 ) ( SetItem ( 4700 ) ( SetItem ( 4705 ) ( SetItem ( 4716 ) ( SetItem ( 4721 ) ( SetItem ( 4723 ) ( SetItem ( 4731 ) ( SetItem ( 4749 ) ( SetItem ( 4757 ) ( SetItem ( 4768 ) ( SetItem ( 4773 ) ( SetItem ( 478 ) ( SetItem ( 4790 ) ( SetItem ( 486 ) ( SetItem ( 494 ) ( SetItem ( 502 ) ( SetItem ( 515 ) ( SetItem ( 573 ) ( SetItem ( 603 ) ( SetItem ( 613 ) ( SetItem ( 709 ) ( SetItem ( 805 ) ( SetItem ( 819 ) ( SetItem ( 847 ) ( SetItem ( 864 ) ( SetItem ( 892 ) SetItem ( 981 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
                      =>
-                   ( SetItem ( 16 ) ( SetItem ( 46 ) ( SetItem ( 117 ) ( SetItem ( 108 ) ( SetItem ( 101 ) ( SetItem ( 106 ) ( SetItem ( 174 ) ( SetItem ( 169 ) ( SetItem ( 160 ) ( SetItem ( 132 ) ( SetItem ( 122 ) ( SetItem ( 124 ) ( SetItem ( 191 ) ( SetItem ( 150 ) SetItem ( 158 ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
+                   ( SetItem ( 16 ) ( SetItem ( 46 ) ( SetItem ( 117 ) ( SetItem ( 101 ) ( SetItem ( 106 ) ( SetItem ( 174 ) ( SetItem ( 169 ) ( SetItem ( 132 ) ( SetItem ( 122 ) ( SetItem ( 124 ) ( SetItem ( 191 ) ( SetItem ( 150 ) SetItem ( 158 ) ) ) ) ) ) ) ) ) ) ) ) )
                  </jumpDests>
                  <id>
                    ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 )

tests/specs/kontrol/test-allowchangestest-testfailallowchangestostorage-0-spec.k

@@ -143,7 +143,7 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCHANGESTOSTORAGE-0-SPEC
                  <jumpDests>
                    ( SetItem ( 1001 ) ( SetItem ( 102 ) ( SetItem ( 1097 ) ( SetItem ( 1117 ) ( SetItem ( 1163 ) ( SetItem ( 1189 ) ( SetItem ( 1209 ) ( SetItem ( 1217 ) ( SetItem ( 1231 ) ( SetItem ( 1259 ) ( SetItem ( 1276 ) ( SetItem ( 1304 ) ( SetItem ( 1393 ) ( SetItem ( 1413 ) ( SetItem ( 1509 ) ( SetItem ( 151 ) ( SetItem ( 1529 ) ( SetItem ( 1579 ) ( SetItem ( 16 ) ( SetItem ( 1615 ) ( SetItem ( 1723 ) ( SetItem ( 1785 ) ( SetItem ( 1809 ) ( SetItem ( 1818 ) ( SetItem ( 1854 ) ( SetItem ( 1885 ) ( SetItem ( 1929 ) ( SetItem ( 1963 ) ( SetItem ( 1977 ) ( SetItem ( 2006 ) ( SetItem ( 2026 ) ( SetItem ( 2062 ) ( SetItem ( 211 ) ( SetItem ( 2170 ) ( SetItem ( 2232 ) ( SetItem ( 2256 ) ( SetItem ( 2292 ) ( SetItem ( 2323 ) ( SetItem ( 2367 ) ( SetItem ( 2401 ) ( SetItem ( 2415 ) ( SetItem ( 2444 ) ( SetItem ( 2464 ) ( SetItem ( 2498 ) ( SetItem ( 256 ) ( SetItem ( 261 ) ( SetItem ( 2640 ) ( SetItem ( 2666 ) ( SetItem ( 269 ) ( SetItem ( 2727 ) ( SetItem ( 2732 ) ( SetItem ( 2756 ) ( SetItem ( 2760 ) ( SetItem ( 2765 ) ( SetItem ( 2779 ) ( SetItem ( 2807 ) ( SetItem ( 282 ) ( SetItem ( 2824 ) ( SetItem ( 2852 ) ( SetItem ( 291 ) ( SetItem ( 2941 ) ( SetItem ( 2961 ) ( SetItem ( 299 ) ( SetItem ( 3057 ) ( SetItem ( 307 ) ( SetItem ( 3077 ) ( SetItem ( 3126 ) ( SetItem ( 315 ) ( SetItem ( 317 ) ( SetItem ( 3222 ) ( SetItem ( 3236 ) ( SetItem ( 325 ) ( SetItem ( 3264 ) ( SetItem ( 3281 ) ( SetItem ( 3309 ) ( SetItem ( 333 ) ( SetItem ( 3398 ) ( SetItem ( 3418 ) ( SetItem ( 346 ) ( SetItem ( 3514 ) ( SetItem ( 3534 ) ( SetItem ( 354 ) ( SetItem ( 3585 ) ( SetItem ( 3595 ) ( SetItem ( 3597 ) ( SetItem ( 367 ) ( SetItem ( 3697 ) ( SetItem ( 3713 ) ( SetItem ( 3716 ) ( SetItem ( 375 ) ( SetItem ( 383 ) ( SetItem ( 3870 ) ( SetItem ( 3896 ) ( SetItem ( 391 ) ( SetItem ( 3957 ) ( SetItem ( 3962 ) ( SetItem ( 3967 ) ( SetItem ( 3984 ) ( SetItem ( 3996 ) ( SetItem ( 4024 ) ( SetItem ( 4061 ) ( SetItem ( 407 ) ( SetItem ( 4073 ) ( SetItem ( 4113 ) ( SetItem ( 4174 ) ( SetItem ( 4216 ) ( SetItem ( 4237 ) ( SetItem ( 4252 ) ( SetItem ( 4255 ) ( SetItem ( 4279 ) ( SetItem ( 4294 ) ( SetItem ( 4300 ) ( SetItem ( 4339 ) ( SetItem ( 4378 ) ( SetItem ( 4409 ) ( SetItem ( 4422 ) ( SetItem ( 4442 ) ( SetItem ( 446 ) ( SetItem ( 4474 ) ( SetItem ( 4480 ) ( SetItem ( 4515 ) ( SetItem ( 4529 ) ( SetItem ( 4547 ) ( SetItem ( 4557 ) ( SetItem ( 4575 ) ( SetItem ( 4591 ) ( SetItem ( 4615 ) ( SetItem ( 4645 ) ( SetItem ( 470 ) ( SetItem ( 4700 ) ( SetItem ( 4705 ) ( SetItem ( 4716 ) ( SetItem ( 4721 ) ( SetItem ( 4723 ) ( SetItem ( 4731 ) ( SetItem ( 4749 ) ( SetItem ( 4757 ) ( SetItem ( 4768 ) ( SetItem ( 4773 ) ( SetItem ( 478 ) ( SetItem ( 4790 ) ( SetItem ( 486 ) ( SetItem ( 494 ) ( SetItem ( 502 ) ( SetItem ( 515 ) ( SetItem ( 573 ) ( SetItem ( 603 ) ( SetItem ( 613 ) ( SetItem ( 709 ) ( SetItem ( 805 ) ( SetItem ( 819 ) ( SetItem ( 847 ) ( SetItem ( 864 ) ( SetItem ( 892 ) SetItem ( 981 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
                      =>
-                   ( SetItem ( 16 ) ( SetItem ( 46 ) ( SetItem ( 117 ) ( SetItem ( 108 ) ( SetItem ( 101 ) ( SetItem ( 106 ) ( SetItem ( 174 ) ( SetItem ( 169 ) ( SetItem ( 160 ) ( SetItem ( 132 ) ( SetItem ( 122 ) ( SetItem ( 124 ) ( SetItem ( 191 ) ( SetItem ( 150 ) SetItem ( 158 ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
+                   ( SetItem ( 16 ) ( SetItem ( 46 ) ( SetItem ( 117 ) ( SetItem ( 101 ) ( SetItem ( 106 ) ( SetItem ( 174 ) ( SetItem ( 169 ) ( SetItem ( 132 ) ( SetItem ( 122 ) ( SetItem ( 124 ) ( SetItem ( 191 ) ( SetItem ( 150 ) SetItem ( 158 ) ) ) ) ) ) ) ) ) ) ) ) )
                  </jumpDests>
                  <id>
                    ( 728815563385977040452943777879061427756277306518 => 491460923342184218035706888008750043977755113263 )
@@ -487,7 +487,7 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCHANGESTOSTORAGE-0-SPEC
                    b"`\x80`@R4\x80\x15a\x00\x10W`\x00\x80\xfd[P`\xdd\x80a\x00\x1f`\x009`\x00\xf3\xfe`\x80`@R4\x80\x15`\x0fW`\x00\x80\xfd[P`\x046\x10`FW`\x005`\xe0\x1c\x80c\x15\xe6z\xa6\x14`KW\x80c03A;\x14`]W\x80c]3\xa2\x7f\x14`wW\x80cak\x8d\x05\x14`\x7fW[`\x00\x80\xfd[`[`V6`\x04`\x8fV[`\x01UV[\x00[`e`\x00T\x81V[`@Q\x90\x81R` \x01`@Q\x80\x91\x03\x90\xf3[`e`\x01T\x81V[`[`\x8a6`\x04`\x8fV[`\x00UV[`\x00` \x82\x84\x03\x12\x15`\xa0W`\x00\x80\xfd[P5\x91\x90PV\xfe\xa2dipfsX\"\x12 k\xdd\x86\x85\x7f\xfc\x83n#6Y\x8de\xd5'\xc1*\x92U3\x1e\xbcVQ\x12,\xdc\x15\x7fVH\xf5dsolcC\x00\x08\r\x003"
                  </program>
                  <jumpDests>
-                   ( SetItem ( 16 ) ( SetItem ( 46 ) ( SetItem ( 117 ) ( SetItem ( 108 ) ( SetItem ( 101 ) ( SetItem ( 106 ) ( SetItem ( 174 ) ( SetItem ( 169 ) ( SetItem ( 160 ) ( SetItem ( 132 ) ( SetItem ( 122 ) ( SetItem ( 124 ) ( SetItem ( 191 ) ( SetItem ( 150 ) SetItem ( 158 ) ) ) ) ) ) ) ) ) ) ) ) ) ) )
+                   ( SetItem ( 16 ) ( SetItem ( 46 ) ( SetItem ( 117 ) ( SetItem ( 101 ) ( SetItem ( 106 ) ( SetItem ( 174 ) ( SetItem ( 169 ) ( SetItem ( 132 ) ( SetItem ( 122 ) ( SetItem ( 124 ) ( SetItem ( 191 ) ( SetItem ( 150 ) SetItem ( 158 ) ) ) ) ) ) ) ) ) ) ) ) )
                  </jumpDests>
                  <id>
                    ( 491460923342184218035706888008750043977755113263 => 263400868551549723330807389252719309078400616203 )