regorus/.github/workflows/verus.yml at 06f7dc563d1f15323e08941ae32e5c15b05a174b · microsoft/regorus · 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
# 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 a pinned Verus release asset,
# 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: 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.08.23.fbbbbcf/verus-0.2026.08.23.fbbbbcf-x86-linux.zip
        asset_sha256=b65483714e6bf2ae72bfe7c7199e1c608495a941306b979260e9ed585d5899c9
        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="$(sed -n 's/.*"toolchain"[[:space:]]*:[[:space:]]*"\([^"]*\)".*/\1/p' "$version_json")"
        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