# 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@c19371144df3bb44fab255c43d04cbc2ab54d1c4 # v2.9.1
      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.07.12.0b42f4c/verus-0.2026.07.12.0b42f4c-x86-linux.zip
        asset_sha256=f6f4f5d08e07d3e1ad721d775bda5ba96b9dd0c73b48fc17f2e071866fbd01c0
        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 --features verus