halmos/.github/workflows/test-external.yml at 079bb4241d1b460baf986257d56ea86977d73451 · a16z/halmos · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
name: Test external projects

on:
  push:
    branches: [main, chore-workflows]
  workflow_dispatch:
    inputs:
      halmos-options:
        description: "additional halmos options"
        required: false
        type: string
        default: ""

jobs:
  test:
    runs-on: ubuntu-latest

    strategy:
      fail-fast: false
      matrix:
        cache-solver: ["", "--cache-solver"]
        project:
          - repo: "morpho-org/morpho-data-structures"
            dir: "morpho-data-structures"
            cmd: "--function testProve --loop 4 --solver-threads 3 --disable-gc"
            branch: ""
            profile: ""
          - repo: "morpho-org/morpho-blue"
            dir: "morpho-blue"
            cmd: "--solver-threads 3"
            branch: ""
            profile: "test"
          - repo: "a16z/cicada"
            dir: "cicada"
            cmd: "--contract LibUint1024Test --function testProve --loop 256 --solver-threads 3"
            branch: ""
            profile: ""
          - repo: "a16z/cicada"
            dir: "cicada"
            cmd: "--contract LibPrimeTest --function testProve --loop 256 --solver-threads 3"
            branch: ""
            profile: ""
          - repo: "farcasterxyz/contracts"
            dir: "farcaster-contracts"
            cmd: "--solver-threads 3"
            branch: ""
            profile: ""
          - repo: "zobront/halmos-solady"
            dir: "halmos-solady"
            cmd: "--function testCheck --solver bitwuzla --solver-threads 3"
            branch: ""
            profile: ""
          - repo: "pcaversaccio/snekmate"
            dir: "snekmate"
            cmd: "--config test/halmos.toml --contract ERC20TestHalmos --solver-command 'jsi --model --sequence yices,bitwuzla-abstraction' --solver-threads 1"
            branch: ""
            profile: "halmos-venom"
          - repo: "pcaversaccio/snekmate"
            dir: "snekmate"
            cmd: "--config test/halmos.toml --contract ERC721TestHalmos --solver-command 'jsi --model --sequence yices,bitwuzla-abstraction' --solver-threads 1"
            branch: ""
            profile: "halmos-venom"
          - repo: "pcaversaccio/snekmate"
            dir: "snekmate"
            cmd: "--config test/halmos.toml --contract ERC1155TestHalmos --solver-command 'jsi --model --sequence yices,bitwuzla-abstraction' --solver-threads 1"
            branch: ""
            profile: "halmos-venom"
          - repo: "pcaversaccio/snekmate"
            dir: "snekmate"
            cmd: "--config test/halmos.toml --contract MathTestHalmos --solver-command 'jsi --model --sequence yices,bitwuzla-abstraction' --solver-threads 1"
            branch: ""
            profile: "halmos-venom"
          - repo: "daejunpark/sys-asm-halmos"
            dir: "sys-asm-halmos"
            cmd: "--solver-threads 3 --loop 2"
            branch: ""
            profile: ""

    steps:
      - name: Checkout halmos
        uses: actions/checkout@v4
        with:
          # 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: Run foundryup
        run: |
          # run foundryup in halmos-image, save the result as a new image
          docker run --name halmos-image-foundryup halmos-image foundryup

          # commit the result back to halmos-image
          docker commit halmos-image-foundryup halmos-image

      # for snekmate
      - name: Install Vyper
        if: ${{ matrix.project.dir == 'snekmate' }}
        run: |
          docker run --name halmos-image-vyper halmos-image uv pip install git+https://github.com/vyperlang/vyper@master
          docker commit halmos-image-vyper halmos-image

      # for sys-asm-halmos
      - name: Install Geas
        run: |
          docker run --name tmp-halmos-image halmos-image bash -c "\
            apt-get update && \
            apt-get install -y golang-go && \
            go version && \
            env 'GOBIN=/halmos/bin' go install github.com/fjl/geas/cmd/geas@latest && \
            geas -h"
          docker commit tmp-halmos-image halmos-image

      - name: Checkout external repo
        uses: actions/checkout@v4
        with:
          repository: ${{ matrix.project.repo }}
          path: ${{ matrix.project.dir }}
          ref: ${{ matrix.project.branch }}
          submodules: recursive

      - name: Print forge version
        run: docker run halmos-image forge --version

      - name: Print halmos version
        run: docker run halmos-image halmos --version

      - name: Test external repo
        run: docker run -e FOUNDRY_PROFILE -v .:/workspace halmos-image halmos ${{ matrix.project.cmd }} --statistics --solver-timeout-assertion 0 ${{ matrix.cache-solver }} ${{ inputs.halmos-options }}
        working-directory: ${{ matrix.project.dir }}
        env:
          FOUNDRY_PROFILE: ${{ matrix.project.profile }}