Add new Kontrol CLI args (#774)

* view-kcfg: add --use-hex-encoding arg

* update kontrol.toml template

* formatting

* add --optimize-performance flag

* rm kore-rpc-options from apply_optimizations

* Update src/kontrol/cli.py

Co-authored-by: Petar Maksimović <PetarMax@users.noreply.github.com>

* Update options.py

Co-authored-by: Petar Maksimović <PetarMax@users.noreply.github.com>

* Update options.py

Co-authored-by: Petar Maksimović <PetarMax@users.noreply.github.com>

* Update src/kontrol/cli.py

Co-authored-by: Palina Tolmach <polina.tolmach@gmail.com>

---------

Co-authored-by: Petar Maksimović <PetarMax@users.noreply.github.com>
Co-authored-by: Palina Tolmach <polina.tolmach@gmail.com>

src/kontrol/__main__.py

@@ -330,7 +330,9 @@ def exec_list(options: ListOptions) -> None:
 
 
 def exec_view_kcfg(options: ViewKcfgOptions) -> None:
-    foundry = _load_foundry(options.foundry_root, use_hex_encoding=True, add_enum_constraints=options.enum_constraints)
+    foundry = _load_foundry(
+        options.foundry_root, use_hex_encoding=options.use_hex_encoding, add_enum_constraints=options.enum_constraints
+    )
     test_id = foundry.get_test_id(options.test, options.version)
     contract_name, _ = test_id.split('.')
     proof = foundry.get_apr_proof(test_id)

src/kontrol/cli.py

@@ -552,6 +552,17 @@ def parse(s: str) -> list[T]:
         action='store_true',
         help='Remove all outdated KCFGs.',
     )
+    prove_args.add_argument(
+        '--optimize-performance',
+        type=int,
+        default=None,
+        dest='optimize_performance',
+        help=(
+            'Optimize performance for proof execution. Takes the number of parallel threads to be used.'
+            "Will overwrite other settings of 'assume-defined', 'log-success-rewrites', 'max-frontier-parallel',"
+            "'maintenance-rate', 'smt-timeout', 'smt-retry-limit', 'max-depth', and 'max-iterations'."
+        ),
+    )
 
     show_args = command_parser.add_parser(
         'show',
@@ -623,7 +634,7 @@ def parse(s: str) -> list[T]:
         ],
     )
 
-    command_parser.add_parser(
+    view_kcfg_args = command_parser.add_parser(
         'view-kcfg',
         help='Explore a given proof in the KCFG visualizer.',
         parents=[
@@ -634,6 +645,14 @@ def parse(s: str) -> list[T]:
         ],
     )
 
+    view_kcfg_args.add_argument(
+        '--use-hex-encoding',
+        dest='use_hex_encoding',
+        default=None,
+        action='store_true',
+        help='Print elements in hexadecimal encoding.',
+    )
+
     command_parser.add_parser(
         'minimize-proof',
         help='Minimize the KCFG of the proof for a given test.',

src/kontrol/options.py

@@ -368,6 +368,11 @@ class ProveOptions(
     config_type: ConfigType
     hide_status_bar: bool
     remove_old_proofs: bool
+    optimize_performance: int | None
+
+    def __init__(self, args: dict[str, Any]) -> None:
+        super().__init__(args)
+        self.apply_optimizations()
 
     @staticmethod
     def default() -> dict[str, Any]:
@@ -391,6 +396,7 @@ def default() -> dict[str, Any]:
             'config_type': ConfigType.TEST_CONFIG,
             'hide_status_bar': False,
             'remove_old_proofs': False,
+            'optimize_performance': None,
         }
 
     @staticmethod
@@ -434,6 +440,24 @@ def get_argument_type() -> dict[str, Callable]:
             }
         )
 
+    def apply_optimizations(self) -> None:
+        """Applies a series of performance optimizations based on the value of the
+        `optimize_performance` attribute.
+
+        If `optimize_performance` is not `None`, this method will adjust several
+        internal parameters to enhance performance. The integer value of `optimize_performance`
+        is used to set the level of parallelism for frontier exploration and maintenance rate.
+        """
+        if self.optimize_performance is not None:
+            self.assume_defined = True
+            self.log_succ_rewrites = False
+            self.max_frontier_parallel = self.optimize_performance
+            self.maintenance_rate = 2 * self.optimize_performance
+            self.smt_timeout = 120000
+            self.smt_retry_limit = 0
+            self.max_depth = 100000
+            self.max_iterations = 10000
+
 
 class RefuteNodeOptions(LoggingOptions, FoundryTestOptions, FoundryOptions):
     node: NodeIdLike
@@ -747,6 +771,15 @@ def get_argument_type() -> dict[str, Callable]:
 
 
 class ViewKcfgOptions(FoundryTestOptions, LoggingOptions, FoundryOptions):
+
+    use_hex_encoding: bool
+
+    @staticmethod
+    def default() -> dict[str, Any]:
+        return {
+            'use_hex_encoding': False,
+        }
+
     @staticmethod
     def from_option_string() -> dict[str, str]:
         return (

src/kontrol/utils.py

@@ -174,8 +174,13 @@ def kontrol_toml_file_contents() -> str:
 
 [show.default]
 foundry-project-root       = '.'
-verbose                    = true
+verbose                    = false
 debug                      = false
+use-hex-encoding           = false
+
+[view-kcfg.default]
+foundry-project-root       = '.'
+use-hex-encoding           = false
 """