From 59cc9cc0740fbc5594b7bb5c30340d687eac796f Mon Sep 17 00:00:00 2001
From: Asher Yan <polarnova@outlook.com>
Date: Fri, 24 Jul 2026 01:25:05 -0400
Subject: [PATCH] Reuse verified Lean proofs across release platforms

---
 .github/scripts/prepare_release_builder.sh |  26 ++++++
 .github/workflows/release.yml              | 104 ++++++++++++++++-----
 2 files changed, 108 insertions(+), 22 deletions(-)
 create mode 100755 .github/scripts/prepare_release_builder.sh

diff --git a/.github/scripts/prepare_release_builder.sh b/.github/scripts/prepare_release_builder.sh
new file mode 100755
index 0000000..6fb9e7a
--- /dev/null
+++ b/.github/scripts/prepare_release_builder.sh
@@ -0,0 +1,26 @@
+#!/usr/bin/env bash
+
+set -euo pipefail
+
+if [[ $# -ne 1 ]]; then
+  echo "usage: $0 <consumer-directory>" >&2
+  exit 2
+fi
+
+root="$(cd "$(dirname "${BASH_SOURCE[0]}")/../.." && pwd -P)"
+consumer_dir="$1"
+
+mkdir -p "$consumer_dir"
+cp "$root/lean-toolchain" "$consumer_dir/lean-toolchain"
+{
+  echo 'name = "CryptBooleanReleaseBuilder"'
+  echo 'version = "0.0.0"'
+  echo
+  echo '[[require]]'
+  echo 'name = "CryptBooleanFunction"'
+  printf 'path = "%s"\n' "$root"
+} > "$consumer_dir/lakefile.toml"
+
+lake -d="$consumer_dir" update
+lake -d="$consumer_dir" exe cache get
+"$root/.github/scripts/require_latest_fabl_release.sh" "$consumer_dir"
diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
index 7e13037..78886e8 100644
--- a/.github/workflows/release.yml
+++ b/.github/workflows/release.yml
@@ -48,16 +48,10 @@ jobs:
           git rev-parse --verify "refs/tags/$REQUESTED_TAG"
           echo "tag=$REQUESTED_TAG" >> "$GITHUB_OUTPUT"
 
-  build:
+  prove:
     needs: prepare
     if: github.event_name == 'push' || inputs.verify_only != true
-    strategy:
-      fail-fast: false
-      matrix:
-        runner:
-          - ubuntu-latest
-          - macos-15
-    runs-on: ${{ matrix.runner }}
+    runs-on: ubuntu-latest
     timeout-minutes: 120
 
     steps:
@@ -88,19 +82,7 @@ jobs:
         run: |
           set -euo pipefail
           consumer_dir="$RUNNER_TEMP/cryptboolean-release-builder"
-          mkdir -p "$consumer_dir"
-          cp lean-toolchain "$consumer_dir/lean-toolchain"
-          {
-            echo 'name = "CryptBooleanReleaseBuilder"'
-            echo 'version = "0.0.0"'
-            echo
-            echo '[[require]]'
-            echo 'name = "CryptBooleanFunction"'
-            printf 'path = "%s"\n' "$GITHUB_WORKSPACE"
-          } > "$consumer_dir/lakefile.toml"
-          lake -d="$consumer_dir" update
-          lake -d="$consumer_dir" exe cache get
-          ./.github/scripts/require_latest_fabl_release.sh "$consumer_dir"
+          ./.github/scripts/prepare_release_builder.sh "$consumer_dir"
           lake --wfail --no-cache -d="$consumer_dir" build CryptBoolean
 
       - name: Audit release proofs
@@ -116,6 +98,84 @@ jobs:
           path: .lake/build
           key: ${{ steps.cryptboolean-cache.outputs.cache-primary-key }}
 
+      - name: Pack portable proof archive
+        run: |
+          set -euo pipefail
+          lake pack
+          shopt -s nullglob
+          archives=(.lake/CryptBoolean-*.tar.gz)
+          test "${#archives[@]}" -eq 1
+          if tar -tzf "${archives[0]}" |
+              grep -E '\.(o|a|dylib|dll|so(\.[0-9]+)*)$'; then
+            echo "::error::CryptBoolean proof archive contains native artifacts"
+            exit 1
+          fi
+          mkdir -p proof-dist
+          cp "${archives[0]}" proof-dist/
+
+      - name: Preserve the verified proof archive
+        uses: actions/upload-artifact@v7
+        with:
+          name: cryptboolean-proof-seed
+          path: proof-dist/CryptBoolean-x86_64-unknown-linux-gnu.tar.gz
+          if-no-files-found: error
+          retention-days: 1
+
+  pack:
+    needs:
+      - prepare
+      - prove
+    if: github.event_name == 'push' || inputs.verify_only != true
+    strategy:
+      fail-fast: false
+      matrix:
+        runner:
+          - ubuntu-latest
+          - macos-15
+    runs-on: ${{ matrix.runner }}
+    timeout-minutes: 45
+
+    steps:
+      - uses: actions/checkout@v7
+        with:
+          ref: ${{ needs.prepare.outputs.tag }}
+
+      - name: Set up Lean and restore Mathlib cache
+        uses: leanprover/lean-action@v1
+        with:
+          auto-config: false
+          build: false
+          use-mathlib-cache: true
+          use-github-cache: false
+
+      - name: Collect the verified proof archive
+        uses: actions/download-artifact@v8
+        with:
+          name: cryptboolean-proof-seed
+          path: proof-seed
+
+      - name: Unpack the verified proof archive
+        run: |
+          set -euo pipefail
+          archive="proof-seed/CryptBoolean-x86_64-unknown-linux-gnu.tar.gz"
+          test -f "$archive"
+          lake unpack "$archive"
+
+      - name: Validate the proof archive as a dependency
+        env:
+          GH_TOKEN: ${{ github.token }}
+        run: |
+          set -euo pipefail
+          consumer_dir="$RUNNER_TEMP/cryptboolean-release-builder"
+          ./.github/scripts/prepare_release_builder.sh "$consumer_dir"
+          lake --rehash --no-build -d="$consumer_dir" build CryptBoolean
+
+      - name: Audit packed release proofs
+        run: |
+          ./.github/scripts/forbidden_tokens.sh
+          ./.github/scripts/audit_axioms.sh \
+            "$RUNNER_TEMP/cryptboolean-release-builder"
+
       - name: Pack Lake release archive
         run: |
           set -euo pipefail
@@ -137,7 +197,7 @@ jobs:
   publish:
     needs:
       - prepare
-      - build
+      - pack
     runs-on: ubuntu-latest
     timeout-minutes: 10
     permissions: