Prebuild optimized definition

.github/workflows/test-pr.yml

@@ -52,10 +52,10 @@ jobs:
         uses: ./.github/actions/with-docker
         with:
           container-name: kontrol-ci-profile-${{ github.sha }}
-      - name: 'Build KEVM'
+      - name: 'Build Kontrol'
         run: |
             docker exec -u github-user kontrol-ci-profile-${GITHUB_SHA} /bin/bash -c 'poetry install'
-            docker exec -u github-user kontrol-ci-profile-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kdist --verbose build -j`nproc` kontrol.foundry'
+            docker exec -u github-user kontrol-ci-profile-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kdist --verbose build -j`nproc` kontrol.*'
       - name: 'Run profiling'
         run: |
           PROF_ARGS=--numprocesses=8
@@ -84,10 +84,10 @@ jobs:
         uses: ./.github/actions/with-docker
         with:
           container-name: kontrol-ci-integration-${{ github.sha }}
-      - name: 'Build KEVM'
+      - name: 'Build Kontrol'
         run: |
             docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'poetry install'
-            docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kdist --verbose build -j`nproc` evm-semantics.haskell kontrol.foundry'
+            docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kdist --verbose build -j`nproc` kontrol.*'
       - name: 'Run integration tests'
         run: |
           TEST_ARGS='-vv --force-sequential -k "not (test_kontrol_cse or test_foundry_minimize_proof or test_kontrol_end_to_end)"'
@@ -116,10 +116,10 @@ jobs:
         uses: ./.github/actions/with-docker
         with:
           container-name: kontrol-ci-integration-${{ github.sha }}
-      - name: 'Build KEVM'
+      - name: 'Build Kontrol'
         run: |
             docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'poetry install'
-            docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kdist --verbose build -j`nproc` evm-semantics.haskell kontrol.foundry'
+            docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kdist --verbose build -j`nproc` kontrol.*'
       - name: 'Run CSE and Minimize tests'
         run: |
           TEST_ARGS='--numprocesses=8 --force-sequential -vv -k "test_kontrol_cse or test_foundry_minimize_proof"'
@@ -143,10 +143,10 @@ jobs:
         uses: ./.github/actions/with-docker
         with:
           container-name: kontrol-ci-integration-${{ github.sha }}
-      - name: 'Build KEVM'
+      - name: 'Build Kontrol'
         run: |
             docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'poetry install'
-            docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kdist --verbose build -j`nproc` evm-semantics.haskell kontrol.foundry'
+            docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kdist --verbose build -j`nproc` kontrol.*'
       - name: 'Run end-to-end tests'
         run: |
           TEST_ARGS='--numprocesses=6 -vv --force-sequential -k "test_kontrol_end_to_end"'

.github/workflows/update-expected-output.yml

@@ -25,7 +25,7 @@ jobs:
       - name: 'Build Kontrol'
         run: |
             docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'poetry install'
-            docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kdist --verbose build -j`nproc` evm-semantics.haskell kontrol.foundry'
+            docker exec -u github-user kontrol-ci-integration-${GITHUB_SHA} /bin/bash -c 'CXX=clang++-14 poetry run kdist --verbose build -j`nproc` kontrol.*'
       - name: 'Run integration tests'
         run: |
           TEST_ARGS="--maxfail=1000 --numprocesses=2 --update-expected-output --force-sequential -vv"

CONTRIBUTING.md

@@ -29,7 +29,7 @@ The first step is to develop and test your changes locally.
 kup install k.openssl.secp256k1 --version v$(cat deps/k_release)
 poetry install
 poetry run kdist clean
-CXX=clang++-14 poetry run kdist --verbose build -j2 evm-semantics.haskell kontrol.foundry
+CXX=clang++-14 poetry run kdist --verbose build -j2 kontrol.*
 ```
 (see more detailed instructions [here](https://github.com/runtimeverification/kontrol?tab=readme-ov-file#build-from-source))
 

README.md

@@ -34,19 +34,21 @@ poetry install
 
 #### Build using the virtual environment
 
-In order to build `kontrol`, you need to build these specific targets:
+In order to build `kontrol`, you need to build these specific targets.
+Note that you can use `kontrol.base` (without [keccak](https://github.com/runtimeverification/kontrol/blob/master/src/kontrol/kdist/keccak.md) or [aux](https://github.com/runtimeverification/kontrol/blob/master/src/kontrol/kdist/kontrol_lemmas.md) lemmas), `kontrol.aux` (with aux lemmas), `kontrol.keccak` (with keccak lemmas) and `kontrol.full` (with all lemmas) instead of `kontrol.*` (which builds them all).
+
 ```sh
-poetry run kdist --verbose build -j2 evm-semantics.haskell kontrol.foundry
+poetry run kdist --verbose build -j2 kontrol.*
 ```
 
 To change the default compiler:
 ```sh
-CXX=clang++-14 poetry run kdist --verbose build -j2 evm-semantics.haskell kontrol.foundry
+CXX=clang++-14 poetry run kdist --verbose build -j2 kontrol.*
 ```
 
 On Apple Silicon:
 ```sh
-APPLE_SILICON=true poetry run kdist --verbose build -j2 evm-semantics.haskell kontrol.foundry
+APPLE_SILICON=true poetry run kdist --verbose build -j2 kontrol.*
 ```
 
 Targets can be cleaned with:

flake.nix

@@ -89,7 +89,7 @@
                   prev.lib.optionalString
                   (prev.stdenv.isAarch64 && prev.stdenv.isDarwin)
                   "APPLE_SILICON=true"
-                } kdist -v build kontrol.foundry
+                } kdist -v build kontrol.base
               '';
 
               installPhase = ''

src/kontrol/cli.py

@@ -587,7 +587,7 @@ def parse(s: str) -> list[T]:
         dest='extra_module',
         default=None,
         help=(
-            'File and extra module to include for verification (which must import FOUNDRY-MAIN module).'
+            'File and extra module to include for verification (which must import KONTROL-MAIN module).'
             'Format is <file>:<module name>.'
         ),
     )

src/kontrol/foundry.py

@@ -258,7 +258,7 @@ def _filter_constraints_by_simplification(
 
         # Set up initial configuration for constraint simplification, and simplify it to get all
         # of the kept constraints in the form in which they will appear after constraint simplification
-        kevm = KEVM(kdist.get('kontrol.foundry'))
+        kevm = KEVM(kdist.get('kontrol.base'))
         empty_config: CTerm = CTerm.from_kast(kevm.definition.empty_config(GENERATED_TOP_CELL))
         initial_cterm, _ = cterm_symbolic.simplify(CTerm(empty_config.config, constraints_to_keep))
         constraints_to_keep = set(initial_cterm.constraints)

src/kontrol/kdist/kontrol.md

@@ -0,0 +1,34 @@
+Kontrol Definitions
+===================
+
+This file defines the pre-built Kontrol definitions you get with a fresh install of Kontrol.
+They include the base Foundry definition, and some optional lemmas (using command-line arguments to specify which ones to include).
+
+```k
+requires "foundry.md"
+requires "no_stack_checks.md"
+requires "no_code_size_checks.md"
+requires "keccak.md"
+requires "kontrol_lemmas.md"
+
+module KONTROL-BASE
+    imports FOUNDRY
+    imports NO-STACK-CHECKS
+    imports NO-CODE-SIZE-CHECKS
+endmodule
+
+module KONTROL-AUX
+    imports KONTROL-BASE
+    imports KONTROL-AUX-LEMMAS
+endmodule
+
+module KONTROL-KECCAK
+    imports KONTROL-BASE
+    imports KECCAK-LEMMAS
+endmodule
+
+module KONTROL-FULL
+    imports KONTROL-AUX
+    imports KONTROL-KECCAK
+endmodule
+```

src/kontrol/kdist/no_code_size_checks.md

@@ -38,8 +38,7 @@ module NO-CODE-SIZE-CHECKS
            <nonce> NONCE </nonce>
            ...
          </account>
-         <schedule> SCHED </schedule>
       [preserves-definedness, priority(30)]
 
 endmodule
-```
+```

src/kontrol/kdist/plugin.py

@@ -12,12 +12,36 @@
 
 
 __TARGETS__: Final = {
-    'foundry': KEVMTarget(
+    'base': KEVMTarget(
         {
             'target': KompileTarget.HASKELL,
-            'main_file': KSRC_DIR / 'foundry.md',
-            'main_module': 'FOUNDRY',
-            'syntax_module': 'FOUNDRY',
+            'main_file': KSRC_DIR / 'kontrol.md',
+            'main_module': 'KONTROL-BASE',
+            'syntax_module': 'KONTROL-BASE',
+        },
+    ),
+    'keccak': KEVMTarget(
+        {
+            'target': KompileTarget.HASKELL,
+            'main_file': KSRC_DIR / 'kontrol.md',
+            'main_module': 'KONTROL-KECCAK',
+            'syntax_module': 'KONTROL-KECCAK',
+        },
+    ),
+    'aux': KEVMTarget(
+        {
+            'target': KompileTarget.HASKELL,
+            'main_file': KSRC_DIR / 'kontrol.md',
+            'main_module': 'KONTROL-AUX',
+            'syntax_module': 'KONTROL-AUX',
+        },
+    ),
+    'full': KEVMTarget(
+        {
+            'target': KompileTarget.HASKELL,
+            'main_file': KSRC_DIR / 'kontrol.md',
+            'main_module': 'KONTROL-FULL',
+            'syntax_module': 'KONTROL-FULL',
         },
     ),
 }

src/kontrol/kompile.py

@@ -34,7 +34,14 @@ def foundry_kompile(
 ) -> None:
     foundry_requires_dir = foundry.kompiled / 'requires'
     kompiled_timestamp = foundry.kompiled / 'timestamp'
-    main_module = 'FOUNDRY-MAIN'
+    main_module = 'KONTROL-MAIN'
+    base_definition = 'KONTROL-BASE'
+    if options.keccak_lemmas and not options.auxiliary_lemmas:
+        base_definition = 'KONTROL-KECCAK'
+    elif not options.keccak_lemmas and options.auxiliary_lemmas:
+        base_definition = 'KONTROL-AUX'
+    else:
+        base_definition = 'KONTROL-FULL'
     includes = [Path(include) for include in options.includes if Path(include).exists()] + [KSRC_DIR]
     requires_paths: dict[str, str] = {}
 
@@ -56,15 +63,7 @@ def foundry_kompile(
         foundry_up_to_date = False
 
     options.requires = [str(foundry._root / r) for r in options.requires]
-
-    requires = (
-        options.requires
-        + ([KSRC_DIR / 'keccak.md'] if options.keccak_lemmas else [])
-        + ([KSRC_DIR / 'kontrol_lemmas.md'] if options.auxiliary_lemmas else [])
-        + ([KSRC_DIR / 'no_stack_checks.md'])
-        + ([KSRC_DIR / 'no_code_size_checks.md'])
-    )
-    for r in tuple(requires):
+    for r in options.requires:
         req = Path(r)
         if not req.exists():
             raise ValueError(f'No such file: {req}')
@@ -107,13 +106,14 @@ def foundry_kompile(
         flattened_imports = list(unique([imp for module_imports in _imports.values() for imp in module_imports]))
         contract_main_definition = _foundry_to_main_def(
             main_module=main_module,
-            requires=(['foundry.md'] + copied_requires),
+            base_definition=base_definition,
+            requires=(['kontrol.md'] + copied_requires),
             imports=flattened_imports,
             keccak_lemmas=options.keccak_lemmas,
             auxiliary_lemmas=options.auxiliary_lemmas,
         )
 
-        kevm = KEVM(kdist.get('kontrol.foundry'))
+        kevm = KEVM(kdist.get('kontrol.base'))
         foundry.main_file.write_text(kevm.pretty_print(contract_main_definition) + '\n')
         _LOGGER.info(f'Wrote file: {foundry.main_file}')
 
@@ -174,20 +174,15 @@ def should_rekompile() -> bool:
 
 def _foundry_to_main_def(
     main_module: str,
+    base_definition: str,
     requires: Iterable[str],
     imports: list[str],
     keccak_lemmas: bool,
     auxiliary_lemmas: bool,
 ) -> KDefinition:
     _main_module = KFlatModule(
         main_module,
-        imports=tuple(
-            [KImport(imp) for imp in imports]
-            + ([KImport('KECCAK-LEMMAS')] if keccak_lemmas else [])
-            + ([KImport('KONTROL-AUX-LEMMAS')] if auxiliary_lemmas else [])
-            + ([KImport('NO-STACK-CHECKS')])
-            + ([KImport('NO-CODE-SIZE-CHECKS')])
-        ),
+        imports=tuple([KImport(imp) for imp in imports] + [KImport(base_definition)]),
     )
 
     return KDefinition(

src/kontrol/solc_to_k.py

@@ -31,7 +31,7 @@
 
 
 def solc_to_k(options: SolcToKOptions) -> str:
-    definition_dir = kdist.get('evm-semantics.haskell')
+    definition_dir = kdist.get('kontrol.base')
 
     solc_json = solc_compile(options.contract_file)
     contract_json = solc_json['contracts'][options.contract_file.name][options.contract_name]

src/tests/integration/test-data/show/foundry.k.expected

@@ -1,20 +1,15 @@
-requires "foundry.md"
+requires "kontrol.md"
 requires "requires/lemmas.k"
 requires "requires/cse-lemmas.k"
 requires "requires/pausability-lemmas.k"
 requires "requires/symbolic-bytes-lemmas.k"
-requires "requires/keccak.md"
-requires "requires/no_stack_checks.md"
-requires "requires/no_code_size_checks.md"
 
-module FOUNDRY-MAIN
+module KONTROL-MAIN
     imports public CSE-LEMMAS
     imports public SYMBOLIC-BYTES-LEMMAS
     imports public SUM-TO-N-INVARIANT
     imports public PAUSABILITY-LEMMAS
-    imports public KECCAK-LEMMAS
-    imports public NO-STACK-CHECKS
-    imports public NO-CODE-SIZE-CHECKS
+    imports public KONTROL-KECCAK
 
 
 

src/tests/integration/test-data/xor-lemmas.k

@@ -1,5 +1,5 @@
 module XOR-LEMMAS
-    imports FOUNDRY-MAIN
+    imports KONTROL-MAIN
 
     rule A xorInt A => 0 [simplification]