Add proof exploration and display options to CLI

docs/conf.py

@@ -9,8 +9,8 @@
 project = 'pyk'
 author = 'Runtime Verification, Inc'
 copyright = '2024, Runtime Verification, Inc'
-version = '0.1.768'
-release = '0.1.768'
+version = '0.1.769'
+release = '0.1.769'
 
 # -- General configuration ---------------------------------------------------
 # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration

package/version

@@ -1 +1 @@
-0.1.768
+0.1.769

pyproject.toml

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

regression-new/kprove-haskell/Makefile

@@ -2,6 +2,7 @@ DEF=verif
 EXT=verif
 TESTDIR=.
 KOMPILE_BACKEND=haskell
+KPROVE_FLAGS=--show-kcfg
 export KORE_EXEC_OPTS=--log-level error
 
 include ../include/ktest.mak

regression-new/kprove-haskell/sum-spec.k.out

@@ -11,3 +11,126 @@ APRProof: 3b7070ca4603e18d26d032c0fe64dd71ffadc2c63dae9d57315e8e471a371bd3
     bounded: 0
     execution time: 0s
 Subproofs: 0
+
+┌─ 1 (root, init)
+│     <generatedTop>
+│       <k>
+│         addCounter ( N:Int )
+│         ~> K_CELL_fc656f08:K
+│       </k>
+│       <counter>
+│         C:Int
+│       </counter>
+│       <sum>
+│         S:Int
+│       </sum>
+│       <generatedCounter>
+│         GENERATEDCOUNTER_CELL_949ec677:Int
+│       </generatedCounter>
+│     </generatedTop>
+│     #And { true #Equals N:Int >=Int 0 }
+┃
+┃ (1 step)
+┣━━┓
+┃  │
+┃  ├─ 3
+┃  │     <generatedTop>
+┃  │       <k>
+┃  │         addCounter ( N:Int +Int -1 )
+┃  │         ~> K_CELL_fc656f08:K
+┃  │       </k>
+┃  │       <counter>
+┃  │         C:Int +Int 1
+┃  │       </counter>
+┃  │       <sum>
+┃  │         S:Int +Int C:Int
+┃  │       </sum>
+┃  │       <generatedCounter>
+┃  │         GENERATEDCOUNTER_CELL_949ec677:Int
+┃  │       </generatedCounter>
+┃  │     </generatedTop>
+┃  │     #And { true #Equals N:Int >Int 0 }
+┃  │     #And { true #Equals N:Int >=Int 0 }
+┃  │
+┃  │  (1 step)
+┃  ├─ 5
+┃  │     <generatedTop>
+┃  │       <k>
+┃  │         K_CELL_fc656f08:K
+┃  │       </k>
+┃  │       <counter>
+┃  │         ?_COUNTER_CELL_af8c44a5:Int
+┃  │       </counter>
+┃  │       <sum>
+┃  │         S:Int +Int C:Int +Int N:Int +Int -1 *Int C:Int +Int 1 +Int N:Int +Int -2 *Int N:Int +Int -1 /Int 2
+┃  │       </sum>
+┃  │       <generatedCounter>
+┃  │         ?_GENERATEDCOUNTER_CELL_5e3e01ba:Int
+┃  │       </generatedCounter>
+┃  │     </generatedTop>
+┃  │     #And { true #Equals N:Int >Int 0 }
+┃  │     #And { true #Equals N:Int >=Int 0 }
+┃  │     #And { true #Equals N:Int +Int -1 >=Int 0 }
+┃  │
+┃  ┊  constraint: OMITTED CONSTRAINT
+┃  ┊  subst: OMITTED SUBST
+┃  └─ 2 (leaf, target)
+┃        <generatedTop>
+┃          <k>
+┃            K_CELL_fc656f08:K ~> .K
+┃          </k>
+┃          <counter>
+┃            COUNTER_CELL_af8c44a5:Int
+┃          </counter>
+┃          <sum>
+┃            ?S:Int
+┃          </sum>
+┃          <generatedCounter>
+┃            GENERATEDCOUNTER_CELL_5e3e01ba:Int
+┃          </generatedCounter>
+┃        </generatedTop>
+┃        #And { true #Equals N:Int >=Int 0 }
+┃        #And { true #Equals ?S:Int ==Int S:Int +Int N:Int *Int C:Int +Int N:Int -Int 1 *Int N:Int /Int 2 }
+┃
+┗━━┓
+   │
+   ├─ 4
+   │     <generatedTop>
+   │       <k>
+   │         K_CELL_fc656f08:K
+   │       </k>
+   │       <counter>
+   │         C:Int
+   │       </counter>
+   │       <sum>
+   │         S:Int
+   │       </sum>
+   │       <generatedCounter>
+   │         GENERATEDCOUNTER_CELL_949ec677:Int
+   │       </generatedCounter>
+   │     </generatedTop>
+   │     #And { N:Int #Equals 0 }
+   │
+   ┊  constraint: OMITTED CONSTRAINT
+   ┊  subst: OMITTED SUBST
+   └─ 2 (leaf, target)
+         <generatedTop>
+           <k>
+             K_CELL_fc656f08:K ~> .K
+           </k>
+           <counter>
+             COUNTER_CELL_af8c44a5:Int
+           </counter>
+           <sum>
+             ?S:Int
+           </sum>
+           <generatedCounter>
+             GENERATEDCOUNTER_CELL_5e3e01ba:Int
+           </generatedCounter>
+         </generatedTop>
+         #And { true #Equals N:Int >=Int 0 }
+         #And { true #Equals ?S:Int ==Int S:Int +Int N:Int *Int C:Int +Int N:Int -Int 1 *Int N:Int /Int 2 }
+
+
+
+

regression-new/kprove-haskell/test-fail-spec.k.out

@@ -26,3 +26,40 @@ Failing nodes:
   Failed to generate a model.
 
 Join the Runtime Verification Discord server for support: https://discord.gg/CurfmXNtbN
+
+┌─ 1 (root, stuck, leaf, init)
+│     <generatedTop>
+│       <k>
+│         doIt ( -3 )
+│         ~> K_CELL_fc656f08:K
+│       </k>
+│       <counter>
+│         COUNTER_CELL
+│       </counter>
+│       <sum>
+│         SUM_CELL
+│       </sum>
+│       <generatedCounter>
+│         GENERATEDCOUNTER_CELL_c84b0b5f:Int
+│       </generatedCounter>
+│     </generatedTop>
+
+┌─ 2 (root, leaf, target)
+│     <generatedTop>
+│       <k>
+│         doIt ( 0 )
+│         ~> K_CELL_fc656f08:K
+│       </k>
+│       <counter>
+│         COUNTER_CELL
+│       </counter>
+│       <sum>
+│         SUM_CELL
+│       </sum>
+│       <generatedCounter>
+│         GENERATEDCOUNTER_CELL_6de8d71b:Int
+│       </generatedCounter>
+│     </generatedTop>
+
+
+

regression-new/kprove-haskell/test-spec.k.out

@@ -11,3 +11,61 @@ APRProof: 8b72c409e7e4e821e957233b93c93d850e4c2f79fa4be4a12f32ab064030dce7
     bounded: 0
     execution time: 0s
 Subproofs: 0
+
+┌─ 1 (root, init)
+│     <generatedTop>
+│       <k>
+│         doIt ( 3 )
+│         ~> K_CELL_fc656f08:K
+│       </k>
+│       <counter>
+│         COUNTER_CELL
+│       </counter>
+│       <sum>
+│         SUM_CELL
+│       </sum>
+│       <generatedCounter>
+│         GENERATEDCOUNTER_CELL_c84b0b5f:Int
+│       </generatedCounter>
+│     </generatedTop>
+│
+│  (3 steps)
+├─ 3
+│     <generatedTop>
+│       <k>
+│         doIt ( 0 )
+│         ~> K_CELL_fc656f08:K
+│       </k>
+│       <counter>
+│         COUNTER_CELL:Int
+│       </counter>
+│       <sum>
+│         SUM_CELL:Int
+│       </sum>
+│       <generatedCounter>
+│         GENERATEDCOUNTER_CELL_c84b0b5f:Int
+│       </generatedCounter>
+│     </generatedTop>
+│
+┊  constraint: true
+┊  subst: GENERATEDCOUNTER_CELL_6de8d71b <- GENERATEDCOUNTER_CELL_c84b0b5f:Int
+└─ 2 (leaf, target)
+      <generatedTop>
+        <k>
+          doIt ( 0 )
+          ~> K_CELL_fc656f08:K
+        </k>
+        <counter>
+          COUNTER_CELL
+        </counter>
+        <sum>
+          SUM_CELL
+        </sum>
+        <generatedCounter>
+          GENERATEDCOUNTER_CELL_6de8d71b:Int
+        </generatedCounter>
+      </generatedTop>
+
+
+
+

src/pyk/__main__.py

@@ -13,7 +13,7 @@
 
 from .cli.args import KCLIArgs
 from .cli.pyk import generate_options
-from .cli.utils import LOG_FORMAT, dir_path, file_path, loglevel
+from .cli.utils import LOG_FORMAT, dir_path, loglevel
 from .coverage import get_rule_by_id, strip_coverage_logger
 from .cterm import CTerm
 from .kast.inner import KInner
@@ -30,14 +30,14 @@
 from .kore.parser import KoreParser
 from .kore.rpc import ExecuteResult, StopReason
 from .kore.syntax import Pattern, kore_term
-from .ktool import TypeInferenceMode
 from .ktool.kompile import Kompile, KompileBackend
 from .ktool.kprint import KPrint
 from .ktool.kprove import KProve
 from .ktool.krun import KRun
 from .prelude.k import GENERATED_TOP_CELL
 from .prelude.ml import is_top, mlAnd, mlOr
-from .proof.reachability import APRFailureInfo
+from .proof.reachability import APRFailureInfo, APRProof
+from .proof.show import APRProofNodePrinter, APRProofShow
 from .utils import check_file_path, ensure_dir_path, exit_with_process_error
 
 if TYPE_CHECKING:
@@ -248,17 +248,32 @@ def exec_prove(options: ProveOptions) -> None:
         _LOGGER.info(f'Using kompiled directory: {kompiled_directory}.')
     else:
         kompiled_directory = options.definition_dir
-    kprove = KProve(kompiled_directory)
-    proofs = kprove.prove_rpc(options=options)
+    kprove = KProve(kompiled_directory, use_directory=options.temp_directory)
+    try:
+        proofs = kprove.prove_rpc(options=options)
+    except RuntimeError as err:
+        _, _, _, cpe = err.args
+        exit_with_process_error(cpe)
     for proof in sorted(proofs, key=lambda p: p.id):
         print('\n'.join(proof.summary.lines))
         if proof.failed and options.failure_info:
             failure_info = proof.failure_info
             if type(failure_info) is APRFailureInfo:
                 print('\n'.join(failure_info.print()))
+        if options.show_kcfg and type(proof) is APRProof:
+            node_printer = APRProofNodePrinter(proof, kprove, full_printer=True, minimize=False)
+            show = APRProofShow(kprove, node_printer=node_printer)
+            print('\n'.join(show.show(proof)))
     sys.exit(len([p.id for p in proofs if not p.passed]))
 
 
+def exec_show(options: ProveOptions) -> None:
+    options.max_iterations = 0
+    options.show_kcfg = True
+    options.failure_info = True
+    exec_prove(options)
+
+
 def exec_kompile(options: KompileCommandOptions) -> None:
     main_file = Path(options.main_file)
     check_file_path(main_file)
@@ -453,15 +468,39 @@ def create_argument_parser() -> ArgumentParser:
     prove_args = pyk_args_command.add_parser(
         'prove',
         help='Prove an input specification (using RPC based prover).',
-        parents=[k_cli_args.logging_args],
+        parents=[k_cli_args.logging_args, k_cli_args.spec_args],
     )
-    prove_args.add_argument('spec_file', type=file_path, help='File with the specification module.')
-    prove_args.add_argument('--definition', type=dir_path, dest='definition_dir', help='Path to definition to use.')
-    prove_args.add_argument('--spec-module', dest='spec_module', type=str, help='Module with claims to be proven.')
     prove_args.add_argument(
-        '--type-inference-mode', type=TypeInferenceMode, help='Mode for doing K rule type inference in.'
+        '--failure-info',
+        default=None,
+        action='store_true',
+        help='Print out more information about proof failures.',
     )
     prove_args.add_argument(
+        '--show-kcfg',
+        default=None,
+        action='store_true',
+        help='Display the resulting proof KCFG.',
+    )
+    prove_args.add_argument(
+        '--max-depth',
+        default=None,
+        type=int,
+        help='Maximum number of steps to take in symbolic execution per basic block.',
+    )
+    prove_args.add_argument(
+        '--max-iterations',
+        default=None,
+        type=int,
+        help='Maximum number of KCFG explorations to take in attempting to discharge proof.',
+    )
+
+    show_args = pyk_args_command.add_parser(
+        'show',
+        help='Display the status of a given proof.',
+        parents=[k_cli_args.logging_args, k_cli_args.spec_args],
+    )
+    show_args.add_argument(
         '--failure-info',
         default=None,
         action='store_true',