feat: portfolio pmplementation (#60)

* refactor

* setup baselines

* ovalbab mnist [skip ci]

* ovalbab experiments [skip ci]

* wip hydra update [skip ci]

* wip [skip ci]

* exp setup [skip ci]

* exp setup [skip ci]

* fix instances [skip ci]

* move func [skip ci]

* wt lim [skip ci]

* exps [skip ci]

* better err reporting [skip ci]

* setup exp [skip ci]

* tighten abcrown configspace [skip ci]

* eval scripts [skip ci]

* warmup param [skip ci]

* ready [skip ci]

* mnist cfg [skip ci]

* wip refactor [skip ci]

* delete bench [skip ci]

* wip refactor [skip ci]

* add onnx req [skip ci]

* fix no filter arg [skip ci]

* verinet fixes [skip ci]

* hacky verinet params [skip ci]

* start on tests, minor changes [skip ci]

* more tests, lib path fix [skip ci]

* update verinet commit hash [skip ci]

* nnenum cfg, more util tests [skip ci]

* update nnenum [skip ci]

* add more tests [skip ci]

* more tests [skip ci]

* eval scripts [skip ci]

* tuning and tempfile cleaning [skip ci]

* remove comment [skip ci]

* abcrown yaml override [skip ci]

* update verinet [skip ci]

* eval fix [skip ci]

* add and fix some tests [skip ci]

* update nnenum hash [skip ci]

* experiment setup [skip ci]

* create csv if it doesnt exist yet [skip ci]

* fix paths [skip ci]

* fix nnenum experiment params [skip ci]

* fix typo [skip ci]

* lib paths, smac util [skip ci]

* fix cli args [skip ci]

* remove print [skip ci]

* update nnenum hash [skip ci]

* bump smac, add more tests [skip ci]

* update eval script [skip ci]

* vnn-compat eval arg [skip ci]

* compat eval arg [skip ci]

* fix typo [skip ci]

* hydra setup

* mark gpu tests

* number of cores arg [skip ci]

* update allocation init [skip ci]

* hacky gpu alloc [skip ci]

* enable nnenum inf params again [skip ci]

* hydra picking

* mark more gpu test

* enable integration tests

* update marks

* shorten imports [skip ci]

* pf exp ready

* fix tests

* fix setting resource in hydra portfolio

* wip [skip ci]

* vbs runner wip [skip ci]

* fix timing out [skip ci]

* more accurate timeout

* remove dead code

* wip pf runner [skip ci]

* exit PF runner gracefully [skip ci]

* add csv logging back [skip ci]

* ecdf plot, update parsers [skip ci]

* types, lints, tests

* remove print

* check version cmd [skip ci]

* check if a gpu avail [skip ci]

* instance file arg name [skip ci]

* use simplified networks and verifier specific kwargs [skip ci]

* fix types and lints

* remove prints [skip ci]

* realloc if shorter len [skip ci]

* update verinet, arg passing in pf runner [skip ci]

* actually allocate in pf runner [skip ci]

* abcrown configspace rework [skip ci]

* fix using simple instance [skip ci]

* abcrown configspace more params [skip ci]

* update verinet commit hash [skip ci]

* uniq network func [skip ci]

* use simple net in eval [skip ci]

* update verinet hash [skip ci]

* cfgspace test [skip ci]

* remove print

* more tests [skip ci]

* docs start [skip ci]

* update abcrown cfgspace [skip ci]

* sync [skip ci]

* remove tempfiles [skip ci]

* fix type and lint [skip ci]

* update docs [skip ci]

* wip docstrings [skip ci]

* more docstrings [skip ci]

* mockable cpu/gpu counts for tests

* Update docstrings, remove debug prints

* fix mark name

* actually push tests

Dockerfile

@@ -19,7 +19,9 @@ RUN pip install -e '.[dev]' # dev reqs needed for tests
 # Check if installation was succesful
 RUN auto-verify --version
 RUN auto-verify install nnenum
-RUN auto-verify install abcrown
+# RUN auto-verify install abcrown
+# RUN auto-verify install verinet
+# RUN auto-verify install ovalbab
 
 RUN echo $'set +euo pipefail \n\
 conda activate av \n\
@@ -28,7 +30,7 @@ RUN chmod +x entrypoint.sh
 
 # Integration tests, should fail if installing went wrong. 
 # No GPU on gh-actions
-RUN if ! python -m pytest -v -m "not uses_gpu"; then exit 1; fi
+RUN if ! python -m pytest tests -v -m "not verifier"; then exit 1; fi
 
 ENTRYPOINT ["./entrypoint.sh"]
 # Clean up all images: docker rmi -f $(docker images -aq)

autoverify/__init__.py

@@ -2,4 +2,6 @@
 from pathlib import Path
 
 __version__ = "0.0.1"
+
 ROOT_DIR = Path(os.path.dirname(os.path.abspath(__file__)))
+DEFAULT_VERIFICATION_TIMEOUT_SEC = 600

autoverify/cli/install/__init__.py

@@ -2,6 +2,7 @@
     AV_HOME,
     TOOL_DIR_NAME,
     VERIFIER_DIR,
+    check_commit_hashes,
     try_install_verifiers,
     try_uninstall_verifiers,
 )
@@ -12,4 +13,5 @@
     "TOOL_DIR_NAME",
     "try_install_verifiers",
     "try_uninstall_verifiers",
+    "check_commit_hashes",
 ]

autoverify/cli/install/install.py

@@ -1,6 +1,9 @@
 """TODO summary."""
 import logging
+import shlex
 import shutil
+import subprocess
+from collections.abc import Iterable
 from subprocess import CalledProcessError
 
 from result import Err, Ok, Result
@@ -11,8 +14,9 @@
     get_av_conda_envs,
     get_verifier_conda_env_name,
 )
+from autoverify.util.env import cwd
 
-from .installers import installers
+from .installers import installers, repo_infos
 
 AV_HOME = xdg_data_home() / "autoverify"
 VERIFIER_DIR = AV_HOME / "verifiers"
@@ -81,8 +85,14 @@ def _install_verifier(verifier: str) -> Result[None, str]:
         return Err("Exception during installation")
 
 
-def try_install_verifiers(verifiers: list[str]):
-    """_summary_."""
+def try_install_verifiers(verifiers: Iterable[str]):
+    """Tries to install the specified verifiers.
+
+    Will print the result of each attempt to stdout.
+
+    Args:
+        verifiers: Names of the verifiers to install.
+    """
     _create_base_dirs()
 
     for verifier in verifiers:
@@ -96,8 +106,14 @@ def try_install_verifiers(verifiers: list[str]):
             print(f"Error installing {verifier}: {install_result.err()}")
 
 
-def try_uninstall_verifiers(verifiers: list[str]):
-    """_summary_."""
+def try_uninstall_verifiers(verifiers: Iterable[str]):
+    """Tries to uninstall the specified verifiers.
+
+    Will print the result of each attempt to stdout.
+
+    Args:
+        verifiers: Names of the verifiers to uninstall.
+    """
     for verifier in verifiers:
         print(f"\nUninstalling {verifier}...")
 
@@ -107,3 +123,35 @@ def try_uninstall_verifiers(verifiers: list[str]):
             print(f"Succesfully uninstalled {verifier}")
         elif isinstance(uninstall_result, Err):
             print(f"Error uninstalling {verifier}: {uninstall_result.err()}")
+
+
+def check_commit_hashes():
+    """Check if all commit hashes are up to date."""
+    all_up_to_date = True
+
+    for file in VERIFIER_DIR.iterdir():
+        if not file.is_dir():
+            continue
+
+        repo_info = repo_infos[file.name]
+        cmd = f"git rev-parse {repo_info.branch}"
+
+        with cwd(file / "tool"):
+            commit_hash = subprocess.run(
+                shlex.split(cmd), capture_output=True
+            ).stdout.decode()
+
+            # Currently have short hashes in install files
+            # Switching to long ones might be good
+            commit_hash = commit_hash[:7]
+
+            if commit_hash != repo_info.commit_hash:
+                all_up_to_date = False
+                print(
+                    f"Verifier {file.name} has commit_hash {commit_hash}, "
+                    f"but commit hash in installation file "
+                    f"is {repo_info.commit_hash}"
+                )
+
+    if all_up_to_date:
+        print("Everything up to date.")

autoverify/cli/install/installers/__init__.py

@@ -1,18 +1,36 @@
 from pathlib import Path
 from typing import Callable
 
+from autoverify.cli.util.git import GitRepoInfo
+
+from .abcrown.install import AbCrownRepoInfo
 from .abcrown.install import install as install_abcrown
-from .dummy.install import install as install_dummy_verifier
+from .mnbab.install import MnBabRepoInfo
 from .mnbab.install import install as install_mnbab
+from .nnenum.install import NnenumRepoInfo
 from .nnenum.install import install as install_nnenum
+from .ovalbab.install import OvalBabRepoInfo
 from .ovalbab.install import install as install_ovalbab
+from .verinet.install import VerinetRepoInfo
+from .verinet.install import install as install_verinet
 
 installers: dict[str, Callable[[Path], None]] = {
-    "DummyVerifier": install_dummy_verifier,
     "nnenum": install_nnenum,
     "abcrown": install_abcrown,
     "mnbab": install_mnbab,
     "ovalbab": install_ovalbab,
+    "verinet": install_verinet,
+}
+
+repo_infos: dict[str, GitRepoInfo] = {
+    "nnenum": NnenumRepoInfo,
+    "abcrown": AbCrownRepoInfo,
+    "mnbab": MnBabRepoInfo,
+    "ovalbab": OvalBabRepoInfo,
+    "verinet": VerinetRepoInfo,
 }
 
-__all__ = ["installers"]
+__all__ = [
+    "installers",
+    "repo_infos",
+]

autoverify/cli/install/installers/abcrown/install.py

@@ -6,14 +6,18 @@
 from autoverify.util.env import copy_env_file_to
 
 AbCrownRepoInfo = GitRepoInfo(
-    main_branch="main",
+    branch="main",
     commit_hash="7b3d507",
     clone_url="https://github.com/Verified-Intelligence/alpha-beta-CROWN",
 )
 
 
 def install(install_dir: Path):
-    """_summary_."""
+    """Installs abcrown.
+
+    Args:
+        install_dir: Path where ab-crown is installed.
+    """
     clone_checkout_verifier(AbCrownRepoInfo, install_dir)
     copy_env_file_to(Path(__file__), install_dir)
     create_env_from_file(install_dir / "environment.yml")

autoverify/cli/install/installers/mnbab/install.py

@@ -1,5 +1,4 @@
 """mnbab installer."""
-import os
 import shlex
 import subprocess
 from pathlib import Path
@@ -14,14 +13,18 @@
 from autoverify.util.env import copy_env_file_to, cwd, environment
 
 MnBabRepoInfo = GitRepoInfo(
-    main_branch="public",
-    commit_hash="3b6fd05",
-    clone_url="https://github.com/mnmueller/mn_bab_vnn_2022.git",
+    branch="SABR_ready",
+    commit_hash="70751b8",
+    clone_url="https://github.com/eth-sri/mn-bab",
 )
 
 
 def install(install_dir: Path):
-    """_summary_."""
+    """Installs mnbab.
+
+    Args:
+        install_dir: Path where ab-crown is installed.
+    """
     clone_checkout_verifier(MnBabRepoInfo, install_dir, init_submodules=True)
     copy_env_file_to(Path(__file__), install_dir)
     create_env_from_file(install_dir / "environment.yml")
@@ -54,8 +57,4 @@ def install(install_dir: Path):
     with cwd(install_dir / "tool"), environment(
         MPFR_PREFIX=mpfr_path, CDD_PREFIX=cddlib_path
     ):
-        subprocess.run(
-            elina_cmd,
-            executable="/bin/bash",
-            shell=True,
-        )
+        subprocess.run(elina_cmd, shell=True)

autoverify/cli/install/installers/nnenum/install.py

@@ -6,14 +6,18 @@
 from autoverify.util.env import copy_env_file_to
 
 NnenumRepoInfo = GitRepoInfo(
-    main_branch="master",
-    commit_hash="cf7c0e7",
-    clone_url="https://github.com/stanleybak/nnenum.git",
+    branch="vnncomp2022",
+    commit_hash="c68562d",
+    clone_url="https://github.com/kw-corne/nnenum",
 )
 
 
 def install(install_dir: Path):
-    """_summary_."""
+    """Installs nnenum.
+
+    Args:
+        install_dir: Path where ab-crown is installed.
+    """
     clone_checkout_verifier(NnenumRepoInfo, install_dir)
     copy_env_file_to(Path(__file__), install_dir)
     create_env_from_file(install_dir / "environment.yml")

autoverify/cli/install/installers/ovalbab/install.py

@@ -12,14 +12,18 @@
 from autoverify.util.env import copy_env_file_to
 
 OvalBabRepoInfo = GitRepoInfo(
-    main_branch="main",
+    branch="main",
     commit_hash="5de3113",
     clone_url="https://github.com/oval-group/oval-bab",
 )
 
 
 def install(install_dir: Path):
-    """_summary_."""
+    """Installs nnenum.
+
+    Args:
+        install_dir: Path where ab-crown is installed.
+    """
     clone_checkout_verifier(OvalBabRepoInfo, install_dir)
     copy_env_file_to(Path(__file__), install_dir)
     create_env_from_file(install_dir / "environment.yml")