Mnehmos · Jul 26, 2026 · Jul 26, 2026 · Jul 26, 2026 · Jul 26, 2026 · Jul 26, 2026
@@ -4,6 +4,12 @@ on:
   push:
     branches: [main]
   workflow_dispatch:
+    inputs:
+      pilot_c:
+        description: Run the exact BH Pilot C project publication lifecycle
+        required: false
+        default: false
+        type: boolean
 
 permissions:
   contents: read
@@ -15,7 +21,9 @@ concurrency:
 jobs:
   boundary:
     name: Attested publication candidate boundary
-    if: github.ref == 'refs/heads/main'
+    if: >-
+      github.ref == 'refs/heads/main' &&
+      (github.event_name != 'workflow_dispatch' || inputs.pilot_c != true)
     runs-on: ubuntu-latest
     timeout-minutes: 20
     outputs:
@@ -265,7 +273,9 @@ jobs:
   comparator:
     name: Protected official Comparator execution
     needs: boundary
-    if: github.ref == 'refs/heads/main'
+    if: >-
+      github.ref == 'refs/heads/main' &&
+      (github.event_name != 'workflow_dispatch' || inputs.pilot_c != true)
     runs-on: ubuntu-latest
     timeout-minutes: 45
     permissions:
@@ -396,3 +406,266 @@ jobs:
             ${{ runner.temp }}/comparator-run-attestation-verification/
             ${{ steps.attest_comparator.outputs.bundle-path }}
             ${{ runner.temp }}/comparator-authority-state/comparator-authority-output/
+
+  pilot_c:
+    name: Protected BH Pilot C project lifecycle
+    if: >-
+      github.ref == 'refs/heads/main' &&
+      github.event_name == 'workflow_dispatch' &&
+      inputs.pilot_c == true
+    runs-on: ubuntu-latest
+    timeout-minutes: 360
+    permissions:
+      contents: read
+      id-token: write
+      attestations: write
+      artifact-metadata: write
+    steps:
+      - name: Check out exact source without credentials
+        uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683
+        with:
+          persist-credentials: false
+      - name: Require protected GitHub-hosted main context
+        shell: bash
+        run: |
+          set -euo pipefail
+          [[ "${GITHUB_REF_PROTECTED:-}" == "true" \
+            && "${GITHUB_REF}" == "refs/heads/main" \
+            && "${RUNNER_ENVIRONMENT}" == "github-hosted" ]] || {
+            echo "Pilot C publication requires protected main on a GitHub-hosted runner" >&2
+            exit 65
+          }
+      - name: Install exact Lean RC1 toolchain
+        shell: bash
+        run: |
+          set -euo pipefail
+          archive="${RUNNER_TEMP}/elan.tar.gz"
+          curl --fail --location --proto '=https' --tlsv1.2 \
+            --output "${archive}" \
+            https://github.com/leanprover/elan/releases/download/v4.2.3/elan-x86_64-unknown-linux-gnu.tar.gz
+          echo "df0b2b3a439961ffcbb3985214365ffe40f49bc871df04dff268c7d8e21ca8b2  ${archive}" \
+            | sha256sum --check --strict
+          tar --extract --gzip --file "${archive}" --directory "${RUNNER_TEMP}"
+          "${RUNNER_TEMP}/elan-init" -y --default-toolchain none --no-modify-path
+          echo "${HOME}/.elan/bin" >> "${GITHUB_PATH}"
+          "${HOME}/.elan/bin/elan" toolchain install leanprover/lean4:v4.32.0-rc1
+      - name: Install publication isolation control
+        shell: bash
+        run: |
+          set -euo pipefail
+          sudo apt-get update
+          sudo apt-get install --yes --no-install-recommends bubblewrap jq util-linux
+          /usr/bin/bwrap --version
+          /usr/bin/prlimit --version
+          jq --version
+      - name: Add bounded swap for the exact serial BH build
+        shell: bash
+        run: |
+          set -euo pipefail
+          sudo fallocate -l 14G /mnt/mathos-pilot-c.swap
+          sudo chmod 600 /mnt/mathos-pilot-c.swap
+          sudo mkswap /mnt/mathos-pilot-c.swap
+          sudo swapon /mnt/mathos-pilot-c.swap
+          swapon --show
+      - name: Build the reviewed Pilot C generator
+        shell: bash
+        run: cargo build --locked --bin mcl
+      - name: Install pinned attestation verifier
+        shell: bash
+        run: |
+          set -euo pipefail
+          version="2.96.0"
+          archive="${RUNNER_TEMP}/gh_${version}_linux_amd64.tar.gz"
+          curl --fail --location --proto '=https' --tlsv1.2 \
+            --output "${archive}" \
+            "https://github.com/cli/cli/releases/download/v${version}/gh_${version}_linux_amd64.tar.gz"
+          echo "83d5c2ccad5498f58bf6368acb1ab32588cf43ab3a4b1c301bf36328b1c8bd60  ${archive}" \
+            | sha256sum --check --strict
+          tar --extract --gzip --no-same-owner --file "${archive}" --directory "${RUNNER_TEMP}"
+          gh_bin="${RUNNER_TEMP}/gh_${version}_linux_amd64/bin/gh"
+          echo "56b8bbbb27b066ecb33dbef9a256dc9d1314adaeff0908a752feba6c34053b40  ${gh_bin}" \
+            | sha256sum --check --strict
+          echo "${RUNNER_TEMP}/gh_${version}_linux_amd64/bin" >> "${GITHUB_PATH}"
+      - name: Build and validate the exact protected Pilot C closure
+        shell: bash
+        env:
+          PUBLICATION_CONTEXT_MODE: protected-main
+          PUBLICATION_REPOSITORY: ${{ github.repository }}
+          PUBLICATION_WORKFLOW_PATH: .github/workflows/publication.yml
+          PUBLICATION_WORKFLOW_REF: ${{ github.workflow_ref }}
+          PUBLICATION_SOURCE_REF: ${{ github.ref }}
+          PUBLICATION_SOURCE_COMMIT_SHA: ${{ github.sha }}
+          PUBLICATION_WORKFLOW_RUN_ID: ${{ github.run_id }}
+          PUBLICATION_WORKFLOW_RUN_ATTEMPT: ${{ github.run_attempt }}
+          PUBLICATION_RUNNER_ENVIRONMENT: github_hosted
+        run: |
+          set -euo pipefail
+          export PUBLICATION_SOURCE_TREE_SHA
+          PUBLICATION_SOURCE_TREE_SHA="$(git rev-parse 'HEAD^{tree}')"
+          bash scripts/publication-candidate.sh \
+            "${RUNNER_TEMP}/publication-pilot-c" \
+            pilot-c
+      - name: Attest exact Pilot C publication report
+        id: attest_pilot_c
+        uses: actions/attest@59d89421af93a897026c735860bf21b6eb4f7b26
+        with:
+          subject-path: ${{ runner.temp }}/publication-pilot-c/publication-report.json
+      - name: Verify exact Pilot C attestation
+        shell: bash
+        env:
+          PUBLICATION_GH_BIN: ${{ runner.temp }}/gh_2.96.0_linux_amd64/bin/gh
+          PILOT_C_BUNDLE_PATH: ${{ steps.attest_pilot_c.outputs.bundle-path }}
+        run: |
+          scripts/publication-attestation-verify.sh \
+            "${RUNNER_TEMP}/publication-pilot-c/publication-report.json" \
+            "${PILOT_C_BUNDLE_PATH}" \
+            "${RUNNER_TEMP}/publication-pilot-c-attestation-verification"
+      - name: Stage, ingest, and promote exact Pilot C authority and fidelity
+        shell: bash
+        env:
+          PILOT_C_BUNDLE_PATH: ${{ steps.attest_pilot_c.outputs.bundle-path }}
+        run: |
+          scripts/publication-ingest.sh \
+            "${RUNNER_TEMP}/publication-pilot-c" \
+            "${PILOT_C_BUNDLE_PATH}" \
+            "${RUNNER_TEMP}/publication-pilot-c/authority-ingestion"
+      - name: Snapshot exact Pilot C state and evidence for transfer
+        if: always()
+        shell: bash
+        env:
+          PRIOR_JOB_STATUS: ${{ job.status }}
+          PILOT_C_BUNDLE_PATH: ${{ steps.attest_pilot_c.outputs.bundle-path }}
+        run: |
+          set -euo pipefail
+          snapshot="${RUNNER_TEMP}/publication-pilot-c-transfer"
+          mkdir -- "$snapshot"
+          if [[ -d "${RUNNER_TEMP}/publication-pilot-c" ]]; then
+            cp -a -- "${RUNNER_TEMP}/publication-pilot-c" "$snapshot/publication-pilot-c"
+          fi
+          if [[ -d "${RUNNER_TEMP}/publication-pilot-c-attestation-verification" ]]; then
+            cp -a -- \
+              "${RUNNER_TEMP}/publication-pilot-c-attestation-verification" \
+              "$snapshot/publication-pilot-c-attestation-verification"
+          fi
+          if [[ -n "${PILOT_C_BUNDLE_PATH:-}" && -f "${PILOT_C_BUNDLE_PATH}" ]]; then
+            cp -- "${PILOT_C_BUNDLE_PATH}" "$snapshot/publication-attestation.bundle.json"
+          fi
+          if [[ "$PRIOR_JOB_STATUS" == "success" ]]; then
+            [[ -f "$snapshot/publication-pilot-c/.mcl/state.sqlite3" \
+                && -f "$snapshot/publication-pilot-c/mcl.toml" \
+                && -d "$snapshot/publication-pilot-c/authority-ingestion" \
+                && -f "$snapshot/publication-attestation.bundle.json" ]] || {
+              echo "successful Pilot C transfer snapshot is incomplete" >&2
+              exit 71
+            }
+          fi
+      - name: Retain and transfer Pilot C closure, authority, diagnostics, and attestation
        if: always()
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
+        with:
+          name: publication-pilot-c-${{ github.sha }}
+          if-no-files-found: error
+          include-hidden-files: true
+          retention-days: 90
+          compression-level: 6
+          path: ${{ runner.temp }}/publication-pilot-c-transfer/
+
+  pilot_c_release:
+    name: Protected BH Pilot C database-free release replay
+    needs: pilot_c
+    if: >-
+      needs.pilot_c.result == 'success' &&
+      github.ref == 'refs/heads/main' &&
+      github.event_name == 'workflow_dispatch' &&
+      inputs.pilot_c == true
+    runs-on: ubuntu-latest
+    timeout-minutes: 360
+    permissions:
+      actions: read
+      contents: read
+    steps:
+      - name: Check out exact source without credentials
+        uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683
+        with:
+          persist-credentials: false
+      - name: Require protected GitHub-hosted main context
+        shell: bash
+        run: |
+          set -euo pipefail
+          [[ "${GITHUB_REF_PROTECTED:-}" == "true" \
+            && "${GITHUB_REF}" == "refs/heads/main" \
+            && "${RUNNER_ENVIRONMENT}" == "github-hosted" ]] || {
+            echo "Pilot C release replay requires protected main on a GitHub-hosted runner" >&2
+            exit 65
+          }
+      - name: Install exact Lean RC1 toolchain
+        shell: bash
+        run: |
+          set -euo pipefail
+          archive="${RUNNER_TEMP}/elan.tar.gz"
+          curl --fail --location --proto '=https' --tlsv1.2 \
+            --output "${archive}" \
+            https://github.com/leanprover/elan/releases/download/v4.2.3/elan-x86_64-unknown-linux-gnu.tar.gz
+          echo "df0b2b3a439961ffcbb3985214365ffe40f49bc871df04dff268c7d8e21ca8b2  ${archive}" \
+            | sha256sum --check --strict
+          tar --extract --gzip --file "${archive}" --directory "${RUNNER_TEMP}"
+          "${RUNNER_TEMP}/elan-init" -y --default-toolchain none --no-modify-path
+          echo "${HOME}/.elan/bin" >> "${GITHUB_PATH}"
+          "${HOME}/.elan/bin/elan" toolchain install leanprover/lean4:v4.32.0-rc1
+      - name: Install publication isolation control
+        shell: bash
+        run: |
+          set -euo pipefail
+          sudo apt-get update
+          sudo apt-get install --yes --no-install-recommends bubblewrap jq util-linux
+          /usr/bin/bwrap --version
+          /usr/bin/prlimit --version
+          jq --version
+      - name: Add bounded swap for the exact serial BH replay
+        shell: bash
+        run: |
+          set -euo pipefail
+          sudo fallocate -l 14G /mnt/mathos-pilot-c-release.swap
+          sudo chmod 600 /mnt/mathos-pilot-c-release.swap
+          sudo mkswap /mnt/mathos-pilot-c-release.swap
+          sudo swapon /mnt/mathos-pilot-c-release.swap
+          swapon --show
+      - name: Build the reviewed database-free release verifier
+        shell: bash
+        run: cargo build --locked --bin mcl
+      - name: Download exact same-run Pilot C authority state
+        uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093
+        with:
+          name: publication-pilot-c-${{ github.sha }}
+          path: ${{ runner.temp }}/pilot-c-transfer
+      - name: Build and verify private Pilot C release and MathCorpus/MCIP export without SQLite
+        shell: bash
+        run: |
+          set -euo pipefail
+          state_root="${RUNNER_TEMP}/pilot-c-transfer/publication-pilot-c"
+          [[ -f "${state_root}/.mcl/state.sqlite3" \
+              && -f "${state_root}/mcl.toml" \
+              && -d "${state_root}/authority-ingestion" ]] || {
+            echo "downloaded Pilot C authority state is incomplete" >&2
+            exit 71
+          }
+          bash scripts/release-pilot-c.sh \
+            "${state_root}" \
+            "${state_root}" \
+            "${state_root}/authority-ingestion" \
+            "${RUNNER_TEMP}/pilot-c-portable-release" \
+            "${RUNNER_TEMP}/pilot-c-mathcorpus-mcip-export"
+      - name: Retain Pilot C release, export, database-free copies, and replay evidence
+        if: always()
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
+        with:
+          name: publication-pilot-c-release-${{ github.sha }}
+          if-no-files-found: error
+          retention-days: 90
+          compression-level: 6
+          path: |
+            ${{ runner.temp }}/pilot-c-transfer/publication-pilot-c/pilot-c-release-evidence/
+            ${{ runner.temp }}/pilot-c-portable-release/
+            ${{ runner.temp }}/pilot-c-portable-release-clean-copy/
+            ${{ runner.temp }}/pilot-c-mathcorpus-mcip-export/
+            ${{ runner.temp }}/pilot-c-mathcorpus-mcip-export-clean-copy/
@@ -16,6 +16,7 @@ serde = { version = "1", features = ["derive"] }
 serde_json = "1"
 serde_json_canonicalizer = "0.3.2"
 sha2 = "0.10"
+tar = "0.4"
 tempfile = "3"
 toml = "0.9"
 tokio = { version = "1", features = ["io-std", "macros", "rt-multi-thread"] }

@@ -2,7 +2,7 @@
 
 Date: 2026-07-19
 
-Status: accepted
+Status: accepted; publication-profile execution added by ADR-0019
 
 ## Context
 
@@ -22,7 +22,10 @@ Wall-clock time and combined retained output are bounded. The worker kills and r
 
 Every report from this boundary has `authoritative: false`. An `elaborated` classification means only that the selected Lean executable accepted the controlled driver in the observed local environment. A `rejected` classification is an execution result, not a source-claim refutation. Operational job success means the attempt completed and its report was committed. It does not mean the theorem or source claim succeeded.
 
-The local report states that memory enforcement and network isolation are false. The local worker refuses publication-profile environments. Publication evidence requires a later protected Linux CI boundary with dependency closure, network isolation, proof-closure scans, axiom audit, and retained reports.
+The local report states that memory enforcement and network isolation are false. This decision did
+not implement publication-profile execution. ADR-0019 later adds a separate Linux-only
+publication branch to the same typed worker surface; it does not strengthen or reinterpret local
+reports.
 
 ## Consequences