docs(rivet): wire scry cross-repo traceability — SCRY-001/REQ-011 + FEAT-023/REQ-012 #704
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: CI | |
| on: | |
| push: | |
| branches: [main] | |
| pull_request: | |
| branches: [main] | |
| env: | |
| CARGO_TERM_COLOR: always | |
| jobs: | |
| test: | |
| name: Test | |
| # NOTE: moved back to ubuntu-latest from [self-hosted, linux, x64, rust-cpu] | |
| # because z3-sys's C++ build was exhausting the smithy runners' temp disk | |
| # ("No space left on device" while compiling z3 AST sources). The Test job | |
| # builds the entire workspace including synth-verify (which depends on z3), | |
| # so the disk pressure is real. Once the smithy runners get a bigger /tmp | |
| # we can move this back. | |
| runs-on: ubuntu-latest | |
| env: | |
| RUSTFLAGS: -Dwarnings | |
| steps: | |
| - uses: actions/checkout@v6 | |
| - uses: dtolnay/rust-toolchain@stable | |
| - name: Cache Cargo dependencies | |
| uses: actions/cache@v5 | |
| with: | |
| path: | | |
| ~/.cargo/registry | |
| ~/.cargo/git | |
| target/ | |
| key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }} | |
| restore-keys: | | |
| ${{ runner.os }}-cargo- | |
| - name: Run tests | |
| run: cargo test --workspace | |
| clippy: | |
| name: Clippy | |
| # Same reasoning as Test — z3-sys build exhausts the smithy runner's /tmp. | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v6 | |
| - uses: dtolnay/rust-toolchain@stable | |
| with: | |
| components: clippy | |
| - name: Cache Cargo dependencies | |
| uses: actions/cache@v5 | |
| with: | |
| path: | | |
| ~/.cargo/registry | |
| ~/.cargo/git | |
| target/ | |
| key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }} | |
| restore-keys: | | |
| ${{ runner.os }}-cargo- | |
| - name: Run clippy | |
| run: cargo clippy --workspace --all-targets -- -D warnings | |
| fmt: | |
| name: Format | |
| runs-on: [self-hosted, linux, x64, light] | |
| steps: | |
| - uses: actions/checkout@v6 | |
| - uses: dtolnay/rust-toolchain@stable | |
| with: | |
| components: rustfmt | |
| - name: Cache Cargo dependencies | |
| uses: actions/cache@v5 | |
| with: | |
| path: | | |
| ~/.cargo/registry | |
| ~/.cargo/git | |
| target/ | |
| key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }} | |
| restore-keys: | | |
| ${{ runner.os }}-cargo- | |
| - name: Check formatting | |
| run: cargo fmt --all -- --check | |
| pin-sweep: | |
| name: Version Pin Sweep | |
| runs-on: [self-hosted, linux, x64, light] | |
| steps: | |
| - uses: actions/checkout@v6 | |
| # Issue #145: fail at PR time if [workspace.package].version drifts from | |
| # any intra-workspace path-dep `version =` pin or MODULE.bazel — the | |
| # v0.7.0-class desync that breaks release.yml + publish at tag-push time. | |
| - name: Check intra-workspace version pins | |
| run: python3 scripts/check_version_pins.py | |
| verify: | |
| name: Z3 Verification | |
| # Stays on ubuntu-latest: needs `sudo apt-get install -y libz3-dev` | |
| # (smithy runners have no sudo). Move once libz3-dev is added to | |
| # the smithy toolchains role. | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v6 | |
| - uses: dtolnay/rust-toolchain@stable | |
| - name: Cache Cargo dependencies | |
| uses: actions/cache@v5 | |
| with: | |
| path: | | |
| ~/.cargo/registry | |
| ~/.cargo/git | |
| target/ | |
| key: ${{ runner.os }}-cargo-${{ hashFiles('**/Cargo.lock') }} | |
| restore-keys: | | |
| ${{ runner.os }}-cargo- | |
| - name: Install Z3 | |
| run: sudo apt-get update && sudo apt-get install -y libz3-dev | |
| - name: Run verification tests | |
| run: cargo test -p synth-verify --features z3-solver,arm | |
| - name: Run comprehensive verification | |
| run: cargo test -p synth-verify --test comprehensive_verification --features z3-solver,arm | |
| coverage: | |
| name: Code Coverage | |
| needs: [test] | |
| runs-on: [self-hosted, linux, x64, rust-cpu] | |
| steps: | |
| - uses: actions/checkout@v6 | |
| - uses: dtolnay/rust-toolchain@nightly | |
| - name: Cache Cargo dependencies | |
| uses: actions/cache@v5 | |
| with: | |
| path: | | |
| ~/.cargo/registry | |
| ~/.cargo/git | |
| target/ | |
| key: ${{ runner.os }}-coverage-${{ hashFiles('**/Cargo.lock') }} | |
| restore-keys: | | |
| ${{ runner.os }}-coverage- | |
| - name: Install cargo-llvm-cov | |
| uses: taiki-e/install-action@v2 | |
| with: | |
| tool: cargo-llvm-cov | |
| - name: Generate coverage (LCOV) | |
| run: | | |
| cargo llvm-cov --workspace --lcov --output-path lcov.info \ | |
| --exclude synth-verify --exclude synth-qemu \ | |
| --exclude synth-backend-awsm --exclude synth-backend-wasker | |
| - name: Upload to Codecov | |
| uses: codecov/codecov-action@v7 | |
| with: | |
| files: lcov.info | |
| fail_ci_if_error: false | |
| env: | |
| CODECOV_TOKEN: ${{ secrets.CODECOV_TOKEN }} | |
| kani: | |
| name: Kani Verification | |
| # Stays on ubuntu-latest: Kani-CBMC bundle is not yet provisioned | |
| # in the smithy toolchains role (tracked in playbook out-of-scope | |
| # table). Move once smithy ships kani-verifier + CBMC. | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v6 | |
| - name: Install Kani | |
| run: cargo install --locked kani-verifier && cargo kani setup | |
| - name: Run Kani proofs | |
| run: cargo kani -p synth-backend --tests | |
| timeout-minutes: 30 | |
| rivet: | |
| name: Rivet Validation | |
| runs-on: [self-hosted, linux, x64, rust-cpu] | |
| steps: | |
| - uses: actions/checkout@v6 | |
| - uses: dtolnay/rust-toolchain@stable | |
| - name: Cache Cargo dependencies | |
| uses: actions/cache@v5 | |
| with: | |
| path: | | |
| ~/.cargo/registry | |
| ~/.cargo/git | |
| ~/.cargo/bin | |
| target/ | |
| key: ${{ runner.os }}-rivet-${{ hashFiles('**/Cargo.lock') }} | |
| restore-keys: | | |
| ${{ runner.os }}-rivet- | |
| - name: Install rivet | |
| run: cargo install --force --git https://github.com/pulseengine/rivet --branch main rivet-cli | |
| - name: Validate artifacts | |
| run: | | |
| sed -i '/^externals:/,$d' rivet.yaml | |
| # Allow cross-repo link errors (kiln/gale/sigil haven't set up rivet yet) | |
| # but fail on any non-cross-repo errors (schema, missing fields, broken local refs) | |
| rivet validate 2>&1 | tee /tmp/rivet-output.txt | |
| # Check if all errors are cross-repo links (contain ':' in target) | |
| if grep -q "^ ERROR:" /tmp/rivet-output.txt; then | |
| NON_XREF=$(grep "^ ERROR:" /tmp/rivet-output.txt | grep -v "targets '.*:.*' which does not exist" | grep -cv "missing '.*' link to" || true) | |
| if [ "$NON_XREF" -gt 0 ]; then | |
| echo "::error::Found $NON_XREF non-cross-repo validation errors" | |
| exit 1 | |
| fi | |
| echo "::warning::Cross-repo link errors present (expected — external projects need rivet init)" | |
| fi | |
| - name: Check coverage | |
| run: rivet coverage | |
| bazel: | |
| name: Bazel Build & Proofs | |
| # Stays on ubuntu-latest: needs Nix + Bazel + Rocq via Bazel | |
| # (none provisioned on smithy; tracked in playbook out-of-scope | |
| # table for both Bazel and Rocq). | |
| runs-on: ubuntu-latest | |
| timeout-minutes: 45 | |
| steps: | |
| - uses: actions/checkout@v6 | |
| - name: Install Nix | |
| uses: cachix/install-nix-action@v31 | |
| with: | |
| nix_path: nixpkgs=channel:nixos-unstable | |
| - name: Setup Bazel | |
| uses: bazel-contrib/setup-bazel@0.19.0 | |
| with: | |
| bazelisk-cache: true | |
| disk-cache: ${{ github.workflow }} | |
| repository-cache: true | |
| - name: Build Rust via Bazel | |
| run: bazel build //crates:synth | |
| - name: Verify Rocq proofs | |
| run: bazel test //coq:verify_proofs | |
| - name: Run Renode emulation tests | |
| run: bazel test //tests/renode/... --test_tag_filters=wast || [ $? -eq 4 ] | |
| timeout-minutes: 10 |