add intermediary halmos-builder image and dockerize more workflows (#308

)

Co-authored-by: Daejun Park <[email protected]>

.github/workflows/publish-halmos-builder-package.yml

@@ -0,0 +1,56 @@
+# based on https://docs.github.com/en/packages/managing-github-packages-using-github-actions-workflows/publishing-and-installing-a-package-with-github-actions#upgrading-a-workflow-that-accesses-a-registry-using-a-personal-access-token
+name: Push halmos-builder package
+
+on:
+  # only trigger manually, this is independent from halmos releases
+  workflow_dispatch:
+  push:
+    paths:
+      - packages/halmos-builder/**/*
+      - .github/workflows/publish-halmos-builder-package.yml
+
+env:
+  IMAGE_NAME: halmos-builder
+
+jobs:
+  # This pushes the image to GitHub Packages.
+  push:
+    runs-on: ubuntu-latest
+    permissions:
+      packages: write
+      contents: read
+
+    steps:
+      - name: Login to GitHub Container Registry
+        uses: docker/login-action@v3
+        with:
+          registry: ghcr.io
+          username: ${{ github.actor }}
+          password: ${{ secrets.GITHUB_TOKEN }}
+
+      - uses: actions/checkout@v4
+        with:
+          submodules: false
+
+      - name: Build image
+        run: docker build . --file packages/halmos-builder/Dockerfile --tag $IMAGE_NAME --label "runnumber=${GITHUB_RUN_ID}"
+
+      - name: Push image
+        run: |
+          IMAGE_ID=ghcr.io/${{ github.repository_owner }}/$IMAGE_NAME
+
+          # This changes all uppercase characters to lowercase.
+          IMAGE_ID=$(echo $IMAGE_ID | tr '[A-Z]' '[a-z]')
+
+          # This strips the git ref prefix from the version.
+          VERSION=$(echo "${{ github.ref }}" | sed -e 's,.*/\(.*\),\1,')
+
+          # This strips the "v" prefix from the tag name.
+          [[ "${{ github.ref }}" == "refs/tags/"* ]] && VERSION=$(echo $VERSION | sed -e 's/^v//')
+
+          # This uses the Docker `latest` tag convention.
+          [ "$VERSION" == "main" ] && VERSION=latest
+          echo IMAGE_ID=$IMAGE_ID
+          echo VERSION=$VERSION
+          docker tag $IMAGE_NAME $IMAGE_ID:$VERSION
+          docker push $IMAGE_ID:$VERSION

.github/workflows/publish-halmos-package.yml

@@ -0,0 +1,63 @@
+# based on https://docs.github.com/en/packages/managing-github-packages-using-github-actions-workflows/publishing-and-installing-a-package-with-github-actions#upgrading-a-workflow-that-accesses-a-registry-using-a-personal-access-token
+name: Push halmos package
+
+on:
+  workflow_dispatch:
+  push:
+    paths:
+      - packages/halmos/**/*
+      - .github/workflows/publish-halmos-package.yml
+    tags:
+      # push when we release a new tagged version
+      - 'v*'
+
+
+env:
+  IMAGE_NAME: halmos
+
+jobs:
+  # This pushes the image to GitHub Packages.
+  push:
+    runs-on: ubuntu-latest
+    permissions:
+      packages: write
+      contents: read
+
+    steps:
+      - name: Login to GitHub Container Registry
+        uses: docker/login-action@v3
+        with:
+          registry: ghcr.io
+          username: ${{ github.actor }}
+          password: ${{ secrets.GITHUB_TOKEN }}
+
+      - uses: actions/checkout@v4
+        with:
+          # we may need tests/lib for the workflows using this image
+          submodules: recursive
+
+      - name: Build image
+        run: docker build . --file packages/halmos/Dockerfile --tag $IMAGE_NAME --label "runnumber=${GITHUB_RUN_ID}"
+
+      - name: Print halmos version
+        run: docker run $IMAGE_NAME --version
+
+      - name: Push image
+        run: |
+          IMAGE_ID=ghcr.io/${{ github.repository_owner }}/$IMAGE_NAME
+
+          # This changes all uppercase characters to lowercase.
+          IMAGE_ID=$(echo $IMAGE_ID | tr '[A-Z]' '[a-z]')
+
+          # This strips the git ref prefix from the version.
+          VERSION=$(echo "${{ github.ref }}" | sed -e 's,.*/\(.*\),\1,')
+
+          # This strips the "v" prefix from the tag name.
+          [[ "${{ github.ref }}" == "refs/tags/"* ]] && VERSION=$(echo $VERSION | sed -e 's/^v//')
+
+          # This uses the Docker `latest` tag convention.
+          [ "$VERSION" == "main" ] && VERSION=latest
+          echo IMAGE_ID=$IMAGE_ID
+          echo VERSION=$VERSION
+          docker tag $IMAGE_NAME $IMAGE_ID:$VERSION
+          docker push $IMAGE_ID:$VERSION

.github/workflows/solvers-publish.yml → .github/workflows/publish-solvers-package.yml

@@ -4,7 +4,10 @@ name: Push solvers package
 on:
   # only trigger manually, this is independent from halmos releases
   workflow_dispatch:
-
+  push:
+    paths:
+      - packages/solvers/**/*
+      - .github/workflows/publish-solvers-package.yml
 env:
   IMAGE_NAME: solvers
 
@@ -17,18 +20,20 @@ jobs:
       contents: read
 
     steps:
-      - uses: actions/checkout@v4
-
-      - name: Build image
-        run: docker build . --file packages/solvers/Dockerfile --tag $IMAGE_NAME --label "runnumber=${GITHUB_RUN_ID}"
-
       - name: Login to GitHub Container Registry
         uses: docker/login-action@v3
         with:
           registry: ghcr.io
           username: ${{ github.actor }}
           password: ${{ secrets.GITHUB_TOKEN }}
 
+      - uses: actions/checkout@v4
+        with:
+          submodules: false
+
+      - name: Build image
+        run: docker build . --file packages/solvers/Dockerfile --tag $IMAGE_NAME --label "runnumber=${GITHUB_RUN_ID}"
+
       - name: Push image
         run: |
           IMAGE_ID=ghcr.io/${{ github.repository_owner }}/$IMAGE_NAME

.github/workflows/test-external.yml

@@ -2,7 +2,9 @@ name: Test external projects
 
 on:
   push:
-    branches: [main]
+    branches: [main, chore-workflows]
+    paths:
+      - .github/workflows/test-external.yml
   workflow_dispatch:
     inputs:
       halmos-options:
@@ -22,43 +24,59 @@ jobs:
         project:
           - repo: "morpho-org/morpho-data-structures"
             dir: "morpho-data-structures"
-            cmd: "halmos --function testProve --loop 4 --symbolic-storage"
+            cmd: "--function testProve --loop 4 --symbolic-storage"
             branch: ""
             profile: ""
           - repo: "a16z/cicada"
             dir: "cicada"
-            cmd: "halmos --contract LibUint1024Test --function testProve --loop 256"
+            cmd: "--contract LibUint1024Test --function testProve --loop 256 --solver-command yices-smt2"
             branch: ""
             profile: ""
           - repo: "a16z/cicada"
             dir: "cicada"
-            cmd: "halmos --contract LibPrimeTest --function testProve --loop 256"
+            cmd: "--contract LibPrimeTest --function testProve --loop 256 --solver-command bitwuzla"
             branch: ""
             profile: ""
           - repo: "farcasterxyz/contracts"
             dir: "farcaster-contracts"
-            cmd: "halmos"
+            cmd: "--solver-command yices-smt2"
             branch: ""
             profile: ""
           - repo: "zobront/halmos-solady"
             dir: "halmos-solady"
-            cmd: "halmos --function testCheck"
+            cmd: "--function testCheck --solver-command yices-smt2"
             branch: ""
             profile: ""
           - repo: "pcaversaccio/snekmate"
             dir: "snekmate"
-            cmd: "halmos --config test/halmos.toml"
+            cmd: "--config test/halmos.toml --solver-command yices-smt2"
             branch: ""
             profile: "halmos"
 
     steps:
-      - name: Checkout
+      # TODO: remove this step once halmos-builder package is public
+      - name: Login to GitHub Container Registry
+        uses: docker/login-action@v3
+        with:
+          registry: ghcr.io
+          username: ${{ github.actor }}
+          password: ${{ secrets.GITHUB_TOKEN }}
+
+      - name: Checkout halmos
         uses: actions/checkout@v4
         with:
-          path: halmos
           # we won't be needing tests/lib for this workflow
           submodules: false
 
+      - name: Build image
+        run: docker build -t halmos-image . --file packages/halmos/Dockerfile
+
+      - name: Install Vyper
+        if: ${{ matrix.project.dir == 'snekmate' }}
+        run: |
+          docker run --name halmos-vyper --entrypoint uv halmos-image pip install vyper
+          docker commit --change 'ENTRYPOINT ["halmos"]' halmos-vyper halmos-image
+
       - name: Checkout external repo
         uses: actions/checkout@v4
         with:
@@ -67,35 +85,11 @@ jobs:
           ref: ${{ matrix.project.branch }}
           submodules: recursive
 
-      - name: Install Foundry
-        uses: foundry-rs/foundry-toolchain@v1
-
-      - name: Set up Python
-        uses: actions/setup-python@v5
-        with:
-          python-version: "3.12"
-
-      - name: Install dependencies
-        run: python -m pip install --upgrade pip
-
-      - name: Install Halmos
-        run: python -m pip install -e ./halmos
-
-      - name: Install Vyper
-        if: ${{ matrix.project.dir == 'snekmate' }}
-        run: python -m pip install vyper
-
-      - name: Install Yices 2 SMT solver
-        run: |
-          wget https://github.com/SRI-CSL/yices2/releases/download/Yices-2.6.4/yices-2.6.4-x86_64-pc-linux-gnu.tar.gz
-          tar -xzvf yices-2.6.4-x86_64-pc-linux-gnu.tar.gz
-          sudo mv yices-2.6.4/bin/* /usr/local/bin/
-          sudo mv yices-2.6.4/lib/* /usr/local/lib/
-          sudo mv yices-2.6.4/include/* /usr/local/include/
-          rm -rf yices-2.6.4
+      - name: Print halmos version
+        run: docker run halmos-image --version
 
       - name: Test external repo
-        run: ${{ matrix.project.cmd }} --statistics --solver-timeout-assertion 0 --solver-threads 4 --solver-command yices-smt2 ${{ matrix.cache-solver }} ${{ inputs.halmos-options }}
+        run: docker run -v .:/workspace halmos-image ${{ matrix.project.cmd }} --statistics --solver-timeout-assertion 0 --solver-threads 4 ${{ matrix.cache-solver }} ${{ inputs.halmos-options }}
         working-directory: ${{ matrix.project.dir }}
         env:
           FOUNDRY_PROFILE: ${{ matrix.project.profile }}

.github/workflows/test-ffi.yml

@@ -2,13 +2,16 @@ name: Test FFI
 
 on:
   push:
-    branches: [main]
+    branches: [main, chore-workflows]
+    paths:
+      - .github/workflows/test-ffi.yml
   pull_request:
     branches: [main]
+  workflow_dispatch:
 
 jobs:
   test:
-    runs-on: macos-latest
+    runs-on: ubuntu-latest
 
     strategy:
       fail-fast: false
@@ -17,25 +20,24 @@ jobs:
         - testname: "tests/ffi"
 
     steps:
-      - uses: actions/checkout@v4
+      # TODO: remove this step once halmos-builder package is public
+      - name: Login to GitHub Container Registry
+        uses: docker/login-action@v3
         with:
-          submodules: recursive
+          registry: ghcr.io
+          username: ${{ github.actor }}
+          password: ${{ secrets.GITHUB_TOKEN }}
 
-      - name: Install Foundry
-        uses: foundry-rs/foundry-toolchain@v1
-
-      - name: Set up Python
-        uses: actions/setup-python@v5
+      - uses: actions/checkout@v4
         with:
-          python-version: "3.12"
+          submodules: recursive
 
-      - name: Install dependencies
+      - name: Build image
         run: |
-          python -m pip install --upgrade pip
-          python -m pip install pytest
+          docker build -t halmos-image . --file packages/halmos/Dockerfile
 
-      - name: Install Halmos
-        run: python -m pip install -e .
+      - name: Print halmos version
+        run: docker run halmos-image --version
 
       - name: Run pytest
-        run: pytest -v tests/test_halmos.py -k ${{ matrix.testname }} --halmos-options="--ffi -v -st --solver-timeout-assertion 0"
+        run: docker run -v .:/workspace --entrypoint pytest halmos-image -v tests/test_halmos.py -k ${{ matrix.testname }} --halmos-options="--ffi -v -st --solver-timeout-assertion 0"

.github/workflows/test-long.yml

@@ -2,7 +2,9 @@ name: Test long
 
 on:
   push:
-    branches: [main]
+    branches: [main, chore-workflows]
+    paths:
+      - .github/workflows/test-long.yml
   workflow_dispatch:
     inputs:
       halmos-options:
@@ -26,22 +28,26 @@ jobs:
           - "examples/tokens/ERC721"
 
     steps:
-      - name: Checkout repository
-        uses: actions/checkout@v4
-        with:
-          submodules: recursive
-
+      # TODO: remove this step once halmos-builder package is public
       - name: Login to GitHub Container Registry
         uses: docker/login-action@v3
         with:
           registry: ghcr.io
           username: ${{ github.actor }}
           password: ${{ secrets.GITHUB_TOKEN }}
 
+      - name: Checkout repository
+        uses: actions/checkout@v4
+        with:
+          submodules: recursive
+
       - name: Build image
         run: |
-          docker build -t halmos . --file packages/halmos/Dockerfile
+          docker build -t halmos-image . --file packages/halmos/Dockerfile
+
+      - name: Print halmos version
+        run: docker run halmos-image --version
 
-      - name: Run Pytest
+      - name: Run pytest
         run: |
-          docker run -v .:/workspace --entrypoint pytest halmos -x -v tests/test_halmos.py -k ${{ matrix.testname }} --halmos-options='-st --solver-timeout-assertion 0 --solver-threads 4 --solver-command yices-smt2 ${{ matrix.cache-solver }} ${{ inputs.halmos-options }}' -s --log-cli-level=
+          docker run -v .:/workspace --entrypoint pytest halmos-image -x -v tests/test_halmos.py -k ${{ matrix.testname }} --halmos-options='-st --solver-timeout-assertion 0 --solver-threads 4 --solver-command yices-smt2 ${{ matrix.cache-solver }} ${{ inputs.halmos-options }}' -s --log-cli-level=