Factor out kontrol module from kevm-pyk codebase (#1985)

* kevm-pyk/src/kontrol: separate module for kontrol

* src/kevm_pyk: remove kontrol related functionality

* kevm-pyk/pyproject: expose kontrol binary

* kevm-pyk/src/kontrol/__init__: add stub init module

* kevm_pyk/src/tests: adjust for new kontrol module

* bin/kevm: route foundry-* commands through kontrol module

* Set Version: 1.0.244

* flake.nix: patch kontrol calls for nix builds too

* bin/kevm: add kontrol help to help message

* flake.nix: fix flake

* bin/kevm: correct syntax error

* bin/kevm, flake.nix: simplify calls to gst-to-kore/kontrol

* bin/kevm, flake.nix: simplify how kevm-pyk is invoked

* {kontrol,kevm_pyk}/__main__: adjust CLI name

* kevm-pyk/pyproject.toml: publish two separate packages

* package/docker/Dockerfile: try setting up PATH appropriately

* package/docker/Dockerfile: use newer version of poetry

* package/docker/Dockerfile: correct PATH

* Set Version: 1.0.250

* kevm-pyk/pyproject: publish packages correctly

* Set Version: 1.0.251

* Set Version: 1.0.252

* package/docker/Dockerfile: correct PATH

* Set Version: 1.0.254

* flake.nix: correct substitution for new file location

* Set Version: 1.0.261

* .github/test-pr: correct to normal runner for booster tests

---------

Co-authored-by: devops <[email protected]>

.github/workflows/test-pr.yml

@@ -171,7 +171,7 @@ jobs:
   test-prove-foundry-booster:
     name: 'Build and Test KEVM Foundry proofs (booster)'
     needs: kevm-pyk-code-quality-checks
-    runs-on: [self-hosted, linux, huge]
+    runs-on: [self-hosted, linux, normal]
     timeout-minutes: 150
     steps:
       - name: 'Check out code'

bin/kevm

@@ -49,14 +49,28 @@ run_kevm_pyk() {
     local pyk_command pyk_args
     pyk_command="$1" ; shift
     case "${pyk_command}" in
-        run|prove|prove-legacy|solc-to-k|foundry-kompile|foundry-prove|view-kcfg|show-kcfg|prune-proof)
+        run|prove|prove-legacy|view-kcfg|show-kcfg|prune-proof)
             pyk_args=(--definition "${backend_dir}")
             pyk_args+=(-I "${INSTALL_INCLUDE}/kframework")
             ;;
     esac
     ! ${verbose} || pyk_args+=(--verbose)
     ! ${debug}   || pyk_args+=(--debug)
-    execute python3 -m kevm_pyk "${pyk_command}" "$@" "${pyk_args[@]}"
+    execute kevm-pyk "${pyk_command}" "$@" "${pyk_args[@]}"
+}
+
+run_kontrol() {
+    local pyk_command pyk_args
+    pyk_command="$1" ; shift
+    case "${pyk_command}" in
+        solc-to-k|foundry-kompile|foundry-prove)
+            pyk_args=(--definition "${backend_dir}")
+            pyk_args+=(-I "${INSTALL_INCLUDE}/kframework")
+            ;;
+    esac
+    ! ${verbose} || pyk_args+=(--verbose)
+    ! ${debug}   || pyk_args+=(--debug)
+    execute kontrol "${pyk_command}" "$@" "${pyk_args[@]}"
 }
 
 # User Commands
@@ -94,8 +108,8 @@ run_kast() {
     fi
 
     case "${run_file}-${output_mode}" in
-        *.json-kore) check_k_install ; gst-to-kore "${run_file}" --schedule "${schedule}" --mode "${mode}" --chainid "${chainid}" "$@" ;;
-        *)           check_k_install ; kast --definition "${backend_dir}" "${run_file}" --output "${output_mode}" "$@" ;;
+        *.json-kore) check_k_install ; execute gst-to-kore "${run_file}" --schedule "${schedule}" --mode "${mode}" --chainid "${chainid}" "$@" ;;
+        *)           check_k_install ; execute kast --definition "${backend_dir}" "${run_file}" --output "${output_mode}" "$@" ;;
     esac
 }
 
@@ -138,6 +152,7 @@ if [[ "$run_command" == 'help' ]] || [[ "$run_command" == '--help' ]] ; then
     "
 
     run_kevm_pyk --help
+    run_kontrol --help
     exit 0
 fi
 
@@ -193,6 +208,7 @@ fi
 case "$run_command-$backend" in
     run-@(llvm|haskell|haskell-standalone) ) run_krun "$@" ;;
     kast-@(llvm|haskell)                   ) run_kast "$@" ;;
-    @(kompile|prune-proof|view-kcfg|show-kcfg|solc-to-k|prove|prove-legacy|foundry)-* ) run_kevm_pyk ${run_command} "$@" ;;
+    @(solc|compile|foundry)* )               run_kontrol ${run_command} "$@" ;;
+    @(kompile|prune-proof|view-kcfg|show-kcfg|prove|prove-legacy)-* ) run_kevm_pyk ${run_command} "$@" ;;
     *) ${KEVM} help ; fatal "Unknown command on backend: $run_command $backend" ;;
 esac

flake.nix

@@ -91,9 +91,11 @@
               substituteInPlace ./cmake/node/CMakeLists.txt \
                 --replace 'set(K_LIB ''${K_BIN}/../lib)' 'set(K_LIB ${k}/lib)'
               substituteInPlace ./bin/kevm \
-                --replace 'execute python3 -m kevm_pyk' 'execute ${final.kevm-pyk}/bin/kevm-pyk'
+                --replace 'execute kevm-pyk' 'execute ${final.kevm-pyk}/bin/kevm-pyk'
               substituteInPlace ./bin/kevm \
-                --replace 'gst-to-kore' '${final.kevm-pyk}/bin/gst-to-kore'
+                --replace 'execute kontrol' 'execute ${final.kevm-pyk}/bin/kontrol'
+              substituteInPlace ./bin/kevm \
+                --replace 'execute gst-to-kore' 'execute ${final.kevm-pyk}/bin/gst-to-kore'
             '';
 
             buildFlagsArray = "NIX_LIBS=${nixLibs prev}";
@@ -154,7 +156,7 @@
           projectDir = ./kevm-pyk;
 
           postPatch = ''
-              substituteInPlace ./src/kevm_pyk/foundry.py \
+              substituteInPlace ./src/kontrol/foundry.py \
                 --replace "'forge', 'build'," "'forge', 'build', '--no-auto-detect',"
             '';
 

kevm-pyk/pyproject.toml

@@ -4,11 +4,15 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.260"
+version = "1.0.261"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",
 ]
+packages = [
+    { include = "kevm_pyk", from = "src/" },
+    { include = "kontrol", from = "src/" },
+]
 
 [tool.poetry.dependencies]
 python = "^3.10"
@@ -36,6 +40,7 @@ pyupgrade = "*"
 [tool.poetry.scripts]
 kevm-pyk = "kevm_pyk.__main__:main"
 gst-to-kore = "kevm_pyk.gst_to_kore:main"
+kontrol = "kontrol.__main__:main"
 
 [tool.isort]
 profile = "black"