Small documentation improvements/fixes with max-iterations, max-depth…

…, and bmc-depth (#2014)

* Add more specific help messages for bmc-depth and max-depth, correct max-iterations help message, give user more information about setUp failures

* Set Version: 1.0.255

* Simplify get_final_accounts_cell and improve error message

* Fix formatting

* Set Version: 1.0.257

* Set Version: 1.0.260

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: Andrei Văcaru <[email protected]>

kevm-pyk/pyproject.toml

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

kevm-pyk/src/kevm_pyk/__main__.py

@@ -978,7 +978,7 @@ def parse(s: str) -> list[T]:
         dest='bmc_depth',
         default=None,
         type=int,
-        help='Max depth of loop unrolling during bounded model checking',
+        help='Enables bounded model checking. Specifies the maximum depth to unroll all loops to.',
     )
     foundry_prove_args.add_argument(
         '--use-booster',

kevm-pyk/src/kevm_pyk/cli.py

@@ -235,14 +235,14 @@ def explore_args(self) -> ArgumentParser:
             dest='max_depth',
             default=1000,
             type=int,
-            help='Store every Nth state in the CFG for inspection.',
+            help='Maximum number of K steps before the state is saved in a new node in the CFG. Branching will cause this to happen earlier.',
         )
         args.add_argument(
             '--max-iterations',
             dest='max_iterations',
             default=None,
             type=int,
-            help='Store every Nth state in the CFG for inspection.',
+            help='Number of times to expand the next pending node in the CFG.',
         )
         args.add_argument(
             '--kore-rpc-command',

kevm-pyk/src/kevm_pyk/foundry.py

@@ -1038,7 +1038,14 @@ def _method_to_cfg(
 def get_final_accounts_cell(proof_digest: str, proof_dir: Path) -> tuple[KInner, Iterable[KInner]]:
     apr_proof = APRProof.read_proof_data(proof_dir, proof_digest)
     target = apr_proof.kcfg.node(apr_proof.target)
-    cterm = single(apr_proof.kcfg.covers(target_id=target.id)).source.cterm
+    target_states = apr_proof.kcfg.covers(target_id=target.id)
+    if len(target_states) == 0:
+        raise ValueError(
+            f'setUp() function for {apr_proof.id} did not reach the end of execution. Maybe --max-iterations is too low?'
+        )
+    if len(target_states) > 1:
+        raise ValueError(f'setUp() function for {apr_proof.id} branched and has {len(target_states)} target states.')
+    cterm = single(target_states).source.cterm
     acct_cell = cterm.cell('ACCOUNTS_CELL')
     fvars = free_vars(acct_cell)
     acct_cons = constraints_for(fvars, cterm.constraints)

package/debian/changelog

@@ -1,4 +1,4 @@
-kevm (1.0.259) unstable; urgency=medium
+kevm (1.0.260) unstable; urgency=medium
 
   * Initial Release.
 

package/version

@@ -1 +1 @@
-1.0.259
+1.0.260