Repository navigation
fix: preserve literal namespace components across evaluation paths #243
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
| # Copyright (c) Microsoft Corporation. All rights reserved. | |
| # | |
| name: verus | |
| on: | |
| push: | |
| branches: [ "main" ] | |
| pull_request: | |
| branches: [ "main" ] | |
| env: | |
| CARGO_TERM_COLOR: always | |
| # This workflow only checks out code, downloads pinned Verus and Z3 release | |
| # assets, and runs verification. It never writes to the repository, so | |
| # restrict the GITHUB_TOKEN to read-only access to repository contents. | |
| permissions: | |
| contents: read | |
| jobs: | |
| verify: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 | |
| - name: Setup Rust toolchain | |
| uses: ./.github/actions/toolchains/rust | |
| with: | |
| components: "" | |
| - name: Install z3 | |
| shell: bash | |
| run: | | |
| set -euxo pipefail | |
| z3_url=https://github.com/Z3Prover/z3/releases/download/z3-4.16.0/z3-4.16.0-x64-glibc-2.39.zip | |
| z3_sha256=7288c49a5bd6dbafd7b0b0d1f65956b91672da24b08f09242919af159be3418e | |
| curl -fsSL "$z3_url" -o z3.zip | |
| echo "${z3_sha256} z3.zip" | sha256sum --check --strict | |
| unzip -q z3.zip | |
| echo "$PWD/z3-4.16.0-x64-glibc-2.39/bin" >> "$GITHUB_PATH" | |
| - name: Cache cargo | |
| uses: Swatinem/rust-cache@6323deb102c322ba6fcbdcafc7e3dddab59af2b6 # v2.9.2 | |
| with: | |
| shared-key: ${{ runner.os }}-regorus-verus | |
| - name: Install Verus and run verification | |
| shell: bash | |
| run: | | |
| set -euxo pipefail | |
| asset_url=https://github.com/verus-lang/verus/releases/download/release%2F0.2026.09.06.8dea4a2/verus-0.2026.09.06.8dea4a2-x86-linux.zip | |
| asset_sha256=13d01e134c0620c3b29770874707d16c33b3d227c843a489c8ceb744d43c0a16 | |
| test -n "$asset_url" | |
| curl -fsSL "$asset_url" -o verus.zip | |
| # Verify the download integrity before trusting/executing its contents. | |
| echo "${asset_sha256} verus.zip" | sha256sum --check --strict | |
| unzip -q verus.zip -d verus-dist | |
| # Search under an absolute path so that `find` yields absolute paths; | |
| # this keeps the PATH entries below valid regardless of the working | |
| # directory. | |
| verus_bin="$(find "$PWD/verus-dist" -type f -name verus -perm -u+x | head -n1)" | |
| cargo_verus_bin="$(find "$PWD/verus-dist" -type f -name cargo-verus -perm -u+x | head -n1)" | |
| version_json="$(find "$PWD/verus-dist" -type f -name version.json | head -n1)" | |
| test -n "$verus_bin" | |
| test -n "$cargo_verus_bin" | |
| test -n "$version_json" | |
| # Verus is built against a specific Rust toolchain and refuses to run | |
| # against any other version. Read the required toolchain from the | |
| # release metadata so we track it automatically instead of hardcoding. | |
| required_toolchain="$( | |
| python3 - "$version_json" <<'PY' | |
| import json | |
| import sys | |
| with open(sys.argv[1], encoding="utf-8") as version_file: | |
| toolchain = json.load(version_file).get("verus", {}).get("toolchain", "") | |
| if not toolchain: | |
| raise SystemExit("missing verus.toolchain in version.json") | |
| # Some Verus release metadata includes rustup's | |
| # "(overridden by environment variable RUSTUP_TOOLCHAIN)" suffix. | |
| # rustup needs only the installable toolchain token. | |
| print(toolchain.split()[0]) | |
| PY | |
| )" | |
| test -n "$required_toolchain" | |
| echo "Verus requires Rust toolchain: $required_toolchain" | |
| # Install the exact toolchain Verus expects, including the extra | |
| # components (rustc-dev, llvm-tools) that Verus links against and that | |
| # are not part of the default rustup profile. | |
| rustup toolchain install "$required_toolchain" \ | |
| --profile minimal \ | |
| --component rustc-dev --component llvm-tools --component rustfmt | |
| # Force cargo/rustc to resolve to the Verus toolchain for the commands | |
| # below, overriding any repository/directory toolchain override. | |
| export RUSTUP_TOOLCHAIN="$required_toolchain" | |
| # Put cargo-verus on PATH for the commands below. | |
| export PATH="$(dirname "$cargo_verus_bin"):$(dirname "$verus_bin"):$PATH" | |
| cargo verus --help | |
| cargo fetch --locked | |
| cargo verus verify --locked |