Verus toolchain at HEAD (8a2bbf6) has librustc_driver .so mismatch

[avrabe]

Problem

Bumping rules_verus from 6e03a1d to 8a2bbf6 (HEAD) in Gale's MODULE.bazel causes the Verus verifier to fail at runtime:

rust_verify: error while loading shared libraries: librustc_driver-90863c8161c83a53.so: cannot open shared object file: No such file or directory

The Verus toolchain bundled at 8a2bbf6 expects a Rust librustc_driver version that doesn't match what's installed on the CI runner (GitHub Actions ubuntu-22.04 with rustup stable).

Context

Gale tried to adopt the verus_strip + verus_strip_test rules added in the 8a2bbf6 range (PR #7). The strip rules themselves work, but the Verus verifier toolchain (verus_toolchains_x86_64_unknown_linux_gnu/rust_verify) shipped alongside them has the .so mismatch.

Reverted to 6e03a1d for now: pulseengine/gale@72eefdb

Expected

The rules_verus toolchain should either:

1. Bundle a compatible librustc_driver, or
2. Document which Rust toolchain version is required (e.g., rust-toolchain.toml), or
3. Dynamically link against the host's librustc_driver

Environment

• Runner: ubuntu-22.04 (GitHub Actions)
• Rust: stable (installed via rustup)
• Bazel: 7.x

[avrabe]

Still failing with c6fae27 — different error now:

error[E0463]: can't find crate for `core`

The sysroot path fix changed the .so lookup, but the derived sysroot doesn't contain the standard library (core). The CI installs dtolnay/rust-toolchain@stable — the Verus rust_verify binary needs a compatible sysroot with core/std from the matching nightly.

The old commit (6e03a1d) worked because it used the host Rust sysroot directly. The new sysroot derivation logic seems to resolve to a path that doesn't have the std crates.

[avrabe]

Fixed in #19 — sysroot path is now derived from dirname(rust_verify) at runtime, so it resolves correctly in both build actions (f.path) and test runfiles (f.short_path).

[avrabe]

Reopening — the path derivation fix in #19 was incorrect diagnosis. The actual issue is that rust_verify is built against a nightly Rust, but the sysroot download fetches stable 1.93.0 which doesn't have matching core/std.

[avrabe]

Diagnostic results from 2a6907b

The sysroot verification shows the wrong platform is being selected:

Verus SMT job (ubuntu-22.04):

Error in fail: Sysroot missing libcore for aarch64-apple-darwin. Contents:
rust_sysroot/lib/rustlib/etc/gdb_lookup.py
rust_sysroot/lib/rustlib/aarch64-apple-darwin/bin/wasm-component-ld
rust_sysroot/lib/rustlib/aarch64-apple-darwin/bin/rust-objcopy

Rocq job (ubuntu-22.04):

Error in fail: Sysroot missing libcore for x86_64-unknown-linux-gnu. Contents:
rust_sysroot/lib/rustlib/etc/gdb_lookup.py

Two problems:

1. Wrong target triple: The Verus SMT job resolves to aarch64-apple-darwin on a Linux x86_64 runner. The toolchain registration or exec platform detection is wrong.
2. Missing lib/ directory: Even when the correct triple is used (Rocq job shows x86_64-unknown-linux-gnu), the sysroot only contains etc/ and bin/ — the lib/ directory with libcore*.rlib is not in the runfiles tree.

This confirms Theory 1 (runfiles gap): the sysroot files exist in the external repo but aren't materialized in the test's runfiles. The glob() in the Bazel rule likely doesn't capture the lib/rustlib/*/lib/*.rlib files.

Full CI run: https://github.com/pulseengine/gale/actions/runs/24032496779