Prepare provider execution and qualify Scheme runtime

.github/actions/prepare-toolchain/action.yml

@@ -10,7 +10,7 @@ runs:
     - name: Select standard Go
       uses: actions/setup-go@924ae3a1cded613372ab5595356fb5720e22ba16 # v6
       with:
-        go-version: '1.26.1'
+        go-version: '1.27.3'
         cache: false
     - name: Select Node for Quint
       if: env.WEAVER_VERIFY_SUITE == 'check-policy'
@@ -20,3 +20,18 @@ runs:
     - name: Install Ubuntu or Darwin packages
       shell: sh
       run: go -C go run ./cmd/weaver-dev prepare-ci-tools
+    - name: Prepare the pinned Lean release
+      if: env.WEAVER_VERIFY_SUITE == 'check-policy' && runner.os == 'Linux'
+      shell: bash
+      run: bash "${{ github.action_path }}/install-lean.sh"
+    - name: Bind the Cedar solver
+      if: env.WEAVER_VERIFY_SUITE == 'check-policy'
+      shell: sh
+      run: |
+        solver=$(command -v cvc5)
+        case "$solver" in
+          /*) test -x "$solver" ;;
+          *) exit 1 ;;
+        esac
+        "$solver" --version
+        printf 'CVC5=%s\n' "$solver" >> "$GITHUB_ENV"

.github/actions/prepare-toolchain/install-lean.sh

@@ -0,0 +1,29 @@
+#!/usr/bin/env bash
+# SPDX-FileCopyrightText: 2026 hardenedlinux Linux Team and Contributors
+#
+# SPDX-License-Identifier: LGPL-2.1-or-later AND Apache-2.0
+
+set -euo pipefail
+
+read -r toolchain < dev/proofs/cedar/lean-toolchain
+[[ "$toolchain" == leanprover/lean4:v* ]]
+tag="${toolchain#*:}"
+asset_name="lean-${tag#v}-linux.tar.zst"
+tag_uri="$(jq -nr --arg tag "$tag" '$tag | @uri')"
+read -r asset_id sha256 < <(
+  curl --fail --silent --show-error --location --retry 3 \
+    "https://api.github.com/repos/leanprover/lean4/releases/tags/$tag_uri" |
+    jq -er --arg name "$asset_name" \
+      '.assets[] | select(.name == $name) | [.id, (.digest | ltrimstr("sha256:"))] | @tsv'
+)
+[[ "$asset_id" =~ ^[0-9]+$ && "$sha256" =~ ^[0-9a-f]{64}$ ]]
+archive="${RUNNER_TEMP:?}/$asset_name"
+release_root="$RUNNER_TEMP/weaver-lean"
+curl --fail --location --retry 3 --header 'Accept: application/octet-stream' \
+  --output "$archive" \
+  "https://api.github.com/repos/leanprover/lean4/releases/assets/$asset_id"
+echo "$sha256  $archive" | shasum -a 256 --check
+mkdir -p "$release_root"
+tar --zstd -xf "$archive" -C "$release_root" --strip-components=1
+elan toolchain link "$toolchain" "$release_root"
+elan run "$toolchain" lean --version

.github/actions/prepare-toolchain/sigpipe-backtrace.gdb

@@ -0,0 +1,28 @@
+# SPDX-FileCopyrightText: 2026 hardenedlinux Linux Team and Contributors
+#
+# SPDX-License-Identifier: LGPL-2.1-or-later AND Apache-2.0
+
+# Failure-only observation. Pass every signal through to the unchanged process.
+set pagination off
+set confirm off
+set debuginfod enabled off
+set print frame-arguments none
+set follow-fork-mode parent
+handle all nostop noprint pass
+handle SIGPIPE stop print pass
+set $weaver_sigpipe_events = 0
+catch signal SIGPIPE
+commands
+  silent
+  set $weaver_sigpipe_events = $weaver_sigpipe_events + 1
+  if $weaver_sigpipe_events <= 16
+    printf "WEAVER-SIGPIPE event=%d\n", $weaver_sigpipe_events
+    thread
+    bt 24
+    if $weaver_sigpipe_events == 1
+      thread apply all bt 24
+    end
+  end
+  continue
+end
+run

.github/workflows/verify-suite.yml

@@ -24,12 +24,18 @@ jobs:
   verify:
     name: ${{ inputs.label }}
     runs-on: ${{ inputs.runner }}
-    timeout-minutes: 45
+    # Full dependency preparation has no phase cutoff. Reserve room for the
+    # unchanged 37-minute Scheme suite and receipt upload after preparation.
+    timeout-minutes: ${{ inputs.suite == 'check-scheme' && 120 || 65 }}
     env:
       GOTOOLCHAIN: local
       WEAVER_VERIFY_SUITE: ${{ inputs.suite }}
+      # Gerbil std/make defaults to serial compilation without this setting.
+      GERBIL_BUILD_CORES: '4'
     steps:
       - name: Check out committed source
+        id: checkout
+        timeout-minutes: 2
         uses: actions/checkout@d23441a48e516b6c34aea4fa41551a30e30af803 # v6
         with:
           persist-credentials: false
@@ -38,38 +44,110 @@ jobs:
             /*
             !/dev/proofs/evidence/
             !/dev/specs/evidence/
+      - name: Verify tested revision
+        id: source
+        timeout-minutes: 1
+        run: |
+          checkout_sha=$(git rev-parse HEAD)
+          test "$checkout_sha" = "$GITHUB_SHA"
+          printf 'revision=%s\n' "$checkout_sha" >> "$GITHUB_OUTPUT"
       - name: Prepare deterministic toolchain
+        id: toolchain
+        timeout-minutes: 10
         uses: ./.github/actions/prepare-toolchain
       - name: Fetch locked Rust and Go dependencies
-        run: go -C go run ./cmd/weaver-dev -clean-source bootstrap-build
+        id: bootstrap_build
+        timeout-minutes: 4
+        run: go -C go run ./cmd/weaver-dev -clean-source -timeout 3m bootstrap-build
       - name: Prepare Cedar and Lean proof dependencies
+        id: bootstrap_proofs
         if: inputs.suite == 'check-policy'
-        run: go -C go run ./cmd/weaver-dev -clean-source bootstrap-proofs
+        timeout-minutes: 8
+        run: go -C go run ./cmd/weaver-dev -clean-source -timeout 7m bootstrap-proofs
       - name: Prepare published Scheme SDK
-        if: inputs.suite == 'check-scheme'
-        uses: tao3k/gerbil-scheme-rust/.github/actions/setup-gerbil@838af1ab4e6c0c8177fed176efba448c694012b5
+        id: scheme_sdk
+        if: contains(fromJSON('["check-rust", "check-go", "check-policy", "check-scheme", "bench"]'), inputs.suite)
+        timeout-minutes: 5
+        uses: tao3k/gerbil-scheme-rust/.github/actions/setup-gerbil@bfe803f597a15a3654b70a64c3a039980c31da8a
         with:
           release-root: ${{ runner.temp }}/gerbil-sdk
+      - name: Prepare macOS Scheme build watchdog
+        id: scheme_watchdog
+        if: inputs.suite == 'check-scheme' && runner.os == 'macOS'
+        timeout-minutes: 4
+        env:
+          HOMEBREW_NO_AUTO_UPDATE: '1'
+        run: |
+          brew install coreutils
+          echo "$(brew --prefix coreutils)/libexec/gnubin" >> "$GITHUB_PATH"
       - name: Install declared Scheme dependencies
+        id: scheme_dependencies
         if: inputs.suite == 'check-scheme'
         env:
           GERBIL_PATH: ${{ runner.temp }}/weaver-gerbil
-        run: gerbil deps --install
+        run: go -C go run ./cmd/weaver-dev -clean-source bootstrap-scheme
       - name: Verify declared suite
+        id: verify_suite
         if: inputs.suite != 'check-scheme'
-        run: go -C go run ./cmd/weaver-dev -clean-source "$WEAVER_VERIFY_SUITE"
+        timeout-minutes: 30
+        run: go -C go run ./cmd/weaver-dev -clean-source -timeout 28m "$WEAVER_VERIFY_SUITE"
       - name: Verify Scheme modules, Cedar FFI and streaming recovery
+        id: verify_scheme
         if: inputs.suite == 'check-scheme'
+        # The source-closure watchdog is separate. Give the suite room for
+        # its prelude and all three independently bounded native stages.
+        timeout-minutes: 37
         env:
           GERBIL_GXI: ${{ env.GERBIL_PREFIX }}/bin/gxi
           GERBIL_PATH: ${{ runner.temp }}/weaver-gerbil
-        run: go -C go run ./cmd/weaver-dev -clean-source check-scheme
-      - name: Publish latest structured result
+        run: go -C go run ./cmd/weaver-dev -clean-source -timeout 35m check-scheme
+      - name: Write verification job receipt
+        if: always()
+        timeout-minutes: 1
+        env:
+          JOB_RECEIPT: >-
+            {
+              "schema": "weaver.ci-job.v1",
+              "suite": ${{ toJSON(inputs.suite) }},
+              "runId": ${{ toJSON(github.run_id) }},
+              "runAttempt": ${{ toJSON(github.run_attempt) }},
+              "headRevision": ${{ toJSON(github.event.pull_request.head.sha || github.sha) }},
+              "expectedCheckoutRevision": ${{ toJSON(github.sha) }},
+              "checkoutRevision": ${{ toJSON(steps.source.outputs.revision || null) }},
+              "os": ${{ toJSON(runner.os) }},
+              "arch": ${{ toJSON(runner.arch) }},
+              "status": ${{ toJSON(job.status) }},
+              "schemeDependencyBudgetMinutes": null,
+              "schemeDependencyBuildCores": ${{ inputs.suite == 'check-scheme' && 4 || 'null' }},
+              "phases": {
+                "checkout": ${{ toJSON(steps.checkout.outcome || 'skipped') }},
+                "source": ${{ toJSON(steps.source.outcome || 'skipped') }},
+                "toolchain": ${{ toJSON(steps.toolchain.outcome || 'skipped') }},
+                "bootstrapBuild": ${{ toJSON(steps.bootstrap_build.outcome || 'skipped') }},
+                "bootstrapProofs": ${{ toJSON(steps.bootstrap_proofs.outcome || 'skipped') }},
+                "schemeSdk": ${{ toJSON(steps.scheme_sdk.outcome || 'skipped') }},
+                "schemeWatchdog": ${{ toJSON(steps.scheme_watchdog.outcome || 'skipped') }},
+                "schemeDependencies": ${{ toJSON(steps.scheme_dependencies.outcome || 'skipped') }},
+                "verifySuite": ${{ toJSON(steps.verify_suite.outcome || 'skipped') }},
+                "verifyScheme": ${{ toJSON(steps.verify_scheme.outcome || 'skipped') }}
+              }
+            }
+        run: |
+          mkdir -p .cache/verification
+          printf '%s\n' "$JOB_RECEIPT" > .cache/verification/ci-job.json
+      - name: Publish structured verification receipts
         if: always()
+        timeout-minutes: 2
         uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 # v4
         with:
-          name: ${{ inputs.suite }}-${{ runner.os }}-${{ runner.arch }}-${{ github.sha }}
-          path: .cache/verification/latest-*
+          name: ${{ inputs.suite }}-${{ runner.os }}-${{ runner.arch }}-${{ github.sha }}-attempt-${{ github.run_attempt }}
+          path: |
+            .cache/verification/ci-job.json
+            .cache/verification/latest-bootstrap-build.json
+            .cache/verification/latest-bootstrap-proofs.json
+            .cache/verification/latest-bootstrap-scheme.json
+            .cache/verification/latest-${{ inputs.suite }}.json
+            .cache/verification/spec/*/receipt.json
           include-hidden-files: true
-          if-no-files-found: warn
+          if-no-files-found: error
           retention-days: 7