Add isolated IRC11 toolchain CI

[hiroki-chen]

This is the first step toward incrementally integrating weak-memory support into vostd. The existing toolchain and verification CI remain unchanged, so the current OSTD/RCU verification path is not affected.

• Add an isolated GitHub Actions workflow for the IRC11 Verus toolchain.
• Pin the Verus base revision and apply the IRC11 and vstd compatibility patches.
• Build vstd with --vstd-weak-memory.
• Add a smoke test ensuring SC and IRC11 atomics can coexist.

[Marsman1996]

so the current OSTD/RCU verification path is not affected.

This solves my previous concern.

But I have another question: if the proof code is merged, can I still verify VOSTD with main branch Verus?

[hiroki-chen]

Not as-is. The weak-memory proofs directly depend on IRC11-specific vstd APIs, so main-branch Verus cannot resolve or type-check them. To preserve compatibility, we need to feature-gate the weak-memory proofs, keep the existing SC path as the default, and verify both configurations in separate CI jobs.

[Marsman1996]

To preserve compatibility, we need to feature-gate the weak-memory proofs

Then I guess this is a good start,
hope Verus could merge the IRC11 branch soon.

[Marsman1996]

And can the patches here be merged into the upstream Verus IRC11 branch?

[hiroki-chen]

And can the patches here be merged into the upstream Verus IRC11 branch?

The patches apply to the asterinas' fork of Verus; if needed we can use verus-lang/verus' IRC11 branch w/o these patches.

[Marsman1996]

And can the patches here be merged into the upstream Verus IRC11 branch?

The patches apply to the asterinas' fork of Verus; if needed we can use verus-lang/verus' IRC11 branch w/o these patches.

Are these patches general enough that we could eventually submit them as PRs to the upstream Verus repository, or are they specifically designed for Asterinas?

[hiroki-chen]

And can the patches here be merged into the upstream Verus IRC11 branch?

The patches apply to the asterinas' fork of Verus; if needed we can use verus-lang/verus' IRC11 branch w/o these patches.

Are these patches general enough that we could eventually submit them as PRs to the upstream Verus repository, or are they specifically designed for Asterinas?

These patches were cherry-picked from IRC11 to make Asterinas' fork of verus work so there is no need to submit individual PRs for Verus.

[Marsman1996]

And can the patches here be merged into the upstream Verus IRC11 branch?

The patches apply to the asterinas' fork of Verus; if needed we can use verus-lang/verus' IRC11 branch w/o these patches.

Are these patches general enough that we could eventually submit them as PRs to the upstream Verus repository, or are they specifically designed for Asterinas?

These patches were cherry-picked from IRC11 to make Asterinas' fork of verus work so there is no need to submit individual PRs for Verus.

Sorry for the mistake, I thought they are for the upstream Verus...

[Marsman1996]

After thinking about it, I think maintaining these patches in Asterinas' fork of Verus is reasonable. Since Verus's IRC11 branch is behind main, VOSTD already contains some code that can only be verified with the latest Verus version.

Revert the latest commit and this PR is good to me