formalization(tc): verify WHNF, inference, DefEq, and the recursive method knot

.github/workflows/ci.yml

@@ -8,16 +8,45 @@ on:
 
 permissions:
   contents: read
-  # The zkVM gates' `gh cache list` check (for lean-test's nataddcomm.ixe cache)
-  # needs the Actions read scope. (actions/cache/restore uses the runner's own
-  # cache token, not this.)
-  actions: read
 
 concurrency:
   group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }}
   cancel-in-progress: true
 
 jobs:
+  # Produce the small real-program fixture consumed by both zkVM execution
+  # gates independently of the full Lean test job. A workflow artifact is the
+  # right synchronization primitive here: the file is unique to this run and
+  # must be available before either consumer starts.
+  zkvm-fixture:
+    name: zkVM execution fixture
+    runs-on: warp-ubuntu-latest-x64-16x
+    steps:
+      - uses: actions/checkout@v7
+      - uses: actions-rust-lang/setup-rust-toolchain@v1
+      # Build only the compiler executable and its dependencies. In particular,
+      # a failure in an unrelated Tests module must not prevent fixture
+      # publication. Disable the Lean cache because lean-test builds the same
+      # revision concurrently and the two jobs must not race to save one key.
+      - uses: leanprover/lean-action@v1
+        with:
+          auto-config: false
+          build: true
+          build-args: "ix --wfail -v"
+          use-github-cache: false
+      # `Nat.add_comm`'s transitive-dependency closure (~40 kB, ~40 constants)
+      # is a real theorem, not an empty environment. `--consts` keeps this much
+      # smaller than the complete Init+Std environment used by benchmarks.
+      - name: Compile nataddcomm.ixe
+        run: lake exe ix compile Ix.lean --consts Nat.add_comm --out nataddcomm.ixe
+      - name: Upload nataddcomm.ixe
+        uses: actions/upload-artifact@v4
+        with:
+          name: nataddcomm-ixe
+          path: nataddcomm.ixe
+          if-no-files-found: error
+          retention-days: 1
+
   lean-test:
     runs-on: warp-ubuntu-latest-x64-16x
     steps:
@@ -39,22 +68,6 @@ jobs:
         run: lake build IxTcVerify
       - name: Check codegen'd IxVM kernel is up to date
         run: lake exe ix codegen --check
-      # Compile the `.ixe` the zkVM execution gates run the guests over:
-      # `Nat.add_comm`'s transitive-dep closure (~40 kB, ~40 constants — a real
-      # theorem, not an empty env). Seeded from `Ix.lean` (already built above)
-      # via `--consts`, so it's the constant's closure, NOT the 184 MB full
-      # Init+Std env `bench-main`'s compile job produces. Root package has no
-      # Mathlib dep, so no cache fetch. Cached for the sp1-build / zisk-build
-      # jobs, which have no Lean toolchain to compile it.
-      - name: Compile nataddcomm.ixe for zkVM execution gates
-        run: lake exe ix compile Ix.lean --consts Nat.add_comm --out nataddcomm.ixe
-      # Keyed by commit sha so every run gets a fresh entry (the .ixe is not
-      # byte-reproducible).
-      - name: Cache nataddcomm.ixe for the zkVM execution gates
-        uses: actions/cache/save@v6
-        with:
-          path: nataddcomm.ixe
-          key: nataddcomm-ixe-${{ github.sha }}
       - name: Test Ix CLI
         run: lake test --wfail -- cli
       - name: Aiur tests
@@ -96,8 +109,8 @@ jobs:
   # failures by design (dropped rows, OOM sentinels), so they never turn red
   # on a breakage. These jobs are the red-X signal: each builds its host, then
   # runs the guest in the VM over `nataddcomm.ixe` (a ~40-constant closure the
-  # lean-test job compiles + caches). They run in parallel with lean-test, each
-  # waiting for that cache entry before its execute step. Both hosts exit
+  # dedicated zkvm-fixture job publishes). They run in parallel with lean-test
+  # and with each other after that narrow producer succeeds. Both hosts exit
   # non-zero when the kernel rejects a constant (sp1: EXIT_REJECTED; zisk:
   # `reject_failures`), so a guest that compiles but panics / faults / rejects
   # fails the job. SP1 execute is pure RISC-V emulation (no key). Zisk execute
@@ -111,6 +124,7 @@ jobs:
   # SP1's host crates need pkg-config + libssl-dev).
   sp1-build:
     name: SP1 host build
+    needs: zkvm-fixture
     runs-on: warp-ubuntu-latest-x64-16x
     steps:
       - uses: actions/checkout@v7
@@ -132,25 +146,11 @@ jobs:
           # sp1-build skips the guest compilation and the host cfg-gates its
           # ELF embed accordingly, so this lints host code only.
           cargo clippy --release --workspace --all-targets -- -D warnings
-      # Wait 5 minutes max for `lean-test` to upload `nataddcomm.ixe`
-      - name: Wait for the nataddcomm.ixe cache
-        env:
-          GH_TOKEN: ${{ github.token }}
-        run: |
-          key=nataddcomm-ixe-${{ github.sha }}
-          for i in $(seq 1 30); do
-            if gh cache list --key "$key" --json id | grep -q '"id"'; then
-              echo "$key is cached"; exit 0
-            fi
-            echo "waiting for $key cache ($i/30)…"; sleep 10
-          done
-          echo "::error::timed out waiting for $key cache (did lean-test fail before caching?)"
-          exit 1
-      - uses: actions/cache/restore@v6
+      - name: Download nataddcomm.ixe
+        uses: actions/download-artifact@v4
         with:
-          path: nataddcomm.ixe
-          key: nataddcomm-ixe-${{ github.sha }}
-          fail-on-cache-miss: true
+          name: nataddcomm-ixe
+          path: .
       # Run the guest ELF in SP1's RISC-V executor over the nataddcomm env —
       # pure emulation, no GPU or proving key. `--execute` exits 3
       # (EXIT_REJECTED) if the kernel rejects any constant and non-zero on any
@@ -163,6 +163,7 @@ jobs:
 
   zisk-build:
     name: Zisk host build
+    needs: zkvm-fixture
     runs-on: warp-ubuntu-latest-x64-16x
     steps:
       - uses: actions/checkout@v7
@@ -185,24 +186,11 @@ jobs:
           # --release shares the build's dep artifacts (including the guest
           # ELFs its build scripts already produced).
           cargo clippy --release --workspace --all-targets -- -D warnings
-      - name: Wait for the nataddcomm.ixe cache
-        env:
-          GH_TOKEN: ${{ github.token }}
-        run: |
-          key=nataddcomm-ixe-${{ github.sha }}
-          for i in $(seq 1 30); do
-            if gh cache list --key "$key" --json id | grep -q '"id"'; then
-              echo "$key is cached"; exit 0
-            fi
-            echo "waiting for $key cache ($i/30)…"; sleep 10
-          done
-          echo "::error::timed out waiting for $key cache (did lean-test fail before caching?)"
-          exit 1
-      - uses: actions/cache/restore@v6
+      - name: Download nataddcomm.ixe
+        uses: actions/download-artifact@v4
         with:
-          path: nataddcomm.ixe
-          key: nataddcomm-ixe-${{ github.sha }}
-          fail-on-cache-miss: true
+          name: nataddcomm-ixe
+          path: .
       # Run the guest ELF in the Zisk VM over the nataddcomm env. `zisk-host`
       # exits 3 (EXIT_REJECTED, via `reject_failures`) if the kernel rejects any
       # constant and non-zero on any VM fault — so the tool errors on failures,