sui-prover.yml

name: Sui-Prover Test Action

on: [pull_request]

jobs:
  build-prover:
    runs-on: macos-latest

    concurrency:
      group: build-prover-${{ github.head_ref || github.ref_name }}
      cancel-in-progress: true

    outputs:
      artifact-name: ${{ steps.set-artifact.outputs.name }}

    steps:
      - name: Checkout repository
        uses: actions/checkout@v4

      - uses: dtolnay/rust-toolchain@stable

      - uses: Swatinem/rust-cache@v2
        with:
          shared-key: "sui-prover"
          cache-on-failure: true

      - name: Install dependencies and build prover
        run: |
          INSTALL_DIR="$HOME/.local/temp/sui-prover"
          BIN_DIR="$HOME/.local/bin"

          mkdir -p "$INSTALL_DIR" "$BIN_DIR"

          brew install z3

          cargo install --locked --path ./crates/sui-prover --root "$INSTALL_DIR"

          git clone --branch master https://github.com/boogie-org/boogie.git boogie-src
          cd boogie-src
          dotnet build Source/Boogie.sln -c Release
          cp -r Source/BoogieDriver/bin/Release/net8.0/* "$INSTALL_DIR"
          ln -sf "$INSTALL_DIR/BoogieDriver" "$BIN_DIR/boogie"
          chmod +x "$BIN_DIR/boogie"
          cd ..
          rm -rf boogie-src

          cat <<EOF > "$BIN_DIR/sui-prover"
          #!/bin/bash
          export BOOGIE_EXE="$BIN_DIR/boogie"
          export Z3_EXE="$(brew --prefix z3)/bin/z3"
          exec "$INSTALL_DIR/bin/sui-prover" "\$@"
          EOF

          chmod +x "$BIN_DIR/sui-prover"

          echo "export PATH=$BIN_DIR:\$PATH" >> ~/.bashrc

      - name: Set artifact name
        id: set-artifact
        run: echo "name=sui-prover-${{ github.run_id }}" >> $GITHUB_OUTPUT

      - name: Prepare artifact bundle
        run: |
          mkdir -p ~/artifact-bundle/bin
          mkdir -p ~/artifact-bundle/z3
          mkdir -p ~/artifact-bundle/boogie

          # Copy sui-prover binary
          cp target/release/sui-prover ~/artifact-bundle/bin/

          # Copy boogie executable and all its dependencies
          cp -r $HOME/.local/temp/sui-prover/* ~/artifact-bundle/boogie/
          ln -s ~/artifact-bundle/boogie/BoogieDriver ~/artifact-bundle/bin/boogie

          # Copy Z3 (just the bin directory is needed)
          cp -r "$(brew --prefix z3)/bin" ~/artifact-bundle/z3/

      - name: Upload prover binary and dependencies
        uses: actions/upload-artifact@v4
        with:
          name: ${{ steps.set-artifact.outputs.name }}
          path: ~/artifact-bundle
          retention-days: 1
          if-no-files-found: error
          compression-level: 6

      - name: Verify installation
        run: |
          chmod +x ~/artifact-bundle/bin/sui-prover
          chmod +x ~/artifact-bundle/bin/boogie

          ~/artifact-bundle/bin/sui-prover --version
          ~/artifact-bundle/bin/boogie /version

  kit-specs:
    needs: build-prover
    runs-on: macos-latest

    concurrency:
      group: kit-specs-${{ github.head_ref || github.ref_name }}
      cancel-in-progress: true

    steps:
      - name: Download
        uses: actions/download-artifact@v4
        with:
          name: ${{ needs.build-prover.outputs.artifact-name }}
          path: ~/prover-bundle

      - name: Setup
        run: |
          mkdir -p ~/.local/bin
          
          mkdir -p "$HOME/.asymptotic" 
          echo "${{ secrets.CLOUD_EXEC_CONFIG }}" > "$HOME/.asymptotic/sui_prover.toml"

          cp ~/prover-bundle/bin/sui-prover ~/.local/bin/
          ln -s ~/prover-bundle/boogie/BoogieDriver ~/.local/bin/boogie

          chmod +x ~/.local/bin/boogie
          chmod +x ~/.local/bin/sui-prover
          chmod +x ~/prover-bundle/z3/bin/z3

          # Add to PATH
          echo "$HOME/.local/bin" >> $GITHUB_PATH
          echo "$HOME/prover-bundle/z3/bin" >> $GITHUB_PATH

          echo "BOOGIE_EXE=$HOME/.local/bin/boogie" >> $GITHUB_ENV
          echo "Z3_EXE=$HOME/prover-bundle/z3/bin/z3" >> $GITHUB_ENV

      - name: Run
        run: |
          git clone https://github.com/asymptotic-code/sui-kit.git sui-kit

          cd sui-kit/examples/amm
          sui-prover --ci --cloud

          cd ../showcase
          sui-prover --ci --cloud

          cd ../guide
          sui-prover --ci --cloud

  internal-tests-prover:
    # check if prover needed
    needs: build-prover
    runs-on: macos-latest

    concurrency:
      group: internal-tests-prover-${{ github.head_ref || github.ref_name }}
      cancel-in-progress: true

    steps:
      - name: Checkout repository
        uses: actions/checkout@v4

      - uses: dtolnay/rust-toolchain@stable

      - uses: Swatinem/rust-cache@v2
        with:
          shared-key: "sui-prover"
          save-if: false

      - name: Download
        uses: actions/download-artifact@v4
        with:
          name: ${{ needs.build-prover.outputs.artifact-name }}
          path: ~/prover-bundle

      - name: Setup
        run: |
          mkdir -p ~/.local/bin

          cp ~/prover-bundle/bin/sui-prover ~/.local/bin/
          ln -s ~/prover-bundle/boogie/BoogieDriver ~/.local/bin/boogie

          chmod +x ~/.local/bin/boogie
          chmod +x ~/.local/bin/sui-prover
          chmod +x ~/prover-bundle/z3/bin/z3

          echo "$HOME/.local/bin" >> $GITHUB_PATH
          echo "$HOME/prover-bundle/z3/bin" >> $GITHUB_PATH

          echo "BOOGIE_EXE=$HOME/.local/bin/boogie" >> $GITHUB_ENV
          echo "Z3_EXE=$HOME/prover-bundle/z3/bin/z3" >> $GITHUB_ENV

      - name: Run
        run: |
          cd ./crates/sui-prover
          cargo test

  internal-tests-stackless-bytecode:
    # check if prover needed
    needs: build-prover
    runs-on: macos-latest

    concurrency:
      group: internal-tests-stackless-bytecode-${{ github.head_ref || github.ref_name }}
      cancel-in-progress: true

    steps:
      - name: Checkout repository
        uses: actions/checkout@v4

      - uses: dtolnay/rust-toolchain@stable

      - uses: Swatinem/rust-cache@v2
        with:
          shared-key: "sui-prover"
          save-if: false

      - name: Run
        run: |
          cargo test -p move-stackless-bytecode --test testsuite -- 'test_runner::conditional_merge_insertion'
        env:
          STACKLESS_TEST_IGNORE_DEPS: 1

  integer-mate-specs:
    needs: build-prover
    runs-on: macos-latest

    concurrency:
      group: integer-mate-specs-${{ github.head_ref || github.ref_name }}
      cancel-in-progress: true

    steps:
      - name: Download
        uses: actions/download-artifact@v4
        with:
          name: ${{ needs.build-prover.outputs.artifact-name }}
          path: ~/prover-bundle

      - name: Setup
        run: |
          mkdir -p ~/.local/bin

          mkdir -p "$HOME/.asymptotic" 
          echo "${{ secrets.CLOUD_EXEC_CONFIG }}" > "$HOME/.asymptotic/sui_prover.toml"

          cp ~/prover-bundle/bin/sui-prover ~/.local/bin/
          ln -s ~/prover-bundle/boogie/BoogieDriver ~/.local/bin/boogie

          chmod +x ~/.local/bin/boogie
          chmod +x ~/.local/bin/sui-prover
          chmod +x ~/prover-bundle/z3/bin/z3

          echo "$HOME/.local/bin" >> $GITHUB_PATH
          echo "$HOME/prover-bundle/z3/bin" >> $GITHUB_PATH

          echo "BOOGIE_EXE=$HOME/.local/bin/boogie" >> $GITHUB_ENV
          echo "Z3_EXE=$HOME/prover-bundle/z3/bin/z3" >> $GITHUB_ENV

      - name: Run
        run: |
          git clone https://github.com/asymptotic-code/integer-library int-lib

          cd int-lib/specs
          sui-prover --ci --cloud

          cd ../specs-bv
          sui-prover --no-bv-int-encoding --ci --cloud

  token-distribution-specs:
    needs: build-prover
    runs-on: macos-latest

    concurrency:
      group: token-distribution-specs-${{ github.head_ref || github.ref_name }}
      cancel-in-progress: true

    steps:
      - name: Download
        uses: actions/download-artifact@v4
        with:
          name: ${{ needs.build-prover.outputs.artifact-name }}
          path: ~/prover-bundle

      - name: Setup
        run: |
          mkdir -p ~/.local/bin

          mkdir -p "$HOME/.asymptotic" 
          echo "${{ secrets.CLOUD_EXEC_CONFIG }}" > "$HOME/.asymptotic/sui_prover.toml"

          cp ~/prover-bundle/bin/sui-prover ~/.local/bin/
          ln -s ~/prover-bundle/boogie/BoogieDriver ~/.local/bin/boogie

          chmod +x ~/.local/bin/boogie
          chmod +x ~/.local/bin/sui-prover
          chmod +x ~/prover-bundle/z3/bin/z3

          echo "$HOME/.local/bin" >> $GITHUB_PATH
          echo "$HOME/prover-bundle/z3/bin" >> $GITHUB_PATH

          echo "BOOGIE_EXE=$HOME/.local/bin/boogie" >> $GITHUB_ENV
          echo "Z3_EXE=$HOME/prover-bundle/z3/bin/z3" >> $GITHUB_ENV

      - name: Run
        run: |
          git clone --depth 1 -b fix/prover_specs https://github.com/asymptotic-code/sui-smart-contracts.git sui-smart-contracts
          cd sui-smart-contracts/token-distribution-specs 
          sui-prover --ci --cloud

  scallop-bpl-generation:
    needs: build-prover
    runs-on: macos-latest

    concurrency:
      group: scallop-bpl-generation-${{ github.head_ref || github.ref_name }}
      cancel-in-progress: true

    steps:
      - name: Download
        uses: actions/download-artifact@v4
        with:
          name: ${{ needs.build-prover.outputs.artifact-name }}
          path: ~/prover-bundle

      - name: Setup
        run: |
          mkdir -p ~/.local/bin

          cp ~/prover-bundle/bin/sui-prover ~/.local/bin/
          ln -s ~/prover-bundle/boogie/BoogieDriver ~/.local/bin/boogie

          chmod +x ~/.local/bin/boogie
          chmod +x ~/.local/bin/sui-prover
          chmod +x ~/prover-bundle/z3/bin/z3

          echo "$HOME/.local/bin" >> $GITHUB_PATH
          echo "$HOME/prover-bundle/z3/bin" >> $GITHUB_PATH

          echo "BOOGIE_EXE=$HOME/.local/bin/boogie" >> $GITHUB_ENV
          echo "Z3_EXE=$HOME/prover-bundle/z3/bin/z3" >> $GITHUB_ENV

      - name: Clone scallop repo
        uses: actions/checkout@v4
        with:
          repository: asymptotic-code/scallop-lending
          ref: specs
          token: ${{ secrets.PAT_TOKEN }}
          path: scallop

      - name: Run
        run: |
          cd scallop/contracts/specs
          sui-prover -g --ci

  cetus-bpl-generation:
    needs: build-prover
    runs-on: macos-latest

    concurrency:
      group: cetus-bpl-generation-${{ github.head_ref || github.ref_name }}
      cancel-in-progress: true

    steps:
      - name: Download
        uses: actions/download-artifact@v4
        with:
          name: ${{ needs.build-prover.outputs.artifact-name }}
          path: ~/prover-bundle

      - name: Setup
        run: |
          mkdir -p ~/.local/bin

          cp ~/prover-bundle/bin/sui-prover ~/.local/bin/
          ln -s ~/prover-bundle/boogie/BoogieDriver ~/.local/bin/boogie

          chmod +x ~/.local/bin/boogie
          chmod +x ~/.local/bin/sui-prover
          chmod +x ~/prover-bundle/z3/bin/z3

          echo "$HOME/.local/bin" >> $GITHUB_PATH
          echo "$HOME/prover-bundle/z3/bin" >> $GITHUB_PATH

          echo "BOOGIE_EXE=$HOME/.local/bin/boogie" >> $GITHUB_ENV
          echo "Z3_EXE=$HOME/prover-bundle/z3/bin/z3" >> $GITHUB_ENV

      - name: Clone cetus repo
        uses: actions/checkout@v4
        with:
          repository: asymptotic-code/cetus-clmm
          ref: clmm-specs
          token: ${{ secrets.PAT_TOKEN }}
          path: cetus    

      - name: Run
        run: |
          cd cetus/cetus_clmm_specs
          sui-prover -g --ci

  ika-bpl-generation:
    needs: build-prover
    runs-on: macos-latest

    concurrency:
      group: ika-bpl-generation-${{ github.head_ref || github.ref_name }}
      cancel-in-progress: true

    steps:
      - name: Download
        uses: actions/download-artifact@v4
        with:
          name: ${{ needs.build-prover.outputs.artifact-name }}
          path: ~/prover-bundle

      - name: Setup
        run: |
          mkdir -p ~/.local/bin

          cp ~/prover-bundle/bin/sui-prover ~/.local/bin/
          ln -s ~/prover-bundle/boogie/BoogieDriver ~/.local/bin/boogie

          chmod +x ~/.local/bin/boogie
          chmod +x ~/.local/bin/sui-prover
          chmod +x ~/prover-bundle/z3/bin/z3

          echo "$HOME/.local/bin" >> $GITHUB_PATH
          echo "$HOME/prover-bundle/z3/bin" >> $GITHUB_PATH

          echo "BOOGIE_EXE=$HOME/.local/bin/boogie" >> $GITHUB_ENV
          echo "Z3_EXE=$HOME/prover-bundle/z3/bin/z3" >> $GITHUB_ENV

      - name: Clone ika repo
        uses: actions/checkout@v4
        with:
          repository: asymptotic-code/ika-fv
          ref: specs
          token: ${{ secrets.PAT_TOKEN }}
          path: ika

      - name: Run
        run: |
          cd ika/contracts/specs
          sui-prover -g --ci