Remove kontrolx and associated tests/files

.github/workflows/Dockerfile

@@ -3,26 +3,19 @@ ARG K_VERSION
 ARG BASE_DISTRO
 ARG LLVM_VERSION
 
-FROM ghcr.io/foundry-rs/foundry:nightly-ca67d15f4abd46394b324c50e21e66f306a1162d as FOUNDRY
-
 ARG Z3_VERSION
 FROM runtimeverificationinc/z3:ubuntu-jammy-${Z3_VERSION} as Z3
 
 ARG K_VERSION
 FROM runtimeverificationinc/kframework-k:ubuntu-jammy-${K_VERSION}
 
-COPY --from=FOUNDRY /usr/local/bin/forge /usr/local/bin/forge
-COPY --from=FOUNDRY /usr/local/bin/anvil /usr/local/bin/anvil
-COPY --from=FOUNDRY /usr/local/bin/cast /usr/local/bin/cast
-
 COPY --from=Z3 /usr/bin/z3 /usr/bin/z3
 
 ARG LLVM_VERSION
 
 RUN    apt-get update                  \
     && apt-get upgrade --yes           \
     && apt-get install --yes           \
-            cargo                      \
             clang-${LLVM_VERSION}      \
             cmake                      \
             curl                       \
@@ -48,11 +41,7 @@ USER ${USER}:${GROUP}
 RUN mkdir /home/${USER}/workspace
 WORKDIR /home/${USER}/workspace
 
-ENV PATH=/home/${USER}/.cargo/bin:/home/${USER}/.local/bin:/usr/local/bin/:${PATH}
+ENV PATH=/home/${USER}/.local/bin:${PATH}
 
-RUN    curl -sSL https://install.python-poetry.org | python3 - \
+RUN    curl -sSL https://install.python-poetry.org | python3 - --version 1.6.1 \
     && poetry --version
-
-RUN    cargo install svm-rs --version 0.3.0 --locked \
-    && svm install 0.8.13                            \
-    && solc --version

.gitignore

@@ -10,17 +10,6 @@
 /package/src
 /pkg
 /tests/**/*.debug-log
-/tests/foundry/cache
-/tests/foundry/foundry.k
-/tests/foundry/foundry.k.check.stripped
-/tests/foundry/contracts.k.check.stripped
-/tests/foundry/foundry-list.check.stripped
-/tests/foundry/golden/*.out
-/tests/foundry/*.out
-/tests/foundry/out
-/tests/foundry/test/filecopy2.txt
-/tests/foundry/test/filecopy.txt
-/tests/foundry/test/fileline.txt
 /tests/**/*.rule-profile
 /tests/specs/foundry/*.out
 /tests/specs/**/haskell

Makefile

@@ -30,11 +30,6 @@ kevm-pyk: poetry-env
 test: test-integration test-conformance test-prove test-prove-pyk test-prove-kprove test-interactive
 
 
-# Foundry Tests
-
-test-foundry-prove: poetry
-	$(MAKE) -C kevm-pyk/ test-integration PYTEST_ARGS+="-k test_foundry_prove.py"
-
 # Conformance Tests
 
 test-conformance: poetry

README.md

@@ -47,7 +47,6 @@ These additional files extend the semantics to make the repository more useful:
 -   [abi.md](kevm-pyk/src/kevm_pyk/kproj/evm-semantics/abi.md) defines the [Contract ABI Specification](https://docs.soliditylang.org/en/v0.8.22/abi-spec.html) for use in proofs and easy contract/function specification.
 -   [hashed-locations.md](kevm-pyk/src/kevm_pyk/kproj/evm-semantics/hashed-locations.md) defines the `#hashedLocation` abstraction used to specify Solidity-generated storage layouts.
 -   [edsl.md](kevm-pyk/src/kevm_pyk/kproj/evm-semantics/edsl.md) combines the previous three abstractions for ease-of-use.
--   [foundry.md](kevm-pyk/src/kevm_pyk/kproj/evm-semantics/foundry.md) adds Foundry capabilities to KEVM.
 
 These files are used for testing the semantics itself:
 

flake.nix

@@ -25,21 +25,10 @@
       flake = false;
     };
     haskell-backend.follows = "k-framework/haskell-backend";
-    foundry = {
-      url =
-        "github:shazow/foundry.nix/monthly"; # Use monthly branch for permanent releases
-      inputs.nixpkgs.follows = "k-framework/nixpkgs";
-      inputs.flake-utils.follows = "k-framework/flake-utils";
-    };
-    solc = {
-      url = "github:hellwolf/solc.nix";
-      inputs.nixpkgs.follows = "k-framework/nixpkgs";
-      inputs.flake-utils.follows = "k-framework/flake-utils";
-    };
   };
   outputs = { self, k-framework, haskell-backend, nixpkgs, flake-utils
     , blockchain-k-plugin, ethereum-tests, ethereum-legacytests, rv-utils, pyk
-    , foundry, solc, ... }@inputs:
+    , ... }@inputs:
     let
       nixLibs = pkgs:
         with pkgs;
@@ -61,7 +50,6 @@
           pkg-config
           procps
           python310-pyk
-          (solc.mkDefault pkgs solc_0_8_13)
           time
         ] ++ lib.optional (!stdenv.isDarwin) elfutils;
 
@@ -125,14 +113,6 @@
                   k-framework.packages.${prev.system}.k
                 ]
               } --set NIX_LIBS "${nixLibs prev}" --set KEVM_DIST_DIR $out
-              makeWrapper ${final.kevm-pyk}/bin/kontrolx $out/bin/kontrolx --prefix PATH : ${
-                prev.lib.makeBinPath [
-                  (solc.mkDefault final final.solc_0_8_13)
-                  final.foundry-bin
-                  prev.which
-                  k-framework.packages.${prev.system}.k
-                ]
-              } --set NIX_LIBS "${nixLibs prev}" --set KEVM_DIST_DIR $out
             '';
           };
 
@@ -167,12 +147,6 @@
           kevm-pyk = poetry2nix.mkPoetryApplication {
             python = nixpkgs-pyk.python310;
             projectDir = ./kevm-pyk;
-
-            postPatch = ''
-              substituteInPlace ./src/kontrolx/foundry.py \
-                --replace "'forge', 'build'," "'forge', 'build', '--no-auto-detect',"
-            '';
-
             overrides = poetry2nix.overrides.withDefaults
               (finalPython: prevPython: {
                 pyk = nixpkgs-pyk.pyk-python310;
@@ -185,7 +159,6 @@
             groups = [ ];
             # We remove `"dev"` from `checkGroups`, so that poetry2nix does not try to resolve dev dependencies.
             checkGroups = [ ];
-
             postInstall = ''
               mkdir -p $out/${nixpkgs-pyk.python310.sitePackages}/kevm_pyk/kproj/plugin
               cp -rv ${prev.blockchain-k-plugin-src}/* $out/${nixpkgs-pyk.python310.sitePackages}/kevm_pyk/kproj/plugin/
@@ -209,8 +182,6 @@
             })
             k-framework.overlay
             blockchain-k-plugin.overlay
-            foundry.overlay
-            solc.overlay
             overlay
           ];
         };
@@ -219,7 +190,7 @@
         packages.default = kevm;
         devShell = pkgs.mkShell {
           buildInputs = buildInputs pkgs
-            ++ [ pkgs.poetry-nixpkgs pkgs.foundry-bin ];
+            ++ [ pkgs.poetry-nixpkgs ];
 
           shellHook = ''
             export NIX_LIBS="${nixLibs pkgs}"

kevm-pyk/pyproject.toml

@@ -9,10 +9,6 @@ description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",
 ]
-packages = [
-    { include = "kevm_pyk", from = "src/" },
-    { include = "kontrolx", from = "src/" },
-]
 
 [tool.poetry.dependencies]
 python = "^3.10"
@@ -45,7 +41,6 @@ kevm = "kevm_pyk.__main__:main"
 kevm-pyk = "kevm_pyk.__main__:main"
 kevm-dist = "kevm_pyk.kdist.__main__:main"
 gst-to-kore = "kevm_pyk.gst_to_kore:main"
-kontrolx = "kontrolx.__main__:main"
 
 [tool.poetry.plugins.kdist]
 evm-semantics = "kevm_pyk.kdist.plugin"

kevm-pyk/src/kevm_pyk/cli.py

@@ -2,11 +2,9 @@
 
 from argparse import ArgumentParser
 from functools import cached_property
-from pathlib import Path
 from typing import TYPE_CHECKING
 
 from pyk.cli.args import KCLIArgs
-from pyk.cli.utils import dir_path
 
 from .utils import arg_pair_of
 
@@ -150,25 +148,6 @@ def display_args(self) -> ArgumentParser:
         )
         return args
 
-    @cached_property
-    def foundry_args(self) -> ArgumentParser:
-        args = ArgumentParser(add_help=False)
-        args.add_argument(
-            '--foundry-project-root',
-            dest='foundry_root',
-            type=dir_path,
-            default=Path('.'),
-            help='Path to Foundry project root directory.',
-        )
-        return args
-
-    @cached_property
-    def foundry_test_args(self) -> ArgumentParser:
-        args = ArgumentParser(add_help=False)
-        args.add_argument('test', type=str, help='Test to run')
-        args.add_argument('--version', type=int, default=None, required=False, help='Version of the test to use')
-        return args
-
     @cached_property
     def rpc_args(self) -> ArgumentParser:
         args = ArgumentParser(add_help=False)

kevm-pyk/src/kevm_pyk/kevm.py

@@ -129,7 +129,6 @@ def cut_point_rules(break_on_jumpi: bool, break_on_calls: bool) -> list[str]:
                     'EVM.staticcall',
                     'EVM.create',
                     'EVM.create2',
-                    'FOUNDRY.foundry.call',
                     'EVM.end',
                     'EVM.return.exception',
                     'EVM.return.revert',