Make booster the default

.github/workflows/test-pr.yml

@@ -85,7 +85,7 @@ jobs:
       - name: 'Run profiling'
         run: |
           PROF_ARGS=--numprocesses=8
-          [ ${{ matrix.backend }} == 'booster' ] && PROF_ARGS+=' --use-booster'
+          [ ${{ matrix.backend }} == 'legacy' ] && PROF_ARGS+=' --no-use-booster'
           docker exec -u github-user kontrol-ci-profile-${GITHUB_SHA} make profile PROF_ARGS="${PROF_ARGS}"
       - name: 'Tear down Docker'
         if: always()
@@ -117,7 +117,7 @@ jobs:
       - name: 'Run integration tests'
         run: |
           TEST_ARGS=--numprocesses=8
-          [ ${{ matrix.backend }} == 'booster' ] && TEST_ARGS+=' --use-booster'
+          [ ${{ matrix.backend }} == 'legacy' ] && TEST_ARGS+=' --no-use-booster'
           docker exec --user github-user kontrol-ci-integration-${GITHUB_SHA} make cov-integration TEST_ARGS="${TEST_ARGS}"
       - name: 'Tear down Docker'
         if: always()
@@ -173,7 +173,7 @@ jobs:
       - name: 'Run kontrol build'
         run: docker exec --user ${DOCKER_USER} --workdir ${FOUNDRY_ROOT} ${CONTAINER_NAME} kontrol build
       - name: 'Run kontrol prove'
-        run: docker exec --user ${DOCKER_USER} --workdir ${FOUNDRY_ROOT} ${CONTAINER_NAME} kontrol prove --use-booster --match-test 'AssertTest.test_assert_true()'
+        run: docker exec --user ${DOCKER_USER} --workdir ${FOUNDRY_ROOT} ${CONTAINER_NAME} kontrol prove --match-test 'AssertTest.test_assert_true()'
       - name: 'Run kontrol show'
         run: docker exec --user ${DOCKER_USER} --workdir ${FOUNDRY_ROOT} ${CONTAINER_NAME} kontrol show 'AssertTest.test_assert_true()'
       - name: 'Tear down Docker'

package/version

@@ -1 +1 @@
-0.1.97
+0.1.98

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.97"
+version = "0.1.98"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

src/kontrol/__init__.py

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

src/kontrol/__main__.py

@@ -217,7 +217,7 @@ def exec_prove(
     bmc_depth: int | None = None,
     bug_report: BugReport | None = None,
     kore_rpc_command: str | Iterable[str] | None = None,
-    use_booster: bool = False,
+    use_booster: bool = True,
     smt_timeout: int | None = None,
     smt_retry_limit: int | None = None,
     smt_tactic: str | None = None,

src/kontrol/cli.py

@@ -85,10 +85,16 @@ def rpc_args(self) -> ArgumentParser:
         args.add_argument(
             '--use-booster',
             dest='use_booster',
-            default=False,
+            default=True,
             action='store_true',
             help='Use the booster RPC server instead of kore-rpc.',
         )
+        args.add_argument(
+            '--no-use-booster',
+            dest='use_booster',
+            action='store_false',
+            help='Do not use the booster RPC server instead of kore-rpc.',
+        )
         args.add_argument(
             '--port',
             dest='port',

src/tests/conftest.py

@@ -24,10 +24,10 @@ def pytest_addoption(parser: Parser) -> None:
         help='Write expected output files for proof tests',
     )
     parser.addoption(
-        '--use-booster',
+        '--no-use-booster',
         action='store_true',
         default=False,
-        help='Use the kore-rpc-booster binary instead of kore-rpc',
+        help='Use the kore-rpc binary instead of kore-rpc-booster',
     )
 
 
@@ -42,5 +42,5 @@ def update_expected_output(request: FixtureRequest) -> bool:
 
 
 @pytest.fixture(scope='session')
-def use_booster(request: FixtureRequest) -> bool:
-    return request.config.getoption('--use-booster')
+def no_use_booster(request: FixtureRequest) -> bool:
+    return request.config.getoption('--no-use-booster')

src/tests/integration/test_foundry_prove.py

@@ -42,9 +42,9 @@
 
 
 @pytest.fixture(scope='module')
-def server(foundry: Foundry, use_booster: bool) -> Iterator[KoreServer]:
-    llvm_definition_dir = foundry.out / 'kompiled' / 'llvm-library' if use_booster else None
-    kore_rpc_command = ('kore-rpc-booster',) if use_booster else ('kore-rpc',)
+def server(foundry: Foundry, no_use_booster: bool) -> Iterator[KoreServer]:
+    llvm_definition_dir = foundry.out / 'kompiled' / 'llvm-library' if not no_use_booster else None
+    kore_rpc_command = ('kore-rpc-booster',) if not no_use_booster else ('kore-rpc',)
 
     yield kore_server(
         definition_dir=foundry.kevm.definition_dir,
@@ -86,8 +86,8 @@ def foundry(foundry_root_dir: Path | None, tmp_path_factory: TempPathFactory, wo
     return Foundry(session_foundry_root)
 
 
-def test_foundry_kompile(foundry: Foundry, update_expected_output: bool, use_booster: bool) -> None:
-    if use_booster:
+def test_foundry_kompile(foundry: Foundry, update_expected_output: bool, no_use_booster: bool) -> None:
+    if not no_use_booster:
         return
     # Then
     assert_or_update_k_output(
@@ -130,13 +130,13 @@ def test_foundry_prove(
     test_id: str,
     foundry: Foundry,
     update_expected_output: bool,
-    use_booster: bool,
+    no_use_booster: bool,
     bug_report: BugReport | None,
     server: KoreServer,
 ) -> None:
     if (
         test_id in SKIPPED_PROVE_TESTS
-        or (not use_booster and test_id in SKIPPED_LEGACY_TESTS)
+        or (no_use_booster and test_id in SKIPPED_LEGACY_TESTS)
         or (update_expected_output and not test_id in SHOW_TESTS)
     ):
         pytest.skip()
@@ -157,7 +157,7 @@ def test_foundry_prove(
     # Then
     assert_pass(test_id, single(prove_res))
 
-    if test_id not in SHOW_TESTS or use_booster:
+    if test_id not in SHOW_TESTS or not no_use_booster:
         return
 
     # And when
@@ -186,7 +186,7 @@ def test_foundry_fail(
     test_id: str,
     foundry: Foundry,
     update_expected_output: bool,
-    use_booster: bool,
+    no_use_booster: bool,
     bug_report: BugReport | None,
     server: KoreServer,
 ) -> None:
@@ -206,7 +206,7 @@ def test_foundry_fail(
     # Then
     assert_fail(test_id, single(prove_res))
 
-    if test_id not in SHOW_TESTS or use_booster:
+    if test_id not in SHOW_TESTS or not no_use_booster:
         return
 
     # And when
@@ -319,7 +319,7 @@ def test_foundry_auto_abstraction(
     update_expected_output: bool,
     bug_report: BugReport | None,
     server: KoreServer,
-    use_booster: bool,
+    no_use_booster: bool,
 ) -> None:
     test_id = 'GasTest.testInfiniteGas()'
 
@@ -335,7 +335,7 @@ def test_foundry_auto_abstraction(
         ),
     )
 
-    if use_booster:
+    if not no_use_booster:
         return
 
     show_res = foundry_show(
@@ -478,7 +478,7 @@ def test_foundry_resume_proof(
 
 
 @pytest.mark.parametrize('test', ALL_INIT_CODE_TESTS)
-def test_foundry_init_code(test: str, foundry: Foundry, bug_report: BugReport | None, use_booster: bool) -> None:
+def test_foundry_init_code(test: str, foundry: Foundry, bug_report: BugReport | None, no_use_booster: bool) -> None:
     # When
     prove_res = foundry_prove(
         foundry,
@@ -490,7 +490,7 @@ def test_foundry_init_code(test: str, foundry: Foundry, bug_report: BugReport |
         rpc_options=RPCOptions(
             smt_timeout=300,
             smt_retry_limit=10,
-            use_booster=use_booster,
+            use_booster=not no_use_booster,
         ),
     )
 

src/tests/profiling/test_foundry_prove.py

@@ -27,7 +27,7 @@
 FORGE_STD_REF: Final = '75f1746'
 
 
-def test_foundy_prove(profile: Profiler, use_booster: bool, bug_report: BugReport | None, tmp_path: Path) -> None:
+def test_foundy_prove(profile: Profiler, no_use_booster: bool, bug_report: BugReport | None, tmp_path: Path) -> None:
     foundry_root = tmp_path / 'foundry'
     foundry = _forge_build(foundry_root)
 
@@ -45,7 +45,7 @@ def test_foundy_prove(profile: Profiler, use_booster: bool, bug_report: BugRepor
             rpc_options=RPCOptions(
                 smt_timeout=300,
                 smt_retry_limit=10,
-                use_booster=use_booster,
+                use_booster=not no_use_booster,
             ),
         )