fix: added quantifiers to deterministic whitelist #830
Workflow file for this run
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 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: | |
| # check if prover needed | |
| needs: build-prover | |
| runs-on: macos-latest | |
| concurrency: | |
| group: internal-tests-${{ 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 | |
| - name: Run conditional merge insertion tests | |
| 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 |