Lint a Verus project's version compatibility

verusversionlint.py

#!/usr/bin/env python3

"""Lint that rust-toolchain.toml and the vstd pin match the installed verus."""

import json
import shutil
import subprocess
import sys
import tomllib
from pathlib import Path


def rust_toolchain_channel() -> str:
    with Path("rust-toolchain.toml").open("rb") as f:
        data = tomllib.load(f)
    return data["toolchain"]["channel"]


def verus_toolchain() -> str:
    output = subprocess.check_output(
        ["verus", "--version", "--output-json"], text=True
    )
    data = json.loads(output)
    return data["verus"]["toolchain"]


def canonical_vstd_version() -> str:
    verus_bin = shutil.which("verus")
    vstd_cargo_toml_path = Path(verus_bin).parent / "vstd" / "Cargo.toml"
    with vstd_cargo_toml_path.open("rb") as f:
        data = tomllib.load(f)
    return data["package"]["version"]


def resolved_vstd_version() -> str | None:
    output = subprocess.check_output(
        ["cargo", "metadata", "--format-version", "1", "--locked"], text=True
    )
    metadata = json.loads(output)
    for package in metadata["packages"]:
        if package["name"] == "vstd":
            return package["version"]
    return None


def main() -> int:
    errors = []

    channel = rust_toolchain_channel()
    expected_toolchain = verus_toolchain()
    if not expected_toolchain.startswith(channel):
        errors.append(
            f"rust-toolchain.toml says {channel}, "
            f"verus expects {expected_toolchain}"
        )

    canonical = canonical_vstd_version()
    resolved = resolved_vstd_version()
    if resolved is not None and resolved != canonical:
        errors.append(
            f"Cargo.lock resolves vstd to {resolved}, "
            f"installed verus expects {canonical}"
        )

    for error in errors:
        print(f"error: {error}", file=sys.stderr)
    return 1 if errors else 0


if __name__ == "__main__":
    sys.exit(main())