feat: add devnet 5 support

.github/workflows/ci.yml

@@ -98,21 +98,10 @@ jobs:
           path: leanSpec/packages/testing/src/consensus_testing/test_keys/prod_scheme
           key: prod-keys-${{ steps.prod-keys-url.outputs.hash }}
 
-      # Download + extract the keys ourselves rather than via
-      # `consensus_testing.keys --download`. The pinned leanSpec commit predates
-      # leanSpec PR #745, whose `download_keys` reads the still-open (unflushed)
-      # download tempfile, intermittently truncating the gzip tail and aborting
-      # with EOFError. curl+tar fully writes the archive before reading it.
-      # Remove once the pin moves past PR #745.
       - name: Download production keys
         if: steps.cache-fixtures.outputs.cache-hit != 'true' && steps.cache-prod-keys.outputs.cache-hit != 'true'
         working-directory: leanSpec
-        run: |
-          KEYS_URL=$(uv run python -c "from consensus_testing.keys import KEY_DOWNLOAD_URLS; print(KEY_DOWNLOAD_URLS['prod'])")
-          KEYS_DIR=packages/testing/src/consensus_testing/test_keys
-          mkdir -p "$KEYS_DIR"
-          curl -sSL "$KEYS_URL" -o /tmp/prod_scheme.tar.gz
-          tar -xzf /tmp/prod_scheme.tar.gz -C "$KEYS_DIR"
+        run: uv run python -m consensus_testing.keys --download --scheme prod
 
       # Save production keys even if a later step fails, so a re-run does
       # not have to re-download. See: https://github.com/actions/cache/tree/main/save#always-save-cache
@@ -128,15 +117,30 @@ jobs:
           path: leanSpec/packages/testing/src/consensus_testing/test_keys/prod_scheme
           key: ${{ steps.cache-prod-keys.outputs.cache-primary-key }}
 
+      # `-n 1` (not `-n auto`) runs a single leanVM prover at a time. The
+      # devnet5 prover peaks at ~12 GiB per proof (measured), so more workers
+      # blow past the 4-vCPU/16 GiB runner's RAM: `-n auto` (4 provers) hard
+      # OOM-killed the runner, `-n 2` thrashed and lost its heartbeat so GitHub
+      # cancelled the job. One prover peaks ~12.4 GiB with 0 swap and completes
+      # in ~2h36m. The Makefile keeps `-n auto` for local machines with more RAM.
       - name: Generate test fixtures
+        id: generate-fixtures
         if: steps.cache-fixtures.outputs.cache-hit != 'true'
         working-directory: leanSpec
-        run: uv run fill --fork=Lstar --scheme prod -o fixtures -n auto
-
-      # Save fixtures even if a later step fails, so a re-run does not
-      # have to regenerate them. See: https://github.com/actions/cache/tree/main/save#always-save-cache
+        run: uv run fill --fork Lstar -n 1 --scheme prod -o fixtures
+
+      # Save fixtures only when generation actually SUCCEEDED. A bare
+      # `always()` here previously saved the (empty) fixtures dir when
+      # generation was cancelled or OOM-killed mid-run, poisoning the cache:
+      # later runs hit the empty cache, skipped generation, and the Rust tests
+      # failed with no fixtures. Gating on the generate step's outcome keeps
+      # the "save even if the later Rust test step fails" intent without ever
+      # persisting a partial fixture set.
       - name: Save test fixtures cache
-        if: always() && steps.cache-fixtures.outputs.cache-hit != 'true'
+        if: >-
+          always()
+          && steps.cache-fixtures.outputs.cache-hit != 'true'
+          && steps.generate-fixtures.outcome == 'success'
         uses: actions/cache/save@v5
         with:
           path: leanSpec/fixtures