fix: Decouple arch-specific constants from PagingConstsTrait trait definitions, fix specifications, and prove axioms.
#1286
Workflow file for this run
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Format and Verify VOSTD (Main) | |
| on: | |
| push: | |
| branches: | |
| - main | |
| pull_request: | |
| branches: | |
| - main | |
| workflow_dispatch: | |
| inputs: | |
| branch: | |
| description: "Branch to run the workflow on" | |
| required: true | |
| default: "main" | |
| jobs: | |
| format-and-verify: | |
| runs-on: ubuntu-24.04 | |
| env: | |
| CARGO_TERM_COLOR: always | |
| steps: | |
| - name: Checkout repository | |
| uses: actions/checkout@v6 | |
| with: | |
| submodules: recursive | |
| - name: Install dependencies | |
| run: | | |
| sudo apt update -qq | |
| sudo apt install -y build-essential unzip pkg-config libssl-dev llvm | |
| - name: Get Rust toolchain version | |
| id: rust-toolchain | |
| run: | | |
| RUST_VERSION=$(grep 'channel' rust-toolchain.toml | sed -E 's/.*= *"(.*)"/\1/') | |
| if [ -z "$RUST_VERSION" ]; then | |
| echo "Failed to extract Rust version from rust-toolchain.toml" | |
| exit 1 | |
| fi | |
| echo "RUST_VERSION=$RUST_VERSION" >> "$GITHUB_ENV" | |
| echo "Rust version: $RUST_VERSION" | |
| - name: Cache Rust toolchain | |
| uses: actions/cache@v5 | |
| with: | |
| path: | | |
| ~/.rustup/toolchains | |
| ~/.rustup/update-hashes | |
| ~/.rustup/tmp | |
| key: ${{ runner.os }}-rust-toolchain-${{ env.RUST_VERSION }} | |
| - name: Cache Cargo dependencies | |
| uses: actions/cache@v5 | |
| with: | |
| path: | | |
| ~/.cargo/registry | |
| ~/.cargo/git | |
| key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }} | |
| restore-keys: | | |
| ${{ runner.os }}-cargo- | |
| - name: Get Verus commit | |
| id: verus | |
| run: | | |
| VERUS_COMMIT=$(git ls-remote https://github.com/asterinas/verus HEAD | cut -f1) | |
| echo "VERUS_COMMIT=$VERUS_COMMIT" >> "$GITHUB_ENV" | |
| echo "Using Verus commit: $VERUS_COMMIT" | |
| DV_COMMIT=$(git rev-parse HEAD:dv) | |
| echo "DV_COMMIT=$DV_COMMIT" >> "$GITHUB_ENV" | |
| echo "Using dv commit: $DV_COMMIT" | |
| - name: Cache dv build artifacts | |
| uses: actions/cache@v5 | |
| with: | |
| path: dv/target | |
| key: ${{ runner.os }}-dv-${{ env.DV_COMMIT }} | |
| - name: Cache Verus | |
| id: cache-verus | |
| uses: actions/cache@v5 | |
| with: | |
| path: tools/verus | |
| key: ${{ runner.os }}-verus-${{ env.VERUS_COMMIT }} | |
| - name: Cache verusfmt | |
| id: cache-verusfmt | |
| uses: actions/cache@v5 | |
| with: | |
| path: ~/.cargo/bin/verusfmt | |
| key: ${{ runner.os }}-verusfmt-${{ env.VERUS_COMMIT }} | |
| - name: Bootstrap Verus (if needed) | |
| run: | | |
| if [ "${{ steps.cache-verus.outputs.cache-hit }}" = "true" ]; then | |
| echo "Using cached Verus" | |
| else | |
| echo "Cache miss, bootstrapping Verus..." | |
| rm -rf tools/verus | |
| cargo dv bootstrap | |
| fi | |
| if ! command -v verusfmt >/dev/null 2>&1; then | |
| echo "verusfmt not found, installing via cargo dv bootstrap..." | |
| cargo dv bootstrap | |
| fi | |
| verusfmt --version | |
| - name: Run verification | |
| run: | | |
| set -o pipefail | |
| if ! make 2>&1; then | |
| echo "❌ Verification failed" | |
| echo "VERIFY_FAILED=1" >> "$GITHUB_ENV" | |
| exit 1 | |
| else | |
| echo "✅ Verification passed!" | |
| fi | |
| - name: Run format | |
| if: always() | |
| run: make fmt | |
| - name: Check for formatting changes | |
| if: always() | |
| run: | | |
| if [[ -n $(git status --porcelain) ]]; then | |
| echo "Code is not properly formatted. Run 'make fmt'." | |
| git diff | |
| echo "FMT_FAILED=1" >> "$GITHUB_ENV" | |
| exit 1 | |
| fi | |
| - name: Publish summary | |
| if: always() | |
| run: | | |
| { | |
| echo "# CI Summary" | |
| if [[ "${FMT_FAILED:-0}" == "1" ]]; then | |
| echo "- Formatting: ❌ failed" | |
| else | |
| echo "- Formatting: ✅ passed" | |
| fi | |
| if [[ "${VERIFY_FAILED:-0}" == "1" ]]; then | |
| echo "- Verification: ❌ failed" | |
| else | |
| echo "- Verification: ✅ passed" | |
| fi | |
| } >> "$GITHUB_STEP_SUMMARY" |