Remove option to not simplify initial states (#113)

* kontrol/{prove,__main__}: remove option to skip simplifying init states * Set Version: 0.1.30 * src/tests/integration: update expected output * Set Version: 0.1.31 --------- Co-authored-by: devops <devops@runtimeverification.com>
runtimeverification · Oct 19, 2023 · 21f786c · 21f786c
1 parent ec83f45
commit 21f786c
Show file tree

Hide file tree

Showing 20 changed files with 359 additions and 534 deletions.
diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.30
+0.1.31
diff --git a/pyproject.toml b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.30"
+version = "0.1.31"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py
@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '0.1.30'
+VERSION: Final = '0.1.31'
diff --git a/src/kontrol/__main__.py b/src/kontrol/__main__.py
@@ -146,7 +146,6 @@ def exec_prove(
     reinit: bool = False,
     tests: Iterable[tuple[str, int | None]] = (),
     workers: int = 1,
-    simplify_init: bool = True,
     break_every_step: bool = False,
     break_on_jumpi: bool = False,
     break_on_calls: bool = True,
@@ -183,7 +182,6 @@ def exec_prove(
         reinit=reinit,
         tests=tests,
         workers=workers,
-        simplify_init=simplify_init,
         break_every_step=break_every_step,
         break_on_jumpi=break_on_jumpi,
         break_on_calls=break_on_calls,

diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
@@ -48,7 +48,6 @@ def foundry_prove(
     reinit: bool = False,
     tests: Iterable[tuple[str, int | None]] = (),
     workers: int = 1,
-    simplify_init: bool = True,
     break_every_step: bool = False,
     break_on_jumpi: bool = False,
     break_on_calls: bool = True,
@@ -115,7 +114,6 @@ def run_prover(test_suite: list[FoundryTest]) -> dict[tuple[str, int], tuple[boo
             max_depth=max_depth,
             max_iterations=max_iterations,
             workers=workers,
-            simplify_init=simplify_init,
             break_every_step=break_every_step,
             break_on_jumpi=break_on_jumpi,
             break_on_calls=break_on_calls,
@@ -221,7 +219,6 @@ def _run_cfg_group(
     max_depth: int,
     max_iterations: int | None,
     workers: int,
-    simplify_init: bool,
     break_every_step: bool,
     break_on_jumpi: bool,
     break_on_calls: bool,
@@ -258,7 +255,6 @@ def init_and_run_proof(test: FoundryTest) -> tuple[bool, list[str] | None]:
                 foundry,
                 test,
                 kcfg_explore,
-                simplify_init=simplify_init,
                 bmc_depth=bmc_depth,
                 run_constructor=run_constructor,
             )
@@ -296,7 +292,6 @@ def method_to_apr_proof(
     foundry: Foundry,
     test: FoundryTest,
     kcfg_explore: KCFGExplore,
-    simplify_init: bool = True,
     bmc_depth: int | None = None,
     run_constructor: bool = False,
 ) -> APRProof | APRBMCProof:
@@ -320,7 +315,6 @@ def method_to_apr_proof(
         test,
         kcfg_explore,
         setup_proof=setup_proof,
-        simplify_init=simplify_init,
     )
 
     if bmc_depth is not None:
@@ -361,7 +355,6 @@ def _method_to_initialized_cfg(
     kcfg_explore: KCFGExplore,
     *,
     setup_proof: APRProof | None = None,
-    simplify_init: bool = True,
 ) -> tuple[KCFG, int, int]:
     _LOGGER.info(f'Initializing KCFG for test: {test.id}')
 
@@ -388,9 +381,8 @@ def _method_to_initialized_cfg(
     target_cterm = CTerm.from_kast(target_term)
     kcfg.replace_node(target_node_id, target_cterm)
 
-    if simplify_init:
-        _LOGGER.info(f'Simplifying KCFG for test: {test.name}')
-        kcfg_explore.simplify(kcfg, {})
+    _LOGGER.info(f'Simplifying KCFG for test: {test.name}')
+    kcfg_explore.simplify(kcfg, {})
 
     return kcfg, init_node_id, target_node_id
 

diff --git a/src/tests/integration/test-data/gas-abstraction.expected b/src/tests/integration/test-data/gas-abstraction.expected
@@ -1,9 +1,9 @@
 
 ┌─ 1 (root, init)
-│   k: #execute ~> CONTINUATION
+│   k: #execute ~> CONTINUATION:K
 │   pc: 0
 │   callDepth: 0
-│   statusCode: STATUSCODE
+│   statusCode: STATUSCODE:StatusCode
 │
 │  (683 steps)
 ├─ 3
@@ -78,11 +78,11 @@
     statusCode: EVMC_REVERT
 
 
-┌─ 2 (root, leaf, target)
-│   k: #halt ~> CONTINUATION
-│   pc: PC_CELL_5d410f2a
-│   callDepth: CALLDEPTH_CELL_5d410f2a
-│   statusCode: STATUSCODE_FINAL
+┌─ 2 (root, leaf, target, terminal)
+│   k: #halt ~> CONTINUATION:K
+│   pc: PC_CELL_5d410f2a:Int
+│   callDepth: CALLDEPTH_CELL_5d410f2a:Int
+│   statusCode: STATUSCODE_FINAL:StatusCode
 
 
 Node 6:
@@ -397,11 +397,10 @@ Node 6:
     rule [BASIC-BLOCK-1-TO-3]: <foundry>
            <kevm>
              <k>
-               ( #execute
-               ~> CONTINUATION => #end EVMC_REVERT
-               ~> #pc [ REVERT ]
+               ( .K => #end EVMC_REVERT
+               ~> #pc [ REVERT ] )
                ~> #execute
-               ~> CONTINUATION:K )
+               ~> _CONTINUATION
              </k>
              <mode>
                NORMAL
@@ -427,10 +426,10 @@ Node 6:
                      728815563385977040452943777879061427756277306518
                    </id>
                    <caller>
-                     CALLER_ID
+                     CALLER_ID:Int
                    </caller>
                    <callData>
-                     ( S2KGasTest . S2KtestInfiniteGas ( ) => b"c\xfe\xc36" )
+                     b"c\xfe\xc36"
                    </callData>
                    <callValue>
                      0
@@ -439,7 +438,7 @@ Node 6:
                      ( .WordStack => ( 778 : ( ( VGAS:Int +Int -298 ) : ( 583 : ( 928 : ( 345 : ( ( VGAS:Int +Int -207 ) : ( 266 : ( selector ( "testInfiniteGas()" ) : .WordStack ) ) ) ) ) ) ) ) )
                    </wordStack>
                    <localMem>
-                     ( .Bytes => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80" )
+                     ( b"" => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80" )
                    </localMem>
                    ...
                    ...
@@ -467,11 +466,11 @@ Node 6:
                    ...
                  </substate>
                  <origin>
-                   ORIGIN_ID
+                   ORIGIN_ID:Int
                  </origin>
                  <block>
                    <number>
-                     NUMBER_CELL
+                     NUMBER_CELL:Int
                    </number>
                    ...
                  </block>
@@ -560,7 +559,7 @@ Node 6:
                  0
                </expectedValue>
                <expectedData>
-                 ( .Bytes => b"" )
+                 b""
                </expectedData>
                <opcodeType>
                  .OpcodeType
@@ -591,24 +590,14 @@ Node 6:
              </whitelist>
            </cheatcodes>
          </foundry>
-      requires ( 0 <=Int CALLER_ID
-       andBool ( CALLER_ID <Int pow160
-       andBool ( 0 <=Int ORIGIN_ID
-       andBool ( ORIGIN_ID <Int pow160
-       andBool ( 0 <=Int NUMBER_CELL
-       andBool ( NUMBER_CELL <=Int maxSInt256
-       andBool ( lengthBytes ( S2KGasTest . S2KtestInfiniteGas ( ) ) <Int pow128
-       andBool ( 0 <=Int 728815563385977040452943777879061427756277306518
-       andBool ( 728815563385977040452943777879061427756277306518 <Int pow160
-               )))))))))
-       ensures ( 0 <=Int CALLER_ID:Int
+      requires ( 0 <=Int CALLER_ID:Int
        andBool ( 0 <=Int ORIGIN_ID:Int
        andBool ( 0 <=Int NUMBER_CELL:Int
        andBool ( CALLER_ID:Int <Int pow160
        andBool ( ORIGIN_ID:Int <Int pow160
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
-       andBool ( VGAS:Int <Int ( VGAS:Int +Int 91 )
-               )))))))
+               ))))))
+       ensures VGAS:Int <Int ( VGAS:Int +Int 91 )
       [label(BASIC-BLOCK-1-TO-3)]
 
     rule [BASIC-BLOCK-4-TO-5]: <foundry>