From 141305dec1d742e8a07e79866d4f04737d2d439e Mon Sep 17 00:00:00 2001
From: Ralf Anton Beier <ralf_beier@me.com>
Date: Sat, 25 Apr 2026 22:29:41 +0200
Subject: [PATCH 1/2] fix(ci): Kani PR-smoke split, Mutation 4-shard, Verus log
 upload

Three CI fixes in one workflow PR:

- Kani: split into PR-only --only-codegen smoke (~5 min) and main-only
  full run. Resolves 45m15s timeout cancellations on PRs while keeping
  full verification nightly. The workflow comment at line 400 already
  named this as the planned approach.

- Mutation rivet-core: shard into 4 (rivet-core x {0,1,2,3}/4) so each
  arm fits in ~15-20 min instead of timing out at 55+ min on the
  3677-mutant corpus. rivet-cli stays single-arm.

- Verus: always-upload bazel test.log as `verus-test-log` artifact.
  Required for debugging spec failures from the GitHub UI; without it
  the test log is invisible and we have to guess at SMT errors.

Diagnosed by parallel research agents in REQ-004 follow-up sweep.

Trace: skip
---
 .github/workflows/ci.yml | 35 +++++++++++++++++++++++++++++------
 1 file changed, 29 insertions(+), 6 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 00b7be8..1521439 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -312,19 +312,24 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        crate: [rivet-core, rivet-cli]
+        include:
+          - { crate: rivet-cli,  shard: '0/1', shard_id: '0-of-1' }
+          - { crate: rivet-core, shard: '0/4', shard_id: '0-of-4' }
+          - { crate: rivet-core, shard: '1/4', shard_id: '1-of-4' }
+          - { crate: rivet-core, shard: '2/4', shard_id: '2-of-4' }
+          - { crate: rivet-core, shard: '3/4', shard_id: '3-of-4' }
     steps:
       - uses: actions/checkout@v6
       - uses: dtolnay/rust-toolchain@stable
       - uses: Swatinem/rust-cache@v2
         with:
-          key: mutants-${{ matrix.crate }}
+          key: mutants-${{ matrix.crate }}-${{ matrix.shard_id }}
       - name: Install cargo-mutants
         uses: taiki-e/install-action@v2
         with:
           tool: cargo-mutants
       - name: Run cargo-mutants
-        run: cargo mutants -p ${{ matrix.crate }} --timeout 90 --jobs 4 --output mutants-out -- --lib || true
+        run: cargo mutants -p ${{ matrix.crate }} --shard ${{ matrix.shard }} --timeout 90 --jobs 4 --output mutants-out -- --lib || true
       - name: Check surviving mutants
         run: |
           MISSED=0
@@ -341,7 +346,7 @@ jobs:
         if: always()
         uses: actions/upload-artifact@v4
         with:
-          name: mutants-report-${{ matrix.crate }}
+          name: mutants-report-${{ matrix.crate }}-${{ matrix.shard_id }}
           path: mutants-out/
 
   # ── Fuzz testing (main only — too slow for PRs) ───────────────────
@@ -409,8 +414,17 @@ jobs:
     timeout-minutes: 45
     steps:
       - uses: actions/checkout@v6
-      - uses: model-checking/kani-github-action@v1
-      - run: cargo kani -p rivet-core
+      # PR runs: smoke-test only (--only-codegen, ~5 min). Full Kani
+      # runs on push to main (still 45 min budget). The 27-harness
+      # full suite was overrunning the 45 min budget mid-unwind.
+      - if: github.event_name == 'pull_request'
+        uses: model-checking/kani-github-action@v1
+        with:
+          args: '-p rivet-core --only-codegen'
+      - if: github.event_name == 'push' && github.ref == 'refs/heads/main'
+        uses: model-checking/kani-github-action@v1
+      - if: github.event_name == 'push' && github.ref == 'refs/heads/main'
+        run: cargo kani -p rivet-core
 
   # ── Verus SMT verification ──────────────────────────────────────────
   # Toolchain + workspace are now correct (rules_verus@fc7b636 past the
@@ -445,6 +459,15 @@ jobs:
           nix_path: nixpkgs=channel:nixos-unstable
       - name: Verify Verus specs
         run: bazel test //verus:rivet_specs_verify
+      - name: Upload Verus test log
+        if: always()
+        uses: actions/upload-artifact@v4
+        with:
+          name: verus-test-log
+          path: |
+            bazel-out/*/testlogs/verus/rivet_specs_verify/test.log
+            bazel-testlogs/verus/rivet_specs_verify/test.log
+          if-no-files-found: warn
 
   # ── Rocq metamodel proofs ─────────────────────────────────────────
   # Not yet a hard gate: the proofs were written against an older Rocq and

From 5367d1e290b4229905f670035daf4710ead1ba9c Mon Sep 17 00:00:00 2001
From: Ralf Anton Beier <ralf_beier@me.com>
Date: Sat, 25 Apr 2026 22:31:57 +0200
Subject: [PATCH 2/2] style(ci): drop double space in mutants matrix to satisfy
 yamllint

The vertical-aligned `rivet-cli,  shard:` tripped yamllint's
`commas: too many spaces after comma` rule on line 316. Use a
single space; we lose the column alignment but unblock the gate.

Trace: skip
---
 .github/workflows/ci.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 1521439..856df79 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -313,7 +313,7 @@ jobs:
       fail-fast: false
       matrix:
         include:
-          - { crate: rivet-cli,  shard: '0/1', shard_id: '0-of-1' }
+          - { crate: rivet-cli, shard: '0/1', shard_id: '0-of-1' }
           - { crate: rivet-core, shard: '0/4', shard_id: '0-of-4' }
           - { crate: rivet-core, shard: '1/4', shard_id: '1-of-4' }
           - { crate: rivet-core, shard: '2/4', shard_id: '2-of-4' }